[STATEMENT]
lemma factoringlemma_withconstant:
    fixes A
          and b::real
          and c::real
      assumes c: "c \<ge> 1"
      assumes dist: "\<forall>e\<in>S0. distinct e"
      assumes notempty: "\<forall>e\<in>S0. length e > 0"
      (* A has pairwise property *)
      assumes pw: "pairwise A"
      (* A is c-competitive on list of length 2 *)
      assumes on2: "\<forall>s0\<in>S0. \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. \<forall>(x,y)\<in>{(x,y). x \<in> set s0 \<and> y\<in>set s0 \<and> x<y}. T\<^sub>p_on_rand A (Lxy s0 {x,y}) (Lxy qs {x,y})  \<le> c * (T\<^sub>p_opt (Lxy s0 {x,y}) (Lxy qs {x,y})) + b"
      assumes nopaid: "\<And>is s q. \<forall>((free,paid),_) \<in> (snd A (s, is) q). paid=[]"
      assumes 4: "\<And>init qs. distinct init \<Longrightarrow> set qs \<subseteq> set init \<Longrightarrow> (\<And>x. x<length qs \<Longrightarrow> finite (set_pmf (config'' A qs init x)))"
      (* then A is c-competitive on arbitrary list lengths *)
      shows "\<forall>s0\<in>S0. \<exists>b\<ge>0.  \<forall>qs\<in>{x. set x \<subseteq> set s0}.
              T\<^sub>p_on_rand A s0 qs \<le> c * real (T\<^sub>p_opt s0 qs) + b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s0\<in>S0. \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. T\<^sub>p_on_rand' A (fst A s0 \<bind> (\<lambda>is. return_pmf (s0, is))) qs \<le> c * real (T\<^sub>p_opt s0 qs) + b
[PROOF STEP]
proof (standard, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s0. s0 \<in> S0 \<Longrightarrow> \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. T\<^sub>p_on_rand' A (fst A s0 \<bind> (\<lambda>is. return_pmf (s0, is))) qs \<le> c * real (T\<^sub>p_opt s0 qs) + b
[PROOF STEP]
case (1 init)
[PROOF STATE]
proof (state)
this:
init \<in> S0

goal (1 subgoal):
 1. \<And>s0. s0 \<in> S0 \<Longrightarrow> \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. T\<^sub>p_on_rand' A (fst A s0 \<bind> (\<lambda>is. return_pmf (s0, is))) qs \<le> c * real (T\<^sub>p_opt s0 qs) + b
[PROOF STEP]
have d: "distinct init"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct init
[PROOF STEP]
using  dist 1
[PROOF STATE]
proof (prove)
using this:
\<forall>e\<in>S0. distinct e
init \<in> S0

goal (1 subgoal):
 1. distinct init
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct init

goal (1 subgoal):
 1. \<And>s0. s0 \<in> S0 \<Longrightarrow> \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. T\<^sub>p_on_rand' A (fst A s0 \<bind> (\<lambda>is. return_pmf (s0, is))) qs \<le> c * real (T\<^sub>p_opt s0 qs) + b
[PROOF STEP]
have d2: "init \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init \<noteq> []
[PROOF STEP]
using  notempty 1
[PROOF STATE]
proof (prove)
using this:
\<forall>e\<in>S0. 0 < length e
init \<in> S0

goal (1 subgoal):
 1. init \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
init \<noteq> []

goal (1 subgoal):
 1. \<And>s0. s0 \<in> S0 \<Longrightarrow> \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. T\<^sub>p_on_rand' A (fst A s0 \<bind> (\<lambda>is. return_pmf (s0, is))) qs \<le> c * real (T\<^sub>p_opt s0 qs) + b
[PROOF STEP]
obtain b where on3: "\<forall>qs\<in>{x. set x \<subseteq> set init}. \<forall>(x,y)\<in>{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}. T\<^sub>p_on_rand A  (Lxy init {x,y}) (Lxy qs {x,y}) \<le> c * (T\<^sub>p_opt (Lxy init {x,y}) (Lxy qs {x,y})) + b"
        and b: "b\<ge>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>b. \<lbrakk>\<forall>qs\<in>{x. set x \<subseteq> set init}. \<forall>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<le> c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b; 0 \<le> b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using on2 1
[PROOF STATE]
proof (prove)
using this:
\<forall>s0\<in>S0. \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. \<forall>(x, y)\<in>{(x, y). x \<in> set s0 \<and> y \<in> set s0 \<and> x < y}. T\<^sub>p_on_rand' A (fst A (Lxy s0 {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy s0 {x, y}, is))) (Lxy qs {x, y}) \<le> c * real (T\<^sub>p_opt (Lxy s0 {x, y}) (Lxy qs {x, y})) + b
init \<in> S0

goal (1 subgoal):
 1. (\<And>b. \<lbrakk>\<forall>qs\<in>{x. set x \<subseteq> set init}. \<forall>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<le> c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b; 0 \<le> b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>qs\<in>{x. set x \<subseteq> set init}. \<forall>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<le> c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b
0 \<le> b

goal (1 subgoal):
 1. \<And>s0. s0 \<in> S0 \<Longrightarrow> \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. T\<^sub>p_on_rand' A (fst A s0 \<bind> (\<lambda>is. return_pmf (s0, is))) qs \<le> c * real (T\<^sub>p_opt s0 qs) + b
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>qs\<in>{x. set x \<subseteq> set init}. \<forall>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<le> c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b
0 \<le> b

goal (1 subgoal):
 1. \<And>s0. s0 \<in> S0 \<Longrightarrow> \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. T\<^sub>p_on_rand' A (fst A s0 \<bind> (\<lambda>is. return_pmf (s0, is))) qs \<le> c * real (T\<^sub>p_opt s0 qs) + b
[PROOF STEP]
fix qs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s0. s0 \<in> S0 \<Longrightarrow> \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. T\<^sub>p_on_rand' A (fst A s0 \<bind> (\<lambda>is. return_pmf (s0, is))) qs \<le> c * real (T\<^sub>p_opt s0 qs) + b
[PROOF STEP]
assume drin: "set qs \<subseteq> set init"
[PROOF STATE]
proof (state)
this:
set qs \<subseteq> set init

goal (1 subgoal):
 1. \<And>s0. s0 \<in> S0 \<Longrightarrow> \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. T\<^sub>p_on_rand' A (fst A s0 \<bind> (\<lambda>is. return_pmf (s0, is))) qs \<le> c * real (T\<^sub>p_opt s0 qs) + b
[PROOF STEP]
have "T\<^sub>p_on_rand A init qs =
(\<Sum>(x,y)\<in>{(x, y) . x \<in> set init \<and> y \<in> set init \<and> x < y}.
       T\<^sub>p_on_rand A (Lxy init {x,y}) (Lxy qs {x, y})) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}))
[PROOF STEP]
apply(rule umf_pair)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. List_Factoring.pairwise A
 2. \<And>is s q. \<forall>((free, paid), uu_)\<in>set_pmf (snd A (s, is) q). paid = []
 3. set qs \<subseteq> set init
 4. distinct init
 5. \<And>x. x < length qs \<Longrightarrow> finite (set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)))
[PROOF STEP]
apply(fact)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x < length qs \<Longrightarrow> finite (set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)))
[PROOF STEP]
using 4[of init qs] drin d
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct init; set qs \<subseteq> set init; ?x < length qs\<rbrakk> \<Longrightarrow> finite (set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take ?x qs)))
set qs \<subseteq> set init
distinct init

goal (1 subgoal):
 1. \<And>x. x < length qs \<Longrightarrow> finite (set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)))
[PROOF STEP]
by(simp add: split_def)
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}))

goal (1 subgoal):
 1. \<And>s0. s0 \<in> S0 \<Longrightarrow> \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. T\<^sub>p_on_rand' A (fst A s0 \<bind> (\<lambda>is. return_pmf (s0, is))) qs \<le> c * real (T\<^sub>p_opt s0 qs) + b
[PROOF STEP]
(* 1.4 *)
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}))

goal (1 subgoal):
 1. \<And>s0. s0 \<in> S0 \<Longrightarrow> \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. T\<^sub>p_on_rand' A (fst A s0 \<bind> (\<lambda>is. return_pmf (s0, is))) qs \<le> c * real (T\<^sub>p_opt s0 qs) + b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}))

goal (1 subgoal):
 1. \<And>s0. s0 \<in> S0 \<Longrightarrow> \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. T\<^sub>p_on_rand' A (fst A s0 \<bind> (\<lambda>is. return_pmf (s0, is))) qs \<le> c * real (T\<^sub>p_opt s0 qs) + b
[PROOF STEP]
have "\<dots> \<le> (\<Sum>(x,y)\<in>{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}. c * (T\<^sub>p_opt (Lxy init {x,y}) (Lxy qs {x,y})) + b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y})) \<le> (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b)
[PROOF STEP]
apply(rule sum_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<in> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<Longrightarrow> (case i of (x, y) \<Rightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y})) \<le> (case i of (x, y) \<Rightarrow> c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b)
[PROOF STEP]
using on3 drin
[PROOF STATE]
proof (prove)
using this:
\<forall>qs\<in>{x. set x \<subseteq> set init}. \<forall>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<le> c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b
set qs \<subseteq> set init

