[STATEMENT]
lemma valid_node_in_EP_D:
  assumes vn: "JVMCFG_Interpret.valid_node (Abs_wf_jvmprog (EP, Phi_EP)) ''C'' ''M'' n"
  shows "n \<in> {
  (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter),
  (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Return),
  (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter),
  (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal),
  (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Return),
  (''C'', ''M'', None, Enter),
  (''C'', ''M'', \<lfloor>0\<rfloor>, Enter),
  (''C'', ''M'', \<lfloor>1\<rfloor>, Enter),
  (''C'', ''M'', None, Return)
  }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
using vn
[PROOF STATE]
proof (prove)
using this:
JVMCFG_Interpret.valid_node (Abs_wf_jvmprog (EP, Phi_EP)) ''C'' ''M'' n

goal (1 subgoal):
 1. n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
proof (cases rule: JVMCFG_Interpret.valid_node_cases')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>e. \<lbrakk>valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') e; sourcenode e = n\<rbrakk> \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
 2. \<And>e. \<lbrakk>valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') e; targetnode e = n\<rbrakk> \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
let ?prog = "Abs_wf_jvmprog (EP, Phi_EP)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>e. \<lbrakk>valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') e; sourcenode e = n\<rbrakk> \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
 2. \<And>e. \<lbrakk>valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') e; targetnode e = n\<rbrakk> \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
case (Source e)
[PROOF STATE]
proof (state)
this:
valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') e
sourcenode e = n

goal (2 subgoals):
 1. \<And>e. \<lbrakk>valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') e; sourcenode e = n\<rbrakk> \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
 2. \<And>e. \<lbrakk>valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') e; targetnode e = n\<rbrakk> \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') e
sourcenode e = n
[PROOF STEP]
obtain C M pc nt ek C' M' pc' nt'
    where [simp]: "e = ((C, M, pc, nt), ek, (C', M', pc', nt'))"
    and [simp]: "n = (C, M, pc, nt)"
    and edge: "(?prog, ''C'', ''M'') \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc', nt')"
[PROOF STATE]
proof (prove)
using this:
valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') e
sourcenode e = n

goal (1 subgoal):
 1. (\<And>C M pc nt ek C' M' pc' nt'. \<lbrakk>e = ((C, M, pc, nt), ek, C', M', pc', nt'); n = (C, M, pc, nt);  (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc', nt')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases e) (fastforce simp: valid_edge_def)
[PROOF STATE]
proof (state)
this:
e = ((C, M, pc, nt), ek, C', M', pc', nt')
n = (C, M, pc, nt)
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc', nt')

goal (2 subgoals):
 1. \<And>e. \<lbrakk>valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') e; sourcenode e = n\<rbrakk> \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
 2. \<And>e. \<lbrakk>valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') e; targetnode e = n\<rbrakk> \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
from edge
[PROOF STATE]
proof (chain)
picking this:
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc', nt')
[PROOF STEP]
have src_reachable: "(?prog, ''C'', ''M'') \<turnstile> \<Rightarrow>(C, M, pc, nt)"
[PROOF STATE]
proof (prove)
using this:
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc', nt')

goal (1 subgoal):
 1.  (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> \<Rightarrow>(C, M, pc, nt)
[PROOF STEP]
by -(drule sourcenode_reachable)
[PROOF STATE]
proof (state)
this:
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> \<Rightarrow>(C, M, pc, nt)

goal (2 subgoals):
 1. \<And>e. \<lbrakk>valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') e; sourcenode e = n\<rbrakk> \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
 2. \<And>e. \<lbrakk>valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') e; targetnode e = n\<rbrakk> \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
proof (cases "C = ClassMain ?prog")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. C = ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
 2. C \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
C = ClassMain (Abs_wf_jvmprog (EP, Phi_EP))

goal (2 subgoals):
 1. C = ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
 2. C \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
with src_reachable
[PROOF STATE]
proof (chain)
picking this:
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> \<Rightarrow>(C, M, pc, nt)
C = ClassMain (Abs_wf_jvmprog (EP, Phi_EP))
[PROOF STEP]
have "M = MethodMain ?prog"
[PROOF STATE]
proof (prove)
using this:
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> \<Rightarrow>(C, M, pc, nt)
C = ClassMain (Abs_wf_jvmprog (EP, Phi_EP))

goal (1 subgoal):
 1. M = MethodMain (Abs_wf_jvmprog (EP, Phi_EP))
[PROOF STEP]
by (fastforce dest: ClassMain_imp_MethodMain)
[PROOF STATE]
proof (state)
this:
M = MethodMain (Abs_wf_jvmprog (EP, Phi_EP))

goal (2 subgoals):
 1. C = ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
 2. C \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
with True edge
[PROOF STATE]
proof (chain)
picking this:
C = ClassMain (Abs_wf_jvmprog (EP, Phi_EP))
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc', nt')
M = MethodMain (Abs_wf_jvmprog (EP, Phi_EP))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C = ClassMain (Abs_wf_jvmprog (EP, Phi_EP))
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc', nt')
M = MethodMain (Abs_wf_jvmprog (EP, Phi_EP))

