### Nuprl Lemma : hdf-sqequal8-3

`∀[mk-hdf,a,s,X,x:Top].`
`  (let b ⟵ a`
`   in case null(b) of inl(x1) => let s' ⟵ s in <mk-hdf <X, s'>, x> | inr(y1) => <mk-hdf <X, b>, x> ~ let b ⟵ a`
`                                                                         in let s' ⟵ if null(b) then s else b fi `
`                                                                            in <mk-hdf <X, s'>, x>)`

Proof

Definitions occuring in Statement :  null: `null(as)` callbyvalueall: callbyvalueall ifthenelse: `if b then t else f fi ` uall: `∀[x:A]. B[x]` top: `Top` apply: `f a` pair: `<a, b>` decide: `case b of inl(x) => s[x] | inr(y) => t[y]` sqequal: `s ~ t`
Definitions unfolded in proof :  null: `null(as)` uall: `∀[x:A]. B[x]` so_lambda: `so_lambda(x,y,z,w.t[x; y; z; w])` member: `t ∈ T` 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` bfalse: `ff` btrue: `tt` callbyvalueall: callbyvalueall evalall: `evalall(t)` ifthenelse: `if b then t else f fi ` has-valueall: `has-valueall(a)`

Latex:
\mforall{}[mk-hdf,a,s,X,x:Top].
(let  b  \mleftarrow{}{}  a
in  case  null(b)  of  inl(x1)  =>  let  s'  \mleftarrow{}{}  s  in  <mk-hdf  <X,  s'>,  x>  |  inr(y1)  =>  <mk-hdf  <X,  b>,  x>  \000C\msim{}  let  b  \mleftarrow{}{}  a
in  let  s'  \mleftarrow{}{}  if  null(b)
then  s
else  b
fi
in  <mk-hdf  <X,  s'>,  x>)

Date html generated: 2016_05_16-AM-10_45_11
Last ObjectModification: 2016_01_17-AM-11_13_02

Theory : halting!dataflow

Home Index