Nuprl Lemma : hdf-sqequal8

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


Definitions occuring in Statement :  null: null(as) callbyvalueall: callbyvalueall 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) 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'>,  s'>  |  inr(y1)  =>  <mk-hdf  <X,  b>,  b>\000C  \msim{}  let  b  \mleftarrow{}{}  a
                                                                                                                                                    in  let  s'  \mleftarrow{}{}  case  null(b)
                                                                                                                                                            of  inl(x1)  =>
                                                                                                                                                            |  inr(y1)  =>
                                                                                                                                                          in  <mk-hdf  <X,  s'>,  s'>\000C)

Date html generated: 2016_05_16-AM-10_45_05
Last ObjectModification: 2016_01_17-AM-11_12_03

Theory : halting!dataflow

Home Index