Byzantská dohoda: Spec3
Lema 2: ? ?r: r ? 0:: conr[u, v] = obsr[u, v] ?
r = 0: sum0[u, v] ? t /* z (B2) */
?con0[u, v] /* z predošlého a (E5) */
r > 1: obsr[u, v] = dr?1[v] /* lema 1 */
? ?w, w’:: obsr[w, v] = obsr[w’, v] ? /* z ?*/
obsr[u, v] = sumr[u, v] > 2.t /* z ? a (D1), (D2) */
obsr[u, v] = conr[u, v] /* z (E5) */
Veta: ? ?r: r ? 1:: conr[u, v] = dr?1[v] ?
Veta: ? ?r: r ? 0:: conr[u, x] ? conr+1[v, x] ?
sumr[u, v] > 2.t /* z (E5) */
? ?w:: sumr[w, x] > t ? /* z (D3) */
? ?w:: obsr+1[w, x] ? /* z (E3) */
sumr+1[v, x] > 2.t /* z (D2) */
conr+1[v, x] /* z (E5) */