[STATEMENT]
lemma degen_run_find_acc_aux:
    assumes NN0[simp]: "num_acc \<noteq> 0"
    assumes AR: "degen.is_acc_run T m r"
    assumes A: "r i = (q,0)" "0 \<in> acc q" "n<num_acc"
    shows "\<exists>j qj. i\<le>j \<and> r j = (qj,n) \<and> n \<in> acc qj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j qj. i \<le> j \<and> r j = (qj, n) \<and> n \<in> acc qj
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>j qj. i \<le> j \<and> r j = (qj, n) \<and> n \<in> acc qj
[PROOF STEP]
from AR
[PROOF STATE]
proof (chain)
picking this:
b_graph.is_acc_run (degeneralize_ext m) r
[PROOF STEP]
have R: "degen.is_run T m r"
      and ACC: "\<exists>\<^sub>\<infinity>i. r i \<in> degen.F T m"
[PROOF STATE]
proof (prove)
using this:
b_graph.is_acc_run (degeneralize_ext m) r

goal (1 subgoal):
 1. graph_defs.is_run (degeneralize_ext m) r &&& \<exists>\<^sub>\<infinity>i. r i \<in> bg_F (degeneralize_ext m)
[PROOF STEP]
(*and ACC: "limit r \<inter> bg_F (degeneralize_ext ecnv) \<noteq> {}"*)
[PROOF STATE]
proof (prove)
using this:
b_graph.is_acc_run (degeneralize_ext m) r

goal (1 subgoal):
 1. graph_defs.is_run (degeneralize_ext m) r &&& \<exists>\<^sub>\<infinity>i. r i \<in> bg_F (degeneralize_ext m)
[PROOF STEP]
unfolding degen.is_acc_run_def degen.is_acc_def
[PROOF STATE]
proof (prove)
using this:
graph_defs.is_run (degeneralize_ext m) r \<and> (\<exists>\<^sub>\<infinity>i. r i \<in> bg_F (degeneralize_ext m))

goal (1 subgoal):
 1. graph_defs.is_run (degeneralize_ext m) r &&& \<exists>\<^sub>\<infinity>i. r i \<in> bg_F (degeneralize_ext m)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
graph_defs.is_run (degeneralize_ext m) r
\<exists>\<^sub>\<infinity>i. r i \<in> bg_F (degeneralize_ext m)

goal (1 subgoal):
 1. \<exists>j qj. i \<le> j \<and> r j = (qj, n) \<and> n \<in> acc qj
[PROOF STEP]
from ACC
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<^sub>\<infinity>i. r i \<in> bg_F (degeneralize_ext m)
[PROOF STEP]
have ACC': "\<forall>i. \<exists>j>i. r j \<in> degen.F T m"
[PROOF STATE]
proof (prove)
using this:
\<exists>\<^sub>\<infinity>i. r i \<in> bg_F (degeneralize_ext m)

goal (1 subgoal):
 1. \<forall>i. \<exists>j>i. r j \<in> bg_F (degeneralize_ext m)
[PROOF STEP]
by (auto simp: INFM_nat)
[PROOF STATE]
proof (state)
this:
\<forall>i. \<exists>j>i. r j \<in> bg_F (degeneralize_ext m)

goal (1 subgoal):
 1. \<exists>j qj. i \<le> j \<and> r j = (qj, n) \<and> n \<in> acc qj
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j qj. i \<le> j \<and> r j = (qj, n) \<and> n \<in> acc qj
[PROOF STEP]
using \<open>n<num_acc\<close>
[PROOF STATE]
proof (prove)
using this:
n < num_acc

goal (1 subgoal):
 1. \<exists>j qj. i \<le> j \<and> r j = (qj, n) \<and> n \<in> acc qj
