Nuprl Lemma : list_of_lists_of_given_size_in_fin_spr1
B: List  . k:. a: List.  (((a  fspr(B)))  (||a|| = k)  (a  list_of_lists_of_given_size_in_fin_spr(B;k)))
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), 
list-in-fin_spr: (a  fspr(B)), 
length: ||as||, 
assert: b, 
nat: , 
all: x:A. B[x], 
iff: P  Q, 
and: P  Q, 
function: x:A  B[x], 
equal: s = t, 
l_member: (x  l)
Definitions : 
all: x:A. B[x], 
list_of_lists_of_given_size_in_fin_spr: list_of_lists_of_given_size_in_fin_spr(B;k), 
member: t  T, 
primrec: primrec(n;b;c), 
implies: P  Q, 
ge: i  j , 
le: A  B, 
not: A, 
false: False, 
nat: , 
iff: P  Q, 
and: P  Q, 
rev_implies: P  Q, 
prop: , 
nil: Error :nil, 
length: ||as||, 
so_lambda: x.t[x], 
list_ind: Error :list_ind, 
it: , 
assert: b, 
ifthenelse: if b then t else f fi , 
eq_int: (i = j), 
btrue: tt, 
true: True, 
top: Top, 
bfalse: ff, 
exists: x:A. B[x], 
squash: T, 
cand: A c B, 
int_iseg: {i...j}, 
guard: {T}, 
uall: [x:A]. B[x], 
bool: , 
unit: Unit, 
uimplies: b supposing a, 
sq_type: SQType(T), 
so_apply: x[s], 
uiff: uiff(P;Q), 
bnot: b, 
or: P  Q, 
nequal: a  b  T , 
cons: Error :cons
Lemmas : 
nat_wf, 
Error :list_wf, 
nat_properties, 
ge_wf, 
member_singleton, 
Error :isaxiom_wf_list, 
bool_wf, 
Error :unit_subtype_list, 
Error :axiom-list, 
Error :nil_wf, 
Error :product_subtype_list, 
Error :non-axiom-list, 
non_neg_length, 
length_wf_nat, 
assert_wf, 
list-in-fin_spr_wf, 
le_wf, 
l_member_wf, 
Error :cons_wf, 
subtype_base_sq, 
set_subtype_base, 
int_subtype_base, 
list_subtype_base, 
list-in-fin_spr_unfold, 
equal_wf, 
Error :primrec-unroll, 
eq_int_wf, 
eqtt_to_assert, 
assert_of_eq_int, 
eqff_to_assert, 
bool_cases_sqequal, 
bool_subtype_base, 
Error :assert-bnot, 
neg_assert_of_eq_int, 
l-union-list_wf, 
list-deq_wf, 
nat-deq_wf, 
map_wf, 
list_of_extensions_in_fin_spr_wf, 
top_wf, 
list_of_lists_of_given_size_in_fin_spr_wf, 
Error :non_null_iff_length, 
subtype_rel_list, 
subtype_top, 
length_wf, 
Error :firstn_last_sq, 
length_firstn, 
firstn_wf, 
list-in-fin_spr_unfold_prp, 
last_wf, 
member-l-union-list, 
member_map, 
and_wf, 
length_firstn_eq, 
list_of_extensions_in_fin_spr1, 
assert_functionality_wrt_uiff, 
append_wf, 
squash_wf, 
true_wf, 
firstn_last, 
bnot_wf, 
not_wf, 
bool_cases, 
iff_transitivity, 
iff_weakening_uiff, 
assert_of_bnot, 
Error :zero-le-nat
\mforall{}B:\mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}.  \mforall{}k:\mBbbN{}.  \mforall{}a:\mBbbN{}  List.
    ((\muparrow{}(a  \mmember{}  fspr(B)))  \mwedge{}  (||a||  =  k)  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  list\_of\_lists\_of\_given\_size\_in\_fin\_spr(B;k)))
Date html generated:
2013_03_20-AM-10_36_43
Last ObjectModification:
2013_03_19-PM-07_18_01
Home
Index