goal (1 subgoal):
 1. \<And>i. i \<in> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<Longrightarrow> (case i of (x, y) \<Rightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y})) \<le> (case i of (x, y) \<Rightarrow> c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b)
[PROOF STEP]
by(simp add: split_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y})) \<le> (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b)

goal (1 subgoal):
 1. \<And>s0. s0 \<in> S0 \<Longrightarrow> \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. T\<^sub>p_on_rand' A (fst A s0 \<bind> (\<lambda>is. return_pmf (s0, is))) qs \<le> c * real (T\<^sub>p_opt s0 qs) + b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y})) \<le> (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b)

goal (1 subgoal):
 1. \<And>s0. s0 \<in> S0 \<Longrightarrow> \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. T\<^sub>p_on_rand' A (fst A s0 \<bind> (\<lambda>is. return_pmf (s0, is))) qs \<le> c * real (T\<^sub>p_opt s0 qs) + b
[PROOF STEP]
have "\<dots> = c * (\<Sum>(x,y)\<in>{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}. T\<^sub>p_opt (Lxy init {x,y}) (Lxy qs {x,y})) + b*(((length init)*(length init-1)) / 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b) = c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b) = c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b) = c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2)
[PROOF STEP]
fix S::"'a list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b) = c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2)
[PROOF STEP]
assume dis: "distinct S"
[PROOF STATE]
proof (state)
this:
distinct S

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b) = c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2)
[PROOF STEP]
assume d2: "S \<noteq> []"
[PROOF STATE]
proof (state)
this:
S \<noteq> []

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b) = c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S \<noteq> []
[PROOF STEP]
have d3: "sort S \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
S \<noteq> []

goal (1 subgoal):
 1. sort S \<noteq> []
[PROOF STEP]
by (metis length_0_conv length_sort)
[PROOF STATE]
proof (state)
this:
sort S \<noteq> []

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b) = c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2)
[PROOF STEP]
have "card {(x,y). x \<in> set S \<and> y\<in>set S \<and> x<y}
            = card {(x,y). x \<in> set (sort S) \<and> y\<in>set (sort S) \<and> x<y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {(x, y). x \<in> set S \<and> y \<in> set S \<and> x < y} = card {(x, y). x \<in> set (sort S) \<and> y \<in> set (sort S) \<and> x < y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card {(x, y). x \<in> set S \<and> y \<in> set S \<and> x < y} = card {(x, y). x \<in> set (sort S) \<and> y \<in> set (sort S) \<and> x < y}

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b) = c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card {(x, y). x \<in> set S \<and> y \<in> set S \<and> x < y} = card {(x, y). x \<in> set (sort S) \<and> y \<in> set (sort S) \<and> x < y}

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b) = c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2)
[PROOF STEP]
have "\<dots> = (length (sort S) * (length (sort S) - 1)) / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (card {(x, y). x \<in> set (sort S) \<and> y \<in> set (sort S) \<and> x < y}) = real (length (sort S) * (length (sort S) - 1)) / 2
[PROOF STEP]
apply(rule cardofpairs)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. sort S \<noteq> []
 2. sorted (sort S)
 3. distinct (sort S)
[PROOF STEP]
using dis d2 d3
[PROOF STATE]
proof (prove)
using this:
distinct S
S \<noteq> []
sort S \<noteq> []

goal (3 subgoals):
 1. sort S \<noteq> []
 2. sorted (sort S)
 3. distinct (sort S)
[PROOF STEP]
by (simp_all)
[PROOF STATE]
proof (state)
this:
real (card {(x, y). x \<in> set (sort S) \<and> y \<in> set (sort S) \<and> x < y}) = real (length (sort S) * (length (sort S) - 1)) / 2

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b) = c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real (card {(x, y). x \<in> set S \<and> y \<in> set S \<and> x < y}) = real (length (sort S) * (length (sort S) - 1)) / 2
[PROOF STEP]
have "card {(x, y) . x \<in> set S \<and> y \<in> set S \<and> x < y} =
              (length (sort S) * (length (sort S) - 1)) / 2 "
[PROOF STATE]
proof (prove)
using this:
real (card {(x, y). x \<in> set S \<and> y \<in> set S \<and> x < y}) = real (length (sort S) * (length (sort S) - 1)) / 2

goal (1 subgoal):
 1. real (card {(x, y). x \<in> set S \<and> y \<in> set S \<and> x < y}) = real (length (sort S) * (length (sort S) - 1)) / 2
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
real (card {(x, y). x \<in> set S \<and> y \<in> set S \<and> x < y}) = real (length (sort S) * (length (sort S) - 1)) / 2

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b) = c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>distinct ?S2; ?S2 \<noteq> []\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set ?S2 \<and> y \<in> set ?S2 \<and> x < y}) = real (length (sort ?S2) * (length (sort ?S2) - 1)) / 2

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b) = c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2)
[PROOF STEP]
with d d2
[PROOF STATE]
proof (chain)
picking this:
distinct init
init \<noteq> []
\<lbrakk>distinct ?S2; ?S2 \<noteq> []\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set ?S2 \<and> y \<in> set ?S2 \<and> x < y}) = real (length (sort ?S2) * (length (sort ?S2) - 1)) / 2
[PROOF STEP]
have e: "card {(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y} = ((length init)*(length init-1)) / 2"
[PROOF STATE]
proof (prove)
using this:
distinct init
init \<noteq> []
\<lbrakk>distinct ?S2; ?S2 \<noteq> []\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set ?S2 \<and> y \<in> set ?S2 \<and> x < y}) = real (length (sort ?S2) * (length (sort ?S2) - 1)) / 2

goal (1 subgoal):
 1. real (card {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}) = real (length init * (length init - 1)) / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real (card {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}) = real (length init * (length init - 1)) / 2

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b) = c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2)
[PROOF STEP]
show ?thesis  (is "(\<Sum>(x,y)\<in>?S. c * (?T x y) + b) = c * ?R + b*?T2")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b) = c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b) = c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2)
[PROOF STEP]
have "(\<Sum>(x,y)\<in>?S. c * (?T x y) + b) =
              c * (\<Sum>(x,y)\<in>?S. (?T x y)) + (\<Sum>(x,y)\<in>?S. b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b) = c * (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y}))) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. b)
[PROOF STEP]
by(simp add: split_def sum.distrib sum_distrib_left)
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b) = c * (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y}))) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. b)

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b) = c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b) = c * (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y}))) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. b)

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b) = c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2)
[PROOF STEP]
have "\<dots> = c * (\<Sum>(x,y)\<in>?S. (?T x y)) + b*?T2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c * (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y}))) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. b) = c * (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y}))) + b * (real (length init * (length init - 1)) / 2)
[PROOF STEP]
using e
[PROOF STATE]
proof (prove)
using this:
real (card {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}) = real (length init * (length init - 1)) / 2

goal (1 subgoal):
 1. c * (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y}))) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. b) = c * (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y}))) + b * (real (length init * (length init - 1)) / 2)
[PROOF STEP]
by(simp add: split_def)
[PROOF STATE]
proof (state)
this:
c * (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y}))) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. b) = c * (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y}))) + b * (real (length init * (length init - 1)) / 2)

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b) = c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b) = c * (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y}))) + b * (real (length init * (length init - 1)) / 2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b) = c * (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y}))) + b * (real (length init * (length init - 1)) / 2)

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b) = c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2)
[PROOF STEP]
by(simp add: split_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b) = c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b) = c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b) = c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2)

goal (1 subgoal):
 1. \<And>s0. s0 \<in> S0 \<Longrightarrow> \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. T\<^sub>p_on_rand' A (fst A s0 \<bind> (\<lambda>is. return_pmf (s0, is))) qs \<le> c * real (T\<^sub>p_opt s0 qs) + b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. c * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b) = c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2)

goal (1 subgoal):
 1. \<And>s0. s0 \<in> S0 \<Longrightarrow> \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. T\<^sub>p_on_rand' A (fst A s0 \<bind> (\<lambda>is. return_pmf (s0, is))) qs \<le> c * real (T\<^sub>p_opt s0 qs) + b
[PROOF STEP]
have "\<dots> \<le> c * T\<^sub>p_opt init qs + (b*((length init)*(length init-1)) / 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2) \<le> c * real (T\<^sub>p_opt init qs) + b * real (length init * (length init - 1)) / 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2) \<le> c * real (T\<^sub>p_opt init qs) + b * real (length init * (length init - 1)) / 2
[PROOF STEP]
have "(\<Sum>(x, y)\<in>{(x, y) . x \<in> set init \<and>
              y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x,y}) (Lxy qs {x, y}))
              \<le>  T\<^sub>p_opt init qs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) \<le> T\<^sub>p_opt init qs
[PROOF STEP]
using OPT_zerlegen drin d d2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct ?init; ?init \<noteq> []; set ?qs \<subseteq> set ?init\<rbrakk> \<Longrightarrow> (\<Sum>(x, y)\<in>{(x, y). x \<in> set ?init \<and> y \<in> set ?init \<and> x < y}. T\<^sub>p_opt (Lxy ?init {x, y}) (Lxy ?qs {x, y})) \<le> T\<^sub>p_opt ?init ?qs
set qs \<subseteq> set init
distinct init
init \<noteq> []

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) \<le> T\<^sub>p_opt init qs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) \<le> T\<^sub>p_opt init qs

