Nuprl Lemma : hdf-buffer-transformation3

∀[init,s,L,S,G:Top]. ∀[m:ℕ].
  (hdf-buffer(fix((λmk-hdf,s. (inl (λa.cbva_seq(L[s;a]; λg.<mk-hdf S[s;a;g], G[s;a;g]>; m))))) s;init) 
  ~ fix((λmk-hdf,s. (inl (λa.cbva_seq(λn.if (n =z m)
                                         then mk_lambdas_fun(λg.∪f∈G[fst(s);a;g].∪b∈snd(s).f b;m)
                                         else L[fst(s);a] n
                                         fi ; λg.<mk-hdf 
                                                  <S[fst(s);a;partial_ap(g;m + 1;m)]
                                                  , if bag-null(select_fun_last(g;m))
                                                    then snd(s)
                                                    else select_fun_last(g;m)
                                                    fi 
                                                  >
                                                 , select_fun_last(g;m)
                                                 >; m + 1))))) 
    <s, init>)


Proof



Definitions occuring in Statement :  hdf-buffer: hdf-buffer(X;bs),  nat: ℕ,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  uall: ∀[x:A]. B[x],  top: Top,  so_apply: x[s1;s2;s3],  so_apply: x[s1;s2],  pi1: fst(t),  pi2: snd(t),  apply: f a,  fix: fix(F),  lambda: λx.A[x],  pair: <a, b>,  inl: inl x,  add: n + m,  natural_number: $n,  sqequal: s ~ t,  bag-combine: ∪x∈bs.f[x],  bag-null: bag-null(bs),  select_fun_last: select_fun_last(g;m),  partial_ap: partial_ap(g;n;m),  mk_lambdas_fun: mk_lambdas_fun(F;m),  cbva_seq: cbva_seq(L; F; m)
Lemmas :  lifting-strict-spread,  has-value_wf_base,  base_wf,  base_sq,  lifting-strict-int_eq,  top_wf,  pair-eta,  lifting-strict-decide,  strict4-spread,  lifting-strict-callbyvalueall,  nat_properties,  less_than_transitivity1,  less_than_irreflexivity,  ge_wf,  less_than_wf,  nat_wf,  fun_exp0_lemma,  strictness-apply,  bottom-sqle,  decidable__le,  subtract_wf,  false_wf,  not-ge-2,  less-iff-le,  condition-implies-le,  minus-one-mul,  zero-add,  minus-add,  minus-minus,  add-associates,  add-swap,  add-commutes,  add_functionality_wrt_le,  add-zero,  le-add-cancel,  fun_exp_unroll_1,  int_subtype_base,  le_wf,  set_subtype_base,  cbva_seq_extend,  cbva_seq-spread
\mforall{}[init,s,L,S,G:Top].  \mforall{}[m:\mBbbN{}].
    (hdf-buffer(fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(L[s;a];  \mlambda{}g.<mk-hdf  S[s;a;g],  G[s;a;g]>  m)))))  s;ini\000Ct) 
    \msim{}  fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(\mlambda{}n.if  (n  =\msubz{}  m)
                                                                                  then  mk\_lambdas\_fun(\mlambda{}g.\mcup{}f\mmember{}G[fst(s);a;g].\mcup{}b\mmember{}snd(s).f  b;m)
                                                                                  else  L[fst(s);a]  n
                                                                                  fi  ;  \mlambda{}g.<mk-hdf 
                                                                                                    <S[fst(s);a;partial\_ap(g;m  +  1;m)]
                                                                                                    ,  if  bag-null(select\_fun\_last(g;m))
                                                                                                        then  snd(s)
                                                                                                        else  select\_fun\_last(g;m)
                                                                                                        fi 
                                                                                                    >
                                                                                                  ,  select\_fun\_last(g;m)
                                                                                                  >  m  +  1))))) 
        <s,  init>)


Date html generated: 2015_07_17-AM-08_08_50
Last ObjectModification: 2015_04_23-PM-10_57_41

Home Index