---

Step * 1 1 2 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. y : Unit
10. strict-majority(eq;L1) = (inr y ) ∈ (T?)
11. x : T
12. strict-majority(eq;L2) = (inl x) ∈ (T?)
⊢ (inr y ) = (inl x) ∈ (T?)
BY
{ ((RWO "8<" (-1) THENA Auto)
   THEN (RWO "5<" (-1) THENA Auto)
   THEN (RWO "6<" (-1) THENA Auto)
   THEN (RWO "7" (-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.  y  :  Unit
10.  strict-majority(eq;L1)  =  (inr  y  )
11.  x  :  T
12.  strict-majority(eq;L2)  =  (inl  x)
\mvdash{}  (inr  y  )  =  (inl  x)


By

---

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

---

Home Index