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