Verbose proof for C1.

C1:

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

Installing automatic rewrites: send ax

distr

C1:

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

Inducting on r ,

we get 3 subgoals:

C1.1:

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

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

C1.2:

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

Applying disjunctive simplification to flatten sequent,

C1.2:

\begin{matrix}\{-1\} & 0 ≤ m \\ \{1\} & C1 prop(0) \end{matrix}

Expanding the definition of C1 prop ,

C1.2:

{-1} 0 ≤ m ; {1} (∀ (p : {s : nat | s < n}), (q : {s : nat | s < n}), (G : {s : nat | s < n}), (caucus : [{s : nat | s < n} → bool]), (t : T) : ok(p)∧ ok(q)∧ p ∈ caucus∧ q ∈ caucus∧ G ∈ caucus∧ |caucus| > 0∧ 0 ≥ |nok(caucus)| ⊃ OMBG(G, 0, t, caucus)(p) = OMBG(G, 0, t, caucus)(q))

Skolemizing and flattening,

C1.2:

{-1} 0 ≤ m
{-2} ok(p′)
{-3} ok(q′)
{-4} p′ ∈ caucus′
{-5} q′ ∈ caucus′
{-6} G′ ∈ caucus′
{-7} |caucus′| > 0
{-8} 0 ≥ |nok(caucus′)|
{1} OMBG(G′, 0, t′, caucus′)(p′) = OMBG(G′, 0, t′, caucus′)(q′)

Simplifying, rewriting, and recording with decision procedures,

C1.2:

{-1} 0 ≤ m
{-2} ok(p′)
{-3} ok(q′)
{-4} p′ ∈ caucus′
{-5} q′ ∈ caucus′
{-6} G′ ∈ caucus′
{-7} |caucus′| > 0
{-8} 0 ≥ |nok(caucus′)|
{1} OMBG(G′, 0, t′, caucus′)(p′) = OMBG(G′, 0, t′, caucus′)(q′)

Case splitting on ok(G′) ,

we get 2 subgoals:

C1.2.1:

{-1} ok(G′)
{-2} 0 ≤ m
{-3} ok(p′)
{-4} ok(q′)
{-5} p′ ∈ caucus′
{-6} q′ ∈ caucus′
{-7} G′ ∈ caucus′
{-8} |caucus′| > 0
{-9} 0 ≥ |nok(caucus′)|
{1} OMBG(G′, 0, t′, caucus′)(p′) = OMBG(G′, 0, t′, caucus′)(q′)

Expanding the definition of OMBG ,

C1.2.1:

[-1] ok(G′)
[-2] 0 ≤ m
[-3] ok(p′)
[-4] ok(q′)
[-5] p′ ∈ caucus′
[-6] q′ ∈ caucus′
[-7] G′ ∈ caucus′
[-8] |caucus′| > 0
[-9] 0 ≥ |nok(caucus′)|
{1} send(t′, G′, p′) = send(t′, G′, q′)

Simplifying, rewriting, and recording with decision procedures, This completes the proof of C1.2.1.

C1.2.2:

{-1} 0 ≤ m
{-2} ok(p′)
{-3} ok(q′)
{-4} p′ ∈ caucus′
{-5} q′ ∈ caucus′
{-6} G′ ∈ caucus′
{-7} |caucus′| > 0
{-8} 0 ≥ |nok(caucus′)|
{1} ok(G′)
{2} OMBG(G′, 0, t′, caucus′)(p′) = OMBG(G′, 0, t′, caucus′)(q′)

Hiding formulas: 2,

C1.2.2:

[-1] 0 ≤ m
[-2] ok(p′)
[-3] ok(q′)
[-4] p′ ∈ caucus′
[-5] q′ ∈ caucus′
[-6] G′ ∈ caucus′
[-7] |caucus′| > 0
[-8] 0 ≥ |nok(caucus′)|
[1] ok(G′)

Adding type constraints for |nok(caucus′)| ,

C1.2.2:

{-1} |nok(caucus′)| ≥ 0
[-2] 0 ≤ m
[-3] ok(p′)
[-4] ok(q′)
[-5] p′ ∈ caucus′
[-6] q′ ∈ caucus′
[-7] G′ ∈ caucus′
[-8] |caucus′| > 0
[-9] 0 ≥ |nok(caucus′)|
[1] ok(G′)

Using lemma fincard non empty ,

C1.2.2:

{-1} (∃ (z : {s : nat | s < n}) : nok(caucus′)(z)) ⇔

|nok(caucus′)| ≠ 0

{-2} |nok(caucus′)| ≥ 0
[-3] 0 ≤ m
[-4] ok(p′)
[-5] ok(q′)
[-6] p′ ∈ caucus′
[-7] q′ ∈ caucus′
[-8] G′ ∈ caucus′
[-9] |caucus′| > 0
[-10] 0 ≥ |nok(caucus′)|
[1] ok(G′)

Applying propositional simplification and decision procedures,

C1.2.2:

