Step
*
1
1
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))))
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))
16. t : T
17. (t ∈ sa) ⇐⇒ (¬↑null(sa)) ∧ (t ∈ s) ∧ ((t = last(sa) ∈ T) ∨ (R t last(sa)))
⊢ (t ∈ sb) ⇐⇒ (t ∈ s) ∧ (R last(sa) t)
BY
{ xxx(RepeatFor 2 (D 0) 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))
16. t : T
17. (t ∈ sa) ⇒ ((¬↑null(sa)) ∧ (t ∈ s) ∧ ((t = last(sa) ∈ T) ∨ (R t last(sa))))
18. (t ∈ sa) ⇐ (¬↑null(sa)) ∧ (t ∈ s) ∧ ((t = last(sa) ∈ T) ∨ (R t last(sa)))
19. (t ∈ sb)
⊢ (t ∈ 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))
16. t : T
17. (t ∈ sa) ⇒ ((¬↑null(sa)) ∧ (t ∈ s) ∧ ((t = last(sa) ∈ T) ∨ (R t last(sa))))
18. (t ∈ sa) ⇐ (¬↑null(sa)) ∧ (t ∈ s) ∧ ((t = last(sa) ∈ T) ∨ (R t last(sa)))
19. (t ∈ sb)
20. (t ∈ s)
⊢ R last(sa) t
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))
16. t : T
17. (t ∈ sa) ⇒ ((¬↑null(sa)) ∧ (t ∈ s) ∧ ((t = last(sa) ∈ T) ∨ (R t last(sa))))
18. (t ∈ sa) ⇐ (¬↑null(sa)) ∧ (t ∈ s) ∧ ((t = last(sa) ∈ T) ∨ (R t last(sa)))
19. (t ∈ s)
20. R last(sa) t
⊢ (t ∈ 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))))
15. \mforall{}[sa,sb:T List].
(sa = sb) supposing (sorted-by(R;sa) and sorted-by(R;sb) and set-equal(T;sa;sb))
16. t : T
17. (t \mmember{} sa) \mLeftarrow{}{}\mRightarrow{} (\mneg{}\muparrow{}null(sa)) \mwedge{} (t \mmember{} s) \mwedge{} ((t = last(sa)) \mvee{} (R t last(sa)))
\mvdash{} (t \mmember{} sb) \mLeftarrow{}{}\mRightarrow{} (t \mmember{} s) \mwedge{} (R last(sa) t)
By
Latex:
xxx(RepeatFor 2 (D 0) THEN Auto)xxx
Home
Index