---

Step * 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|| ∈ ℤ
⊢ strict-majority(eq;L1) = strict-majority(eq;L2) ∈ (T?)
BY
{ ((InstLemma `strict-majority-property` [⌜T⌝;⌜eq⌝;⌜L1⌝]⋅ THENA Auto)
   THEN (InstLemma `strict-majority-property` [⌜T⌝;⌜eq⌝;⌜L2⌝]⋅ THENA 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|| ∈ ℤ
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?))
⊢ strict-majority(eq;L1) = strict-majority(eq;L2) ∈ (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||
\mvdash{}  strict-majority(eq;L1)  =  strict-majority(eq;L2)


By

---

Latex:
((InstLemma  `strict-majority-property`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}L1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `strict-majority-property`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}L2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  )

---

Home Index