Nuprl Lemma : spr_choice_fun
g:
List 
. (spr(g) 
(
h: List . a: List. (((g a) = 0) ((g (a @ [h a])) = 0))))
Proof
Definitions occuring in Statement :
append: as @ bs,
nat: ,
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
apply: f a,
function: x:A B[x],
natural_number: $n,
equal: s = t
Definitions :
all: x:A. B[x],
implies: P Q,
member: t 
T,
nat: ,
and: P 
Q,
exists: x:A. B[x],
gt: i > j,
ifthenelse: if b then t else f fi ,
le: A 
B,
unit: Unit,
btrue: tt,
top: Top,
not: 
A,
false: False,
prop: 
,
so_lambda: 
x.t[x],
subtype: S 
T,
bfalse: ff,
true: True,
squash: 
T,
pi1: fst(t),
spr: spr(g),
uall: [x:A]. B[x],
bool: 
,
uimplies: b supposing a,
assert: 
b,
uiff: uiff(P;Q),
so_apply: x[s],
bnot: 
b,
or: P 
Q,
sq_type: SQType(T),
guard: {T},
nequal: a 
b T ,
it: 
Lemmas :
spr_wf,
Error :list_wf,
nat_wf,
eq_int_wf,
bool_wf,
eqtt_to_assert,
assert_of_eq_int,
pi1_wf_top,
le_wf,
exists_wf,
equal_wf,
append_wf,
Error :cons_wf,
Error :nil_wf,
gt_wf,
all_wf,
it_wf,
equal_subtype,
eqff_to_assert,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
Error :assert-bnot,
neg_assert_of_eq_int,
subtype_rel_set_simple,
and_wf,
Error :zero-le-nat,
top_wf
\mforall{}g:\mBbbN{} List {}\mrightarrow{} \mBbbN{}. (spr(g) {}\mRightarrow{} (\mexists{}h:\mBbbN{} List {}\mrightarrow{} \mBbbN{}. \mforall{}a:\mBbbN{} List. (((g a) = 0) {}\mRightarrow{} ((g (a @ [h a])) = 0))))
Date html generated:
2013_03_20-AM-10_32_18
Last ObjectModification:
2013_03_01-PM-05_55_10
Home
Index