---

Step * 2 1 1 1 of Lemma poss-maj-invariant


1. T : Type
2. eq : EqDecider(T)
3. x : T
4. ys : T List
5. y : T
6. n : ℕ
7. z : T
8. ((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])))))
BY
{ (Repeat (AutoSplit)
   THEN Auto
   THEN (RWW "count-append count-single" 0 THENA Auto)
   THEN Reduce 0
   THEN Repeat (AutoSplit)
   THEN AllHyps (\h. (D h THEN Complete ((RW assert_pushdownC 0 THEN Auto))) )⋅) }

1
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. ys : T List
5. y : T
6. n : ℕ
7. z : T
8. (count(eq z;ys) - count(λt.(¬b(eq z t));ys)) ≤ n
9. ∀y:T. ((¬↑(eq z y)) ⇒ (n ≤ (count(λt.(¬b(eq y t));ys) - count(eq y;ys))))
10. y = z ∈ T
11. (count(eq z;ys @ [y]) - count(λt.(¬b(eq z t));ys @ [y])) ≤ (n + 1)
12. y@0 : T
13. ¬(y@0 = y ∈ T)
14. ¬↑(eq z y@0)
⊢ (n + 1) ≤ ((count(λt.(¬b(eq y@0 t));ys) + 1) - count(eq y@0;ys) + 0)

2
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. ys : T List
5. y : T
6. n : ℕ
7. z : T
8. ¬(y = z ∈ T)
9. (count(eq z;ys) - count(λt.(¬b(eq z t));ys)) ≤ n
10. ∀y:T. ((¬↑(eq z y)) ⇒ (n ≤ (count(λt.(¬b(eq y t));ys) - count(eq y;ys))))
11. n = 0 ∈ ℤ
12. y = y ∈ T
⊢ ((count(eq y;ys) + 1) - count(λt.(¬b(eq y t));ys) + 0) ≤ 1

3
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. ys : T List
5. y : T
6. n : ℕ
7. z : T
8. ¬(y = z ∈ T)
9. (count(eq z;ys) - count(λt.(¬b(eq z t));ys)) ≤ n
10. ∀y:T. ((¬↑(eq z y)) ⇒ (n ≤ (count(λt.(¬b(eq y t));ys) - count(eq y;ys))))
11. n = 0 ∈ ℤ
12. (count(eq y;ys @ [y]) - count(λt.(¬b(eq y t));ys @ [y])) ≤ 1
13. y@0 : T
14. ¬(y@0 = y ∈ T)
15. ¬↑(eq y y@0)
⊢ 1 ≤ ((count(λt.(¬b(eq y@0 t));ys) + 1) - count(eq y@0;ys) + 0)

4
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. ys : T List
5. y : T
6. n : {1...}
7. z : T
8. ¬(y = z ∈ T)
9. (count(eq z;ys) - count(λt.(¬b(eq z t));ys)) ≤ n
10. ∀y:T. ((¬↑(eq z y)) ⇒ (n ≤ (count(λt.(¬b(eq y t));ys) - count(eq y;ys))))
11. (count(eq z;ys @ [y]) - count(λt.(¬b(eq z t));ys @ [y])) ≤ (n - 1)
12. y@0 : T
13. ¬↑(eq z y@0)
14. y@0 = y ∈ T
⊢ (n - 1) ≤ ((count(λt.(¬b(eq y@0 t));ys) + 0) - count(eq y@0;ys) + 1)

5
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. ys : T List
5. y : T
6. n : {1...}
7. z : T
8. ¬(y = z ∈ T)
9. (count(eq z;ys) - count(λt.(¬b(eq z t));ys)) ≤ n
10. ∀y:T. ((¬↑(eq z y)) ⇒ (n ≤ (count(λt.(¬b(eq y t));ys) - count(eq y;ys))))
11. (count(eq z;ys @ [y]) - count(λt.(¬b(eq z t));ys @ [y])) ≤ (n - 1)
12. y@0 : T
13. ¬(y@0 = y ∈ T)
14. ¬↑(eq z y@0)
⊢ (n - 1) ≤ ((count(λt.(¬b(eq y@0 t));ys) + 1) - count(eq y@0;ys) + 0)

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  T
4.  ys  :  T  List
5.  y  :  T
6.  n  :  \mBbbN{}
7.  z  :  T
8.  ((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)))))
\mvdash{}  let  n,z@0  =  if  eq  y  z  then  <n  +  1,  z>
    if  (n  =\msubz{}  0)  then  ə,  y>
    else  <n  -  1,  z>
    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:
(Repeat  (AutoSplit)
  THEN  Auto
  THEN  (RWW  "count-append  count-single"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Repeat  (AutoSplit)
  THEN  AllHyps  (\mbackslash{}h.  (D  h  THEN  Complete  ((RW  assert\_pushdownC  0  THEN  Auto)))  )\mcdot{})

---

Home Index