---

Step * of Lemma iseg-remainder-as-filter

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[sa,s,sb:T List].
  (∀[dR:T ⟶ T ⟶ 𝔹]
     (sb = filter(dR last(sa);s) ∈ (T List)) supposing ((¬↑null(sa)) and (∀x,y:T.  (↑(dR x y) ⇐⇒ R x y)))) supposing 
     (Trans(T;a,b.R a b) and 
     sorted-by(R;s) and 
     (s = (sa @ sb) ∈ (T List)) and 
     AntiSym(T;x,y.R x y) and 
     Irrefl(T;x,y.R x y))
BY
{ xxx(InstLemma `member-iseg-sorted-by` []
      THEN RepeatFor 4 ((ParallelLast' THENA Auto))
      THEN (Auto THEN Repeat (ThinTrivial))
      THEN (D -1 THENA (With ⌜sb⌝ (D 0)⋅ THEN Auto))
      THEN ThinTrivial)xxx }

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

---

Latex:

---

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


By

---

Latex:
xxx(InstLemma  `member-iseg-sorted-by`  []
        THEN  RepeatFor  4  ((ParallelLast'  THENA  Auto))
        THEN  (Auto  THEN  Repeat  (ThinTrivial))
        THEN  (D  -1  THENA  (With  \mkleeneopen{}sb\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto))
        THEN  ThinTrivial)xxx

---

Home Index