[STATEMENT]
lemma box_partial_correctness:
  "|x]1 = 1 \<longleftrightarrow> x * bot \<le> Z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (| x ] (1::'a) = (1::'a)) = (x * bot \<le> Z)
[PROOF STEP]
by (simp add: box_x_1 a_strict)


[STATEMENT]
lemma diamond_split:
  "|x>y = d(z) * |x>y \<squnion> a(z) * |x>y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > y = d z * | x > y \<squnion> a z * | x > y
[PROOF STEP]
by (metis d_def diamond_def sup_monoid.add_commute tests_dual.sba_dual.sup_cases tests_dual.sub_commutative)


[STATEMENT]
lemma box_import_shunting:
  "-p * -q \<le> |x](-r) \<longleftrightarrow> -q \<le> |-p * x](-r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a p * a q \<le> | x ] a r) = (a q \<le> | a p * x ] a r)
[PROOF STEP]
by (smt box_demodalisation_2 mult_assoc sub_comm sub_mult_closed)


[STATEMENT]
lemma diamond_right_dist_sup:
  "|x>(y \<squnion> z) = |x>y \<squnion> |x>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > (y \<squnion> z) = | x > y \<squnion> | x > z
[PROOF STEP]
by (simp add: d_dist_sup diamond_def mult_left_dist_sup)


[STATEMENT]
lemma box_right_mult_d_d:
  "|x](d(y) * d(z)) = |x]d(y) * |x]d(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] (d y * d z) = | x ] d y * | x ] d z
[PROOF STEP]
using a_dist_sup box_d_a box_def d_def mult_left_dist_sup
[PROOF STATE]
proof (prove)
using this:
a (?x \<squnion> ?y) = a ?x * a ?y
| d ?x ] a ?y = a ?x \<squnion> a ?y
| ?x ] ?y = a (?x * a ?y)
d ?x = a (a ?x)
?x * (?y \<squnion> ?z) = ?x * ?y \<squnion> ?x * ?z

goal (1 subgoal):
 1. | x ] (d y * d z) = | x ] d y * | x ] d z
[PROOF STEP]
by auto


[STATEMENT]
lemma box_right_mult_a_d:
  "|x](a(y) * d(z)) = |x]a(y) * |x]d(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] (a y * d z) = | x ] a y * | x ] d z
[PROOF STEP]
by (metis box_right_mult_d_d a_d_closed)


[STATEMENT]
lemma box_right_mult_d_a:
  "|x](d(y) * a(z)) = |x]d(y) * |x]a(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] (d y * a z) = | x ] d y * | x ] a z
[PROOF STEP]
using box_right_mult_a_d box_def box_x_a d_def
[PROOF STATE]
proof (prove)
using this:
| ?x ] (a ?y * d ?z) = | ?x ] a ?y * | ?x ] d ?z
| ?x ] ?y = a (?x * a ?y)
| ?x ] a ?y = a (?x * ?y)
d ?x = a (a ?x)

goal (1 subgoal):
 1. | x ] (d y * a z) = | x ] d y * | x ] a z
[PROOF STEP]
by auto


[STATEMENT]
lemma box_right_mult_a_a:
  "|x](a(y) * a(z)) = |x]a(y) * |x]a(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] (a y * a z) = | x ] a y * | x ] a z
[PROOF STEP]
using a_dist_sup box_def mult_left_dist_sup tests_dual.sub_sup_demorgan
[PROOF STATE]
proof (prove)
using this:
a (?x \<squnion> ?y) = a ?x * a ?y
| ?x ] ?y = a (?x * a ?y)
?x * (?y \<squnion> ?z) = ?x * ?y \<squnion> ?x * ?z
a (a ?x * a ?y) = a (a ?x) \<squnion> a (a ?y)

goal (1 subgoal):
 1. | x ] (a y * a z) = | x ] a y * | x ] a z
[PROOF STEP]
by force


[STATEMENT]
lemma box_demodalisation_3:
  assumes "d(x) \<le> |y]d(z)"
    shows "d(x) * y \<le> y * d(z) \<squnion> Z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x * y \<le> y * d z \<squnion> Z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d x * y \<le> y * d z \<squnion> Z
[PROOF STEP]
have "d(x) * y * a(z) \<le> Z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x * y * a z \<le> Z
[PROOF STEP]
using assms a_greatest_left_absorber box_x_d d_def mult_assoc
[PROOF STATE]
proof (prove)
using this:
d x \<le> | y ] d z
(a ?x * ?y \<le> Z) = (a ?x \<le> a ?y)
| ?x ] d ?y = a (?x * a ?y)
d ?x = a (a ?x)
?a * ?b * ?c = ?a * (?b * ?c)

goal (1 subgoal):
 1. d x * y * a z \<le> Z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d x * y * a z \<le> Z

goal (1 subgoal):
 1. d x * y \<le> y * d z \<squnion> Z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
d x * y * a z \<le> Z

goal (1 subgoal):
 1. d x * y \<le> y * d z \<squnion> Z
[PROOF STEP]
by (simp add: a_a_below case_split_right_sup d_def sup_commute mult_assoc)
[PROOF STATE]
proof (state)
this:
d x * y \<le> y * d z \<squnion> Z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fbox_diff:
  "|x](d(y) \<squnion> a(z)) \<le> |x]y \<squnion> a( |x]z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] (d y \<squnion> a z) \<le> | x ] y \<squnion> a (| x ] z)
[PROOF STEP]
by (smt (z3) a_compl_intro a_dist_sup a_mult_d a_plus_left_lower_bound sup_commute box_def d_def mult_left_dist_sup tests_dual.sba_dual.shunting)


[STATEMENT]
lemma diamond_diff_var:
  "|x>d(y) \<le> |x>(d(y) * a(z)) \<squnion> |x>d(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > d y \<le> | x > (d y * a z) \<squnion> | x > d z
[PROOF STEP]
by (metis d_cancellation_1 diamond_right_dist_sup diamond_right_isotone sup_commute)


[STATEMENT]
lemma diamond_diff:
  "|x>y * a( |x>z) \<le> |x>(d(y) * a(z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > y * a (| x > z) \<le> | x > (d y * a z)
[PROOF STEP]
by (metis d_a_shunting d_involutive diamond_def diamond_diff_var diamond_x_und)


[STATEMENT]
lemma pre_sub_distr:
  "x\<guillemotleft>-p*-q \<le> (x\<guillemotleft>-p)*(x\<guillemotleft>-q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<guillemotleft> - p * - q \<le> (x \<guillemotleft> - p) * (x \<guillemotleft> - q)
[PROOF STEP]
by (smt (z3) pre_closed pre_lower_bound_right tests_dual.sub_commutative tests_dual.sub_sup_closed tests_dual.least_upper_bound)


[STATEMENT]
lemma pre_below_one:
  "x\<guillemotleft>-p \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<guillemotleft> - p \<le> (1::'a)
[PROOF STEP]
by (metis pre_closed tests_dual.sub_bot_least)


[STATEMENT]
lemma pre_lower_bound_left:
  "x\<guillemotleft>-p*-q \<le> x\<guillemotleft>-p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<guillemotleft> - p * - q \<le> x \<guillemotleft> - p
[PROOF STEP]
using pre_lower_bound_right tests_dual.sub_commutative
[PROOF STATE]
proof (prove)
using this:
?x \<guillemotleft> - ?p * - ?q \<le> ?x \<guillemotleft> - ?q
- ?x * - ?y = - ?y * - ?x

goal (1 subgoal):
 1. x \<guillemotleft> - p * - q \<le> x \<guillemotleft> - p
[PROOF STEP]
by fastforce


[STATEMENT]
lemma pre_iso:
  "-p \<le> -q \<Longrightarrow> x\<guillemotleft>-p \<le> x\<guillemotleft>-q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - p \<le> - q \<Longrightarrow> x \<guillemotleft> - p \<le> x \<guillemotleft> - q
[PROOF STEP]
by (metis leq_def pre_lower_bound_right)


[STATEMENT]
lemma pre_below_pre_one:
  "x\<guillemotleft>-p \<le> x\<guillemotleft>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<guillemotleft> - p \<le> x \<guillemotleft> (1::'a)
