### Nuprl Lemma : hdf-with-state-pair-left-axiom

`∀[L,S,G,init:Top]. ∀[m:ℕ].`
`  (fix((λmk-hdf,s. (inl (λa.cbva_seq(L[s;a]; λg.<mk-hdf <Ax, S[s;a;g]>, G[s;a;g]>; m))))) <Ax, init> ~ fix((λmk-hdf,s. (\000Cinl (λa.cbva_seq(L[<Ax, s>;a]; λg.<mk-hdf S[<Ax, s>;a;g], G[<Ax, s>;a;g]>; m))))) init)`

Proof

Definitions occuring in Statement :  nat: `ℕ` uall: `∀[x:A]. B[x]` top: `Top` so_apply: `x[s1;s2;s3]` so_apply: `x[s1;s2]` apply: `f a` fix: `fix(F)` lambda: `λx.A[x]` pair: `<a, b>` inl: `inl x` sqequal: `s ~ t` axiom: `Ax` cbva_seq: `cbva_seq(L; F; m)`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` 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` all: `∀x:A. B[x]` top: `Top` and: `P ∧ Q` prop: `ℙ` decidable: `Dec(P)` or: `P ∨ Q` nat_plus: `ℕ+` so_apply: `x[s1;s2]` so_apply: `x[s1;s2;s3]`

Latex:
\mforall{}[L,S,G,init:Top].  \mforall{}[m:\mBbbN{}].
(fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(L[s;a];  \mlambda{}g.<mk-hdf  <Ax,  S[s;a;g]>,  G[s;a;g]>  m)))))  <Ax,  init>\000C  \msim{}  fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(L[<Ax,  s>a];  \mlambda{}g.<mk-hdf  S[<Ax,  s>a;g],  G[<Ax,  s>a;g]>  m))))\000C)  init)

Date html generated: 2016_05_16-AM-10_50_35
Last ObjectModification: 2016_01_17-AM-11_07_58

Theory : halting!dataflow

Home Index