---

Step * of Lemma sorted-by-strict-unique

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (∀[sa,sb:T List].
     (sa = sb ∈ (T List)) supposing (sorted-by(R;sa) and sorted-by(R;sb) and set-equal(T;sa;sb))) supposing 
     ((∀a:T. (¬(R a a))) and 
     AntiSym(T;a,b.R a b) and 
     Trans(T;a,b.R a b))
BY
{ (InstLemma `sorted-by-unique` []
   THEN RepeatFor 4 ((ParallelLast' THENA Auto))
   THEN Auto
   THEN BackThruSomeHyp
   THEN Auto) }

1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. Trans(T;a,b.R a b)
4. AntiSym(T;a,b.R a b)
5. ∀[sa,sb:T List].
     (sa = sb ∈ (T List)) supposing 
        (no_repeats(T;sa) and 
        sorted-by(R;sa) and 
        no_repeats(T;sb) and 
        sorted-by(R;sb) and 
        set-equal(T;sa;sb))
6. ∀a:T. (¬(R a a))
7. sa : T List
8. sb : T List
9. set-equal(T;sa;sb)
10. sorted-by(R;sb)
11. sorted-by(R;sa)
⊢ no_repeats(T;sb)

2
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. Trans(T;a,b.R a b)
4. AntiSym(T;a,b.R a b)
5. ∀[sa,sb:T List].
     (sa = sb ∈ (T List)) supposing 
        (no_repeats(T;sa) and 
        sorted-by(R;sa) and 
        no_repeats(T;sb) and 
        sorted-by(R;sb) and 
        set-equal(T;sa;sb))
6. ∀a:T. (¬(R a a))
7. sa : T List
8. sb : T List
9. set-equal(T;sa;sb)
10. sorted-by(R;sb)
11. sorted-by(R;sa)
⊢ no_repeats(T;sa)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (\mforall{}[sa,sb:T  List].
          (sa  =  sb)  supposing  (sorted-by(R;sa)  and  sorted-by(R;sb)  and  set-equal(T;sa;sb)))  supposing 
          ((\mforall{}a:T.  (\mneg{}(R  a  a)))  and 
          AntiSym(T;a,b.R  a  b)  and 
          Trans(T;a,b.R  a  b))


By

---

Latex:
(InstLemma  `sorted-by-unique`  []
  THEN  RepeatFor  4  ((ParallelLast'  THENA  Auto))
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index