[STATEMENT]
lemma exists_disjoint_vars:
  fixes Q1 Q2 :: ppolynomial
  fixes A :: relation
  assumes "is_dioph_rel A"
  shows "\<exists>P1 P2. disjoint_var (P1 \<^bold>+ P2) (Q1 \<^bold>+ Q2)
                \<and> (\<forall>a. eval A a \<longleftrightarrow> (\<exists>v. ppeval P1 a v = ppeval P2 a v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P1 P2. disjoint_var (P1 \<^bold>+ P2) (Q1 \<^bold>+ Q2) \<and> (\<forall>a. eval A a = (\<exists>v. ppeval P1 a v = ppeval P2 a v))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1 P2. disjoint_var (P1 \<^bold>+ P2) (Q1 \<^bold>+ Q2) \<and> (\<forall>a. eval A a = (\<exists>v. ppeval P1 a v = ppeval P2 a v))
[PROOF STEP]
obtain P1 P2 where p_defs: "\<forall>a. eval A a \<longleftrightarrow> (\<exists>v. ppeval P1 a v = ppeval P2 a v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P1 P2. \<forall>a. eval A a = (\<exists>v. ppeval P1 a v = ppeval P2 a v) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms is_dioph_rel_def
[PROOF STATE]
proof (prove)
using this:
is_dioph_rel A
is_dioph_rel ?DR = (\<exists>P\<^sub>1 P\<^sub>2. \<forall>a. eval ?DR a = (\<exists>v. ppeval P\<^sub>1 a v = ppeval P\<^sub>2 a v))

goal (1 subgoal):
 1. (\<And>P1 P2. \<forall>a. eval A a = (\<exists>v. ppeval P1 a v = ppeval P2 a v) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>a. eval A a = (\<exists>v. ppeval P1 a v = ppeval P2 a v)

goal (1 subgoal):
 1. \<exists>P1 P2. disjoint_var (P1 \<^bold>+ P2) (Q1 \<^bold>+ Q2) \<and> (\<forall>a. eval A a = (\<exists>v. ppeval P1 a v = ppeval P2 a v))
[PROOF STEP]
define n::nat where "n \<equiv> Max (var_set (Q1 \<^bold>+ Q2))"
[PROOF STATE]
proof (state)
this:
n \<equiv> Max (var_set (Q1 \<^bold>+ Q2))

goal (1 subgoal):
 1. \<exists>P1 P2. disjoint_var (P1 \<^bold>+ P2) (Q1 \<^bold>+ Q2) \<and> (\<forall>a. eval A a = (\<exists>v. ppeval P1 a v = ppeval P2 a v))
[PROOF STEP]
define P1' P2' where p'_defs: "P1' \<equiv> push_var P1 (Suc n)" "P2' \<equiv> push_var P2 (Suc n)"
[PROOF STATE]
proof (state)
this:
P1' \<equiv> push_var P1 (Suc n)
P2' \<equiv> push_var P2 (Suc n)

goal (1 subgoal):
 1. \<exists>P1 P2. disjoint_var (P1 \<^bold>+ P2) (Q1 \<^bold>+ Q2) \<and> (\<forall>a. eval A a = (\<exists>v. ppeval P1 a v = ppeval P2 a v))
[PROOF STEP]
have "disjoint_var (P1' \<^bold>+ P2') (Q1 \<^bold>+ Q2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. disjoint_var (P1' \<^bold>+ P2') (Q1 \<^bold>+ Q2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. disjoint_var (P1' \<^bold>+ P2') (Q1 \<^bold>+ Q2)
[PROOF STEP]
have "finite (var_set (Q1 \<^bold>+ Q2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (var_set (Q1 \<^bold>+ Q2))
[PROOF STEP]
apply (induction Q1, auto)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite (var_set Q2)
 2. finite (var_set Q2)
 3. finite (var_set Q2)
[PROOF STEP]
by (induction Q2, auto)+
[PROOF STATE]
proof (state)
this:
finite (var_set (Q1 \<^bold>+ Q2))

goal (1 subgoal):
 1. disjoint_var (P1' \<^bold>+ P2') (Q1 \<^bold>+ Q2)
[PROOF STEP]
hence "\<forall>x \<in> var_set (Q1 \<^bold>+ Q2). x \<le> n"
[PROOF STATE]
proof (prove)
using this:
finite (var_set (Q1 \<^bold>+ Q2))

goal (1 subgoal):
 1. \<forall>x\<in>var_set (Q1 \<^bold>+ Q2). x \<le> n
[PROOF STEP]
unfolding n_def
[PROOF STATE]
proof (prove)
using this:
finite (var_set (Q1 \<^bold>+ Q2))

goal (1 subgoal):
 1. \<forall>x\<in>var_set (Q1 \<^bold>+ Q2). x \<le> Max (var_set (Q1 \<^bold>+ Q2))
[PROOF STEP]
using Max.coboundedI
[PROOF STATE]
proof (prove)
using this:
finite (var_set (Q1 \<^bold>+ Q2))
\<lbrakk>finite ?A; ?a \<in> ?A\<rbrakk> \<Longrightarrow> ?a \<le> Max ?A

goal (1 subgoal):
 1. \<forall>x\<in>var_set (Q1 \<^bold>+ Q2). x \<le> Max (var_set (Q1 \<^bold>+ Q2))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>var_set (Q1 \<^bold>+ Q2). x \<le> n

goal (1 subgoal):
 1. disjoint_var (P1' \<^bold>+ P2') (Q1 \<^bold>+ Q2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>var_set (Q1 \<^bold>+ Q2). x \<le> n

goal (1 subgoal):
 1. disjoint_var (P1' \<^bold>+ P2') (Q1 \<^bold>+ Q2)
[PROOF STEP]
have "\<forall>x \<in> var_set (P1' \<^bold>+ P2'). x > n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>var_set (P1' \<^bold>+ P2'). n < x
[PROOF STEP]
unfolding p'_defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>var_set (push_var P1 (Suc n) \<^bold>+ push_var P2 (Suc n)). n < x
[PROOF STEP]
using push_var_bound
[PROOF STATE]
proof (prove)
using this:
?x \<in> var_set (push_var ?P (Suc ?n)) \<Longrightarrow> ?n < ?x

goal (1 subgoal):
 1. \<forall>x\<in>var_set (push_var P1 (Suc n) \<^bold>+ push_var P2 (Suc n)). n < x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>var_set (P1' \<^bold>+ P2'). n < x

goal (1 subgoal):
 1. disjoint_var (P1' \<^bold>+ P2') (Q1 \<^bold>+ Q2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>var_set (Q1 \<^bold>+ Q2). x \<le> n
\<forall>x\<in>var_set (P1' \<^bold>+ P2'). n < x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>var_set (Q1 \<^bold>+ Q2). x \<le> n
\<forall>x\<in>var_set (P1' \<^bold>+ P2'). n < x

goal (1 subgoal):
 1. disjoint_var (P1' \<^bold>+ P2') (Q1 \<^bold>+ Q2)
[PROOF STEP]
unfolding disjoint_var_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>var_set (Q1 \<^bold>+ Q2). x \<le> n
\<forall>x\<in>var_set (P1' \<^bold>+ P2'). n < x

goal (1 subgoal):
 1. var_set (P1' \<^bold>+ P2') \<inter> var_set (Q1 \<^bold>+ Q2) = {}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
disjoint_var (P1' \<^bold>+ P2') (Q1 \<^bold>+ Q2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
disjoint_var (P1' \<^bold>+ P2') (Q1 \<^bold>+ Q2)

goal (1 subgoal):
 1. \<exists>P1 P2. disjoint_var (P1 \<^bold>+ P2) (Q1 \<^bold>+ Q2) \<and> (\<forall>a. eval A a = (\<exists>v. ppeval P1 a v = ppeval P2 a v))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
disjoint_var (P1' \<^bold>+ P2') (Q1 \<^bold>+ Q2)

goal (1 subgoal):
 1. \<exists>P1 P2. disjoint_var (P1 \<^bold>+ P2) (Q1 \<^bold>+ Q2) \<and> (\<forall>a. eval A a = (\<exists>v. ppeval P1 a v = ppeval P2 a v))
[PROOF STEP]
have "\<forall>a. eval A a \<longleftrightarrow> (\<exists>v. ppeval P1' a v = ppeval P2' a v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a. eval A a = (\<exists>v. ppeval P1' a v = ppeval P2' a v)
[PROOF STEP]
unfolding p'_defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a. eval A a = (\<exists>v. ppeval (push_var P1 (Suc n)) a v = ppeval (push_var P2 (Suc n)) a v)
[PROOF STEP]
apply (auto simp add: p_defs push_var_pull_assignment pull_assignment_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a v. ppeval P1 a v = ppeval P2 a v \<Longrightarrow> \<exists>v. ppeval P1 a (\<lambda>x. v (Suc (x + n))) = ppeval P2 a (\<lambda>x. v (Suc (x + n)))
[PROOF STEP]
subgoal for a v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ppeval P1 a v = ppeval P2 a v \<Longrightarrow> \<exists>v. ppeval P1 a (\<lambda>x. v (Suc (x + n))) = ppeval P2 a (\<lambda>x. v (Suc (x + n)))
[PROOF STEP]
by (rule exI[of _ "\<lambda>i. v (i - Suc n)"]) auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<forall>a. eval A a = (\<exists>v. ppeval P1' a v = ppeval P2' a v)

goal (1 subgoal):
 1. \<exists>P1 P2. disjoint_var (P1 \<^bold>+ P2) (Q1 \<^bold>+ Q2) \<and> (\<forall>a. eval A a = (\<exists>v. ppeval P1 a v = ppeval P2 a v))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
disjoint_var (P1' \<^bold>+ P2') (Q1 \<^bold>+ Q2)
\<forall>a. eval A a = (\<exists>v. ppeval P1' a v = ppeval P2' a v)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
disjoint_var (P1' \<^bold>+ P2') (Q1 \<^bold>+ Q2)
\<forall>a. eval A a = (\<exists>v. ppeval P1' a v = ppeval P2' a v)

goal (1 subgoal):
 1. \<exists>P1 P2. disjoint_var (P1 \<^bold>+ P2) (Q1 \<^bold>+ Q2) \<and> (\<forall>a. eval A a = (\<exists>v. ppeval P1 a v = ppeval P2 a v))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>P1 P2. disjoint_var (P1 \<^bold>+ P2) (Q1 \<^bold>+ Q2) \<and> (\<forall>a. eval A a = (\<exists>v. ppeval P1 a v = ppeval P2 a v))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma and_dioph:
  assumes "is_dioph_rel A" and "is_dioph_rel B"
  shows "is_dioph_rel (A [\<and>] B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel (A [\<and>] B)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_dioph_rel (A [\<and>] B)
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
is_dioph_rel A
[PROOF STEP]
obtain PA1 PA2 where PA: "\<forall>a. (eval A a) \<longleftrightarrow> (\<exists>v. ppeval PA1 a v = ppeval PA2 a v)"
[PROOF STATE]
proof (prove)
using this:
is_dioph_rel A

goal (1 subgoal):
 1. (\<And>PA1 PA2. \<forall>a. eval A a = (\<exists>v. ppeval PA1 a v = ppeval PA2 a v) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: is_dioph_rel_def)
[PROOF STATE]
proof (state)
this:
\<forall>a. eval A a = (\<exists>v. ppeval PA1 a v = ppeval PA2 a v)

goal (1 subgoal):
 1. is_dioph_rel (A [\<and>] B)
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
is_dioph_rel B
[PROOF STEP]
obtain PB1 PB2 where disj: "disjoint_var (PB1 \<^bold>+ PB2) (PA1 \<^bold>+ PA2)"
                                   and PB: "(\<forall>a. eval B a \<longleftrightarrow> (\<exists>v. ppeval PB1 a v = ppeval PB2 a v))"
[PROOF STATE]
proof (prove)
using this:
is_dioph_rel B

goal (1 subgoal):
 1. (\<And>PB1 PB2. \<lbrakk>disjoint_var (PB1 \<^bold>+ PB2) (PA1 \<^bold>+ PA2); \<forall>a. eval B a = (\<exists>v. ppeval PB1 a v = ppeval PB2 a v)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using exists_disjoint_vars[of B]
[PROOF STATE]
proof (prove)
using this:
is_dioph_rel B
is_dioph_rel B \<Longrightarrow> \<exists>P1 P2. disjoint_var (P1 \<^bold>+ P2) (?Q1.0 \<^bold>+ ?Q2.0) \<and> (\<forall>a. eval B a = (\<exists>v. ppeval P1 a v = ppeval P2 a v))

goal (1 subgoal):
 1. (\<And>PB1 PB2. \<lbrakk>disjoint_var (PB1 \<^bold>+ PB2) (PA1 \<^bold>+ PA2); \<forall>a. eval B a = (\<exists>v. ppeval PB1 a v = ppeval PB2 a v)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
disjoint_var (PB1 \<^bold>+ PB2) (PA1 \<^bold>+ PA2)
\<forall>a. eval B a = (\<exists>v. ppeval PB1 a v = ppeval PB2 a v)

goal (1 subgoal):
 1. is_dioph_rel (A [\<and>] B)
[PROOF STEP]
from disjoint_var_unifies
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<exists>v1. ppeval ?P1.0 ?a v1 = ppeval ?P2.0 ?a v1; \<exists>v2. ppeval ?Q1.0 ?a v2 = ppeval ?Q2.0 ?a v2; disjoint_var (?P1.0 \<^bold>+ ?P2.0) (?Q1.0 \<^bold>+ ?Q2.0)\<rbrakk> \<Longrightarrow> \<exists>v. ppeval ?P1.0 ?a v = ppeval ?P2.0 ?a v \<and> ppeval ?Q1.0 ?a v = ppeval ?Q2.0 ?a v
[PROOF STEP]
have unified: "\<forall>a. (eval (A [\<and>] B) a)
                        \<longleftrightarrow> (\<exists>v. ppeval PA1 a v = ppeval PA2 a v \<and> ppeval PB1 a v = ppeval PB2 a v)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<exists>v1. ppeval ?P1.0 ?a v1 = ppeval ?P2.0 ?a v1; \<exists>v2. ppeval ?Q1.0 ?a v2 = ppeval ?Q2.0 ?a v2; disjoint_var (?P1.0 \<^bold>+ ?P2.0) (?Q1.0 \<^bold>+ ?Q2.0)\<rbrakk> \<Longrightarrow> \<exists>v. ppeval ?P1.0 ?a v = ppeval ?P2.0 ?a v \<and> ppeval ?Q1.0 ?a v = ppeval ?Q2.0 ?a v

goal (1 subgoal):
 1. \<forall>a. eval (A [\<and>] B) a = (\<exists>v. ppeval PA1 a v = ppeval PA2 a v \<and> ppeval PB1 a v = ppeval PB2 a v)
[PROOF STEP]
using PA PB disj disjoint_var_sym
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<exists>v1. ppeval ?P1.0 ?a v1 = ppeval ?P2.0 ?a v1; \<exists>v2. ppeval ?Q1.0 ?a v2 = ppeval ?Q2.0 ?a v2; disjoint_var (?P1.0 \<^bold>+ ?P2.0) (?Q1.0 \<^bold>+ ?Q2.0)\<rbrakk> \<Longrightarrow> \<exists>v. ppeval ?P1.0 ?a v = ppeval ?P2.0 ?a v \<and> ppeval ?Q1.0 ?a v = ppeval ?Q2.0 ?a v
\<forall>a. eval A a = (\<exists>v. ppeval PA1 a v = ppeval PA2 a v)
\<forall>a. eval B a = (\<exists>v. ppeval PB1 a v = ppeval PB2 a v)
disjoint_var (PB1 \<^bold>+ PB2) (PA1 \<^bold>+ PA2)
disjoint_var ?P ?Q = disjoint_var ?Q ?P

goal (1 subgoal):
 1. \<forall>a. eval (A [\<and>] B) a = (\<exists>v. ppeval PA1 a v = ppeval PA2 a v \<and> ppeval PB1 a v = ppeval PB2 a v)
[PROOF STEP]
by simp blast
[PROOF STATE]
proof (state)
this:
\<forall>a. eval (A [\<and>] B) a = (\<exists>v. ppeval PA1 a v = ppeval PA2 a v \<and> ppeval PB1 a v = ppeval PB2 a v)

goal (1 subgoal):
 1. is_dioph_rel (A [\<and>] B)
[PROOF STEP]
(* AND means (A1 - A2)^2 + (B1 - B2)^2 = 0
     Rewrite as A1^2 + A2^2 + B1^2 + B2^2 = 2*A1*A2 + 2*B1*B2 to eliminate subtraction. *)
[PROOF STATE]
proof (state)
this:
\<forall>a. eval (A [\<and>] B) a = (\<exists>v. ppeval PA1 a v = ppeval PA2 a v \<and> ppeval PB1 a v = ppeval PB2 a v)

goal (1 subgoal):
 1. is_dioph_rel (A [\<and>] B)
[PROOF STEP]
have h0: "p1 = p2 \<longleftrightarrow> p1^2 + p2^2 = 2*p1*p2" for p1 p2 :: nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p1 = p2) = (p1\<^sup>2 + p2\<^sup>2 = 2 * p1 * p2)
[PROOF STEP]
apply (auto simp: algebra_simps power2_eq_square)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p1 * p1 + p2 * p2 = p1 * (p2 * 2) \<Longrightarrow> p1 = p2
[PROOF STEP]
using crossproduct_eq
[PROOF STATE]
proof (prove)
using this:
(?w * ?y + ?x * ?z = ?w * ?z + ?x * ?y) = (?w = ?x \<or> ?y = ?z)

goal (1 subgoal):
 1. p1 * p1 + p2 * p2 = p1 * (p2 * 2) \<Longrightarrow> p1 = p2
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(?p1.0 = ?p2.0) = (?p1.0\<^sup>2 + ?p2.0\<^sup>2 = 2 * ?p1.0 * ?p2.0)

goal (1 subgoal):
 1. is_dioph_rel (A [\<and>] B)
[PROOF STEP]
have "p1 = p2 \<and> q1 = q2 \<longleftrightarrow> p1^2 + p2^2 + q1^2 + q2^2 = 2*p1*p2 + 2*q1*q2" for p1 p2 q1 q2 :: nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p1 = p2 \<and> q1 = q2) = (p1\<^sup>2 + p2\<^sup>2 + q1\<^sup>2 + q2\<^sup>2 = 2 * p1 * p2 + 2 * q1 * q2)
[PROOF STEP]
proof (rule)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p1 = p2 \<and> q1 = q2 \<Longrightarrow> p1\<^sup>2 + p2\<^sup>2 + q1\<^sup>2 + q2\<^sup>2 = 2 * p1 * p2 + 2 * q1 * q2
 2. p1\<^sup>2 + p2\<^sup>2 + q1\<^sup>2 + q2\<^sup>2 = 2 * p1 * p2 + 2 * q1 * q2 \<Longrightarrow> p1 = p2 \<and> q1 = q2
[PROOF STEP]
assume "p1 = p2 \<and> q1 = q2"
[PROOF STATE]
proof (state)
this:
p1 = p2 \<and> q1 = q2

goal (2 subgoals):
 1. p1 = p2 \<and> q1 = q2 \<Longrightarrow> p1\<^sup>2 + p2\<^sup>2 + q1\<^sup>2 + q2\<^sup>2 = 2 * p1 * p2 + 2 * q1 * q2
 2. p1\<^sup>2 + p2\<^sup>2 + q1\<^sup>2 + q2\<^sup>2 = 2 * p1 * p2 + 2 * q1 * q2 \<Longrightarrow> p1 = p2 \<and> q1 = q2
[PROOF STEP]
thus "p1\<^sup>2 + p2\<^sup>2 + q1\<^sup>2 + q2\<^sup>2 = 2 * p1 * p2 + 2 * q1 * q2"
[PROOF STATE]
proof (prove)
using this:
p1 = p2 \<and> q1 = q2

goal (1 subgoal):
 1. p1\<^sup>2 + p2\<^sup>2 + q1\<^sup>2 + q2\<^sup>2 = 2 * p1 * p2 + 2 * q1 * q2
[PROOF STEP]
by (auto simp: algebra_simps power2_eq_square)
[PROOF STATE]
proof (state)
this:
p1\<^sup>2 + p2\<^sup>2 + q1\<^sup>2 + q2\<^sup>2 = 2 * p1 * p2 + 2 * q1 * q2

goal (1 subgoal):
 1. p1\<^sup>2 + p2\<^sup>2 + q1\<^sup>2 + q2\<^sup>2 = 2 * p1 * p2 + 2 * q1 * q2 \<Longrightarrow> p1 = p2 \<and> q1 = q2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p1\<^sup>2 + p2\<^sup>2 + q1\<^sup>2 + q2\<^sup>2 = 2 * p1 * p2 + 2 * q1 * q2 \<Longrightarrow> p1 = p2 \<and> q1 = q2
[PROOF STEP]
assume "p1\<^sup>2 + p2\<^sup>2 + q1\<^sup>2 + q2\<^sup>2 = 2 * p1 * p2 + 2 * q1 * q2"
[PROOF STATE]
proof (state)
this:
p1\<^sup>2 + p2\<^sup>2 + q1\<^sup>2 + q2\<^sup>2 = 2 * p1 * p2 + 2 * q1 * q2

goal (1 subgoal):
 1. p1\<^sup>2 + p2\<^sup>2 + q1\<^sup>2 + q2\<^sup>2 = 2 * p1 * p2 + 2 * q1 * q2 \<Longrightarrow> p1 = p2 \<and> q1 = q2
[PROOF STEP]
hence "(int p1)\<^sup>2 + (int p2)\<^sup>2 + (int q1)\<^sup>2 + (int q2)\<^sup>2 - 2 * int p1 * int p2 - 2 * int q1 * int q2 = 0"
[PROOF STATE]
proof (prove)
using this:
p1\<^sup>2 + p2\<^sup>2 + q1\<^sup>2 + q2\<^sup>2 = 2 * p1 * p2 + 2 * q1 * q2

goal (1 subgoal):
 1. (int p1)\<^sup>2 + (int p2)\<^sup>2 + (int q1)\<^sup>2 + (int q2)\<^sup>2 - 2 * int p1 * int p2 - 2 * int q1 * int q2 = 0
[PROOF STEP]
by (auto) (smt (verit, best) mult_2 of_nat_add of_nat_mult power2_eq_square)
[PROOF STATE]
proof (state)
this:
(int p1)\<^sup>2 + (int p2)\<^sup>2 + (int q1)\<^sup>2 + (int q2)\<^sup>2 - 2 * int p1 * int p2 - 2 * int q1 * int q2 = 0

goal (1 subgoal):
 1. p1\<^sup>2 + p2\<^sup>2 + q1\<^sup>2 + q2\<^sup>2 = 2 * p1 * p2 + 2 * q1 * q2 \<Longrightarrow> p1 = p2 \<and> q1 = q2
[PROOF STEP]
hence "(int p1 - int p2)^2 + (int q1 - int q2)^2 = 0"
[PROOF STATE]
proof (prove)
using this:
(int p1)\<^sup>2 + (int p2)\<^sup>2 + (int q1)\<^sup>2 + (int q2)\<^sup>2 - 2 * int p1 * int p2 - 2 * int q1 * int q2 = 0

goal (1 subgoal):
 1. (int p1 - int p2)\<^sup>2 + (int q1 - int q2)\<^sup>2 = 0
[PROOF STEP]
by (simp add: power2_diff)
[PROOF STATE]
proof (state)
this:
(int p1 - int p2)\<^sup>2 + (int q1 - int q2)\<^sup>2 = 0

goal (1 subgoal):
 1. p1\<^sup>2 + p2\<^sup>2 + q1\<^sup>2 + q2\<^sup>2 = 2 * p1 * p2 + 2 * q1 * q2 \<Longrightarrow> p1 = p2 \<and> q1 = q2
[PROOF STEP]
hence "int p1 = int p2" and "int q1 = int q2"
[PROOF STATE]
proof (prove)
using this:
(int p1 - int p2)\<^sup>2 + (int q1 - int q2)\<^sup>2 = 0

goal (1 subgoal):
 1. int p1 = int p2 &&& int q1 = int q2
[PROOF STEP]
by (simp add: sum_power2_eq_zero_iff)+
[PROOF STATE]
proof (state)
this:
int p1 = int p2
int q1 = int q2

goal (1 subgoal):
 1. p1\<^sup>2 + p2\<^sup>2 + q1\<^sup>2 + q2\<^sup>2 = 2 * p1 * p2 + 2 * q1 * q2 \<Longrightarrow> p1 = p2 \<and> q1 = q2
[PROOF STEP]
thus "p1 = p2 \<and> q1 = q2"
[PROOF STATE]
proof (prove)
using this:
int p1 = int p2
int q1 = int q2

goal (1 subgoal):
 1. p1 = p2 \<and> q1 = q2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p1 = p2 \<and> q1 = q2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(?p1.0 = ?p2.0 \<and> ?q1.0 = ?q2.0) = (?p1.0\<^sup>2 + ?p2.0\<^sup>2 + ?q1.0\<^sup>2 + ?q2.0\<^sup>2 = 2 * ?p1.0 * ?p2.0 + 2 * ?q1.0 * ?q2.0)

goal (1 subgoal):
 1. is_dioph_rel (A [\<and>] B)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(?p1.0 = ?p2.0 \<and> ?q1.0 = ?q2.0) = (?p1.0\<^sup>2 + ?p2.0\<^sup>2 + ?q1.0\<^sup>2 + ?q2.0\<^sup>2 = 2 * ?p1.0 * ?p2.0 + 2 * ?q1.0 * ?q2.0)

goal (1 subgoal):
 1. is_dioph_rel (A [\<and>] B)
[PROOF STEP]
apply (simp only: is_dioph_rel_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p1 p2 q1 q2. (p1 = p2 \<and> q1 = q2) = (p1\<^sup>2 + p2\<^sup>2 + q1\<^sup>2 + q2\<^sup>2 = 2 * p1 * p2 + 2 * q1 * q2)) \<Longrightarrow> \<exists>P\<^sub>1 P\<^sub>2. \<forall>a. eval (A [\<and>] B) a = (\<exists>v. ppeval P\<^sub>1 a v = ppeval P\<^sub>2 a v)
[PROOF STEP]
apply (rule exI[of _ "PA1\<^bold>^\<^bold>2 \<^bold>+ PA2\<^bold>^\<^bold>2 \<^bold>+ PB1\<^bold>^\<^bold>2 \<^bold>+ PB2\<^bold>^\<^bold>2"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p1 p2 q1 q2. (p1 = p2 \<and> q1 = q2) = (p1\<^sup>2 + p2\<^sup>2 + q1\<^sup>2 + q2\<^sup>2 = 2 * p1 * p2 + 2 * q1 * q2)) \<Longrightarrow> \<exists>P\<^sub>2. \<forall>a. eval (A [\<and>] B) a = (\<exists>v. ppeval (PA1 \<^bold>^\<^bold>2 \<^bold>+ PA2 \<^bold>^\<^bold>2 \<^bold>+ PB1 \<^bold>^\<^bold>2 \<^bold>+ PB2 \<^bold>^\<^bold>2) a v = ppeval P\<^sub>2 a v)
[PROOF STEP]
apply (rule exI[of _ "(ppolynomial.Const 2) \<^bold>* PA1 \<^bold>* PA2 \<^bold>+ (ppolynomial.Const 2) \<^bold>* PB1 \<^bold>* PB2"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p1 p2 q1 q2. (p1 = p2 \<and> q1 = q2) = (p1\<^sup>2 + p2\<^sup>2 + q1\<^sup>2 + q2\<^sup>2 = 2 * p1 * p2 + 2 * q1 * q2)) \<Longrightarrow> \<forall>a. eval (A [\<and>] B) a = (\<exists>v. ppeval (PA1 \<^bold>^\<^bold>2 \<^bold>+ PA2 \<^bold>^\<^bold>2 \<^bold>+ PB1 \<^bold>^\<^bold>2 \<^bold>+ PB2 \<^bold>^\<^bold>2) a v = ppeval (ppolynomial.Const 2 \<^bold>* PA1 \<^bold>* PA2 \<^bold>+ ppolynomial.Const 2 \<^bold>* PB1 \<^bold>* PB2) a v)
[PROOF STEP]
apply (subst unified)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p1 p2 q1 q2. (p1 = p2 \<and> q1 = q2) = (p1\<^sup>2 + p2\<^sup>2 + q1\<^sup>2 + q2\<^sup>2 = 2 * p1 * p2 + 2 * q1 * q2)) \<Longrightarrow> \<forall>a. (\<exists>v. ppeval PA1 a v = ppeval PA2 a v \<and> ppeval PB1 a v = ppeval PB2 a v) = (\<exists>v. ppeval (PA1 \<^bold>^\<^bold>2 \<^bold>+ PA2 \<^bold>^\<^bold>2 \<^bold>+ PB1 \<^bold>^\<^bold>2 \<^bold>+ PB2 \<^bold>^\<^bold>2) a v = ppeval (ppolynomial.Const 2 \<^bold>* PA1 \<^bold>* PA2 \<^bold>+ ppolynomial.Const 2 \<^bold>* PB1 \<^bold>* PB2) a v)
[PROOF STEP]
by (simp add: Sq_pp_def power2_eq_square)
[PROOF STATE]
proof (state)
this:
is_dioph_rel (A [\<and>] B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma true_dioph[dioph]: "is_dioph_rel TRUE"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel TRUE
[PROOF STEP]
unfolding TRUE_def UNARY_def is_dioph_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P\<^sub>1 P\<^sub>2. \<forall>a. eval (NARY (\<lambda>l. 0 = l ! 0) [polynomial.Const 0]) a = (\<exists>v. ppeval P\<^sub>1 a v = ppeval P\<^sub>2 a v)
[PROOF STEP]
by auto


[STATEMENT]
lemma eq_dioph[dioph]: "is_dioph_rel (Q [=] R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel (Q [=] R)
[PROOF STEP]
unfolding is_dioph_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P\<^sub>1 P\<^sub>2. \<forall>a. eval (Q [=] R) a = (\<exists>v. ppeval P\<^sub>1 a v = ppeval P\<^sub>2 a v)
[PROOF STEP]
apply (rule exI[of _ "convert Q"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P\<^sub>2. \<forall>a. eval (Q [=] R) a = (\<exists>v. ppeval (convert Q) a v = ppeval P\<^sub>2 a v)
[PROOF STEP]
apply (rule exI[of _ "convert R"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a. eval (Q [=] R) a = (\<exists>v. ppeval (convert Q) a v = ppeval (convert R) a v)
[PROOF STEP]
using convert_eval BINARY_def
[PROOF STATE]
proof (prove)
using this:
peval ?P ?a = ppeval (convert ?P) ?a ?v
BINARY ?R ?P\<^sub>1 ?P\<^sub>2 = NARY (\<lambda>l. ?R (l ! 0) (l ! 1)) [?P\<^sub>1, ?P\<^sub>2]

goal (1 subgoal):
 1. \<forall>a. eval (Q [=] R) a = (\<exists>v. ppeval (convert Q) a v = ppeval (convert R) a v)
[PROOF STEP]
by (auto simp: eq_def)


[STATEMENT]
lemma lt_dioph[dioph]: "is_dioph_rel (Q [<] R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel (Q [<] R)
[PROOF STEP]
unfolding is_dioph_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P\<^sub>1 P\<^sub>2. \<forall>a. eval (Q [<] R) a = (\<exists>v. ppeval P\<^sub>1 a v = ppeval P\<^sub>2 a v)
[PROOF STEP]
apply (rule exI[of _ "(ppolynomial.Const 1) \<^bold>+ (ppolynomial.Var 0) \<^bold>+ convert Q"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P\<^sub>2. \<forall>a. eval (Q [<] R) a = (\<exists>v. ppeval (ppolynomial.Const 1 \<^bold>+ Var 0 \<^bold>+ convert Q) a v = ppeval P\<^sub>2 a v)
[PROOF STEP]
apply (rule exI[of _ "convert R"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a. eval (Q [<] R) a = (\<exists>v. ppeval (ppolynomial.Const 1 \<^bold>+ Var 0 \<^bold>+ convert Q) a v = ppeval (convert R) a v)
[PROOF STEP]
using convert_eval BINARY_def
[PROOF STATE]
proof (prove)
using this:
peval ?P ?a = ppeval (convert ?P) ?a ?v
BINARY ?R ?P\<^sub>1 ?P\<^sub>2 = NARY (\<lambda>l. ?R (l ! 0) (l ! 1)) [?P\<^sub>1, ?P\<^sub>2]

goal (1 subgoal):
 1. \<forall>a. eval (Q [<] R) a = (\<exists>v. ppeval (ppolynomial.Const 1 \<^bold>+ Var 0 \<^bold>+ convert Q) a v = ppeval (convert R) a v)
[PROOF STEP]
apply (auto simp: lt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<And>P a v. peval P a = ppeval (convert P) a v; \<And>R P\<^sub>1 P\<^sub>2. BINARY R P\<^sub>1 P\<^sub>2 = NARY (\<lambda>l. R (l ! 0) (l ! Suc 0)) [P\<^sub>1, P\<^sub>2]; peval Q a < peval R a\<rbrakk> \<Longrightarrow> \<exists>v. Suc (v 0 + peval Q a) = peval R a
[PROOF STEP]
by (metis add.commute add.right_neutral less_natE)


[STATEMENT]
lemma zero_dioph[dioph]: "is_dioph_rel ([0=] Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel ([0=] Q)
[PROOF STEP]
unfolding zero_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel (\<^bold>0 [=] Q)
[PROOF STEP]
by (auto simp: eq_dioph)


[STATEMENT]
lemma gt_dioph[dioph]: "is_dioph_rel (Q [>] R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel (Q [>] R)
[PROOF STEP]
unfolding gt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel (R [<] Q)
[PROOF STEP]
by (auto simp: lt_dioph)


[STATEMENT]
lemma le_dioph[dioph]: "is_dioph_rel (Q [\<le>] R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel (Q [\<le>] R)
[PROOF STEP]
unfolding le_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel (Q [<] R [\<or>] Q [=] R)
[PROOF STEP]
by (auto simp: lt_dioph eq_dioph or_dioph)


[STATEMENT]
lemma ge_dioph[dioph]: "is_dioph_rel (Q [\<ge>] R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel (Q [\<ge>] R)
[PROOF STEP]
unfolding ge_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel (Q [>] R [\<or>] Q [=] R)
[PROOF STEP]
by (auto simp: gt_dioph eq_dioph or_dioph)


[STATEMENT]
lemma ALLC_LIST_dioph[dioph]: "list_all (is_dioph_rel \<circ> DF) L \<Longrightarrow> is_dioph_rel ([\<forall> in L] DF)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all (is_dioph_rel \<circ> DF) L \<Longrightarrow> is_dioph_rel [\<forall> in L] DF
[PROOF STEP]
by (induction L, auto simp add: dioph)


[STATEMENT]
lemma ALLC_dioph[dioph]: "\<forall>i<n. is_dioph_rel (DF i) \<Longrightarrow> is_dioph_rel ([\<forall><n] DF)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<n. is_dioph_rel (DF i) \<Longrightarrow> is_dioph_rel [\<forall><n] DF
[PROOF STEP]
unfolding ALLC_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<n. is_dioph_rel (DF i) \<Longrightarrow> is_dioph_rel [\<forall> in [0..<n]] DF
[PROOF STEP]
using ALLC_LIST_dioph[of DF "[0..<n]"]
[PROOF STATE]
proof (prove)
using this:
list_all (is_dioph_rel \<circ> DF) [0..<n] \<Longrightarrow> is_dioph_rel [\<forall> in [0..<n]] DF

goal (1 subgoal):
 1. \<forall>i<n. is_dioph_rel (DF i) \<Longrightarrow> is_dioph_rel [\<forall> in [0..<n]] DF
[PROOF STEP]
by (auto simp: list_all_length)


[STATEMENT]
lemma show_law_real [show_law_intros]:
  "show_law showsp_real r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. show_law showsp_real r
[PROOF STEP]
by (rule show_lawI) (simp add: showsp_real_def show_law_simps)


[STATEMENT]
lemma showsp_real_append [show_law_simps]:
  "showsp_real p r (x @ y) = showsp_real p r x @ y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. showsp_real p r (x @ y) = showsp_real p r x @ y
[PROOF STEP]
by (intro show_lawD show_law_intros)


[STATEMENT]
lemma vpeq_s_nt:
  assumes prec_t: "precondition (next_state t execs2) (next_action t execs2)"
  assumes not_ifp_curr_u: "\<not> ifp^** (current t) u"
  assumes vpeq_s_t: "\<forall> v . ifp^** v u \<longrightarrow> vpeq v s t"
  shows "(\<forall> v . ifp^** v u \<longrightarrow> vpeq v s (step (next_state t execs2) (next_action t execs2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v s (step (next_state t execs2) (next_action t execs2))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v s (step (next_state t execs2) (next_action t execs2))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v s (step (next_state t execs2) (next_action t execs2))
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v s (step (next_state t execs2) (next_action t execs2))
[PROOF STEP]
assume ifp_v_u: "ifp^** v u"
[PROOF STATE]
proof (state)
this:
ifp\<^sup>*\<^sup>* v u

goal (1 subgoal):
 1. \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v s (step (next_state t execs2) (next_action t execs2))
[PROOF STEP]
from ifp_v_u not_ifp_curr_u
[PROOF STATE]
proof (chain)
picking this:
ifp\<^sup>*\<^sup>* v u
unrelated (current t) u
[PROOF STEP]
have unrelated: "\<not>ifp^** (current t) v"
[PROOF STATE]
proof (prove)
using this:
ifp\<^sup>*\<^sup>* v u
unrelated (current t) u

goal (1 subgoal):
 1. unrelated (current t) v
[PROOF STEP]
using rtranclp_trans
[PROOF STATE]
proof (prove)
using this:
ifp\<^sup>*\<^sup>* v u
unrelated (current t) u
\<lbrakk>?r\<^sup>*\<^sup>* ?x ?y; ?r\<^sup>*\<^sup>* ?y ?z\<rbrakk> \<Longrightarrow> ?r\<^sup>*\<^sup>* ?x ?z

goal (1 subgoal):
 1. unrelated (current t) v
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
unrelated (current t) v

goal (1 subgoal):
 1. \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v s (step (next_state t execs2) (next_action t execs2))
[PROOF STEP]
from this current_next_state[THEN spec,THEN spec,where x1=t]
         locally_respects[THEN spec,THEN spec,THEN spec,where x1="next_state t execs2"] vpeq_reflexive
         prec_t
[PROOF STATE]
proof (chain)
picking this:
unrelated (current t) v
current (next_state t ?x) = current t
\<not> ifp (current (next_state t execs2)) ?x \<and> kprecondition (next_state t execs2) ?x2 \<longrightarrow> vpeq ?x (next_state t execs2) (kstep (next_state t execs2) ?x2)
\<forall>a u. vpeq u a a
precondition (next_state t execs2) (next_action t execs2)
[PROOF STEP]
have "vpeq v (next_state t execs2) (step (next_state t execs2) (next_action t execs2))"
[PROOF STATE]
proof (prove)
using this:
unrelated (current t) v
current (next_state t ?x) = current t
\<not> ifp (current (next_state t execs2)) ?x \<and> kprecondition (next_state t execs2) ?x2 \<longrightarrow> vpeq ?x (next_state t execs2) (kstep (next_state t execs2) ?x2)
\<forall>a u. vpeq u a a
precondition (next_state t execs2) (next_action t execs2)

goal (1 subgoal):
 1. vpeq v (next_state t execs2) (step (next_state t execs2) (next_action t execs2))
[PROOF STEP]
unfolding step_def precondition_def B_def
[PROOF STATE]
proof (prove)
using this:
unrelated (current t) v
current (next_state t ?x) = current t
\<not> ifp (current (next_state t execs2)) ?x \<and> kprecondition (next_state t execs2) ?x2 \<longrightarrow> vpeq ?x (next_state t execs2) (kstep (next_state t execs2) ?x2)
\<forall>a u. vpeq u a a
case next_action t execs2 of None \<Rightarrow> True | Some a \<Rightarrow> kprecondition (next_state t execs2) a

goal (1 subgoal):
 1. vpeq v (next_state t execs2) (case next_action t execs2 of None \<Rightarrow> next_state t execs2 | Some a \<Rightarrow> kstep (next_state t execs2) a)
[PROOF STEP]
by (cases "next_action t execs2",auto)
[PROOF STATE]
proof (state)
this:
vpeq v (next_state t execs2) (step (next_state t execs2) (next_action t execs2))

goal (1 subgoal):
 1. \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v s (step (next_state t execs2) (next_action t execs2))
[PROOF STEP]
from unrelated this locally_respects_next_state vpeq_transitive
[PROOF STATE]
proof (chain)
picking this:
unrelated (current t) v
vpeq v (next_state t execs2) (step (next_state t execs2) (next_action t execs2))
\<forall>s u execs. \<not> ifp (current s) u \<longrightarrow> vpeq u s (next_state s execs)
\<forall>a b c u. vpeq u a b \<and> vpeq u b c \<longrightarrow> vpeq u a c
[PROOF STEP]
have "vpeq v t (step (next_state t execs2) (next_action t execs2))"
[PROOF STATE]
proof (prove)
using this:
unrelated (current t) v
vpeq v (next_state t execs2) (step (next_state t execs2) (next_action t execs2))
\<forall>s u execs. \<not> ifp (current s) u \<longrightarrow> vpeq u s (next_state s execs)
\<forall>a b c u. vpeq u a b \<and> vpeq u b c \<longrightarrow> vpeq u a c

goal (1 subgoal):
 1. vpeq v t (step (next_state t execs2) (next_action t execs2))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vpeq v t (step (next_state t execs2) (next_action t execs2))

goal (1 subgoal):
 1. \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v s (step (next_state t execs2) (next_action t execs2))
[PROOF STEP]
from this and ifp_v_u and vpeq_s_t and vpeq_symmetric and vpeq_transitive
[PROOF STATE]
proof (chain)
picking this:
vpeq v t (step (next_state t execs2) (next_action t execs2))
ifp\<^sup>*\<^sup>* v u
\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v s t
\<forall>a b u. vpeq u a b \<longrightarrow> vpeq u b a
\<forall>a b c u. vpeq u a b \<and> vpeq u b c \<longrightarrow> vpeq u a c
[PROOF STEP]
have "vpeq v s (step (next_state t execs2) (next_action t execs2))"
[PROOF STATE]
proof (prove)
using this:
vpeq v t (step (next_state t execs2) (next_action t execs2))
ifp\<^sup>*\<^sup>* v u
\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v s t
\<forall>a b u. vpeq u a b \<longrightarrow> vpeq u b a
\<forall>a b c u. vpeq u a b \<and> vpeq u b c \<longrightarrow> vpeq u a c

goal (1 subgoal):
 1. vpeq v s (step (next_state t execs2) (next_action t execs2))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
vpeq v s (step (next_state t execs2) (next_action t execs2))

goal (1 subgoal):
 1. \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v s (step (next_state t execs2) (next_action t execs2))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
ifp\<^sup>*\<^sup>* ?v2 u \<Longrightarrow> vpeq ?v2 s (step (next_state t execs2) (next_action t execs2))

goal (1 subgoal):
 1. \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v s (step (next_state t execs2) (next_action t execs2))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ifp\<^sup>*\<^sup>* ?v2 u \<Longrightarrow> vpeq ?v2 s (step (next_state t execs2) (next_action t execs2))

goal (1 subgoal):
 1. \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v s (step (next_state t execs2) (next_action t execs2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v s (step (next_state t execs2) (next_action t execs2))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vpeq_ns_t:
  assumes prec_s: "precondition (next_state s execs) (next_action s execs)"
  assumes not_ifp_curr_u: "\<not> ifp^** (current s) u"
  assumes vpeq_s_t: "\<forall> v . ifp^** v u \<longrightarrow> vpeq v s t"
  shows "\<forall> v . ifp^** v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) t
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) t
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) t
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) t
[PROOF STEP]
assume ifp_v_u: "ifp^** v u"
[PROOF STATE]
proof (state)
this:
ifp\<^sup>*\<^sup>* v u

goal (1 subgoal):
 1. \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) t
[PROOF STEP]
from ifp_v_u and not_ifp_curr_u
[PROOF STATE]
proof (chain)
picking this:
ifp\<^sup>*\<^sup>* v u
unrelated (current s) u
[PROOF STEP]
have unrelated: "\<not>ifp^** (current s) v"
[PROOF STATE]
proof (prove)
using this:
ifp\<^sup>*\<^sup>* v u
unrelated (current s) u

goal (1 subgoal):
 1. unrelated (current s) v
[PROOF STEP]
using rtranclp_trans
[PROOF STATE]
proof (prove)
using this:
ifp\<^sup>*\<^sup>* v u
unrelated (current s) u
\<lbrakk>?r\<^sup>*\<^sup>* ?x ?y; ?r\<^sup>*\<^sup>* ?y ?z\<rbrakk> \<Longrightarrow> ?r\<^sup>*\<^sup>* ?x ?z

goal (1 subgoal):
 1. unrelated (current s) v
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
unrelated (current s) v

goal (1 subgoal):
 1. \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) t
[PROOF STEP]
from this current_next_state[THEN spec,THEN spec,where x1=s] vpeq_reflexive
         unrelated locally_respects[THEN spec,THEN spec,THEN spec,where x1="next_state s execs" and x=v and x2="the (next_action s execs)"] prec_s
[PROOF STATE]
proof (chain)
picking this:
unrelated (current s) v
current (next_state s ?x) = current s
\<forall>a u. vpeq u a a
unrelated (current s) v
\<not> ifp (current (next_state s execs)) v \<and> kprecondition (next_state s execs) (the (next_action s execs)) \<longrightarrow> vpeq v (next_state s execs) (kstep (next_state s execs) (the (next_action s execs)))
precondition (next_state s execs) (next_action s execs)
[PROOF STEP]
have "vpeq v (next_state s execs) (step (next_state s execs) (next_action s execs))"
[PROOF STATE]
proof (prove)
using this:
unrelated (current s) v
current (next_state s ?x) = current s
\<forall>a u. vpeq u a a
unrelated (current s) v
\<not> ifp (current (next_state s execs)) v \<and> kprecondition (next_state s execs) (the (next_action s execs)) \<longrightarrow> vpeq v (next_state s execs) (kstep (next_state s execs) (the (next_action s execs)))
precondition (next_state s execs) (next_action s execs)

goal (1 subgoal):
 1. vpeq v (next_state s execs) (step (next_state s execs) (next_action s execs))
[PROOF STEP]
unfolding step_def precondition_def B_def
[PROOF STATE]
proof (prove)
using this:
unrelated (current s) v
current (next_state s ?x) = current s
\<forall>a u. vpeq u a a
unrelated (current s) v
\<not> ifp (current (next_state s execs)) v \<and> kprecondition (next_state s execs) (the (next_action s execs)) \<longrightarrow> vpeq v (next_state s execs) (kstep (next_state s execs) (the (next_action s execs)))
case next_action s execs of None \<Rightarrow> True | Some a \<Rightarrow> kprecondition (next_state s execs) a

goal (1 subgoal):
 1. vpeq v (next_state s execs) (case next_action s execs of None \<Rightarrow> next_state s execs | Some a \<Rightarrow> kstep (next_state s execs) a)
[PROOF STEP]
by (cases "next_action s execs",auto)
[PROOF STATE]
proof (state)
this:
vpeq v (next_state s execs) (step (next_state s execs) (next_action s execs))

goal (1 subgoal):
 1. \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) t
[PROOF STEP]
from unrelated this locally_respects_next_state vpeq_transitive
[PROOF STATE]
proof (chain)
picking this:
unrelated (current s) v
vpeq v (next_state s execs) (step (next_state s execs) (next_action s execs))
\<forall>s u execs. \<not> ifp (current s) u \<longrightarrow> vpeq u s (next_state s execs)
\<forall>a b c u. vpeq u a b \<and> vpeq u b c \<longrightarrow> vpeq u a c
[PROOF STEP]
have "vpeq v s (step (next_state s execs) (next_action s execs))"
[PROOF STATE]
proof (prove)
using this:
unrelated (current s) v
vpeq v (next_state s execs) (step (next_state s execs) (next_action s execs))
\<forall>s u execs. \<not> ifp (current s) u \<longrightarrow> vpeq u s (next_state s execs)
\<forall>a b c u. vpeq u a b \<and> vpeq u b c \<longrightarrow> vpeq u a c

goal (1 subgoal):
 1. vpeq v s (step (next_state s execs) (next_action s execs))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vpeq v s (step (next_state s execs) (next_action s execs))

goal (1 subgoal):
 1. \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) t
[PROOF STEP]
from this and ifp_v_u and vpeq_s_t and vpeq_symmetric and vpeq_transitive
[PROOF STATE]
proof (chain)
picking this:
vpeq v s (step (next_state s execs) (next_action s execs))
ifp\<^sup>*\<^sup>* v u
\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v s t
\<forall>a b u. vpeq u a b \<longrightarrow> vpeq u b a
\<forall>a b c u. vpeq u a b \<and> vpeq u b c \<longrightarrow> vpeq u a c
[PROOF STEP]
have "vpeq v (step (next_state s execs) (next_action s execs)) t"
[PROOF STATE]
proof (prove)
using this:
vpeq v s (step (next_state s execs) (next_action s execs))
ifp\<^sup>*\<^sup>* v u
\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v s t
\<forall>a b u. vpeq u a b \<longrightarrow> vpeq u b a
\<forall>a b c u. vpeq u a b \<and> vpeq u b c \<longrightarrow> vpeq u a c

goal (1 subgoal):
 1. vpeq v (step (next_state s execs) (next_action s execs)) t
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
vpeq v (step (next_state s execs) (next_action s execs)) t

goal (1 subgoal):
 1. \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) t
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
ifp\<^sup>*\<^sup>* ?v2 u \<Longrightarrow> vpeq ?v2 (step (next_state s execs) (next_action s execs)) t

goal (1 subgoal):
 1. \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ifp\<^sup>*\<^sup>* ?v2 u \<Longrightarrow> vpeq ?v2 (step (next_state s execs) (next_action s execs)) t

goal (1 subgoal):
 1. \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vpeq_ns_nt_ifp_u:
assumes vpeq_s_t: "\<forall> v . ifp^** v u \<longrightarrow> vpeq v s t'"
    and current_s_t: "current s = current t'"
shows "precondition (next_state s execs) a \<and> precondition (next_state t' execs) a \<Longrightarrow> (ifp^** (current s) u \<Longrightarrow>  (\<forall> v . ifp^** v u \<longrightarrow> vpeq v (step (next_state s execs) a) (step (next_state t' execs) a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>precondition (next_state s execs) a \<and> precondition (next_state t' execs) a; ifp\<^sup>*\<^sup>* (current s) u\<rbrakk> \<Longrightarrow> \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) a) (step (next_state t' execs) a)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>precondition (next_state s execs) a \<and> precondition (next_state t' execs) a; ifp\<^sup>*\<^sup>* (current s) u\<rbrakk> \<Longrightarrow> \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) a) (step (next_state t' execs) a)
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>precondition (next_state s execs) a \<and> precondition (next_state t' execs) a; ifp\<^sup>*\<^sup>* (current s) u\<rbrakk> \<Longrightarrow> \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) a) (step (next_state t' execs) a)
[PROOF STEP]
assume precs: "precondition (next_state s execs) a \<and> precondition (next_state t' execs) a"
[PROOF STATE]
proof (state)
this:
precondition (next_state s execs) a \<and> precondition (next_state t' execs) a

goal (1 subgoal):
 1. \<lbrakk>precondition (next_state s execs) a \<and> precondition (next_state t' execs) a; ifp\<^sup>*\<^sup>* (current s) u\<rbrakk> \<Longrightarrow> \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) a) (step (next_state t' execs) a)
[PROOF STEP]
assume ifp_curr: "ifp^** (current s) u"
[PROOF STATE]
proof (state)
this:
ifp\<^sup>*\<^sup>* (current s) u

goal (1 subgoal):
 1. \<lbrakk>precondition (next_state s execs) a \<and> precondition (next_state t' execs) a; ifp\<^sup>*\<^sup>* (current s) u\<rbrakk> \<Longrightarrow> \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) a) (step (next_state t' execs) a)
[PROOF STEP]
from vpeq_s_t
[PROOF STATE]
proof (chain)
picking this:
\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v s t'
[PROOF STEP]
have vpeq_curr_s_t: "ifp^** (current s) u \<longrightarrow> vpeq (current s) s t'"
[PROOF STATE]
proof (prove)
using this:
\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v s t'

goal (1 subgoal):
 1. ifp\<^sup>*\<^sup>* (current s) u \<longrightarrow> vpeq (current s) s t'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ifp\<^sup>*\<^sup>* (current s) u \<longrightarrow> vpeq (current s) s t'

goal (1 subgoal):
 1. \<lbrakk>precondition (next_state s execs) a \<and> precondition (next_state t' execs) a; ifp\<^sup>*\<^sup>* (current s) u\<rbrakk> \<Longrightarrow> \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) a) (step (next_state t' execs) a)
[PROOF STEP]
from ifp_curr precs
    next_state_consistent[THEN spec,THEN spec,where x1=s and x=t'] vpeq_curr_s_t vpeq_s_t
    current_next_state current_s_t weakly_step_consistent[THEN spec,THEN spec,THEN spec,THEN spec,where x3="next_state s execs" and x2="next_state t' execs" and x="the a"]
[PROOF STATE]
proof (chain)
picking this:
ifp\<^sup>*\<^sup>* (current s) u
precondition (next_state s execs) a \<and> precondition (next_state t' execs) a
\<forall>u execs. vpeq (current s) s t' \<and> vpeq u s t' \<and> current s = current t' \<longrightarrow> vpeq u (next_state s execs) (next_state t' execs)
ifp\<^sup>*\<^sup>* (current s) u \<longrightarrow> vpeq (current s) s t'
\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v s t'
\<forall>s execs. current (next_state s execs) = current s
current s = current t'
vpeq ?x1 (next_state s execs) (next_state t' execs) \<and> vpeq (current (next_state s execs)) (next_state s execs) (next_state t' execs) \<and> kprecondition (next_state s execs) (the a) \<and> kprecondition (next_state t' execs) (the a) \<and> current (next_state s execs) = current (next_state t' execs) \<longrightarrow> vpeq ?x1 (kstep (next_state s execs) (the a)) (kstep (next_state t' execs) (the a))
[PROOF STEP]
show "\<forall> v . ifp^** v u \<longrightarrow> vpeq v (step (next_state s execs) a) (step (next_state t' execs) a)"
[PROOF STATE]
proof (prove)
using this:
ifp\<^sup>*\<^sup>* (current s) u
precondition (next_state s execs) a \<and> precondition (next_state t' execs) a
\<forall>u execs. vpeq (current s) s t' \<and> vpeq u s t' \<and> current s = current t' \<longrightarrow> vpeq u (next_state s execs) (next_state t' execs)
ifp\<^sup>*\<^sup>* (current s) u \<longrightarrow> vpeq (current s) s t'
\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v s t'
\<forall>s execs. current (next_state s execs) = current s
current s = current t'
vpeq ?x1 (next_state s execs) (next_state t' execs) \<and> vpeq (current (next_state s execs)) (next_state s execs) (next_state t' execs) \<and> kprecondition (next_state s execs) (the a) \<and> kprecondition (next_state t' execs) (the a) \<and> current (next_state s execs) = current (next_state t' execs) \<longrightarrow> vpeq ?x1 (kstep (next_state s execs) (the a)) (kstep (next_state t' execs) (the a))

goal (1 subgoal):
 1. \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) a) (step (next_state t' execs) a)
[PROOF STEP]
unfolding step_def precondition_def B_def
[PROOF STATE]
proof (prove)
using this:
ifp\<^sup>*\<^sup>* (current s) u
(case a of None \<Rightarrow> True | Some a \<Rightarrow> kprecondition (next_state s execs) a) \<and> (case a of None \<Rightarrow> True | Some a \<Rightarrow> kprecondition (next_state t' execs) a)
\<forall>u execs. vpeq (current s) s t' \<and> vpeq u s t' \<and> current s = current t' \<longrightarrow> vpeq u (next_state s execs) (next_state t' execs)
ifp\<^sup>*\<^sup>* (current s) u \<longrightarrow> vpeq (current s) s t'
\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v s t'
\<forall>s execs. current (next_state s execs) = current s
current s = current t'
vpeq ?x1 (next_state s execs) (next_state t' execs) \<and> vpeq (current (next_state s execs)) (next_state s execs) (next_state t' execs) \<and> kprecondition (next_state s execs) (the a) \<and> kprecondition (next_state t' execs) (the a) \<and> current (next_state s execs) = current (next_state t' execs) \<longrightarrow> vpeq ?x1 (kstep (next_state s execs) (the a)) (kstep (next_state t' execs) (the a))

goal (1 subgoal):
 1. \<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (case a of None \<Rightarrow> next_state s execs | Some a \<Rightarrow> kstep (next_state s execs) a) (case a of None \<Rightarrow> next_state t' execs | Some a \<Rightarrow> kstep (next_state t' execs) a)
[PROOF STEP]
by (cases a,auto)
[PROOF STATE]
proof (state)
this:
\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) a) (step (next_state t' execs) a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vpeq_ns_nt_not_ifp_u:
assumes purged_a_a2: "purged_relation u execs execs2"
    and prec_s: "precondition (next_state s execs) (next_action s execs)"
    and current_s_t: "current s = current t'"
    and vpeq_s_t: "\<forall> v . ifp^** v u \<longrightarrow> vpeq v s t'"
shows "\<not>ifp^** (current s) u \<and> precondition (next_state t' execs2) (next_action t' execs2) \<longrightarrow> (\<forall> v . ifp^** v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) (step (next_state t' execs2) (next_action t' execs2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unrelated (current s) u \<and> precondition (next_state t' execs2) (next_action t' execs2) \<longrightarrow> (\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) (step (next_state t' execs2) (next_action t' execs2)))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. unrelated (current s) u \<and> precondition (next_state t' execs2) (next_action t' execs2) \<longrightarrow> (\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) (step (next_state t' execs2) (next_action t' execs2)))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. unrelated (current s) u \<and> precondition (next_state t' execs2) (next_action t' execs2) \<longrightarrow> (\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) (step (next_state t' execs2) (next_action t' execs2)))
[PROOF STEP]
assume not_ifp: "\<not>ifp^** (current s) u"
[PROOF STATE]
proof (state)
this:
unrelated (current s) u

goal (1 subgoal):
 1. unrelated (current s) u \<and> precondition (next_state t' execs2) (next_action t' execs2) \<longrightarrow> (\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) (step (next_state t' execs2) (next_action t' execs2)))
[PROOF STEP]
assume prec_t: "precondition (next_state t' execs2) (next_action t' execs2)"
[PROOF STATE]
proof (state)
this:
precondition (next_state t' execs2) (next_action t' execs2)

goal (1 subgoal):
 1. unrelated (current s) u \<and> precondition (next_state t' execs2) (next_action t' execs2) \<longrightarrow> (\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) (step (next_state t' execs2) (next_action t' execs2)))
[PROOF STEP]
fix a a' v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. unrelated (current s) u \<and> precondition (next_state t' execs2) (next_action t' execs2) \<longrightarrow> (\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) (step (next_state t' execs2) (next_action t' execs2)))
[PROOF STEP]
assume ifp_v_u: "ifp^** v u"
[PROOF STATE]
proof (state)
this:
ifp\<^sup>*\<^sup>* v u

goal (1 subgoal):
 1. unrelated (current s) u \<and> precondition (next_state t' execs2) (next_action t' execs2) \<longrightarrow> (\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) (step (next_state t' execs2) (next_action t' execs2)))
[PROOF STEP]
from not_ifp and purged_a_a2
[PROOF STATE]
proof (chain)
picking this:
unrelated (current s) u
purged_relation u execs execs2
[PROOF STEP]
have "\<not>ifp^** (current s) u"
[PROOF STATE]
proof (prove)
using this:
unrelated (current s) u
purged_relation u execs execs2

goal (1 subgoal):
 1. unrelated (current s) u
[PROOF STEP]
unfolding purged_relation_def
[PROOF STATE]
proof (prove)
using this:
unrelated (current s) u
\<forall>d. ifp\<^sup>*\<^sup>* d u \<longrightarrow> execs d = execs2 d

goal (1 subgoal):
 1. unrelated (current s) u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
unrelated (current s) u

goal (1 subgoal):
 1. unrelated (current s) u \<and> precondition (next_state t' execs2) (next_action t' execs2) \<longrightarrow> (\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) (step (next_state t' execs2) (next_action t' execs2)))
[PROOF STEP]
from this and ifp_v_u
[PROOF STATE]
proof (chain)
picking this:
unrelated (current s) u
ifp\<^sup>*\<^sup>* v u
[PROOF STEP]
have not_ifp_curr_v: "\<not>ifp^** (current s) v"
[PROOF STATE]
proof (prove)
using this:
unrelated (current s) u
ifp\<^sup>*\<^sup>* v u

goal (1 subgoal):
 1. unrelated (current s) v
[PROOF STEP]
using rtranclp_trans
[PROOF STATE]
proof (prove)
using this:
unrelated (current s) u
ifp\<^sup>*\<^sup>* v u
\<lbrakk>?r\<^sup>*\<^sup>* ?x ?y; ?r\<^sup>*\<^sup>* ?y ?z\<rbrakk> \<Longrightarrow> ?r\<^sup>*\<^sup>* ?x ?z

goal (1 subgoal):
 1. unrelated (current s) v
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
unrelated (current s) v

goal (1 subgoal):
 1. unrelated (current s) u \<and> precondition (next_state t' execs2) (next_action t' execs2) \<longrightarrow> (\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) (step (next_state t' execs2) (next_action t' execs2)))
[PROOF STEP]
from this current_next_state[THEN spec,THEN spec,where x1=s and x=execs] prec_s vpeq_reflexive
       locally_respects[THEN spec,THEN spec,THEN spec,where x1="next_state s execs" and x2="the (next_action s execs)" and x=v]
[PROOF STATE]
proof (chain)
picking this:
unrelated (current s) v
current (next_state s execs) = current s
precondition (next_state s execs) (next_action s execs)
\<forall>a u. vpeq u a a
\<not> ifp (current (next_state s execs)) v \<and> kprecondition (next_state s execs) (the (next_action s execs)) \<longrightarrow> vpeq v (next_state s execs) (kstep (next_state s execs) (the (next_action s execs)))
[PROOF STEP]
have "vpeq v (next_state s execs) (step (next_state s execs) (next_action s execs))"
[PROOF STATE]
proof (prove)
using this:
unrelated (current s) v
current (next_state s execs) = current s
precondition (next_state s execs) (next_action s execs)
\<forall>a u. vpeq u a a
\<not> ifp (current (next_state s execs)) v \<and> kprecondition (next_state s execs) (the (next_action s execs)) \<longrightarrow> vpeq v (next_state s execs) (kstep (next_state s execs) (the (next_action s execs)))

goal (1 subgoal):
 1. vpeq v (next_state s execs) (step (next_state s execs) (next_action s execs))
[PROOF STEP]
unfolding step_def precondition_def B_def
[PROOF STATE]
proof (prove)
using this:
unrelated (current s) v
current (next_state s execs) = current s
case next_action s execs of None \<Rightarrow> True | Some a \<Rightarrow> kprecondition (next_state s execs) a
\<forall>a u. vpeq u a a
\<not> ifp (current (next_state s execs)) v \<and> kprecondition (next_state s execs) (the (next_action s execs)) \<longrightarrow> vpeq v (next_state s execs) (kstep (next_state s execs) (the (next_action s execs)))

goal (1 subgoal):
 1. vpeq v (next_state s execs) (case next_action s execs of None \<Rightarrow> next_state s execs | Some a \<Rightarrow> kstep (next_state s execs) a)
[PROOF STEP]
by (cases "next_action s execs",auto)
[PROOF STATE]
proof (state)
this:
vpeq v (next_state s execs) (step (next_state s execs) (next_action s execs))

goal (1 subgoal):
 1. unrelated (current s) u \<and> precondition (next_state t' execs2) (next_action t' execs2) \<longrightarrow> (\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) (step (next_state t' execs2) (next_action t' execs2)))
[PROOF STEP]
from not_ifp_curr_v this locally_respects_next_state vpeq_transitive
[PROOF STATE]
proof (chain)
picking this:
unrelated (current s) v
vpeq v (next_state s execs) (step (next_state s execs) (next_action s execs))
\<forall>s u execs. \<not> ifp (current s) u \<longrightarrow> vpeq u s (next_state s execs)
\<forall>a b c u. vpeq u a b \<and> vpeq u b c \<longrightarrow> vpeq u a c
[PROOF STEP]
have vpeq_s_ns: "vpeq v s (step (next_state s execs) (next_action s execs))"
[PROOF STATE]
proof (prove)
using this:
unrelated (current s) v
vpeq v (next_state s execs) (step (next_state s execs) (next_action s execs))
\<forall>s u execs. \<not> ifp (current s) u \<longrightarrow> vpeq u s (next_state s execs)
\<forall>a b c u. vpeq u a b \<and> vpeq u b c \<longrightarrow> vpeq u a c

goal (1 subgoal):
 1. vpeq v s (step (next_state s execs) (next_action s execs))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vpeq v s (step (next_state s execs) (next_action s execs))

goal (1 subgoal):
 1. unrelated (current s) u \<and> precondition (next_state t' execs2) (next_action t' execs2) \<longrightarrow> (\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) (step (next_state t' execs2) (next_action t' execs2)))
[PROOF STEP]
from not_ifp_curr_v current_s_t current_next_state[THEN spec,THEN spec,where x1=t' and x=execs2] prec_t
       locally_respects[THEN spec,THEN spec,where x="next_state t' execs2"] vpeq_reflexive
[PROOF STATE]
proof (chain)
picking this:
unrelated (current s) v
current s = current t'
current (next_state t' execs2) = current t'
precondition (next_state t' execs2) (next_action t' execs2)
\<forall>u. \<not> ifp (current (next_state t' execs2)) u \<and> kprecondition (next_state t' execs2) ?x1 \<longrightarrow> vpeq u (next_state t' execs2) (kstep (next_state t' execs2) ?x1)
\<forall>a u. vpeq u a a
[PROOF STEP]
have 0: "vpeq v (next_state t' execs2) (step (next_state t' execs2) (next_action t' execs2))"
[PROOF STATE]
proof (prove)
using this:
unrelated (current s) v
current s = current t'
current (next_state t' execs2) = current t'
precondition (next_state t' execs2) (next_action t' execs2)
\<forall>u. \<not> ifp (current (next_state t' execs2)) u \<and> kprecondition (next_state t' execs2) ?x1 \<longrightarrow> vpeq u (next_state t' execs2) (kstep (next_state t' execs2) ?x1)
\<forall>a u. vpeq u a a

goal (1 subgoal):
 1. vpeq v (next_state t' execs2) (step (next_state t' execs2) (next_action t' execs2))
[PROOF STEP]
unfolding step_def precondition_def B_def
[PROOF STATE]
proof (prove)
using this:
unrelated (current s) v
current s = current t'
current (next_state t' execs2) = current t'
case next_action t' execs2 of None \<Rightarrow> True | Some a \<Rightarrow> kprecondition (next_state t' execs2) a
\<forall>u. \<not> ifp (current (next_state t' execs2)) u \<and> kprecondition (next_state t' execs2) ?x1 \<longrightarrow> vpeq u (next_state t' execs2) (kstep (next_state t' execs2) ?x1)
\<forall>a u. vpeq u a a

goal (1 subgoal):
 1. vpeq v (next_state t' execs2) (case next_action t' execs2 of None \<Rightarrow> next_state t' execs2 | Some a \<Rightarrow> kstep (next_state t' execs2) a)
[PROOF STEP]
by (cases "next_action t' execs2",auto)
[PROOF STATE]
proof (state)
this:
vpeq v (next_state t' execs2) (step (next_state t' execs2) (next_action t' execs2))

goal (1 subgoal):
 1. unrelated (current s) u \<and> precondition (next_state t' execs2) (next_action t' execs2) \<longrightarrow> (\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) (step (next_state t' execs2) (next_action t' execs2)))
[PROOF STEP]
from not_ifp_curr_v current_s_t current_next_state
[PROOF STATE]
proof (chain)
picking this:
unrelated (current s) v
current s = current t'
\<forall>s execs. current (next_state s execs) = current s
[PROOF STEP]
have 1: "\<not>ifp^** (current t') v"
[PROOF STATE]
proof (prove)
using this:
unrelated (current s) v
current s = current t'
\<forall>s execs. current (next_state s execs) = current s

goal (1 subgoal):
 1. unrelated (current t') v
[PROOF STEP]
using rtranclp_trans
[PROOF STATE]
proof (prove)
using this:
unrelated (current s) v
current s = current t'
\<forall>s execs. current (next_state s execs) = current s
\<lbrakk>?r\<^sup>*\<^sup>* ?x ?y; ?r\<^sup>*\<^sup>* ?y ?z\<rbrakk> \<Longrightarrow> ?r\<^sup>*\<^sup>* ?x ?z

goal (1 subgoal):
 1. unrelated (current t') v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
unrelated (current t') v

goal (1 subgoal):
 1. unrelated (current s) u \<and> precondition (next_state t' execs2) (next_action t' execs2) \<longrightarrow> (\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) (step (next_state t' execs2) (next_action t' execs2)))
[PROOF STEP]
from 0 1 locally_respects_next_state vpeq_transitive
[PROOF STATE]
proof (chain)
picking this:
vpeq v (next_state t' execs2) (step (next_state t' execs2) (next_action t' execs2))
unrelated (current t') v
\<forall>s u execs. \<not> ifp (current s) u \<longrightarrow> vpeq u s (next_state s execs)
\<forall>a b c u. vpeq u a b \<and> vpeq u b c \<longrightarrow> vpeq u a c
[PROOF STEP]
have vpeq_t_nt: "vpeq v t' (step (next_state t' execs2) (next_action t' execs2))"
[PROOF STATE]
proof (prove)
using this:
vpeq v (next_state t' execs2) (step (next_state t' execs2) (next_action t' execs2))
unrelated (current t') v
\<forall>s u execs. \<not> ifp (current s) u \<longrightarrow> vpeq u s (next_state s execs)
\<forall>a b c u. vpeq u a b \<and> vpeq u b c \<longrightarrow> vpeq u a c

goal (1 subgoal):
 1. vpeq v t' (step (next_state t' execs2) (next_action t' execs2))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vpeq v t' (step (next_state t' execs2) (next_action t' execs2))

goal (1 subgoal):
 1. unrelated (current s) u \<and> precondition (next_state t' execs2) (next_action t' execs2) \<longrightarrow> (\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) (step (next_state t' execs2) (next_action t' execs2)))
[PROOF STEP]
from vpeq_s_ns and vpeq_t_nt and vpeq_s_t and ifp_v_u and vpeq_symmetric and vpeq_transitive
[PROOF STATE]
proof (chain)
picking this:
vpeq v s (step (next_state s execs) (next_action s execs))
vpeq v t' (step (next_state t' execs2) (next_action t' execs2))
\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v s t'
ifp\<^sup>*\<^sup>* v u
\<forall>a b u. vpeq u a b \<longrightarrow> vpeq u b a
\<forall>a b c u. vpeq u a b \<and> vpeq u b c \<longrightarrow> vpeq u a c
[PROOF STEP]
have vpeq_ns_nt: "vpeq v (step (next_state s execs) (next_action s execs)) (step (next_state t' execs2) (next_action t' execs2))"
[PROOF STATE]
proof (prove)
using this:
vpeq v s (step (next_state s execs) (next_action s execs))
vpeq v t' (step (next_state t' execs2) (next_action t' execs2))
\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v s t'
ifp\<^sup>*\<^sup>* v u
\<forall>a b u. vpeq u a b \<longrightarrow> vpeq u b a
\<forall>a b c u. vpeq u a b \<and> vpeq u b c \<longrightarrow> vpeq u a c

goal (1 subgoal):
 1. vpeq v (step (next_state s execs) (next_action s execs)) (step (next_state t' execs2) (next_action t' execs2))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vpeq v (step (next_state s execs) (next_action s execs)) (step (next_state t' execs2) (next_action t' execs2))

goal (1 subgoal):
 1. unrelated (current s) u \<and> precondition (next_state t' execs2) (next_action t' execs2) \<longrightarrow> (\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) (step (next_state t' execs2) (next_action t' execs2)))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>unrelated (current s) u; precondition (next_state t' execs2) (next_action t' execs2); ifp\<^sup>*\<^sup>* ?v2 u\<rbrakk> \<Longrightarrow> vpeq ?v2 (step (next_state s execs) (next_action s execs)) (step (next_state t' execs2) (next_action t' execs2))

goal (1 subgoal):
 1. unrelated (current s) u \<and> precondition (next_state t' execs2) (next_action t' execs2) \<longrightarrow> (\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) (step (next_state t' execs2) (next_action t' execs2)))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>unrelated (current s) u; precondition (next_state t' execs2) (next_action t' execs2); ifp\<^sup>*\<^sup>* ?v2 u\<rbrakk> \<Longrightarrow> vpeq ?v2 (step (next_state s execs) (next_action s execs)) (step (next_state t' execs2) (next_action t' execs2))

goal (1 subgoal):
 1. unrelated (current s) u \<and> precondition (next_state t' execs2) (next_action t' execs2) \<longrightarrow> (\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) (step (next_state t' execs2) (next_action t' execs2)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
unrelated (current s) u \<and> precondition (next_state t' execs2) (next_action t' execs2) \<longrightarrow> (\<forall>v. ifp\<^sup>*\<^sup>* v u \<longrightarrow> vpeq v (step (next_state s execs) (next_action s execs)) (step (next_state t' execs2) (next_action t' execs2)))

goal:
No subgoals!
[PROOF STEP]
qed