---

Step * of Lemma local-class-equality

∀[Info,A:Type]. ∀[X:EClass(A)].
  ∀p,q:LocalClass(X).
    p = q ∈ (Id ⟶ hdataflow(Info;A)) 
    supposing ∀i:Id. ∀inputs:Info List.  hdf-halted(p i*(inputs)) = hdf-halted(q i*(inputs))
BY
{ (Auto THEN DVar `p' THEN DVar `q' THEN Ext THEN Auto THEN BLemma `hdataflow-equal` THEN Auto) }

1
1. Info : Type
2. A : Type
3. X : EClass(A)
4. p : Id ⟶ hdataflow(Info;A)@i'
5. ∀es:EO+(Info). ∀e:E.  (X(e) = (snd(p loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(A))@i'
6. q : Id ⟶ hdataflow(Info;A)@i'
7. ∀es:EO+(Info). ∀e:E.  (X(e) = (snd(q loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(A))@i'
8. ∀i:Id. ∀inputs:Info List.  hdf-halted(p i*(inputs)) = hdf-halted(q i*(inputs))
9. x : Id
10. inputs : Info List
11. hdf-halted(p x*(inputs)) = hdf-halted(q x*(inputs))
12. a : Info
⊢ hdf-out(p x*(inputs);a) = hdf-out(q x*(inputs);a) ∈ bag(A)

---

Latex:

---

Latex:
\mforall{}[Info,A:Type].  \mforall{}[X:EClass(A)].
    \mforall{}p,q:LocalClass(X).
        p  =  q  supposing  \mforall{}i:Id.  \mforall{}inputs:Info  List.    hdf-halted(p  i*(inputs))  =  hdf-halted(q  i*(inputs))


By

---

Latex:
(Auto  THEN  DVar  `p'  THEN  DVar  `q'  THEN  Ext  THEN  Auto  THEN  BLemma  `hdataflow-equal`  THEN  Auto)

---

Home Index