Nuprl Lemma : ctt-term-induction
∀[P:CttTerm ⟶ ℙ{i'''''}]
((∀v:{v:varname()| ¬(v = nullvar() ∈ varname())} . P[varterm(v)])
⇒ (∀f:CttOp. ∀bts:{bts:(varname() List × CttTerm) List|
(||bts|| = ||ctt-arity(f)|| ∈ ℤ)
∧ (∀i:ℕ||bts||
((||fst(bts[i])|| = (fst(ctt-arity(f)[i])) ∈ ℤ)
∧ (ctt-kind(snd(bts[i])) = (snd(ctt-arity(f)[i])) ∈ ℤ)))} .
((∀i:ℕ||bts||. P[snd(bts[i])]) ⇒ P[mkwfterm(f;bts)]))
⇒ {∀t:CttTerm. P[t]})
Proof
Definitions occuring in Statement :
ctt-term: CttTerm,
ctt-arity: ctt-arity(x),
ctt-kind: ctt-kind(t),
ctt-op: CttOp,
mkwfterm: mkwfterm(f;bts),
varterm: varterm(v),
nullvar: nullvar(),
varname: varname(),
select: L[n],
length: ||as||,
list: T List,
int_seg: {i..j-},
uall: ∀[x:A]. B[x],
prop: ℙ,
guard: {T},
so_apply: x[s],
pi1: fst(t),
pi2: snd(t),
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
product: x:A × B[x],
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
all: ∀x:A. B[x],
wf-bound-terms: wf-bound-terms(opr;sort;arity;f),
ctt-term: CttTerm
Lemmas referenced :
wf-term-induction,
ctt-op_wf,
ctt-kind_wf,
term_wf,
ctt-arity_wf
Rules used in proof :
cut,
instantiate,
introduction,
extract_by_obid,
sqequalHypSubstitution,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isectElimination,
thin,
cumulativity,
hypothesis,
dependent_functionElimination,
lambdaEquality_alt,
hypothesisEquality,
universeIsType,
sqequalRule
Latex:
\mforall{}[P:CttTerm {}\mrightarrow{} \mBbbP{}\{i'''''\}]
((\mforall{}v:\{v:varname()| \mneg{}(v = nullvar())\} . P[varterm(v)])
{}\mRightarrow{} (\mforall{}f:CttOp. \mforall{}bts:\{bts:(varname() List \mtimes{} CttTerm) List|
(||bts|| = ||ctt-arity(f)||)
\mwedge{} (\mforall{}i:\mBbbN{}||bts||
((||fst(bts[i])|| = (fst(ctt-arity(f)[i])))
\mwedge{} (ctt-kind(snd(bts[i])) = (snd(ctt-arity(f)[i])))))\} .
((\mforall{}i:\mBbbN{}||bts||. P[snd(bts[i])]) {}\mRightarrow{} P[mkwfterm(f;bts)]))
{}\mRightarrow{} \{\mforall{}t:CttTerm. P[t]\})
Date html generated:
2020_05_20-PM-08_20_30
Last ObjectModification:
2020_05_13-PM-02_26_52
Theory : cubical!type!theory
Home
Index