Nuprl Lemma : dl-ind-dl-box

[aprog,comp,choose,iterate,test,aprop,false,implies,and,or,box,diamond,x,x1:Top].
  (dl-ind(
          dl-aprog(x0) aprog[x0];
          dl-comp(x1,x2) x3,x4.comp[x1;x2;x3;x4];
          dl-choose(x5,x6) x7,x8.choose[x5;x6;x7;x8];
          dl-iterate(x9) x10.iterate[x9;x10];
          dl-test(x11) x12.test[x11;x12];
          dl-aprop(x13) aprop[x13];
          dl-false false;
          dl-implies(x14,x15) x16,x17.implies[x14;x15;x16;x17];
          dl-and(x18,x19) x20,x21.and[x18;x19;x20;x21];
          dl-or(x22,x23) x24,x25.or[x22;x23;x24;x25];
          dl-box(x26,x27) x28,x29.box[x26;x27;x28;x29];
          dl-diamond(x30,x31) x32,x33.diamond[x30;x31;x32;x33])  
   prop([x] x1) box[x;x1;dl-ind(
                                  dl-aprog(x0) aprog[x0];
                                  dl-comp(x1,x2) x3,x4.comp[x1;x2;x3;x4];
                                  dl-choose(x5,x6) x7,x8.choose[x5;x6;x7;x8];
                                  dl-iterate(x9) x10.iterate[x9;x10];
                                  dl-test(x11) x12.test[x11;x12];
                                  dl-aprop(x13) aprop[x13];
                                  dl-false false;
                                  dl-implies(x14,x15) x16,x17.implies[x14;x15;x16;x17];
                                  dl-and(x18,x19) x20,x21.and[x18;x19;x20;x21];
                                  dl-or(x22,x23) x24,x25.or[x22;x23;x24;x25];
                                  dl-box(x26,x27) x28,x29.box[x26;x27;x28;x29];
                                  dl-diamond(x30,x31) x32,x33.diamond[x30;x31;x32;x33])  
                           prog(x);dl-ind(
                                          dl-aprog(x0) aprog[x0];
                                          dl-comp(x1,x2) x3,x4.comp[x1;x2;x3;x4];
                                          dl-choose(x5,x6) x7,x8.choose[x5;x6;x7;x8];
                                          dl-iterate(x9) x10.iterate[x9;x10];
                                          dl-test(x11) x12.test[x11;x12];
                                          dl-aprop(x13) aprop[x13];
                                          dl-false false;
                                          dl-implies(x14,x15) x16,x17.implies[x14;x15;x16;x17];
                                          dl-and(x18,x19) x20,x21.and[x18;x19;x20;x21];
                                          dl-or(x22,x23) x24,x25.or[x22;x23;x24;x25];
                                          dl-box(x26,x27) x28,x29.box[x26;x27;x28;x29];
                                          dl-diamond(x30,x31) x32,x33.diamond[x30;x31;x32;x33])  
                                   prop(x1)])


Proof




Definitions occuring in Statement :  dl-ind: dl-ind dl-box: [x1] x dl-prop-obj: prop(x) dl-prog-obj: prog(x) uall: [x:A]. B[x] top: Top so_apply: x[s1;s2;s3;s4] so_apply: x[s1;s2] so_apply: x[s] apply: a sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] dl-ind: dl-ind dl-induction mrec_ind: mrec_ind(L;h;x) dl-prop-obj: prop(x) genrec-ap: genrec-ap dl-box: [x1] x mk-prec: mk-prec(lbl;x) assert_of_eq_atom eqff_to_assert decidable__atom_equal apply-alist: apply-alist(eq;L;x) list_ind: list_ind dl-Spec: dl-Spec() cons: [a b] ifthenelse: if then else fi  atom-deq: AtomDeq eq_atom: =a y pi1: fst(t) bfalse: ff btrue: tt pi2: snd(t) all: x:A. B[x] member: t ∈ T top: Top eqof: eqof(d) bool_cases_sqequal let: let select: L[n] select-tuple: x.n eq_int: (i =z j) subtract: m dl-prog-obj: prog(x)
Lemmas referenced :  apply_alist_cons_lemma istype-void length_of_cons_lemma length_of_nil_lemma istype-top dl-induction assert_of_eq_atom eqff_to_assert decidable__atom_equal bool_cases_sqequal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt sqequalRule cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality_alt voidElimination hypothesis because_Cache inhabitedIsType hypothesisEquality

