[STATEMENT]
lemma degen_invar: "b_graph (degeneralize_ext ecnv)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b_graph (degeneralize_ext ecnv)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. g_V0 (degeneralize_ext ecnv) \<subseteq> g_V (degeneralize_ext ecnv)
 2. g_E (degeneralize_ext ecnv) \<subseteq> g_V (degeneralize_ext ecnv) \<times> g_V (degeneralize_ext ecnv)
 3. bg_F (degeneralize_ext ecnv) \<subseteq> g_V (degeneralize_ext ecnv)
[PROOF STEP]
let ?G' = "degeneralize_ext ecnv"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. g_V0 (degeneralize_ext ecnv) \<subseteq> g_V (degeneralize_ext ecnv)
 2. g_E (degeneralize_ext ecnv) \<subseteq> g_V (degeneralize_ext ecnv) \<times> g_V (degeneralize_ext ecnv)
 3. bg_F (degeneralize_ext ecnv) \<subseteq> g_V (degeneralize_ext ecnv)
[PROOF STEP]
show "g_V0 ?G' \<subseteq> g_V ?G'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g_V0 (degeneralize_ext ecnv) \<subseteq> g_V (degeneralize_ext ecnv)
[PROOF STEP]
unfolding degeneralize_ext_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g_V0 (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> = ecnv 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> = ecnv G\<rparr>) \<subseteq> g_V (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> = ecnv 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> = ecnv G\<rparr>)
[PROOF STEP]
using V0_ss
[PROOF STATE]
proof (prove)
using this:
V0 \<subseteq> V

goal (1 subgoal):
 1. g_V0 (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> = ecnv 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> = ecnv G\<rparr>) \<subseteq> g_V (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> = ecnv 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> = ecnv G\<rparr>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g_V0 (degeneralize_ext ecnv) \<subseteq> g_V (degeneralize_ext ecnv)

goal (2 subgoals):
 1. g_E (degeneralize_ext ecnv) \<subseteq> g_V (degeneralize_ext ecnv) \<times> g_V (degeneralize_ext ecnv)
 2. bg_F (degeneralize_ext ecnv) \<subseteq> g_V (degeneralize_ext ecnv)
[PROOF STEP]
show "g_E ?G' \<subseteq> g_V ?G' \<times> g_V ?G'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g_E (degeneralize_ext ecnv) \<subseteq> g_V (degeneralize_ext ecnv) \<times> g_V (degeneralize_ext ecnv)
[PROOF STEP]
unfolding degeneralize_ext_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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> = ecnv 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> = ecnv G\<rparr>) \<subseteq> g_V (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> = ecnv 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> = ecnv G\<rparr>) \<times> g_V (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> = ecnv 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> = ecnv G\<rparr>)
[PROOF STEP]
using E_ss
[PROOF STATE]
proof (prove)
using this:
E \<subseteq> V \<times> V

goal (1 subgoal):
 1. 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> = ecnv 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> = ecnv G\<rparr>) \<subseteq> g_V (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> = ecnv 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> = ecnv G\<rparr>) \<times> g_V (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> = ecnv 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> = ecnv G\<rparr>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g_E (degeneralize_ext ecnv) \<subseteq> g_V (degeneralize_ext ecnv) \<times> g_V (degeneralize_ext ecnv)

goal (1 subgoal):
 1. bg_F (degeneralize_ext ecnv) \<subseteq> g_V (degeneralize_ext ecnv)
[PROOF STEP]
show "bg_F ?G' \<subseteq> g_V ?G'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bg_F (degeneralize_ext ecnv) \<subseteq> g_V (degeneralize_ext ecnv)
[PROOF STEP]
unfolding degeneralize_ext_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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> = ecnv 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> = ecnv G\<rparr>) \<subseteq> g_V (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> = ecnv 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> = ecnv G\<rparr>)
[PROOF STEP]
using acc_ss
[PROOF STATE]
proof (prove)
using this:
acc ?q \<noteq> {} \<Longrightarrow> ?q \<in> V

goal (1 subgoal):
 1. 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> = ecnv 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> = ecnv G\<rparr>) \<subseteq> g_V (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> = ecnv 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> = ecnv G\<rparr>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bg_F (degeneralize_ext ecnv) \<subseteq> g_V (degeneralize_ext ecnv)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma degen_finite_reachable:
    assumes [simp, intro]: "finite (E\<^sup>* `` V0)"
    shows "finite ((g_E (degeneralize_ext ecnv))\<^sup>* `` g_V0 (degeneralize_ext ecnv))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ((g_E (degeneralize_ext ecnv))\<^sup>* `` g_V0 (degeneralize_ext ecnv))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite ((g_E (degeneralize_ext ecnv))\<^sup>* `` g_V0 (degeneralize_ext ecnv))
[PROOF STEP]
let ?G' = "degeneralize_ext ecnv"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite ((g_E (degeneralize_ext ecnv))\<^sup>* `` g_V0 (degeneralize_ext ecnv))
[PROOF STEP]
have "((g_E ?G')\<^sup>* `` g_V0 ?G')
      \<subseteq> E\<^sup>*``V0 \<times> {0..num_acc}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g_E (degeneralize_ext ecnv))\<^sup>* `` g_V0 (degeneralize_ext ecnv) \<subseteq> reachable \<times> {0..num_acc}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (g_E (degeneralize_ext ecnv))\<^sup>* `` g_V0 (degeneralize_ext ecnv) \<subseteq> reachable \<times> {0..num_acc}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (g_E (degeneralize_ext ecnv))\<^sup>* `` g_V0 (degeneralize_ext ecnv) \<subseteq> reachable \<times> {0..num_acc}
[PROOF STEP]
fix q n q' n'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (g_E (degeneralize_ext ecnv))\<^sup>* `` g_V0 (degeneralize_ext ecnv) \<subseteq> reachable \<times> {0..num_acc}
[PROOF STEP]
assume "((q,n),(q',n'))\<in>(g_E ?G')\<^sup>*"
          and 0: "(q,n)\<in>g_V0 ?G'"
[PROOF STATE]
proof (state)
this:
((q, n), q', n') \<in> (g_E (degeneralize_ext ecnv))\<^sup>*
(q, n) \<in> g_V0 (degeneralize_ext ecnv)

goal (1 subgoal):
 1. (g_E (degeneralize_ext ecnv))\<^sup>* `` g_V0 (degeneralize_ext ecnv) \<subseteq> reachable \<times> {0..num_acc}
[PROOF STEP]
hence G1: "(q,q')\<in>E\<^sup>* \<and> n'\<le>num_acc"
[PROOF STATE]
proof (prove)
using this:
((q, n), q', n') \<in> (g_E (degeneralize_ext ecnv))\<^sup>*
(q, n) \<in> g_V0 (degeneralize_ext ecnv)

