---

Step * of Lemma strict-majority_functionality

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L1,L2:T List].
  (strict-majority(eq;L1) = strict-majority(eq;L2) ∈ (T?)) supposing 
     ((||L1|| = ||L2|| ∈ ℤ) and 
     (∀x:T. (||filter(λy.(eq y x);L1)|| = ||filter(λy.(eq y x);L2)|| ∈ ℤ)))
BY
{ Auto }

1
1. T : Type
2. eq : EqDecider(T)
3. L1 : T List
4. L2 : T List
5. ∀x:T. (||filter(λy.(eq y x);L1)|| = ||filter(λy.(eq y x);L2)|| ∈ ℤ)
6. ||L1|| = ||L2|| ∈ ℤ
⊢ strict-majority(eq;L1) = strict-majority(eq;L2) ∈ (T?)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[L1,L2:T  List].
    (strict-majority(eq;L1)  =  strict-majority(eq;L2))  supposing 
          ((||L1||  =  ||L2||)  and 
          (\mforall{}x:T.  (||filter(\mlambda{}y.(eq  y  x);L1)||  =  ||filter(\mlambda{}y.(eq  y  x);L2)||)))


By

---

Latex:
Auto

---

Home Index