[STATEMENT]
lemma irs_SDG_path_realizable:
  assumes "n irs-ns\<rightarrow>\<^sub>d* n'" and "n \<noteq> n'"
  obtains ns' where "realizable (CFG_node (_Entry_)) ns' n'" and "n \<in> set ns'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ns'. \<lbrakk>realizable (CFG_node (_Entry_)) ns' n'; n \<in> set ns'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns'
[PROOF STEP]
from \<open>n irs-ns\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n irs-ns\<rightarrow>\<^sub>d* n'
[PROOF STEP]
have "n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')"
[PROOF STATE]
proof (prove)
using this:
n irs-ns\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
proof(rule irs_SDG_path_split)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
 2. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
assume "n is-ns\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (state)
this:
n is-ns\<rightarrow>\<^sub>d* n'

goal (2 subgoals):
 1. n is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
 2. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
proof(cases "ns = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ns = [] \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
 2. ns \<noteq> [] \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
ns = []

goal (2 subgoals):
 1. ns = [] \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
 2. ns \<noteq> [] \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
with \<open>n is-ns\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n is-ns\<rightarrow>\<^sub>d* n'
ns = []
[PROOF STEP]
have "n = n'"
[PROOF STATE]
proof (prove)
using this:
n is-ns\<rightarrow>\<^sub>d* n'
ns = []

goal (1 subgoal):
 1. n = n'
[PROOF STEP]
by(fastforce elim:intra_sum_SDG_path.cases)
[PROOF STATE]
proof (state)
this:
n = n'

goal (2 subgoals):
 1. ns = [] \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
 2. ns \<noteq> [] \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
n = n'

goal (1 subgoal):
 1. n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')

goal (1 subgoal):
 1. ns \<noteq> [] \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ns \<noteq> [] \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
ns \<noteq> []

goal (1 subgoal):
 1. ns \<noteq> [] \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
with \<open>n is-ns\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n is-ns\<rightarrow>\<^sub>d* n'
ns \<noteq> []
[PROOF STEP]
have "n \<in> set ns"
[PROOF STATE]
proof (prove)
using this:
n is-ns\<rightarrow>\<^sub>d* n'
ns \<noteq> []

goal (1 subgoal):
 1. n \<in> set ns
[PROOF STEP]
by(fastforce dest:is_SDG_path_hd)
[PROOF STATE]
proof (state)
this:
n \<in> set ns

goal (1 subgoal):
 1. ns \<noteq> [] \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
from \<open>n is-ns\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n is-ns\<rightarrow>\<^sub>d* n'
[PROOF STEP]
have "valid_SDG_node n" and "valid_SDG_node n'"
[PROOF STATE]
proof (prove)
using this:
n is-ns\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. valid_SDG_node n &&& valid_SDG_node n'
[PROOF STEP]
by(rule is_SDG_path_valid_SDG_node)+
[PROOF STATE]
proof (state)
this:
valid_SDG_node n
valid_SDG_node n'

goal (1 subgoal):
 1. ns \<noteq> [] \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
hence "valid_node (parent_node n)"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n
valid_SDG_node n'

goal (1 subgoal):
 1. valid_node (parent_node n)
[PROOF STEP]
by -(rule valid_SDG_CFG_node)
[PROOF STATE]
proof (state)
this:
valid_node (parent_node n)

goal (1 subgoal):
 1. ns \<noteq> [] \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
from \<open>n is-ns\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n is-ns\<rightarrow>\<^sub>d* n'
[PROOF STEP]
obtain ns' where "matched n ns' n'" and "set ns \<subseteq> set ns'"
[PROOF STATE]
proof (prove)
using this:
n is-ns\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. (\<And>ns'. \<lbrakk>matched n ns' n'; set ns \<subseteq> set ns'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(erule is_SDG_path_matched)
[PROOF STATE]
proof (state)
this:
matched n ns' n'
set ns \<subseteq> set ns'

goal (1 subgoal):
 1. ns \<noteq> [] \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
with \<open>n \<in> set ns\<close>
[PROOF STATE]
proof (chain)
picking this:
n \<in> set ns
matched n ns' n'
set ns \<subseteq> set ns'
[PROOF STEP]
have "n \<in> set ns'"
[PROOF STATE]
proof (prove)
using this:
n \<in> set ns
matched n ns' n'
set ns \<subseteq> set ns'

goal (1 subgoal):
 1. n \<in> set ns'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
n \<in> set ns'

goal (1 subgoal):
 1. ns \<noteq> [] \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
from \<open>valid_node (parent_node n)\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_node (parent_node n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
valid_node (parent_node n)

goal (1 subgoal):
 1. n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
proof(cases "parent_node n = (_Exit_)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>valid_node (parent_node n); parent_node n = (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
 2. \<lbrakk>valid_node (parent_node n); parent_node n \<noteq> (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
parent_node n = (_Exit_)

goal (2 subgoals):
 1. \<lbrakk>valid_node (parent_node n); parent_node n = (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
 2. \<lbrakk>valid_node (parent_node n); parent_node n \<noteq> (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
with \<open>valid_SDG_node n\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n
parent_node n = (_Exit_)
[PROOF STEP]
have "n = CFG_node (_Exit_)"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n
parent_node n = (_Exit_)

goal (1 subgoal):
 1. n = CFG_node (_Exit_)
[PROOF STEP]
by(rule valid_SDG_node_parent_Exit)
[PROOF STATE]
proof (state)
this:
n = CFG_node (_Exit_)

goal (2 subgoals):
 1. \<lbrakk>valid_node (parent_node n); parent_node n = (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
 2. \<lbrakk>valid_node (parent_node n); parent_node n \<noteq> (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
from \<open>n is-ns\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n is-ns\<rightarrow>\<^sub>d* n'
[PROOF STEP]
obtain as where "parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'"
[PROOF STATE]
proof (prove)
using this:
n is-ns\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. (\<And>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by -(erule is_SDG_path_intra_CFG_path)
[PROOF STATE]
proof (state)
this:
parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'

goal (2 subgoals):
 1. \<lbrakk>valid_node (parent_node n); parent_node n = (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
 2. \<lbrakk>valid_node (parent_node n); parent_node n \<noteq> (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
with \<open>n = CFG_node (_Exit_)\<close>
[PROOF STATE]
proof (chain)
picking this:
n = CFG_node (_Exit_)
parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
have "parent_node n' = (_Exit_)"
[PROOF STATE]
proof (prove)
using this:
n = CFG_node (_Exit_)
parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'

goal (1 subgoal):
 1. parent_node n' = (_Exit_)
[PROOF STEP]
by(fastforce dest:path_Exit_source simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
parent_node n' = (_Exit_)

goal (2 subgoals):
 1. \<lbrakk>valid_node (parent_node n); parent_node n = (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
 2. \<lbrakk>valid_node (parent_node n); parent_node n \<noteq> (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
with \<open>valid_SDG_node n'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n'
parent_node n' = (_Exit_)
[PROOF STEP]
have "n' = CFG_node (_Exit_)"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n'
parent_node n' = (_Exit_)

goal (1 subgoal):
 1. n' = CFG_node (_Exit_)
[PROOF STEP]
by(rule valid_SDG_node_parent_Exit)
[PROOF STATE]
proof (state)
this:
n' = CFG_node (_Exit_)

goal (2 subgoals):
 1. \<lbrakk>valid_node (parent_node n); parent_node n = (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
 2. \<lbrakk>valid_node (parent_node n); parent_node n \<noteq> (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
with \<open>n = CFG_node (_Exit_)\<close>
[PROOF STATE]
proof (chain)
picking this:
n = CFG_node (_Exit_)
n' = CFG_node (_Exit_)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n = CFG_node (_Exit_)
n' = CFG_node (_Exit_)

goal (1 subgoal):
 1. n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')

goal (1 subgoal):
 1. \<lbrakk>valid_node (parent_node n); parent_node n \<noteq> (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>valid_node (parent_node n); parent_node n \<noteq> (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
parent_node n \<noteq> (_Exit_)

goal (1 subgoal):
 1. \<lbrakk>valid_node (parent_node n); parent_node n \<noteq> (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
with \<open>valid_SDG_node n\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n
parent_node n \<noteq> (_Exit_)
[PROOF STEP]
obtain nsx where "CFG_node (_Entry_) cc-nsx\<rightarrow>\<^sub>d* n"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n
parent_node n \<noteq> (_Exit_)

goal (1 subgoal):
 1. (\<And>nsx. CFG_node (_Entry_) cc-nsx\<rightarrow>\<^sub>d* n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(erule Entry_cc_SDG_path_to_inner_node)
[PROOF STATE]
proof (state)
this:
CFG_node (_Entry_) cc-nsx\<rightarrow>\<^sub>d* n

goal (1 subgoal):
 1. \<lbrakk>valid_node (parent_node n); parent_node n \<noteq> (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
hence "realizable (CFG_node (_Entry_)) nsx n"
[PROOF STATE]
proof (prove)
using this:
CFG_node (_Entry_) cc-nsx\<rightarrow>\<^sub>d* n

goal (1 subgoal):
 1. realizable (CFG_node (_Entry_)) nsx n
[PROOF STEP]
by(rule cdep_SDG_path_realizable)
[PROOF STATE]
proof (state)
this:
realizable (CFG_node (_Entry_)) nsx n

goal (1 subgoal):
 1. \<lbrakk>valid_node (parent_node n); parent_node n \<noteq> (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
with \<open>matched n ns' n'\<close>
[PROOF STATE]
proof (chain)
picking this:
matched n ns' n'
realizable (CFG_node (_Entry_)) nsx n
[PROOF STEP]
have "realizable (CFG_node (_Entry_)) (nsx@ns') n'"
[PROOF STATE]
proof (prove)
using this:
matched n ns' n'
realizable (CFG_node (_Entry_)) nsx n

goal (1 subgoal):
 1. realizable (CFG_node (_Entry_)) (nsx @ ns') n'
[PROOF STEP]
by -(rule realizable_Append_matched)
[PROOF STATE]
proof (state)
this:
realizable (CFG_node (_Entry_)) (nsx @ ns') n'

goal (1 subgoal):
 1. \<lbrakk>valid_node (parent_node n); parent_node n \<noteq> (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
with \<open>n \<in> set ns'\<close>
[PROOF STATE]
proof (chain)
picking this:
n \<in> set ns'
realizable (CFG_node (_Entry_)) (nsx @ ns') n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n \<in> set ns'
realizable (CFG_node (_Entry_)) (nsx @ ns') n'

goal (1 subgoal):
 1. n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
fix nsx nsx' nx nx' p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
assume "ns = nsx@nx#nsx'" and "n irs-nsx\<rightarrow>\<^sub>d* nx"
      and "nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')" and "nx' is-nsx'\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (state)
this:
ns = nsx @ nx # nsx'
n irs-nsx\<rightarrow>\<^sub>d* nx
nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')
nx' is-nsx'\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
from \<open>nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')\<close>
[PROOF STATE]
proof (chain)
picking this:
nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')
[PROOF STEP]
have "CFG_node (parent_node nx) s-p\<rightarrow>\<^bsub>ret\<^esub> CFG_node (parent_node nx')"
[PROOF STATE]
proof (prove)
using this:
nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')

goal (1 subgoal):
 1. CFG_node (parent_node nx) s-p\<rightarrow>\<^bsub>ret\<^esub> CFG_node (parent_node nx')
[PROOF STEP]
by(fastforce elim:sum_SDG_edge.cases intro:sum_SDG_return_edge)
[PROOF STATE]
proof (state)
this:
CFG_node (parent_node nx) s-p\<rightarrow>\<^bsub>ret\<^esub> CFG_node (parent_node nx')

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
CFG_node (parent_node nx) s-p\<rightarrow>\<^bsub>ret\<^esub> CFG_node (parent_node nx')
[PROOF STEP]
obtain a Q f where "valid_edge a" and "kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f"
      and "parent_node nx = sourcenode a" and "parent_node nx' = targetnode a"
[PROOF STATE]
proof (prove)
using this:
CFG_node (parent_node nx) s-p\<rightarrow>\<^bsub>ret\<^esub> CFG_node (parent_node nx')

goal (1 subgoal):
 1. (\<And>a Q f. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; parent_node nx = sourcenode a; parent_node nx' = targetnode a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:sum_SDG_edge.cases)
[PROOF STATE]
proof (state)
this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
parent_node nx = sourcenode a
parent_node nx' = targetnode a

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
[PROOF STEP]
obtain a' Q' r' fs'
      where "a \<in> get_return_edges a'" and "valid_edge a'" and "kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'"
      and "CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f

goal (1 subgoal):
 1. (\<And>a' Q' r' fs'. \<lbrakk>a \<in> get_return_edges a'; valid_edge a'; kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'; CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(erule return_edge_determines_call_and_sum_edge)
[PROOF STATE]
proof (state)
this:
a \<in> get_return_edges a'
valid_edge a'
kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'
CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
from \<open>valid_edge a'\<close> \<open>kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'
[PROOF STEP]
have "CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a')"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'

goal (1 subgoal):
 1. CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a')
[PROOF STEP]
by(fastforce intro:sum_SDG_call_edge)
[PROOF STATE]
proof (state)
this:
CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a')

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
from \<open>n irs-nsx\<rightarrow>\<^sub>d* nx\<close> \<open>nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')\<close>
[PROOF STATE]
proof (chain)
picking this:
n irs-nsx\<rightarrow>\<^sub>d* nx
nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')
[PROOF STEP]
obtain m ms where "matched m ms nx'" and "n \<in> set ms"
      and "m s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node nx')"
[PROOF STATE]
proof (prove)
using this:
n irs-nsx\<rightarrow>\<^sub>d* nx
nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')

goal (1 subgoal):
 1. (\<And>m ms. \<lbrakk>matched m ms nx'; n \<in> set ms; m s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node nx')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:irs_SDG_path_matched)
[PROOF STATE]
proof (state)
this:
matched m ms nx'
n \<in> set ms
m s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node nx')

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
from \<open>nx' is-nsx'\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
nx' is-nsx'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
obtain ms' where "matched nx' ms' n'"
      and "set nsx' \<subseteq> set ms'"
[PROOF STATE]
proof (prove)
using this:
nx' is-nsx'\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. (\<And>ms'. \<lbrakk>matched nx' ms' n'; set nsx' \<subseteq> set ms'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(erule is_SDG_path_matched)
[PROOF STATE]
proof (state)
this:
matched nx' ms' n'
set nsx' \<subseteq> set ms'

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
with \<open>matched m ms nx'\<close>
[PROOF STATE]
proof (chain)
picking this:
matched m ms nx'
matched nx' ms' n'
set nsx' \<subseteq> set ms'
[PROOF STEP]
have "matched m (ms@ms') n'"
[PROOF STATE]
proof (prove)
using this:
matched m ms nx'
matched nx' ms' n'
set nsx' \<subseteq> set ms'

goal (1 subgoal):
 1. matched m (ms @ ms') n'
[PROOF STEP]
by -(rule matched_Append)
[PROOF STATE]
proof (state)
this:
matched m (ms @ ms') n'

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
from \<open>m s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node nx')\<close>
[PROOF STATE]
proof (chain)
picking this:
m s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node nx')
[PROOF STEP]
have "valid_SDG_node m"
[PROOF STATE]
proof (prove)
using this:
m s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node nx')

goal (1 subgoal):
 1. valid_SDG_node m
[PROOF STEP]
by(rule sum_SDG_edge_valid_SDG_node)
[PROOF STATE]
proof (state)
this:
valid_SDG_node m

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
hence "valid_node (parent_node m)"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node m

goal (1 subgoal):
 1. valid_node (parent_node m)
[PROOF STEP]
by(rule valid_SDG_CFG_node)
[PROOF STATE]
proof (state)
this:
valid_node (parent_node m)

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
valid_node (parent_node m)

goal (1 subgoal):
 1. n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
proof(cases "parent_node m = (_Exit_)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>valid_node (parent_node m); parent_node m = (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
 2. \<lbrakk>valid_node (parent_node m); parent_node m \<noteq> (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
parent_node m = (_Exit_)

goal (2 subgoals):
 1. \<lbrakk>valid_node (parent_node m); parent_node m = (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
 2. \<lbrakk>valid_node (parent_node m); parent_node m \<noteq> (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
from \<open>m s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node nx')\<close>
[PROOF STATE]
proof (chain)
picking this:
m s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node nx')
[PROOF STEP]
obtain a where "valid_edge a"
        and "sourcenode a = parent_node m"
[PROOF STATE]
proof (prove)
using this:
m s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node nx')

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>valid_edge a; sourcenode a = parent_node m\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:sum_SDG_edge.cases)
[PROOF STATE]
proof (state)
this:
valid_edge a
sourcenode a = parent_node m

goal (2 subgoals):
 1. \<lbrakk>valid_node (parent_node m); parent_node m = (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
 2. \<lbrakk>valid_node (parent_node m); parent_node m \<noteq> (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
parent_node m = (_Exit_)
valid_edge a
sourcenode a = parent_node m
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
parent_node m = (_Exit_)
valid_edge a
sourcenode a = parent_node m

goal (1 subgoal):
 1. False
[PROOF STEP]
by -(rule Exit_source,simp_all)
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. \<lbrakk>valid_node (parent_node m); parent_node m = (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
 2. \<lbrakk>valid_node (parent_node m); parent_node m \<noteq> (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')

goal (1 subgoal):
 1. \<lbrakk>valid_node (parent_node m); parent_node m \<noteq> (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>valid_node (parent_node m); parent_node m \<noteq> (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
parent_node m \<noteq> (_Exit_)

goal (1 subgoal):
 1. \<lbrakk>valid_node (parent_node m); parent_node m \<noteq> (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
with \<open>valid_SDG_node m\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node m
parent_node m \<noteq> (_Exit_)
[PROOF STEP]
obtain ms'' where "CFG_node (_Entry_) cc-ms''\<rightarrow>\<^sub>d* m"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node m
parent_node m \<noteq> (_Exit_)

goal (1 subgoal):
 1. (\<And>ms''. CFG_node (_Entry_) cc-ms''\<rightarrow>\<^sub>d* m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(erule Entry_cc_SDG_path_to_inner_node)
[PROOF STATE]
proof (state)
this:
CFG_node (_Entry_) cc-ms''\<rightarrow>\<^sub>d* m

goal (1 subgoal):
 1. \<lbrakk>valid_node (parent_node m); parent_node m \<noteq> (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
hence "realizable (CFG_node (_Entry_)) ms'' m"
[PROOF STATE]
proof (prove)
using this:
CFG_node (_Entry_) cc-ms''\<rightarrow>\<^sub>d* m

goal (1 subgoal):
 1. realizable (CFG_node (_Entry_)) ms'' m
[PROOF STEP]
by(rule cdep_SDG_path_realizable)
[PROOF STATE]
proof (state)
this:
realizable (CFG_node (_Entry_)) ms'' m

goal (1 subgoal):
 1. \<lbrakk>valid_node (parent_node m); parent_node m \<noteq> (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
with \<open>matched m (ms@ms') n'\<close>
[PROOF STATE]
proof (chain)
picking this:
matched m (ms @ ms') n'
realizable (CFG_node (_Entry_)) ms'' m
[PROOF STEP]
have "realizable (CFG_node (_Entry_)) (ms''@(ms@ms')) n'"
[PROOF STATE]
proof (prove)
using this:
matched m (ms @ ms') n'
realizable (CFG_node (_Entry_)) ms'' m

goal (1 subgoal):
 1. realizable (CFG_node (_Entry_)) (ms'' @ ms @ ms') n'
[PROOF STEP]
by -(rule realizable_Append_matched)
[PROOF STATE]
proof (state)
this:
realizable (CFG_node (_Entry_)) (ms'' @ ms @ ms') n'

goal (1 subgoal):
 1. \<lbrakk>valid_node (parent_node m); parent_node m \<noteq> (_Exit_)\<rbrakk> \<Longrightarrow> n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
with \<open>n \<in> set ms\<close>
[PROOF STATE]
proof (chain)
picking this:
n \<in> set ms
realizable (CFG_node (_Entry_)) (ms'' @ ms @ ms') n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n \<in> set ms
realizable (CFG_node (_Entry_)) (ms'' @ ms @ ms') n'

goal (1 subgoal):
 1. n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')

goal (1 subgoal):
 1. \<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns'
[PROOF STEP]
with \<open>n \<noteq> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n \<noteq> n'
n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')
[PROOF STEP]
show "\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns'"
[PROOF STATE]
proof (prove)
using this:
n \<noteq> n'
n = n' \<or> (\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns')

goal (1 subgoal):
 1. \<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>ns'. realizable (CFG_node (_Entry_)) ns' n' \<and> n \<in> set ns'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eff_NatRuleI:
  "nat_rule rule c ants
    \<Longrightarrow> entail = (\<Gamma> \<turnstile> subst s (freshen a c))
    \<Longrightarrow> hyps = ((\<lambda>ant. ((\<lambda>p. subst s (freshen a p)) |`| a_hyps ant |\<union>| \<Gamma> \<turnstile> subst s (freshen a (a_conc ant)))) |`| ants)
    \<Longrightarrow> (\<And> ant f. ant |\<in>| ants \<Longrightarrow> f |\<in>| \<Gamma> \<Longrightarrow> freshenLC a ` (a_fresh ant) \<inter> lconsts f = {})
    \<Longrightarrow> (\<And> ant. ant |\<in>| ants \<Longrightarrow> freshenLC a ` (a_fresh ant) \<inter> subst_lconsts s = {})
    \<Longrightarrow> eff (NatRule rule) entail hyps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nat_rule rule c ants; entail = (\<Gamma> \<turnstile> subst s (freshen a c)); hyps = (\<lambda>ant. (\<lambda>p. subst s (freshen a p)) |`| a_hyps ant |\<union>| \<Gamma> \<turnstile> subst s (freshen a (a_conc ant))) |`| ants; \<And>ant f. \<lbrakk>ant |\<in>| ants; f |\<in>| \<Gamma>\<rbrakk> \<Longrightarrow> freshenLC a ` a_fresh ant \<inter> lconsts f = {}; \<And>ant. ant |\<in>| ants \<Longrightarrow> freshenLC a ` a_fresh ant \<inter> subst_lconsts s = {}\<rbrakk> \<Longrightarrow> eff (NatRule rule) entail hyps
[PROOF STEP]
by (drule eff.intros(2)) simp_all


[STATEMENT]
lemma  natEff_InstI:
  "rule = (r,c)
  \<Longrightarrow> c \<in> set (consequent r)
  \<Longrightarrow> antec = f_antecedent r
  \<Longrightarrow> natEff_Inst rule c antec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rule = (r, c); c \<in> set (consequent r); antec = f_antecedent r\<rbrakk> \<Longrightarrow> natEff_Inst rule c antec
[PROOF STEP]
by (metis natEff_Inst.intros)


[STATEMENT]
lemma "task1_1.solved"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. task1_1.solved
[PROOF STEP]
unfolding task1_1.solved_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c. c |\<in>| task1_1.conc_forms \<longrightarrow> (\<exists>\<Gamma> t. fst (tree.root t) = (\<Gamma> \<turnstile> c) \<and> \<Gamma> |\<subseteq>| task1_1.ass_forms \<and> task1_1.wf t \<and> tfinite t)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<Gamma> t. fst (tree.root t) = (\<Gamma> \<turnstile> A) \<and> \<Gamma> |\<subseteq>| task1_1.ass_forms \<and> task1_1.wf t \<and> tfinite t
[PROOF STEP]
apply (rule_tac x="{|A|}" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t. fst (tree.root t) = ({|A|} \<turnstile> A) \<and> {|A|} |\<subseteq>| task1_1.ass_forms \<and> task1_1.wf t \<and> tfinite t
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t. fst (tree.root t) = ({|A|} \<turnstile> A) \<and> task1_1.wf t \<and> tfinite t
[PROOF STEP]
apply (rule_tac x="Node ({|A|} \<turnstile> A, Axiom) {||}" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (tree.root (Node ({|A|} \<turnstile> A, Axiom) {||})) = ({|A|} \<turnstile> A) \<and> task1_1.wf (Node ({|A|} \<turnstile> A, Axiom) {||}) \<and> tfinite (Node ({|A|} \<turnstile> A, Axiom) {||})
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. task1_1.wf (Node ({|A|} \<turnstile> A, Axiom) {||}) \<and> tfinite (Node ({|A|} \<turnstile> A, Axiom) {||})
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. task1_1.wf (Node ({|A|} \<turnstile> A, Axiom) {||})
 2. tfinite (Node ({|A|} \<turnstile> A, Axiom) {||})
[PROOF STEP]
apply (rule task1_1.wf)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. snd (tree.root (Node ({|A|} \<turnstile> A, Axiom) {||})) \<in> task1_1.R
 2. task1_1.effStep (tree.root (Node ({|A|} \<turnstile> A, Axiom) {||})) ((fst \<circ> tree.root) |`| cont (Node ({|A|} \<turnstile> A, Axiom) {||}))
 3. \<And>t'. t' |\<in>| cont (Node ({|A|} \<turnstile> A, Axiom) {||}) \<Longrightarrow> task1_1.wf t'
 4. tfinite (Node ({|A|} \<turnstile> A, Axiom) {||})
[PROOF STEP]
apply (solves clarsimp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. task1_1.effStep (tree.root (Node ({|A|} \<turnstile> A, Axiom) {||})) ((fst \<circ> tree.root) |`| cont (Node ({|A|} \<turnstile> A, Axiom) {||}))
 2. \<And>t'. t' |\<in>| cont (Node ({|A|} \<turnstile> A, Axiom) {||}) \<Longrightarrow> task1_1.wf t'
 3. tfinite (Node ({|A|} \<turnstile> A, Axiom) {||})
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. task1_1.eff Axiom ({|A|} \<turnstile> A) {||}
 2. \<And>t'. t' |\<in>| cont (Node ({|A|} \<turnstile> A, Axiom) {||}) \<Longrightarrow> task1_1.wf t'
 3. tfinite (Node ({|A|} \<turnstile> A, Axiom) {||})
[PROOF STEP]
apply (rule task1_1.eff.intros(1))
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. A |\<in>| {|A|}
 2. \<And>t'. t' |\<in>| cont (Node ({|A|} \<turnstile> A, Axiom) {||}) \<Longrightarrow> task1_1.wf t'
 3. tfinite (Node ({|A|} \<turnstile> A, Axiom) {||})
[PROOF STEP]
apply (solves simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t'. t' |\<in>| cont (Node ({|A|} \<turnstile> A, Axiom) {||}) \<Longrightarrow> task1_1.wf t'
 2. tfinite (Node ({|A|} \<turnstile> A, Axiom) {||})
[PROOF STEP]
apply (solves clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tfinite (Node ({|A|} \<turnstile> A, Axiom) {||})
[PROOF STEP]
by (auto intro: tfinite.intros)


[STATEMENT]
lemma n_andI [simp]: "n_andI = (andI, Fun and [X,Y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n_andI = (andI, Fun prop_funs.and [X, Y])
[PROOF STEP]
unfolding task2_11.n_rules_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. flat (smap (\<lambda>r. map (Pair r) (consequent r)) prop_rules) !! 0 = (andI, Fun prop_funs.and [X, Y])
[PROOF STEP]
by (simp add: prop_rules_def)


[STATEMENT]
lemma n_andE1 [simp]: "n_andE1 = (andE, X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n_andE1 = (andE, X)
[PROOF STEP]
unfolding task2_11.n_rules_def One_nat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. flat (smap (\<lambda>r. map (Pair r) (consequent r)) prop_rules) !! Suc 0 = (andE, X)
[PROOF STEP]
by (simp add: prop_rules_def)


[STATEMENT]
lemma n_andE2 [simp]: "n_andE2 = (andE, Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n_andE2 = (andE, Y)
[PROOF STEP]
unfolding task2_11.n_rules_def numeral_2_eq_2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. flat (smap (\<lambda>r. map (Pair r) (consequent r)) prop_rules) !! Suc (Suc 0) = (andE, Y)
[PROOF STEP]
by (simp add: prop_rules_def)


[STATEMENT]
lemma n_impI [simp]: "n_impI = (impI, Fun imp [X,Y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n_impI = (impI, Fun imp [X, Y])
[PROOF STEP]
unfolding task2_11.n_rules_def numeral_3_eq_3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. flat (smap (\<lambda>r. map (Pair r) (consequent r)) prop_rules) !! Suc (Suc (Suc 0)) = (impI, Fun imp [X, Y])
[PROOF STEP]
by (simp add: prop_rules_def)


[STATEMENT]
lemma n_impE [simp]: "n_impE = (impE, Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n_impE = (impE, Y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n_impE = (impE, Y)
[PROOF STEP]
have "n_impE = task2_11.n_rules !! Suc 3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n_impE = task2_11.n_rules !! Suc 3
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n_impE = task2_11.n_rules !! Suc 3

goal (1 subgoal):
 1. n_impE = (impE, Y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
n_impE = task2_11.n_rules !! Suc 3

goal (1 subgoal):
 1. n_impE = (impE, Y)
[PROOF STEP]
have "... = (impE, Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. task2_11.n_rules !! Suc 3 = (impE, Y)
[PROOF STEP]
unfolding task2_11.n_rules_def numeral_3_eq_3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. flat (smap (\<lambda>r. map (Pair r) (consequent r)) prop_rules) !! Suc (Suc (Suc (Suc 0))) = (impE, Y)
[PROOF STEP]
by (simp add: prop_rules_def)
[PROOF STATE]
proof (state)
this:
task2_11.n_rules !! Suc 3 = (impE, Y)

goal (1 subgoal):
 1. n_impE = (impE, Y)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
n_impE = (impE, Y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n_impE = (impE, Y)

goal (1 subgoal):
 1. n_impE = (impE, Y)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
n_impE = (impE, Y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subst_Var_eq_id [simp]: "subst Var = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst Var = id
[PROOF STEP]
by (rule ext) (induct_tac x; auto simp: map_idI)


[STATEMENT]
lemma xy_update: "f = undefined(''X'' := x, ''Y'' := y) \<Longrightarrow> x = f ''X'' \<and> y = f ''Y''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = undefined(''X'' := x, ''Y'' := y) \<Longrightarrow> x = f ''X'' \<and> y = f ''Y''
[PROOF STEP]
by force


[STATEMENT]
lemma y_update: "f = undefined(''Y'':=y) \<Longrightarrow> y = f ''Y''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = undefined(''Y'' := y) \<Longrightarrow> y = f ''Y''
[PROOF STEP]
by force


[STATEMENT]
lemma "steps0 (1, [], <([]::nat list)>) tm_onestroke 2 = (0, [Bk], [Oc])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. steps0 (1, [], <[]>) tm_onestroke 2 = (0, [Bk], [Oc])
[PROOF STEP]
by (simp add: tape_of_nat_def tape_of_list_def
                tm_onestroke_def
                numeral_eqs_upto_12
                step.simps steps.simps)


[STATEMENT]
lemma "steps0 (1, [], <[0::nat]>) tm_onestroke 4 = (0, [Bk, Bk], [Oc])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. steps0 (1, [], <[0]>) tm_onestroke 4 = (0, [Bk, Bk], [Oc])
[PROOF STEP]
by (simp add: tape_of_nat_def tape_of_list_def
                tm_onestroke_def
                numeral_eqs_upto_12
                step.simps steps.simps)


[STATEMENT]
lemma "steps0 (1, [], <[0::nat,0]>) tm_onestroke 7 = (0, [Bk, Bk, Bk, Bk], [Oc])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. steps0 (1, [], <[0, 0]>) tm_onestroke 7 = (0, [Bk, Bk, Bk, Bk], [Oc])
[PROOF STEP]
by (simp add: tape_of_nat_def tape_of_list_def
                tm_onestroke_def
                numeral_eqs_upto_12
                step.simps steps.simps)


[STATEMENT]
lemma "steps0 (1, [], <[1::nat,1]>) tm_onestroke 11 = (0, [Bk, Bk, Bk, Bk, Bk, Bk], [Oc])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. steps0 (1, [], <[1, 1]>) tm_onestroke 11 = (0, [Bk, Bk, Bk, Bk, Bk, Bk], [Oc])
[PROOF STEP]
by (simp add: tape_of_nat_def tape_of_list_def
                tm_onestroke_def
                numeral_eqs_upto_12
                step.simps steps.simps)


[STATEMENT]
lemma tm_onestroke_cases:
  fixes s::nat
  assumes "inv_tm_onestroke (s,l,r)"
    and "s=0 \<Longrightarrow> P"
    and "s=1 \<Longrightarrow> P"
    and "s=2 \<Longrightarrow> P"
    and "s=3 \<Longrightarrow> P"
  shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P
[PROOF STEP]
have "s < 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s < 4
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> s < 4 \<Longrightarrow> False
[PROOF STEP]
assume "\<not> s < 4"
[PROOF STATE]
proof (state)
this:
\<not> s < 4

goal (1 subgoal):
 1. \<not> s < 4 \<Longrightarrow> False
[PROOF STEP]
with \<open>inv_tm_onestroke (s,l,r)\<close>
[PROOF STATE]
proof (chain)
picking this:
inv_tm_onestroke (s, l, r)
\<not> s < 4
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
inv_tm_onestroke (s, l, r)
\<not> s < 4

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

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

goal (1 subgoal):
 1. P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s < 4
[PROOF STEP]
have "s = 0 \<or> s = 1 \<or> s = 2 \<or> s = 3"
[PROOF STATE]
proof (prove)
using this:
s < 4

goal (1 subgoal):
 1. s = 0 \<or> s = 1 \<or> s = 2 \<or> s = 3
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s = 0 \<or> s = 1 \<or> s = 2 \<or> s = 3

goal (1 subgoal):
 1. P
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
inv_tm_onestroke (s, l, r)
s = 0 \<Longrightarrow> P
s = 1 \<Longrightarrow> P
s = 2 \<Longrightarrow> P
s = 3 \<Longrightarrow> P
s = 0 \<or> s = 1 \<or> s = 2 \<or> s = 3
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inv_tm_onestroke (s, l, r)
s = 0 \<Longrightarrow> P
s = 1 \<Longrightarrow> P
s = 2 \<Longrightarrow> P
s = 3 \<Longrightarrow> P
s = 0 \<or> s = 1 \<or> s = 2 \<or> s = 3

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inv_tm_onestroke_step:
  assumes "inv_tm_onestroke cf"
  shows "inv_tm_onestroke (step0 cf tm_onestroke)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
proof (cases cf)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c. cf = (a, b, c) \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
case (fields s l r)
[PROOF STATE]
proof (state)
this:
cf = (s, l, r)

goal (1 subgoal):
 1. \<And>a b c. cf = (a, b, c) \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cf = (s, l, r)
[PROOF STEP]
have cf_cases: "cf = (s, l, r)"
[PROOF STATE]
proof (prove)
using this:
cf = (s, l, r)

goal (1 subgoal):
 1. cf = (s, l, r)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
cf = (s, l, r)

goal (1 subgoal):
 1. \<And>a b c. cf = (a, b, c) \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
show "inv_tm_onestroke (step0 cf tm_onestroke)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
proof (rule tm_onestroke_cases)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. inv_tm_onestroke (?s, ?l, ?r)
 2. ?s = 0 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
 3. ?s = 1 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
 4. ?s = 2 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
 5. ?s = 3 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
from cf_cases and assms
[PROOF STATE]
proof (chain)
picking this:
cf = (s, l, r)
inv_tm_onestroke cf
[PROOF STEP]
show "inv_tm_onestroke (s, l, r)"
[PROOF STATE]
proof (prove)
using this:
cf = (s, l, r)
inv_tm_onestroke cf

goal (1 subgoal):
 1. inv_tm_onestroke (s, l, r)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (s, l, r)

goal (4 subgoals):
 1. s = 0 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
 2. s = 1 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
 3. s = 2 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
 4. s = 3 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. s = 0 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
 2. s = 1 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
 3. s = 2 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
 4. s = 3 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
assume "s = 0"
[PROOF STATE]
proof (state)
this:
s = 0

goal (4 subgoals):
 1. s = 0 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
 2. s = 1 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
 3. s = 2 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
 4. s = 3 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
with cf_cases and assms
[PROOF STATE]
proof (chain)
picking this:
cf = (s, l, r)
inv_tm_onestroke cf
s = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cf = (s, l, r)
inv_tm_onestroke cf
s = 0

goal (1 subgoal):
 1. inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
by (auto simp add: tm_onestroke_def)
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (step0 cf tm_onestroke)

goal (3 subgoals):
 1. s = 1 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
 2. s = 2 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
 3. s = 3 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. s = 1 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
 2. s = 2 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
 3. s = 3 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
assume "s = 1"
[PROOF STATE]
proof (state)
this:
s = 1

goal (3 subgoals):
 1. s = 1 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
 2. s = 2 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
 3. s = 3 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
have "inv_tm_onestroke (step0 (1, l, r) tm_onestroke)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
proof (cases r)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r = [] \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
 2. \<And>a list. r = a # list \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
r = []

goal (2 subgoals):
 1. r = [] \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
 2. \<And>a list. r = a # list \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r = []
[PROOF STEP]
have "r = []"
[PROOF STATE]
proof (prove)
using this:
r = []

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

goal (2 subgoals):
 1. r = [] \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
 2. \<And>a list. r = a # list \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
with assms and cf_cases and \<open>s = 1\<close>
[PROOF STATE]
proof (chain)
picking this:
inv_tm_onestroke cf
cf = (s, l, r)
s = 1
r = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inv_tm_onestroke cf
cf = (s, l, r)
s = 1
r = []

goal (1 subgoal):
 1. inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
by (auto simp add: tm_onestroke_def step.simps steps.simps)
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (step0 (1, l, r) tm_onestroke)

goal (1 subgoal):
 1. \<And>a list. r = a # list \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. r = a # list \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
case (Cons a rs)
[PROOF STATE]
proof (state)
this:
r = a # rs

goal (1 subgoal):
 1. \<And>a list. r = a # list \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r = a # rs
[PROOF STEP]
have "r = a # rs"
[PROOF STATE]
proof (prove)
using this:
r = a # rs

goal (1 subgoal):
 1. r = a # rs
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
r = a # rs

goal (1 subgoal):
 1. \<And>a list. r = a # list \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
proof (cases a)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
 2. a = Oc \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
 2. a = Oc \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
case Oc
[PROOF STATE]
proof (state)
this:
a = Oc

goal (2 subgoals):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
 2. a = Oc \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = Oc
[PROOF STEP]
have "a = Oc"
[PROOF STATE]
proof (prove)
using this:
a = Oc

goal (1 subgoal):
 1. a = Oc
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
a = Oc

goal (2 subgoals):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
 2. a = Oc \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
with assms and \<open>r = a # rs\<close> and cf_cases and \<open>s = 1\<close>
[PROOF STATE]
proof (chain)
picking this:
inv_tm_onestroke cf
r = a # rs
cf = (s, l, r)
s = 1
a = Oc
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inv_tm_onestroke cf
r = a # rs
cf = (s, l, r)
s = 1
a = Oc

goal (1 subgoal):
 1. inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
by (auto simp add: tm_onestroke_def noDblBk_def
                               step.simps steps.simps)
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (step0 (1, l, r) tm_onestroke)

goal (1 subgoal):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
case Bk
[PROOF STATE]
proof (state)
this:
a = Bk

goal (1 subgoal):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = Bk
[PROOF STEP]
have "a = Bk"
[PROOF STATE]
proof (prove)
using this:
a = Bk

goal (1 subgoal):
 1. a = Bk
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
a = Bk

goal (1 subgoal):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
from assms and cf_cases  and \<open>s = 1\<close>
[PROOF STATE]
proof (chain)
picking this:
inv_tm_onestroke cf
cf = (s, l, r)
s = 1
[PROOF STEP]
have "noDblBk r"
[PROOF STATE]
proof (prove)
using this:
inv_tm_onestroke cf
cf = (s, l, r)
s = 1

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

goal (1 subgoal):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
with \<open>r = a # rs\<close>
[PROOF STATE]
proof (chain)
picking this:
r = a # rs
noDblBk r
[PROOF STEP]
have "noDblBk rs"
[PROOF STATE]
proof (prove)
using this:
r = a # rs
noDblBk r

goal (1 subgoal):
 1. noDblBk rs
[PROOF STEP]
by (auto simp add: noDblBk_def)
[PROOF STATE]
proof (state)
this:
noDblBk rs

goal (1 subgoal):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
from \<open>r = a # rs\<close> and \<open>a = Bk\<close> and \<open>noDblBk r\<close>
[PROOF STATE]
proof (chain)
picking this:
r = a # rs
a = Bk
noDblBk r
[PROOF STEP]
have "r!0 = Bk \<and> (rs = [] \<or> r!(Suc 0) = Oc)"
[PROOF STATE]
proof (prove)
using this:
r = a # rs
a = Bk
noDblBk r

goal (1 subgoal):
 1. r ! 0 = Bk \<and> (rs = [] \<or> r ! Suc 0 = Oc)
[PROOF STEP]
using noDblBk_def
[PROOF STATE]
proof (prove)
using this:
r = a # rs
a = Bk
noDblBk r
noDblBk ?cs \<equiv> \<forall>i. Suc i < length ?cs \<and> ?cs ! i = Bk \<longrightarrow> ?cs ! Suc i = Oc

goal (1 subgoal):
 1. r ! 0 = Bk \<and> (rs = [] \<or> r ! Suc 0 = Oc)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
r ! 0 = Bk \<and> (rs = [] \<or> r ! Suc 0 = Oc)

goal (1 subgoal):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
with \<open>r = a # rs\<close>
[PROOF STATE]
proof (chain)
picking this:
r = a # rs
r ! 0 = Bk \<and> (rs = [] \<or> r ! Suc 0 = Oc)
[PROOF STEP]
have  "(rs = [] \<or> rs!0 = Oc)"
[PROOF STATE]
proof (prove)
using this:
r = a # rs
r ! 0 = Bk \<and> (rs = [] \<or> r ! Suc 0 = Oc)

goal (1 subgoal):
 1. rs = [] \<or> rs ! 0 = Oc
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rs = [] \<or> rs ! 0 = Oc

goal (1 subgoal):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rs = [] \<or> rs ! 0 = Oc
[PROOF STEP]
have "(rs = [] \<or> (\<exists>rs'. rs = Oc#rs'))"
[PROOF STATE]
proof (prove)
using this:
rs = [] \<or> rs ! 0 = Oc

goal (1 subgoal):
 1. rs = [] \<or> (\<exists>rs'. rs = Oc # rs')
[PROOF STEP]
by (metis hd_conv_nth list.collapse)
[PROOF STATE]
proof (state)
this:
rs = [] \<or> (\<exists>rs'. rs = Oc # rs')

goal (1 subgoal):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
from \<open>a = Bk\<close> and \<open>r = a # rs\<close> and cf_cases and \<open>s = 1\<close>
[PROOF STATE]
proof (chain)
picking this:
a = Bk
r = a # rs
cf = (s, l, r)
s = 1
[PROOF STEP]
have "inv_tm_onestroke (step0 (1, l, r) tm_onestroke) =
                  inv_tm_onestroke (step0 (1, l, Bk#rs) tm_onestroke)"
[PROOF STATE]
proof (prove)
using this:
a = Bk
r = a # rs
cf = (s, l, r)
s = 1

goal (1 subgoal):
 1. inv_tm_onestroke (step0 (1, l, r) tm_onestroke) = inv_tm_onestroke (step0 (1, l, Bk # rs) tm_onestroke)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (step0 (1, l, r) tm_onestroke) = inv_tm_onestroke (step0 (1, l, Bk # rs) tm_onestroke)

goal (1 subgoal):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (step0 (1, l, r) tm_onestroke) = inv_tm_onestroke (step0 (1, l, Bk # rs) tm_onestroke)

goal (1 subgoal):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
have "... = inv_tm_onestroke (3, Bk#l,rs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_tm_onestroke (step0 (1, l, Bk # rs) tm_onestroke) = inv_tm_onestroke (3, Bk # l, rs)
[PROOF STEP]
by (auto simp add: tm_onestroke_def step.simps steps.simps)
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (step0 (1, l, Bk # rs) tm_onestroke) = inv_tm_onestroke (3, Bk # l, rs)

goal (1 subgoal):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (step0 (1, l, Bk # rs) tm_onestroke) = inv_tm_onestroke (3, Bk # l, rs)

goal (1 subgoal):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
with assms and \<open>r = a # rs\<close>  and \<open>a = Bk\<close> and \<open>a = Bk\<close>
            and cf_cases and \<open>s = 1\<close> and \<open>noDblBk rs\<close>
            and \<open>(rs = [] \<or> (\<exists>rs'. rs = Oc#rs'))\<close>
[PROOF STATE]
proof (chain)
picking this:
inv_tm_onestroke cf
r = a # rs
a = Bk
a = Bk
cf = (s, l, r)
s = 1
noDblBk rs
rs = [] \<or> (\<exists>rs'. rs = Oc # rs')
inv_tm_onestroke (step0 (1, l, Bk # rs) tm_onestroke) = inv_tm_onestroke (3, Bk # l, rs)
[PROOF STEP]
have "... = True"
[PROOF STATE]
proof (prove)
using this:
inv_tm_onestroke cf
r = a # rs
a = Bk
a = Bk
cf = (s, l, r)
s = 1
noDblBk rs
rs = [] \<or> (\<exists>rs'. rs = Oc # rs')
inv_tm_onestroke (step0 (1, l, Bk # rs) tm_onestroke) = inv_tm_onestroke (3, Bk # l, rs)

goal (1 subgoal):
 1. inv_tm_onestroke (3, Bk # l, rs) = True
[PROOF STEP]
by (auto simp add: tm_onestroke_def numeral_eqs_upto_12)
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (3, Bk # l, rs) = True

goal (1 subgoal):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
inv_tm_onestroke (step0 (1, l, r) tm_onestroke) = True
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inv_tm_onestroke (step0 (1, l, r) tm_onestroke) = True

goal (1 subgoal):
 1. inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (step0 (1, l, r) tm_onestroke)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (step0 (1, l, r) tm_onestroke)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (step0 (1, l, r) tm_onestroke)

goal (1 subgoal):
 1. inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
with cf_cases and \<open>s=1\<close>
[PROOF STATE]
proof (chain)
picking this:
cf = (s, l, r)
s = 1
inv_tm_onestroke (step0 (1, l, r) tm_onestroke)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cf = (s, l, r)
s = 1
inv_tm_onestroke (step0 (1, l, r) tm_onestroke)

goal (1 subgoal):
 1. inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (step0 cf tm_onestroke)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (step0 cf tm_onestroke)

goal (2 subgoals):
 1. s = 2 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
 2. s = 3 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s = 2 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
 2. s = 3 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
assume "s = 2"
[PROOF STATE]
proof (state)
this:
s = 2

goal (2 subgoals):
 1. s = 2 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
 2. s = 3 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
show "inv_tm_onestroke (step0 cf tm_onestroke)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
have "inv_tm_onestroke (step0 (2, l, r) tm_onestroke)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_tm_onestroke (step0 (2, l, r) tm_onestroke)
[PROOF STEP]
proof (cases r)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r = [] \<Longrightarrow> inv_tm_onestroke (step0 (2, l, r) tm_onestroke)
 2. \<And>a list. r = a # list \<Longrightarrow> inv_tm_onestroke (step0 (2, l, r) tm_onestroke)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
r = []

goal (2 subgoals):
 1. r = [] \<Longrightarrow> inv_tm_onestroke (step0 (2, l, r) tm_onestroke)
 2. \<And>a list. r = a # list \<Longrightarrow> inv_tm_onestroke (step0 (2, l, r) tm_onestroke)
[PROOF STEP]
with assms and cf_cases and \<open>s = 2\<close>
[PROOF STATE]
proof (chain)
picking this:
inv_tm_onestroke cf
cf = (s, l, r)
s = 2
r = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inv_tm_onestroke cf
cf = (s, l, r)
s = 2
r = []

goal (1 subgoal):
 1. inv_tm_onestroke (step0 (2, l, r) tm_onestroke)
[PROOF STEP]
by (auto simp add: tm_onestroke_def numeral_eqs_upto_12)
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (step0 (2, l, r) tm_onestroke)

goal (1 subgoal):
 1. \<And>a list. r = a # list \<Longrightarrow> inv_tm_onestroke (step0 (2, l, r) tm_onestroke)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. r = a # list \<Longrightarrow> inv_tm_onestroke (step0 (2, l, r) tm_onestroke)
[PROOF STEP]
case (Cons a rs)
[PROOF STATE]
proof (state)
this:
r = a # rs

goal (1 subgoal):
 1. \<And>a list. r = a # list \<Longrightarrow> inv_tm_onestroke (step0 (2, l, r) tm_onestroke)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r = a # rs
[PROOF STEP]
have "r = a # rs"
[PROOF STATE]
proof (prove)
using this:
r = a # rs

goal (1 subgoal):
 1. r = a # rs
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
r = a # rs

goal (1 subgoal):
 1. \<And>a list. r = a # list \<Longrightarrow> inv_tm_onestroke (step0 (2, l, r) tm_onestroke)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_tm_onestroke (step0 (2, l, r) tm_onestroke)
[PROOF STEP]
proof (cases a)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (2, l, r) tm_onestroke)
 2. a = Oc \<Longrightarrow> inv_tm_onestroke (step0 (2, l, r) tm_onestroke)
[PROOF STEP]
case Bk
[PROOF STATE]
proof (state)
this:
a = Bk

goal (2 subgoals):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (2, l, r) tm_onestroke)
 2. a = Oc \<Longrightarrow> inv_tm_onestroke (step0 (2, l, r) tm_onestroke)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = Bk
[PROOF STEP]
have "a = Bk"
[PROOF STATE]
proof (prove)
using this:
a = Bk

goal (1 subgoal):
 1. a = Bk
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
a = Bk

goal (2 subgoals):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (2, l, r) tm_onestroke)
 2. a = Oc \<Longrightarrow> inv_tm_onestroke (step0 (2, l, r) tm_onestroke)
[PROOF STEP]
with assms and \<open>r = a # rs\<close> and cf_cases and \<open>s = 2\<close>
[PROOF STATE]
proof (chain)
picking this:
inv_tm_onestroke cf
r = a # rs
cf = (s, l, r)
s = 2
a = Bk
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inv_tm_onestroke cf
r = a # rs
cf = (s, l, r)
s = 2
a = Bk

goal (1 subgoal):
 1. inv_tm_onestroke (step0 (2, l, r) tm_onestroke)
[PROOF STEP]
by (auto simp add: tm_onestroke_def numeral_eqs_upto_12
                               step.simps steps.simps)
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (step0 (2, l, r) tm_onestroke)

goal (1 subgoal):
 1. a = Oc \<Longrightarrow> inv_tm_onestroke (step0 (2, l, r) tm_onestroke)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a = Oc \<Longrightarrow> inv_tm_onestroke (step0 (2, l, r) tm_onestroke)
[PROOF STEP]
case Oc
[PROOF STATE]
proof (state)
this:
a = Oc

goal (1 subgoal):
 1. a = Oc \<Longrightarrow> inv_tm_onestroke (step0 (2, l, r) tm_onestroke)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = Oc
[PROOF STEP]
have "a = Oc"
[PROOF STATE]
proof (prove)
using this:
a = Oc

goal (1 subgoal):
 1. a = Oc
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
a = Oc

goal (1 subgoal):
 1. a = Oc \<Longrightarrow> inv_tm_onestroke (step0 (2, l, r) tm_onestroke)
[PROOF STEP]
with assms and \<open>r = a # rs\<close> and cf_cases and \<open>s = 2\<close>
[PROOF STATE]
proof (chain)
picking this:
inv_tm_onestroke cf
r = a # rs
cf = (s, l, r)
s = 2
a = Oc
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inv_tm_onestroke cf
r = a # rs
cf = (s, l, r)
s = 2
a = Oc

goal (1 subgoal):
 1. inv_tm_onestroke (step0 (2, l, r) tm_onestroke)
[PROOF STEP]
by (auto simp add: tm_onestroke_def numeral_eqs_upto_12)
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (step0 (2, l, r) tm_onestroke)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (step0 (2, l, r) tm_onestroke)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (step0 (2, l, r) tm_onestroke)

goal (1 subgoal):
 1. inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
with cf_cases and \<open>s=2\<close>
[PROOF STATE]
proof (chain)
picking this:
cf = (s, l, r)
s = 2
inv_tm_onestroke (step0 (2, l, r) tm_onestroke)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cf = (s, l, r)
s = 2
inv_tm_onestroke (step0 (2, l, r) tm_onestroke)

goal (1 subgoal):
 1. inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (step0 cf tm_onestroke)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (step0 cf tm_onestroke)

goal (1 subgoal):
 1. s = 3 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s = 3 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
assume "s = 3"
[PROOF STATE]
proof (state)
this:
s = 3

goal (1 subgoal):
 1. s = 3 \<Longrightarrow> inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
show "inv_tm_onestroke (step0 cf tm_onestroke)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
have "inv_tm_onestroke (step0 (3, l, r) tm_onestroke)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_tm_onestroke (step0 (3, l, r) tm_onestroke)
[PROOF STEP]
proof (cases r)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r = [] \<Longrightarrow> inv_tm_onestroke (step0 (3, l, r) tm_onestroke)
 2. \<And>a list. r = a # list \<Longrightarrow> inv_tm_onestroke (step0 (3, l, r) tm_onestroke)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
r = []

goal (2 subgoals):
 1. r = [] \<Longrightarrow> inv_tm_onestroke (step0 (3, l, r) tm_onestroke)
 2. \<And>a list. r = a # list \<Longrightarrow> inv_tm_onestroke (step0 (3, l, r) tm_onestroke)
[PROOF STEP]
with assms and cf_cases and \<open>s = 3\<close>
[PROOF STATE]
proof (chain)
picking this:
inv_tm_onestroke cf
cf = (s, l, r)
s = 3
r = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inv_tm_onestroke cf
cf = (s, l, r)
s = 3
r = []

goal (1 subgoal):
 1. inv_tm_onestroke (step0 (3, l, r) tm_onestroke)
[PROOF STEP]
by (auto simp add: tm_onestroke_def numeral_eqs_upto_12 noDblBk_def
                             step.simps steps.simps)
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (step0 (3, l, r) tm_onestroke)

goal (1 subgoal):
 1. \<And>a list. r = a # list \<Longrightarrow> inv_tm_onestroke (step0 (3, l, r) tm_onestroke)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. r = a # list \<Longrightarrow> inv_tm_onestroke (step0 (3, l, r) tm_onestroke)
[PROOF STEP]
case (Cons a rs)
[PROOF STATE]
proof (state)
this:
r = a # rs

goal (1 subgoal):
 1. \<And>a list. r = a # list \<Longrightarrow> inv_tm_onestroke (step0 (3, l, r) tm_onestroke)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r = a # rs
[PROOF STEP]
have "r = a # rs"
[PROOF STATE]
proof (prove)
using this:
r = a # rs

goal (1 subgoal):
 1. r = a # rs
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
r = a # rs

goal (1 subgoal):
 1. \<And>a list. r = a # list \<Longrightarrow> inv_tm_onestroke (step0 (3, l, r) tm_onestroke)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_tm_onestroke (step0 (3, l, r) tm_onestroke)
[PROOF STEP]
proof (cases a)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (3, l, r) tm_onestroke)
 2. a = Oc \<Longrightarrow> inv_tm_onestroke (step0 (3, l, r) tm_onestroke)
[PROOF STEP]
case Oc
[PROOF STATE]
proof (state)
this:
a = Oc

goal (2 subgoals):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (3, l, r) tm_onestroke)
 2. a = Oc \<Longrightarrow> inv_tm_onestroke (step0 (3, l, r) tm_onestroke)
[PROOF STEP]
with assms and \<open>r = a # rs\<close> and cf_cases and \<open>s = 3\<close>
[PROOF STATE]
proof (chain)
picking this:
inv_tm_onestroke cf
r = a # rs
cf = (s, l, r)
s = 3
a = Oc
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inv_tm_onestroke cf
r = a # rs
cf = (s, l, r)
s = 3
a = Oc

goal (1 subgoal):
 1. inv_tm_onestroke (step0 (3, l, r) tm_onestroke)
[PROOF STEP]
by (auto simp add: tm_onestroke_def numeral_eqs_upto_12 noDblBk_def
                               step.simps steps.simps)
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (step0 (3, l, r) tm_onestroke)

goal (1 subgoal):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (3, l, r) tm_onestroke)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (3, l, r) tm_onestroke)
[PROOF STEP]
case Bk
[PROOF STATE]
proof (state)
this:
a = Bk

goal (1 subgoal):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (3, l, r) tm_onestroke)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = Bk
[PROOF STEP]
have "a = Bk"
[PROOF STATE]
proof (prove)
using this:
a = Bk

goal (1 subgoal):
 1. a = Bk
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
a = Bk

goal (1 subgoal):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (3, l, r) tm_onestroke)
[PROOF STEP]
from assms and cf_cases and \<open>s = 3\<close>
[PROOF STATE]
proof (chain)
picking this:
inv_tm_onestroke cf
cf = (s, l, r)
s = 3
[PROOF STEP]
have "(r= [] \<or> (\<exists>rs. r = Oc#rs))"
[PROOF STATE]
proof (prove)
using this:
inv_tm_onestroke cf
cf = (s, l, r)
s = 3

goal (1 subgoal):
 1. r = [] \<or> (\<exists>rs. r = Oc # rs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r = [] \<or> (\<exists>rs. r = Oc # rs)

goal (1 subgoal):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (3, l, r) tm_onestroke)
[PROOF STEP]
with \<open>a = Bk\<close> and  \<open>r = a # rs\<close>
[PROOF STATE]
proof (chain)
picking this:
a = Bk
r = a # rs
r = [] \<or> (\<exists>rs. r = Oc # rs)
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
a = Bk
r = a # rs
r = [] \<or> (\<exists>rs. r = Oc # rs)

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

goal (1 subgoal):
 1. a = Bk \<Longrightarrow> inv_tm_onestroke (step0 (3, l, r) tm_onestroke)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. inv_tm_onestroke (step0 (3, l, r) tm_onestroke)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (step0 (3, l, r) tm_onestroke)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (step0 (3, l, r) tm_onestroke)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (step0 (3, l, r) tm_onestroke)

goal (1 subgoal):
 1. inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
with cf_cases and \<open>s=3\<close>
[PROOF STATE]
proof (chain)
picking this:
cf = (s, l, r)
s = 3
inv_tm_onestroke (step0 (3, l, r) tm_onestroke)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cf = (s, l, r)
s = 3
inv_tm_onestroke (step0 (3, l, r) tm_onestroke)

goal (1 subgoal):
 1. inv_tm_onestroke (step0 cf tm_onestroke)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (step0 cf tm_onestroke)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (step0 cf tm_onestroke)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (step0 cf tm_onestroke)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inv_tm_onestroke_steps:
  assumes "inv_tm_onestroke cf"
  shows "inv_tm_onestroke (steps0 cf tm_onestroke stp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_tm_onestroke (steps0 cf tm_onestroke stp)
[PROOF STEP]
proof (induct stp)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inv_tm_onestroke (steps0 cf tm_onestroke 0)
 2. \<And>stp. inv_tm_onestroke (steps0 cf tm_onestroke stp) \<Longrightarrow> inv_tm_onestroke (steps0 cf tm_onestroke (Suc stp))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. inv_tm_onestroke (steps0 cf tm_onestroke 0)
 2. \<And>stp. inv_tm_onestroke (steps0 cf tm_onestroke stp) \<Longrightarrow> inv_tm_onestroke (steps0 cf tm_onestroke (Suc stp))
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
inv_tm_onestroke cf
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
inv_tm_onestroke cf

goal (1 subgoal):
 1. inv_tm_onestroke (steps0 cf tm_onestroke 0)
[PROOF STEP]
by (auto simp add: inv_tm_onestroke_step step.simps steps.simps)
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (steps0 cf tm_onestroke 0)

goal (1 subgoal):
 1. \<And>stp. inv_tm_onestroke (steps0 cf tm_onestroke stp) \<Longrightarrow> inv_tm_onestroke (steps0 cf tm_onestroke (Suc stp))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>stp. inv_tm_onestroke (steps0 cf tm_onestroke stp) \<Longrightarrow> inv_tm_onestroke (steps0 cf tm_onestroke (Suc stp))
[PROOF STEP]
case (Suc stp)
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (steps0 cf tm_onestroke stp)

goal (1 subgoal):
 1. \<And>stp. inv_tm_onestroke (steps0 cf tm_onestroke stp) \<Longrightarrow> inv_tm_onestroke (steps0 cf tm_onestroke (Suc stp))
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
inv_tm_onestroke cf
inv_tm_onestroke (steps0 cf tm_onestroke stp)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
inv_tm_onestroke cf
inv_tm_onestroke (steps0 cf tm_onestroke stp)

goal (1 subgoal):
 1. inv_tm_onestroke (steps0 cf tm_onestroke (Suc stp))
[PROOF STEP]
using inv_tm_onestroke_step step_red
[PROOF STATE]
proof (prove)
using this:
inv_tm_onestroke cf
inv_tm_onestroke (steps0 cf tm_onestroke stp)
inv_tm_onestroke ?cf \<Longrightarrow> inv_tm_onestroke (step0 ?cf tm_onestroke)
steps ?c ?p (Suc ?n) = step (steps ?c ?p ?n) ?p

goal (1 subgoal):
 1. inv_tm_onestroke (steps0 cf tm_onestroke (Suc stp))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (steps0 cf tm_onestroke (Suc stp))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tm_onestroke_partial_correctness:
  assumes "\<exists>stp. is_final (steps0 (1, [], <nl:: nat list>) tm_onestroke stp)"
  shows "\<lbrace> \<lambda>tap. tap = ([], <nl:: nat list>) \<rbrace>
           tm_onestroke
         \<lbrace> \<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc]  @ Bk \<up>l) \<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([], <nl>)\<rbrace> tm_onestroke \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
proof (rule Hoare_consequence)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lambda>tap. tap = ([], <nl>) \<mapsto> ?P
 2. \<lbrace>?P\<rbrace> tm_onestroke \<lbrace>?Q\<rbrace>
 3. ?Q \<mapsto> \<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)
[PROOF STEP]
show "(\<lambda>tap. tap = ([], <nl>)) \<mapsto> (\<lambda>tap. tap = ([], <nl>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lambda>tap. tap = ([], <nl>) \<mapsto> \<lambda>tap. tap = ([], <nl>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lambda>tap. tap = ([], <nl>) \<mapsto> \<lambda>tap. tap = ([], <nl>)

goal (2 subgoals):
 1. \<lbrace>\<lambda>tap. tap = ([], <nl>)\<rbrace> tm_onestroke \<lbrace>?Q\<rbrace>
 2. ?Q \<mapsto> \<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrace>\<lambda>tap. tap = ([], <nl>)\<rbrace> tm_onestroke \<lbrace>?Q\<rbrace>
 2. ?Q \<mapsto> \<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)
[PROOF STEP]
show "inv_tm_onestroke0 \<mapsto> (\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc]  @ Bk \<up>l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_tm_onestroke0 \<mapsto> \<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)
[PROOF STEP]
using assert_imp_def
[PROOF STATE]
proof (prove)
using this:
?P \<mapsto> ?Q \<equiv> \<forall>l r. ?P (l, r) \<longrightarrow> ?Q (l, r)

goal (1 subgoal):
 1. inv_tm_onestroke0 \<mapsto> \<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke0 \<mapsto> \<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)

goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([], <nl>)\<rbrace> tm_onestroke \<lbrace>inv_tm_onestroke0\<rbrace>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([], <nl>)\<rbrace> tm_onestroke \<lbrace>inv_tm_onestroke0\<rbrace>
[PROOF STEP]
show "\<lbrace> \<lambda>tap. tap = ([], <nl:: nat list>) \<rbrace> tm_onestroke \<lbrace> inv_tm_onestroke0 \<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([], <nl>)\<rbrace> tm_onestroke \<lbrace>inv_tm_onestroke0\<rbrace>
[PROOF STEP]
proof (rule Hoare_haltI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l r. (l, r) = ([], <nl>) \<Longrightarrow> \<exists>n. is_final (steps0 (1, l, r) tm_onestroke n) \<and> inv_tm_onestroke0 holds_for steps0 (1, l, r) tm_onestroke n
[PROOF STEP]
fix l::"cell list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l r. (l, r) = ([], <nl>) \<Longrightarrow> \<exists>n. is_final (steps0 (1, l, r) tm_onestroke n) \<and> inv_tm_onestroke0 holds_for steps0 (1, l, r) tm_onestroke n
[PROOF STEP]
fix r:: "cell list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l r. (l, r) = ([], <nl>) \<Longrightarrow> \<exists>n. is_final (steps0 (1, l, r) tm_onestroke n) \<and> inv_tm_onestroke0 holds_for steps0 (1, l, r) tm_onestroke n
[PROOF STEP]
assume "(l, r) = ([], <nl:: nat list>)"
[PROOF STATE]
proof (state)
this:
(l, r) = ([], <nl>)

goal (1 subgoal):
 1. \<And>l r. (l, r) = ([], <nl>) \<Longrightarrow> \<exists>n. is_final (steps0 (1, l, r) tm_onestroke n) \<and> inv_tm_onestroke0 holds_for steps0 (1, l, r) tm_onestroke n
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
\<exists>stp. is_final (steps0 (1, [], <nl>) tm_onestroke stp)
(l, r) = ([], <nl>)
[PROOF STEP]
have "\<exists>n. is_final (steps0 (1, l, r) tm_onestroke n)"
[PROOF STATE]
proof (prove)
using this:
\<exists>stp. is_final (steps0 (1, [], <nl>) tm_onestroke stp)
(l, r) = ([], <nl>)

goal (1 subgoal):
 1. \<exists>n. is_final (steps0 (1, l, r) tm_onestroke n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>n. is_final (steps0 (1, l, r) tm_onestroke n)

goal (1 subgoal):
 1. \<And>l r. (l, r) = ([], <nl>) \<Longrightarrow> \<exists>n. is_final (steps0 (1, l, r) tm_onestroke n) \<and> inv_tm_onestroke0 holds_for steps0 (1, l, r) tm_onestroke n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. is_final (steps0 (1, l, r) tm_onestroke n)
[PROOF STEP]
obtain stp where w_n: "is_final (steps0 (1, l, r) tm_onestroke stp)"
[PROOF STATE]
proof (prove)
using this:
\<exists>n. is_final (steps0 (1, l, r) tm_onestroke n)

goal (1 subgoal):
 1. (\<And>stp. is_final (steps0 (1, l, r) tm_onestroke stp) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_final (steps0 (1, l, r) tm_onestroke stp)

goal (1 subgoal):
 1. \<And>l r. (l, r) = ([], <nl>) \<Longrightarrow> \<exists>n. is_final (steps0 (1, l, r) tm_onestroke n) \<and> inv_tm_onestroke0 holds_for steps0 (1, l, r) tm_onestroke n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_final (steps0 (1, l, r) tm_onestroke stp)

goal (1 subgoal):
 1. \<And>l r. (l, r) = ([], <nl>) \<Longrightarrow> \<exists>n. is_final (steps0 (1, l, r) tm_onestroke n) \<and> inv_tm_onestroke0 holds_for steps0 (1, l, r) tm_onestroke n
[PROOF STEP]
have "inv_tm_onestroke0 holds_for steps0 (1, l, r) tm_onestroke stp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_tm_onestroke0 holds_for steps0 (1, l, r) tm_onestroke stp
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inv_tm_onestroke0 holds_for steps0 (1, l, r) tm_onestroke stp
[PROOF STEP]
have h: "inv_tm_onestroke (steps0 (1, [], <nl:: nat list>) tm_onestroke stp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_tm_onestroke (steps0 (1, [], <nl>) tm_onestroke stp)
[PROOF STEP]
by  (rule inv_tm_onestroke_steps)(auto simp add: noDblBk_tape_of_nat_list)
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (steps0 (1, [], <nl>) tm_onestroke stp)

goal (1 subgoal):
 1. inv_tm_onestroke0 holds_for steps0 (1, l, r) tm_onestroke stp
[PROOF STEP]
with  \<open>(l, r) = ([], <nl:: nat list>)\<close>
[PROOF STATE]
proof (chain)
picking this:
(l, r) = ([], <nl>)
inv_tm_onestroke (steps0 (1, [], <nl>) tm_onestroke stp)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(l, r) = ([], <nl>)
inv_tm_onestroke (steps0 (1, [], <nl>) tm_onestroke stp)

goal (1 subgoal):
 1. inv_tm_onestroke0 holds_for steps0 (1, l, r) tm_onestroke stp
[PROOF STEP]
by (metis Pair_inject holds_for.elims(3) inv_tm_onestroke.elims(2) is_final_eq w_n)
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke0 holds_for steps0 (1, l, r) tm_onestroke stp

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke0 holds_for steps0 (1, l, r) tm_onestroke stp

goal (1 subgoal):
 1. \<And>l r. (l, r) = ([], <nl>) \<Longrightarrow> \<exists>n. is_final (steps0 (1, l, r) tm_onestroke n) \<and> inv_tm_onestroke0 holds_for steps0 (1, l, r) tm_onestroke n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_final (steps0 (1, l, r) tm_onestroke stp)
inv_tm_onestroke0 holds_for steps0 (1, l, r) tm_onestroke stp
[PROOF STEP]
show "\<exists>n. is_final (steps0 (1, l, r) tm_onestroke n) \<and>
              inv_tm_onestroke0 holds_for steps0 (1, l, r) tm_onestroke n"
[PROOF STATE]
proof (prove)
using this:
is_final (steps0 (1, l, r) tm_onestroke stp)
inv_tm_onestroke0 holds_for steps0 (1, l, r) tm_onestroke stp

goal (1 subgoal):
 1. \<exists>n. is_final (steps0 (1, l, r) tm_onestroke n) \<and> inv_tm_onestroke0 holds_for steps0 (1, l, r) tm_onestroke n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>n. is_final (steps0 (1, l, r) tm_onestroke n) \<and> inv_tm_onestroke0 holds_for steps0 (1, l, r) tm_onestroke n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrace>\<lambda>tap. tap = ([], <nl>)\<rbrace> tm_onestroke \<lbrace>inv_tm_onestroke0\<rbrace>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wf_measure_tm_onestroke: "wf measure_tm_onestroke"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf measure_tm_onestroke
[PROOF STEP]
unfolding measure_tm_onestroke_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (measures [\<lambda>(s, l, r). if s = 0 then 0 else 1, \<lambda>(s, l, y). length y, \<lambda>(s, l, r). count_list r Oc, \<lambda>(s, l, r). if s = 3 then 0 else 1])
[PROOF STEP]
by (auto)


[STATEMENT]
lemma measure_tm_onestroke_induct [case_names Step]:
  "\<lbrakk>\<And>n. \<not> P (f n) \<Longrightarrow> (f (Suc n), (f n)) \<in> measure_tm_onestroke\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. \<not> P (f n) \<Longrightarrow> (f (Suc n), f n) \<in> measure_tm_onestroke) \<Longrightarrow> \<exists>n. P (f n)
[PROOF STEP]
using wf_measure_tm_onestroke
[PROOF STATE]
proof (prove)
using this:
wf measure_tm_onestroke

goal (1 subgoal):
 1. (\<And>n. \<not> P (f n) \<Longrightarrow> (f (Suc n), f n) \<in> measure_tm_onestroke) \<Longrightarrow> \<exists>n. P (f n)
[PROOF STEP]
by (metis wf_iff_no_infinite_down_chain)