Nuprl Lemma : hdf-compose1-transformation3

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


Proof




Definitions occuring in Statement :  hdf-compose1: X nat: ifthenelse: if then else fi  eq_int: (i =z j) uall: [x:A]. B[x] top: Top so_apply: x[s1;s2;s3] so_apply: x[s1;s2] apply: a fix: fix(F) lambda: λx.A[x] pair: <a, b> inl: inl x add: m natural_number: $n sqequal: t bag-map: bag-map(f;bs) select_fun_ap: select_fun_ap(g;n;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-decide has-value_wf_base base_wf lifting-strict-int_eq top_wf lifting-strict-spread 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_diverge 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 set_subtype_base le_wf int_subtype_base
\mforall{}[f,L,S,G,init:Top].  \mforall{}[m:\mBbbN{}].
    (f  o  (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)))))  init) 
    \msim{}  fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(\mlambda{}n.if  (n  =\msubz{}  m)
                                                                                  then  mk\_lambdas\_fun(\mlambda{}g.bag-map(f;G[s;a;g]);m)
                                                                                  else  L[s;a]  n
                                                                                  fi  ;  \mlambda{}g.<mk-hdf  S[s;a;partial\_ap(g;m  +  1;m)]
                                                                                                  ,  select\_fun\_ap(g;m  +  1;m)
                                                                                                  >  m  +  1))))) 
        init)



Date html generated: 2015_07_17-AM-08_08_41
Last ObjectModification: 2015_01_27-PM-00_08_00

Home Index