[STATEMENT]
lemma c_tl_aux3: "c_tl u = (sgn1 ((c_len u) - 1))*((c_pair (c_len u - (2::nat)) (c_snd (c_snd (u-(1::nat))))) + 1)" (is "_ = ?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
have S1: "u=0 \<Longrightarrow> ?thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u = 0 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
u = 0 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)

goal (1 subgoal):
 1. c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
have S2: "u>0 \<Longrightarrow> ?thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < u \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < u \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
assume A1: "u>0"
[PROOF STATE]
proof (state)
this:
0 < u

goal (1 subgoal):
 1. 0 < u \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
have S2_1: "c_len u = 1 \<Longrightarrow> ?thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_len u = 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
by (simp add: c_tl_aux1)
[PROOF STATE]
proof (state)
this:
c_len u = 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)

goal (1 subgoal):
 1. 0 < u \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
have S2_2: "c_len u \<noteq> 1 \<Longrightarrow> ?thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_len u \<noteq> 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c_len u \<noteq> 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
assume A2_2_1: "c_len u \<noteq> 1"
[PROOF STATE]
proof (state)
this:
c_len u \<noteq> 1

goal (1 subgoal):
 1. c_len u \<noteq> 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
from A1
[PROOF STATE]
proof (chain)
picking this:
0 < u
[PROOF STEP]
have S2_2_1: "c_len u > 0"
[PROOF STATE]
proof (prove)
using this:
0 < u

goal (1 subgoal):
 1. 0 < c_len u
[PROOF STEP]
by (rule c_len_3)
[PROOF STATE]
proof (state)
this:
0 < c_len u

goal (1 subgoal):
 1. c_len u \<noteq> 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
from A2_2_1 S2_2_1
[PROOF STATE]
proof (chain)
picking this:
c_len u \<noteq> 1
0 < c_len u
[PROOF STEP]
have S2_2_2: "c_len u > 1"
[PROOF STATE]
proof (prove)
using this:
c_len u \<noteq> 1
0 < c_len u

goal (1 subgoal):
 1. 1 < c_len u
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
1 < c_len u

goal (1 subgoal):
 1. c_len u \<noteq> 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
1 < c_len u
[PROOF STEP]
have S2_2_3: "c_len u - 1 > 0"
[PROOF STATE]
proof (prove)
using this:
1 < c_len u

goal (1 subgoal):
 1. 0 < c_len u - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < c_len u - 1

goal (1 subgoal):
 1. c_len u \<noteq> 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
0 < c_len u - 1
[PROOF STEP]
have S2_2_4: "sgn1 (c_len u - 1)=1"
[PROOF STATE]
proof (prove)
using this:
0 < c_len u - 1

goal (1 subgoal):
 1. sgn1 (c_len u - 1) = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sgn1 (c_len u - 1) = 1

goal (1 subgoal):
 1. c_len u \<noteq> 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
from S2_2_4
[PROOF STATE]
proof (chain)
picking this:
sgn1 (c_len u - 1) = 1
[PROOF STEP]
have S2_2_5: "?R = (c_pair (c_len u - (2::nat)) (c_snd (c_snd (u-(1::nat))))) + 1"
[PROOF STATE]
proof (prove)
using this:
sgn1 (c_len u - 1) = 1

goal (1 subgoal):
 1. sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1) = c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1) = c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1

goal (1 subgoal):
 1. c_len u \<noteq> 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
from S2_2_2
[PROOF STATE]
proof (chain)
picking this:
1 < c_len u
[PROOF STEP]
have S2_2_6: "c_tl u = (c_pair (c_len u - (2::nat)) (c_snd (c_snd (u-(1::nat))))) + 1"
[PROOF STATE]
proof (prove)
using this:
1 < c_len u

goal (1 subgoal):
 1. c_tl u = c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1
[PROOF STEP]
by (rule c_tl_aux2)
[PROOF STATE]
proof (state)
this:
c_tl u = c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1

goal (1 subgoal):
 1. c_len u \<noteq> 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
from S2_2_5 S2_2_6
[PROOF STATE]
proof (chain)
picking this:
sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1) = c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1
c_tl u = c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1) = c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1
c_tl u = c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1

goal (1 subgoal):
 1. c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
c_len u \<noteq> 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)

goal (1 subgoal):
 1. 0 < u \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
from S2_1 S2_2
[PROOF STATE]
proof (chain)
picking this:
c_len u = 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
c_len u \<noteq> 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c_len u = 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
c_len u \<noteq> 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)

goal (1 subgoal):
 1. c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < u \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)

goal (1 subgoal):
 1. c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
from S1 S2
[PROOF STATE]
proof (chain)
picking this:
u = 0 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
0 < u \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u = 0 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
0 < u \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)

goal (1 subgoal):
 1. c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)

goal:
No subgoals!
[PROOF STEP]
qed