---

Step * of Lemma poss-maj-unanimous

∀T:Type. ∀eq:EqDecider(T). ∀L:T List. ∀x,y:T.  ((poss-maj(eq;L;x) = <||L||, y> ∈ (ℕ × T)) ⇒ (∀z∈L.z = y ∈ T))
BY
{ (InstLemma `poss-maj-invariant` []
   THEN RepeatFor 4 (ParallelLast')
   THEN MoveToConcl (-1)
   THEN GenConclAtAddr [1;1]
   THEN Thin (-1)
   THEN D -1
   THEN RenameVar `n' (-2)
   THEN RenameVar `z' (-1)
   THEN Reduce 0
   THEN Auto
   THEN Assert ⌜(n = ||L|| ∈ ℕ) ∧ (z = y ∈ T)⌝⋅
   THEN Auto
   THEN D 0⋅
   THEN Auto
   THEN ElimVar `n'
   THEN ElimVar `y'
   THEN Auto
   THEN AutoBoolCase ⌜eq z L[i]⌝⋅
   THEN ((InstHyp [⌜L[i]⌝] (-6)⋅ THEN Auto) THENA (RW assert_pushdownC 0 THEN Auto))⋅) }

1
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. x : T
5. n : ℕ
6. ||L|| ∈ ℕ
7. z : T
8. (count(eq z;L) - count(λt.(¬b(eq z t));L)) ≤ ||L||
9. ∀y:T. ((¬↑(eq z y)) ⇒ (||L|| ≤ (count(λt.(¬b(eq y t));L) - count(eq y;L))))
10. y : T
11. z ∈ T
12. <||L||, z> = <||L||, z> ∈ (ℕ × T)
13. i : ℕ||L||
14. ¬(z = L[i] ∈ T)
15. ||L|| ≤ (count(λt.(¬b(eq L[i] t));L) - count(eq L[i];L))
⊢ L[i] = z ∈ T

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}eq:EqDecider(T).  \mforall{}L:T  List.  \mforall{}x,y:T.    ((poss-maj(eq;L;x)  =  <||L||,  y>)  {}\mRightarrow{}  (\mforall{}z\mmember{}L.z  =  y))


By

---

Latex:
(InstLemma  `poss-maj-invariant`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  MoveToConcl  (-1)
  THEN  GenConclAtAddr  [1;1]
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  RenameVar  `n'  (-2)
  THEN  RenameVar  `z'  (-1)
  THEN  Reduce  0
  THEN  Auto
  THEN  Assert  \mkleeneopen{}(n  =  ||L||)  \mwedge{}  (z  =  y)\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  D  0\mcdot{}
  THEN  Auto
  THEN  ElimVar  `n'
  THEN  ElimVar  `y'
  THEN  Auto
  THEN  AutoBoolCase  \mkleeneopen{}eq  z  L[i]\mkleeneclose{}\mcdot{}
  THEN  ((InstHyp  [\mkleeneopen{}L[i]\mkleeneclose{}]  (-6)\mcdot{}  THEN  Auto)  THENA  (RW  assert\_pushdownC  0  THEN  Auto))\mcdot{})

---

Home Index