[STATEMENT]
lemma set_der_stack_lt: "k \<in> set (der_stack i\<^sub>0) \<Longrightarrow> k<i\<^sub>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<in> set (local.der_stack i\<^sub>0) \<Longrightarrow> k < i\<^sub>0
[PROOF STEP]
apply (induction i\<^sub>0 rule: der_stack.induct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<lbrakk>local.has_left i; k \<in> set (local.der_stack (local.the_left i))\<rbrakk> \<Longrightarrow> k < local.the_left i; k \<in> set (local.der_stack i)\<rbrakk> \<Longrightarrow> k < i
[PROOF STEP]
apply (subst (asm) der_stack.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<lbrakk>local.has_left i; k \<in> set (local.der_stack (local.the_left i))\<rbrakk> \<Longrightarrow> k < local.the_left i; k \<in> set (if local.has_left i then local.the_left i # local.der_stack (local.the_left i) else [])\<rbrakk> \<Longrightarrow> k < i
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>k < local.the_left i; local.has_left i; k \<in> set (local.der_stack (local.the_left i))\<rbrakk> \<Longrightarrow> k < i
[PROOF STEP]
using less_trans the_leftI
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x < ?y; ?y < ?z\<rbrakk> \<Longrightarrow> ?x < ?z
local.has_left ?j \<Longrightarrow> local.the_left ?j < ?j \<and> xs ! local.the_left ?j < xs ! ?j

goal (1 subgoal):
 1. \<And>i. \<lbrakk>k < local.the_left i; local.has_left i; k \<in> set (local.der_stack (local.the_left i))\<rbrakk> \<Longrightarrow> k < i
[PROOF STEP]
by blast