Step * 2 2 of Lemma consensus-refinement5


1. [V] Type
2. Id List@i
3. {a:Id| (a ∈ A)}  List List@i
4. 1 < ||W||@i
5. two-intersection(A;W)@i
⊢ ∀x:ts-reachable(consensus-ts5(V;A;W))
    ((ts-final(consensus-ts5(V;A;W)) x)
     (∃y:ts-reachable(consensus-ts6(V;A;W))
         ((ts-final(consensus-ts6(V;A;W)) y)
         ∧ (((λs.cs-events-to-state(A; s)) y) x ∈ ts-type(consensus-ts5(V;A;W))))))
BY
(Auto
   THEN -2
   THEN (RepUR ``ts-type consensus-ts5`` -3 THEN -3)
   THEN RepUR ``ts-final consensus-ts5`` -1
   THEN RepUR ``ts-type consensus-ts5`` 0
   THEN ExRepD
   THEN (InstConcl [⌈λa.[Archive(v)]⌉]⋅
         THENA Try ((Auto THEN -1 THEN RepUR ``ts-type consensus-ts6`` -2 THEN Auto))
         )) }

1
.....wf..... 
1. Type
2. Id List@i
3. {a:Id| (a ∈ A)}  List List@i
4. 1 < ||W||@i
5. two-intersection(A;W)@i
6. x1 ConsensusState@i
7. x2 Knowledge(ConsensusState)@i
8. ts-init(consensus-ts5(V;A;W)) (ts-rel(consensus-ts5(V;A;W))^*) <x1, x2>@i
9. V@i
10. ∀a:{a:Id| (a ∈ A)} 
      ((Inning(x1;a) 0 ∈ ℤ)
      ∧ (Estimate(x1;a) v ∈ i:ℤ fp-> V)
      ∧ (Knowledge(x2;a) mk_fpf(A;λb.<0, ff>) ∈ b:Id fp-> ℤ × (ℤ × Top)))@i
⊢ λa.[Archive(v)] ∈ ts-reachable(consensus-ts6(V;A;W))

2
1. [V] Type
2. Id List@i
3. {a:Id| (a ∈ A)}  List List@i
4. 1 < ||W||@i
5. two-intersection(A;W)@i
6. x1 ConsensusState@i
7. x2 Knowledge(ConsensusState)@i
8. \\%4 ts-init(consensus-ts5(V;A;W)) (ts-rel(consensus-ts5(V;A;W))^*) <x1, x2>@i
9. V@i
10. ∀a:{a:Id| (a ∈ A)} 
      ((Inning(x1;a) 0 ∈ ℤ)
      ∧ (Estimate(x1;a) v ∈ i:ℤ fp-> V)
      ∧ (Knowledge(x2;a) mk_fpf(A;λb.<0, ff>) ∈ b:Id fp-> ℤ × (ℤ × Top)))@i
⊢ (ts-final(consensus-ts6(V;A;W)) a.[Archive(v)]))
∧ (cs-events-to-state(A; λa.[Archive(v)]) = <x1, x2> ∈ (ConsensusState × Knowledge(ConsensusState)))


Latex:



1.  [V]  :  Type
2.  A  :  Id  List@i
3.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List@i
4.  1  <  ||W||@i
5.  two-intersection(A;W)@i
\mvdash{}  \mforall{}x:ts-reachable(consensus-ts5(V;A;W))
        ((ts-final(consensus-ts5(V;A;W))  x)
        {}\mRightarrow{}  (\mexists{}y:ts-reachable(consensus-ts6(V;A;W))
                  ((ts-final(consensus-ts6(V;A;W))  y)  \mwedge{}  (((\mlambda{}s.cs-events-to-state(A;  s))  y)  =  x))))


By

(Auto
  THEN  D  -2
  THEN  (RepUR  ``ts-type  consensus-ts5``  -3  THEN  D  -3)
  THEN  RepUR  ``ts-final  consensus-ts5``  -1
  THEN  RepUR  ``ts-type  consensus-ts5``  0
  THEN  ExRepD
  THEN  (InstConcl  [\mkleeneopen{}\mlambda{}a.[Archive(v)]\mkleeneclose{}]\mcdot{}
              THENA  Try  ((Auto  THEN  D  -1  THEN  RepUR  ``ts-type  consensus-ts6``  -2  THEN  Auto))
              ))




Home Index