---

Step * of Lemma before_all_imp_count_zero

∀s:QOSet. ∀a:|s|. ∀cs:|s| List.  ((↑(∀bc(:|s|) ∈ cs. (c <b a))) ⇒ ((a #∈ cs) = 0 ∈ ℤ))
BY
{ (InductionOnListA THEN Reduce 0 THEN Auto) }

1
1. s : QOSet
2. a : |s|
3. c : |s|
4. cs : |s| List
5. (↑(∀bc(:|s|) ∈ cs. (c <b a))) ⇒ ((a #∈ cs) = 0 ∈ ℤ)
6. ↑((c <b a) ∧b (∀bc(:|s|) ∈ cs. (c <b a)))
⊢ (b2i(c (=b) a) + (a #∈ cs)) = 0 ∈ ℤ

---

Latex:

---

Latex:
\mforall{}s:QOSet.  \mforall{}a:|s|.  \mforall{}cs:|s|  List.    ((\muparrow{}(\mforall{}\msubb{}c(:|s|)  \mmember{}  cs.  (c  <\msubb{}  a)))  {}\mRightarrow{}  ((a  \#\mmember{}  cs)  =  0))


By

---

Latex:
(InductionOnListA  THEN  Reduce  0  THEN  Auto)

---

Home Index