### Nuprl Lemma : test-rel-connected

`∀T:Type. ∀R:T ⟶ T ⟶ ℙ. ∀x,y,z,w:T.  ((x (R^*) y) `` (y = z ∈ T) `` (z (R^*) w) `` (x (R^*) w))`

Proof

Definitions occuring in Statement :  rel_star: `R^*` prop: `ℙ` infix_ap: `x f y` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` infix_ap: `x f y` uall: `∀[x:A]. B[x]` rel-connected: `x──R⟶y` guard: `{T}` uimplies: `b supposing a`
Lemmas referenced :  rel_star_wf equal_wf rel-connected_transitivity rel-connected_weakening
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation applyEquality cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis functionEquality cumulativity universeEquality independent_functionElimination independent_isectElimination

Latex:
\mforall{}T:Type.  \mforall{}R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.  \mforall{}x,y,z,w:T.
((x  (R\^{}*)  y)  {}\mRightarrow{}  (y  =  z)  {}\mRightarrow{}  (z  (R\^{}*)  w)  {}\mRightarrow{}  (x  rel\_star(T;  R)  w))

Date html generated: 2016_05_13-PM-04_19_21
Last ObjectModification: 2015_12_26-AM-11_33_36

Theory : relations

Home Index