### Nuprl Lemma : AF-induction4

`∀T:Type. ∀R:T ⟶ T ⟶ ℙ.`
`  ∀Q:T ⟶ ℙ. 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]` TI: `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 :  all: `∀x:A. B[x]` uimplies: `b supposing a` member: `t ∈ T` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` implies: `P `` Q` uall: `∀[x:A]. B[x]` subtype_rel: `A ⊆r B` prop: `ℙ` trans: `Trans(T;x,y.E[x; y])` infix_ap: `x f y` so_lambda: `λ2x.t[x]` so_apply: `x[s]` and: `P ∧ Q` exists: `∃x:A. B[x]` cand: `A c∧ B` not: `¬A` false: `False` squash: `↓T` true: `True`
Lemmas referenced :  rel_plus-TI AF-induction3 rel_plus_wf rel_plus_trans exists_wf almost-full_wf all_wf not_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality sqequalRule lambdaEquality applyEquality functionExtensionality cumulativity independent_functionElimination isectElimination because_Cache hypothesis universeEquality independent_isectElimination functionEquality instantiate productEquality productElimination dependent_pairFormation independent_pairFormation voidElimination addLevel hyp_replacement equalitySymmetry levelHypothesis imageElimination natural_numberEquality imageMemberEquality baseClosed

Latex:
\mforall{}T:Type.  \mforall{}R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.
\mforall{}Q:T  {}\mrightarrow{}  \mBbbP{}.  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: 2016_10_21-AM-10_50_09
Last ObjectModification: 2016_07_12-AM-05_54_30

Theory : relations2

Home Index