### Nuprl Lemma : hdf-sqequal6-2

`∀[s,F,G:Top].`
`  (fix((λmk-hdf,s0. (inl (λa.let bs' ⟵ ⋃f∈[λb.[G[a;b]]].⋃b∈s0.f b`
`                             in <mk-hdf case null(bs') of inl() => s0 | inr() => bs', F[s0;bs']>)))) `
`   [s] ~ fix((λmk-hdf,s0. (inl (λa.let bs' ⟵ G[a;s0] in <mk-hdf bs', F[[s0];[bs']]>)))) s)`

Proof

Definitions occuring in Statement :  null: `null(as)` cons: `[a / b]` nil: `[]` callbyvalueall: callbyvalueall uall: `∀[x:A]. B[x]` top: `Top` so_apply: `x[s1;s2]` apply: `f a` fix: `fix(F)` lambda: `λx.A[x]` pair: `<a, b>` decide: `case b of inl(x) => s[x] | inr(y) => t[y]` inl: `inl x` sqequal: `s ~ t` bag-combine: `⋃x∈bs.f[x]`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` nat: `ℕ` implies: `P `` Q` false: `False` ge: `i ≥ j ` uimplies: `b supposing a` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` not: `¬A` top: `Top` and: `P ∧ Q` prop: `ℙ` fun_exp: `f^n` primrec: `primrec(n;b;c)` decidable: `Dec(P)` or: `P ∨ Q` nat_plus: `ℕ+` so_lambda: `λ2x.t[x]` so_apply: `x[s]` subtype_rel: `A ⊆r B` null: `null(as)` cons: `[a / b]` bfalse: `ff` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]`

Latex:
\mforall{}[s,F,G:Top].
(fix((\mlambda{}mk-hdf,s0.  (inl  (\mlambda{}a.let  bs'  \mleftarrow{}{}  \mcup{}f\mmember{}[\mlambda{}b.[G[a;b]]].\mcup{}b\mmember{}s0.f  b
in  <mk-hdf  case  null(bs')  of  inl()  =>  s0  |  inr()  =>  bs',  F[s0;bs']>))))\000C
[s]  \msim{}  fix((\mlambda{}mk-hdf,s0.  (inl  (\mlambda{}a.let  bs'  \mleftarrow{}{}  G[a;s0]  in  <mk-hdf  bs',  F[[s0];[bs']]>))))  s)

Date html generated: 2016_05_16-AM-10_51_28
Last ObjectModification: 2016_01_17-AM-11_09_25

Theory : halting!dataflow

Home Index