goal (1 subgoal):
 1. n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
by clarsimp (erule JVMCFG.cases, simp_all)
[PROOF STATE]
proof (state)
this:
n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}

goal (1 subgoal):
 1. C \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. C \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
C \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP))

goal (1 subgoal):
 1. C \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
with src_reachable
[PROOF STATE]
proof (chain)
picking this:
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> \<Rightarrow>(C, M, pc, nt)
C \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP))
[PROOF STEP]
obtain T Ts mb where "EP \<turnstile> C sees M:Ts\<rightarrow>T = mb in C"
[PROOF STATE]
proof (prove)
using this:
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> \<Rightarrow>(C, M, pc, nt)
C \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP))

goal (1 subgoal):
 1. (\<And>Ts T mb. EP \<turnstile> C sees M: Ts\<rightarrow>T = mb in C \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (fastforce dest: method_of_reachable_node_exists)
[PROOF STATE]
proof (state)
this:
EP \<turnstile> C sees M: Ts\<rightarrow>T = mb in C

goal (1 subgoal):
 1. C \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
hence [simp]: "C = ''C''"
      and [simp]: "M = ''M''"
      and [simp]: "Ts = []"
      and [simp]: "T = Void"
      and [simp]: "mb = (1, 0, [Push Unit, instr.Return], [])"
[PROOF STATE]
proof (prove)
using this:
EP \<turnstile> C sees M: Ts\<rightarrow>T = mb in C

goal (1 subgoal):
 1. (C = ''C'' &&& M = ''M'') &&& Ts = [] &&& T = Void &&& mb = (1, 0, [Push Unit, instr.Return], [])
[PROOF STEP]
by (cases mb, fastforce dest: method_in_EP_is_M)+
[PROOF STATE]
proof (state)
this:
C = ''C''
M = ''M''
Ts = []
T = Void
mb = (1, 0, [Push Unit, instr.Return], [])

goal (1 subgoal):
 1. C \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
from src_reachable False
[PROOF STATE]
proof (chain)
picking this:
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> \<Rightarrow>(C, M, pc, nt)
C \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP))
[PROOF STEP]
have "pc \<in> {None, \<lfloor>0\<rfloor>, \<lfloor>1\<rfloor>}"
[PROOF STATE]
proof (prove)
using this:
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> \<Rightarrow>(C, M, pc, nt)
C \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP))

goal (1 subgoal):
 1. pc \<in> {None, \<lfloor>0\<rfloor>, \<lfloor>1\<rfloor>}
[PROOF STEP]
by (fastforce dest: instr_of_reachable_node_typable)
[PROOF STATE]
proof (state)
this:
pc \<in> {None, \<lfloor>0\<rfloor>, \<lfloor>1\<rfloor>}

goal (1 subgoal):
 1. C \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
proof (cases pc)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pc = None \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
 2. \<And>a. pc = \<lfloor>a\<rfloor> \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
pc = None

goal (2 subgoals):
 1. pc = None \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
 2. \<And>a. pc = \<lfloor>a\<rfloor> \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
with edge False
[PROOF STATE]
proof (chain)
picking this:
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc', nt')
C \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP))
pc = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc', nt')
C \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP))
pc = None

goal (1 subgoal):
 1. n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
by clarsimp (erule JVMCFG.cases, simp_all)
[PROOF STATE]
proof (state)
this:
n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}