goal (1 subgoal):
 1. c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2) \<le> c * real (T\<^sub>p_opt init qs) + b * real (length init * (length init - 1)) / 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) \<le> T\<^sub>p_opt init qs
[PROOF STEP]
have "  real (\<Sum>(x, y)\<in>{(x, y) . x \<in> set init \<and>
              y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x,y}) (Lxy qs {x, y}))
              \<le>    (T\<^sub>p_opt init qs)"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) \<le> T\<^sub>p_opt init qs

goal (1 subgoal):
 1. real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) \<le> real (T\<^sub>p_opt init qs)
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) \<le> real (T\<^sub>p_opt init qs)

goal (1 subgoal):
 1. c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2) \<le> c * real (T\<^sub>p_opt init qs) + b * real (length init * (length init - 1)) / 2
[PROOF STEP]
with c
[PROOF STATE]
proof (chain)
picking this:
1 \<le> c
real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) \<le> real (T\<^sub>p_opt init qs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
1 \<le> c
real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) \<le> real (T\<^sub>p_opt init qs)

goal (1 subgoal):
 1. c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2) \<le> c * real (T\<^sub>p_opt init qs) + b * real (length init * (length init - 1)) / 2
[PROOF STEP]
by(auto simp: split_def)
[PROOF STATE]
proof (state)
this:
c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2) \<le> c * real (T\<^sub>p_opt init qs) + b * real (length init * (length init - 1)) / 2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
c * real (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b * (real (length init * (length init - 1)) / 2) \<le> c * real (T\<^sub>p_opt init qs) + b * real (length init * (length init - 1)) / 2

goal (1 subgoal):
 1. \<And>s0. s0 \<in> S0 \<Longrightarrow> \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. T\<^sub>p_on_rand' A (fst A s0 \<bind> (\<lambda>is. return_pmf (s0, is))) qs \<le> c * real (T\<^sub>p_opt s0 qs) + b
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<le> c * real (T\<^sub>p_opt init qs) + b * real (length init * (length init - 1)) / 2
[PROOF STEP]
have f: "T\<^sub>p_on_rand A init qs \<le> c * real (T\<^sub>p_opt init qs) + (b*((length init)*(length init-1)) / 2)"
[PROOF STATE]
proof (prove)
using this:
T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<le> c * real (T\<^sub>p_opt init qs) + b * real (length init * (length init - 1)) / 2

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<le> c * real (T\<^sub>p_opt init qs) + b * real (length init * (length init - 1)) / 2
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<le> c * real (T\<^sub>p_opt init qs) + b * real (length init * (length init - 1)) / 2

goal (1 subgoal):
 1. \<And>s0. s0 \<in> S0 \<Longrightarrow> \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. T\<^sub>p_on_rand' A (fst A s0 \<bind> (\<lambda>is. return_pmf (s0, is))) qs \<le> c * real (T\<^sub>p_opt s0 qs) + b
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
set ?qs2 \<subseteq> set init \<Longrightarrow> T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) ?qs2 \<le> c * real (T\<^sub>p_opt init ?qs2) + b * real (length init * (length init - 1)) / 2

goal (1 subgoal):
 1. \<And>s0. s0 \<in> S0 \<Longrightarrow> \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. T\<^sub>p_on_rand' A (fst A s0 \<bind> (\<lambda>is. return_pmf (s0, is))) qs \<le> c * real (T\<^sub>p_opt s0 qs) + b
[PROOF STEP]
note all=this
[PROOF STATE]
proof (state)
this:
set ?qs2 \<subseteq> set init \<Longrightarrow> T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) ?qs2 \<le> c * real (T\<^sub>p_opt init ?qs2) + b * real (length init * (length init - 1)) / 2

goal (1 subgoal):
 1. \<And>s0. s0 \<in> S0 \<Longrightarrow> \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. T\<^sub>p_on_rand' A (fst A s0 \<bind> (\<lambda>is. return_pmf (s0, is))) qs \<le> c * real (T\<^sub>p_opt s0 qs) + b
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set init}. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<le> c * real (T\<^sub>p_opt init qs) + b
[PROOF STEP]
unfolding compet_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set init}. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<le> c * real (T\<^sub>p_opt init qs) + b
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>b\<ge>0. \<forall>qs. set qs \<subseteq> set init \<longrightarrow> T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<le> c * real (T\<^sub>p_opt init qs) + b
[PROOF STEP]
apply(rule exI[where x="(b*((length init)*(length init-1)) / 2)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> b * real (length init * (length init - 1)) / 2 \<and> (\<forall>qs. set qs \<subseteq> set init \<longrightarrow> T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<le> c * real (T\<^sub>p_opt init qs) + b * real (length init * (length init - 1)) / 2)
[PROOF STEP]
apply(safe)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 \<le> b * real (length init * (length init - 1)) / 2
 2. \<And>qs. set qs \<subseteq> set init \<Longrightarrow> T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<le> c * real (T\<^sub>p_opt init qs) + b * real (length init * (length init - 1)) / 2
[PROOF STEP]
using notempty 1 b
[PROOF STATE]
proof (prove)
using this:
\<forall>e\<in>S0. 0 < length e
init \<in> S0
0 \<le> b

goal (2 subgoals):
 1. 0 \<le> b * real (length init * (length init - 1)) / 2
 2. \<And>qs. set qs \<subseteq> set init \<Longrightarrow> T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<le> c * real (T\<^sub>p_opt init qs) + b * real (length init * (length init - 1)) / 2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>qs. set qs \<subseteq> set init \<Longrightarrow> T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<le> c * real (T\<^sub>p_opt init qs) + b * real (length init * (length init - 1)) / 2
[PROOF STEP]
using all b
[PROOF STATE]
proof (prove)
using this:
set ?qs2 \<subseteq> set init \<Longrightarrow> T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) ?qs2 \<le> c * real (T\<^sub>p_opt init ?qs2) + b * real (length init * (length init - 1)) / 2
0 \<le> b

goal (1 subgoal):
 1. \<And>qs. set qs \<subseteq> set init \<Longrightarrow> T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<le> c * real (T\<^sub>p_opt init qs) + b * real (length init * (length init - 1)) / 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set init}. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<le> c * real (T\<^sub>p_opt init qs) + b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma factoringlemma_withconstant':
    fixes A
          and b::real
          and c::real
      assumes c: "c \<ge> 1"
      assumes dist: "\<forall>e\<in>S0. distinct e"
      assumes notempty: "\<forall>e\<in>S0. length e > 0"
      (* A has pairwise property *)
      assumes pw: "pairwise A"
      (* A is c-competitive on list of length 2 *)
      assumes on2: "\<forall>s0\<in>S0. \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. \<forall>(x,y)\<in>{(x,y). x \<in> set s0 \<and> y\<in>set s0 \<and> x<y}. T\<^sub>p_on_rand A (Lxy s0 {x,y}) (Lxy qs {x,y})  \<le> c * (T\<^sub>p_opt (Lxy s0 {x,y}) (Lxy qs {x,y})) + b"
      assumes nopaid: "\<And>is s q. \<forall>((free,paid),_) \<in> (snd A (s, is) q). paid=[]"
      assumes 4: "\<And>init qs. distinct init \<Longrightarrow> set qs \<subseteq> set init \<Longrightarrow> (\<And>x. x<length qs \<Longrightarrow> finite (set_pmf (config'' A qs init x)))"
      (* then A is c-competitive on arbitrary list lengths *)
      shows "compet_rand A c S0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Cost_Model.compet_rand A c S0
