Proof of Nuprl Lemma : three-cs-archive-condition

Step * 1 2 1 2 1 2 of Lemma three-cs-archive-condition

1. V : Type@i'
2. A : Id List@i
3. t : ℕ⁺@i
4. f : (V List) ─→ V@i
5. s : {a:Id| (a ∈ A)}  ─→ (consensus-rcv(V;A) List)@i
6. ts-init(three-consensus-ts(V;A;t;f)) (ts-rel(three-consensus-ts(V;A;t;f))^*) s@i
7. y : {a:Id| (a ∈ A)}  ─→ (consensus-rcv(V;A) List)@i
8. ∀v:V. ∀a:{a:Id| (a ∈ A)} . ∀n:ℕ⁺. ∀L:consensus-rcv(V;A) List.
     (L ≤ s a
     ⇒ archive-condition(V;A;t;f;n;v;L)
     ⇒ (∃as:{a:Id| (a ∈ A)}  List
          (no_repeats({a:Id| (a ∈ A)} ;as)
          ∧ (||as|| = ((2 * t) + 1) ∈ ℤ)
          ∧ (∃vs:V List
              ((||vs|| = ||as|| ∈ ℤ)
              ∧ (v = (f vs) ∈ V)
              ∧ (∀i:ℕ||as||

                   ∃L:consensus-rcv(V;A) List. (L ≤ s as[i] ∧ archive-condition(V;A;t;f;n - 1;vs[i];L))))))))@i

9. a1 : {a:Id| (a ∈ A)} @i
10. y2 : {b:Id| (b ∈ A)} @i
11. y4 : ℕ@i
12. y5 : V@i
13. ∀b:{a:Id| (a ∈ A)} . ∀i:ℕ. ∀v:V.
((Vote[y2;y4;y5] = Vote[b;i;v] ∈ consensus-rcv(V;A))
⇒

 ((∃L:consensus-rcv(V;A) List. (L ≤ s b ∧ archive-condition(V;A;t;f;i;v;L))) ∧ (¬(Vote[y2;y4;y5] ∈ s a1))))@i

14. ∀b:{a:Id| (a ∈ A)} . ((¬(b = a1 ∈ Id)) ⇒ ((y b) = (s b) ∈ (consensus-rcv(V;A) List)))@i
15. (y a1) = ((s a1) @ [Vote[y2;y4;y5]]) ∈ (consensus-rcv(V;A) List)@i
16. v : V@i
17. n : ℕ⁺@i
18. 0 < n
19. ||values-for-distinct(IdDeq;votes-from-inning(n - 1;s a1))|| ≤ (2 * t)
20. ↑null(filter(λr.n - 1 <z inning(r);s a1))
21. ((y4 = n ∈ ℤ) ∧ (v = y5 ∈ V))
∨ ((((2 * t) + 1) ≤ ||values-for-distinct(IdDeq;votes-from-inning(n - 1;(s a1) @ [Vote[y2;y4;y5]]))||)
  ∧ ((f values-for-distinct(IdDeq;votes-from-inning(n - 1;(s a1) @ [Vote[y2;y4;y5]]))) = v ∈ V))
22. (∃as:{a:Id| (a ∈ A)}  List
      (no_repeats({a:Id| (a ∈ A)} ;as)
      ∧ (||as|| = ((2 * t) + 1) ∈ ℤ)
      ∧ (∃vs:V List
          ((||vs|| = ||as|| ∈ ℤ)
          ∧ (v = (f vs) ∈ V)

          ∧ (∀i:ℕ||as||. ∃L:consensus-rcv(V;A) List. (L ≤ s as[i] ∧ archive-condition(V;A;t;f;n - 1;vs[i];L)))))))

⇒ (∃as:{a:Id| (a ∈ A)}  List
     (no_repeats({a:Id| (a ∈ A)} ;as)
     ∧ (||as|| = ((2 * t) + 1) ∈ ℤ)
     ∧ (∃vs:V List
         ((||vs|| = ||as|| ∈ ℤ)
         ∧ (v = (f vs) ∈ V)

         ∧ (∀i:ℕ||as||. ∃L:consensus-rcv(V;A) List. (L ≤ y as[i] ∧ archive-condition(V;A;t;f;n - 1;vs[i];L)))))))

