Nuprl Lemma : hdf-memory-transformation2

[init,L,G:Top]. ∀[m:ℕ].
  (hdf-memory(fix((λmk-hdf.(inl a.cbva_seq(L[a]; λg.<mk-hdf, G[g]>m)))));init) 
  fix((λmk-hdf,s. (inl a.cbva_seq(λn.if (n =z 1)
                                           then mk_lambdas_fun(λg.if bag-null(select_fun_last(g;m))
                                                                  then s
                                                                  else select_fun_last(g;m)
                                                                  fi ;m 1)
                                         if (n =z m) then mk_lambdas_fun(λg.∪f∈G[g].bag-map(f;s);m)
                                         else L[a] n
                                         fi ; λg.<mk-hdf select_fun_last(g;m 1), s>2))))) 
    init)


Proof




Definitions occuring in Statement :  hdf-memory: hdf-memory(X;bs) nat: ifthenelse: if then else fi  eq_int: (i =z j) uall: [x:A]. B[x] top: Top so_apply: x[s] apply: a fix: fix(F) lambda: λx.A[x] pair: <a, b> inl: inl x add: m natural_number: $n sqequal: t bag-combine: x∈bs.f[x] bag-null: bag-null(bs) bag-map: bag-map(f;bs) select_fun_last: select_fun_last(g;m) mk_lambdas_fun: mk_lambdas_fun(F;m) cbva_seq: cbva_seq(L; F; m)
Lemmas :  lifting-strict-spread strict4-spread lifting-strict-int_eq has-value_wf_base base_wf base_sq lifting-strict-callbyvalueall nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf less_than_wf nat_wf top_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 cbva_seq-spread cbva_seq_extend not-le-2 sq_stable__le le_wf subtype_base_sq int_subtype_base set_subtype_base
\mforall{}[init,L,G:Top].  \mforall{}[m:\mBbbN{}].
    (hdf-memory(fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.cbva\_seq(L[a];  \mlambda{}g.<mk-hdf,  G[g]>  m)))));init) 
    \msim{}  fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(\mlambda{}n.if  (n  =\msubz{}  m  +  1)
                                                                                      then  mk\_lambdas\_fun(\mlambda{}g.if  bag-null(select\_fun\_last(g;m))
                                                                                                                                    then  s
                                                                                                                                    else  select\_fun\_last(g;m)
                                                                                                                                    fi  ;m  +  1)
                                                                                  if  (n  =\msubz{}  m)  then  mk\_lambdas\_fun(\mlambda{}g.\mcup{}f\mmember{}G[g].bag-map(f;s);m)
                                                                                  else  L[a]  n
                                                                                  fi  ;  \mlambda{}g.<mk-hdf  select\_fun\_last(g;m  +  1),  s>  m  +  2))))) 
        init)



Date html generated: 2015_07_17-AM-08_09_14
Last ObjectModification: 2015_04_30-PM-00_52_15

Home Index