[STATEMENT]
lemma ladder_cut_prefix_i: 
  assumes index_bound: "index < length L"
  assumes length_L: "length L > 0"
  shows "ladder_i (ladder_cut_prefix d L) index = ladder_i L index - d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ladder_i (ladder_cut_prefix d L) index = ladder_i L index - d
[PROOF STEP]
apply (simp add: ladder_i_def ladder_cut_prefix_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (index = 0 \<longrightarrow> deriv_i (hd ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)])) = deriv_i (hd L) - d) \<and> (0 < index \<longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)]) (index - Suc 0) = ladder_j L (index - Suc 0) - d)
[PROOF STEP]
apply (cases index)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. index = 0 \<Longrightarrow> (index = 0 \<longrightarrow> deriv_i (hd ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)])) = deriv_i (hd L) - d) \<and> (0 < index \<longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)]) (index - Suc 0) = ladder_j L (index - Suc 0) - d)
 2. \<And>nat. index = Suc nat \<Longrightarrow> (index = 0 \<longrightarrow> deriv_i (hd ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)])) = deriv_i (hd L) - d) \<and> (0 < index \<longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)]) (index - Suc 0) = ladder_j L (index - Suc 0) - d)
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. index = 0 \<Longrightarrow> deriv_i (hd ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)])) = deriv_i (hd L) - d
 2. \<And>nat. index = Suc nat \<Longrightarrow> (index = 0 \<longrightarrow> deriv_i (hd ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)])) = deriv_i (hd L) - d) \<and> (0 < index \<longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)]) (index - Suc 0) = ladder_j L (index - Suc 0) - d)
[PROOF STEP]
apply (subst hd_0_subst)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. index = 0 \<Longrightarrow> 0 < length (ladder_shift_j d L)
 2. index = 0 \<Longrightarrow> deriv_i (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d) = deriv_i (hd L) - d
 3. \<And>nat. index = Suc nat \<Longrightarrow> (index = 0 \<longrightarrow> deriv_i (hd ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)])) = deriv_i (hd L) - d) \<and> (0 < index \<longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)]) (index - Suc 0) = ladder_j L (index - Suc 0) - d)
[PROOF STEP]
using length_L ladder_shift_j_length
[PROOF STATE]
proof (prove)
using this:
0 < length L
length (ladder_shift_j ?d ?L) = length ?L

goal (3 subgoals):
 1. index = 0 \<Longrightarrow> 0 < length (ladder_shift_j d L)
 2. index = 0 \<Longrightarrow> deriv_i (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d) = deriv_i (hd L) - d
 3. \<And>nat. index = Suc nat \<Longrightarrow> (index = 0 \<longrightarrow> deriv_i (hd ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)])) = deriv_i (hd L) - d) \<and> (0 < index \<longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)]) (index - Suc 0) = ladder_j L (index - Suc 0) - d)
[PROOF STEP]
apply metis
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. index = 0 \<Longrightarrow> deriv_i (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d) = deriv_i (hd L) - d
 2. \<And>nat. index = Suc nat \<Longrightarrow> (index = 0 \<longrightarrow> deriv_i (hd ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)])) = deriv_i (hd L) - d) \<and> (0 < index \<longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)]) (index - Suc 0) = ladder_j L (index - Suc 0) - d)
[PROOF STEP]
apply (auto simp add: deriv_i_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. index = Suc nat \<Longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, snd (snd (hd L)) - d)]) nat = ladder_j L nat - d
[PROOF STEP]
apply (case_tac nat)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>nat. \<lbrakk>index = Suc nat; nat = 0\<rbrakk> \<Longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, snd (snd (hd L)) - d)]) nat = ladder_j L nat - d
 2. \<And>nat nata. \<lbrakk>index = Suc nat; nat = Suc nata\<rbrakk> \<Longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, snd (snd (hd L)) - d)]) nat = ladder_j L nat - d
