---

Step * 1 1 1 of Lemma strict-majority_functionality


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|| ∈ ℤ
7. ∀[x:T]. uiff(||L1|| < 2 * ||filter(λy.(eq y x);L1)||;strict-majority(eq;L1) = (inl x) ∈ (T?))
8. ∀[x:T]. uiff(||L2|| < 2 * ||filter(λy.(eq y x);L2)||;strict-majority(eq;L2) = (inl x) ∈ (T?))
9. x : T
10. strict-majority(eq;L1) = (inl x) ∈ (T?)
⊢ (inl x) = strict-majority(eq;L2) ∈ (T?)
BY
{ ((RWO "7<" (-1) THENA Auto)
   THEN (RWO "5" (-1) THENA Auto)
   THEN (RWO "6" (-1) THENA Auto)
   THEN (RWO "8" (-1) THEN Auto)⋅)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L1  :  T  List
4.  L2  :  T  List
5.  \mforall{}x:T.  (||filter(\mlambda{}y.(eq  y  x);L1)||  =  ||filter(\mlambda{}y.(eq  y  x);L2)||)
6.  ||L1||  =  ||L2||
7.  \mforall{}[x:T].  uiff(||L1||  <  2  *  ||filter(\mlambda{}y.(eq  y  x);L1)||;strict-majority(eq;L1)  =  (inl  x))
8.  \mforall{}[x:T].  uiff(||L2||  <  2  *  ||filter(\mlambda{}y.(eq  y  x);L2)||;strict-majority(eq;L2)  =  (inl  x))
9.  x  :  T
10.  strict-majority(eq;L1)  =  (inl  x)
\mvdash{}  (inl  x)  =  strict-majority(eq;L2)


By

---

Latex:
((RWO  "7<"  (-1)  THENA  Auto)
  THEN  (RWO  "5"  (-1)  THENA  Auto)
  THEN  (RWO  "6"  (-1)  THENA  Auto)
  THEN  (RWO  "8"  (-1)  THEN  Auto)\mcdot{})\mcdot{}

---

Home Index