{ 
[T:Type]. [R:T 
T 
].
(SWellFounded(x R y)
(x,y:T. Dec(x R y))
rel_finite(T;R)
rel_finite(T;
x,y.(x (R^*) y))) }
{ Proof }
Definitions occuring in Statement :
decidable: Dec(P),
uall: [x:A]. B[x],
prop: ,
infix_ap: x f y,
all: x:A. B[x],
implies: P Q,
lambda: x.A[x],
function: x:A B[x],
universe: Type,
rel_star: R^*,
rel_finite: rel_finite(T;R),
strongwellfounded: SWellFounded(R[x; y])
Definitions :
uall: [x:A]. B[x],
prop: ,
implies: P Q,
infix_ap: x f y,
all: x:A. B[x],
rel_finite: rel_finite(T;R),
member: t 
T,
exists: 
x:A. B[x],
so_lambda: 
x y.t[x; y],
or: P 
Q,
guard: {T},
iff: P 
Q,
and: P 
Q,
rev_implies: P Q,
so_apply: x[s1;s2]
Lemmas :
rel_plus_finite,
rel-star-iff-rel-plus-or,
cons_member,
rel_star_wf,
l_member_wf,
rel_finite_wf,
decidable_wf,
strongwellfounded_wf
\mforall{}[T:Type]. \mforall{}[R:T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}].
(SWellFounded(x R y)
{}\mRightarrow{} (\mforall{}x,y:T. Dec(x R y))
{}\mRightarrow{} rel\_finite(T;R)
{}\mRightarrow{} rel\_finite(T;\mlambda{}x,y.(x rel\_star(T; R) y)))
Date html generated:
2011_08_16-AM-10_18_46
Last ObjectModification:
2011_06_18-AM-09_07_38
Home
Index