Nuprl Lemma : gammaFIM_fun_id
g,h: List  .
  (spr(g)
   (a: List. (((g a) = 0)  ((g (a @ [h a])) = 0)))
   ((g []) = 0)
   (f:  . ((f  spr(g))  (f = (n.gammaFIM(mklist(n + 1;f);g;h)[n])))))
Proof
Definitions occuring in Statement : 
gammaFIM: gammaFIM(a;g;h), 
in_spr: (f  spr(g)), 
select: l[i], 
append: as @ bs, 
nat: , 
all: x:A. B[x], 
implies: P  Q, 
apply: f a, 
lambda: x.A[x], 
function: x:A  B[x], 
add: n + m, 
natural_number: $n, 
equal: s = t, 
mklist: mklist(n;f)
Definitions : 
all: x:A. B[x], 
nat: , 
implies: P  Q, 
member: t  T, 
prop: , 
le: A  B, 
not: A, 
false: False, 
so_lambda: x.t[x], 
int_seg: {i..j}, 
squash: T, 
true: True, 
lelt: i  j < k, 
and: P  Q, 
cand: A c B, 
rev_implies: P  Q, 
iff: P  Q, 
uall: [x:A]. B[x], 
so_apply: x[s], 
uimplies: b supposing a, 
in_spr: (f  spr(g)), 
guard: {T}
Lemmas : 
in_spr_wf, 
nat_wf, 
equal_wf, 
Error :nil_wf, 
le_wf, 
all_wf, 
Error :list_wf, 
append_wf, 
Error :cons_wf, 
spr_wf, 
select_wf, 
gammaFIM_wf, 
mklist_wf, 
subtype_rel_dep_function, 
int_seg_wf, 
subtype_rel_sets, 
lelt_wf, 
squash_wf, 
length_wf, 
gammaFIM_id, 
gammaFIM_equi_length_mklist, 
mklist_select
\mforall{}g,h:\mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}.
    (spr(g)
    {}\mRightarrow{}  (\mforall{}a:\mBbbN{}  List.  (((g  a)  =  0)  {}\mRightarrow{}  ((g  (a  @  [h  a]))  =  0)))
    {}\mRightarrow{}  ((g  [])  =  0)
    {}\mRightarrow{}  (\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((f  \mmember{}  spr(g))  {}\mRightarrow{}  (f  =  (\mlambda{}n.gammaFIM(mklist(n  +  1;f);g;h)[n])))))
Date html generated:
2013_03_20-AM-10_33_48
Last ObjectModification:
2013_03_16-PM-07_58_15
Home
Index