Nuprl Lemma : list_of_extensions_in_fin_spr_wf
[B:
List 
]. [b: List]. (list_of_extensions_in_fin_spr(B;b) 
List List)
Proof
Definitions occuring in Statement :
list_of_extensions_in_fin_spr: list_of_extensions_in_fin_spr(B;b),
nat: ,
uall: [x:A]. B[x],
member: t T,
function: x:A B[x]
Definitions :
uall: [x:A]. B[x],
nat: ,
member: t T,
list_of_extensions_in_fin_spr: list_of_extensions_in_fin_spr(B;b),
ifthenelse: if b then t else f fi ,
all: x:A. B[x],
implies: P 
Q,
btrue: tt,
and: P 
Q,
int_seg: {i..j
},
lelt: i 
j < k,
so_lambda: 
x.t[x],
bfalse: ff,
bool: 
,
unit: Unit,
uimplies: b supposing a,
uiff: uiff(P;Q),
prop: 
,
so_apply: x[s],
it: 
Lemmas :
list-in-fin_spr_wf,
bool_wf,
eqtt_to_assert,
mklist_wf,
Error :zero-le-nat,
le_wf,
append_wf,
Error :cons_wf,
subtype_rel_sets,
lelt_wf,
Error :nil_wf,
int_seg_wf,
uiff_transitivity,
equal_wf,
assert_wf,
bnot_wf,
not_wf,
eqff_to_assert,
assert_of_bnot,
Error :list_wf,
nat_wf
\mforall{}[B:\mBbbN{} List {}\mrightarrow{} \mBbbN{}]. \mforall{}[b:\mBbbN{} List]. (list\_of\_extensions\_in\_fin\_spr(B;b) \mmember{} \mBbbN{} List List)
Date html generated:
2013_03_20-AM-10_36_03
Last ObjectModification:
2013_03_18-PM-10_21_24
Home
Index