Synchronous One-Error Gossip with Correction

Call Correction

Single Call Correction

def Error.Call.cor {n : ℕ} : Agent → Call → Call

Equations

• Error.Call.cor x✝ ⌜a c⌝ = ⌜a c⌝
• Error.Call.cor x✝ ⌜a^e c⌝ = if e = x✝ then ⌜a c⌝ else ⌜a^e c⌝
• Error.Call.cor x✝ ⌜a c^e⌝ = if e = x✝ then ⌜a c⌝ else ⌜a c^e⌝

theorem Error.Call.cor_cons_maxOne {n✝ : ℕ} {κ : Call} {σ : List Call} {b : Agent} : maxOne (κ :: σ) → maxOne (cor b κ :: σ)

@[simp]

theorem Error.Call.cor_same_role {n : ℕ} {a b : Agent} {κ : Call} : roleOfIn a (cor b κ) = roleOfIn a κ

@[simp]

theorem Error.call_cor_pair {n : ℕ} (b : Agent) (κ : Call) : (Call.cor b κ).pair = κ.pair

The pair of κ.cor is the same as pair of κ.

Sequence Call Correction

@[irreducible]

def Error.cor {n : ℕ} : Agent → Sequence → Sequence

Equations

• Error.cor x✝ [] = []
• Error.cor x✝ (⌜a c⌝ :: σ) = ⌜a c⌝ :: Error.cor x✝ σ
• Error.cor x✝ (⌜a^e c⌝ :: σ) = if e = x✝ then ⌜a c⌝ :: Error.cor x✝ σ else ⌜a^e c⌝ :: Error.cor x✝ σ
• Error.cor x✝ (⌜a c^e⌝ :: σ) = if e = x✝ then ⌜a c⌝ :: Error.cor x✝ σ else ⌜a c^e⌝ :: Error.cor x✝ σ

@[simp]

theorem Error.cor_errFree {n : ℕ} {σ : Sequence} {b : Agent} (h : errFree σ) : errFree (cor b σ)

@[simp]

theorem Error.cor_maxOne {n : ℕ} {σ : Sequence} {b : Agent} (h : maxOne σ) : maxOne (cor b σ)

@[simp]

theorem Error.cor_same_length {n✝ : ℕ} {b : Agent} {σ : Sequence} : List.length (cor b σ) = List.length σ

theorem Error.cor_cons {n : ℕ} {b : Agent} {κ : Call} {σ : Sequence} : cor b (κ :: σ) = Call.cor b κ :: cor b σ

theorem Error.not_in_call_then_consider_cor {n✝ : ℕ} {a : Agent} {κ : Call} {S : Dist} {σ : List Call} {o : maxOne (κ :: σ)} {a✝ : ℕ} {h1 : OSequence.length ⟨κ :: σ, o⟩ = a✝} {b : Agent} {o' : maxOne (Call.cor b κ :: σ)} {h2 : OSequence.length ⟨Call.cor b κ :: σ, o'⟩ = a✝} (not_in_call : roleOfIn a κ = Role.Other) : equiv a (S, ⟨⟨κ :: σ, o⟩, h1⟩) (S, ⟨⟨Call.cor b κ :: σ, o'⟩, h2⟩)

@[simp]

theorem Error.cor_errFree_id {n : ℕ} (b : Agent) (σ : Sequence) (h : errFree σ) : cor b σ = σ

If σ is error-free, then cor b σ = σ.