⊢ ∃as:{a:Id| (a ∈ A)}  List
   (no_repeats({a:Id| (a ∈ A)} ;as)
   ∧ (||as|| = ((2 * t) + 1) ∈ ℤ)
   ∧ (∃vs:V List
       ((||vs|| = ||as|| ∈ ℤ)
       ∧ (v = (f vs) ∈ V)

       ∧ (∀i:ℕ||as||. ∃L:consensus-rcv(V;A) List. (L ≤ y as[i] ∧ archive-condition(V;A;t;f;n - 1;vs[i];L))))))

BY
{ D -2 }

1
1. V : Type@i'
2. A : Id List@i
3. t : ℕ⁺@i
4. f : (V List) ─→ V@i
5. s : {a:Id| (a ∈ A)}  ─→ (consensus-rcv(V;A) List)@i
6. ts-init(three-consensus-ts(V;A;t;f)) (ts-rel(three-consensus-ts(V;A;t;f))^*) s@i
7. y : {a:Id| (a ∈ A)}  ─→ (consensus-rcv(V;A) List)@i
8. ∀v:V. ∀a:{a:Id| (a ∈ A)} . ∀n:ℕ⁺. ∀L:consensus-rcv(V;A) List.
     (L ≤ s a
     ⇒ archive-condition(V;A;t;f;n;v;L)
     ⇒ (∃as:{a:Id| (a ∈ A)}  List
          (no_repeats({a:Id| (a ∈ A)} ;as)
          ∧ (||as|| = ((2 * t) + 1) ∈ ℤ)
          ∧ (∃vs:V List
              ((||vs|| = ||as|| ∈ ℤ)
              ∧ (v = (f vs) ∈ V)
              ∧ (∀i:ℕ||as||

                   ∃L:consensus-rcv(V;A) List. (L ≤ s as[i] ∧ archive-condition(V;A;t;f;n - 1;vs[i];L))))))))@i

 ((∃L:consensus-rcv(V;A) List. (L ≤ s b ∧ archive-condition(V;A;t;f;i;v;L))) ∧ (¬(Vote[y2;y4;y5] ∈ s a1))))@i

14. ∀b:{a:Id| (a ∈ A)} . ((¬(b = a1 ∈ Id)) ⇒ ((y b) = (s b) ∈ (consensus-rcv(V;A) List)))@i
15. (y a1) = ((s a1) @ [Vote[y2;y4;y5]]) ∈ (consensus-rcv(V;A) List)@i
16. v : V@i
17. n : ℕ⁺@i
18. 0 < n
19. ||values-for-distinct(IdDeq;votes-from-inning(n - 1;s a1))|| ≤ (2 * t)
20. ↑null(filter(λr.n - 1 <z inning(r);s a1))
21. (y4 = n ∈ ℤ) ∧ (v = y5 ∈ V)
22. (∃as:{a:Id| (a ∈ A)}  List
      (no_repeats({a:Id| (a ∈ A)} ;as)
      ∧ (||as|| = ((2 * t) + 1) ∈ ℤ)
      ∧ (∃vs:V List
          ((||vs|| = ||as|| ∈ ℤ)
          ∧ (v = (f vs) ∈ V)

          ∧ (∀i:ℕ||as||. ∃L:consensus-rcv(V;A) List. (L ≤ s as[i] ∧ archive-condition(V;A;t;f;n - 1;vs[i];L)))))))

         ∧ (∀i:ℕ||as||. ∃L:consensus-rcv(V;A) List. (L ≤ y as[i] ∧ archive-condition(V;A;t;f;n - 1;vs[i];L)))))))

       ∧ (∀i:ℕ||as||. ∃L:consensus-rcv(V;A) List. (L ≤ y as[i] ∧ archive-condition(V;A;t;f;n - 1;vs[i];L))))))

