Nuprl Lemma : test-induction
∀[T:test-Obj() ⟶ TYPE]
((∀x:Atom. T[test-prog-obj(test-aprog(x))])
⇒ (∀x:test-foo(). (T[test-foo-obj(x)] ⇒ T[test-prog-obj(test-iterate(x))]))
⇒ (∀x:test-prop(). (T[test-prop-obj(x)] ⇒ T[test-prog-obj(test-test(x))]))
⇒ (∀x:Atom. T[test-foo-obj(test-afoo(x))])
⇒ (∀x:test-foo(). (T[test-foo-obj(x)] ⇒ T[test-foo-obj(test-bar(x))]))
⇒ (∀x:test-prop(). ∀x1:test-prog(). (T[test-prop-obj(x)] ⇒ T[test-prog-obj(x1)] ⇒ T[test-foo-obj(test-xx(x;x1))]))
⇒ (∀x:Atom. T[test-prop-obj(test-aprop(x))])
⇒ T[test-prop-obj(test-false())]
⇒ (∀x,x1:test-prop(). (T[test-prop-obj(x)] ⇒ T[test-prop-obj(x1)] ⇒ T[test-prop-obj(test-implies(x;x1))]))
⇒ (∀x:test-prog(). ∀x1:test-prop().
(T[test-prog-obj(x)] ⇒ T[test-prop-obj(x1)] ⇒ T[test-prop-obj(test-box(x;x1))]))
⇒ (∀x:test-foo(). ∀x1:test-prop().
(T[test-foo-obj(x)] ⇒ T[test-prop-obj(x1)] ⇒ T[test-prop-obj(test-diamond(x;x1))]))
⇒ (∀x:test-Obj(). T[x]))
Proof
Definitions occuring in Statement :
test-diamond: test-diamond(x1;x),
test-box: test-box(x1;x),
test-implies: test-implies(x1;x),
test-false: test-false(),
test-aprop: test-aprop(x),
test-xx: test-xx(x1;x),
test-bar: test-bar(x),
test-afoo: test-afoo(x),
test-test: test-test(x),
test-iterate: test-iterate(x),
test-aprog: test-aprog(x),
test-prop-obj: test-prop-obj(x),
test-foo-obj: test-foo-obj(x),
test-prog-obj: test-prog-obj(x),
test-prop: test-prop(),
test-foo: test-foo(),
test-prog: test-prog(),
test-Obj: test-Obj(),
uall: ∀[x:A]. B[x],
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
function: x:A ⟶ B[x],
atom: Atom
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
all: ∀x:A. B[x],
mrecind: mrecind(L;x.P[x]),
mkinds: mKinds,
eager-map: eager-map(f;as),
list_ind: list_ind,
test-Spec: test-Spec(),
cons: [a / b],
pi1: fst(t),
nil: [],
it: ⋅,
member: t ∈ T,
decidable: Dec(P),
or: P ∨ Q,
uimplies: b supposing a,
sq_type: SQType(T),
guard: {T},
mrec-spec: mrec-spec(L;lbl;p),
apply-alist: apply-alist(eq;L;x),
ifthenelse: if b then t else f fi ,
atom-deq: AtomDeq,
eq_atom: x =a y,
btrue: tt,
pi2: snd(t),
top: Top,
eqof: eqof(d),
bool: 𝔹,
unit: Unit,
uiff: uiff(P;Q),
and: P ∧ Q,
prec-arg-types: prec-arg-types(lbl,p.a[lbl; p];i;lbl),
int_seg: {i..j-},
lelt: i ≤ j < k,
not: ¬A,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
prop: ℙ,
false: False,
select: L[n],
test-aprog: test-aprog(x),
test-prog-obj: test-prog-obj(x),
le: A ≤ B,
bfalse: ff,
bnot: ¬bb,
assert: ↑b,
mrec: mrec(L;i),
nequal: a ≠ b ∈ T ,
select-tuple: x.n,
eq_int: (i =z j),
subtract: n - m,
test-foo-obj: test-foo-obj(x),
test-foo: test-foo(),
test-iterate: test-iterate(x),
so_apply: x[s],
test-prop-obj: test-prop-obj(x),
test-prop: test-prop(),
test-test: test-test(x),
less_than: a < b,
squash: ↓T,
less_than': less_than'(a;b),
test-afoo: test-afoo(x),
test-bar: test-bar(x),
test-prog: test-prog(),
test-xx: test-xx(x1;x),
test-aprop: test-aprop(x),
test-false: test-false(),
test-implies: test-implies(x1;x),
test-box: test-box(x1;x),
test-diamond: test-diamond(x1;x),
iff: P ⇐⇒ Q,
so_lambda: λ2x.t[x],
test-Obj: test-Obj()
Lemmas referenced :
decidable__atom_equal,
subtype_base_sq,
atom_subtype_base,
apply_alist_cons_lemma,
istype-void,
eq_atom_wf,
eqtt_to_assert,
assert_of_eq_atom,
length_of_cons_lemma,
length_of_nil_lemma,
atomdeq_reduce_lemma,
map_cons_lemma,
map_nil_lemma,
tupletype_cons_lemma,
null_nil_lemma,
tupletype_nil_lemma,
decidable__le,
full-omega-unsat,
intformnot_wf,
intformle_wf,
itermConstant_wf,
istype-int,
int_formula_prop_not_lemma,
int_formula_prop_le_lemma,
int_term_value_constant_lemma,
int_formula_prop_wf,
decidable__lt,
intformless_wf,
int_formula_prop_less_lemma,
istype-le,
istype-less_than,
int_seg_wf,
decidable__equal_int,
int_subtype_base,
int_seg_properties,
true_wf,
int_seg_subtype_special,
int_seg_cases,
intformand_wf,
itermVar_wf,
int_formula_prop_and_lemma,
int_term_value_var_lemma,
eqff_to_assert,
bool_cases_sqequal,
bool_wf,
bool_subtype_base,
assert-bnot,
neg_assert_of_eq_atom,
test-foo-obj_wf,
mrec_wf,
test-Spec_wf,
test-prop-obj_wf,
length_wf,
mrec-spec_wf,
null_cons_lemma,
test-prog-obj_wf,
unit_wf2,
cons_member,
cons_wf,
nil_wf,
member_singleton,
mkinds_wf,
mrec_ind_wf,
mobj_wf,
test-Obj_wf,
test-diamond_wf,
test-prog_wf,
test-box_wf,
test-implies_wf,
test-false_wf,
test-aprop_wf,
test-xx_wf,
test-bar_wf,
test-afoo_wf,
test-prop_wf,
test-test_wf,
test-foo_wf,
test-iterate_wf,
istype-atom,
test-aprog_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
lambdaFormation_alt,
cut,
thin,
sqequalHypSubstitution,
setElimination,
rename,
sqequalRule,
hypothesis,
introduction,
extract_by_obid,
dependent_functionElimination,
hypothesisEquality,
tokenEquality,
unionElimination,
instantiate,
isectElimination,
cumulativity,
atomEquality,
independent_isectElimination,
because_Cache,
independent_functionElimination,
equalityTransitivity,
equalitySymmetry,
isect_memberEquality_alt,
voidElimination,
inhabitedIsType,
equalityElimination,
productElimination,
dependent_set_memberEquality_alt,
natural_numberEquality,
independent_pairFormation,
approximateComputation,
dependent_pairFormation_alt,
lambdaEquality_alt,
universeIsType,
productIsType,
functionIsType,
intEquality,
hypothesis_subsumption,
int_eqEquality,
equalityIstype,
promote_hyp,
TYPEMemberIsType,
applyEquality,
imageElimination,
setIsType,
unionEquality,
universeEquality,
TYPEIsType
Latex:
\mforall{}[T:test-Obj() {}\mrightarrow{} TYPE]
((\mforall{}x:Atom. T[test-prog-obj(test-aprog(x))])
{}\mRightarrow{} (\mforall{}x:test-foo(). (T[test-foo-obj(x)] {}\mRightarrow{} T[test-prog-obj(test-iterate(x))]))
{}\mRightarrow{} (\mforall{}x:test-prop(). (T[test-prop-obj(x)] {}\mRightarrow{} T[test-prog-obj(test-test(x))]))
{}\mRightarrow{} (\mforall{}x:Atom. T[test-foo-obj(test-afoo(x))])
{}\mRightarrow{} (\mforall{}x:test-foo(). (T[test-foo-obj(x)] {}\mRightarrow{} T[test-foo-obj(test-bar(x))]))
{}\mRightarrow{} (\mforall{}x:test-prop(). \mforall{}x1:test-prog().
(T[test-prop-obj(x)] {}\mRightarrow{} T[test-prog-obj(x1)] {}\mRightarrow{} T[test-foo-obj(test-xx(x;x1))]))
{}\mRightarrow{} (\mforall{}x:Atom. T[test-prop-obj(test-aprop(x))])
{}\mRightarrow{} T[test-prop-obj(test-false())]
{}\mRightarrow{} (\mforall{}x,x1:test-prop().
(T[test-prop-obj(x)] {}\mRightarrow{} T[test-prop-obj(x1)] {}\mRightarrow{} T[test-prop-obj(test-implies(x;x1))]))
{}\mRightarrow{} (\mforall{}x:test-prog(). \mforall{}x1:test-prop().
(T[test-prog-obj(x)] {}\mRightarrow{} T[test-prop-obj(x1)] {}\mRightarrow{} T[test-prop-obj(test-box(x;x1))]))
{}\mRightarrow{} (\mforall{}x:test-foo(). \mforall{}x1:test-prop().
(T[test-foo-obj(x)] {}\mRightarrow{} T[test-prop-obj(x1)] {}\mRightarrow{} T[test-prop-obj(test-diamond(x;x1))]))
{}\mRightarrow{} (\mforall{}x:test-Obj(). T[x]))
Date html generated:
2019_10_15-AM-10_51_24
Last ObjectModification:
2019_03_25-PM-01_46_34
Theory : tree_1
Home
Index