Verbose proof for C2.

C2:

{1} (∀ (r : {s : nat | s ≤ m}) : C2 prop(r))

Installing automatic rewrites: send ax

distr remove lemma nok lemma1

C2:

[1] (∀ (r : {s : nat | s ≤ m}) : C2 prop(r))

Inducting on r ,

we get 3 subgoals:

C2.1:

\begin{matrix}\{1\} & r′ ≤ m \\ \{2\} & C2 prop(r′) \end{matrix}

Simplifying, rewriting, and recording with decision procedures, This completes the proof of C2.1.

C2.2:

{1} 0 ≤ m ⊃ C2 prop(0)

Simplifying, rewriting, and recording with decision procedures,

C2.2:

[1] 0 ≤ m ⊃ C2 prop(0)

Expanding the definition of C2 prop ,

C2.2:

{1} (∀ (p : {s : nat | s < n}), (G : {s : nat | s < n}), (t : T), (caucus : [{s : nat | s < n} → bool]) : ok(p)∧ ok(G)∧ p ∈ caucus∧ G ∈ caucus∧ |caucus| > 2 × |nok(caucus)| ⊃ OMBG(G, 0, t, caucus)(p) = t)

Skolemizing and flattening,

C2.2:

{-1} ok(p′)
{-2} ok(G′)
{-3} p′ ∈ caucus′
{-4} G′ ∈ caucus′
{-5} |caucus′| > 2 × |nok(caucus′)|
{1} OMBG(G′, 0, t′, caucus′)(p′) = t′

Expanding the definition of OMBG ,

C2.2:

{-1} ok(p′)
{-2} ok(G′)
{-3} p′ ∈ caucus′
{-4} G′ ∈ caucus′
{-5} |caucus′| > 2 × |nok(caucus′)|

{1}

if G′ ∈ caucus′ ∧ p′ ∈ caucus′

then send(t′, G′, p′)

else arb

endif = t′

Applying propositional simplification and decision procedures, This completes the proof of C2.2.

C2.3:

{1} (∀ (j : {i : integer | i ≥ 0}) : j ≤ m ⊃ C2 prop(j) ⊃ j + 1 ≤ m ⊃ C2 prop(j + 1))

Skolemizing and flattening,

C2.3:

{-1} j′ ≤ m ⊃ C2 prop(j′)
{-2} j′ + 1 ≤ m
{1} C2 prop(j′ + 1)

Expanding the definition of C2 prop ,

C2.3:

{-1} j′ ≤ m ⊃ C2 prop(j′)
{-2} j′ + 1 ≤ m

{1} (∀ (p : {s : nat | s < n}), (G : {s : nat | s < n}), (t : T), (caucus : [{s : nat | s < n} → bool]) :

ok(p)∧
ok(G)∧
p ∈ caucus∧
G ∈ caucus∧

|caucus| > 1 + 2 × |nok(caucus)| + j′ ⊃ OMBG(G, 1 + j′, t, caucus)(p) = t)

Skolemizing and flattening,

C2.3:

{-1} j′ ≤ m ⊃ C2 prop(j′)
{-2} j′ + 1 ≤ m
{-3} ok(p′)
{-4} ok(G′)
{-5} p′ ∈ caucus′
{-6} G′ ∈ caucus′
{-7} |caucus′| > 1 + 2 × |nok(caucus′)| + j′
{1} OMBG(G′, 1 + j′, t′, caucus′)(p′) = t′

Expanding the definition of OMBG ,

C2.3:

{-1} j′ ≤ m ⊃ C2 prop(j′)
{-2} j′ + 1 ≤ m
{-3} ok(p′)
{-4} ok(G′)
{-5} p′ ∈ caucus′
{-6} G′ ∈ caucus′
{-7} |caucus′| > 1 + 2 × |nok(caucus′)| + j′

{1}

if G′ ∈ caucus′ ∧ p′ ∈ caucus′
then if p′ = G′

then send(t′, G′, G′)

else

maj(caucus′ \ {G′}, (λ (q : {s : nat | s < n}) : OMBG(q, j′, send(t′, G′, q), caucus′ \ {G′})(p′)))

endif

else arb

endif = t′

Repeatedly simplifying with BDDs, decision procedures, rewriting, and if-lifting,

C2.3:

{-1} C2 prop(j′)
{-2} 1 + j′ ≤ m
{-3} ok(p′)
{-4} ok(G′)
{-5} p′ ∈ caucus′
{-6} G′ ∈ caucus′
{-7} |caucus′| > 1 + 2 × |nok(caucus′)| + j′
{1} p′ = G′
{2} maj(caucus′ \ {G′}, (λ (q : {s : nat | s < n}) : OMBG(q, j′, send(t′, G′, q), caucus′ \ {G′})(p′))) = t′

