---

Step * of Lemma iseg-as-filter

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[sa,sb:T List].
  (∀[dR:T ⟶ T ⟶ 𝔹]
     (sa = filter(λx.(dR x last(sa));sb) ∈ (T List)) supposing 
        ((¬↑null(sa)) and 
        (∀x,y:T.  (↑(dR x y) ⇐⇒ (R x y) ∨ (x = y ∈ T))))) supposing 
     (Trans(T;a,b.R a b) and 
     sorted-by(R;sb) and 
     sa ≤ sb and 
     AntiSym(T;x,y.R x y) and 
     Irrefl(T;x,y.R x y))
BY
{ (InstLemma `member-iseg-sorted-by` []
   THEN RepeatFor 8 ((ParallelLast' THENA Auto))
   THEN Auto
   THEN (InstLemma `sorted-by-strict-unique` [⌜T⌝;⌜R⌝]⋅ THENA Auto)
   THEN BHyp -1 
   THEN Auto) }

1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. sa : T List
4. sb : T List
5. Irrefl(T;x,y.R x y)
6. AntiSym(T;x,y.R x y)
7. sa ≤ sb
8. sorted-by(R;sb)
9. ∀x:T. ((x ∈ sa) ⇐⇒ (¬↑null(sa)) ∧ (x ∈ sb) ∧ ((x = last(sa) ∈ T) ∨ (R x last(sa))))
10. Trans(T;a,b.R a b)
11. dR : T ⟶ T ⟶ 𝔹
12. ∀x,y:T.  (↑(dR x y) ⇐⇒ (R x y) ∨ (x = y ∈ T))
13. ¬↑null(sa)
14. ∀[sa,sb:T List].  (sa = sb ∈ (T List)) supposing (sorted-by(R;sa) and sorted-by(R;sb) and set-equal(T;sa;sb))
⊢ set-equal(T;sa;filter(λx.(dR x last(sa));sb))

2
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. sa : T List
4. sb : T List
5. Irrefl(T;x,y.R x y)
6. AntiSym(T;x,y.R x y)
7. sa ≤ sb
8. sorted-by(R;sb)
9. ∀x:T. ((x ∈ sa) ⇐⇒ (¬↑null(sa)) ∧ (x ∈ sb) ∧ ((x = last(sa) ∈ T) ∨ (R x last(sa))))
10. Trans(T;a,b.R a b)
11. dR : T ⟶ T ⟶ 𝔹
12. ∀x,y:T.  (↑(dR x y) ⇐⇒ (R x y) ∨ (x = y ∈ T))
13. ¬↑null(sa)
14. ∀[sa,sb:T List].  (sa = sb ∈ (T List)) supposing (sorted-by(R;sa) and sorted-by(R;sb) and set-equal(T;sa;sb))
⊢ sorted-by(R;filter(λx.(dR x last(sa));sb))

3
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. sa : T List
4. sb : T List
5. Irrefl(T;x,y.R x y)
6. AntiSym(T;x,y.R x y)
7. sa ≤ sb
8. sorted-by(R;sb)
9. ∀x:T. ((x ∈ sa) ⇐⇒ (¬↑null(sa)) ∧ (x ∈ sb) ∧ ((x = last(sa) ∈ T) ∨ (R x last(sa))))
10. Trans(T;a,b.R a b)
11. dR : T ⟶ T ⟶ 𝔹
12. ∀x,y:T.  (↑(dR x y) ⇐⇒ (R x y) ∨ (x = y ∈ T))
13. ¬↑null(sa)
14. ∀[sa,sb:T List].  (sa = sb ∈ (T List)) supposing (sorted-by(R;sa) and sorted-by(R;sb) and set-equal(T;sa;sb))
⊢ sorted-by(R;sa)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[sa,sb:T  List].
    (\mforall{}[dR:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}]
          (sa  =  filter(\mlambda{}x.(dR  x  last(sa));sb))  supposing 
                ((\mneg{}\muparrow{}null(sa))  and 
                (\mforall{}x,y:T.    (\muparrow{}(dR  x  y)  \mLeftarrow{}{}\mRightarrow{}  (R  x  y)  \mvee{}  (x  =  y)))))  supposing 
          (Trans(T;a,b.R  a  b)  and 
          sorted-by(R;sb)  and 
          sa  \mleq{}  sb  and 
          AntiSym(T;x,y.R  x  y)  and 
          Irrefl(T;x,y.R  x  y))


By

---

Latex:
(InstLemma  `member-iseg-sorted-by`  []
  THEN  RepeatFor  8  ((ParallelLast'  THENA  Auto))
  THEN  Auto
  THEN  (InstLemma  `sorted-by-strict-unique`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  BHyp  -1 
  THEN  Auto)

---

Home Index