---

Step * 2 1 of Lemma poss-maj-invariant


1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. ¬↑null(L)
5. ||L|| ≥ 1 
6. x : T
7. ys : T List
8. y : T
⊢ let n,z = poss-maj(eq;ys;x) 
  in ((count(eq z;ys) - count(λt.(¬b(eq z t));ys)) ≤ n)
     ∧ (∀y:T. ((¬↑(eq z y)) ⇒ (n ≤ (count(λt.(¬b(eq y t));ys) - count(eq y;ys)))))
⇒ let n,z@0 = let n,x = poss-maj(eq;ys;x) 
               in if eq y x then <n + 1, x>
                  if (n =z 0) then <1, y>
                  else <n - 1, x>
                  fi  
   in ((count(eq z@0;ys @ [y]) - count(λt.(¬b(eq z@0 t));ys @ [y])) ≤ n)
      ∧ (∀y@0:T. ((¬↑(eq z@0 y@0)) ⇒ (n ≤ (count(λt.(¬b(eq y@0 t));ys @ [y]) - count(eq y@0;ys @ [y])))))
BY
{ (GenConclAtAddr[1;1]
   THEN Thin(-1)
   THEN D -1
   THEN RenameVar `n' (-2)
   THEN RenameVar `z' (-1)
   THEN Reduce 0
   THEN (D 0 THENA Auto))⋅ }

1
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. ¬↑null(L)
5. ||L|| ≥ 1 
6. x : T
7. ys : T List
8. y : T
9. n : ℕ
10. z : T
11. ((count(eq z;ys) - count(λt.(¬b(eq z t));ys)) ≤ n)
∧ (∀y:T. ((¬↑(eq z y)) ⇒ (n ≤ (count(λt.(¬b(eq y t));ys) - count(eq y;ys)))))
⊢ let n,z@0 = if eq y z then <n + 1, z>
  if (n =z 0) then <1, y>
  else <n - 1, z>
  fi  
  in ((count(eq z@0;ys @ [y]) - count(λt.(¬b(eq z@0 t));ys @ [y])) ≤ n)
     ∧ (∀y@0:T. ((¬↑(eq z@0 y@0)) ⇒ (n ≤ (count(λt.(¬b(eq y@0 t));ys @ [y]) - count(eq y@0;ys @ [y])))))

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
4.  \mneg{}\muparrow{}null(L)
5.  ||L||  \mgeq{}  1 
6.  x  :  T
7.  ys  :  T  List
8.  y  :  T
\mvdash{}  let  n,z  =  poss-maj(eq;ys;x) 
    in  ((count(eq  z;ys)  -  count(\mlambda{}t.(\mneg{}\msubb{}(eq  z  t));ys))  \mleq{}  n)
          \mwedge{}  (\mforall{}y:T.  ((\mneg{}\muparrow{}(eq  z  y))  {}\mRightarrow{}  (n  \mleq{}  (count(\mlambda{}t.(\mneg{}\msubb{}(eq  y  t));ys)  -  count(eq  y;ys)))))
{}\mRightarrow{}  let  n,z@0  =  let  n,x  =  poss-maj(eq;ys;x) 
                              in  if  eq  y  x  then  <n  +  1,  x>
                                    if  (n  =\msubz{}  0)  then  ə,  y>
                                    else  <n  -  1,  x>
                                    fi   
      in  ((count(eq  z@0;ys  @  [y])  -  count(\mlambda{}t.(\mneg{}\msubb{}(eq  z@0  t));ys  @  [y]))  \mleq{}  n)
            \mwedge{}  (\mforall{}y@0:T
                      ((\mneg{}\muparrow{}(eq  z@0  y@0))  {}\mRightarrow{}  (n  \mleq{}  (count(\mlambda{}t.(\mneg{}\msubb{}(eq  y@0  t));ys  @  [y])  -  count(eq  y@0;ys  @  [y])))))


By

---

Latex:
(GenConclAtAddr[1;1]
  THEN  Thin(-1)
  THEN  D  -1
  THEN  RenameVar  `n'  (-2)
  THEN  RenameVar  `z'  (-1)
  THEN  Reduce  0
  THEN  (D  0  THENA  Auto))\mcdot{}

---

Home Index