---

Step * of Lemma es-interface-history-pred

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A:Type]. ∀[X:EClass(A List)]. ∀[e:E].
  es-interface-history(es;X;e)
  = if e ∈b X then es-interface-history(es;X;pred(e)) @ X(e) else es-interface-history(es;X;pred(e)) fi 
  ∈ (A List) 
  supposing ¬↑first(e)
BY
{ (Auto
   THEN (RW (AddrC [2] (UnfoldC `es-interface-history`)) 0 THEN RW (AddrC [2] (UnfoldC `es-le-before`)) 0)
   THEN (RWO "mapfilter-append" 0 THENA Auto)
   THEN (RWO "concat_append" 0 THENA Auto)⋅) }

1
1. Info : Type
2. es : EO+(Info)
3. A : Type
4. X : EClass(A List)
5. e : E
6. ¬↑first(e)
⊢ (concat(mapfilter(λe.X(e);λe.e ∈b X;before(e))) @ concat(mapfilter(λe.X(e);λe.e ∈b X;[e])))
= if e ∈b X then es-interface-history(es;X;pred(e)) @ X(e) else es-interface-history(es;X;pred(e)) fi 
∈ (A List)

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A:Type].  \mforall{}[X:EClass(A  List)].  \mforall{}[e:E].
    es-interface-history(es;X;e)
    =  if  e  \mmember{}\msubb{}  X
        then  es-interface-history(es;X;pred(e))  @  X(e)
        else  es-interface-history(es;X;pred(e))
        fi   
    supposing  \mneg{}\muparrow{}first(e)


By

---

Latex:
(Auto
  THEN  (RW  (AddrC  [2]  (UnfoldC  `es-interface-history`))  0
              THEN  RW  (AddrC  [2]  (UnfoldC  `es-le-before`))  0
              )
  THEN  (RWO  "mapfilter-append"  0  THENA  Auto)
  THEN  (RWO  "concat\_append"  0  THENA  Auto)\mcdot{})

---

Home Index