goal (1 subgoal):
 1. (q, q') \<in> E\<^sup>* \<and> n' \<le> num_acc
[PROOF STEP]
apply (induction rule: rtrancl_induct2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (q, n) \<in> g_V0 (degeneralize_ext ecnv) \<Longrightarrow> (q, q) \<in> E\<^sup>* \<and> n \<le> num_acc
 2. \<And>a b aa ba. \<lbrakk>((q, n), a, b) \<in> (g_E (degeneralize_ext ecnv))\<^sup>*; ((a, b), aa, ba) \<in> g_E (degeneralize_ext ecnv); (q, n) \<in> g_V0 (degeneralize_ext ecnv) \<Longrightarrow> (q, a) \<in> E\<^sup>* \<and> b \<le> num_acc; (q, n) \<in> g_V0 (degeneralize_ext ecnv)\<rbrakk> \<Longrightarrow> (q, aa) \<in> E\<^sup>* \<and> ba \<le> num_acc
[PROOF STEP]
by (auto simp: degeneralize_ext_def split: if_split_asm)
[PROOF STATE]
proof (state)
this:
(q, q') \<in> E\<^sup>* \<and> n' \<le> num_acc

goal (1 subgoal):
 1. (g_E (degeneralize_ext ecnv))\<^sup>* `` g_V0 (degeneralize_ext ecnv) \<subseteq> reachable \<times> {0..num_acc}
[PROOF STEP]
from 0
[PROOF STATE]
proof (chain)
picking this:
(q, n) \<in> g_V0 (degeneralize_ext ecnv)
[PROOF STEP]
have G2: "q\<in>V0 \<and> n\<le>num_acc"
[PROOF STATE]
proof (prove)
using this:
(q, n) \<in> g_V0 (degeneralize_ext ecnv)

goal (1 subgoal):
 1. q \<in> V0 \<and> n \<le> num_acc
[PROOF STEP]
by (auto simp: degeneralize_ext_def split: if_split_asm)
[PROOF STATE]
proof (state)
this:
q \<in> V0 \<and> n \<le> num_acc

goal (1 subgoal):
 1. (g_E (degeneralize_ext ecnv))\<^sup>* `` g_V0 (degeneralize_ext ecnv) \<subseteq> reachable \<times> {0..num_acc}
[PROOF STEP]
note G1 G2
[PROOF STATE]
proof (state)
this:
(q, q') \<in> E\<^sup>* \<and> n' \<le> num_acc
q \<in> V0 \<and> n \<le> num_acc

goal (1 subgoal):
 1. (g_E (degeneralize_ext ecnv))\<^sup>* `` g_V0 (degeneralize_ext ecnv) \<subseteq> reachable \<times> {0..num_acc}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>((?q4, ?n4), ?q'4, ?n'4) \<in> (g_E (degeneralize_ext ecnv))\<^sup>*; (?q4, ?n4) \<in> g_V0 (degeneralize_ext ecnv)\<rbrakk> \<Longrightarrow> (?q4, ?q'4) \<in> E\<^sup>* \<and> ?n'4 \<le> num_acc
\<lbrakk>((?q4, ?n4), ?q'4, ?n'4) \<in> (g_E (degeneralize_ext ecnv))\<^sup>*; (?q4, ?n4) \<in> g_V0 (degeneralize_ext ecnv)\<rbrakk> \<Longrightarrow> ?q4 \<in> V0 \<and> ?n4 \<le> num_acc

goal (1 subgoal):
 1. (g_E (degeneralize_ext ecnv))\<^sup>* `` g_V0 (degeneralize_ext ecnv) \<subseteq> reachable \<times> {0..num_acc}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>((?q4, ?n4), ?q'4, ?n'4) \<in> (g_E (degeneralize_ext ecnv))\<^sup>*; (?q4, ?n4) \<in> g_V0 (degeneralize_ext ecnv)\<rbrakk> \<Longrightarrow> (?q4, ?q'4) \<in> E\<^sup>* \<and> ?n'4 \<le> num_acc
\<lbrakk>((?q4, ?n4), ?q'4, ?n'4) \<in> (g_E (degeneralize_ext ecnv))\<^sup>*; (?q4, ?n4) \<in> g_V0 (degeneralize_ext ecnv)\<rbrakk> \<Longrightarrow> ?q4 \<in> V0 \<and> ?n4 \<le> num_acc

goal (1 subgoal):
 1. (g_E (degeneralize_ext ecnv))\<^sup>* `` g_V0 (degeneralize_ext ecnv) \<subseteq> reachable \<times> {0..num_acc}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(g_E (degeneralize_ext ecnv))\<^sup>* `` g_V0 (degeneralize_ext ecnv) \<subseteq> reachable \<times> {0..num_acc}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(g_E (degeneralize_ext ecnv))\<^sup>* `` g_V0 (degeneralize_ext ecnv) \<subseteq> reachable \<times> {0..num_acc}

goal (1 subgoal):
 1. finite ((g_E (degeneralize_ext ecnv))\<^sup>* `` g_V0 (degeneralize_ext ecnv))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(g_E (degeneralize_ext ecnv))\<^sup>* `` g_V0 (degeneralize_ext ecnv) \<subseteq> reachable \<times> {0..num_acc}

goal (1 subgoal):
 1. finite ((g_E (degeneralize_ext ecnv))\<^sup>* `` g_V0 (degeneralize_ext ecnv))
[PROOF STEP]
have "finite \<dots>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (reachable \<times> {0..num_acc})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (reachable \<times> {0..num_acc})

goal (1 subgoal):
 1. finite ((g_E (degeneralize_ext ecnv))\<^sup>* `` g_V0 (degeneralize_ext ecnv))
[PROOF STEP]
finally (finite_subset)
[PROOF STATE]
proof (chain)
picking this:
finite ((g_E (degeneralize_ext ecnv))\<^sup>* `` g_V0 (degeneralize_ext ecnv))
[PROOF STEP]
show "finite ((g_E ?G')\<^sup>* `` g_V0 ?G')"
[PROOF STATE]
proof (prove)
using this:
finite ((g_E (degeneralize_ext ecnv))\<^sup>* `` g_V0 (degeneralize_ext ecnv))

goal (1 subgoal):
 1. finite ((g_E (degeneralize_ext ecnv))\<^sup>* `` g_V0 (degeneralize_ext ecnv))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
finite ((g_E (degeneralize_ext ecnv))\<^sup>* `` g_V0 (degeneralize_ext ecnv))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma degen_is_run_sound:
    "degen.is_run T m r \<Longrightarrow> is_run (fst o r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph_defs.is_run (degeneralize_ext m) r \<Longrightarrow> is_run (fst \<circ> r)
[PROOF STEP]
unfolding degen.is_run_def is_run_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r 0 \<in> g_V0 (degeneralize_ext m) \<and> ipath (g_E (degeneralize_ext m)) r \<Longrightarrow> (fst \<circ> r) 0 \<in> V0 \<and> ipath E (fst \<circ> r)
[PROOF STEP]
unfolding degeneralize_ext_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r 0 \<in> g_V0 (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>) \<and> ipath (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>)) r \<Longrightarrow> (fst \<circ> r) 0 \<in> V0 \<and> ipath E (fst \<circ> r)
[PROOF STEP]
apply (clarsimp split: if_split_asm simp: ipath_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x i. \<lbrakk>num_acc = 0; \<forall>i. \<exists>q. r i = (q, 0) \<and> (\<exists>q'. r (Suc i) = (q', 0) \<and> (q, q') \<in> E); x \<in> V0; r 0 = (x, 0)\<rbrakk> \<Longrightarrow> (fst (r i), fst (r (Suc i))) \<in> E
 2. \<And>x i. \<lbrakk>0 < num_acc; \<forall>i. \<exists>ia q. (ia \<in> acc q \<longrightarrow> r i = (q, ia) \<and> (\<exists>q'. r (Suc i) = (q', Suc ia mod num_acc) \<and> (q, q') \<in> E)) \<and> (ia \<in> acc q \<or> ia < num_acc \<and> r i = (q, ia) \<and> (\<exists>q'. r (Suc i) = (q', ia) \<and> (q, q') \<in> E)); x \<in> V0; r 0 = (x, 0)\<rbrakk> \<Longrightarrow> (fst (r i), fst (r (Suc i))) \<in> E
[PROOF STEP]
apply (metis fst_conv)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma degen_path_sound:
    assumes "path (degen.E T m) u p v"
    shows "path E (fst u) (map fst p) (fst v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path E (fst u) (map fst p) (fst v)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
path (g_E (degeneralize_ext m)) u p v

goal (1 subgoal):
 1. path E (fst u) (map fst p) (fst v)
[PROOF STEP]
by induction (auto simp: degeneralize_ext_def path_simps split: if_split_asm)


[STATEMENT]
lemma degen_V0_sound:
    assumes "u \<in> degen.V0 T m"
    shows "fst u \<in> V0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst u \<in> V0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
u \<in> g_V0 (degeneralize_ext m)

goal (1 subgoal):
 1. fst u \<in> V0
[PROOF STEP]
by (auto simp: degeneralize_ext_def path_simps split: if_split_asm)


[STATEMENT]
lemma degen_visit_acc:
    assumes "path (degen.E T m) (q,n) p (q',n')"
    assumes "n\<noteq>n'"
    shows "\<exists>qa. (qa,n)\<in>set p \<and> n\<in>acc qa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>qa. (qa, n) \<in> set p \<and> n \<in> acc qa
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
path (g_E (degeneralize_ext m)) (q, n) p (q', n')
n \<noteq> n'

goal (1 subgoal):
 1. \<exists>qa. (qa, n) \<in> set p \<and> n \<in> acc qa
[PROOF STEP]
proof (induction _ "(q,n)" p "(q',n')" arbitrary: q rule: path.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>n = n'; n \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>qa. (qa, n) \<in> set [] \<and> n \<in> acc qa
 2. \<And>v l q. \<lbrakk>((q, n), v) \<in> g_E (degeneralize_ext m); path (g_E (degeneralize_ext m)) v l (q', n'); \<And>q. \<lbrakk>v = (q, n); n \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>qa. (qa, n) \<in> set l \<and> n \<in> acc qa; n \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>qa. (qa, n) \<in> set ((q, n) # l) \<and> n \<in> acc qa
[PROOF STEP]
case (path_prepend qnh p)
[PROOF STATE]
proof (state)
this:
((q, n), qnh) \<in> g_E (degeneralize_ext m)
path (g_E (degeneralize_ext m)) qnh p (q', n')
\<lbrakk>qnh = (?q2, n); n \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>qa. (qa, n) \<in> set p \<and> n \<in> acc qa
n \<noteq> n'

goal (2 subgoals):
 1. \<lbrakk>n = n'; n \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>qa. (qa, n) \<in> set [] \<and> n \<in> acc qa
 2. \<And>v l q. \<lbrakk>((q, n), v) \<in> g_E (degeneralize_ext m); path (g_E (degeneralize_ext m)) v l (q', n'); \<And>q. \<lbrakk>v = (q, n); n \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>qa. (qa, n) \<in> set l \<and> n \<in> acc qa; n \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>qa. (qa, n) \<in> set ((q, n) # l) \<and> n \<in> acc qa
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((q, n), qnh) \<in> g_E (degeneralize_ext m)
path (g_E (degeneralize_ext m)) qnh p (q', n')
\<lbrakk>qnh = (?q2, n); n \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>qa. (qa, n) \<in> set p \<and> n \<in> acc qa
n \<noteq> n'
[PROOF STEP]
obtain qh nh where [simp]: "qnh=(qh,nh)"
[PROOF STATE]
proof (prove)
using this:
((q, n), qnh) \<in> g_E (degeneralize_ext m)
path (g_E (degeneralize_ext m)) qnh p (q', n')
\<lbrakk>qnh = (?q2, n); n \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>qa. (qa, n) \<in> set p \<and> n \<in> acc qa
n \<noteq> n'

goal (1 subgoal):
 1. (\<And>qh nh. qnh = (qh, nh) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases qnh)
[PROOF STATE]
proof (state)
this:
qnh = (qh, nh)

goal (2 subgoals):
 1. \<lbrakk>n = n'; n \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>qa. (qa, n) \<in> set [] \<and> n \<in> acc qa
 2. \<And>v l q. \<lbrakk>((q, n), v) \<in> g_E (degeneralize_ext m); path (g_E (degeneralize_ext m)) v l (q', n'); \<And>q. \<lbrakk>v = (q, n); n \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>qa. (qa, n) \<in> set l \<and> n \<in> acc qa; n \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>qa. (qa, n) \<in> set ((q, n) # l) \<and> n \<in> acc qa
[PROOF STEP]
from \<open>((q,n),qnh) \<in> degen.E T m\<close>
[PROOF STATE]
proof (chain)
picking this:
((q, n), qnh) \<in> g_E (degeneralize_ext m)
[PROOF STEP]
have "nh=n \<or> (nh=(n+1) mod num_acc \<and> n\<in>acc q)"
[PROOF STATE]
proof (prove)
using this:
((q, n), qnh) \<in> g_E (degeneralize_ext m)

goal (1 subgoal):
 1. nh = n \<or> nh = (n + 1) mod num_acc \<and> n \<in> acc q
[PROOF STEP]
by (auto simp: degeneralize_ext_def split: if_split_asm)
[PROOF STATE]
proof (state)
this:
nh = n \<or> nh = (n + 1) mod num_acc \<and> n \<in> acc q

goal (2 subgoals):
 1. \<lbrakk>n = n'; n \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>qa. (qa, n) \<in> set [] \<and> n \<in> acc qa
 2. \<And>v l q. \<lbrakk>((q, n), v) \<in> g_E (degeneralize_ext m); path (g_E (degeneralize_ext m)) v l (q', n'); \<And>q. \<lbrakk>v = (q, n); n \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>qa. (qa, n) \<in> set l \<and> n \<in> acc qa; n \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>qa. (qa, n) \<in> set ((q, n) # l) \<and> n \<in> acc qa
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
nh = n \<or> nh = (n + 1) mod num_acc \<and> n \<in> acc q

goal (1 subgoal):
 1. \<exists>qaa. (qaa, n) \<in> set ((q, n) # p) \<and> n \<in> acc qaa
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. nh = n \<Longrightarrow> \<exists>qaa. (qaa, n) \<in> set ((q, n) # p) \<and> n \<in> acc qaa
 2. nh = (n + 1) mod num_acc \<and> n \<in> acc q \<Longrightarrow> \<exists>qaa. (qaa, n) \<in> set ((q, n) # p) \<and> n \<in> acc qaa
[PROOF STEP]
assume [simp]: "nh=n"
[PROOF STATE]
proof (state)
this:
nh = n

goal (2 subgoals):
 1. nh = n \<Longrightarrow> \<exists>qaa. (qaa, n) \<in> set ((q, n) # p) \<and> n \<in> acc qaa
 2. nh = (n + 1) mod num_acc \<and> n \<in> acc q \<Longrightarrow> \<exists>qaa. (qaa, n) \<in> set ((q, n) # p) \<and> n \<in> acc qaa
[PROOF STEP]
from path_prepend
[PROOF STATE]
proof (chain)
picking this:
((q, n), qnh) \<in> g_E (degeneralize_ext m)
path (g_E (degeneralize_ext m)) qnh p (q', n')
\<lbrakk>qnh = (?q2, n); n \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>qa. (qa, n) \<in> set p \<and> n \<in> acc qa
n \<noteq> n'
[PROOF STEP]
obtain qa where "(qa, n) \<in> set p" and "n \<in> acc qa"
[PROOF STATE]
proof (prove)
using this:
((q, n), qnh) \<in> g_E (degeneralize_ext m)
path (g_E (degeneralize_ext m)) qnh p (q', n')
\<lbrakk>qnh = (?q2, n); n \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>qa. (qa, n) \<in> set p \<and> n \<in> acc qa
n \<noteq> n'

goal (1 subgoal):
 1. (\<And>qa. \<lbrakk>(qa, n) \<in> set p; n \<in> acc qa\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(qa, n) \<in> set p
n \<in> acc qa

goal (2 subgoals):
 1. nh = n \<Longrightarrow> \<exists>qaa. (qaa, n) \<in> set ((q, n) # p) \<and> n \<in> acc qaa
 2. nh = (n + 1) mod num_acc \<and> n \<in> acc q \<Longrightarrow> \<exists>qaa. (qaa, n) \<in> set ((q, n) # p) \<and> n \<in> acc qaa
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(qa, n) \<in> set p
n \<in> acc qa

goal (1 subgoal):
 1. \<exists>qaa. (qaa, n) \<in> set ((q, n) # p) \<and> n \<in> acc qaa
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>qaa. (qaa, n) \<in> set ((q, n) # p) \<and> n \<in> acc qaa

goal (1 subgoal):
 1. nh = (n + 1) mod num_acc \<and> n \<in> acc q \<Longrightarrow> \<exists>qaa. (qaa, n) \<in> set ((q, n) # p) \<and> n \<in> acc qaa
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nh = (n + 1) mod num_acc \<and> n \<in> acc q \<Longrightarrow> \<exists>qaa. (qaa, n) \<in> set ((q, n) # p) \<and> n \<in> acc qaa
[PROOF STEP]
assume "(nh=(n+1) mod num_acc \<and> n\<in>acc q)"
[PROOF STATE]
proof (state)
this:
nh = (n + 1) mod num_acc \<and> n \<in> acc q

goal (1 subgoal):
 1. nh = (n + 1) mod num_acc \<and> n \<in> acc q \<Longrightarrow> \<exists>qaa. (qaa, n) \<in> set ((q, n) # p) \<and> n \<in> acc qaa
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
nh = (n + 1) mod num_acc \<and> n \<in> acc q

goal (1 subgoal):
 1. \<exists>qaa. (qaa, n) \<in> set ((q, n) # p) \<and> n \<in> acc qaa
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>qaa. (qaa, n) \<in> set ((q, n) # p) \<and> n \<in> acc qaa

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>qaa. (qaa, n) \<in> set ((q, n) # p) \<and> n \<in> acc qaa

goal (1 subgoal):
 1. \<lbrakk>n = n'; n \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>qa. (qa, n) \<in> set [] \<and> n \<in> acc qa
[PROOF STEP]
qed simp


[STATEMENT]
lemma degen_run_complete0:
    assumes [simp]: "num_acc = 0"
    assumes R: "is_run r"
    shows "degen.is_run T m (\<lambda>i. (r i,0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph_defs.is_run (degeneralize_ext m) (\<lambda>i. (r i, 0))
[PROOF STEP]
using R
[PROOF STATE]
proof (prove)
using this:
is_run r

goal (1 subgoal):
 1. graph_defs.is_run (degeneralize_ext m) (\<lambda>i. (r i, 0))
[PROOF STEP]
unfolding degen.is_run_def is_run_def
[PROOF STATE]
proof (prove)
using this:
r 0 \<in> V0 \<and> ipath E r

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

goal (1 subgoal):
 1. (r 0, 0) \<in> g_V0 (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>) \<and> (\<forall>i. ((r i, 0), r (Suc i), 0) \<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>))
[PROOF STEP]
by auto


[STATEMENT]
lemma degen_acc_run_complete0:
    assumes [simp]: "num_acc = 0"
    assumes R: "is_acc_run r"
    shows "degen.is_acc_run T m (\<lambda>i. (r i,0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b_graph.is_acc_run (degeneralize_ext m) (\<lambda>i. (r i, 0))
[PROOF STEP]
using R
[PROOF STATE]
proof (prove)
using this:
is_acc_run r

goal (1 subgoal):
 1. b_graph.is_acc_run (degeneralize_ext m) (\<lambda>i. (r i, 0))
[PROOF STEP]
unfolding degen.is_acc_run_def is_acc_run_def is_acc_def degen.is_acc_def
[PROOF STATE]
proof (prove)
using this:
is_run r \<and> (\<forall>n<num_acc. \<exists>\<^sub>\<infinity>i. n \<in> acc (r i))

goal (1 subgoal):
 1. graph_defs.is_run (degeneralize_ext m) (\<lambda>i. (r i, 0)) \<and> (\<exists>\<^sub>\<infinity>i. (r i, 0) \<in> bg_F (degeneralize_ext m))
[PROOF STEP]
apply (simp add: degen_run_complete0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_run r \<Longrightarrow> \<exists>\<^sub>\<infinity>i. (r i, 0) \<in> bg_F (degeneralize_ext m)
[PROOF STEP]
unfolding degeneralize_ext_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_run r \<Longrightarrow> \<exists>\<^sub>\<infinity>i. (r i, 0) \<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>)
[PROOF STEP]
using run_reachable[of r] reachable_V
[PROOF STATE]
proof (prove)
using this:
is_run r \<Longrightarrow> range r \<subseteq> reachable
reachable \<subseteq> V

goal (1 subgoal):
 1. is_run r \<Longrightarrow> \<exists>\<^sub>\<infinity>i. (r i, 0) \<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>)
[PROOF STEP]
by (auto simp: INFM_nat)


[STATEMENT]
lemma degen_run_complete:
    assumes [simp]: "num_acc \<noteq> 0"
    assumes R: "is_run r"
    shows "\<exists>r'. degen.is_run T m r' \<and> r = fst o r'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r'. graph_defs.is_run (degeneralize_ext m) r' \<and> r = fst \<circ> r'
[PROOF STEP]
using R
[PROOF STATE]
proof (prove)
using this:
is_run r

goal (1 subgoal):
 1. \<exists>r'. graph_defs.is_run (degeneralize_ext m) r' \<and> r = fst \<circ> r'
[PROOF STEP]
unfolding degen.is_run_def is_run_def ipath_def
[PROOF STATE]
proof (prove)
using this:
r 0 \<in> V0 \<and> (\<forall>i. (r i, r (Suc i)) \<in> E)

goal (1 subgoal):
 1. \<exists>r'. (r' 0 \<in> g_V0 (degeneralize_ext m) \<and> (\<forall>i. (r' i, r' (Suc i)) \<in> g_E (degeneralize_ext m))) \<and> r = fst \<circ> r'
[PROOF STEP]
apply (elim conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r 0 \<in> V0; \<forall>i. (r i, r (Suc i)) \<in> E\<rbrakk> \<Longrightarrow> \<exists>r'. (r' 0 \<in> g_V0 (degeneralize_ext m) \<and> (\<forall>i. (r' i, r' (Suc i)) \<in> g_E (degeneralize_ext m))) \<and> r = fst \<circ> r'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>r 0 \<in> V0; \<forall>i. (r i, r (Suc i)) \<in> E\<rbrakk> \<Longrightarrow> \<exists>r'. (r' 0 \<in> g_V0 (degeneralize_ext m) \<and> (\<forall>i. (r' i, r' (Suc i)) \<in> g_E (degeneralize_ext m))) \<and> r = fst \<circ> r'
[PROOF STEP]
assume R0: "r 0 \<in> V0" and RS: "\<forall>i. (r i, r (Suc i)) \<in> E"
[PROOF STATE]
proof (state)
this:
r 0 \<in> V0
\<forall>i. (r i, r (Suc i)) \<in> E

goal (1 subgoal):
 1. \<lbrakk>r 0 \<in> V0; \<forall>i. (r i, r (Suc i)) \<in> E\<rbrakk> \<Longrightarrow> \<exists>r'. (r' 0 \<in> g_V0 (degeneralize_ext m) \<and> (\<forall>i. (r' i, r' (Suc i)) \<in> g_E (degeneralize_ext m))) \<and> r = fst \<circ> r'
[PROOF STEP]
define r' where "r' = rec_nat
      (r 0,0)
      (\<lambda>i (q,n). (r (Suc i), if n \<in> acc q then (n+1) mod num_acc else n))"
[PROOF STATE]
proof (state)
this:
r' = rec_nat (r 0, 0) (\<lambda>i (q, n). (r (Suc i), if n \<in> acc q then (n + 1) mod num_acc else n))

goal (1 subgoal):
 1. \<lbrakk>r 0 \<in> V0; \<forall>i. (r i, r (Suc i)) \<in> E\<rbrakk> \<Longrightarrow> \<exists>r'. (r' 0 \<in> g_V0 (degeneralize_ext m) \<and> (\<forall>i. (r' i, r' (Suc i)) \<in> g_E (degeneralize_ext m))) \<and> r = fst \<circ> r'
[PROOF STEP]
have [simp]:
      "r' 0 = (r 0,0)"
      "\<And>i. r' (Suc i) = (
        let
          (q,n)=r' i
        in
          (r (Suc i), if n \<in> acc q then (n+1) mod num_acc else n)
      )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r' 0 = (r 0, 0) &&& (\<And>i. r' (Suc i) = (let (q, n) = r' i in (r (Suc i), if n \<in> acc q then (n + 1) mod num_acc else n)))
[PROOF STEP]
unfolding r'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_nat (r 0, 0) (\<lambda>i (q, n). (r (Suc i), if n \<in> acc q then (n + 1) mod num_acc else n)) 0 = (r 0, 0) &&& (\<And>i. rec_nat (r 0, 0) (\<lambda>i (q, n). (r (Suc i), if n \<in> acc q then (n + 1) mod num_acc else n)) (Suc i) = (let (q, n) = rec_nat (r 0, 0) (\<lambda>i (q, n). (r (Suc i), if n \<in> acc q then (n + 1) mod num_acc else n)) i in (r (Suc i), if n \<in> acc q then (n + 1) mod num_acc else n)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r' 0 = (r 0, 0)
r' (Suc ?i2) = (let (q, n) = r' ?i2 in (r (Suc ?i2), if n \<in> acc q then (n + 1) mod num_acc else n))

goal (1 subgoal):
 1. \<lbrakk>r 0 \<in> V0; \<forall>i. (r i, r (Suc i)) \<in> E\<rbrakk> \<Longrightarrow> \<exists>r'. (r' 0 \<in> g_V0 (degeneralize_ext m) \<and> (\<forall>i. (r' i, r' (Suc i)) \<in> g_E (degeneralize_ext m))) \<and> r = fst \<circ> r'
[PROOF STEP]
have R0': "r' 0 \<in> degen.V0 T m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r' 0 \<in> g_V0 (degeneralize_ext m)
[PROOF STEP]
using R0
[PROOF STATE]
proof (prove)
using this:
r 0 \<in> V0

goal (1 subgoal):
 1. r' 0 \<in> g_V0 (degeneralize_ext m)
[PROOF STEP]
unfolding degeneralize_ext_def
[PROOF STATE]
proof (prove)
using this:
r 0 \<in> V0

goal (1 subgoal):
 1. r' 0 \<in> g_V0 (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>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r' 0 \<in> g_V0 (degeneralize_ext m)

goal (1 subgoal):
 1. \<lbrakk>r 0 \<in> V0; \<forall>i. (r i, r (Suc i)) \<in> E\<rbrakk> \<Longrightarrow> \<exists>r'. (r' 0 \<in> g_V0 (degeneralize_ext m) \<and> (\<forall>i. (r' i, r' (Suc i)) \<in> g_E (degeneralize_ext m))) \<and> r = fst \<circ> r'
[PROOF STEP]
have MAP: "r = fst o r'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r = fst \<circ> r'
[PROOF STEP]
proof (rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. r x = (fst \<circ> r') x
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. r x = (fst \<circ> r') x
[PROOF STEP]
show "r i = (fst o r') i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r i = (fst \<circ> r') i
[PROOF STEP]
by (cases i) (auto simp: split: prod.split)
[PROOF STATE]
proof (state)
this:
r i = (fst \<circ> r') i

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

goal (1 subgoal):
 1. \<lbrakk>r 0 \<in> V0; \<forall>i. (r i, r (Suc i)) \<in> E\<rbrakk> \<Longrightarrow> \<exists>r'. (r' 0 \<in> g_V0 (degeneralize_ext m) \<and> (\<forall>i. (r' i, r' (Suc i)) \<in> g_E (degeneralize_ext m))) \<and> r = fst \<circ> r'
[PROOF STEP]
have [simp]: "0<num_acc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < num_acc
[PROOF STEP]
by (cases num_acc) auto
[PROOF STATE]
proof (state)
this:
0 < num_acc

goal (1 subgoal):
 1. \<lbrakk>r 0 \<in> V0; \<forall>i. (r i, r (Suc i)) \<in> E\<rbrakk> \<Longrightarrow> \<exists>r'. (r' 0 \<in> g_V0 (degeneralize_ext m) \<and> (\<forall>i. (r' i, r' (Suc i)) \<in> g_E (degeneralize_ext m))) \<and> r = fst \<circ> r'
[PROOF STEP]
have SND_LESS: "\<And>i. snd (r' i) < num_acc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. snd (r' i) < num_acc
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. snd (r' i) < num_acc
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. snd (r' i) < num_acc
[PROOF STEP]
show "snd (r' i) < num_acc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (r' i) < num_acc
[PROOF STEP]
by (induction i) (auto split: prod.split)
[PROOF STATE]
proof (state)
this:
snd (r' i) < num_acc

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
snd (r' ?i2) < num_acc

goal (1 subgoal):
 1. \<lbrakk>r 0 \<in> V0; \<forall>i. (r i, r (Suc i)) \<in> E\<rbrakk> \<Longrightarrow> \<exists>r'. (r' 0 \<in> g_V0 (degeneralize_ext m) \<and> (\<forall>i. (r' i, r' (Suc i)) \<in> g_E (degeneralize_ext m))) \<and> r = fst \<circ> r'
[PROOF STEP]
have RS': "\<forall>i. (r' i, r' (Suc i)) \<in> degen.E T m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. (r' i, r' (Suc i)) \<in> g_E (degeneralize_ext m)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. (r' i, r' (Suc i)) \<in> g_E (degeneralize_ext m)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. (r' i, r' (Suc i)) \<in> g_E (degeneralize_ext m)
[PROOF STEP]
obtain n where [simp]: "r' i = (r i,n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. r' i = (r i, n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (cases i)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>n. r' i = (r i, n) \<Longrightarrow> thesis; i = 0\<rbrakk> \<Longrightarrow> thesis
 2. \<And>nat. \<lbrakk>\<And>n. r' i = (r i, n) \<Longrightarrow> thesis; i = Suc nat\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (force)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>\<And>n. r' i = (r i, n) \<Longrightarrow> thesis; i = Suc nat\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (force split: prod.split)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
r' i = (r i, n)

goal (1 subgoal):
 1. \<And>i. (r' i, r' (Suc i)) \<in> g_E (degeneralize_ext m)
[PROOF STEP]
from SND_LESS[of i]
[PROOF STATE]
proof (chain)
picking this:
snd (r' i) < num_acc
[PROOF STEP]
have [simp]: "n<num_acc"
[PROOF STATE]
proof (prove)
using this:
snd (r' i) < num_acc

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

goal (1 subgoal):
 1. \<And>i. (r' i, r' (Suc i)) \<in> g_E (degeneralize_ext m)
[PROOF STEP]
show "(r' i, r' (Suc i)) \<in> degen.E T m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r' i, r' (Suc i)) \<in> g_E (degeneralize_ext m)
[PROOF STEP]
using RS
[PROOF STATE]
proof (prove)
using this:
\<forall>i. (r i, r (Suc i)) \<in> E

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i. (r' i, r' (Suc i)) \<in> g_E (degeneralize_ext m)

goal (1 subgoal):
 1. \<lbrakk>r 0 \<in> V0; \<forall>i. (r i, r (Suc i)) \<in> E\<rbrakk> \<Longrightarrow> \<exists>r'. (r' 0 \<in> g_V0 (degeneralize_ext m) \<and> (\<forall>i. (r' i, r' (Suc i)) \<in> g_E (degeneralize_ext m))) \<and> r = fst \<circ> r'
[PROOF STEP]
from R0' RS' MAP
[PROOF STATE]
proof (chain)
picking this:
r' 0 \<in> g_V0 (degeneralize_ext m)
\<forall>i. (r' i, r' (Suc i)) \<in> g_E (degeneralize_ext m)
r = fst \<circ> r'
[PROOF STEP]
show
      "\<exists>r'. (r' 0 \<in> degen.V0 T m
      \<and> (\<forall>i. (r' i, r' (Suc i)) \<in> degen.E T m))
      \<and> r = fst \<circ> r'"
[PROOF STATE]
proof (prove)
using this:
r' 0 \<in> g_V0 (degeneralize_ext m)
\<forall>i. (r' i, r' (Suc i)) \<in> g_E (degeneralize_ext m)
r = fst \<circ> r'

goal (1 subgoal):
 1. \<exists>r'. (r' 0 \<in> g_V0 (degeneralize_ext m) \<and> (\<forall>i. (r' i, r' (Suc i)) \<in> g_E (degeneralize_ext m))) \<and> r = fst \<circ> r'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>r'. (r' 0 \<in> g_V0 (degeneralize_ext m) \<and> (\<forall>i. (r' i, r' (Suc i)) \<in> g_E (degeneralize_ext m))) \<and> r = fst \<circ> r'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma degen_run_bound:
    assumes [simp]: "num_acc \<noteq> 0"
    assumes R: "degen.is_run T m r"
    shows "snd (r i) < num_acc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (r i) < num_acc
[PROOF STEP]
apply (induction i)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. snd (r 0) < num_acc
 2. \<And>i. snd (r i) < num_acc \<Longrightarrow> snd (r (Suc i)) < num_acc
[PROOF STEP]
using R
[PROOF STATE]
proof (prove)
using this:
graph_defs.is_run (degeneralize_ext m) r

goal (2 subgoals):
 1. snd (r 0) < num_acc
 2. \<And>i. snd (r i) < num_acc \<Longrightarrow> snd (r (Suc i)) < num_acc
[PROOF STEP]
unfolding degen.is_run_def is_run_def
[PROOF STATE]
proof (prove)
using this:
r 0 \<in> g_V0 (degeneralize_ext m) \<and> ipath (g_E (degeneralize_ext m)) r

goal (2 subgoals):
 1. snd (r 0) < num_acc
 2. \<And>i. snd (r i) < num_acc \<Longrightarrow> snd (r (Suc i)) < num_acc
[PROOF STEP]
unfolding degeneralize_ext_def ipath_def
[PROOF STATE]
proof (prove)
using this:
r 0 \<in> g_V0 (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>) \<and> (\<forall>i. (r i, r (Suc i)) \<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 (2 subgoals):
 1. snd (r 0) < num_acc
 2. \<And>i. snd (r i) < num_acc \<Longrightarrow> snd (r (Suc i)) < num_acc
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. r 0 \<in> g_V0 (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>) \<and> (\<forall>i. (r i, r (Suc i)) \<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>)) \<Longrightarrow> snd (r 0) < num_acc
 2. \<And>i. \<lbrakk>snd (r i) < num_acc; r 0 \<in> g_V0 (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>) \<and> (\<forall>i. (r i, r (Suc i)) \<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>))\<rbrakk> \<Longrightarrow> snd (r (Suc i)) < num_acc
[PROOF STEP]
apply auto []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>snd (r i) < num_acc; r 0 \<in> g_V0 (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>) \<and> (\<forall>i. (r i, r (Suc i)) \<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>))\<rbrakk> \<Longrightarrow> snd (r (Suc i)) < num_acc
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i x. \<lbrakk>snd (r i) < num_acc; \<forall>i. \<exists>ia q. r i = (q, ia) \<and> (\<exists>q'. r (Suc i) = (q', if ia \<in> acc q then (ia + 1) mod num_acc else ia) \<and> ia < num_acc \<and> (q, q') \<in> E); x \<in> V0; r 0 = (x, 0)\<rbrakk> \<Longrightarrow> snd (r (Suc i)) < num_acc
[PROOF STEP]
by (metis snd_conv)


[STATEMENT]
lemma degen_acc_run_complete_aux1:
    assumes NN0[simp]: "num_acc \<noteq> 0"
    assumes R: "degen.is_run T m r"
    assumes EXJ: "\<exists>j\<ge>i. n \<in> acc (fst (r j))"
    assumes RI: "r i = (q,n)"
    shows "\<exists>j\<ge>i. \<exists>q'. r j = (q',n) \<and> n \<in> acc q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j\<ge>i. \<exists>q'. r j = (q', n) \<and> n \<in> acc q'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>j\<ge>i. \<exists>q'. r j = (q', n) \<and> n \<in> acc q'
[PROOF STEP]
define j where "j = (LEAST j. j\<ge>i \<and> n \<in> acc (fst (r j)))"
[PROOF STATE]
proof (state)
this:
j = (LEAST j. i \<le> j \<and> n \<in> acc (fst (r j)))

goal (1 subgoal):
 1. \<exists>j\<ge>i. \<exists>q'. r j = (q', n) \<and> n \<in> acc q'
[PROOF STEP]
from RI
[PROOF STATE]
proof (chain)
picking this:
r i = (q, n)
[PROOF STEP]
have "n<num_acc"
[PROOF STATE]
proof (prove)
using this:
r i = (q, n)

goal (1 subgoal):
 1. n < num_acc
[PROOF STEP]
using degen_run_bound[OF NN0 R, of i]
[PROOF STATE]
proof (prove)
using this:
r i = (q, n)
snd (r i) < num_acc

goal (1 subgoal):
 1. n < num_acc
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n < num_acc

goal (1 subgoal):
 1. \<exists>j\<ge>i. \<exists>q'. r j = (q', n) \<and> n \<in> acc q'
[PROOF STEP]
from EXJ
[PROOF STATE]
proof (chain)
picking this:
\<exists>j\<ge>i. n \<in> acc (fst (r j))
[PROOF STEP]
have
      "j\<ge>i"
      "n \<in> acc (fst (r j))"
      "\<forall>k\<ge>i. n \<in> acc (fst (r k)) \<longrightarrow> j\<le>k"
[PROOF STATE]
proof (prove)
using this:
\<exists>j\<ge>i. n \<in> acc (fst (r j))

goal (1 subgoal):
 1. i \<le> j &&& n \<in> acc (fst (r j)) &&& \<forall>k\<ge>i. n \<in> acc (fst (r k)) \<longrightarrow> j \<le> k
[PROOF STEP]
using LeastI_ex[OF EXJ]
[PROOF STATE]
proof (prove)
using this:
\<exists>j\<ge>i. n \<in> acc (fst (r j))
i \<le> (LEAST j. i \<le> j \<and> n \<in> acc (fst (r j))) \<and> n \<in> acc (fst (r (LEAST j. i \<le> j \<and> n \<in> acc (fst (r j)))))

goal (1 subgoal):
 1. i \<le> j &&& n \<in> acc (fst (r j)) &&& \<forall>k\<ge>i. n \<in> acc (fst (r k)) \<longrightarrow> j \<le> k
[PROOF STEP]
unfolding j_def
[PROOF STATE]
proof (prove)
using this:
\<exists>j\<ge>i. n \<in> acc (fst (r j))
i \<le> (LEAST j. i \<le> j \<and> n \<in> acc (fst (r j))) \<and> n \<in> acc (fst (r (LEAST j. i \<le> j \<and> n \<in> acc (fst (r j)))))

goal (1 subgoal):
 1. i \<le> (LEAST j. i \<le> j \<and> n \<in> acc (fst (r j))) &&& n \<in> acc (fst (r (LEAST j. i \<le> j \<and> n \<in> acc (fst (r j))))) &&& \<forall>k\<ge>i. n \<in> acc (fst (r k)) \<longrightarrow> (LEAST j. i \<le> j \<and> n \<in> acc (fst (r j))) \<le> k
[PROOF STEP]
apply (auto) [2]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<ge>i. n \<in> acc (fst (r k)) \<longrightarrow> (LEAST j. i \<le> j \<and> n \<in> acc (fst (r j))) \<le> k
[PROOF STEP]
apply (metis (lifting) Least_le)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
i \<le> j
n \<in> acc (fst (r j))
\<forall>k\<ge>i. n \<in> acc (fst (r k)) \<longrightarrow> j \<le> k

goal (1 subgoal):
 1. \<exists>j\<ge>i. \<exists>q'. r j = (q', n) \<and> n \<in> acc q'
[PROOF STEP]
hence "\<forall>k\<ge>i. k<j \<longrightarrow> n \<notin> acc (fst (r k))"
[PROOF STATE]
proof (prove)
using this:
i \<le> j
n \<in> acc (fst (r j))
\<forall>k\<ge>i. n \<in> acc (fst (r k)) \<longrightarrow> j \<le> k

goal (1 subgoal):
 1. \<forall>k\<ge>i. k < j \<longrightarrow> n \<notin> acc (fst (r k))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>k\<ge>i. k < j \<longrightarrow> n \<notin> acc (fst (r k))

goal (1 subgoal):
 1. \<exists>j\<ge>i. \<exists>q'. r j = (q', n) \<and> n \<in> acc q'
[PROOF STEP]
have "\<forall>k. k\<ge>i \<and> k\<le>j \<longrightarrow> (snd (r k) = n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k. i \<le> k \<and> k \<le> j \<longrightarrow> snd (r k) = n
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>i \<le> k; k \<le> j\<rbrakk> \<Longrightarrow> snd (r k) = n
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>i \<le> k; k \<le> j\<rbrakk> \<Longrightarrow> snd (r k) = n
[PROOF STEP]
assume "i\<le>k" "k\<le>j"
[PROOF STATE]
proof (state)
this:
i \<le> k
k \<le> j

goal (1 subgoal):
 1. \<And>k. \<lbrakk>i \<le> k; k \<le> j\<rbrakk> \<Longrightarrow> snd (r k) = n
[PROOF STEP]
thus "snd (r k) = n"
[PROOF STATE]
proof (prove)
using this:
i \<le> k
k \<le> j

goal (1 subgoal):
 1. snd (r k) = n
[PROOF STEP]
proof (induction k rule: less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>y < x; i \<le> y; y \<le> j\<rbrakk> \<Longrightarrow> snd (r y) = n; i \<le> x; x \<le> j\<rbrakk> \<Longrightarrow> snd (r x) = n
[PROOF STEP]
case (less k)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y2 < k; i \<le> ?y2; ?y2 \<le> j\<rbrakk> \<Longrightarrow> snd (r ?y2) = n
i \<le> k
k \<le> j

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>y < x; i \<le> y; y \<le> j\<rbrakk> \<Longrightarrow> snd (r y) = n; i \<le> x; x \<le> j\<rbrakk> \<Longrightarrow> snd (r x) = n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (r k) = n
[PROOF STEP]
proof (cases "k=i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k = i \<Longrightarrow> snd (r k) = n
 2. k \<noteq> i \<Longrightarrow> snd (r k) = n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
k = i

goal (2 subgoals):
 1. k = i \<Longrightarrow> snd (r k) = n
 2. k \<noteq> i \<Longrightarrow> snd (r k) = n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
k = i

goal (1 subgoal):
 1. snd (r k) = n
[PROOF STEP]
using RI
[PROOF STATE]
proof (prove)
using this:
k = i
r i = (q, n)

goal (1 subgoal):
 1. snd (r k) = n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
snd (r k) = n

goal (1 subgoal):
 1. k \<noteq> i \<Longrightarrow> snd (r k) = n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k \<noteq> i \<Longrightarrow> snd (r k) = n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
k \<noteq> i

goal (1 subgoal):
 1. k \<noteq> i \<Longrightarrow> snd (r k) = n
[PROOF STEP]
with less.prems
[PROOF STATE]
proof (chain)
picking this:
i \<le> k
k \<le> j
k \<noteq> i
[PROOF STEP]
have "k - 1 < k" "i \<le> k - 1" "k - 1\<le>j"
[PROOF STATE]
proof (prove)
using this:
i \<le> k
k \<le> j
k \<noteq> i

goal (1 subgoal):
 1. k - 1 < k &&& i \<le> k - 1 &&& k - 1 \<le> j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k - 1 < k
i \<le> k - 1
k - 1 \<le> j

goal (1 subgoal):
 1. k \<noteq> i \<Longrightarrow> snd (r k) = n
[PROOF STEP]
from less.IH[OF this]
[PROOF STATE]
proof (chain)
picking this:
snd (r (k - 1)) = n
[PROOF STEP]
have "snd (r (k - 1)) = n"
[PROOF STATE]
proof (prove)
using this:
snd (r (k - 1)) = n

goal (1 subgoal):
 1. snd (r (k - 1)) = n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
snd (r (k - 1)) = n

goal (1 subgoal):
 1. k \<noteq> i \<Longrightarrow> snd (r k) = n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
snd (r (k - 1)) = n

goal (1 subgoal):
 1. k \<noteq> i \<Longrightarrow> snd (r k) = n
[PROOF STEP]
from R
[PROOF STATE]
proof (chain)
picking this:
graph_defs.is_run (degeneralize_ext m) r
[PROOF STEP]
have
            "(r (k - 1), r k) \<in> degen.E T m"
[PROOF STATE]
proof (prove)
using this:
graph_defs.is_run (degeneralize_ext m) r

goal (1 subgoal):
 1. (r (k - 1), r k) \<in> g_E (degeneralize_ext m)
[PROOF STEP]
unfolding degen.is_run_def 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 (k - 1), r k) \<in> g_E (degeneralize_ext m)
[PROOF STEP]
by clarsimp (metis One_nat_def Suc_diff_1 \<open>k - 1 < k\<close>
              less_nat_zero_code neq0_conv)
[PROOF STATE]
proof (state)
this:
(r (k - 1), r k) \<in> g_E (degeneralize_ext m)

goal (1 subgoal):
 1. k \<noteq> i \<Longrightarrow> snd (r k) = n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(r (k - 1), r k) \<in> g_E (degeneralize_ext m)

goal (1 subgoal):
 1. k \<noteq> i \<Longrightarrow> snd (r k) = n
[PROOF STEP]
have "n \<notin> acc (fst (r (k - 1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<notin> acc (fst (r (k - 1)))
[PROOF STEP]
using \<open>\<forall>k\<ge>i. k < j \<longrightarrow> n \<notin> acc (fst (r k))\<close> \<open>i \<le> k - 1\<close> \<open>k - 1 < k\<close>
              dual_order.strict_trans1 less.prems(2)
[PROOF STATE]
proof (prove)
using this:
\<forall>k\<ge>i. k < j \<longrightarrow> n \<notin> acc (fst (r k))
i \<le> k - 1
k - 1 < k
\<lbrakk>?b \<le> ?a; ?c < ?b\<rbrakk> \<Longrightarrow> ?c < ?a
k \<le> j

goal (1 subgoal):
 1. n \<notin> acc (fst (r (k - 1)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n \<notin> acc (fst (r (k - 1)))

goal (1 subgoal):
 1. k \<noteq> i \<Longrightarrow> snd (r k) = n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
snd (r (k - 1)) = n
(r (k - 1), r k) \<in> g_E (degeneralize_ext m)
n \<notin> acc (fst (r (k - 1)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
snd (r (k - 1)) = n
(r (k - 1), r k) \<in> g_E (degeneralize_ext m)
n \<notin> acc (fst (r (k - 1)))

goal (1 subgoal):
 1. snd (r k) = n
[PROOF STEP]
by (auto simp: degeneralize_ext_def)
[PROOF STATE]
proof (state)
this:
snd (r k) = n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
snd (r k) = n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
snd (r k) = n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>k. i \<le> k \<and> k \<le> j \<longrightarrow> snd (r k) = n

goal (1 subgoal):
 1. \<exists>j\<ge>i. \<exists>q'. r j = (q', n) \<and> n \<in> acc q'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>k. i \<le> k \<and> k \<le> j \<longrightarrow> snd (r k) = n

goal (1 subgoal):
 1. \<exists>j\<ge>i. \<exists>q'. r j = (q', n) \<and> n \<in> acc q'
[PROOF STEP]
by (metis \<open>i \<le> j\<close> \<open>n \<in> local.acc (fst (r j))\<close>
        order_refl surjective_pairing)
[PROOF STATE]
proof (state)
this:
\<exists>j\<ge>i. \<exists>q'. r j = (q', n) \<and> n \<in> acc q'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma degen_acc_run_complete_aux1':
    assumes NN0[simp]: "num_acc \<noteq> 0"
    assumes R: "degen.is_run T m r"
    assumes ACC: "\<forall>n<num_acc. \<exists>\<^sub>\<infinity>i. n \<in> acc (fst (r i))"
    assumes RI: "r i = (q,n)"
    shows "\<exists>j\<ge>i. \<exists>q'. r j = (q',n) \<and> n \<in> acc q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j\<ge>i. \<exists>q'. r j = (q', n) \<and> n \<in> acc q'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>j\<ge>i. \<exists>q'. r j = (q', n) \<and> n \<in> acc q'
[PROOF STEP]
from RI
[PROOF STATE]
proof (chain)
picking this:
r i = (q, n)
[PROOF STEP]
have "n<num_acc"
[PROOF STATE]
proof (prove)
using this:
r i = (q, n)

goal (1 subgoal):
 1. n < num_acc
[PROOF STEP]
using degen_run_bound[OF NN0 R, of i]
[PROOF STATE]
proof (prove)
using this:
r i = (q, n)
snd (r i) < num_acc

goal (1 subgoal):
 1. n < num_acc
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n < num_acc

goal (1 subgoal):
 1. \<exists>j\<ge>i. \<exists>q'. r j = (q', n) \<and> n \<in> acc q'
[PROOF STEP]
with ACC
[PROOF STATE]
proof (chain)
picking this:
\<forall>n<num_acc. \<exists>\<^sub>\<infinity>i. n \<in> acc (fst (r i))
n < num_acc
[PROOF STEP]
have EXJ: "\<exists>j\<ge>i. n \<in> acc (fst (r j))"
[PROOF STATE]
proof (prove)
using this:
\<forall>n<num_acc. \<exists>\<^sub>\<infinity>i. n \<in> acc (fst (r i))
n < num_acc

goal (1 subgoal):
 1. \<exists>j\<ge>i. n \<in> acc (fst (r j))
[PROOF STEP]
unfolding INFM_nat_le
[PROOF STATE]
proof (prove)
using this:
\<forall>n<num_acc. \<forall>m. \<exists>na\<ge>m. n \<in> acc (fst (r na))
n < num_acc

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

goal (1 subgoal):
 1. \<exists>j\<ge>i. \<exists>q'. r j = (q', n) \<and> n \<in> acc q'
[PROOF STEP]
from degen_acc_run_complete_aux1[OF NN0 R EXJ RI]
[PROOF STATE]
proof (chain)
picking this:
\<exists>j\<ge>i. \<exists>q'. r j = (q', n) \<and> n \<in> acc q'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>j\<ge>i. \<exists>q'. r j = (q', n) \<and> n \<in> acc q'

goal (1 subgoal):
 1. \<exists>j\<ge>i. \<exists>q'. r j = (q', n) \<and> n \<in> acc q'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<exists>j\<ge>i. \<exists>q'. r j = (q', n) \<and> n \<in> acc q'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma degen_acc_run_complete_aux2:
    assumes NN0[simp]: "num_acc \<noteq> 0"
    assumes R: "degen.is_run T m r"
    assumes ACC: "\<forall>n<num_acc. \<exists>\<^sub>\<infinity>i. n \<in> acc (fst (r i))"
    assumes RI: "r i = (q,n)" and OFS: "ofs<num_acc"
    shows "\<exists>j\<ge>i. \<exists>q'.
      r j = (q',(n + ofs) mod num_acc) \<and> (n + ofs) mod num_acc \<in> acc q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j\<ge>i. \<exists>q'. r j = (q', (n + ofs) mod num_acc) \<and> (n + ofs) mod num_acc \<in> acc q'
[PROOF STEP]
using RI OFS
[PROOF STATE]
proof (prove)
using this:
r i = (q, n)
ofs < num_acc

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

goal (2 subgoals):
 1. \<And>q n i. \<lbrakk>r i = (q, n); 0 < num_acc\<rbrakk> \<Longrightarrow> \<exists>j\<ge>i. \<exists>q'. r j = (q', (n + 0) mod num_acc) \<and> (n + 0) mod num_acc \<in> acc q'
 2. \<And>ofs q n i. \<lbrakk>\<And>q n i. \<lbrakk>r i = (q, n); ofs < num_acc\<rbrakk> \<Longrightarrow> \<exists>j\<ge>i. \<exists>q'. r j = (q', (n + ofs) mod num_acc) \<and> (n + ofs) mod num_acc \<in> acc q'; r i = (q, n); Suc ofs < num_acc\<rbrakk> \<Longrightarrow> \<exists>j\<ge>i. \<exists>q'. r j = (q', (n + Suc ofs) mod num_acc) \<and> (n + Suc ofs) mod num_acc \<in> acc q'
[PROOF STEP]
from degen_run_bound[OF NN0 R, of i] \<open>r i = (q, n)\<close>
[PROOF STATE]
proof (chain)
picking this:
snd (r i) < num_acc
r i = (q, n)
[PROOF STEP]
have NLE: "n<num_acc"
[PROOF STATE]
proof (prove)
using this:
snd (r i) < num_acc
r i = (q, n)

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

goal (2 subgoals):
 1. \<And>q n i. \<lbrakk>r i = (q, n); 0 < num_acc\<rbrakk> \<Longrightarrow> \<exists>j\<ge>i. \<exists>q'. r j = (q', (n + 0) mod num_acc) \<and> (n + 0) mod num_acc \<in> acc q'
 2. \<And>ofs q n i. \<lbrakk>\<And>q n i. \<lbrakk>r i = (q, n); ofs < num_acc\<rbrakk> \<Longrightarrow> \<exists>j\<ge>i. \<exists>q'. r j = (q', (n + ofs) mod num_acc) \<and> (n + ofs) mod num_acc \<in> acc q'; r i = (q, n); Suc ofs < num_acc\<rbrakk> \<Longrightarrow> \<exists>j\<ge>i. \<exists>q'. r j = (q', (n + Suc ofs) mod num_acc) \<and> (n + Suc ofs) mod num_acc \<in> acc q'
[PROOF STEP]
with degen_acc_run_complete_aux1'[OF NN0 R ACC \<open>r i = (q, n)\<close>]
[PROOF STATE]
proof (chain)
picking this:
\<exists>j\<ge>i. \<exists>q'. r j = (q', n) \<and> n \<in> acc q'
n < num_acc
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>j\<ge>i. \<exists>q'. r j = (q', n) \<and> n \<in> acc q'
n < num_acc

goal (1 subgoal):
 1. \<exists>j\<ge>i. \<exists>q'. r j = (q', (n + 0) mod num_acc) \<and> (n + 0) mod num_acc \<in> acc q'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>j\<ge>i. \<exists>q'. r j = (q', (n + 0) mod num_acc) \<and> (n + 0) mod num_acc \<in> acc q'

goal (1 subgoal):
 1. \<And>ofs q n i. \<lbrakk>\<And>q n i. \<lbrakk>r i = (q, n); ofs < num_acc\<rbrakk> \<Longrightarrow> \<exists>j\<ge>i. \<exists>q'. r j = (q', (n + ofs) mod num_acc) \<and> (n + ofs) mod num_acc \<in> acc q'; r i = (q, n); Suc ofs < num_acc\<rbrakk> \<Longrightarrow> \<exists>j\<ge>i. \<exists>q'. r j = (q', (n + Suc ofs) mod num_acc) \<and> (n + Suc ofs) mod num_acc \<in> acc q'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ofs q n i. \<lbrakk>\<And>q n i. \<lbrakk>r i = (q, n); ofs < num_acc\<rbrakk> \<Longrightarrow> \<exists>j\<ge>i. \<exists>q'. r j = (q', (n + ofs) mod num_acc) \<and> (n + ofs) mod num_acc \<in> acc q'; r i = (q, n); Suc ofs < num_acc\<rbrakk> \<Longrightarrow> \<exists>j\<ge>i. \<exists>q'. r j = (q', (n + Suc ofs) mod num_acc) \<and> (n + Suc ofs) mod num_acc \<in> acc q'
[PROOF STEP]
case (Suc ofs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>r ?i2 = (?q2, ?n2); ofs < num_acc\<rbrakk> \<Longrightarrow> \<exists>j\<ge>?i2. \<exists>q'. r j = (q', (?n2 + ofs) mod num_acc) \<and> (?n2 + ofs) mod num_acc \<in> acc q'
r i = (q, n)
Suc ofs < num_acc

goal (1 subgoal):
 1. \<And>ofs q n i. \<lbrakk>\<And>q n i. \<lbrakk>r i = (q, n); ofs < num_acc\<rbrakk> \<Longrightarrow> \<exists>j\<ge>i. \<exists>q'. r j = (q', (n + ofs) mod num_acc) \<and> (n + ofs) mod num_acc \<in> acc q'; r i = (q, n); Suc ofs < num_acc\<rbrakk> \<Longrightarrow> \<exists>j\<ge>i. \<exists>q'. r j = (q', (n + Suc ofs) mod num_acc) \<and> (n + Suc ofs) mod num_acc \<in> acc q'
[PROOF STEP]
from Suc.IH[OF Suc.prems(1)] Suc.prems(2)
[PROOF STATE]
proof (chain)
picking this:
ofs < num_acc \<Longrightarrow> \<exists>j\<ge>i. \<exists>q'. r j = (q', (n + ofs) mod num_acc) \<and> (n + ofs) mod num_acc \<in> acc q'
Suc ofs < num_acc
[PROOF STEP]
obtain j q' where "j\<ge>i" and RJ: "r j = (q',(n+ofs) mod num_acc)"
      and A: "(n+ofs) mod num_acc \<in> acc q'"
[PROOF STATE]
proof (prove)
using this:
ofs < num_acc \<Longrightarrow> \<exists>j\<ge>i. \<exists>q'. r j = (q', (n + ofs) mod num_acc) \<and> (n + ofs) mod num_acc \<in> acc q'
Suc ofs < num_acc

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

goal (1 subgoal):
 1. \<And>ofs q n i. \<lbrakk>\<And>q n i. \<lbrakk>r i = (q, n); ofs < num_acc\<rbrakk> \<Longrightarrow> \<exists>j\<ge>i. \<exists>q'. r j = (q', (n + ofs) mod num_acc) \<and> (n + ofs) mod num_acc \<in> acc q'; r i = (q, n); Suc ofs < num_acc\<rbrakk> \<Longrightarrow> \<exists>j\<ge>i. \<exists>q'. r j = (q', (n + Suc ofs) mod num_acc) \<and> (n + Suc ofs) mod num_acc \<in> acc q'
[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]
by (auto simp: degen.is_run_def is_run_def ipath_def)
[PROOF STATE]
proof (state)
this:
(r j, r (Suc j)) \<in> g_E (degeneralize_ext m)

goal (1 subgoal):
 1. \<And>ofs q n i. \<lbrakk>\<And>q n i. \<lbrakk>r i = (q, n); ofs < num_acc\<rbrakk> \<Longrightarrow> \<exists>j\<ge>i. \<exists>q'. r j = (q', (n + ofs) mod num_acc) \<and> (n + ofs) mod num_acc \<in> acc q'; r i = (q, n); Suc ofs < num_acc\<rbrakk> \<Longrightarrow> \<exists>j\<ge>i. \<exists>q'. r j = (q', (n + Suc ofs) mod num_acc) \<and> (n + Suc ofs) mod num_acc \<in> acc q'
[PROOF STEP]
with RJ A
[PROOF STATE]
proof (chain)
picking this:
r j = (q', (n + ofs) mod num_acc)
(n + ofs) mod num_acc \<in> acc q'
(r j, r (Suc j)) \<in> g_E (degeneralize_ext m)
[PROOF STEP]
obtain q2 where RSJ: "r (Suc j) = (q2,(n+Suc ofs) mod num_acc)"
[PROOF STATE]
proof (prove)
using this:
r j = (q', (n + ofs) mod num_acc)
(n + ofs) mod num_acc \<in> acc q'
(r j, r (Suc j)) \<in> g_E (degeneralize_ext m)

goal (1 subgoal):
 1. (\<And>q2. r (Suc j) = (q2, (n + Suc ofs) mod num_acc) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: degeneralize_ext_def mod_simps)
[PROOF STATE]
proof (state)
this:
r (Suc j) = (q2, (n + Suc ofs) mod num_acc)

goal (1 subgoal):
 1. \<And>ofs q n i. \<lbrakk>\<And>q n i. \<lbrakk>r i = (q, n); ofs < num_acc\<rbrakk> \<Longrightarrow> \<exists>j\<ge>i. \<exists>q'. r j = (q', (n + ofs) mod num_acc) \<and> (n + ofs) mod num_acc \<in> acc q'; r i = (q, n); Suc ofs < num_acc\<rbrakk> \<Longrightarrow> \<exists>j\<ge>i. \<exists>q'. r j = (q', (n + Suc ofs) mod num_acc) \<and> (n + Suc ofs) mod num_acc \<in> acc q'
[PROOF STEP]
have aux: "\<And>j'. i\<le>j \<Longrightarrow> Suc j \<le> j' \<Longrightarrow> i\<le>j'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j'. \<lbrakk>i \<le> j; Suc j \<le> j'\<rbrakk> \<Longrightarrow> i \<le> j'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<le> j; Suc j \<le> ?j'2\<rbrakk> \<Longrightarrow> i \<le> ?j'2

goal (1 subgoal):
 1. \<And>ofs q n i. \<lbrakk>\<And>q n i. \<lbrakk>r i = (q, n); ofs < num_acc\<rbrakk> \<Longrightarrow> \<exists>j\<ge>i. \<exists>q'. r j = (q', (n + ofs) mod num_acc) \<and> (n + ofs) mod num_acc \<in> acc q'; r i = (q, n); Suc ofs < num_acc\<rbrakk> \<Longrightarrow> \<exists>j\<ge>i. \<exists>q'. r j = (q', (n + Suc ofs) mod num_acc) \<and> (n + Suc ofs) mod num_acc \<in> acc q'
[PROOF STEP]
from degen_acc_run_complete_aux1'[OF NN0 R ACC RSJ] \<open>j\<ge>i\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>ja\<ge>Suc j. \<exists>q'. r ja = (q', (n + Suc ofs) mod num_acc) \<and> (n + Suc ofs) mod num_acc \<in> acc q'
i \<le> j
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>ja\<ge>Suc j. \<exists>q'. r ja = (q', (n + Suc ofs) mod num_acc) \<and> (n + Suc ofs) mod num_acc \<in> acc q'
i \<le> j

goal (1 subgoal):
 1. \<exists>j\<ge>i. \<exists>q'. r j = (q', (n + Suc ofs) mod num_acc) \<and> (n + Suc ofs) mod num_acc \<in> acc q'
[PROOF STEP]
by (auto dest: aux)
[PROOF STATE]
proof (state)
this:
\<exists>j\<ge>i. \<exists>q'. r j = (q', (n + Suc ofs) mod num_acc) \<and> (n + Suc ofs) mod num_acc \<in> acc q'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma degen_acc_run_complete:
    assumes AR: "is_acc_run r"
    obtains r'
    where "degen.is_acc_run T m r'" and "r = fst o r'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r'. \<lbrakk>b_graph.is_acc_run (degeneralize_ext m) r'; r = fst \<circ> r'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (cases "num_acc = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>r'. \<lbrakk>b_graph.is_acc_run (degeneralize_ext m) r'; r = fst \<circ> r'\<rbrakk> \<Longrightarrow> thesis; num_acc = 0\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>r'. \<lbrakk>b_graph.is_acc_run (degeneralize_ext m) r'; r = fst \<circ> r'\<rbrakk> \<Longrightarrow> thesis; num_acc \<noteq> 0\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
num_acc = 0

goal (2 subgoals):
 1. \<lbrakk>\<And>r'. \<lbrakk>b_graph.is_acc_run (degeneralize_ext m) r'; r = fst \<circ> r'\<rbrakk> \<Longrightarrow> thesis; num_acc = 0\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>r'. \<lbrakk>b_graph.is_acc_run (degeneralize_ext m) r'; r = fst \<circ> r'\<rbrakk> \<Longrightarrow> thesis; num_acc \<noteq> 0\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
with AR degen_acc_run_complete0
[PROOF STATE]
proof (chain)
picking this:
is_acc_run r
\<lbrakk>num_acc = 0; is_acc_run ?r\<rbrakk> \<Longrightarrow> b_graph.is_acc_run (degeneralize_ext ?m) (\<lambda>i. (?r i, 0))
num_acc = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_acc_run r
\<lbrakk>num_acc = 0; is_acc_run ?r\<rbrakk> \<Longrightarrow> b_graph.is_acc_run (degeneralize_ext ?m) (\<lambda>i. (?r i, 0))
num_acc = 0

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (auto intro!: that[of "(\<lambda>i. (r i, 0))"])
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. \<lbrakk>\<And>r'. \<lbrakk>b_graph.is_acc_run (degeneralize_ext m) r'; r = fst \<circ> r'\<rbrakk> \<Longrightarrow> thesis; num_acc \<noteq> 0\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>r'. \<lbrakk>b_graph.is_acc_run (degeneralize_ext m) r'; r = fst \<circ> r'\<rbrakk> \<Longrightarrow> thesis; num_acc \<noteq> 0\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
num_acc \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>\<And>r'. \<lbrakk>b_graph.is_acc_run (degeneralize_ext m) r'; r = fst \<circ> r'\<rbrakk> \<Longrightarrow> thesis; num_acc \<noteq> 0\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume NN0[simp]: "num_acc \<noteq> 0"
[PROOF STATE]
proof (state)
this:
num_acc \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>\<And>r'. \<lbrakk>b_graph.is_acc_run (degeneralize_ext m) r'; r = fst \<circ> r'\<rbrakk> \<Longrightarrow> thesis; num_acc \<noteq> 0\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from AR
[PROOF STATE]
proof (chain)
picking this:
is_acc_run r
[PROOF STEP]
have R: "is_run r" and ACC: "\<forall>n<num_acc. \<exists>\<^sub>\<infinity>i. n \<in> acc (r i)"
[PROOF STATE]
proof (prove)
using this:
is_acc_run r

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

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

goal (1 subgoal):
 1. \<lbrakk>\<And>r'. \<lbrakk>b_graph.is_acc_run (degeneralize_ext m) r'; r = fst \<circ> r'\<rbrakk> \<Longrightarrow> thesis; num_acc \<noteq> 0\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from degen_run_complete[OF NN0 R]
[PROOF STATE]
proof (chain)
picking this:
\<exists>r'. graph_defs.is_run (degeneralize_ext ?m) r' \<and> r = fst \<circ> r'
[PROOF STEP]
obtain r' where
      R': "degen.is_run T m r'"
      and [simp]: "r = fst \<circ> r'"
[PROOF STATE]
proof (prove)
using this:
\<exists>r'. graph_defs.is_run (degeneralize_ext ?m) r' \<and> r = fst \<circ> r'

goal (1 subgoal):
 1. (\<And>r'. \<lbrakk>graph_defs.is_run (degeneralize_ext m) r'; r = fst \<circ> r'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
graph_defs.is_run (degeneralize_ext m) r'
r = fst \<circ> r'

goal (1 subgoal):
 1. \<lbrakk>\<And>r'. \<lbrakk>b_graph.is_acc_run (degeneralize_ext m) r'; r = fst \<circ> r'\<rbrakk> \<Longrightarrow> thesis; num_acc \<noteq> 0\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from ACC
[PROOF STATE]
proof (chain)
picking this:
\<forall>n<num_acc. \<exists>\<^sub>\<infinity>i. n \<in> acc (r i)
[PROOF STEP]
have ACC': "\<forall>n<num_acc. \<exists>\<^sub>\<infinity>i. n \<in> acc (fst (r' i))"
[PROOF STATE]
proof (prove)
using this:
\<forall>n<num_acc. \<exists>\<^sub>\<infinity>i. n \<in> acc (r i)

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

goal (1 subgoal):
 1. \<lbrakk>\<And>r'. \<lbrakk>b_graph.is_acc_run (degeneralize_ext m) r'; r = fst \<circ> r'\<rbrakk> \<Longrightarrow> thesis; num_acc \<noteq> 0\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "\<forall>i. \<exists>j>i. r' j \<in> degen.F T m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. \<exists>j>i. r' j \<in> bg_F (degeneralize_ext m)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<exists>j>i. r' j \<in> bg_F (degeneralize_ext m)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<exists>j>i. r' j \<in> bg_F (degeneralize_ext m)
[PROOF STEP]
obtain q n where RI: "r' (Suc i) = (q,n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q n. r' (Suc i) = (q, n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "r' (Suc i)")
[PROOF STATE]
proof (state)
this:
r' (Suc i) = (q, n)

goal (1 subgoal):
 1. \<And>i. \<exists>j>i. r' j \<in> bg_F (degeneralize_ext m)
[PROOF STEP]
have "(n + (num_acc - n mod num_acc)) mod num_acc = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n + (num_acc - n mod num_acc)) mod num_acc = 0
[PROOF STEP]
apply (rule dvd_imp_mod_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_acc dvd n + (num_acc - n mod num_acc)
[PROOF STEP]
apply (metis (mono_tags, lifting) NN0 add_diff_inverse mod_0_imp_dvd
          mod_add_left_eq mod_less_divisor mod_self nat_diff_split not_gr_zero zero_less_diff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(n + (num_acc - n mod num_acc)) mod num_acc = 0

goal (1 subgoal):
 1. \<And>i. \<exists>j>i. r' j \<in> bg_F (degeneralize_ext m)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(n + (num_acc - n mod num_acc)) mod num_acc = 0
[PROOF STEP]
obtain ofs where
        OFS_LESS: "ofs<num_acc"
        and [simp]: "(n + ofs) mod num_acc = 0"
[PROOF STATE]
proof (prove)
using this:
(n + (num_acc - n mod num_acc)) mod num_acc = 0

goal (1 subgoal):
 1. (\<And>ofs. \<lbrakk>ofs < num_acc; (n + ofs) mod num_acc = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis NN0 Nat.add_0_right diff_less neq0_conv)
[PROOF STATE]
proof (state)
this:
ofs < num_acc
(n + ofs) mod num_acc = 0

goal (1 subgoal):
 1. \<And>i. \<exists>j>i. r' j \<in> bg_F (degeneralize_ext m)
[PROOF STEP]
with degen_acc_run_complete_aux2[OF NN0 R' ACC' RI OFS_LESS]
[PROOF STATE]
proof (chain)
picking this:
\<exists>j\<ge>Suc i. \<exists>q'. r' j = (q', (n + ofs) mod num_acc) \<and> (n + ofs) mod num_acc \<in> acc q'
ofs < num_acc
(n + ofs) mod num_acc = 0
[PROOF STEP]
obtain j q' where
        "j>i" "r' j = (q',0)" and "0\<in>acc q'"
[PROOF STATE]
proof (prove)
using this:
\<exists>j\<ge>Suc i. \<exists>q'. r' j = (q', (n + ofs) mod num_acc) \<and> (n + ofs) mod num_acc \<in> acc q'
ofs < num_acc
(n + ofs) mod num_acc = 0

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

goal (1 subgoal):
 1. \<And>i. \<exists>j>i. r' j \<in> bg_F (degeneralize_ext m)
[PROOF STEP]
thus "\<exists>j>i. r' j \<in> degen.F T m"
[PROOF STATE]
proof (prove)
using this:
i < j
r' j = (q', 0)
0 \<in> acc q'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i. \<exists>j>i. r' j \<in> bg_F (degeneralize_ext m)

goal (1 subgoal):
 1. \<lbrakk>\<And>r'. \<lbrakk>b_graph.is_acc_run (degeneralize_ext m) r'; r = fst \<circ> r'\<rbrakk> \<Longrightarrow> thesis; num_acc \<noteq> 0\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence "\<exists>\<^sub>\<infinity>i. r' i \<in> degen.F T m"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<exists>j>i. r' j \<in> bg_F (degeneralize_ext m)

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

goal (1 subgoal):
 1. \<lbrakk>\<And>r'. \<lbrakk>b_graph.is_acc_run (degeneralize_ext m) r'; r = fst \<circ> r'\<rbrakk> \<Longrightarrow> thesis; num_acc \<noteq> 0\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "degen.is_acc_run T m r'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b_graph.is_acc_run (degeneralize_ext m) r'
[PROOF STEP]
unfolding degen.is_acc_run_def degen.is_acc_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph_defs.is_run (degeneralize_ext m) r' \<and> (\<exists>\<^sub>\<infinity>i. r' i \<in> bg_F (degeneralize_ext m))
[PROOF STEP]
by rule fact+
[PROOF STATE]
proof (state)
this:
b_graph.is_acc_run (degeneralize_ext m) r'

goal (1 subgoal):
 1. \<lbrakk>\<And>r'. \<lbrakk>b_graph.is_acc_run (degeneralize_ext m) r'; r = fst \<circ> r'\<rbrakk> \<Longrightarrow> thesis; num_acc \<noteq> 0\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
b_graph.is_acc_run (degeneralize_ext m) r'

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma degen_run_find_change:
    assumes NN0[simp]: "num_acc \<noteq> 0"
    assumes R: "degen.is_run T m r"
    assumes A: "i\<le>j" "r i = (q,n)" "r j = (q',n')" "n\<noteq>n'"
    obtains k qk where "i\<le>k" "k<j" "r k = (qk,n)" "n \<in> acc qk"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k qk. \<lbrakk>i \<le> k; k < j; r k = (qk, n); n \<in> acc qk\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>k qk. \<lbrakk>i \<le> k; k < j; r k = (qk, n); n \<in> acc qk\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from degen_run_bound[OF NN0 R] A
[PROOF STATE]
proof (chain)
picking this:
snd (r ?i) < num_acc
i \<le> j
r i = (q, n)
r j = (q', n')
n \<noteq> n'
[PROOF STEP]
have "n<num_acc" "n'<num_acc"
[PROOF STATE]
proof (prove)
using this:
snd (r ?i) < num_acc
i \<le> j
r i = (q, n)
r j = (q', n')
n \<noteq> n'

goal (1 subgoal):
 1. n < num_acc &&& n' < num_acc
[PROOF STEP]
by (metis snd_conv)+
[PROOF STATE]
proof (state)
this:
n < num_acc
n' < num_acc

goal (1 subgoal):
 1. (\<And>k qk. \<lbrakk>i \<le> k; k < j; r k = (qk, n); n \<in> acc qk\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define k where "k = (LEAST k. i<k \<and> snd (r k) \<noteq> n)"
[PROOF STATE]
proof (state)
this:
k = (LEAST k. i < k \<and> snd (r k) \<noteq> n)

goal (1 subgoal):
 1. (\<And>k qk. \<lbrakk>i \<le> k; k < j; r k = (qk, n); n \<in> acc qk\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "i<k" "snd (r k) \<noteq> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < k &&& snd (r k) \<noteq> n
[PROOF STEP]
by (metis (lifting, mono_tags) LeastI_ex A k_def leD less_linear snd_conv)+
[PROOF STATE]
proof (state)
this:
i < k
snd (r k) \<noteq> n

goal (1 subgoal):
 1. (\<And>k qk. \<lbrakk>i \<le> k; k < j; r k = (qk, n); n \<in> acc qk\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from Least_le[where P="\<lambda>k. i<k \<and> snd (r k) \<noteq> n", folded k_def]
[PROOF STATE]
proof (chain)
picking this:
i < ?k \<and> snd (r ?k) \<noteq> n \<Longrightarrow> k \<le> ?k
[PROOF STEP]
have LEK_EQN: "\<forall>k'. i\<le>k' \<and> k'<k \<longrightarrow> snd (r k') = n"
[PROOF STATE]
proof (prove)
using this:
i < ?k \<and> snd (r ?k) \<noteq> n \<Longrightarrow> k \<le> ?k

goal (1 subgoal):
 1. \<forall>k'. i \<le> k' \<and> k' < k \<longrightarrow> snd (r k') = n
[PROOF STEP]
using \<open>r i = (q,n)\<close>
[PROOF STATE]
proof (prove)
using this:
i < ?k \<and> snd (r ?k) \<noteq> n \<Longrightarrow> k \<le> ?k
r i = (q, n)

goal (1 subgoal):
 1. \<forall>k'. i \<le> k' \<and> k' < k \<longrightarrow> snd (r k') = n
[PROOF STEP]
by clarsimp (metis le_neq_implies_less not_le snd_conv)
[PROOF STATE]
proof (state)
this:
\<forall>k'. i \<le> k' \<and> k' < k \<longrightarrow> snd (r k') = n

goal (1 subgoal):
 1. (\<And>k qk. \<lbrakk>i \<le> k; k < j; r k = (qk, n); n \<in> acc qk\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence SND_RKMO: "snd (r (k - 1)) = n"
[PROOF STATE]
proof (prove)
using this:
\<forall>k'. i \<le> k' \<and> k' < k \<longrightarrow> snd (r k') = n

goal (1 subgoal):
 1. snd (r (k - 1)) = n
[PROOF STEP]
using \<open>i<k\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>k'. i \<le> k' \<and> k' < k \<longrightarrow> snd (r k') = n
i < k

goal (1 subgoal):
 1. snd (r (k - 1)) = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
snd (r (k - 1)) = n

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

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

goal (1 subgoal):
 1. (r (k - 1), r k) \<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 (k - 1), r k) \<in> g_E (degeneralize_ext m)
[PROOF STEP]
using \<open>i<k\<close>
[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))
i < k

goal (1 subgoal):
 1. (r (k - 1), r k) \<in> g_E (degeneralize_ext m)
[PROOF STEP]
by clarsimp (metis Suc_pred gr_implies_not0 neq0_conv)
[PROOF STATE]
proof (state)
this:
(r (k - 1), r k) \<in> g_E (degeneralize_ext m)

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

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

goal (1 subgoal):
 1. (\<And>k qk. \<lbrakk>i \<le> k; k < j; r k = (qk, n); n \<in> acc qk\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
snd (r (k - 1)) = n
(r (k - 1), r k) \<in> g_E (degeneralize_ext m)
snd (r k) \<noteq> n
[PROOF STEP]
have "n \<in> acc (fst (r (k - 1)))"
[PROOF STATE]
proof (prove)
using this:
snd (r (k - 1)) = n
(r (k - 1), r k) \<in> g_E (degeneralize_ext m)
snd (r k) \<noteq> n

goal (1 subgoal):
 1. n \<in> acc (fst (r (k - 1)))
[PROOF STEP]
by (auto simp: degeneralize_ext_def split: if_split_asm)
[PROOF STATE]
proof (state)
this:
n \<in> acc (fst (r (k - 1)))

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

goal (1 subgoal):
 1. (\<And>k qk. \<lbrakk>i \<le> k; k < j; r k = (qk, n); n \<in> acc qk\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "k - 1 < j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k - 1 < j
[PROOF STEP]
using A LEK_EQN
[PROOF STATE]
proof (prove)
using this:
i \<le> j
r i = (q, n)
r j = (q', n')
n \<noteq> n'
\<forall>k'. i \<le> k' \<and> k' < k \<longrightarrow> snd (r k') = n

goal (1 subgoal):
 1. k - 1 < j
[PROOF STEP]
apply (rule_tac ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<le> j; r i = (q, n); r j = (q', n'); n \<noteq> n'; \<forall>k'. i \<le> k' \<and> k' < k \<longrightarrow> snd (r k') = n; \<not> k - 1 < j\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<le> j; r i = (q, n); r j = (q', n'); n \<noteq> n'; \<forall>k'. i \<le> k' \<and> k' < k \<longrightarrow> snd (r k') = n; \<not> k - Suc 0 < j\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (metis One_nat_def \<open>snd (r (k - 1)) = n\<close> less_Suc_eq
        less_imp_diff_less not_less_eq snd_conv)
[PROOF STATE]
proof (state)
this:
k - 1 < j

goal (1 subgoal):
 1. (\<And>k qk. \<lbrakk>i \<le> k; k < j; r k = (qk, n); n \<in> acc qk\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n \<in> acc (fst (r (k - 1)))
k - 1 < j
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
n \<in> acc (fst (r (k - 1)))
k - 1 < j

goal (1 subgoal):
 1. thesis
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<in> acc (fst (r (k - 1))); k - 1 < j\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (rule that[of "k - 1" "fst (r (k - 1))"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>n \<in> acc (fst (r (k - 1))); k - 1 < j\<rbrakk> \<Longrightarrow> i \<le> k - 1
 2. \<lbrakk>n \<in> acc (fst (r (k - 1))); k - 1 < j\<rbrakk> \<Longrightarrow> k - 1 < j
 3. \<lbrakk>n \<in> acc (fst (r (k - 1))); k - 1 < j\<rbrakk> \<Longrightarrow> r (k - 1) = (fst (r (k - 1)), n)
 4. \<lbrakk>n \<in> acc (fst (r (k - 1))); k - 1 < j\<rbrakk> \<Longrightarrow> n \<in> acc (fst (r (k - 1)))
[PROOF STEP]
using \<open>i<k\<close> SND_RKMO
[PROOF STATE]
proof (prove)
using this:
i < k
snd (r (k - 1)) = n

goal (4 subgoals):
 1. \<lbrakk>n \<in> acc (fst (r (k - 1))); k - 1 < j\<rbrakk> \<Longrightarrow> i \<le> k - 1
 2. \<lbrakk>n \<in> acc (fst (r (k - 1))); k - 1 < j\<rbrakk> \<Longrightarrow> k - 1 < j
 3. \<lbrakk>n \<in> acc (fst (r (k - 1))); k - 1 < j\<rbrakk> \<Longrightarrow> r (k - 1) = (fst (r (k - 1)), n)
 4. \<lbrakk>n \<in> acc (fst (r (k - 1))); k - 1 < j\<rbrakk> \<Longrightarrow> n \<in> acc (fst (r (k - 1)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed