---

Step * 1 1 1 of Lemma local-class-equality


1. Info : Type
2. x : Id
3. inputs : Info List
4. a : Info
5. ∃es:EO+(Info). ∃e:E. ((loc(e) = x ∈ Id) ∧ ((inputs @ [a]) = map(λe.info(e);≤loc(e)) ∈ (Info List)))
⊢ ∃es:EO+(Info). ∃e:E. ((loc(e) = x ∈ Id) ∧ (map(λx.info(x);before(e)) = inputs ∈ (Info List)) ∧ (info(e) = a ∈ Info))
BY
{ (RepeatFor 2 (ParallelLast) THEN SplitAndHyps) }

1
1. Info : Type
2. x : Id
3. inputs : Info List
4. a : Info
5. es : EO+(Info)
6. e : E
7. loc(e) = x ∈ Id
8. (inputs @ [a]) = map(λe.info(e);≤loc(e)) ∈ (Info List)
⊢ (loc(e) = x ∈ Id) ∧ (map(λx.info(x);before(e)) = inputs ∈ (Info List)) ∧ (info(e) = a ∈ Info)

---

Latex:

---

Latex:

1.  Info  :  Type
2.  x  :  Id
3.  inputs  :  Info  List
4.  a  :  Info
5.  \mexists{}es:EO+(Info).  \mexists{}e:E.  ((loc(e)  =  x)  \mwedge{}  ((inputs  @  [a])  =  map(\mlambda{}e.info(e);\mleq{}loc(e))))
\mvdash{}  \mexists{}es:EO+(Info).  \mexists{}e:E.  ((loc(e)  =  x)  \mwedge{}  (map(\mlambda{}x.info(x);before(e))  =  inputs)  \mwedge{}  (info(e)  =  a))


By

---

Latex:
(RepeatFor  2  (ParallelLast)  THEN  SplitAndHyps)

---

Home Index