---

Step * 1 1 of Lemma local-class-equality


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))
BY
{ (InstLemma `list2extended-eo` [⌜Info⌝;⌜inputs @ [a]⌝;⌜x⌝]⋅ THENA (Auto THEN MemTypeCD THEN Auto')) }

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

---

Latex:

---

Latex:

1.  Info  :  Type
2.  x  :  Id
3.  inputs  :  Info  List
4.  a  :  Info
\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:
(InstLemma  `list2extended-eo`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}inputs  @  [a]\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  (Auto  THEN  MemTypeCD  THEN  Auto'))

---

Home Index