[STATEMENT]
lemma order_le_prod [iff]: "order(Product.le r\<^sub>A r\<^sub>B) = (order r\<^sub>A & order r\<^sub>B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order (Product.le r\<^sub>A r\<^sub>B) = (order r\<^sub>A \<and> order r\<^sub>B)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order (Product.le r\<^sub>A r\<^sub>B) = (order r\<^sub>A \<and> order r\<^sub>B)
[PROOF STEP]
apply (unfold order_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>x. x <=(r\<^sub>A,r\<^sub>B) x) \<and> (\<forall>x y. x <=(r\<^sub>A,r\<^sub>B) y \<and> y <=(r\<^sub>A,r\<^sub>B) x \<longrightarrow> x = y) \<and> (\<forall>x y z. x <=(r\<^sub>A,r\<^sub>B) y \<and> y <=(r\<^sub>A,r\<^sub>B) z \<longrightarrow> x <=(r\<^sub>A,r\<^sub>B) z)) = (((\<forall>x. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x) \<and> (\<forall>x y. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<longrightarrow> x = y) \<and> (\<forall>x y z. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z)) \<and> (\<forall>x. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x) \<and> (\<forall>x y. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x \<longrightarrow> x = y) \<and> (\<forall>x y z. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>a. a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> a) \<and> (\<forall>b. b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> b) \<and> (\<forall>a b aa ba. a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> aa \<and> b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ba \<and> aa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> a \<and> ba \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> b \<longrightarrow> a = aa \<and> b = ba) \<and> (\<forall>a b aa ba ab bb. a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> aa \<and> b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ba \<and> aa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> ab \<and> ba \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> bb \<longrightarrow> a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> ab \<and> b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> bb)) = ((\<forall>x. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x) \<and> (\<forall>x y. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<longrightarrow> x = y) \<and> (\<forall>x y z. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z) \<and> (\<forall>x. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x) \<and> (\<forall>x y. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x \<longrightarrow> x = y) \<and> (\<forall>x y z. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z))
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>x y. \<lbrakk>\<forall>a. a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> a; \<forall>b. b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> b; \<forall>a b aa ba. a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> aa \<and> b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ba \<and> aa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> a \<and> ba \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> b \<longrightarrow> a = aa \<and> b = ba; \<forall>a b aa ba ab bb. a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> aa \<and> b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ba \<and> aa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> ab \<and> ba \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> bb \<longrightarrow> a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> ab \<and> b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> bb; x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y; y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x\<rbrakk> \<Longrightarrow> x = y
 2. \<And>x y z. \<lbrakk>\<forall>a. a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> a; \<forall>b. b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> b; \<forall>a b aa ba. a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> aa \<and> b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ba \<and> aa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> a \<and> ba \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> b \<longrightarrow> a = aa \<and> b = ba; \<forall>a b aa ba ab bb. a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> aa \<and> b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ba \<and> aa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> ab \<and> ba \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> bb \<longrightarrow> a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> ab \<and> b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> bb; x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y; y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z
 3. \<And>x y. \<lbrakk>\<forall>a. a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> a; \<forall>b. b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> b; \<forall>a b aa ba. a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> aa \<and> b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ba \<and> aa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> a \<and> ba \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> b \<longrightarrow> a = aa \<and> b = ba; \<forall>a b aa ba ab bb. a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> aa \<and> b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ba \<and> aa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> ab \<and> ba \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> bb \<longrightarrow> a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> ab \<and> b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> bb; x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y; y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x\<rbrakk> \<Longrightarrow> x = y
 4. \<And>x y z. \<lbrakk>\<forall>a. a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> a; \<forall>b. b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> b; \<forall>a b aa ba. a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> aa \<and> b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ba \<and> aa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> a \<and> ba \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> b \<longrightarrow> a = aa \<and> b = ba; \<forall>a b aa ba ab bb. a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> aa \<and> b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ba \<and> aa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> ab \<and> ba \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> bb \<longrightarrow> a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> ab \<and> b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> bb; x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y; y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z
 5. \<And>a b aa ba. \<lbrakk>\<forall>x. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x; \<forall>x y. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<longrightarrow> x = y; \<forall>x y z. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z; \<forall>x. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x; \<forall>x y. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x \<longrightarrow> x = y; \<forall>x y z. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z; a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> aa; b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ba; aa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> a; ba \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> b\<rbrakk> \<Longrightarrow> a = aa
 6. \<And>a b aa ba. \<lbrakk>\<forall>x. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x; \<forall>x y. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<longrightarrow> x = y; \<forall>x y z. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z; \<forall>x. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x; \<forall>x y. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x \<longrightarrow> x = y; \<forall>x y z. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z; a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> aa; b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ba; aa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> a; ba \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> b\<rbrakk> \<Longrightarrow> b = ba
 7. \<And>a b aa ba ab bb. \<lbrakk>\<forall>x. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x; \<forall>x y. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<longrightarrow> x = y; \<forall>x y z. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z; \<forall>x. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x; \<forall>x y. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x \<longrightarrow> x = y; \<forall>x y z. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z; a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> aa; b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ba; aa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> ab; ba \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> bb\<rbrakk> \<Longrightarrow> a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> ab
 8. \<And>a b aa ba ab bb. \<lbrakk>\<forall>x. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x; \<forall>x y. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<longrightarrow> x = y; \<forall>x y z. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z; \<forall>x. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x; \<forall>x y. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x \<longrightarrow> x = y; \<forall>x y z. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z; a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> aa; b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ba; aa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> ab; ba \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> bb\<rbrakk> \<Longrightarrow> b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> bb
[PROOF STEP]
apply blast+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma lemma_1:
  fixes as :: "(('a, 'b) fmap \<times> ('a, 'b) fmap) list" and PPROB
  assumes "(s \<in> valid_states PROB)" "(as \<in> valid_plans PROB)"
  shows "((last ` (state_set (state_list s as))) \<subseteq> valid_states PROB)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. last ` state_set (state_list s as) \<subseteq> valid_states PROB
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
s \<in> valid_states PROB
as \<in> valid_plans PROB

