Nuprl Lemma : list_of_lists_of_given_size_in_fin_spr_wf
[B:
List 
]. [k:]. (list_of_lists_of_given_size_in_fin_spr(B;k) 
List List)
Proof
Definitions occuring in Statement :
list_of_lists_of_given_size_in_fin_spr: list_of_lists_of_given_size_in_fin_spr(B;k),
nat: ,
uall: [x:A]. B[x],
member: t T,
function: x:A B[x]
Definitions :
uall: [x:A]. B[x],
member: t T,
list_of_lists_of_given_size_in_fin_spr: list_of_lists_of_given_size_in_fin_spr(B;k),
nat:
Lemmas :
Error :primrec_wf,
Error :list_wf,
Error :cons_wf,
Error :nil_wf,
l-union-list_wf,
list-deq_wf,
nat-deq_wf,
map_wf,
list_of_extensions_in_fin_spr_wf,
int_seg_wf,
nat_wf
\mforall{}[B:\mBbbN{} List {}\mrightarrow{} \mBbbN{}]. \mforall{}[k:\mBbbN{}]. (list\_of\_lists\_of\_given\_size\_in\_fin\_spr(B;k) \mmember{} \mBbbN{} List List)
Date html generated:
2013_03_20-AM-10_36_24
Last ObjectModification:
2013_03_18-PM-10_57_19
Home
Index