[PROOF STEP]
apply (simp add: ladder_j_def deriv_j_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>nat. \<lbrakk>index = Suc 0; nat = 0\<rbrakk> \<Longrightarrow> fst (snd ((ladder_shift_j d L)[0 := (ladder_n L 0, fst (snd (L ! 0)) - d, snd (snd (hd L)) - d)] ! 0)) = fst (snd (L ! 0)) - d
 2. \<And>nat nata. \<lbrakk>index = Suc nat; nat = Suc nata\<rbrakk> \<Longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, snd (snd (hd L)) - d)]) nat = ladder_j L nat - d
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. index = Suc 0 \<Longrightarrow> fst (snd ((ladder_shift_j d L)[0 := (ladder_n L 0, fst (snd (L ! 0)) - d, snd (snd (hd L)) - d)] ! 0)) = fst (snd (L ! 0)) - d
 2. \<And>nata. index = Suc (Suc nata) \<Longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, snd (snd (hd L)) - d)]) (Suc nata) = ladder_j L (Suc nata) - d
[PROOF STEP]
apply (subst nth_list_update_eq)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. index = Suc 0 \<Longrightarrow> 0 < length (ladder_shift_j d L)
 2. index = Suc 0 \<Longrightarrow> fst (snd (ladder_n L 0, fst (snd (L ! 0)) - d, snd (snd (hd L)) - d)) = fst (snd (L ! 0)) - d
 3. \<And>nata. index = Suc (Suc nata) \<Longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, snd (snd (hd L)) - d)]) (Suc nata) = ladder_j L (Suc nata) - d
[PROOF STEP]
using length_L ladder_shift_j_length
[PROOF STATE]
proof (prove)
using this:
0 < length L
length (ladder_shift_j ?d ?L) = length ?L

goal (3 subgoals):
 1. index = Suc 0 \<Longrightarrow> 0 < length (ladder_shift_j d L)
 2. index = Suc 0 \<Longrightarrow> fst (snd (ladder_n L 0, fst (snd (L ! 0)) - d, snd (snd (hd L)) - d)) = fst (snd (L ! 0)) - d
 3. \<And>nata. index = Suc (Suc nata) \<Longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, snd (snd (hd L)) - d)]) (Suc nata) = ladder_j L (Suc nata) - d
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. index = Suc 0 \<Longrightarrow> fst (snd (ladder_n L 0, fst (snd (L ! 0)) - d, snd (snd (hd L)) - d)) = fst (snd (L ! 0)) - d
 2. \<And>nata. index = Suc (Suc nata) \<Longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, snd (snd (hd L)) - d)]) (Suc nata) = ladder_j L (Suc nata) - d
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nata. index = Suc (Suc nata) \<Longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, snd (snd (hd L)) - d)]) (Suc nata) = ladder_j L (Suc nata) - d
[PROOF STEP]
apply (simp add: ladder_j_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nata. index = Suc (Suc nata) \<Longrightarrow> deriv_j (ladder_shift_j d L ! Suc nata) = deriv_j (L ! Suc nata) - d
[PROOF STEP]
apply (subst deriv_j_ladder_shift_j)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>nata. index = Suc (Suc nata) \<Longrightarrow> Suc nata < length L
 2. \<And>nata. index = Suc (Suc nata) \<Longrightarrow> deriv_j (L ! Suc nata) - d = deriv_j (L ! Suc nata) - d
[PROOF STEP]
using index_bound
[PROOF STATE]
proof (prove)
using this:
index < length L

goal (2 subgoals):
 1. \<And>nata. index = Suc (Suc nata) \<Longrightarrow> Suc nata < length L
 2. \<And>nata. index = Suc (Suc nata) \<Longrightarrow> deriv_j (L ! Suc nata) - d = deriv_j (L ! Suc nata) - d
[PROOF STEP]
apply arith
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nata. index = Suc (Suc nata) \<Longrightarrow> deriv_j (L ! Suc nata) - d = deriv_j (L ! Suc nata) - d
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done