Nuprl Lemma : fin_spr_as_list2
f:
. B: List . ((f 
fspr(B)) 
(x:. (
(mklist(x;f) fspr(B)))))
Proof
Definitions occuring in Statement :
list-in-fin_spr: (a fspr(B)),
in_fin_spr: (f fspr(B)),
assert: b,
nat: ,
all: x:A. B[x],
implies: P Q,
function: x:A B[x],
mklist: mklist(n;f)
Definitions :
all: x:A. B[x],
implies: P Q,
member: t T,
mklist: mklist(n;f),
assert: b,
list-in-fin_spr: (a fspr(B)),
ifthenelse: if b then t else f fi ,
list_ind_reverse: Error :list_ind_reverse,
eq_int: (i =
j),
length: ||as||,
list_ind: Error :list_ind,
primrec: primrec(n;b;c),
nil: Error :nil,
it: 
,
btrue: tt,
true: True,
le: A 
B,
ge: i 
j ,
not: 
A,
false: False,
nat_plus: 
,
top: Top,
nat: ,
and: P 
Q,
int_seg: {i..j
},
so_lambda: 
x.t[x],
lelt: i j < k,
cand: A c B,
in_fin_spr: (f fspr(B)),
uall: [x:A]. B[x],
iff: P 
Q,
prop: 
,
uimplies: b supposing a,
so_apply: x[s],
rev_implies: P Q,
guard: {T}
Lemmas :
nat_wf,
in_fin_spr_wf,
Error :list_wf,
nat_properties,
ge_wf,
Error :mklist_add1,
list-in-fin_spr_unfold_prp,
mklist_wf,
le_wf,
subtype_rel_dep_function,
int_seg_wf,
subtype_rel_sets,
lelt_wf
\mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. \mforall{}B:\mBbbN{} List {}\mrightarrow{} \mBbbN{}. ((f \mmember{} fspr(B)) {}\mRightarrow{} (\mforall{}x:\mBbbN{}. (\muparrow{}(mklist(x;f) \mmember{} fspr(B)))))
Date html generated:
2013_03_20-AM-10_35_39
Last ObjectModification:
2013_03_18-PM-04_59_03
Home
Index