Latex:
\mforall{}[aprog,comp,choose,iterate,test,aprop,false,implies,and,or,box,diamond,x,x1:Top].
    (dl-ind(
                    dl-aprog(x0){}\mRightarrow{}  aprog[x0];
                    dl-comp(x1,x2){}\mRightarrow{}  x3,x4.comp[x1;x2;x3;x4];
                    dl-choose(x5,x6){}\mRightarrow{}  x7,x8.choose[x5;x6;x7;x8];
                    dl-iterate(x9){}\mRightarrow{}  x10.iterate[x9;x10];
                    dl-test(x11){}\mRightarrow{}  x12.test[x11;x12];
                    dl-aprop(x13){}\mRightarrow{}  aprop[x13];
                    dl-false{}\mRightarrow{}  false;
                    dl-implies(x14,x15){}\mRightarrow{}  x16,x17.implies[x14;x15;x16;x17];
                    dl-and(x18,x19){}\mRightarrow{}  x20,x21.and[x18;x19;x20;x21];
                    dl-or(x22,x23){}\mRightarrow{}  x24,x25.or[x22;x23;x24;x25];
                    dl-box(x26,x27){}\mRightarrow{}  x28,x29.box[x26;x27;x28;x29];
                    dl-diamond(x30,x31){}\mRightarrow{}  x32,x33.diamond[x30;x31;x32;x33])   
      prop([x]  x1)  \msim{}  box[x;x1;dl-ind(
                                                                    dl-aprog(x0){}\mRightarrow{}  aprog[x0];
                                                                    dl-comp(x1,x2){}\mRightarrow{}  x3,x4.comp[x1;x2;x3;x4];
                                                                    dl-choose(x5,x6){}\mRightarrow{}  x7,x8.choose[x5;x6;x7;x8];
                                                                    dl-iterate(x9){}\mRightarrow{}  x10.iterate[x9;x10];
                                                                    dl-test(x11){}\mRightarrow{}  x12.test[x11;x12];
                                                                    dl-aprop(x13){}\mRightarrow{}  aprop[x13];
                                                                    dl-false{}\mRightarrow{}  false;
                                                                    dl-implies(x14,x15){}\mRightarrow{}  x16,x17.implies[x14;x15;x16;x17];
                                                                    dl-and(x18,x19){}\mRightarrow{}  x20,x21.and[x18;x19;x20;x21];
                                                                    dl-or(x22,x23){}\mRightarrow{}  x24,x25.or[x22;x23;x24;x25];
                                                                    dl-box(x26,x27){}\mRightarrow{}  x28,x29.box[x26;x27;x28;x29];
                                                                    dl-diamond(x30,x31){}\mRightarrow{}  x32,x33.diamond[x30;x31;x32;x33])   
                                                      prog(x);dl-ind(
                                                                                    dl-aprog(x0){}\mRightarrow{}  aprog[x0];
                                                                                    dl-comp(x1,x2){}\mRightarrow{}  x3,x4.comp[x1;x2;x3;x4];
                                                                                    dl-choose(x5,x6){}\mRightarrow{}  x7,x8.choose[x5;x6;x7;x8];
                                                                                    dl-iterate(x9){}\mRightarrow{}  x10.iterate[x9;x10];
                                                                                    dl-test(x11){}\mRightarrow{}  x12.test[x11;x12];
                                                                                    dl-aprop(x13){}\mRightarrow{}  aprop[x13];
                                                                                    dl-false{}\mRightarrow{}  false;
                                                                                    dl-implies(x14,x15){}\mRightarrow{}  x16,x17.implies[x14;x15;x16;x17];
                                                                                    dl-and(x18,x19){}\mRightarrow{}  x20,x21.and[x18;x19;x20;x21];
                                                                                    dl-or(x22,x23){}\mRightarrow{}  x24,x25.or[x22;x23;x24;x25];
                                                                                    dl-box(x26,x27){}\mRightarrow{}  x28,x29.box[x26;x27;x28;x29];
                                                                                    dl-diamond(x30,x31){}\mRightarrow{}  x32,x33.diamond[x30;x31;x32;x33])   
                                                                      prop(x1)])



Date html generated: 2019_10_15-AM-11_42_26
Last ObjectModification: 2019_03_26-AM-11_26_21

Theory : dynamic!logic


Home Index