Nuprl Lemma : hdf-sqequal8-3

  (let b ⟵ a
   in case null(b) of inl(x1) => let s' ⟵ in <mk-hdf <X, s'>x> inr(y1) => <mk-hdf <X, b>x> let b ⟵ a
                                                                         in let s' ⟵ if null(b) then else fi 
                                                                            in <mk-hdf <X, s'>x>)


Definitions occuring in Statement :  null: null(as) callbyvalueall: callbyvalueall ifthenelse: if then else fi  uall: [x:A]. B[x] top: Top apply: a pair: <a, b> decide: case of inl(x) => s[x] inr(y) => t[y] sqequal: 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: supposing a strict4: strict4(F) and: P ∧ Q all: x:A. B[x] implies:  Q has-value: (a)↓ prop: guard: {T} or: P ∨ Q squash: T bfalse: ff btrue: tt callbyvalueall: callbyvalueall evalall: evalall(t) ifthenelse: if then else fi  has-valueall: has-valueall(a)

    (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
                                                                                                                                                        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