Nuprl Lemma : gammaFIM_unfold1
g,h:
List 
. a: List.
(gammaFIM(a;g;h)
= if (||a|| =
0) then []
if (g (gammaFIM(firstn(||a|| - 1;a);g;h) @ [last(a)]) = 0) then gammaFIM(firstn(||a|| - 1;a);g;h) @ [last(a)]
else gammaFIM(firstn(||a|| - 1;a);g;h) @ [h gammaFIM(firstn(||a|| - 1;a);g;h)]
fi )
Proof
Definitions occuring in Statement :
gammaFIM: gammaFIM(a;g;h),
firstn: firstn(n;as),
length: ||as||,
append: as @ bs,
eq_int: (i = j),
ifthenelse: if b then t else f fi ,
nat: ,
all: x:A. B[x],
apply: f a,
function: x:A B[x],
subtract: n - m,
natural_number: $n,
equal: s = t,
last: last(L)
Definitions :
all: x:A. B[x],
nat: ,
member: t 
T,
so_lambda: 
x.t[x],
uall: [x:A]. B[x],
uimplies: b supposing a,
so_apply: x[s]
Lemmas :
gammaFIM_unfold,
gammaFIM_wf,
subtype_rel_dep_function,
subtype_rel_weakening,
ext-eq_weakening,
subtype_rel_set_simple,
le_wf,
Error :list_wf,
nat_wf
\mforall{}g,h:\mBbbN{} List {}\mrightarrow{} \mBbbN{}. \mforall{}a:\mBbbN{} List.
(gammaFIM(a;g;h)
= if (||a|| =\msubz{} 0) then []
if (g (gammaFIM(firstn(||a|| - 1;a);g;h) @ [last(a)]) =\msubz{} 0)
then gammaFIM(firstn(||a|| - 1;a);g;h) @ [last(a)]
else gammaFIM(firstn(||a|| - 1;a);g;h) @ [h gammaFIM(firstn(||a|| - 1;a);g;h)]
fi )
Date html generated:
2013_03_20-AM-10_33_08
Last ObjectModification:
2013_03_09-AM-00_38_51
Home
Index