---

Step * 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. ∀m1,m2:M.  Dec(m1 = m2 ∈ M)@i
16. e1 : E@i
17. e2 : E@i
18. n : ℕ@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 < n ⇒ (∃msg':M. ∃e':E. ((e' <loc e1) ∧ <sndr, n - 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 < n ⇒ (∃msg':M. ∃e':E. ((e' <loc e2) ∧ <sndr, n - 1, msg'> ∈ OARDeliver(e2)))
32. L : 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)||
BY
{ ((BagToList 8 THENA Auto)
   THEN ((InstLemma `l_intersection-size` [⌈Id⌉;⌈IdDeq⌉;⌈L⌉;⌈L1⌉;⌈orderers⌉]⋅
         THENM (All (Unfold `bag-size`) THEN Auto')
         )
         THENA (Auto
                THEN Unfold `l_contains` 0
                ⋅
                THEN OnMaybeHyp 28 (\h. (RepeatFor 2 (ParallelOp h)
                                         THEN Auto
                                         THEN RWO  "bag-member-list" (-2)
                                         THEN Complete (Auto))))
         )
   ) }

---

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.  \mforall{}m1,m2:M.    Dec(m1  =  m2)@i
16.  e1  :  E@i
17.  e2  :  E@i
18.  n  :  \mBbbN{}@i
19.  sndr  :  Id@i
20.  m1  :  M@i
21.  m2  :  M@i
22.  <sndr,  n,  m1>  \mmember{}  OARDeliver(e1)@i
23.  <sndr,  n,  m2>  \mmember{}  OARDeliver(e2)@i
24.  correct  loc(e1)@i
25.  correct  loc(e2)@i
26.  0  <  n  {}\mRightarrow{}  (\mexists{}msg':M.  \mexists{}e':E.  ((e'  <loc  e1)  \mwedge{}  <sndr,  n  -  1,  msg'>  \mmember{}  OARDeliver(e1)))
27.  L1  :  Id  List
28.  ||L1||  =  ((2  *  f)  +  1)
29.  no\_repeats(Id;L1)
30.  (\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')))))
31.  0  <  n  {}\mRightarrow{}  (\mexists{}msg':M.  \mexists{}e':E.  ((e'  <loc  e2)  \mwedge{}  <sndr,  n  -  1,  msg'>  \mmember{}  OARDeliver(e2)))
32.  L  :  Id  List
33.  ||L||  =  ((2  *  f)  +  1)
34.  no\_repeats(Id;L)
35.  (\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')))))
36.  \mforall{}o:Id.  ((o  \mmember{}  L1)  {}\mRightarrow{}  (o  \mmember{}  L)  {}\mRightarrow{}  (\mneg{}(correct  o)))@i
\mvdash{}  f  <  ||l\_intersection(IdDeq;L;L1)||


By

---

Latex:
((BagToList  8  THENA  Auto)
  THEN  ((InstLemma  `l\_intersection-size`  [\mkleeneopen{}Id\mkleeneclose{};\mkleeneopen{}IdDeq\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}L1\mkleeneclose{};\mkleeneopen{}orderers\mkleeneclose{}]\mcdot{}
              THENM  (All  (Unfold  `bag-size`)  THEN  Auto')
              )
              THENA  (Auto
                            THEN  Unfold  `l\_contains`  0
                            \mcdot{}
                            THEN  OnMaybeHyp  28  (\mbackslash{}h.  (RepeatFor  2  (ParallelOp  h)
                                                                              THEN  Auto
                                                                              THEN  RWO    "bag-member-list"  (-2)
                                                                              THEN  Complete  (Auto))))
              )
  )

---

Home Index