[STATEMENT]
lemma att_elem_seq[rule_format]: "\<turnstile> x1 \<longrightarrow> (\<forall> x \<in> fst(attack x1).
                     (\<exists> y. y \<in> snd(attack x1) \<and> x \<rightarrow>\<^sub>i* y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile>x1 \<longrightarrow> (\<forall>x\<in>fst (attack x1). \<exists>y. y \<in> snd (attack x1) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
text \<open>First attack tree induction\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile>x1 \<longrightarrow> (\<forall>x\<in>fst (attack x1). \<exists>y. y \<in> snd (attack x1) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
proof (induction x1)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. \<turnstile>\<N>\<^bsub>x\<^esub> \<longrightarrow> (\<forall>xa\<in>fst (attack \<N>\<^bsub>x\<^esub>). \<exists>y. y \<in> snd (attack \<N>\<^bsub>x\<^esub>) \<and> xa \<rightarrow>\<^sub>i* y)
 2. \<And>x1a x2. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<turnstile>x1a \<oplus>\<^sub>\<and>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (x1a \<oplus>\<^sub>\<and>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<and>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)
 3. \<And>x1a x2. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<turnstile>x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
case (BaseAttack x)
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>x. \<turnstile>\<N>\<^bsub>x\<^esub> \<longrightarrow> (\<forall>xa\<in>fst (attack \<N>\<^bsub>x\<^esub>). \<exists>y. y \<in> snd (attack \<N>\<^bsub>x\<^esub>) \<and> xa \<rightarrow>\<^sub>i* y)
 2. \<And>x1a x2. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<turnstile>x1a \<oplus>\<^sub>\<and>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (x1a \<oplus>\<^sub>\<and>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<and>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)
 3. \<And>x1a x2. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<turnstile>x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile>\<N>\<^bsub>x\<^esub> \<longrightarrow> (\<forall>xa\<in>fst (attack \<N>\<^bsub>x\<^esub>). \<exists>y. y \<in> snd (attack \<N>\<^bsub>x\<^esub>) \<and> xa \<rightarrow>\<^sub>i* y)
[PROOF STEP]
by (metis AT.att_base EF_step EF_step_star_rev attack.simps(1))
[PROOF STATE]
proof (state)
this:
\<turnstile>\<N>\<^bsub>x\<^esub> \<longrightarrow> (\<forall>xa\<in>fst (attack \<N>\<^bsub>x\<^esub>). \<exists>y. y \<in> snd (attack \<N>\<^bsub>x\<^esub>) \<and> xa \<rightarrow>\<^sub>i* y)

goal (2 subgoals):
 1. \<And>x1a x2. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<turnstile>x1a \<oplus>\<^sub>\<and>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (x1a \<oplus>\<^sub>\<and>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<and>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)
 2. \<And>x1a x2. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<turnstile>x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1a x2. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<turnstile>x1a \<oplus>\<^sub>\<and>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (x1a \<oplus>\<^sub>\<and>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<and>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)
 2. \<And>x1a x2. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<turnstile>x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
case (AndAttack x1a x2)
[PROOF STATE]
proof (state)
this:
?x1aa \<in> set x1a \<Longrightarrow> \<turnstile>?x1aa \<longrightarrow> (\<forall>x\<in>fst (attack ?x1aa). \<exists>y. y \<in> snd (attack ?x1aa) \<and> x \<rightarrow>\<^sub>i* y)

goal (2 subgoals):
 1. \<And>x1a x2. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<turnstile>x1a \<oplus>\<^sub>\<and>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (x1a \<oplus>\<^sub>\<and>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<and>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)
 2. \<And>x1a x2. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<turnstile>x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x1aa \<in> set x1a \<Longrightarrow> \<turnstile>?x1aa \<longrightarrow> (\<forall>x\<in>fst (attack ?x1aa). \<exists>y. y \<in> snd (attack ?x1aa) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?x1aa \<in> set x1a \<Longrightarrow> \<turnstile>?x1aa \<longrightarrow> (\<forall>x\<in>fst (attack ?x1aa). \<exists>y. y \<in> snd (attack ?x1aa) \<and> x \<rightarrow>\<^sub>i* y)

goal (1 subgoal):
 1. \<turnstile>x1a \<oplus>\<^sub>\<and>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (x1a \<oplus>\<^sub>\<and>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<and>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
apply (rule_tac x = x2 in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<forall>x. \<turnstile>x1a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x1a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y)
[PROOF STEP]
apply (subgoal_tac "(\<forall> x1aa::'a attree.
                              x1aa \<in> set x1a \<longrightarrow>
                               \<turnstile>x1aa \<longrightarrow>
                               (\<forall>x::'a\<in>fst (attack x1aa). \<exists>y::'a. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)\<rbrakk> \<Longrightarrow> \<forall>x. \<turnstile>x1a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x1a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y)
 2. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
apply (rule mp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)\<rbrakk> \<Longrightarrow> ?P4 \<longrightarrow> (\<forall>x. \<turnstile>x1a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x1a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y))
 2. \<lbrakk>\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)\<rbrakk> \<Longrightarrow> ?P4
 3. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)\<rbrakk> \<Longrightarrow> ?P4
 2. \<lbrakk>\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)\<rbrakk> \<Longrightarrow> ?P4 \<longrightarrow> (\<forall>x. \<turnstile>x1a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x1a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y))
 3. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
