### Nuprl Lemma : hdf-compose1-transformation0

`∀[f,F:Top].`
`  (f o fix((λmk-hdf.(inl (λa.<mk-hdf, F[a]>)))) `
`  ~ fix((λmk-hdf.(inl (λa.simple-cbva-seq(λn.bag-map(f;F[a]);λout.<mk-hdf, out>;1))))))`

Proof

Definitions occuring in Statement :  hdf-compose1: `f o X` uall: `∀[x:A]. B[x]` top: `Top` so_apply: `x[s]` fix: `fix(F)` lambda: `λx.A[x]` pair: `<a, b>` inl: `inl x` natural_number: `\$n` sqequal: `s ~ t` bag-map: `bag-map(f;bs)` simple-cbva-seq: `simple-cbva-seq(L;F;m)`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` simple-cbva-seq: `simple-cbva-seq(L;F;m)` eq_int: `(i =z j)` subtract: `n - m` ifthenelse: `if b then t else f fi ` bfalse: `ff` mk_lambdas: `mk_lambdas(F;m)` cbva-seq: `cbva-seq(L;F;m)` all: `∀x:A. B[x]` top: `Top` callbyvalueall-seq: `callbyvalueall-seq(L;G;F;n;m)` le_int: `i ≤z j` lt_int: `i <z j` bnot: `¬bb` btrue: `tt` hdf-compose1: `f o X` mk-hdf: `mk-hdf(s,m.G[s; m];st.H[st];s0)` hdf-halted: `hdf-halted(P)` isr: `isr(x)` 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]` so_apply: `x[s]` uimplies: `b supposing a` strict4: `strict4(F)` and: `P ∧ Q` implies: `P `` Q` has-value: `(a)↓` prop: `ℙ` guard: `{T}` or: `P ∨ Q` squash: `↓T` hdf-run: `hdf-run(P)` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` hdf-ap: `X(a)` bag-map: `bag-map(f;bs)` map: `map(f;as)` list_ind: list_ind cons: `[a / b]` nil: `[]` it: `⋅` callbyvalueall: callbyvalueall evalall: `evalall(t)` empty-bag: `{}` hdf-halt: `hdf-halt()` 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: `ℕ` ge: `i ≥ j ` sq_type: `SQType(T)`

Latex:
\mforall{}[f,F:Top].
(f  o  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.<mk-hdf,  F[a]>))))
\msim{}  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.simple-cbva-seq(\mlambda{}n.bag-map(f;F[a]);\mlambda{}out.<mk-hdf,  out>1))))))

Date html generated: 2016_05_16-AM-10_45_38
Last ObjectModification: 2016_01_17-AM-11_10_15

Theory : halting!dataflow

Home Index