---

Step * of Lemma interface-predecessors-split

∀[Info:Type]
  ∀es:EO+(Info). ∀X:EClass(Top). ∀e:E(X). ∀A,B:E(X) List.
    (∃p:E(X)
      (p ≤loc e 
      ∧ (≤(X)(p) = A ∈ (E(X) List))
      ∧ (filter(λa.p <loc a;≤(X)(e)) = B ∈ (E(X) List))
      ∧ (p <loc e) supposing ¬↑null(B)
      ∧ (p = last(A) ∈ E))) supposing 
       ((¬↑null(A)) and 
       (≤(X)(e) = (A @ B) ∈ (E(X) List)))
BY
{ (InstLemma `iseg-interface-predecessors` []
   THEN RepeatFor 4 (ParallelLast')
   THEN Auto
   THEN (InstHyp [⌜A⌝] 5⋅ THENA Auto)
   THEN D -1
   THEN Thin (-1)
   THEN (D -1 THENA (With ⌜B⌝ (D 0)⋅ THEN Auto))
   THEN D -1
   THEN Auto
   THEN ParallelLast
   THEN Auto) }

1
1. Info : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. e : E(X)@i
5. ∀L:E(X) List
     (L ≤ ≤(X)(e)
     ⇐⇒ (↑null(L)) ∨ ((¬↑null(L)) ∧ (∃p:E(X). (p ≤loc e  ∧ (L = ≤(X)(p) ∈ (E(X) List)) ∧ (p = last(L) ∈ E)))))
6. A : E(X) List@i
7. B : E(X) List@i
8. ≤(X)(e) = (A @ B) ∈ (E(X) List)
9. ¬↑null(A)
10. ¬↑null(A)
11. p : E(X)
12. p ≤loc e 
13. A = ≤(X)(p) ∈ (E(X) List)
14. p = last(A) ∈ E
15. p ≤loc e 
16. ≤(X)(p) = A ∈ (E(X) List)
⊢ filter(λa.p <loc a;≤(X)(e)) = B ∈ (E(X) List)

2
1. Info : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. e : E(X)@i
5. ∀L:E(X) List
     (L ≤ ≤(X)(e)
     ⇐⇒ (↑null(L)) ∨ ((¬↑null(L)) ∧ (∃p:E(X). (p ≤loc e  ∧ (L = ≤(X)(p) ∈ (E(X) List)) ∧ (p = last(L) ∈ E)))))
6. A : E(X) List@i
7. B : E(X) List@i
8. ≤(X)(e) = (A @ B) ∈ (E(X) List)
9. ¬↑null(A)
10. ¬↑null(A)
11. p : E(X)
12. p = e ∈ E
13. A = ≤(X)(p) ∈ (E(X) List)
14. p = last(A) ∈ E
15. p = e ∈ E
16. ≤(X)(p) = A ∈ (E(X) List)
17. filter(λa.p <loc a;≤(X)(e)) = B ∈ (E(X) List)
18. ¬↑null(B)
⊢ (p <loc e)

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}e:E(X).  \mforall{}A,B:E(X)  List.
        (\mexists{}p:E(X)
            (p  \mleq{}loc  e 
            \mwedge{}  (\mleq{}(X)(p)  =  A)
            \mwedge{}  (filter(\mlambda{}a.p  <loc  a;\mleq{}(X)(e))  =  B)
            \mwedge{}  (p  <loc  e)  supposing  \mneg{}\muparrow{}null(B)
            \mwedge{}  (p  =  last(A))))  supposing 
              ((\mneg{}\muparrow{}null(A))  and 
              (\mleq{}(X)(e)  =  (A  @  B)))


By

---

Latex:
(InstLemma  `iseg-interface-predecessors`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}A\mkleeneclose{}]  5\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  Thin  (-1)
  THEN  (D  -1  THENA  (With  \mkleeneopen{}B\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto))
  THEN  D  -1
  THEN  Auto
  THEN  ParallelLast
  THEN  Auto)

---

Home Index