Faulty channels 11 ? ...a jeho správnost
Pri dokazovaní správnosti protokolu pouzijeme upravené invarianty (I1), (I2)
invariant y ? kr ? x.dex ? ks ? y + 1 (I1)
invariant x.val ? ms ? mr ? ms ? |mr| = kr (I2)
(I1) sa dá prepísat (x, y môzu byt nedefinované, ak zodpovedajúce kanály sú null) nasledovným spôsobom:
??y: y ? acks ? y ? ackr:: y ? kr ? ks ? y + 1? ?
??x: x ? cs ? x ? cr:: kr ? x.dex ? ks? ?
kr ? ks ? kr + 1
podobne sa dá prepísat aj (I2)
potrebujeme ešte jeden invariant:
invariant cs.dex, cr.dex, acks, ackr sú neklesajúce
postupnosti (I3)
dôkaz (I1), (I2), (I3) a nasledujúcej progress podmienky: