Nuprl Definition : dl-localT

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

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

Latex:
localT == dl-ind( dl-aprog(a){}\mRightarrow{} []; dl-comp(alpha,beta){}\mRightarrow{} L1,L2.[]; dl-choose(alpha,beta){}\mRightarrow{} L1,L2.[]; dl-iterate(a){}\mRightarrow{} L.[]; dl-test(phi){}\mRightarrow{} L.[]; dl-aprop(a){}\mRightarrow{} []; dl-false{}\mRightarrow{} [0]; dl-implies(phi,psi){}\mRightarrow{} l1,l2.[]; dl-and(phi,psi){}\mRightarrow{} l1,l2.l1 @ l2; dl-or(phi,psi){}\mRightarrow{} l1,l2.[]; dl-box(alpha,phi){}\mRightarrow{} L1,L2.[]; dl-diamond(alpha,phi){}\mRightarrow{} L1,L2.[]) Date html generated: 2019_10_16-AM-11_24_21 Last ObjectModification: 2019_05_15-AM-10_10_28 Theory : dynamic!logic Home Index