Step * 1 of Lemma OARcast_lemma1


1. Info Type
2. es EO+(Info)@i'
3. Type@i'
4. EClass(Id × Atom1 × Id × ℕ × M)@i'
5. EClass(Id × Atom1 × Id × ℕ × M)@i'
6. correct Id ─→ ℙ@i'
7. : ℕ@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 <  (∃msg':M. ∃e':E. ((e' <loc e) ∧ <sndr, 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 ↓∈  (x ↓∈ orderers ∧ (correct x)))))))@i
16. ∀m1,m2:M.  Dec(m1 m2 ∈ M)@i
17. e1 E@i
18. e2 E@i
19. : ℕ@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 <  (∃msg':M. ∃e':E. ((e' <loc e1) ∧ <sndr, 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 <  (∃msg':M. ∃e':E. ((e' <loc e2) ∧ <sndr, 1, msg'> ∈ OARDeliver(e2)))
33. 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')))))
⊢ m1 m2 ∈ M
BY
(Assert ¬(∀o:Id. ((o ∈ L1)  (o ∈ L)  (correct o)))) BY
         (ParallelOp 15
          THEN With ⌈l_intersection(IdDeq;L;L1)⌉ (D 0)⋅
          THEN Auto
          THEN Try ((BLemma `bag-no-repeats-list` THEN Auto THEN Unfold `l_intersection` THEN Auto))
          THEN Try (((FLemma `bag-member-list` [-2] THENA Auto) THEN RWO "member-intersection" (-1)⋅ THEN Auto))
          THEN Try (((FLemma `bag-member-list` [-1] THENA Auto)
                     THEN RWO "member-intersection" (-1)⋅
                     THEN Auto
                     THEN OnMaybeHyp 34 (\h. (RWO "l_all_iff" THEN Complete (Auto)))))
          THEN Unfold `bag-size` 0)) }

1
1. Info Type
2. es EO+(Info)@i'
3. Type@i'
4. EClass(Id × Atom1 × Id × ℕ × M)@i'
5. EClass(Id × Atom1 × Id × ℕ × M)@i'
6. correct Id ─→ ℙ@i'
7. : ℕ@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 <  (∃msg':M. ∃e':E. ((e' <loc e) ∧ <sndr, 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. ∀m1,m2:M.  Dec(m1 m2 ∈ M)@i
16. e1 E@i
17. e2 E@i
18. : ℕ@i
19. sndr Id@i
20. m1 M@i
21. m2 M@i
22. <sndr, n, m1> ∈ OARDeliver(e1)@i
23. <sndr, n, m2> ∈ OARDeliver(e2)@i
24. correct loc(e1)@i
25. correct loc(e2)@i
26. 0 <  (∃msg':M. ∃e':E. ((e' <loc e1) ∧ <sndr, 1, msg'> ∈ OARDeliver(e1)))
27. L1 Id List
28. ||L1|| ((2 f) 1) ∈ ℤ
29. no_repeats(Id;L1)
30. (∀o∈L1.o ↓∈ orderers ∧ (∃e':E(V). (e' ≤loc e1  ∧ (∃sig:Atom1. <o, sig, sndr, n, m1> ∈ V(e')))))
31. 0 <  (∃msg':M. ∃e':E. ((e' <loc e2) ∧ <sndr, 1, msg'> ∈ OARDeliver(e2)))
32. Id List
33. ||L|| ((2 f) 1) ∈ ℤ
34. no_repeats(Id;L)
35. (∀o∈L.o ↓∈ orderers ∧ (∃e':E(V). (e' ≤loc e2  ∧ (∃sig:Atom1. <o, sig, sndr, n, m2> ∈ V(e')))))
36. ∀o:Id. ((o ∈ L1)  (o ∈ L)  (correct o)))@i
⊢ f < ||l_intersection(IdDeq;L;L1)||

2
1. Info Type
2. es EO+(Info)@i'
3. Type@i'
4. EClass(Id × Atom1 × Id × ℕ × M)@i'
5. EClass(Id × Atom1 × Id × ℕ × M)@i'
6. correct Id ─→ ℙ@i'
7. : ℕ@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 <  (∃msg':M. ∃e':E. ((e' <loc e) ∧ <sndr, 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 ↓∈  (x ↓∈ orderers ∧ (correct x)))))))@i
16. ∀m1,m2:M.  Dec(m1 m2 ∈ M)@i
17. e1 E@i
18. e2 E@i
19. : ℕ@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 <  (∃msg':M. ∃e':E. ((e' <loc e1) ∧ <sndr, 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 <  (∃msg':M. ∃e':E. ((e' <loc e2) ∧ <sndr, 1, msg'> ∈ OARDeliver(e2)))
33. 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))))
⊢ m1 m2 ∈ M


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')))))
\mvdash{}  m1  =  m2


By


Latex:
(Assert  \mneg{}(\mforall{}o:Id.  ((o  \mmember{}  L1)  {}\mRightarrow{}  (o  \mmember{}  L)  {}\mRightarrow{}  (\mneg{}(correct  o))))  BY
              (ParallelOp  15
                THEN  With  \mkleeneopen{}l\_intersection(IdDeq;L;L1)\mkleeneclose{}  (D  0)\mcdot{}
                THEN  Auto
                THEN  Try  ((BLemma  `bag-no-repeats-list`  THEN  Auto  THEN  Unfold  `l\_intersection`  0  THEN  Auto))
                THEN  Try  (((FLemma  `bag-member-list`  [-2]  THENA  Auto)
                                      THEN  RWO  "member-intersection"  (-1)\mcdot{}
                                      THEN  Auto))
                THEN  Try  (((FLemma  `bag-member-list`  [-1]  THENA  Auto)
                                      THEN  RWO  "member-intersection"  (-1)\mcdot{}
                                      THEN  Auto
                                      THEN  OnMaybeHyp  34  (\mbackslash{}h.  (RWO  "l\_all\_iff"  h  THEN  Complete  (Auto)))))
                THEN  Unfold  `bag-size`  0))




Home Index