{ 
[P:
]
((n:. Dec(P[n]))
(n:
((y:. 
P[y] supposing y 
n)
(
y:
((y n) 
P[y] (x:. P[x] supposing (y < x) (x n))))))) }
{ Proof }
Definitions occuring in Statement :
nat: ,
decidable: Dec(P),
uimplies: b supposing a,
uall: [x:A]. B[x],
prop: ,
so_apply: x[s],
le: A B,
all: x:A. B[x],
exists: x:A. B[x],
not: A,
implies: P Q,
or: P Q,
and: P Q,
less_than: a < b,
function: x:A B[x]
Definitions :
uall: [x:A]. B[x],
prop: ,
implies: P Q,
all: x:A. B[x],
so_apply: x[s],
uimplies: b supposing a,
exists: x:A. B[x],
and: P Q,
member: t 
T,
or: P Q,
le: A B,
not: A,
false: False,
ge: i 
j ,
nat: ,
guard: {T},
decidable: Dec(P),
sq_type: SQType(T)
Lemmas :
nat_wf,
decidable_wf,
nat_properties,
ge_wf,
le_wf,
not_wf,
subtype_base_sq,
int_subtype_base
\mforall{}[P:\mBbbN{} {}\mrightarrow{} \mBbbP{}]
((\mforall{}n:\mBbbN{}. Dec(P[n]))
{}\mRightarrow{} (\mforall{}n:\mBbbN{}
((\mforall{}y:\mBbbN{}. \mneg{}P[y] supposing y \mleq{} n)
\mvee{} (\mexists{}y:\mBbbN{}. ((y \mleq{} n) \mwedge{} P[y] \mwedge{} (\mforall{}x:\mBbbN{}. \mneg{}P[x] supposing (y < x) \mwedge{} (x \mleq{} n)))))))
Date html generated:
2011_08_16-AM-11_19_52
Last ObjectModification:
2011_06_20-AM-00_24_50
Home
Index