Nuprl Lemma : hdf-buffer-transformation2

[init,L,G:Top]. ∀[m:ℕ].
  (hdf-buffer(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) then mk_lambdas_fun(λg.∪f∈G[g].∪b∈s.f b;m) else L[a] fi ;
                                      λg.<mk-hdf if bag-null(select_fun_last(g;m)) then else select_fun_last(g;m) fi 
                                         select_fun_last(g;m)
                                         >1))))) 
    init)


Proof




Definitions occuring in Statement :  hdf-buffer: hdf-buffer(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) 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 has-value_wf_base base_wf is-exception_wf lifting-strict-int_eq top_wf lifting-strict-decide strict4-spread lifting-strict-callbyvalueall nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf less_than_wf strictness-apply lifting-strict-less lifting-strict-ispair lifting-strict-isaxiom strictness-decide 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 le_weakening2 le_wf eq_int_wf bool_wf eqtt_to_assert assert_of_eq_int le_weakening eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int nat_wf cbva_seq-spread cbva_seq_extend set_subtype_base int_subtype_base
\mforall{}[init,L,G:Top].  \mforall{}[m:\mBbbN{}].
    (hdf-buffer(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)
                                                                                  then  mk\_lambdas\_fun(\mlambda{}g.\mcup{}f\mmember{}G[g].\mcup{}b\mmember{}s.f  b;m)
                                                                                  else  L[a]  n
                                                                                  fi  ;  \mlambda{}g.<mk-hdf 
                                                                                                    if  bag-null(select\_fun\_last(g;m))
                                                                                                    then  s
                                                                                                    else  select\_fun\_last(g;m)
                                                                                                    fi 
                                                                                                  ,  select\_fun\_last(g;m)
                                                                                                  >  m  +  1))))) 
        init)



Date html generated: 2015_07_17-AM-08_08_48
Last ObjectModification: 2015_06_19-PM-01_00_23

Home Index