[PROOF STEP]
using tests_dual.sba_dual.one_def pre_iso tests_dual.sub_bot_least
[PROOF STATE]
proof (prove)
using this:
(1::'a) = - bot
- ?p \<le> - ?q \<Longrightarrow> ?x \<guillemotleft> - ?p \<le> ?x \<guillemotleft> - ?q
- ?x \<le> (1::'a)

goal (1 subgoal):
 1. x \<guillemotleft> - p \<le> x \<guillemotleft> (1::'a)
[PROOF STEP]
by blast


[STATEMENT]
lemma pre_seq_below_pre_one:
  "x*y\<guillemotleft>1 \<le> x\<guillemotleft>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y \<guillemotleft> (1::'a) \<le> x \<guillemotleft> (1::'a)
[PROOF STEP]
by (metis one_def pre_below_pre_one pre_closed pre_seq)


[STATEMENT]
lemma pre_compose:
  "-p \<le> x\<guillemotleft>-q \<Longrightarrow> -q \<le> y\<guillemotleft>-r \<Longrightarrow> -p \<le> x*y\<guillemotleft>-r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>- p \<le> x \<guillemotleft> - q; - q \<le> y \<guillemotleft> - r\<rbrakk> \<Longrightarrow> - p \<le> x * y \<guillemotleft> - r
[PROOF STEP]
by (metis pre_closed pre_iso tests_dual.transitive pre_seq)


[STATEMENT]
lemma pre_one:
  "1\<guillemotleft>-p = -p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) \<guillemotleft> - p = - p
[PROOF STEP]
by (metis pre_closed pre_test_test tests_dual.sba_dual.one_def tests_dual.sup_left_unit)


[STATEMENT]
lemma pre_import:
  "-p*(x\<guillemotleft>-q) = -p*(-p*x\<guillemotleft>-q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - p * (x \<guillemotleft> - q) = - p * (- p * x \<guillemotleft> - q)
[PROOF STEP]
by (metis pre_closed pre_seq pre_test_test)


[STATEMENT]
lemma pre_import_composition:
  "-p*(-p*x*y\<guillemotleft>-q) = -p*(x\<guillemotleft>y\<guillemotleft>-q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - p * (- p * x * y \<guillemotleft> - q) = - p * (x \<guillemotleft> y \<guillemotleft> - q)
[PROOF STEP]
by (metis pre_closed pre_seq pre_import)


[STATEMENT]
lemma pre_import_equiv:
  "-p \<le> x\<guillemotleft>-q \<longleftrightarrow> -p \<le> -p*x\<guillemotleft>-q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- p \<le> x \<guillemotleft> - q) = (- p \<le> - p * x \<guillemotleft> - q)
[PROOF STEP]
by (metis leq_def pre_closed pre_import)


[STATEMENT]
lemma pre_import_equiv_mult:
  "-p*-q \<le> x\<guillemotleft>-s \<longleftrightarrow> -p*-q \<le> -q*x\<guillemotleft>-s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- p * - q \<le> x \<guillemotleft> - s) = (- p * - q \<le> - q * x \<guillemotleft> - s)
[PROOF STEP]
by (smt leq_def pre_closed sub_assoc sub_mult_closed pre_import)


[STATEMENT]
lemma pre_mult_test_promote:
  "x*-p\<guillemotleft>-q = x*-p\<guillemotleft>-p*-q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * - p \<guillemotleft> - q = x * - p \<guillemotleft> - p * - q
[PROOF STEP]
by (metis pre_seq pre_test_promote sub_mult_closed)


[STATEMENT]
lemma pre_test_neg:
  "--p*(-p\<guillemotleft>-q) = --p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - - p * (- p \<guillemotleft> - q) = - - p
[PROOF STEP]
by (simp add: pre_test)


[STATEMENT]
lemma pre_bot:
  "bot\<guillemotleft>-q = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bot \<guillemotleft> - q = (1::'a)
[PROOF STEP]
by (metis pre_test tests_dual.sba_dual.one_def tests_dual.sba_dual.sup_left_zero tests_dual.top_double_complement)


[STATEMENT]
lemma pre_export:
  "-p*x\<guillemotleft>-q = --p\<squnion>(x\<guillemotleft>-q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - p * x \<guillemotleft> - q = - - p \<squnion> (x \<guillemotleft> - q)
[PROOF STEP]
by (metis pre_closed pre_seq pre_test)


[STATEMENT]
lemma pre_neg_mult:
  "--p \<le> -p*x\<guillemotleft>-q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - - p \<le> - p * x \<guillemotleft> - q
[PROOF STEP]
by (metis leq_def pre_closed pre_seq pre_test_neg)


[STATEMENT]
lemma pre_test_test_same:
  "-p\<guillemotleft>-p = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - p \<guillemotleft> - p = (1::'a)
[PROOF STEP]
using pre_test tests_dual.sba_dual.less_eq_sup_top tests_dual.sba_dual.reflexive
[PROOF STATE]
proof (prove)
using this:
- ?p \<guillemotleft> - ?q = - - ?p \<squnion> - ?q
(- ?x \<le> - ?y) = (- - ?x \<squnion> - ?y = (1::'a))
- ?x \<le> - ?x

goal (1 subgoal):
 1. - p \<guillemotleft> - p = (1::'a)
[PROOF STEP]
by auto


[STATEMENT]
lemma test_below_pre_test_mult:
  "-q \<le> -p\<guillemotleft>-p*-q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - q \<le> - p \<guillemotleft> - p * - q
[PROOF STEP]
by (metis pre_test tests_dual.sba_dual.reflexive tests_dual.sba_dual.shunting tests_dual.sub_sup_closed)


[STATEMENT]
lemma test_below_pre_test:
  "-q \<le> -p\<guillemotleft>-q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - q \<le> - p \<guillemotleft> - q
[PROOF STEP]
by (simp add: pre_test tests_dual.sba_dual.upper_bound_right)


[STATEMENT]
lemma test_below_pre_test_2:
  "--p \<le> -p\<guillemotleft>-q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - - p \<le> - p \<guillemotleft> - q
[PROOF STEP]
by (simp add: pre_test tests_dual.sba_dual.upper_bound_left)


[STATEMENT]
lemma pre_test_bot:
  "-p\<guillemotleft>bot = --p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - p \<guillemotleft> bot = - - p
[PROOF STEP]
by (metis pre_test tests_dual.sba_dual.sup_right_unit tests_dual.top_double_complement)


[STATEMENT]
lemma pre_test_one:
  "-p\<guillemotleft>1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - p \<guillemotleft> (1::'a) = (1::'a)
[PROOF STEP]
by (metis pre_seq pre_bot tests_dual.sup_right_zero)


[STATEMENT]
lemma pre_test_neg:
  "--p*(-p\<guillemotleft>-q) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - - p * (- p \<guillemotleft> - q) = bot
[PROOF STEP]
by (simp add: pre_test tests_dual.sub_associative tests_dual.sub_commutative)


[STATEMENT]
lemma pre_bot:
  "bot\<guillemotleft>-q = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bot \<guillemotleft> - q = bot
[PROOF STEP]
by (metis pre_test tests_dual.sup_left_zero tests_dual.top_double_complement)


[STATEMENT]
lemma pre_export:
  "-p*x\<guillemotleft>-q = -p*(x\<guillemotleft>-q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - p * x \<guillemotleft> - q = - p * (x \<guillemotleft> - q)
[PROOF STEP]
by (metis pre_closed pre_seq pre_test)


[STATEMENT]
lemma pre_neg_mult:
  "-p*x\<guillemotleft>-q \<le> -p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - p * x \<guillemotleft> - q \<le> - p
[PROOF STEP]
by (metis pre_closed pre_export tests_dual.upper_bound_left)


[STATEMENT]
lemma pre_test_test_same:
  "-p\<guillemotleft>-p = -p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - p \<guillemotleft> - p = - p
[PROOF STEP]
by (simp add: pre_test)


[STATEMENT]
lemma test_above_pre_test_plus:
  "--p\<guillemotleft>-p\<squnion>-q \<le> -q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - - p \<guillemotleft> - p \<squnion> - q \<le> - q
[PROOF STEP]
using pre_test tests_dual.sba_dual.inf_complement_intro tests_dual.sub_commutative tests_dual.sub_inf_def tests_dual.upper_bound_left
[PROOF STATE]
proof (prove)
using this:
- ?p \<guillemotleft> - ?q = - ?p * - ?q
(- ?x \<squnion> - ?y) * - - ?x = - ?y * - - ?x
- ?x * - ?y = - ?y * - ?x
- ?x \<squnion> - ?y = - (- - ?x * - - ?y)
- ?x * - ?y \<le> - ?x

goal (1 subgoal):
 1. - - p \<guillemotleft> - p \<squnion> - q \<le> - q
[PROOF STEP]
by auto


[STATEMENT]
lemma test_above_pre_test:
  "-p\<guillemotleft>-q \<le> -q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - p \<guillemotleft> - q \<le> - q
[PROOF STEP]
by (simp add: pre_test tests_dual.upper_bound_right)


[STATEMENT]
lemma test_above_pre_test_2:
  "-p\<guillemotleft>-q \<le> -p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - p \<guillemotleft> - q \<le> - p
[PROOF STEP]
by (simp add: pre_test tests_dual.upper_bound_left)


[STATEMENT]
lemma pre_test_bot:
  "-p\<guillemotleft>bot = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - p \<guillemotleft> bot = bot
[PROOF STEP]
by (metis pre_test tests_dual.sup_right_zero tests_dual.top_double_complement)


[STATEMENT]
lemma pre_test_one:
  "-p\<guillemotleft>1 = -p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - p \<guillemotleft> (1::'a) = - p
[PROOF STEP]
by (metis pre_test tests_dual.complement_top tests_dual.sup_right_unit)


[STATEMENT]
lemma mon_pl_empty[simp]: "mon_pl [] = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mon_pl [] = {}
[PROOF STEP]
by (unfold mon_pl_def, auto)


[STATEMENT]
lemma mon_pl_cons[simp]: "mon_pl (e#w) = fst e \<union> snd e \<union> mon_pl w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mon_pl (e # w) = fst e \<union> snd e \<union> mon_pl w
[PROOF STEP]
by (unfold mon_pl_def) (simp, subst foldl_un_empty_eq, auto)


[STATEMENT]
lemma mon_pl_unconc: "!!b. mon_pl (a@b) = mon_pl a \<union> mon_pl b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. mon_pl (a @ b) = mon_pl a \<union> mon_pl b
[PROOF STEP]
by (induct a) auto


[STATEMENT]
lemma mon_pl_ileq: "w\<preceq>w' \<Longrightarrow> mon_pl w \<subseteq> mon_pl w'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<preceq> w' \<Longrightarrow> mon_pl w \<subseteq> mon_pl w'
[PROOF STEP]
by (induct rule: less_eq_list_induct) auto


[STATEMENT]
lemma mon_pl_set: "mon_pl w = \<Union>{ fst e \<union> snd e | e. e\<in>set w }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mon_pl w = \<Union> {fst e \<union> snd e |e. e \<in> set w}
[PROOF STEP]
by (auto simp add: mon_pl_def foldl_set) blast+


[STATEMENT]
lemma cil_last_case_split[cases set, case_names left right]: "
  \<lbrakk> w\<in>e1#w1 \<otimes>\<^bsub>\<alpha>\<^esub> e2#w2;
    !!w'. \<lbrakk>w=e1#w'; w'\<in>(w1 \<otimes>\<^bsub>\<alpha>\<^esub> e2#w2);
           fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2#w2)) = {} \<rbrakk> \<Longrightarrow> P;
    !!w'. \<lbrakk>w=e2#w'; w'\<in>(e1#w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2);
           fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1#w1)) = {} \<rbrakk> \<Longrightarrow> P
  \<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; \<And>w'. \<lbrakk>w = e1 # w'; w' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}\<rbrakk> \<Longrightarrow> P; \<And>w'. \<lbrakk>w = e2 # w'; w' \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2; fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (auto elim: list_set_cons_cases split: if_split_asm)


[STATEMENT]
lemma cil_cases[cases set, case_names both_empty left_empty right_empty app_left app_right]: "
  \<lbrakk> w\<in>wa\<otimes>\<^bsub>\<alpha>\<^esub>wb;
    \<lbrakk> w=[]; wa=[]; wb=[] \<rbrakk> \<Longrightarrow> P;
    \<lbrakk>wa=[]; w=wb\<rbrakk> \<Longrightarrow> P;
    \<lbrakk> w=wa; wb=[] \<rbrakk> \<Longrightarrow> P;
    !!ea wa' w'. \<lbrakk>w=ea#w'; wa=ea#wa'; w'\<in>wa'\<otimes>\<^bsub>\<alpha>\<^esub>wb;
                  fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> wb) = {}  \<rbrakk> \<Longrightarrow> P;
    !!eb wb' w'. \<lbrakk>w=eb#w'; wb=eb#wb'; w'\<in>wa\<otimes>\<^bsub>\<alpha>\<^esub>wb';
                  fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> wa) = {}  \<rbrakk> \<Longrightarrow> P
  \<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w \<in> wa \<otimes>\<^bsub>\<alpha>\<^esub> wb; \<lbrakk>w = []; wa = []; wb = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>wa = []; w = wb\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = wa; wb = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; wa = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> wb; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> wb) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; wb = eb # wb'; w' \<in> wa \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> wa) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
proof (induct wa \<alpha> wb rule: cil.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>\<alpha> wa. \<lbrakk>w \<in> [] \<otimes>\<^bsub>\<alpha>\<^esub> wa; \<lbrakk>w = []; [] = []; wa = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>[] = []; w = wa\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = []; wa = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; [] = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> wa; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> wa) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; wa = eb # wb'; w' \<in> [] \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> []) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 2. \<And>v va \<alpha>. \<lbrakk>w \<in> v # va \<otimes>\<^bsub>\<alpha>\<^esub> []; \<lbrakk>w = []; v # va = []; [] = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>v # va = []; w = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = v # va; [] = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; v # va = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> []; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> []) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; [] = eb # wb'; w' \<in> v # va \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (v # va)) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 3. \<And>e1 w1 \<alpha> e2 w2. \<lbrakk>\<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}; w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; \<lbrakk>w = []; w1 = []; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>w1 = []; w = e2 # w2\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = w1; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; w1 = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; e2 # w2 = eb # wb'; w' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> w1) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<lbrakk>fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}; w \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2; \<lbrakk>w = []; e1 # w1 = []; w2 = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>e1 # w1 = []; w = w2\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = e1 # w1; w2 = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; e1 # w1 = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> w2; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> w2) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; w2 = eb # wb'; w' \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; w \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; \<lbrakk>w = []; e1 # w1 = []; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>e1 # w1 = []; w = e2 # w2\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = e1 # w1; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; e1 # w1 = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; e2 # w2 = eb # wb'; w' \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
w \<in> [] \<otimes>\<^bsub>\<alpha>_\<^esub> w_
\<lbrakk>w = []; [] = []; w_ = []\<rbrakk> \<Longrightarrow> P
\<lbrakk>[] = []; w = w_\<rbrakk> \<Longrightarrow> P
\<lbrakk>w = []; w_ = []\<rbrakk> \<Longrightarrow> P
\<lbrakk>w = ?ea # ?w'; [] = ?ea # ?wa'; ?w' \<in> ?wa' \<otimes>\<^bsub>\<alpha>_\<^esub> w_; fst (\<alpha>_ ?ea) \<inter> mon_pl (map \<alpha>_ w_) = {}\<rbrakk> \<Longrightarrow> P
\<lbrakk>w = ?eb # ?w'; w_ = ?eb # ?wb'; ?w' \<in> [] \<otimes>\<^bsub>\<alpha>_\<^esub> ?wb'; fst (\<alpha>_ ?eb) \<inter> mon_pl (map \<alpha>_ []) = {}\<rbrakk> \<Longrightarrow> P

goal (3 subgoals):
 1. \<And>\<alpha> wa. \<lbrakk>w \<in> [] \<otimes>\<^bsub>\<alpha>\<^esub> wa; \<lbrakk>w = []; [] = []; wa = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>[] = []; w = wa\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = []; wa = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; [] = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> wa; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> wa) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; wa = eb # wb'; w' \<in> [] \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> []) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 2. \<And>v va \<alpha>. \<lbrakk>w \<in> v # va \<otimes>\<^bsub>\<alpha>\<^esub> []; \<lbrakk>w = []; v # va = []; [] = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>v # va = []; w = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = v # va; [] = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; v # va = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> []; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> []) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; [] = eb # wb'; w' \<in> v # va \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (v # va)) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 3. \<And>e1 w1 \<alpha> e2 w2. \<lbrakk>\<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}; w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; \<lbrakk>w = []; w1 = []; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>w1 = []; w = e2 # w2\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = w1; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; w1 = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; e2 # w2 = eb # wb'; w' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> w1) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<lbrakk>fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}; w \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2; \<lbrakk>w = []; e1 # w1 = []; w2 = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>e1 # w1 = []; w = w2\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = e1 # w1; w2 = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; e1 # w1 = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> w2; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> w2) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; w2 = eb # wb'; w' \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; w \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; \<lbrakk>w = []; e1 # w1 = []; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>e1 # w1 = []; w = e2 # w2\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = e1 # w1; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; e1 # w1 = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; e2 # w2 = eb # wb'; w' \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
w \<in> [] \<otimes>\<^bsub>\<alpha>_\<^esub> w_
\<lbrakk>w = []; [] = []; w_ = []\<rbrakk> \<Longrightarrow> P
\<lbrakk>[] = []; w = w_\<rbrakk> \<Longrightarrow> P
\<lbrakk>w = []; w_ = []\<rbrakk> \<Longrightarrow> P
\<lbrakk>w = ?ea # ?w'; [] = ?ea # ?wa'; ?w' \<in> ?wa' \<otimes>\<^bsub>\<alpha>_\<^esub> w_; fst (\<alpha>_ ?ea) \<inter> mon_pl (map \<alpha>_ w_) = {}\<rbrakk> \<Longrightarrow> P
\<lbrakk>w = ?eb # ?w'; w_ = ?eb # ?wb'; ?w' \<in> [] \<otimes>\<^bsub>\<alpha>_\<^esub> ?wb'; fst (\<alpha>_ ?eb) \<inter> mon_pl (map \<alpha>_ []) = {}\<rbrakk> \<Longrightarrow> P

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

goal (2 subgoals):
 1. \<And>v va \<alpha>. \<lbrakk>w \<in> v # va \<otimes>\<^bsub>\<alpha>\<^esub> []; \<lbrakk>w = []; v # va = []; [] = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>v # va = []; w = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = v # va; [] = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; v # va = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> []; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> []) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; [] = eb # wb'; w' \<in> v # va \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (v # va)) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 2. \<And>e1 w1 \<alpha> e2 w2. \<lbrakk>\<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}; w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; \<lbrakk>w = []; w1 = []; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>w1 = []; w = e2 # w2\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = w1; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; w1 = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; e2 # w2 = eb # wb'; w' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> w1) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<lbrakk>fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}; w \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2; \<lbrakk>w = []; e1 # w1 = []; w2 = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>e1 # w1 = []; w = w2\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = e1 # w1; w2 = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; e1 # w1 = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> w2; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> w2) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; w2 = eb # wb'; w' \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; w \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; \<lbrakk>w = []; e1 # w1 = []; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>e1 # w1 = []; w = e2 # w2\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = e1 # w1; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; e1 # w1 = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; e2 # w2 = eb # wb'; w' \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v va \<alpha>. \<lbrakk>w \<in> v # va \<otimes>\<^bsub>\<alpha>\<^esub> []; \<lbrakk>w = []; v # va = []; [] = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>v # va = []; w = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = v # va; [] = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; v # va = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> []; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> []) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; [] = eb # wb'; w' \<in> v # va \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (v # va)) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 2. \<And>e1 w1 \<alpha> e2 w2. \<lbrakk>\<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}; w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; \<lbrakk>w = []; w1 = []; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>w1 = []; w = e2 # w2\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = w1; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; w1 = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; e2 # w2 = eb # wb'; w' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> w1) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<lbrakk>fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}; w \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2; \<lbrakk>w = []; e1 # w1 = []; w2 = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>e1 # w1 = []; w = w2\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = e1 # w1; w2 = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; e1 # w1 = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> w2; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> w2) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; w2 = eb # wb'; w' \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; w \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; \<lbrakk>w = []; e1 # w1 = []; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>e1 # w1 = []; w = e2 # w2\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = e1 # w1; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; e1 # w1 = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; e2 # w2 = eb # wb'; w' \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
w \<in> v_ # va_ \<otimes>\<^bsub>\<alpha>_\<^esub> []
\<lbrakk>w = []; v_ # va_ = []; [] = []\<rbrakk> \<Longrightarrow> P
\<lbrakk>v_ # va_ = []; w = []\<rbrakk> \<Longrightarrow> P
\<lbrakk>w = v_ # va_; [] = []\<rbrakk> \<Longrightarrow> P
\<lbrakk>w = ?ea # ?w'; v_ # va_ = ?ea # ?wa'; ?w' \<in> ?wa' \<otimes>\<^bsub>\<alpha>_\<^esub> []; fst (\<alpha>_ ?ea) \<inter> mon_pl (map \<alpha>_ []) = {}\<rbrakk> \<Longrightarrow> P
\<lbrakk>w = ?eb # ?w'; [] = ?eb # ?wb'; ?w' \<in> v_ # va_ \<otimes>\<^bsub>\<alpha>_\<^esub> ?wb'; fst (\<alpha>_ ?eb) \<inter> mon_pl (map \<alpha>_ (v_ # va_)) = {}\<rbrakk> \<Longrightarrow> P

goal (2 subgoals):
 1. \<And>v va \<alpha>. \<lbrakk>w \<in> v # va \<otimes>\<^bsub>\<alpha>\<^esub> []; \<lbrakk>w = []; v # va = []; [] = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>v # va = []; w = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = v # va; [] = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; v # va = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> []; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> []) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; [] = eb # wb'; w' \<in> v # va \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (v # va)) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 2. \<And>e1 w1 \<alpha> e2 w2. \<lbrakk>\<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}; w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; \<lbrakk>w = []; w1 = []; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>w1 = []; w = e2 # w2\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = w1; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; w1 = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; e2 # w2 = eb # wb'; w' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> w1) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<lbrakk>fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}; w \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2; \<lbrakk>w = []; e1 # w1 = []; w2 = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>e1 # w1 = []; w = w2\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = e1 # w1; w2 = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; e1 # w1 = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> w2; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> w2) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; w2 = eb # wb'; w' \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; w \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; \<lbrakk>w = []; e1 # w1 = []; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>e1 # w1 = []; w = e2 # w2\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = e1 # w1; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; e1 # w1 = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; e2 # w2 = eb # wb'; w' \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
w \<in> v_ # va_ \<otimes>\<^bsub>\<alpha>_\<^esub> []
\<lbrakk>w = []; v_ # va_ = []; [] = []\<rbrakk> \<Longrightarrow> P
\<lbrakk>v_ # va_ = []; w = []\<rbrakk> \<Longrightarrow> P
\<lbrakk>w = v_ # va_; [] = []\<rbrakk> \<Longrightarrow> P
\<lbrakk>w = ?ea # ?w'; v_ # va_ = ?ea # ?wa'; ?w' \<in> ?wa' \<otimes>\<^bsub>\<alpha>_\<^esub> []; fst (\<alpha>_ ?ea) \<inter> mon_pl (map \<alpha>_ []) = {}\<rbrakk> \<Longrightarrow> P
\<lbrakk>w = ?eb # ?w'; [] = ?eb # ?wb'; ?w' \<in> v_ # va_ \<otimes>\<^bsub>\<alpha>_\<^esub> ?wb'; fst (\<alpha>_ ?eb) \<inter> mon_pl (map \<alpha>_ (v_ # va_)) = {}\<rbrakk> \<Longrightarrow> P

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

goal (1 subgoal):
 1. \<And>e1 w1 \<alpha> e2 w2. \<lbrakk>\<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}; w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; \<lbrakk>w = []; w1 = []; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>w1 = []; w = e2 # w2\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = w1; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; w1 = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; e2 # w2 = eb # wb'; w' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> w1) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<lbrakk>fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}; w \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2; \<lbrakk>w = []; e1 # w1 = []; w2 = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>e1 # w1 = []; w = w2\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = e1 # w1; w2 = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; e1 # w1 = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> w2; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> w2) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; w2 = eb # wb'; w' \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; w \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; \<lbrakk>w = []; e1 # w1 = []; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>e1 # w1 = []; w = e2 # w2\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = e1 # w1; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; e1 # w1 = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; e2 # w2 = eb # wb'; w' \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e1 w1 \<alpha> e2 w2. \<lbrakk>\<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}; w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; \<lbrakk>w = []; w1 = []; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>w1 = []; w = e2 # w2\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = w1; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; w1 = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; e2 # w2 = eb # wb'; w' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> w1) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<lbrakk>fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}; w \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2; \<lbrakk>w = []; e1 # w1 = []; w2 = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>e1 # w1 = []; w = w2\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = e1 # w1; w2 = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; e1 # w1 = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> w2; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> w2) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; w2 = eb # wb'; w' \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; w \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; \<lbrakk>w = []; e1 # w1 = []; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>e1 # w1 = []; w = e2 # w2\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = e1 # w1; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; e1 # w1 = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; e2 # w2 = eb # wb'; w' \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
case (3 ea wa' \<alpha> eb wb')
[PROOF STATE]
proof (state)
this:
\<lbrakk>fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> (eb # wb')) = {}; w \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> eb # wb'; \<lbrakk>w = []; wa' = []; eb # wb' = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>wa' = []; w = eb # wb'\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = wa'; eb # wb' = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa'a w'. \<lbrakk>w = ea # w'; wa' = ea # wa'a; w' \<in> wa'a \<otimes>\<^bsub>\<alpha>\<^esub> eb # wb'; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> (eb # wb')) = {}\<rbrakk> \<Longrightarrow> P; \<And>eba wb'a w'. \<lbrakk>w = eba # w'; eb # wb' = eba # wb'a; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> wb'a; fst (\<alpha> eba) \<inter> mon_pl (map \<alpha> wa') = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
\<lbrakk>fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (ea # wa')) = {}; w \<in> ea # wa' \<otimes>\<^bsub>\<alpha>\<^esub> wb'; \<lbrakk>w = []; ea # wa' = []; wb' = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>ea # wa' = []; w = wb'\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = ea # wa'; wb' = []\<rbrakk> \<Longrightarrow> P; \<And>eaa wa'a w'. \<lbrakk>w = eaa # w'; ea # wa' = eaa # wa'a; w' \<in> wa'a \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eaa) \<inter> mon_pl (map \<alpha> wb') = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb'a w'. \<lbrakk>w = eb # w'; wb' = eb # wb'a; w' \<in> ea # wa' \<otimes>\<^bsub>\<alpha>\<^esub> wb'a; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (ea # wa')) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
w \<in> ea # wa' \<otimes>\<^bsub>\<alpha>\<^esub> eb # wb'
\<lbrakk>w = []; ea # wa' = []; eb # wb' = []\<rbrakk> \<Longrightarrow> P
\<lbrakk>ea # wa' = []; w = eb # wb'\<rbrakk> \<Longrightarrow> P
\<lbrakk>w = ea # wa'; eb # wb' = []\<rbrakk> \<Longrightarrow> P
\<lbrakk>w = ?ea # ?w'; ea # wa' = ?ea # ?wa'; ?w' \<in> ?wa' \<otimes>\<^bsub>\<alpha>\<^esub> eb # wb'; fst (\<alpha> ?ea) \<inter> mon_pl (map \<alpha> (eb # wb')) = {}\<rbrakk> \<Longrightarrow> P
\<lbrakk>w = ?eb # ?w'; eb # wb' = ?eb # ?wb'; ?w' \<in> ea # wa' \<otimes>\<^bsub>\<alpha>\<^esub> ?wb'; fst (\<alpha> ?eb) \<inter> mon_pl (map \<alpha> (ea # wa')) = {}\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. \<And>e1 w1 \<alpha> e2 w2. \<lbrakk>\<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}; w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; \<lbrakk>w = []; w1 = []; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>w1 = []; w = e2 # w2\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = w1; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; w1 = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; e2 # w2 = eb # wb'; w' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> w1) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<lbrakk>fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}; w \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2; \<lbrakk>w = []; e1 # w1 = []; w2 = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>e1 # w1 = []; w = w2\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = e1 # w1; w2 = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; e1 # w1 = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> w2; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> w2) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; w2 = eb # wb'; w' \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; w \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; \<lbrakk>w = []; e1 # w1 = []; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<lbrakk>e1 # w1 = []; w = e2 # w2\<rbrakk> \<Longrightarrow> P; \<lbrakk>w = e1 # w1; e2 # w2 = []\<rbrakk> \<Longrightarrow> P; \<And>ea wa' w'. \<lbrakk>w = ea # w'; e1 # w1 = ea # wa'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> e2 # w2; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}\<rbrakk> \<Longrightarrow> P; \<And>eb wb' w'. \<lbrakk>w = eb # w'; e2 # w2 = eb # wb'; w' \<in> e1 # w1 \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
from "3.prems"(1)
[PROOF STATE]
proof (chain)
picking this:
w \<in> ea # wa' \<otimes>\<^bsub>\<alpha>\<^esub> eb # wb'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
w \<in> ea # wa' \<otimes>\<^bsub>\<alpha>\<^esub> eb # wb'

goal (1 subgoal):
 1. P
[PROOF STEP]
proof (cases rule: cil_last_case_split)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>w'. \<lbrakk>w = ea # w'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> eb # wb'; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> (eb # wb')) = {}\<rbrakk> \<Longrightarrow> P
 2. \<And>w'. \<lbrakk>w = eb # w'; w' \<in> ea # wa' \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (ea # wa')) = {}\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
case (left w')
[PROOF STATE]
proof (state)
this:
w = ea # w'
w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> eb # wb'
fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> (eb # wb')) = {}

goal (2 subgoals):
 1. \<And>w'. \<lbrakk>w = ea # w'; w' \<in> wa' \<otimes>\<^bsub>\<alpha>\<^esub> eb # wb'; fst (\<alpha> ea) \<inter> mon_pl (map \<alpha> (eb # wb')) = {}\<rbrakk> \<Longrightarrow> P
 2. \<And>w'. \<lbrakk>w = eb # w'; w' \<in> ea # wa' \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (ea # wa')) = {}\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
from "3.prems"(5)[OF left(1) _ left(2,3)]
[PROOF STATE]
proof (chain)
picking this:
ea # wa' = ea # wa' \<Longrightarrow> P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ea # wa' = ea # wa' \<Longrightarrow> P

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

goal (1 subgoal):
 1. \<And>w'. \<lbrakk>w = eb # w'; w' \<in> ea # wa' \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (ea # wa')) = {}\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w'. \<lbrakk>w = eb # w'; w' \<in> ea # wa' \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (ea # wa')) = {}\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
case (right w')
[PROOF STATE]
proof (state)
this:
w = eb # w'
w' \<in> ea # wa' \<otimes>\<^bsub>\<alpha>\<^esub> wb'
fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (ea # wa')) = {}

goal (1 subgoal):
 1. \<And>w'. \<lbrakk>w = eb # w'; w' \<in> ea # wa' \<otimes>\<^bsub>\<alpha>\<^esub> wb'; fst (\<alpha> eb) \<inter> mon_pl (map \<alpha> (ea # wa')) = {}\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
from "3.prems"(6)[OF right(1) _ right(2,3)]
[PROOF STATE]
proof (chain)
picking this:
eb # wb' = eb # wb' \<Longrightarrow> P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eb # wb' = eb # wb' \<Longrightarrow> P

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cil_induct'[case_names both_empty left_empty right_empty append]: "\<lbrakk>
  \<And>\<alpha>. P \<alpha> [] [];
  \<And>\<alpha> ad ae. P \<alpha> [] (ad # ae);
  \<And>\<alpha> z aa. P \<alpha> (z # aa) [];
  \<And>\<alpha> e1 w1 e2 w2. \<lbrakk>
    \<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}\<rbrakk> \<Longrightarrow> P \<alpha> w1 (e2 # w2);
    \<lbrakk>fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) w2\<rbrakk>
  \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)
  \<rbrakk> \<Longrightarrow> P \<alpha> wa wb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>\<alpha>. P \<alpha> [] []; \<And>\<alpha> ad ae. P \<alpha> [] (ad # ae); \<And>\<alpha> z aa. P \<alpha> (z # aa) []; \<And>\<alpha> e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<Longrightarrow> P \<alpha> w1 (e2 # w2); fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<Longrightarrow> P \<alpha> (e1 # w1) w2\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> wa wb
[PROOF STEP]
apply (induct wa \<alpha> wb rule: cil.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>\<alpha> w. \<lbrakk>\<And>\<alpha>. P \<alpha> [] []; \<And>\<alpha> ad ae. P \<alpha> [] (ad # ae); \<And>\<alpha> z aa. P \<alpha> (z # aa) []; \<And>\<alpha> e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<Longrightarrow> P \<alpha> w1 (e2 # w2); fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<Longrightarrow> P \<alpha> (e1 # w1) w2\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> [] w
 2. \<And>v va \<alpha>. \<lbrakk>\<And>\<alpha>. P \<alpha> [] []; \<And>\<alpha> ad ae. P \<alpha> [] (ad # ae); \<And>\<alpha> z aa. P \<alpha> (z # aa) []; \<And>\<alpha> e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<Longrightarrow> P \<alpha> w1 (e2 # w2); fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<Longrightarrow> P \<alpha> (e1 # w1) w2\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (v # va) []
 3. \<And>e1 w1 \<alpha> e2 w2. \<lbrakk>\<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}; \<And>\<alpha>. P \<alpha> [] []; \<And>\<alpha> ad ae. P \<alpha> [] (ad # ae); \<And>\<alpha> z aa. P \<alpha> (z # aa) []; \<And>\<alpha> e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<Longrightarrow> P \<alpha> w1 (e2 # w2); fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<Longrightarrow> P \<alpha> (e1 # w1) w2\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> w1 (e2 # w2); \<lbrakk>fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}; \<And>\<alpha>. P \<alpha> [] []; \<And>\<alpha> ad ae. P \<alpha> [] (ad # ae); \<And>\<alpha> z aa. P \<alpha> (z # aa) []; \<And>\<alpha> e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<Longrightarrow> P \<alpha> w1 (e2 # w2); fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<Longrightarrow> P \<alpha> (e1 # w1) w2\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) w2; \<And>\<alpha>. P \<alpha> [] []; \<And>\<alpha> ad ae. P \<alpha> [] (ad # ae); \<And>\<alpha> z aa. P \<alpha> (z # aa) []; \<And>\<alpha> e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<Longrightarrow> P \<alpha> w1 (e2 # w2); fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<Longrightarrow> P \<alpha> (e1 # w1) w2\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)
[PROOF STEP]
apply (case_tac w)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>\<alpha> w. \<lbrakk>\<And>\<alpha>. P \<alpha> [] []; \<And>\<alpha> ad ae. P \<alpha> [] (ad # ae); \<And>\<alpha> z aa. P \<alpha> (z # aa) []; \<And>\<alpha> e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<Longrightarrow> P \<alpha> w1 (e2 # w2); fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<Longrightarrow> P \<alpha> (e1 # w1) w2\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2); w = []\<rbrakk> \<Longrightarrow> P \<alpha> [] w
 2. \<And>\<alpha> w a list. \<lbrakk>\<And>\<alpha>. P \<alpha> [] []; \<And>\<alpha> ad ae. P \<alpha> [] (ad # ae); \<And>\<alpha> z aa. P \<alpha> (z # aa) []; \<And>\<alpha> e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<Longrightarrow> P \<alpha> w1 (e2 # w2); fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<Longrightarrow> P \<alpha> (e1 # w1) w2\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2); w = a # list\<rbrakk> \<Longrightarrow> P \<alpha> [] w
 3. \<And>v va \<alpha>. \<lbrakk>\<And>\<alpha>. P \<alpha> [] []; \<And>\<alpha> ad ae. P \<alpha> [] (ad # ae); \<And>\<alpha> z aa. P \<alpha> (z # aa) []; \<And>\<alpha> e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<Longrightarrow> P \<alpha> w1 (e2 # w2); fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<Longrightarrow> P \<alpha> (e1 # w1) w2\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (v # va) []
 4. \<And>e1 w1 \<alpha> e2 w2. \<lbrakk>\<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}; \<And>\<alpha>. P \<alpha> [] []; \<And>\<alpha> ad ae. P \<alpha> [] (ad # ae); \<And>\<alpha> z aa. P \<alpha> (z # aa) []; \<And>\<alpha> e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<Longrightarrow> P \<alpha> w1 (e2 # w2); fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<Longrightarrow> P \<alpha> (e1 # w1) w2\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> w1 (e2 # w2); \<lbrakk>fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}; \<And>\<alpha>. P \<alpha> [] []; \<And>\<alpha> ad ae. P \<alpha> [] (ad # ae); \<And>\<alpha> z aa. P \<alpha> (z # aa) []; \<And>\<alpha> e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<Longrightarrow> P \<alpha> w1 (e2 # w2); fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<Longrightarrow> P \<alpha> (e1 # w1) w2\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) w2; \<And>\<alpha>. P \<alpha> [] []; \<And>\<alpha> ad ae. P \<alpha> [] (ad # ae); \<And>\<alpha> z aa. P \<alpha> (z # aa) []; \<And>\<alpha> e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<Longrightarrow> P \<alpha> w1 (e2 # w2); fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<Longrightarrow> P \<alpha> (e1 # w1) w2\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma cil_induct_fix\<alpha>: "\<lbrakk>
  P \<alpha> [] [];
  \<And>ad ae. P \<alpha> [] (ad # ae);
  \<And>z aa. P \<alpha> (z # aa) [];
  \<And>e1 w1 e2 w2.
    \<lbrakk>fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<longrightarrow> P \<alpha> (e1 # w1) w2;
     fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<longrightarrow> P \<alpha> w1 (e2 # w2)\<rbrakk>
     \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk>
  \<Longrightarrow> P \<alpha> v w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<alpha> [] []; \<And>ad ae. P \<alpha> [] (ad # ae); \<And>z aa. P \<alpha> (z # aa) []; \<And>e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<longrightarrow> P \<alpha> (e1 # w1) w2; fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<longrightarrow> P \<alpha> w1 (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> v w
[PROOF STEP]
apply (induct v \<alpha> w rule: cil.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>\<alpha> w. \<lbrakk>P \<alpha> [] []; \<And>ad ae. P \<alpha> [] (ad # ae); \<And>z aa. P \<alpha> (z # aa) []; \<And>e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<longrightarrow> P \<alpha> (e1 # w1) w2; fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<longrightarrow> P \<alpha> w1 (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> [] w
 2. \<And>v va \<alpha>. \<lbrakk>P \<alpha> [] []; \<And>ad ae. P \<alpha> [] (ad # ae); \<And>z aa. P \<alpha> (z # aa) []; \<And>e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<longrightarrow> P \<alpha> (e1 # w1) w2; fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<longrightarrow> P \<alpha> w1 (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (v # va) []
 3. \<And>e1 w1 \<alpha> e2 w2. \<lbrakk>\<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}; P \<alpha> [] []; \<And>ad ae. P \<alpha> [] (ad # ae); \<And>z aa. P \<alpha> (z # aa) []; \<And>e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<longrightarrow> P \<alpha> (e1 # w1) w2; fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<longrightarrow> P \<alpha> w1 (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> w1 (e2 # w2); \<lbrakk>fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}; P \<alpha> [] []; \<And>ad ae. P \<alpha> [] (ad # ae); \<And>z aa. P \<alpha> (z # aa) []; \<And>e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<longrightarrow> P \<alpha> (e1 # w1) w2; fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<longrightarrow> P \<alpha> w1 (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) w2; P \<alpha> [] []; \<And>ad ae. P \<alpha> [] (ad # ae); \<And>z aa. P \<alpha> (z # aa) []; \<And>e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<longrightarrow> P \<alpha> (e1 # w1) w2; fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<longrightarrow> P \<alpha> w1 (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)
[PROOF STEP]
apply (case_tac w)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>\<alpha> w. \<lbrakk>P \<alpha> [] []; \<And>ad ae. P \<alpha> [] (ad # ae); \<And>z aa. P \<alpha> (z # aa) []; \<And>e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<longrightarrow> P \<alpha> (e1 # w1) w2; fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<longrightarrow> P \<alpha> w1 (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2); w = []\<rbrakk> \<Longrightarrow> P \<alpha> [] w
 2. \<And>\<alpha> w a list. \<lbrakk>P \<alpha> [] []; \<And>ad ae. P \<alpha> [] (ad # ae); \<And>z aa. P \<alpha> (z # aa) []; \<And>e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<longrightarrow> P \<alpha> (e1 # w1) w2; fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<longrightarrow> P \<alpha> w1 (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2); w = a # list\<rbrakk> \<Longrightarrow> P \<alpha> [] w
 3. \<And>v va \<alpha>. \<lbrakk>P \<alpha> [] []; \<And>ad ae. P \<alpha> [] (ad # ae); \<And>z aa. P \<alpha> (z # aa) []; \<And>e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<longrightarrow> P \<alpha> (e1 # w1) w2; fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<longrightarrow> P \<alpha> w1 (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (v # va) []
 4. \<And>e1 w1 \<alpha> e2 w2. \<lbrakk>\<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}; P \<alpha> [] []; \<And>ad ae. P \<alpha> [] (ad # ae); \<And>z aa. P \<alpha> (z # aa) []; \<And>e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<longrightarrow> P \<alpha> (e1 # w1) w2; fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<longrightarrow> P \<alpha> w1 (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> w1 (e2 # w2); \<lbrakk>fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}; P \<alpha> [] []; \<And>ad ae. P \<alpha> [] (ad # ae); \<And>z aa. P \<alpha> (z # aa) []; \<And>e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<longrightarrow> P \<alpha> (e1 # w1) w2; fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<longrightarrow> P \<alpha> w1 (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) w2; P \<alpha> [] []; \<And>ad ae. P \<alpha> [] (ad # ae); \<And>z aa. P \<alpha> (z # aa) []; \<And>e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<longrightarrow> P \<alpha> (e1 # w1) w2; fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<longrightarrow> P \<alpha> w1 (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma cil_induct_fix\<alpha>'[case_names both_empty left_empty right_empty append]: "\<lbrakk>
  P \<alpha> [] [];
  \<And>ad ae. P \<alpha> [] (ad # ae);
  \<And>z aa. P \<alpha> (z # aa) [];
  \<And>e1 w1 e2 w2. \<lbrakk>
    fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<Longrightarrow> P \<alpha> w1 (e2 # w2);
    fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<Longrightarrow> P \<alpha> (e1 # w1) w2\<rbrakk>
    \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)
  \<rbrakk> \<Longrightarrow> P \<alpha> wa wb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<alpha> [] []; \<And>ad ae. P \<alpha> [] (ad # ae); \<And>z aa. P \<alpha> (z # aa) []; \<And>e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<Longrightarrow> P \<alpha> w1 (e2 # w2); fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<Longrightarrow> P \<alpha> (e1 # w1) w2\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> wa wb
[PROOF STEP]
apply (induct wa \<alpha> wb rule: cil.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>\<alpha> w. \<lbrakk>P \<alpha> [] []; \<And>ad ae. P \<alpha> [] (ad # ae); \<And>z aa. P \<alpha> (z # aa) []; \<And>e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<Longrightarrow> P \<alpha> w1 (e2 # w2); fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<Longrightarrow> P \<alpha> (e1 # w1) w2\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> [] w
 2. \<And>v va \<alpha>. \<lbrakk>P \<alpha> [] []; \<And>ad ae. P \<alpha> [] (ad # ae); \<And>z aa. P \<alpha> (z # aa) []; \<And>e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<Longrightarrow> P \<alpha> w1 (e2 # w2); fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<Longrightarrow> P \<alpha> (e1 # w1) w2\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (v # va) []
 3. \<And>e1 w1 \<alpha> e2 w2. \<lbrakk>\<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}; P \<alpha> [] []; \<And>ad ae. P \<alpha> [] (ad # ae); \<And>z aa. P \<alpha> (z # aa) []; \<And>e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<Longrightarrow> P \<alpha> w1 (e2 # w2); fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<Longrightarrow> P \<alpha> (e1 # w1) w2\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> w1 (e2 # w2); \<lbrakk>fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}; P \<alpha> [] []; \<And>ad ae. P \<alpha> [] (ad # ae); \<And>z aa. P \<alpha> (z # aa) []; \<And>e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<Longrightarrow> P \<alpha> w1 (e2 # w2); fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<Longrightarrow> P \<alpha> (e1 # w1) w2\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) w2; P \<alpha> [] []; \<And>ad ae. P \<alpha> [] (ad # ae); \<And>z aa. P \<alpha> (z # aa) []; \<And>e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<Longrightarrow> P \<alpha> w1 (e2 # w2); fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<Longrightarrow> P \<alpha> (e1 # w1) w2\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)
[PROOF STEP]
apply (case_tac w)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>\<alpha> w. \<lbrakk>P \<alpha> [] []; \<And>ad ae. P \<alpha> [] (ad # ae); \<And>z aa. P \<alpha> (z # aa) []; \<And>e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<Longrightarrow> P \<alpha> w1 (e2 # w2); fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<Longrightarrow> P \<alpha> (e1 # w1) w2\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2); w = []\<rbrakk> \<Longrightarrow> P \<alpha> [] w
 2. \<And>\<alpha> w a list. \<lbrakk>P \<alpha> [] []; \<And>ad ae. P \<alpha> [] (ad # ae); \<And>z aa. P \<alpha> (z # aa) []; \<And>e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<Longrightarrow> P \<alpha> w1 (e2 # w2); fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<Longrightarrow> P \<alpha> (e1 # w1) w2\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2); w = a # list\<rbrakk> \<Longrightarrow> P \<alpha> [] w
 3. \<And>v va \<alpha>. \<lbrakk>P \<alpha> [] []; \<And>ad ae. P \<alpha> [] (ad # ae); \<And>z aa. P \<alpha> (z # aa) []; \<And>e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<Longrightarrow> P \<alpha> w1 (e2 # w2); fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<Longrightarrow> P \<alpha> (e1 # w1) w2\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (v # va) []
 4. \<And>e1 w1 \<alpha> e2 w2. \<lbrakk>\<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {}; P \<alpha> [] []; \<And>ad ae. P \<alpha> [] (ad # ae); \<And>z aa. P \<alpha> (z # aa) []; \<And>e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<Longrightarrow> P \<alpha> w1 (e2 # w2); fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<Longrightarrow> P \<alpha> (e1 # w1) w2\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> w1 (e2 # w2); \<lbrakk>fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {}; P \<alpha> [] []; \<And>ad ae. P \<alpha> [] (ad # ae); \<And>z aa. P \<alpha> (z # aa) []; \<And>e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<Longrightarrow> P \<alpha> w1 (e2 # w2); fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<Longrightarrow> P \<alpha> (e1 # w1) w2\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) w2; P \<alpha> [] []; \<And>ad ae. P \<alpha> [] (ad # ae); \<And>z aa. P \<alpha> (z # aa) []; \<And>e1 w1 e2 w2. \<lbrakk>fst (\<alpha> e1) \<inter> mon_pl (map \<alpha> (e2 # w2)) = {} \<Longrightarrow> P \<alpha> w1 (e2 # w2); fst (\<alpha> e2) \<inter> mon_pl (map \<alpha> (e1 # w1)) = {} \<Longrightarrow> P \<alpha> (e1 # w1) w2\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk> \<Longrightarrow> P \<alpha> (e1 # w1) (e2 # w2)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [simp]: "w\<otimes>\<^bsub>\<alpha>\<^esub>[] = {w}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<otimes>\<^bsub>\<alpha>\<^esub> [] = {w}
[PROOF STEP]
by (cases w, auto)


[STATEMENT]
lemma cil_contains_empty[rule_format, simp]: "([] \<in> wa\<otimes>\<^bsub>\<alpha>\<^esub>wb) = (wa=[] \<and> wb=[])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([] \<in> wa \<otimes>\<^bsub>\<alpha>\<^esub> wb) = (wa = [] \<and> wb = [])
[PROOF STEP]
by (induct wa \<alpha> wb rule: cil.induct) auto


[STATEMENT]
lemma cil_cons_cases[cases set, case_names left right]: "\<lbrakk> e#w \<in> w1\<otimes>\<^bsub>\<alpha>\<^esub>w2;
  !!w1'. \<lbrakk>w1=e#w1'; w\<in>w1'\<otimes>\<^bsub>\<alpha>\<^esub>w2; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w2) = {} \<rbrakk> \<Longrightarrow> P;
  !!w2'. \<lbrakk>w2=e#w2'; w\<in>w1\<otimes>\<^bsub>\<alpha>\<^esub>w2'; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w1) = {} \<rbrakk> \<Longrightarrow> P
\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2; \<And>w1'. \<lbrakk>w1 = e # w1'; w \<in> w1' \<otimes>\<^bsub>\<alpha>\<^esub> w2; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w2) = {}\<rbrakk> \<Longrightarrow> P; \<And>w2'. \<lbrakk>w2 = e # w2'; w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2'; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w1) = {}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (cases rule: cil_cases) auto


[STATEMENT]
lemma cil_set_induct[induct set, case_names empty left right]: "!!\<alpha> w1 w2. \<lbrakk>
    w\<in>w1\<otimes>\<^bsub>\<alpha>\<^esub>w2;
    !!\<alpha>. P [] \<alpha> [] [];
    !!\<alpha> e w' w1' w2. \<lbrakk>w'\<in>w1'\<otimes>\<^bsub>\<alpha>\<^esub>w2; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w2) = {};
                      P w' \<alpha> w1' w2 \<rbrakk> \<Longrightarrow> P (e#w') \<alpha> (e#w1') w2;
    !!\<alpha> e w' w2' w1. \<lbrakk>w'\<in>w1\<otimes>\<^bsub>\<alpha>\<^esub>w2'; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w1) = {};
                      P w' \<alpha> w1 w2' \<rbrakk> \<Longrightarrow> P (e#w') \<alpha> w1 (e#w2')
  \<rbrakk> \<Longrightarrow> P w \<alpha> w1 w2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<alpha> w1 w2. \<lbrakk>w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2; \<And>\<alpha>. P [] \<alpha> [] []; \<And>\<alpha> e w' w1' w2. \<lbrakk>w' \<in> w1' \<otimes>\<^bsub>\<alpha>\<^esub> w2; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w2) = {}; P w' \<alpha> w1' w2\<rbrakk> \<Longrightarrow> P (e # w') \<alpha> (e # w1') w2; \<And>\<alpha> e w' w2' w1. \<lbrakk>w' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2'; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w1) = {}; P w' \<alpha> w1 w2'\<rbrakk> \<Longrightarrow> P (e # w') \<alpha> w1 (e # w2')\<rbrakk> \<Longrightarrow> P w \<alpha> w1 w2
[PROOF STEP]
by (induct w) (auto intro!: cil_contains_empty elim: cil_cons_cases)


[STATEMENT]
lemma cil_set_induct_fix\<alpha>[induct set, case_names empty left right]: "!!w1 w2. \<lbrakk>
    w\<in>w1\<otimes>\<^bsub>\<alpha>\<^esub>w2;
    P [] \<alpha> [] [];
    !!e w' w1' w2. \<lbrakk>w'\<in>w1'\<otimes>\<^bsub>\<alpha>\<^esub>w2; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w2) = {};
                    P w' \<alpha> w1' w2 \<rbrakk> \<Longrightarrow> P (e#w') \<alpha> (e#w1') w2;
    !!e w' w2' w1. \<lbrakk>w'\<in>w1\<otimes>\<^bsub>\<alpha>\<^esub>w2'; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w1) = {};
                    P w' \<alpha> w1 w2' \<rbrakk> \<Longrightarrow> P (e#w') \<alpha> w1 (e#w2')
  \<rbrakk> \<Longrightarrow> P w \<alpha> w1 w2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w1 w2. \<lbrakk>w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2; P [] \<alpha> [] []; \<And>e w' w1' w2. \<lbrakk>w' \<in> w1' \<otimes>\<^bsub>\<alpha>\<^esub> w2; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w2) = {}; P w' \<alpha> w1' w2\<rbrakk> \<Longrightarrow> P (e # w') \<alpha> (e # w1') w2; \<And>e w' w2' w1. \<lbrakk>w' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2'; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w1) = {}; P w' \<alpha> w1 w2'\<rbrakk> \<Longrightarrow> P (e # w') \<alpha> w1 (e # w2')\<rbrakk> \<Longrightarrow> P w \<alpha> w1 w2
[PROOF STEP]
by (induct w) (auto intro!: cil_contains_empty elim: cil_cons_cases)


[STATEMENT]
lemma cil_cons1: "\<lbrakk>w\<in>wa\<otimes>\<^bsub>\<alpha>\<^esub>wb; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> wb) = {}\<rbrakk>
                  \<Longrightarrow> e#w \<in> e#wa \<otimes>\<^bsub>\<alpha>\<^esub> wb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w \<in> wa \<otimes>\<^bsub>\<alpha>\<^esub> wb; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> wb) = {}\<rbrakk> \<Longrightarrow> e # w \<in> e # wa \<otimes>\<^bsub>\<alpha>\<^esub> wb
[PROOF STEP]
by (cases wb) auto


[STATEMENT]
lemma cil_cons2: "\<lbrakk>w\<in>wa\<otimes>\<^bsub>\<alpha>\<^esub>wb; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> wa) = {}\<rbrakk>
                  \<Longrightarrow> e#w \<in> wa \<otimes>\<^bsub>\<alpha>\<^esub> e#wb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w \<in> wa \<otimes>\<^bsub>\<alpha>\<^esub> wb; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> wa) = {}\<rbrakk> \<Longrightarrow> e # w \<in> wa \<otimes>\<^bsub>\<alpha>\<^esub> e # wb
[PROOF STEP]
by (cases wa) auto


[STATEMENT]
lemma cil_subset_il': "w\<in>w1\<otimes>\<^bsub>\<alpha>\<^esub>w2 \<Longrightarrow> w\<in>w1\<otimes>w2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2 \<Longrightarrow> w \<in> w1 \<otimes> w2
[PROOF STEP]
using cil_subset_il
[PROOF STATE]
proof (prove)
using this:
?w \<otimes>\<^bsub>?\<alpha>\<^esub> ?w' \<subseteq> ?w \<otimes> ?w'

goal (1 subgoal):
 1. w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2 \<Longrightarrow> w \<in> w1 \<otimes> w2
[PROOF STEP]
by (auto)

\<comment> \<open>Consistent interleaving preserves the set of letters of both operands\<close>


[STATEMENT]
lemma cil_set: "w\<in>w1\<otimes>\<^bsub>\<alpha>\<^esub>w2 \<Longrightarrow> set w = set w1 \<union> set w2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2 \<Longrightarrow> set w = set w1 \<union> set w2
[PROOF STEP]
by (induct rule: cil_set_induct_fix\<alpha>) auto


[STATEMENT]
lemma cil_length[rule_format]: "\<forall>w\<in>wa\<otimes>\<^bsub>\<alpha>\<^esub>wb. length w = length wa + length wb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w\<in>wa \<otimes>\<^bsub>\<alpha>\<^esub> wb. length w = length wa + length wb
[PROOF STEP]
by (induct rule: cil.induct) auto

\<comment> \<open>Consistent interleaving contains all letters of each operand in the original order\<close>


[STATEMENT]
lemma cil_ileq: "w\<in>w1\<otimes>\<^bsub>\<alpha>\<^esub>w2 \<Longrightarrow> w1\<preceq>w \<and> w2\<preceq>w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2 \<Longrightarrow> w1 \<preceq> w \<and> w2 \<preceq> w
[PROOF STEP]
by (intro conjI cil_subset_il' ileq_interleave)

\<comment> \<open>Consistent interleaving is commutative and associative\<close>


[STATEMENT]
lemma cil_commute: "w\<otimes>\<^bsub>\<alpha>\<^esub>w' = w'\<otimes>\<^bsub>\<alpha>\<^esub>w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<otimes>\<^bsub>\<alpha>\<^esub> w' = w' \<otimes>\<^bsub>\<alpha>\<^esub> w
[PROOF STEP]
by (induct rule: cil.induct) auto