[STATEMENT]
lemma tm_skip_first_arg_len_eq_1_cases: 
  fixes s::nat
  assumes "inv_tm_skip_first_arg_len_eq_1 n (s,l,r)"
    and "s=0 \<Longrightarrow> P"
    and "s=1 \<Longrightarrow> P"
    and "s=2 \<Longrightarrow> P"
    and "s=3 \<Longrightarrow> P"
    and "s=4 \<Longrightarrow> P"
    and "s=5 \<Longrightarrow> P"
  shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P
[PROOF STEP]
have "s < 6"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s < 6
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> s < 6 \<Longrightarrow> False
[PROOF STEP]
assume "\<not> s < 6"
[PROOF STATE]
proof (state)
this:
\<not> s < 6

goal (1 subgoal):
 1. \<not> s < 6 \<Longrightarrow> False
[PROOF STEP]
with \<open>inv_tm_skip_first_arg_len_eq_1 n (s,l,r)\<close>
[PROOF STATE]
proof (chain)
picking this:
inv_tm_skip_first_arg_len_eq_1 n (s, l, r)
\<not> s < 6
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
inv_tm_skip_first_arg_len_eq_1 n (s, l, r)
\<not> s < 6

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
s < 6

goal (1 subgoal):
 1. P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s < 6
[PROOF STEP]
have "s = 0 \<or> s = 1 \<or> s = 2 \<or> s = 3  \<or> s = 4 \<or> s = 5"
[PROOF STATE]
proof (prove)
using this:
s < 6

goal (1 subgoal):
 1. s = 0 \<or> s = 1 \<or> s = 2 \<or> s = 3 \<or> s = 4 \<or> s = 5
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s = 0 \<or> s = 1 \<or> s = 2 \<or> s = 3 \<or> s = 4 \<or> s = 5

goal (1 subgoal):
 1. P
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
inv_tm_skip_first_arg_len_eq_1 n (s, l, r)
s = 0 \<Longrightarrow> P
s = 1 \<Longrightarrow> P
s = 2 \<Longrightarrow> P
s = 3 \<Longrightarrow> P
s = 4 \<Longrightarrow> P
s = 5 \<Longrightarrow> P
s = 0 \<or> s = 1 \<or> s = 2 \<or> s = 3 \<or> s = 4 \<or> s = 5
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inv_tm_skip_first_arg_len_eq_1 n (s, l, r)
s = 0 \<Longrightarrow> P
s = 1 \<Longrightarrow> P
s = 2 \<Longrightarrow> P
s = 3 \<Longrightarrow> P
s = 4 \<Longrightarrow> P
s = 5 \<Longrightarrow> P
s = 0 \<or> s = 1 \<or> s = 2 \<or> s = 3 \<or> s = 4 \<or> s = 5

goal (1 subgoal):
 1. P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P

goal:
No subgoals!
[PROOF STEP]
qed