Nuprl Lemma : TC-ind-ext
∀[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 :
lifting-strict-spread,
has-value_wf_base,
base_wf,
is-exception_wf
\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_37
Last ObjectModification:
2015_06_19-PM-01_31_29
Home
Index