Nuprl Lemma : TC_wf
∀[Dom:Type]. ∀[F:Dom ─→ Dom ─→ ℙ]. ∀[a,b:Dom]. (TC(λx,y.F[x;y])(a,b) ∈ ℙ)
Proof
Definitions occuring in Statement :
TC: TC(λx,y.F[x; y])(a,b),
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s1;s2],
member: t ∈ T,
function: x:A ─→ B[x],
universe: Type
Lemmas :
transitive-closure_wf
\mforall{}[Dom:Type]. \mforall{}[F:Dom {}\mrightarrow{} Dom {}\mrightarrow{} \mBbbP{}]. \mforall{}[a,b:Dom]. (TC(\mlambda{}x,y.F[x;y])(a,b) \mmember{} \mBbbP{})
Date html generated:
2015_07_17-AM-07_52_32
Last ObjectModification:
2015_01_30-AM-01_13_14
Home
Index