### Nuprl Lemma : AF-uniform-induction4-ext

`∀T:Type. ∀R:T ⟶ T ⟶ ℙ.`
`  ∀Q:T ⟶ ℙ. uniform-TI(T;x,y.R[x;y];t.Q[t]) `
`  supposing ∃R':T ⟶ T ⟶ ℙ. (AFx,y:T.R'[x;y] ∧ (∀x,y:T.  (R+[x;y] `` (¬R'[x;y]))))`

Proof

Definitions occuring in Statement :  rel_plus: `R+` almost-full: `AFx,y:T.R[x; y]` uniform-TI: `uniform-TI(T;x,y.R[x; y];t.Q[t])` uimplies: `b supposing a` prop: `ℙ` so_apply: `x[s1;s2]` so_apply: `x[s]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` implies: `P `` Q` and: `P ∧ Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  member: `t ∈ T` AF-uniform-induction4 rel_plus-uniform-TI AF-uniform-induction3 AF-uniform-induction2 AF-uniform-induction
Lemmas referenced :  AF-uniform-induction4 rel_plus-uniform-TI AF-uniform-induction3 AF-uniform-induction2 AF-uniform-induction
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution equalityTransitivity equalitySymmetry

Latex:
\mforall{}T:Type.  \mforall{}R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.
\mforall{}Q:T  {}\mrightarrow{}  \mBbbP{}.  uniform-TI(T;x,y.R[x;y];t.Q[t])
supposing  \mexists{}R':T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.  (AFx,y:T.R'[x;y]  \mwedge{}  (\mforall{}x,y:T.    (R\msupplus{}[x;y]  {}\mRightarrow{}  (\mneg{}R'[x;y]))))

Date html generated: 2018_05_21-PM-00_52_15
Last ObjectModification: 2018_05_19-AM-06_40_45

Theory : relations2

Home Index