[PROOF STEP]
unfolding compet_rand_def static_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s\<in>S0. \<exists>b\<ge>0. \<forall>rs. set rs \<subseteq> set s \<longrightarrow> T\<^sub>p_on_rand' A (fst A s \<bind> (\<lambda>is. return_pmf (s, is))) rs \<le> c * real (T\<^sub>p_opt s rs) + b
[PROOF STEP]
using factoringlemma_withconstant[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>init qs x. \<lbrakk>distinct init; set qs \<subseteq> set init; x < length qs\<rbrakk> \<Longrightarrow> distinct init; \<And>init qs x. \<lbrakk>distinct init; set qs \<subseteq> set init; x < length qs\<rbrakk> \<Longrightarrow> set qs \<subseteq> set init; \<And>init qs x. \<lbrakk>distinct init; set qs \<subseteq> set init; x < length qs\<rbrakk> \<Longrightarrow> x < length qs\<rbrakk> \<Longrightarrow> \<forall>s0\<in>S0. \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. T\<^sub>p_on_rand' A (fst A s0 \<bind> (\<lambda>is. return_pmf (s0, is))) qs \<le> c * real (T\<^sub>p_opt s0 qs) + b

goal (1 subgoal):
 1. \<forall>s\<in>S0. \<exists>b\<ge>0. \<forall>rs. set rs \<subseteq> set s \<longrightarrow> T\<^sub>p_on_rand' A (fst A s \<bind> (\<lambda>is. return_pmf (s, is))) rs \<le> c * real (T\<^sub>p_opt s rs) + b
[PROOF STEP]
by simp


[STATEMENT]
lemma iso_classes_iff:
  assumes "group G"
  assumes "group H"
  shows "(\<exists>\<phi>. \<phi> \<in> iso G H) = (group.iso_class G = group.iso_class H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>\<phi>. \<phi> \<in> Group.iso G H) = (group.iso_class G = group.iso_class H)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<exists>\<phi>. \<phi> \<in> Group.iso G H) = (group.iso_class G = group.iso_class H)
[PROOF STEP]
from assms(1,2)
[PROOF STATE]
proof (chain)
picking this:
Group.group G
Group.group H
[PROOF STEP]
have groups:"group (monoid.truncate G)" "group (monoid.truncate H)"
[PROOF STATE]
proof (prove)
using this:
Group.group G
Group.group H

goal (1 subgoal):
 1. Group.group (monoid.truncate G) &&& Group.group (monoid.truncate H)
[PROOF STEP]
unfolding monoid.truncate_def group_def group_axioms_def Units_def monoid_def
[PROOF STATE]
proof (prove)
using this:
(((\<forall>x y. x \<in> carrier G \<longrightarrow> y \<in> carrier G \<longrightarrow> x \<otimes>\<^bsub>G\<^esub> y \<in> carrier G) \<and> (\<forall>x y z. x \<in> carrier G \<longrightarrow> y \<in> carrier G \<longrightarrow> z \<in> carrier G \<longrightarrow> x \<otimes>\<^bsub>G\<^esub> y \<otimes>\<^bsub>G\<^esub> z = x \<otimes>\<^bsub>G\<^esub> (y \<otimes>\<^bsub>G\<^esub> z))) \<and> \<one>\<^bsub>G\<^esub> \<in> carrier G \<and> (\<forall>x. x \<in> carrier G \<longrightarrow> \<one>\<^bsub>G\<^esub> \<otimes>\<^bsub>G\<^esub> x = x) \<and> (\<forall>x. x \<in> carrier G \<longrightarrow> x \<otimes>\<^bsub>G\<^esub> \<one>\<^bsub>G\<^esub> = x)) \<and> carrier G \<subseteq> {y \<in> carrier G. \<exists>x\<in>carrier G. x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> \<and> y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>}
(((\<forall>x y. x \<in> carrier H \<longrightarrow> y \<in> carrier H \<longrightarrow> x \<otimes>\<^bsub>H\<^esub> y \<in> carrier H) \<and> (\<forall>x y z. x \<in> carrier H \<longrightarrow> y \<in> carrier H \<longrightarrow> z \<in> carrier H \<longrightarrow> x \<otimes>\<^bsub>H\<^esub> y \<otimes>\<^bsub>H\<^esub> z = x \<otimes>\<^bsub>H\<^esub> (y \<otimes>\<^bsub>H\<^esub> z))) \<and> \<one>\<^bsub>H\<^esub> \<in> carrier H \<and> (\<forall>x. x \<in> carrier H \<longrightarrow> \<one>\<^bsub>H\<^esub> \<otimes>\<^bsub>H\<^esub> x = x) \<and> (\<forall>x. x \<in> carrier H \<longrightarrow> x \<otimes>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = x)) \<and> carrier H \<subseteq> {y \<in> carrier H. \<exists>x\<in>carrier H. x \<otimes>\<^bsub>H\<^esub> y = \<one>\<^bsub>H\<^esub> \<and> y \<otimes>\<^bsub>H\<^esub> x = \<one>\<^bsub>H\<^esub>}

goal (1 subgoal):
 1. (((\<forall>x y. x \<in> carrier \<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr> \<longrightarrow> y \<in> carrier \<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr> \<longrightarrow> x \<otimes>\<^bsub>\<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> y \<in> carrier \<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr>) \<and> (\<forall>x y z. x \<in> carrier \<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr> \<longrightarrow> y \<in> carrier \<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr> \<longrightarrow> z \<in> carrier \<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr> \<longrightarrow> x \<otimes>\<^bsub>\<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> y \<otimes>\<^bsub>\<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> z = x \<otimes>\<^bsub>\<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> (y \<otimes>\<^bsub>\<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> z))) \<and> \<one>\<^bsub>\<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> \<in> carrier \<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr> \<and> (\<forall>x. x \<in> carrier \<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr> \<longrightarrow> \<one>\<^bsub>\<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> \<otimes>\<^bsub>\<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> x = x) \<and> (\<forall>x. x \<in> carrier \<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr> \<longrightarrow> x \<otimes>\<^bsub>\<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> \<one>\<^bsub>\<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> = x)) \<and> carrier \<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr> \<subseteq> {y \<in> carrier \<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr>. \<exists>x\<in>carrier \<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr>. x \<otimes>\<^bsub>\<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> y = \<one>\<^bsub>\<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> \<and> y \<otimes>\<^bsub>\<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> x = \<one>\<^bsub>\<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr>\<^esub>} &&& (((\<forall>x y. x \<in> carrier \<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr> \<longrightarrow> y \<in> carrier \<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr> \<longrightarrow> x \<otimes>\<^bsub>\<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr>\<^esub> y \<in> carrier \<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr>) \<and> (\<forall>x y z. x \<in> carrier \<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr> \<longrightarrow> y \<in> carrier \<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr> \<longrightarrow> z \<in> carrier \<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr> \<longrightarrow> x \<otimes>\<^bsub>\<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr>\<^esub> y \<otimes>\<^bsub>\<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr>\<^esub> z = x \<otimes>\<^bsub>\<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr>\<^esub> (y \<otimes>\<^bsub>\<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr>\<^esub> z))) \<and> \<one>\<^bsub>\<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr>\<^esub> \<in> carrier \<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr> \<and> (\<forall>x. x \<in> carrier \<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr> \<longrightarrow> \<one>\<^bsub>\<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr>\<^esub> \<otimes>\<^bsub>\<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr>\<^esub> x = x) \<and> (\<forall>x. x \<in> carrier \<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr> \<longrightarrow> x \<otimes>\<^bsub>\<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr>\<^esub> \<one>\<^bsub>\<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr>\<^esub> = x)) \<and> carrier \<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr> \<subseteq> {y \<in> carrier \<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr>. \<exists>x\<in>carrier \<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr>. x \<otimes>\<^bsub>\<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr>\<^esub> y = \<one>\<^bsub>\<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr>\<^esub> \<and> y \<otimes>\<^bsub>\<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr>\<^esub> x = \<one>\<^bsub>\<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr>\<^esub>}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Group.group (monoid.truncate G)
Group.group (monoid.truncate H)

goal (1 subgoal):
 1. (\<exists>\<phi>. \<phi> \<in> Group.iso G H) = (group.iso_class G = group.iso_class H)
[PROOF STEP]
have "(\<exists>\<phi>. \<phi> \<in> iso G H) = (\<exists>\<phi>. \<phi> \<in> iso (monoid.truncate G) (monoid.truncate H))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>\<phi>. \<phi> \<in> Group.iso G H) = (\<exists>\<phi>. \<phi> \<in> Group.iso (monoid.truncate G) (monoid.truncate H))
[PROOF STEP]
unfolding iso_def hom_def monoid.truncate_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>\<phi>. \<phi> \<in> {h \<in> {h \<in> carrier G \<rightarrow> carrier H. \<forall>x\<in>carrier G. \<forall>y\<in>carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y}. bij_betw h (carrier G) (carrier H)}) = (\<exists>\<phi>. \<phi> \<in> {h \<in> {h \<in> carrier \<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr> \<rightarrow> carrier \<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr>. \<forall>x\<in>carrier \<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr>. \<forall>y\<in>carrier \<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr>. h (x \<otimes>\<^bsub>\<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> y) = h x \<otimes>\<^bsub>\<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr>\<^esub> h y}. bij_betw h (carrier \<lparr>carrier = carrier G, mult = (\<otimes>\<^bsub>G\<^esub>), one = \<one>\<^bsub>G\<^esub>\<rparr>) (carrier \<lparr>carrier = carrier H, mult = (\<otimes>\<^bsub>H\<^esub>), one = \<one>\<^bsub>H\<^esub>\<rparr>)})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<exists>\<phi>. \<phi> \<in> Group.iso G H) = (\<exists>\<phi>. \<phi> \<in> Group.iso (monoid.truncate G) (monoid.truncate H))

goal (1 subgoal):
 1. (\<exists>\<phi>. \<phi> \<in> Group.iso G H) = (group.iso_class G = group.iso_class H)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<exists>\<phi>. \<phi> \<in> Group.iso G H) = (\<exists>\<phi>. \<phi> \<in> Group.iso (monoid.truncate G) (monoid.truncate H))

goal (1 subgoal):
 1. (\<exists>\<phi>. \<phi> \<in> Group.iso G H) = (group.iso_class G = group.iso_class H)
[PROOF STEP]
have "\<dots> = group_iso_rel (Abs_group (monoid.truncate G)) (Abs_group (monoid.truncate H))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>\<phi>. \<phi> \<in> Group.iso (monoid.truncate G) (monoid.truncate H)) = group_iso_rel (Abs_group (monoid.truncate G)) (Abs_group (monoid.truncate H))
[PROOF STEP]
unfolding group_iso_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>\<phi>. \<phi> \<in> Group.iso (monoid.truncate G) (monoid.truncate H)) = (\<exists>\<phi>. \<phi> \<in> Group.iso (Rep_group (Abs_group (monoid.truncate G))) (Rep_group (Abs_group (monoid.truncate H))))
[PROOF STEP]
using groups group.Abs_group_inverse
[PROOF STATE]
proof (prove)
using this:
Group.group (monoid.truncate G)
Group.group (monoid.truncate H)
?y \<in> {G. Group.group G} \<Longrightarrow> Rep_group (Abs_group ?y) = ?y

goal (1 subgoal):
 1. (\<exists>\<phi>. \<phi> \<in> Group.iso (monoid.truncate G) (monoid.truncate H)) = (\<exists>\<phi>. \<phi> \<in> Group.iso (Rep_group (Abs_group (monoid.truncate G))) (Rep_group (Abs_group (monoid.truncate H))))
[PROOF STEP]
by (metis mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
(\<exists>\<phi>. \<phi> \<in> Group.iso (monoid.truncate G) (monoid.truncate H)) = group_iso_rel (Abs_group (monoid.truncate G)) (Abs_group (monoid.truncate H))

goal (1 subgoal):
 1. (\<exists>\<phi>. \<phi> \<in> Group.iso G H) = (group.iso_class G = group.iso_class H)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<exists>\<phi>. \<phi> \<in> Group.iso (monoid.truncate G) (monoid.truncate H)) = group_iso_rel (Abs_group (monoid.truncate G)) (Abs_group (monoid.truncate H))

goal (1 subgoal):
 1. (\<exists>\<phi>. \<phi> \<in> Group.iso G H) = (group.iso_class G = group.iso_class H)
[PROOF STEP]
have "\<dots> = (group.iso_class G = group.iso_class H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. group_iso_rel (Abs_group (monoid.truncate G)) (Abs_group (monoid.truncate H)) = (group.iso_class G = group.iso_class H)
[PROOF STEP]
using group.iso_class_def assms group_iso_class.abs_eq_iff
[PROOF STATE]
proof (prove)
using this:
Group.group ?G \<Longrightarrow> group.iso_class ?G = Abs_group_iso (Abs_group (monoid.truncate ?G))
Group.group G
Group.group H
(Abs_group_iso ?x = Abs_group_iso ?y) = group_iso_rel ?x ?y

goal (1 subgoal):
 1. group_iso_rel (Abs_group (monoid.truncate G)) (Abs_group (monoid.truncate H)) = (group.iso_class G = group.iso_class H)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
group_iso_rel (Abs_group (monoid.truncate G)) (Abs_group (monoid.truncate H)) = (group.iso_class G = group.iso_class H)

goal (1 subgoal):
 1. (\<exists>\<phi>. \<phi> \<in> Group.iso G H) = (group.iso_class G = group.iso_class H)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<exists>\<phi>. \<phi> \<in> Group.iso G H) = (group.iso_class G = group.iso_class H)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<exists>\<phi>. \<phi> \<in> Group.iso G H) = (group.iso_class G = group.iso_class H)

goal (1 subgoal):
 1. (\<exists>\<phi>. \<phi> \<in> Group.iso G H) = (group.iso_class G = group.iso_class H)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<exists>\<phi>. \<phi> \<in> Group.iso G H) = (group.iso_class G = group.iso_class H)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<Delta>\<^sub>\<epsilon>_states: "\<Delta>\<^sub>\<epsilon>_set \<A> \<B> \<subseteq> fset (\<Q> \<A> |\<times>| \<Q> \<B>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta>\<^sub>\<epsilon>_set \<A> \<B> \<subseteq> fset (\<Q> \<A> |\<times>| \<Q> \<B>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Delta>\<^sub>\<epsilon>_set \<A> \<B> \<subseteq> fset (\<Q> \<A> |\<times>| \<Q> \<B>)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Delta>\<^sub>\<epsilon>_set \<A> \<B> \<subseteq> fset (\<Q> \<A> |\<times>| \<Q> \<B>)
[PROOF STEP]
fix p q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Delta>\<^sub>\<epsilon>_set \<A> \<B> \<subseteq> fset (\<Q> \<A> |\<times>| \<Q> \<B>)
[PROOF STEP]
assume "(p, q) \<in> \<Delta>\<^sub>\<epsilon>_set \<A> \<B>"
[PROOF STATE]
proof (state)
this:
(p, q) \<in> \<Delta>\<^sub>\<epsilon>_set \<A> \<B>

goal (1 subgoal):
 1. \<Delta>\<^sub>\<epsilon>_set \<A> \<B> \<subseteq> fset (\<Q> \<A> |\<times>| \<Q> \<B>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(p, q) \<in> \<Delta>\<^sub>\<epsilon>_set \<A> \<B>
[PROOF STEP]
have "(p, q) \<in> fset (\<Q> \<A> |\<times>| \<Q> \<B>)"
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> \<Delta>\<^sub>\<epsilon>_set \<A> \<B>

goal (1 subgoal):
 1. (p, q) \<in> fset (\<Q> \<A> |\<times>| \<Q> \<B>)
[PROOF STEP]
by (induct) (auto dest: rule_statesD eps_statesD simp flip: fmember.rep_eq)
[PROOF STATE]
proof (state)
this:
(p, q) \<in> fset (\<Q> \<A> |\<times>| \<Q> \<B>)

goal (1 subgoal):
 1. \<Delta>\<^sub>\<epsilon>_set \<A> \<B> \<subseteq> fset (\<Q> \<A> |\<times>| \<Q> \<B>)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?p2, ?q2) \<in> \<Delta>\<^sub>\<epsilon>_set \<A> \<B> \<Longrightarrow> (?p2, ?q2) \<in> fset (\<Q> \<A> |\<times>| \<Q> \<B>)

