---

Step * of Lemma sd_ordered_count

∀s:QOSet. ∀as:|s| List.  ((↑sd_ordered(as)) ⇒ (∀c:|s|. ((c #∈ as) ≤ 1)))
BY
{ (InductionOnListA
   THEN Auto
   THEN ((RWH (LemmaC `sd_ordered_char`) (-2) 
   THENM Reduce (-2) 
   THENM RW bool_to_propC (-2) THENM D (-2)) THENA Auto)) }

1
1. s : QOSet
2. a : |s|
3. as : |s| List
4. (↑sd_ordered(as)) ⇒ (∀c:|s|. ((c #∈ as) ≤ 1))
5. ↑(∀bw(:|s|) ∈ as
        (w <b a))
6. ↑(HTFor{<𝔹,∧b>} v::vs ∈ as. ∀bw(:|s|) ∈ vs
                                  (w <b v))
7. c : |s|
⊢ (c #∈ [a / as]) ≤ 1

---

Latex:

---

Latex:
\mforall{}s:QOSet.  \mforall{}as:|s|  List.    ((\muparrow{}sd\_ordered(as))  {}\mRightarrow{}  (\mforall{}c:|s|.  ((c  \#\mmember{}  as)  \mleq{}  1)))


By

---

Latex:
(InductionOnListA
  THEN  Auto
  THEN  ((RWH  (LemmaC  `sd\_ordered\_char`)  (-2) 
  THENM  Reduce  (-2) 
  THENM  RW  bool\_to\_propC  (-2)  THENM  D  (-2))  THENA  Auto))

---

Home Index