# Theory Three_Steps

```(*<*)
theory Three_Steps
imports "../Consensus_Misc"
begin
(*>*)
subsection ‹Step definitions for 3-step algorithms›

abbreviation (input) "nr_steps ≡ 3"

definition three_phase where "three_phase (r::nat) ≡ r div nr_steps"

definition three_step where "three_step (r::nat) ≡ r mod nr_steps"

lemma three_phase_zero [simp]: "three_phase 0 = 0"

lemma three_step_zero [simp]: "three_step 0 = 0"

lemma three_phase_step: "(three_phase r * nr_steps) + three_step r = r"
by (auto simp add: three_phase_def three_step_def)

lemma three_step_Suc:
"three_step r = 0 ⟹ three_step (Suc (Suc r)) = 2"
"three_step r = 0 ⟹ three_step (Suc r) = 1"
"three_step r = (Suc 0) ⟹ three_step (Suc r) = 2"
"three_step r = (Suc 0) ⟹ three_step (Suc (Suc r)) = 0"
"three_step r = (Suc (Suc 0)) ⟹ three_step ((Suc r)) = 0"

lemma three_step_phase_Suc:
"three_step r = 0 ⟹ three_phase (Suc r) = three_phase r"
"three_step r = 0 ⟹ three_phase (Suc (Suc r)) = three_phase r"
"three_step r = 0 ⟹ three_phase (Suc (Suc (Suc r))) = Suc (three_phase r)"
"three_step r = (Suc 0) ⟹ three_phase (Suc r) = three_phase r"
"three_step r = (Suc 0) ⟹ three_phase (Suc (Suc r)) = Suc (three_phase r)"
"three_step r = (Suc (Suc 0)) ⟹ three_phase (Suc r) = Suc (three_phase r)"
by(simp_all add: three_step_def three_phase_def mod_Suc div_Suc)

lemma three_step2_phase_Suc:
"three_step r = 2 ⟹ (3 * (Suc (three_phase r)) - 1) = r"