Nuprl Lemma : FIM26_5
B:
((s,z,w:. ((B s z) 
(w 
z ) (B s w)))
(b:. ((s:. ((s 
b) (
z:. (B s z)))) (z:. s:. ((s b) (B s z))))))
Proof
Definitions occuring in Statement :
nat: ,
prop: ,
ge: i j ,
le: A B,
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
apply: f a,
function: x:A B[x]
Definitions :
all: x:A. B[x],
nat: ,
prop: ,
implies: P Q,
ge: i j ,
exists: x:A. B[x],
member: t 
T,
so_lambda: 
x.t[x],
le: A B,
not: 
A,
false: False,
imax: imax(a;b),
or: P 
Q,
guard: {T},
ifthenelse: if b then t else f fi ,
btrue: tt,
bfalse: ff,
uall: [x:A]. B[x],
so_apply: x[s],
sq_type: SQType(T),
uimplies: b supposing a,
iff: P 
Q,
and: P 
Q,
rev_implies: P Q,
bool: 
,
unit: Unit,
assert: 
b,
uiff: uiff(P;Q),
bnot: 
b,
true: True,
it: 
Lemmas :
all_wf,
nat_wf,
le_wf,
subtype_rel_set_simple,
exists_wf,
subtype_rel_self,
ge_wf,
nat_properties,
subtype_base_sq,
set_subtype_base,
int_subtype_base,
imax_wf,
Error :zero-le-nat,
imax_ub,
le_int_wf,
bool_wf,
eqtt_to_assert,
assert_of_le_int,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
bool_subtype_base,
Error :assert-bnot
\mforall{}B:\mBbbN{} {}\mrightarrow{} \mBbbN{} {}\mrightarrow{} \mBbbP{}
((\mforall{}s,z,w:\mBbbN{}. ((B s z) {}\mRightarrow{} (w \mgeq{} z ) {}\mRightarrow{} (B s w)))
{}\mRightarrow{} (\mforall{}b:\mBbbN{}. ((\mforall{}s:\mBbbN{}. ((s \mleq{} b) {}\mRightarrow{} (\mexists{}z:\mBbbN{}. (B s z)))) {}\mRightarrow{} (\mexists{}z:\mBbbN{}. \mforall{}s:\mBbbN{}. ((s \mleq{} b) {}\mRightarrow{} (B s z))))))
Date html generated:
2013_03_20-AM-10_34_50
Last ObjectModification:
2013_03_09-PM-05_45_02
Home
Index