Nuprl Lemma : prec-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)| prec_sub+(P;lbl,p.a[lbl;p]) <j, z> <i, x>} .\000C 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_sub+: prec_sub+(P;lbl,p.a[lbl; p]),
prec: prec(lbl,p.a[lbl; p];i),
list: T List,
uall: ∀[x:A]. B[x],
so_apply: x[s1;s2],
all: ∀x:A. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
pair: <a, b>,
union: left + right,
atom: Atom,
universe: Type
Definitions unfolded in proof :
member: t ∈ T,
genrec-ap: genrec-ap,
prec-induction,
prec-size-induction-ext
Lemmas referenced :
prec-induction,
prec-size-induction-ext
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)| prec\_sub+(P;lbl,p.a[lbl;p]) <j, z> <i, x>\} . Q[j;z]) {}\mRightarrow{}\000C 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_14_30
Last ObjectModification:
2019_03_25-PM-08_52_10
Theory : tuples
Home
Index