Nuprl Lemma : wf-term-induction
∀[opr:Type]
∀sort:term(opr) ⟶ ℕ. ∀arity:opr ⟶ ((ℕ × ℕ) List).
∀[P:wfterm(opr;sort;arity) ⟶ ℙ]
((∀v:{v:varname()| ¬(v = nullvar() ∈ varname())} . P[varterm(v)])
⇒ (∀f:opr. ∀bts:wf-bound-terms(opr;sort;arity;f). ((∀i:ℕ||bts||. P[snd(bts[i])]) ⇒ P[mkwfterm(f;bts)]))
⇒ {∀t:wfterm(opr;sort;arity). P[t]})
Proof
Definitions occuring in Statement :
mkwfterm: mkwfterm(f;bts),
wf-bound-terms: wf-bound-terms(opr;sort;arity;f),
wfterm: wfterm(opr;sort;arity),
varterm: varterm(v),
term: term(opr),
nullvar: nullvar(),
varname: varname(),
select: L[n],
length: ||as||,
list: T List,
int_seg: {i..j-},
nat: ℕ,
uall: ∀[x:A]. B[x],
prop: ℙ,
guard: {T},
so_apply: x[s],
pi2: snd(t),
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
product: 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,
all: ∀x:A. B[x],
guard: {T},
implies: P ⇒ Q,
so_apply: x[s],
wf-bound-terms: wf-bound-terms(opr;sort;arity;f),
prop: ℙ,
int_seg: {i..j-},
uimplies: b supposing a,
lelt: i ≤ j < k,
and: P ∧ Q,
le: A ≤ B,
less_than: a < b,
squash: ↓T,
decidable: Dec(P),
or: P ∨ Q,
not: ¬A,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
false: False,
pi2: snd(t),
assert: ↑b,
ifthenelse: if b then t else f fi ,
wf-term: wf-term(arity;sort;t),
varterm: varterm(v),
btrue: tt,
true: True,
wfterm: wfterm(opr;sort;arity)
Lemmas referenced :
term-ind_wf_wfterm,
wfterm_wf,
wf-bound-terms_wf,
int_seg_wf,
length_wf,
list_wf,
varname_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,
mkwfterm_wf,
nullvar_wf,
istype-void,
varterm_wf,
istype-assert,
wf-term_wf,
nat_wf,
term_wf,
istype-nat,
istype-universe
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
lambdaFormation_alt,
sqequalRule,
equalityTransitivity,
equalitySymmetry,
universeIsType,
functionIsType,
natural_numberEquality,
productEquality,
setElimination,
rename,
applyEquality,
functionExtensionality,
because_Cache,
independent_isectElimination,
productElimination,
imageElimination,
dependent_functionElimination,
unionElimination,
approximateComputation,
independent_functionElimination,
dependent_pairFormation_alt,
lambdaEquality_alt,
int_eqEquality,
Error :memTop,
independent_pairFormation,
voidElimination,
inhabitedIsType,
equalityIstype,
setIsType,
dependent_set_memberEquality_alt,
universeEquality,
instantiate
Latex:
\mforall{}[opr:Type]
\mforall{}sort:term(opr) {}\mrightarrow{} \mBbbN{}. \mforall{}arity:opr {}\mrightarrow{} ((\mBbbN{} \mtimes{} \mBbbN{}) List).
\mforall{}[P:wfterm(opr;sort;arity) {}\mrightarrow{} \mBbbP{}]
((\mforall{}v:\{v:varname()| \mneg{}(v = nullvar())\} . P[varterm(v)])
{}\mRightarrow{} (\mforall{}f:opr. \mforall{}bts:wf-bound-terms(opr;sort;arity;f).
((\mforall{}i:\mBbbN{}||bts||. P[snd(bts[i])]) {}\mRightarrow{} P[mkwfterm(f;bts)]))
{}\mRightarrow{} \{\mforall{}t:wfterm(opr;sort;arity). P[t]\})
Date html generated:
2020_05_19-PM-09_58_56
Last ObjectModification:
2020_03_09-PM-04_10_28
Theory : terms
Home
Index