goal (1 subgoal):
 1. \<Delta>\<^sub>\<epsilon>_set \<A> \<B> \<subseteq> fset (\<Q> \<A> |\<times>| \<Q> \<B>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(?p2, ?q2) \<in> \<Delta>\<^sub>\<epsilon>_set \<A> \<B> \<Longrightarrow> (?p2, ?q2) \<in> fset (\<Q> \<A> |\<times>| \<Q> \<B>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(?p2, ?q2) \<in> \<Delta>\<^sub>\<epsilon>_set \<A> \<B> \<Longrightarrow> (?p2, ?q2) \<in> fset (\<Q> \<A> |\<times>| \<Q> \<B>)

goal (1 subgoal):
 1. \<Delta>\<^sub>\<epsilon>_set \<A> \<B> \<subseteq> fset (\<Q> \<A> |\<times>| \<Q> \<B>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Delta>\<^sub>\<epsilon>_set \<A> \<B> \<subseteq> fset (\<Q> \<A> |\<times>| \<Q> \<B>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_\<Delta>\<^sub>\<epsilon> [simp]: "finite (\<Delta>\<^sub>\<epsilon>_set \ \)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (\<Delta>\<^sub>\<epsilon>_set \ \)
[PROOF STEP]
using finite_subset[OF \<Delta>\<^sub>\<epsilon>_states]
[PROOF STATE]
proof (prove)
using this:
finite (fset (\<Q> ?\1 |\<times>| \<Q> ?\1)) \<Longrightarrow> finite (\<Delta>\<^sub>\<epsilon>_set ?\1 ?\1)

goal (1 subgoal):
 1. finite (\<Delta>\<^sub>\<epsilon>_set \ \)
[PROOF STEP]
by simp


[STATEMENT]
lemma finite_alt_def [simp]:
  "finite {(\<alpha>, \<beta>). (\<exists>t. ground t \<and> \<alpha> |\<in>| ta_der \<A> t \<and> \<beta> |\<in>| ta_der \<B> t)}" (is "finite ?S")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {(\<alpha>, \<beta>). \<exists>t. ground t \<and> \<alpha> |\<in>| ta_der \<A> t \<and> \<beta> |\<in>| ta_der \<B> t}
[PROOF STEP]
by (auto dest: ground_ta_der_states[THEN fsubsetD] simp flip: fmember.rep_eq
           intro!: finite_subset[of ?S "fset (\<Q> \<A> |\<times>| \<Q> \<B>)"])


[STATEMENT]
lemma \<Delta>\<^sub>\<epsilon>_fmember:
  "(p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \<A> \<B> \<longleftrightarrow> (\<exists>t. ground t \<and> p |\<in>| ta_der \<A> t \<and> q |\<in>| ta_der \<B> t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \<A> \<B>) = (\<exists>t. ground t \<and> p |\<in>| ta_der \<A> t \<and> q |\<in>| ta_der \<B> t)
[PROOF STEP]
by (auto simp: \<Delta>\<^sub>\<epsilon>_def')


[STATEMENT]
lemma gtt_syms_GTT_comp:
  "gtt_syms (GTT_comp A B) = gtt_syms A |\<union>| gtt_syms B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gtt_syms (GTT_comp A B) = gtt_syms A |\<union>| gtt_syms B
[PROOF STEP]
by (auto simp: GTT_comp_def ta_sig_def Let_def)


[STATEMENT]
lemma \<Delta>\<^sub>\<epsilon>_statesD:
  "(p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \<A> \<B> \<Longrightarrow> p |\<in>| \<Q> \<A>"
  "(p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \<A> \<B> \<Longrightarrow> q |\<in>| \<Q> \<B>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \<A> \<B> \<Longrightarrow> p |\<in>| \<Q> \<A>) &&& ((p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \<A> \<B> \<Longrightarrow> q |\<in>| \<Q> \<B>)
[PROOF STEP]
using subsetD[OF \<Delta>\<^sub>\<epsilon>_states, of "(p, q)" \<A> \<B>]
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> \<Delta>\<^sub>\<epsilon>_set \<A> \<B> \<Longrightarrow> (p, q) \<in> fset (\<Q> \<A> |\<times>| \<Q> \<B>)

goal (1 subgoal):
 1. ((p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \<A> \<B> \<Longrightarrow> p |\<in>| \<Q> \<A>) &&& ((p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \<A> \<B> \<Longrightarrow> q |\<in>| \<Q> \<B>)
[PROOF STEP]
by (auto simp flip: \<Delta>\<^sub>\<epsilon>.rep_eq fmember.rep_eq)


[STATEMENT]
lemma \<Delta>\<^sub>\<epsilon>_statesD':
  "q |\<in>| eps_states (\<Delta>\<^sub>\<epsilon> \<A> \<B>) \<Longrightarrow> q |\<in>| \<Q> \<A> |\<union>| \<Q> \<B>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q |\<in>| eps_states (\<Delta>\<^sub>\<epsilon> \<A> \<B>) \<Longrightarrow> q |\<in>| \<Q> \<A> |\<union>| \<Q> \<B>
[PROOF STEP]
by (auto simp: eps_states_def fmember.abs_eq dest: \<Delta>\<^sub>\<epsilon>_statesD)


[STATEMENT]
lemma \<Delta>\<^sub>\<epsilon>_swap:
  "prod.swap p |\<in>| \<Delta>\<^sub>\<epsilon> \<A> \<B> \<longleftrightarrow> p |\<in>| \<Delta>\<^sub>\<epsilon> \<B> \<A>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (prod.swap p |\<in>| \<Delta>\<^sub>\<epsilon> \<A> \<B>) = (p |\<in>| \<Delta>\<^sub>\<epsilon> \<B> \<A>)
[PROOF STEP]
by (auto simp: \<Delta>\<^sub>\<epsilon>_def')


[STATEMENT]
lemma \<Delta>\<^sub>\<epsilon>_inverse [simp]:
  "(\<Delta>\<^sub>\<epsilon> \<A> \<B>)|\<inverse>| = \<Delta>\<^sub>\<epsilon> \<B> \<A>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Delta>\<^sub>\<epsilon> \<A> \<B>)|\<inverse>| = \<Delta>\<^sub>\<epsilon> \<B> \<A>
[PROOF STEP]
by (auto simp: \<Delta>\<^sub>\<epsilon>_def')


[STATEMENT]
lemma gtt_states_comp_union:
  "gtt_states (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2) |\<subseteq>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gtt_states (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2) |\<subseteq>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2
[PROOF STEP]
proof (intro fsubsetI, goal_cases lr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x |\<in>| gtt_states (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2) \<Longrightarrow> x |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2
[PROOF STEP]
case (lr q)
[PROOF STATE]
proof (state)
this:
q |\<in>| gtt_states (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)

goal (1 subgoal):
 1. \<And>x. x |\<in>| gtt_states (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2) \<Longrightarrow> x |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q |\<in>| gtt_states (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
q |\<in>| gtt_states (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)

goal (1 subgoal):
 1. q |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2
[PROOF STEP]
by (auto simp: GTT_comp_def gtt_states_def \<Q>_def dest: \<Delta>\<^sub>\<epsilon>_statesD')
[PROOF STATE]
proof (state)
this:
q |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma GTT_comp_swap [simp]:
  "GTT_comp (prod.swap \<G>\<^sub>2) (prod.swap \<G>\<^sub>1) = prod.swap (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. GTT_comp (prod.swap \<G>\<^sub>2) (prod.swap \<G>\<^sub>1) = prod.swap (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)
[PROOF STEP]
by (simp add: GTT_comp_def ac_simps)


[STATEMENT]
lemma gtt_comp_complete_semi:
  assumes s: "q |\<in>| gta_der (fst \<G>\<^sub>1) s" and u: "q |\<in>| gta_der (snd \<G>\<^sub>1) u" and ut: "gtt_accept \<G>\<^sub>2 u t"
  shows "q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s" "q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s &&& q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
[PROOF STEP]
proof (goal_cases L R)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s
 2. q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
[PROOF STEP]
let ?\<G> = "GTT_comp \<G>\<^sub>1 \<G>\<^sub>2"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s
 2. q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
[PROOF STEP]
have  sub1l: "rules (fst \<G>\<^sub>1) |\<subseteq>| rules (fst ?\<G>)" "eps (fst \<G>\<^sub>1) |\<subseteq>| eps (fst ?\<G>)"
    and sub1r: "rules (snd \<G>\<^sub>1) |\<subseteq>| rules (snd ?\<G>)" "eps (snd \<G>\<^sub>1) |\<subseteq>| eps (snd ?\<G>)"
    and sub2r: "rules (snd \<G>\<^sub>2) |\<subseteq>| rules (snd ?\<G>)" "eps (snd \<G>\<^sub>2) |\<subseteq>| eps (snd ?\<G>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rules (fst \<G>\<^sub>1) |\<subseteq>| rules (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) &&& eps (fst \<G>\<^sub>1) |\<subseteq>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))) &&& (rules (snd \<G>\<^sub>1) |\<subseteq>| rules (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) &&& eps (snd \<G>\<^sub>1) |\<subseteq>| eps (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))) &&& rules (snd \<G>\<^sub>2) |\<subseteq>| rules (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) &&& eps (snd \<G>\<^sub>2) |\<subseteq>| eps (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
[PROOF STEP]
by (auto simp: GTT_comp_def)
[PROOF STATE]
proof (state)
this:
rules (fst \<G>\<^sub>1) |\<subseteq>| rules (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
eps (fst \<G>\<^sub>1) |\<subseteq>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
rules (snd \<G>\<^sub>1) |\<subseteq>| rules (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
eps (snd \<G>\<^sub>1) |\<subseteq>| eps (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
rules (snd \<G>\<^sub>2) |\<subseteq>| rules (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
eps (snd \<G>\<^sub>2) |\<subseteq>| eps (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))

goal (2 subgoals):
 1. q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s
 2. q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
rules (fst \<G>\<^sub>1) |\<subseteq>| rules (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
eps (fst \<G>\<^sub>1) |\<subseteq>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
rules (snd \<G>\<^sub>1) |\<subseteq>| rules (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
eps (snd \<G>\<^sub>1) |\<subseteq>| eps (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
rules (snd \<G>\<^sub>2) |\<subseteq>| rules (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
eps (snd \<G>\<^sub>2) |\<subseteq>| eps (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))

goal (2 subgoals):
 1. q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s
 2. q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
[PROOF STEP]
case L
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s
 2. q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s
[PROOF STEP]
using s ta_der_mono[OF sub1l]
[PROOF STATE]
proof (prove)
using this:
q |\<in>| gta_der (fst \<G>\<^sub>1) s
ta_der (fst \<G>\<^sub>1) ?t |\<subseteq>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) ?t

goal (1 subgoal):
 1. q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s
[PROOF STEP]
by (auto simp: gta_der_def)
[PROOF STATE]
proof (state)
this:
q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s

goal (1 subgoal):
 1. q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
[PROOF STEP]
case R
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
[PROOF STEP]
using ut u
[PROOF STATE]
proof (prove)
using this:
gtt_accept \<G>\<^sub>2 u t
q |\<in>| gta_der (snd \<G>\<^sub>1) u

goal (1 subgoal):
 1. q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
[PROOF STEP]
unfolding gtt_accept_def
[PROOF STATE]
proof (prove)
using this:
(u, t) \<in> gtt_lang \<G>\<^sub>2
q |\<in>| gta_der (snd \<G>\<^sub>1) u

goal (1 subgoal):
 1. q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
[PROOF STEP]
proof (induct arbitrary: q s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s t q. \<lbrakk>(s, t) \<in> agtt_lang \<G>\<^sub>2; q |\<in>| gta_der (snd \<G>\<^sub>1) s\<rbrakk> \<Longrightarrow> q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
 2. \<And>ss ts f q. \<lbrakk>length ss = length ts; \<forall>i<length ts. (ss ! i, ts ! i) \<in> gtt_lang \<G>\<^sub>2 \<and> (\<forall>x. x |\<in>| gta_der (snd \<G>\<^sub>1) (ss ! i) \<longrightarrow> x |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (ts ! i)); (f, length ss) \<in> UNIV; q |\<in>| gta_der (snd \<G>\<^sub>1) (GFun f ss)\<rbrakk> \<Longrightarrow> q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (GFun f ts)
[PROOF STEP]
case (base s t)
[PROOF STATE]
proof (state)
this:
(s, t) \<in> agtt_lang \<G>\<^sub>2
q |\<in>| gta_der (snd \<G>\<^sub>1) s

goal (2 subgoals):
 1. \<And>s t q. \<lbrakk>(s, t) \<in> agtt_lang \<G>\<^sub>2; q |\<in>| gta_der (snd \<G>\<^sub>1) s\<rbrakk> \<Longrightarrow> q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
 2. \<And>ss ts f q. \<lbrakk>length ss = length ts; \<forall>i<length ts. (ss ! i, ts ! i) \<in> gtt_lang \<G>\<^sub>2 \<and> (\<forall>x. x |\<in>| gta_der (snd \<G>\<^sub>1) (ss ! i) \<longrightarrow> x |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (ts ! i)); (f, length ss) \<in> UNIV; q |\<in>| gta_der (snd \<G>\<^sub>1) (GFun f ss)\<rbrakk> \<Longrightarrow> q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (GFun f ts)
[PROOF STEP]
from base(1)
[PROOF STATE]
proof (chain)
picking this:
(s, t) \<in> agtt_lang \<G>\<^sub>2
[PROOF STEP]
obtain p where p: "p |\<in>| gta_der (fst \<G>\<^sub>2) s" "p |\<in>| gta_der (snd \<G>\<^sub>2) t"
[PROOF STATE]
proof (prove)
using this:
(s, t) \<in> agtt_lang \<G>\<^sub>2

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p |\<in>| gta_der (fst \<G>\<^sub>2) s; p |\<in>| gta_der (snd \<G>\<^sub>2) t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: agtt_lang_def)
[PROOF STATE]
proof (state)
this:
p |\<in>| gta_der (fst \<G>\<^sub>2) s
p |\<in>| gta_der (snd \<G>\<^sub>2) t

goal (2 subgoals):
 1. \<And>s t q. \<lbrakk>(s, t) \<in> agtt_lang \<G>\<^sub>2; q |\<in>| gta_der (snd \<G>\<^sub>1) s\<rbrakk> \<Longrightarrow> q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
 2. \<And>ss ts f q. \<lbrakk>length ss = length ts; \<forall>i<length ts. (ss ! i, ts ! i) \<in> gtt_lang \<G>\<^sub>2 \<and> (\<forall>x. x |\<in>| gta_der (snd \<G>\<^sub>1) (ss ! i) \<longrightarrow> x |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (ts ! i)); (f, length ss) \<in> UNIV; q |\<in>| gta_der (snd \<G>\<^sub>1) (GFun f ss)\<rbrakk> \<Longrightarrow> q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (GFun f ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p |\<in>| gta_der (fst \<G>\<^sub>2) s
p |\<in>| gta_der (snd \<G>\<^sub>2) t
[PROOF STEP]
have "(p, q) |\<in>| eps (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))"
[PROOF STATE]
proof (prove)
using this:
p |\<in>| gta_der (fst \<G>\<^sub>2) s
p |\<in>| gta_der (snd \<G>\<^sub>2) t

goal (1 subgoal):
 1. (p, q) |\<in>| eps (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
[PROOF STEP]
using \<Delta>\<^sub>\<epsilon>_fmember[of p q "fst \<G>\<^sub>2" "snd \<G>\<^sub>1"] base(2)
[PROOF STATE]
proof (prove)
using this:
p |\<in>| gta_der (fst \<G>\<^sub>2) s
p |\<in>| gta_der (snd \<G>\<^sub>2) t
((p, q) |\<in>| \<Delta>\<^sub>\<epsilon> (fst \<G>\<^sub>2) (snd \<G>\<^sub>1)) = (\<exists>t. ground t \<and> p |\<in>| ta_der (fst \<G>\<^sub>2) t \<and> q |\<in>| ta_der (snd \<G>\<^sub>1) t)
q |\<in>| gta_der (snd \<G>\<^sub>1) s

goal (1 subgoal):
 1. (p, q) |\<in>| eps (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
[PROOF STEP]
by (auto simp: GTT_comp_def gta_der_def)
[PROOF STATE]
proof (state)
this:
(p, q) |\<in>| eps (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))

goal (2 subgoals):
 1. \<And>s t q. \<lbrakk>(s, t) \<in> agtt_lang \<G>\<^sub>2; q |\<in>| gta_der (snd \<G>\<^sub>1) s\<rbrakk> \<Longrightarrow> q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
 2. \<And>ss ts f q. \<lbrakk>length ss = length ts; \<forall>i<length ts. (ss ! i, ts ! i) \<in> gtt_lang \<G>\<^sub>2 \<and> (\<forall>x. x |\<in>| gta_der (snd \<G>\<^sub>1) (ss ! i) \<longrightarrow> x |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (ts ! i)); (f, length ss) \<in> UNIV; q |\<in>| gta_der (snd \<G>\<^sub>1) (GFun f ss)\<rbrakk> \<Longrightarrow> q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (GFun f ts)
[PROOF STEP]
from ta_der_eps[OF this]
[PROOF STATE]
proof (chain)
picking this:
p |\<in>| ta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) ?t \<Longrightarrow> q |\<in>| ta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) ?t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p |\<in>| ta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) ?t \<Longrightarrow> q |\<in>| ta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) ?t

goal (1 subgoal):
 1. q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
[PROOF STEP]
using p ta_der_mono[OF sub2r]
[PROOF STATE]
proof (prove)
using this:
p |\<in>| ta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) ?t \<Longrightarrow> q |\<in>| ta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) ?t
p |\<in>| gta_der (fst \<G>\<^sub>2) s
p |\<in>| gta_der (snd \<G>\<^sub>2) t
ta_der (snd \<G>\<^sub>2) ?t |\<subseteq>| ta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) ?t

goal (1 subgoal):
 1. q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
[PROOF STEP]
by (auto simp add: gta_der_def)
[PROOF STATE]
proof (state)
this:
q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t

goal (1 subgoal):
 1. \<And>ss ts f q. \<lbrakk>length ss = length ts; \<forall>i<length ts. (ss ! i, ts ! i) \<in> gtt_lang \<G>\<^sub>2 \<and> (\<forall>x. x |\<in>| gta_der (snd \<G>\<^sub>1) (ss ! i) \<longrightarrow> x |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (ts ! i)); (f, length ss) \<in> UNIV; q |\<in>| gta_der (snd \<G>\<^sub>1) (GFun f ss)\<rbrakk> \<Longrightarrow> q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (GFun f ts)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ss ts f q. \<lbrakk>length ss = length ts; \<forall>i<length ts. (ss ! i, ts ! i) \<in> gtt_lang \<G>\<^sub>2 \<and> (\<forall>x. x |\<in>| gta_der (snd \<G>\<^sub>1) (ss ! i) \<longrightarrow> x |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (ts ! i)); (f, length ss) \<in> UNIV; q |\<in>| gta_der (snd \<G>\<^sub>1) (GFun f ss)\<rbrakk> \<Longrightarrow> q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (GFun f ts)
[PROOF STEP]
case (step ss ts f)
[PROOF STATE]
proof (state)
this:
length ss = length ts
\<forall>i<length ts. (ss ! i, ts ! i) \<in> gtt_lang \<G>\<^sub>2 \<and> (\<forall>x. x |\<in>| gta_der (snd \<G>\<^sub>1) (ss ! i) \<longrightarrow> x |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (ts ! i))
(f, length ss) \<in> UNIV
q |\<in>| gta_der (snd \<G>\<^sub>1) (GFun f ss)

goal (1 subgoal):
 1. \<And>ss ts f q. \<lbrakk>length ss = length ts; \<forall>i<length ts. (ss ! i, ts ! i) \<in> gtt_lang \<G>\<^sub>2 \<and> (\<forall>x. x |\<in>| gta_der (snd \<G>\<^sub>1) (ss ! i) \<longrightarrow> x |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (ts ! i)); (f, length ss) \<in> UNIV; q |\<in>| gta_der (snd \<G>\<^sub>1) (GFun f ss)\<rbrakk> \<Longrightarrow> q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (GFun f ts)
[PROOF STEP]
from step(1, 4)
[PROOF STATE]
proof (chain)
picking this:
length ss = length ts
q |\<in>| gta_der (snd \<G>\<^sub>1) (GFun f ss)
[PROOF STEP]
obtain ps p where "TA_rule f ps p |\<in>| rules (snd \<G>\<^sub>1)" "p = q \<or> (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|"
        "length ps = length ts" "\<And>i. i < length ts \<Longrightarrow> ps ! i |\<in>| gta_der (snd \<G>\<^sub>1) (ss ! i)"
[PROOF STATE]
proof (prove)
using this:
length ss = length ts
q |\<in>| gta_der (snd \<G>\<^sub>1) (GFun f ss)

goal (1 subgoal):
 1. (\<And>ps p. \<lbrakk>f ps \<rightarrow> p |\<in>| rules (snd \<G>\<^sub>1); p = q \<or> (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|; length ps = length ts; \<And>i. i < length ts \<Longrightarrow> ps ! i |\<in>| gta_der (snd \<G>\<^sub>1) (ss ! i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding gta_der_def
[PROOF STATE]
proof (prove)
using this:
length ss = length ts
q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm (GFun f ss))

goal (1 subgoal):
 1. (\<And>ps p. \<lbrakk>f ps \<rightarrow> p |\<in>| rules (snd \<G>\<^sub>1); p = q \<or> (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|; length ps = length ts; \<And>i. i < length ts \<Longrightarrow> ps ! i |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm (ss ! i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f ps \<rightarrow> p |\<in>| rules (snd \<G>\<^sub>1)
p = q \<or> (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|
length ps = length ts
?i < length ts \<Longrightarrow> ps ! ?i |\<in>| gta_der (snd \<G>\<^sub>1) (ss ! ?i)

goal (1 subgoal):
 1. \<And>ss ts f q. \<lbrakk>length ss = length ts; \<forall>i<length ts. (ss ! i, ts ! i) \<in> gtt_lang \<G>\<^sub>2 \<and> (\<forall>x. x |\<in>| gta_der (snd \<G>\<^sub>1) (ss ! i) \<longrightarrow> x |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (ts ! i)); (f, length ss) \<in> UNIV; q |\<in>| gta_der (snd \<G>\<^sub>1) (GFun f ss)\<rbrakk> \<Longrightarrow> q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (GFun f ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f ps \<rightarrow> p |\<in>| rules (snd \<G>\<^sub>1)
p = q \<or> (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|
length ps = length ts
?i < length ts \<Longrightarrow> ps ! ?i |\<in>| gta_der (snd \<G>\<^sub>1) (ss ! ?i)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
f ps \<rightarrow> p |\<in>| rules (snd \<G>\<^sub>1)
p = q \<or> (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|
length ps = length ts
?i < length ts \<Longrightarrow> ps ! ?i |\<in>| gta_der (snd \<G>\<^sub>1) (ss ! ?i)

goal (1 subgoal):
 1. q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (GFun f ts)
[PROOF STEP]
using step(1, 2) sub1r(1) ftrancl_mono[OF _ sub1r(2)]
[PROOF STATE]
proof (prove)
using this:
f ps \<rightarrow> p |\<in>| rules (snd \<G>\<^sub>1)
p = q \<or> (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|
length ps = length ts
?i < length ts \<Longrightarrow> ps ! ?i |\<in>| gta_der (snd \<G>\<^sub>1) (ss ! ?i)
length ss = length ts
\<forall>i<length ts. (ss ! i, ts ! i) \<in> gtt_lang \<G>\<^sub>2 \<and> (\<forall>x. x |\<in>| gta_der (snd \<G>\<^sub>1) (ss ! i) \<longrightarrow> x |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (ts ! i))
rules (snd \<G>\<^sub>1) |\<subseteq>| rules (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
?p |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+| \<Longrightarrow> ?p |\<in>| (eps (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|

goal (1 subgoal):
 1. q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (GFun f ts)
[PROOF STEP]
by (auto simp: gta_der_def intro!: exI[of _ p] exI[of _ ps])
[PROOF STATE]
proof (state)
this:
q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (GFun f ts)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gtt_comp_acomplete:
  "gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2) \<subseteq> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2) \<subseteq> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)
[PROOF STEP]
proof (intro subrelI, goal_cases LR)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2) \<Longrightarrow> (x, y) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)
[PROOF STEP]
case (LR s t)
[PROOF STATE]
proof (state)
this:
(s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)

goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2) \<Longrightarrow> (x, y) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
consider
      q u where "q |\<in>| gta_der (fst \<G>\<^sub>1) s" "q |\<in>| gta_der (snd \<G>\<^sub>1) u" "gtt_accept \<G>\<^sub>2 u t"
    | q u where "q |\<in>| gta_der (snd \<G>\<^sub>2) t" "q |\<in>| gta_der (fst \<G>\<^sub>2) u" "gtt_accept \<G>\<^sub>1 s u"
[PROOF STATE]
proof (prove)
using this:
(s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)

goal (1 subgoal):
 1. \<lbrakk>\<And>q u. \<lbrakk>q |\<in>| gta_der (fst \<G>\<^sub>1) s; q |\<in>| gta_der (snd \<G>\<^sub>1) u; gtt_accept \<G>\<^sub>2 u t\<rbrakk> \<Longrightarrow> thesis; \<And>q u. \<lbrakk>q |\<in>| gta_der (snd \<G>\<^sub>2) t; q |\<in>| gta_der (fst \<G>\<^sub>2) u; gtt_accept \<G>\<^sub>1 s u\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: gcomp_rel_def gtt_accept_def elim!: agtt_langE)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>q u. \<lbrakk>q |\<in>| gta_der (fst \<G>\<^sub>1) s; q |\<in>| gta_der (snd \<G>\<^sub>1) u; gtt_accept \<G>\<^sub>2 u t\<rbrakk> \<Longrightarrow> ?thesis; \<And>q u. \<lbrakk>q |\<in>| gta_der (snd \<G>\<^sub>2) t; q |\<in>| gta_der (fst \<G>\<^sub>2) u; gtt_accept \<G>\<^sub>1 s u\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2) \<Longrightarrow> (x, y) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>q u. \<lbrakk>q |\<in>| gta_der (fst \<G>\<^sub>1) s; q |\<in>| gta_der (snd \<G>\<^sub>1) u; gtt_accept \<G>\<^sub>2 u t\<rbrakk> \<Longrightarrow> ?thesis; \<And>q u. \<lbrakk>q |\<in>| gta_der (snd \<G>\<^sub>2) t; q |\<in>| gta_der (fst \<G>\<^sub>2) u; gtt_accept \<G>\<^sub>1 s u\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>q u. \<lbrakk>q |\<in>| gta_der (fst \<G>\<^sub>1) s; q |\<in>| gta_der (snd \<G>\<^sub>1) u; gtt_accept \<G>\<^sub>2 u t\<rbrakk> \<Longrightarrow> ?thesis; \<And>q u. \<lbrakk>q |\<in>| gta_der (snd \<G>\<^sub>2) t; q |\<in>| gta_der (fst \<G>\<^sub>2) u; gtt_accept \<G>\<^sub>1 s u\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (s, t) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>q u. \<lbrakk>q |\<in>| gta_der (fst \<G>\<^sub>1) s; q |\<in>| gta_der (snd \<G>\<^sub>1) u; gtt_accept \<G>\<^sub>2 u t\<rbrakk> \<Longrightarrow> (s, t) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)
 2. \<And>q u. \<lbrakk>q |\<in>| gta_der (snd \<G>\<^sub>2) t; q |\<in>| gta_der (fst \<G>\<^sub>2) u; gtt_accept \<G>\<^sub>1 s u\<rbrakk> \<Longrightarrow> (s, t) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
q |\<in>| gta_der (fst \<G>\<^sub>1) s
q |\<in>| gta_der (snd \<G>\<^sub>1) u
gtt_accept \<G>\<^sub>2 u t

goal (2 subgoals):
 1. \<And>q u. \<lbrakk>q |\<in>| gta_der (fst \<G>\<^sub>1) s; q |\<in>| gta_der (snd \<G>\<^sub>1) u; gtt_accept \<G>\<^sub>2 u t\<rbrakk> \<Longrightarrow> (s, t) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)
 2. \<And>q u. \<lbrakk>q |\<in>| gta_der (snd \<G>\<^sub>2) t; q |\<in>| gta_der (fst \<G>\<^sub>2) u; gtt_accept \<G>\<^sub>1 s u\<rbrakk> \<Longrightarrow> (s, t) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s, t) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)
[PROOF STEP]
using gtt_comp_complete_semi[OF 1]
[PROOF STATE]
proof (prove)
using this:
q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s
q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t

goal (1 subgoal):
 1. (s, t) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)
[PROOF STEP]
by (auto simp: agtt_lang_def gta_der_def)
[PROOF STATE]
proof (state)
this:
(s, t) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)

goal (1 subgoal):
 1. \<And>q u. \<lbrakk>q |\<in>| gta_der (snd \<G>\<^sub>2) t; q |\<in>| gta_der (fst \<G>\<^sub>2) u; gtt_accept \<G>\<^sub>1 s u\<rbrakk> \<Longrightarrow> (s, t) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q u. \<lbrakk>q |\<in>| gta_der (snd \<G>\<^sub>2) t; q |\<in>| gta_der (fst \<G>\<^sub>2) u; gtt_accept \<G>\<^sub>1 s u\<rbrakk> \<Longrightarrow> (s, t) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
q |\<in>| gta_der (snd \<G>\<^sub>2) t
q |\<in>| gta_der (fst \<G>\<^sub>2) u
gtt_accept \<G>\<^sub>1 s u

goal (1 subgoal):
 1. \<And>q u. \<lbrakk>q |\<in>| gta_der (snd \<G>\<^sub>2) t; q |\<in>| gta_der (fst \<G>\<^sub>2) u; gtt_accept \<G>\<^sub>1 s u\<rbrakk> \<Longrightarrow> (s, t) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s, t) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)
[PROOF STEP]
using gtt_comp_complete_semi'[OF 2]
[PROOF STATE]
proof (prove)
using this:
q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s

goal (1 subgoal):
 1. (s, t) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)
[PROOF STEP]
by (auto simp: agtt_lang_def gta_der_def)
[PROOF STATE]
proof (state)
this:
(s, t) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(s, t) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)

goal:
No subgoals!
[PROOF STEP]
qed