Proof of Nuprl Lemma : consensus-ts5-archive-invariant

Step * 3 1 of Lemma consensus-ts5-archive-invariant

1. [V] : Type
2. ∀v1,v2:V. Dec(v1 = v2 ∈ V)@i
3. ∃v,v':V. (¬(v = v' ∈ V))@i
4. A : Id List@i
5. W : {a:Id| (a ∈ A)} List List@i
6. x1 : ConsensusState@i
7. x2 : Knowledge(ConsensusState)@i
8. \\%3 : ts-init(consensus-ts5(V;A;W)) (ts-rel(consensus-ts5(V;A;W))^*) <x1, x2>@i
9. y1 : ConsensusState@i
10. y2 : Knowledge(ConsensusState)@i
11. \\%5 : ts-init(consensus-ts5(V;A;W)) (ts-rel(consensus-ts5(V;A;W))^*) <y1, y2>@i
12. ∀v:V. ∀b:{a:Id| (a ∈ A)} . ∀i:ℤ.

      (state x1 may consider v in inning i) supposing ((Estimate(x1;b)(i) = v ∈ V) and (↑i ∈ dom(Estimate(x1;b))))@i

13. <x1, x2> ts-rel(consensus-ts5(V;A;W)) <y1, y2>@i
14. v : V@i
15. b : {a:Id| (a ∈ A)} @i
16. i : ℤ@i
17. ↑i ∈ dom(Estimate(y1;b))
18. Estimate(y1;b)(i) = v ∈ V
⊢ state y1 may consider v in inning i
BY

{ (RepUR ``ts-rel consensus-ts5`` -6 THEN D -6 THEN Reduce (-6) THEN D -6 THEN SplitOrHyps THEN D -6 THEN ExRepD) }

