Byzantská dohoda: Spec3
Správnost Spec3 (ukázeme, ze Spec3 ? Spec2)
(D1) ? ?w:: obsr[w, x] ? ? sumr[u, x] ? t
(D2) ? ?w:: obsr[w, x] ? ? sumr[u, x] > 2.t
(D3) sumr[u, x] > 2.t ? sumr[v, x] > t
(Dôkaz: sumr[u, x] > 2.t ? ? +w: obsr[w, x]:: 1 ? > t
sumr[v, x] ? ? +w: obsr[w, x]:: 1 ? > t)
Lema 1: ? ?r: r ? 0:: obsr+1[u, v] = dr[v] ?
r = 0: z (E3): obs1[u, v] = (obs0[u, v] ? sum0[u, v] > t ? val0[u, v])
z (B2) (?w:: ?obs0[w, v]) a (D1) máme:
obs1[u, v] = val0[u, v] a z (E4) napokon obs1[u, v] = d0[v]
r > 1: obsr+1[u, v] = (obsr[u, v] ? sumr[u, v] > t ? valr[u, v])
sumr[u, v] > t ? ? ?w:: obsr[w, v] ? /* z (D1) */
obsr[u, x] ? sumr[u, x] > t ? ? ?w:: obsr[w, v] ?
? ?w:: obsr[w, v] ? ? dr?1[v] /* indukcia */
dr?1[v] ? dr[v] /* z (E1) */
valr[u, v] = dr[v] /* (E4) */
obsr+1[u, v] = dr[v] /* z ? */