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: 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:  Q and: P ∧ Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  all: x:A. B[x] uimplies: supposing a member: t ∈ T so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] implies:  Q uall: [x:A]. B[x] subtype_rel: A ⊆B prop: trans: Trans(T;x,y.E[x; y]) infix_ap: y so_lambda: λ2x.t[x] so_apply: x[s] and: P ∧ Q exists: x:A. B[x] cand: 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