---

Step * of Lemma rec_dataflow_ap_lemma

∀a,next,s0:Top.  (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
{ (UnivCD THENA Auto) }

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

---

Latex:

---

Latex:
\mforall{}a,next,s0:Top.
    (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:
(UnivCD  THENA  Auto)

---

Home Index