Nuprl Definition : dlo-le

dlo-le() ==
  dl-ind(
         dl-aprog(x)⇒ λa.dlo_eq(prog(atm(x));a);
         dl-comp(b1,b2)⇒ l1,l2.λa.(((l1 a) ∨b(l2 a)) ∨bdlo_eq(prog((b1;b2));a));
         dl-choose(b1,b2)⇒ l1,l2.λa.(((l1 a) ∨b(l2 a)) ∨bdlo_eq(prog(b1 ⋃ b2);a));
         dl-iterate(b1)⇒ l1.λa.((l1 a) ∨bdlo_eq(prog((b1)*);a));
         dl-test(b1)⇒ l1.λa.((l1 a) ∨bdlo_eq(prog((b1)?);a));
         dl-aprop(x)⇒ λa.dlo_eq(prop(atm(x));a);
         dl-false⇒ λa.dlo_eq(prop(0);a);
         dl-implies(b1,b2)⇒ l1,l2.λa.(((l1 a) ∨b(l2 a)) ∨bdlo_eq(prop(b1 ⇒ b2);a));
         dl-and(b1,b2)⇒ l1,l2.λa.(((l1 a) ∨b(l2 a)) ∨bdlo_eq(prop(b1 ∧ b2);a));
         dl-or(b1,b2)⇒ l1,l2.λa.(((l1 a) ∨b(l2 a)) ∨bdlo_eq(prop(b1 ∨ b2);a));
         dl-box(b1,b2)⇒ l1,l2.λa.(((l1 a) ∨b(l2 a)) ∨bdlo_eq(prop([b1] b2);a));
         dl-diamond(b1,b2)⇒ l1,l2.λa.(((l1 a) ∨b(l2 a)) ∨bdlo_eq(prop(<b1> b2);a))) 


Definitions occuring in Statement :  dlo_eq: dlo_eq(a;b),  dl-ind: dl-ind,  dl-diamond: <x1> x,  dl-box: [x1] x,  dl-or: x1 ∨ x,  dl-and: x1 ∧ x,  dl-implies: x1 ⇒ x,  dl-false: 0,  dl-aprop: atm(x),  dl-test: (x)?,  dl-iterate: (x)*,  dl-choose: x1 ⋃ x,  dl-comp: (x1;x),  dl-aprog: atm(x),  dl-prop-obj: prop(x),  dl-prog-obj: prog(x),  bor: p ∨bq,  apply: f a,  lambda: λx.A[x]
Definitions occuring in definition :  dl-ind: dl-ind,  dl-aprog: atm(x),  dl-comp: (x1;x),  dl-choose: x1 ⋃ x,  dl-iterate: (x)*,  dl-prog-obj: prog(x),  dl-test: (x)?,  dl-aprop: atm(x),  dl-false: 0,  dl-implies: x1 ⇒ x,  dl-and: x1 ∧ x,  dl-or: x1 ∨ x,  dl-box: [x1] x,  lambda: λx.A[x],  bor: p ∨bq,  apply: f a,  dlo_eq: dlo_eq(a;b),  dl-prop-obj: prop(x),  dl-diamond: <x1> x
FDL editor aliases :  dlo-le
Latex:
dlo-le()  ==
    dl-ind(
                  dl-aprog(x){}\mRightarrow{}  \mlambda{}a.dlo\_eq(prog(atm(x));a);
                  dl-comp(b1,b2){}\mRightarrow{}  l1,l2.\mlambda{}a.(((l1  a)  \mvee{}\msubb{}(l2  a))  \mvee{}\msubb{}dlo\_eq(prog((b1;b2));a));
                  dl-choose(b1,b2){}\mRightarrow{}  l1,l2.\mlambda{}a.(((l1  a)  \mvee{}\msubb{}(l2  a))  \mvee{}\msubb{}dlo\_eq(prog(b1  \mcup{}  b2);a));
                  dl-iterate(b1){}\mRightarrow{}  l1.\mlambda{}a.((l1  a)  \mvee{}\msubb{}dlo\_eq(prog((b1)*);a));
                  dl-test(b1){}\mRightarrow{}  l1.\mlambda{}a.((l1  a)  \mvee{}\msubb{}dlo\_eq(prog((b1)?);a));
                  dl-aprop(x){}\mRightarrow{}  \mlambda{}a.dlo\_eq(prop(atm(x));a);
                  dl-false{}\mRightarrow{}  \mlambda{}a.dlo\_eq(prop(0);a);
                  dl-implies(b1,b2){}\mRightarrow{}  l1,l2.\mlambda{}a.(((l1  a)  \mvee{}\msubb{}(l2  a))  \mvee{}\msubb{}dlo\_eq(prop(b1  {}\mRightarrow{}  b2);a));
                  dl-and(b1,b2){}\mRightarrow{}  l1,l2.\mlambda{}a.(((l1  a)  \mvee{}\msubb{}(l2  a))  \mvee{}\msubb{}dlo\_eq(prop(b1  \mwedge{}  b2);a));
                  dl-or(b1,b2){}\mRightarrow{}  l1,l2.\mlambda{}a.(((l1  a)  \mvee{}\msubb{}(l2  a))  \mvee{}\msubb{}dlo\_eq(prop(b1  \mvee{}  b2);a));
                  dl-box(b1,b2){}\mRightarrow{}  l1,l2.\mlambda{}a.(((l1  a)  \mvee{}\msubb{}(l2  a))  \mvee{}\msubb{}dlo\_eq(prop([b1]  b2);a));
                  dl-diamond(b1,b2){}\mRightarrow{}  l1,l2.\mlambda{}a.(((l1  a)  \mvee{}\msubb{}(l2  a))  \mvee{}\msubb{}dlo\_eq(prop(<b1>  b2);a))) 


Date html generated: 2019_10_15-AM-11_43_10
Last ObjectModification: 2019_04_11-PM-01_53_30

Theory : dynamic!logic


Home Index