goal (1 subgoal):
 1. \<And>a. pc = \<lfloor>a\<rfloor> \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. pc = \<lfloor>a\<rfloor> \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
case (Some pc')
[PROOF STATE]
proof (state)
this:
pc = \<lfloor>pc'\<rfloor>

goal (1 subgoal):
 1. \<And>a. pc = \<lfloor>a\<rfloor> \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
proof (cases pc')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pc' = 0 \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
 2. \<And>nat. pc' = Suc nat \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
pc' = 0

goal (2 subgoals):
 1. pc' = 0 \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
 2. \<And>nat. pc' = Suc nat \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
with Some False edge
[PROOF STATE]
proof (chain)
picking this:
pc = \<lfloor>pc'\<rfloor>
C \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP))
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc'__, nt')
pc' = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pc = \<lfloor>pc'\<rfloor>
C \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP))
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc'__, nt')
pc' = 0

goal (1 subgoal):
 1. n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
by clarsimp (erule JVMCFG.cases, fastforce+)
[PROOF STATE]
proof (state)
this:
n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}

goal (1 subgoal):
 1. \<And>nat. pc' = Suc nat \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. pc' = Suc nat \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
pc' = Suc n

goal (1 subgoal):
 1. \<And>nat. pc' = Suc nat \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
with \<open>pc \<in> {None, \<lfloor>0\<rfloor>, \<lfloor>1\<rfloor>}\<close> Some
[PROOF STATE]
proof (chain)
picking this:
pc \<in> {None, \<lfloor>0\<rfloor>, \<lfloor>1\<rfloor>}
pc = \<lfloor>pc'\<rfloor>
pc' = Suc n
[PROOF STEP]
have "pc = \<lfloor>1\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
pc \<in> {None, \<lfloor>0\<rfloor>, \<lfloor>1\<rfloor>}
pc = \<lfloor>pc'\<rfloor>
pc' = Suc n

goal (1 subgoal):
 1. pc = \<lfloor>1\<rfloor>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pc = \<lfloor>1\<rfloor>

goal (1 subgoal):
 1. \<And>nat. pc' = Suc nat \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
with False edge
[PROOF STATE]
proof (chain)
picking this:
C \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP))
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc'__, nt')
pc = \<lfloor>1\<rfloor>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP))
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc'__, nt')
pc = \<lfloor>1\<rfloor>

goal (1 subgoal):
 1. n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
by clarsimp (erule JVMCFG.cases, fastforce+)
[PROOF STATE]
proof (state)
this:
n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}

goal (1 subgoal):
 1. \<And>e. \<lbrakk>valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') e; targetnode e = n\<rbrakk> \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e. \<lbrakk>valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') e; targetnode e = n\<rbrakk> \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
let ?prog = "Abs_wf_jvmprog (EP, Phi_EP)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e. \<lbrakk>valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') e; targetnode e = n\<rbrakk> \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
case (Target e)
[PROOF STATE]
proof (state)
this:
valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') e
targetnode e = n

goal (1 subgoal):
 1. \<And>e. \<lbrakk>valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') e; targetnode e = n\<rbrakk> \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') e
targetnode e = n
[PROOF STEP]
obtain C M pc nt ek C' M' pc' nt'
    where [simp]: "e = ((C, M, pc, nt), ek, (C', M', pc', nt'))"
    and [simp]: "n = (C', M', pc', nt')"
    and edge: "(?prog, ''C'', ''M'') \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc', nt')"
[PROOF STATE]
proof (prove)
using this:
valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') e
targetnode e = n

goal (1 subgoal):
 1. (\<And>C M pc nt ek C' M' pc' nt'. \<lbrakk>e = ((C, M, pc, nt), ek, C', M', pc', nt'); n = (C', M', pc', nt');  (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc', nt')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases e) (fastforce simp: valid_edge_def)
[PROOF STATE]
proof (state)
this:
e = ((C, M, pc, nt), ek, C', M', pc', nt')
n = (C', M', pc', nt')
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc', nt')

goal (1 subgoal):
 1. \<And>e. \<lbrakk>valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') e; targetnode e = n\<rbrakk> \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
