# Theory Three_Steps

(*<*)
theory Three_Steps
imports
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]:

lemma three_step_zero [simp]:

lemma three_phase_step:
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 (Suc (Suc r))) = Suc (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"