Nuprl Lemma : TC-min
∀[Dom:Type]. ∀[R,Q:Dom ─→ Dom ─→ ℙ].
((∀x,y,z:Dom. ((Q x y) ⇒ (Q y z) ⇒ (Q x z)))
⇒ (∀x,y:Dom. ((R x y) ⇒ (Q x y)))
⇒ (∀x,y:Dom. (TC(λa,b.R a b)(x,y) ⇒ (Q 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 :
TC_wf,
all_wf,
transitive-closure-minimal,
rel_implies_wf
\mforall{}[Dom:Type]. \mforall{}[R,Q:Dom {}\mrightarrow{} Dom {}\mrightarrow{} \mBbbP{}].
((\mforall{}x,y,z:Dom. ((Q x y) {}\mRightarrow{} (Q y z) {}\mRightarrow{} (Q x z)))
{}\mRightarrow{} (\mforall{}x,y:Dom. ((R x y) {}\mRightarrow{} (Q x y)))
{}\mRightarrow{} (\mforall{}x,y:Dom. (TC(\mlambda{}a,b.R a b)(x,y) {}\mRightarrow{} (Q x y))))
Date html generated:
2015_07_17-AM-07_52_34
Last ObjectModification:
2015_01_30-AM-01_13_28
Home
Index