2
1. V : Type@i'
2. A : Id List@i
3. t : ℕ⁺@i
4. f : (V List) ─→ V@i
5. s : {a:Id| (a ∈ A)}  ─→ (consensus-rcv(V;A) List)@i
6. ts-init(three-consensus-ts(V;A;t;f)) (ts-rel(three-consensus-ts(V;A;t;f))^*) s@i
7. y : {a:Id| (a ∈ A)}  ─→ (consensus-rcv(V;A) List)@i
8. ∀v:V. ∀a:{a:Id| (a ∈ A)} . ∀n:ℕ⁺. ∀L:consensus-rcv(V;A) List.
     (L ≤ s a
     ⇒ archive-condition(V;A;t;f;n;v;L)
     ⇒ (∃as:{a:Id| (a ∈ A)}  List
          (no_repeats({a:Id| (a ∈ A)} ;as)
          ∧ (||as|| = ((2 * t) + 1) ∈ ℤ)
          ∧ (∃vs:V List
              ((||vs|| = ||as|| ∈ ℤ)
              ∧ (v = (f vs) ∈ V)
              ∧ (∀i:ℕ||as||

                   ∃L:consensus-rcv(V;A) List. (L ≤ s as[i] ∧ archive-condition(V;A;t;f;n - 1;vs[i];L))))))))@i

 ((∃L:consensus-rcv(V;A) List. (L ≤ s b ∧ archive-condition(V;A;t;f;i;v;L))) ∧ (¬(Vote[y2;y4;y5] ∈ s a1))))@i

14. ∀b:{a:Id| (a ∈ A)} . ((¬(b = a1 ∈ Id)) ⇒ ((y b) = (s b) ∈ (consensus-rcv(V;A) List)))@i
15. (y a1) = ((s a1) @ [Vote[y2;y4;y5]]) ∈ (consensus-rcv(V;A) List)@i
16. v : V@i
17. n : ℕ⁺@i
18. 0 < n
19. ||values-for-distinct(IdDeq;votes-from-inning(n - 1;s a1))|| ≤ (2 * t)
20. ↑null(filter(λr.n - 1 <z inning(r);s a1))
21. (((2 * t) + 1) ≤ ||values-for-distinct(IdDeq;votes-from-inning(n - 1;(s a1) @ [Vote[y2;y4;y5]]))||)
∧ ((f values-for-distinct(IdDeq;votes-from-inning(n - 1;(s a1) @ [Vote[y2;y4;y5]]))) = v ∈ V)
22. (∃as:{a:Id| (a ∈ A)}  List
      (no_repeats({a:Id| (a ∈ A)} ;as)
      ∧ (||as|| = ((2 * t) + 1) ∈ ℤ)
      ∧ (∃vs:V List
          ((||vs|| = ||as|| ∈ ℤ)
          ∧ (v = (f vs) ∈ V)

          ∧ (∀i:ℕ||as||. ∃L:consensus-rcv(V;A) List. (L ≤ s as[i] ∧ archive-condition(V;A;t;f;n - 1;vs[i];L)))))))

         ∧ (∀i:ℕ||as||. ∃L:consensus-rcv(V;A) List. (L ≤ y as[i] ∧ archive-condition(V;A;t;f;n - 1;vs[i];L)))))))

       ∧ (∀i:ℕ||as||. ∃L:consensus-rcv(V;A) List. (L ≤ y as[i] ∧ archive-condition(V;A;t;f;n - 1;vs[i];L))))))

Latex:

