Nuprl Lemma : TC-trans
∀[Dom:Type]. ∀[R:Dom ─→ Dom ─→ ℙ]. ∀[x,y,z:Dom]. (TC(λa,b.R a b)(x,y) ⇒ TC(λa,b.R a b)(y,z) ⇒ TC(λa,b.R a b)(x,z))
Proof
Definitions occuring in Statement :
TC: TC(λx,y.F[x; y])(a,b),
uall: ∀[x:A]. B[x],
prop: ℙ,
implies: P ⇒ Q,
apply: f a,
function: x:A ─→ B[x],
universe: Type
Lemmas :
transitive-closure-transitive,
TC_wf
\mforall{}[Dom:Type]. \mforall{}[R:Dom {}\mrightarrow{} Dom {}\mrightarrow{} \mBbbP{}]. \mforall{}[x,y,z:Dom].
(TC(\mlambda{}a,b.R a b)(x,y) {}\mRightarrow{} TC(\mlambda{}a,b.R a b)(y,z) {}\mRightarrow{} TC(\mlambda{}a,b.R a b)(x,z))
Date html generated:
2015_07_17-AM-07_52_36
Last ObjectModification:
2015_01_30-AM-01_13_20
Home
Index