---

Step * 1 1 2 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?)
⊢ (inr y ) = strict-majority(eq;L2) ∈ (T?)
BY
{ (GenConclAtAddr [3] THEN D -2)⋅ }

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|| ∈ ℤ
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?)

2
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. y1 : Unit
12. strict-majority(eq;L2) = (inr y1 ) ∈ (T?)
⊢ (inr y ) = (inr y1 ) ∈ (T?)

---

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  )
\mvdash{}  (inr  y  )  =  strict-majority(eq;L2)


By

---

Latex:
(GenConclAtAddr  [3]  THEN  D  -2)\mcdot{}

---

Home Index