apply (rotate_tac -1)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)\<rbrakk> \<Longrightarrow> ?P4
 2. \<lbrakk>\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)\<rbrakk> \<Longrightarrow> ?P4 \<longrightarrow> (\<forall>x. \<turnstile>x1a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x1a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y))
 3. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)\<rbrakk> \<Longrightarrow> (\<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>x1a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x1a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y))
 2. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
text \<open>Induction for @{text \<open>\<and>\<close>}: the manual instantiation seems tedious but in the @{text \<open>\<and>\<close>}
            case necessary to get the right induction hypothesis.\<close>
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)\<rbrakk> \<Longrightarrow> (\<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>x1a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x1a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y))
 2. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
proof (rule_tac list = "x1a" in list.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)\<rbrakk> \<Longrightarrow> (\<forall>x1aa. x1aa \<in> set [] \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>[] \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack ([] \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack ([] \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y))
 2. \<And>x1 x2. \<lbrakk>\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); (\<forall>x1aa. x1aa \<in> set x2 \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y))\<rbrakk> \<Longrightarrow> (\<forall>x1aa. x1aa \<in> set (x1 # x2) \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>x1 # x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x1 # x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x1 # x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y))
 3. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
text \<open>The @{text \<open>\<and>\<close>} induction empty case\<close>
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)\<rbrakk> \<Longrightarrow> (\<forall>x1aa. x1aa \<in> set [] \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>[] \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack ([] \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack ([] \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y))
 2. \<And>x1 x2. \<lbrakk>\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); (\<forall>x1aa. x1aa \<in> set x2 \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y))\<rbrakk> \<Longrightarrow> (\<forall>x1aa. x1aa \<in> set (x1 # x2) \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>x1 # x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x1 # x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x1 # x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y))
 3. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
show "(\<forall>x1aa::'a attree.
           x1aa \<in> set [] \<longrightarrow>
           \<turnstile>x1aa \<longrightarrow> (\<forall>x::'a\<in>fst (attack x1aa). \<exists>y::'a. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow>
       (\<forall>x::'a set \<times> 'a set.
           \<turnstile>([] \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>) \<longrightarrow>
           (\<forall>xa::'a\<in>fst (attack ([] \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y::'a. y \<in> snd (attack ([] \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x1aa. x1aa \<in> set [] \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>[] \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack ([] \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack ([] \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y))
[PROOF STEP]
using att_and_empty state_transition_refl_def
[PROOF STATE]
proof (prove)
using this:
\<turnstile>[] \<oplus>\<^sub>\<and>\<^bsup>(?s', ?s'')\<^esup> \<Longrightarrow> ?s' \<subseteq> ?s''
?s \<rightarrow>\<^sub>i* ?s' \<equiv> (?s, ?s') \<in> {(x, y). x \<rightarrow>\<^sub>i y}\<^sup>*

goal (1 subgoal):
 1. (\<forall>x1aa. x1aa \<in> set [] \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>[] \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack ([] \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack ([] \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(\<forall>x1aa. x1aa \<in> set [] \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>[] \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack ([] \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack ([] \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y))

goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); (\<forall>x1aa. x1aa \<in> set x2 \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y))\<rbrakk> \<Longrightarrow> (\<forall>x1aa. x1aa \<in> set (x1 # x2) \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>x1 # x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x1 # x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x1 # x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y))
 2. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
text \<open>The @{text \<open>\<and>\<close>} induction case nonempty\<close>
[PROOF STATE]
proof (state)
this:
(\<forall>x1aa. x1aa \<in> set [] \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>[] \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack ([] \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack ([] \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y))

goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); (\<forall>x1aa. x1aa \<in> set x2 \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y))\<rbrakk> \<Longrightarrow> (\<forall>x1aa. x1aa \<in> set (x1 # x2) \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>x1 # x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x1 # x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x1 # x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y))
 2. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); (\<forall>x1aa. x1aa \<in> set x2 \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y))\<rbrakk> \<Longrightarrow> (\<forall>x1aa. x1aa \<in> set (x1 # x2) \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>x1 # x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x1 # x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x1 # x2 \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y))
 2. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
show "\<And>(x1a::'a attree list) (x2::'a set \<times> 'a set) (x1::'a attree) (x2a::'a attree list).
       (\<And>x1aa::'a attree.
           (x1aa \<in> set x1a) \<Longrightarrow>
           ((\<turnstile>x1aa) \<longrightarrow> (\<forall>x::'a\<in>fst (attack x1aa). \<exists>y::'a. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y))) \<Longrightarrow>
       \<forall>x1aa::'a attree.
          (x1aa \<in> set x1a) \<longrightarrow>
          (\<turnstile>x1aa) \<longrightarrow> ((\<forall>x::'a\<in>fst (attack x1aa). \<exists>y::'a. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow>
       (\<forall>x1aa::'a attree.
           (x1aa \<in> set x2a) \<longrightarrow>
           (\<turnstile>x1aa) \<longrightarrow> (\<forall>x::'a\<in>fst (attack x1aa). \<exists>y::'a. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow>
       (\<forall>x::'a set \<times> 'a set.
           (\<turnstile>(x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<longrightarrow>
           ((\<forall>xa::'a\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y::'a. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y))) \<Longrightarrow>
       ((\<forall>x1aa::'a attree.
           (x1aa \<in> set (x1 # x2a)) \<longrightarrow>
           (\<turnstile>x1aa) \<longrightarrow> ((\<forall>x::'a\<in>fst (attack x1aa). \<exists>y::'a. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y))) \<longrightarrow>
       (\<forall>x::'a set \<times> 'a set.
          ( \<turnstile>(x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<longrightarrow>
           (\<forall>xa::'a\<in>fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)).
               (\<exists>y::'a. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> (xa \<rightarrow>\<^sub>i* y)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a. \<lbrakk>\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); (\<forall>x1aa. x1aa \<in> set x2a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y))\<rbrakk> \<Longrightarrow> (\<forall>x1aa. x1aa \<in> set (x1 # x2a) \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y))
[PROOF STEP]
apply (rule impI, rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a x. \<lbrakk>\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); (\<forall>x1aa. x1aa \<in> set x2a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y)); \<forall>x1aa. x1aa \<in> set (x1 # x2a) \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>\<rbrakk> \<Longrightarrow> \<forall>xa\<in>fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
text \<open>Set free the Induction Hypothesis: this is necessary to provide the grounds for specific
              instantiations in the step.\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a x. \<lbrakk>\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); (\<forall>x1aa. x1aa \<in> set x2a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y)); \<forall>x1aa. x1aa \<in> set (x1 # x2a) \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>\<rbrakk> \<Longrightarrow> \<forall>xa\<in>fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
apply (subgoal_tac "(\<forall>x::'a set \<times> 'a set.
                             \<turnstile>(x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>) \<longrightarrow>
                             (\<forall>xa::'a\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)).
                              \<exists>y::'a. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1a x2 x1 x2a x. \<lbrakk>\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); (\<forall>x1aa. x1aa \<in> set x2a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y)); \<forall>x1aa. x1aa \<in> set (x1 # x2a) \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; \<forall>x. \<turnstile>x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y)\<rbrakk> \<Longrightarrow> \<forall>xa\<in>fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
 2. \<And>x1a x2 x1 x2a x. \<lbrakk>\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); (\<forall>x1aa. x1aa \<in> set x2a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y)); \<forall>x1aa. x1aa \<in> set (x1 # x2a) \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>\<rbrakk> \<Longrightarrow> \<forall>x. \<turnstile>x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1a x2 x1 x2a x. \<lbrakk>\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); (\<forall>x1aa. x1aa \<in> set x2a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y)); \<forall>x1aa. x1aa \<in> set (x1 # x2a) \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>\<rbrakk> \<Longrightarrow> \<forall>x. \<turnstile>x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y)
 2. \<And>x1a x2 x1 x2a x. \<lbrakk>\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); (\<forall>x1aa. x1aa \<in> set x2a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y)); \<forall>x1aa. x1aa \<in> set (x1 # x2a) \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; \<forall>x. \<turnstile>x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y)\<rbrakk> \<Longrightarrow> \<forall>xa\<in>fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a x. \<lbrakk>\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); (\<forall>x1aa. x1aa \<in> set x2a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y)); \<forall>x1aa. x1aa \<in> set (x1 # x2a) \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; \<forall>x. \<turnstile>x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y)\<rbrakk> \<Longrightarrow> \<forall>xa\<in>fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
text \<open>The following induction step for @{text \<open>\<and>\<close>} needs a number of manual instantiations
              so that the proof is not found automatically. In the subsequent case for @{text \<open>\<or>\<close>},
              sledgehammer finds the proof.\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a x. \<lbrakk>\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); (\<forall>x1aa. x1aa \<in> set x2a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y)); \<forall>x1aa. x1aa \<in> set (x1 # x2a) \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; \<forall>x. \<turnstile>x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y)\<rbrakk> \<Longrightarrow> \<forall>xa\<in>fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a x. \<lbrakk>\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); (\<forall>x1aa. x1aa \<in> set x2a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y)); \<forall>x1aa. x1aa \<in> set (x1 # x2a) \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; \<forall>x. \<turnstile>x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y)\<rbrakk> \<Longrightarrow> \<forall>xa\<in>fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
show "\<And>(x1a::'a attree list) (x2::'a set \<times> 'a set) (x1::'a attree) (x2a::'a attree list) x::'a set \<times> 'a set.
       \<forall>x1aa::'a attree.
          x1aa \<in> set (x1 # x2a) \<longrightarrow>
          \<turnstile>x1aa \<longrightarrow> (\<forall>x::'a\<in>fst (attack x1aa). \<exists>y::'a. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y) \<Longrightarrow>
       \<turnstile>(x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>) \<Longrightarrow>
       \<forall>x::'a set \<times> 'a set.
          \<turnstile>(x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>) \<longrightarrow>
          (\<forall>xa::'a\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y::'a. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y) \<Longrightarrow>
       \<forall>xa::'a\<in>fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y::'a. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a x. \<lbrakk>\<forall>x1aa. x1aa \<in> set (x1 # x2a) \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; \<forall>x. \<turnstile>x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y)\<rbrakk> \<Longrightarrow> \<forall>xa\<in>fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a x xa. \<lbrakk>\<forall>x1aa. x1aa \<in> set (x1 # x2a) \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; \<forall>x. \<turnstile>x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y); xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>))\<rbrakk> \<Longrightarrow> \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
apply (rename_tac xa)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a x xa. \<lbrakk>\<forall>x1aa. x1aa \<in> set (x1 # x2a) \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; \<forall>x. \<turnstile>x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y); xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>))\<rbrakk> \<Longrightarrow> \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
text \<open>Prepare the steps\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a x xa. \<lbrakk>\<forall>x1aa. x1aa \<in> set (x1 # x2a) \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; \<forall>x. \<turnstile>x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y); xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>))\<rbrakk> \<Longrightarrow> \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
apply (drule_tac x = "(snd(attack x1), snd x)" in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a x xa. \<lbrakk>\<forall>x1aa. x1aa \<in> set (x1 # x2a) \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); \<turnstile>x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y)\<rbrakk> \<Longrightarrow> \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
apply (rotate_tac -1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a x xa. \<lbrakk>\<turnstile>x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y); \<forall>x1aa. x1aa \<in> set (x1 # x2a) \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>))\<rbrakk> \<Longrightarrow> \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
apply (erule impE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1a x2 x1 x2a x xa. \<lbrakk>\<forall>x1aa. x1aa \<in> set (x1 # x2a) \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>))\<rbrakk> \<Longrightarrow> \<turnstile>x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>
 2. \<And>x1a x2 x1 x2a x xa. \<lbrakk>\<forall>x1aa. x1aa \<in> set (x1 # x2a) \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); \<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y\<rbrakk> \<Longrightarrow> \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
apply (erule att_andD2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a x xa. \<lbrakk>\<forall>x1aa. x1aa \<in> set (x1 # x2a) \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); \<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y\<rbrakk> \<Longrightarrow> \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
text \<open>Premise for x1\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a x xa. \<lbrakk>\<forall>x1aa. x1aa \<in> set (x1 # x2a) \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); \<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y\<rbrakk> \<Longrightarrow> \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
apply (drule_tac x = x1 in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a x xa. \<lbrakk>\<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); \<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y; x1 \<in> set (x1 # x2a) \<longrightarrow> \<turnstile>x1 \<longrightarrow> (\<forall>x\<in>fst (attack x1). \<exists>y. y \<in> snd (attack x1) \<and> x \<rightarrow>\<^sub>i* y)\<rbrakk> \<Longrightarrow> \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
apply (drule mp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1a x2 x1 x2a x xa. \<lbrakk>\<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); \<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y\<rbrakk> \<Longrightarrow> x1 \<in> set (x1 # x2a)
 2. \<And>x1a x2 x1 x2a x xa. \<lbrakk>\<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); \<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y; \<turnstile>x1 \<longrightarrow> (\<forall>x\<in>fst (attack x1). \<exists>y. y \<in> snd (attack x1) \<and> x \<rightarrow>\<^sub>i* y)\<rbrakk> \<Longrightarrow> \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a x xa. \<lbrakk>\<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); \<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y; \<turnstile>x1 \<longrightarrow> (\<forall>x\<in>fst (attack x1). \<exists>y. y \<in> snd (attack x1) \<and> x \<rightarrow>\<^sub>i* y)\<rbrakk> \<Longrightarrow> \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
apply (drule mp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1a x2 x1 x2a x xa. \<lbrakk>\<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); \<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y\<rbrakk> \<Longrightarrow> \<turnstile>x1
 2. \<And>x1a x2 x1 x2a x xa. \<lbrakk>\<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); \<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y; \<forall>x\<in>fst (attack x1). \<exists>y. y \<in> snd (attack x1) \<and> x \<rightarrow>\<^sub>i* y\<rbrakk> \<Longrightarrow> \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
apply (erule att_andD1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a x xa. \<lbrakk>\<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); \<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y; \<forall>x\<in>fst (attack x1). \<exists>y. y \<in> snd (attack x1) \<and> x \<rightarrow>\<^sub>i* y\<rbrakk> \<Longrightarrow> \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
text \<open>Instantiate first step for xa\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a x xa. \<lbrakk>\<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); \<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y; \<forall>x\<in>fst (attack x1). \<exists>y. y \<in> snd (attack x1) \<and> x \<rightarrow>\<^sub>i* y\<rbrakk> \<Longrightarrow> \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
apply (rotate_tac -1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a x xa. \<lbrakk>\<forall>x\<in>fst (attack x1). \<exists>y. y \<in> snd (attack x1) \<and> x \<rightarrow>\<^sub>i* y; \<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); \<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y\<rbrakk> \<Longrightarrow> \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
apply (drule_tac x = xa in bspec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1a x2 x1 x2a x xa. \<lbrakk>\<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); \<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y\<rbrakk> \<Longrightarrow> xa \<in> fst (attack x1)
 2. \<And>x1a x2 x1 x2a x xa. \<lbrakk>\<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); \<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y; \<exists>y. y \<in> snd (attack x1) \<and> xa \<rightarrow>\<^sub>i* y\<rbrakk> \<Longrightarrow> \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
apply (erule att_and_fst_lem, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a x xa. \<lbrakk>\<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); \<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y; \<exists>y. y \<in> snd (attack x1) \<and> xa \<rightarrow>\<^sub>i* y\<rbrakk> \<Longrightarrow> \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
apply (erule exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a x xa y. \<lbrakk>\<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); \<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y; y \<in> snd (attack x1) \<and> xa \<rightarrow>\<^sub>i* y\<rbrakk> \<Longrightarrow> \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a x xa y. \<lbrakk>\<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); \<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y; y \<in> snd (attack x1); xa \<rightarrow>\<^sub>i* y\<rbrakk> \<Longrightarrow> \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
text \<open>Take this y and put it as first into the second part\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a x xa y. \<lbrakk>\<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); \<forall>xa\<in>fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)). \<exists>y. y \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y; y \<in> snd (attack x1); xa \<rightarrow>\<^sub>i* y\<rbrakk> \<Longrightarrow> \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
apply (drule_tac x = y in bspec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1a x2 x1 x2a x xa y. \<lbrakk>\<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); y \<in> snd (attack x1); xa \<rightarrow>\<^sub>i* y\<rbrakk> \<Longrightarrow> y \<in> fst (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>))
 2. \<And>x1a x2 x1 x2a x xa y. \<lbrakk>\<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); y \<in> snd (attack x1); xa \<rightarrow>\<^sub>i* y; \<exists>ya. ya \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)) \<and> y \<rightarrow>\<^sub>i* ya\<rbrakk> \<Longrightarrow> \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a x xa y. \<lbrakk>\<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); y \<in> snd (attack x1); xa \<rightarrow>\<^sub>i* y; \<exists>ya. ya \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)) \<and> y \<rightarrow>\<^sub>i* ya\<rbrakk> \<Longrightarrow> \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
apply (erule exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a x xa y ya. \<lbrakk>\<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); y \<in> snd (attack x1); xa \<rightarrow>\<^sub>i* y; ya \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)) \<and> y \<rightarrow>\<^sub>i* ya\<rbrakk> \<Longrightarrow> \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a x xa y ya. \<lbrakk>\<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); y \<in> snd (attack x1); xa \<rightarrow>\<^sub>i* y; ya \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)); y \<rightarrow>\<^sub>i* ya\<rbrakk> \<Longrightarrow> \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
text \<open>Bind the first @{text \<open>xa \<rightarrow>\<^sub>i* y\<close>} and second @{text \<open>y \<rightarrow>\<^sub>i* ya\<close>} together for solution\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a x xa y ya. \<lbrakk>\<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); y \<in> snd (attack x1); xa \<rightarrow>\<^sub>i* y; ya \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)); y \<rightarrow>\<^sub>i* ya\<rbrakk> \<Longrightarrow> \<exists>y. y \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y
[PROOF STEP]
apply (rule_tac x = ya in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a x xa y ya. \<lbrakk>\<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); y \<in> snd (attack x1); xa \<rightarrow>\<^sub>i* y; ya \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)); y \<rightarrow>\<^sub>i* ya\<rbrakk> \<Longrightarrow> ya \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* ya
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1a x2 x1 x2a x xa y ya. \<lbrakk>\<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); y \<in> snd (attack x1); xa \<rightarrow>\<^sub>i* y; ya \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)); y \<rightarrow>\<^sub>i* ya\<rbrakk> \<Longrightarrow> ya \<in> snd (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>))
 2. \<And>x1a x2 x1 x2a x xa y ya. \<lbrakk>\<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); y \<in> snd (attack x1); xa \<rightarrow>\<^sub>i* y; ya \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)); y \<rightarrow>\<^sub>i* ya\<rbrakk> \<Longrightarrow> xa \<rightarrow>\<^sub>i* ya
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x1 x2a x xa y ya. \<lbrakk>\<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>; xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)); y \<in> snd (attack x1); xa \<rightarrow>\<^sub>i* y; ya \<in> snd (attack (x2a \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd x)\<^esup>)); y \<rightarrow>\<^sub>i* ya\<rbrakk> \<Longrightarrow> xa \<rightarrow>\<^sub>i* ya
[PROOF STEP]
by (simp add: state_transition_refl_def)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>x1aa. x1aa \<in> set (?x1.0 # ?x2a) \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<turnstile>?x1.0 # ?x2a \<oplus>\<^sub>\<and>\<^bsup>?x\<^esup>; \<forall>x. \<turnstile>?x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (?x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (?x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y)\<rbrakk> \<Longrightarrow> \<forall>xa\<in>fst (attack (?x1.0 # ?x2a \<oplus>\<^sub>\<and>\<^bsup>?x\<^esup>)). \<exists>y. y \<in> snd (attack (?x1.0 # ?x2a \<oplus>\<^sub>\<and>\<^bsup>?x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>x1aa. x1aa \<in> set ?x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); \<forall>x1aa. x1aa \<in> set ?x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y); (\<forall>x1aa. x1aa \<in> set ?x2a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>?x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (?x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (?x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y))\<rbrakk> \<Longrightarrow> (\<forall>x1aa. x1aa \<in> set (?x1.0 # ?x2a) \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<longrightarrow> (\<forall>x. \<turnstile>?x1.0 # ?x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>xa\<in>fst (attack (?x1.0 # ?x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)). \<exists>y. y \<in> snd (attack (?x1.0 # ?x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<and> xa \<rightarrow>\<^sub>i* y))

goal (1 subgoal):
 1. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<forall>x1aa. x1aa \<in> set x1a \<longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
\<turnstile>x1a \<oplus>\<^sub>\<and>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (x1a \<oplus>\<^sub>\<and>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<and>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)

goal (1 subgoal):
 1. \<And>x1a x2. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<turnstile>x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1a x2. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<turnstile>x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
case (OrAttack x1a x2)
[PROOF STATE]
proof (state)
this:
?x1aa \<in> set x1a \<Longrightarrow> \<turnstile>?x1aa \<longrightarrow> (\<forall>x\<in>fst (attack ?x1aa). \<exists>y. y \<in> snd (attack ?x1aa) \<and> x \<rightarrow>\<^sub>i* y)

goal (1 subgoal):
 1. \<And>x1a x2. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<turnstile>x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x1aa \<in> set x1a \<Longrightarrow> \<turnstile>?x1aa \<longrightarrow> (\<forall>x\<in>fst (attack ?x1aa). \<exists>y. y \<in> snd (attack ?x1aa) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?x1aa \<in> set x1a \<Longrightarrow> \<turnstile>?x1aa \<longrightarrow> (\<forall>x\<in>fst (attack ?x1aa). \<exists>y. y \<in> snd (attack ?x1aa) \<and> x \<rightarrow>\<^sub>i* y)

goal (1 subgoal):
 1. \<turnstile>x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
proof (induction x1a arbitrary: x2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x2. (\<And>x1aa. x1aa \<in> set [] \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<turnstile>[] \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack ([] \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack ([] \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)
 2. \<And>a x1a x2. \<lbrakk>\<And>x2. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<turnstile>x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y); \<And>x1aa. x1aa \<in> set (a # x1a) \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)\<rbrakk> \<Longrightarrow> \<turnstile>a # x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (a # x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (a # x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
?x1aa \<in> set [] \<Longrightarrow> \<turnstile>?x1aa \<longrightarrow> (\<forall>x\<in>fst (attack ?x1aa). \<exists>y. y \<in> snd (attack ?x1aa) \<and> x \<rightarrow>\<^sub>i* y)

goal (2 subgoals):
 1. \<And>x2. (\<And>x1aa. x1aa \<in> set [] \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<turnstile>[] \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack ([] \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack ([] \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)
 2. \<And>a x1a x2. \<lbrakk>\<And>x2. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<turnstile>x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y); \<And>x1aa. x1aa \<in> set (a # x1a) \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)\<rbrakk> \<Longrightarrow> \<turnstile>a # x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (a # x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (a # x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x1aa \<in> set [] \<Longrightarrow> \<turnstile>?x1aa \<longrightarrow> (\<forall>x\<in>fst (attack ?x1aa). \<exists>y. y \<in> snd (attack ?x1aa) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?x1aa \<in> set [] \<Longrightarrow> \<turnstile>?x1aa \<longrightarrow> (\<forall>x\<in>fst (attack ?x1aa). \<exists>y. y \<in> snd (attack ?x1aa) \<and> x \<rightarrow>\<^sub>i* y)

goal (1 subgoal):
 1. \<turnstile>[] \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack ([] \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack ([] \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
by (metis EF_lem2a EF_step_star_rev att_or_empty attack.simps(3) subsetD surjective_pairing)
[PROOF STATE]
proof (state)
this:
\<turnstile>[] \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack ([] \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack ([] \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)

goal (1 subgoal):
 1. \<And>a x1a x2. \<lbrakk>\<And>x2. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<turnstile>x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y); \<And>x1aa. x1aa \<in> set (a # x1a) \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)\<rbrakk> \<Longrightarrow> \<turnstile>a # x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (a # x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (a # x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a x1a x2. \<lbrakk>\<And>x2. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<turnstile>x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y); \<And>x1aa. x1aa \<in> set (a # x1a) \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)\<rbrakk> \<Longrightarrow> \<turnstile>a # x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (a # x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (a # x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
case (Cons a x1a)
[PROOF STATE]
proof (state)
this:
(\<And>x1aaa. x1aaa \<in> set x1a \<Longrightarrow> \<turnstile>x1aaa \<longrightarrow> (\<forall>x\<in>fst (attack x1aaa). \<exists>y. y \<in> snd (attack x1aaa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<turnstile>x1a \<oplus>\<^sub>\<or>\<^bsup>?x2.0\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>?x2.0\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>?x2.0\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)
?x1aa \<in> set (a # x1a) \<Longrightarrow> \<turnstile>?x1aa \<longrightarrow> (\<forall>x\<in>fst (attack ?x1aa). \<exists>y. y \<in> snd (attack ?x1aa) \<and> x \<rightarrow>\<^sub>i* y)

goal (1 subgoal):
 1. \<And>a x1a x2. \<lbrakk>\<And>x2. (\<And>x1aa. x1aa \<in> set x1a \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<turnstile>x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y); \<And>x1aa. x1aa \<in> set (a # x1a) \<Longrightarrow> \<turnstile>x1aa \<longrightarrow> (\<forall>x\<in>fst (attack x1aa). \<exists>y. y \<in> snd (attack x1aa) \<and> x \<rightarrow>\<^sub>i* y)\<rbrakk> \<Longrightarrow> \<turnstile>a # x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (a # x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (a # x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<And>x1aaa. x1aaa \<in> set x1a \<Longrightarrow> \<turnstile>x1aaa \<longrightarrow> (\<forall>x\<in>fst (attack x1aaa). \<exists>y. y \<in> snd (attack x1aaa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<turnstile>x1a \<oplus>\<^sub>\<or>\<^bsup>?x2.0\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>?x2.0\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>?x2.0\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)
?x1aa \<in> set (a # x1a) \<Longrightarrow> \<turnstile>?x1aa \<longrightarrow> (\<forall>x\<in>fst (attack ?x1aa). \<exists>y. y \<in> snd (attack ?x1aa) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<And>x1aaa. x1aaa \<in> set x1a \<Longrightarrow> \<turnstile>x1aaa \<longrightarrow> (\<forall>x\<in>fst (attack x1aaa). \<exists>y. y \<in> snd (attack x1aaa) \<and> x \<rightarrow>\<^sub>i* y)) \<Longrightarrow> \<turnstile>x1a \<oplus>\<^sub>\<or>\<^bsup>?x2.0\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>?x2.0\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>?x2.0\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)
?x1aa \<in> set (a # x1a) \<Longrightarrow> \<turnstile>?x1aa \<longrightarrow> (\<forall>x\<in>fst (attack ?x1aa). \<exists>y. y \<in> snd (attack ?x1aa) \<and> x \<rightarrow>\<^sub>i* y)

goal (1 subgoal):
 1. \<turnstile>a # x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (a # x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (a # x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)
[PROOF STEP]
by (smt DiffI att_orD1 att_orD2 att_or_snd_att attack.simps(3) insert_iff list.set(2) prod.sel(1) snd_conv subset_iff)
[PROOF STATE]
proof (state)
this:
\<turnstile>a # x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (a # x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (a # x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<turnstile>x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup> \<longrightarrow> (\<forall>x\<in>fst (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)). \<exists>y. y \<in> snd (attack (x1a \<oplus>\<^sub>\<or>\<^bsup>x2\<^esup>)) \<and> x \<rightarrow>\<^sub>i* y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma att_elem_seq0: "\<turnstile> x1 \<Longrightarrow> (\<forall> x \<in> fst(attack x1).
                     (\<exists> y. y \<in> snd(attack x1) \<and> x \<rightarrow>\<^sub>i* y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile>x1 \<Longrightarrow> \<forall>x\<in>fst (attack x1). \<exists>y. y \<in> snd (attack x1) \<and> x \<rightarrow>\<^sub>i* y
[PROOF STEP]
by (simp add: att_elem_seq)


[STATEMENT]
lemma ref_valI: " A \<sqsubseteq> A'\<Longrightarrow>  \<turnstile> A' \<Longrightarrow> \<turnstile>\<^sub>V A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<sqsubseteq> A'; \<turnstile>A'\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>V A
[PROOF STEP]
using ref_validity_def valid_ref_def
[PROOF STATE]
proof (prove)
using this:
\<turnstile>\<^sub>V ?A \<equiv> \<exists>A'. ?A \<sqsubseteq>\<^sub>V A'
?A \<sqsubseteq>\<^sub>V ?A' \<equiv> ?A \<sqsubseteq> ?A' \<and> \<turnstile>?A'

goal (1 subgoal):
 1. \<lbrakk>A \<sqsubseteq> A'; \<turnstile>A'\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>V A
[PROOF STEP]
by blast


[STATEMENT]
lemma nth_app_eq[rule_format]:
              "\<forall> sl x. sl \<noteq> [] \<longrightarrow> sl ! (length sl - Suc (0)) = x
              \<longrightarrow> (l @ sl) ! (length l + length sl - Suc (0)) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>sl x. sl \<noteq> [] \<longrightarrow> sl ! (length sl - Suc 0) = x \<longrightarrow> (l @ sl) ! (length l + length sl - Suc 0) = x
[PROOF STEP]
by (induction l) auto


[STATEMENT]
lemma nth_app_eq1[rule_format]: "i < length sla \<Longrightarrow> (sla @ sl) ! i = sla ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length sla \<Longrightarrow> (sla @ sl) ! i = sla ! i
[PROOF STEP]
by (simp add: nth_append)


[STATEMENT]
lemma nth_app_eq1_rev:   "i < length sla \<Longrightarrow>  sla ! i = (sla @ sl) ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length sla \<Longrightarrow> sla ! i = (sla @ sl) ! i
[PROOF STEP]
by (simp add: nth_append)


[STATEMENT]
lemma nth_app_eq2[rule_format]: "\<forall> sl i. length sla \<le> i \<and> i < length (sla @ sl)
                     \<longrightarrow> (sla @ sl) ! i = sl ! (i - (length sla))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>sl i. length sla \<le> i \<and> i < length (sla @ sl) \<longrightarrow> (sla @ sl) ! i = sl ! (i - length sla)
[PROOF STEP]
by (simp add: nth_append)


[STATEMENT]
lemma tl_ne_ex[rule_format]: "l \<noteq> [] \<longrightarrow> (? x . l = x # (tl l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<noteq> [] \<longrightarrow> (\<exists>x. l = x # tl l)
[PROOF STEP]
by (induction l, auto)


[STATEMENT]
lemma tl_nempty_lngth[rule_format]: "tl sl \<noteq> [] \<longrightarrow> 2 \<le> length(sl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl sl \<noteq> [] \<longrightarrow> 2 \<le> length sl
[PROOF STEP]
using le_less
[PROOF STATE]
proof (prove)
using this:
(?x \<le> ?y) = (?x < ?y \<or> ?x = ?y)

goal (1 subgoal):
 1. tl sl \<noteq> [] \<longrightarrow> 2 \<le> length sl
[PROOF STEP]
by fastforce


[STATEMENT]
lemma list_app_one_length: "length l = n \<Longrightarrow> (l @ [s]) ! n = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length l = n \<Longrightarrow> (l @ [s]) ! n = s
[PROOF STEP]
by (erule subst, simp)


[STATEMENT]
lemma tl_lem1[rule_format]: "l \<noteq> [] \<longrightarrow> tl l = [] \<longrightarrow> length l = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<noteq> [] \<longrightarrow> tl l = [] \<longrightarrow> length l = 1
[PROOF STEP]
by (induction l, simp+)


[STATEMENT]
lemma nth_tl_length[rule_format]: "tl sl \<noteq> [] \<longrightarrow>
      tl sl ! (length (tl sl) - Suc (0)) = sl ! (length sl - Suc (0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl sl \<noteq> [] \<longrightarrow> tl sl ! (length (tl sl) - Suc 0) = sl ! (length sl - Suc 0)
[PROOF STEP]
by (induction sl, simp+)


[STATEMENT]
lemma nth_tl_length1[rule_format]: "tl sl \<noteq> [] \<longrightarrow>
      tl sl ! n = sl ! (n + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl sl \<noteq> [] \<longrightarrow> tl sl ! n = sl ! (n + 1)
[PROOF STEP]
by (induction sl, simp+)


[STATEMENT]
lemma ineq1: "i < length sla - n  \<Longrightarrow>
       (0) \<le> n \<Longrightarrow> i < length sla"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < length sla - n; 0 \<le> n\<rbrakk> \<Longrightarrow> i < length sla
[PROOF STEP]
by simp


[STATEMENT]
lemma ineq2[rule_format]: "length sla \<le> i \<longrightarrow> i + (1) - length sla = i - length sla + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length sla \<le> i \<longrightarrow> i + 1 - length sla = i - length sla + 1
[PROOF STEP]
by arith


[STATEMENT]
lemma ineq3: "tl sl \<noteq> []  \<Longrightarrow> length sla \<le> i \<Longrightarrow> i < length (sla @ tl sl) - (1)
              \<Longrightarrow> i - length sla + (1) < length sl - (1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tl sl \<noteq> []; length sla \<le> i; i < length (sla @ tl sl) - 1\<rbrakk> \<Longrightarrow> i - length sla + 1 < length sl - 1
[PROOF STEP]
by simp


[STATEMENT]
lemma tl_eq1[rule_format]: "sl \<noteq> [] \<longrightarrow> tl sl ! (0) = sl ! Suc (0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sl \<noteq> [] \<longrightarrow> tl sl ! 0 = sl ! Suc 0
[PROOF STEP]
by (induction sl, simp+)


[STATEMENT]
lemma tl_eq2[rule_format]: "tl sl = [] \<longrightarrow> sl ! (0) = sl ! (length sl - (1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl sl = [] \<longrightarrow> sl ! 0 = sl ! (length sl - 1)
[PROOF STEP]
by (induction sl, simp+)


[STATEMENT]
lemma tl_eq3[rule_format]: "tl sl \<noteq> [] \<longrightarrow>
    tl sl ! (length sl - Suc (Suc (0))) = sl ! (length sl - Suc (0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl sl \<noteq> [] \<longrightarrow> tl sl ! (length sl - Suc (Suc 0)) = sl ! (length sl - Suc 0)
[PROOF STEP]
by (induction sl, simp+)