Nuprl Definition : dl-localF

localF ==
  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)⇒ [atm(a)];
         dl-false⇒ [0];
         dl-implies(phi,psi)⇒ l1,l2.[];
         dl-and(phi,psi)⇒ l1,l2.[phi] @ [psi];
         dl-or(phi,psi)⇒ l1,l2.[phi] @ [psi];
         dl-box(alpha,phi)⇒ L1,L2.[];
         dl-diamond(alpha,phi)⇒ L1,L2.[])

Definitions occuring in Statement : dl-ind: dl-ind, dl-false: 0, dl-aprop: atm(x), append: as @ bs, cons: [a / b], nil: []
Definitions occuring in definition : dl-ind: dl-ind, dl-aprop: atm(x), dl-false: 0, append: as @ bs, cons: [a / b], nil: []
FDL editor aliases : dl-localF

Latex:
localF == 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{} [atm(a)]; dl-false{}\mRightarrow{} [0]; dl-implies(phi,psi){}\mRightarrow{} l1,l2.[]; dl-and(phi,psi){}\mRightarrow{} l1,l2.[phi] @ [psi]; dl-or(phi,psi){}\mRightarrow{} l1,l2.[phi] @ [psi]; dl-box(alpha,phi){}\mRightarrow{} L1,L2.[]; dl-diamond(alpha,phi){}\mRightarrow{} L1,L2.[]) Date html generated: 2020_05_20-AM-09_01_56 Last ObjectModification: 2019_11_27-PM-02_27_30 Theory : dynamic!logic Home Index