Nuprl Lemma : term-ind_wf
∀[opr:Type]. ∀[P:term(opr) ⟶ ℙ]. ∀[varcase:∀v:{v:varname()| ¬(v = nullvar() ∈ varname())} . P[varterm(v)]].
∀[mktermcase:∀f:opr. ∀bts:bound-term(opr) List. ((∀i:ℕ||bts||. P[snd(bts[i])]) ⇒ P[mkterm(f;bts)])]. ∀[t:term(opr)].
(term-ind(x.varcase[x];f,bts,r.mktermcase[f;bts;r];t) ∈ P[t])
Proof
Definitions occuring in Statement :
term-ind: term-ind,
bound-term: bound-term(opr),
mkterm: mkterm(opr;bts),
varterm: varterm(v),
term: term(opr),
nullvar: nullvar(),
varname: varname(),
select: L[n],
length: ||as||,
list: T List,
int_seg: {i..j-},
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s1;s2;s3],
so_apply: x[s],
pi2: snd(t),
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
member: t ∈ T,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
natural_number: $n,
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
term-ind: term-ind,
genrec-ap: genrec-ap,
term-induction1-ext,
all: ∀x:A. B[x],
implies: P ⇒ Q,
so_apply: x[s],
subtype_rel: A ⊆r B,
prop: ℙ,
not: ¬A,
false: False,
uimplies: b supposing a,
int_seg: {i..j-},
lelt: i ≤ j < k,
and: P ∧ Q,
le: A ≤ B,
less_than: a < b,
squash: ↓T,
decidable: Dec(P),
or: P ∨ Q,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
bound-term: bound-term(opr),
pi2: snd(t),
guard: {T},
so_lambda: λ2x.t[x]
Lemmas referenced :
term-induction1-ext,
term_wf,
varname_wf,
nullvar_wf,
istype-void,
varterm_wf,
list_wf,
bound-term_wf,
int_seg_wf,
length_wf,
select_wf,
int_seg_properties,
decidable__le,
full-omega-unsat,
intformand_wf,
intformnot_wf,
intformle_wf,
itermConstant_wf,
itermVar_wf,
istype-int,
int_formula_prop_and_lemma,
int_formula_prop_not_lemma,
int_formula_prop_le_lemma,
int_term_value_constant_lemma,
int_term_value_var_lemma,
int_formula_prop_wf,
decidable__lt,
intformless_wf,
int_formula_prop_less_lemma,
mkterm_wf,
all_wf,
not_wf,
equal_wf,
equal-wf-T-base,
istype-universe
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
cut,
sqequalRule,
lambdaEquality_alt,
isectElimination,
hypothesisEquality,
equalityTransitivity,
equalitySymmetry,
hypothesis,
inhabitedIsType,
lambdaFormation_alt,
thin,
equalityIstype,
sqequalHypSubstitution,
dependent_functionElimination,
independent_functionElimination,
isectIsType,
functionIsType,
universeIsType,
introduction,
extract_by_obid,
universeEquality,
setIsType,
because_Cache,
applyEquality,
setElimination,
rename,
independent_isectElimination,
voidElimination,
natural_numberEquality,
productElimination,
imageElimination,
unionElimination,
approximateComputation,
dependent_pairFormation_alt,
int_eqEquality,
Error :memTop,
independent_pairFormation,
functionEquality,
instantiate,
functionExtensionality,
closedConclusion,
setEquality,
baseClosed
Latex:
\mforall{}[opr:Type]. \mforall{}[P:term(opr) {}\mrightarrow{} \mBbbP{}]. \mforall{}[varcase:\mforall{}v:\{v:varname()| \mneg{}(v = nullvar())\} . P[varterm(v)]].
\mforall{}[mktermcase:\mforall{}f:opr. \mforall{}bts:bound-term(opr) List.
((\mforall{}i:\mBbbN{}||bts||. P[snd(bts[i])]) {}\mRightarrow{} P[mkterm(f;bts)])]. \mforall{}[t:term(opr)].
(term-ind(x.varcase[x];f,bts,r.mktermcase[f;bts;r];t) \mmember{} P[t])
Date html generated:
2020_05_19-PM-09_54_28
Last ObjectModification:
2020_03_09-PM-04_08_36
Theory : terms
Home
Index