Nuprl Lemma : pv8_p2_first_unoccupied_wf
pv8_p2_first_unoccupied() 
List 
Proof not projected
Definitions occuring in Statement :
pv8_p2_first_unoccupied: pv8_p2_first_unoccupied(),
member: t T,
function: x:A B[x],
list: type List,
int:
Definitions :
so_lambda: 
x y.t[x; y],
cand: A c
B,
and: P Q,
pv8_p2_first_unoccupied: pv8_p2_first_unoccupied(),
member: t T,
prop: 
,
all: 
x:A. B[x],
so_apply: x[s1;s2],
uall: [x:A]. B[x]
Lemmas :
int-deq_wf,
eqof_wf,
ifthenelse_wf,
permutation_wf,
l_member_wf,
le_wf,
sorted-by_wf,
quicksort-int_wf,
list_accum_wf
pv8\_p2\_first\_unoccupied() \mmember{} \mBbbZ{} List {}\mrightarrow{} \mBbbZ{}
Date html generated:
2012_02_20-PM-07_39_41
Last ObjectModification:
2012_02_06-PM-03_12_24
Home
Index