Nuprl Definition : dlo-eq

dlo-eq() ==
  dl-ind(
         dl-aprog(x)⇒ λa.(dl-kind(a) =a "prog" ∧b dl-aprog?(dl-obj-prog(a)) ∧b (dl-aprog-1(dl-obj-prog(a)) =z x));
         dl-comp(b1,b2)⇒ l1,l2.λa.(dl-kind(a) =a "prog"
                                   ∧b dl-comp?(dl-obj-prog(a))
                                   ∧b (l1 prog(dl-comp-1(dl-obj-prog(a))))
                                   ∧b (l2 prog(dl-comp-2(dl-obj-prog(a)))));
         dl-choose(b1,b2)⇒ l1,l2.λa.(dl-kind(a) =a "prog"
                                     ∧b dl-choose?(dl-obj-prog(a))
                                     ∧b (l1 prog(dl-choose-1(dl-obj-prog(a))))
                                     ∧b (l2 prog(dl-choose-2(dl-obj-prog(a)))));
         dl-iterate(b1)⇒ l1.λa.(dl-kind(a) =a "prog"
                                ∧b dl-iterate?(dl-obj-prog(a))
                                ∧b (l1 prog(dl-iterate-1(dl-obj-prog(a)))));
         dl-test(phi)⇒ l1.λa.(dl-kind(a) =a "prog"
                              ∧b dl-test?(dl-obj-prog(a))
                              ∧b (l1 prop(dl-test-1(dl-obj-prog(a)))));
         dl-aprop(x)⇒ λa.(dl-kind(a) =a "prop" ∧b dl-aprop?(dl-obj-prop(a)) ∧b (dl-aprop-1(dl-obj-prop(a)) =z x));
         dl-false⇒ λa.(dl-kind(a) =a "prop" ∧b dl-false?(dl-obj-prop(a)));
         dl-implies(p,q)⇒ l1,l2.λa.(dl-kind(a) =a "prop"
                                    ∧b dl-implies?(dl-obj-prop(a))
                                    ∧b (l1 prop(dl-implies-1(dl-obj-prop(a))))
                                    ∧b (l2 prop(dl-implies-2(dl-obj-prop(a)))));
         dl-and(p,q)⇒ l1,l2.λa.(dl-kind(a) =a "prop"
                                ∧b dl-and?(dl-obj-prop(a))
                                ∧b (l1 prop(dl-and-1(dl-obj-prop(a))))
                                ∧b (l2 prop(dl-and-2(dl-obj-prop(a)))));
         dl-or(p,q)⇒ l1,l2.λa.(dl-kind(a) =a "prop"
                               ∧b dl-or?(dl-obj-prop(a))
                               ∧b (l1 prop(dl-or-1(dl-obj-prop(a))))
                               ∧b (l2 prop(dl-or-2(dl-obj-prop(a)))));
         dl-box(alpha,phi)⇒ l1,l2.λa.(dl-kind(a) =a "prop"
                                      ∧b dl-box?(dl-obj-prop(a))
                                      ∧b (l1 prog(dl-box-1(dl-obj-prop(a))))
                                      ∧b (l2 prop(dl-box-2(dl-obj-prop(a)))));
         dl-diamond(alpha,phi)⇒ l1,l2.λa.(dl-kind(a) =a "prop"
                                          ∧b dl-diamond?(dl-obj-prop(a))
                                          ∧b (l1 prog(dl-diamond-1(dl-obj-prop(a))))
                                          ∧b (l2 prop(dl-diamond-2(dl-obj-prop(a)))))) 


