---

Step * 2 1 of Lemma interface-predecessors-split


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)
BY
{ ((ApFunToHypEquands `Z' ⌈||Z||⌉ ⌈ℤ⌉ 8⋅ THENA Auto) THEN (RWO "length-append" (-1) THENA 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 = 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)
19. ||≤(X)(e)|| = (||A|| + ||B||) ∈ ℤ
⊢ (p <loc e)

---

Latex:

---

Latex:

1.  Info  :  Type
2.  es  :  EO+(Info)@i'
3.  X  :  EClass(Top)@i'
4.  e  :  E(X)@i
5.  \mforall{}L:E(X)  List
          (L  \mleq{}  \mleq{}(X)(e)
          \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}null(L))  \mvee{}  ((\mneg{}\muparrow{}null(L))  \mwedge{}  (\mexists{}p:E(X).  (p  \mleq{}loc  e    \mwedge{}  (L  =  \mleq{}(X)(p))  \mwedge{}  (p  =  last(L))))))
6.  A  :  E(X)  List@i
7.  B  :  E(X)  List@i
8.  \mleq{}(X)(e)  =  (A  @  B)
9.  \mneg{}\muparrow{}null(A)
10.  \mneg{}\muparrow{}null(A)
11.  p  :  E(X)
12.  p  =  e
13.  A  =  \mleq{}(X)(p)
14.  p  =  last(A)
15.  p  =  e
16.  \mleq{}(X)(p)  =  A
17.  filter(\mlambda{}a.p  <loc  a;\mleq{}(X)(e))  =  B
18.  \mneg{}\muparrow{}null(B)
\mvdash{}  (p  <loc  e)


By

---

Latex:
((ApFunToHypEquands  `Z'  \mkleeneopen{}||Z||\mkleeneclose{}  \mkleeneopen{}\mBbbZ{}\mkleeneclose{}  8\mcdot{}  THENA  Auto)  THEN  (RWO  "length-append"  (-1)  THENA  Auto))

---

Home Index