---

Step * of Lemma OARcast_lemma1

∀[Info:Type]
  ∀es:EO+(Info). ∀M:Type. ∀V,S:EClass(Id × Atom1 × Id × ℕ × M). ∀correct:Id ─→ ℙ. ∀f:ℕ. ∀orderers:bag(Id).
  ∀OARDeliver:EClass(Id × ℕ × M).
    (oar-deliver(es;M;V;correct;orderers;f;OARDeliver)
    ⇒ oar-order(es;M;S;correct;orderers)
    ⇒ oar-crypto(es;M;V;S;correct)
    ⇒ oar-failure-model(orderers;f;correct)
    ⇒ (∀m1,m2:M.  Dec(m1 = m2 ∈ M))
    ⇒ oar-consistency(es;M;correct;OARDeliver))
BY
{ (Unfolds ``oar-consistency oar-failure-model`` 0
   THEN (Auto THEN Unfold `oar-deliver` 10 THEN RepeatFor 2 ((FHyp 10 [-4] THENA Auto)) THEN Auto THEN ExRepD)
   ) }

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
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')))))
⊢ m1 = m2 ∈ M

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}M:Type.  \mforall{}V,S:EClass(Id  \mtimes{}  Atom1  \mtimes{}  Id  \mtimes{}  \mBbbN{}  \mtimes{}  M).  \mforall{}correct:Id  {}\mrightarrow{}  \mBbbP{}.  \mforall{}f:\mBbbN{}.
    \mforall{}orderers:bag(Id).  \mforall{}OARDeliver:EClass(Id  \mtimes{}  \mBbbN{}  \mtimes{}  M).
        (oar-deliver(es;M;V;correct;orderers;f;OARDeliver)
        {}\mRightarrow{}  oar-order(es;M;S;correct;orderers)
        {}\mRightarrow{}  oar-crypto(es;M;V;S;correct)
        {}\mRightarrow{}  oar-failure-model(orderers;f;correct)
        {}\mRightarrow{}  (\mforall{}m1,m2:M.    Dec(m1  =  m2))
        {}\mRightarrow{}  oar-consistency(es;M;correct;OARDeliver))


By

---

Latex:
(Unfolds  ``oar-consistency  oar-failure-model``  0
  THEN  (Auto
              THEN  Unfold  `oar-deliver`  10
              THEN  RepeatFor  2  ((FHyp  10  [-4]  THENA  Auto))
              THEN  Auto
              THEN  ExRepD)
  )

---

Home Index