Nuprl Lemma : hdf-compose2-transformation1

∀[L1,L2,init,S:Base]. ∀[m1,m2:ℕ+].
  (fix((λmk-hdf.(inl (λa.simple-cbva-seq(L1[a];λout.<mk-hdf, out>;m1)))))
   o (fix((λmk-hdf,s. (inl (λa.simple-cbva-seq(L2[a];λout.<mk-hdf S[s], out>;m2))))) init) 
  ~ fix((λmk-hdf,s. (inl (λa.simple-cbva-seq(λ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(λfs.mk_lambdas(λbs.∪f∈fs.∪b∈bs.f b;m2 - 1);m1 - 1)
                                                fi ;λout.<mk-hdf S[s], out>;(m1 + m2) + 1))))) 
    init)


Proof



Definitions occuring in Statement :  hdf-compose2: X o Y,  nat_plus: ℕ+,  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  uall: ∀[x:A]. B[x],  so_apply: x[s],  apply: f a,  fix: fix(F),  lambda: λx.A[x],  pair: <a, b>,  inl: inl x,  subtract: n - m,  add: n + m,  natural_number: $n,  base: Base,  sqequal: s ~ t,  bag-combine: ∪x∈bs.f[x],  simple-cbva-seq: simple-cbva-seq(L;F;m),  mk_lambdas: mk_lambdas(F;m)
Lemmas :  lifting-strict-spread,  top_wf,  has-value_wf_base,  base_wf,  base_sq,  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,  lifting-strict-less,  simple-cbva-seq-spread,  simple-cbva-seq-extend-2,  simple-cbva-seq-combine,  decidable__lt,  less-iff-le,  condition-implies-le,  minus-add,  minus-one-mul,  zero-add,  add-commutes,  add_functionality_wrt_le,  add-associates,  add-zero,  le-add-cancel,  less_than_wf,  decide_bfalse_lemma,  lifting-strict-int_eq,  general_add_assoc,  simple-cbva-seq-list-case2,  nat_plus_subtype_nat,  simple-cbva-seq-sqequal-n,  set_subtype_base,  int_subtype_base,  subtype_base_sq,  add-swap,  decidable__le,  not-le-2,  minus-zero,  minus-minus,  le-add-cancel2,  lelt_wf,  not-equal-2,  le-add-cancel-alt,  nat_wf,  nat_plus_wf,  all_wf,  sqequal_n_wf,  int_seg_subtype-nat,  set_wf,  primrec-wf2,  sq_stable__le,  add-mul-special,  zero-mul
\mforall{}[L1,L2,init,S:Base].  \mforall{}[m1,m2:\mBbbN{}\msupplus{}].
    (fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.simple-cbva-seq(L1[a];\mlambda{}out.<mk-hdf,  out>m1)))))
      o  (fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.simple-cbva-seq(L2[a];\mlambda{}out.<mk-hdf  S[s],  out>m2)))))  init) 
    \msim{}  fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.simple-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(\mlambda{}fs.mk\_lambdas(\mlambda{}bs.\mcup{}f\mmember{}fs.\mcup{}b\mmember{}bs.f 
                                                                                                                                                                                              b;m2 
                                                                                                                                        -  1);m1  -  1)
                                                                                                fi  ;\mlambda{}out.<mk-hdf  S[s],  out>(m1  +  m2)  +  1))))) 
        init)


Date html generated: 2015_07_17-AM-08_09_36
Last ObjectModification: 2015_04_23-PM-10_58_07

Home Index