goal (1 subgoal):
 1. last ` state_set (state_list s as) \<subseteq> valid_states PROB
[PROOF STEP]
proof (induction as arbitrary: s PROB)
  \<comment> \<open>NOTE Base case simplifies to @{term "{s} \<subseteq> valid_states PROB"} which itself follows directly from
    1st assumption.\<close>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s PROB. \<lbrakk>s \<in> valid_states PROB; [] \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s []) \<subseteq> valid_states PROB
 2. \<And>a as s PROB. \<lbrakk>\<And>s PROB. \<lbrakk>s \<in> valid_states PROB; as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s as) \<subseteq> valid_states PROB; s \<in> valid_states PROB; a # as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s (a # as)) \<subseteq> valid_states PROB
[PROOF STEP]
case (Cons a as)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?s \<in> valid_states ?PROB; as \<in> valid_plans ?PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list ?s as) \<subseteq> valid_states ?PROB
s \<in> valid_states PROB
a # as \<in> valid_plans PROB

goal (2 subgoals):
 1. \<And>s PROB. \<lbrakk>s \<in> valid_states PROB; [] \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s []) \<subseteq> valid_states PROB
 2. \<And>a as s PROB. \<lbrakk>\<And>s PROB. \<lbrakk>s \<in> valid_states PROB; as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s as) \<subseteq> valid_states PROB; s \<in> valid_states PROB; a # as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s (a # as)) \<subseteq> valid_states PROB
[PROOF STEP]
text \<open> Split the 'insert' term produced by @{term "state_set (state_list s (a # as))"} and proof
      inclusion in 'valid\_states PROB' for both parts. \<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>?s \<in> valid_states ?PROB; as \<in> valid_plans ?PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list ?s as) \<subseteq> valid_states ?PROB
s \<in> valid_states PROB
a # as \<in> valid_plans PROB

goal (2 subgoals):
 1. \<And>s PROB. \<lbrakk>s \<in> valid_states PROB; [] \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s []) \<subseteq> valid_states PROB
 2. \<And>a as s PROB. \<lbrakk>\<And>s PROB. \<lbrakk>s \<in> valid_states PROB; as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s as) \<subseteq> valid_states PROB; s \<in> valid_states PROB; a # as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s (a # as)) \<subseteq> valid_states PROB
[PROOF STEP]
{
    \<comment> \<open>NOTE Inclusion of the first subset follows from the induction premise by simplification.
      The inclusion of the second subset is shown by applying the induction hypothesis to
      `state\_succ s a` and some elementary set simplifications.\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>?s \<in> valid_states ?PROB; as \<in> valid_plans ?PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list ?s as) \<subseteq> valid_states ?PROB
s \<in> valid_states PROB
a # as \<in> valid_plans PROB

goal (2 subgoals):
 1. \<And>s PROB. \<lbrakk>s \<in> valid_states PROB; [] \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s []) \<subseteq> valid_states PROB
 2. \<And>a as s PROB. \<lbrakk>\<And>s PROB. \<lbrakk>s \<in> valid_states PROB; as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s as) \<subseteq> valid_states PROB; s \<in> valid_states PROB; a # as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s (a # as)) \<subseteq> valid_states PROB
[PROOF STEP]
have "last [s] \<in> valid_states PROB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. last [s] \<in> valid_states PROB
[PROOF STEP]
using Cons.prems(1)
[PROOF STATE]
proof (prove)
using this:
s \<in> valid_states PROB

goal (1 subgoal):
 1. last [s] \<in> valid_states PROB
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
last [s] \<in> valid_states PROB

goal (2 subgoals):
 1. \<And>s PROB. \<lbrakk>s \<in> valid_states PROB; [] \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s []) \<subseteq> valid_states PROB
 2. \<And>a as s PROB. \<lbrakk>\<And>s PROB. \<lbrakk>s \<in> valid_states PROB; as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s as) \<subseteq> valid_states PROB; s \<in> valid_states PROB; a # as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s (a # as)) \<subseteq> valid_states PROB
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
last [s] \<in> valid_states PROB

goal (2 subgoals):
 1. \<And>s PROB. \<lbrakk>s \<in> valid_states PROB; [] \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s []) \<subseteq> valid_states PROB
 2. \<And>a as s PROB. \<lbrakk>\<And>s PROB. \<lbrakk>s \<in> valid_states PROB; as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s as) \<subseteq> valid_states PROB; s \<in> valid_states PROB; a # as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s (a # as)) \<subseteq> valid_states PROB
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
last [s] \<in> valid_states PROB

goal (2 subgoals):
 1. \<And>s PROB. \<lbrakk>s \<in> valid_states PROB; [] \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s []) \<subseteq> valid_states PROB
 2. \<And>a as s PROB. \<lbrakk>\<And>s PROB. \<lbrakk>s \<in> valid_states PROB; as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s as) \<subseteq> valid_states PROB; s \<in> valid_states PROB; a # as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s (a # as)) \<subseteq> valid_states PROB
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
last [s] \<in> valid_states PROB

goal (2 subgoals):
 1. \<And>s PROB. \<lbrakk>s \<in> valid_states PROB; [] \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s []) \<subseteq> valid_states PROB
 2. \<And>a as s PROB. \<lbrakk>\<And>s PROB. \<lbrakk>s \<in> valid_states PROB; as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s as) \<subseteq> valid_states PROB; s \<in> valid_states PROB; a # as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s (a # as)) \<subseteq> valid_states PROB
[PROOF STEP]
have "a \<in> PROB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> PROB
[PROOF STEP]
using Cons.prems(2) valid_plan_valid_head
[PROOF STATE]
proof (prove)
using this:
a # as \<in> valid_plans PROB
?h # ?as \<in> valid_plans ?PROB \<Longrightarrow> ?h \<in> ?PROB

goal (1 subgoal):
 1. a \<in> PROB
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
a \<in> PROB

goal (2 subgoals):
 1. \<And>s PROB. \<lbrakk>s \<in> valid_states PROB; [] \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s []) \<subseteq> valid_states PROB
 2. \<And>a as s PROB. \<lbrakk>\<And>s PROB. \<lbrakk>s \<in> valid_states PROB; as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s as) \<subseteq> valid_states PROB; s \<in> valid_states PROB; a # as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s (a # as)) \<subseteq> valid_states PROB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> PROB
[PROOF STEP]
have "state_succ s a \<in> valid_states PROB"
[PROOF STATE]
proof (prove)
using this:
a \<in> PROB

goal (1 subgoal):
 1. state_succ s a \<in> valid_states PROB
[PROOF STEP]
using Cons.prems(1) lemma_1_i
[PROOF STATE]
proof (prove)
using this:
a \<in> PROB
s \<in> valid_states PROB
\<lbrakk>?s \<in> valid_states ?PROB; ?a \<in> ?PROB\<rbrakk> \<Longrightarrow> state_succ ?s ?a \<in> valid_states ?PROB

goal (1 subgoal):
 1. state_succ s a \<in> valid_states PROB
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
state_succ s a \<in> valid_states PROB

goal (2 subgoals):
 1. \<And>s PROB. \<lbrakk>s \<in> valid_states PROB; [] \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s []) \<subseteq> valid_states PROB
 2. \<And>a as s PROB. \<lbrakk>\<And>s PROB. \<lbrakk>s \<in> valid_states PROB; as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s as) \<subseteq> valid_states PROB; s \<in> valid_states PROB; a # as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s (a # as)) \<subseteq> valid_states PROB
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
state_succ s a \<in> valid_states PROB

goal (2 subgoals):
 1. \<And>s PROB. \<lbrakk>s \<in> valid_states PROB; [] \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s []) \<subseteq> valid_states PROB
 2. \<And>a as s PROB. \<lbrakk>\<And>s PROB. \<lbrakk>s \<in> valid_states PROB; as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s as) \<subseteq> valid_states PROB; s \<in> valid_states PROB; a # as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s (a # as)) \<subseteq> valid_states PROB
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
state_succ s a \<in> valid_states PROB

goal (2 subgoals):
 1. \<And>s PROB. \<lbrakk>s \<in> valid_states PROB; [] \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s []) \<subseteq> valid_states PROB
 2. \<And>a as s PROB. \<lbrakk>\<And>s PROB. \<lbrakk>s \<in> valid_states PROB; as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s as) \<subseteq> valid_states PROB; s \<in> valid_states PROB; a # as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s (a # as)) \<subseteq> valid_states PROB
[PROOF STEP]
have "as \<in> valid_plans PROB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. as \<in> valid_plans PROB
[PROOF STEP]
using Cons.prems(2) valid_plan_valid_tail
[PROOF STATE]
proof (prove)
using this:
a # as \<in> valid_plans PROB
?h # ?as \<in> valid_plans ?PROB \<Longrightarrow> ?as \<in> valid_plans ?PROB

goal (1 subgoal):
 1. as \<in> valid_plans PROB
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
as \<in> valid_plans PROB

goal (2 subgoals):
 1. \<And>s PROB. \<lbrakk>s \<in> valid_states PROB; [] \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s []) \<subseteq> valid_states PROB
 2. \<And>a as s PROB. \<lbrakk>\<And>s PROB. \<lbrakk>s \<in> valid_states PROB; as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s as) \<subseteq> valid_states PROB; s \<in> valid_states PROB; a # as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s (a # as)) \<subseteq> valid_states PROB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
as \<in> valid_plans PROB
[PROOF STEP]
have "(last ` state_set (state_list (state_succ s a) as)) \<subseteq> valid_states PROB"
[PROOF STATE]
proof (prove)
using this:
as \<in> valid_plans PROB

