Nuprl Lemma : dl-ind-dl-test

∀[aprog,comp,choose,iterate,test,aprop,false,implies,and,or,box,diamond,x: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])  
   prog((x)?) ~ test[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(x)])


Proof



Definitions occuring in Statement :  dl-ind: dl-ind,  dl-test: (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: f a,  sqequal: s ~ t
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  dl-ind: dl-ind,  dl-induction,  mrec_ind: mrec_ind(L;h;x),  dl-prog-obj: prog(x),  genrec-ap: genrec-ap,  dl-test: (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 b then t else f fi ,  atom-deq: AtomDeq,  eq_atom: x =a y,  pi1: fst(t),  btrue: tt,  pi2: snd(t),  all: ∀x:A. B[x],  member: t ∈ T,  top: Top,  eqof: eqof(d),  bfalse: ff,  bool_cases_sqequal,  let: let,  select: L[n],  select-tuple: x.n,  eq_int: (i =z j),  subtract: n - m,  dl-prop-obj: prop(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: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])   
      prog((x)?)  \msim{}  test[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(x)])


Date html generated: 2019_10_15-AM-11_42_11
Last ObjectModification: 2019_03_26-AM-11_25_41

Theory : dynamic!logic


Home Index