---

Step * 1 of Lemma iseg-remainder-as-filter


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)
BY
{ xxx((InstLemma `sorted-by-strict-unique` [⌜T⌝;⌜R⌝]⋅ THENA Auto) THEN BHyp -1  THEN Auto)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))))
15. ∀[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;sb;filter(dR last(sa);s))

2
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))))
15. ∀[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(dR last(sa);s))

3
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))))
15. ∀[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;sb)

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
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)
9.  sorted-by(R;s)
10.  Trans(T;a,b.R  a  b)
11.  dR  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}
12.  \mforall{}x,y:T.    (\muparrow{}(dR  x  y)  \mLeftarrow{}{}\mRightarrow{}  R  x  y)
13.  \mneg{}\muparrow{}null(sa)
14.  \mforall{}x:T.  ((x  \mmember{}  sa)  \mLeftarrow{}{}\mRightarrow{}  (\mneg{}\muparrow{}null(sa))  \mwedge{}  (x  \mmember{}  s)  \mwedge{}  ((x  =  last(sa))  \mvee{}  (R  x  last(sa))))
\mvdash{}  sb  =  filter(dR  last(sa);s)


By

---

Latex:
xxx((InstLemma  `sorted-by-strict-unique`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  BHyp  -1    THEN  Auto)xxx

---

Home Index