---

Step * 1 of Lemma archive-condition-innings


1. V : Type
2. A : Id List
3. t : ℕ+
4. f : (V List) ─→ V
5. L1 : consensus-rcv(V;A) List
6. L2 : consensus-rcv(V;A) List
7. n1 : ℤ
8. n2 : ℤ
9. v1 : V
10. v2 : V
11. archive-condition(V;A;t;f;n1;v1;L1)
12. L1 < L2
13. L' : consensus-rcv(V;A) List
14. r : consensus-rcv(V;A)
15. L2 = (L' @ [r]) ∈ (consensus-rcv(V;A) List)
16. (L' = [] ∈ (consensus-rcv(V;A) List))
∧ (((r = Init[v2] ∈ consensus-rcv(V;A)) ∧ (n2 = 0 ∈ ℤ))
  ∨ ((0 ≤ n2) ∧ (∃a:{a:Id| (a ∈ A)} . (r = Vote[a;n2;v2] ∈ consensus-rcv(V;A)))))
⊢ n1 < n2
BY
{ ((Assert L1 < L' @ [r] BY
          Auto)
   THEN RWO "proper-iseg-append-one" (-1)
   THEN Auto
   THEN ((HypSubst' -3 -1 THENA Auto) THEN (FLemma `iseg_nil` [-1] THENA Auto))
   THEN DVar `L1'
   THEN Reduce (-1)
   THEN Auto
   THEN OnMaybeHyp 10 (\h. (FLemma `archive-condition-nil` [h] THEN Auto))) }

---

Latex:



1.  V  :  Type
2.  A  :  Id  List
3.  t  :  \mBbbN{}\msupplus{}
4.  f  :  (V  List)  {}\mrightarrow{}  V
5.  L1  :  consensus-rcv(V;A)  List
6.  L2  :  consensus-rcv(V;A)  List
7.  n1  :  \mBbbZ{}
8.  n2  :  \mBbbZ{}
9.  v1  :  V
10.  v2  :  V
11.  archive-condition(V;A;t;f;n1;v1;L1)
12.  L1  <  L2
13.  L'  :  consensus-rcv(V;A)  List
14.  r  :  consensus-rcv(V;A)
15.  L2  =  (L'  @  [r])
16.  (L'  =  [])
\mwedge{}  (((r  =  Init[v2])  \mwedge{}  (n2  =  0))  \mvee{}  ((0  \mleq{}  n2)  \mwedge{}  (\mexists{}a:\{a:Id|  (a  \mmember{}  A)\}  .  (r  =  Vote[a;n2;v2]))))
\mvdash{}  n1  <  n2


By

((Assert  L1  <  L'  @  [r]  BY
                Auto)
  THEN  RWO  "proper-iseg-append-one"  (-1)
  THEN  Auto
  THEN  ((HypSubst'  -3  -1  THENA  Auto)  THEN  (FLemma  `iseg\_nil`  [-1]  THENA  Auto))
  THEN  DVar  `L1'
  THEN  Reduce  (-1)
  THEN  Auto
  THEN  OnMaybeHyp  10  (\mbackslash{}h.  (FLemma  `archive-condition-nil`  [h]  THEN  Auto)))

---

Home Index