Nuprl Lemma : hdf-state-transformation2

∀[init,L,G:Top]. ∀[m:ℕ].
  (hdf-state(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 m + 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), select_fun_last(g;m + 1)>; m + 2)))))\000C 
    init)


Proof



Definitions occuring in Statement :  hdf-state: hdf-state(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[s],  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),  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-state(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)
                                                                                                  ,  select\_fun\_last(g;m  +  1)
                                                                                                  >  m  +  2))))) 
        init)


Date html generated: 2015_07_17-AM-08_08_52
Last ObjectModification: 2015_04_30-PM-00_52_12

Home Index