Proof of Nuprl Lemma : consensus-accum-num-property3

Step * 2 of Lemma consensus-accum-num-property3

1. [V] : Type
2. A : Id List@i
3. t : ℕ⁺@i
4. f : (V List) ─→ V@i
5. v0 : V@i
⊢ ∀ys:consensus-rcv(V;A) List. ∀y:consensus-rcv(V;A).
    (let b,i,as,vs,v = consensus-accum-num-state(t;f;v0;ys) in if b
    then archive-condition(V;A;t;f;i - 1;v;ys)
    else ∀v:V. (¬archive-condition(V;A;t;f;i;v;ys))
    fi
    ⇒ let b,i,as,vs,v = consensus-accum-num-state(t;f;v0;ys @ [y]) in if b
       then archive-condition(V;A;t;f;i - 1;v;ys @ [y])
       else ∀v:V. (¬archive-condition(V;A;t;f;i;v;ys @ [y]))
       fi )
BY
{ ((Assert IdDeq ∈ EqDecider({b:Id| (b ∈ A)} ) BY
          Auto)
   THEN (RepeatFor 2 ((D 0 THENA Auto)) THEN (Assert y ∈ consensus-rcv(V;A) BY Trivial))
   THEN (At ⌈Type⌉ (D 0)⋅ THENA Auto)
   THEN (InstLemma `consensus-accum-num-property1` [⌈V⌉;⌈A⌉;⌈t⌉;⌈f⌉;⌈v0⌉]⋅ THENA Auto)
   THEN ((InstHyp [⌈ys @ [y]⌉] (-1)⋅ THENA Auto) THEN MoveToConcl (-1))
   THEN (InstHyp [⌈ys⌉] (-1)⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN Thin (-1)
   THEN MoveToConcl (-1)
   THEN Unfold `consensus-accum-num-state` 0
   THEN (RWO "list_accum_append" 0 THENA Auto)
   THEN Fold `consensus-accum-num-state` 0
   THEN GenConclAtAddr [1;1]
   THEN RepeatFor 4 (D -2)
   THEN Reduce 0
   THEN (D 0 THENA Auto)
   THEN (D -9 THEN Try (RepeatFor 2 (D -9)))
   THEN RepUR ``consensus-accum-num let`` 0
   THEN All (Folds ``cs-initial-rcv cs-rcv-vote``)⋅
   THEN Repeat (((SplitOnConclITE THENA Auto) THEN Reduce 0))
   THEN (UnivCD THENA Auto)
   THEN ExRepD
   THEN ((Try ((D 0 THENA Auto))
          THEN Try (((RWO "archive-condition-append-init" (-1) THENA Auto) THEN D -1 THEN Auto))
          THEN Try ((RWO "archive-condition-append-init" 0 THENA Auto)))

         THEN Try (((RWO "archive-condition-append-vote" (-1) THENA Auto) THEN RepeatFor 2 ((SplitOrHyps THEN ExRepD))))

         )
   THEN Try ((RWO "archive-condition-append-vote" (0) THENA Auto))
   THEN Auto) }

1
1. [V] : Type
2. A : Id List@i
3. t : ℕ⁺@i
4. f : (V List) ─→ V@i
5. v0 : V@i
6. IdDeq ∈ EqDecider({b:Id| (b ∈ A)} )
7. ys : consensus-rcv(V;A) List@i
8. x : V@i
9. Init[x] ∈ consensus-rcv(V;A)
10. v1 : 𝔹@i
11. v3 : ℤ@i
12. v5 : {a:Id| (a ∈ A)}  List@i
13. v7 : V List@i
14. v8 : V@i

15. consensus-accum-num-state(t;f;v0;ys) = <v1, v3, v5, v7, v8> ∈ (𝔹 × ℤ × {a:Id| (a ∈ A)}  List × V List × V)@i

16. if v1 then archive-condition(V;A;t;f;v3 - 1;v8;ys) else ∀v:V. (¬archive-condition(V;A;t;f;v3;v;ys)) fi @i

17. v3 = 0 ∈ ℤ
18. filter(λr.v3 - 1 <z inning(r);ys) = [] ∈ (consensus-rcv(V;A) List)@i
19. ||v5|| = ||v7|| ∈ ℤ@i
20. zip(v5;v7) = votes-from-inning(v3 - 1;ys) ∈ (({b:Id| (b ∈ A)}  × V) List)@i
21. 0 ≤ v3@i
22. 1 ≤ v3 supposing ¬↑null(ys)@i
23. ||values-for-distinct(IdDeq;votes-from-inning(v3 - 1;ys))|| ≤ (2 * t)@i
24. filter(λr.0 <z inning(r);ys @ [Init[x]]) = [] ∈ (consensus-rcv(V;A) List)@i
25. 0 = 0 ∈ ℤ@i
26. [] = votes-from-inning(0;ys @ [Init[x]]) ∈ (({b:Id| (b ∈ A)}  × V) List)@i
27. 0 ≤ 1@i
28. 1 ≤ 1 supposing ¬↑null(ys @ [Init[x]])@i
29. ||values-for-distinct(IdDeq;votes-from-inning(0;ys @ [Init[x]]))|| ≤ (2 * t)@i
⊢ {(ys = [] ∈ (consensus-rcv(V;A) List)) ∧ (0 = 0 ∈ ℤ) ∧ (x = x ∈ V)}

2
1. [V] : Type
2. A : Id List@i
3. t : ℕ⁺@i
4. f : (V List) ─→ V@i
5. v0 : V@i
6. IdDeq ∈ EqDecider({b:Id| (b ∈ A)} )
7. ys : consensus-rcv(V;A) List@i
8. y2 : {b:Id| (b ∈ A)} @i
9. y4 : ℕ@i
10. y5 : V@i
11. Vote[y2;y4;y5] ∈ consensus-rcv(V;A)
12. v1 : 𝔹@i
13. v3 : ℤ@i
14. v5 : {a:Id| (a ∈ A)}  List@i
15. v7 : V List@i
16. v8 : V@i

17. consensus-accum-num-state(t;f;v0;ys) = <v1, v3, v5, v7, v8> ∈ (𝔹 × ℤ × {a:Id| (a ∈ A)}  List × V List × V)@i

18. if v1 then archive-condition(V;A;t;f;v3 - 1;v8;ys) else ∀v:V. (¬archive-condition(V;A;t;f;v3;v;ys)) fi @i

19. (v3 - 1) ≤ y4
20. v3 - 1 < y4
21. filter(λr.v3 - 1 <z inning(r);ys) = [] ∈ (consensus-rcv(V;A) List)@i
22. ||v5|| = ||v7|| ∈ ℤ@i
23. zip(v5;v7) = votes-from-inning(v3 - 1;ys) ∈ (({b:Id| (b ∈ A)} × V) List)@i
24. 0 ≤ v3@i
25. 1 ≤ v3 supposing ¬↑null(ys)@i
26. ||values-for-distinct(IdDeq;votes-from-inning(v3 - 1;ys))|| ≤ (2 * t)@i
27. filter(λr.(y4 + 1) - 1 <z inning(r);ys @ [Vote[y2;y4;y5]]) = [] ∈ (consensus-rcv(V;A) List)@i
28. 1 = 1 ∈ ℤ@i

29. [<y2, y5>] = votes-from-inning((y4 + 1) - 1;ys @ [Vote[y2;y4;y5]]) ∈ (({b:Id| (b ∈ A)}  × V) List)@i

30. 0 ≤ (y4 + 1)@i
31. 1 ≤ (y4 + 1) supposing ¬↑null(ys @ [Vote[y2;y4;y5]])@i
32. ||values-for-distinct(IdDeq;votes-from-inning((y4 + 1) - 1;ys @ [Vote[y2;y4;y5]]))|| ≤ (2 * t)@i

⊢ ((ys = [] ∈ (consensus-rcv(V;A) List)) ∧ (y4 = ((y4 + 1) - 1) ∈ ℤ) ∧ (y5 = y5 ∈ V))

∨ ((0 < (y4 + 1) - 1 ∧ (||values-for-distinct(IdDeq;votes-from-inning((y4 + 1) - 1 - 1;ys))|| ≤ (2 * t)))

∧ (↑null(filter(λr.(y4 + 1) - 1 - 1 <z inning(r);ys)))
∧ (((y4 = ((y4 + 1) - 1) ∈ ℤ) ∧ (y5 = y5 ∈ V))

    ∨ ((((2 * t) + 1) ≤ ||values-for-distinct(IdDeq;votes-from-inning((y4 + 1) - 1 - 1;ys @ [Vote[y2;y4;y5]]))||)

      ∧ ((f values-for-distinct(IdDeq;votes-from-inning((y4 + 1) - 1 - 1;ys @ [Vote[y2;y4;y5]]))) = y5 ∈ V))))

3
1. [V] : Type
2. A : Id List@i
3. t : ℕ⁺@i
4. f : (V List) ─→ V@i
5. v0 : V@i
6. IdDeq ∈ EqDecider({b:Id| (b ∈ A)} )
7. ys : consensus-rcv(V;A) List@i
8. y2 : {b:Id| (b ∈ A)} @i
9. y4 : ℕ@i
10. y5 : V@i
11. Vote[y2;y4;y5] ∈ consensus-rcv(V;A)
12. v1 : 𝔹@i
13. v3 : ℤ@i
14. v5 : {a:Id| (a ∈ A)} List@i
15. v7 : V List@i
16. v8 : V@i

17. consensus-accum-num-state(t;f;v0;ys) = <v1, v3, v5, v7, v8> ∈ (𝔹 × ℤ × {a:Id| (a ∈ A)}  List × V List × V)@i

18. if v1 then archive-condition(V;A;t;f;v3 - 1;v8;ys) else ∀v:V. (¬archive-condition(V;A;t;f;v3;v;ys)) fi @i

19. (v3 - 1) ≤ y4
20. y4 ≤ (v3 - 1)
21. ||remove-repeats(IdDeq;v5 @ [y2])|| = ((2 * t) + 1) ∈ ℤ
22. filter(λr.v3 - 1 <z inning(r);ys) = [] ∈ (consensus-rcv(V;A) List)@i
23. ||v5|| = ||v7|| ∈ ℤ@i
24. zip(v5;v7) = votes-from-inning(v3 - 1;ys) ∈ (({b:Id| (b ∈ A)} × V) List)@i
25. 0 ≤ v3@i
26. 1 ≤ v3 supposing ¬↑null(ys)@i
27. ||values-for-distinct(IdDeq;votes-from-inning(v3 - 1;ys))|| ≤ (2 * t)@i
28. filter(λr.(v3 + 1) - 1 <z inning(r);ys @ [Vote[y2;y4;y5]]) = [] ∈ (consensus-rcv(V;A) List)@i
29. 0 = 0 ∈ ℤ@i
30. [] = votes-from-inning((v3 + 1) - 1;ys @ [Vote[y2;y4;y5]]) ∈ (({b:Id| (b ∈ A)} × V) List)@i
31. 0 ≤ (v3 + 1)@i
32. 1 ≤ (v3 + 1) supposing ¬↑null(ys @ [Vote[y2;y4;y5]])@i
33. ||values-for-distinct(IdDeq;votes-from-inning((v3 + 1) - 1;ys @ [Vote[y2;y4;y5]]))|| ≤ (2 * t)@i
⊢ ((ys = [] ∈ (consensus-rcv(V;A) List))
∧ (y4 = ((v3 + 1) - 1) ∈ ℤ)
∧ ((f values-for-distinct(IdDeq;zip(v5 @ [y2];v7 @ [y5]))) = y5 ∈ V))

∨ ((0 < (v3 + 1) - 1 ∧ (||values-for-distinct(IdDeq;votes-from-inning((v3 + 1) - 1 - 1;ys))|| ≤ (2 * t)))

∧ (↑null(filter(λr.(v3 + 1) - 1 - 1 <z inning(r);ys)))

  ∧ (((y4 = ((v3 + 1) - 1) ∈ ℤ) ∧ ((f values-for-distinct(IdDeq;zip(v5 @ [y2];v7 @ [y5]))) = y5 ∈ V))

    ∨ ((((2 * t) + 1) ≤ ||values-for-distinct(IdDeq;votes-from-inning((v3 + 1) - 1 - 1;ys @ [Vote[y2;y4;y5]]))||)

      ∧ ((f values-for-distinct(IdDeq;votes-from-inning((v3 + 1) - 1 - 1;ys @ [Vote[y2;y4;y5]])))
        = (f values-for-distinct(IdDeq;zip(v5 @ [y2];v7 @ [y5])))
        ∈ V))))

Latex:

1. [V] : Type 2. A : Id List@i 3. t : \mBbbN{}\msupplus{}@i 4. f : (V List) {}\mrightarrow{} V@i 5. v0 : V@i \mvdash{} \mforall{}ys:consensus-rcv(V;A) List. \mforall{}y:consensus-rcv(V;A). (let b,i,as,vs,v = consensus-accum-num-state(t;f;v0;ys) in if b then archive-condition(V;A;t;f;i - 1;v;ys) else \mforall{}v:V. (\mneg{}archive-condition(V;A;t;f;i;v;ys)) fi {}\mRightarrow{} let b,i,as,vs,v = consensus-accum-num-state(t;f;v0;ys @ [y]) in if b then archive-condition(V;A;t;f;i - 1;v;ys @ [y]) else \mforall{}v:V. (\mneg{}archive-condition(V;A;t;f;i;v;ys @ [y])) fi ) By ((Assert IdDeq \mmember{} EqDecider(\{b:Id| (b \mmember{} A)\} ) BY Auto) THEN (RepeatFor 2 ((D 0 THENA Auto)) THEN (Assert y \mmember{} consensus-rcv(V;A) BY Trivial)) THEN (At \mkleeneopen{}Type\mkleeneclose{} (D 0)\mcdot{} THENA Auto) THEN (InstLemma `consensus-accum-num-property1` [\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}v0\mkleeneclose{}]\mcdot{} THENA Auto) THEN ((InstHyp [\mkleeneopen{}ys @ [y]\mkleeneclose{}] (-1)\mcdot{} THENA Auto) THEN MoveToConcl (-1)) THEN (InstHyp [\mkleeneopen{}ys\mkleeneclose{}] (-1)\mcdot{} THENA Auto) THEN MoveToConcl (-1) THEN Thin (-1) THEN MoveToConcl (-1) THEN Unfold `consensus-accum-num-state` 0 THEN (RWO "list\_accum\_append" 0 THENA Auto) THEN Fold `consensus-accum-num-state` 0 THEN GenConclAtAddr [1;1] THEN RepeatFor 4 (D -2) THEN Reduce 0 THEN (D 0 THENA Auto) THEN (D -9 THEN Try (RepeatFor 2 (D -9))) THEN RepUR ``consensus-accum-num let`` 0 THEN All (Folds ``cs-initial-rcv cs-rcv-vote``)\mcdot{} THEN Repeat (((SplitOnConclITE THENA Auto) THEN Reduce 0)) THEN (UnivCD THENA Auto) THEN ExRepD THEN ((Try ((D 0 THENA Auto)) THEN Try (((RWO "archive-condition-append-init" (-1) THENA Auto) THEN D -1 THEN Auto)) THEN Try ((RWO "archive-condition-append-init" 0 THENA Auto))) THEN Try (((RWO "archive-condition-append-vote" (-1) THENA Auto) THEN RepeatFor 2 ((SplitOrHyps THEN ExRepD)) )) ) THEN Try ((RWO "archive-condition-append-vote" (0) THENA Auto)) THEN Auto) Home Index