### Nuprl Lemma : hdf-compose2-transformation1-2-0

`∀[L1,L2,G1,G2,init,S:Base]. ∀[m1,m2:ℕ+].`
`  (fix((λmk-hdf.(inl (λa.cbva_seq(L1[a]; λg.<mk-hdf, G1[g]>; m1)))))`
`   o (fix((λmk-hdf,s. (inl (λa.cbva_seq(L2[a]; λg.<mk-hdf S[s], G2[g]>; m2))))) init) `
`  ~ fix((λmk-hdf,s. (inl (λa.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_fun(λg1.mk_lambdas_fun(λg2.∪f∈G1[g1].∪b∈G2[g2].f b;m2);m1)`
`                                         fi ; λg.<mk-hdf S[s], select_fun_last(g;m1 + m2)>; (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]` select_fun_last: `select_fun_last(g;m)` mk_lambdas: `mk_lambdas(F;m)` mk_lambdas_fun: `mk_lambdas_fun(F;m)` cbva_seq: `cbva_seq(L; F; m)`
\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[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[s],  select\_fun\_last(g;m1  +  m2)>  (m1
+  m2)
+  1)))))
init)

Date html generated: 2015_07_17-AM-08_09_39
Last ObjectModification: 2015_04_23-PM-10_58_00

Home Index