---

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


1. t : ℕ
2. u : ℤ
3. v : ℤ List
4. ∀v@0:ℤ
     (case strict-majority(IntDeq;[u / v]) of inl(x) => x | inr(z) => imax-list([u / v]) = v@0 ∈ ℤ) supposing 
        (((t + 1) ≤ ||if (u =z v@0) then [u / filter(λx.(x =z v@0);v)] else filter(λx.(x =z v@0);v) fi ||) and 
        ((||v|| + 1) = ((2 * t) + 1) ∈ ℤ))
5. (||v|| + 1) ≥ 1 
6. y : Unit
7. strict-majority(IntDeq;[u / v]) = (inr y ) ∈ (ℤ?)
⊢ (imax-list([u / v]) ∈ [u / v])
BY
{ (BLemma `imax-list-member` THEN Reduce 0 THEN Auto')⋅ }

---

Latex:

---

Latex:

1.  t  :  \mBbbN{}
2.  u  :  \mBbbZ{}
3.  v  :  \mBbbZ{}  List
4.  \mforall{}v@0:\mBbbZ{}
          (case  strict-majority(IntDeq;[u  /  v])  of  inl(x)  =>  x  |  inr(z)  =>  imax-list([u  /  v])
                =  v@0)  supposing 
                (((t  +  1)  \mleq{}  ||if  (u  =\msubz{}  v@0)
                    then  [u  /  filter(\mlambda{}x.(x  =\msubz{}  v@0);v)]
                    else  filter(\mlambda{}x.(x  =\msubz{}  v@0);v)
                    fi  ||)  and 
                ((||v||  +  1)  =  ((2  *  t)  +  1)))
5.  (||v||  +  1)  \mgeq{}  1 
6.  y  :  Unit
7.  strict-majority(IntDeq;[u  /  v])  =  (inr  y  )
\mvdash{}  (imax-list([u  /  v])  \mmember{}  [u  /  v])


By

---

Latex:
(BLemma  `imax-list-member`  THEN  Reduce  0  THEN  Auto')\mcdot{}

---

Home Index