---

Step * 1 1 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)
6. e : E
7. loc(e) = x ∈ Id
8. (inputs @ [a]) = map(λe.info(e);before(e) @ [e]) ∈ (Info List)
⊢ (loc(e) = x ∈ Id) ∧ (map(λx.info(x);before(e)) = inputs ∈ (Info List)) ∧ (info(e) = a ∈ Info)
BY
{ ((RWO "map_append" (-1) THENM Reduce (-1)) THENA Auto) }

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);before(e)) @ [info(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.  es  :  EO+(Info)
6.  e  :  E
7.  loc(e)  =  x
8.  (inputs  @  [a])  =  map(\mlambda{}e.info(e);before(e)  @  [e])
\mvdash{}  (loc(e)  =  x)  \mwedge{}  (map(\mlambda{}x.info(x);before(e))  =  inputs)  \mwedge{}  (info(e)  =  a)


By

---

Latex:
((RWO  "map\_append"  (-1)  THENM  Reduce  (-1))  THENA  Auto)

---

Home Index