Proof of Nuprl Lemma : OARcast

Step * 1 2 1 1 1 1 1 1 of Lemma OARcast_lemma1

1. Info : Type
2. es : EO+(Info)@i'
3. M : Type@i'
4. V : EClass(Id × Atom1 × Id × ℕ × M)@i'
5. S : EClass(Id × Atom1 × Id × ℕ × M)@i'
6. correct : Id ─→ ℙ@i'
7. f : ℕ@i
8. orderers : bag(Id)@i
9. OARDeliver : EClass(Id × ℕ × M)@i'
10. ∀n:ℕ. ∀sndr:Id. ∀msg:M. ∀e:E.
      (<sndr, n, msg> ∈ OARDeliver(e)
      ⇒ (correct loc(e))
      ⇒ {(0 < n ⇒ (∃msg':M. ∃e':E. ((e' <loc e) ∧ <sndr, n - 1, msg'> ∈ OARDeliver(e))))
         ∧ (∃L:Id List
             ((||L|| = ((2 * f) + 1) ∈ ℤ)
             ∧ no_repeats(Id;L)

             ∧ (∀o∈L.o ↓∈ orderers ∧ (∃e':E(V). (e' ≤loc e  ∧ (∃sig:Atom1. <o, sig, sndr, n, msg> ∈ V(e')))))))})@i

11. oar-order(es;M;S;correct;orderers)@i
12. oar-crypto(es;M;V;S;correct)@i
13. #(orderers) = ((3 * f) + 1) ∈ ℤ@i
14. bag-no-repeats(Id;orderers)@i
15. ¬(∃b:bag(Id). (f < #(b) ∧ bag-no-repeats(Id;b) ∧ (∀x:Id. (x ↓∈ b ⇒ (x ↓∈ orderers ∧ (¬(correct x)))))))@i
16. ∀m1,m2:M. Dec(m1 = m2 ∈ M)@i
17. e1 : E@i
18. e2 : E@i
19. n : ℕ@i
20. sndr : Id@i
21. m1 : M@i
22. m2 : M@i
23. <sndr, n, m1> ∈ OARDeliver(e1)@i
24. <sndr, n, m2> ∈ OARDeliver(e2)@i
25. correct loc(e1)@i
26. correct loc(e2)@i
27. 0 < n ⇒ (∃msg':M. ∃e':E. ((e' <loc e1) ∧ <sndr, n - 1, msg'> ∈ OARDeliver(e1)))
28. L1 : Id List
29. ||L1|| = ((2 * f) + 1) ∈ ℤ
30. no_repeats(Id;L1)

31. (∀o∈L1.o ↓∈ orderers ∧ (∃e':E(V). (e' ≤loc e1  ∧ (∃sig:Atom1. <o, sig, sndr, n, m1> ∈ V(e')))))

32. 0 < n ⇒ (∃msg':M. ∃e':E. ((e' <loc e2) ∧ <sndr, n - 1, msg'> ∈ OARDeliver(e2)))
33. L : Id List
34. ||L|| = ((2 * f) + 1) ∈ ℤ
35. no_repeats(Id;L)

36. (∀o∈L.o ↓∈ orderers ∧ (∃e':E(V). (e' ≤loc e2  ∧ (∃sig:Atom1. <o, sig, sndr, n, m2> ∈ V(e')))))

37. ¬(∀o:Id. ((o ∈ L1) ⇒ (o ∈ L) ⇒ (¬(correct o))))
38. o : Id@i
39. (o ∈ L1)@i
40. (o ∈ L)@i
41. correct o@i
42. o ↓∈ orderers
43. e3 : E(V)
44. e3 ≤loc e2
45. s1 : Atom1
46. <o, s1, sndr, n, m2> ∈ V(e3)
47. o ↓∈ orderers
48. e' : E(V)
49. e' ≤loc e1
50. sig : Atom1
51. <o, sig, sndr, n, m1> ∈ V(e')
52. a : E
53. loc(a) = o ∈ Id
54. <o, sig, sndr, n, m1> ∈ S(a)
55. b : E
56. loc(b) = o ∈ Id
57. <o, s1, sndr, n, m2> ∈ S(b)
⊢ m1 = m2 ∈ M
BY
{ ((Assert ¬(a <loc b) BY
          ((D 0 THENA Auto)
           THEN Unfold `oar-order` 11
           THEN (InstHyp [⌈n⌉;⌈sndr⌉;⌈m2⌉;⌈s1⌉;⌈o⌉;⌈b⌉] 11⋅ THENA Auto)
           THEN RepeatFor 2 (D -1)
           THEN InstHyp [⌈m1⌉;⌈sig⌉;⌈a⌉] (-2)⋅
           THEN Auto))
   THEN (Assert ¬(b <loc a) BY
               ((D 0 THENA Auto)
                THEN Unfold `oar-order` 11

                THEN (InstHyp [⌈n⌉;⌈sndr⌉;⌈m1⌉;⌈sig⌉;⌈o⌉;⌈a⌉] 11⋅ THENA Auto)

                THEN RepeatFor 2 (D -1)
                THEN InstHyp [⌈m2⌉;⌈s1⌉;⌈b⌉] (-2)⋅
                THEN Auto))
   THEN (Assert a = b ∈ E BY
               ((Assert loc(a) = loc(b) ∈ Id BY
                       Auto)
                THEN (RWO "es-locl-trichotomy" (-1) THENA Auto)
                THEN RepeatFor 2 ((D -1 THEN Auto))))) }

1
1. Info : Type
2. es : EO+(Info)@i'
3. M : Type@i'
4. V : EClass(Id × Atom1 × Id × ℕ × M)@i'
5. S : EClass(Id × Atom1 × Id × ℕ × M)@i'
6. correct : Id ─→ ℙ@i'
7. f : ℕ@i
8. orderers : bag(Id)@i
9. OARDeliver : EClass(Id × ℕ × M)@i'
10. ∀n:ℕ. ∀sndr:Id. ∀msg:M. ∀e:E.
      (<sndr, n, msg> ∈ OARDeliver(e)
      ⇒ (correct loc(e))
      ⇒ {(0 < n ⇒ (∃msg':M. ∃e':E. ((e' <loc e) ∧ <sndr, n - 1, msg'> ∈ OARDeliver(e))))
         ∧ (∃L:Id List
             ((||L|| = ((2 * f) + 1) ∈ ℤ)
             ∧ no_repeats(Id;L)

             ∧ (∀o∈L.o ↓∈ orderers ∧ (∃e':E(V). (e' ≤loc e  ∧ (∃sig:Atom1. <o, sig, sndr, n, msg> ∈ V(e')))))))})@i

31. (∀o∈L1.o ↓∈ orderers ∧ (∃e':E(V). (e' ≤loc e1  ∧ (∃sig:Atom1. <o, sig, sndr, n, m1> ∈ V(e')))))

32. 0 < n ⇒ (∃msg':M. ∃e':E. ((e' <loc e2) ∧ <sndr, n - 1, msg'> ∈ OARDeliver(e2)))
33. L : Id List
34. ||L|| = ((2 * f) + 1) ∈ ℤ
35. no_repeats(Id;L)

36. (∀o∈L.o ↓∈ orderers ∧ (∃e':E(V). (e' ≤loc e2  ∧ (∃sig:Atom1. <o, sig, sndr, n, m2> ∈ V(e')))))

Latex:

Latex:
1. Info : Type 2. es : EO+(Info)@i' 3. M : Type@i' 4. V : EClass(Id \mtimes{} Atom1 \mtimes{} Id \mtimes{} \mBbbN{} \mtimes{} M)@i' 5. S : EClass(Id \mtimes{} Atom1 \mtimes{} Id \mtimes{} \mBbbN{} \mtimes{} M)@i' 6. correct : Id {}\mrightarrow{} \mBbbP{}@i' 7. f : \mBbbN{}@i 8. orderers : bag(Id)@i 9. OARDeliver : EClass(Id \mtimes{} \mBbbN{} \mtimes{} M)@i' 10. \mforall{}n:\mBbbN{}. \mforall{}sndr:Id. \mforall{}msg:M. \mforall{}e:E. (<sndr, n, msg> \mmember{} OARDeliver(e) {}\mRightarrow{} (correct loc(e)) {}\mRightarrow{} \{(0 < n {}\mRightarrow{} (\mexists{}msg':M. \mexists{}e':E. ((e' <loc e) \mwedge{} <sndr, n - 1, msg'> \mmember{} OARDeliver(e)))) \mwedge{} (\mexists{}L:Id List ((||L|| = ((2 * f) + 1)) \mwedge{} no\_repeats(Id;L) \mwedge{} (\mforall{}o\mmember{}L.o \mdownarrow{}\mmember{} orderers \mwedge{} (\mexists{}e':E(V). (e' \mleq{}loc e \mwedge{} (\mexists{}sig:Atom1. <o, sig, sndr, n, msg> \mmember{} V(e')))))))\})@i 11. oar-order(es;M;S;correct;orderers)@i 12. oar-crypto(es;M;V;S;correct)@i 13. \#(orderers) = ((3 * f) + 1)@i 14. bag-no-repeats(Id;orderers)@i 15. \mneg{}(\mexists{}b:bag(Id) (f < \#(b) \mwedge{} bag-no-repeats(Id;b) \mwedge{} (\mforall{}x:Id. (x \mdownarrow{}\mmember{} b {}\mRightarrow{} (x \mdownarrow{}\mmember{} orderers \mwedge{} (\mneg{}(correct x)))))))@i 16. \mforall{}m1,m2:M. Dec(m1 = m2)@i 17. e1 : E@i 18. e2 : E@i 19. n : \mBbbN{}@i 20. sndr : Id@i 21. m1 : M@i 22. m2 : M@i 23. <sndr, n, m1> \mmember{} OARDeliver(e1)@i 24. <sndr, n, m2> \mmember{} OARDeliver(e2)@i 25. correct loc(e1)@i 26. correct loc(e2)@i 27. 0 < n {}\mRightarrow{} (\mexists{}msg':M. \mexists{}e':E. ((e' <loc e1) \mwedge{} <sndr, n - 1, msg'> \mmember{} OARDeliver(e1))) 28. L1 : Id List 29. ||L1|| = ((2 * f) + 1) 30. no\_repeats(Id;L1) 31. (\mforall{}o\mmember{}L1.o \mdownarrow{}\mmember{} orderers \mwedge{} (\mexists{}e':E(V). (e' \mleq{}loc e1 \mwedge{} (\mexists{}sig:Atom1. <o, sig, sndr, n, m1> \mmember{} V(e'))))) 32. 0 < n {}\mRightarrow{} (\mexists{}msg':M. \mexists{}e':E. ((e' <loc e2) \mwedge{} <sndr, n - 1, msg'> \mmember{} OARDeliver(e2))) 33. L : Id List 34. ||L|| = ((2 * f) + 1) 35. no\_repeats(Id;L) 36. (\mforall{}o\mmember{}L.o \mdownarrow{}\mmember{} orderers \mwedge{} (\mexists{}e':E(V). (e' \mleq{}loc e2 \mwedge{} (\mexists{}sig:Atom1. <o, sig, sndr, n, m2> \mmember{} V(e'))))) 37. \mneg{}(\mforall{}o:Id. ((o \mmember{} L1) {}\mRightarrow{} (o \mmember{} L) {}\mRightarrow{} (\mneg{}(correct o)))) 38. o : Id@i 39. (o \mmember{} L1)@i 40. (o \mmember{} L)@i 41. correct o@i 42. o \mdownarrow{}\mmember{} orderers 43. e3 : E(V) 44. e3 \mleq{}loc e2 45. s1 : Atom1 46. <o, s1, sndr, n, m2> \mmember{} V(e3) 47. o \mdownarrow{}\mmember{} orderers 48. e' : E(V) 49. e' \mleq{}loc e1 50. sig : Atom1 51. <o, sig, sndr, n, m1> \mmember{} V(e') 52. a : E 53. loc(a) = o 54. <o, sig, sndr, n, m1> \mmember{} S(a) 55. b : E 56. loc(b) = o 57. <o, s1, sndr, n, m2> \mmember{} S(b) \mvdash{} m1 = m2 By Latex: ((Assert \mneg{}(a <loc b) BY ((D 0 THENA Auto) THEN Unfold `oar-order` 11 THEN (InstHyp [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}sndr\mkleeneclose{};\mkleeneopen{}m2\mkleeneclose{};\mkleeneopen{}s1\mkleeneclose{};\mkleeneopen{}o\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}] 11\mcdot{} THENA Auto) THEN RepeatFor 2 (D -1) THEN InstHyp [\mkleeneopen{}m1\mkleeneclose{};\mkleeneopen{}sig\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}] (-2)\mcdot{} THEN Auto)) THEN (Assert \mneg{}(b <loc a) BY ((D 0 THENA Auto) THEN Unfold `oar-order` 11 THEN (InstHyp [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}sndr\mkleeneclose{};\mkleeneopen{}m1\mkleeneclose{};\mkleeneopen{}sig\mkleeneclose{};\mkleeneopen{}o\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}] 11\mcdot{} THENA Auto) THEN RepeatFor 2 (D -1) THEN InstHyp [\mkleeneopen{}m2\mkleeneclose{};\mkleeneopen{}s1\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}] (-2)\mcdot{} THEN Auto)) THEN (Assert a = b BY ((Assert loc(a) = loc(b) BY Auto) THEN (RWO "es-locl-trichotomy" (-1) THENA Auto) THEN RepeatFor 2 ((D -1 THEN Auto))))) Home Index