{ 
[T:Type]
((x,y:T. Dec(x = y))
([R:T 
T 
]
(SWellFounded(x R y)
rel_finite(T;R)
(x,y:T. Dec(x R y))
([P:T ]
((x:T. Dec(P[x]))
(y:T. Dec(
x:T. ((x (R^*) y) 
P[x])))))))) }
{ Proof }
Definitions occuring in Statement :
decidable: Dec(P),
uall: [x:A]. B[x],
prop: ,
infix_ap: x f y,
so_apply: x[s],
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
and: P Q,
function: x:A B[x],
universe: Type,
equal: s = t,
rel_star: R^*,
rel_finite: rel_finite(T;R),
strongwellfounded: SWellFounded(R[x; y])
Definitions :
uall: [x:A]. B[x],
implies: P Q,
all: x:A. B[x],
prop: ,
infix_ap: x f y,
so_apply: x[s],
member: t 
T,
so_lambda: 
x.t[x],
so_lambda: x y.t[x; y],
rel_finite: rel_finite(T;R),
so_apply: x[s1;s2]
Lemmas :
decidable__rel_star,
rel_star_finite,
decidable__exists-rel_finite,
rel_star_wf,
decidable_wf,
rel_finite_wf,
strongwellfounded_wf
\mforall{}[T:Type]
((\mforall{}x,y:T. Dec(x = y))
{}\mRightarrow{} (\mforall{}[R:T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}]
(SWellFounded(x R y)
{}\mRightarrow{} rel\_finite(T;R)
{}\mRightarrow{} (\mforall{}x,y:T. Dec(x R y))
{}\mRightarrow{} (\mforall{}[P:T {}\mrightarrow{} \mBbbP{}]. ((\mforall{}x:T. Dec(P[x])) {}\mRightarrow{} (\mforall{}y:T. Dec(\mexists{}x:T. ((x rel\_star(T; R) y) \mwedge{} P[x]))))))))
Date html generated:
2011_08_16-AM-10_19_05
Last ObjectModification:
2011_06_18-AM-09_08_00
Home
Index