Nuprl Lemma : initseg_sum0
h:
. t: List. (initseg_sum(0;[h / t]) = h)
Proof
Definitions occuring in Statement :
initseg_sum: initseg_sum(r;L),
cons: [a / b],
list: T List,
all: x:A. B[x],
natural_number: $n,
int: ,
equal: s = t
Definitions :
member: t 
T,
all: x:A. B[x],
initseg_sum: initseg_sum(r;L),
btrue: tt,
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
firstn: firstn(n;as),
l_sum: l_sum(L),
uall: [x:A]. B[x],
uimplies: b supposing a,
subtype_rel: A 
r B
Lemmas :
list_wf,
subtype_top,
top_wf,
subtype_rel_list,
first0
\mforall{}h:\mBbbZ{}. \mforall{}t:\mBbbZ{} List. (initseg\_sum(0;[h / t]) = h)
Date html generated:
2014_03_27-PM-01_47_23
Last ObjectModification:
2013_11_04-AM-09_40_56
Home
Index