---

Step * 1 of Lemma local-class-equality


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)
BY
{ (Assert ⌈∃es:EO+(Info)
            ∃e:E. ((loc(e) = x ∈ Id) ∧ (map(λx.info(x);before(e)) = inputs ∈ (Info List)) ∧ (info(e) = a ∈ Info))⌉⋅
   THEN Try ((ExRepD
              THEN AllHyps h.(InstHyp [⌈es⌉;⌈e⌉] h⋅ THENA Complete (Auto)) 
              THEN SubstFor ⌈x⌉ 0⋅
              THEN (SubstFor ⌈inputs⌉ 0⋅ THENA Auto)
              THEN (SubstFor ⌈a⌉ 0⋅ THENA Auto)
              THEN Unfold `hdf-out` 0
              THEN Auto))
   THEN All Thin) }

1
1. Info : Type
2. x : Id
3. inputs : Info List
4. a : Info
⊢ ∃es:EO+(Info). ∃e:E. ((loc(e) = x ∈ Id) ∧ (map(λx.info(x);before(e)) = inputs ∈ (Info List)) ∧ (info(e) = a ∈ Info))

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  X  :  EClass(A)
4.  p  :  Id  {}\mrightarrow{}  hdataflow(Info;A)@i'
5.  \mforall{}es:EO+(Info).  \mforall{}e:E.    (X(e)  =  (snd(p  loc(e)*(map(\mlambda{}x.info(x);before(e)))(info(e)))))@i'
6.  q  :  Id  {}\mrightarrow{}  hdataflow(Info;A)@i'
7.  \mforall{}es:EO+(Info).  \mforall{}e:E.    (X(e)  =  (snd(q  loc(e)*(map(\mlambda{}x.info(x);before(e)))(info(e)))))@i'
8.  \mforall{}i:Id.  \mforall{}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
\mvdash{}  hdf-out(p  x*(inputs);a)  =  hdf-out(q  x*(inputs);a)


By

---

Latex:
(Assert  \mkleeneopen{}\mexists{}es:EO+(Info).  \mexists{}e:E.  ((loc(e)  =  x)  \mwedge{}  (map(\mlambda{}x.info(x);before(e))  =  inputs)  \mwedge{}  (info(e)  =  a))\mkleeneclose{}
  \mcdot{}
  THEN  Try  ((ExRepD
                        THEN  AllHyps  h.(InstHyp  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]  h\mcdot{}  THENA  Complete  (Auto)) 
                        THEN  SubstFor  \mkleeneopen{}x\mkleeneclose{}  0\mcdot{}
                        THEN  (SubstFor  \mkleeneopen{}inputs\mkleeneclose{}  0\mcdot{}  THENA  Auto)
                        THEN  (SubstFor  \mkleeneopen{}a\mkleeneclose{}  0\mcdot{}  THENA  Auto)
                        THEN  Unfold  `hdf-out`  0
                        THEN  Auto))
  THEN  All  Thin)

---

Home Index