[STATEMENT]
lemma [code]: "fold f [] = id" "fold f (x # xs) s = fold f xs (f x s)" "fold f [x, y] u \<equiv> f y (f x u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fold f [] = id &&& fold f (x # xs) s = fold f xs (f x s) &&& fold f [x, y] u \<equiv> f y (f x u)
[PROOF STEP]
by auto


[STATEMENT]
lemma "List_fold = fold"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. List_fold = fold
[PROOF STEP]
by (rule valid)


[STATEMENT]
lemma "Test__Dict__Construction_h = h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Test__Dict__Construction_h = h
[PROOF STEP]
by (fact valid)


[STATEMENT]
lemma contrived[code]: "c = d 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c = d 0
[PROOF STEP]
unfolding c_def d_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 = (if 0 = 0 then 0 else 0)
[PROOF STEP]
by simp


[STATEMENT]
lemma "Test__Dict__Construction_c = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Test__Dict__Construction_c = c
[PROOF STEP]
by (fact valid)


[STATEMENT]
lemma [code]: "j 0 = 0" "j (Suc n) = j n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j 0 = 0 &&& j (Suc n) = j n
[PROOF STEP]
unfolding j_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 = 0 &&& 0 = 0
[PROOF STEP]
by auto


[STATEMENT]
lemma f_code[code]: "k n = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k n = 0
[PROOF STEP]
by (induct n) simp+


[STATEMENT]
lemma infinite_contains_2_elems:
  assumes "infinite A"
  shows "\<exists> x y. x \<noteq> y \<and> x \<in> A \<and> y \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x y. x \<noteq> y \<and> x \<in> A \<and> y \<in> A
