Byzantská dohoda: Spec2
Veta: ? ?u, v:: dt+1[u] = dt+1[v] ?
Dôkaz: Ak g je spolahlivý, tak platnost vyplýva z predošlej vety. Nech teda g je nespolahlivý.
Nech r je najmenšie také, ze dr[u] platí pre nejaké u. Ak také r neexistuje, veta platí. Ukázeme, ze platí r ? t a dr+1[v] pre ? v.
?dr?1[u] ? dr[u] /* výber r a u */
conr[u, ?] ? r ? conr[u, g] /* (a), z (E1) */
conr[u, x] ? conr+1[v, x] /* z (A2) */
?conr[u, u] /* z (A1), ?dr?1[u] */
conr+1[v, u] /* z (A1), dr[u] */
conr+1[v, ?] > conr+1[u, ?] /* z predošlých troch */
conr+1[v, ?] ? r + 1 /* z (a) */
conr+1[v, g] /* z (a) a (A2) */
dr+1[v] /* z predošlých dvoch */
Ukázeme, ze r ? t, cím dostaneme dr+1[u] ? dt+1[v] z (E1).
Vyberali sme r tak, ze bolo najmenšie, teda
?conr[u, w] /* (b), z (A1) */
(b) pre spolahlivé neplatí, môze to platit teda len pre nespolahlivé (nie nutne pre všetky), ktorých je t. Cize
r ? conr[u, ?] ? t /* z (a) */