{ 
[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_finite: rel_finite(T;R),
rel_plus: 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),
nat: 
,
le: A 
B,
ge: i 
j ,
member: t 
T,
not: 
A,
false: False,
so_lambda: 
x y.t[x; y],
exists: 
x:A. B[x],
isl: isl(x),
iff: P 
Q,
assert: 
b,
btrue: tt,
bfalse: ff,
ifthenelse: if b then t else f fi ,
true: True,
and: P 
Q,
rev_implies: P Q,
or: P 
Q,
pi1: fst(t),
guard: {T},
int_seg: {i..j
},
cand: A c B,
lelt: i j < k,
top: Top,
subtype: S 
T,
strongwellfounded: SWellFounded(R[x; y]),
so_apply: x[s1;s2],
decidable: Dec(P),
uimplies: b supposing a,
l_member: (x l)
Lemmas :
nat_properties,
ge_wf,
nat_wf,
le_wf,
rel_finite_wf,
decidable_wf,
strongwellfounded_wf,
btrue_wf,
bfalse_wf,
true_wf,
false_wf,
iff_wf,
assert_wf,
filter_wf,
l_member_wf,
member_filter,
assert_witness,
select_wf,
length_wf1,
int_seg_wf,
select_member,
append_wf,
concat_wf,
map_wf,
upto_wf,
rel_plus_wf,
iff_transitivity,
member_append,
or_functionality_wrt_iff,
member-concat,
rel_plus_iff,
rel_star_wf,
and_functionality_wrt_iff,
rel-star-iff-rel-plus-or,
member_wf,
member_map,
member_upto2,
length_wf_nat,
top_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 R\msupplus{} y)))
Date html generated:
2011_08_16-AM-10_18_41
Last ObjectModification:
2011_06_18-AM-09_07_34
Home
Index