---

Step * 4 of Lemma consensus-ts6-reachability1


1. [V] : Type
2. A : Id List@i
3. W : {a:Id| (a ∈ A)}  List List@i
⊢ ∀ys:consensus-event(V;A) List. ∀y:consensus-event(V;A).
    ((∀x,y:{a:Id| (a ∈ A)}  ─→ (consensus-event(V;A) List). ∀a:{a:Id| (a ∈ A)} .
        ((∀b:{a:Id| (a ∈ A)} . ∀i:ℕ. ∀z:ℕi × V?.
            ((consensus-message(b;i;z) ∈ ys)
            ⇒ let i',est,knw = consensus-accum-state(A;x b) in 
               (i ≤ i')
               ∧ case z
                  of inl(p) =>
                  let j,v = p 
                  in (↑j ∈ dom(est)) ∧ (∀k:ℤ. (¬↑k ∈ dom(est)) supposing (k < i and j < k)) ∧ (v = est(j) ∈ V)
                  | inr(a) =>
                  ∀j:ℤ. ¬↑j ∈ dom(est) supposing j < i))
           ⇒ (∀v:V. ∀j:ℕ||ys||.
                 let i,est,knw = consensus-accum-state(A;(x a) @ firstn(j;ys)) in 
                 (¬(i ∈ fpf-domain(est))) ∧ may consider v in inning i based on knowledge (knw) 
                 supposing ys[j] = Archive(v) ∈ consensus-event(V;A))
           ⇒ (x (ts-rel(consensus-ts6(V;A;W))^*) y)) supposing 
           (((y a) = ((x a) @ ys) ∈ (consensus-event(V;A) List)) and 
           (∀b:{a:Id| (a ∈ A)} . (y b) = (x b) ∈ (consensus-event(V;A) List) supposing ¬(b = a ∈ Id))))
    ⇒ (∀x,y@0:{a:Id| (a ∈ A)}  ─→ (consensus-event(V;A) List). ∀a:{a:Id| (a ∈ A)} .
          ((∀b:{a:Id| (a ∈ A)} . ∀i:ℕ. ∀z:ℕi × V?.
              ((consensus-message(b;i;z) ∈ ys @ [y])
              ⇒ let i',est,knw = consensus-accum-state(A;x b) in 
                 (i ≤ i')
                 ∧ case z
                    of inl(p) =>
                    let j,v = p 
                    in (↑j ∈ dom(est)) ∧ (∀k:ℤ. (¬↑k ∈ dom(est)) supposing (k < i and j < k)) ∧ (v = est(j) ∈ V)
                    | inr(a) =>
                    ∀j:ℤ. ¬↑j ∈ dom(est) supposing j < i))
             ⇒ (∀v:V. ∀j:ℕ||ys @ [y]||.
                   let i,est,knw = consensus-accum-state(A;(x a) @ firstn(j;ys @ [y])) in 
                   (¬(i ∈ fpf-domain(est))) ∧ may consider v in inning i based on knowledge (knw) 
                   supposing ys @ [y][j] = Archive(v) ∈ consensus-event(V;A))
             ⇒ (x (ts-rel(consensus-ts6(V;A;W))^*) y@0)) supposing 
             (((y@0 a) = ((x a) @ ys @ [y]) ∈ (consensus-event(V;A) List)) and 
             (∀b:{a:Id| (a ∈ A)} . (y@0 b) = (x b) ∈ (consensus-event(V;A) List) supposing ¬(b = a ∈ Id)))))
BY
{ (UnivCD THENA Try (QuickAuto))⋅ }

1
1. [V] : Type
2. A : Id List@i
3. W : {a:Id| (a ∈ A)}  List List@i
4. ys : consensus-event(V;A) List@i
5. y : consensus-event(V;A)@i
6. ∀x,y:{a:Id| (a ∈ A)}  ─→ (consensus-event(V;A) List). ∀a:{a:Id| (a ∈ A)} .
     ((∀b:{a:Id| (a ∈ A)} . ∀i:ℕ. ∀z:ℕi × V?.
         ((consensus-message(b;i;z) ∈ ys)
         ⇒ let i',est,knw = consensus-accum-state(A;x b) in 
            (i ≤ i')
            ∧ case z
               of inl(p) =>
               let j,v = p 
               in (↑j ∈ dom(est)) ∧ (∀k:ℤ. (¬↑k ∈ dom(est)) supposing (k < i and j < k)) ∧ (v = est(j) ∈ V)
               | inr(a) =>
               ∀j:ℤ. ¬↑j ∈ dom(est) supposing j < i))
        ⇒ (∀v:V. ∀j:ℕ||ys||.
              let i,est,knw = consensus-accum-state(A;(x a) @ firstn(j;ys)) in 
              (¬(i ∈ fpf-domain(est))) ∧ may consider v in inning i based on knowledge (knw) 
              supposing ys[j] = Archive(v) ∈ consensus-event(V;A))
        ⇒ (x (ts-rel(consensus-ts6(V;A;W))^*) y)) supposing 
        (((y a) = ((x a) @ ys) ∈ (consensus-event(V;A) List)) and 
        (∀b:{a:Id| (a ∈ A)} . (y b) = (x b) ∈ (consensus-event(V;A) List) supposing ¬(b = a ∈ Id)))@i
7. x : {a:Id| (a ∈ A)}  ─→ (consensus-event(V;A) List)@i
8. y@0 : {a:Id| (a ∈ A)}  ─→ (consensus-event(V;A) List)@i
9. a : {a:Id| (a ∈ A)} @i
10. ∀b:{a:Id| (a ∈ A)} . (y@0 b) = (x b) ∈ (consensus-event(V;A) List) supposing ¬(b = a ∈ Id)
11. (y@0 a) = ((x a) @ ys @ [y]) ∈ (consensus-event(V;A) List)
12. ∀b:{a:Id| (a ∈ A)} . ∀i:ℕ. ∀z:ℕi × V?.
      ((consensus-message(b;i;z) ∈ ys @ [y])
      ⇒ let i',est,knw = consensus-accum-state(A;x b) in 
         (i ≤ i')
         ∧ case z
            of inl(p) =>
            let j,v = p 
            in (↑j ∈ dom(est)) ∧ (∀k:ℤ. (¬↑k ∈ dom(est)) supposing (k < i and j < k)) ∧ (v = est(j) ∈ V)
            | inr(a) =>
            ∀j:ℤ. ¬↑j ∈ dom(est) supposing j < i)@i
13. ∀v:V. ∀j:ℕ||ys @ [y]||.
      let i,est,knw = consensus-accum-state(A;(x a) @ firstn(j;ys @ [y])) in 
      (¬(i ∈ fpf-domain(est))) ∧ may consider v in inning i based on knowledge (knw) 
      supposing ys @ [y][j] = Archive(v) ∈ consensus-event(V;A)@i
⊢ x (ts-rel(consensus-ts6(V;A;W))^*) y@0

2
.....wf..... 
1. V : Type
2. A : Id List@i
3. W : {a:Id| (a ∈ A)}  List List@i
4. ys : consensus-event(V;A) List@i
5. y : consensus-event(V;A)@i
6. ∀x,y:{a:Id| (a ∈ A)}  ─→ (consensus-event(V;A) List). ∀a:{a:Id| (a ∈ A)} .
     ((∀b:{a:Id| (a ∈ A)} . ∀i:ℕ. ∀z:ℕi × V?.
         ((consensus-message(b;i;z) ∈ ys)
         ⇒ let i',est,knw = consensus-accum-state(A;x b) in 
            (i ≤ i')
            ∧ case z
               of inl(p) =>
               let j,v = p 
               in (↑j ∈ dom(est)) ∧ (∀k:ℤ. (¬↑k ∈ dom(est)) supposing (k < i and j < k)) ∧ (v = est(j) ∈ V)
               | inr(a) =>
               ∀j:ℤ. ¬↑j ∈ dom(est) supposing j < i))
        ⇒ (∀v:V. ∀j:ℕ||ys||.
              let i,est,knw = consensus-accum-state(A;(x a) @ firstn(j;ys)) in 
              (¬(i ∈ fpf-domain(est))) ∧ may consider v in inning i based on knowledge (knw) 
              supposing ys[j] = Archive(v) ∈ consensus-event(V;A))
        ⇒ (x (ts-rel(consensus-ts6(V;A;W))^*) y)) supposing 
        (((y a) = ((x a) @ ys) ∈ (consensus-event(V;A) List)) and 
        (∀b:{a:Id| (a ∈ A)} . (y b) = (x b) ∈ (consensus-event(V;A) List) supposing ¬(b = a ∈ Id)))@i
7. x : {a:Id| (a ∈ A)}  ─→ (consensus-event(V;A) List)@i
8. y@0 : {a:Id| (a ∈ A)}  ─→ (consensus-event(V;A) List)@i
9. a : {a:Id| (a ∈ A)} @i
10. ∀b:{a:Id| (a ∈ A)} . (y@0 b) = (x b) ∈ (consensus-event(V;A) List) supposing ¬(b = a ∈ Id)
11. (y@0 a) = ((x a) @ ys @ [y]) ∈ (consensus-event(V;A) List)
12. ∀b:{a:Id| (a ∈ A)} . ∀i:ℕ. ∀z:ℕi × V?.
      ((consensus-message(b;i;z) ∈ ys @ [y])
      ⇒ let i',est,knw = consensus-accum-state(A;x b) in 
         (i ≤ i')
         ∧ case z
            of inl(p) =>
            let j,v = p 
            in (↑j ∈ dom(est)) ∧ (∀k:ℤ. (¬↑k ∈ dom(est)) supposing (k < i and j < k)) ∧ (v = est(j) ∈ V)
            | inr(a) =>
            ∀j:ℤ. ¬↑j ∈ dom(est) supposing j < i)@i
⊢ ∀v:V. ∀j:ℕ||ys @ [y]||.
    let i,est,knw = consensus-accum-state(A;(x a) @ firstn(j;ys @ [y])) in 
    (¬(i ∈ fpf-domain(est))) ∧ may consider v in inning i based on knowledge (knw) 
    supposing ys @ [y][j] = Archive(v) ∈ consensus-event(V;A) ∈ ℙ

3
.....wf..... 
1. V : Type
2. A : Id List@i
3. W : {a:Id| (a ∈ A)}  List List@i
4. ys : consensus-event(V;A) List@i
5. y : consensus-event(V;A)@i
6. ∀x,y:{a:Id| (a ∈ A)}  ─→ (consensus-event(V;A) List). ∀a:{a:Id| (a ∈ A)} .
     ((∀b:{a:Id| (a ∈ A)} . ∀i:ℕ. ∀z:ℕi × V?.
         ((consensus-message(b;i;z) ∈ ys)
         ⇒ let i',est,knw = consensus-accum-state(A;x b) in 
            (i ≤ i')
            ∧ case z
               of inl(p) =>
               let j,v = p 
               in (↑j ∈ dom(est)) ∧ (∀k:ℤ. (¬↑k ∈ dom(est)) supposing (k < i and j < k)) ∧ (v = est(j) ∈ V)
               | inr(a) =>
               ∀j:ℤ. ¬↑j ∈ dom(est) supposing j < i))
        ⇒ (∀v:V. ∀j:ℕ||ys||.
              let i,est,knw = consensus-accum-state(A;(x a) @ firstn(j;ys)) in 
              (¬(i ∈ fpf-domain(est))) ∧ may consider v in inning i based on knowledge (knw) 
              supposing ys[j] = Archive(v) ∈ consensus-event(V;A))
        ⇒ (x (ts-rel(consensus-ts6(V;A;W))^*) y)) supposing 
        (((y a) = ((x a) @ ys) ∈ (consensus-event(V;A) List)) and 
        (∀b:{a:Id| (a ∈ A)} . (y b) = (x b) ∈ (consensus-event(V;A) List) supposing ¬(b = a ∈ Id)))@i
7. x : {a:Id| (a ∈ A)}  ─→ (consensus-event(V;A) List)@i
8. y@0 : {a:Id| (a ∈ A)}  ─→ (consensus-event(V;A) List)@i
9. a : {a:Id| (a ∈ A)} @i
10. ∀b:{a:Id| (a ∈ A)} . (y@0 b) = (x b) ∈ (consensus-event(V;A) List) supposing ¬(b = a ∈ Id)
11. (y@0 a) = ((x a) @ ys @ [y]) ∈ (consensus-event(V;A) List)
⊢ ∀b:{a:Id| (a ∈ A)} . ∀i:ℕ. ∀z:ℕi × V?.
    ((consensus-message(b;i;z) ∈ ys @ [y])
    ⇒ let i',est,knw = consensus-accum-state(A;x b) in 
       (i ≤ i')
       ∧ case z
          of inl(p) =>
          let j,v = p 
          in (↑j ∈ dom(est)) ∧ (∀k:ℤ. (¬↑k ∈ dom(est)) supposing (k < i and j < k)) ∧ (v = est(j) ∈ V)
          | inr(a) =>
          ∀j:ℤ. ¬↑j ∈ dom(est) supposing j < i) ∈ ℙ

4
.....wf..... 
1. V : Type
2. A : Id List@i
3. W : {a:Id| (a ∈ A)}  List List@i
4. ys : consensus-event(V;A) List@i
5. y : consensus-event(V;A)@i
⊢ ∀x,y:{a:Id| (a ∈ A)}  ─→ (consensus-event(V;A) List). ∀a:{a:Id| (a ∈ A)} .
    ((∀b:{a:Id| (a ∈ A)} . ∀i:ℕ. ∀z:ℕi × V?.
        ((consensus-message(b;i;z) ∈ ys)
        ⇒ let i',est,knw = consensus-accum-state(A;x b) in 
           (i ≤ i')
           ∧ case z
              of inl(p) =>
              let j,v = p 
              in (↑j ∈ dom(est)) ∧ (∀k:ℤ. (¬↑k ∈ dom(est)) supposing (k < i and j < k)) ∧ (v = est(j) ∈ V)
              | inr(a) =>
              ∀j:ℤ. ¬↑j ∈ dom(est) supposing j < i))
       ⇒ (∀v:V. ∀j:ℕ||ys||.
             let i,est,knw = consensus-accum-state(A;(x a) @ firstn(j;ys)) in 
             (¬(i ∈ fpf-domain(est))) ∧ may consider v in inning i based on knowledge (knw) 
             supposing ys[j] = Archive(v) ∈ consensus-event(V;A))
       ⇒ (x (ts-rel(consensus-ts6(V;A;W))^*) y)) supposing 
       (((y a) = ((x a) @ ys) ∈ (consensus-event(V;A) List)) and 
       (∀b:{a:Id| (a ∈ A)} . (y b) = (x b) ∈ (consensus-event(V;A) List) supposing ¬(b = a ∈ Id))) ∈ ℙ

---

Latex:



1.  [V]  :  Type
2.  A  :  Id  List@i
3.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List@i
\mvdash{}  \mforall{}ys:consensus-event(V;A)  List.  \mforall{}y:consensus-event(V;A).
        ((\mforall{}x,y:\{a:Id|  (a  \mmember{}  A)\}    {}\mrightarrow{}  (consensus-event(V;A)  List).  \mforall{}a:\{a:Id|  (a  \mmember{}  A)\}  .
                ((\mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  \mforall{}i:\mBbbN{}.  \mforall{}z:\mBbbN{}i  \mtimes{}  V?.
                        ((consensus-message(b;i;z)  \mmember{}  ys)
                        {}\mRightarrow{}  let  i',est,knw  =  consensus-accum-state(A;x  b)  in 
                              (i  \mleq{}  i')
                              \mwedge{}  case  z
                                    of  inl(p)  =>
                                    let  j,v  =  p 
                                    in  (\muparrow{}j  \mmember{}  dom(est))  \mwedge{}  (\mforall{}k:\mBbbZ{}.  (\mneg{}\muparrow{}k  \mmember{}  dom(est))  supposing  (k  <  i  and  j  <  k))  \mwedge{}  (v  =  e\000Cst(j))
                                    |  inr(a)  =>
                                    \mforall{}j:\mBbbZ{}.  \mneg{}\muparrow{}j  \mmember{}  dom(est)  supposing  j  <  i))
                      {}\mRightarrow{}  (\mforall{}v:V.  \mforall{}j:\mBbbN{}||ys||.
                                  let  i,est,knw  =  consensus-accum-state(A;(x  a)  @  firstn(j;ys))  in 
                                  (\mneg{}(i  \mmember{}  fpf-domain(est)))  \mwedge{}  may  consider  v  in  inning  i  based  on  knowledge  (knw) 
                                  supposing  ys[j]  =  Archive(v))
                      {}\mRightarrow{}  (x 
                              (ts-rel(consensus-ts6(V;A;W))\^{}*) 
                              y))  supposing 
                      (((y  a)  =  ((x  a)  @  ys))  and 
                      (\mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  (y  b)  =  (x  b)  supposing  \mneg{}(b  =  a))))
        {}\mRightarrow{}  (\mforall{}x,y@0:\{a:Id|  (a  \mmember{}  A)\}    {}\mrightarrow{}  (consensus-event(V;A)  List).  \mforall{}a:\{a:Id|  (a  \mmember{}  A)\}  .
                    ((\mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  \mforall{}i:\mBbbN{}.  \mforall{}z:\mBbbN{}i  \mtimes{}  V?.
                            ((consensus-message(b;i;z)  \mmember{}  ys  @  [y])
                            {}\mRightarrow{}  let  i',est,knw  =  consensus-accum-state(A;x  b)  in 
                                  (i  \mleq{}  i')
                                  \mwedge{}  case  z
                                        of  inl(p)  =>
                                        let  j,v  =  p 
                                        in  (\muparrow{}j  \mmember{}  dom(est))
                                              \mwedge{}  (\mforall{}k:\mBbbZ{}.  (\mneg{}\muparrow{}k  \mmember{}  dom(est))  supposing  (k  <  i  and  j  <  k))
                                              \mwedge{}  (v  =  est(j))
                                        |  inr(a)  =>
                                        \mforall{}j:\mBbbZ{}.  \mneg{}\muparrow{}j  \mmember{}  dom(est)  supposing  j  <  i))
                          {}\mRightarrow{}  (\mforall{}v:V.  \mforall{}j:\mBbbN{}||ys  @  [y]||.
                                      let  i,est,knw  =  consensus-accum-state(A;(x  a)  @  firstn(j;ys  @  [y]))  in 
                                      (\mneg{}(i  \mmember{}  fpf-domain(est)))  \mwedge{}  may  consider  v  in  inning  i  based  on  knowledge  (knw) 
                                      supposing  ys  @  [y][j]  =  Archive(v))
                          {}\mRightarrow{}  (x 
                                  (ts-rel(consensus-ts6(V;A;W))\^{}*) 
                                  y@0))  supposing 
                          (((y@0  a)  =  ((x  a)  @  ys  @  [y]))  and 
                          (\mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  (y@0  b)  =  (x  b)  supposing  \mneg{}(b  =  a)))))


By

(UnivCD  THENA  Try  (QuickAuto))\mcdot{}

---

Home Index