---

Step * of Lemma three-cs-archive-invariant

∀[V:Type]
  ∀eq:EqDecider(V). ∀A:Id List. ∀t:ℕ+. ∀f:(V List) ─→ V.
    ((∀vs:V List. (f vs ∈ vs) supposing ||vs|| ≥ 1 )
    ⇒ (∀s:ts-reachable(three-consensus-ts(V;A;t;f)). ∀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)
          ⇒ (∃a∈A. (||s a|| ≥ 1 ) ∧ (hd(s a) = Init[v] ∈ consensus-rcv(V;A))))))
BY
{ ((RepeatFor 6 ((D 0 THENA Auto))
    THEN (InstLemma `decidable-equal-deq` [⌈V⌉]⋅ THENA Auto)
    THEN (Assert ∀s:{a:Id| (a ∈ A)}  ─→ (consensus-rcv(V;A) List). ∀v:V.
                   Dec((∃a∈A. (||s a|| ≥ 1 ) ∧ (hd(s a) = Init[v] ∈ consensus-rcv(V;A)))) BY
                (Unfold `and` 0
                 THEN Fold `cand` 0
                 THEN (UnivCD THENA Auto)
                 THEN GenConcl ⌈A = L ∈ ({a:Id| (a ∈ A)}  List)⌉⋅
                 THEN Auto)))
   THEN (Assert ts-reachable(three-consensus-ts(V;A;t;f)) ⊆r ({a:Id| (a ∈ A)}  ─→ (consensus-rcv(V;A) List)) BY
               (D 0 THEN Auto THEN D (-1) THEN DoSubsume THEN Auto))
   THEN ((BLemma `ts-reachable-induction` THENA 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 Auto⋅
         THEN AllHyps h.(Unfold `ts-rel` h THEN RepUR ``three-consensus-ts`` h THEN ExRepD) )⋅) }

1
1. [V] : Type
2. eq : EqDecider(V)@i
3. A : Id List@i
4. t : ℕ+@i
5. f : (V List) ─→ V@i
6. ∀vs:V List. (f vs ∈ vs) supposing ||vs|| ≥ 1 @i
7. ∀x,y:V.  Dec(x = y ∈ V)
8. ∀s:{a:Id| (a ∈ A)}  ─→ (consensus-rcv(V;A) List). ∀v:V.
     Dec((∃a∈A. (||s a|| ≥ 1 ) ∧ (hd(s a) = Init[v] ∈ consensus-rcv(V;A))))
9. ts-reachable(three-consensus-ts(V;A;t;f)) ⊆r ({a:Id| (a ∈ A)}  ─→ (consensus-rcv(V;A) List))
10. s : ts-reachable(three-consensus-ts(V;A;t;f))@i
11. y : ts-reachable(three-consensus-ts(V;A;t;f))@i
12. ∀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)
      ⇒ (∃a∈A. (||s a|| ≥ 1 ) ∧ (hd(s a) = Init[v] ∈ consensus-rcv(V;A))))@i
13. a1 : {a:Id| (a ∈ A)} @i
14. e : consensus-rcv(V;A)@i
15. ∀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 a1))))@i
16. ∀b:{a:Id| (a ∈ A)} . ((¬(b = a1 ∈ Id)) ⇒ ((y b) = (s b) ∈ (consensus-rcv(V;A) List)))@i
17. (y a1) = ((s a1) @ [e]) ∈ (consensus-rcv(V;A) List)@i
18. v : V@i
19. a : {a:Id| (a ∈ A)} @i
20. n : ℤ@i
21. L : consensus-rcv(V;A) List@i
22. L ≤ y a@i
23. archive-condition(V;A;t;f;n;v;L)@i
⊢ (∃a∈A. (||y a|| ≥ 1 ) ∧ (hd(y a) = Init[v] ∈ consensus-rcv(V;A)))

---

Latex:


\mforall{}[V:Type]
    \mforall{}eq:EqDecider(V).  \mforall{}A:Id  List.  \mforall{}t:\mBbbN{}\msupplus{}.  \mforall{}f:(V  List)  {}\mrightarrow{}  V.
        ((\mforall{}vs:V  List.  (f  vs  \mmember{}  vs)  supposing  ||vs||  \mgeq{}  1  )
        {}\mRightarrow{}  (\mforall{}s:ts-reachable(three-consensus-ts(V;A;t;f)).  \mforall{}v:V.  \mforall{}a:\{a:Id|  (a  \mmember{}  A)\}  .  \mforall{}n:\mBbbZ{}.
                \mforall{}L:consensus-rcv(V;A)  List.
                    (L  \mleq{}  s  a
                    {}\mRightarrow{}  archive-condition(V;A;t;f;n;v;L)
                    {}\mRightarrow{}  (\mexists{}a\mmember{}A.  (||s  a||  \mgeq{}  1  )  \mwedge{}  (hd(s  a)  =  Init[v])))))


By

((RepeatFor  6  ((D  0  THENA  Auto))
    THEN  (InstLemma  `decidable-equal-deq`  [\mkleeneopen{}V\mkleeneclose{}]\mcdot{}  THENA  Auto)
    THEN  (Assert  \mforall{}s:\{a:Id|  (a  \mmember{}  A)\}    {}\mrightarrow{}  (consensus-rcv(V;A)  List).  \mforall{}v:V.
                                  Dec((\mexists{}a\mmember{}A.  (||s  a||  \mgeq{}  1  )  \mwedge{}  (hd(s  a)  =  Init[v])))  BY
                            (Unfold  `and`  0
                              THEN  Fold  `cand`  0
                              THEN  (UnivCD  THENA  Auto)
                              THEN  GenConcl  \mkleeneopen{}A  =  L\mkleeneclose{}\mcdot{}
                              THEN  Auto)))
  THEN  (Assert  ts-reachable(three-consensus-ts(V;A;t;f))  \msubseteq{}r  (\{a:Id|  (a  \mmember{}  A)\}    {}\mrightarrow{}  (consensus-rcv(V;A)  \000CList))  BY
                          (D  0  THEN  Auto  THEN  D  (-1)  THEN  DoSubsume  THEN  Auto))
  THEN  ((BLemma  `ts-reachable-induction`  THENA  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  Auto\mcdot{}
              THEN  AllHyps  h.(Unfold  `ts-rel`  h  THEN  RepUR  ``three-consensus-ts``  h  THEN  ExRepD)  )\mcdot{})

---

Home Index