[PROOF STEP]
by (metis assms finite.simps is_singletonI' is_singleton_def)


[STATEMENT]
lemma infinite_contains_3_elems:
  assumes "infinite A"
  shows "\<exists> x y z. x \<noteq> y \<and> x \<noteq> z \<and> y \<noteq> z \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x y z. x \<noteq> y \<and> x \<noteq> z \<and> y \<noteq> z \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A
[PROOF STEP]
by (metis Diff_iff assms infinite_contains_2_elems infinite_remove insertI1)


[STATEMENT]
lemma card_geq_2_iff_contains_2_elems:
  shows "card A \<ge> 2 \<longleftrightarrow> finite A \<and> (\<exists> x y. x \<noteq> y \<and> x \<in> A \<and> y \<in> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (2 \<le> card A) = (finite A \<and> (\<exists>x y. x \<noteq> y \<and> x \<in> A \<and> y \<in> A))
[PROOF STEP]
proof (intro iffI conjI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. 2 \<le> card A \<Longrightarrow> finite A
 2. 2 \<le> card A \<Longrightarrow> \<exists>x y. x \<noteq> y \<and> x \<in> A \<and> y \<in> A
 3. finite A \<and> (\<exists>x y. x \<noteq> y \<and> x \<in> A \<and> y \<in> A) \<Longrightarrow> 2 \<le> card A
[PROOF STEP]
assume *: "finite A \<and> (\<exists> x y. x \<noteq> y \<and> x \<in> A \<and> y \<in> A)"
[PROOF STATE]
proof (state)
this:
finite A \<and> (\<exists>x y. x \<noteq> y \<and> x \<in> A \<and> y \<in> A)

goal (3 subgoals):
 1. 2 \<le> card A \<Longrightarrow> finite A
 2. 2 \<le> card A \<Longrightarrow> \<exists>x y. x \<noteq> y \<and> x \<in> A \<and> y \<in> A
 3. finite A \<and> (\<exists>x y. x \<noteq> y \<and> x \<in> A \<and> y \<in> A) \<Longrightarrow> 2 \<le> card A
[PROOF STEP]
thus "card A \<ge> 2"
[PROOF STATE]
proof (prove)
using this:
finite A \<and> (\<exists>x y. x \<noteq> y \<and> x \<in> A \<and> y \<in> A)

goal (1 subgoal):
 1. 2 \<le> card A
[PROOF STEP]
by (metis card_0_eq card_Suc_eq empty_iff leI less_2_cases singletonD)
[PROOF STATE]
proof (state)
this:
2 \<le> card A

goal (2 subgoals):
 1. 2 \<le> card A \<Longrightarrow> finite A
 2. 2 \<le> card A \<Longrightarrow> \<exists>x y. x \<noteq> y \<and> x \<in> A \<and> y \<in> A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 2 \<le> card A \<Longrightarrow> finite A
 2. 2 \<le> card A \<Longrightarrow> \<exists>x y. x \<noteq> y \<and> x \<in> A \<and> y \<in> A
[PROOF STEP]
assume *: "2 \<le> card A"
[PROOF STATE]
proof (state)
this:
2 \<le> card A

goal (2 subgoals):
 1. 2 \<le> card A \<Longrightarrow> finite A
 2. 2 \<le> card A \<Longrightarrow> \<exists>x y. x \<noteq> y \<and> x \<in> A \<and> y \<in> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 \<le> card A
[PROOF STEP]
show "finite A"
[PROOF STATE]
proof (prove)
using this:
2 \<le> card A

goal (1 subgoal):
 1. finite A
[PROOF STEP]
using card.infinite
[PROOF STATE]
proof (prove)
using this:
2 \<le> card A
infinite ?A \<Longrightarrow> card ?A = 0

goal (1 subgoal):
 1. finite A
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
finite A

goal (1 subgoal):
 1. 2 \<le> card A \<Longrightarrow> \<exists>x y. x \<noteq> y \<and> x \<in> A \<and> y \<in> A
[PROOF STEP]
show "\<exists> x y. x \<noteq> y \<and> x \<in> A \<and> y \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x y. x \<noteq> y \<and> x \<in> A \<and> y \<in> A
[PROOF STEP]
by (meson "*" card_2_iff' in_mono obtain_subset_with_card_n)
[PROOF STATE]
proof (state)
this:
\<exists>x y. x \<noteq> y \<and> x \<in> A \<and> y \<in> A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma card_geq_3_iff_contains_3_elems:
  shows "card A \<ge> 3 \<longleftrightarrow> finite A \<and> (\<exists> x y z. x \<noteq> y \<and> x \<noteq> z \<and> y \<noteq> z \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (3 \<le> card A) = (finite A \<and> (\<exists>x y z. x \<noteq> y \<and> x \<noteq> z \<and> y \<noteq> z \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A))
[PROOF STEP]
proof (intro iffI conjI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. 3 \<le> card A \<Longrightarrow> finite A
 2. 3 \<le> card A \<Longrightarrow> \<exists>x y z. x \<noteq> y \<and> x \<noteq> z \<and> y \<noteq> z \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A
 3. finite A \<and> (\<exists>x y z. x \<noteq> y \<and> x \<noteq> z \<and> y \<noteq> z \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A) \<Longrightarrow> 3 \<le> card A
[PROOF STEP]
assume *: "card A \<ge> 3"
[PROOF STATE]
proof (state)
this:
3 \<le> card A

goal (3 subgoals):
 1. 3 \<le> card A \<Longrightarrow> finite A
 2. 3 \<le> card A \<Longrightarrow> \<exists>x y z. x \<noteq> y \<and> x \<noteq> z \<and> y \<noteq> z \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A
 3. finite A \<and> (\<exists>x y z. x \<noteq> y \<and> x \<noteq> z \<and> y \<noteq> z \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A) \<Longrightarrow> 3 \<le> card A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
3 \<le> card A
[PROOF STEP]
show "finite A"
[PROOF STATE]
proof (prove)
using this:
3 \<le> card A

goal (1 subgoal):
 1. finite A
[PROOF STEP]
using card.infinite
[PROOF STATE]
proof (prove)
using this:
3 \<le> card A
infinite ?A \<Longrightarrow> card ?A = 0

goal (1 subgoal):
 1. finite A
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
finite A

goal (2 subgoals):
 1. 3 \<le> card A \<Longrightarrow> \<exists>x y z. x \<noteq> y \<and> x \<noteq> z \<and> y \<noteq> z \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A
 2. finite A \<and> (\<exists>x y z. x \<noteq> y \<and> x \<noteq> z \<and> y \<noteq> z \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A) \<Longrightarrow> 3 \<le> card A
[PROOF STEP]
show "\<exists> x y z. x \<noteq> y \<and> x \<noteq> z \<and> y \<noteq> z \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x y z. x \<noteq> y \<and> x \<noteq> z \<and> y \<noteq> z \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A
[PROOF STEP]
by (smt (verit, best) "*" card_2_iff' card_geq_2_iff_contains_2_elems le_cases3 not_less_eq_eq numeral_2_eq_2 numeral_3_eq_3)
[PROOF STATE]
proof (state)
this:
\<exists>x y z. x \<noteq> y \<and> x \<noteq> z \<and> y \<noteq> z \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A

goal (1 subgoal):
 1. finite A \<and> (\<exists>x y z. x \<noteq> y \<and> x \<noteq> z \<and> y \<noteq> z \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A) \<Longrightarrow> 3 \<le> card A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite A \<and> (\<exists>x y z. x \<noteq> y \<and> x \<noteq> z \<and> y \<noteq> z \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A) \<Longrightarrow> 3 \<le> card A
[PROOF STEP]
assume *: "finite A \<and> (\<exists> x y z. x \<noteq> y \<and> x \<noteq> z \<and> y \<noteq> z \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A)"
[PROOF STATE]
proof (state)
this:
finite A \<and> (\<exists>x y z. x \<noteq> y \<and> x \<noteq> z \<and> y \<noteq> z \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A)

goal (1 subgoal):
 1. finite A \<and> (\<exists>x y z. x \<noteq> y \<and> x \<noteq> z \<and> y \<noteq> z \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A) \<Longrightarrow> 3 \<le> card A
[PROOF STEP]
thus "card A \<ge> 3"
[PROOF STATE]
proof (prove)
using this:
finite A \<and> (\<exists>x y z. x \<noteq> y \<and> x \<noteq> z \<and> y \<noteq> z \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A)

goal (1 subgoal):
 1. 3 \<le> card A
[PROOF STEP]
by (metis One_nat_def Suc_le_eq card_2_iff' card_le_Suc0_iff_eq leI numeral_3_eq_3 one_add_one order_class.order.eq_iff plus_1_eq_Suc)
[PROOF STATE]
proof (state)
this:
3 \<le> card A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma card_eq_2_iff_doubleton: "card A = 2 \<longleftrightarrow> (\<exists> x y. x \<noteq> y \<and> A = {x, y})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (card A = 2) = (\<exists>x y. x \<noteq> y \<and> A = {x, y})
[PROOF STEP]
using card_geq_2_iff_contains_2_elems[of A]
[PROOF STATE]
proof (prove)
using this:
(2 \<le> card A) = (finite A \<and> (\<exists>x y. x \<noteq> y \<and> x \<in> A \<and> y \<in> A))

goal (1 subgoal):
 1. (card A = 2) = (\<exists>x y. x \<noteq> y \<and> A = {x, y})
[PROOF STEP]
using card_geq_3_iff_contains_3_elems[of A]
[PROOF STATE]
proof (prove)
using this:
(2 \<le> card A) = (finite A \<and> (\<exists>x y. x \<noteq> y \<and> x \<in> A \<and> y \<in> A))
(3 \<le> card A) = (finite A \<and> (\<exists>x y z. x \<noteq> y \<and> x \<noteq> z \<and> y \<noteq> z \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A))

goal (1 subgoal):
 1. (card A = 2) = (\<exists>x y. x \<noteq> y \<and> A = {x, y})
[PROOF STEP]
by auto (rule_tac x=x in exI, rule_tac x=y in exI, auto)


[STATEMENT]
lemma card_eq_2_doubleton:
  assumes "card A = 2" and "x \<noteq> y" and "x \<in> A" and "y \<in> A"
  shows "A = {x, y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = {x, y}
[PROOF STEP]
using assms card_eq_2_iff_doubleton[of A]
[PROOF STATE]
proof (prove)
using this:
card A = 2
x \<noteq> y
x \<in> A
y \<in> A
(card A = 2) = (\<exists>x y. x \<noteq> y \<and> A = {x, y})

goal (1 subgoal):
 1. A = {x, y}
[PROOF STEP]
by auto


[STATEMENT]
lemma bij_image_singleton:
  shows "\<lbrakk>f ` A = {b}; f a = b; bij f\<rbrakk> \<Longrightarrow> A = {a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f ` A = {b}; f a = b; bij f\<rbrakk> \<Longrightarrow> A = {a}
[PROOF STEP]
by (metis bij_betw_def image_empty image_insert inj_image_eq_iff)


[STATEMENT]
lemma all_equations_dioph:
  fixes A f e d c b q :: polynomial
  fixes r z s :: "polynomial list"
  assumes "length r = n" "length z = n" "length s = Suc m"
  defines "DR \<equiv> [ALLEQ] A q b c d e f r z s"
  shows "is_dioph_rel DR"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel DR
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_dioph_rel DR
[PROOF STEP]
define DS where "DS \<equiv> ([REG] A b q r z s)
                     [\<and>] ([STATE] b e q z s)
                     [\<and>] ([MASK] c d e f r z)
                     [\<and>] ([CONST] b c d e f q)
                     [\<and>] [MISC] A c q"
[PROOF STATE]
proof (state)
this:
DS \<equiv> [REG] A b q r z s [\<and>] [STATE] b e q z s [\<and>] [MASK] c d e f r z [\<and>] [CONST] b c d e f q [\<and>] [MISC] A c q

goal (1 subgoal):
 1. is_dioph_rel DR
[PROOF STEP]
have "eval DS a = eval DR a" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval DS a = eval DR a
[PROOF STEP]
unfolding DR_def DS_def all_equations_relation_def all_equations_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval ([REG] A b q r z s [\<and>] [STATE] b e q z s [\<and>] [MASK] c d e f r z [\<and>] [CONST] b c d e f q [\<and>] [MISC] A c q) a = eval (LARY (\<lambda>ll. rm_eq_fixes.register_equations p n (ll ! 0 ! 0) (ll ! 0 ! 2) (ll ! 0 ! 1) ((!) (ll ! 1)) ((!) (ll ! 2)) ((!) (ll ! 3)) \<and> rm_eq_fixes.state_equations p (ll ! 0 ! 2) (ll ! 0 ! 5) (ll ! 0 ! 1) ((!) (ll ! 2)) ((!) (ll ! 3)) \<and> rm_eq_fixes.mask_equations n (ll ! 0 ! 3) (ll ! 0 ! 4) (ll ! 0 ! 5) (ll ! 0 ! 6) ((!) (ll ! 1)) ((!) (ll ! 2)) \<and> rm_eq_fixes.constants_equations (ll ! 0 ! 2) (ll ! 0 ! 3) (ll ! 0 ! 4) (ll ! 0 ! 5) (ll ! 0 ! 6) (ll ! 0 ! 1) \<and> rm_eq_fixes.miscellaneous_equations (ll ! 0 ! 0) (ll ! 0 ! 3) (ll ! 0 ! 1)) [[A, q, b, c, d, e, f], r, z, s]) a
[PROOF STEP]
unfolding register_equations_relation_def state_equations_relation_def
      mask_equations_relation_def rm_constant_equations_def rm_miscellaneous_equations_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (LARY (\<lambda>ll. rm_eq_fixes.register_equations p n (ll ! 0 ! 0) (ll ! 0 ! 1) (ll ! 0 ! 2) ((!) (ll ! 1)) ((!) (ll ! 2)) ((!) (ll ! 3))) [[A, b, q], r, z, s] [\<and>] LARY (\<lambda>ll. rm_eq_fixes.state_equations p (ll ! 0 ! 0) (ll ! 0 ! 1) (ll ! 0 ! 2) ((!) (ll ! 1)) ((!) (ll ! 2))) [[b, e, q], z, s] [\<and>] LARY (\<lambda>ll. rm_eq_fixes.mask_equations n (ll ! 0 ! 0) (ll ! 0 ! 1) (ll ! 0 ! 2) (ll ! 0 ! 3) ((!) (ll ! 1)) ((!) (ll ! 2))) [[c, d, e, f], r, z] [\<and>] NARY (\<lambda>l. rm_eq_fixes.constants_equations (l ! 0) (l ! 1) (l ! 2) (l ! 3) (l ! 4) (l ! 5)) [b, c, d, e, f, q] [\<and>] NARY (\<lambda>l. rm_eq_fixes.miscellaneous_equations (l ! 0) (l ! 1) (l ! 2)) [A, c, q]) a = eval (LARY (\<lambda>ll. rm_eq_fixes.register_equations p n (ll ! 0 ! 0) (ll ! 0 ! 2) (ll ! 0 ! 1) ((!) (ll ! 1)) ((!) (ll ! 2)) ((!) (ll ! 3)) \<and> rm_eq_fixes.state_equations p (ll ! 0 ! 2) (ll ! 0 ! 5) (ll ! 0 ! 1) ((!) (ll ! 2)) ((!) (ll ! 3)) \<and> rm_eq_fixes.mask_equations n (ll ! 0 ! 3) (ll ! 0 ! 4) (ll ! 0 ! 5) (ll ! 0 ! 6) ((!) (ll ! 1)) ((!) (ll ! 2)) \<and> rm_eq_fixes.constants_equations (ll ! 0 ! 2) (ll ! 0 ! 3) (ll ! 0 ! 4) (ll ! 0 ! 5) (ll ! 0 ! 6) (ll ! 0 ! 1) \<and> rm_eq_fixes.miscellaneous_equations (ll ! 0 ! 0) (ll ! 0 ! 3) (ll ! 0 ! 1)) [[A, q, b, c, d, e, f], r, z, s]) a
[PROOF STEP]
by (simp add: defs)
[PROOF STATE]
proof (state)
this:
eval DS ?a = eval DR ?a

goal (1 subgoal):
 1. is_dioph_rel DR
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eval DS ?a = eval DR ?a

goal (1 subgoal):
 1. is_dioph_rel DR
[PROOF STEP]
have "is_dioph_rel DS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel DS
[PROOF STEP]
unfolding DS_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel ([REG] A b q r z s [\<and>] [STATE] b e q z s [\<and>] [MASK] c d e f r z [\<and>] [CONST] b c d e f q [\<and>] [MISC] A c q)
[PROOF STEP]
apply (rule and_dioph)+
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. is_dioph_rel [REG] A b q r z s
 2. is_dioph_rel [STATE] b e q z s
 3. is_dioph_rel [MASK] c d e f r z
 4. is_dioph_rel [CONST] b c d e f q
 5. is_dioph_rel [MISC] A c q
[PROOF STEP]
apply (simp_all add: rm_constant_equations_dioph rm_miscellaneous_equations_dioph)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. is_dioph_rel [REG] A b q r z s
 2. is_dioph_rel [STATE] b e q z s
 3. is_dioph_rel [MASK] c d e f r z
[PROOF STEP]
using assms reg_dioph[of r z s A b q] state_equations_dioph[of s z b e q]
          mask_equations_relation_dioph[of r z c d e f]
[PROOF STATE]
proof (prove)
using this:
length r = n
length z = n
length s = Suc m
DR \<equiv> [ALLEQ] A q b c d e f r z s
\<lbrakk>length r = n; length z = n; length s = Suc m\<rbrakk> \<Longrightarrow> is_dioph_rel [REG] A b q r z s
\<lbrakk>length s = Suc m; length z = n\<rbrakk> \<Longrightarrow> is_dioph_rel [STATE] b e q z s
\<lbrakk>n = length r; n = length z\<rbrakk> \<Longrightarrow> is_dioph_rel [MASK] c d e f r z

goal (3 subgoals):
 1. is_dioph_rel [REG] A b q r z s
 2. is_dioph_rel [STATE] b e q z s
 3. is_dioph_rel [MASK] c d e f r z
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
is_dioph_rel DS

goal (1 subgoal):
 1. is_dioph_rel DR
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eval DS ?a = eval DR ?a
is_dioph_rel DS
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval DS ?a = eval DR ?a
is_dioph_rel DS

goal (1 subgoal):
 1. is_dioph_rel DR
[PROOF STEP]
using is_dioph_rel_def
[PROOF STATE]
proof (prove)
using this:
eval DS ?a = eval DR ?a
is_dioph_rel DS
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. is_dioph_rel DR
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_dioph_rel DR

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rm_dioph:
  fixes A
  fixes ic :: configuration
  defines "DR \<equiv> [RM] A"
  shows "is_dioph_rel DR"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel DR
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_dioph_rel DR
[PROOF STEP]
define q b c d e f where "q \<equiv> Param 0" and
                           "b \<equiv> Param 1" and
                           "c \<equiv> Param 2" and
                           "d \<equiv> Param 3" and
                           "e \<equiv> Param 4" and
                           "f \<equiv> Param 5"
[PROOF STATE]
proof (state)
this:
q \<equiv> polynomial.Param 0
b \<equiv> polynomial.Param 1
c \<equiv> polynomial.Param 2
d \<equiv> polynomial.Param 3
e \<equiv> polynomial.Param 4
f \<equiv> polynomial.Param 5

goal (1 subgoal):
 1. is_dioph_rel DR
[PROOF STEP]
define r where "r \<equiv> map Param [6..<n + 6]"
[PROOF STATE]
proof (state)
this:
r \<equiv> map polynomial.Param [6..<n + 6]

goal (1 subgoal):
 1. is_dioph_rel DR
[PROOF STEP]
define z where "z \<equiv> map Param [n+6..<2*n + 6]"
[PROOF STATE]
proof (state)
this:
z \<equiv> map polynomial.Param [n + 6..<2 * n + 6]

goal (1 subgoal):
 1. is_dioph_rel DR
[PROOF STEP]
define s where "s \<equiv> map Param [2*n + 6..<2*n + 6 + m + 1]"
[PROOF STATE]
proof (state)
this:
s \<equiv> map polynomial.Param [2 * n + 6..<2 * n + 6 + m + 1]

goal (1 subgoal):
 1. is_dioph_rel DR
[PROOF STEP]
define number_of_ex_vars where "number_of_ex_vars \<equiv> 2*n + 6 + m + 1"
[PROOF STATE]
proof (state)
this:
number_of_ex_vars \<equiv> 2 * n + 6 + m + 1

goal (1 subgoal):
 1. is_dioph_rel DR
[PROOF STEP]
define A' where "A' \<equiv> push_param A number_of_ex_vars"
[PROOF STATE]
proof (state)
this:
A' \<equiv> push_param A number_of_ex_vars

goal (1 subgoal):
 1. is_dioph_rel DR
[PROOF STEP]
define DS where "DS \<equiv> [\<exists>number_of_ex_vars] [ALLEQ] A' q b c d e f r z s"
[PROOF STATE]
proof (state)
this:
DS \<equiv> [\<exists>number_of_ex_vars] [ALLEQ] A' q b c d e f r z s

goal (1 subgoal):
 1. is_dioph_rel DR
[PROOF STEP]
have "length r = n" and "length z = n" and "length s = Suc m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length r = n &&& length z = n &&& length s = Suc m
[PROOF STEP]
unfolding r_def z_def s_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map polynomial.Param [6..<n + 6]) = n &&& length (map polynomial.Param [n + 6..<2 * n + 6]) = n &&& length (map polynomial.Param [2 * n + 6..<2 * n + 6 + m + 1]) = Suc m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length r = n
length z = n
length s = Suc m

goal (1 subgoal):
 1. is_dioph_rel DR
[PROOF STEP]
have "eval DS a = eval DR a" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval DS a = eval DR a
[PROOF STEP]
proof (rule)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. eval DS a \<Longrightarrow> eval DR a
 2. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
assume "eval DS a"
[PROOF STATE]
proof (state)
this:
eval DS a

goal (2 subgoals):
 1. eval DS a \<Longrightarrow> eval DR a
 2. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval DS a
[PROOF STEP]
obtain ks where
      ks_length: "number_of_ex_vars = length ks" and
      ALLEQ: "eval ([ALLEQ] A' q b c d e f r z s) (push_list a ks)"
[PROOF STATE]
proof (prove)
using this:
eval DS a

goal (1 subgoal):
 1. (\<And>ks. \<lbrakk>number_of_ex_vars = length ks; eval [ALLEQ] A' q b c d e f r z s (push_list a ks)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding DS_def
[PROOF STATE]
proof (prove)
using this:
eval ([\<exists>number_of_ex_vars] [ALLEQ] A' q b c d e f r z s) a

goal (1 subgoal):
 1. (\<And>ks. \<lbrakk>number_of_ex_vars = length ks; eval [ALLEQ] A' q b c d e f r z s (push_list a ks)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: defs)
[PROOF STATE]
proof (state)
this:
number_of_ex_vars = length ks
eval [ALLEQ] A' q b c d e f r z s (push_list a ks)

goal (2 subgoals):
 1. eval DS a \<Longrightarrow> eval DR a
 2. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
define q' b' c' d' e' f' where "q' \<equiv> ks!0" and
                                   "b' \<equiv> ks!1" and
                                   "c' \<equiv> ks!2" and
                                   "d' \<equiv> ks!3" and
                                   "e' \<equiv> ks!4" and
                                   "f' \<equiv> ks!5"
[PROOF STATE]
proof (state)
this:
q' \<equiv> ks ! 0
b' \<equiv> ks ! 1
c' \<equiv> ks ! 2
d' \<equiv> ks ! 3
e' \<equiv> ks ! 4
f' \<equiv> ks ! 5

goal (2 subgoals):
 1. eval DS a \<Longrightarrow> eval DR a
 2. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
define r_list where "r_list \<equiv> (take n (drop 6 ks))"
[PROOF STATE]
proof (state)
this:
r_list \<equiv> take n (drop 6 ks)

goal (2 subgoals):
 1. eval DS a \<Longrightarrow> eval DR a
 2. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
define z_list where "z_list \<equiv> (take n (drop (6+n) ks))"
[PROOF STATE]
proof (state)
this:
z_list \<equiv> take n (drop (6 + n) ks)

goal (2 subgoals):
 1. eval DS a \<Longrightarrow> eval DR a
 2. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
define s_list where "s_list \<equiv> (drop (6 + 2*n) ks)"
[PROOF STATE]
proof (state)
this:
s_list \<equiv> drop (6 + 2 * n) ks

goal (2 subgoals):
 1. eval DS a \<Longrightarrow> eval DR a
 2. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
define r' where "r' \<equiv> (!) r_list"
[PROOF STATE]
proof (state)
this:
r' \<equiv> (!) r_list

goal (2 subgoals):
 1. eval DS a \<Longrightarrow> eval DR a
 2. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
define z' where "z' \<equiv> (!) z_list"
[PROOF STATE]
proof (state)
this:
z' \<equiv> (!) z_list

goal (2 subgoals):
 1. eval DS a \<Longrightarrow> eval DR a
 2. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
define s' where "s' \<equiv> (!) s_list"
[PROOF STATE]
proof (state)
this:
s' \<equiv> (!) s_list

goal (2 subgoals):
 1. eval DS a \<Longrightarrow> eval DR a
 2. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
have A: "peval A' (push_list a ks) = peval A a" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval A' (push_list a ks) = peval A a
[PROOF STEP]
using ks_length push_push_simp
[PROOF STATE]
proof (prove)
using this:
number_of_ex_vars = length ks
peval (push_param ?P (length ?ns)) (push_list ?a ?ns) = peval ?P ?a

goal (1 subgoal):
 1. peval A' (push_list a ks) = peval A a
[PROOF STEP]
unfolding A'_def
[PROOF STATE]
proof (prove)
using this:
number_of_ex_vars = length ks
peval (push_param ?P (length ?ns)) (push_list ?a ?ns) = peval ?P ?a

goal (1 subgoal):
 1. peval (push_param A number_of_ex_vars) (push_list a ks) = peval A a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
peval A' (push_list ?a ks) = peval A ?a

goal (2 subgoals):
 1. eval DS a \<Longrightarrow> eval DR a
 2. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
have q: "peval q (push_list a ks) = q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval q (push_list a ks) = q'
[PROOF STEP]
unfolding q_def q'_def push_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval (polynomial.Param 0) (\<lambda>i. if i < length ks then ks ! i else a (i - length ks)) = ks ! 0
[PROOF STEP]
using ks_length
[PROOF STATE]
proof (prove)
using this:
number_of_ex_vars = length ks

goal (1 subgoal):
 1. peval (polynomial.Param 0) (\<lambda>i. if i < length ks then ks ! i else a (i - length ks)) = ks ! 0
[PROOF STEP]
unfolding number_of_ex_vars_def
[PROOF STATE]
proof (prove)
using this:
2 * n + 6 + m + 1 = length ks

goal (1 subgoal):
 1. peval (polynomial.Param 0) (\<lambda>i. if i < length ks then ks ! i else a (i - length ks)) = ks ! 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
peval q (push_list a ks) = q'

goal (2 subgoals):
 1. eval DS a \<Longrightarrow> eval DR a
 2. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
have b: "peval b (push_list a ks) = b'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval b (push_list a ks) = b'
[PROOF STEP]
unfolding b_def b'_def push_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval (polynomial.Param 1) (\<lambda>i. if i < length ks then ks ! i else a (i - length ks)) = ks ! 1
[PROOF STEP]
using ks_length
[PROOF STATE]
proof (prove)
using this:
number_of_ex_vars = length ks

goal (1 subgoal):
 1. peval (polynomial.Param 1) (\<lambda>i. if i < length ks then ks ! i else a (i - length ks)) = ks ! 1
[PROOF STEP]
unfolding number_of_ex_vars_def
[PROOF STATE]
proof (prove)
using this:
2 * n + 6 + m + 1 = length ks

goal (1 subgoal):
 1. peval (polynomial.Param 1) (\<lambda>i. if i < length ks then ks ! i else a (i - length ks)) = ks ! 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
peval b (push_list a ks) = b'

goal (2 subgoals):
 1. eval DS a \<Longrightarrow> eval DR a
 2. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
have c: "peval c (push_list a ks) = c'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval c (push_list a ks) = c'
[PROOF STEP]
unfolding c_def c'_def push_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval (polynomial.Param 2) (\<lambda>i. if i < length ks then ks ! i else a (i - length ks)) = ks ! 2
[PROOF STEP]
using ks_length
[PROOF STATE]
proof (prove)
using this:
number_of_ex_vars = length ks

goal (1 subgoal):
 1. peval (polynomial.Param 2) (\<lambda>i. if i < length ks then ks ! i else a (i - length ks)) = ks ! 2
[PROOF STEP]
unfolding number_of_ex_vars_def
[PROOF STATE]
proof (prove)
using this:
2 * n + 6 + m + 1 = length ks

goal (1 subgoal):
 1. peval (polynomial.Param 2) (\<lambda>i. if i < length ks then ks ! i else a (i - length ks)) = ks ! 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
peval c (push_list a ks) = c'

goal (2 subgoals):
 1. eval DS a \<Longrightarrow> eval DR a
 2. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
have d: "peval d (push_list a ks) = d'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval d (push_list a ks) = d'
[PROOF STEP]
unfolding d_def d'_def push_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval (polynomial.Param 3) (\<lambda>i. if i < length ks then ks ! i else a (i - length ks)) = ks ! 3
[PROOF STEP]
using ks_length
[PROOF STATE]
proof (prove)
using this:
number_of_ex_vars = length ks

goal (1 subgoal):
 1. peval (polynomial.Param 3) (\<lambda>i. if i < length ks then ks ! i else a (i - length ks)) = ks ! 3
[PROOF STEP]
unfolding number_of_ex_vars_def
[PROOF STATE]
proof (prove)
using this:
2 * n + 6 + m + 1 = length ks

goal (1 subgoal):
 1. peval (polynomial.Param 3) (\<lambda>i. if i < length ks then ks ! i else a (i - length ks)) = ks ! 3
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
peval d (push_list a ks) = d'

goal (2 subgoals):
 1. eval DS a \<Longrightarrow> eval DR a
 2. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
have e: "peval e (push_list a ks) = e'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval e (push_list a ks) = e'
[PROOF STEP]
unfolding e_def e'_def push_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval (polynomial.Param 4) (\<lambda>i. if i < length ks then ks ! i else a (i - length ks)) = ks ! 4
[PROOF STEP]
using ks_length
[PROOF STATE]
proof (prove)
using this:
number_of_ex_vars = length ks

goal (1 subgoal):
 1. peval (polynomial.Param 4) (\<lambda>i. if i < length ks then ks ! i else a (i - length ks)) = ks ! 4
[PROOF STEP]
unfolding number_of_ex_vars_def
[PROOF STATE]
proof (prove)
using this:
2 * n + 6 + m + 1 = length ks

goal (1 subgoal):
 1. peval (polynomial.Param 4) (\<lambda>i. if i < length ks then ks ! i else a (i - length ks)) = ks ! 4
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
peval e (push_list a ks) = e'

goal (2 subgoals):
 1. eval DS a \<Longrightarrow> eval DR a
 2. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
have f: "peval f (push_list a ks) = f'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval f (push_list a ks) = f'
[PROOF STEP]
unfolding f_def f'_def push_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval (polynomial.Param 5) (\<lambda>i. if i < length ks then ks ! i else a (i - length ks)) = ks ! 5
[PROOF STEP]
using ks_length
[PROOF STATE]
proof (prove)
using this:
number_of_ex_vars = length ks

goal (1 subgoal):
 1. peval (polynomial.Param 5) (\<lambda>i. if i < length ks then ks ! i else a (i - length ks)) = ks ! 5
[PROOF STEP]
unfolding number_of_ex_vars_def
[PROOF STATE]
proof (prove)
using this:
2 * n + 6 + m + 1 = length ks

goal (1 subgoal):
 1. peval (polynomial.Param 5) (\<lambda>i. if i < length ks then ks ! i else a (i - length ks)) = ks ! 5
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
peval f (push_list a ks) = f'

goal (2 subgoals):
 1. eval DS a \<Longrightarrow> eval DR a
 2. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
have r: "(!) (map (\<lambda>P. peval P (push_list a ks)) r) x = (!) r_list x" if "x < n" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>P. peval P (push_list a ks)) r ! x = r_list ! x
[PROOF STEP]
unfolding r_def r_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>P. peval P (push_list a ks)) (map polynomial.Param [6..<n + 6]) ! x = take n (drop 6 ks) ! x
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x < n

goal (1 subgoal):
 1. map (\<lambda>P. peval P (push_list a ks)) (map polynomial.Param [6..<n + 6]) ! x = take n (drop 6 ks) ! x
[PROOF STEP]
unfolding push_list_def
[PROOF STATE]
proof (prove)
using this:
x < n

goal (1 subgoal):
 1. map (\<lambda>P. peval P (\<lambda>i. if i < length ks then ks ! i else a (i - length ks))) (map polynomial.Param [6..<n + 6]) ! x = take n (drop 6 ks) ! x
[PROOF STEP]
using ks_length
[PROOF STATE]
proof (prove)
using this:
x < n
number_of_ex_vars = length ks

goal (1 subgoal):
 1. map (\<lambda>P. peval P (\<lambda>i. if i < length ks then ks ! i else a (i - length ks))) (map polynomial.Param [6..<n + 6]) ! x = take n (drop 6 ks) ! x
[PROOF STEP]
unfolding number_of_ex_vars_def
[PROOF STATE]
proof (prove)
using this:
x < n
2 * n + 6 + m + 1 = length ks

goal (1 subgoal):
 1. map (\<lambda>P. peval P (\<lambda>i. if i < length ks then ks ! i else a (i - length ks))) (map polynomial.Param [6..<n + 6]) ! x = take n (drop 6 ks) ! x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x < n \<Longrightarrow> map (\<lambda>P. peval P (push_list a ks)) r ! ?x = r_list ! ?x

goal (2 subgoals):
 1. eval DS a \<Longrightarrow> eval DR a
 2. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
have z: "(map (\<lambda>P. peval P (push_list a ks)) z) ! x = z_list ! x" if "x < n" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>P. peval P (push_list a ks)) z ! x = z_list ! x
[PROOF STEP]
unfolding z_def z_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>P. peval P (push_list a ks)) (map polynomial.Param [n + 6..<2 * n + 6]) ! x = take n (drop (6 + n) ks) ! x
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x < n

goal (1 subgoal):
 1. map (\<lambda>P. peval P (push_list a ks)) (map polynomial.Param [n + 6..<2 * n + 6]) ! x = take n (drop (6 + n) ks) ! x
[PROOF STEP]
unfolding push_list_def
[PROOF STATE]
proof (prove)
using this:
x < n

goal (1 subgoal):
 1. map (\<lambda>P. peval P (\<lambda>i. if i < length ks then ks ! i else a (i - length ks))) (map polynomial.Param [n + 6..<2 * n + 6]) ! x = take n (drop (6 + n) ks) ! x
[PROOF STEP]
using ks_length
[PROOF STATE]
proof (prove)
using this:
x < n
number_of_ex_vars = length ks

goal (1 subgoal):
 1. map (\<lambda>P. peval P (\<lambda>i. if i < length ks then ks ! i else a (i - length ks))) (map polynomial.Param [n + 6..<2 * n + 6]) ! x = take n (drop (6 + n) ks) ! x
[PROOF STEP]
unfolding number_of_ex_vars_def
[PROOF STATE]
proof (prove)
using this:
x < n
2 * n + 6 + m + 1 = length ks

goal (1 subgoal):
 1. map (\<lambda>P. peval P (\<lambda>i. if i < length ks then ks ! i else a (i - length ks))) (map polynomial.Param [n + 6..<2 * n + 6]) ! x = take n (drop (6 + n) ks) ! x
[PROOF STEP]
by (auto simp add: add.commute)
[PROOF STATE]
proof (state)
this:
?x < n \<Longrightarrow> map (\<lambda>P. peval P (push_list a ks)) z ! ?x = z_list ! ?x

goal (2 subgoals):
 1. eval DS a \<Longrightarrow> eval DR a
 2. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
have s: "(map (\<lambda>P. peval P (push_list a ks)) s) ! x = s_list ! x" if "x < Suc m" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>P. peval P (push_list a ks)) s ! x = s_list ! x
[PROOF STEP]
unfolding s_def s_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>P. peval P (push_list a ks)) (map polynomial.Param [2 * n + 6..<2 * n + 6 + m + 1]) ! x = drop (6 + 2 * n) ks ! x
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x < Suc m

goal (1 subgoal):
 1. map (\<lambda>P. peval P (push_list a ks)) (map polynomial.Param [2 * n + 6..<2 * n + 6 + m + 1]) ! x = drop (6 + 2 * n) ks ! x
[PROOF STEP]
unfolding push_list_def
[PROOF STATE]
proof (prove)
using this:
x < Suc m

goal (1 subgoal):
 1. map (\<lambda>P. peval P (\<lambda>i. if i < length ks then ks ! i else a (i - length ks))) (map polynomial.Param [2 * n + 6..<2 * n + 6 + m + 1]) ! x = drop (6 + 2 * n) ks ! x
[PROOF STEP]
using ks_length
[PROOF STATE]
proof (prove)
using this:
x < Suc m
number_of_ex_vars = length ks

goal (1 subgoal):
 1. map (\<lambda>P. peval P (\<lambda>i. if i < length ks then ks ! i else a (i - length ks))) (map polynomial.Param [2 * n + 6..<2 * n + 6 + m + 1]) ! x = drop (6 + 2 * n) ks ! x
[PROOF STEP]
unfolding number_of_ex_vars_def
[PROOF STATE]
proof (prove)
using this:
x < Suc m
2 * n + 6 + m + 1 = length ks

goal (1 subgoal):
 1. map (\<lambda>P. peval P (\<lambda>i. if i < length ks then ks ! i else a (i - length ks))) (map polynomial.Param [2 * n + 6..<2 * n + 6 + m + 1]) ! x = drop (6 + 2 * n) ks ! x
[PROOF STEP]
by (auto simp add: add.commute)
[PROOF STATE]
proof (state)
this:
?x < Suc m \<Longrightarrow> map (\<lambda>P. peval P (push_list a ks)) s ! ?x = s_list ! ?x

goal (2 subgoals):
 1. eval DS a \<Longrightarrow> eval DR a
 2. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
have "all_equations (peval A a) q' b' c' d' e' f' r' z' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_equations (peval A a) q' b' c' d' e' f' r' z' s'
[PROOF STEP]
using ALLEQ
[PROOF STATE]
proof (prove)
using this:
eval [ALLEQ] A' q b c d e f r z s (push_list a ks)

goal (1 subgoal):
 1. all_equations (peval A a) q' b' c' d' e' f' r' z' s'
[PROOF STEP]
unfolding all_equations_relation_def
[PROOF STATE]
proof (prove)
using this:
eval (LARY (\<lambda>ll. all_equations (ll ! 0 ! 0) (ll ! 0 ! 1) (ll ! 0 ! 2) (ll ! 0 ! 3) (ll ! 0 ! 4) (ll ! 0 ! 5) (ll ! 0 ! 6) ((!) (ll ! 1)) ((!) (ll ! 2)) ((!) (ll ! 3))) [[A', q, b, c, d, e, f], r, z, s]) (push_list a ks)

goal (1 subgoal):
 1. all_equations (peval A a) q' b' c' d' e' f' r' z' s'
[PROOF STEP]
apply (simp add: defs)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_equations (peval A' (push_list a ks)) (peval q (push_list a ks)) (peval b (push_list a ks)) (peval c (push_list a ks)) (peval d (push_list a ks)) (peval e (push_list a ks)) (peval f (push_list a ks)) ((!) (map (\<lambda>P. peval P (push_list a ks)) r)) ((!) (map (\<lambda>P. peval P (push_list a ks)) z)) ((!) (map (\<lambda>P. peval P (push_list a ks)) s)) \<Longrightarrow> all_equations (peval A a) q' b' c' d' e' f' r' z' s'
[PROOF STEP]
unfolding A q b c d e f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_equations (peval A a) q' b' c' d' e' f' ((!) (map (\<lambda>P. peval P (push_list a ks)) r)) ((!) (map (\<lambda>P. peval P (push_list a ks)) z)) ((!) (map (\<lambda>P. peval P (push_list a ks)) s)) \<Longrightarrow> all_equations (peval A a) q' b' c' d' e' f' r' z' s'
[PROOF STEP]
using all_equations_invariance[of
                                     "(!) (map (\<lambda>P. peval P (push_list a ks)) r)" r'
                                     "(!) (map (\<lambda>P. peval P (push_list a ks)) z)" z'
                                     "(!) (map (\<lambda>P. peval P (push_list a ks)) s)" s'
                                     "peval A a" q' b' c' d' e' f'] r z s
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<forall>i<n. map (\<lambda>P. peval P (push_list a ks)) r ! i = r' i; \<forall>i<n. map (\<lambda>P. peval P (push_list a ks)) z ! i = z' i; \<forall>i<Suc m. map (\<lambda>P. peval P (push_list a ks)) s ! i = s' i\<rbrakk> \<Longrightarrow> all_equations (peval A a) q' b' c' d' e' f' ((!) (map (\<lambda>P. peval P (push_list a ks)) r)) ((!) (map (\<lambda>P. peval P (push_list a ks)) z)) ((!) (map (\<lambda>P. peval P (push_list a ks)) s)) = all_equations (peval A a) q' b' c' d' e' f' r' z' s'
?x < n \<Longrightarrow> map (\<lambda>P. peval P (push_list a ks)) r ! ?x = r_list ! ?x
?x < n \<Longrightarrow> map (\<lambda>P. peval P (push_list a ks)) z ! ?x = z_list ! ?x
?x < Suc m \<Longrightarrow> map (\<lambda>P. peval P (push_list a ks)) s ! ?x = s_list ! ?x

goal (1 subgoal):
 1. all_equations (peval A a) q' b' c' d' e' f' ((!) (map (\<lambda>P. peval P (push_list a ks)) r)) ((!) (map (\<lambda>P. peval P (push_list a ks)) z)) ((!) (map (\<lambda>P. peval P (push_list a ks)) s)) \<Longrightarrow> all_equations (peval A a) q' b' c' d' e' f' r' z' s'
[PROOF STEP]
using r'_def s'_def z'_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<forall>i<n. map (\<lambda>P. peval P (push_list a ks)) r ! i = r' i; \<forall>i<n. map (\<lambda>P. peval P (push_list a ks)) z ! i = z' i; \<forall>i<Suc m. map (\<lambda>P. peval P (push_list a ks)) s ! i = s' i\<rbrakk> \<Longrightarrow> all_equations (peval A a) q' b' c' d' e' f' ((!) (map (\<lambda>P. peval P (push_list a ks)) r)) ((!) (map (\<lambda>P. peval P (push_list a ks)) z)) ((!) (map (\<lambda>P. peval P (push_list a ks)) s)) = all_equations (peval A a) q' b' c' d' e' f' r' z' s'
?x < n \<Longrightarrow> map (\<lambda>P. peval P (push_list a ks)) r ! ?x = r_list ! ?x
?x < n \<Longrightarrow> map (\<lambda>P. peval P (push_list a ks)) z ! ?x = z_list ! ?x
?x < Suc m \<Longrightarrow> map (\<lambda>P. peval P (push_list a ks)) s ! ?x = s_list ! ?x
r' \<equiv> (!) r_list
s' \<equiv> (!) s_list
z' \<equiv> (!) z_list

goal (1 subgoal):
 1. all_equations (peval A a) q' b' c' d' e' f' ((!) (map (\<lambda>P. peval P (push_list a ks)) r)) ((!) (map (\<lambda>P. peval P (push_list a ks)) z)) ((!) (map (\<lambda>P. peval P (push_list a ks)) s)) \<Longrightarrow> all_equations (peval A a) q' b' c' d' e' f' r' z' s'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
all_equations (peval A a) q' b' c' d' e' f' r' z' s'

goal (2 subgoals):
 1. eval DS a \<Longrightarrow> eval DR a
 2. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
thus "eval DR a"
[PROOF STATE]
proof (prove)
using this:
all_equations (peval A a) q' b' c' d' e' f' r' z' s'

goal (1 subgoal):
 1. eval DR a
[PROOF STEP]
unfolding DR_def rm_equations_def rm_equations_relation_def
[PROOF STATE]
proof (prove)
using this:
all_equations (peval A a) q' b' c' d' e' f' r' z' s'

goal (1 subgoal):
 1. eval (UNARY (\<lambda>a. \<exists>q b c d e f r z s. all_equations a q b c d e f r z s) A) a
[PROOF STEP]
by (auto simp: defs) (blast)
[PROOF STATE]
proof (state)
this:
eval DR a

goal (1 subgoal):
 1. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
assume "eval DR a"
[PROOF STATE]
proof (state)
this:
eval DR a

goal (1 subgoal):
 1. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval DR a
[PROOF STEP]
obtain q' b' c' d' e' f' r' z' s' where
         all_eq: "all_equations (peval A a) q' b' c' d' e' f' r' z' s'"
[PROOF STATE]
proof (prove)
using this:
eval DR a

goal (1 subgoal):
 1. (\<And>q' b' c' d' e' f' r' z' s'. all_equations (peval A a) q' b' c' d' e' f' r' z' s' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding DR_def rm_equations_def rm_equations_relation_def
[PROOF STATE]
proof (prove)
using this:
eval (UNARY (\<lambda>a. \<exists>q b c d e f r z s. all_equations a q b c d e f r z s) A) a

goal (1 subgoal):
 1. (\<And>q' b' c' d' e' f' r' z' s'. all_equations (peval A a) q' b' c' d' e' f' r' z' s' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: defs)
[PROOF STATE]
proof (state)
this:
all_equations (peval A a) q' b' c' d' e' f' r' z' s'

goal (1 subgoal):
 1. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
define r_list where "r_list \<equiv> map r' [0..<n]"
[PROOF STATE]
proof (state)
this:
r_list \<equiv> map r' [0..<n]

goal (1 subgoal):
 1. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
define z_list where "z_list \<equiv> map z' [0..<n]"
[PROOF STATE]
proof (state)
this:
z_list \<equiv> map z' [0..<n]

goal (1 subgoal):
 1. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
define s_list where "s_list \<equiv> map s' [0..<Suc m]"
[PROOF STATE]
proof (state)
this:
s_list \<equiv> map s' [0..<Suc m]

goal (1 subgoal):
 1. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
define ks where "ks \<equiv> [q', b', c', d', e', f'] @ r_list @ z_list @ s_list"
[PROOF STATE]
proof (state)
this:
ks \<equiv> [q', b', c', d', e', f'] @ r_list @ z_list @ s_list

goal (1 subgoal):
 1. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
have "number_of_ex_vars = length ks"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. number_of_ex_vars = length ks
[PROOF STEP]
unfolding number_of_ex_vars_def ks_def r_list_def z_list_def s_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * n + 6 + m + 1 = length ([q', b', c', d', e', f'] @ map r' [0..<n] @ map z' [0..<n] @ map s' [0..<Suc m])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
number_of_ex_vars = length ks

goal (1 subgoal):
 1. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
have A: "peval A' (push_list a ks) = peval A a" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval A' (push_list a ks) = peval A a
[PROOF STEP]
unfolding A'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval (push_param A number_of_ex_vars) (push_list a ks) = peval A a
[PROOF STEP]
using push_push_simp[of A ks a]
[PROOF STATE]
proof (prove)
using this:
peval (push_param A (length ks)) (push_list a ks) = peval A a

goal (1 subgoal):
 1. peval (push_param A number_of_ex_vars) (push_list a ks) = peval A a
[PROOF STEP]
unfolding \<open>number_of_ex_vars = length ks\<close>
[PROOF STATE]
proof (prove)
using this:
peval (push_param A (length ks)) (push_list a ks) = peval A a

goal (1 subgoal):
 1. peval (push_param A (length ks)) (push_list a ks) = peval A a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
peval A' (push_list ?a ks) = peval A ?a

goal (1 subgoal):
 1. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
have q: "peval q (push_list a ks) = q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval q (push_list a ks) = q'
[PROOF STEP]
unfolding q_def ks_def push_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval (polynomial.Param 0) (\<lambda>i. if i < length ([q', b', c', d', e', f'] @ r_list @ z_list @ s_list) then ([q', b', c', d', e', f'] @ r_list @ z_list @ s_list) ! i else a (i - length ([q', b', c', d', e', f'] @ r_list @ z_list @ s_list))) = q'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
peval q (push_list a ks) = q'

goal (1 subgoal):
 1. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
have b: "peval b (push_list a ks) = b'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval b (push_list a ks) = b'
[PROOF STEP]
unfolding b_def ks_def push_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval (polynomial.Param 1) (\<lambda>i. if i < length ([q', b', c', d', e', f'] @ r_list @ z_list @ s_list) then ([q', b', c', d', e', f'] @ r_list @ z_list @ s_list) ! i else a (i - length ([q', b', c', d', e', f'] @ r_list @ z_list @ s_list))) = b'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
peval b (push_list a ks) = b'

goal (1 subgoal):
 1. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
have c: "peval c (push_list a ks) = c'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval c (push_list a ks) = c'
[PROOF STEP]
unfolding c_def ks_def push_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval (polynomial.Param 2) (\<lambda>i. if i < length ([q', b', c', d', e', f'] @ r_list @ z_list @ s_list) then ([q', b', c', d', e', f'] @ r_list @ z_list @ s_list) ! i else a (i - length ([q', b', c', d', e', f'] @ r_list @ z_list @ s_list))) = c'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
peval c (push_list a ks) = c'

goal (1 subgoal):
 1. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
have d: "peval d (push_list a ks) = d'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval d (push_list a ks) = d'
[PROOF STEP]
unfolding d_def ks_def push_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval (polynomial.Param 3) (\<lambda>i. if i < length ([q', b', c', d', e', f'] @ r_list @ z_list @ s_list) then ([q', b', c', d', e', f'] @ r_list @ z_list @ s_list) ! i else a (i - length ([q', b', c', d', e', f'] @ r_list @ z_list @ s_list))) = d'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
peval d (push_list a ks) = d'

goal (1 subgoal):
 1. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
have e: "peval e (push_list a ks) = e'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval e (push_list a ks) = e'
[PROOF STEP]
unfolding e_def ks_def push_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval (polynomial.Param 4) (\<lambda>i. if i < length ([q', b', c', d', e', f'] @ r_list @ z_list @ s_list) then ([q', b', c', d', e', f'] @ r_list @ z_list @ s_list) ! i else a (i - length ([q', b', c', d', e', f'] @ r_list @ z_list @ s_list))) = e'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
peval e (push_list a ks) = e'

goal (1 subgoal):
 1. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
have f: "peval f (push_list a ks) = f'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval f (push_list a ks) = f'
[PROOF STEP]
unfolding f_def ks_def push_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval (polynomial.Param 5) (\<lambda>i. if i < length ([q', b', c', d', e', f'] @ r_list @ z_list @ s_list) then ([q', b', c', d', e', f'] @ r_list @ z_list @ s_list) ! i else a (i - length ([q', b', c', d', e', f'] @ r_list @ z_list @ s_list))) = f'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
peval f (push_list a ks) = f'

goal (1 subgoal):
 1. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
have r: "(map (\<lambda>P. peval P (push_list a ks)) r) ! x = r' x" if "x < n" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>P. peval P (push_list a ks)) r ! x = r' x
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x < n

goal (1 subgoal):
 1. map (\<lambda>P. peval P (push_list a ks)) r ! x = r' x
[PROOF STEP]
unfolding ks_def r_list_def r_def push_list_def
[PROOF STATE]
proof (prove)
using this:
x < n

goal (1 subgoal):
 1. map (\<lambda>P. peval P (\<lambda>i. if i < length ([q', b', c', d', e', f'] @ map r' [0..<n] @ z_list @ s_list) then ([q', b', c', d', e', f'] @ map r' [0..<n] @ z_list @ s_list) ! i else a (i - length ([q', b', c', d', e', f'] @ map r' [0..<n] @ z_list @ s_list)))) (map polynomial.Param [6..<n + 6]) ! x = r' x
[PROOF STEP]
using nth_append[of "map r' [0..<n]" "z_list @ s_list"]
[PROOF STATE]
proof (prove)
using this:
x < n
(map r' [0..<n] @ z_list @ s_list) ! ?n = (if ?n < length (map r' [0..<n]) then map r' [0..<n] ! ?n else (z_list @ s_list) ! (?n - length (map r' [0..<n])))

goal (1 subgoal):
 1. map (\<lambda>P. peval P (\<lambda>i. if i < length ([q', b', c', d', e', f'] @ map r' [0..<n] @ z_list @ s_list) then ([q', b', c', d', e', f'] @ map r' [0..<n] @ z_list @ s_list) ! i else a (i - length ([q', b', c', d', e', f'] @ map r' [0..<n] @ z_list @ s_list)))) (map polynomial.Param [6..<n + 6]) ! x = r' x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x < n \<Longrightarrow> map (\<lambda>P. peval P (push_list a ks)) r ! ?x = r' ?x

goal (1 subgoal):
 1. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
have z: "(map (\<lambda>P. peval P (push_list a ks)) z) ! x = z' x" if "x < n" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>P. peval P (push_list a ks)) z ! x = z' x
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x < n

goal (1 subgoal):
 1. map (\<lambda>P. peval P (push_list a ks)) z ! x = z' x
[PROOF STEP]
unfolding ks_def z_list_def r_list_def z_def push_list_def
[PROOF STATE]
proof (prove)
using this:
x < n

goal (1 subgoal):
 1. map (\<lambda>P. peval P (\<lambda>i. if i < length ([q', b', c', d', e', f'] @ map r' [0..<n] @ map z' [0..<n] @ s_list) then ([q', b', c', d', e', f'] @ map r' [0..<n] @ map z' [0..<n] @ s_list) ! i else a (i - length ([q', b', c', d', e', f'] @ map r' [0..<n] @ map z' [0..<n] @ s_list)))) (map polynomial.Param [n + 6..<2 * n + 6]) ! x = z' x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < n \<Longrightarrow> (map r' [0..<n] @ map z' [0..<n] @ s_list) ! (n + x) = z' x
[PROOF STEP]
using nth_append[of "map r' [0..<n] @ map z' [0..<n]" "s_list"]
[PROOF STATE]
proof (prove)
using this:
((map r' [0..<n] @ map z' [0..<n]) @ s_list) ! ?n = (if ?n < length (map r' [0..<n] @ map z' [0..<n]) then (map r' [0..<n] @ map z' [0..<n]) ! ?n else s_list ! (?n - length (map r' [0..<n] @ map z' [0..<n])))

goal (1 subgoal):
 1. x < n \<Longrightarrow> (map r' [0..<n] @ map z' [0..<n] @ s_list) ! (n + x) = z' x
[PROOF STEP]
by (metis add_diff_cancel_left' gen_length_def length_code length_map length_upt
          not_add_less1 nth_append nth_map_upt)
[PROOF STATE]
proof (state)
this:
?x < n \<Longrightarrow> map (\<lambda>P. peval P (push_list a ks)) z ! ?x = z' ?x

goal (1 subgoal):
 1. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
have s: "(map (\<lambda>P. peval P (push_list a ks)) s) ! x = s' x" if "x < Suc m" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>P. peval P (push_list a ks)) s ! x = s' x
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x < Suc m

goal (1 subgoal):
 1. map (\<lambda>P. peval P (push_list a ks)) s ! x = s' x
[PROOF STEP]
unfolding ks_def r_list_def z_list_def s_list_def s_def push_list_def
[PROOF STATE]
proof (prove)
using this:
x < Suc m

goal (1 subgoal):
 1. map (\<lambda>P. peval P (\<lambda>i. if i < length ([q', b', c', d', e', f'] @ map r' [0..<n] @ map z' [0..<n] @ map s' [0..<Suc m]) then ([q', b', c', d', e', f'] @ map r' [0..<n] @ map z' [0..<n] @ map s' [0..<Suc m]) ! i else a (i - length ([q', b', c', d', e', f'] @ map r' [0..<n] @ map z' [0..<n] @ map s' [0..<Suc m])))) (map polynomial.Param [2 * n + 6..<2 * n + 6 + m + 1]) ! x = s' x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < Suc m \<Longrightarrow> (map r' [0..<n] @ map z' [0..<n] @ map s' [0..<m] @ [s' m]) ! (2 * n + x) = s' x
[PROOF STEP]
using nth_append[of "map r' [0..<n] @ map z' [0..<n]" "map s' [0..<m] @ [s' m]" "(2 * n + x)"]
[PROOF STATE]
proof (prove)
using this:
((map r' [0..<n] @ map z' [0..<n]) @ map s' [0..<m] @ [s' m]) ! (2 * n + x) = (if 2 * n + x < length (map r' [0..<n] @ map z' [0..<n]) then (map r' [0..<n] @ map z' [0..<n]) ! (2 * n + x) else (map s' [0..<m] @ [s' m]) ! (2 * n + x - length (map r' [0..<n] @ map z' [0..<n])))

goal (1 subgoal):
 1. x < Suc m \<Longrightarrow> (map r' [0..<n] @ map z' [0..<n] @ map s' [0..<m] @ [s' m]) ! (2 * n + x) = s' x
[PROOF STEP]
by (auto) (metis (mono_tags, lifting) add_cancel_left_left diff_zero length_map length_upt
          less_antisym nth_append nth_append_length nth_map_upt)
[PROOF STATE]
proof (state)
this:
?x < Suc m \<Longrightarrow> map (\<lambda>P. peval P (push_list a ks)) s ! ?x = s' ?x

goal (1 subgoal):
 1. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
have "eval ([ALLEQ] A' q b c d e f r z s) (push_list a ks)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval [ALLEQ] A' q b c d e f r z s (push_list a ks)
[PROOF STEP]
using all_eq
[PROOF STATE]
proof (prove)
using this:
all_equations (peval A a) q' b' c' d' e' f' r' z' s'

goal (1 subgoal):
 1. eval [ALLEQ] A' q b c d e f r z s (push_list a ks)
[PROOF STEP]
unfolding all_equations_relation_def
[PROOF STATE]
proof (prove)
using this:
all_equations (peval A a) q' b' c' d' e' f' r' z' s'

goal (1 subgoal):
 1. eval (LARY (\<lambda>ll. all_equations (ll ! 0 ! 0) (ll ! 0 ! 1) (ll ! 0 ! 2) (ll ! 0 ! 3) (ll ! 0 ! 4) (ll ! 0 ! 5) (ll ! 0 ! 6) ((!) (ll ! 1)) ((!) (ll ! 2)) ((!) (ll ! 3))) [[A', q, b, c, d, e, f], r, z, s]) (push_list a ks)
[PROOF STEP]
apply (simp add: defs)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_equations (peval A a) q' b' c' d' e' f' r' z' s' \<Longrightarrow> all_equations (peval A' (push_list a ks)) (peval q (push_list a ks)) (peval b (push_list a ks)) (peval c (push_list a ks)) (peval d (push_list a ks)) (peval e (push_list a ks)) (peval f (push_list a ks)) ((!) (map (\<lambda>P. peval P (push_list a ks)) r)) ((!) (map (\<lambda>P. peval P (push_list a ks)) z)) ((!) (map (\<lambda>P. peval P (push_list a ks)) s))
[PROOF STEP]
unfolding A q b c d e f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_equations (peval A a) q' b' c' d' e' f' r' z' s' \<Longrightarrow> all_equations (peval A a) q' b' c' d' e' f' ((!) (map (\<lambda>P. peval P (push_list a ks)) r)) ((!) (map (\<lambda>P. peval P (push_list a ks)) z)) ((!) (map (\<lambda>P. peval P (push_list a ks)) s))
[PROOF STEP]
using all_equations_invariance[of "(!) (map (\<lambda>P. peval P (push_list a ks)) r)" r'
                                        "(!) (map (\<lambda>P. peval P (push_list a ks)) z)" z'
                                        "(!) (map (\<lambda>P. peval P (push_list a ks)) s)" s'
                                        "peval A a" q' b' c' d' e' f'] r z s
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<forall>i<n. map (\<lambda>P. peval P (push_list a ks)) r ! i = r' i; \<forall>i<n. map (\<lambda>P. peval P (push_list a ks)) z ! i = z' i; \<forall>i<Suc m. map (\<lambda>P. peval P (push_list a ks)) s ! i = s' i\<rbrakk> \<Longrightarrow> all_equations (peval A a) q' b' c' d' e' f' ((!) (map (\<lambda>P. peval P (push_list a ks)) r)) ((!) (map (\<lambda>P. peval P (push_list a ks)) z)) ((!) (map (\<lambda>P. peval P (push_list a ks)) s)) = all_equations (peval A a) q' b' c' d' e' f' r' z' s'
?x < n \<Longrightarrow> map (\<lambda>P. peval P (push_list a ks)) r ! ?x = r' ?x
?x < n \<Longrightarrow> map (\<lambda>P. peval P (push_list a ks)) z ! ?x = z' ?x
?x < Suc m \<Longrightarrow> map (\<lambda>P. peval P (push_list a ks)) s ! ?x = s' ?x

goal (1 subgoal):
 1. all_equations (peval A a) q' b' c' d' e' f' r' z' s' \<Longrightarrow> all_equations (peval A a) q' b' c' d' e' f' ((!) (map (\<lambda>P. peval P (push_list a ks)) r)) ((!) (map (\<lambda>P. peval P (push_list a ks)) z)) ((!) (map (\<lambda>P. peval P (push_list a ks)) s))
[PROOF STEP]
using r_list_def s_list_def z_list_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<forall>i<n. map (\<lambda>P. peval P (push_list a ks)) r ! i = r' i; \<forall>i<n. map (\<lambda>P. peval P (push_list a ks)) z ! i = z' i; \<forall>i<Suc m. map (\<lambda>P. peval P (push_list a ks)) s ! i = s' i\<rbrakk> \<Longrightarrow> all_equations (peval A a) q' b' c' d' e' f' ((!) (map (\<lambda>P. peval P (push_list a ks)) r)) ((!) (map (\<lambda>P. peval P (push_list a ks)) z)) ((!) (map (\<lambda>P. peval P (push_list a ks)) s)) = all_equations (peval A a) q' b' c' d' e' f' r' z' s'
?x < n \<Longrightarrow> map (\<lambda>P. peval P (push_list a ks)) r ! ?x = r' ?x
?x < n \<Longrightarrow> map (\<lambda>P. peval P (push_list a ks)) z ! ?x = z' ?x
?x < Suc m \<Longrightarrow> map (\<lambda>P. peval P (push_list a ks)) s ! ?x = s' ?x
r_list \<equiv> map r' [0..<n]
s_list \<equiv> map s' [0..<Suc m]
z_list \<equiv> map z' [0..<n]

goal (1 subgoal):
 1. all_equations (peval A a) q' b' c' d' e' f' r' z' s' \<Longrightarrow> all_equations (peval A a) q' b' c' d' e' f' ((!) (map (\<lambda>P. peval P (push_list a ks)) r)) ((!) (map (\<lambda>P. peval P (push_list a ks)) z)) ((!) (map (\<lambda>P. peval P (push_list a ks)) s))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval [ALLEQ] A' q b c d e f r z s (push_list a ks)

goal (1 subgoal):
 1. eval DR a \<Longrightarrow> eval DS a
[PROOF STEP]
thus "eval DS a"
[PROOF STATE]
proof (prove)
using this:
eval [ALLEQ] A' q b c d e f r z s (push_list a ks)

goal (1 subgoal):
 1. eval DS a
[PROOF STEP]
unfolding DS_def
[PROOF STATE]
proof (prove)
using this:
eval [ALLEQ] A' q b c d e f r z s (push_list a ks)

goal (1 subgoal):
 1. eval ([\<exists>number_of_ex_vars] [ALLEQ] A' q b c d e f r z s) a
[PROOF STEP]
using \<open>number_of_ex_vars = length ks\<close>
[PROOF STATE]
proof (prove)
using this:
eval [ALLEQ] A' q b c d e f r z s (push_list a ks)
number_of_ex_vars = length ks

goal (1 subgoal):
 1. eval ([\<exists>number_of_ex_vars] [ALLEQ] A' q b c d e f r z s) a
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
eval DS a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eval DS ?a = eval DR ?a

goal (1 subgoal):
 1. is_dioph_rel DR
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eval DS ?a = eval DR ?a

goal (1 subgoal):
 1. is_dioph_rel DR
[PROOF STEP]
have "is_dioph_rel DS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel DS
[PROOF STEP]
unfolding DS_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel ([\<exists>number_of_ex_vars] [ALLEQ] A' q b c d e f r z s)
[PROOF STEP]
using all_equations_dioph \<open>length r = n\<close> \<open>length z = n\<close> \<open>length s = Suc m\<close> assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length ?r = n; length ?z = n; length ?s = Suc m\<rbrakk> \<Longrightarrow> is_dioph_rel [ALLEQ] ?A ?q ?b ?c ?d ?e ?f ?r ?z ?s
length r = n
length z = n
length s = Suc m
DR \<equiv> [RM] A

goal (1 subgoal):
 1. is_dioph_rel ([\<exists>number_of_ex_vars] [ALLEQ] A' q b c d e f r z s)
[PROOF STEP]
by (auto simp: dioph)
[PROOF STATE]
proof (state)
this:
is_dioph_rel DS

goal (1 subgoal):
 1. is_dioph_rel DR
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eval DS ?a = eval DR ?a
is_dioph_rel DS
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval DS ?a = eval DR ?a
is_dioph_rel DS

goal (1 subgoal):
 1. is_dioph_rel DR
[PROOF STEP]
using is_dioph_rel_def
[PROOF STATE]
proof (prove)
using this:
eval DS ?a = eval DR ?a
is_dioph_rel DS
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. is_dioph_rel DR
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_dioph_rel DR

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unfold_lesub_list: "xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys = Listn.le r xs ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys) = Listn.le r xs ys
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys) = Listn.le r xs ys
[PROOF STEP]
by (simp add: lesub_def)


[STATEMENT]
lemma Nil_le_conv [iff]: "([] [\<sqsubseteq>\<^bsub>r\<^esub>] ys) = (ys = [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([] [\<sqsubseteq>\<^bsub>r\<^esub>] ys) = (ys = [])
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([] [\<sqsubseteq>\<^bsub>r\<^esub>] ys) = (ys = [])
[PROOF STEP]
apply (unfold lesub_def Listn.le_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all2 r [] ys = (ys = [])
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Cons_notle_Nil [iff]: "\<not> x#xs [\<sqsubseteq>\<^bsub>r\<^esub>] []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> x # xs [\<sqsubseteq>\<^bsub>r\<^esub>] []
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> x # xs [\<sqsubseteq>\<^bsub>r\<^esub>] []
[PROOF STEP]
apply (unfold lesub_def Listn.le_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> list_all2 r (x # xs) []
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_update_le_cong:
  "\<lbrakk> i<size xs; xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys; x \<sqsubseteq>\<^sub>r y \<rbrakk> \<Longrightarrow> xs[i:=x] [\<sqsubseteq>\<^bsub>r\<^esub>] ys[i:=y]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < length xs; xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys; x \<sqsubseteq>\<^bsub>r\<^esub> y\<rbrakk> \<Longrightarrow> xs[i := x] [\<sqsubseteq>\<^bsub>r\<^esub>] ys[i := y]
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < length xs; xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys; x \<sqsubseteq>\<^bsub>r\<^esub> y\<rbrakk> \<Longrightarrow> xs[i := x] [\<sqsubseteq>\<^bsub>r\<^esub>] ys[i := y]
[PROOF STEP]
apply (unfold unfold_lesub_list)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < length xs; Listn.le r xs ys; x \<sqsubseteq>\<^bsub>r\<^esub> y\<rbrakk> \<Longrightarrow> Listn.le r (xs[i := x]) (ys[i := y])
[PROOF STEP]
apply (unfold Listn.le_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < length xs; list_all2 (\<lambda>x. lesub x r) xs ys; x \<sqsubseteq>\<^bsub>r\<^esub> y\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x. lesub x r) (xs[i := x]) (ys[i := y])
[PROOF STEP]
apply (simp add: list_all2_update_cong)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma le_listD: "\<lbrakk> xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys; p < size xs \<rbrakk> \<Longrightarrow> xs!p \<sqsubseteq>\<^sub>r ys!p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys; p < length xs\<rbrakk> \<Longrightarrow> xs ! p \<sqsubseteq>\<^bsub>r\<^esub> ys ! p
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys; p < length xs\<rbrakk> \<Longrightarrow> xs ! p \<sqsubseteq>\<^bsub>r\<^esub> ys ! p
[PROOF STEP]
by (simp add: Listn.le_def lesub_def list_all2_nthD)


[STATEMENT]
lemma le_list_refl: "\<forall>x. x \<sqsubseteq>\<^sub>r x \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. x \<sqsubseteq>\<^bsub>r\<^esub> x \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] xs
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. x \<sqsubseteq>\<^bsub>r\<^esub> x \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] xs
[PROOF STEP]
apply (simp add: unfold_lesub_list lesub_def Listn.le_def list_all2_refl)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma le_list_trans: "\<lbrakk> order r; xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys; ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs \<rbrakk> \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>order r; xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys; ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs\<rbrakk> \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>order r; xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys; ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs\<rbrakk> \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs
[PROOF STEP]
apply (unfold unfold_lesub_list)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>order r; Listn.le r xs ys; Listn.le r ys zs\<rbrakk> \<Longrightarrow> Listn.le r xs zs
[PROOF STEP]
apply (unfold Listn.le_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>order r; list_all2 (\<lambda>x. lesub x r) xs ys; list_all2 (\<lambda>x. lesub x r) ys zs\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x. lesub x r) xs zs
[PROOF STEP]
apply (rule list_all2_trans)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b c. \<lbrakk>order r; list_all2 (\<lambda>x. lesub x r) xs ys; list_all2 (\<lambda>x. lesub x r) ys zs; ?P1.0 a b; ?P2.0 b c\<rbrakk> \<Longrightarrow> a \<sqsubseteq>\<^bsub>r\<^esub> c
 2. \<lbrakk>order r; list_all2 (\<lambda>x. lesub x r) xs ys; list_all2 (\<lambda>x. lesub x r) ys zs\<rbrakk> \<Longrightarrow> list_all2 ?P1.0 xs ?bs
 3. \<lbrakk>order r; list_all2 (\<lambda>x. lesub x r) xs ys; list_all2 (\<lambda>x. lesub x r) ys zs\<rbrakk> \<Longrightarrow> list_all2 ?P2.0 ?bs zs
[PROOF STEP]
apply (erule order_trans)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b c. \<lbrakk>list_all2 (\<lambda>x. lesub x r) xs ys; list_all2 (\<lambda>x. lesub x r) ys zs; ?P1.0 a b; ?P2.0 b c\<rbrakk> \<Longrightarrow> a \<sqsubseteq>\<^bsub>r\<^esub> ?y4 a b c
 2. \<And>a b c. \<lbrakk>list_all2 (\<lambda>x. lesub x r) xs ys; list_all2 (\<lambda>x. lesub x r) ys zs; ?P1.0 a b; ?P2.0 b c\<rbrakk> \<Longrightarrow> ?y4 a b c \<sqsubseteq>\<^bsub>r\<^esub> c
 3. \<lbrakk>order r; list_all2 (\<lambda>x. lesub x r) xs ys; list_all2 (\<lambda>x. lesub x r) ys zs\<rbrakk> \<Longrightarrow> list_all2 ?P1.0 xs ?bs
 4. \<lbrakk>order r; list_all2 (\<lambda>x. lesub x r) xs ys; list_all2 (\<lambda>x. lesub x r) ys zs\<rbrakk> \<Longrightarrow> list_all2 ?P2.0 ?bs zs
[PROOF STEP]
apply assumption+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma le_list_antisym: "\<lbrakk> order r; xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys; ys [\<sqsubseteq>\<^bsub>r\<^esub>] xs \<rbrakk> \<Longrightarrow> xs = ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>order r; xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys; ys [\<sqsubseteq>\<^bsub>r\<^esub>] xs\<rbrakk> \<Longrightarrow> xs = ys
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>order r; xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys; ys [\<sqsubseteq>\<^bsub>r\<^esub>] xs\<rbrakk> \<Longrightarrow> xs = ys
[PROOF STEP]
apply (unfold unfold_lesub_list)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>order r; Listn.le r xs ys; Listn.le r ys xs\<rbrakk> \<Longrightarrow> xs = ys
[PROOF STEP]
apply (unfold Listn.le_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>order r; list_all2 (\<lambda>x. lesub x r) xs ys; list_all2 (\<lambda>x. lesub x r) ys xs\<rbrakk> \<Longrightarrow> xs = ys
[PROOF STEP]
apply (rule list_all2_antisym)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>order r; list_all2 (\<lambda>x. lesub x r) xs ys; list_all2 (\<lambda>x. lesub x r) ys xs; ?P x y; ?Q y x\<rbrakk> \<Longrightarrow> x = y
 2. \<lbrakk>order r; list_all2 (\<lambda>x. lesub x r) xs ys; list_all2 (\<lambda>x. lesub x r) ys xs\<rbrakk> \<Longrightarrow> list_all2 ?P xs ys
 3. \<lbrakk>order r; list_all2 (\<lambda>x. lesub x r) xs ys; list_all2 (\<lambda>x. lesub x r) ys xs\<rbrakk> \<Longrightarrow> list_all2 ?Q ys xs
[PROOF STEP]
apply (rule order_antisym)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>order r; list_all2 (\<lambda>x. lesub x r) xs ys; list_all2 (\<lambda>x. lesub x r) ys xs; ?P x y; ?Q y x\<rbrakk> \<Longrightarrow> order (?r4 x y)
 2. \<And>x y. \<lbrakk>order r; list_all2 (\<lambda>x. lesub x r) xs ys; list_all2 (\<lambda>x. lesub x r) ys xs; ?P x y; ?Q y x\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>?r4 x y\<^esub> y
 3. \<And>x y. \<lbrakk>order r; list_all2 (\<lambda>x. lesub x r) xs ys; list_all2 (\<lambda>x. lesub x r) ys xs; ?P x y; ?Q y x\<rbrakk> \<Longrightarrow> y \<sqsubseteq>\<^bsub>?r4 x y\<^esub> x
 4. \<lbrakk>order r; list_all2 (\<lambda>x. lesub x r) xs ys; list_all2 (\<lambda>x. lesub x r) ys xs\<rbrakk> \<Longrightarrow> list_all2 ?P xs ys
 5. \<lbrakk>order r; list_all2 (\<lambda>x. lesub x r) xs ys; list_all2 (\<lambda>x. lesub x r) ys xs\<rbrakk> \<Longrightarrow> list_all2 ?Q ys xs
[PROOF STEP]
apply assumption+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma order_listI [simp, intro!]: "order r \<Longrightarrow> order(Listn.le r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order r \<Longrightarrow> order (Listn.le r)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order r \<Longrightarrow> order (Listn.le r)
[PROOF STEP]
apply (subst order_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order r \<Longrightarrow> (\<forall>x. x [\<sqsubseteq>\<^bsub>r\<^esub>] x) \<and> (\<forall>x y. x [\<sqsubseteq>\<^bsub>r\<^esub>] y \<and> y [\<sqsubseteq>\<^bsub>r\<^esub>] x \<longrightarrow> x = y) \<and> (\<forall>x y z. x [\<sqsubseteq>\<^bsub>r\<^esub>] y \<and> y [\<sqsubseteq>\<^bsub>r\<^esub>] z \<longrightarrow> x [\<sqsubseteq>\<^bsub>r\<^esub>] z)
[PROOF STEP]
apply (blast intro: le_list_refl le_list_trans le_list_antisym
             dest: order_refl)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma lesub_list_impl_same_size [simp]: "xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys \<Longrightarrow> size ys = size xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys \<Longrightarrow> length ys = length xs
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys \<Longrightarrow> length ys = length xs
[PROOF STEP]
apply (unfold Listn.le_def lesub_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all2 r xs ys \<Longrightarrow> length ys = length xs
[PROOF STEP]
apply (simp add: list_all2_lengthD)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma lesssub_lengthD: "xs [\<sqsubset>\<^sub>r] ys \<Longrightarrow> size ys = size xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs [\<sqsubset>\<^bsub>r\<^esub>] ys \<Longrightarrow> length ys = length xs
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs [\<sqsubset>\<^bsub>r\<^esub>] ys \<Longrightarrow> length ys = length xs
[PROOF STEP]
apply (unfold lesssub_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys \<and> xs \<noteq> ys \<Longrightarrow> length ys = length xs
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma le_list_appendI: "a [\<sqsubseteq>\<^bsub>r\<^esub>] b \<Longrightarrow> c [\<sqsubseteq>\<^bsub>r\<^esub>] d \<Longrightarrow> a@c [\<sqsubseteq>\<^bsub>r\<^esub>] b@d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a [\<sqsubseteq>\<^bsub>r\<^esub>] b; c [\<sqsubseteq>\<^bsub>r\<^esub>] d\<rbrakk> \<Longrightarrow> a @ c [\<sqsubseteq>\<^bsub>r\<^esub>] b @ d
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a [\<sqsubseteq>\<^bsub>r\<^esub>] b; c [\<sqsubseteq>\<^bsub>r\<^esub>] d\<rbrakk> \<Longrightarrow> a @ c [\<sqsubseteq>\<^bsub>r\<^esub>] b @ d
[PROOF STEP]
apply (unfold Listn.le_def lesub_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_all2 r a b; list_all2 r c d\<rbrakk> \<Longrightarrow> list_all2 r (a @ c) (b @ d)
[PROOF STEP]
apply (rule list_all2_appendI, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma le_listI:
  assumes "length a = length b"
  assumes "\<And>n. n < length a \<Longrightarrow> a!n \<sqsubseteq>\<^sub>r b!n"
  shows "a [\<sqsubseteq>\<^bsub>r\<^esub>] b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a [\<sqsubseteq>\<^bsub>r\<^esub>] b
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a [\<sqsubseteq>\<^bsub>r\<^esub>] b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a [\<sqsubseteq>\<^bsub>r\<^esub>] b
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
length a = length b
?n < length a \<Longrightarrow> a ! ?n \<sqsubseteq>\<^bsub>r\<^esub> b ! ?n
[PROOF STEP]
have "list_all2 r a b"
[PROOF STATE]
proof (prove)
using this:
length a = length b
?n < length a \<Longrightarrow> a ! ?n \<sqsubseteq>\<^bsub>r\<^esub> b ! ?n

goal (1 subgoal):
 1. list_all2 r a b
[PROOF STEP]
by (simp add: list_all2_all_nthI lesub_def)
[PROOF STATE]
proof (state)
this:
list_all2 r a b

goal (1 subgoal):
 1. a [\<sqsubseteq>\<^bsub>r\<^esub>] b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
list_all2 r a b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
list_all2 r a b

goal (1 subgoal):
 1. a [\<sqsubseteq>\<^bsub>r\<^esub>] b
[PROOF STEP]
by (simp add: Listn.le_def lesub_def)
[PROOF STATE]
proof (state)
this:
a [\<sqsubseteq>\<^bsub>r\<^esub>] b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma listI: "\<lbrakk> size xs = n; set xs \<subseteq> A \<rbrakk> \<Longrightarrow> xs \<in> list n A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs = n; set xs \<subseteq> A\<rbrakk> \<Longrightarrow> xs \<in> list n A
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs = n; set xs \<subseteq> A\<rbrakk> \<Longrightarrow> xs \<in> list n A
[PROOF STEP]
apply (unfold list_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs = n; set xs \<subseteq> A\<rbrakk> \<Longrightarrow> xs \<in> {xs. length xs = n \<and> set xs \<subseteq> A}
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma listE_length [simp]: "xs \<in> list n A \<Longrightarrow> size xs = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> list n A \<Longrightarrow> length xs = n
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> list n A \<Longrightarrow> length xs = n
[PROOF STEP]
apply (unfold list_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> {xs. length xs = n \<and> set xs \<subseteq> A} \<Longrightarrow> length xs = n
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma less_lengthI: "\<lbrakk> xs \<in> list n A; p < n \<rbrakk> \<Longrightarrow> p < size xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs \<in> list n A; p < n\<rbrakk> \<Longrightarrow> p < length xs
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs \<in> list n A; p < n\<rbrakk> \<Longrightarrow> p < length xs
[PROOF STEP]
by simp


[STATEMENT]
lemma listE_set [simp]: "xs \<in> list n A \<Longrightarrow> set xs \<subseteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> list n A \<Longrightarrow> set xs \<subseteq> A
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> list n A \<Longrightarrow> set xs \<subseteq> A
[PROOF STEP]
apply (unfold list_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> {xs. length xs = n \<and> set xs \<subseteq> A} \<Longrightarrow> set xs \<subseteq> A
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_0 [simp]: "list 0 A = {[]}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list 0 A = {[]}
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list 0 A = {[]}
[PROOF STEP]
apply (unfold list_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {xs. length xs = 0 \<and> set xs \<subseteq> A} = {[]}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma in_list_Suc_iff:
  "(xs \<in> list (Suc n) A) = (\<exists>y\<in>A. \<exists>ys \<in> list n A. xs = y#ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs \<in> list (Suc n) A) = (\<exists>y\<in>A. \<exists>ys\<in>list n A. xs = y # ys)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs \<in> list (Suc n) A) = (\<exists>y\<in>A. \<exists>ys\<in>list n A. xs = y # ys)
[PROOF STEP]
apply (unfold list_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs \<in> {xs. length xs = Suc n \<and> set xs \<subseteq> A}) = (\<exists>y\<in>A. \<exists>ys\<in>{xs. length xs = n \<and> set xs \<subseteq> A}. xs = y # ys)
[PROOF STEP]
apply (case_tac "xs")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. xs = [] \<Longrightarrow> (xs \<in> {xs. length xs = Suc n \<and> set xs \<subseteq> A}) = (\<exists>y\<in>A. \<exists>ys\<in>{xs. length xs = n \<and> set xs \<subseteq> A}. xs = y # ys)
 2. \<And>a list. xs = a # list \<Longrightarrow> (xs \<in> {xs. length xs = Suc n \<and> set xs \<subseteq> A}) = (\<exists>y\<in>A. \<exists>ys\<in>{xs. length xs = n \<and> set xs \<subseteq> A}. xs = y # ys)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Cons_in_list_Suc [iff]:
  "(x#xs \<in> list (Suc n) A) = (x\<in>A \<and> xs \<in> list n A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x # xs \<in> list (Suc n) A) = (x \<in> A \<and> xs \<in> list n A)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x # xs \<in> list (Suc n) A) = (x \<in> A \<and> xs \<in> list n A)
[PROOF STEP]
apply (simp add: in_list_Suc_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_not_empty:
  "\<exists>a. a\<in>A \<Longrightarrow> \<exists>xs. xs \<in> list n A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. a \<in> A \<Longrightarrow> \<exists>xs. xs \<in> list n A
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. a \<in> A \<Longrightarrow> \<exists>xs. xs \<in> list n A
[PROOF STEP]
apply (induct "n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<exists>a. a \<in> A \<Longrightarrow> \<exists>xs. xs \<in> list 0 A
 2. \<And>n. \<lbrakk>\<exists>a. a \<in> A \<Longrightarrow> \<exists>xs. xs \<in> list n A; \<exists>a. a \<in> A\<rbrakk> \<Longrightarrow> \<exists>xs. xs \<in> list (Suc n) A
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<exists>a. a \<in> A \<Longrightarrow> \<exists>xs. xs \<in> list n A; \<exists>a. a \<in> A\<rbrakk> \<Longrightarrow> \<exists>xs. xs \<in> list (Suc n) A
[PROOF STEP]
apply (simp add: in_list_Suc_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<exists>xs. xs \<in> list n A; \<exists>a. a \<in> A\<rbrakk> \<Longrightarrow> \<exists>xs. \<exists>y\<in>A. \<exists>ys\<in>list n A. xs = y # ys
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma nth_in [rule_format, simp]:
  "\<forall>i n. size xs = n \<longrightarrow> set xs \<subseteq> A \<longrightarrow> i < n \<longrightarrow> (xs!i) \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i n. length xs = n \<longrightarrow> set xs \<subseteq> A \<longrightarrow> i < n \<longrightarrow> xs ! i \<in> A
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i n. length xs = n \<longrightarrow> set xs \<subseteq> A \<longrightarrow> i < n \<longrightarrow> xs ! i \<in> A
[PROOF STEP]
apply (induct "xs")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>i n. length [] = n \<longrightarrow> set [] \<subseteq> A \<longrightarrow> i < n \<longrightarrow> [] ! i \<in> A
 2. \<And>a xs. \<forall>i n. length xs = n \<longrightarrow> set xs \<subseteq> A \<longrightarrow> i < n \<longrightarrow> xs ! i \<in> A \<Longrightarrow> \<forall>i n. length (a # xs) = n \<longrightarrow> set (a # xs) \<subseteq> A \<longrightarrow> i < n \<longrightarrow> (a # xs) ! i \<in> A
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<forall>i n. length xs = n \<longrightarrow> set xs \<subseteq> A \<longrightarrow> i < n \<longrightarrow> xs ! i \<in> A \<Longrightarrow> \<forall>i n. length (a # xs) = n \<longrightarrow> set (a # xs) \<subseteq> A \<longrightarrow> i < n \<longrightarrow> (a # xs) ! i \<in> A
[PROOF STEP]
apply (simp add: nth_Cons split: nat.split)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma listE_nth_in: "\<lbrakk> xs \<in> list n A; i < n \<rbrakk> \<Longrightarrow> xs!i \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs \<in> list n A; i < n\<rbrakk> \<Longrightarrow> xs ! i \<in> A
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs \<in> list n A; i < n\<rbrakk> \<Longrightarrow> xs ! i \<in> A
[PROOF STEP]
by auto


[STATEMENT]
lemma listn_Cons_Suc [elim!]:
  "l#xs \<in> list n A \<Longrightarrow> (\<And>n'. n = Suc n' \<Longrightarrow> l \<in> A \<Longrightarrow> xs \<in> list n' A \<Longrightarrow> P) \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>l # xs \<in> list n A; \<And>n'. \<lbrakk>n = Suc n'; l \<in> A; xs \<in> list n' A\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>l # xs \<in> list n A; \<And>n'. \<lbrakk>n = Suc n'; l \<in> A; xs \<in> list n' A\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (cases n) auto


[STATEMENT]
lemma listn_appendE [elim!]:
  "a@b \<in> list n A \<Longrightarrow> (\<And>n1 n2. n=n1+n2 \<Longrightarrow> a \<in> list n1 A \<Longrightarrow> b \<in> list n2 A \<Longrightarrow> P) \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a @ b \<in> list n A; \<And>n1 n2. \<lbrakk>n = n1 + n2; a \<in> list n1 A; b \<in> list n2 A\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a @ b \<in> list n A; \<And>n1 n2. \<lbrakk>n = n1 + n2; a \<in> list n1 A; b \<in> list n2 A\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>a @ b \<in> list n A; \<And>n1 n2. \<lbrakk>n = n1 + n2; a \<in> list n1 A; b \<in> list n2 A\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
have "\<And>n. a@b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n=n1+n2 \<and> a \<in> list n1 A \<and> b \<in> list n2 A"
    (is "\<And>n. ?list a n \<Longrightarrow> \<exists>n1 n2. ?P a n n1 n2")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. a @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> a \<in> list n1 A \<and> b \<in> list n2 A
[PROOF STEP]
proof (induct a)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. [] @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> [] \<in> list n1 A \<and> b \<in> list n2 A
 2. \<And>a1 a2 n. \<lbrakk>\<And>n. a2 @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> a2 \<in> list n1 A \<and> b \<in> list n2 A; (a1 # a2) @ b \<in> list n A\<rbrakk> \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> a1 # a2 \<in> list n1 A \<and> b \<in> list n2 A
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. [] @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> [] \<in> list n1 A \<and> b \<in> list n2 A
 2. \<And>a1 a2 n. \<lbrakk>\<And>n. a2 @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> a2 \<in> list n1 A \<and> b \<in> list n2 A; (a1 # a2) @ b \<in> list n A\<rbrakk> \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> a1 # a2 \<in> list n1 A \<and> b \<in> list n2 A
[PROOF STEP]
assume "?list [] n"
[PROOF STATE]
proof (state)
this:
[] @ b \<in> list n A

goal (2 subgoals):
 1. \<And>n. [] @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> [] \<in> list n1 A \<and> b \<in> list n2 A
 2. \<And>a1 a2 n. \<lbrakk>\<And>n. a2 @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> a2 \<in> list n1 A \<and> b \<in> list n2 A; (a1 # a2) @ b \<in> list n A\<rbrakk> \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> a1 # a2 \<in> list n1 A \<and> b \<in> list n2 A
[PROOF STEP]
hence "?P [] n 0 n"
[PROOF STATE]
proof (prove)
using this:
[] @ b \<in> list n A

goal (1 subgoal):
 1. n = 0 + n \<and> [] \<in> list 0 A \<and> b \<in> list n A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n = 0 + n \<and> [] \<in> list 0 A \<and> b \<in> list n A

goal (2 subgoals):
 1. \<And>n. [] @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> [] \<in> list n1 A \<and> b \<in> list n2 A
 2. \<And>a1 a2 n. \<lbrakk>\<And>n. a2 @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> a2 \<in> list n1 A \<and> b \<in> list n2 A; (a1 # a2) @ b \<in> list n A\<rbrakk> \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> a1 # a2 \<in> list n1 A \<and> b \<in> list n2 A
[PROOF STEP]
thus "\<exists>n1 n2. ?P [] n n1 n2"
[PROOF STATE]
proof (prove)
using this:
n = 0 + n \<and> [] \<in> list 0 A \<and> b \<in> list n A

goal (1 subgoal):
 1. \<exists>n1 n2. n = n1 + n2 \<and> [] \<in> list n1 A \<and> b \<in> list n2 A
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<exists>n1 n2. n = n1 + n2 \<and> [] \<in> list n1 A \<and> b \<in> list n2 A

goal (1 subgoal):
 1. \<And>a1 a2 n. \<lbrakk>\<And>n. a2 @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> a2 \<in> list n1 A \<and> b \<in> list n2 A; (a1 # a2) @ b \<in> list n A\<rbrakk> \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> a1 # a2 \<in> list n1 A \<and> b \<in> list n2 A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a1 a2 n. \<lbrakk>\<And>n. a2 @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> a2 \<in> list n1 A \<and> b \<in> list n2 A; (a1 # a2) @ b \<in> list n A\<rbrakk> \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> a1 # a2 \<in> list n1 A \<and> b \<in> list n2 A
[PROOF STEP]
fix n l ls
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a1 a2 n. \<lbrakk>\<And>n. a2 @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> a2 \<in> list n1 A \<and> b \<in> list n2 A; (a1 # a2) @ b \<in> list n A\<rbrakk> \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> a1 # a2 \<in> list n1 A \<and> b \<in> list n2 A
[PROOF STEP]
assume "?list (l#ls) n"
[PROOF STATE]
proof (state)
this:
(l # ls) @ b \<in> list n A

goal (1 subgoal):
 1. \<And>a1 a2 n. \<lbrakk>\<And>n. a2 @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> a2 \<in> list n1 A \<and> b \<in> list n2 A; (a1 # a2) @ b \<in> list n A\<rbrakk> \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> a1 # a2 \<in> list n1 A \<and> b \<in> list n2 A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(l # ls) @ b \<in> list n A
[PROOF STEP]
obtain n' where n: "n = Suc n'" "l \<in> A" and n': "ls@b \<in> list n' A"
[PROOF STATE]
proof (prove)
using this:
(l # ls) @ b \<in> list n A

goal (1 subgoal):
 1. (\<And>n'. \<lbrakk>n = Suc n'; l \<in> A; ls @ b \<in> list n' A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
n = Suc n'
l \<in> A
ls @ b \<in> list n' A

goal (1 subgoal):
 1. \<And>a1 a2 n. \<lbrakk>\<And>n. a2 @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> a2 \<in> list n1 A \<and> b \<in> list n2 A; (a1 # a2) @ b \<in> list n A\<rbrakk> \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> a1 # a2 \<in> list n1 A \<and> b \<in> list n2 A
[PROOF STEP]
assume "\<And>n. ls @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A"
[PROOF STATE]
proof (state)
this:
ls @ b \<in> list ?n A \<Longrightarrow> \<exists>n1 n2. ?n = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A

goal (1 subgoal):
 1. \<And>a1 a2 n. \<lbrakk>\<And>n. a2 @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> a2 \<in> list n1 A \<and> b \<in> list n2 A; (a1 # a2) @ b \<in> list n A\<rbrakk> \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> a1 # a2 \<in> list n1 A \<and> b \<in> list n2 A
[PROOF STEP]
from this and n'
[PROOF STATE]
proof (chain)
picking this:
ls @ b \<in> list ?n A \<Longrightarrow> \<exists>n1 n2. ?n = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A
ls @ b \<in> list n' A
[PROOF STEP]
have "\<exists>n1 n2. n' = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A"
[PROOF STATE]
proof (prove)
using this:
ls @ b \<in> list ?n A \<Longrightarrow> \<exists>n1 n2. ?n = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A
ls @ b \<in> list n' A

goal (1 subgoal):
 1. \<exists>n1 n2. n' = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<exists>n1 n2. n' = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A

goal (1 subgoal):
 1. \<And>a1 a2 n. \<lbrakk>\<And>n. a2 @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> a2 \<in> list n1 A \<and> b \<in> list n2 A; (a1 # a2) @ b \<in> list n A\<rbrakk> \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> a1 # a2 \<in> list n1 A \<and> b \<in> list n2 A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n1 n2. n' = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A
[PROOF STEP]
obtain n1 n2 where "n' = n1 + n2" "ls \<in> list n1 A" "b \<in> list n2 A"
[PROOF STATE]
proof (prove)
using this:
\<exists>n1 n2. n' = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A

goal (1 subgoal):
 1. (\<And>n1 n2. \<lbrakk>n' = n1 + n2; ls \<in> list n1 A; b \<in> list n2 A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
n' = n1 + n2
ls \<in> list n1 A
b \<in> list n2 A

goal (1 subgoal):
 1. \<And>a1 a2 n. \<lbrakk>\<And>n. a2 @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> a2 \<in> list n1 A \<and> b \<in> list n2 A; (a1 # a2) @ b \<in> list n A\<rbrakk> \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> a1 # a2 \<in> list n1 A \<and> b \<in> list n2 A
[PROOF STEP]
with n
[PROOF STATE]
proof (chain)
picking this:
n = Suc n'
l \<in> A
n' = n1 + n2
ls \<in> list n1 A
b \<in> list n2 A
[PROOF STEP]
have "?P (l#ls) n (n1+1) n2"
[PROOF STATE]
proof (prove)
using this:
n = Suc n'
l \<in> A
n' = n1 + n2
ls \<in> list n1 A
b \<in> list n2 A

goal (1 subgoal):
 1. n = n1 + 1 + n2 \<and> l # ls \<in> list (n1 + 1) A \<and> b \<in> list n2 A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n = n1 + 1 + n2 \<and> l # ls \<in> list (n1 + 1) A \<and> b \<in> list n2 A

goal (1 subgoal):
 1. \<And>a1 a2 n. \<lbrakk>\<And>n. a2 @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> a2 \<in> list n1 A \<and> b \<in> list n2 A; (a1 # a2) @ b \<in> list n A\<rbrakk> \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> a1 # a2 \<in> list n1 A \<and> b \<in> list n2 A
[PROOF STEP]
thus "\<exists>n1 n2. ?P (l#ls) n n1 n2"
[PROOF STATE]
proof (prove)
using this:
n = n1 + 1 + n2 \<and> l # ls \<in> list (n1 + 1) A \<and> b \<in> list n2 A

goal (1 subgoal):
 1. \<exists>n1 n2. n = n1 + n2 \<and> l # ls \<in> list n1 A \<and> b \<in> list n2 A
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>n1 n2. n = n1 + n2 \<and> l # ls \<in> list n1 A \<and> b \<in> list n2 A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
a @ b \<in> list ?n A \<Longrightarrow> \<exists>n1 n2. ?n = n1 + n2 \<and> a \<in> list n1 A \<and> b \<in> list n2 A

goal (1 subgoal):
 1. \<lbrakk>a @ b \<in> list n A; \<And>n1 n2. \<lbrakk>n = n1 + n2; a \<in> list n1 A; b \<in> list n2 A\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a @ b \<in> list ?n A \<Longrightarrow> \<exists>n1 n2. ?n = n1 + n2 \<and> a \<in> list n1 A \<and> b \<in> list n2 A

goal (1 subgoal):
 1. \<lbrakk>a @ b \<in> list n A; \<And>n1 n2. \<lbrakk>n = n1 + n2; a \<in> list n1 A; b \<in> list n2 A\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
assume "a@b \<in> list n A" "\<And>n1 n2. n=n1+n2 \<Longrightarrow> a \<in> list n1 A \<Longrightarrow> b \<in> list n2 A \<Longrightarrow> P"
[PROOF STATE]
proof (state)
this:
a @ b \<in> list n A
\<lbrakk>n = ?n1.0 + ?n2.0; a \<in> list ?n1.0 A; b \<in> list ?n2.0 A\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. \<lbrakk>a @ b \<in> list n A; \<And>n1 n2. \<lbrakk>n = n1 + n2; a \<in> list n1 A; b \<in> list n2 A\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a @ b \<in> list ?n A \<Longrightarrow> \<exists>n1 n2. ?n = n1 + n2 \<and> a \<in> list n1 A \<and> b \<in> list n2 A
a @ b \<in> list n A
\<lbrakk>n = ?n1.0 + ?n2.0; a \<in> list ?n1.0 A; b \<in> list ?n2.0 A\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a @ b \<in> list ?n A \<Longrightarrow> \<exists>n1 n2. ?n = n1 + n2 \<and> a \<in> list n1 A \<and> b \<in> list n2 A
a @ b \<in> list n A
\<lbrakk>n = ?n1.0 + ?n2.0; a \<in> list ?n1.0 A; b \<in> list ?n2.0 A\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma listt_update_in_list [simp, intro!]:
  "\<lbrakk> xs \<in> list n A; x\<in>A \<rbrakk> \<Longrightarrow> xs[i := x] \<in> list n A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs \<in> list n A; x \<in> A\<rbrakk> \<Longrightarrow> xs[i := x] \<in> list n A
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs \<in> list n A; x \<in> A\<rbrakk> \<Longrightarrow> xs[i := x] \<in> list n A
[PROOF STEP]
apply (unfold list_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs \<in> {xs. length xs = n \<and> set xs \<subseteq> A}; x \<in> A\<rbrakk> \<Longrightarrow> xs[i := x] \<in> {xs. length xs = n \<and> set xs \<subseteq> A}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_appendI [intro?]:
  "\<lbrakk> a \<in> list n A; b \<in> list m A \<rbrakk> \<Longrightarrow> a @ b \<in> list (n+m) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> list n A; b \<in> list m A\<rbrakk> \<Longrightarrow> a @ b \<in> list (n + m) A
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> list n A; b \<in> list m A\<rbrakk> \<Longrightarrow> a @ b \<in> list (n + m) A
[PROOF STEP]
by (unfold list_def) auto


[STATEMENT]
lemma list_map [simp]: "(map f xs \<in> list (size xs) A) = (f ` set xs \<subseteq> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (map f xs \<in> list (length xs) A) = (f ` set xs \<subseteq> A)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (map f xs \<in> list (length xs) A) = (f ` set xs \<subseteq> A)
[PROOF STEP]
by (unfold list_def) simp


[STATEMENT]
lemma list_replicateI [intro]: "x \<in> A \<Longrightarrow> replicate n x \<in> list n A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> A \<Longrightarrow> replicate n x \<in> list n A
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> A \<Longrightarrow> replicate n x \<in> list n A
[PROOF STEP]
by (induct n) auto


[STATEMENT]
lemma plus_list_Nil [simp]: "[] [\<squnion>\<^bsub>f\<^esub>] xs = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] [+f] xs = []
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] [+f] xs = []
[PROOF STEP]
apply (unfold plussub_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map2 f [] xs = []
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma plus_list_Cons [simp]:
  "(x#xs) [\<squnion>\<^bsub>f\<^esub>] ys = (case ys of [] \<Rightarrow> [] | y#ys \<Rightarrow> (x \<squnion>\<^sub>f y)#(xs [\<squnion>\<^bsub>f\<^esub>] ys))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x # xs [+f] ys = (case ys of [] \<Rightarrow> [] | y # ys \<Rightarrow> (x \<squnion>\<^bsub>f\<^esub> y) # xs [+f] ys)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x # xs [+f] ys = (case ys of [] \<Rightarrow> [] | y # ys \<Rightarrow> (x \<squnion>\<^bsub>f\<^esub> y) # xs [+f] ys)
[PROOF STEP]
by (simp add: plussub_def split: list.split)


[STATEMENT]
lemma length_plus_list [rule_format, simp]:
  "\<forall>ys. size(xs [\<squnion>\<^bsub>f\<^esub>] ys) = min(size xs) (size ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ys. length (xs [+f] ys) = min (length xs) (length ys)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ys. length (xs [+f] ys) = min (length xs) (length ys)
[PROOF STEP]
apply (induct xs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>ys. length ([] [+f] ys) = min (length []) (length ys)
 2. \<And>a xs. \<forall>ys. length (xs [+f] ys) = min (length xs) (length ys) \<Longrightarrow> \<forall>ys. length (a # xs [+f] ys) = min (length (a # xs)) (length ys)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<forall>ys. length (xs [+f] ys) = min (length xs) (length ys) \<Longrightarrow> \<forall>ys. length (a # xs [+f] ys) = min (length (a # xs)) (length ys)
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs ys. \<forall>ys. length (xs [+f] ys) = min (length xs) (length ys) \<Longrightarrow> length (a # xs [+f] ys) = min (length (a # xs)) (length ys)
[PROOF STEP]
apply (simp (no_asm_simp) split: list.split)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done