[PROOF STEP]
proof (induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < num_acc \<Longrightarrow> \<exists>j qj. i \<le> j \<and> r j = (qj, 0) \<and> 0 \<in> acc qj
 2. \<And>n. \<lbrakk>n < num_acc \<Longrightarrow> \<exists>j qj. i \<le> j \<and> r j = (qj, n) \<and> n \<in> acc qj; Suc n < num_acc\<rbrakk> \<Longrightarrow> \<exists>j qj. i \<le> j \<and> r j = (qj, Suc n) \<and> Suc n \<in> acc qj
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 < num_acc

goal (2 subgoals):
 1. 0 < num_acc \<Longrightarrow> \<exists>j qj. i \<le> j \<and> r j = (qj, 0) \<and> 0 \<in> acc qj
 2. \<And>n. \<lbrakk>n < num_acc \<Longrightarrow> \<exists>j qj. i \<le> j \<and> r j = (qj, n) \<and> n \<in> acc qj; Suc n < num_acc\<rbrakk> \<Longrightarrow> \<exists>j qj. i \<le> j \<and> r j = (qj, Suc n) \<and> Suc n \<in> acc qj
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
0 < num_acc

goal (1 subgoal):
 1. \<exists>j qj. i \<le> j \<and> r j = (qj, 0) \<and> 0 \<in> acc qj
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
0 < num_acc
r i = (q, 0)
0 \<in> acc q
n < num_acc

goal (1 subgoal):
 1. \<exists>j qj. i \<le> j \<and> r j = (qj, 0) \<and> 0 \<in> acc qj
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>j qj. i \<le> j \<and> r j = (qj, 0) \<and> 0 \<in> acc qj

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < num_acc \<Longrightarrow> \<exists>j qj. i \<le> j \<and> r j = (qj, n) \<and> n \<in> acc qj; Suc n < num_acc\<rbrakk> \<Longrightarrow> \<exists>j qj. i \<le> j \<and> r j = (qj, Suc n) \<and> Suc n \<in> acc qj
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < num_acc \<Longrightarrow> \<exists>j qj. i \<le> j \<and> r j = (qj, n) \<and> n \<in> acc qj; Suc n < num_acc\<rbrakk> \<Longrightarrow> \<exists>j qj. i \<le> j \<and> r j = (qj, Suc n) \<and> Suc n \<in> acc qj
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
n < num_acc \<Longrightarrow> \<exists>j qj. i \<le> j \<and> r j = (qj, n) \<and> n \<in> acc qj
Suc n < num_acc

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < num_acc \<Longrightarrow> \<exists>j qj. i \<le> j \<and> r j = (qj, n) \<and> n \<in> acc qj; Suc n < num_acc\<rbrakk> \<Longrightarrow> \<exists>j qj. i \<le> j \<and> r j = (qj, Suc n) \<and> Suc n \<in> acc qj
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n < num_acc \<Longrightarrow> \<exists>j qj. i \<le> j \<and> r j = (qj, n) \<and> n \<in> acc qj
Suc n < num_acc
[PROOF STEP]
obtain j qj where "i\<le>j" "r j = (qj,n)" "n\<in>acc qj"
[PROOF STATE]
proof (prove)
using this:
n < num_acc \<Longrightarrow> \<exists>j qj. i \<le> j \<and> r j = (qj, n) \<and> n \<in> acc qj
Suc n < num_acc

goal (1 subgoal):
 1. (\<And>j qj. \<lbrakk>i \<le> j; r j = (qj, n); n \<in> acc qj\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<le> j
r j = (qj, n)
n \<in> acc qj

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < num_acc \<Longrightarrow> \<exists>j qj. i \<le> j \<and> r j = (qj, n) \<and> n \<in> acc qj; Suc n < num_acc\<rbrakk> \<Longrightarrow> \<exists>j qj. i \<le> j \<and> r j = (qj, Suc n) \<and> Suc n \<in> acc qj
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<le> j
r j = (qj, n)
n \<in> acc qj

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < num_acc \<Longrightarrow> \<exists>j qj. i \<le> j \<and> r j = (qj, n) \<and> n \<in> acc qj; Suc n < num_acc\<rbrakk> \<Longrightarrow> \<exists>j qj. i \<le> j \<and> r j = (qj, Suc n) \<and> Suc n \<in> acc qj
[PROOF STEP]
from R
[PROOF STATE]
proof (chain)
picking this:
graph_defs.is_run (degeneralize_ext m) r
[PROOF STEP]
have "(r j, r (Suc j)) \<in> degen.E T m"
[PROOF STATE]
proof (prove)
using this:
graph_defs.is_run (degeneralize_ext m) r

goal (1 subgoal):
 1. (r j, r (Suc j)) \<in> g_E (degeneralize_ext m)
[PROOF STEP]
unfolding degen.is_run_def ipath_def
[PROOF STATE]
proof (prove)
using this:
r 0 \<in> g_V0 (degeneralize_ext m) \<and> (\<forall>i. (r i, r (Suc i)) \<in> g_E (degeneralize_ext m))

goal (1 subgoal):
 1. (r j, r (Suc j)) \<in> g_E (degeneralize_ext m)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(r j, r (Suc j)) \<in> g_E (degeneralize_ext m)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < num_acc \<Longrightarrow> \<exists>j qj. i \<le> j \<and> r j = (qj, n) \<and> n \<in> acc qj; Suc n < num_acc\<rbrakk> \<Longrightarrow> \<exists>j qj. i \<le> j \<and> r j = (qj, Suc n) \<and> Suc n \<in> acc qj
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<le> j
r j = (qj, n)
n \<in> acc qj
(r j, r (Suc j)) \<in> g_E (degeneralize_ext m)
[PROOF STEP]
obtain qsj where RSJ: "r (Suc j) = (qsj,Suc n)"
[PROOF STATE]
proof (prove)
using this:
i \<le> j
r j = (qj, n)
n \<in> acc qj
(r j, r (Suc j)) \<in> g_E (degeneralize_ext m)

goal (1 subgoal):
 1. (\<And>qsj. r (Suc j) = (qsj, Suc n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding degeneralize_ext_def
[PROOF STATE]
proof (prove)
using this:
i \<le> j
r j = (qj, n)
n \<in> acc qj
(r j, r (Suc j)) \<in> g_E (if num_acc = 0 then \<lparr>g_V = V \<times> {0}, g_E = {((q, 0), q', 0) |q q'. (q, q') \<in> E}, g_V0 = V0 \<times> {0}, bg_F = V \<times> {0}, \<dots> = m G\<rparr> else \<lparr>g_V = V \<times> {0..<num_acc}, g_E = {((q, i), q', i') |i i' q q'. i < num_acc \<and> (q, q') \<in> E \<and> i' = (if i \<in> acc q then (i + 1) mod num_acc else i)}, g_V0 = V0 \<times> {0}, bg_F = {(q, 0) |q. 0 \<in> acc q}, \<dots> = m G\<rparr>)

goal (1 subgoal):
 1. (\<And>qsj. r (Suc j) = (qsj, Suc n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>Suc n<num_acc\<close>
[PROOF STATE]
proof (prove)
using this:
i \<le> j
r j = (qj, n)
n \<in> acc qj
(r j, r (Suc j)) \<in> g_E (if num_acc = 0 then \<lparr>g_V = V \<times> {0}, g_E = {((q, 0), q', 0) |q q'. (q, q') \<in> E}, g_V0 = V0 \<times> {0}, bg_F = V \<times> {0}, \<dots> = m G\<rparr> else \<lparr>g_V = V \<times> {0..<num_acc}, g_E = {((q, i), q', i') |i i' q q'. i < num_acc \<and> (q, q') \<in> E \<and> i' = (if i \<in> acc q then (i + 1) mod num_acc else i)}, g_V0 = V0 \<times> {0}, bg_F = {(q, 0) |q. 0 \<in> acc q}, \<dots> = m G\<rparr>)
Suc n < num_acc

goal (1 subgoal):
 1. (\<And>qsj. r (Suc j) = (qsj, Suc n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r (Suc j) = (qsj, Suc n)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < num_acc \<Longrightarrow> \<exists>j qj. i \<le> j \<and> r j = (qj, n) \<and> n \<in> acc qj; Suc n < num_acc\<rbrakk> \<Longrightarrow> \<exists>j qj. i \<le> j \<and> r j = (qj, Suc n) \<and> Suc n \<in> acc qj
[PROOF STEP]
from ACC'
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. \<exists>j>i. r j \<in> bg_F (degeneralize_ext m)
[PROOF STEP]
obtain k q0 where "Suc j \<le> k" "r k = (q0, 0)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<exists>j>i. r j \<in> bg_F (degeneralize_ext m)

goal (1 subgoal):
 1. (\<And>k q0. \<lbrakk>Suc j \<le> k; r k = (q0, 0)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding degeneralize_ext_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<exists>j>i. r j \<in> bg_F (if num_acc = 0 then \<lparr>g_V = V \<times> {0}, g_E = {((q, 0), q', 0) |q q'. (q, q') \<in> E}, g_V0 = V0 \<times> {0}, bg_F = V \<times> {0}, \<dots> = m G\<rparr> else \<lparr>g_V = V \<times> {0..<num_acc}, g_E = {((q, i), q', i') |i i' q q'. i < num_acc \<and> (q, q') \<in> E \<and> i' = (if i \<in> acc q then (i + 1) mod num_acc else i)}, g_V0 = V0 \<times> {0}, bg_F = {(q, 0) |q. 0 \<in> acc q}, \<dots> = m G\<rparr>)

goal (1 subgoal):
 1. (\<And>k q0. \<lbrakk>Suc j \<le> k; r k = (q0, 0)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>k q0. \<lbrakk>Suc j \<le> k; r k = (q0, 0)\<rbrakk> \<Longrightarrow> thesis; \<forall>i. \<exists>j>i. \<exists>q. r j = (q, 0) \<and> 0 \<in> acc q\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (metis less_imp_le_nat)
[PROOF STATE]
proof (state)
this:
Suc j \<le> k
r k = (q0, 0)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < num_acc \<Longrightarrow> \<exists>j qj. i \<le> j \<and> r j = (qj, n) \<and> n \<in> acc qj; Suc n < num_acc\<rbrakk> \<Longrightarrow> \<exists>j qj. i \<le> j \<and> r j = (qj, Suc n) \<and> Suc n \<in> acc qj
[PROOF STEP]
from degen_run_find_change[OF NN0 R \<open>Suc j \<le> k\<close> RSJ \<open>r k = (q0, 0)\<close>]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>Suc n \<noteq> 0; \<And>ka qk. \<lbrakk>Suc j \<le> ka; ka < k; r ka = (qk, Suc n); Suc n \<in> acc qk\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
obtain l ql where
        "Suc j \<le> l" "l < k" "r l = (ql, Suc n)" "Suc n \<in> acc ql"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Suc n \<noteq> 0; \<And>ka qk. \<lbrakk>Suc j \<le> ka; ka < k; r ka = (qk, Suc n); Suc n \<in> acc qk\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>l ql. \<lbrakk>Suc j \<le> l; l < k; r l = (ql, Suc n); Suc n \<in> acc ql\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Suc j \<le> l
l < k
r l = (ql, Suc n)
Suc n \<in> acc ql

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < num_acc \<Longrightarrow> \<exists>j qj. i \<le> j \<and> r j = (qj, n) \<and> n \<in> acc qj; Suc n < num_acc\<rbrakk> \<Longrightarrow> \<exists>j qj. i \<le> j \<and> r j = (qj, Suc n) \<and> Suc n \<in> acc qj
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
Suc j \<le> l
l < k
r l = (ql, Suc n)
Suc n \<in> acc ql

goal (1 subgoal):
 1. \<exists>j qj. i \<le> j \<and> r j = (qj, Suc n) \<and> Suc n \<in> acc qj
[PROOF STEP]
using \<open>i \<le> j\<close>
[PROOF STATE]
proof (prove)
using this:
Suc j \<le> l
l < k
r l = (ql, Suc n)
Suc n \<in> acc ql
i \<le> j

goal (1 subgoal):
 1. \<exists>j qj. i \<le> j \<and> r j = (qj, Suc n) \<and> Suc n \<in> acc qj
[PROOF STEP]
by (intro exI[where x=l] exI[where x=ql]) auto
[PROOF STATE]
proof (state)
this:
\<exists>j qj. i \<le> j \<and> r j = (qj, Suc n) \<and> Suc n \<in> acc qj

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>j qj. i \<le> j \<and> r j = (qj, n) \<and> n \<in> acc qj

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma degen_acc_run_sound:
    assumes A: "degen.is_acc_run T m r"
    shows "is_acc_run (fst o r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_acc_run (fst \<circ> r)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_acc_run (fst \<circ> r)
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
b_graph.is_acc_run (degeneralize_ext m) r
[PROOF STEP]
have R: "degen.is_run T m r"
      and ACC: "\<exists>\<^sub>\<infinity>i. r i \<in> degen.F T m"
[PROOF STATE]
proof (prove)
using this:
b_graph.is_acc_run (degeneralize_ext m) r

goal (1 subgoal):
 1. graph_defs.is_run (degeneralize_ext m) r &&& \<exists>\<^sub>\<infinity>i. r i \<in> bg_F (degeneralize_ext m)
[PROOF STEP]
unfolding degen.is_acc_run_def degen.is_acc_def
[PROOF STATE]
proof (prove)
using this:
graph_defs.is_run (degeneralize_ext m) r \<and> (\<exists>\<^sub>\<infinity>i. r i \<in> bg_F (degeneralize_ext m))

goal (1 subgoal):
 1. graph_defs.is_run (degeneralize_ext m) r &&& \<exists>\<^sub>\<infinity>i. r i \<in> bg_F (degeneralize_ext m)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
graph_defs.is_run (degeneralize_ext m) r
\<exists>\<^sub>\<infinity>i. r i \<in> bg_F (degeneralize_ext m)

goal (1 subgoal):
 1. is_acc_run (fst \<circ> r)
[PROOF STEP]
from degen_is_run_sound[OF R]
[PROOF STATE]
proof (chain)
picking this:
is_run (fst \<circ> r)
[PROOF STEP]
have R': "is_run (fst o r)"
[PROOF STATE]
proof (prove)
using this:
is_run (fst \<circ> r)

goal (1 subgoal):
 1. is_run (fst \<circ> r)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
is_run (fst \<circ> r)

goal (1 subgoal):
 1. is_acc_run (fst \<circ> r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_acc_run (fst \<circ> r)
[PROOF STEP]
proof (cases "num_acc = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. num_acc = 0 \<Longrightarrow> is_acc_run (fst \<circ> r)
 2. num_acc \<noteq> 0 \<Longrightarrow> is_acc_run (fst \<circ> r)
[PROOF STEP]
case NN0[simp]: False
[PROOF STATE]
proof (state)
this:
num_acc \<noteq> 0

goal (2 subgoals):
 1. num_acc = 0 \<Longrightarrow> is_acc_run (fst \<circ> r)
 2. num_acc \<noteq> 0 \<Longrightarrow> is_acc_run (fst \<circ> r)
[PROOF STEP]
from ACC
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<^sub>\<infinity>i. r i \<in> bg_F (degeneralize_ext m)
[PROOF STEP]
have ACC': "\<forall>i. \<exists>j>i. r j \<in> degen.F T m"
[PROOF STATE]
proof (prove)
using this:
\<exists>\<^sub>\<infinity>i. r i \<in> bg_F (degeneralize_ext m)

goal (1 subgoal):
 1. \<forall>i. \<exists>j>i. r j \<in> bg_F (degeneralize_ext m)
[PROOF STEP]
by (auto simp: INFM_nat)
[PROOF STATE]
proof (state)
this:
\<forall>i. \<exists>j>i. r j \<in> bg_F (degeneralize_ext m)

goal (2 subgoals):
 1. num_acc = 0 \<Longrightarrow> is_acc_run (fst \<circ> r)
 2. num_acc \<noteq> 0 \<Longrightarrow> is_acc_run (fst \<circ> r)
[PROOF STEP]
have "\<forall>n<num_acc. \<forall>i. \<exists>j>i. n \<in> acc (fst (r j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n<num_acc. \<forall>i. \<exists>j>i. n \<in> acc (fst (r j))
[PROOF STEP]
proof (intro allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n i. n < num_acc \<Longrightarrow> \<exists>j>i. n \<in> acc (fst (r j))
[PROOF STEP]
fix n i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n i. n < num_acc \<Longrightarrow> \<exists>j>i. n \<in> acc (fst (r j))
[PROOF STEP]
obtain j qj where "j>i" and RJ: "r j = (qj,0)" and ACCJ: "0 \<in> acc (qj)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j qj. \<lbrakk>i < j; r j = (qj, 0); 0 \<in> acc qj\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ACC'
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<exists>j>i. r j \<in> bg_F (degeneralize_ext m)

goal (1 subgoal):
 1. (\<And>j qj. \<lbrakk>i < j; r j = (qj, 0); 0 \<in> acc qj\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding degeneralize_ext_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<exists>j>i. r j \<in> bg_F (if num_acc = 0 then \<lparr>g_V = V \<times> {0}, g_E = {((q, 0), q', 0) |q q'. (q, q') \<in> E}, g_V0 = V0 \<times> {0}, bg_F = V \<times> {0}, \<dots> = m G\<rparr> else \<lparr>g_V = V \<times> {0..<num_acc}, g_E = {((q, i), q', i') |i i' q q'. i < num_acc \<and> (q, q') \<in> E \<and> i' = (if i \<in> acc q then (i + 1) mod num_acc else i)}, g_V0 = V0 \<times> {0}, bg_F = {(q, 0) |q. 0 \<in> acc q}, \<dots> = m G\<rparr>)

goal (1 subgoal):
 1. (\<And>j qj. \<lbrakk>i < j; r j = (qj, 0); 0 \<in> acc qj\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
i < j
r j = (qj, 0)
0 \<in> acc qj

goal (1 subgoal):
 1. \<And>n i. n < num_acc \<Longrightarrow> \<exists>j>i. n \<in> acc (fst (r j))
[PROOF STEP]
assume NLESS: "n<num_acc"
[PROOF STATE]
proof (state)
this:
n < num_acc

goal (1 subgoal):
 1. \<And>n i. n < num_acc \<Longrightarrow> \<exists>j>i. n \<in> acc (fst (r j))
[PROOF STEP]
show "\<exists>j>i. n \<in> acc (fst (r j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j>i. n \<in> acc (fst (r j))
[PROOF STEP]
proof (cases n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>j>i. n \<in> acc (fst (r j))
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>j>i. n \<in> acc (fst (r j))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>j>i. n \<in> acc (fst (r j))
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>j>i. n \<in> acc (fst (r j))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
n = 0

goal (1 subgoal):
 1. \<exists>j>i. n \<in> acc (fst (r j))
[PROOF STEP]
using \<open>j>i\<close> RJ ACCJ
[PROOF STATE]
proof (prove)
using this:
n = 0
i < j
r j = (qj, 0)
0 \<in> acc qj

goal (1 subgoal):
 1. \<exists>j>i. n \<in> acc (fst (r j))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>j>i. n \<in> acc (fst (r j))

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>j>i. n \<in> acc (fst (r j))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>j>i. n \<in> acc (fst (r j))
[PROOF STEP]
case [simp]: (Suc n')
[PROOF STATE]
proof (state)
this:
n = Suc n'

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>j>i. n \<in> acc (fst (r j))
[PROOF STEP]
from degen_run_find_acc_aux[OF NN0 A RJ ACCJ NLESS]
[PROOF STATE]
proof (chain)
picking this:
\<exists>ja qj. j \<le> ja \<and> r ja = (qj, n) \<and> n \<in> acc qj
[PROOF STEP]
obtain k qk where
            "j\<le>k" "r k = (qk,n)" "n \<in> acc qk"
[PROOF STATE]
proof (prove)
using this:
\<exists>ja qj. j \<le> ja \<and> r ja = (qj, n) \<and> n \<in> acc qj

goal (1 subgoal):
 1. (\<And>k qk. \<lbrakk>j \<le> k; r k = (qk, n); n \<in> acc qk\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j \<le> k
r k = (qk, n)
n \<in> acc qk

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>j>i. n \<in> acc (fst (r j))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
j \<le> k
r k = (qk, n)
n \<in> acc qk

goal (1 subgoal):
 1. \<exists>j>i. n \<in> acc (fst (r j))
[PROOF STEP]
by (metis \<open>i < j\<close> dual_order.strict_trans1 fst_conv)
[PROOF STATE]
proof (state)
this:
\<exists>j>i. n \<in> acc (fst (r j))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>j>i. n \<in> acc (fst (r j))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n<num_acc. \<forall>i. \<exists>j>i. n \<in> acc (fst (r j))

goal (2 subgoals):
 1. num_acc = 0 \<Longrightarrow> is_acc_run (fst \<circ> r)
 2. num_acc \<noteq> 0 \<Longrightarrow> is_acc_run (fst \<circ> r)
[PROOF STEP]
hence "\<forall>n<num_acc. \<exists>\<^sub>\<infinity>i. n \<in> acc (fst (r i))"
[PROOF STATE]
proof (prove)
using this:
\<forall>n<num_acc. \<forall>i. \<exists>j>i. n \<in> acc (fst (r j))

goal (1 subgoal):
 1. \<forall>n<num_acc. \<exists>\<^sub>\<infinity>i. n \<in> acc (fst (r i))
[PROOF STEP]
by (auto simp: INFM_nat)
[PROOF STATE]
proof (state)
this:
\<forall>n<num_acc. \<exists>\<^sub>\<infinity>i. n \<in> acc (fst (r i))

goal (2 subgoals):
 1. num_acc = 0 \<Longrightarrow> is_acc_run (fst \<circ> r)
 2. num_acc \<noteq> 0 \<Longrightarrow> is_acc_run (fst \<circ> r)
[PROOF STEP]
with R'
[PROOF STATE]
proof (chain)
picking this:
is_run (fst \<circ> r)
\<forall>n<num_acc. \<exists>\<^sub>\<infinity>i. n \<in> acc (fst (r i))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_run (fst \<circ> r)
\<forall>n<num_acc. \<exists>\<^sub>\<infinity>i. n \<in> acc (fst (r i))

goal (1 subgoal):
 1. is_acc_run (fst \<circ> r)
[PROOF STEP]
unfolding is_acc_run_def is_acc_def
[PROOF STATE]
proof (prove)
using this:
is_run (fst \<circ> r)
\<forall>n<num_acc. \<exists>\<^sub>\<infinity>i. n \<in> acc (fst (r i))

goal (1 subgoal):
 1. is_run (fst \<circ> r) \<and> (\<forall>n<num_acc. \<exists>\<^sub>\<infinity>i. n \<in> acc ((fst \<circ> r) i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_acc_run (fst \<circ> r)

goal (1 subgoal):
 1. num_acc = 0 \<Longrightarrow> is_acc_run (fst \<circ> r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. num_acc = 0 \<Longrightarrow> is_acc_run (fst \<circ> r)
[PROOF STEP]
case [simp]: True
[PROOF STATE]
proof (state)
this:
num_acc = 0

goal (1 subgoal):
 1. num_acc = 0 \<Longrightarrow> is_acc_run (fst \<circ> r)
[PROOF STEP]
with R'
[PROOF STATE]
proof (chain)
picking this:
is_run (fst \<circ> r)
num_acc = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_run (fst \<circ> r)
num_acc = 0

goal (1 subgoal):
 1. is_acc_run (fst \<circ> r)
[PROOF STEP]
unfolding is_acc_run_def is_acc_def
[PROOF STATE]
proof (prove)
using this:
is_run (fst \<circ> r)
num_acc = 0

goal (1 subgoal):
 1. is_run (fst \<circ> r) \<and> (\<forall>n<num_acc. \<exists>\<^sub>\<infinity>i. n \<in> acc ((fst \<circ> r) i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_acc_run (fst \<circ> r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_acc_run (fst \<circ> r)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma degen_acc_run_iff:
    "is_acc_run r \<longleftrightarrow> (\<exists>r'. fst o r' = r \<and> degen.is_acc_run T m r')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_acc_run r = (\<exists>r'. fst \<circ> r' = r \<and> b_graph.is_acc_run (degeneralize_ext m) r')
[PROOF STEP]
using degen_acc_run_complete degen_acc_run_sound
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_acc_run ?r; \<And>r'. \<lbrakk>b_graph.is_acc_run (degeneralize_ext ?m) r'; ?r = fst \<circ> r'\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
b_graph.is_acc_run (degeneralize_ext ?m) ?r \<Longrightarrow> is_acc_run (fst \<circ> ?r)

goal (1 subgoal):
 1. is_acc_run r = (\<exists>r'. fst \<circ> r' = r \<and> b_graph.is_acc_run (degeneralize_ext m) r')
[PROOF STEP]
by blast


[STATEMENT]
lemma langI[intro?]: "accept w \<Longrightarrow> w\<in>lang"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. accept w \<Longrightarrow> w \<in> lang
[PROOF STEP]
by (auto simp: lang_def)


[STATEMENT]
lemma prod_invar: "igb_graph prod"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. igb_graph prod
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. g_V0 prod \<subseteq> g_V prod
 2. g_E prod \<subseteq> g_V prod \<times> g_V prod
 3. \<Union> (range (igbg_acc prod)) \<subseteq> {0..<igbg_num_acc prod}
 4. \<And>q. igbg_acc prod q \<noteq> {} \<Longrightarrow> q \<in> g_V prod
[PROOF STEP]
using igba.V0_ss sa.V0_ss
[PROOF STATE]
proof (prove)
using this:
igba.V0 \<subseteq> igba.V
sa.V0 \<subseteq> sa.V

goal (4 subgoals):
 1. g_V0 prod \<subseteq> g_V prod
 2. g_E prod \<subseteq> g_V prod \<times> g_V prod
 3. \<Union> (range (igbg_acc prod)) \<subseteq> {0..<igbg_num_acc prod}
 4. \<And>q. igbg_acc prod q \<noteq> {} \<Longrightarrow> q \<in> g_V prod
[PROOF STEP]
apply (auto simp: prod_def) []
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. g_E prod \<subseteq> g_V prod \<times> g_V prod
 2. \<Union> (range (igbg_acc prod)) \<subseteq> {0..<igbg_num_acc prod}
 3. \<And>q. igbg_acc prod q \<noteq> {} \<Longrightarrow> q \<in> g_V prod
[PROOF STEP]
using igba.E_ss sa.E_ss
[PROOF STATE]
proof (prove)
using this:
igba.E \<subseteq> igba.V \<times> igba.V
sa.E \<subseteq> sa.V \<times> sa.V

goal (3 subgoals):
 1. g_E prod \<subseteq> g_V prod \<times> g_V prod
 2. \<Union> (range (igbg_acc prod)) \<subseteq> {0..<igbg_num_acc prod}
 3. \<And>q. igbg_acc prod q \<noteq> {} \<Longrightarrow> q \<in> g_V prod
[PROOF STEP]
apply (auto simp: prod_def) []
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<Union> (range (igbg_acc prod)) \<subseteq> {0..<igbg_num_acc prod}
 2. \<And>q. igbg_acc prod q \<noteq> {} \<Longrightarrow> q \<in> g_V prod
[PROOF STEP]
using igba.acc_bound
[PROOF STATE]
proof (prove)
using this:
\<Union> (range igba.acc) \<subseteq> {0..<igba.num_acc}

goal (2 subgoals):
 1. \<Union> (range (igbg_acc prod)) \<subseteq> {0..<igbg_num_acc prod}
 2. \<And>q. igbg_acc prod q \<noteq> {} \<Longrightarrow> q \<in> g_V prod
[PROOF STEP]
apply (auto simp: prod_def split: if_split_asm) []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. igbg_acc prod q \<noteq> {} \<Longrightarrow> q \<in> g_V prod
[PROOF STEP]
using igba.acc_ss
[PROOF STATE]
proof (prove)
using this:
igba.acc ?q \<noteq> {} \<Longrightarrow> ?q \<in> igba.V

goal (1 subgoal):
 1. \<And>q. igbg_acc prod q \<noteq> {} \<Longrightarrow> q \<in> g_V prod
[PROOF STEP]
apply (fastforce simp: prod_def split: if_split_asm) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prod_finite_reachable:
    assumes "finite (igba.E\<^sup>* `` igba.V0)" "finite (sa.E\<^sup>* `` sa.V0)"
    shows "finite ((g_E prod)\<^sup>* `` g_V0 prod)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite prod.reachable
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite prod.reachable
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite prod.reachable
[PROOF STEP]
fix q s q' s'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite prod.reachable
[PROOF STEP]
assume "((q,s),(q',s')) \<in> (g_E prod)\<^sup>*"
[PROOF STATE]
proof (state)
this:
((q, s), q', s') \<in> prod.E\<^sup>*

goal (1 subgoal):
 1. finite prod.reachable
[PROOF STEP]
hence "(q,q') \<in> (igba.E)\<^sup>* \<and> (s,s') \<in> (sa.E)\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
((q, s), q', s') \<in> prod.E\<^sup>*

goal (1 subgoal):
 1. (q, q') \<in> igba.E\<^sup>* \<and> (s, s') \<in> sa.E\<^sup>*
[PROOF STEP]
apply (induction rule: rtrancl_induct2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (q, q) \<in> igba.E\<^sup>* \<and> (s, s) \<in> sa.E\<^sup>*
 2. \<And>a b aa ba. \<lbrakk>((q, s), a, b) \<in> prod.E\<^sup>*; ((a, b), aa, ba) \<in> prod.E; (q, a) \<in> igba.E\<^sup>* \<and> (s, b) \<in> sa.E\<^sup>*\<rbrakk> \<Longrightarrow> (q, aa) \<in> igba.E\<^sup>* \<and> (s, ba) \<in> sa.E\<^sup>*
[PROOF STEP]
apply (auto simp: prod_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(q, q') \<in> igba.E\<^sup>* \<and> (s, s') \<in> sa.E\<^sup>*

goal (1 subgoal):
 1. finite prod.reachable
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
((?q4, ?s4), ?q'4, ?s'4) \<in> prod.E\<^sup>* \<Longrightarrow> (?q4, ?q'4) \<in> igba.E\<^sup>* \<and> (?s4, ?s'4) \<in> sa.E\<^sup>*

goal (1 subgoal):
 1. finite prod.reachable
[PROOF STEP]
note gsp_reach=this
[PROOF STATE]
proof (state)
this:
((?q4, ?s4), ?q'4, ?s'4) \<in> prod.E\<^sup>* \<Longrightarrow> (?q4, ?q'4) \<in> igba.E\<^sup>* \<and> (?s4, ?s'4) \<in> sa.E\<^sup>*

goal (1 subgoal):
 1. finite prod.reachable
[PROOF STEP]
have [simp]: "\<And>q s. (q,s) \<in> g_V0 prod \<longleftrightarrow> q \<in> igba.V0 \<and> s \<in> sa.V0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q s. ((q, s) \<in> prod.V0) = (q \<in> igba.V0 \<and> s \<in> sa.V0)
[PROOF STEP]
by (auto simp: prod_def)
[PROOF STATE]
proof (state)
this:
((?q2, ?s2) \<in> prod.V0) = (?q2 \<in> igba.V0 \<and> ?s2 \<in> sa.V0)

goal (1 subgoal):
 1. finite prod.reachable
[PROOF STEP]
have reachSS:
      "((g_E prod)\<^sup>* `` g_V0 prod)
      \<subseteq> ((igba.E)\<^sup>* `` igba.V0) \<times> (sa.E\<^sup>* `` sa.V0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod.reachable \<subseteq> igba.reachable \<times> sa.reachable
[PROOF STEP]
by (auto dest: gsp_reach)
[PROOF STATE]
proof (state)
this:
prod.reachable \<subseteq> igba.reachable \<times> sa.reachable

goal (1 subgoal):
 1. finite prod.reachable
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite prod.reachable
[PROOF STEP]
apply (rule finite_subset[OF reachSS])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (igba.reachable \<times> sa.reachable)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite igba.reachable
finite sa.reachable

goal (1 subgoal):
 1. finite (igba.reachable \<times> sa.reachable)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite prod.reachable

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prod_fields:
    "prod.V = igba.V \<times> sa.V"
    "prod.E = { ((q,s),(q',s')).
      igba.L q (sa.L s) \<and> (q,q') \<in> igba.E \<and> (s,s') \<in> sa.E }"
    "prod.V0 = igba.V0 \<times> sa.V0"
    "prod.num_acc = igba.num_acc"
    "prod.acc = (\<lambda>(q,s). if s\<in>sa.V then igba.acc q else {} )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (prod.V = igba.V \<times> sa.V &&& prod.E = {((q, s), q', s'). local.igba.L q (local.sa.L s) \<and> (q, q') \<in> igba.E \<and> (s, s') \<in> sa.E}) &&& prod.V0 = igba.V0 \<times> sa.V0 &&& prod.num_acc = igba.num_acc &&& prod.acc = (\<lambda>(q, s). if s \<in> sa.V then igba.acc q else {})
[PROOF STEP]
unfolding prod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g_V \<lparr>g_V = igba.V \<times> sa.V, g_E = {((q, s), q', s'). local.igba.L q (local.sa.L s) \<and> (q, q') \<in> igba.E \<and> (s, s') \<in> sa.E}, g_V0 = igba.V0 \<times> sa.V0, igbg_num_acc = igba.num_acc, igbg_acc = \<lambda>(q, s). if s \<in> sa.V then igba.acc q else {}\<rparr> = igba.V \<times> sa.V &&& g_E \<lparr>g_V = igba.V \<times> sa.V, g_E = {((q, s), q', s'). local.igba.L q (local.sa.L s) \<and> (q, q') \<in> igba.E \<and> (s, s') \<in> sa.E}, g_V0 = igba.V0 \<times> sa.V0, igbg_num_acc = igba.num_acc, igbg_acc = \<lambda>(q, s). if s \<in> sa.V then igba.acc q else {}\<rparr> = {((q, s), q', s'). local.igba.L q (local.sa.L s) \<and> (q, q') \<in> igba.E \<and> (s, s') \<in> sa.E}) &&& g_V0 \<lparr>g_V = igba.V \<times> sa.V, g_E = {((q, s), q', s'). local.igba.L q (local.sa.L s) \<and> (q, q') \<in> igba.E \<and> (s, s') \<in> sa.E}, g_V0 = igba.V0 \<times> sa.V0, igbg_num_acc = igba.num_acc, igbg_acc = \<lambda>(q, s). if s \<in> sa.V then igba.acc q else {}\<rparr> = igba.V0 \<times> sa.V0 &&& igbg_num_acc \<lparr>g_V = igba.V \<times> sa.V, g_E = {((q, s), q', s'). local.igba.L q (local.sa.L s) \<and> (q, q') \<in> igba.E \<and> (s, s') \<in> sa.E}, g_V0 = igba.V0 \<times> sa.V0, igbg_num_acc = igba.num_acc, igbg_acc = \<lambda>(q, s). if s \<in> sa.V then igba.acc q else {}\<rparr> = igba.num_acc &&& igbg_acc \<lparr>g_V = igba.V \<times> sa.V, g_E = {((q, s), q', s'). local.igba.L q (local.sa.L s) \<and> (q, q') \<in> igba.E \<and> (s, s') \<in> sa.E}, g_V0 = igba.V0 \<times> sa.V0, igbg_num_acc = igba.num_acc, igbg_acc = \<lambda>(q, s). if s \<in> sa.V then igba.acc q else {}\<rparr> = (\<lambda>(q, s). if s \<in> sa.V then igba.acc q else {})
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prod_run: "prod.is_run r \<longleftrightarrow>
      igba.is_run (fst o r)
    \<and> sa.is_run (snd o r)
    \<and> (\<forall>i. igba.L (fst (r i)) (sa.L (snd (r i))))" (is "?L=?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod.is_run r = (igba.is_run (fst \<circ> r) \<and> sa.is_run (snd \<circ> r) \<and> (\<forall>i. local.igba.L (fst (r i)) (local.sa.L (snd (r i)))))
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. prod.is_run r \<Longrightarrow> igba.is_run (fst \<circ> r) \<and> sa.is_run (snd \<circ> r) \<and> (\<forall>i. local.igba.L (fst (r i)) (local.sa.L (snd (r i))))
 2. igba.is_run (fst \<circ> r) \<and> sa.is_run (snd \<circ> r) \<and> (\<forall>i. local.igba.L (fst (r i)) (local.sa.L (snd (r i)))) \<Longrightarrow> prod.is_run r
[PROOF STEP]
unfolding igba.is_run_def sa.is_run_def prod.is_run_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. r 0 \<in> prod.V0 \<and> ipath prod.E r \<Longrightarrow> ((fst \<circ> r) 0 \<in> igba.V0 \<and> ipath igba.E (fst \<circ> r)) \<and> ((snd \<circ> r) 0 \<in> sa.V0 \<and> ipath sa.E (snd \<circ> r)) \<and> (\<forall>i. local.igba.L (fst (r i)) (local.sa.L (snd (r i))))
 2. ((fst \<circ> r) 0 \<in> igba.V0 \<and> ipath igba.E (fst \<circ> r)) \<and> ((snd \<circ> r) 0 \<in> sa.V0 \<and> ipath sa.E (snd \<circ> r)) \<and> (\<forall>i. local.igba.L (fst (r i)) (local.sa.L (snd (r i)))) \<Longrightarrow> r 0 \<in> prod.V0 \<and> ipath prod.E r
[PROOF STEP]
unfolding prod_def ipath_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. r 0 \<in> g_V0 \<lparr>g_V = igba.V \<times> sa.V, g_E = {((q, s), q', s'). local.igba.L q (local.sa.L s) \<and> (q, q') \<in> igba.E \<and> (s, s') \<in> sa.E}, g_V0 = igba.V0 \<times> sa.V0, igbg_num_acc = igba.num_acc, igbg_acc = \<lambda>(q, s). if s \<in> sa.V then igba.acc q else {}\<rparr> \<and> (\<forall>i. (r i, r (Suc i)) \<in> g_E \<lparr>g_V = igba.V \<times> sa.V, g_E = {((q, s), q', s'). local.igba.L q (local.sa.L s) \<and> (q, q') \<in> igba.E \<and> (s, s') \<in> sa.E}, g_V0 = igba.V0 \<times> sa.V0, igbg_num_acc = igba.num_acc, igbg_acc = \<lambda>(q, s). if s \<in> sa.V then igba.acc q else {}\<rparr>) \<Longrightarrow> ((fst \<circ> r) 0 \<in> igba.V0 \<and> (\<forall>i. ((fst \<circ> r) i, (fst \<circ> r) (Suc i)) \<in> igba.E)) \<and> ((snd \<circ> r) 0 \<in> sa.V0 \<and> (\<forall>i. ((snd \<circ> r) i, (snd \<circ> r) (Suc i)) \<in> sa.E)) \<and> (\<forall>i. local.igba.L (fst (r i)) (local.sa.L (snd (r i))))
 2. ((fst \<circ> r) 0 \<in> igba.V0 \<and> (\<forall>i. ((fst \<circ> r) i, (fst \<circ> r) (Suc i)) \<in> igba.E)) \<and> ((snd \<circ> r) 0 \<in> sa.V0 \<and> (\<forall>i. ((snd \<circ> r) i, (snd \<circ> r) (Suc i)) \<in> sa.E)) \<and> (\<forall>i. local.igba.L (fst (r i)) (local.sa.L (snd (r i)))) \<Longrightarrow> r 0 \<in> g_V0 \<lparr>g_V = igba.V \<times> sa.V, g_E = {((q, s), q', s'). local.igba.L q (local.sa.L s) \<and> (q, q') \<in> igba.E \<and> (s, s') \<in> sa.E}, g_V0 = igba.V0 \<times> sa.V0, igbg_num_acc = igba.num_acc, igbg_acc = \<lambda>(q, s). if s \<in> sa.V then igba.acc q else {}\<rparr> \<and> (\<forall>i. (r i, r (Suc i)) \<in> g_E \<lparr>g_V = igba.V \<times> sa.V, g_E = {((q, s), q', s'). local.igba.L q (local.sa.L s) \<and> (q, q') \<in> igba.E \<and> (s, s') \<in> sa.E}, g_V0 = igba.V0 \<times> sa.V0, igbg_num_acc = igba.num_acc, igbg_acc = \<lambda>(q, s). if s \<in> sa.V then igba.acc q else {}\<rparr>)
[PROOF STEP]
apply (auto split: prod.split_asm intro: in_prod_fst_sndI)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x y i. \<lbrakk>\<forall>i x1 x2. r i = (x1, x2) \<longrightarrow> (\<forall>x1a x2a. r (Suc i) = (x1a, x2a) \<longrightarrow> (x1, x1a) \<in> igba.E \<and> local.igba.L x1 (local.sa.L x2) \<and> (x2, x2a) \<in> sa.E); x \<in> igba.V0; y \<in> sa.V0; r 0 = (x, y)\<rbrakk> \<Longrightarrow> (fst (r i), fst (r (Suc i))) \<in> igba.E
 2. \<And>x y i. \<lbrakk>\<forall>i x1 x2. r i = (x1, x2) \<longrightarrow> (\<forall>x1a x2a. r (Suc i) = (x1a, x2a) \<longrightarrow> (x1, x1a) \<in> igba.E \<and> local.igba.L x1 (local.sa.L x2) \<and> (x2, x2a) \<in> sa.E); x \<in> igba.V0; y \<in> sa.V0; r 0 = (x, y)\<rbrakk> \<Longrightarrow> (snd (r i), snd (r (Suc i))) \<in> sa.E
 3. \<And>i q s. \<lbrakk>fst (r 0) \<in> igba.V0; \<forall>i. (fst (r i), fst (r (Suc i))) \<in> igba.E; snd (r 0) \<in> sa.V0; \<forall>i. (snd (r i), snd (r (Suc i))) \<in> sa.E; \<forall>i. local.igba.L (fst (r i)) (local.sa.L (snd (r i))); (q, s) = r i\<rbrakk> \<Longrightarrow> local.igba.L q (local.sa.L s)
 4. \<And>i q s q' s'. \<lbrakk>fst (r 0) \<in> igba.V0; \<forall>i. (fst (r i), fst (r (Suc i))) \<in> igba.E; snd (r 0) \<in> sa.V0; \<forall>i. (snd (r i), snd (r (Suc i))) \<in> sa.E; \<forall>i. local.igba.L (fst (r i)) (local.sa.L (snd (r i))); (q, s) = r i; r (Suc i) = (q', s')\<rbrakk> \<Longrightarrow> (q, q') \<in> igba.E
 5. \<And>i q s q' s'. \<lbrakk>fst (r 0) \<in> igba.V0; \<forall>i. (fst (r i), fst (r (Suc i))) \<in> igba.E; snd (r 0) \<in> sa.V0; \<forall>i. (snd (r i), snd (r (Suc i))) \<in> sa.E; \<forall>i. local.igba.L (fst (r i)) (local.sa.L (snd (r i))); (q, s) = r i; r (Suc i) = (q', s')\<rbrakk> \<Longrightarrow> (s, s') \<in> sa.E
[PROOF STEP]
apply (metis surjective_pairing)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x y i. \<lbrakk>\<forall>i x1 x2. r i = (x1, x2) \<longrightarrow> (\<forall>x1a x2a. r (Suc i) = (x1a, x2a) \<longrightarrow> (x1, x1a) \<in> igba.E \<and> local.igba.L x1 (local.sa.L x2) \<and> (x2, x2a) \<in> sa.E); x \<in> igba.V0; y \<in> sa.V0; r 0 = (x, y)\<rbrakk> \<Longrightarrow> (snd (r i), snd (r (Suc i))) \<in> sa.E
 2. \<And>i q s. \<lbrakk>fst (r 0) \<in> igba.V0; \<forall>i. (fst (r i), fst (r (Suc i))) \<in> igba.E; snd (r 0) \<in> sa.V0; \<forall>i. (snd (r i), snd (r (Suc i))) \<in> sa.E; \<forall>i. local.igba.L (fst (r i)) (local.sa.L (snd (r i))); (q, s) = r i\<rbrakk> \<Longrightarrow> local.igba.L q (local.sa.L s)
 3. \<And>i q s q' s'. \<lbrakk>fst (r 0) \<in> igba.V0; \<forall>i. (fst (r i), fst (r (Suc i))) \<in> igba.E; snd (r 0) \<in> sa.V0; \<forall>i. (snd (r i), snd (r (Suc i))) \<in> sa.E; \<forall>i. local.igba.L (fst (r i)) (local.sa.L (snd (r i))); (q, s) = r i; r (Suc i) = (q', s')\<rbrakk> \<Longrightarrow> (q, q') \<in> igba.E
 4. \<And>i q s q' s'. \<lbrakk>fst (r 0) \<in> igba.V0; \<forall>i. (fst (r i), fst (r (Suc i))) \<in> igba.E; snd (r 0) \<in> sa.V0; \<forall>i. (snd (r i), snd (r (Suc i))) \<in> sa.E; \<forall>i. local.igba.L (fst (r i)) (local.sa.L (snd (r i))); (q, s) = r i; r (Suc i) = (q', s')\<rbrakk> \<Longrightarrow> (s, s') \<in> sa.E
[PROOF STEP]
apply (metis surjective_pairing)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>i q s. \<lbrakk>fst (r 0) \<in> igba.V0; \<forall>i. (fst (r i), fst (r (Suc i))) \<in> igba.E; snd (r 0) \<in> sa.V0; \<forall>i. (snd (r i), snd (r (Suc i))) \<in> sa.E; \<forall>i. local.igba.L (fst (r i)) (local.sa.L (snd (r i))); (q, s) = r i\<rbrakk> \<Longrightarrow> local.igba.L q (local.sa.L s)
 2. \<And>i q s q' s'. \<lbrakk>fst (r 0) \<in> igba.V0; \<forall>i. (fst (r i), fst (r (Suc i))) \<in> igba.E; snd (r 0) \<in> sa.V0; \<forall>i. (snd (r i), snd (r (Suc i))) \<in> sa.E; \<forall>i. local.igba.L (fst (r i)) (local.sa.L (snd (r i))); (q, s) = r i; r (Suc i) = (q', s')\<rbrakk> \<Longrightarrow> (q, q') \<in> igba.E
 3. \<And>i q s q' s'. \<lbrakk>fst (r 0) \<in> igba.V0; \<forall>i. (fst (r i), fst (r (Suc i))) \<in> igba.E; snd (r 0) \<in> sa.V0; \<forall>i. (snd (r i), snd (r (Suc i))) \<in> sa.E; \<forall>i. local.igba.L (fst (r i)) (local.sa.L (snd (r i))); (q, s) = r i; r (Suc i) = (q', s')\<rbrakk> \<Longrightarrow> (s, s') \<in> sa.E
[PROOF STEP]
apply (metis fst_conv snd_conv)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i q s q' s'. \<lbrakk>fst (r 0) \<in> igba.V0; \<forall>i. (fst (r i), fst (r (Suc i))) \<in> igba.E; snd (r 0) \<in> sa.V0; \<forall>i. (snd (r i), snd (r (Suc i))) \<in> sa.E; \<forall>i. local.igba.L (fst (r i)) (local.sa.L (snd (r i))); (q, s) = r i; r (Suc i) = (q', s')\<rbrakk> \<Longrightarrow> (q, q') \<in> igba.E
 2. \<And>i q s q' s'. \<lbrakk>fst (r 0) \<in> igba.V0; \<forall>i. (fst (r i), fst (r (Suc i))) \<in> igba.E; snd (r 0) \<in> sa.V0; \<forall>i. (snd (r i), snd (r (Suc i))) \<in> sa.E; \<forall>i. local.igba.L (fst (r i)) (local.sa.L (snd (r i))); (q, s) = r i; r (Suc i) = (q', s')\<rbrakk> \<Longrightarrow> (s, s') \<in> sa.E
[PROOF STEP]
apply (metis fst_conv snd_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i q s q' s'. \<lbrakk>fst (r 0) \<in> igba.V0; \<forall>i. (fst (r i), fst (r (Suc i))) \<in> igba.E; snd (r 0) \<in> sa.V0; \<forall>i. (snd (r i), snd (r (Suc i))) \<in> sa.E; \<forall>i. local.igba.L (fst (r i)) (local.sa.L (snd (r i))); (q, s) = r i; r (Suc i) = (q', s')\<rbrakk> \<Longrightarrow> (s, s') \<in> sa.E
[PROOF STEP]
apply (metis fst_conv snd_conv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prod_acc:
    assumes A: "range (snd o r) \<subseteq> sa.V"
    shows "prod.is_acc r \<longleftrightarrow> igba.is_acc (fst o r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod.is_acc r = igba.is_acc (fst \<circ> r)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prod.is_acc r = igba.is_acc (fst \<circ> r)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prod.is_acc r = igba.is_acc (fst \<circ> r)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prod.is_acc r = igba.is_acc (fst \<circ> r)
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
range (snd \<circ> r) \<subseteq> sa.V
[PROOF STEP]
have "prod.acc (r i) = igba.acc (fst (r i))"
[PROOF STATE]
proof (prove)
using this:
range (snd \<circ> r) \<subseteq> sa.V

goal (1 subgoal):
 1. prod.acc (r i) = igba.acc (fst (r i))
[PROOF STEP]
unfolding prod_fields
[PROOF STATE]
proof (prove)
using this:
range (snd \<circ> r) \<subseteq> sa.V

goal (1 subgoal):
 1. (case r i of (q, s) \<Rightarrow> if s \<in> sa.V then igba.acc q else {}) = igba.acc (fst (r i))
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa y. \<lbrakk>range (snd \<circ> r) \<subseteq> sa.V; r i = (xa, y); x \<in> (if y \<in> sa.V then igba.acc xa else {})\<rbrakk> \<Longrightarrow> x \<in> igba.acc (fst (r i))
 2. \<And>x q s. \<lbrakk>range (snd \<circ> r) \<subseteq> sa.V; x \<in> igba.acc (fst (r i)); r i = (q, s)\<rbrakk> \<Longrightarrow> x \<in> (if s \<in> sa.V then igba.acc q else {})
[PROOF STEP]
apply (clarsimp_all split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x q s. \<lbrakk>range (\<lambda>x. snd (r x)) \<subseteq> sa.V; x \<in> igba.acc q; r i = (q, s)\<rbrakk> \<Longrightarrow> s \<in> sa.V
[PROOF STEP]
by (metis UNIV_I comp_apply imageI snd_conv subsetD)
[PROOF STATE]
proof (state)
this:
prod.acc (r i) = igba.acc (fst (r i))

goal (1 subgoal):
 1. prod.is_acc r = igba.is_acc (fst \<circ> r)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
prod.acc (r ?i4) = igba.acc (fst (r ?i4))

goal (1 subgoal):
 1. prod.is_acc r = igba.is_acc (fst \<circ> r)
[PROOF STEP]
note [simp] = this
[PROOF STATE]
proof (state)
this:
prod.acc (r ?i4) = igba.acc (fst (r ?i4))

goal (1 subgoal):
 1. prod.is_acc r = igba.is_acc (fst \<circ> r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod.is_acc r = igba.is_acc (fst \<circ> r)
[PROOF STEP]
unfolding prod.is_acc_def igba.is_acc_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>n<prod.num_acc. \<exists>\<^sub>\<infinity>i. n \<in> prod.acc (r i)) = (\<forall>n<igba.num_acc. \<exists>\<^sub>\<infinity>i. n \<in> igba.acc ((fst \<circ> r) i))
[PROOF STEP]
by (simp add: prod_fields(4))
[PROOF STATE]
proof (state)
this:
prod.is_acc r = igba.is_acc (fst \<circ> r)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gsp_correct1:
    assumes A: "prod.is_acc_run r"
    shows "sa.is_run (snd o r) \<and> (sa.L o snd o r \<in> igba.lang)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sa.is_run (snd \<circ> r) \<and> local.sa.L \<circ> snd \<circ> r \<in> local.igba.lang
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sa.is_run (snd \<circ> r) \<and> local.sa.L \<circ> snd \<circ> r \<in> local.igba.lang
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
prod.is_acc_run r
[PROOF STEP]
have PR: "prod.is_run r" and PA: "prod.is_acc r"
[PROOF STATE]
proof (prove)
using this:
prod.is_acc_run r

goal (1 subgoal):
 1. prod.is_run r &&& prod.is_acc r
[PROOF STEP]
unfolding prod.is_acc_run_def
[PROOF STATE]
proof (prove)
using this:
prod.is_run r \<and> prod.is_acc r

goal (1 subgoal):
 1. prod.is_run r &&& prod.is_acc r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prod.is_run r
prod.is_acc r

goal (1 subgoal):
 1. sa.is_run (snd \<circ> r) \<and> local.sa.L \<circ> snd \<circ> r \<in> local.igba.lang
[PROOF STEP]
have PRR: "range r \<subseteq> prod.V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range r \<subseteq> prod.V
[PROOF STEP]
using prod.run_reachable prod.reachable_V PR
[PROOF STATE]
proof (prove)
using this:
prod.is_run ?r \<Longrightarrow> range ?r \<subseteq> prod.reachable
prod.reachable \<subseteq> prod.V
prod.is_run r

goal (1 subgoal):
 1. range r \<subseteq> prod.V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
range r \<subseteq> prod.V

goal (1 subgoal):
 1. sa.is_run (snd \<circ> r) \<and> local.sa.L \<circ> snd \<circ> r \<in> local.igba.lang
[PROOF STEP]
have RSR: "range (snd o r) \<subseteq> sa.V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range (snd \<circ> r) \<subseteq> sa.V
[PROOF STEP]
using PRR
[PROOF STATE]
proof (prove)
using this:
range r \<subseteq> prod.V

goal (1 subgoal):
 1. range (snd \<circ> r) \<subseteq> sa.V
[PROOF STEP]
unfolding prod_fields
[PROOF STATE]
proof (prove)
using this:
range r \<subseteq> igba.V \<times> sa.V

goal (1 subgoal):
 1. range (snd \<circ> r) \<subseteq> sa.V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
range (snd \<circ> r) \<subseteq> sa.V

goal (1 subgoal):
 1. sa.is_run (snd \<circ> r) \<and> local.sa.L \<circ> snd \<circ> r \<in> local.igba.lang
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sa.is_run (snd \<circ> r) \<and> local.sa.L \<circ> snd \<circ> r \<in> local.igba.lang
[PROOF STEP]
using PR PA
[PROOF STATE]
proof (prove)
using this:
prod.is_run r
prod.is_acc r

goal (1 subgoal):
 1. sa.is_run (snd \<circ> r) \<and> local.sa.L \<circ> snd \<circ> r \<in> local.igba.lang
[PROOF STEP]
unfolding igba.is_acc_run_def
        igba.lang_def igba.accept_def[abs_def]
[PROOF STATE]
proof (prove)
using this:
prod.is_run r
prod.is_acc r

goal (1 subgoal):
 1. sa.is_run (snd \<circ> r) \<and> local.sa.L \<circ> snd \<circ> r \<in> {w. \<exists>r. (igba.is_run r \<and> igba.is_acc r) \<and> (\<forall>i. local.igba.L (r i) (w i))}
[PROOF STEP]
apply (auto simp: prod_run prod_acc[OF RSR])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
sa.is_run (snd \<circ> r) \<and> local.sa.L \<circ> snd \<circ> r \<in> local.igba.lang

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gsp_correct2:
    assumes A: "sa.is_run r" "sa.L o r \<in> igba.lang"
    shows "\<exists>r'. r = snd o r' \<and> prod.is_acc_run r'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r'. r = snd \<circ> r' \<and> prod.is_acc_run r'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>r'. r = snd \<circ> r' \<and> prod.is_acc_run r'
[PROOF STEP]
have [simp]: "\<And>r r'. fst o (\<lambda>i. (r i, r' i)) = r"
      "\<And>r r'. snd o (\<lambda>i. (r i, r' i)) = r'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r r'. fst \<circ> (\<lambda>i. (r i, r' i)) = r) &&& (\<And>r r'. snd \<circ> (\<lambda>i. (r i, r' i)) = r')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst \<circ> (\<lambda>i. (?r2 i, ?r'2 i)) = ?r2
snd \<circ> (\<lambda>i. (?r2 i, ?r'2 i)) = ?r'2

goal (1 subgoal):
 1. \<exists>r'. r = snd \<circ> r' \<and> prod.is_acc_run r'
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
sa.is_run r
local.sa.L \<circ> r \<in> local.igba.lang
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sa.is_run r
local.sa.L \<circ> r \<in> local.igba.lang

goal (1 subgoal):
 1. \<exists>r'. r = snd \<circ> r' \<and> prod.is_acc_run r'
[PROOF STEP]
unfolding prod.is_acc_run_def
        igba.lang_def igba.accept_def[abs_def] igba.is_acc_run_def
[PROOF STATE]
proof (prove)
using this:
sa.is_run r
local.sa.L \<circ> r \<in> {w. \<exists>r. (igba.is_run r \<and> igba.is_acc r) \<and> (\<forall>i. local.igba.L (r i) (w i))}

goal (1 subgoal):
 1. \<exists>r'. r = snd \<circ> r' \<and> prod.is_run r' \<and> prod.is_acc r'
[PROOF STEP]
apply (clarsimp simp: prod_run)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ra. \<lbrakk>sa.is_run r; igba.is_run ra; igba.is_acc ra; \<forall>i. local.igba.L (ra i) (local.sa.L (r i))\<rbrakk> \<Longrightarrow> \<exists>r'. r = snd \<circ> r' \<and> igba.is_run (fst \<circ> r') \<and> sa.is_run (snd \<circ> r') \<and> (\<forall>i. local.igba.L (fst (r' i)) (local.sa.L (snd (r' i)))) \<and> prod.is_acc r'
[PROOF STEP]
apply (rename_tac ra)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ra. \<lbrakk>sa.is_run r; igba.is_run ra; igba.is_acc ra; \<forall>i. local.igba.L (ra i) (local.sa.L (r i))\<rbrakk> \<Longrightarrow> \<exists>r'. r = snd \<circ> r' \<and> igba.is_run (fst \<circ> r') \<and> sa.is_run (snd \<circ> r') \<and> (\<forall>i. local.igba.L (fst (r' i)) (local.sa.L (snd (r' i)))) \<and> prod.is_acc r'
[PROOF STEP]
apply (rule_tac x="\<lambda>i. (ra i, r i)" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ra. \<lbrakk>sa.is_run r; igba.is_run ra; igba.is_acc ra; \<forall>i. local.igba.L (ra i) (local.sa.L (r i))\<rbrakk> \<Longrightarrow> r = snd \<circ> (\<lambda>i. (ra i, r i)) \<and> igba.is_run (fst \<circ> (\<lambda>i. (ra i, r i))) \<and> sa.is_run (snd \<circ> (\<lambda>i. (ra i, r i))) \<and> (\<forall>i. local.igba.L (fst (ra i, r i)) (local.sa.L (snd (ra i, r i)))) \<and> prod.is_acc (\<lambda>i. (ra i, r i))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ra. \<lbrakk>sa.is_run r; igba.is_run ra; igba.is_acc ra; \<forall>i. local.igba.L (ra i) (local.sa.L (r i))\<rbrakk> \<Longrightarrow> prod.is_acc (\<lambda>i. (ra i, r i))
[PROOF STEP]
apply (subst prod_acc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ra. \<lbrakk>sa.is_run r; igba.is_run ra; igba.is_acc ra; \<forall>i. local.igba.L (ra i) (local.sa.L (r i))\<rbrakk> \<Longrightarrow> range (snd \<circ> (\<lambda>i. (ra i, r i))) \<subseteq> sa.V
 2. \<And>ra. \<lbrakk>sa.is_run r; igba.is_run ra; igba.is_acc ra; \<forall>i. local.igba.L (ra i) (local.sa.L (r i))\<rbrakk> \<Longrightarrow> igba.is_acc (fst \<circ> (\<lambda>i. (ra i, r i)))
[PROOF STEP]
using order_trans[OF sa.run_reachable sa.reachable_V]
[PROOF STATE]
proof (prove)
using this:
sa.is_run ?r2 \<Longrightarrow> range ?r2 \<subseteq> sa.V

goal (2 subgoals):
 1. \<And>ra. \<lbrakk>sa.is_run r; igba.is_run ra; igba.is_acc ra; \<forall>i. local.igba.L (ra i) (local.sa.L (r i))\<rbrakk> \<Longrightarrow> range (snd \<circ> (\<lambda>i. (ra i, r i))) \<subseteq> sa.V
 2. \<And>ra. \<lbrakk>sa.is_run r; igba.is_run ra; igba.is_acc ra; \<forall>i. local.igba.L (ra i) (local.sa.L (r i))\<rbrakk> \<Longrightarrow> igba.is_acc (fst \<circ> (\<lambda>i. (ra i, r i)))
[PROOF STEP]
apply auto []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ra. \<lbrakk>sa.is_run r; igba.is_run ra; igba.is_acc ra; \<forall>i. local.igba.L (ra i) (local.sa.L (r i))\<rbrakk> \<Longrightarrow> igba.is_acc (fst \<circ> (\<lambda>i. (ra i, r i)))
[PROOF STEP]
apply auto []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>r'. r = snd \<circ> r' \<and> prod.is_acc_run r'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma var_onceI:
  assumes "map_of \<Gamma> x = Some e"
  shows "(\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G\<^sup>* (delete x \<Gamma>, e , S@[Dummy x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G\<^sup>* (delete x \<Gamma>, e, S @ [Dummy x])
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G\<^sup>* (delete x \<Gamma>, e, S @ [Dummy x])
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
map_of \<Gamma> x = Some e
[PROOF STEP]
have "(\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G (delete x \<Gamma>, e , Upd x # S)"
[PROOF STATE]
proof (prove)
using this:
map_of \<Gamma> x = Some e

goal (1 subgoal):
 1. (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G (delete x \<Gamma>, e, Upd x # S)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G (delete x \<Gamma>, e, Upd x # S)

goal (1 subgoal):
 1. (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G\<^sup>* (delete x \<Gamma>, e, S @ [Dummy x])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G (delete x \<Gamma>, e, Upd x # S)

goal (1 subgoal):
 1. (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G\<^sup>* (delete x \<Gamma>, e, S @ [Dummy x])
[PROOF STEP]
have "\<dots> \<Rightarrow>\<^sub>G  (delete x \<Gamma>, e, S@[Dummy x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (delete x \<Gamma>, e, Upd x # S) \<Rightarrow>\<^sub>G (delete x \<Gamma>, e, S @ [Dummy x])
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(delete x \<Gamma>, e, Upd x # S) \<Rightarrow>\<^sub>G (delete x \<Gamma>, e, S @ [Dummy x])

goal (1 subgoal):
 1. (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G\<^sup>* (delete x \<Gamma>, e, S @ [Dummy x])
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G (delete x \<Gamma>, e, Upd x # S)
(delete x \<Gamma>, e, Upd x # S) \<Rightarrow>\<^sub>G (delete x \<Gamma>, e, S @ [Dummy x])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G (delete x \<Gamma>, e, Upd x # S)
(delete x \<Gamma>, e, Upd x # S) \<Rightarrow>\<^sub>G (delete x \<Gamma>, e, S @ [Dummy x])

goal (1 subgoal):
 1. (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G\<^sup>* (delete x \<Gamma>, e, S @ [Dummy x])
[PROOF STEP]
by (rule converse_rtranclp_into_rtranclp[OF _ r_into_rtranclp])
[PROOF STATE]
proof (state)
this:
(\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G\<^sup>* (delete x \<Gamma>, e, S @ [Dummy x])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma normal_trans:  "c \<Rightarrow>\<^sup>* c' \<Longrightarrow> c \<Rightarrow>\<^sub>G\<^sup>* c'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<Rightarrow>\<^sup>* c' \<Longrightarrow> c \<Rightarrow>\<^sub>G\<^sup>* c'
[PROOF STEP]
by (induction rule:rtranclp_induct)
     (simp, metis normal rtranclp.rtrancl_into_rtrancl)


[STATEMENT]
lemma restr_stack_map_Dummy[simp]: "restr_stack V (map Dummy l) = map Dummy l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restr_stack V (map Dummy l) = map Dummy l
[PROOF STEP]
by (induction l) auto


[STATEMENT]
lemma restr_stack_append[simp]: "restr_stack V (l@l') = restr_stack V l @ restr_stack V l'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restr_stack V (l @ l') = restr_stack V l @ restr_stack V l'
[PROOF STEP]
by (induction l rule: restr_stack.induct) auto


[STATEMENT]
lemma to_gc_conf_append[simp]:
  "to_gc_conf (r@r') c = to_gc_conf r (to_gc_conf r' c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_gc_conf (r @ r') c = to_gc_conf r (to_gc_conf r' c)
[PROOF STEP]
by (cases c) auto


[STATEMENT]
lemma to_gc_conf_eqE[elim!]:
  assumes  "to_gc_conf r c = (\<Gamma>, e, S)"
  obtains \<Gamma>' S' where "c = (\<Gamma>', e, S')" and "\<Gamma> = restrictA (- set r) \<Gamma>'" and "S = restr_stack (- set r) S' @ map Dummy (rev r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<Gamma>' S'. \<lbrakk>c = (\<Gamma>', e, S'); \<Gamma> = restrictA (- set r) \<Gamma>'; S = restr_stack (- set r) S' @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
to_gc_conf r c = (\<Gamma>, e, S)

goal (1 subgoal):
 1. (\<And>\<Gamma>' S'. \<lbrakk>c = (\<Gamma>', e, S'); \<Gamma> = restrictA (- set r) \<Gamma>'; S = restr_stack (- set r) S' @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases c) auto


[STATEMENT]
lemma safe_hd_None[simp]: "safe_hd xs = None \<longleftrightarrow> xs = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (safe_hd xs = None) = (xs = [])
[PROOF STEP]
by (cases xs) auto


[STATEMENT]
lemma safe_hd_restr_stack[simp]:
  "Some a = safe_hd (restr_stack V (a # S)) \<longleftrightarrow> restr_stack V (a # S) = a # restr_stack V S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Some a = safe_hd (restr_stack V (a # S))) = (restr_stack V (a # S) = a # restr_stack V S)
[PROOF STEP]
apply (cases a)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12. a = Alts x11 x12 \<Longrightarrow> (Some a = safe_hd (restr_stack V (a # S))) = (restr_stack V (a # S) = a # restr_stack V S)
 2. \<And>x2. a = Arg x2 \<Longrightarrow> (Some a = safe_hd (restr_stack V (a # S))) = (restr_stack V (a # S) = a # restr_stack V S)
 3. \<And>x3. a = Upd x3 \<Longrightarrow> (Some a = safe_hd (restr_stack V (a # S))) = (restr_stack V (a # S) = a # restr_stack V S)
 4. \<And>x4. a = Dummy x4 \<Longrightarrow> (Some a = safe_hd (restr_stack V (a # S))) = (restr_stack V (a # S) = a # restr_stack V S)
[PROOF STEP]
apply (auto split: if_splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>a = Upd x3; x3 \<notin> V; Some (Upd x3) = safe_hd (restr_stack V S)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (thin_tac "P a" for P)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>x3 \<notin> V; Some (Upd x3) = safe_hd (restr_stack V S)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (induction S rule: restr_stack.induct)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>V x3. \<lbrakk>x3 \<notin> V; Some (Upd x3) = safe_hd (restr_stack V [])\<rbrakk> \<Longrightarrow> False
 2. \<And>V e1 e2 S x3. \<lbrakk>\<And>x3. \<lbrakk>x3 \<notin> V; Some (Upd x3) = safe_hd (restr_stack V S)\<rbrakk> \<Longrightarrow> False; x3 \<notin> V; Some (Upd x3) = safe_hd (restr_stack V (Alts e1 e2 # S))\<rbrakk> \<Longrightarrow> False
 3. \<And>V x S x3. \<lbrakk>\<And>x3. \<lbrakk>x3 \<notin> V; Some (Upd x3) = safe_hd (restr_stack V S)\<rbrakk> \<Longrightarrow> False; x3 \<notin> V; Some (Upd x3) = safe_hd (restr_stack V (Arg x # S))\<rbrakk> \<Longrightarrow> False
 4. \<And>V x S x3. \<lbrakk>\<And>x3. \<lbrakk>x \<in> V; x3 \<notin> V; Some (Upd x3) = safe_hd (restr_stack V S)\<rbrakk> \<Longrightarrow> False; \<And>x3. \<lbrakk>x \<notin> V; x3 \<notin> V; Some (Upd x3) = safe_hd (restr_stack V S)\<rbrakk> \<Longrightarrow> False; x3 \<notin> V; Some (Upd x3) = safe_hd (restr_stack V (Upd x # S))\<rbrakk> \<Longrightarrow> False
 5. \<And>V x S x3. \<lbrakk>\<And>x3. \<lbrakk>x3 \<notin> V; Some (Upd x3) = safe_hd (restr_stack V S)\<rbrakk> \<Longrightarrow> False; x3 \<notin> V; Some (Upd x3) = safe_hd (restr_stack V (Dummy x # S))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (auto split: if_splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sestoftUnGCStack:
  assumes "heap_upds_ok (\<Gamma>, S)"
  obtains \<Gamma>' S' where
    "(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')"
    "to_gc_conf r (\<Gamma>, e, S) = to_gc_conf r (\<Gamma>', e, S')"
    "\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<Gamma>' S'. \<lbrakk>(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S'); to_gc_conf r (\<Gamma>, e, S) = to_gc_conf r (\<Gamma>', e, S'); \<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>\<Gamma>' S'. \<lbrakk>(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S'); to_gc_conf r (\<Gamma>, e, S) = to_gc_conf r (\<Gamma>', e, S'); \<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof(cases "isVal e")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. isVal e \<Longrightarrow> thesis
 2. \<not> isVal e \<Longrightarrow> thesis
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> isVal e

goal (2 subgoals):
 1. isVal e \<Longrightarrow> thesis
 2. \<not> isVal e \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> isVal e

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<not> isVal e
heap_upds_ok (\<Gamma>, S)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by -(rule that, auto)
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. isVal e \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. isVal e \<Longrightarrow> thesis
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
isVal e

goal (1 subgoal):
 1. isVal e \<Longrightarrow> thesis
[PROOF STEP]
from that assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (?\<Gamma>', e, ?S'); to_gc_conf r (\<Gamma>, e, S) = to_gc_conf r (?\<Gamma>', e, ?S'); \<not> isVal e \<or> safe_hd ?S' = safe_hd (restr_stack (- set r) ?S')\<rbrakk> \<Longrightarrow> thesis
heap_upds_ok (\<Gamma>, S)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (?\<Gamma>', e, ?S'); to_gc_conf r (\<Gamma>, e, S) = to_gc_conf r (?\<Gamma>', e, ?S'); \<not> isVal e \<or> safe_hd ?S' = safe_hd (restr_stack (- set r) ?S')\<rbrakk> \<Longrightarrow> thesis
heap_upds_ok (\<Gamma>, S)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
apply (atomize_elim)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. heap_upds_ok (\<Gamma>, S) \<Longrightarrow> \<exists>\<Gamma>' S'. (\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S') \<and> to_gc_conf r (\<Gamma>, e, S) = to_gc_conf r (\<Gamma>', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
[PROOF STEP]
proof(induction S arbitrary: \<Gamma>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<Gamma>. heap_upds_ok (\<Gamma>, []) \<Longrightarrow> \<exists>\<Gamma>' S'. (\<Gamma>, e, []) \<Rightarrow>\<^sup>* (\<Gamma>', e, S') \<and> to_gc_conf r (\<Gamma>, e, []) = to_gc_conf r (\<Gamma>', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
 2. \<And>a S \<Gamma>. \<lbrakk>\<And>\<Gamma>. heap_upds_ok (\<Gamma>, S) \<Longrightarrow> \<exists>\<Gamma>' S'. (\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S') \<and> to_gc_conf r (\<Gamma>, e, S) = to_gc_conf r (\<Gamma>', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S')); heap_upds_ok (\<Gamma>, a # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>' S'. (\<Gamma>, e, a # S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S') \<and> to_gc_conf r (\<Gamma>, e, a # S) = to_gc_conf r (\<Gamma>', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
heap_upds_ok (\<Gamma>, [])

goal (2 subgoals):
 1. \<And>\<Gamma>. heap_upds_ok (\<Gamma>, []) \<Longrightarrow> \<exists>\<Gamma>' S'. (\<Gamma>, e, []) \<Rightarrow>\<^sup>* (\<Gamma>', e, S') \<and> to_gc_conf r (\<Gamma>, e, []) = to_gc_conf r (\<Gamma>', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
 2. \<And>a S \<Gamma>. \<lbrakk>\<And>\<Gamma>. heap_upds_ok (\<Gamma>, S) \<Longrightarrow> \<exists>\<Gamma>' S'. (\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S') \<and> to_gc_conf r (\<Gamma>, e, S) = to_gc_conf r (\<Gamma>', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S')); heap_upds_ok (\<Gamma>, a # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>' S'. (\<Gamma>, e, a # S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S') \<and> to_gc_conf r (\<Gamma>, e, a # S) = to_gc_conf r (\<Gamma>', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
heap_upds_ok (\<Gamma>, [])

goal (1 subgoal):
 1. \<exists>\<Gamma>'' S'. (\<Gamma>, e, []) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> to_gc_conf r (\<Gamma>, e, []) = to_gc_conf r (\<Gamma>'', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
[PROOF STEP]
by (fastforce)
[PROOF STATE]
proof (state)
this:
\<exists>\<Gamma>'' S'. (\<Gamma>, e, []) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> to_gc_conf r (\<Gamma>, e, []) = to_gc_conf r (\<Gamma>'', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))

goal (1 subgoal):
 1. \<And>a S \<Gamma>. \<lbrakk>\<And>\<Gamma>. heap_upds_ok (\<Gamma>, S) \<Longrightarrow> \<exists>\<Gamma>' S'. (\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S') \<and> to_gc_conf r (\<Gamma>, e, S) = to_gc_conf r (\<Gamma>', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S')); heap_upds_ok (\<Gamma>, a # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>' S'. (\<Gamma>, e, a # S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S') \<and> to_gc_conf r (\<Gamma>, e, a # S) = to_gc_conf r (\<Gamma>', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a S \<Gamma>. \<lbrakk>\<And>\<Gamma>. heap_upds_ok (\<Gamma>, S) \<Longrightarrow> \<exists>\<Gamma>' S'. (\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S') \<and> to_gc_conf r (\<Gamma>, e, S) = to_gc_conf r (\<Gamma>', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S')); heap_upds_ok (\<Gamma>, a # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>' S'. (\<Gamma>, e, a # S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S') \<and> to_gc_conf r (\<Gamma>, e, a # S) = to_gc_conf r (\<Gamma>', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
[PROOF STEP]
case (Cons s S)
[PROOF STATE]
proof (state)
this:
heap_upds_ok (?\<Gamma>, S) \<Longrightarrow> \<exists>\<Gamma>' S'. (?\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S') \<and> to_gc_conf r (?\<Gamma>, e, S) = to_gc_conf r (\<Gamma>', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
heap_upds_ok (\<Gamma>, s # S)

goal (1 subgoal):
 1. \<And>a S \<Gamma>. \<lbrakk>\<And>\<Gamma>. heap_upds_ok (\<Gamma>, S) \<Longrightarrow> \<exists>\<Gamma>' S'. (\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S') \<and> to_gc_conf r (\<Gamma>, e, S) = to_gc_conf r (\<Gamma>', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S')); heap_upds_ok (\<Gamma>, a # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>' S'. (\<Gamma>, e, a # S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S') \<and> to_gc_conf r (\<Gamma>, e, a # S) = to_gc_conf r (\<Gamma>', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<Gamma>'' S'. (\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> to_gc_conf r (\<Gamma>, e, s # S) = to_gc_conf r (\<Gamma>'', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
[PROOF STEP]
proof(cases "Some s = safe_hd (restr_stack (- set r) (s#S))")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Some s = safe_hd (restr_stack (- set r) (s # S)) \<Longrightarrow> \<exists>\<Gamma>'' S'. (\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> to_gc_conf r (\<Gamma>, e, s # S) = to_gc_conf r (\<Gamma>'', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
 2. Some s \<noteq> safe_hd (restr_stack (- set r) (s # S)) \<Longrightarrow> \<exists>\<Gamma>'' S'. (\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> to_gc_conf r (\<Gamma>, e, s # S) = to_gc_conf r (\<Gamma>'', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Some s = safe_hd (restr_stack (- set r) (s # S))

goal (2 subgoals):
 1. Some s = safe_hd (restr_stack (- set r) (s # S)) \<Longrightarrow> \<exists>\<Gamma>'' S'. (\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> to_gc_conf r (\<Gamma>, e, s # S) = to_gc_conf r (\<Gamma>'', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
 2. Some s \<noteq> safe_hd (restr_stack (- set r) (s # S)) \<Longrightarrow> \<exists>\<Gamma>'' S'. (\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> to_gc_conf r (\<Gamma>, e, s # S) = to_gc_conf r (\<Gamma>'', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Some s = safe_hd (restr_stack (- set r) (s # S))

goal (1 subgoal):
 1. \<exists>\<Gamma>'' S'. (\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> to_gc_conf r (\<Gamma>, e, s # S) = to_gc_conf r (\<Gamma>'', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
[PROOF STEP]
using \<open>isVal e\<close> \<open>heap_upds_ok (\<Gamma>, s # S)\<close>
[PROOF STATE]
proof (prove)
using this:
Some s = safe_hd (restr_stack (- set r) (s # S))
isVal e
heap_upds_ok (\<Gamma>, s # S)

goal (1 subgoal):
 1. \<exists>\<Gamma>'' S'. (\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> to_gc_conf r (\<Gamma>, e, s # S) = to_gc_conf r (\<Gamma>'', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>restr_stack (- set r) (s # S) = s # restr_stack (- set r) S; isVal e; heap_upds_ok (\<Gamma>, s # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' S'. (\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> restrictA (- set r) \<Gamma> = restrictA (- set r) \<Gamma>'' \<and> s # restr_stack (- set r) S = restr_stack (- set r) S' \<and> safe_hd S' = safe_hd (restr_stack (- set r) S')
[PROOF STEP]
apply (intro exI conjI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>restr_stack (- set r) (s # S) = s # restr_stack (- set r) S; isVal e; heap_upds_ok (\<Gamma>, s # S)\<rbrakk> \<Longrightarrow> (\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (?\<Gamma>'3, e, ?S'4)
 2. \<lbrakk>restr_stack (- set r) (s # S) = s # restr_stack (- set r) S; isVal e; heap_upds_ok (\<Gamma>, s # S)\<rbrakk> \<Longrightarrow> restrictA (- set r) \<Gamma> = restrictA (- set r) ?\<Gamma>'3
 3. \<lbrakk>restr_stack (- set r) (s # S) = s # restr_stack (- set r) S; isVal e; heap_upds_ok (\<Gamma>, s # S)\<rbrakk> \<Longrightarrow> s # restr_stack (- set r) S = restr_stack (- set r) ?S'4
 4. \<lbrakk>restr_stack (- set r) (s # S) = s # restr_stack (- set r) S; isVal e; heap_upds_ok (\<Gamma>, s # S)\<rbrakk> \<Longrightarrow> safe_hd ?S'4 = safe_hd (restr_stack (- set r) ?S'4)
[PROOF STEP]
apply (rule rtranclp.intros(1))
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>restr_stack (- set r) (s # S) = s # restr_stack (- set r) S; isVal e; heap_upds_ok (\<Gamma>, s # S)\<rbrakk> \<Longrightarrow> restrictA (- set r) \<Gamma> = restrictA (- set r) \<Gamma>
 2. \<lbrakk>restr_stack (- set r) (s # S) = s # restr_stack (- set r) S; isVal e; heap_upds_ok (\<Gamma>, s # S)\<rbrakk> \<Longrightarrow> s # restr_stack (- set r) S = restr_stack (- set r) (s # S)
 3. \<lbrakk>restr_stack (- set r) (s # S) = s # restr_stack (- set r) S; isVal e; heap_upds_ok (\<Gamma>, s # S)\<rbrakk> \<Longrightarrow> safe_hd (s # S) = safe_hd (restr_stack (- set r) (s # S))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>\<Gamma>'' S'. (\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> to_gc_conf r (\<Gamma>, e, s # S) = to_gc_conf r (\<Gamma>'', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))

goal (1 subgoal):
 1. Some s \<noteq> safe_hd (restr_stack (- set r) (s # S)) \<Longrightarrow> \<exists>\<Gamma>'' S'. (\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> to_gc_conf r (\<Gamma>, e, s # S) = to_gc_conf r (\<Gamma>'', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Some s \<noteq> safe_hd (restr_stack (- set r) (s # S)) \<Longrightarrow> \<exists>\<Gamma>'' S'. (\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> to_gc_conf r (\<Gamma>, e, s # S) = to_gc_conf r (\<Gamma>'', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
Some s \<noteq> safe_hd (restr_stack (- set r) (s # S))

goal (1 subgoal):
 1. Some s \<noteq> safe_hd (restr_stack (- set r) (s # S)) \<Longrightarrow> \<exists>\<Gamma>'' S'. (\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> to_gc_conf r (\<Gamma>, e, s # S) = to_gc_conf r (\<Gamma>'', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Some s \<noteq> safe_hd (restr_stack (- set r) (s # S))
[PROOF STEP]
obtain x where [simp]: "s = Upd x" and [simp]: "x \<in> set r"
[PROOF STATE]
proof (prove)
using this:
Some s \<noteq> safe_hd (restr_stack (- set r) (s # S))

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>s = Upd x; x \<in> set r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s) (auto split: if_splits)
[PROOF STATE]
proof (state)
this:
s = Upd x
x \<in> set r

goal (1 subgoal):
 1. Some s \<noteq> safe_hd (restr_stack (- set r) (s # S)) \<Longrightarrow> \<exists>\<Gamma>'' S'. (\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> to_gc_conf r (\<Gamma>, e, s # S) = to_gc_conf r (\<Gamma>'', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
[PROOF STEP]
from \<open>heap_upds_ok (\<Gamma>, s # S)\<close> \<open>s = Upd x\<close>
[PROOF STATE]
proof (chain)
picking this:
heap_upds_ok (\<Gamma>, s # S)
s = Upd x
[PROOF STEP]
have [simp]: "x \<notin> domA \<Gamma>" and "heap_upds_ok ((x,e) # \<Gamma>, S)"
[PROOF STATE]
proof (prove)
using this:
heap_upds_ok (\<Gamma>, s # S)
s = Upd x

goal (1 subgoal):
 1. x \<notin> domA \<Gamma> &&& heap_upds_ok ((x, e) # \<Gamma>, S)
[PROOF STEP]
by (auto dest: heap_upds_okE)
[PROOF STATE]
proof (state)
this:
x \<notin> domA \<Gamma>
heap_upds_ok ((x, e) # \<Gamma>, S)

goal (1 subgoal):
 1. Some s \<noteq> safe_hd (restr_stack (- set r) (s # S)) \<Longrightarrow> \<exists>\<Gamma>'' S'. (\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> to_gc_conf r (\<Gamma>, e, s # S) = to_gc_conf r (\<Gamma>'', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
[PROOF STEP]
have "(\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>, e, Upd x # S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>, e, Upd x # S)
[PROOF STEP]
unfolding \<open>s = _\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Gamma>, e, Upd x # S) \<Rightarrow>\<^sup>* (\<Gamma>, e, Upd x # S)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>, e, Upd x # S)

goal (1 subgoal):
 1. Some s \<noteq> safe_hd (restr_stack (- set r) (s # S)) \<Longrightarrow> \<exists>\<Gamma>'' S'. (\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> to_gc_conf r (\<Gamma>, e, s # S) = to_gc_conf r (\<Gamma>'', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>, e, Upd x # S)

goal (1 subgoal):
 1. Some s \<noteq> safe_hd (restr_stack (- set r) (s # S)) \<Longrightarrow> \<exists>\<Gamma>'' S'. (\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> to_gc_conf r (\<Gamma>, e, s # S) = to_gc_conf r (\<Gamma>'', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
[PROOF STEP]
have "\<dots> \<Rightarrow> ((x,e) # \<Gamma>, e, S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Gamma>, e, Upd x # S) \<Rightarrow> ((x, e) # \<Gamma>, e, S)
[PROOF STEP]
by (rule step.var\<^sub>2[OF \<open>x \<notin> domA \<Gamma>\<close> \<open>isVal e\<close>])
[PROOF STATE]
proof (state)
this:
(\<Gamma>, e, Upd x # S) \<Rightarrow> ((x, e) # \<Gamma>, e, S)

goal (1 subgoal):
 1. Some s \<noteq> safe_hd (restr_stack (- set r) (s # S)) \<Longrightarrow> \<exists>\<Gamma>'' S'. (\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> to_gc_conf r (\<Gamma>, e, s # S) = to_gc_conf r (\<Gamma>'', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Gamma>, e, Upd x # S) \<Rightarrow> ((x, e) # \<Gamma>, e, S)

goal (1 subgoal):
 1. Some s \<noteq> safe_hd (restr_stack (- set r) (s # S)) \<Longrightarrow> \<exists>\<Gamma>'' S'. (\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> to_gc_conf r (\<Gamma>, e, s # S) = to_gc_conf r (\<Gamma>'', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
[PROOF STEP]
from Cons.IH[OF \<open>heap_upds_ok ((x,e) # \<Gamma>, S)\<close> ]
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<Gamma>'' S'. ((x, e) # \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> to_gc_conf r ((x, e) # \<Gamma>, e, S) = to_gc_conf r (\<Gamma>'', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
[PROOF STEP]
obtain \<Gamma>' S' where  "((x,e) # \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')"
            and res: "to_gc_conf r ((x,e) # \<Gamma>, e, S) = to_gc_conf r (\<Gamma>', e, S')"
                     "(\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))"
[PROOF STATE]
proof (prove)
using this:
\<exists>\<Gamma>'' S'. ((x, e) # \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> to_gc_conf r ((x, e) # \<Gamma>, e, S) = to_gc_conf r (\<Gamma>'', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))

goal (1 subgoal):
 1. (\<And>\<Gamma>'' S'. \<lbrakk>((x, e) # \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S'); to_gc_conf r ((x, e) # \<Gamma>, e, S) = to_gc_conf r (\<Gamma>'', e, S'); \<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
((x, e) # \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')
to_gc_conf r ((x, e) # \<Gamma>, e, S) = to_gc_conf r (\<Gamma>', e, S')
\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S')

goal (1 subgoal):
 1. Some s \<noteq> safe_hd (restr_stack (- set r) (s # S)) \<Longrightarrow> \<exists>\<Gamma>'' S'. (\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> to_gc_conf r (\<Gamma>, e, s # S) = to_gc_conf r (\<Gamma>'', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
[PROOF STEP]
note this(1)
[PROOF STATE]
proof (state)
this:
((x, e) # \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')

goal (1 subgoal):
 1. Some s \<noteq> safe_hd (restr_stack (- set r) (s # S)) \<Longrightarrow> \<exists>\<Gamma>'' S'. (\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> to_gc_conf r (\<Gamma>, e, s # S) = to_gc_conf r (\<Gamma>'', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')
[PROOF STEP]
have "(\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')"
[PROOF STATE]
proof (prove)
using this:
(\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')

goal (1 subgoal):
 1. (\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')

goal (1 subgoal):
 1. Some s \<noteq> safe_hd (restr_stack (- set r) (s # S)) \<Longrightarrow> \<exists>\<Gamma>'' S'. (\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> to_gc_conf r (\<Gamma>, e, s # S) = to_gc_conf r (\<Gamma>'', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')

goal (1 subgoal):
 1. \<exists>\<Gamma>'' S'. (\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> to_gc_conf r (\<Gamma>, e, s # S) = to_gc_conf r (\<Gamma>'', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
[PROOF STEP]
using res
[PROOF STATE]
proof (prove)
using this:
(\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')
to_gc_conf r ((x, e) # \<Gamma>, e, S) = to_gc_conf r (\<Gamma>', e, S')
\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S')

goal (1 subgoal):
 1. \<exists>\<Gamma>'' S'. (\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> to_gc_conf r (\<Gamma>, e, s # S) = to_gc_conf r (\<Gamma>'', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>\<Gamma>'' S'. (\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> to_gc_conf r (\<Gamma>, e, s # S) = to_gc_conf r (\<Gamma>'', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>\<Gamma>'' S'. (\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>'', e, S') \<and> to_gc_conf r (\<Gamma>, e, s # S) = to_gc_conf r (\<Gamma>'', e, S') \<and> (\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma perm_exI_trivial:
  "P x x \<Longrightarrow> \<exists> \<pi>. P (\<pi> \<bullet> x) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P x x \<Longrightarrow> \<exists>\<pi>. P (\<pi> \<bullet> x) x
[PROOF STEP]
by (rule exI[where x = "0::perm"]) auto


[STATEMENT]
lemma upds_list_restr_stack[simp]:
  "upds_list (restr_stack V S) = filter (\<lambda> x. x\<in>V) (upds_list S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upds_list (restr_stack V S) = filter (\<lambda>x. x \<in> V) (upds_list S)
[PROOF STEP]
by (induction S rule: restr_stack.induct) auto


[STATEMENT]
lemma heap_upd_ok_to_gc_conf:
  "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> to_gc_conf r (\<Gamma>, e, S) = (\<Gamma>'', e'', S'') \<Longrightarrow> heap_upds_ok (\<Gamma>'', S'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_upds_ok (\<Gamma>, S); to_gc_conf r (\<Gamma>, e, S) = (\<Gamma>'', e'', S'')\<rbrakk> \<Longrightarrow> heap_upds_ok (\<Gamma>'', S'')
[PROOF STEP]
by (auto simp add: heap_upds_ok.simps)


[STATEMENT]
lemma delete_restrictA_conv:
  "delete x \<Gamma> = restrictA (-{x}) \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delete x \<Gamma> = restrictA (- {x}) \<Gamma>
[PROOF STEP]
by (induction \<Gamma>) auto