[STATEMENT]
lemma prod_decode_triangle_add: "prod_decode (triangle k + m) = prod_decode_aux k m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_decode (triangle k + m) = prod_decode_aux k m
[PROOF STEP]
proof (induct k arbitrary: m)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m. prod_decode (triangle 0 + m) = prod_decode_aux 0 m
 2. \<And>k m. (\<And>m. prod_decode (triangle k + m) = prod_decode_aux k m) \<Longrightarrow> prod_decode (triangle (Suc k) + m) = prod_decode_aux (Suc k) m
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:


goal (2 subgoals):
 1. \<And>m. prod_decode (triangle 0 + m) = prod_decode_aux 0 m
 2. \<And>k m. (\<And>m. prod_decode (triangle k + m) = prod_decode_aux k m) \<Longrightarrow> prod_decode (triangle (Suc k) + m) = prod_decode_aux (Suc k) m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_decode (triangle 0 + m) = prod_decode_aux 0 m
[PROOF STEP]
by (simp add: prod_decode_def)
[PROOF STATE]
proof (state)
this:
prod_decode (triangle 0 + m) = prod_decode_aux 0 m

goal (1 subgoal):
 1. \<And>k m. (\<And>m. prod_decode (triangle k + m) = prod_decode_aux k m) \<Longrightarrow> prod_decode (triangle (Suc k) + m) = prod_decode_aux (Suc k) m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k m. (\<And>m. prod_decode (triangle k + m) = prod_decode_aux k m) \<Longrightarrow> prod_decode (triangle (Suc k) + m) = prod_decode_aux (Suc k) m
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
prod_decode (triangle k + ?m) = prod_decode_aux k ?m

goal (1 subgoal):
 1. \<And>k m. (\<And>m. prod_decode (triangle k + m) = prod_decode_aux k m) \<Longrightarrow> prod_decode (triangle (Suc k) + m) = prod_decode_aux (Suc k) m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prod_decode (triangle k + ?m) = prod_decode_aux k ?m
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
prod_decode (triangle k + ?m) = prod_decode_aux k ?m

goal (1 subgoal):
 1. prod_decode (triangle (Suc k) + m) = prod_decode_aux (Suc k) m
[PROOF STEP]
by (metis ab_semigroup_add_class.add_ac(1) add_diff_cancel_left' le_add1 not_less_eq_eq prod_decode_aux.simps triangle_Suc)
[PROOF STATE]
proof (state)
this:
prod_decode (triangle (Suc k) + m) = prod_decode_aux (Suc k) m

goal:
No subgoals!
[PROOF STEP]
qed