---

Step * 1 of Lemma poss-maj-invariant


1. T : Type
2. eq : EqDecider(T)
⊢ ∀x:T
    let n,z@0 = poss-maj(eq;[];x) 
    in ((count(eq z@0;[]) - count(λt.(¬b(eq z@0 t));[])) ≤ n)
       ∧ (∀y:T. ((¬↑(eq z@0 y)) ⇒ (n ≤ (count(λt.(¬b(eq y t));[]) - count(eq y;[])))))
BY
{ (RepUR ``poss-maj count`` 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
\mvdash{}  \mforall{}x:T
        let  n,z@0  =  poss-maj(eq;[];x) 
        in  ((count(eq  z@0;[])  -  count(\mlambda{}t.(\mneg{}\msubb{}(eq  z@0  t));[]))  \mleq{}  n)
              \mwedge{}  (\mforall{}y:T.  ((\mneg{}\muparrow{}(eq  z@0  y))  {}\mRightarrow{}  (n  \mleq{}  (count(\mlambda{}t.(\mneg{}\msubb{}(eq  y  t));[])  -  count(eq  y;[])))))


By

---

Latex:
(RepUR  ``poss-maj  count``  0  THEN  Auto)\mcdot{}

---

Home Index