byzantine[m, n : nat, T : nonempty type] : theory begin assuming mn prop : assumption 3 × m < n endassuming npos : lemma n > 0 proc : type = below[n] rounds : type = upto[m] vector : type = [proc → T] procset : type = setof[proc] ok : procset id : (bijective?[proc, proc]) = (λ (p : proc) : p) importing cardinality@finite cardinality[proc, n, id], cardinality@card set[proc, n, id] G, p, q, z : var proc r : var rounds caucus : var procset v : var vector t : var T nok(caucus) : procset = {z : proc | z ∈ caucus ∧ ¬ok(z)} allprocs : procset = fullset[proc] allset card : lemma |allprocs| = n max faults : axiom |nok(allprocs)| ≤ m remove lemma : lemma p ∈ caucus ⊃ |caucus \ {p}| = |caucus| − 1 nok lemma1 : lemma ok(p) ⊃ |nok(caucus \ {p})| = |nok(caucus)| nok lemma3 : lemma

¬ok(p) ∧ p ∈ caucus ⊃ |nok(caucus \ {p})| = |nok(caucus)| − 1 maj(caucus, v) : T maj ax : axiom |caucus| > 2 × |nok(caucus)|∧

(∀ p : ok(p) ∧ p ∈ caucus ⊃ v(p) = t) ⊃ maj(caucus, v) = t

maj ext : axiom ∀ (v_{1}, v_{2} : vector) : (∀ p : p ∈ caucus ⊃ v_{1}(p) = v_{2}(p)) ⊃ maj(caucus, v_{1}) = maj(caucus, v_{2})

send : [T, proc, proc → T]

send ax : axiom ok(p) ∧ ok(q) ⊃ send(t, p, q) = t

distr(t, p) : vector = (λ (z : proc) : send(t, p, z))

arb : T

OMBG(G, r, t, caucus)(p) : recursive T = if r = 0

then if G ∈ caucus ∧ p ∈ caucus

then send(t, G, p)

else arb

endif

else if G ∈ caucus ∧ p ∈ caucus then if p = G then send(t, G, G) else maj(caucus \ {G}, (λ q : OMBG(q, r − 1, send(t, G, q), caucus \ {G})(p))) endif

else arb

endif endif measure r

C2 prop(r) : bool = (∀ p, G, t, caucus :

ok(p)∧

ok(G)∧
p ∈ caucus∧
G ∈ caucus∧
|caucus| > 2 × |nok(caucus)| + r ⊃
OMBG(G, r, t, caucus)(p) = t)

C_{2} : lemma C2 prop(r)

C2 final : theorem ok(p) ∧ ok(G) ⊃ OMBG(G, m, t, allprocs)(p) = t

C1 prop(r) : bool = (∀ p, q, G, caucus, t :

ok(p)∧

ok(q)∧
p ∈ caucus∧
q ∈ caucus∧
G ∈ caucus∧
|caucus| > 3 × r∧
r ≥ |nok(caucus)| ⊃
OMBG(G, r, t, caucus)(p) = OMBG(G, r, t, caucus)(q))

C_{1} : lemma C1 prop(r) C1 final : theorem

ok(p) ∧ ok(q) ⊃ ∀ (G : proc) : OMBG(G, m, t, allprocs)(p) = OMBG(G, m, t, allprocs)(q)

end byzantine