Rewriting using maj ax ,

C2.3:

{-1} C2 prop(j′)
{-2} 1 + j′ ≤ m
{-3} ok(p′)
{-4} ok(G′)
{-5} p′ ∈ caucus′
{-6} G′ ∈ caucus′
{-7} |caucus′| > 1 + 2 × |nok(caucus′)| + j′

{1} (∀ (p : {s : nat | s < n}) :

ok(p) ∧ p ∈ caucus′ \ {G′} ⊃

OMBG(p, j′, send(t′, G′, p), caucus′ \ {G′})(p′) = t′)
{2} p′ = G′
{3} maj(caucus′ \ {G′}, (λ (q : {s : nat | s < n}) : OMBG(q, j′, send(t′, G′, q), caucus′ \ {G′})(p′))) = t′

Hiding formulas: -7, 3,

C2.3:

{-1} C2 prop(j′)
{-2} 1 + j′ ≤ m
{-3} ok(p′)
{-4} ok(G′)
{-5} p′ ∈ caucus′
{-6} G′ ∈ caucus′

{1} (∀ (p : {s : nat | s < n}) : ok(p) ∧ p ∈ caucus′ \ {G′} ⊃

OMBG(p, j′, send(t′, G′, p), caucus′ \ {G′})(p′) = t′)
{2} p′ = G′

Skolemizing and flattening,

C2.3:

{-1} ok(p′′)
{-2} p′′ ∈ caucus′ \ {G′}
{-3} C2 prop(j′)
{-4} 1 + j′ ≤ m
{-5} ok(p′)
{-6} ok(G′)
{-7} p′ ∈ caucus′
{-8} G′ ∈ caucus′
{1} OMBG(p′′, j′, send(t′, G′, p′′), caucus′ \ {G′})(p′) = t′
{2} p′ = G′

Expanding the definition of C2 prop ,

C2.3:

{-1} ok(p′′)
{-2} p′′ ∈ caucus′ \ {G′}

{-3} (∀ (p : {s : nat | s < n}), (G : {s : nat | s < n}), (t : T), (caucus : [{s : nat | s < n} → bool]) :

ok(p)∧
ok(G)∧
p ∈ caucus∧
G ∈ caucus∧
|caucus| > 2 × |nok(caucus)| + j′ ⊃
OMBG(G, j′, t, caucus)(p) = t)
{-4} 1 + j′ ≤ m
{-5} ok(p′)
{-6} ok(G′)
{-7} p′ ∈ caucus′
{-8} G′ ∈ caucus′
{1} OMBG(p′′, j′, send(t′, G′, p′′), caucus′ \ {G′})(p′) = t′
{2} p′ = G′

Instantiating quantified variables,

C2.3:

{-1} ok(p′′)
{-2} p′′ ∈ caucus′ \ {G′}

{-3} ok(p′)∧ ok(p′′)∧

p′ ∈ caucus′ \ {G′}∧
p′′ ∈ caucus′ \ {G′}∧

|caucus′ \ {G′}| > 2 × |nok(caucus′ \ {G′})| + j′ ⊃ OMBG(p′′, j′, send(t′, G′, p′′), caucus′ \ {G′})(p′) = send(t′, G′, p′′)

{-4} 1 + j′ ≤ m
{-5} ok(p′)
{-6} ok(G′)
{-7} p′ ∈ caucus′
{-8} G′ ∈ caucus′
{1} OMBG(p′′, j′, send(t′, G′, p′′), caucus′ \ {G′})(p′) = t′
{2} p′ = G′

Applying propositional simplification and decision procedures, we get 2 subgoals:

C2.3.1:

{-1} OMBG(p′′, j′, send(t′, G′, p′′), caucus′ \ {G′})(p′) = send(t′, G′, p′′)
{-2} ok(p′′)
{-3} p′′ ∈ caucus′ \ {G′}
{-4} 1 + j′ ≤ m
{-5} ok(p′)
{-6} ok(G′)
{-7} p′ ∈ caucus′
{-8} G′ ∈ caucus′
{1} OMBG(p′′, j′, t′, caucus′ \ {G′})(p′) = t′
{2} p′ = G′

Simplifying, rewriting, and recording with decision procedures, This completes the proof of C2.3.1.

C2.3.2:

{-1} ok(p′′)
{-2} p′′ ∈ caucus′ \ {G′}
{-3} 1 + j′ ≤ m
{-4} ok(p′)
{-5} ok(G′)
{-6} p′ ∈ caucus′
{-7} G′ ∈ caucus′
{1} p′ ∈ caucus′ \ {G′}
{2} OMBG(p′′, j′, t′, caucus′ \ {G′})(p′) = t′
{3} p′ = G′

Trying repeated skolemization, instantiation, and if-lifting, This completes the proof of C2.3.2. Q.E.D.