* Some simple examples of parameterised propositions.
* Parameterising on a modality:
prop A(a) = [a]F;
prop A;
cp (c.0, A(b));
cp (b.0, A(b));
cp (b.0, A({a,b}));
cp (a.0, A({a,b}));
set Set = {a,b};
cp (c.0, A(Set));
cp (b.0, A(Set));
* Actual parameters can be negative modalities:
cp (b.0, A(-Set));
cp (a.0, A(-Set));
cp (a.0+c.0, A(-Set));
cp (b.0, A(-));
cp (b.0, A(-b));
cp (b.0, A(-a));
cp (b.0, A({-a,b})); * this is how the CWB represents negative action lists...
cp (b.0, A(-{a,b})); * this synonym is provided for user convenience.
* Parameterising on a proposition:
prop B(C) = [a]C;
prop P(Q) = <a>Q;
prop B;
cp (a.0,B(F));
cp (b.0,B(F));
cp (a.0,P(F));
cp (b.0,P(F));
cp (a.0,B(T|F));
cp (b.0,B(T|F));
cp (a.0,P(T|F));
cp (b.0,P(T|F));

prop D = T|F;
cp (a.0,B(D));
cp (b.0,B(D));
cp (a.0,P(D));
cp (b.0,P(D));

prop E = B(D);
prop G = P(D); * remember not to use F as a user-defined proposition name!
cp (a.0,E);
cp (b.0,E);
cp (a.0,G);
cp (b.0,G);