[STATEMENT]
lemma phiDefNodes_aux_unvisited_monotonic:
    assumes "set un \<subseteq> set un'"
    shows "phiDefNodes_aux g v un n \<subseteq> phiDefNodes_aux g v un' n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. phiDefNodes_aux g v un n \<subseteq> phiDefNodes_aux g v un' n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set un \<subseteq> set un'

goal (1 subgoal):
 1. phiDefNodes_aux g v un n \<subseteq> phiDefNodes_aux g v un' n
[PROOF STEP]
proof (induction un arbitrary: un' n rule:removeAll_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs un' n. \<lbrakk>\<And>x un' n. \<lbrakk>x \<in> set xs; set (removeAll x xs) \<subseteq> set un'\<rbrakk> \<Longrightarrow> phiDefNodes_aux g v (removeAll x xs) n \<subseteq> phiDefNodes_aux g v un' n; set xs \<subseteq> set un'\<rbrakk> \<Longrightarrow> phiDefNodes_aux g v xs n \<subseteq> phiDefNodes_aux g v un' n
[PROOF STEP]
case (1 un)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2 \<in> set un; set (removeAll ?x2 un) \<subseteq> set ?un'2\<rbrakk> \<Longrightarrow> phiDefNodes_aux g v (removeAll ?x2 un) ?n2 \<subseteq> phiDefNodes_aux g v ?un'2 ?n2
set un \<subseteq> set un'

goal (1 subgoal):
 1. \<And>xs un' n. \<lbrakk>\<And>x un' n. \<lbrakk>x \<in> set xs; set (removeAll x xs) \<subseteq> set un'\<rbrakk> \<Longrightarrow> phiDefNodes_aux g v (removeAll x xs) n \<subseteq> phiDefNodes_aux g v un' n; set xs \<subseteq> set un'\<rbrakk> \<Longrightarrow> phiDefNodes_aux g v xs n \<subseteq> phiDefNodes_aux g v un' n
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2 \<in> set un; set (removeAll ?x2 un) \<subseteq> set ?un'2\<rbrakk> \<Longrightarrow> phiDefNodes_aux g v (removeAll ?x2 un) ?n2 \<subseteq> phiDefNodes_aux g v ?un'2 ?n2
set un \<subseteq> set un'

goal (1 subgoal):
 1. \<And>xs un' n. \<lbrakk>\<And>x un' n. \<lbrakk>x \<in> set xs; set (removeAll x xs) \<subseteq> set un'\<rbrakk> \<Longrightarrow> phiDefNodes_aux g v (removeAll x xs) n \<subseteq> phiDefNodes_aux g v un' n; set xs \<subseteq> set un'\<rbrakk> \<Longrightarrow> phiDefNodes_aux g v xs n \<subseteq> phiDefNodes_aux g v un' n
[PROOF STEP]
fix m A
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs un' n. \<lbrakk>\<And>x un' n. \<lbrakk>x \<in> set xs; set (removeAll x xs) \<subseteq> set un'\<rbrakk> \<Longrightarrow> phiDefNodes_aux g v (removeAll x xs) n \<subseteq> phiDefNodes_aux g v un' n; set xs \<subseteq> set un'\<rbrakk> \<Longrightarrow> phiDefNodes_aux g v xs n \<subseteq> phiDefNodes_aux g v un' n
[PROOF STEP]
assume "n \<in> set un"
[PROOF STATE]
proof (state)
this:
n \<in> set un

goal (1 subgoal):
 1. \<And>xs un' n. \<lbrakk>\<And>x un' n. \<lbrakk>x \<in> set xs; set (removeAll x xs) \<subseteq> set un'\<rbrakk> \<Longrightarrow> phiDefNodes_aux g v (removeAll x xs) n \<subseteq> phiDefNodes_aux g v un' n; set xs \<subseteq> set un'\<rbrakk> \<Longrightarrow> phiDefNodes_aux g v xs n \<subseteq> phiDefNodes_aux g v un' n
[PROOF STEP]
hence a: "\<And>m. phiDefNodes_aux g v (removeAll n un) m \<subseteq> phiDefNodes_aux g v (removeAll n un') m"
[PROOF STATE]
proof (prove)
using this:
n \<in> set un

goal (1 subgoal):
 1. \<And>m. phiDefNodes_aux g v (removeAll n un) m \<subseteq> phiDefNodes_aux g v (removeAll n un') m
[PROOF STEP]
apply (rule 1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m. set (removeAll n un) \<subseteq> set (removeAll n un')
[PROOF STEP]
using 1(2)
[PROOF STATE]
proof (prove)
using this:
set un \<subseteq> set un'

goal (1 subgoal):
 1. \<And>m. set (removeAll n un) \<subseteq> set (removeAll n un')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
phiDefNodes_aux g v (removeAll n un) ?m2 \<subseteq> phiDefNodes_aux g v (removeAll n un') ?m2

goal (1 subgoal):
 1. \<And>xs un' n. \<lbrakk>\<And>x un' n. \<lbrakk>x \<in> set xs; set (removeAll x xs) \<subseteq> set un'\<rbrakk> \<Longrightarrow> phiDefNodes_aux g v (removeAll x xs) n \<subseteq> phiDefNodes_aux g v un' n; set xs \<subseteq> set un'\<rbrakk> \<Longrightarrow> phiDefNodes_aux g v xs n \<subseteq> phiDefNodes_aux g v un' n
[PROOF STEP]
assume "m \<in> fold (\<union>) (map (phiDefNodes_aux g v (removeAll n un)) (predecessors g n)) A"
[PROOF STATE]
proof (state)
this:
m \<in> fold (\<union>) (map (phiDefNodes_aux g v (removeAll n un)) (predecessors g n)) A

goal (1 subgoal):
 1. \<And>xs un' n. \<lbrakk>\<And>x un' n. \<lbrakk>x \<in> set xs; set (removeAll x xs) \<subseteq> set un'\<rbrakk> \<Longrightarrow> phiDefNodes_aux g v (removeAll x xs) n \<subseteq> phiDefNodes_aux g v un' n; set xs \<subseteq> set un'\<rbrakk> \<Longrightarrow> phiDefNodes_aux g v xs n \<subseteq> phiDefNodes_aux g v un' n
[PROOF STEP]
hence "m \<in> fold (\<union>) (map (phiDefNodes_aux g v (removeAll n un')) (predecessors g n)) A"
[PROOF STATE]
proof (prove)
using this:
m \<in> fold (\<union>) (map (phiDefNodes_aux g v (removeAll n un)) (predecessors g n)) A

goal (1 subgoal):
 1. m \<in> fold (\<union>) (map (phiDefNodes_aux g v (removeAll n un')) (predecessors g n)) A
[PROOF STEP]
apply (rule fold_union_elem)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ys. \<lbrakk>m \<in> ys; ys \<in> set (map (phiDefNodes_aux g v (removeAll n un)) (predecessors g n)) \<union> {A}\<rbrakk> \<Longrightarrow> m \<in> fold (\<union>) (map (phiDefNodes_aux g v (removeAll n un')) (predecessors g n)) A
[PROOF STEP]
apply (rule fold_union_elemI')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ys. \<lbrakk>m \<in> ys; ys \<in> set (map (phiDefNodes_aux g v (removeAll n un)) (predecessors g n)) \<union> {A}\<rbrakk> \<Longrightarrow> m \<in> A \<or> (\<exists>xs\<in>set (map (phiDefNodes_aux g v (removeAll n un')) (predecessors g n)). m \<in> xs)
[PROOF STEP]
apply (auto simp: image_def dest: a[THEN subsetD])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
m \<in> fold (\<union>) (map (phiDefNodes_aux g v (removeAll n un')) (predecessors g n)) A

goal (1 subgoal):
 1. \<And>xs un' n. \<lbrakk>\<And>x un' n. \<lbrakk>x \<in> set xs; set (removeAll x xs) \<subseteq> set un'\<rbrakk> \<Longrightarrow> phiDefNodes_aux g v (removeAll x xs) n \<subseteq> phiDefNodes_aux g v un' n; set xs \<subseteq> set un'\<rbrakk> \<Longrightarrow> phiDefNodes_aux g v xs n \<subseteq> phiDefNodes_aux g v un' n
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>n \<in> set un; ?m4 \<in> fold (\<union>) (map (phiDefNodes_aux g v (removeAll n un)) (predecessors g n)) ?A4\<rbrakk> \<Longrightarrow> ?m4 \<in> fold (\<union>) (map (phiDefNodes_aux g v (removeAll n un')) (predecessors g n)) ?A4

goal (1 subgoal):
 1. \<And>xs un' n. \<lbrakk>\<And>x un' n. \<lbrakk>x \<in> set xs; set (removeAll x xs) \<subseteq> set un'\<rbrakk> \<Longrightarrow> phiDefNodes_aux g v (removeAll x xs) n \<subseteq> phiDefNodes_aux g v un' n; set xs \<subseteq> set un'\<rbrakk> \<Longrightarrow> phiDefNodes_aux g v xs n \<subseteq> phiDefNodes_aux g v un' n
[PROOF STEP]
with 1(2)
[PROOF STATE]
proof (chain)
picking this:
set un \<subseteq> set un'
\<lbrakk>n \<in> set un; ?m4 \<in> fold (\<union>) (map (phiDefNodes_aux g v (removeAll n un)) (predecessors g n)) ?A4\<rbrakk> \<Longrightarrow> ?m4 \<in> fold (\<union>) (map (phiDefNodes_aux g v (removeAll n un')) (predecessors g n)) ?A4
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set un \<subseteq> set un'
\<lbrakk>n \<in> set un; ?m4 \<in> fold (\<union>) (map (phiDefNodes_aux g v (removeAll n un)) (predecessors g n)) ?A4\<rbrakk> \<Longrightarrow> ?m4 \<in> fold (\<union>) (map (phiDefNodes_aux g v (removeAll n un')) (predecessors g n)) ?A4

goal (1 subgoal):
 1. phiDefNodes_aux g v un n \<subseteq> phiDefNodes_aux g v un' n
[PROOF STEP]
apply (subst(1 2) phiDefNodes_aux.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set un \<subseteq> set un'; \<And>m A. \<lbrakk>n \<in> set un; m \<in> fold (\<union>) (map (phiDefNodes_aux g v (removeAll n un)) (predecessors g n)) A\<rbrakk> \<Longrightarrow> m \<in> fold (\<union>) (map (phiDefNodes_aux g v (removeAll n un')) (predecessors g n)) A\<rbrakk> \<Longrightarrow> (if n \<notin> set un \<or> v \<in> defs g n then {} else fold (\<union>) (map (phiDefNodes_aux g v (removeAll n un)) (predecessors g n)) (if length (predecessors g n) \<noteq> 1 then {n} else {})) \<subseteq> (if n \<notin> set un' \<or> v \<in> defs g n then {} else fold (\<union>) (map (phiDefNodes_aux g v (removeAll n un')) (predecessors g n)) (if length (predecessors g n) \<noteq> 1 then {n} else {}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
phiDefNodes_aux g v un n \<subseteq> phiDefNodes_aux g v un' n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma phiDefNodes_aux_single_pred:
    assumes "predecessors g n = [m]"
    shows "phiDefNodes_aux g v (removeAll n un) m = phiDefNodes_aux g v un m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. phiDefNodes_aux g v (removeAll n un) m = phiDefNodes_aux g v un m
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. phiDefNodes_aux g v (removeAll n un) m = phiDefNodes_aux g v un m
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. phiDefNodes_aux g v (removeAll n un) m = phiDefNodes_aux g v un m
[PROOF STEP]
fix n' ns
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. phiDefNodes_aux g v (removeAll n un) m = phiDefNodes_aux g v un m
[PROOF STEP]
assume asm: "g \<turnstile> n'-ns\<rightarrow>m" "distinct ns" "length (predecessors g n') \<noteq> 1" "n \<in> set ns"
[PROOF STATE]
proof (state)
this:
g \<turnstile> n'-ns\<rightarrow>m
distinct ns
length (predecessors g n') \<noteq> 1
n \<in> set ns

goal (1 subgoal):
 1. phiDefNodes_aux g v (removeAll n un) m = phiDefNodes_aux g v un m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
g \<turnstile> n'-ns\<rightarrow>m
distinct ns
length (predecessors g n') \<noteq> 1
n \<in> set ns
[PROOF STEP]
obtain ns\<^sub>1 ns\<^sub>2 where split: "g \<turnstile> n'-ns\<^sub>1\<rightarrow>n" "g \<turnstile> n-ns\<^sub>2\<rightarrow>m" "ns = butlast ns\<^sub>1 @ ns\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
g \<turnstile> n'-ns\<rightarrow>m
distinct ns
length (predecessors g n') \<noteq> 1
n \<in> set ns

goal (1 subgoal):
 1. (\<And>ns\<^sub>1 ns\<^sub>2. \<lbrakk>g \<turnstile> n'-ns\<^sub>1\<rightarrow>n; g \<turnstile> n-ns\<^sub>2\<rightarrow>m; ns = butlast ns\<^sub>1 @ ns\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by - (rule path2_split_ex)
[PROOF STATE]
proof (state)
this:
g \<turnstile> n'-ns\<^sub>1\<rightarrow>n
g \<turnstile> n-ns\<^sub>2\<rightarrow>m
ns = butlast ns\<^sub>1 @ ns\<^sub>2

goal (1 subgoal):
 1. phiDefNodes_aux g v (removeAll n un) m = phiDefNodes_aux g v un m
[PROOF STEP]
with \<open>distinct ns\<close>
[PROOF STATE]
proof (chain)
picking this:
distinct ns
g \<turnstile> n'-ns\<^sub>1\<rightarrow>n
g \<turnstile> n-ns\<^sub>2\<rightarrow>m
ns = butlast ns\<^sub>1 @ ns\<^sub>2
[PROOF STEP]
have "m \<notin> set (butlast ns\<^sub>1)"
[PROOF STATE]
proof (prove)
using this:
distinct ns
g \<turnstile> n'-ns\<^sub>1\<rightarrow>n
g \<turnstile> n-ns\<^sub>2\<rightarrow>m
ns = butlast ns\<^sub>1 @ ns\<^sub>2

goal (1 subgoal):
 1. m \<notin> set (butlast ns\<^sub>1)
[PROOF STEP]
by (auto dest: path2_last_in_ns)
[PROOF STATE]
proof (state)
this:
m \<notin> set (butlast ns\<^sub>1)

goal (1 subgoal):
 1. phiDefNodes_aux g v (removeAll n un) m = phiDefNodes_aux g v un m
[PROOF STEP]
from split(1,2)
[PROOF STATE]
proof (chain)
picking this:
g \<turnstile> n'-ns\<^sub>1\<rightarrow>n
g \<turnstile> n-ns\<^sub>2\<rightarrow>m
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
g \<turnstile> n'-ns\<^sub>1\<rightarrow>n
g \<turnstile> n-ns\<^sub>2\<rightarrow>m

goal (1 subgoal):
 1. False
[PROOF STEP]
apply-
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g \<turnstile> n'-ns\<^sub>1\<rightarrow>n; g \<turnstile> n-ns\<^sub>2\<rightarrow>m\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule path2_unsnoc)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>g \<turnstile> n'-ns\<^sub>1\<rightarrow>n; g \<turnstile> n-ns\<^sub>2\<rightarrow>m\<rbrakk> \<Longrightarrow> 2 \<le> length ns\<^sub>1
 2. \<lbrakk>g \<turnstile> n'-ns\<^sub>1\<rightarrow>n; g \<turnstile> n-ns\<^sub>2\<rightarrow>m; g \<turnstile> n'-butlast ns\<^sub>1\<rightarrow>last (butlast ns\<^sub>1); last (butlast ns\<^sub>1) \<in> set (predecessors g n)\<rbrakk> \<Longrightarrow> ?thesis2
 3. \<lbrakk>g \<turnstile> n'-ns\<^sub>1\<rightarrow>n; g \<turnstile> n-ns\<^sub>2\<rightarrow>m; ?thesis2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule path2_nontrivial)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. g \<turnstile> n-ns\<^sub>2\<rightarrow>m \<Longrightarrow> n' \<noteq> n
 2. \<lbrakk>g \<turnstile> n'-ns\<^sub>1\<rightarrow>n; g \<turnstile> n-ns\<^sub>2\<rightarrow>m; g \<turnstile> n'-butlast ns\<^sub>1\<rightarrow>last (butlast ns\<^sub>1); last (butlast ns\<^sub>1) \<in> set (predecessors g n)\<rbrakk> \<Longrightarrow> ?thesis2
 3. \<lbrakk>g \<turnstile> n'-ns\<^sub>1\<rightarrow>n; g \<turnstile> n-ns\<^sub>2\<rightarrow>m; ?thesis2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using assms asm(3) \<open>m \<notin> set (butlast ns\<^sub>1)\<close>
[PROOF STATE]
proof (prove)
using this:
predecessors g n = [m]
length (predecessors g n') \<noteq> 1
m \<notin> set (butlast ns\<^sub>1)

goal (3 subgoals):
 1. g \<turnstile> n-ns\<^sub>2\<rightarrow>m \<Longrightarrow> n' \<noteq> n
 2. \<lbrakk>g \<turnstile> n'-ns\<^sub>1\<rightarrow>n; g \<turnstile> n-ns\<^sub>2\<rightarrow>m; g \<turnstile> n'-butlast ns\<^sub>1\<rightarrow>last (butlast ns\<^sub>1); last (butlast ns\<^sub>1) \<in> set (predecessors g n)\<rbrakk> \<Longrightarrow> ?thesis2
 3. \<lbrakk>g \<turnstile> n'-ns\<^sub>1\<rightarrow>n; g \<turnstile> n-ns\<^sub>2\<rightarrow>m; ?thesis2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (auto dest: path2_not_Nil)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. phiDefNodes_aux g v (removeAll n un) m = phiDefNodes_aux g v un m
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>g \<turnstile> ?n'4-?ns4\<rightarrow>m; distinct ?ns4; length (predecessors g ?n'4) \<noteq> 1; n \<in> set ?ns4\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. phiDefNodes_aux g v (removeAll n un) m = phiDefNodes_aux g v un m
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
predecessors g n = [m]
\<lbrakk>g \<turnstile> ?n'4-?ns4\<rightarrow>m; distinct ?ns4; length (predecessors g ?n'4) \<noteq> 1; n \<in> set ?ns4\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
predecessors g n = [m]
\<lbrakk>g \<turnstile> ?n'4-?ns4\<rightarrow>m; distinct ?ns4; length (predecessors g ?n'4) \<noteq> 1; n \<in> set ?ns4\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. phiDefNodes_aux g v (removeAll n un) m = phiDefNodes_aux g v un m
[PROOF STEP]
apply-
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>predecessors g n = [m]; \<And>n' ns. \<lbrakk>g \<turnstile> n'-ns\<rightarrow>m; distinct ns; length (predecessors g n') \<noteq> 1; n \<in> set ns\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> phiDefNodes_aux g v (removeAll n un) m = phiDefNodes_aux g v un m
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>predecessors g n = [m]; \<And>n' ns. \<lbrakk>g \<turnstile> n'-ns\<rightarrow>m; distinct ns; length (predecessors g n') \<noteq> 1; n \<in> set ns\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> phiDefNodes_aux g v (removeAll n un) m \<subseteq> phiDefNodes_aux g v un m
 2. \<lbrakk>predecessors g n = [m]; \<And>n' ns. \<lbrakk>g \<turnstile> n'-ns\<rightarrow>m; distinct ns; length (predecessors g n') \<noteq> 1; n \<in> set ns\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> phiDefNodes_aux g v un m \<subseteq> phiDefNodes_aux g v (removeAll n un) m
[PROOF STEP]
apply (rule phiDefNodes_aux_unvisited_monotonic; auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>predecessors g n = [m]; \<And>n' ns. \<lbrakk>g \<turnstile> n'-ns\<rightarrow>m; distinct ns; length (predecessors g n') \<noteq> 1; n \<in> set ns\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> phiDefNodes_aux g v un m \<subseteq> phiDefNodes_aux g v (removeAll n un) m
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>predecessors g n = [m]; \<And>n' ns. \<lbrakk>g \<turnstile> n'-ns\<rightarrow>m; distinct ns; length (predecessors g n') \<noteq> 1; n \<in> set ns\<rbrakk> \<Longrightarrow> False; x \<in> phiDefNodes_aux g v un m\<rbrakk> \<Longrightarrow> x \<in> phiDefNodes_aux g v (removeAll n un) m
[PROOF STEP]
apply (rename_tac n')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n'. \<lbrakk>predecessors g n = [m]; \<And>n' ns. \<lbrakk>g \<turnstile> n'-ns\<rightarrow>m; distinct ns; length (predecessors g n') \<noteq> 1; n \<in> set ns\<rbrakk> \<Longrightarrow> False; n' \<in> phiDefNodes_aux g v un m\<rbrakk> \<Longrightarrow> n' \<in> phiDefNodes_aux g v (removeAll n un) m
[PROOF STEP]
apply (erule phiDefNodes_auxE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n'. \<lbrakk>predecessors g n = [m]; \<And>n' ns. \<lbrakk>g \<turnstile> n'-ns\<rightarrow>m; distinct ns; length (predecessors g n') \<noteq> 1; n \<in> set ns\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> m \<in> set (\<alpha>n g)
 2. \<And>n' ns. \<lbrakk>predecessors g n = [m]; \<And>n' ns. \<lbrakk>g \<turnstile> n'-ns\<rightarrow>m; distinct ns; length (predecessors g n') \<noteq> 1; n \<in> set ns\<rbrakk> \<Longrightarrow> False; g \<turnstile> n'-ns\<rightarrow>m; \<forall>n\<in>set ns. v \<notin> defs g n; length (predecessors g n') \<noteq> 1; unvisitedPath un ns\<rbrakk> \<Longrightarrow> n' \<in> phiDefNodes_aux g v (removeAll n un) m
[PROOF STEP]
apply (rule predecessor_is_node[where n'=n]; auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n' ns. \<lbrakk>predecessors g n = [m]; \<And>n' ns. \<lbrakk>g \<turnstile> n'-ns\<rightarrow>m; distinct ns; length (predecessors g n') \<noteq> 1; n \<in> set ns\<rbrakk> \<Longrightarrow> False; g \<turnstile> n'-ns\<rightarrow>m; \<forall>n\<in>set ns. v \<notin> defs g n; length (predecessors g n') \<noteq> 1; unvisitedPath un ns\<rbrakk> \<Longrightarrow> n' \<in> phiDefNodes_aux g v (removeAll n un) m
[PROOF STEP]
apply (rule phiDefNodes_auxI; auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
phiDefNodes_aux g v (removeAll n un) m = phiDefNodes_aux g v un m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma phis'_aux_finite:
    assumes "finite (Mapping.keys phis)"
    shows "finite (Mapping.keys (phis'_aux g v ns phis))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (Mapping.keys (phis'_aux g v ns phis))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (Mapping.keys (phis'_aux g v ns phis))
[PROOF STEP]
have a: "\<And>n. phiDefNodes_aux g v [n\<leftarrow>\<alpha>n g . (n, v) \<notin> dom (Mapping.lookup phis)] n \<subseteq> (set (\<alpha>n g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> dom (Mapping.lookup phis)) (\<alpha>n g)) n \<subseteq> set (\<alpha>n g)
[PROOF STEP]
by (rule subset_trans, rule phiDefNodes_aux_in_unvisited, auto)
[PROOF STATE]
proof (state)
this:
phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> dom (Mapping.lookup phis)) (\<alpha>n g)) ?n2 \<subseteq> set (\<alpha>n g)

goal (1 subgoal):
 1. finite (Mapping.keys (phis'_aux g v ns phis))
[PROOF STEP]
have "Mapping.keys (phis'_aux g v ns phis) \<subseteq> set (\<alpha>n g) \<times> vars g \<union> Mapping.keys phis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.keys (phis'_aux g v ns phis) \<subseteq> set (\<alpha>n g) \<times> vars g \<union> Mapping.keys phis
[PROOF STEP]
by (auto simp: phis'_aux_def keys_dom_lookup split: if_split_asm dest: subsetD[OF a])
[PROOF STATE]
proof (state)
this:
Mapping.keys (phis'_aux g v ns phis) \<subseteq> set (\<alpha>n g) \<times> vars g \<union> Mapping.keys phis

goal (1 subgoal):
 1. finite (Mapping.keys (phis'_aux g v ns phis))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Mapping.keys (phis'_aux g v ns phis) \<subseteq> set (\<alpha>n g) \<times> vars g \<union> Mapping.keys phis

goal (1 subgoal):
 1. finite (Mapping.keys (phis'_aux g v ns phis))
[PROOF STEP]
by (rule finite_subset, auto intro: assms)
[PROOF STATE]
proof (state)
this:
finite (Mapping.keys (phis'_aux g v ns phis))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma phiDefNodes_aux_redirect:
    assumes asm: "g \<turnstile> n-ns\<rightarrow>m"  "\<forall>n \<in> set ns. v \<notin> defs g n" "length (predecessors g n) \<noteq> 1" "unvisitedPath un ns"
    assumes n': "n' \<in> set ns" "n' \<in> phiDefNodes_aux g v un m'" "m' \<in> set (\<alpha>n g)"
    shows "n \<in> phiDefNodes_aux g v un m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<in> phiDefNodes_aux g v un m'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<in> phiDefNodes_aux g v un m'
[PROOF STEP]
from asm(1) n'(1)
[PROOF STATE]
proof (chain)
picking this:
g \<turnstile> n-ns\<rightarrow>m
n' \<in> set ns
[PROOF STEP]
obtain ns\<^sub>1 where ns\<^sub>1: "g \<turnstile> n-ns\<^sub>1\<rightarrow>n'" "set ns\<^sub>1 \<subseteq> set ns"
[PROOF STATE]
proof (prove)
using this:
g \<turnstile> n-ns\<rightarrow>m
n' \<in> set ns

goal (1 subgoal):
 1. (\<And>ns\<^sub>1. \<lbrakk>g \<turnstile> n-ns\<^sub>1\<rightarrow>n'; set ns\<^sub>1 \<subseteq> set ns\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule path2_split_ex, simp)
[PROOF STATE]
proof (state)
this:
g \<turnstile> n-ns\<^sub>1\<rightarrow>n'
set ns\<^sub>1 \<subseteq> set ns

goal (1 subgoal):
 1. n \<in> phiDefNodes_aux g v un m'
[PROOF STEP]
from n'(2-3)
[PROOF STATE]
proof (chain)
picking this:
n' \<in> phiDefNodes_aux g v un m'
m' \<in> set (\<alpha>n g)
[PROOF STEP]
obtain ns' where ns': "g \<turnstile> n'-ns'\<rightarrow>m'" "\<forall>n \<in> set ns'. v \<notin> defs g n" "length (predecessors g n') \<noteq> 1"
      "unvisitedPath un ns'"
[PROOF STATE]
proof (prove)
using this:
n' \<in> phiDefNodes_aux g v un m'
m' \<in> set (\<alpha>n g)

goal (1 subgoal):
 1. (\<And>ns'. \<lbrakk>g \<turnstile> n'-ns'\<rightarrow>m'; \<forall>n\<in>set ns'. v \<notin> defs g n; length (predecessors g n') \<noteq> 1; unvisitedPath un ns'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule phiDefNodes_auxE)
[PROOF STATE]
proof (state)
this:
g \<turnstile> n'-ns'\<rightarrow>m'
\<forall>n\<in>set ns'. v \<notin> defs g n
length (predecessors g n') \<noteq> 1
unvisitedPath un ns'

goal (1 subgoal):
 1. n \<in> phiDefNodes_aux g v un m'
[PROOF STEP]
from ns\<^sub>1(1) ns'(1)
[PROOF STATE]
proof (chain)
picking this:
g \<turnstile> n-ns\<^sub>1\<rightarrow>n'
g \<turnstile> n'-ns'\<rightarrow>m'
[PROOF STEP]
obtain ms where ms: "g \<turnstile> n-ms\<rightarrow>m'" "distinct ms" "set ms \<subseteq> set ns\<^sub>1 \<union> set (tl ns')"
[PROOF STATE]
proof (prove)
using this:
g \<turnstile> n-ns\<^sub>1\<rightarrow>n'
g \<turnstile> n'-ns'\<rightarrow>m'

goal (1 subgoal):
 1. (\<And>ms. \<lbrakk>g \<turnstile> n-ms\<rightarrow>m'; distinct ms; set ms \<subseteq> set ns\<^sub>1 \<union> set (tl ns')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by - (drule path2_app, auto elim: simple_path2)
[PROOF STATE]
proof (state)
this:
g \<turnstile> n-ms\<rightarrow>m'
distinct ms
set ms \<subseteq> set ns\<^sub>1 \<union> set (tl ns')

goal (1 subgoal):
 1. n \<in> phiDefNodes_aux g v un m'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<in> phiDefNodes_aux g v un m'
[PROOF STEP]
using ms(1)
[PROOF STATE]
proof (prove)
using this:
g \<turnstile> n-ms\<rightarrow>m'

goal (1 subgoal):
 1. n \<in> phiDefNodes_aux g v un m'
[PROOF STEP]
apply (rule phiDefNodes_auxI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. unvisitedPath un ms
 2. \<forall>n\<in>set ms. v \<notin> defs g n
 3. length (predecessors g n) \<noteq> 1
[PROOF STEP]
using ms asm(4) ns\<^sub>1(2) ns'(4)
[PROOF STATE]
proof (prove)
using this:
g \<turnstile> n-ms\<rightarrow>m'
distinct ms
set ms \<subseteq> set ns\<^sub>1 \<union> set (tl ns')
unvisitedPath un ns
set ns\<^sub>1 \<subseteq> set ns
unvisitedPath un ns'

goal (3 subgoals):
 1. unvisitedPath un ms
 2. \<forall>n\<in>set ms. v \<notin> defs g n
 3. length (predecessors g n) \<noteq> 1
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>g \<turnstile> n-ms\<rightarrow>m'; distinct ms; set ms \<subseteq> set ns\<^sub>1 \<union> set (tl ns'); set ns\<^sub>1 \<subseteq> set ns; x \<in> set ms; distinct ns; set ns \<subseteq> set un; distinct ns'; set ns' \<subseteq> set un\<rbrakk> \<Longrightarrow> x \<in> set un
 2. \<forall>n\<in>set ms. v \<notin> defs g n
 3. length (predecessors g n) \<noteq> 1
[PROOF STEP]
apply (rename_tac x)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>g \<turnstile> n-ms\<rightarrow>m'; distinct ms; set ms \<subseteq> set ns\<^sub>1 \<union> set (tl ns'); set ns\<^sub>1 \<subseteq> set ns; x \<in> set ms; distinct ns; set ns \<subseteq> set un; distinct ns'; set ns' \<subseteq> set un\<rbrakk> \<Longrightarrow> x \<in> set un
 2. \<forall>n\<in>set ms. v \<notin> defs g n
 3. length (predecessors g n) \<noteq> 1
[PROOF STEP]
apply (case_tac "x \<in> set ns\<^sub>1")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>g \<turnstile> n-ms\<rightarrow>m'; distinct ms; set ms \<subseteq> set ns\<^sub>1 \<union> set (tl ns'); set ns\<^sub>1 \<subseteq> set ns; x \<in> set ms; distinct ns; set ns \<subseteq> set un; distinct ns'; set ns' \<subseteq> set un; x \<in> set ns\<^sub>1\<rbrakk> \<Longrightarrow> x \<in> set un
 2. \<And>x. \<lbrakk>g \<turnstile> n-ms\<rightarrow>m'; distinct ms; set ms \<subseteq> set ns\<^sub>1 \<union> set (tl ns'); set ns\<^sub>1 \<subseteq> set ns; x \<in> set ms; distinct ns; set ns \<subseteq> set un; distinct ns'; set ns' \<subseteq> set un; x \<notin> set ns\<^sub>1\<rbrakk> \<Longrightarrow> x \<in> set un
 3. \<forall>n\<in>set ms. v \<notin> defs g n
 4. length (predecessors g n) \<noteq> 1
[PROOF STEP]
apply (drule_tac A="set ns" and c=x in subsetD; auto)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>g \<turnstile> n-ms\<rightarrow>m'; distinct ms; set ms \<subseteq> set ns\<^sub>1 \<union> set (tl ns'); set ns\<^sub>1 \<subseteq> set ns; x \<in> set ms; distinct ns; set ns \<subseteq> set un; distinct ns'; set ns' \<subseteq> set un; x \<notin> set ns\<^sub>1\<rbrakk> \<Longrightarrow> x \<in> set un
 2. \<forall>n\<in>set ms. v \<notin> defs g n
 3. length (predecessors g n) \<noteq> 1
[PROOF STEP]
apply (drule_tac A="set ns'" and c=x in subsetD; auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>n\<in>set ms. v \<notin> defs g n
 2. length (predecessors g n) \<noteq> 1
[PROOF STEP]
using asm(2-3) ns\<^sub>1(2) ns'(2) ms(3)
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<in>set ns. v \<notin> defs g n
length (predecessors g n) \<noteq> 1
set ns\<^sub>1 \<subseteq> set ns
\<forall>n\<in>set ns'. v \<notin> defs g n
set ms \<subseteq> set ns\<^sub>1 \<union> set (tl ns')

goal (2 subgoals):
 1. \<forall>n\<in>set ms. v \<notin> defs g n
 2. length (predecessors g n) \<noteq> 1
[PROOF STEP]
apply (auto dest!: bspec)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
n \<in> phiDefNodes_aux g v un m'

goal:
No subgoals!
[PROOF STEP]
qed