---

Step * of Lemma three-cs-archive-condition

∀V:Type. ∀A:Id List. ∀t:ℕ+. ∀f:(V List) ─→ V. ∀s:ts-type(three-consensus-ts(V;A;t;f)).
  ((ts-init(three-consensus-ts(V;A;t;f)) (ts-rel(three-consensus-ts(V;A;t;f))^*) s)
  ⇒ (∀v:V. ∀a:{a:Id| (a ∈ A)} . ∀n:ℕ+. ∀L:consensus-rcv(V;A) List.
        (L ≤ s a
        ⇒ archive-condition(V;A;t;f;n;v;L)
        ⇒ (∃as:{a:Id| (a ∈ A)}  List
             (no_repeats({a:Id| (a ∈ A)} ;as)
             ∧ (||as|| = ((2 * t) + 1) ∈ ℤ)
             ∧ (∃vs:V List
                 ((||vs|| = ||as|| ∈ ℤ)
                 ∧ (v = (f vs) ∈ V)
                 ∧ (∀i:ℕ||as||
                      ∃L:consensus-rcv(V;A) List. (L ≤ s as[i] ∧ archive-condition(V;A;t;f;n - 1;vs[i];L))))))))))
BY
{ (RepeatFor 4 ((D 0 THENA Auto))
   THEN (BLemma `ts-reachable-induction3`
         THENA (Auto THEN DVar `s' THEN AllHyps h.(RepUR ``ts-type three-consensus-ts`` h THEN Auto) )
         )
   THEN Try ((RepUR ``ts-init three-consensus-ts`` 0
              THEN Auto
              THEN (FLemma `iseg_nil` [-2] THENA Auto)
              THEN DVar `L'
              THEN Reduce (-1)
              THEN Auto
              THEN FLemma `archive-condition-nil` [-2]
              THEN Auto))
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN RepUR ``ts-type three-consensus-ts`` -2
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN Thin (-1)
   THEN RepUR ``ts-type three-consensus-ts`` -1
   THEN RepUR ``ts-rel three-consensus-ts`` 0
   THEN Auto) }

1
1. V : Type@i'
2. A : Id List@i
3. t : ℕ+@i
4. f : (V List) ─→ V@i
5. s : {a:Id| (a ∈ A)}  ─→ (consensus-rcv(V;A) List)@i
6. ts-init(three-consensus-ts(V;A;t;f)) (ts-rel(three-consensus-ts(V;A;t;f))^*) s@i
7. y : {a:Id| (a ∈ A)}  ─→ (consensus-rcv(V;A) List)@i
8. ∀v:V. ∀a:{a:Id| (a ∈ A)} . ∀n:ℕ+. ∀L:consensus-rcv(V;A) List.
     (L ≤ s a
     ⇒ archive-condition(V;A;t;f;n;v;L)
     ⇒ (∃as:{a:Id| (a ∈ A)}  List
          (no_repeats({a:Id| (a ∈ A)} ;as)
          ∧ (||as|| = ((2 * t) + 1) ∈ ℤ)
          ∧ (∃vs:V List
              ((||vs|| = ||as|| ∈ ℤ)
              ∧ (v = (f vs) ∈ V)
              ∧ (∀i:ℕ||as||
                   ∃L:consensus-rcv(V;A) List. (L ≤ s as[i] ∧ archive-condition(V;A;t;f;n - 1;vs[i];L))))))))@i
9. ∃a:{a:Id| (a ∈ A)} 
    ∃e:consensus-rcv(V;A)
     ((∀b:{a:Id| (a ∈ A)} . ∀i:ℕ. ∀v:V.
         ((e = Vote[b;i;v] ∈ consensus-rcv(V;A))
         ⇒ ((∃L:consensus-rcv(V;A) List. (L ≤ s b ∧ archive-condition(V;A;t;f;i;v;L))) ∧ (¬(e ∈ s a)))))
     ∧ (∀b:{a:Id| (a ∈ A)} . ((¬(b = a ∈ Id)) ⇒ ((y b) = (s b) ∈ (consensus-rcv(V;A) List))))
     ∧ ((y a) = ((s a) @ [e]) ∈ (consensus-rcv(V;A) List)))@i
10. v : V@i
11. a : {a:Id| (a ∈ A)} @i
12. n : ℕ+@i
13. L : consensus-rcv(V;A) List@i
14. L ≤ y a@i
15. archive-condition(V;A;t;f;n;v;L)@i
⊢ ∃as:{a:Id| (a ∈ A)}  List
   (no_repeats({a:Id| (a ∈ A)} ;as)
   ∧ (||as|| = ((2 * t) + 1) ∈ ℤ)
   ∧ (∃vs:V List
       ((||vs|| = ||as|| ∈ ℤ)
       ∧ (v = (f vs) ∈ V)
       ∧ (∀i:ℕ||as||. ∃L:consensus-rcv(V;A) List. (L ≤ y as[i] ∧ archive-condition(V;A;t;f;n - 1;vs[i];L))))))

---

Latex:


\mforall{}V:Type.  \mforall{}A:Id  List.  \mforall{}t:\mBbbN{}\msupplus{}.  \mforall{}f:(V  List)  {}\mrightarrow{}  V.  \mforall{}s:ts-type(three-consensus-ts(V;A;t;f)).
    ((ts-init(three-consensus-ts(V;A;t;f))  (ts-rel(three-consensus-ts(V;A;t;f))\^{}*)  s)
    {}\mRightarrow{}  (\mforall{}v:V.  \mforall{}a:\{a:Id|  (a  \mmember{}  A)\}  .  \mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}L:consensus-rcv(V;A)  List.
                (L  \mleq{}  s  a
                {}\mRightarrow{}  archive-condition(V;A;t;f;n;v;L)
                {}\mRightarrow{}  (\mexists{}as:\{a:Id|  (a  \mmember{}  A)\}    List
                          (no\_repeats(\{a:Id|  (a  \mmember{}  A)\}  ;as)
                          \mwedge{}  (||as||  =  ((2  *  t)  +  1))
                          \mwedge{}  (\mexists{}vs:V  List
                                  ((||vs||  =  ||as||)
                                  \mwedge{}  (v  =  (f  vs))
                                  \mwedge{}  (\mforall{}i:\mBbbN{}||as||
                                            \mexists{}L:consensus-rcv(V;A)  List
                                              (L  \mleq{}  s  as[i]  \mwedge{}  archive-condition(V;A;t;f;n  -  1;vs[i];L))))))))))


By

(RepeatFor  4  ((D  0  THENA  Auto))
  THEN  (BLemma  `ts-reachable-induction3`
              THENA  (Auto  THEN  DVar  `s'  THEN  AllHyps  h.(RepUR  ``ts-type  three-consensus-ts``  h  THEN  Auto)  )
              )
  THEN  Try  ((RepUR  ``ts-init  three-consensus-ts``  0
                        THEN  Auto
                        THEN  (FLemma  `iseg\_nil`  [-2]  THENA  Auto)
                        THEN  DVar  `L'
                        THEN  Reduce  (-1)
                        THEN  Auto
                        THEN  FLemma  `archive-condition-nil`  [-2]
                        THEN  Auto))
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  RepUR  ``ts-type  three-consensus-ts``  -2
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  Thin  (-1)
  THEN  RepUR  ``ts-type  three-consensus-ts``  -1
  THEN  RepUR  ``ts-rel  three-consensus-ts``  0
  THEN  Auto)

---

Home Index