{-1} |nok(caucus′)| = 0
{-2} |nok(caucus′)| ≥ 0
[-3] 0 ≤ m
[-4] ok(p′)
[-5] ok(q′)
[-6] p′ ∈ caucus′
[-7] q′ ∈ caucus′
[-8] G′ ∈ caucus′
[-9] |caucus′| > 0
[-10] 0 ≥ |nok(caucus′)|
{1} (∃ (z : {s : nat | s < n}) : nok(caucus′)(z))
[2] ok(G′)

Instantiating the top quantifier in 1 with the terms: G!1 ,

C1.2.2:

{-1} |nok(caucus′)| = 0
{-2} |nok(caucus′)| ≥ 0
[-3] 0 ≤ m
[-4] ok(p′)
[-5] ok(q′)
[-6] p′ ∈ caucus′
[-7] q′ ∈ caucus′
[-8] G′ ∈ caucus′
[-9] |caucus′| > 0
[-10] 0 ≥ |nok(caucus′)|
{1} nok(caucus′)(G′)
[2] ok(G′)

Expanding the definition of nok ,

C1.2.2:

{-1} |{z : proc | z ∈ caucus′ ∧ ¬ok(z)}| = 0
{-2} |{z : proc | z ∈ caucus′ ∧ ¬ok(z)}| ≥ 0
[-3] 0 ≤ m
[-4] ok(p′)
[-5] ok(q′)
[-6] p′ ∈ caucus′
[-7] q′ ∈ caucus′
[-8] G′ ∈ caucus′
[-9] |caucus′| > 0
{-10} 0 ≥ |{z : proc | z ∈ caucus′ ∧ ¬ok(z)}|
{1} true
[2] ok(G′)

which is trivially true. This completes the proof of C1.2.2.

C1.3:

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

Skolemizing and flattening,

C1.3:

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

Expanding the definition of C1 prop ,

C1.3:

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

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

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

|caucus| > 3 + 3 × j′∧ 1 + j′ ≥ |nok(caucus)| ⊃

OMBG(G, 1 + j′, t, caucus)(p) = OMBG(G, 1 + j′, t, caucus)(q))

Skolemizing and flattening,

C1.3:

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

{1} OMBG(G′, 1 + j′, t′, caucus′)(p′) = OMBG(G′, 1 + j′, t′, caucus′)(q′)

Simplifying, rewriting, and recording with decision procedures,

C1.3:

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

{1} OMBG(G′, 1 + j′, t′, caucus′)(p′) = OMBG(G′, 1 + j′, t′, caucus′)(q′)

Case splitting on ok(G′) ,

we get 2 subgoals:

{-1} ok(G′)
{-2} C1 prop(j′)
{-3} 1 + j′ ≤ m
{-4} ok(p′)
{-5} ok(q′)
{-6} p′ ∈ caucus′
{-7} q′ ∈ caucus′
{-8} G′ ∈ caucus′
{-9} |caucus′| > 3 + 3 × j′
{-10} 1 + j′ ≥ |nok(caucus′)|

{1} OMBG(G′, 1 + j′, t′, caucus′)(p′) = OMBG(G′, 1 + j′, t′, caucus′)(q′)

Applying C2 where

C1.3.1:

{-1} (∀ (r : {s : nat | s ≤ m}) : C2 prop(r))
[-2] ok(G′)
[-3] C1 prop(j′)
[-4] 1 + j′ ≤ m
[-5] ok(p′)
[-6] ok(q′)
[-7] p′ ∈ caucus′
[-8] q′ ∈ caucus′
[-9] G′ ∈ caucus′
[-10] |caucus′| > 3 + 3 × j′
[-11] 1 + j′ ≥ |nok(caucus′)|

[1] OMBG(G′, 1 + j′, t′, caucus′)(p′) = OMBG(G′, 1 + j′, t′, caucus′)(q′)

Expanding the definition of C2 prop ,

C1.3.1:

