---

Step * of Lemma consensus-accum-num-property1

∀[V:Type]
  ∀A:Id List. ∀t:ℕ+. ∀f:(V List) ⟶ V. ∀v0:V. ∀L:consensus-rcv(V;A) List.
    let b,i,as,vs,v = consensus-accum-num-state(t;f;v0;L) in (filter(λr.i - 1 <z inning(r);L)
                                                             = []
                                                             ∈ (consensus-rcv(V;A) List))
    ∧ (||as|| = ||vs|| ∈ ℤ)
    ∧ (zip(as;vs) = votes-from-inning(i - 1;L) ∈ (({b:Id| (b ∈ A)}  × V) List))
    ∧ (0 ≤ i)
    ∧ 1 ≤ i supposing ¬↑null(L)
    ∧ (||values-for-distinct(IdDeq;votes-from-inning(i - 1;L))|| ≤ (2 * t))
BY
{ ((RepeatFor 5 ((D 0 THENA Auto)) THEN (Assert IdDeq ∈ EqDecider({b:Id| (b ∈ A)} ) BY Auto))
   THEN (BLemma `last_induction` THENA (Auto THEN GenConclAtAddr [2;1] THEN Auto))
   THEN Repeat ((D 0 THENA Complete (Auto)))
   THEN RepUR ``consensus-accum-num-state`` 0
   THEN Try ((RepUR ``votes-from-inning mapfilter values-for-distinct`` 0 THEN Complete ((Auto THEN Auto'))))
   THEN (RWO "list_accum_append" 0 THENA Auto)
   THEN Fold `consensus-accum-num-state` 0
   THEN (GenConclAtAddr [1;1] THENA Auto)
   THEN Thin (-1)
   THEN RepeatFor 4 (D -1)
   THEN Reduce 0
   THEN D -6
   THEN Try (RepeatFor 2 (D -6))
   THEN RepUR ``consensus-accum-num let`` 0
   THEN Folds ``cs-initial-rcv cs-rcv-vote`` 0
   THEN Repeat (((SplitOnConclITE THENA Complete (Auto)) THEN Reduce 0))
   THEN Auto
   THEN Try (((RevHypSubst' (-3) 0 THENM RepUR ``values-for-distinct`` 0) THEN Complete (Auto)))
   THEN ...
   THEN Try ((((RWO "filter_append_sq" 0 THENM (Reduce 0 THEN SplitOnConclITE)) THENA UsingVars [`A';`V'] Auto)
              THEN RepUR ``rcvd-inning-gt rcv-vote? cs-initial-rcv cs-rcv-vote rcvd-vote`` -1
              THEN Auto
              THEN Try ((RWO "append-nil" 0 THEN Auto))
              THEN Try ((RW assert_pushdownC (-1) THEN Auto))))
   THEN Try (\p. ((Using [`i',get_addressed_subterm [2;1;1;1] (concl p)] (FLemma `rcvd-innings-nil` [-7])⋅ THEN Auto)
                  THEN HypSubst' (-1) 0
                  THEN Auto) p⋅)
   THEN Try (\p. 
             ((Using [`i', get_addressed_subterm [3;1;1] (concl p)] (FLemma `votes-from-inning-is-nil` [-8])⋅
               THENA Complete (Auto)
               )
              THEN HypSubst' -1 0
              THEN RepUR ``votes-from-inning mapfilter rcvd-inning-eq rcv-vote? cs-initial-rcv cs-rcv-vote rcvd-vote`` 0
              THEN Try (SplitOnConclITE)
              THEN Reduce 0
              THEN Auto) p⋅)
   THEN Try (Complete ((\p. Subst (mk_sqequal_term (get_addressed_subterm [3;2] (concl p))⌜[]⌝) 0 p⋅
                        THENL [(...
                                THEN Try (SplitOnConclITE)
                                THEN Reduce 0
                                THEN Auto)
                              ; (RWO "append-nil" 0 THEN Complete (Auto))]
                       )))) }

1
1. V : Type
2. A : Id List@i
3. t : ℕ+@i
4. f : (V List) ⟶ V@i
5. v0 : V@i
6. IdDeq ∈ EqDecider({b:Id| (b ∈ A)} )
7. ys : consensus-rcv(V;A) List@i
8. y2 : {b:Id| (b ∈ A)} @i
9. y4 : ℕ@i
10. y5 : V@i
11. v1 : 𝔹@i
12. v3 : ℤ@i
13. v5 : {a:Id| (a ∈ A)}  List@i
14. v7 : V List@i
15. v8 : V@i
16. (v3 - 1) ≤ y4
17. y4 ≤ (v3 - 1)
18. ¬(||remove-repeats(IdDeq;v5 @ [y2])|| = ((2 * t) + 1) ∈ ℤ)
19. filter(λr.v3 - 1 <z inning(r);ys) = [] ∈ (consensus-rcv(V;A) List)@i
20. ||v5|| = ||v7|| ∈ ℤ@i
21. zip(v5;v7) = votes-from-inning(v3 - 1;ys) ∈ (({b:Id| (b ∈ A)}  × V) List)@i
22. 0 ≤ v3@i
23. 1 ≤ v3 supposing ¬↑null(ys)@i
24. ||values-for-distinct(IdDeq;votes-from-inning(v3 - 1;ys))|| ≤ (2 * t)@i
25. filter(λr.v3 - 1 <z inning(r);ys @ [Vote[y2;y4;y5]]) = [] ∈ (consensus-rcv(V;A) List)
26. ||v5 @ [y2]|| = ||v7 @ [y5]|| ∈ ℤ
⊢ zip(v5 @ [y2];v7 @ [y5])
= (votes-from-inning(v3 - 1;ys) @ votes-from-inning(v3 - 1;[Vote[y2;y4;y5]]))
∈ (({b:Id| (b ∈ A)}  × V) List)

2
1. V : Type
2. A : Id List@i
3. t : ℕ+@i
4. f : (V List) ⟶ V@i
5. v0 : V@i
6. IdDeq ∈ EqDecider({b:Id| (b ∈ A)} )
7. ys : consensus-rcv(V;A) List@i
8. y2 : {b:Id| (b ∈ A)} @i
9. y4 : ℕ@i
10. y5 : V@i
11. v1 : 𝔹@i
12. v3 : ℤ@i
13. v5 : {a:Id| (a ∈ A)}  List@i
14. v7 : V List@i
15. v8 : V@i
16. (v3 - 1) ≤ y4
17. y4 ≤ (v3 - 1)
18. ¬(||remove-repeats(IdDeq;v5 @ [y2])|| = ((2 * t) + 1) ∈ ℤ)
19. filter(λr.v3 - 1 <z inning(r);ys) = [] ∈ (consensus-rcv(V;A) List)@i
20. ||v5|| = ||v7|| ∈ ℤ@i
21. zip(v5;v7) = votes-from-inning(v3 - 1;ys) ∈ (({b:Id| (b ∈ A)}  × V) List)@i
22. 0 ≤ v3@i
23. 1 ≤ v3 supposing ¬↑null(ys)@i
24. ||values-for-distinct(IdDeq;votes-from-inning(v3 - 1;ys))|| ≤ (2 * t)@i
25. filter(λr.v3 - 1 <z inning(r);ys @ [Vote[y2;y4;y5]]) = [] ∈ (consensus-rcv(V;A) List)
26. ||v5 @ [y2]|| = ||v7 @ [y5]|| ∈ ℤ
27. zip(v5 @ [y2];v7 @ [y5]) = votes-from-inning(v3 - 1;ys @ [Vote[y2;y4;y5]]) ∈ (({b:Id| (b ∈ A)}  × V) List)
28. 0 ≤ v3
29. 1 ≤ v3 supposing ¬↑null(ys @ [Vote[y2;y4;y5]])
⊢ ||values-for-distinct(IdDeq;votes-from-inning(v3 - 1;ys) @ votes-from-inning(v3 - 1;[Vote[y2;y4;y5]]))|| ≤ (2 * t)

---

Latex:

---

Latex:
\mforall{}[V:Type]
    \mforall{}A:Id  List.  \mforall{}t:\mBbbN{}\msupplus{}.  \mforall{}f:(V  List)  {}\mrightarrow{}  V.  \mforall{}v0:V.  \mforall{}L:consensus-rcv(V;A)  List.
        let  b,i,as,vs,v  =  consensus-accum-num-state(t;f;v0;L)  in  (filter(\mlambda{}r.i  -  1  <z  inning(r);L)  =  [])
        \mwedge{}  (||as||  =  ||vs||)
        \mwedge{}  (zip(as;vs)  =  votes-from-inning(i  -  1;L))
        \mwedge{}  (0  \mleq{}  i)
        \mwedge{}  1  \mleq{}  i  supposing  \mneg{}\muparrow{}null(L)
        \mwedge{}  (||values-for-distinct(IdDeq;votes-from-inning(i  -  1;L))||  \mleq{}  (2  *  t))


By

---

Latex:
((RepeatFor  5  ((D  0  THENA  Auto))  THEN  (Assert  IdDeq  \mmember{}  EqDecider(\{b:Id|  (b  \mmember{}  A)\}  )  BY  Auto))
  THEN  (BLemma  `last\_induction`  THENA  (Auto  THEN  GenConclAtAddr  [2;1]  THEN  Auto))
  THEN  Repeat  ((D  0  THENA  Complete  (Auto)))
  THEN  RepUR  ``consensus-accum-num-state``  0
  THEN  Try  ((RepUR  ``votes-from-inning  mapfilter  values-for-distinct``  0
                        THEN  Complete  ((Auto  THEN  Auto'))
                        ))
  THEN  (RWO  "list\_accum\_append"  0  THENA  Auto)
  THEN  Fold  `consensus-accum-num-state`  0
  THEN  (GenConclAtAddr  [1;1]  THENA  Auto)
  THEN  Thin  (-1)
  THEN  RepeatFor  4  (D  -1)
  THEN  Reduce  0
  THEN  D  -6
  THEN  Try  (RepeatFor  2  (D  -6))
  THEN  RepUR  ``consensus-accum-num  let``  0
  THEN  Folds  ``cs-initial-rcv  cs-rcv-vote``  0
  THEN  Repeat  (((SplitOnConclITE  THENA  Complete  (Auto))  THEN  Reduce  0))
  THEN  Auto
  THEN  Try  (((RevHypSubst'  (-3)  0  THENM  RepUR  ``values-for-distinct``  0)  THEN  Complete  (Auto)))
  THEN  Try  ((Unfold  `votes-from-inning`  0
                        THEN  ((RWO  "mapfilter-append"  0  THENA  Auto)  THEN  Fold  `votes-from-inning`  0)
                        ))
  THEN  Try  ((((RWO  "filter\_append\_sq"  0  THENM  (Reduce  0  THEN  SplitOnConclITE))
                          THENA  UsingVars  [`A';`V']  Auto
                          )
                        THEN  RepUR  ``rcvd-inning-gt  rcv-vote?  cs-initial-rcv  cs-rcv-vote  rcvd-vote``  -1
                        THEN  Auto
                        THEN  Try  ((RWO  "append-nil"  0  THEN  Auto))
                        THEN  Try  ((RW  assert\_pushdownC  (-1)  THEN  Auto))))
  THEN  Try  (\mbackslash{}p. 
                      ((Using  [`i',get\_addressed\_subterm  [2;1;1;1]  (concl  p)]  (FLemma  `rcvd-innings-nil`  [-7])\mcdot{}
                          THEN  Auto
                          )
                        THEN  HypSubst'  (-1)  0
                        THEN  Auto)  p\mcdot{})
  THEN  Try  (\mbackslash{}p. 
                      ((...\mcdot{}
                          THENA  Complete  (Auto)
                          )
                        THEN  HypSubst'  -1  0
                        THEN  ...
                        THEN  Try  (SplitOnConclITE)
                        THEN  Reduce  0
                        THEN  Auto)  p\mcdot{})
  THEN  Try  (Complete  ((\mbackslash{}p.  Subst  (mk\_sqequal\_term  (get\_addressed\_subterm  [3;2]  (concl  p))\mkleeneopen{}[]\mkleeneclose{})  0  p\mcdot{}
                                            THENL  [(...
                                                            THEN  Try  (SplitOnConclITE)
                                                            THEN  Reduce  0
                                                            THEN  Auto)
                                                        ;  (RWO  "append-nil"  0  THEN  Complete  (Auto))]
                                          ))))

---

Home Index