---

Step * of Lemma cs-inning-committable-step

∀V:Type
  ((∀v,v':V.  Dec(v = v' ∈ V))
  ⇒ (∀A:Id List. ∀W:{a:Id| (a ∈ A)}  List List. ∀x,y:ts-reachable(consensus-ts4(V;A;W)). ∀i:ℕ. ∀v:V.
        ((x ts-rel(consensus-ts4(V;A;W)) y)
        ⇒ in state y, inning i could commit v 
        ⇒ in state x, inning i could commit v )))
BY
{ (Auto
   THEN Try ((DVar `y' THEN RepUR ``ts-type consensus-ts4`` -5 THEN Complete (Auto)))
   THEN (Assert ∀a:{a:Id| (a ∈ A)} . ∀i:ℤ.  ((i ∈ fpf-domain(Estimate(x;a))) ⇒ (i ≤ Inning(x;a))) BY
               ((D 0 THENA Auto)
                THEN (InstLemma `consensus-ts4-estimate-domain` [⌈V⌉;⌈A⌉;⌈W⌉;⌈a⌉;⌈x⌉]⋅ THENA Auto)
                THEN Trivial))) }

1
1. V : Type@i'
2. ∀v,v':V.  Dec(v = v' ∈ V)@i
3. A : Id List@i
4. W : {a:Id| (a ∈ A)}  List List@i
5. x : ts-reachable(consensus-ts4(V;A;W))@i
6. y : ts-reachable(consensus-ts4(V;A;W))@i
7. i : ℕ@i
8. v : V@i
9. x ts-rel(consensus-ts4(V;A;W)) y@i
10. in state y, inning i could commit v @i
11. ∀a:{a:Id| (a ∈ A)} . ∀i:ℤ.  ((i ∈ fpf-domain(Estimate(x;a))) ⇒ (i ≤ Inning(x;a)))
⊢ in state x, inning i could commit v 

---

Latex:


\mforall{}V:Type
    ((\mforall{}v,v':V.    Dec(v  =  v'))
    {}\mRightarrow{}  (\mforall{}A:Id  List.  \mforall{}W:\{a:Id|  (a  \mmember{}  A)\}    List  List.  \mforall{}x,y:ts-reachable(consensus-ts4(V;A;W)).  \mforall{}i:\mBbbN{}.  \mforall{}v:V\000C.
                ((x  ts-rel(consensus-ts4(V;A;W))  y)
                {}\mRightarrow{}  in  state  y,  inning  i  could  commit  v 
                {}\mRightarrow{}  in  state  x,  inning  i  could  commit  v  )))


By

(Auto
  THEN  Try  ((DVar  `y'  THEN  RepUR  ``ts-type  consensus-ts4``  -5  THEN  Complete  (Auto)))
  THEN  (Assert  \mforall{}a:\{a:Id|  (a  \mmember{}  A)\}  .  \mforall{}i:\mBbbZ{}.    ((i  \mmember{}  fpf-domain(Estimate(x;a)))  {}\mRightarrow{}  (i  \mleq{}  Inning(x;a)))  BY
                          ((D  0  THENA  Auto)
                            THEN  (InstLemma  `consensus-ts4-estimate-domain`  [\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}W\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  Trivial)))

---

Home Index