---

Step * of Lemma poss-maj-property

∀T:Type. ∀eq:EqDecider(T). ∀L:T List. ∀x:T.  possible-majority(T;eq;L;snd(poss-maj(eq;L;x)))
BY
{ TACTIC:(InstLemma `poss-maj-invariant` [] THEN RepeatFor 4 (ParallelLast')) }

1
1. T : Type@i'
2. eq : EqDecider(T)@i
3. L : T List@i
4. x : T@i
5. let n,z = poss-maj(eq;L;x) 
   in ((count(eq z;L) - count(λt.(¬b(eq z t));L)) ≤ n)
      ∧ (∀y:T. ((¬↑(eq z y)) ⇒ (n ≤ (count(λt.(¬b(eq y t));L) - count(eq y;L)))))
⊢ possible-majority(T;eq;L;snd(poss-maj(eq;L;x)))

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}eq:EqDecider(T).  \mforall{}L:T  List.  \mforall{}x:T.    possible-majority(T;eq;L;snd(poss-maj(eq;L;x)))


By

---

Latex:
TACTIC:(InstLemma  `poss-maj-invariant`  []  THEN  RepeatFor  4  (ParallelLast'))

---

Home Index