---

Step * 1 of Lemma iseg-filter-es-interval


1. es : EO
2. L : E List
3. e1 : E
4. e2 : E
5. P : {x:E| (x ∈ [e1, e2])}  ─→ 𝔹
6. L ≤ filter(P;[e1, e2])
7. ¬↑null(L)
8. (last(L) ∈ L)
9. (last(L) ∈ [e1, e2])
⊢ L = filter(P;[e1, last(L)]) ∈ (E List)
BY
{ ((InstLemma `l-ordered-equality` [⌈E⌉;⌈λ2x.λ2y.(x <loc y)⌉;⌈L⌉;⌈filter(P;[e1, last(L)])⌉]⋅
    THENA (AllReduce THEN Auto)
    )
   THEN Try (Complete ((D 0 THEN Auto)))
   THEN Try ((RWO "-1" 0 THEN Auto))
   THEN Try (Complete ((DoSubsume
                        THEN Auto
                        THEN SubtypeReasoning
                        THEN Auto
                        THEN (RW ListC (-1) THENA Auto)
                        THEN (RW ListC 0 THEN Auto)
                        THEN (RW ListC (-6) THEN Auto)
                        THEN FLemma `es-le_transitivity` [-2;-6]
                        THEN Auto)))) }

1
1. es : EO
2. L : E List
3. e1 : E
4. e2 : E
5. P : {x:E| (x ∈ [e1, e2])}  ─→ 𝔹
6. L ≤ filter(P;[e1, e2])
7. ¬↑null(L)
8. (last(L) ∈ L)
9. (last(L) ∈ [e1, e2])
⊢ l-ordered(E;x,y.(x <loc y);L)

2
1. es : EO
2. L : E List
3. e1 : E
4. e2 : E
5. P : {x:E| (x ∈ [e1, e2])}  ─→ 𝔹
6. L ≤ filter(P;[e1, e2])
7. ¬↑null(L)
8. (last(L) ∈ L)
9. (last(L) ∈ [e1, e2])
⊢ l-ordered(E;x,y.(x <loc y);filter(P;[e1, last(L)]))

3
1. es : EO
2. L : E List
3. e1 : E
4. e2 : E
5. P : {x:E| (x ∈ [e1, e2])}  ─→ 𝔹
6. L ≤ filter(P;[e1, e2])
7. ¬↑null(L)
8. (last(L) ∈ L)
9. (last(L) ∈ [e1, e2])
10. (L = filter(P;[e1, last(L)]) ∈ (E List)) ⇒ (∀x:E. ((x ∈ L) ⇐⇒ (x ∈ filter(P;[e1, last(L)]))))
11. (L = filter(P;[e1, last(L)]) ∈ (E List)) ⇐ ∀x:E. ((x ∈ L) ⇐⇒ (x ∈ filter(P;[e1, last(L)])))
12. x : E@i
13. (x ∈ L)@i
⊢ (x ∈ filter(P;[e1, last(L)]))

4
1. es : EO
2. L : E List
3. e1 : E
4. e2 : E
5. P : {x:E| (x ∈ [e1, e2])}  ─→ 𝔹
6. L ≤ filter(P;[e1, e2])
7. ¬↑null(L)
8. (last(L) ∈ L)
9. (last(L) ∈ [e1, e2])
10. (L = filter(P;[e1, last(L)]) ∈ (E List)) ⇒ (∀x:E. ((x ∈ L) ⇐⇒ (x ∈ filter(P;[e1, last(L)]))))
11. (L = filter(P;[e1, last(L)]) ∈ (E List)) ⇐ ∀x:E. ((x ∈ L) ⇐⇒ (x ∈ filter(P;[e1, last(L)])))
12. x : E@i
13. (x ∈ filter(P;[e1, last(L)]))@i
⊢ (x ∈ L)

5
1. es : EO
2. L : E List
3. e1 : E
4. e2 : E
5. P : {x:E| (x ∈ [e1, e2])}  ─→ 𝔹
6. L ≤ filter(P;[e1, e2])
7. ¬↑null(L)
8. (last(L) ∈ L)
9. (last(L) ∈ [e1, e2])
10. (L = filter(P;[e1, last(L)]) ∈ (E List)) ⇒ (∀x:E. ((x ∈ L) ⇐⇒ (x ∈ filter(P;[e1, last(L)]))))
11. (L = filter(P;[e1, last(L)]) ∈ (E List)) ⇐ ∀x:E. ((x ∈ L) ⇐⇒ (x ∈ filter(P;[e1, last(L)])))
12. x : E@i
⊢ P ∈ {x:E| (x ∈ [e1, last(L)])}  ─→ 𝔹

---

Latex:



1.  es  :  EO
2.  L  :  E  List
3.  e1  :  E
4.  e2  :  E
5.  P  :  \{x:E|  (x  \mmember{}  [e1,  e2])\}    {}\mrightarrow{}  \mBbbB{}
6.  L  \mleq{}  filter(P;[e1,  e2])
7.  \mneg{}\muparrow{}null(L)
8.  (last(L)  \mmember{}  L)
9.  (last(L)  \mmember{}  [e1,  e2])
\mvdash{}  L  =  filter(P;[e1,  last(L)])


By

((InstLemma  `l-ordered-equality`  [\mkleeneopen{}E\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.\mlambda{}\msubtwo{}y.(x  <loc  y)\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}filter(P;[e1,  last(L)])\mkleeneclose{}]\mcdot{}
    THENA  (AllReduce  THEN  Auto)
    )
  THEN  Try  (Complete  ((D  0  THEN  Auto)))
  THEN  Try  ((RWO  "-1"  0  THEN  Auto))
  THEN  Try  (Complete  ((DoSubsume
                                            THEN  Auto
                                            THEN  SubtypeReasoning
                                            THEN  Auto
                                            THEN  (RW  ListC  (-1)  THENA  Auto)
                                            THEN  (RW  ListC  0  THEN  Auto)
                                            THEN  (RW  ListC  (-6)  THEN  Auto)
                                            THEN  FLemma  `es-le\_transitivity`  [-2;-6]
                                            THEN  Auto))))

---

Home Index