{-1} (∀ (r : {s : nat | s ≤ m}) : (∀ (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| > r + 2 × |nok(caucus)| ⊃ OMBG(G, r, t, caucus)(p) = t))

[-2] ok(G′)
[-3] C1 prop(j′)
[-4] 1 + j′ ≤ m
[-5] ok(p′)
[-6] ok(q′)
[-7] p′ ∈ caucus′
[-8] q′ ∈ caucus′
[-9] G′ ∈ caucus′
[-10] |caucus′| > 3 + 3 × j′
[-11] 1 + j′ ≥ |nok(caucus′)|

[1] OMBG(G′, 1 + j′, t′, caucus′)(p′) = OMBG(G′, 1 + j′, t′, caucus′)(q′)

Installing automatic rewrites: -1

C1.3.1:

{-1} (∀ (r : {s : nat | s ≤ m}) : (∀ (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| > r + 2 × |nok(caucus)| ⊃ OMBG(G, r, t, caucus)(p) = t))

[-2] ok(G′)
[-3] C1 prop(j′)
[-4] 1 + j′ ≤ m
[-5] ok(p′)
[-6] ok(q′)
[-7] p′ ∈ caucus′
[-8] q′ ∈ caucus′
[-9] G′ ∈ caucus′
[-10] |caucus′| > 3 + 3 × j′
[-11] 1 + j′ ≥ |nok(caucus′)|

[1] OMBG(G′, 1 + j′, t′, caucus′)(p′) = OMBG(G′, 1 + j′, t′, caucus′)(q′)

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

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

{2} OMBG(G′, 1 + j′, t′, caucus′)(p′) = OMBG(G′, 1 + j′, t′, caucus′)(q′)

Expanding the definition of OMBG ,

C1.3.2:

[-1] C1 prop(j′)
[-2] 1 + j′ ≤ m
[-3] ok(p′)
[-4] ok(q′)
[-5] p′ ∈ caucus′
[-6] q′ ∈ caucus′
[-7] G′ ∈ caucus′
[-8] |caucus′| > 3 + 3 × j′
[-9] 1 + j′ ≥ |nok(caucus′)|
[1] ok(G′)

{2} 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 = ifq′ = G′ then send(t′, G′, G′) else maj(caucus′ \ {G′}, (λ (q : {s : nat | s < n}) : OMBG(q, j′, send(t′, G′, q), caucus′ \ {G′})(q′))) endif

Applying propositional simplification and decision procedures,

[-1] C1 prop(j′)
[-2] 1 + j′ ≤ m
[-3] ok(p′)
[-4] ok(q′)
[-5] p′ ∈ caucus′
[-6] q′ ∈ caucus′
[-7] G′ ∈ caucus′
[-8] |caucus′| > 3 + 3 × j′
[-9] 1 + j′ ≥ |nok(caucus′)|
[1] ok(G′)

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

Rewriting using maj ext ,

C1.3.2:

[-1] C1 prop(j′)
[-2] 1 + j′ ≤ m
[-3] ok(p′)
[-4] ok(q′)
[-5] p′ ∈ caucus′
[-6] q′ ∈ caucus′
[-7] G′ ∈ caucus′
[-8] |caucus′| > 3 + 3 × j′
[-9] 1 + j′ ≥ |nok(caucus′)|

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

p ∈ caucus′ \ {G′} ⊃

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

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

Hiding formulas: 3,

C1.3.2:

[-1] C1 prop(j′)
[-2] 1 + j′ ≤ m
[-3] ok(p′)
[-4] ok(q′)
[-5] p′ ∈ caucus′
[-6] q′ ∈ caucus′
[-7] G′ ∈ caucus′
[-8] |caucus′| > 3 + 3 × j′
[-9] 1 + j′ ≥ |nok(caucus′)|

{1} (∀ (p : {s : nat | s < n}) : p ∈ caucus′ \ {G′} ⊃ OMBG(p, j′, send(t′, G′, p), caucus′ \ {G′})(p′) = OMBG(p, j′, send(t′, G′, p), caucus′ \ {G′})(q′))

[2] ok(G′)

Skolemizing and flattening,

C1.3.2:

{-1} p′′ ∈ caucus′ \ {G′}
[-2] C1 prop(j′)
[-3] 1 + j′ ≤ m
[-4] ok(p′)
[-5] ok(q′)
[-6] p′ ∈ caucus′
[-7] q′ ∈ caucus′
[-8] G′ ∈ caucus′
[-9] |caucus′| > 3 + 3 × j′
[-10] 1 + j′ ≥ |nok(caucus′)|

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

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

[2] ok(G′)

Expanding the definition of C1 prop ,

C1.3.2:

{-1} p′′ ∈ caucus′ \ {G′}

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

ok(q)∧ p ∈ caucus∧

q ∈ caucus∧
G ∈ caucus∧
|caucus| > 3 × j′∧
j′ ≥ |nok(caucus)| ⊃

OMBG(G, j′, t, caucus)(p) = OMBG(G, j′, t, caucus)(q))

[-3] 1 + j′ ≤ m
[-4] ok(p′)
[-5] ok(q′)
[-6] p′ ∈ caucus′
[-7] q′ ∈ caucus′
[-8] G′ ∈ caucus′
[-9] |caucus′| > 3 + 3 × j′
[-10] 1 + j′ ≥ |nok(caucus′)|

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

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

[2] ok(G′)

Instantiating quantified variables,

C1.3.2:

{-1} p′′ ∈ caucus′ \ {G′}

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

|caucus′ \ {G′}| > 3 × j′∧
j′ ≥ |nok(caucus′ \ {G′})| ⊃

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

[-3] 1 + j′ ≤ m
[-4] ok(p′)
[-5] ok(q′)
[-6] p′ ∈ caucus′
[-7] q′ ∈ caucus′
[-8] G′ ∈ caucus′
[-9] |caucus′| > 3 + 3 × j′
[-10] 1 + j′ ≥ |nok(caucus′)|

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

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

[2] ok(G′)

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