goal (1 subgoal):
 1. last ` state_set (state_list (state_succ s a) as) \<subseteq> valid_states PROB
[PROOF STEP]
using  calculation Cons.IH[of "state_succ s a"]
[PROOF STATE]
proof (prove)
using this:
as \<in> valid_plans PROB
state_succ s a \<in> valid_states PROB
\<lbrakk>state_succ s a \<in> valid_states ?PROB; as \<in> valid_plans ?PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list (state_succ s a) as) \<subseteq> valid_states ?PROB

goal (1 subgoal):
 1. last ` state_set (state_list (state_succ s a) as) \<subseteq> valid_states PROB
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
last ` state_set (state_list (state_succ s a) as) \<subseteq> valid_states PROB

goal (2 subgoals):
 1. \<And>s PROB. \<lbrakk>s \<in> valid_states PROB; [] \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s []) \<subseteq> valid_states PROB
 2. \<And>a as s PROB. \<lbrakk>\<And>s PROB. \<lbrakk>s \<in> valid_states PROB; as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s as) \<subseteq> valid_states PROB; s \<in> valid_states PROB; a # as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s (a # as)) \<subseteq> valid_states PROB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
last ` state_set (state_list (state_succ s a) as) \<subseteq> valid_states PROB
[PROOF STEP]
have "(last ` ((#) s ` state_set (state_list (state_succ s a) as))) \<subseteq> valid_states PROB"
[PROOF STATE]
proof (prove)
using this:
last ` state_set (state_list (state_succ s a) as) \<subseteq> valid_states PROB

goal (1 subgoal):
 1. last ` (#) s ` state_set (state_list (state_succ s a) as) \<subseteq> valid_states PROB
[PROOF STEP]
using lemma_1_ii
[PROOF STATE]
proof (prove)
using this:
last ` state_set (state_list (state_succ s a) as) \<subseteq> valid_states PROB
last ` (#) ?s ` state_set (state_list (state_succ ?s ?a) ?as) = last ` state_set (state_list (state_succ ?s ?a) ?as)

goal (1 subgoal):
 1. last ` (#) s ` state_set (state_list (state_succ s a) as) \<subseteq> valid_states PROB
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
last ` (#) s ` state_set (state_list (state_succ s a) as) \<subseteq> valid_states PROB

goal (2 subgoals):
 1. \<And>s PROB. \<lbrakk>s \<in> valid_states PROB; [] \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s []) \<subseteq> valid_states PROB
 2. \<And>a as s PROB. \<lbrakk>\<And>s PROB. \<lbrakk>s \<in> valid_states PROB; as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s as) \<subseteq> valid_states PROB; s \<in> valid_states PROB; a # as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s (a # as)) \<subseteq> valid_states PROB
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
last ` (#) s ` state_set (state_list (state_succ s a) as) \<subseteq> valid_states PROB

goal (2 subgoals):
 1. \<And>s PROB. \<lbrakk>s \<in> valid_states PROB; [] \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s []) \<subseteq> valid_states PROB
 2. \<And>a as s PROB. \<lbrakk>\<And>s PROB. \<lbrakk>s \<in> valid_states PROB; as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s as) \<subseteq> valid_states PROB; s \<in> valid_states PROB; a # as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s (a # as)) \<subseteq> valid_states PROB
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
last [s] \<in> valid_states PROB
last ` (#) s ` state_set (state_list (state_succ s a) as) \<subseteq> valid_states PROB
[PROOF STEP]
have
      "(last ` insert [s] ((#) s ` state_set (state_list (state_succ s a) as))) \<subseteq> valid_states PROB"
[PROOF STATE]
proof (prove)
using this:
last [s] \<in> valid_states PROB
last ` (#) s ` state_set (state_list (state_succ s a) as) \<subseteq> valid_states PROB

goal (1 subgoal):
 1. last ` insert [s] ((#) s ` state_set (state_list (state_succ s a) as)) \<subseteq> valid_states PROB
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
last ` insert [s] ((#) s ` state_set (state_list (state_succ s a) as)) \<subseteq> valid_states PROB

goal (2 subgoals):
 1. \<And>s PROB. \<lbrakk>s \<in> valid_states PROB; [] \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s []) \<subseteq> valid_states PROB
 2. \<And>a as s PROB. \<lbrakk>\<And>s PROB. \<lbrakk>s \<in> valid_states PROB; as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s as) \<subseteq> valid_states PROB; s \<in> valid_states PROB; a # as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s (a # as)) \<subseteq> valid_states PROB
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
last ` insert [s] ((#) s ` state_set (state_list (state_succ s a) as)) \<subseteq> valid_states PROB

goal (2 subgoals):
 1. \<And>s PROB. \<lbrakk>s \<in> valid_states PROB; [] \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s []) \<subseteq> valid_states PROB
 2. \<And>a as s PROB. \<lbrakk>\<And>s PROB. \<lbrakk>s \<in> valid_states PROB; as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s as) \<subseteq> valid_states PROB; s \<in> valid_states PROB; a # as \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s (a # as)) \<subseteq> valid_states PROB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
last ` insert [s] ((#) s ` state_set (state_list (state_succ s a) as)) \<subseteq> valid_states PROB
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
last ` insert [s] ((#) s ` state_set (state_list (state_succ s a) as)) \<subseteq> valid_states PROB

