---

Step * 1 1 of Lemma rec_dataflow_ap_lemma


1. a : Top@i
2. next : Top@i
3. s0 : Top@i
⊢ let s',ext = next[s0;a] 
  in <rec-dataflow(s';s,a.next[s;a]), ext> ~ let s',b = next[s0;a] 
                                             in <rec-dataflow(s';s,a.next[s;a]), b>
BY
{ Try (RW (AddrC [2] (IdC)) 0)⋅ }

1
1. a : Top@i
2. next : Top@i
3. s0 : Top@i
⊢ let s',ext = next[s0;a] 
  in <rec-dataflow(s';s,a.next[s;a]), ext> ~ let s',b = next[s0;a] 
                                             in <rec-dataflow(s';s,a.next[s;a]), b>

---

Latex:

---

Latex:

1.  a  :  Top@i
2.  next  :  Top@i
3.  s0  :  Top@i
\mvdash{}  let  s',ext  =  next[s0;a] 
    in  <rec-dataflow(s';s,a.next[s;a]),  ext>  \msim{}  let  s',b  =  next[s0;a] 
                                                                                          in  <rec-dataflow(s';s,a.next[s;a]),  b>


By

---

Latex:
Try  (RW  (AddrC  [2]  (IdC))  0)\mcdot{}

---

Home Index