---

Step * 1 of Lemma rec_dataflow_ap_lemma


1. a : Top@i
2. next : Top@i
3. s0 : Top@i
⊢ rec-dataflow(s0;s,a.next[s;a])(a) ~ let s',b = next[s0;a] 
                                      in <rec-dataflow(s';s,a.next[s;a]), b>
BY
{ Try (RW (AddrC [1] (RecUnfoldC `rec-dataflow` ANDTHENC UnfoldC `dataflow-ap` ANDTHENC ReduceC)) 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{}  rec-dataflow(s0;s,a.next[s;a])(a)  \msim{}  let  s',b  =  next[s0;a] 
                                                                            in  <rec-dataflow(s';s,a.next[s;a]),  b>


By

---

Latex:
Try  (RW  (AddrC  [1]  (RecUnfoldC  `rec-dataflow`  ANDTHENC  UnfoldC  `dataflow-ap`  ANDTHENC  ReduceC))  0)\mcdot{}

---

Home Index