[STATEMENT]
lemma step_size_ok_3: "\<lbrakk>
  invar (States dir big small); 
  step (States dir big small) = States dir' big' small';
  remaining_steps (States dir big small) + 1 \<le> 4 * size small
\<rbrakk> \<Longrightarrow> remaining_steps (States dir' big' small') + 1 \<le> 4 * size small'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar (States dir big small); step (States dir big small) = States dir' big' small'; remaining_steps (States dir big small) + 1 \<le> 4 * size small\<rbrakk> \<Longrightarrow> remaining_steps (States dir' big' small') + 1 \<le> 4 * size small'
[PROOF STEP]
using remaining_steps_decline step_size_small
[PROOF STATE]
proof (prove)
using this:
invar ?states \<Longrightarrow> remaining_steps (step ?states) \<le> remaining_steps ?states
\<lbrakk>invar (States ?dir ?big ?small); step (States ?dir ?big ?small) = States ?dir' ?big' ?small'\<rbrakk> \<Longrightarrow> size ?small' = size ?small

goal (1 subgoal):
 1. \<lbrakk>invar (States dir big small); step (States dir big small) = States dir' big' small'; remaining_steps (States dir big small) + 1 \<le> 4 * size small\<rbrakk> \<Longrightarrow> remaining_steps (States dir' big' small') + 1 \<le> 4 * size small'
[PROOF STEP]
by (metis Suc_eq_plus1 Suc_le_mono le_trans)