Byzantská dohoda: Spec2
(B1) ? ?u: u ? g :: ?d0[u] ? ? ? ?u, x:: ?con0[u, x] ?
(A1) conr[u, v] = dr?1[v]
(A2) conr?1[u, x] ?conr[v, x]
(E1) dr[u] = dr?1[u] ? (conr[u, ?] ? r ? conr[u, g])
Správnost Spec2 (ukázeme, ze Spec2 ? Spec1)
Veta: Ak g je spolahlivý, tak platí
? ?r: r ? 1:: dr[u] = d0[g] ?
r = 1: z (E1): d1[u] = d0[u] ? (con1[u, ?] ? 1 ? con1[u, g]),
ale con1[u, g] ? con1[u, ?] ? 1
a z (A1) con1[u, g] = d0[g], takze
Ak u = g, tak d1[g] = d0[g] ? d0[g],
ak u ? g, tak d1[u] = false ? d0[g] = d0[g]
r > 1: dr[u] = dr?1[u] ? (conr[u, ?] ? r ? conr[u, g])
z hypotézy vieme, ze dr?1[u] = d0[g]
z (A1) (v := g) conr[u, g] = dr?1[g] (= d0[g]),
teda dr[u] = d0[g] ? (conr[u, ?] ? r ? d0[g]) = d0[g]