@startuml
!pragma teoz true

database DL
actor P1
actor P2
P1 -> DL : <latex>READ()</latex>
DL --> P1 : <latex>P</latex>
P1 -> P1 : <latex>r_{max} = max\{r : (\_, prove(r)) \in P\}</latex>

loop <latex>\textbf{foreach } r \in \{r_{max} + 1, \dots\}</latex>

    ' P1 ->(05) P2 : <latex>RBcast(prop, S, r, 1)</latex>

    P1 -> DL : <latex>PROVE(r)</latex>
    P1 -> DL : <latex>APPEND(r)</latex>

    P1 -> DL : <latex>READ()</latex>
    DL --> P1 : <latex>P</latex>

    alt <latex>(1, \text{prove(}r\text{)}) \in P</latex>
        note over P1 : break
    end
end

P2 -> P2 : <latex>ABdeliver()</latex>
P2 -> DL : <latex>READ()</latex>
DL --> P2 : <latex>P</latex>
note over P2
    line(C4)
    process P2 check locally if 
    <latex>\forall j : (j, prove(r)) \not\in P</latex>
    which is false since P1 correctly 
    PROVE(r) and APPEND(r)

    <latex>\text{P1 is next include in } W_r</latex>
end note

P2 -> DL : <latex>APPEND(r)</latex>
P2 -> DL : <latex>READ()</latex>
DL --> P2 : <latex>P</latex>

note over P2
    line(C9)
    process P2 check locally if
    <latex>\forall j \in W_r : prop[r][j] = \bot</latex>
    which can't be false since P1 didn't
    execute <latex>RBcast(prop, S, r, 1)</latex>

    P2 will never progress and
    deliver any futur messages
end note
hide footbox
@enduml