Nuprl Lemma : TC-ind
∀[Dom:Type]. ∀[B:Dom ─→ ℙ]. ∀[R:Dom ─→ Dom ─→ ℙ].
((∀x,y:Dom. ((R x y) ⇒ (B x) ⇒ (B y))) ⇒ (∀x,y:Dom. (TC(λa,b.R a b)(x,y) ⇒ (B x) ⇒ (B 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-induction
\mforall{}[Dom:Type]. \mforall{}[B:Dom {}\mrightarrow{} \mBbbP{}]. \mforall{}[R:Dom {}\mrightarrow{} Dom {}\mrightarrow{} \mBbbP{}].
((\mforall{}x,y:Dom. ((R x y) {}\mRightarrow{} (B x) {}\mRightarrow{} (B y))) {}\mRightarrow{} (\mforall{}x,y:Dom. (TC(\mlambda{}a,b.R a b)(x,y) {}\mRightarrow{} (B x) {}\mRightarrow{} (B y))))
Date html generated:
2015_07_17-AM-07_52_33
Last ObjectModification:
2015_01_30-AM-01_13_21
Home
Index