---

Step * 1 of Lemma strict-majority-or-max-property


1. t : ℕ
2. L : ℤ List
3. v : ℤ
4. ||L|| = ((2 * t) + 1) ∈ ℤ
5. (t + 1) ≤ ||filter(λx.(x =z v);L)||
⊢ case strict-majority(IntDeq;L) of inl(x) => x | inr(z) => if null(L) then 0 else imax-list(L) fi  = v ∈ ℤ
BY
{ (InstLemma `strict-majority-property` [⌜ℤ⌝;⌜IntDeq⌝;⌜L⌝;⌜v⌝]⋅
   THEN Auto
   THEN (D -2 THENA (RepUR ``int-deq eqof`` 0 THEN Auto'))
   THEN (HypSubst' (-1) 0 THEN Reduce 0)
   THEN Auto) }

---

Latex:

---

Latex:

1.  t  :  \mBbbN{}
2.  L  :  \mBbbZ{}  List
3.  v  :  \mBbbZ{}
4.  ||L||  =  ((2  *  t)  +  1)
5.  (t  +  1)  \mleq{}  ||filter(\mlambda{}x.(x  =\msubz{}  v);L)||
\mvdash{}  case  strict-majority(IntDeq;L)  of  inl(x)  =>  x  |  inr(z)  =>  if  null(L)  then  0  else  imax-list(L)  fi 
=  v


By

---

Latex:
(InstLemma  `strict-majority-property`  [\mkleeneopen{}\mBbbZ{}\mkleeneclose{};\mkleeneopen{}IntDeq\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (D  -2  THENA  (RepUR  ``int-deq  eqof``  0  THEN  Auto'))
  THEN  (HypSubst'  (-1)  0  THEN  Reduce  0)
  THEN  Auto)

---

Home Index