Nuprl Lemma : prec-size-induction-ext
∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[Q:i:P ⟶ prec(lbl,p.a[lbl;p];i) ⟶ TYPE].
((∀i:P. ∀x:prec(lbl,p.a[lbl;p];i). ((∀j:P. ∀z:{z:prec(lbl,p.a[lbl;p];j)| ||j;z|| < ||i;x||} . Q[j;z]) ⇒ Q[i;x]))
⇒ (∀i:P. ∀x:prec(lbl,p.a[lbl;p];i). Q[i;x]))
Proof
Definitions occuring in Statement :
prec-size: ||i;x||,
prec: prec(lbl,p.a[lbl; p];i),
list: T List,
less_than: a < b,
uall: ∀[x:A]. B[x],
so_apply: x[s1;s2],
all: ∀x:A. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
union: left + right,
atom: Atom,
universe: Type
Definitions unfolded in proof :
member: t ∈ T,
genrec-ap: genrec-ap,
prec-size-induction
Lemmas referenced :
prec-size-induction
Rules used in proof :
introduction,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
instantiate,
extract_by_obid,
hypothesis,
sqequalRule,
thin,
sqequalHypSubstitution,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}[P:Type]. \mforall{}[a:Atom {}\mrightarrow{} P {}\mrightarrow{} ((P + P + Type) List)]. \mforall{}[Q:i:P {}\mrightarrow{} prec(lbl,p.a[lbl;p];i) {}\mrightarrow{} TYPE].
((\mforall{}i:P. \mforall{}x:prec(lbl,p.a[lbl;p];i).
((\mforall{}j:P. \mforall{}z:\{z:prec(lbl,p.a[lbl;p];j)| ||j;z|| < ||i;x||\} . Q[j;z]) {}\mRightarrow{} Q[i;x]))
{}\mRightarrow{} (\mforall{}i:P. \mforall{}x:prec(lbl,p.a[lbl;p];i). Q[i;x]))
Date html generated:
2019_06_20-PM-02_05_03
Last ObjectModification:
2019_03_25-PM-05_19_00
Theory : tuples
Home
Index