Nuprl Lemma : hdf-compose2-transformation1-2-1

[L1,L2,G1,G2,init,S:Base]. ∀[m1,m2:ℕ+].
  (fix((λmk-hdf.(inl a.cbva_seq(L1[a]; λg.<mk-hdf, G1[g]>m1)))))
   (fix((λmk-hdf,s. (inl a.cbva_seq(L2[a]; λg.<mk-hdf S[g;s], G2[g]>m2))))) init) 
  fix((λmk-hdf,s. (inl a.cbva_seq(λn.if n <m1 then L1[a] n
                                         if n <m1 m2 then mk_lambdas(L2[a] (n m1);m1)
                                         else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.∪f∈G1[g1].∪b∈G2[g2].f b;m2);m1)
                                         fi ; λg.<mk-hdf S[partial_ap_gen(g;(m1 m2) 1;m1;m2);s]
                                                 select_fun_last(g;m1 m2)
                                                 >(m1 m2) 1))))) 
    init)


Proof




Definitions occuring in Statement :  hdf-compose2: Y nat_plus: + ifthenelse: if then else fi  lt_int: i <j uall: [x:A]. B[x] so_apply: x[s1;s2] so_apply: x[s] apply: a fix: fix(F) lambda: λx.A[x] pair: <a, b> inl: inl x subtract: m add: m natural_number: $n base: Base sqequal: t bag-combine: x∈bs.f[x] select_fun_last: select_fun_last(g;m) partial_ap_gen: partial_ap_gen(g;n;s;m) mk_lambdas: mk_lambdas(F;m) mk_lambdas_fun: mk_lambdas_fun(F;m) cbva_seq: cbva_seq(L; F; m)
Lemmas :  lifting-strict-spread top_wf has-value_wf_base base_wf base_sq lifting-strict-less pair-eta lifting-strict-decide strict4-spread lifting-strict-callbyvalueall less_than_transitivity1 less_than_irreflexivity int_seg_wf decidable__equal_int subtype_rel-int_seg false_wf le_weakening subtract_wf int_seg_properties le_wf cbva_seq-spread nat_plus_subtype_nat cbva_seq_extend cbva_seq-combine decidable__le not-le-2 less-iff-le condition-implies-le minus-add minus-one-mul zero-add add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel decide_bfalse_lemma lifting-strict-int_eq decidable__lt general_add_assoc cbva_seq-list-case2 cbva_seq-sqequal-n set_subtype_base less_than_wf int_subtype_base partial_ap_of_partial_ap_gen1 minus-zero minus-minus le-add-cancel2 add-mul-special zero-mul le-add-cancel-alt lelt_wf select_fun_ap_is_last1 subtype_base_sq not-equal-2 nat_wf nat_plus_wf all_wf sqequal_n_wf int_seg_subtype-nat set_wf primrec-wf2 sq_stable__le
\mforall{}[L1,L2,G1,G2,init,S:Base].  \mforall{}[m1,m2:\mBbbN{}\msupplus{}].
    (fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.cbva\_seq(L1[a];  \mlambda{}g.<mk-hdf,  G1[g]>  m1)))))
      o  (fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(L2[a];  \mlambda{}g.<mk-hdf  S[g;s],  G2[g]>  m2)))))  init) 
    \msim{}  fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(\mlambda{}n.if  n  <z  m1  then  L1[a]  n
                                                                                  if  n  <z  m1  +  m2  then  mk\_lambdas(L2[a]  (n  -  m1);m1)
                                                                                  else  mk\_lambdas\_fun(\mlambda{}g1.mk\_lambdas\_fun(\mlambda{}g2.\mcup{}f\mmember{}G1[g1].
                                                                                                                                                                        \mcup{}b\mmember{}G2[g2].
                                                                                                                                                                        f  b;m2);m1)
                                                                                  fi  ;  \mlambda{}g.<mk-hdf  S[partial\_ap\_gen(g;(m1  +  m2)  +  1;m1;m2);s]
                                                                                                  ,  select\_fun\_last(g;m1  +  m2)
                                                                                                  >  (m1  +  m2)  +  1))))) 
        init)



Date html generated: 2015_07_17-AM-08_15_15
Last ObjectModification: 2015_04_23-PM-10_58_04

Home Index