@startuml
!pragma teoz true

database DL
actor P1
actor Pi

P1 -> P1 : <latex>ABcast(m)</latex>
P1 -> P1 : <latex>m \in S</latex>

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) Pi : <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
    else <latex>(\exists j, r' : (j, prove(r')) \in P \land m \in prop[r'][j])</latex>
        note over P1 : break
    end
end
hide footbox
@enduml