1
1. [V] : Type
2. ∀v1,v2:V. Dec(v1 = v2 ∈ V)@i
3. v1 : V@i
4. v' : V@i
5. ¬(v1 = v' ∈ V)@i
6. A : Id List@i
7. W : {a:Id| (a ∈ A)} List List@i
8. x1 : ConsensusState@i
9. x2 : Knowledge(ConsensusState)@i
10. \\%3 : ts-init(consensus-ts5(V;A;W)) (ts-rel(consensus-ts5(V;A;W))^*) <x1, x2>@i
11. y1 : ConsensusState@i
12. y2 : Knowledge(ConsensusState)@i
13. \\%5 : ts-init(consensus-ts5(V;A;W)) (ts-rel(consensus-ts5(V;A;W))^*) <y1, y2>@i
14. ∀v:V. ∀b:{a:Id| (a ∈ A)} . ∀i:ℤ.

      (state x1 may consider v in inning i) supposing ((Estimate(x1;b)(i) = v ∈ V) and (↑i ∈ dom(Estimate(x1;b))))@i

15. a : {a:Id| (a ∈ A)} @i
16. ∀b:{a:Id| (a ∈ A)}
      ((¬(b = a ∈ Id))
      ⇒ ((Inning(y1;b) = Inning(x1;b) ∈ ℤ)
         ∧ (Estimate(y1;b) = Estimate(x1;b) ∈ i:ℤ fp-> V)
         ∧ (Knowledge(y2;b) = Knowledge(x2;b) ∈ b:Id fp-> ℤ × (ℤ × V + Top))))@i
17. Inning(y1;a) = (Inning(x1;a) + 1) ∈ ℤ@i
18. Estimate(y1;a) = Estimate(x1;a) ∈ i:ℤ fp-> V@i
19. Knowledge(y2;a) = Knowledge(x2;a) ∈ b:Id fp-> ℤ × (ℤ × V + Top)@i
20. v : V@i
21. b : {a:Id| (a ∈ A)} @i
22. i : ℤ@i
23. ↑i ∈ dom(Estimate(y1;b))
24. Estimate(y1;b)(i) = v ∈ V
⊢ state y1 may consider v in inning i

2
1. [V] : Type
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. v2 : V@i
4. v' : V@i
5. ¬(v2 = v' ∈ V)@i
6. A : Id List@i
7. W : {a:Id| (a ∈ A)}  List List@i
8. x1 : ConsensusState@i
9. x2 : Knowledge(ConsensusState)@i
10. \\%3 : ts-init(consensus-ts5(V;A;W)) (ts-rel(consensus-ts5(V;A;W))^*) <x1, x2>@i
11. y1 : ConsensusState@i
12. y2 : Knowledge(ConsensusState)@i
13. \\%5 : ts-init(consensus-ts5(V;A;W)) (ts-rel(consensus-ts5(V;A;W))^*) <y1, y2>@i
14. ∀v:V. ∀b:{a:Id| (a ∈ A)} . ∀i:ℤ.

      (state x1 may consider v in inning i) supposing ((Estimate(x1;b)(i) = v ∈ V) and (↑i ∈ dom(Estimate(x1;b))))@i

15. a : {a:Id| (a ∈ A)} @i
16. ∀b:{a:Id| (a ∈ A)}
      ((¬(b = a ∈ Id))
      ⇒ ((Inning(y1;b) = Inning(x1;b) ∈ ℤ)
         ∧ (Estimate(y1;b) = Estimate(x1;b) ∈ i:ℤ fp-> V)
         ∧ (Knowledge(y2;b) = Knowledge(x2;b) ∈ b:Id fp-> ℤ × (ℤ × V + Top))))@i
17. Inning(y1;a) = Inning(x1;a) ∈ ℤ@i
18. Knowledge(y2;a) = Knowledge(x2;a) ∈ b:Id fp-> ℤ × (ℤ × V + Top)@i
19. ¬(Inning(x1;a) ∈ fpf-domain(Estimate(x1;a)))@i
20. v1 : V@i
21. may consider v1 in inning Inning(x1;a) based on knowledge (Knowledge(x2;a))@i
22. Estimate(y1;a) = Estimate(x1;a) ⊕ Inning(x1;a) : v1 ∈ i:ℤ fp-> V@i
23. v : V@i
24. b : {a:Id| (a ∈ A)} @i
25. i : ℤ@i
26. ↑i ∈ dom(Estimate(y1;b))
27. Estimate(y1;b)(i) = v ∈ V
⊢ state y1 may consider v in inning i

3
1. [V] : Type
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. v1 : V@i
4. v' : V@i
5. ¬(v1 = v' ∈ V)@i
6. A : Id List@i
7. W : {a:Id| (a ∈ A)}  List List@i
8. x1 : ConsensusState@i
9. x2 : Knowledge(ConsensusState)@i
10. \\%3 : ts-init(consensus-ts5(V;A;W)) (ts-rel(consensus-ts5(V;A;W))^*) <x1, x2>@i
11. y1 : ConsensusState@i
12. y2 : Knowledge(ConsensusState)@i
13. \\%5 : ts-init(consensus-ts5(V;A;W)) (ts-rel(consensus-ts5(V;A;W))^*) <y1, y2>@i
14. ∀v:V. ∀b:{a:Id| (a ∈ A)} . ∀i:ℤ.

      (state x1 may consider v in inning i) supposing ((Estimate(x1;b)(i) = v ∈ V) and (↑i ∈ dom(Estimate(x1;b))))@i

∧ (Knowledge(y2;a) = b1 : <i1, inr ⋅ > ⊕ Knowledge(x2;a) ∈ b:Id fp-> ℤ × (ℤ × V + Top)))

∨ (∃j:ℤ
    (j < i1
    ∧ (↑j ∈ dom(Estimate(x1;b1)))
    ∧ (∀k:ℤ. (j < k ⇒ k < i1 ⇒ (¬↑k ∈ dom(Estimate(x1;b1)))))

    ∧ (Knowledge(y2;a) = b1 : <i1, inl <j, Estimate(x1;b1)(j)>> ⊕ Knowledge(x2;a) ∈ b:Id fp-> ℤ × (ℤ × V + Top))))@i

23. v : V@i
24. b : {a:Id| (a ∈ A)} @i
25. i : ℤ@i
26. ↑i ∈ dom(Estimate(y1;b))
27. Estimate(y1;b)(i) = v ∈ V
⊢ state y1 may consider v in inning i

Latex:

1. [V] : Type 2. \mforall{}v1,v2:V. Dec(v1 = v2)@i 3. \mexists{}v,v':V. (\mneg{}(v = v'))@i 4. A : Id List@i 5. W : \{a:Id| (a \mmember{} A)\} List List@i 6. x1 : ConsensusState@i 7. x2 : Knowledge(ConsensusState)@i 8. \mbackslash{}\mbackslash{}\%3 : ts-init(consensus-ts5(V;A;W)) (ts-rel(consensus-ts5(V;A;W))\^{}*) <x1, x2>@i 9. y1 : ConsensusState@i 10. y2 : Knowledge(ConsensusState)@i 11. \mbackslash{}\mbackslash{}\%5 : ts-init(consensus-ts5(V;A;W)) (ts-rel(consensus-ts5(V;A;W))\^{}*) <y1, y2>@i 12. \mforall{}v:V. \mforall{}b:\{a:Id| (a \mmember{} A)\} . \mforall{}i:\mBbbZ{}. (state x1 may consider v in inning i) supposing ((Estimate(x1;b)(i) = v) and (\muparrow{}i \mmember{} dom(Estimate(x1;b))))@i 13. <x1, x2> ts-rel(consensus-ts5(V;A;W)) <y1, y2>@i 14. v : V@i 15. b : \{a:Id| (a \mmember{} A)\} @i 16. i : \mBbbZ{}@i 17. \muparrow{}i \mmember{} dom(Estimate(y1;b)) 18. Estimate(y1;b)(i) = v \mvdash{} state y1 may consider v in inning i By (RepUR ``ts-rel consensus-ts5`` -6 THEN D -6 THEN Reduce (-6) THEN D -6 THEN SplitOrHyps THEN D -6 THEN ExRepD) Home Index