---

Step * 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 ≤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)
BY
{ (Symmetry
   THEN ((InstLemma `iseg-remainder-as-filter` 
          [⌜E(X)⌝;⌜λx,y. (x <loc y)⌝;⌜A⌝;⌜≤(X)(e)⌝;⌜B⌝;⌜λx,y. x <loc y⌝]⋅
         THENM (Reduce (-1) THEN HypSubst' -4 0 THEN Auto)⋅
         )
         THENA (Auto
                THEN Try ((BLemma `es-interface-predecessors-sorted-by-locl` THEN Auto))
                THEN Try ((D 0 THEN Reduce 0 THEN Auto THEN RelRST THEN Auto)⋅)
                THEN All Reduce
                THEN Try ((RW assert_pushdownC (-1)⋅ THEN Auto))
                THEN DVar `a'
                THEN Auto)
         )
   ) }

---

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  \mleq{}loc  e 
13.  A  =  \mleq{}(X)(p)
14.  p  =  last(A)
15.  p  \mleq{}loc  e 
16.  \mleq{}(X)(p)  =  A
\mvdash{}  filter(\mlambda{}a.p  <loc  a;\mleq{}(X)(e))  =  B


By

---

Latex:
(Symmetry
  THEN  ((InstLemma  `iseg-remainder-as-filter` 
                [\mkleeneopen{}E(X)\mkleeneclose{};\mkleeneopen{}\mlambda{}x,y.  (x  <loc  y)\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}\mleq{}(X)(e)\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}\mlambda{}x,y.  x  <loc  y\mkleeneclose{}]\mcdot{}
              THENM  (Reduce  (-1)  THEN  HypSubst'  -4  0  THEN  Auto)\mcdot{}
              )
              THENA  (Auto
                            THEN  Try  ((BLemma  `es-interface-predecessors-sorted-by-locl`  THEN  Auto))
                            THEN  Try  ((D  0  THEN  Reduce  0  THEN  Auto  THEN  RelRST  THEN  Auto)\mcdot{})
                            THEN  All  Reduce
                            THEN  Try  ((RW  assert\_pushdownC  (-1)\mcdot{}  THEN  Auto))
                            THEN  DVar  `a'
                            THEN  Auto)
              )
  )

---

Home Index