[STATEMENT]
lemma exec_step_ind_equiv:
 "exec_step P h stk loc C M pc ics frs sh = (xp', h', frs', sh')
   = exec_step_ind (exec_step_input P C M pc ics) P h stk loc C M pc ics frs sh (xp', h', frs', sh')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (exec_step P h stk loc C M pc ics frs sh = (xp', h', frs', sh')) = exec_step_ind (exec_step_input P C M pc ics) P h stk loc C M pc ics frs sh (xp', h', frs', sh')
[PROOF STEP]
using exec_step_imp_exec_step_ind exec_step_ind_imp_exec_step
[PROOF STATE]
proof (prove)
using this:
exec_step ?P ?h ?stk ?loc ?C ?M ?pc ?ics ?frs ?sh = (?xp', ?h', ?frs', ?sh') \<Longrightarrow> exec_step_ind (exec_step_input ?P ?C ?M ?pc ?ics) ?P ?h ?stk ?loc ?C ?M ?pc ?ics ?frs ?sh (?xp', ?h', ?frs', ?sh')
\<lbrakk>exec_step_ind ?si ?P ?h ?stk ?loc ?C ?M ?pc ?ics ?frs ?sh (?xp', ?h', ?frs', ?sh'); exec_step_input ?P ?C ?M ?pc ?ics = ?si\<rbrakk> \<Longrightarrow> exec_step ?P ?h ?stk ?loc ?C ?M ?pc ?ics ?frs ?sh = (?xp', ?h', ?frs', ?sh')

goal (1 subgoal):
 1. (exec_step P h stk loc C M pc ics frs sh = (xp', h', frs', sh')) = exec_step_ind (exec_step_input P C M pc ics) P h stk loc C M pc ics frs sh (xp', h', frs', sh')
[PROOF STEP]
by auto


[STATEMENT]
lemma set_pred_eq_transfer[transfer_rule]:
  assumes [transfer_rule]: "right_total A"
  shows
    "((rel_set A ===> (=)) ===> (rel_set A ===> (=)) ===> (=))
      (\<lambda>X Y. \<forall>s\<subseteq>Collect (Domainp A). X s = Y s)
      ((=)::['b set \<Rightarrow> bool, 'b set \<Rightarrow> bool] \<Rightarrow> bool)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((rel_set A ===> (=)) ===> (rel_set A ===> (=)) ===> (=)) (\<lambda>X Y. \<forall>s\<subseteq>Collect (Domainp A). X s = Y s) (=)
[PROOF STEP]
proof(intro rel_funI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>(rel_set A ===> (=)) x y; (rel_set A ===> (=)) xa ya\<rbrakk> \<Longrightarrow> (\<forall>s\<subseteq>Collect (Domainp A). x s = xa s) = (y = ya)
[PROOF STEP]
let ?sA = "Collect (Domainp A)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>(rel_set A ===> (=)) x y; (rel_set A ===> (=)) xa ya\<rbrakk> \<Longrightarrow> (\<forall>s\<subseteq>Collect (Domainp A). x s = xa s) = (y = ya)
[PROOF STEP]
fix X Y :: "'a set \<Rightarrow> bool"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>(rel_set A ===> (=)) x y; (rel_set A ===> (=)) xa ya\<rbrakk> \<Longrightarrow> (\<forall>s\<subseteq>Collect (Domainp A). x s = xa s) = (y = ya)
[PROOF STEP]
fix X' Y' :: "'b set \<Rightarrow> bool"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>(rel_set A ===> (=)) x y; (rel_set A ===> (=)) xa ya\<rbrakk> \<Longrightarrow> (\<forall>s\<subseteq>Collect (Domainp A). x s = xa s) = (y = ya)
[PROOF STEP]
assume rs: "(rel_set A ===> (=)) X X'" "(rel_set A ===> (=)) Y Y'"
[PROOF STATE]
proof (state)
this:
(rel_set A ===> (=)) X X'
(rel_set A ===> (=)) Y Y'

goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>(rel_set A ===> (=)) x y; (rel_set A ===> (=)) xa ya\<rbrakk> \<Longrightarrow> (\<forall>s\<subseteq>Collect (Domainp A). x s = xa s) = (y = ya)
[PROOF STEP]
show "(\<forall>s\<subseteq>?sA. X s = Y s) = (X' = Y')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>s\<subseteq>Collect (Domainp A). X s = Y s) = (X' = Y')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>s\<subseteq>Collect (Domainp A). X s = Y s \<Longrightarrow> X' = Y'
 2. X' = Y' \<Longrightarrow> \<forall>s\<subseteq>Collect (Domainp A). X s = Y s
[PROOF STEP]
assume X_eq_Y: "\<forall>s\<subseteq>?sA. X s = Y s"
[PROOF STATE]
proof (state)
this:
\<forall>s\<subseteq>Collect (Domainp A). X s = Y s

goal (2 subgoals):
 1. \<forall>s\<subseteq>Collect (Domainp A). X s = Y s \<Longrightarrow> X' = Y'
 2. X' = Y' \<Longrightarrow> \<forall>s\<subseteq>Collect (Domainp A). X s = Y s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>s\<subseteq>Collect (Domainp A). X s = Y s

goal (2 subgoals):
 1. \<forall>s\<subseteq>Collect (Domainp A). X s = Y s \<Longrightarrow> X' = Y'
 2. X' = Y' \<Longrightarrow> \<forall>s\<subseteq>Collect (Domainp A). X s = Y s
[PROOF STEP]
fix s'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>s\<subseteq>Collect (Domainp A). X s = Y s \<Longrightarrow> X' = Y'
 2. X' = Y' \<Longrightarrow> \<forall>s\<subseteq>Collect (Domainp A). X s = Y s
[PROOF STEP]
assume "X' s'"
[PROOF STATE]
proof (state)
this:
X' s'

goal (2 subgoals):
 1. \<forall>s\<subseteq>Collect (Domainp A). X s = Y s \<Longrightarrow> X' = Y'
 2. X' = Y' \<Longrightarrow> \<forall>s\<subseteq>Collect (Domainp A). X s = Y s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
X' s'
[PROOF STEP]
obtain s where "rel_set A s s'"
[PROOF STATE]
proof (prove)
using this:
X' s'

goal (1 subgoal):
 1. (\<And>s. rel_set A s s' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson assms right_total_def right_total_rel_set)
[PROOF STATE]
proof (state)
this:
rel_set A s s'

goal (2 subgoals):
 1. \<forall>s\<subseteq>Collect (Domainp A). X s = Y s \<Longrightarrow> X' = Y'
 2. X' = Y' \<Longrightarrow> \<forall>s\<subseteq>Collect (Domainp A). X s = Y s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rel_set A s s'
[PROOF STEP]
have "X s"
[PROOF STATE]
proof (prove)
using this:
rel_set A s s'

goal (1 subgoal):
 1. X s
[PROOF STEP]
using rs(1)
[PROOF STATE]
proof (prove)
using this:
rel_set A s s'
(rel_set A ===> (=)) X X'

goal (1 subgoal):
 1. X s
[PROOF STEP]
unfolding rel_fun_def
[PROOF STATE]
proof (prove)
using this:
rel_set A s s'
\<forall>x y. rel_set A x y \<longrightarrow> X x = X' y

goal (1 subgoal):
 1. X s
[PROOF STEP]
by (simp add: \<open>X' s'\<close>)
[PROOF STATE]
proof (state)
this:
X s

goal (2 subgoals):
 1. \<forall>s\<subseteq>Collect (Domainp A). X s = Y s \<Longrightarrow> X' = Y'
 2. X' = Y' \<Longrightarrow> \<forall>s\<subseteq>Collect (Domainp A). X s = Y s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
X s

goal (2 subgoals):
 1. \<forall>s\<subseteq>Collect (Domainp A). X s = Y s \<Longrightarrow> X' = Y'
 2. X' = Y' \<Longrightarrow> \<forall>s\<subseteq>Collect (Domainp A). X s = Y s
[PROOF STEP]
from \<open>rel_set A s s'\<close>
[PROOF STATE]
proof (chain)
picking this:
rel_set A s s'
[PROOF STEP]
have "s \<subseteq> ?sA"
[PROOF STATE]
proof (prove)
using this:
rel_set A s s'

goal (1 subgoal):
 1. s \<subseteq> Collect (Domainp A)
[PROOF STEP]
unfolding Ball_Collect[symmetric]
[PROOF STATE]
proof (prove)
using this:
rel_set A s s'

goal (1 subgoal):
 1. Ball s (Domainp A)
[PROOF STEP]
by (auto dest: rel_setD1)
[PROOF STATE]
proof (state)
this:
s \<subseteq> Collect (Domainp A)

goal (2 subgoals):
 1. \<forall>s\<subseteq>Collect (Domainp A). X s = Y s \<Longrightarrow> X' = Y'
 2. X' = Y' \<Longrightarrow> \<forall>s\<subseteq>Collect (Domainp A). X s = Y s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
X s
s \<subseteq> Collect (Domainp A)
[PROOF STEP]
have "Y' s'"
[PROOF STATE]
proof (prove)
using this:
X s
s \<subseteq> Collect (Domainp A)

goal (1 subgoal):
 1. Y' s'
[PROOF STEP]
using rs(2)[unfolded rel_fun_def] \<open>rel_set A s s'\<close>
[PROOF STATE]
proof (prove)
using this:
X s
s \<subseteq> Collect (Domainp A)
\<forall>x y. rel_set A x y \<longrightarrow> Y x = Y' y
rel_set A s s'

goal (1 subgoal):
 1. Y' s'
[PROOF STEP]
by (simp add: X_eq_Y)
[PROOF STATE]
proof (state)
this:
Y' s'

goal (2 subgoals):
 1. \<forall>s\<subseteq>Collect (Domainp A). X s = Y s \<Longrightarrow> X' = Y'
 2. X' = Y' \<Longrightarrow> \<forall>s\<subseteq>Collect (Domainp A). X s = Y s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
X' ?s'2 \<Longrightarrow> Y' ?s'2

goal (2 subgoals):
 1. \<forall>s\<subseteq>Collect (Domainp A). X s = Y s \<Longrightarrow> X' = Y'
 2. X' = Y' \<Longrightarrow> \<forall>s\<subseteq>Collect (Domainp A). X s = Y s
[PROOF STEP]
note XY = this
[PROOF STATE]
proof (state)
this:
X' ?s'2 \<Longrightarrow> Y' ?s'2

goal (2 subgoals):
 1. \<forall>s\<subseteq>Collect (Domainp A). X s = Y s \<Longrightarrow> X' = Y'
 2. X' = Y' \<Longrightarrow> \<forall>s\<subseteq>Collect (Domainp A). X s = Y s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
X' ?s'2 \<Longrightarrow> Y' ?s'2

goal (2 subgoals):
 1. \<forall>s\<subseteq>Collect (Domainp A). X s = Y s \<Longrightarrow> X' = Y'
 2. X' = Y' \<Longrightarrow> \<forall>s\<subseteq>Collect (Domainp A). X s = Y s
[PROOF STEP]
fix s'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>s\<subseteq>Collect (Domainp A). X s = Y s \<Longrightarrow> X' = Y'
 2. X' = Y' \<Longrightarrow> \<forall>s\<subseteq>Collect (Domainp A). X s = Y s
[PROOF STEP]
assume "Y' s'"
[PROOF STATE]
proof (state)
this:
Y' s'

goal (2 subgoals):
 1. \<forall>s\<subseteq>Collect (Domainp A). X s = Y s \<Longrightarrow> X' = Y'
 2. X' = Y' \<Longrightarrow> \<forall>s\<subseteq>Collect (Domainp A). X s = Y s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Y' s'
[PROOF STEP]
obtain s where "rel_set A s s'"
[PROOF STATE]
proof (prove)
using this:
Y' s'

goal (1 subgoal):
 1. (\<And>s. rel_set A s s' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson assms right_total_def right_total_rel_set)
[PROOF STATE]
proof (state)
this:
rel_set A s s'

goal (2 subgoals):
 1. \<forall>s\<subseteq>Collect (Domainp A). X s = Y s \<Longrightarrow> X' = Y'
 2. X' = Y' \<Longrightarrow> \<forall>s\<subseteq>Collect (Domainp A). X s = Y s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rel_set A s s'
[PROOF STEP]
have "Y s"
[PROOF STATE]
proof (prove)
using this:
rel_set A s s'

goal (1 subgoal):
 1. Y s
[PROOF STEP]
using rs(2)[unfolded rel_fun_def]
[PROOF STATE]
proof (prove)
using this:
rel_set A s s'
\<forall>x y. rel_set A x y \<longrightarrow> Y x = Y' y

goal (1 subgoal):
 1. Y s
[PROOF STEP]
by (simp add: \<open>Y' s'\<close>)
[PROOF STATE]
proof (state)
this:
Y s

goal (2 subgoals):
 1. \<forall>s\<subseteq>Collect (Domainp A). X s = Y s \<Longrightarrow> X' = Y'
 2. X' = Y' \<Longrightarrow> \<forall>s\<subseteq>Collect (Domainp A). X s = Y s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Y s

goal (2 subgoals):
 1. \<forall>s\<subseteq>Collect (Domainp A). X s = Y s \<Longrightarrow> X' = Y'
 2. X' = Y' \<Longrightarrow> \<forall>s\<subseteq>Collect (Domainp A). X s = Y s
[PROOF STEP]
from \<open>rel_set A s s'\<close>
[PROOF STATE]
proof (chain)
picking this:
rel_set A s s'
[PROOF STEP]
have "s \<subseteq> ?sA"
[PROOF STATE]
proof (prove)
using this:
rel_set A s s'

goal (1 subgoal):
 1. s \<subseteq> Collect (Domainp A)
[PROOF STEP]
unfolding Ball_Collect[symmetric]
[PROOF STATE]
proof (prove)
using this:
rel_set A s s'

goal (1 subgoal):
 1. Ball s (Domainp A)
[PROOF STEP]
by (auto dest: rel_setD1)
[PROOF STATE]
proof (state)
this:
s \<subseteq> Collect (Domainp A)

goal (2 subgoals):
 1. \<forall>s\<subseteq>Collect (Domainp A). X s = Y s \<Longrightarrow> X' = Y'
 2. X' = Y' \<Longrightarrow> \<forall>s\<subseteq>Collect (Domainp A). X s = Y s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Y s
s \<subseteq> Collect (Domainp A)
[PROOF STEP]
have "X' s'"
[PROOF STATE]
proof (prove)
using this:
Y s
s \<subseteq> Collect (Domainp A)

goal (1 subgoal):
 1. X' s'
[PROOF STEP]
using X_eq_Y rs(1)[unfolded rel_fun_def] \<open>rel_set A s s'\<close>
[PROOF STATE]
proof (prove)
using this:
Y s
s \<subseteq> Collect (Domainp A)
\<forall>s\<subseteq>Collect (Domainp A). X s = Y s
\<forall>x y. rel_set A x y \<longrightarrow> X x = X' y
rel_set A s s'

goal (1 subgoal):
 1. X' s'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X' s'

goal (2 subgoals):
 1. \<forall>s\<subseteq>Collect (Domainp A). X s = Y s \<Longrightarrow> X' = Y'
 2. X' = Y' \<Longrightarrow> \<forall>s\<subseteq>Collect (Domainp A). X s = Y s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
Y' ?s'2 \<Longrightarrow> X' ?s'2

goal (2 subgoals):
 1. \<forall>s\<subseteq>Collect (Domainp A). X s = Y s \<Longrightarrow> X' = Y'
 2. X' = Y' \<Longrightarrow> \<forall>s\<subseteq>Collect (Domainp A). X s = Y s
[PROOF STEP]
with XY
[PROOF STATE]
proof (chain)
picking this:
X' ?s'2 \<Longrightarrow> Y' ?s'2
Y' ?s'2 \<Longrightarrow> X' ?s'2
[PROOF STEP]
show "X' = Y'"
[PROOF STATE]
proof (prove)
using this:
X' ?s'2 \<Longrightarrow> Y' ?s'2
Y' ?s'2 \<Longrightarrow> X' ?s'2

goal (1 subgoal):
 1. X' = Y'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X' = Y'

goal (1 subgoal):
 1. X' = Y' \<Longrightarrow> \<forall>s\<subseteq>Collect (Domainp A). X s = Y s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. X' = Y' \<Longrightarrow> \<forall>s\<subseteq>Collect (Domainp A). X s = Y s
[PROOF STEP]
assume "X' = Y'"
[PROOF STATE]
proof (state)
this:
X' = Y'

goal (1 subgoal):
 1. X' = Y' \<Longrightarrow> \<forall>s\<subseteq>Collect (Domainp A). X s = Y s
[PROOF STEP]
show "\<forall>s\<subseteq>?sA. X s = Y s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s\<subseteq>Collect (Domainp A). X s = Y s
[PROOF STEP]
unfolding Ball_Collect[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s. Ball s (Domainp A) \<longrightarrow> X s = Y s
[PROOF STEP]
using rs[unfolded rel_fun_def] \<open>X' = Y'\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. rel_set A x y \<longrightarrow> X x = X' y
\<forall>x y. rel_set A x y \<longrightarrow> Y x = Y' y
X' = Y'

goal (1 subgoal):
 1. \<forall>s. Ball s (Domainp A) \<longrightarrow> X s = Y s
[PROOF STEP]
by (metis DomainpE Domainp_set)+
[PROOF STATE]
proof (state)
this:
\<forall>s\<subseteq>Collect (Domainp A). X s = Y s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<forall>s\<subseteq>Collect (Domainp A). X s = Y s) = (X' = Y')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vimage_fst_transfer_h:
  "
  pred_prod (Domainp A) (Domainp B) x =
    (x \<in> Collect (Domainp A) \<times> Collect (Domainp B))
  "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pred_prod (Domainp A) (Domainp B) x = (x \<in> Collect (Domainp A) \<times> Collect (Domainp B))
[PROOF STEP]
unfolding pred_prod_beta mem_Times_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Domainp A (fst x) \<and> Domainp B (snd x)) = (fst x \<in> Collect (Domainp A) \<and> snd x \<in> Collect (Domainp B))
[PROOF STEP]
by simp


[STATEMENT]
lemma vimage_fst_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" "right_total B"
  shows
    "((rel_prod A B ===> A) ===> rel_set A ===> rel_set (rel_prod A B))
      (\<lambda>f S. (f -` S) \<inter> ((Collect (Domainp A)) \<times> (Collect (Domainp B))))
      vimage"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((rel_prod A B ===> A) ===> rel_set A ===> rel_set (rel_prod A B)) (\<lambda>f S. f -` S \<inter> Collect (Domainp A) \<times> Collect (Domainp B)) (-`)
[PROOF STEP]
unfolding vimage_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((rel_prod A B ===> A) ===> rel_set A ===> rel_set (rel_prod A B)) (\<lambda>f S. {x. f x \<in> S} \<inter> Collect (Domainp A) \<times> Collect (Domainp B)) (\<lambda>f B. {x. f x \<in> B})
[PROOF STEP]
apply transfer_prover_start
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. Transfer.Rel (A ===> rel_set A ===> ?Rh7) ?aa7 (\<in>)
 2. Transfer.Rel ((rel_prod A B ===> ?Rh7) ===> rel_set (rel_prod A B)) ?a7 Collect
 3. (\<lambda>f S. {x. f x \<in> S} \<inter> Collect (Domainp A) \<times> Collect (Domainp B)) = (\<lambda>f B. ?a7 (\<lambda>x. ?aa7 (f x) B))
[PROOF STEP]
apply transfer_step+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f S. {x. f x \<in> S} \<inter> Collect (Domainp A) \<times> Collect (Domainp B)) = (\<lambda>f Ba. {x. f x \<in> Ba \<and> pred_prod (Domainp A) (Domainp B) x})
[PROOF STEP]
unfolding vimage_fst_transfer_h
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f S. {x. f x \<in> S} \<inter> Collect (Domainp A) \<times> Collect (Domainp B)) = (\<lambda>f Ba. {x. f x \<in> Ba \<and> x \<in> Collect (Domainp A) \<times> Collect (Domainp B)})
[PROOF STEP]
by auto


[STATEMENT]
lemma vimage_snd_transfer[transfer_rule]:
  assumes [transfer_rule]: "right_total A" "bi_unique B" "right_total B"
  shows
    "((rel_prod A B ===> B) ===> rel_set B ===> rel_set (rel_prod A B))
      (\<lambda>f S. (f -` S) \<inter> ((Collect (Domainp A)) \<times> (Collect (Domainp B))))
      vimage"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((rel_prod A B ===> B) ===> rel_set B ===> rel_set (rel_prod A B)) (\<lambda>f S. f -` S \<inter> Collect (Domainp A) \<times> Collect (Domainp B)) (-`)
[PROOF STEP]
unfolding vimage_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((rel_prod A B ===> B) ===> rel_set B ===> rel_set (rel_prod A B)) (\<lambda>f S. {x. f x \<in> S} \<inter> Collect (Domainp A) \<times> Collect (Domainp B)) (\<lambda>f B. {x. f x \<in> B})
[PROOF STEP]
apply transfer_prover_start
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. Transfer.Rel (B ===> rel_set B ===> ?Rh7) ?aa7 (\<in>)
 2. Transfer.Rel ((rel_prod A B ===> ?Rh7) ===> rel_set (rel_prod A B)) ?a7 Collect
 3. (\<lambda>f S. {x. f x \<in> S} \<inter> Collect (Domainp A) \<times> Collect (Domainp B)) = (\<lambda>f B. ?a7 (\<lambda>x. ?aa7 (f x) B))
[PROOF STEP]
apply transfer_step+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f S. {x. f x \<in> S} \<inter> Collect (Domainp A) \<times> Collect (Domainp B)) = (\<lambda>f Ba. {x. f x \<in> Ba \<and> pred_prod (Domainp A) (Domainp B) x})
[PROOF STEP]
unfolding vimage_fst_transfer_h
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f S. {x. f x \<in> S} \<inter> Collect (Domainp A) \<times> Collect (Domainp B)) = (\<lambda>f Ba. {x. f x \<in> Ba \<and> x \<in> Collect (Domainp A) \<times> Collect (Domainp B)})
[PROOF STEP]
by auto