Definitions occuring in Statement :  dl-obj-prop: dl-obj-prop(x),  dl-obj-prog: dl-obj-prog(x),  dl-ind: dl-ind,  dl-diamond-2: dl-diamond-2(x),  dl-diamond-1: dl-diamond-1(x),  dl-box-2: dl-box-2(x),  dl-box-1: dl-box-1(x),  dl-or-2: dl-or-2(x),  dl-or-1: dl-or-1(x),  dl-and-2: dl-and-2(x),  dl-and-1: dl-and-1(x),  dl-implies-2: dl-implies-2(x),  dl-implies-1: dl-implies-1(x),  dl-aprop-1: dl-aprop-1(x),  dl-test-1: dl-test-1(x),  dl-iterate-1: dl-iterate-1(x),  dl-choose-2: dl-choose-2(x),  dl-choose-1: dl-choose-1(x),  dl-comp-2: dl-comp-2(x),  dl-comp-1: dl-comp-1(x),  dl-aprog-1: dl-aprog-1(x),  dl-diamond?: dl-diamond?(x),  dl-box?: dl-box?(x),  dl-or?: dl-or?(x),  dl-and?: dl-and?(x),  dl-implies?: dl-implies?(x),  dl-false?: dl-false?(x),  dl-aprop?: dl-aprop?(x),  dl-test?: dl-test?(x),  dl-iterate?: dl-iterate?(x),  dl-choose?: dl-choose?(x),  dl-comp?: dl-comp?(x),  dl-aprog?: dl-aprog?(x),  dl-kind: dl-kind(d),  dl-prop-obj: prop(x),  dl-prog-obj: prog(x),  band: p ∧b q,  eq_atom: x =a y,  eq_int: (i =z j),  apply: f a,  lambda: λx.A[x],  token: "$token"
Definitions occuring in definition :  dl-obj-prop: dl-obj-prop(x),  dl-implies-1: dl-implies-1(x),  dl-prop-obj: prop(x),  apply: f a,  band: p ∧b q,  dl-implies?: dl-implies?(x),  token: "$token",  dl-kind: dl-kind(d),  eq_atom: x =a y,  lambda: λx.A[x],  dl-false?: dl-false?(x),  dl-aprop-1: dl-aprop-1(x),  eq_int: (i =z j),  dl-aprop?: dl-aprop?(x),  dl-obj-prog: dl-obj-prog(x),  dl-test-1: dl-test-1(x),  dl-test?: dl-test?(x),  dl-iterate-1: dl-iterate-1(x),  dl-prog-obj: prog(x),  dl-iterate?: dl-iterate?(x),  dl-choose-2: dl-choose-2(x),  dl-choose-1: dl-choose-1(x),  dl-choose?: dl-choose?(x),  dl-comp-2: dl-comp-2(x),  dl-comp-1: dl-comp-1(x),  dl-comp?: dl-comp?(x),  dl-aprog-1: dl-aprog-1(x),  dl-aprog?: dl-aprog?(x),  dl-ind: dl-ind,  dl-implies-2: dl-implies-2(x),  dl-and?: dl-and?(x),  dl-and-1: dl-and-1(x),  dl-and-2: dl-and-2(x),  dl-or?: dl-or?(x),  dl-or-1: dl-or-1(x),  dl-or-2: dl-or-2(x),  dl-box?: dl-box?(x),  dl-box-1: dl-box-1(x),  dl-box-2: dl-box-2(x),  dl-diamond?: dl-diamond?(x),  dl-diamond-1: dl-diamond-1(x),  dl-diamond-2: dl-diamond-2(x)
FDL editor aliases :  dlo-eq
Latex:
dlo-eq()  ==
    dl-ind(
                  dl-aprog(x){}\mRightarrow{}  \mlambda{}a.(dl-kind(a)  =a  "prog"
                                                    \mwedge{}\msubb{}  dl-aprog?(dl-obj-prog(a))
                                                    \mwedge{}\msubb{}  (dl-aprog-1(dl-obj-prog(a))  =\msubz{}  x));
                  dl-comp(b1,b2){}\mRightarrow{}  l1,l2.\mlambda{}a.(dl-kind(a)  =a  "prog"
                                                                      \mwedge{}\msubb{}  dl-comp?(dl-obj-prog(a))
                                                                      \mwedge{}\msubb{}  (l1  prog(dl-comp-1(dl-obj-prog(a))))
                                                                      \mwedge{}\msubb{}  (l2  prog(dl-comp-2(dl-obj-prog(a)))));
                  dl-choose(b1,b2){}\mRightarrow{}  l1,l2.\mlambda{}a.(dl-kind(a)  =a  "prog"
                                                                          \mwedge{}\msubb{}  dl-choose?(dl-obj-prog(a))
                                                                          \mwedge{}\msubb{}  (l1  prog(dl-choose-1(dl-obj-prog(a))))
                                                                          \mwedge{}\msubb{}  (l2  prog(dl-choose-2(dl-obj-prog(a)))));
                  dl-iterate(b1){}\mRightarrow{}  l1.\mlambda{}a.(dl-kind(a)  =a  "prog"
                                                                \mwedge{}\msubb{}  dl-iterate?(dl-obj-prog(a))
                                                                \mwedge{}\msubb{}  (l1  prog(dl-iterate-1(dl-obj-prog(a)))));
                  dl-test(phi){}\mRightarrow{}  l1.\mlambda{}a.(dl-kind(a)  =a  "prog"
                                                            \mwedge{}\msubb{}  dl-test?(dl-obj-prog(a))
                                                            \mwedge{}\msubb{}  (l1  prop(dl-test-1(dl-obj-prog(a)))));
                  dl-aprop(x){}\mRightarrow{}  \mlambda{}a.(dl-kind(a)  =a  "prop"
                                                    \mwedge{}\msubb{}  dl-aprop?(dl-obj-prop(a))
                                                    \mwedge{}\msubb{}  (dl-aprop-1(dl-obj-prop(a))  =\msubz{}  x));
                  dl-false{}\mRightarrow{}  \mlambda{}a.(dl-kind(a)  =a  "prop"  \mwedge{}\msubb{}  dl-false?(dl-obj-prop(a)));
                  dl-implies(p,q){}\mRightarrow{}  l1,l2.\mlambda{}a.(dl-kind(a)  =a  "prop"
                                                                        \mwedge{}\msubb{}  dl-implies?(dl-obj-prop(a))
                                                                        \mwedge{}\msubb{}  (l1  prop(dl-implies-1(dl-obj-prop(a))))
                                                                        \mwedge{}\msubb{}  (l2  prop(dl-implies-2(dl-obj-prop(a)))));
                  dl-and(p,q){}\mRightarrow{}  l1,l2.\mlambda{}a.(dl-kind(a)  =a  "prop"
                                                                \mwedge{}\msubb{}  dl-and?(dl-obj-prop(a))
                                                                \mwedge{}\msubb{}  (l1  prop(dl-and-1(dl-obj-prop(a))))
                                                                \mwedge{}\msubb{}  (l2  prop(dl-and-2(dl-obj-prop(a)))));
                  dl-or(p,q){}\mRightarrow{}  l1,l2.\mlambda{}a.(dl-kind(a)  =a  "prop"
                                                              \mwedge{}\msubb{}  dl-or?(dl-obj-prop(a))
                                                              \mwedge{}\msubb{}  (l1  prop(dl-or-1(dl-obj-prop(a))))
                                                              \mwedge{}\msubb{}  (l2  prop(dl-or-2(dl-obj-prop(a)))));
                  dl-box(alpha,phi){}\mRightarrow{}  l1,l2.\mlambda{}a.(dl-kind(a)  =a  "prop"
                                                                            \mwedge{}\msubb{}  dl-box?(dl-obj-prop(a))
                                                                            \mwedge{}\msubb{}  (l1  prog(dl-box-1(dl-obj-prop(a))))
                                                                            \mwedge{}\msubb{}  (l2  prop(dl-box-2(dl-obj-prop(a)))));
                  dl-diamond(alpha,phi){}\mRightarrow{}  l1,l2.\mlambda{}a.(dl-kind(a)  =a  "prop"
                                                                                    \mwedge{}\msubb{}  dl-diamond?(dl-obj-prop(a))
                                                                                    \mwedge{}\msubb{}  (l1  prog(dl-diamond-1(dl-obj-prop(a))))
                                                                                    \mwedge{}\msubb{}  (l2  prop(dl-diamond-2(dl-obj-prop(a)))))) 


Date html generated: 2019_10_15-AM-11_42_41
Last ObjectModification: 2019_04_04-PM-06_33_44

Theory : dynamic!logic


Home Index