Nuprl Lemma : transitive-closure-minimal-ext

`∀[A:Type]. ∀[R,Q:A ⟶ A ⟶ ℙ].  (R => Q `` Trans(A;x,y.x Q y) `` TC(R) => Q)`

Proof

Definitions occuring in Statement :  transitive-closure: `TC(R)` rel_implies: `R1 => R2` trans: `Trans(T;x,y.E[x; y])` uall: `∀[x:A]. B[x]` prop: `ℙ` infix_ap: `x f y` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  member: `t ∈ T` spreadn: spread3 transitive-closure-minimal
Lemmas referenced :  transitive-closure-minimal
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution equalityTransitivity equalitySymmetry

Latex:
\mforall{}[A:Type].  \mforall{}[R,Q:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].    (R  =>  Q  {}\mRightarrow{}  Trans(A;x,y.x  Q  y)  {}\mRightarrow{}  TC(R)  =>  Q)

Date html generated: 2018_05_21-PM-00_51_42
Last ObjectModification: 2018_05_19-AM-06_40_14

Theory : relations2

Home Index