[STATEMENT]
lemma vimage_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique B" "right_total A"
  shows
    "((A ===> B) ===> (rel_set B) ===> rel_set A)
      (\<lambda>f s. (vimage f s) \<inter> (Collect (Domainp A))) (-`)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> B) ===> rel_set B ===> rel_set A) (\<lambda>f s. f -` s \<inter> Collect (Domainp A)) (-`)
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma pairwise_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A"
  shows "((A ===> A ===> (=)) ===> rel_set A  ===> (=)) pairwise pairwise"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> (=)) ===> rel_set A ===> (=)) pairwise pairwise
[PROOF STEP]
unfolding pairwise_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> (=)) ===> rel_set A ===> (=)) (\<lambda>R S. \<forall>x\<in>S. \<forall>y\<in>S. x \<noteq> y \<longrightarrow> R x y) (\<lambda>R S. \<forall>x\<in>S. \<forall>y\<in>S. x \<noteq> y \<longrightarrow> R x y)
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma disjnt_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A"
  shows "(rel_set A ===> rel_set A  ===> (=)) disjnt disjnt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_set A ===> rel_set A ===> (=)) disjnt disjnt
[PROOF STEP]
unfolding disjnt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_set A ===> rel_set A ===> (=)) (\<lambda>A B. A \<inter> B = {}) (\<lambda>A B. A \<inter> B = {})
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma bij_betw_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "bi_unique B"
  shows "((A ===> B) ===> rel_set A ===> rel_set B ===> (=)) bij_betw bij_betw"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> B) ===> rel_set A ===> rel_set B ===> (=)) bij_betw bij_betw
[PROOF STEP]
unfolding bij_betw_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> B) ===> rel_set A ===> rel_set B ===> (=)) (\<lambda>f A B. inj_on f A \<and> f ` A = B) (\<lambda>f A B. inj_on f A \<and> f ` A = B)
[PROOF STEP]
apply transfer_prover_start
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. Transfer.Rel ((A ===> B) ===> rel_set A ===> ?Rk11) ?ac11 (`)
 2. Transfer.Rel (?Rk11 ===> rel_set B ===> ?Ri11) ?ab11 (=)
 3. Transfer.Rel ((A ===> B) ===> rel_set A ===> ?Rh11) ?aa11 inj_on
 4. Transfer.Rel (?Rh11 ===> ?Ri11 ===> (=)) ?a11 (\<and>)
 5. (\<lambda>f A B. inj_on f A \<and> f ` A = B) = (\<lambda>f A B. ?a11 (?aa11 f A) (?ab11 (?ac11 f A) B))
[PROOF STEP]
apply transfer_step+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f A B. inj_on f A \<and> f ` A = B) = (\<lambda>f A B. inj_on f A \<and> f ` A = B)
[PROOF STEP]
by simp


[STATEMENT]
theorem "l_sorted (l_sort_naive xs [] [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sorted (l_sort_naive xs [] [])
[PROOF STEP]
proof (rule l_sort_naive.induct [of "\<lambda>xs ys zs. l_sorted (l_sort_naive xs ys zs)"],
 simp_all del: l_sort_naive.simps(3))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ys zs. l_sorted (l_sort_naive [] ys zs)
[PROOF STEP]
txt \<open>
\null

Simplification deletes all the subgoals generated by recursive equations.
However, the following subgoal arises from the non-recursive one:

\null

@{subgoals [display]}

\null

which is hopeless as the formula is false for any unsorted list \<open>zs\<close>.

\null
\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ys zs. l_sorted (l_sort_naive [] ys zs)
[PROOF STEP]
oops


[STATEMENT]
lemma l_sort_subset:
  assumes XY: "Y \<in> l_sort_set X"
  shows "l_sort_set Y \<subseteq> l_sort_set X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sort_set Y \<subseteq> l_sort_set X
[PROOF STEP]
proof (rule subsetI, erule l_sort_set.induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x. Y \<in> l_sort_set X
 2. \<And>x xa xs ys. \<lbrakk>(xa # xs, ys, []) \<in> l_sort_set Y; (xa # xs, ys, []) \<in> l_sort_set X\<rbrakk> \<Longrightarrow> (xs, [], ys @ [xa]) \<in> l_sort_set X
 3. \<And>x xa xs ys z zs. \<lbrakk>(xa # xs, ys, z # zs) \<in> l_sort_set Y; (xa # xs, ys, z # zs) \<in> l_sort_set X; xa \<le> z\<rbrakk> \<Longrightarrow> (xs, [], ys @ xa # z # zs) \<in> l_sort_set X
 4. \<And>x xa xs ys z zs. \<lbrakk>(xa # xs, ys, z # zs) \<in> l_sort_set Y; (xa # xs, ys, z # zs) \<in> l_sort_set X; \<not> xa \<le> z\<rbrakk> \<Longrightarrow> (xa # xs, ys @ [z], zs) \<in> l_sort_set X
[PROOF STEP]
show "Y \<in> l_sort_set X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y \<in> l_sort_set X
[PROOF STEP]
using XY
[PROOF STATE]
proof (prove)
using this:
Y \<in> l_sort_set X

goal (1 subgoal):
 1. Y \<in> l_sort_set X
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Y \<in> l_sort_set X

goal (3 subgoals):
 1. \<And>x xa xs ys. \<lbrakk>(xa # xs, ys, []) \<in> l_sort_set Y; (xa # xs, ys, []) \<in> l_sort_set X\<rbrakk> \<Longrightarrow> (xs, [], ys @ [xa]) \<in> l_sort_set X
 2. \<And>x xa xs ys z zs. \<lbrakk>(xa # xs, ys, z # zs) \<in> l_sort_set Y; (xa # xs, ys, z # zs) \<in> l_sort_set X; xa \<le> z\<rbrakk> \<Longrightarrow> (xs, [], ys @ xa # z # zs) \<in> l_sort_set X
 3. \<And>x xa xs ys z zs. \<lbrakk>(xa # xs, ys, z # zs) \<in> l_sort_set Y; (xa # xs, ys, z # zs) \<in> l_sort_set X; \<not> xa \<le> z\<rbrakk> \<Longrightarrow> (xa # xs, ys @ [z], zs) \<in> l_sort_set X
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x xa xs ys. \<lbrakk>(xa # xs, ys, []) \<in> l_sort_set Y; (xa # xs, ys, []) \<in> l_sort_set X\<rbrakk> \<Longrightarrow> (xs, [], ys @ [xa]) \<in> l_sort_set X
 2. \<And>x xa xs ys z zs. \<lbrakk>(xa # xs, ys, z # zs) \<in> l_sort_set Y; (xa # xs, ys, z # zs) \<in> l_sort_set X; xa \<le> z\<rbrakk> \<Longrightarrow> (xs, [], ys @ xa # z # zs) \<in> l_sort_set X
 3. \<And>x xa xs ys z zs. \<lbrakk>(xa # xs, ys, z # zs) \<in> l_sort_set Y; (xa # xs, ys, z # zs) \<in> l_sort_set X; \<not> xa \<le> z\<rbrakk> \<Longrightarrow> (xa # xs, ys @ [z], zs) \<in> l_sort_set X
[PROOF STEP]
fix x xs ys
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x xa xs ys. \<lbrakk>(xa # xs, ys, []) \<in> l_sort_set Y; (xa # xs, ys, []) \<in> l_sort_set X\<rbrakk> \<Longrightarrow> (xs, [], ys @ [xa]) \<in> l_sort_set X
 2. \<And>x xa xs ys z zs. \<lbrakk>(xa # xs, ys, z # zs) \<in> l_sort_set Y; (xa # xs, ys, z # zs) \<in> l_sort_set X; xa \<le> z\<rbrakk> \<Longrightarrow> (xs, [], ys @ xa # z # zs) \<in> l_sort_set X
 3. \<And>x xa xs ys z zs. \<lbrakk>(xa # xs, ys, z # zs) \<in> l_sort_set Y; (xa # xs, ys, z # zs) \<in> l_sort_set X; \<not> xa \<le> z\<rbrakk> \<Longrightarrow> (xa # xs, ys @ [z], zs) \<in> l_sort_set X
[PROOF STEP]
assume "(x # xs, ys, []) \<in> l_sort_set X"
[PROOF STATE]
proof (state)
this:
(x # xs, ys, []) \<in> l_sort_set X

goal (3 subgoals):
 1. \<And>x xa xs ys. \<lbrakk>(xa # xs, ys, []) \<in> l_sort_set Y; (xa # xs, ys, []) \<in> l_sort_set X\<rbrakk> \<Longrightarrow> (xs, [], ys @ [xa]) \<in> l_sort_set X
 2. \<And>x xa xs ys z zs. \<lbrakk>(xa # xs, ys, z # zs) \<in> l_sort_set Y; (xa # xs, ys, z # zs) \<in> l_sort_set X; xa \<le> z\<rbrakk> \<Longrightarrow> (xs, [], ys @ xa # z # zs) \<in> l_sort_set X
 3. \<And>x xa xs ys z zs. \<lbrakk>(xa # xs, ys, z # zs) \<in> l_sort_set Y; (xa # xs, ys, z # zs) \<in> l_sort_set X; \<not> xa \<le> z\<rbrakk> \<Longrightarrow> (xa # xs, ys @ [z], zs) \<in> l_sort_set X
[PROOF STEP]
thus "(xs, [], ys @ [x]) \<in> l_sort_set X"
[PROOF STATE]
proof (prove)
using this:
(x # xs, ys, []) \<in> l_sort_set X

goal (1 subgoal):
 1. (xs, [], ys @ [x]) \<in> l_sort_set X
[PROOF STEP]
by (rule R1)
[PROOF STATE]
proof (state)
this:
(xs, [], ys @ [x]) \<in> l_sort_set X

goal (2 subgoals):
 1. \<And>x xa xs ys z zs. \<lbrakk>(xa # xs, ys, z # zs) \<in> l_sort_set Y; (xa # xs, ys, z # zs) \<in> l_sort_set X; xa \<le> z\<rbrakk> \<Longrightarrow> (xs, [], ys @ xa # z # zs) \<in> l_sort_set X
 2. \<And>x xa xs ys z zs. \<lbrakk>(xa # xs, ys, z # zs) \<in> l_sort_set Y; (xa # xs, ys, z # zs) \<in> l_sort_set X; \<not> xa \<le> z\<rbrakk> \<Longrightarrow> (xa # xs, ys @ [z], zs) \<in> l_sort_set X
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa xs ys z zs. \<lbrakk>(xa # xs, ys, z # zs) \<in> l_sort_set Y; (xa # xs, ys, z # zs) \<in> l_sort_set X; xa \<le> z\<rbrakk> \<Longrightarrow> (xs, [], ys @ xa # z # zs) \<in> l_sort_set X
 2. \<And>x xa xs ys z zs. \<lbrakk>(xa # xs, ys, z # zs) \<in> l_sort_set Y; (xa # xs, ys, z # zs) \<in> l_sort_set X; \<not> xa \<le> z\<rbrakk> \<Longrightarrow> (xa # xs, ys @ [z], zs) \<in> l_sort_set X
[PROOF STEP]
fix x xs ys z zs
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa xs ys z zs. \<lbrakk>(xa # xs, ys, z # zs) \<in> l_sort_set Y; (xa # xs, ys, z # zs) \<in> l_sort_set X; xa \<le> z\<rbrakk> \<Longrightarrow> (xs, [], ys @ xa # z # zs) \<in> l_sort_set X
 2. \<And>x xa xs ys z zs. \<lbrakk>(xa # xs, ys, z # zs) \<in> l_sort_set Y; (xa # xs, ys, z # zs) \<in> l_sort_set X; \<not> xa \<le> z\<rbrakk> \<Longrightarrow> (xa # xs, ys @ [z], zs) \<in> l_sort_set X
[PROOF STEP]
assume "(x # xs, ys, z # zs) \<in> l_sort_set X" and "x \<le> z"
[PROOF STATE]
proof (state)
this:
(x # xs, ys, z # zs) \<in> l_sort_set X
x \<le> z

goal (2 subgoals):
 1. \<And>x xa xs ys z zs. \<lbrakk>(xa # xs, ys, z # zs) \<in> l_sort_set Y; (xa # xs, ys, z # zs) \<in> l_sort_set X; xa \<le> z\<rbrakk> \<Longrightarrow> (xs, [], ys @ xa # z # zs) \<in> l_sort_set X
 2. \<And>x xa xs ys z zs. \<lbrakk>(xa # xs, ys, z # zs) \<in> l_sort_set Y; (xa # xs, ys, z # zs) \<in> l_sort_set X; \<not> xa \<le> z\<rbrakk> \<Longrightarrow> (xa # xs, ys @ [z], zs) \<in> l_sort_set X
[PROOF STEP]
thus "(xs, [], ys @ x # z # zs) \<in> l_sort_set X"
[PROOF STATE]
proof (prove)
using this:
(x # xs, ys, z # zs) \<in> l_sort_set X
x \<le> z

goal (1 subgoal):
 1. (xs, [], ys @ x # z # zs) \<in> l_sort_set X
[PROOF STEP]
by (rule R2)
[PROOF STATE]
proof (state)
this:
(xs, [], ys @ x # z # zs) \<in> l_sort_set X

goal (1 subgoal):
 1. \<And>x xa xs ys z zs. \<lbrakk>(xa # xs, ys, z # zs) \<in> l_sort_set Y; (xa # xs, ys, z # zs) \<in> l_sort_set X; \<not> xa \<le> z\<rbrakk> \<Longrightarrow> (xa # xs, ys @ [z], zs) \<in> l_sort_set X
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa xs ys z zs. \<lbrakk>(xa # xs, ys, z # zs) \<in> l_sort_set Y; (xa # xs, ys, z # zs) \<in> l_sort_set X; \<not> xa \<le> z\<rbrakk> \<Longrightarrow> (xa # xs, ys @ [z], zs) \<in> l_sort_set X
[PROOF STEP]
fix x xs ys z zs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa xs ys z zs. \<lbrakk>(xa # xs, ys, z # zs) \<in> l_sort_set Y; (xa # xs, ys, z # zs) \<in> l_sort_set X; \<not> xa \<le> z\<rbrakk> \<Longrightarrow> (xa # xs, ys @ [z], zs) \<in> l_sort_set X
[PROOF STEP]
assume "(x # xs, ys, z # zs) \<in> l_sort_set X" and "\<not> x \<le> z"
[PROOF STATE]
proof (state)
this:
(x # xs, ys, z # zs) \<in> l_sort_set X
\<not> x \<le> z

goal (1 subgoal):
 1. \<And>x xa xs ys z zs. \<lbrakk>(xa # xs, ys, z # zs) \<in> l_sort_set Y; (xa # xs, ys, z # zs) \<in> l_sort_set X; \<not> xa \<le> z\<rbrakk> \<Longrightarrow> (xa # xs, ys @ [z], zs) \<in> l_sort_set X
[PROOF STEP]
thus "(x # xs, ys @ [z], zs) \<in> l_sort_set X"
[PROOF STATE]
proof (prove)
using this:
(x # xs, ys, z # zs) \<in> l_sort_set X
\<not> x \<le> z

goal (1 subgoal):
 1. (x # xs, ys @ [z], zs) \<in> l_sort_set X
[PROOF STEP]
by (rule R3)
[PROOF STATE]
proof (state)
this:
(x # xs, ys @ [z], zs) \<in> l_sort_set X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma l_sort_aux_set: "l_sort_aux X \<in> l_sort_set X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sort_aux X \<in> l_sort_set X
[PROOF STEP]
proof (induction rule: l_sort_aux.induct, simp_all del: l_sort_aux.simps(2))
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x xs ys. l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (xs, [], ys @ [x]) \<Longrightarrow> l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (x # xs, ys, [])
 2. \<And>x xs ys z zs. \<lbrakk>x \<le> z \<Longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (xs, [], ys @ x # z # zs); \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys @ [z], zs)\<rbrakk> \<Longrightarrow> l_sort_aux (x # xs, ys, z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
 3. \<And>ys zs. ([], ys, zs) \<in> l_sort_set ([], ys, zs)
[PROOF STEP]
fix ys :: "'a list" and zs
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x xs ys. l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (xs, [], ys @ [x]) \<Longrightarrow> l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (x # xs, ys, [])
 2. \<And>x xs ys z zs. \<lbrakk>x \<le> z \<Longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (xs, [], ys @ x # z # zs); \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys @ [z], zs)\<rbrakk> \<Longrightarrow> l_sort_aux (x # xs, ys, z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
 3. \<And>ys zs. ([], ys, zs) \<in> l_sort_set ([], ys, zs)
[PROOF STEP]
show "([], ys, zs) \<in> l_sort_set ([], ys, zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([], ys, zs) \<in> l_sort_set ([], ys, zs)
[PROOF STEP]
by (rule R0)
[PROOF STATE]
proof (state)
this:
([], ys, zs) \<in> l_sort_set ([], ys, zs)

goal (2 subgoals):
 1. \<And>x xs ys. l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (xs, [], ys @ [x]) \<Longrightarrow> l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (x # xs, ys, [])
 2. \<And>x xs ys z zs. \<lbrakk>x \<le> z \<Longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (xs, [], ys @ x # z # zs); \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys @ [z], zs)\<rbrakk> \<Longrightarrow> l_sort_aux (x # xs, ys, z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xs ys. l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (xs, [], ys @ [x]) \<Longrightarrow> l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (x # xs, ys, [])
 2. \<And>x xs ys z zs. \<lbrakk>x \<le> z \<Longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (xs, [], ys @ x # z # zs); \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys @ [z], zs)\<rbrakk> \<Longrightarrow> l_sort_aux (x # xs, ys, z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
fix x :: 'a and xs ys
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xs ys. l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (xs, [], ys @ [x]) \<Longrightarrow> l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (x # xs, ys, [])
 2. \<And>x xs ys z zs. \<lbrakk>x \<le> z \<Longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (xs, [], ys @ x # z # zs); \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys @ [z], zs)\<rbrakk> \<Longrightarrow> l_sort_aux (x # xs, ys, z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
have "(x # xs, ys, []) \<in> l_sort_set (x # xs, ys, [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x # xs, ys, []) \<in> l_sort_set (x # xs, ys, [])
[PROOF STEP]
by (rule R0)
[PROOF STATE]
proof (state)
this:
(x # xs, ys, []) \<in> l_sort_set (x # xs, ys, [])

goal (2 subgoals):
 1. \<And>x xs ys. l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (xs, [], ys @ [x]) \<Longrightarrow> l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (x # xs, ys, [])
 2. \<And>x xs ys z zs. \<lbrakk>x \<le> z \<Longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (xs, [], ys @ x # z # zs); \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys @ [z], zs)\<rbrakk> \<Longrightarrow> l_sort_aux (x # xs, ys, z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
hence "(xs, [], ys @ [x]) \<in> l_sort_set (x # xs, ys, [])"
[PROOF STATE]
proof (prove)
using this:
(x # xs, ys, []) \<in> l_sort_set (x # xs, ys, [])

goal (1 subgoal):
 1. (xs, [], ys @ [x]) \<in> l_sort_set (x # xs, ys, [])
[PROOF STEP]
by (rule R1)
[PROOF STATE]
proof (state)
this:
(xs, [], ys @ [x]) \<in> l_sort_set (x # xs, ys, [])

goal (2 subgoals):
 1. \<And>x xs ys. l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (xs, [], ys @ [x]) \<Longrightarrow> l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (x # xs, ys, [])
 2. \<And>x xs ys z zs. \<lbrakk>x \<le> z \<Longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (xs, [], ys @ x # z # zs); \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys @ [z], zs)\<rbrakk> \<Longrightarrow> l_sort_aux (x # xs, ys, z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
hence "l_sort_set (xs, [], ys @ [x]) \<subseteq> l_sort_set (x # xs, ys, [])"
[PROOF STATE]
proof (prove)
using this:
(xs, [], ys @ [x]) \<in> l_sort_set (x # xs, ys, [])

goal (1 subgoal):
 1. l_sort_set (xs, [], ys @ [x]) \<subseteq> l_sort_set (x # xs, ys, [])
[PROOF STEP]
by (rule l_sort_subset)
[PROOF STATE]
proof (state)
this:
l_sort_set (xs, [], ys @ [x]) \<subseteq> l_sort_set (x # xs, ys, [])

goal (2 subgoals):
 1. \<And>x xs ys. l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (xs, [], ys @ [x]) \<Longrightarrow> l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (x # xs, ys, [])
 2. \<And>x xs ys z zs. \<lbrakk>x \<le> z \<Longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (xs, [], ys @ x # z # zs); \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys @ [z], zs)\<rbrakk> \<Longrightarrow> l_sort_aux (x # xs, ys, z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
l_sort_set (xs, [], ys @ [x]) \<subseteq> l_sort_set (x # xs, ys, [])

goal (2 subgoals):
 1. \<And>x xs ys. l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (xs, [], ys @ [x]) \<Longrightarrow> l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (x # xs, ys, [])
 2. \<And>x xs ys z zs. \<lbrakk>x \<le> z \<Longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (xs, [], ys @ x # z # zs); \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys @ [z], zs)\<rbrakk> \<Longrightarrow> l_sort_aux (x # xs, ys, z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
assume "l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (xs, [], ys @ [x])"
[PROOF STATE]
proof (state)
this:
l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (xs, [], ys @ [x])

goal (2 subgoals):
 1. \<And>x xs ys. l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (xs, [], ys @ [x]) \<Longrightarrow> l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (x # xs, ys, [])
 2. \<And>x xs ys z zs. \<lbrakk>x \<le> z \<Longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (xs, [], ys @ x # z # zs); \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys @ [z], zs)\<rbrakk> \<Longrightarrow> l_sort_aux (x # xs, ys, z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
l_sort_set (xs, [], ys @ [x]) \<subseteq> l_sort_set (x # xs, ys, [])
l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (xs, [], ys @ [x])
[PROOF STEP]
show "l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (x # xs, ys, [])"
[PROOF STATE]
proof (prove)
using this:
l_sort_set (xs, [], ys @ [x]) \<subseteq> l_sort_set (x # xs, ys, [])
l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (xs, [], ys @ [x])

goal (1 subgoal):
 1. l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (x # xs, ys, [])
[PROOF STEP]
by (rule subsetD)
[PROOF STATE]
proof (state)
this:
l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (x # xs, ys, [])

goal (1 subgoal):
 1. \<And>x xs ys z zs. \<lbrakk>x \<le> z \<Longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (xs, [], ys @ x # z # zs); \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys @ [z], zs)\<rbrakk> \<Longrightarrow> l_sort_aux (x # xs, ys, z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs ys z zs. \<lbrakk>x \<le> z \<Longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (xs, [], ys @ x # z # zs); \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys @ [z], zs)\<rbrakk> \<Longrightarrow> l_sort_aux (x # xs, ys, z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
fix x :: 'a and xs ys z zs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs ys z zs. \<lbrakk>x \<le> z \<Longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (xs, [], ys @ x # z # zs); \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys @ [z], zs)\<rbrakk> \<Longrightarrow> l_sort_aux (x # xs, ys, z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
assume
   case1: "x \<le> z \<Longrightarrow>
    l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (xs, [], ys @ x # z # zs)"
  and
   case2: "\<not> x \<le> z \<Longrightarrow>
    l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys @ [z], zs)"
[PROOF STATE]
proof (state)
this:
x \<le> z \<Longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (xs, [], ys @ x # z # zs)
\<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys @ [z], zs)

goal (1 subgoal):
 1. \<And>x xs ys z zs. \<lbrakk>x \<le> z \<Longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (xs, [], ys @ x # z # zs); \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys @ [z], zs)\<rbrakk> \<Longrightarrow> l_sort_aux (x # xs, ys, z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
have 0: "(x # xs, ys, z # zs) \<in> l_sort_set (x # xs, ys, z # zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x # xs, ys, z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
by (rule R0)
[PROOF STATE]
proof (state)
this:
(x # xs, ys, z # zs) \<in> l_sort_set (x # xs, ys, z # zs)

goal (1 subgoal):
 1. \<And>x xs ys z zs. \<lbrakk>x \<le> z \<Longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (xs, [], ys @ x # z # zs); \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys @ [z], zs)\<rbrakk> \<Longrightarrow> l_sort_aux (x # xs, ys, z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
show "l_sort_aux (x # xs, ys, z # zs) \<in> l_sort_set (x # xs, ys, z # zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sort_aux (x # xs, ys, z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
proof (cases "x \<le> z", simp_all)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<le> z \<Longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
 2. \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
assume "x \<le> z"
[PROOF STATE]
proof (state)
this:
x \<le> z

goal (2 subgoals):
 1. x \<le> z \<Longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
 2. \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
with 0
[PROOF STATE]
proof (chain)
picking this:
(x # xs, ys, z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
x \<le> z
[PROOF STEP]
have "(xs, [], ys @ x # z # zs) \<in> l_sort_set (x # xs, ys, z # zs)"
[PROOF STATE]
proof (prove)
using this:
(x # xs, ys, z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
x \<le> z

goal (1 subgoal):
 1. (xs, [], ys @ x # z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
by (rule R2)
[PROOF STATE]
proof (state)
this:
(xs, [], ys @ x # z # zs) \<in> l_sort_set (x # xs, ys, z # zs)

goal (2 subgoals):
 1. x \<le> z \<Longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
 2. \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
hence "l_sort_set (xs, [], ys @ x # z # zs) \<subseteq> l_sort_set (x # xs, ys, z # zs)"
[PROOF STATE]
proof (prove)
using this:
(xs, [], ys @ x # z # zs) \<in> l_sort_set (x # xs, ys, z # zs)

goal (1 subgoal):
 1. l_sort_set (xs, [], ys @ x # z # zs) \<subseteq> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
by (rule l_sort_subset)
[PROOF STATE]
proof (state)
this:
l_sort_set (xs, [], ys @ x # z # zs) \<subseteq> l_sort_set (x # xs, ys, z # zs)

goal (2 subgoals):
 1. x \<le> z \<Longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
 2. \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
l_sort_set (xs, [], ys @ x # z # zs) \<subseteq> l_sort_set (x # xs, ys, z # zs)

goal (2 subgoals):
 1. x \<le> z \<Longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
 2. \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
have "l_sort_aux (xs, [], ys @ x # z # zs) \<in>
     l_sort_set (xs, [], ys @ x # z # zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (xs, [], ys @ x # z # zs)
[PROOF STEP]
using case1 and \<open>x \<le> z\<close>
[PROOF STATE]
proof (prove)
using this:
x \<le> z \<Longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (xs, [], ys @ x # z # zs)
x \<le> z

goal (1 subgoal):
 1. l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (xs, [], ys @ x # z # zs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (xs, [], ys @ x # z # zs)

goal (2 subgoals):
 1. x \<le> z \<Longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
 2. \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
l_sort_set (xs, [], ys @ x # z # zs) \<subseteq> l_sort_set (x # xs, ys, z # zs)
l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (xs, [], ys @ x # z # zs)
[PROOF STEP]
show "l_sort_aux (xs, [], ys @ x # z # zs) \<in>
     l_sort_set (x # xs, ys, z # zs)"
[PROOF STATE]
proof (prove)
using this:
l_sort_set (xs, [], ys @ x # z # zs) \<subseteq> l_sort_set (x # xs, ys, z # zs)
l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (xs, [], ys @ x # z # zs)

goal (1 subgoal):
 1. l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
by (rule subsetD)
[PROOF STATE]
proof (state)
this:
l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (x # xs, ys, z # zs)

goal (1 subgoal):
 1. \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
assume "\<not> x \<le> z"
[PROOF STATE]
proof (state)
this:
\<not> x \<le> z

goal (1 subgoal):
 1. \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
with 0
[PROOF STATE]
proof (chain)
picking this:
(x # xs, ys, z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
\<not> x \<le> z
[PROOF STEP]
have "(x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys, z # zs)"
[PROOF STATE]
proof (prove)
using this:
(x # xs, ys, z # zs) \<in> l_sort_set (x # xs, ys, z # zs)
\<not> x \<le> z

goal (1 subgoal):
 1. (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
by (rule R3)
[PROOF STATE]
proof (state)
this:
(x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys, z # zs)

goal (1 subgoal):
 1. \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
hence "l_sort_set (x # xs, ys @ [z], zs) \<subseteq> l_sort_set (x # xs, ys, z # zs)"
[PROOF STATE]
proof (prove)
using this:
(x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys, z # zs)

goal (1 subgoal):
 1. l_sort_set (x # xs, ys @ [z], zs) \<subseteq> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
by (rule l_sort_subset)
[PROOF STATE]
proof (state)
this:
l_sort_set (x # xs, ys @ [z], zs) \<subseteq> l_sort_set (x # xs, ys, z # zs)

goal (1 subgoal):
 1. \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
l_sort_set (x # xs, ys @ [z], zs) \<subseteq> l_sort_set (x # xs, ys, z # zs)

goal (1 subgoal):
 1. \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
have "l_sort_aux (x # xs, ys @ [z], zs) \<in>
     l_sort_set (x # xs, ys @ [z], zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys @ [z], zs)
[PROOF STEP]
using case2 and \<open>\<not> x \<le> z\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys @ [z], zs)
\<not> x \<le> z

goal (1 subgoal):
 1. l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys @ [z], zs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys @ [z], zs)

goal (1 subgoal):
 1. \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
l_sort_set (x # xs, ys @ [z], zs) \<subseteq> l_sort_set (x # xs, ys, z # zs)
l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys @ [z], zs)
[PROOF STEP]
show "l_sort_aux (x # xs, ys @ [z], zs) \<in>
     l_sort_set (x # xs, ys, z # zs)"
[PROOF STATE]
proof (prove)
using this:
l_sort_set (x # xs, ys @ [z], zs) \<subseteq> l_sort_set (x # xs, ys, z # zs)
l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys @ [z], zs)

goal (1 subgoal):
 1. l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys, z # zs)
[PROOF STEP]
by (rule subsetD)
[PROOF STATE]
proof (state)
this:
l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys, z # zs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l_sort_aux (x # xs, ys, z # zs) \<in> l_sort_set (x # xs, ys, z # zs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "l_sort_aux X \<in> l_sort_set X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sort_aux X \<in> l_sort_set X
[PROOF STEP]
proof (induction rule: l_sort_aux.induct, simp_all)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x xs ys. l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (xs, [], ys @ [x]) \<Longrightarrow> l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (x # xs, ys, [])
 2. \<And>x xs ys z zs. \<lbrakk>x \<le> z \<Longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (xs, [], ys @ x # z # zs); \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys @ [z], zs)\<rbrakk> \<Longrightarrow> (x \<le> z \<longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (x # xs, ys, z # zs)) \<and> (\<not> x \<le> z \<longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys, z # zs))
 3. \<And>ys zs. ([], ys, zs) \<in> l_sort_set ([], ys, zs)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x xs ys. l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (xs, [], ys @ [x]) \<Longrightarrow> l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (x # xs, ys, [])
 2. \<And>x xs ys z zs. \<lbrakk>x \<le> z \<Longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (xs, [], ys @ x # z # zs); \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys @ [z], zs)\<rbrakk> \<Longrightarrow> (x \<le> z \<longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (x # xs, ys, z # zs)) \<and> (\<not> x \<le> z \<longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys, z # zs))
 3. \<And>ys zs. ([], ys, zs) \<in> l_sort_set ([], ys, zs)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x xs ys z zs. \<lbrakk>x \<le> z \<Longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (xs, [], ys @ x # z # zs); \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys @ [z], zs)\<rbrakk> \<Longrightarrow> (x \<le> z \<longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (x # xs, ys, z # zs)) \<and> (\<not> x \<le> z \<longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys, z # zs))
 2. \<And>x xs ys. l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (xs, [], ys @ [x]) \<Longrightarrow> l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (x # xs, ys, [])
 3. \<And>ys zs. ([], ys, zs) \<in> l_sort_set ([], ys, zs)
[PROOF STEP]
(*>*)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x xs ys z zs. \<lbrakk>x \<le> z \<Longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (xs, [], ys @ x # z # zs); \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys @ [z], zs)\<rbrakk> \<Longrightarrow> (x \<le> z \<longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (x # xs, ys, z # zs)) \<and> (\<not> x \<le> z \<longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys, z # zs))
 2. \<And>x xs ys. l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (xs, [], ys @ [x]) \<Longrightarrow> l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (x # xs, ys, [])
 3. \<And>ys zs. ([], ys, zs) \<in> l_sort_set ([], ys, zs)
[PROOF STEP]
txt \<open>
\null

As a result of the application of the rule, the related subgoal takes the
following form:

\null

@{subgoals [display, goals_limit = 1]}

\null

Now the conclusion is comprised of a conjunction of two implications. This is
pointless, since case distinction is faster than the application of conjunction
and implication introduction rules in providing sufficient assumptions for the
simplification of both the induction hypotheses and the conclusion.

\null
\<close>
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x xs ys z zs. \<lbrakk>x \<le> z \<Longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (xs, [], ys @ x # z # zs); \<not> x \<le> z \<Longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys @ [z], zs)\<rbrakk> \<Longrightarrow> (x \<le> z \<longrightarrow> l_sort_aux (xs, [], ys @ x # z # zs) \<in> l_sort_set (x # xs, ys, z # zs)) \<and> (\<not> x \<le> z \<longrightarrow> l_sort_aux (x # xs, ys @ [z], zs) \<in> l_sort_set (x # xs, ys, z # zs))
 2. \<And>x xs ys. l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (xs, [], ys @ [x]) \<Longrightarrow> l_sort_aux (xs, [], ys @ [x]) \<in> l_sort_set (x # xs, ys, [])
 3. \<And>ys zs. ([], ys, zs) \<in> l_sort_set ([], ys, zs)
[PROOF STEP]
oops


[STATEMENT]
lemma l_sort_input_2: "l_sort_inv_2 x xs (xs, [], [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sort_inv_2 x xs (xs, [], [])
[PROOF STEP]
by (simp add: l_sort_inv_2_def l_count_def)


[STATEMENT]
lemma l_sort_intro_1:
 "l_sort_inv_1 X \<Longrightarrow> l_sorted (l_sort_out X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sort_inv_1 X \<Longrightarrow> l_sorted (l_sort_out X)
[PROOF STEP]
by (rule l_sort_inv_1.cases [of X], simp_all add: l_sort_out_def)


[STATEMENT]
lemma l_sort_intro_2:
 "\<lbrakk>l_sort_inv_2 x xs X; l_sort_form X\<rbrakk> \<Longrightarrow>
  l_count x (l_sort_out X) = l_count x xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>l_sort_inv_2 x xs X; l_sort_form X\<rbrakk> \<Longrightarrow> l_count x (l_sort_out X) = l_count x xs
[PROOF STEP]
by (simp add: l_sort_inv_2_def, (erule conjE)+,
 simp add: l_sort_form_def l_sort_out_def l_count_def)


[STATEMENT]
lemma l_sort_form_aux_all: "l_sort_form (l_sort_aux X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sort_form (l_sort_aux X)
[PROOF STEP]
by (rule l_sort_aux.induct [of "\<lambda>X. l_sort_form (l_sort_aux X)"],
 simp_all add: l_sort_form_def)


[STATEMENT]
lemma l_sort_form_aux: "l_sort_form (l_sort_aux (xs, [], []))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sort_form (l_sort_aux (xs, [], []))
[PROOF STEP]
by (rule l_sort_form_aux_all)


[STATEMENT]
lemma l_sorted_app [rule_format]:
 "l_sorted xs \<longrightarrow> l_sorted ys \<longrightarrow> last xs \<le> hd ys \<longrightarrow> l_sorted (xs @ ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sorted xs \<longrightarrow> l_sorted ys \<longrightarrow> last xs \<le> hd ys \<longrightarrow> l_sorted (xs @ ys)
[PROOF STEP]
proof (induction xs rule: l_sorted.induct, simp_all, (rule impI)+)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v. \<lbrakk>l_sorted ys; v \<le> hd ys\<rbrakk> \<Longrightarrow> l_sorted (v # ys)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v. \<lbrakk>l_sorted ys; v \<le> hd ys\<rbrakk> \<Longrightarrow> l_sorted (v # ys)
[PROOF STEP]
assume "l_sorted ys" and "x \<le> hd ys"
[PROOF STATE]
proof (state)
this:
l_sorted ys
x \<le> hd ys

goal (1 subgoal):
 1. \<And>v. \<lbrakk>l_sorted ys; v \<le> hd ys\<rbrakk> \<Longrightarrow> l_sorted (v # ys)
[PROOF STEP]
thus "l_sorted (x # ys)"
[PROOF STATE]
proof (prove)
using this:
l_sorted ys
x \<le> hd ys

goal (1 subgoal):
 1. l_sorted (x # ys)
[PROOF STEP]
by (cases ys, simp_all)
[PROOF STATE]
proof (state)
this:
l_sorted (x # ys)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma l_sort_invariance_1:
  assumes XY: "Y \<in> l_sort_set X" and X: "l_sort_inv_1 X"
  shows "l_sort_inv_1 Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sort_inv_1 Y
[PROOF STEP]
using XY
[PROOF STATE]
proof (prove)
using this:
Y \<in> l_sort_set X

goal (1 subgoal):
 1. l_sort_inv_1 Y
[PROOF STEP]
proof (rule l_sort_set.induct, simp_all)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. Y \<in> l_sort_set X \<Longrightarrow> l_sort_inv_1 X
 2. \<And>x xs ys. \<lbrakk>(x # xs, ys, []) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, []); Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sorted (ys @ [x])
 3. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, z # zs); x \<le> z; Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sorted (ys @ x # z # zs)
 4. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, z # zs); \<not> x \<le> z; Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
show "l_sort_inv_1 X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sort_inv_1 X
[PROOF STEP]
using X
[PROOF STATE]
proof (prove)
using this:
l_sort_inv_1 X

goal (1 subgoal):
 1. l_sort_inv_1 X
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
l_sort_inv_1 X

goal (3 subgoals):
 1. \<And>x xs ys. \<lbrakk>(x # xs, ys, []) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, []); Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sorted (ys @ [x])
 2. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, z # zs); x \<le> z; Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sorted (ys @ x # z # zs)
 3. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, z # zs); \<not> x \<le> z; Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x xs ys. \<lbrakk>(x # xs, ys, []) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, []); Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sorted (ys @ [x])
 2. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, z # zs); x \<le> z; Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sorted (ys @ x # z # zs)
 3. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, z # zs); \<not> x \<le> z; Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
fix x :: 'a and xs ys
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x xs ys. \<lbrakk>(x # xs, ys, []) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, []); Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sorted (ys @ [x])
 2. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, z # zs); x \<le> z; Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sorted (ys @ x # z # zs)
 3. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, z # zs); \<not> x \<le> z; Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
assume I: "l_sort_inv_1 (x # xs, ys, [])"
[PROOF STATE]
proof (state)
this:
l_sort_inv_1 (x # xs, ys, [])

goal (3 subgoals):
 1. \<And>x xs ys. \<lbrakk>(x # xs, ys, []) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, []); Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sorted (ys @ [x])
 2. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, z # zs); x \<le> z; Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sorted (ys @ x # z # zs)
 3. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, z # zs); \<not> x \<le> z; Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
show "l_sorted (ys @ [x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sorted (ys @ [x])
[PROOF STEP]
proof (cases ys, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. ys = a # list \<Longrightarrow> l_sorted (ys @ [x])
[PROOF STEP]
fix a as
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. ys = a # list \<Longrightarrow> l_sorted (ys @ [x])
[PROOF STEP]
assume "ys = a # as"
[PROOF STATE]
proof (state)
this:
ys = a # as

goal (1 subgoal):
 1. \<And>a list. ys = a # list \<Longrightarrow> l_sorted (ys @ [x])
[PROOF STEP]
hence "l_sorted ys \<and> last ys \<le> x"
[PROOF STATE]
proof (prove)
using this:
ys = a # as

goal (1 subgoal):
 1. l_sorted ys \<and> last ys \<le> x
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
ys = a # as
l_sort_inv_1 (x # xs, ys, [])

goal (1 subgoal):
 1. l_sorted ys \<and> last ys \<le> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l_sorted ys \<and> last ys \<le> x

goal (1 subgoal):
 1. \<And>a list. ys = a # list \<Longrightarrow> l_sorted (ys @ [x])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
l_sorted ys \<and> last ys \<le> x

goal (1 subgoal):
 1. \<And>a list. ys = a # list \<Longrightarrow> l_sorted (ys @ [x])
[PROOF STEP]
have "l_sorted [x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sorted [x]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l_sorted [x]

goal (1 subgoal):
 1. \<And>a list. ys = a # list \<Longrightarrow> l_sorted (ys @ [x])
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
l_sorted ys \<and> last ys \<le> x
l_sorted [x]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
l_sorted ys \<and> last ys \<le> x
l_sorted [x]

goal (1 subgoal):
 1. l_sorted (ys @ [x])
[PROOF STEP]
by (simp add: l_sorted_app)
[PROOF STATE]
proof (state)
this:
l_sorted (ys @ [x])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l_sorted (ys @ [x])

goal (2 subgoals):
 1. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, z # zs); x \<le> z; Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sorted (ys @ x # z # zs)
 2. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, z # zs); \<not> x \<le> z; Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, z # zs); x \<le> z; Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sorted (ys @ x # z # zs)
 2. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, z # zs); \<not> x \<le> z; Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
fix x :: 'a and xs ys z zs
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, z # zs); x \<le> z; Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sorted (ys @ x # z # zs)
 2. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, z # zs); \<not> x \<le> z; Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
assume XZ: "x \<le> z" and I: "l_sort_inv_1 (x # xs, ys, z # zs)"
[PROOF STATE]
proof (state)
this:
x \<le> z
l_sort_inv_1 (x # xs, ys, z # zs)

goal (2 subgoals):
 1. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, z # zs); x \<le> z; Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sorted (ys @ x # z # zs)
 2. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, z # zs); \<not> x \<le> z; Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
thus "l_sorted (ys @ x # z # zs)"
[PROOF STATE]
proof (prove)
using this:
x \<le> z
l_sort_inv_1 (x # xs, ys, z # zs)

goal (1 subgoal):
 1. l_sorted (ys @ x # z # zs)
[PROOF STEP]
proof (cases ys, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>x \<le> z; l_sort_inv_1 (x # xs, ys, z # zs); ys = a # list\<rbrakk> \<Longrightarrow> l_sorted (ys @ x # z # zs)
[PROOF STEP]
fix a as
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>x \<le> z; l_sort_inv_1 (x # xs, ys, z # zs); ys = a # list\<rbrakk> \<Longrightarrow> l_sorted (ys @ x # z # zs)
[PROOF STEP]
assume "ys = a # as"
[PROOF STATE]
proof (state)
this:
ys = a # as

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>x \<le> z; l_sort_inv_1 (x # xs, ys, z # zs); ys = a # list\<rbrakk> \<Longrightarrow> l_sorted (ys @ x # z # zs)
[PROOF STEP]
hence *: "l_sorted ys \<and> l_sorted (z # zs) \<and> last ys \<le> x"
[PROOF STATE]
proof (prove)
using this:
ys = a # as

goal (1 subgoal):
 1. l_sorted ys \<and> l_sorted (z # zs) \<and> last ys \<le> x
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
ys = a # as
l_sort_inv_1 (x # xs, ys, z # zs)

goal (1 subgoal):
 1. l_sorted ys \<and> l_sorted (z # zs) \<and> last ys \<le> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l_sorted ys \<and> l_sorted (z # zs) \<and> last ys \<le> x

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>x \<le> z; l_sort_inv_1 (x # xs, ys, z # zs); ys = a # list\<rbrakk> \<Longrightarrow> l_sorted (ys @ x # z # zs)
[PROOF STEP]
with XZ
[PROOF STATE]
proof (chain)
picking this:
x \<le> z
l_sorted ys \<and> l_sorted (z # zs) \<and> last ys \<le> x
[PROOF STEP]
have "l_sorted (x # z # zs)"
[PROOF STATE]
proof (prove)
using this:
x \<le> z
l_sorted ys \<and> l_sorted (z # zs) \<and> last ys \<le> x

goal (1 subgoal):
 1. l_sorted (x # z # zs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l_sorted (x # z # zs)

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>x \<le> z; l_sort_inv_1 (x # xs, ys, z # zs); ys = a # list\<rbrakk> \<Longrightarrow> l_sorted (ys @ x # z # zs)
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
l_sorted ys \<and> l_sorted (z # zs) \<and> last ys \<le> x
l_sorted (x # z # zs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
l_sorted ys \<and> l_sorted (z # zs) \<and> last ys \<le> x
l_sorted (x # z # zs)

goal (1 subgoal):
 1. l_sorted (ys @ x # z # zs)
[PROOF STEP]
by (simp add: l_sorted_app)
[PROOF STATE]
proof (state)
this:
l_sorted (ys @ x # z # zs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l_sorted (ys @ x # z # zs)

goal (1 subgoal):
 1. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, z # zs); \<not> x \<le> z; Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, z # zs); \<not> x \<le> z; Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
fix x :: 'a and xs ys z zs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, z # zs); \<not> x \<le> z; Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
assume "\<not> x \<le> z"
[PROOF STATE]
proof (state)
this:
\<not> x \<le> z

goal (1 subgoal):
 1. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, z # zs); \<not> x \<le> z; Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
hence XZ: "z \<le> x"
[PROOF STATE]
proof (prove)
using this:
\<not> x \<le> z

goal (1 subgoal):
 1. z \<le> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z \<le> x

goal (1 subgoal):
 1. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, z # zs); \<not> x \<le> z; Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
assume "l_sort_inv_1 (x # xs, ys, z # zs)"
[PROOF STATE]
proof (state)
this:
l_sort_inv_1 (x # xs, ys, z # zs)

goal (1 subgoal):
 1. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_1 (x # xs, ys, z # zs); \<not> x \<le> z; Y \<in> l_sort_set X\<rbrakk> \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
thus "l_sort_inv_1 (x # xs, ys @ [z], zs)"
[PROOF STATE]
proof (prove)
using this:
l_sort_inv_1 (x # xs, ys, z # zs)

goal (1 subgoal):
 1. l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
proof (cases ys, simp)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>l_sorted (z # zs); ys = []\<rbrakk> \<Longrightarrow> l_sort_inv_1 (x # xs, [z], zs)
 2. \<And>a list. \<lbrakk>l_sort_inv_1 (x # xs, ys, z # zs); ys = a # list\<rbrakk> \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
assume I: "l_sorted (z # zs)"
[PROOF STATE]
proof (state)
this:
l_sorted (z # zs)

goal (2 subgoals):
 1. \<lbrakk>l_sorted (z # zs); ys = []\<rbrakk> \<Longrightarrow> l_sort_inv_1 (x # xs, [z], zs)
 2. \<And>a list. \<lbrakk>l_sort_inv_1 (x # xs, ys, z # zs); ys = a # list\<rbrakk> \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
show "l_sort_inv_1 (x # xs, [z], zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sort_inv_1 (x # xs, [z], zs)
[PROOF STEP]
proof (cases zs, simp)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. zs = [] \<Longrightarrow> z \<le> x
 2. \<And>a list. zs = a # list \<Longrightarrow> l_sort_inv_1 (x # xs, [z], zs)
[PROOF STEP]
show "z \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<le> x
[PROOF STEP]
using XZ
[PROOF STATE]
proof (prove)
using this:
z \<le> x

goal (1 subgoal):
 1. z \<le> x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
z \<le> x

goal (1 subgoal):
 1. \<And>a list. zs = a # list \<Longrightarrow> l_sort_inv_1 (x # xs, [z], zs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. zs = a # list \<Longrightarrow> l_sort_inv_1 (x # xs, [z], zs)
[PROOF STEP]
fix a as
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. zs = a # list \<Longrightarrow> l_sort_inv_1 (x # xs, [z], zs)
[PROOF STEP]
assume zs: "zs = a # as"
[PROOF STATE]
proof (state)
this:
zs = a # as

goal (1 subgoal):
 1. \<And>a list. zs = a # list \<Longrightarrow> l_sort_inv_1 (x # xs, [z], zs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zs = a # as
[PROOF STEP]
have *: "z \<le> a \<and> l_sorted zs"
[PROOF STATE]
proof (prove)
using this:
zs = a # as

goal (1 subgoal):
 1. z \<le> a \<and> l_sorted zs
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
zs = a # as
l_sorted (z # zs)

goal (1 subgoal):
 1. z \<le> a \<and> l_sorted zs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z \<le> a \<and> l_sorted zs

goal (1 subgoal):
 1. \<And>a list. zs = a # list \<Longrightarrow> l_sort_inv_1 (x # xs, [z], zs)
[PROOF STEP]
have "l_sorted [z]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sorted [z]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l_sorted [z]

goal (1 subgoal):
 1. \<And>a list. zs = a # list \<Longrightarrow> l_sort_inv_1 (x # xs, [z], zs)
[PROOF STEP]
with zs *
[PROOF STATE]
proof (chain)
picking this:
zs = a # as
z \<le> a \<and> l_sorted zs
l_sorted [z]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
zs = a # as
z \<le> a \<and> l_sorted zs
l_sorted [z]

goal (1 subgoal):
 1. l_sort_inv_1 (x # xs, [z], zs)
[PROOF STEP]
using XZ
[PROOF STATE]
proof (prove)
using this:
zs = a # as
z \<le> a \<and> l_sorted zs
l_sorted [z]
z \<le> x

goal (1 subgoal):
 1. l_sort_inv_1 (x # xs, [z], zs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l_sort_inv_1 (x # xs, [z], zs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l_sort_inv_1 (x # xs, [z], zs)

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>l_sort_inv_1 (x # xs, ys, z # zs); ys = a # list\<rbrakk> \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>l_sort_inv_1 (x # xs, ys, z # zs); ys = a # list\<rbrakk> \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
fix a as
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>l_sort_inv_1 (x # xs, ys, z # zs); ys = a # list\<rbrakk> \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
assume YS: "ys = a # as" and "l_sort_inv_1 (x # xs, ys, z # zs)"
[PROOF STATE]
proof (state)
this:
ys = a # as
l_sort_inv_1 (x # xs, ys, z # zs)

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>l_sort_inv_1 (x # xs, ys, z # zs); ys = a # list\<rbrakk> \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
hence I: "l_sorted ys \<and> l_sorted (z # zs) \<and> last ys \<le> z"
[PROOF STATE]
proof (prove)
using this:
ys = a # as
l_sort_inv_1 (x # xs, ys, z # zs)

goal (1 subgoal):
 1. l_sorted ys \<and> l_sorted (z # zs) \<and> last ys \<le> z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l_sorted ys \<and> l_sorted (z # zs) \<and> last ys \<le> z

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>l_sort_inv_1 (x # xs, ys, z # zs); ys = a # list\<rbrakk> \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
have "l_sorted [z]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sorted [z]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l_sorted [z]

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>l_sort_inv_1 (x # xs, ys, z # zs); ys = a # list\<rbrakk> \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
hence I': "l_sorted (ys @ [z])"
[PROOF STATE]
proof (prove)
using this:
l_sorted [z]

goal (1 subgoal):
 1. l_sorted (ys @ [z])
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
l_sorted [z]
l_sorted ys \<and> l_sorted (z # zs) \<and> last ys \<le> z

goal (1 subgoal):
 1. l_sorted (ys @ [z])
[PROOF STEP]
by (simp add: l_sorted_app)
[PROOF STATE]
proof (state)
this:
l_sorted (ys @ [z])

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>l_sort_inv_1 (x # xs, ys, z # zs); ys = a # list\<rbrakk> \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
proof (cases zs, simp)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. zs = [] \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], [])
 2. \<And>a list. zs = a # list \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
show "l_sort_inv_1 (x # xs, ys @ [z], [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sort_inv_1 (x # xs, ys @ [z], [])
[PROOF STEP]
using I' and XZ and YS
[PROOF STATE]
proof (prove)
using this:
l_sorted (ys @ [z])
z \<le> x
ys = a # as

goal (1 subgoal):
 1. l_sort_inv_1 (x # xs, ys @ [z], [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l_sort_inv_1 (x # xs, ys @ [z], [])

goal (1 subgoal):
 1. \<And>a list. zs = a # list \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. zs = a # list \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
fix b bs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. zs = a # list \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
assume zs: "zs = b # bs"
[PROOF STATE]
proof (state)
this:
zs = b # bs

goal (1 subgoal):
 1. \<And>a list. zs = a # list \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zs = b # bs
[PROOF STEP]
have "z \<le> b \<and> l_sorted zs"
[PROOF STATE]
proof (prove)
using this:
zs = b # bs

goal (1 subgoal):
 1. z \<le> b \<and> l_sorted zs
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
zs = b # bs
l_sorted ys \<and> l_sorted (z # zs) \<and> last ys \<le> z

goal (1 subgoal):
 1. z \<le> b \<and> l_sorted zs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z \<le> b \<and> l_sorted zs

goal (1 subgoal):
 1. \<And>a list. zs = a # list \<Longrightarrow> l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
with zs
[PROOF STATE]
proof (chain)
picking this:
zs = b # bs
z \<le> b \<and> l_sorted zs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
zs = b # bs
z \<le> b \<and> l_sorted zs

goal (1 subgoal):
 1. l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
using I and I' and XZ and YS
[PROOF STATE]
proof (prove)
using this:
zs = b # bs
z \<le> b \<and> l_sorted zs
l_sorted ys \<and> l_sorted (z # zs) \<and> last ys \<le> z
l_sorted (ys @ [z])
z \<le> x
ys = a # as

goal (1 subgoal):
 1. l_sort_inv_1 (x # xs, ys @ [z], zs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l_sort_inv_1 (x # xs, ys @ [z], zs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l_sort_inv_1 (x # xs, ys @ [z], zs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l_sort_inv_1 (x # xs, ys @ [z], zs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma l_count_cons: "l_count x (y # ys) = l_count x [y] + l_count x ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_count x (y # ys) = l_count x [y] + l_count x ys
[PROOF STEP]
by (simp add: l_count_def)


[STATEMENT]
lemma l_count_app: "l_count x (ys @ zs) = l_count x ys + l_count x zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_count x (ys @ zs) = l_count x ys + l_count x zs
[PROOF STEP]
by (simp add: l_count_def)


[STATEMENT]
lemma l_sort_invariance_2:
  assumes XY: "Y \<in> l_sort_set X" and X: "l_sort_inv_2 w ws X"
  shows "l_sort_inv_2 w ws Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sort_inv_2 w ws Y
[PROOF STEP]
using XY
[PROOF STATE]
proof (prove)
using this:
Y \<in> l_sort_set X

goal (1 subgoal):
 1. l_sort_inv_2 w ws Y
[PROOF STEP]
proof (rule l_sort_set.induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. l_sort_inv_2 w ws X
 2. \<And>x xs ys. \<lbrakk>(x # xs, ys, []) \<in> l_sort_set X; l_sort_inv_2 w ws (x # xs, ys, [])\<rbrakk> \<Longrightarrow> l_sort_inv_2 w ws (xs, [], ys @ [x])
 3. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_2 w ws (x # xs, ys, z # zs); x \<le> z\<rbrakk> \<Longrightarrow> l_sort_inv_2 w ws (xs, [], ys @ x # z # zs)
 4. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_2 w ws (x # xs, ys, z # zs); \<not> x \<le> z\<rbrakk> \<Longrightarrow> l_sort_inv_2 w ws (x # xs, ys @ [z], zs)
[PROOF STEP]
show "l_sort_inv_2 w ws X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sort_inv_2 w ws X
[PROOF STEP]
using X
[PROOF STATE]
proof (prove)
using this:
l_sort_inv_2 w ws X

goal (1 subgoal):
 1. l_sort_inv_2 w ws X
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
l_sort_inv_2 w ws X

goal (3 subgoals):
 1. \<And>x xs ys. \<lbrakk>(x # xs, ys, []) \<in> l_sort_set X; l_sort_inv_2 w ws (x # xs, ys, [])\<rbrakk> \<Longrightarrow> l_sort_inv_2 w ws (xs, [], ys @ [x])
 2. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_2 w ws (x # xs, ys, z # zs); x \<le> z\<rbrakk> \<Longrightarrow> l_sort_inv_2 w ws (xs, [], ys @ x # z # zs)
 3. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_2 w ws (x # xs, ys, z # zs); \<not> x \<le> z\<rbrakk> \<Longrightarrow> l_sort_inv_2 w ws (x # xs, ys @ [z], zs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x xs ys. \<lbrakk>(x # xs, ys, []) \<in> l_sort_set X; l_sort_inv_2 w ws (x # xs, ys, [])\<rbrakk> \<Longrightarrow> l_sort_inv_2 w ws (xs, [], ys @ [x])
 2. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_2 w ws (x # xs, ys, z # zs); x \<le> z\<rbrakk> \<Longrightarrow> l_sort_inv_2 w ws (xs, [], ys @ x # z # zs)
 3. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_2 w ws (x # xs, ys, z # zs); \<not> x \<le> z\<rbrakk> \<Longrightarrow> l_sort_inv_2 w ws (x # xs, ys @ [z], zs)
[PROOF STEP]
fix x xs ys
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x xs ys. \<lbrakk>(x # xs, ys, []) \<in> l_sort_set X; l_sort_inv_2 w ws (x # xs, ys, [])\<rbrakk> \<Longrightarrow> l_sort_inv_2 w ws (xs, [], ys @ [x])
 2. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_2 w ws (x # xs, ys, z # zs); x \<le> z\<rbrakk> \<Longrightarrow> l_sort_inv_2 w ws (xs, [], ys @ x # z # zs)
 3. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_2 w ws (x # xs, ys, z # zs); \<not> x \<le> z\<rbrakk> \<Longrightarrow> l_sort_inv_2 w ws (x # xs, ys @ [z], zs)
[PROOF STEP]
assume "l_sort_inv_2 w ws (x # xs, ys, [])"
[PROOF STATE]
proof (state)
this:
l_sort_inv_2 w ws (x # xs, ys, [])

goal (3 subgoals):
 1. \<And>x xs ys. \<lbrakk>(x # xs, ys, []) \<in> l_sort_set X; l_sort_inv_2 w ws (x # xs, ys, [])\<rbrakk> \<Longrightarrow> l_sort_inv_2 w ws (xs, [], ys @ [x])
 2. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_2 w ws (x # xs, ys, z # zs); x \<le> z\<rbrakk> \<Longrightarrow> l_sort_inv_2 w ws (xs, [], ys @ x # z # zs)
 3. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_2 w ws (x # xs, ys, z # zs); \<not> x \<le> z\<rbrakk> \<Longrightarrow> l_sort_inv_2 w ws (x # xs, ys @ [z], zs)
[PROOF STEP]
thus "l_sort_inv_2 w ws (xs, [], ys @ [x])"
[PROOF STATE]
proof (prove)
using this:
l_sort_inv_2 w ws (x # xs, ys, [])

goal (1 subgoal):
 1. l_sort_inv_2 w ws (xs, [], ys @ [x])
[PROOF STEP]
proof (simp add: l_sort_inv_2_def, subst (asm) l_count_cons, subst l_count_app)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>l_count w [x] + l_count w xs + l_count w ys + l_count w [] = l_count w ws; l_sort_inv_2 w ws (x # xs, ys, []); l_sort_inv_2 w ws (x # xs, ys, [])\<rbrakk> \<Longrightarrow> l_count w xs + l_count w [] + (l_count w ys + l_count w [x]) = l_count w ws
[PROOF STEP]
qed (simp add: l_count_def ac_simps)
[PROOF STATE]
proof (state)
this:
l_sort_inv_2 w ws (xs, [], ys @ [x])

goal (2 subgoals):
 1. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_2 w ws (x # xs, ys, z # zs); x \<le> z\<rbrakk> \<Longrightarrow> l_sort_inv_2 w ws (xs, [], ys @ x # z # zs)
 2. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_2 w ws (x # xs, ys, z # zs); \<not> x \<le> z\<rbrakk> \<Longrightarrow> l_sort_inv_2 w ws (x # xs, ys @ [z], zs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_2 w ws (x # xs, ys, z # zs); x \<le> z\<rbrakk> \<Longrightarrow> l_sort_inv_2 w ws (xs, [], ys @ x # z # zs)
 2. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_2 w ws (x # xs, ys, z # zs); \<not> x \<le> z\<rbrakk> \<Longrightarrow> l_sort_inv_2 w ws (x # xs, ys @ [z], zs)
[PROOF STEP]
fix x xs ys z zs
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_2 w ws (x # xs, ys, z # zs); x \<le> z\<rbrakk> \<Longrightarrow> l_sort_inv_2 w ws (xs, [], ys @ x # z # zs)
 2. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_2 w ws (x # xs, ys, z # zs); \<not> x \<le> z\<rbrakk> \<Longrightarrow> l_sort_inv_2 w ws (x # xs, ys @ [z], zs)
[PROOF STEP]
assume "l_sort_inv_2 w ws (x # xs, ys, z # zs)"
[PROOF STATE]
proof (state)
this:
l_sort_inv_2 w ws (x # xs, ys, z # zs)

goal (2 subgoals):
 1. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_2 w ws (x # xs, ys, z # zs); x \<le> z\<rbrakk> \<Longrightarrow> l_sort_inv_2 w ws (xs, [], ys @ x # z # zs)
 2. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_2 w ws (x # xs, ys, z # zs); \<not> x \<le> z\<rbrakk> \<Longrightarrow> l_sort_inv_2 w ws (x # xs, ys @ [z], zs)
[PROOF STEP]
thus "l_sort_inv_2 w ws (xs, [], ys @ x # z # zs)"
[PROOF STATE]
proof (prove)
using this:
l_sort_inv_2 w ws (x # xs, ys, z # zs)

goal (1 subgoal):
 1. l_sort_inv_2 w ws (xs, [], ys @ x # z # zs)
[PROOF STEP]
proof (simp add: l_sort_inv_2_def, subst (asm) l_count_cons, subst l_count_app,
   subst l_count_cons)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>l_count w [x] + l_count w xs + l_count w ys + l_count w (z # zs) = l_count w ws; l_sort_inv_2 w ws (x # xs, ys, z # zs); l_sort_inv_2 w ws (x # xs, ys, z # zs); l_sort_inv_2 w ws (x # xs, ys, z # zs)\<rbrakk> \<Longrightarrow> l_count w xs + l_count w [] + (l_count w ys + (l_count w [x] + l_count w (z # zs))) = l_count w ws
[PROOF STEP]
qed (simp add: l_count_def ac_simps)
[PROOF STATE]
proof (state)
this:
l_sort_inv_2 w ws (xs, [], ys @ x # z # zs)

goal (1 subgoal):
 1. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_2 w ws (x # xs, ys, z # zs); \<not> x \<le> z\<rbrakk> \<Longrightarrow> l_sort_inv_2 w ws (x # xs, ys @ [z], zs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_2 w ws (x # xs, ys, z # zs); \<not> x \<le> z\<rbrakk> \<Longrightarrow> l_sort_inv_2 w ws (x # xs, ys @ [z], zs)
[PROOF STEP]
fix x xs ys z zs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_2 w ws (x # xs, ys, z # zs); \<not> x \<le> z\<rbrakk> \<Longrightarrow> l_sort_inv_2 w ws (x # xs, ys @ [z], zs)
[PROOF STEP]
assume "l_sort_inv_2 w ws (x # xs, ys, z # zs)"
[PROOF STATE]
proof (state)
this:
l_sort_inv_2 w ws (x # xs, ys, z # zs)

goal (1 subgoal):
 1. \<And>x xs ys z zs. \<lbrakk>(x # xs, ys, z # zs) \<in> l_sort_set X; l_sort_inv_2 w ws (x # xs, ys, z # zs); \<not> x \<le> z\<rbrakk> \<Longrightarrow> l_sort_inv_2 w ws (x # xs, ys @ [z], zs)
[PROOF STEP]
thus "l_sort_inv_2 w ws (x # xs, ys @ [z], zs)"
[PROOF STATE]
proof (prove)
using this:
l_sort_inv_2 w ws (x # xs, ys, z # zs)

goal (1 subgoal):
 1. l_sort_inv_2 w ws (x # xs, ys @ [z], zs)
[PROOF STEP]
proof (simp add: l_sort_inv_2_def, subst (asm) (2) l_count_cons,
   subst l_count_app)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>l_count w (x # xs) + l_count w ys + (l_count w [z] + l_count w zs) = l_count w ws; l_sort_inv_2 w ws (x # xs, ys, z # zs); l_sort_inv_2 w ws (x # xs, ys, z # zs)\<rbrakk> \<Longrightarrow> l_count w (x # xs) + (l_count w ys + l_count w [z]) + l_count w zs = l_count w ws
[PROOF STEP]
qed (simp add: l_count_def ac_simps)
[PROOF STATE]
proof (state)
this:
l_sort_inv_2 w ws (x # xs, ys @ [z], zs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem "l_sorted (l_sort xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sorted (l_sort xs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l_sorted (l_sort xs)
[PROOF STEP]
let ?X = "(xs, [], [])"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l_sorted (l_sort xs)
[PROOF STEP]
have "l_sort_aux ?X \<in> l_sort_set ?X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sort_aux (xs, [], []) \<in> l_sort_set (xs, [], [])
[PROOF STEP]
by (rule l_sort_aux_set)
[PROOF STATE]
proof (state)
this:
l_sort_aux (xs, [], []) \<in> l_sort_set (xs, [], [])

goal (1 subgoal):
 1. l_sorted (l_sort xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
l_sort_aux (xs, [], []) \<in> l_sort_set (xs, [], [])

goal (1 subgoal):
 1. l_sorted (l_sort xs)
[PROOF STEP]
have "l_sort_inv_1 ?X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sort_inv_1 (xs, [], [])
[PROOF STEP]
by (rule l_sort_input_1)
[PROOF STATE]
proof (state)
this:
l_sort_inv_1 (xs, [], [])

goal (1 subgoal):
 1. l_sorted (l_sort xs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
l_sort_aux (xs, [], []) \<in> l_sort_set (xs, [], [])
l_sort_inv_1 (xs, [], [])
[PROOF STEP]
have "l_sort_inv_1 (l_sort_aux ?X)"
[PROOF STATE]
proof (prove)
using this:
l_sort_aux (xs, [], []) \<in> l_sort_set (xs, [], [])
l_sort_inv_1 (xs, [], [])

goal (1 subgoal):
 1. l_sort_inv_1 (l_sort_aux (xs, [], []))
[PROOF STEP]
by (rule l_sort_invariance_1)
[PROOF STATE]
proof (state)
this:
l_sort_inv_1 (l_sort_aux (xs, [], []))

goal (1 subgoal):
 1. l_sorted (l_sort xs)
[PROOF STEP]
hence "l_sorted (l_sort_out (l_sort_aux ?X))"
[PROOF STATE]
proof (prove)
using this:
l_sort_inv_1 (l_sort_aux (xs, [], []))

goal (1 subgoal):
 1. l_sorted (l_sort_out (l_sort_aux (xs, [], [])))
[PROOF STEP]
by (rule l_sort_intro_1)
[PROOF STATE]
proof (state)
this:
l_sorted (l_sort_out (l_sort_aux (xs, [], [])))

goal (1 subgoal):
 1. l_sorted (l_sort xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
l_sorted (l_sort_out (l_sort_aux (xs, [], [])))

goal (1 subgoal):
 1. l_sorted (l_sort xs)
[PROOF STEP]
have "?X = l_sort_in xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs, [], []) = l_sort_in xs
[PROOF STEP]
by (simp add: l_sort_in_def)
[PROOF STATE]
proof (state)
this:
(xs, [], []) = l_sort_in xs

goal (1 subgoal):
 1. l_sorted (l_sort xs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
l_sorted (l_sort_out (l_sort_aux (xs, [], [])))
(xs, [], []) = l_sort_in xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
l_sorted (l_sort_out (l_sort_aux (xs, [], [])))
(xs, [], []) = l_sort_in xs

goal (1 subgoal):
 1. l_sorted (l_sort xs)
[PROOF STEP]
by (simp add: l_sort_def)
[PROOF STATE]
proof (state)
this:
l_sorted (l_sort xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem "l_count x (l_sort xs) = l_count x xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_count x (l_sort xs) = l_count x xs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l_count x (l_sort xs) = l_count x xs
[PROOF STEP]
let ?X = "(xs, [], [])"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l_count x (l_sort xs) = l_count x xs
[PROOF STEP]
have "l_sort_aux ?X \<in> l_sort_set ?X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sort_aux (xs, [], []) \<in> l_sort_set (xs, [], [])
[PROOF STEP]
by (rule l_sort_aux_set)
[PROOF STATE]
proof (state)
this:
l_sort_aux (xs, [], []) \<in> l_sort_set (xs, [], [])

goal (1 subgoal):
 1. l_count x (l_sort xs) = l_count x xs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
l_sort_aux (xs, [], []) \<in> l_sort_set (xs, [], [])

goal (1 subgoal):
 1. l_count x (l_sort xs) = l_count x xs
[PROOF STEP]
have "l_sort_inv_2 x xs ?X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sort_inv_2 x xs (xs, [], [])
[PROOF STEP]
by (rule l_sort_input_2)
[PROOF STATE]
proof (state)
this:
l_sort_inv_2 x xs (xs, [], [])

goal (1 subgoal):
 1. l_count x (l_sort xs) = l_count x xs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
l_sort_aux (xs, [], []) \<in> l_sort_set (xs, [], [])
l_sort_inv_2 x xs (xs, [], [])
[PROOF STEP]
have "l_sort_inv_2 x xs (l_sort_aux ?X)"
[PROOF STATE]
proof (prove)
using this:
l_sort_aux (xs, [], []) \<in> l_sort_set (xs, [], [])
l_sort_inv_2 x xs (xs, [], [])

goal (1 subgoal):
 1. l_sort_inv_2 x xs (l_sort_aux (xs, [], []))
[PROOF STEP]
by (rule l_sort_invariance_2)
[PROOF STATE]
proof (state)
this:
l_sort_inv_2 x xs (l_sort_aux (xs, [], []))

goal (1 subgoal):
 1. l_count x (l_sort xs) = l_count x xs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
l_sort_inv_2 x xs (l_sort_aux (xs, [], []))

goal (1 subgoal):
 1. l_count x (l_sort xs) = l_count x xs
[PROOF STEP]
have "l_sort_form (l_sort_aux ?X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_sort_form (l_sort_aux (xs, [], []))
[PROOF STEP]
by (rule l_sort_form_aux)
[PROOF STATE]
proof (state)
this:
l_sort_form (l_sort_aux (xs, [], []))

goal (1 subgoal):
 1. l_count x (l_sort xs) = l_count x xs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
l_sort_inv_2 x xs (l_sort_aux (xs, [], []))
l_sort_form (l_sort_aux (xs, [], []))
[PROOF STEP]
have "l_count x (l_sort_out (l_sort_aux ?X)) = l_count x xs"
[PROOF STATE]
proof (prove)
using this:
l_sort_inv_2 x xs (l_sort_aux (xs, [], []))
l_sort_form (l_sort_aux (xs, [], []))

goal (1 subgoal):
 1. l_count x (l_sort_out (l_sort_aux (xs, [], []))) = l_count x xs
[PROOF STEP]
by (rule l_sort_intro_2)
[PROOF STATE]
proof (state)
this:
l_count x (l_sort_out (l_sort_aux (xs, [], []))) = l_count x xs

goal (1 subgoal):
 1. l_count x (l_sort xs) = l_count x xs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
l_count x (l_sort_out (l_sort_aux (xs, [], []))) = l_count x xs

goal (1 subgoal):
 1. l_count x (l_sort xs) = l_count x xs
[PROOF STEP]
have "?X = l_sort_in xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs, [], []) = l_sort_in xs
[PROOF STEP]
by (simp add: l_sort_in_def)
[PROOF STATE]
proof (state)
this:
(xs, [], []) = l_sort_in xs

goal (1 subgoal):
 1. l_count x (l_sort xs) = l_count x xs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
l_count x (l_sort_out (l_sort_aux (xs, [], []))) = l_count x xs
(xs, [], []) = l_sort_in xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
l_count x (l_sort_out (l_sort_aux (xs, [], []))) = l_count x xs
(xs, [], []) = l_sort_in xs

goal (1 subgoal):
 1. l_count x (l_sort xs) = l_count x xs
[PROOF STEP]
by (simp add: l_sort_def)
[PROOF STATE]
proof (state)
this:
l_count x (l_sort xs) = l_count x xs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma var_swap_ref1:
  "rel_R \<lceil>\<lambda>s. s ''x'' = a \<and> s ''y'' = b\<rceil> \<lceil>\<lambda>s. s ''x'' = b \<and> s ''y'' = a\<rceil>
   \<supseteq> (''z'' ::= (\<lambda>s. s ''x'')); rel_R \<lceil>\<lambda>s. s ''z'' = a \<and> s ''y'' = b\<rceil> \<lceil>\<lambda>s. s ''x'' = b \<and> s ''y'' = a\<rceil>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (''z'' ::= (\<lambda>s. s ''x'')) ; rel_R \<lceil>\<lambda>s. s ''z'' = a \<and> s ''y'' = b\<rceil> \<lceil>\<lambda>s. s ''x'' = b \<and> s ''y'' = a\<rceil> \<subseteq> rel_R \<lceil>\<lambda>s. s ''x'' = a \<and> s ''y'' = b\<rceil> \<lceil>\<lambda>s. s ''x'' = b \<and> s ''y'' = a\<rceil>
[PROOF STEP]
by (rule R_assignl, auto)


[STATEMENT]
lemma var_swap_ref2:
  "rel_R \<lceil>\<lambda>s. s ''z'' = a \<and> s ''y'' = b\<rceil> \<lceil>\<lambda>s. s ''x'' = b \<and> s ''y'' = a\<rceil>
   \<supseteq> (''x'' ::= (\<lambda>s. s ''y'')); rel_R \<lceil>\<lambda>s. s ''z'' = a \<and> s ''x'' = b\<rceil> \<lceil>\<lambda>s. s ''x'' = b \<and> s ''y'' = a\<rceil>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (''x'' ::= (\<lambda>s. s ''y'')) ; rel_R \<lceil>\<lambda>s. s ''z'' = a \<and> s ''x'' = b\<rceil> \<lceil>\<lambda>s. s ''x'' = b \<and> s ''y'' = a\<rceil> \<subseteq> rel_R \<lceil>\<lambda>s. s ''z'' = a \<and> s ''y'' = b\<rceil> \<lceil>\<lambda>s. s ''x'' = b \<and> s ''y'' = a\<rceil>
[PROOF STEP]
by (rule R_assignl, auto)


[STATEMENT]
lemma var_swap_ref3:
  "rel_R \<lceil>\<lambda>s. s ''z'' = a \<and> s ''x'' = b\<rceil> \<lceil>\<lambda>s. s ''x'' = b \<and> s ''y'' = a\<rceil>
   \<supseteq> (''y'' ::= (\<lambda>s. s ''z'')); rel_R \<lceil>\<lambda>s. s ''x'' = b \<and> s ''y'' = a\<rceil> \<lceil>\<lambda>s. s ''x'' = b \<and> s ''y'' = a\<rceil>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (''y'' ::= (\<lambda>s. s ''z'')) ; rel_R \<lceil>\<lambda>s. s ''x'' = b \<and> s ''y'' = a\<rceil> \<lceil>\<lambda>s. s ''x'' = b \<and> s ''y'' = a\<rceil> \<subseteq> rel_R \<lceil>\<lambda>s. s ''z'' = a \<and> s ''x'' = b\<rceil> \<lceil>\<lambda>s. s ''x'' = b \<and> s ''y'' = a\<rceil>
[PROOF STEP]
by (rule R_assignl, auto)


[STATEMENT]
lemma var_swap_ref_var:
  "rel_R \<lceil>\<lambda>s. s ''x'' = a \<and> s ''y'' = b\<rceil> \<lceil>\<lambda>s. s ''x'' = b \<and> s ''y'' = a\<rceil>
   \<supseteq> (''z'' ::= (\<lambda>s. s ''x'')); (''x'' ::= (\<lambda>s. s ''y'')); (''y'' ::= (\<lambda>s. s ''z''))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (''z'' ::= (\<lambda>s. s ''x'')) ; (''x'' ::= (\<lambda>s. s ''y'')) ; (''y'' ::= (\<lambda>s. s ''z'')) \<subseteq> rel_R \<lceil>\<lambda>s. s ''x'' = a \<and> s ''y'' = b\<rceil> \<lceil>\<lambda>s. s ''x'' = b \<and> s ''y'' = a\<rceil>
[PROOF STEP]
using var_swap_ref1 var_swap_ref2 var_swap_ref3 rel_rkat.R_skip
[PROOF STATE]
proof (prove)
using this:
(''z'' ::= (\<lambda>s. s ''x'')) ; rel_R \<lceil>\<lambda>s. s ''z'' = ?a \<and> s ''y'' = ?b\<rceil> \<lceil>\<lambda>s. s ''x'' = ?b \<and> s ''y'' = ?a\<rceil> \<subseteq> rel_R \<lceil>\<lambda>s. s ''x'' = ?a \<and> s ''y'' = ?b\<rceil> \<lceil>\<lambda>s. s ''x'' = ?b \<and> s ''y'' = ?a\<rceil>
(''x'' ::= (\<lambda>s. s ''y'')) ; rel_R \<lceil>\<lambda>s. s ''z'' = ?a \<and> s ''x'' = ?b\<rceil> \<lceil>\<lambda>s. s ''x'' = ?b \<and> s ''y'' = ?a\<rceil> \<subseteq> rel_R \<lceil>\<lambda>s. s ''z'' = ?a \<and> s ''y'' = ?b\<rceil> \<lceil>\<lambda>s. s ''x'' = ?b \<and> s ''y'' = ?a\<rceil>
(''y'' ::= (\<lambda>s. s ''z'')) ; rel_R \<lceil>\<lambda>s. s ''x'' = ?b \<and> s ''y'' = ?a\<rceil> \<lceil>\<lambda>s. s ''x'' = ?b \<and> s ''y'' = ?a\<rceil> \<subseteq> rel_R \<lceil>\<lambda>s. s ''z'' = ?a \<and> s ''x'' = ?b\<rceil> \<lceil>\<lambda>s. s ''x'' = ?b \<and> s ''y'' = ?a\<rceil>
Id \<subseteq> rel_R ?p ?p

goal (1 subgoal):
 1. (''z'' ::= (\<lambda>s. s ''x'')) ; (''x'' ::= (\<lambda>s. s ''y'')) ; (''y'' ::= (\<lambda>s. s ''z'')) \<subseteq> rel_R \<lceil>\<lambda>s. s ''x'' = a \<and> s ''y'' = b\<rceil> \<lceil>\<lambda>s. s ''x'' = b \<and> s ''y'' = a\<rceil>
[PROOF STEP]
by fastforce


[STATEMENT]
lemma CFG_equal_Use_equal_call:
  assumes "valid_edge a" and "kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs" and "valid_edge a'"
  and "kind a' = Q':r'\<hookrightarrow>\<^bsub>p'\<^esub>fs'" and "sourcenode a = sourcenode a'"
  and "pred (kind a) s" and "pred (kind a') s'"
  and "snd (hd s) = snd (hd s')" and "length s = length s'"
  and "\<forall>V \<in> Use (sourcenode a). state_val s V = state_val s' V"
  shows "a = a'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = a'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a = a'
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>pred (kind a) s\<close> \<open>snd (hd s) = snd (hd s')\<close>
    \<open>\<forall>V \<in> Use (sourcenode a). state_val s V = state_val s' V\<close> \<open>length s = length s'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
pred (kind a) s
snd (hd s) = snd (hd s')
\<forall>V\<in>Use (sourcenode a). state_val s V = state_val s' V
length s = length s'
[PROOF STEP]
have "pred (kind a) s'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
pred (kind a) s
snd (hd s) = snd (hd s')
\<forall>V\<in>Use (sourcenode a). state_val s V = state_val s' V
length s = length s'

goal (1 subgoal):
 1. pred (kind a) s'
[PROOF STEP]
by(rule CFG_edge_Uses_pred_equal)
[PROOF STATE]
proof (state)
this:
pred (kind a) s'

goal (1 subgoal):
 1. a = a'
[PROOF STEP]
with \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> \<open>valid_edge a'\<close> \<open>kind a' = Q':r'\<hookrightarrow>\<^bsub>p'\<^esub>fs'\<close>
    \<open>sourcenode a = sourcenode a'\<close> \<open>pred (kind a') s'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
valid_edge a'
kind a' = Q':r'\<hookrightarrow>\<^bsub>p'\<^esub>fs'
sourcenode a = sourcenode a'
pred (kind a') s'
pred (kind a) s'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
valid_edge a'
kind a' = Q':r'\<hookrightarrow>\<^bsub>p'\<^esub>fs'
sourcenode a = sourcenode a'
pred (kind a') s'
pred (kind a) s'

goal (1 subgoal):
 1. a = a'
[PROOF STEP]
by -(rule CFG_call_determ)
[PROOF STATE]
proof (state)
this:
a = a'

goal:
No subgoals!
[PROOF STEP]
qed