Nuprl Lemma : test-ind_wf_definition
∀[A,B,C:TYPE]. ∀[aprog:x:Atom ⟶ A]. ∀[iterate:x:test-foo() ⟶ B ⟶ A]. ∀[test:x:test-prop() ⟶ C ⟶ A].
∀[afoo:x:Atom ⟶ B]. ∀[bar:x:test-foo() ⟶ B ⟶ B]. ∀[xx:x:test-prop() ⟶ x1:test-prog() ⟶ C ⟶ A ⟶ B]. ∀[aprop:x:Atom
⟶ C].
∀[false:C]. ∀[implies:x:test-prop() ⟶ x1:test-prop() ⟶ C ⟶ C ⟶ C]. ∀[box:x:test-prog()
⟶ x1:test-prop()
⟶ A
⟶ C
⟶ C]. ∀[diamond:x:test-foo()
⟶ x1:test-prop()
⟶ B
⟶ C
⟶ C].
(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]) ∈ d:test-Obj() ⟶ if test-kind(d) =a "prog"
then A
if test-kind(d) =a "foo" then B
else C
fi )
Proof
Definitions occuring in Statement :
test-ind: test-ind,
test-kind: test-kind(d),
test-prop: test-prop(),
test-foo: test-foo(),
test-prog: test-prog(),
test-Obj: test-Obj(),
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
uall: ∀[x:A]. B[x],
so_apply: x[s1;s2;s3;s4],
so_apply: x[s1;s2],
so_apply: x[s],
member: t ∈ T,
function: x:A ⟶ B[x],
token: "$token",
atom: Atom
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
so_lambda: λ2x.t[x],
subtype_rel: A ⊆r B,
all: ∀x:A. B[x],
implies: P ⇒ Q,
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
ifthenelse: if b then t else f fi ,
bfalse: ff,
uiff: uiff(P;Q),
and: P ∧ Q,
uimplies: b supposing a,
exists: ∃x:A. B[x],
or: P ∨ Q,
sq_type: SQType(T),
guard: {T},
bnot: ¬bb,
assert: ↑b,
false: False,
so_apply: x[s],
eq_atom: x =a y,
test-kind: test-kind(d),
mobj-kind: mobj-kind(x),
pi1: fst(t),
test-prog-obj: test-prog-obj(x),
so_lambda: λ2x y.t[x; y],
test-foo-obj: test-foo-obj(x),
so_apply: x[s1;s2],
test-prop-obj: test-prop-obj(x),
so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]),
so_apply: x[s1;s2;s3;s4]
Lemmas referenced :
test-ind_wf,
eq_atom_wf,
test-kind_wf,
eqff_to_assert,
bool_cases_sqequal,
subtype_base_sq,
bool_wf,
bool_subtype_base,
assert-bnot,
neg_assert_of_eq_atom,
test-Obj_wf,
istype-atom,
test-foo_wf,
test-prop_wf,
test-prog_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
sqequalRule,
lambdaEquality_alt,
hypothesisEquality,
hypothesis,
applyEquality,
because_Cache,
closedConclusion,
tokenEquality,
inhabitedIsType,
lambdaFormation_alt,
unionElimination,
equalityElimination,
productElimination,
independent_isectElimination,
equalityTransitivity,
equalitySymmetry,
dependent_pairFormation_alt,
equalityIstype,
promote_hyp,
dependent_functionElimination,
instantiate,
cumulativity,
independent_functionElimination,
voidElimination,
universeIsType,
TYPEMemberIsType,
functionIsType,
TYPEIsType
Latex:
\mforall{}[A,B,C:TYPE]. \mforall{}[aprog:x:Atom {}\mrightarrow{} A]. \mforall{}[iterate:x:test-foo() {}\mrightarrow{} B {}\mrightarrow{} A]. \mforall{}[test:x:test-prop()
{}\mrightarrow{} C
{}\mrightarrow{} A].
\mforall{}[afoo:x:Atom {}\mrightarrow{} B]. \mforall{}[bar:x:test-foo() {}\mrightarrow{} B {}\mrightarrow{} B]. \mforall{}[xx:x:test-prop()
{}\mrightarrow{} x1:test-prog()
{}\mrightarrow{} C
{}\mrightarrow{} A
{}\mrightarrow{} B]. \mforall{}[aprop:x:Atom {}\mrightarrow{} C]. \mforall{}[false:C].
\mforall{}[implies:x:test-prop() {}\mrightarrow{} x1:test-prop() {}\mrightarrow{} C {}\mrightarrow{} C {}\mrightarrow{} C]. \mforall{}[box:x:test-prog()
{}\mrightarrow{} x1:test-prop()
{}\mrightarrow{} A
{}\mrightarrow{} C
{}\mrightarrow{} C]. \mforall{}[diamond:x:test-foo()
{}\mrightarrow{} x1:test-prop()
{}\mrightarrow{} B
{}\mrightarrow{} C
{}\mrightarrow{} C].
(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]) \mmember{} d:test-Obj()
{}\mrightarrow{} if test-kind(d) =a "prog" then A
if test-kind(d) =a "foo" then B
else C
fi )
Date html generated:
2019_10_15-AM-10_51_32
Last ObjectModification:
2019_03_25-PM-01_49_01
Theory : tree_1
Home
Index