from edge
[PROOF STATE]
proof (chain)
picking this:
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc', nt')
[PROOF STEP]
have trg_reachable: "(?prog, ''C'', ''M'') \<turnstile> \<Rightarrow>(C', M', pc', nt')"
[PROOF STATE]
proof (prove)
using this:
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc', nt')

goal (1 subgoal):
 1.  (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> \<Rightarrow>(C', M', pc', nt')
[PROOF STEP]
by -(drule targetnode_reachable)
[PROOF STATE]
proof (state)
this:
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> \<Rightarrow>(C', M', pc', nt')

goal (1 subgoal):
 1. \<And>e. \<lbrakk>valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') e; targetnode e = n\<rbrakk> \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
proof (cases "C' = ClassMain ?prog")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. C' = ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
 2. C' \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
C' = ClassMain (Abs_wf_jvmprog (EP, Phi_EP))

goal (2 subgoals):
 1. C' = ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
 2. C' \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
with trg_reachable
[PROOF STATE]
proof (chain)
picking this:
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> \<Rightarrow>(C', M', pc', nt')
C' = ClassMain (Abs_wf_jvmprog (EP, Phi_EP))
[PROOF STEP]
have "M' = MethodMain ?prog"
[PROOF STATE]
proof (prove)
using this:
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> \<Rightarrow>(C', M', pc', nt')
C' = ClassMain (Abs_wf_jvmprog (EP, Phi_EP))

goal (1 subgoal):
 1. M' = MethodMain (Abs_wf_jvmprog (EP, Phi_EP))
[PROOF STEP]
by (fastforce dest: ClassMain_imp_MethodMain)
[PROOF STATE]
proof (state)
this:
M' = MethodMain (Abs_wf_jvmprog (EP, Phi_EP))

goal (2 subgoals):
 1. C' = ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
 2. C' \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
with True edge
[PROOF STATE]
proof (chain)
picking this:
C' = ClassMain (Abs_wf_jvmprog (EP, Phi_EP))
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc', nt')
M' = MethodMain (Abs_wf_jvmprog (EP, Phi_EP))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C' = ClassMain (Abs_wf_jvmprog (EP, Phi_EP))
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc', nt')
M' = MethodMain (Abs_wf_jvmprog (EP, Phi_EP))

goal (1 subgoal):
 1. n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
by -(clarsimp, (erule JVMCFG.cases, simp_all))+
[PROOF STATE]
proof (state)
this:
n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}

goal (1 subgoal):
 1. C' \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. C' \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
C' \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP))

goal (1 subgoal):
 1. C' \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
with trg_reachable
[PROOF STATE]
proof (chain)
picking this:
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> \<Rightarrow>(C', M', pc', nt')
C' \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP))
[PROOF STEP]
obtain T Ts mb where "EP \<turnstile> C' sees M':Ts\<rightarrow>T = mb in C'"
[PROOF STATE]
proof (prove)
using this:
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> \<Rightarrow>(C', M', pc', nt')
C' \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP))

goal (1 subgoal):
 1. (\<And>Ts T mb. EP \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (fastforce dest: method_of_reachable_node_exists)
[PROOF STATE]
proof (state)
this:
EP \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'

goal (1 subgoal):
 1. C' \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
hence [simp]: "C' = ''C''"
      and [simp]: "M' = ''M''"
      and [simp]: "Ts = []"
      and [simp]: "T = Void"
      and [simp]: "mb = (1, 0, [Push Unit, instr.Return], [])"
[PROOF STATE]
proof (prove)
using this:
EP \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'

goal (1 subgoal):
 1. (C' = ''C'' &&& M' = ''M'') &&& Ts = [] &&& T = Void &&& mb = (1, 0, [Push Unit, instr.Return], [])
[PROOF STEP]
by (cases mb, fastforce dest: method_in_EP_is_M)+
[PROOF STATE]
proof (state)
this:
C' = ''C''
M' = ''M''
Ts = []
T = Void
mb = (1, 0, [Push Unit, instr.Return], [])

goal (1 subgoal):
 1. C' \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
from trg_reachable False
[PROOF STATE]
proof (chain)
picking this:
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> \<Rightarrow>(C', M', pc', nt')
C' \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP))
[PROOF STEP]
have "pc' \<in> {None, \<lfloor>0\<rfloor>, \<lfloor>1\<rfloor>}"
[PROOF STATE]
proof (prove)
using this:
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> \<Rightarrow>(C', M', pc', nt')
C' \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP))

goal (1 subgoal):
 1. pc' \<in> {None, \<lfloor>0\<rfloor>, \<lfloor>1\<rfloor>}
[PROOF STEP]
by (fastforce dest: instr_of_reachable_node_typable)
[PROOF STATE]
proof (state)
this:
pc' \<in> {None, \<lfloor>0\<rfloor>, \<lfloor>1\<rfloor>}

goal (1 subgoal):
 1. C' \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
proof (cases pc')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pc' = None \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
 2. \<And>a. pc' = \<lfloor>a\<rfloor> \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
pc' = None

goal (2 subgoals):
 1. pc' = None \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
 2. \<And>a. pc' = \<lfloor>a\<rfloor> \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
with edge False
[PROOF STATE]
proof (chain)
picking this:
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc', nt')
C' \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP))
pc' = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc', nt')
C' \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP))
pc' = None

goal (1 subgoal):
 1. n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
by clarsimp (erule JVMCFG.cases, simp_all)
[PROOF STATE]
proof (state)
this:
n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}

