### 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)`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` ifthenelse: `if b then t else f fi ` hdf-compose2: `X o Y` hdf-halted: `hdf-halted(P)` bor: `p ∨bq` hdf-ap: `X(a)` mk-hdf: `mk-hdf(s,m.G[s; m];st.H[st];s0)` hdf-run: `hdf-run(P)` hdf-halt: `hdf-halt()` isr: `isr(x)` btrue: `tt` bfalse: `ff` so_lambda: `so_lambda(x,y,z,w.t[x; y; z; w])` so_apply: `x[s1;s2;s3;s4]` so_lambda: `λ2x.t[x]` top: `Top` so_apply: `x[s]` uimplies: `b supposing a` strict4: `strict4(F)` and: `P ∧ Q` all: `∀x:A. B[x]` implies: `P `` Q` has-value: `(a)↓` prop: `ℙ` guard: `{T}` or: `P ∨ Q` squash: `↓T` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` int_seg: `{i..j-}` lelt: `i ≤ j < k` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` decidable: `Dec(P)` subtype_rel: `A ⊆r B` le: `A ≤ B` less_than': `less_than'(a;b)` nat: `ℕ` lt_int: `i <z j` subtract: `n - m` nat_plus: `ℕ+` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` uiff: `uiff(P;Q)` true: `True` eq_int: `(i =z j)` ge: `i ≥ j ` sq_type: `SQType(T)`

Latex:
\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: 2016_05_16-AM-10_47_32
Last ObjectModification: 2016_01_17-AM-11_11_17

Theory : halting!dataflow

Home Index