[STATEMENT]
lemma word_rec_max:
  assumes "\<forall>m\<ge>n. m \<noteq> - 1 \<longrightarrow> f m = id"
  shows "word_rec z f (- 1) = word_rec z f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_rec z f (- 1) = word_rec z f n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. word_rec z f (- 1) = word_rec z f n
[PROOF STEP]
have \<section>: "\<And>m. \<lbrakk>m < - 1 - n\<rbrakk> \<Longrightarrow> (f \<circ> (+) n) m = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m. m < - 1 - n \<Longrightarrow> (f \<circ> (+) n) m = id
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<ge>n. m \<noteq> - 1 \<longrightarrow> f m = id

goal (1 subgoal):
 1. \<And>m. m < - 1 - n \<Longrightarrow> (f \<circ> (+) n) m = id
[PROOF STEP]
by (metis (mono_tags, lifting) add.commute add_diff_cancel_left' comp_apply less_le olen_add_eqv plus_minus_no_overflow word_n1_ge)
[PROOF STATE]
proof (state)
this:
?m < - 1 - n \<Longrightarrow> (f \<circ> (+) n) ?m = id

goal (1 subgoal):
 1. word_rec z f (- 1) = word_rec z f n
[PROOF STEP]
have "word_rec z f (- 1) = word_rec (word_rec z f (- 1 - (- 1 - n))) (f \<circ> (+) (- 1 - (- 1 - n))) (- 1 - n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_rec z f (- 1) = word_rec (word_rec z f (- 1 - (- 1 - n))) (f \<circ> (+) (- 1 - (- 1 - n))) (- 1 - n)
[PROOF STEP]
by (meson word_n1_ge word_rec_twice)
[PROOF STATE]
proof (state)
this:
word_rec z f (- 1) = word_rec (word_rec z f (- 1 - (- 1 - n))) (f \<circ> (+) (- 1 - (- 1 - n))) (- 1 - n)

goal (1 subgoal):
 1. word_rec z f (- 1) = word_rec z f n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
word_rec z f (- 1) = word_rec (word_rec z f (- 1 - (- 1 - n))) (f \<circ> (+) (- 1 - (- 1 - n))) (- 1 - n)

goal (1 subgoal):
 1. word_rec z f (- 1) = word_rec z f n
[PROOF STEP]
have "... = word_rec z f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_rec (word_rec z f (- 1 - (- 1 - n))) (f \<circ> (+) (- 1 - (- 1 - n))) (- 1 - n) = word_rec z f n
[PROOF STEP]
by (metis (no_types, lifting) \<section> diff_add_cancel minus_diff_eq uminus_add_conv_diff word_rec_id_eq)
[PROOF STATE]
proof (state)
this:
word_rec (word_rec z f (- 1 - (- 1 - n))) (f \<circ> (+) (- 1 - (- 1 - n))) (- 1 - n) = word_rec z f n

goal (1 subgoal):
 1. word_rec z f (- 1) = word_rec z f n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
word_rec z f (- 1) = word_rec z f n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
word_rec z f (- 1) = word_rec z f n

goal (1 subgoal):
 1. word_rec z f (- 1) = word_rec z f n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
word_rec z f (- 1) = word_rec z f n

goal:
No subgoals!
[PROOF STEP]
qed