---

Step * 1 of Lemma three-cs-safety2


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. ∀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))))
8. v : V@i
9. s : ts-reachable(three-consensus-ts(V;A;t;f))@i
10. i : ℤ@i
11. ws : {a:Id| (a ∈ A)}  List@i
12. no_repeats({a:Id| (a ∈ A)} ;ws)@i
13. ||ws|| = ((2 * t) + 1) ∈ ℤ@i
14. (∀a∈ws.∃L:consensus-rcv(V;A) List. (L ≤ s a ∧ archive-condition(V;A;t;f;i;v;L)))@i
⊢ (∃a∈A. (||s a|| ≥ 1 ) ∧ (hd(s a) = Init[v] ∈ consensus-rcv(V;A)))
BY
{ ((DVar `ws' THEN All Reduce  THEN Auto')
   THEN (RWO "l_all_iff" (-1) THENA (Auto THEN DVar `s'⋅ THEN DoSubsume THEN Auto))
   THEN (InstHyp [⌈u⌉] (-1)⋅ THENA Auto)
   THEN ExRepD
   THEN FHyp 7 [-2;-1]
   THEN Auto) }

---

Latex:



1.  [V]  :  Type
2.  eq  :  EqDecider(V)@i
3.  A  :  Id  List@i
4.  t  :  \mBbbN{}\msupplus{}@i
5.  f  :  (V  List)  {}\mrightarrow{}  V@i
6.  \mforall{}vs:V  List.  (f  vs  \mmember{}  vs)  supposing  ||vs||  \mgeq{}  1  @i
7.  \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])))
8.  v  :  V@i
9.  s  :  ts-reachable(three-consensus-ts(V;A;t;f))@i
10.  i  :  \mBbbZ{}@i
11.  ws  :  \{a:Id|  (a  \mmember{}  A)\}    List@i
12.  no\_repeats(\{a:Id|  (a  \mmember{}  A)\}  ;ws)@i
13.  ||ws||  =  ((2  *  t)  +  1)@i
14.  (\mforall{}a\mmember{}ws.\mexists{}L:consensus-rcv(V;A)  List.  (L  \mleq{}  s  a  \mwedge{}  archive-condition(V;A;t;f;i;v;L)))@i
\mvdash{}  (\mexists{}a\mmember{}A.  (||s  a||  \mgeq{}  1  )  \mwedge{}  (hd(s  a)  =  Init[v]))


By

((DVar  `ws'  THEN  All  Reduce    THEN  Auto')
  THEN  (RWO  "l\_all\_iff"  (-1)  THENA  (Auto  THEN  DVar  `s'\mcdot{}  THEN  DoSubsume  THEN  Auto))
  THEN  (InstHyp  [\mkleeneopen{}u\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  FHyp  7  [-2;-1]
  THEN  Auto)

---

Home Index