goal (1 subgoal):
 1. \<And>a. pc' = \<lfloor>a\<rfloor> \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. pc' = \<lfloor>a\<rfloor> \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
case (Some pc'')
[PROOF STATE]
proof (state)
this:
pc' = \<lfloor>pc''\<rfloor>

goal (1 subgoal):
 1. \<And>a. pc' = \<lfloor>a\<rfloor> \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
proof (cases pc'')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pc'' = 0 \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
 2. \<And>nat. pc'' = Suc nat \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
pc'' = 0

goal (2 subgoals):
 1. pc'' = 0 \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
 2. \<And>nat. pc'' = Suc nat \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
with Some False edge
[PROOF STATE]
proof (chain)
picking this:
pc' = \<lfloor>pc''\<rfloor>
C' \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP))
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc', nt')
pc'' = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pc' = \<lfloor>pc''\<rfloor>
C' \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP))
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc', nt')
pc'' = 0

goal (1 subgoal):
 1. n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
by -(clarsimp, (erule JVMCFG.cases, fastforce+))+
[PROOF STATE]
proof (state)
this:
n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}

goal (1 subgoal):
 1. \<And>nat. pc'' = Suc nat \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. pc'' = Suc nat \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
pc'' = Suc n

goal (1 subgoal):
 1. \<And>nat. pc'' = Suc nat \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
with \<open>pc' \<in> {None, \<lfloor>0\<rfloor>, \<lfloor>1\<rfloor>}\<close> Some
[PROOF STATE]
proof (chain)
picking this:
pc' \<in> {None, \<lfloor>0\<rfloor>, \<lfloor>1\<rfloor>}
pc' = \<lfloor>pc''\<rfloor>
pc'' = Suc n
[PROOF STEP]
have "pc' = \<lfloor>1\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
pc' \<in> {None, \<lfloor>0\<rfloor>, \<lfloor>1\<rfloor>}
pc' = \<lfloor>pc''\<rfloor>
pc'' = Suc n

goal (1 subgoal):
 1. pc' = \<lfloor>1\<rfloor>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pc' = \<lfloor>1\<rfloor>

goal (1 subgoal):
 1. \<And>nat. pc'' = Suc nat \<Longrightarrow> n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
with False edge
[PROOF STATE]
proof (chain)
picking this:
C' \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP))
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc', nt')
pc' = \<lfloor>1\<rfloor>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C' \<noteq> ClassMain (Abs_wf_jvmprog (EP, Phi_EP))
 (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc', nt')
pc' = \<lfloor>1\<rfloor>

goal (1 subgoal):
 1. n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}
[PROOF STEP]
by -(clarsimp, (erule JVMCFG.cases, fastforce+))+
[PROOF STATE]
proof (state)
this:
n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n \<in> {(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Enter), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, Normal), (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), \<lfloor>0\<rfloor>, nodeType.Return), (''C'', ''M'', None, Enter), (''C'', ''M'', \<lfloor>0\<rfloor>, Enter), (''C'', ''M'', \<lfloor>1\<rfloor>, Enter), (''C'', ''M'', None, nodeType.Return)}

goal:
No subgoals!
[PROOF STEP]
qed