### Nuprl Lemma : rel-immediate-exists

`∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].`
`  (SWellFounded(R x y) `` (∀x,y:T.  Dec(∃z:T. ((R x z) ∧ (R z y)))) `` (∀y:T. ((∃x:T. (R x y)) `` (∃x:T. (R! x y)))))`

Proof

Definitions occuring in Statement :  rel-immediate: `R!` strongwellfounded: `SWellFounded(R[x; y])` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` all: `∀x:A. B[x]` member: `t ∈ T` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` so_lambda: `λ2x y.t[x; y]` subtype_rel: `A ⊆r B` so_apply: `x[s1;s2]` exists: `∃x:A. B[x]` rel_implies: `R1 => R2` infix_ap: `x f y` iff: `P `⇐⇒` Q` and: `P ∧ Q`
Lemmas referenced :  rel-immediate-rel-plus exists_wf all_wf decidable_wf and_wf strongwellfounded_wf rel-rel-plus rel_plus_iff rel-immediate_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin because_Cache hypothesisEquality independent_functionElimination hypothesis sqequalRule lambdaEquality applyEquality universeEquality functionEquality cumulativity productElimination dependent_functionElimination dependent_pairFormation

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
(SWellFounded(R  x  y)
{}\mRightarrow{}  (\mforall{}x,y:T.    Dec(\mexists{}z:T.  ((R  x  z)  \mwedge{}  (R  z  y))))
{}\mRightarrow{}  (\mforall{}y:T.  ((\mexists{}x:T.  (R  x  y))  {}\mRightarrow{}  (\mexists{}x:T.  (R!  x  y)))))

Date html generated: 2016_05_15-PM-04_54_27
Last ObjectModification: 2015_12_27-PM-02_31_49

Theory : general

Home Index