1. V : Type@i' 2. A : Id List@i 3. t : \mBbbN{}\msupplus{}@i 4. f : (V List) {}\mrightarrow{} V@i 5. s : \{a:Id| (a \mmember{} A)\} {}\mrightarrow{} (consensus-rcv(V;A) List)@i 6. ts-init(three-consensus-ts(V;A;t;f)) (ts-rel(three-consensus-ts(V;A;t;f))\^{}*) s@i 7. y : \{a:Id| (a \mmember{} A)\} {}\mrightarrow{} (consensus-rcv(V;A) List)@i 8. \mforall{}v:V. \mforall{}a:\{a:Id| (a \mmember{} A)\} . \mforall{}n:\mBbbN{}\msupplus{}. \mforall{}L:consensus-rcv(V;A) List. (L \mleq{} s a {}\mRightarrow{} archive-condition(V;A;t;f;n;v;L) {}\mRightarrow{} (\mexists{}as:\{a:Id| (a \mmember{} A)\} List (no\_repeats(\{a:Id| (a \mmember{} A)\} ;as) \mwedge{} (||as|| = ((2 * t) + 1)) \mwedge{} (\mexists{}vs:V List ((||vs|| = ||as||) \mwedge{} (v = (f vs)) \mwedge{} (\mforall{}i:\mBbbN{}||as|| \mexists{}L:consensus-rcv(V;A) List (L \mleq{} s as[i] \mwedge{} archive-condition(V;A;t;f;n - 1;vs[i];L))))))))@i 9. a1 : \{a:Id| (a \mmember{} A)\} @i 10. y2 : \{b:Id| (b \mmember{} A)\} @i 11. y4 : \mBbbN{}@i 12. y5 : V@i 13. \mforall{}b:\{a:Id| (a \mmember{} A)\} . \mforall{}i:\mBbbN{}. \mforall{}v:V. ((Vote[y2;y4;y5] = Vote[b;i;v]) {}\mRightarrow{} ((\mexists{}L:consensus-rcv(V;A) List. (L \mleq{} s b \mwedge{} archive-condition(V;A;t;f;i;v;L))) \mwedge{} (\mneg{}(Vote[y2;y4;y5] \mmember{} s a1))))@i 14. \mforall{}b:\{a:Id| (a \mmember{} A)\} . ((\mneg{}(b = a1)) {}\mRightarrow{} ((y b) = (s b)))@i 15. (y a1) = ((s a1) @ [Vote[y2;y4;y5]])@i 16. v : V@i 17. n : \mBbbN{}\msupplus{}@i 18. 0 < n 19. ||values-for-distinct(IdDeq;votes-from-inning(n - 1;s a1))|| \mleq{} (2 * t) 20. \muparrow{}null(filter(\mlambda{}r.n - 1 <z inning(r);s a1)) 21. ((y4 = n) \mwedge{} (v = y5)) \mvee{} ((((2 * t) + 1) \mleq{} ||values-for-distinct(IdDeq;votes-from-inning(n - 1;(s a1) @ [Vote[y2;y4;y5]]))||) \mwedge{} ((f values-for-distinct(IdDeq;votes-from-inning(n - 1;(s a1) @ [Vote[y2;y4;y5]]))) = v)) 22. (\mexists{}as:\{a:Id| (a \mmember{} A)\} List (no\_repeats(\{a:Id| (a \mmember{} A)\} ;as) \mwedge{} (||as|| = ((2 * t) + 1)) \mwedge{} (\mexists{}vs:V List ((||vs|| = ||as||) \mwedge{} (v = (f vs)) \mwedge{} (\mforall{}i:\mBbbN{}||as|| \mexists{}L:consensus-rcv(V;A) List (L \mleq{} s as[i] \mwedge{} archive-condition(V;A;t;f;n - 1;vs[i];L))))))) {}\mRightarrow{} (\mexists{}as:\{a:Id| (a \mmember{} A)\} List (no\_repeats(\{a:Id| (a \mmember{} A)\} ;as) \mwedge{} (||as|| = ((2 * t) + 1)) \mwedge{} (\mexists{}vs:V List ((||vs|| = ||as||) \mwedge{} (v = (f vs)) \mwedge{} (\mforall{}i:\mBbbN{}||as|| \mexists{}L:consensus-rcv(V;A) List (L \mleq{} y as[i] \mwedge{} archive-condition(V;A;t;f;n - 1;vs[i];L))))))) \mvdash{} \mexists{}as:\{a:Id| (a \mmember{} A)\} List (no\_repeats(\{a:Id| (a \mmember{} A)\} ;as) \mwedge{} (||as|| = ((2 * t) + 1)) \mwedge{} (\mexists{}vs:V List ((||vs|| = ||as||) \mwedge{} (v = (f vs)) \mwedge{} (\mforall{}i:\mBbbN{}||as|| \mexists{}L:consensus-rcv(V;A) List. (L \mleq{} y as[i] \mwedge{} archive-condition(V;A;t;f;n - 1;vs[i];L)))))) By D -2 Home Index