Proof of Nuprl Lemma : consensus-ts6-reachability1

Step * 4 1 of Lemma consensus-ts6-reachability1

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)

{ (Using [`y', ⌈λb.if b = a then (x a) @ ys else x b fi ⌉] (BLemma `rel_star_transitivity`)⋅ THEN Try (CompleteAuto)) }

1
.....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)

            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
⊢ λb.if b = a then (x a) @ ys else x b fi  ∈ ts-type(consensus-ts6(V;A;W))

2
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)

            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))^*) (λb.if b = a then (x a) @ ys else x b fi )

3
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)

            in (↑j ∈ dom(est)) ∧ (∀k:ℤ. (¬↑k ∈ dom(est)) supposing (k < i and j < k)) ∧ (v = est(j) ∈ V)

Latex:

1. [V] : Type 2. A : Id List@i 3. W : \{a:Id| (a \mmember{} A)\} List List@i 4. ys : consensus-event(V;A) List@i 5. y : consensus-event(V;A)@i 6. \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 = est(\000Cj)) | 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 rel\_star(ts-type(consensus-ts6(V;A;W)); 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)))@i 7. x : \{a:Id| (a \mmember{} A)\} {}\mrightarrow{} (consensus-event(V;A) List)@i 8. y@0 : \{a:Id| (a \mmember{} A)\} {}\mrightarrow{} (consensus-event(V;A) List)@i 9. a : \{a:Id| (a \mmember{} A)\} @i 10. \mforall{}b:\{a:Id| (a \mmember{} A)\} . (y@0 b) = (x b) supposing \mneg{}(b = a) 11. (y@0 a) = ((x a) @ ys @ [y]) 12. \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)@i 13. \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)@i \mvdash{} x rel\_star(ts-type(consensus-ts6(V;A;W)); ts-rel(consensus-ts6(V;A;W))) y@0 By (Using [`y', \mkleeneopen{}\mlambda{}b.if b = a then (x a) @ ys else x b fi \mkleeneclose{}] (BLemma `rel\_star\_transitivity`)\mcdot{} THEN Try (CompleteAuto) ) Home Index