Nuprl Definition : dl-prop-atoms

dl-prop-atoms() ==
  dl-ind(
         dl-aprog(a)⇒ [];
         dl-comp(alpha,beta)⇒ L1,L2.L1 @ L2;
         dl-choose(alpha,beta)⇒ L1,L2.L1 @ L2;
         dl-iterate(a)⇒ L.L;
         dl-test(phi)⇒ L.L;
         dl-aprop(a)⇒ [a];
         dl-false⇒ [];
         dl-implies(phi,psi)⇒ L1,L2.L1 @ L2;
         dl-and(phi,psi)⇒ L1,L2.L1 @ L2;
         dl-or(phi,psi)⇒ L1,L2.L1 @ L2;
         dl-box(alpha,phi)⇒ L1,L2.L1 @ L2;
         dl-diamond(alpha,phi)⇒ L1,L2.L1 @ L2)

Definitions occuring in Statement : dl-ind: dl-ind, append: as @ bs, cons: [a / b], nil: []
Definitions occuring in definition : dl-ind: dl-ind, cons: [a / b], nil: [], append: as @ bs
FDL editor aliases : dl-prop-atoms

Latex:
dl-prop-atoms() == dl-ind( dl-aprog(a){}\mRightarrow{} []; dl-comp(alpha,beta){}\mRightarrow{} L1,L2.L1 @ L2; dl-choose(alpha,beta){}\mRightarrow{} L1,L2.L1 @ L2; dl-iterate(a){}\mRightarrow{} L.L; dl-test(phi){}\mRightarrow{} L.L; dl-aprop(a){}\mRightarrow{} [a]; dl-false{}\mRightarrow{} []; dl-implies(phi,psi){}\mRightarrow{} L1,L2.L1 @ L2; dl-and(phi,psi){}\mRightarrow{} L1,L2.L1 @ L2; dl-or(phi,psi){}\mRightarrow{} L1,L2.L1 @ L2; dl-box(alpha,phi){}\mRightarrow{} L1,L2.L1 @ L2; dl-diamond(alpha,phi){}\mRightarrow{} L1,L2.L1 @ L2) Date html generated: 2019_10_15-AM-11_43_51 Last ObjectModification: 2019_03_26-AM-11_28_20 Theory : dynamic!logic Home Index