Nuprl Lemma : dl-ind-dl-comp
∀[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])
prog((x;x1)) ~ comp[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])
prog(x1)])
Proof
Definitions occuring in Statement :
dl-ind: dl-ind,
dl-comp: (x1;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-comp: (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 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
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])
prog((x;x1)) \msim{} comp[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])
prog(x1)])
Date html generated:
2019_10_15-AM-11_42_04
Last ObjectModification:
2019_03_26-AM-11_25_35
Theory : dynamic!logic
Home
Index