Nuprl Lemma : test-ind-test-diamond
∀[aprog,iterate,test,afoo,bar,xx,aprop,false,implies,box,diamond,x,x1:Top].
(test-ind(
test-aprog(x0)⇒ aprog[x0];
test-iterate(x1)⇒ x2.iterate[x1;x2];
test-test(x3)⇒ x4.test[x3;x4];
test-afoo(x5)⇒ afoo[x5];
test-bar(x6)⇒ x7.bar[x6;x7];
test-xx(x8,x9)⇒ x10,x11.xx[x8;x9;x10;x11];
test-aprop(x12)⇒ aprop[x12];
test-false⇒ false;
test-implies(x13,x14)⇒ x15,x16.implies[x13;x14;x15;x16];
test-box(x17,x18)⇒ x19,x20.box[x17;x18;x19;x20];
test-diamond(x21,x22)⇒ x23,x24.diamond[x21;x22;x23;x24])
test-prop-obj(test-diamond(x;x1))
~ diamond[x;x1;test-ind(
test-aprog(x0)⇒ aprog[x0];
test-iterate(x1)⇒ x2.iterate[x1;x2];
test-test(x3)⇒ x4.test[x3;x4];
test-afoo(x5)⇒ afoo[x5];
test-bar(x6)⇒ x7.bar[x6;x7];
test-xx(x8,x9)⇒ x10,x11.xx[x8;x9;x10;x11];
test-aprop(x12)⇒ aprop[x12];
test-false⇒ false;
test-implies(x13,x14)⇒ x15,x16.implies[x13;x14;x15;x16];
test-box(x17,x18)⇒ x19,x20.box[x17;x18;x19;x20];
test-diamond(x21,x22)⇒ x23,x24.diamond[x21;x22;x23;x24])
test-foo-obj(x);test-ind(
test-aprog(x0)⇒ aprog[x0];
test-iterate(x1)⇒ x2.iterate[x1;x2];
test-test(x3)⇒ x4.test[x3;x4];
test-afoo(x5)⇒ afoo[x5];
test-bar(x6)⇒ x7.bar[x6;x7];
test-xx(x8,x9)⇒ x10,x11.xx[x8;x9;x10;x11];
test-aprop(x12)⇒ aprop[x12];
test-false⇒ false;
test-implies(x13,x14)⇒ x15,x16.implies[x13;x14;x15;x16];
test-box(x17,x18)⇒ x19,x20.box[x17;x18;x19;x20];
test-diamond(x21,x22)⇒ x23,x24.diamond[x21;x22;x23;x24])
test-prop-obj(x1)])
Proof
Definitions occuring in Statement :
test-ind: test-ind,
test-diamond: test-diamond(x1;x),
test-prop-obj: test-prop-obj(x),
test-foo-obj: test-foo-obj(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],
test-ind: test-ind,
test-induction,
mrec_ind: mrec_ind(L;h;x),
test-prop-obj: test-prop-obj(x),
genrec-ap: genrec-ap,
test-diamond: test-diamond(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,
test-Spec: test-Spec(),
cons: [a / b],
ifthenelse: if b then t else f fi ,
atom-deq: AtomDeq,
eq_atom: x =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: n - m,
test-foo-obj: test-foo-obj(x)
Lemmas referenced :
apply_alist_cons_lemma,
istype-void,
length_of_cons_lemma,
length_of_nil_lemma,
istype-top,
test-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,iterate,test,afoo,bar,xx,aprop,false,implies,box,diamond,x,x1:Top].
(test-ind(
test-aprog(x0){}\mRightarrow{} aprog[x0];
test-iterate(x1){}\mRightarrow{} x2.iterate[x1;x2];
test-test(x3){}\mRightarrow{} x4.test[x3;x4];
test-afoo(x5){}\mRightarrow{} afoo[x5];
test-bar(x6){}\mRightarrow{} x7.bar[x6;x7];
test-xx(x8,x9){}\mRightarrow{} x10,x11.xx[x8;x9;x10;x11];
test-aprop(x12){}\mRightarrow{} aprop[x12];
test-false{}\mRightarrow{} false;
test-implies(x13,x14){}\mRightarrow{} x15,x16.implies[x13;x14;x15;x16];
test-box(x17,x18){}\mRightarrow{} x19,x20.box[x17;x18;x19;x20];
test-diamond(x21,x22){}\mRightarrow{} x23,x24.diamond[x21;x22;x23;x24])
test-prop-obj(test-diamond(x;x1))
\msim{} diamond[x;x1;test-ind(
test-aprog(x0){}\mRightarrow{} aprog[x0];
test-iterate(x1){}\mRightarrow{} x2.iterate[x1;x2];
test-test(x3){}\mRightarrow{} x4.test[x3;x4];
test-afoo(x5){}\mRightarrow{} afoo[x5];
test-bar(x6){}\mRightarrow{} x7.bar[x6;x7];
test-xx(x8,x9){}\mRightarrow{} x10,x11.xx[x8;x9;x10;x11];
test-aprop(x12){}\mRightarrow{} aprop[x12];
test-false{}\mRightarrow{} false;
test-implies(x13,x14){}\mRightarrow{} x15,x16.implies[x13;x14;x15;x16];
test-box(x17,x18){}\mRightarrow{} x19,x20.box[x17;x18;x19;x20];
test-diamond(x21,x22){}\mRightarrow{} x23,x24.diamond[x21;x22;x23;x24])
test-foo-obj(x);...
test-prop-obj(x1)])
Date html generated:
2019_10_15-AM-10_52_05
Last ObjectModification:
2019_03_25-PM-01_49_59
Theory : tree_1
Home
Index