goal (1 subgoal):
 1. last ` state_set (state_list s (a # as)) \<subseteq> valid_states PROB
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
last ` state_set (state_list s (a # as)) \<subseteq> valid_states PROB

goal (1 subgoal):
 1. \<And>s PROB. \<lbrakk>s \<in> valid_states PROB; [] \<in> valid_plans PROB\<rbrakk> \<Longrightarrow> last ` state_set (state_list s []) \<subseteq> valid_states PROB
[PROOF STEP]
qed auto

\<comment> \<open>TODO unwrap metis proof.\<close>


[STATEMENT]
lemma (in gram_schmidt_fs) Gramian_determinant_det: assumes A: "A \<in> carrier_mat n n"
  shows "Gramian_determinant (rows A) n = det A * det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gramian_determinant (rows A) n = det A * det A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Gramian_determinant (rows A) n = det A * det A
[PROOF STEP]
have [simp]: "mat_of_rows n (rows A) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_rows n (rows A) = A
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. mat_of_rows n (rows A) = A
[PROOF STEP]
by (intro eq_matI, auto)
[PROOF STATE]
proof (state)
this:
mat_of_rows n (rows A) = A

goal (1 subgoal):
 1. Gramian_determinant (rows A) n = det A * det A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gramian_determinant (rows A) n = det A * det A
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. Gramian_determinant (rows A) n = det A * det A
[PROOF STEP]
unfolding Gramian_determinant_def
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. det (Gramian_matrix (rows A) n) = det A * det A
[PROOF STEP]
by (subst Gramian_matrix_alt_def, force, simp add: Let_def, subst det_mult[of _ n],
    auto simp: det_transpose)
[PROOF STATE]
proof (state)
this:
Gramian_determinant (rows A) n = det A * det A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ideal_quot_set_ideal [simp]: "ideal (ideal B \<div> x) = (ideal B) \<div> (x::_::comm_ring)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal (ideal B \<div> x) = ideal B \<div> x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ideal (ideal B \<div> x) \<subseteq> ideal B \<div> x
 2. ideal B \<div> x \<subseteq> ideal (ideal B \<div> x)
[PROOF STEP]
show "ideal (ideal B \<div> x) \<subseteq> ideal B \<div> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal (ideal B \<div> x) \<subseteq> ideal B \<div> x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> ideal (ideal B \<div> x) \<Longrightarrow> xa \<in> ideal B \<div> x
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> ideal (ideal B \<div> x) \<Longrightarrow> xa \<in> ideal B \<div> x
[PROOF STEP]
assume "b \<in> ideal (ideal B \<div> x)"
[PROOF STATE]
proof (state)
this:
b \<in> ideal (ideal B \<div> x)

goal (1 subgoal):
 1. \<And>xa. xa \<in> ideal (ideal B \<div> x) \<Longrightarrow> xa \<in> ideal B \<div> x
[PROOF STEP]
thus "b \<in> ideal B \<div> x"
[PROOF STATE]
proof (prove)
using this:
b \<in> ideal (ideal B \<div> x)

goal (1 subgoal):
 1. b \<in> ideal B \<div> x
[PROOF STEP]
proof (induct b rule: ideal.span_induct')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (0::'a) \<in> ideal B \<div> x
 2. \<And>a q p. \<lbrakk>a \<in> ideal (ideal B \<div> x); a \<in> ideal B \<div> x; p \<in> ideal B \<div> x; q \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> a + q * p \<in> ideal B \<div> x
[PROOF STEP]
case base
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. (0::'a) \<in> ideal B \<div> x
 2. \<And>a q p. \<lbrakk>a \<in> ideal (ideal B \<div> x); a \<in> ideal B \<div> x; p \<in> ideal B \<div> x; q \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> a + q * p \<in> ideal B \<div> x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<in> ideal B \<div> x
[PROOF STEP]
by (simp add: quot_set_iff ideal.span_zero)
[PROOF STATE]
proof (state)
this:
(0::'a) \<in> ideal B \<div> x

goal (1 subgoal):
 1. \<And>a q p. \<lbrakk>a \<in> ideal (ideal B \<div> x); a \<in> ideal B \<div> x; p \<in> ideal B \<div> x; q \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> a + q * p \<in> ideal B \<div> x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a q p. \<lbrakk>a \<in> ideal (ideal B \<div> x); a \<in> ideal B \<div> x; p \<in> ideal B \<div> x; q \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> a + q * p \<in> ideal B \<div> x
[PROOF STEP]
case (step b q p)
[PROOF STATE]
proof (state)
this:
b \<in> ideal (ideal B \<div> x)
b \<in> ideal B \<div> x
p \<in> ideal B \<div> x
q \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>a q p. \<lbrakk>a \<in> ideal (ideal B \<div> x); a \<in> ideal B \<div> x; p \<in> ideal B \<div> x; q \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> a + q * p \<in> ideal B \<div> x
[PROOF STEP]
hence "x * b \<in> ideal B" and "x * p \<in> ideal B"
[PROOF STATE]
proof (prove)
using this:
b \<in> ideal (ideal B \<div> x)
b \<in> ideal B \<div> x
p \<in> ideal B \<div> x
q \<noteq> (0::'a)

goal (1 subgoal):
 1. x * b \<in> ideal B &&& x * p \<in> ideal B
[PROOF STEP]
by (simp_all add: quot_set_iff)
[PROOF STATE]
proof (state)
this:
x * b \<in> ideal B
x * p \<in> ideal B

goal (1 subgoal):
 1. \<And>a q p. \<lbrakk>a \<in> ideal (ideal B \<div> x); a \<in> ideal B \<div> x; p \<in> ideal B \<div> x; q \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> a + q * p \<in> ideal B \<div> x
[PROOF STEP]
hence "x * b + q * (x * p) \<in> ideal B"
[PROOF STATE]
proof (prove)
using this:
x * b \<in> ideal B
x * p \<in> ideal B

goal (1 subgoal):
 1. x * b + q * (x * p) \<in> ideal B
[PROOF STEP]
by (intro ideal.span_add ideal.span_scale[where c=q])
[PROOF STATE]
proof (state)
this:
x * b + q * (x * p) \<in> ideal B

goal (1 subgoal):
 1. \<And>a q p. \<lbrakk>a \<in> ideal (ideal B \<div> x); a \<in> ideal B \<div> x; p \<in> ideal B \<div> x; q \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> a + q * p \<in> ideal B \<div> x
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
x * b + q * (x * p) \<in> ideal B

goal (1 subgoal):
 1. b + q * p \<in> ideal B \<div> x
[PROOF STEP]
by (simp only: quot_set_iff algebra_simps)
[PROOF STATE]
proof (state)
this:
b + q * p \<in> ideal B \<div> x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
b \<in> ideal B \<div> x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ideal (ideal B \<div> x) \<subseteq> ideal B \<div> x

goal (1 subgoal):
 1. ideal B \<div> x \<subseteq> ideal (ideal B \<div> x)
[PROOF STEP]
qed (fact ideal.span_superset)


[STATEMENT]
lemma sep_conj_impl1:
  assumes P: "\<And>h. P h \<Longrightarrow> I h"
  shows "(P ** R) h \<Longrightarrow> (I ** R) h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<and>* R) h \<Longrightarrow> (I \<and>* R) h
[PROOF STEP]
by (auto intro: sep_conj_impl P)


[STATEMENT]
lemma pure_split:
  "pure P = (P = sep_true \<or> P = sep_false)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pure P = (P = (\<lambda>s. True) \<or> P = (\<lambda>s. False))
[PROOF STEP]
by (force simp: pure_def intro!: ext)


[STATEMENT]
lemma rawpsubst_subst_fresh_switch:
  assumes "\<phi> \<in> fmla" "snd ` (set txs) \<subseteq> var" and "fst ` (set txs) \<subseteq> trm"
    and "\<forall> x \<in> snd ` (set txs). x \<notin> FvarsT s"
    and "\<forall> t \<in> fst ` (set txs). y \<notin> FvarsT t"
    and "distinct (map snd txs)"
    and "s \<in> trm" and "y \<in> var" "y \<notin> snd ` (set txs)"
  shows "rawpsubst (subst \<phi> s y) txs = rawpsubst \<phi> (txs @ [(s,y)])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rawpsubst (subst \<phi> s y) txs = rawpsubst \<phi> (txs @ [(s, y)])
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
snd ` set txs \<subseteq> var
fst ` set txs \<subseteq> trm
\<forall>x\<in>snd ` set txs. x \<notin> FvarsT s
\<forall>t\<in>fst ` set txs. y \<notin> FvarsT t
distinct (map snd txs)
s \<in> trm
y \<in> var
y \<notin> snd ` set txs

goal (1 subgoal):
 1. rawpsubst (subst \<phi> s y) txs = rawpsubst \<phi> (txs @ [(s, y)])
[PROOF STEP]
proof(induction txs arbitrary: \<phi> s y)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set [] \<subseteq> var; fst ` set [] \<subseteq> trm; \<forall>x\<in>snd ` set []. x \<notin> FvarsT s; \<forall>t\<in>fst ` set []. y \<notin> FvarsT t; distinct (map snd []); s \<in> trm; y \<in> var; y \<notin> snd ` set []\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) [] = rawpsubst \<phi> ([] @ [(s, y)])
 2. \<And>a txs \<phi> s y. \<lbrakk>\<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<forall>x\<in>snd ` set txs. x \<notin> FvarsT s; \<forall>t\<in>fst ` set txs. y \<notin> FvarsT t; distinct (map snd txs); s \<in> trm; y \<in> var; y \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) txs = rawpsubst \<phi> (txs @ [(s, y)]); \<phi> \<in> fmla; snd ` set (a # txs) \<subseteq> var; fst ` set (a # txs) \<subseteq> trm; \<forall>x\<in>snd ` set (a # txs). x \<notin> FvarsT s; \<forall>t\<in>fst ` set (a # txs). y \<notin> FvarsT t; distinct (map snd (a # txs)); s \<in> trm; y \<in> var; y \<notin> snd ` set (a # txs)\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) (a # txs) = rawpsubst \<phi> ((a # txs) @ [(s, y)])
[PROOF STEP]
case (Cons tx txs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<forall>x\<in>snd ` set txs. x \<notin> FvarsT ?s; \<forall>t\<in>fst ` set txs. ?y \<notin> FvarsT t; distinct (map snd txs); ?s \<in> trm; ?y \<in> var; ?y \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> rawpsubst (subst ?\<phi> ?s ?y) txs = rawpsubst ?\<phi> (txs @ [(?s, ?y)])
\<phi> \<in> fmla
snd ` set (tx # txs) \<subseteq> var
fst ` set (tx # txs) \<subseteq> trm
\<forall>x\<in>snd ` set (tx # txs). x \<notin> FvarsT s
\<forall>t\<in>fst ` set (tx # txs). y \<notin> FvarsT t
distinct (map snd (tx # txs))
s \<in> trm
y \<in> var
y \<notin> snd ` set (tx # txs)

goal (2 subgoals):
 1. \<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set [] \<subseteq> var; fst ` set [] \<subseteq> trm; \<forall>x\<in>snd ` set []. x \<notin> FvarsT s; \<forall>t\<in>fst ` set []. y \<notin> FvarsT t; distinct (map snd []); s \<in> trm; y \<in> var; y \<notin> snd ` set []\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) [] = rawpsubst \<phi> ([] @ [(s, y)])
 2. \<And>a txs \<phi> s y. \<lbrakk>\<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<forall>x\<in>snd ` set txs. x \<notin> FvarsT s; \<forall>t\<in>fst ` set txs. y \<notin> FvarsT t; distinct (map snd txs); s \<in> trm; y \<in> var; y \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) txs = rawpsubst \<phi> (txs @ [(s, y)]); \<phi> \<in> fmla; snd ` set (a # txs) \<subseteq> var; fst ` set (a # txs) \<subseteq> trm; \<forall>x\<in>snd ` set (a # txs). x \<notin> FvarsT s; \<forall>t\<in>fst ` set (a # txs). y \<notin> FvarsT t; distinct (map snd (a # txs)); s \<in> trm; y \<in> var; y \<notin> snd ` set (a # txs)\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) (a # txs) = rawpsubst \<phi> ((a # txs) @ [(s, y)])
[PROOF STEP]
obtain t x where tx[simp]: "tx = (t,x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t x. tx = (t, x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
tx = (t, x)

goal (2 subgoals):
 1. \<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set [] \<subseteq> var; fst ` set [] \<subseteq> trm; \<forall>x\<in>snd ` set []. x \<notin> FvarsT s; \<forall>t\<in>fst ` set []. y \<notin> FvarsT t; distinct (map snd []); s \<in> trm; y \<in> var; y \<notin> snd ` set []\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) [] = rawpsubst \<phi> ([] @ [(s, y)])
 2. \<And>a txs \<phi> s y. \<lbrakk>\<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<forall>x\<in>snd ` set txs. x \<notin> FvarsT s; \<forall>t\<in>fst ` set txs. y \<notin> FvarsT t; distinct (map snd txs); s \<in> trm; y \<in> var; y \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) txs = rawpsubst \<phi> (txs @ [(s, y)]); \<phi> \<in> fmla; snd ` set (a # txs) \<subseteq> var; fst ` set (a # txs) \<subseteq> trm; \<forall>x\<in>snd ` set (a # txs). x \<notin> FvarsT s; \<forall>t\<in>fst ` set (a # txs). y \<notin> FvarsT t; distinct (map snd (a # txs)); s \<in> trm; y \<in> var; y \<notin> snd ` set (a # txs)\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) (a # txs) = rawpsubst \<phi> ((a # txs) @ [(s, y)])
[PROOF STEP]
have x: "x \<in> var" and t: "t \<in> trm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> var &&& t \<in> trm
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<forall>x\<in>snd ` set txs. x \<notin> FvarsT ?s; \<forall>t\<in>fst ` set txs. ?y \<notin> FvarsT t; distinct (map snd txs); ?s \<in> trm; ?y \<in> var; ?y \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> rawpsubst (subst ?\<phi> ?s ?y) txs = rawpsubst ?\<phi> (txs @ [(?s, ?y)])
\<phi> \<in> fmla
snd ` set (tx # txs) \<subseteq> var
fst ` set (tx # txs) \<subseteq> trm
\<forall>x\<in>snd ` set (tx # txs). x \<notin> FvarsT s
\<forall>t\<in>fst ` set (tx # txs). y \<notin> FvarsT t
distinct (map snd (tx # txs))
s \<in> trm
y \<in> var
y \<notin> snd ` set (tx # txs)

goal (1 subgoal):
 1. x \<in> var &&& t \<in> trm
[PROOF STEP]
unfolding tx
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<forall>x\<in>snd ` set txs. x \<notin> FvarsT ?s; \<forall>t\<in>fst ` set txs. ?y \<notin> FvarsT t; distinct (map snd txs); ?s \<in> trm; ?y \<in> var; ?y \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> rawpsubst (subst ?\<phi> ?s ?y) txs = rawpsubst ?\<phi> (txs @ [(?s, ?y)])
\<phi> \<in> fmla
snd ` set ((t, x) # txs) \<subseteq> var
fst ` set ((t, x) # txs) \<subseteq> trm
\<forall>x\<in>snd ` set ((t, x) # txs). x \<notin> FvarsT s
\<forall>t\<in>fst ` set ((t, x) # txs). y \<notin> FvarsT t
distinct (map snd ((t, x) # txs))
s \<in> trm
y \<in> var
y \<notin> snd ` set ((t, x) # txs)

goal (1 subgoal):
 1. x \<in> var &&& t \<in> trm
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> var
t \<in> trm

goal (2 subgoals):
 1. \<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set [] \<subseteq> var; fst ` set [] \<subseteq> trm; \<forall>x\<in>snd ` set []. x \<notin> FvarsT s; \<forall>t\<in>fst ` set []. y \<notin> FvarsT t; distinct (map snd []); s \<in> trm; y \<in> var; y \<notin> snd ` set []\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) [] = rawpsubst \<phi> ([] @ [(s, y)])
 2. \<And>a txs \<phi> s y. \<lbrakk>\<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<forall>x\<in>snd ` set txs. x \<notin> FvarsT s; \<forall>t\<in>fst ` set txs. y \<notin> FvarsT t; distinct (map snd txs); s \<in> trm; y \<in> var; y \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) txs = rawpsubst \<phi> (txs @ [(s, y)]); \<phi> \<in> fmla; snd ` set (a # txs) \<subseteq> var; fst ` set (a # txs) \<subseteq> trm; \<forall>x\<in>snd ` set (a # txs). x \<notin> FvarsT s; \<forall>t\<in>fst ` set (a # txs). y \<notin> FvarsT t; distinct (map snd (a # txs)); s \<in> trm; y \<in> var; y \<notin> snd ` set (a # txs)\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) (a # txs) = rawpsubst \<phi> ((a # txs) @ [(s, y)])
[PROOF STEP]
have "rawpsubst \<phi> ((s, y) # (t, x) # txs) = rawpsubst \<phi> ([(s, y),(t, x)] @ txs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rawpsubst \<phi> ((s, y) # (t, x) # txs) = rawpsubst \<phi> ([(s, y), (t, x)] @ txs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rawpsubst \<phi> ((s, y) # (t, x) # txs) = rawpsubst \<phi> ([(s, y), (t, x)] @ txs)

goal (2 subgoals):
 1. \<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set [] \<subseteq> var; fst ` set [] \<subseteq> trm; \<forall>x\<in>snd ` set []. x \<notin> FvarsT s; \<forall>t\<in>fst ` set []. y \<notin> FvarsT t; distinct (map snd []); s \<in> trm; y \<in> var; y \<notin> snd ` set []\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) [] = rawpsubst \<phi> ([] @ [(s, y)])
 2. \<And>a txs \<phi> s y. \<lbrakk>\<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<forall>x\<in>snd ` set txs. x \<notin> FvarsT s; \<forall>t\<in>fst ` set txs. y \<notin> FvarsT t; distinct (map snd txs); s \<in> trm; y \<in> var; y \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) txs = rawpsubst \<phi> (txs @ [(s, y)]); \<phi> \<in> fmla; snd ` set (a # txs) \<subseteq> var; fst ` set (a # txs) \<subseteq> trm; \<forall>x\<in>snd ` set (a # txs). x \<notin> FvarsT s; \<forall>t\<in>fst ` set (a # txs). y \<notin> FvarsT t; distinct (map snd (a # txs)); s \<in> trm; y \<in> var; y \<notin> snd ` set (a # txs)\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) (a # txs) = rawpsubst \<phi> ((a # txs) @ [(s, y)])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rawpsubst \<phi> ((s, y) # (t, x) # txs) = rawpsubst \<phi> ([(s, y), (t, x)] @ txs)

goal (2 subgoals):
 1. \<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set [] \<subseteq> var; fst ` set [] \<subseteq> trm; \<forall>x\<in>snd ` set []. x \<notin> FvarsT s; \<forall>t\<in>fst ` set []. y \<notin> FvarsT t; distinct (map snd []); s \<in> trm; y \<in> var; y \<notin> snd ` set []\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) [] = rawpsubst \<phi> ([] @ [(s, y)])
 2. \<And>a txs \<phi> s y. \<lbrakk>\<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<forall>x\<in>snd ` set txs. x \<notin> FvarsT s; \<forall>t\<in>fst ` set txs. y \<notin> FvarsT t; distinct (map snd txs); s \<in> trm; y \<in> var; y \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) txs = rawpsubst \<phi> (txs @ [(s, y)]); \<phi> \<in> fmla; snd ` set (a # txs) \<subseteq> var; fst ` set (a # txs) \<subseteq> trm; \<forall>x\<in>snd ` set (a # txs). x \<notin> FvarsT s; \<forall>t\<in>fst ` set (a # txs). y \<notin> FvarsT t; distinct (map snd (a # txs)); s \<in> trm; y \<in> var; y \<notin> snd ` set (a # txs)\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) (a # txs) = rawpsubst \<phi> ((a # txs) @ [(s, y)])
[PROOF STEP]
have "\<dots> = rawpsubst (rawpsubst \<phi> [(s, y),(t, x)]) txs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rawpsubst \<phi> ([(s, y), (t, x)] @ txs) = rawpsubst (rawpsubst \<phi> [(s, y), (t, x)]) txs
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<forall>x\<in>snd ` set txs. x \<notin> FvarsT ?s; \<forall>t\<in>fst ` set txs. ?y \<notin> FvarsT t; distinct (map snd txs); ?s \<in> trm; ?y \<in> var; ?y \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> rawpsubst (subst ?\<phi> ?s ?y) txs = rawpsubst ?\<phi> (txs @ [(?s, ?y)])
\<phi> \<in> fmla
snd ` set (tx # txs) \<subseteq> var
fst ` set (tx # txs) \<subseteq> trm
\<forall>x\<in>snd ` set (tx # txs). x \<notin> FvarsT s
\<forall>t\<in>fst ` set (tx # txs). y \<notin> FvarsT t
distinct (map snd (tx # txs))
s \<in> trm
y \<in> var
y \<notin> snd ` set (tx # txs)

goal (1 subgoal):
 1. rawpsubst \<phi> ([(s, y), (t, x)] @ txs) = rawpsubst (rawpsubst \<phi> [(s, y), (t, x)]) txs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rawpsubst \<phi> ([(s, y), (t, x)] @ txs) = rawpsubst (rawpsubst \<phi> [(s, y), (t, x)]) txs

goal (2 subgoals):
 1. \<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set [] \<subseteq> var; fst ` set [] \<subseteq> trm; \<forall>x\<in>snd ` set []. x \<notin> FvarsT s; \<forall>t\<in>fst ` set []. y \<notin> FvarsT t; distinct (map snd []); s \<in> trm; y \<in> var; y \<notin> snd ` set []\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) [] = rawpsubst \<phi> ([] @ [(s, y)])
 2. \<And>a txs \<phi> s y. \<lbrakk>\<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<forall>x\<in>snd ` set txs. x \<notin> FvarsT s; \<forall>t\<in>fst ` set txs. y \<notin> FvarsT t; distinct (map snd txs); s \<in> trm; y \<in> var; y \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) txs = rawpsubst \<phi> (txs @ [(s, y)]); \<phi> \<in> fmla; snd ` set (a # txs) \<subseteq> var; fst ` set (a # txs) \<subseteq> trm; \<forall>x\<in>snd ` set (a # txs). x \<notin> FvarsT s; \<forall>t\<in>fst ` set (a # txs). y \<notin> FvarsT t; distinct (map snd (a # txs)); s \<in> trm; y \<in> var; y \<notin> snd ` set (a # txs)\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) (a # txs) = rawpsubst \<phi> ((a # txs) @ [(s, y)])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rawpsubst \<phi> ([(s, y), (t, x)] @ txs) = rawpsubst (rawpsubst \<phi> [(s, y), (t, x)]) txs

goal (2 subgoals):
 1. \<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set [] \<subseteq> var; fst ` set [] \<subseteq> trm; \<forall>x\<in>snd ` set []. x \<notin> FvarsT s; \<forall>t\<in>fst ` set []. y \<notin> FvarsT t; distinct (map snd []); s \<in> trm; y \<in> var; y \<notin> snd ` set []\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) [] = rawpsubst \<phi> ([] @ [(s, y)])
 2. \<And>a txs \<phi> s y. \<lbrakk>\<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<forall>x\<in>snd ` set txs. x \<notin> FvarsT s; \<forall>t\<in>fst ` set txs. y \<notin> FvarsT t; distinct (map snd txs); s \<in> trm; y \<in> var; y \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) txs = rawpsubst \<phi> (txs @ [(s, y)]); \<phi> \<in> fmla; snd ` set (a # txs) \<subseteq> var; fst ` set (a # txs) \<subseteq> trm; \<forall>x\<in>snd ` set (a # txs). x \<notin> FvarsT s; \<forall>t\<in>fst ` set (a # txs). y \<notin> FvarsT t; distinct (map snd (a # txs)); s \<in> trm; y \<in> var; y \<notin> snd ` set (a # txs)\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) (a # txs) = rawpsubst \<phi> ((a # txs) @ [(s, y)])
[PROOF STEP]
have "rawpsubst \<phi> [(s, y),(t, x)] = rawpsubst \<phi> [(t, x),(s, y)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rawpsubst \<phi> [(s, y), (t, x)] = rawpsubst \<phi> [(t, x), (s, y)]
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<forall>x\<in>snd ` set txs. x \<notin> FvarsT ?s; \<forall>t\<in>fst ` set txs. ?y \<notin> FvarsT t; distinct (map snd txs); ?s \<in> trm; ?y \<in> var; ?y \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> rawpsubst (subst ?\<phi> ?s ?y) txs = rawpsubst ?\<phi> (txs @ [(?s, ?y)])
\<phi> \<in> fmla
snd ` set (tx # txs) \<subseteq> var
fst ` set (tx # txs) \<subseteq> trm
\<forall>x\<in>snd ` set (tx # txs). x \<notin> FvarsT s
\<forall>t\<in>fst ` set (tx # txs). y \<notin> FvarsT t
distinct (map snd (tx # txs))
s \<in> trm
y \<in> var
y \<notin> snd ` set (tx # txs)

goal (1 subgoal):
 1. rawpsubst \<phi> [(s, y), (t, x)] = rawpsubst \<phi> [(t, x), (s, y)]
[PROOF STEP]
by (intro rawpsubst2_fresh_switch) auto
[PROOF STATE]
proof (state)
this:
rawpsubst \<phi> [(s, y), (t, x)] = rawpsubst \<phi> [(t, x), (s, y)]

goal (2 subgoals):
 1. \<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set [] \<subseteq> var; fst ` set [] \<subseteq> trm; \<forall>x\<in>snd ` set []. x \<notin> FvarsT s; \<forall>t\<in>fst ` set []. y \<notin> FvarsT t; distinct (map snd []); s \<in> trm; y \<in> var; y \<notin> snd ` set []\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) [] = rawpsubst \<phi> ([] @ [(s, y)])
 2. \<And>a txs \<phi> s y. \<lbrakk>\<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<forall>x\<in>snd ` set txs. x \<notin> FvarsT s; \<forall>t\<in>fst ` set txs. y \<notin> FvarsT t; distinct (map snd txs); s \<in> trm; y \<in> var; y \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) txs = rawpsubst \<phi> (txs @ [(s, y)]); \<phi> \<in> fmla; snd ` set (a # txs) \<subseteq> var; fst ` set (a # txs) \<subseteq> trm; \<forall>x\<in>snd ` set (a # txs). x \<notin> FvarsT s; \<forall>t\<in>fst ` set (a # txs). y \<notin> FvarsT t; distinct (map snd (a # txs)); s \<in> trm; y \<in> var; y \<notin> snd ` set (a # txs)\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) (a # txs) = rawpsubst \<phi> ((a # txs) @ [(s, y)])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rawpsubst \<phi> [(s, y), (t, x)] = rawpsubst \<phi> [(t, x), (s, y)]

goal (2 subgoals):
 1. \<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set [] \<subseteq> var; fst ` set [] \<subseteq> trm; \<forall>x\<in>snd ` set []. x \<notin> FvarsT s; \<forall>t\<in>fst ` set []. y \<notin> FvarsT t; distinct (map snd []); s \<in> trm; y \<in> var; y \<notin> snd ` set []\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) [] = rawpsubst \<phi> ([] @ [(s, y)])
 2. \<And>a txs \<phi> s y. \<lbrakk>\<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<forall>x\<in>snd ` set txs. x \<notin> FvarsT s; \<forall>t\<in>fst ` set txs. y \<notin> FvarsT t; distinct (map snd txs); s \<in> trm; y \<in> var; y \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) txs = rawpsubst \<phi> (txs @ [(s, y)]); \<phi> \<in> fmla; snd ` set (a # txs) \<subseteq> var; fst ` set (a # txs) \<subseteq> trm; \<forall>x\<in>snd ` set (a # txs). x \<notin> FvarsT s; \<forall>t\<in>fst ` set (a # txs). y \<notin> FvarsT t; distinct (map snd (a # txs)); s \<in> trm; y \<in> var; y \<notin> snd ` set (a # txs)\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) (a # txs) = rawpsubst \<phi> ((a # txs) @ [(s, y)])
[PROOF STEP]
have "rawpsubst (rawpsubst \<phi> [(t, x),(s, y)]) txs = rawpsubst \<phi> ([(t, x),(s, y)] @ txs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rawpsubst (rawpsubst \<phi> [(t, x), (s, y)]) txs = rawpsubst \<phi> ([(t, x), (s, y)] @ txs)
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<forall>x\<in>snd ` set txs. x \<notin> FvarsT ?s; \<forall>t\<in>fst ` set txs. ?y \<notin> FvarsT t; distinct (map snd txs); ?s \<in> trm; ?y \<in> var; ?y \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> rawpsubst (subst ?\<phi> ?s ?y) txs = rawpsubst ?\<phi> (txs @ [(?s, ?y)])
\<phi> \<in> fmla
snd ` set (tx # txs) \<subseteq> var
fst ` set (tx # txs) \<subseteq> trm
\<forall>x\<in>snd ` set (tx # txs). x \<notin> FvarsT s
\<forall>t\<in>fst ` set (tx # txs). y \<notin> FvarsT t
distinct (map snd (tx # txs))
s \<in> trm
y \<in> var
y \<notin> snd ` set (tx # txs)

goal (1 subgoal):
 1. rawpsubst (rawpsubst \<phi> [(t, x), (s, y)]) txs = rawpsubst \<phi> ([(t, x), (s, y)] @ txs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rawpsubst (rawpsubst \<phi> [(t, x), (s, y)]) txs = rawpsubst \<phi> ([(t, x), (s, y)] @ txs)

goal (2 subgoals):
 1. \<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set [] \<subseteq> var; fst ` set [] \<subseteq> trm; \<forall>x\<in>snd ` set []. x \<notin> FvarsT s; \<forall>t\<in>fst ` set []. y \<notin> FvarsT t; distinct (map snd []); s \<in> trm; y \<in> var; y \<notin> snd ` set []\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) [] = rawpsubst \<phi> ([] @ [(s, y)])
 2. \<And>a txs \<phi> s y. \<lbrakk>\<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<forall>x\<in>snd ` set txs. x \<notin> FvarsT s; \<forall>t\<in>fst ` set txs. y \<notin> FvarsT t; distinct (map snd txs); s \<in> trm; y \<in> var; y \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) txs = rawpsubst \<phi> (txs @ [(s, y)]); \<phi> \<in> fmla; snd ` set (a # txs) \<subseteq> var; fst ` set (a # txs) \<subseteq> trm; \<forall>x\<in>snd ` set (a # txs). x \<notin> FvarsT s; \<forall>t\<in>fst ` set (a # txs). y \<notin> FvarsT t; distinct (map snd (a # txs)); s \<in> trm; y \<in> var; y \<notin> snd ` set (a # txs)\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) (a # txs) = rawpsubst \<phi> ((a # txs) @ [(s, y)])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rawpsubst (rawpsubst \<phi> [(t, x), (s, y)]) txs = rawpsubst \<phi> ([(t, x), (s, y)] @ txs)

goal (2 subgoals):
 1. \<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set [] \<subseteq> var; fst ` set [] \<subseteq> trm; \<forall>x\<in>snd ` set []. x \<notin> FvarsT s; \<forall>t\<in>fst ` set []. y \<notin> FvarsT t; distinct (map snd []); s \<in> trm; y \<in> var; y \<notin> snd ` set []\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) [] = rawpsubst \<phi> ([] @ [(s, y)])
 2. \<And>a txs \<phi> s y. \<lbrakk>\<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<forall>x\<in>snd ` set txs. x \<notin> FvarsT s; \<forall>t\<in>fst ` set txs. y \<notin> FvarsT t; distinct (map snd txs); s \<in> trm; y \<in> var; y \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) txs = rawpsubst \<phi> (txs @ [(s, y)]); \<phi> \<in> fmla; snd ` set (a # txs) \<subseteq> var; fst ` set (a # txs) \<subseteq> trm; \<forall>x\<in>snd ` set (a # txs). x \<notin> FvarsT s; \<forall>t\<in>fst ` set (a # txs). y \<notin> FvarsT t; distinct (map snd (a # txs)); s \<in> trm; y \<in> var; y \<notin> snd ` set (a # txs)\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) (a # txs) = rawpsubst \<phi> ((a # txs) @ [(s, y)])
[PROOF STEP]
have "\<dots> = rawpsubst (subst \<phi> t x) (txs @ [(s,y)])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rawpsubst \<phi> ([(t, x), (s, y)] @ txs) = rawpsubst (subst \<phi> t x) (txs @ [(s, y)])
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<forall>x\<in>snd ` set txs. x \<notin> FvarsT ?s; \<forall>t\<in>fst ` set txs. ?y \<notin> FvarsT t; distinct (map snd txs); ?s \<in> trm; ?y \<in> var; ?y \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> rawpsubst (subst ?\<phi> ?s ?y) txs = rawpsubst ?\<phi> (txs @ [(?s, ?y)])
\<phi> \<in> fmla
snd ` set (tx # txs) \<subseteq> var
fst ` set (tx # txs) \<subseteq> trm
\<forall>x\<in>snd ` set (tx # txs). x \<notin> FvarsT s
\<forall>t\<in>fst ` set (tx # txs). y \<notin> FvarsT t
distinct (map snd (tx # txs))
s \<in> trm
y \<in> var
y \<notin> snd ` set (tx # txs)

goal (1 subgoal):
 1. rawpsubst \<phi> ([(t, x), (s, y)] @ txs) = rawpsubst (subst \<phi> t x) (txs @ [(s, y)])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rawpsubst \<phi> ([(t, x), (s, y)] @ txs) = rawpsubst (subst \<phi> t x) (txs @ [(s, y)])

goal (2 subgoals):
 1. \<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set [] \<subseteq> var; fst ` set [] \<subseteq> trm; \<forall>x\<in>snd ` set []. x \<notin> FvarsT s; \<forall>t\<in>fst ` set []. y \<notin> FvarsT t; distinct (map snd []); s \<in> trm; y \<in> var; y \<notin> snd ` set []\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) [] = rawpsubst \<phi> ([] @ [(s, y)])
 2. \<And>a txs \<phi> s y. \<lbrakk>\<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<forall>x\<in>snd ` set txs. x \<notin> FvarsT s; \<forall>t\<in>fst ` set txs. y \<notin> FvarsT t; distinct (map snd txs); s \<in> trm; y \<in> var; y \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) txs = rawpsubst \<phi> (txs @ [(s, y)]); \<phi> \<in> fmla; snd ` set (a # txs) \<subseteq> var; fst ` set (a # txs) \<subseteq> trm; \<forall>x\<in>snd ` set (a # txs). x \<notin> FvarsT s; \<forall>t\<in>fst ` set (a # txs). y \<notin> FvarsT t; distinct (map snd (a # txs)); s \<in> trm; y \<in> var; y \<notin> snd ` set (a # txs)\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) (a # txs) = rawpsubst \<phi> ((a # txs) @ [(s, y)])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rawpsubst \<phi> ([(t, x), (s, y)] @ txs) = rawpsubst (subst \<phi> t x) (txs @ [(s, y)])

goal (2 subgoals):
 1. \<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set [] \<subseteq> var; fst ` set [] \<subseteq> trm; \<forall>x\<in>snd ` set []. x \<notin> FvarsT s; \<forall>t\<in>fst ` set []. y \<notin> FvarsT t; distinct (map snd []); s \<in> trm; y \<in> var; y \<notin> snd ` set []\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) [] = rawpsubst \<phi> ([] @ [(s, y)])
 2. \<And>a txs \<phi> s y. \<lbrakk>\<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<forall>x\<in>snd ` set txs. x \<notin> FvarsT s; \<forall>t\<in>fst ` set txs. y \<notin> FvarsT t; distinct (map snd txs); s \<in> trm; y \<in> var; y \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) txs = rawpsubst \<phi> (txs @ [(s, y)]); \<phi> \<in> fmla; snd ` set (a # txs) \<subseteq> var; fst ` set (a # txs) \<subseteq> trm; \<forall>x\<in>snd ` set (a # txs). x \<notin> FvarsT s; \<forall>t\<in>fst ` set (a # txs). y \<notin> FvarsT t; distinct (map snd (a # txs)); s \<in> trm; y \<in> var; y \<notin> snd ` set (a # txs)\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) (a # txs) = rawpsubst \<phi> ((a # txs) @ [(s, y)])
[PROOF STEP]
have "\<dots> = rawpsubst \<phi> (((t, x) # txs) @ [(s, y)])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rawpsubst (subst \<phi> t x) (txs @ [(s, y)]) = rawpsubst \<phi> (((t, x) # txs) @ [(s, y)])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rawpsubst (subst \<phi> t x) (txs @ [(s, y)]) = rawpsubst \<phi> (((t, x) # txs) @ [(s, y)])

goal (2 subgoals):
 1. \<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set [] \<subseteq> var; fst ` set [] \<subseteq> trm; \<forall>x\<in>snd ` set []. x \<notin> FvarsT s; \<forall>t\<in>fst ` set []. y \<notin> FvarsT t; distinct (map snd []); s \<in> trm; y \<in> var; y \<notin> snd ` set []\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) [] = rawpsubst \<phi> ([] @ [(s, y)])
 2. \<And>a txs \<phi> s y. \<lbrakk>\<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<forall>x\<in>snd ` set txs. x \<notin> FvarsT s; \<forall>t\<in>fst ` set txs. y \<notin> FvarsT t; distinct (map snd txs); s \<in> trm; y \<in> var; y \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) txs = rawpsubst \<phi> (txs @ [(s, y)]); \<phi> \<in> fmla; snd ` set (a # txs) \<subseteq> var; fst ` set (a # txs) \<subseteq> trm; \<forall>x\<in>snd ` set (a # txs). x \<notin> FvarsT s; \<forall>t\<in>fst ` set (a # txs). y \<notin> FvarsT t; distinct (map snd (a # txs)); s \<in> trm; y \<in> var; y \<notin> snd ` set (a # txs)\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) (a # txs) = rawpsubst \<phi> ((a # txs) @ [(s, y)])
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
rawpsubst \<phi> ((s, y) # (t, x) # txs) = rawpsubst \<phi> (((t, x) # txs) @ [(s, y)])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
rawpsubst \<phi> ((s, y) # (t, x) # txs) = rawpsubst \<phi> (((t, x) # txs) @ [(s, y)])

goal (1 subgoal):
 1. rawpsubst (subst \<phi> s y) (tx # txs) = rawpsubst \<phi> ((tx # txs) @ [(s, y)])
[PROOF STEP]
unfolding tx
[PROOF STATE]
proof (prove)
using this:
rawpsubst \<phi> ((s, y) # (t, x) # txs) = rawpsubst \<phi> (((t, x) # txs) @ [(s, y)])

goal (1 subgoal):
 1. rawpsubst (subst \<phi> s y) ((t, x) # txs) = rawpsubst \<phi> (((t, x) # txs) @ [(s, y)])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rawpsubst (subst \<phi> s y) (tx # txs) = rawpsubst \<phi> ((tx # txs) @ [(s, y)])

goal (1 subgoal):
 1. \<And>\<phi> s y. \<lbrakk>\<phi> \<in> fmla; snd ` set [] \<subseteq> var; fst ` set [] \<subseteq> trm; \<forall>x\<in>snd ` set []. x \<notin> FvarsT s; \<forall>t\<in>fst ` set []. y \<notin> FvarsT t; distinct (map snd []); s \<in> trm; y \<in> var; y \<notin> snd ` set []\<rbrakk> \<Longrightarrow> rawpsubst (subst \<phi> s y) [] = rawpsubst \<phi> ([] @ [(s, y)])
[PROOF STEP]
qed auto