[STATEMENT]
lemma foldr_aux_2:
    assumes "set ns \<subseteq> set (\<alpha>n g)" "distinct ns" "foldr (aux_2 g) ns init_state = (u',p')"
    shows "\<And>n. n \<in> set ns \<Longrightarrow> uses' g n = lookup_multimap u' n" "\<And>n. n \<notin> set ns \<Longrightarrow> Mapping.lookup u' n = None"
      "\<And>m v. (if \<exists>n \<in> set ns. m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<and> v \<in> uses g n then
        Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else
        None) = Mapping.lookup p' (m,v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. n \<in> set ns \<Longrightarrow> uses' g n = lookup_multimap u' n) &&& (\<And>n. n \<notin> set ns \<Longrightarrow> Mapping.lookup u' n = None) &&& (\<And>m v. (if \<exists>n\<in>set ns. m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<and> v \<in> uses g n then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else None) = Mapping.lookup p' (m, v))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set ns \<subseteq> set (\<alpha>n g)
distinct ns
foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')

goal (1 subgoal):
 1. (\<And>n. n \<in> set ns \<Longrightarrow> uses' g n = lookup_multimap u' n) &&& (\<And>n. n \<notin> set ns \<Longrightarrow> Mapping.lookup u' n = None) &&& (\<And>m v. (if \<exists>n\<in>set ns. m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<and> v \<in> uses g n then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else None) = Mapping.lookup p' (m, v))
[PROOF STEP]
proof (induction ns arbitrary: u' p')
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>n u' p'. \<lbrakk>n \<in> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 2. \<And>n u' p'. \<lbrakk>n \<notin> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 3. \<And>n v u' p'. \<lbrakk>set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set []. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
 4. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<in> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 5. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<notin> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 6. \<And>a ns n v u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set (a # ns). n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
[PROOF STEP]
case (Cons n ns)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?n2 \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (?u'2, ?p'2)\<rbrakk> \<Longrightarrow> uses' g ?n2 = lookup_multimap ?u'2 ?n2
\<lbrakk>?n2 \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (?u'2, ?p'2)\<rbrakk> \<Longrightarrow> Mapping.lookup ?u'2 ?n2 = None
\<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (?u'2, ?p'2)\<rbrakk> \<Longrightarrow> (if \<exists>n\<in>set ns. ?n2 \<in> phiDefNodes_aux g ?v2 (\<alpha>n g) n \<and> ?v2 \<in> uses g n then Some (map (\<lambda>m. lookupDef g m ?v2) (predecessors g ?n2)) else None) = Mapping.lookup ?p'2 (?n2, ?v2)

goal (6 subgoals):
 1. \<And>n u' p'. \<lbrakk>n \<in> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 2. \<And>n u' p'. \<lbrakk>n \<notin> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 3. \<And>n v u' p'. \<lbrakk>set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set []. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
 4. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<in> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 5. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<notin> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 6. \<And>a ns n v u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set (a # ns). n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
[PROOF STEP]
let ?u = "fst (foldr (aux_2 g) ns init_state)"
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>n u' p'. \<lbrakk>n \<in> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 2. \<And>n u' p'. \<lbrakk>n \<notin> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 3. \<And>n v u' p'. \<lbrakk>set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set []. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
 4. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<in> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 5. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<notin> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 6. \<And>a ns n v u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set (a # ns). n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
[PROOF STEP]
let ?p = "snd (foldr (aux_2 g) ns init_state)"
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>n u' p'. \<lbrakk>n \<in> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 2. \<And>n u' p'. \<lbrakk>n \<notin> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 3. \<And>n v u' p'. \<lbrakk>set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set []. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
 4. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<in> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 5. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<notin> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 6. \<And>a ns n v u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set (a # ns). n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
[PROOF STEP]
fix m u' p'
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>n u' p'. \<lbrakk>n \<in> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 2. \<And>n u' p'. \<lbrakk>n \<notin> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 3. \<And>n v u' p'. \<lbrakk>set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set []. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
 4. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<in> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 5. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<notin> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 6. \<And>a ns n v u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set (a # ns). n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
[PROOF STEP]
assume asm: "set (n#ns) \<subseteq> set (\<alpha>n g)" "distinct (n#ns)" "foldr (aux_2 g) (n#ns) init_state = (u', p')"
[PROOF STATE]
proof (state)
this:
set (n # ns) \<subseteq> set (\<alpha>n g)
distinct (n # ns)
foldr (aux_2 g) (n # ns) (Mapping.empty, Mapping.empty) = (u', p')

goal (6 subgoals):
 1. \<And>n u' p'. \<lbrakk>n \<in> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 2. \<And>n u' p'. \<lbrakk>n \<notin> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 3. \<And>n v u' p'. \<lbrakk>set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set []. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
 4. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<in> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 5. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<notin> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 6. \<And>a ns n v u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set (a # ns). n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
[PROOF STEP]
hence IH:
      "\<And>n. n \<in> set ns \<Longrightarrow> uses' g n = lookup_multimap ?u n"
      "\<And>n. n \<notin> set ns \<Longrightarrow> Mapping.lookup ?u n = None"
      "\<And>m v. (if \<exists>n \<in> set ns. m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<and> v \<in> uses g n then
        Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else
        None) = Mapping.lookup ?p (m,v)"
[PROOF STATE]
proof (prove)
using this:
set (n # ns) \<subseteq> set (\<alpha>n g)
distinct (n # ns)
foldr (aux_2 g) (n # ns) (Mapping.empty, Mapping.empty) = (u', p')

goal (1 subgoal):
 1. (\<And>n. n \<in> set ns \<Longrightarrow> uses' g n = lookup_multimap (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) n) &&& (\<And>n. n \<notin> set ns \<Longrightarrow> Mapping.lookup (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) n = None) &&& (\<And>m v. (if \<exists>n\<in>set ns. m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<and> v \<in> uses g n then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else None) = Mapping.lookup (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) (m, v))
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>na. \<lbrakk>na \<in> set ns; set (n # ns) \<subseteq> set (\<alpha>n g); distinct (n # ns); foldr (aux_2 g) (n # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g na = lookup_multimap (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) na
 2. \<And>na. \<lbrakk>na \<notin> set ns; set (n # ns) \<subseteq> set (\<alpha>n g); distinct (n # ns); foldr (aux_2 g) (n # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) na = None
 3. \<And>m v. \<lbrakk>set (n # ns) \<subseteq> set (\<alpha>n g); distinct (n # ns); foldr (aux_2 g) (n # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>n\<in>set ns. m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<and> v \<in> uses g n then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else None) = Mapping.lookup (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) (m, v)
[PROOF STEP]
apply (rule Cons.IH(1)[where p'2="?p"]; auto; fail)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>na \<notin> set ns; set (n # ns) \<subseteq> set (\<alpha>n g); distinct (n # ns); foldr (aux_2 g) (n # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) na = None
 2. \<And>m v. \<lbrakk>set (n # ns) \<subseteq> set (\<alpha>n g); distinct (n # ns); foldr (aux_2 g) (n # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>n\<in>set ns. m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<and> v \<in> uses g n then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else None) = Mapping.lookup (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) (m, v)
[PROOF STEP]
apply (rule Cons.IH(2)[where p'2="?p"]; auto; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m v. \<lbrakk>set (n # ns) \<subseteq> set (\<alpha>n g); distinct (n # ns); foldr (aux_2 g) (n # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>n\<in>set ns. m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<and> v \<in> uses g n then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else None) = Mapping.lookup (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) (m, v)
[PROOF STEP]
by (rule Cons.IH(3)[where u'2="?u"], auto)
[PROOF STATE]
proof (state)
this:
?n2 \<in> set ns \<Longrightarrow> uses' g ?n2 = lookup_multimap (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) ?n2
?n2 \<notin> set ns \<Longrightarrow> Mapping.lookup (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) ?n2 = None
(if \<exists>n\<in>set ns. ?m2 \<in> phiDefNodes_aux g ?v2 (\<alpha>n g) n \<and> ?v2 \<in> uses g n then Some (map (\<lambda>m. lookupDef g m ?v2) (predecessors g ?m2)) else None) = Mapping.lookup (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) (?m2, ?v2)

goal (6 subgoals):
 1. \<And>n u' p'. \<lbrakk>n \<in> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 2. \<And>n u' p'. \<lbrakk>n \<notin> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 3. \<And>n v u' p'. \<lbrakk>set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set []. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
 4. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<in> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 5. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<notin> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 6. \<And>a ns n v u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set (a # ns). n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
[PROOF STEP]
with this[of n] asm(2)
[PROOF STATE]
proof (chain)
picking this:
n \<in> set ns \<Longrightarrow> uses' g n = lookup_multimap (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) n
n \<notin> set ns \<Longrightarrow> Mapping.lookup (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) n = None
(if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g ?v2 (\<alpha>n g) na \<and> ?v2 \<in> uses g na then Some (map (\<lambda>m. lookupDef g m ?v2) (predecessors g n)) else None) = Mapping.lookup (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) (n, ?v2)
distinct (n # ns)
?n2 \<in> set ns \<Longrightarrow> uses' g ?n2 = lookup_multimap (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) ?n2
?n2 \<notin> set ns \<Longrightarrow> Mapping.lookup (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) ?n2 = None
(if \<exists>n\<in>set ns. ?m2 \<in> phiDefNodes_aux g ?v2 (\<alpha>n g) n \<and> ?v2 \<in> uses g n then Some (map (\<lambda>m. lookupDef g m ?v2) (predecessors g ?m2)) else None) = Mapping.lookup (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) (?m2, ?v2)
[PROOF STEP]
have a': "Mapping.lookup ?u n = None"
[PROOF STATE]
proof (prove)
using this:
n \<in> set ns \<Longrightarrow> uses' g n = lookup_multimap (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) n
n \<notin> set ns \<Longrightarrow> Mapping.lookup (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) n = None
(if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g ?v2 (\<alpha>n g) na \<and> ?v2 \<in> uses g na then Some (map (\<lambda>m. lookupDef g m ?v2) (predecessors g n)) else None) = Mapping.lookup (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) (n, ?v2)
distinct (n # ns)
?n2 \<in> set ns \<Longrightarrow> uses' g ?n2 = lookup_multimap (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) ?n2
?n2 \<notin> set ns \<Longrightarrow> Mapping.lookup (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) ?n2 = None
(if \<exists>n\<in>set ns. ?m2 \<in> phiDefNodes_aux g ?v2 (\<alpha>n g) n \<and> ?v2 \<in> uses g n then Some (map (\<lambda>m. lookupDef g m ?v2) (predecessors g ?m2)) else None) = Mapping.lookup (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) (?m2, ?v2)

goal (1 subgoal):
 1. Mapping.lookup (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) n = None
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Mapping.lookup (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) n = None

goal (6 subgoals):
 1. \<And>n u' p'. \<lbrakk>n \<in> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 2. \<And>n u' p'. \<lbrakk>n \<notin> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 3. \<And>n v u' p'. \<lbrakk>set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set []. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
 4. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<in> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 5. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<notin> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 6. \<And>a ns n v u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set (a # ns). n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Mapping.lookup (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) n = None

goal (6 subgoals):
 1. \<And>n u' p'. \<lbrakk>n \<in> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 2. \<And>n u' p'. \<lbrakk>n \<notin> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 3. \<And>n v u' p'. \<lbrakk>set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set []. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
 4. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<in> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 5. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<notin> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 6. \<And>a ns n v u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set (a # ns). n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
[PROOF STEP]
have "finite (Mapping.keys ?p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (Mapping.keys (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))))
[PROOF STEP]
by (rule finite_subset[where B="set (\<alpha>n g) \<times> vars g"]) (auto simp: keys_dom_lookup IH[symmetric] split: if_split_asm dest!: phiDefNodes_aux_in_unvisited[THEN subsetD])
[PROOF STATE]
proof (state)
this:
finite (Mapping.keys (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))))

goal (6 subgoals):
 1. \<And>n u' p'. \<lbrakk>n \<in> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 2. \<And>n u' p'. \<lbrakk>n \<notin> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 3. \<And>n v u' p'. \<lbrakk>set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set []. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
 4. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<in> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 5. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<notin> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 6. \<And>a ns n v u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set (a # ns). n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (Mapping.keys (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))))

goal (6 subgoals):
 1. \<And>n u' p'. \<lbrakk>n \<in> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 2. \<And>n u' p'. \<lbrakk>n \<notin> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 3. \<And>n v u' p'. \<lbrakk>set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set []. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
 4. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<in> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 5. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<notin> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 6. \<And>a ns n v u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set (a # ns). n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
[PROOF STEP]
have "\<And>n v. (n,v) \<in> Mapping.keys ?p \<Longrightarrow> length (predecessors g n) \<noteq> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n v. (n, v) \<in> Mapping.keys (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) \<Longrightarrow> length (predecessors g n) \<noteq> 1
[PROOF STEP]
by (auto simp: keys_dom_lookup dom_def IH[symmetric] split: if_split_asm dest!: phiDefNode_aux_is_join_node)
[PROOF STATE]
proof (state)
this:
(?n2, ?v2) \<in> Mapping.keys (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) \<Longrightarrow> length (predecessors g ?n2) \<noteq> 1

goal (6 subgoals):
 1. \<And>n u' p'. \<lbrakk>n \<in> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 2. \<And>n u' p'. \<lbrakk>n \<notin> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 3. \<And>n v u' p'. \<lbrakk>set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set []. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
 4. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<in> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 5. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<notin> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 6. \<And>a ns n v u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set (a # ns). n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(?n2, ?v2) \<in> Mapping.keys (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) \<Longrightarrow> length (predecessors g ?n2) \<noteq> 1

goal (6 subgoals):
 1. \<And>n u' p'. \<lbrakk>n \<in> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 2. \<And>n u' p'. \<lbrakk>n \<notin> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 3. \<And>n v u' p'. \<lbrakk>set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set []. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
 4. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<in> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 5. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<notin> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 6. \<And>a ns n v u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set (a # ns). n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
[PROOF STEP]
have "\<And>v. Mapping.lookup ?p (Entry g,v) \<in> {None, Some []}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. Mapping.lookup (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) (Entry g, v) \<in> {None, Some []}
[PROOF STEP]
by (auto simp: IH[symmetric])
[PROOF STATE]
proof (state)
this:
Mapping.lookup (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) (Entry g, ?v2) \<in> {None, Some []}

goal (6 subgoals):
 1. \<And>n u' p'. \<lbrakk>n \<in> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 2. \<And>n u' p'. \<lbrakk>n \<notin> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 3. \<And>n v u' p'. \<lbrakk>set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set []. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
 4. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<in> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 5. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<notin> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 6. \<And>a ns n v u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set (a # ns). n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Mapping.lookup (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) n = None
finite (Mapping.keys (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))))
(?n2, ?v2) \<in> Mapping.keys (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) \<Longrightarrow> length (predecessors g ?n2) \<noteq> 1
Mapping.lookup (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) (Entry g, ?v2) \<in> {None, Some []}
[PROOF STEP]
have aux_2: "lookupDef g n ` uses g n = lookup_multimap u' n" "\<And>m. m \<noteq> n \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup ?u m"
      "\<And>m v. (if m \<in> phiDefNodes_aux g v [n \<leftarrow> \<alpha>n g. (n,v) \<notin> Mapping.keys ?p] n \<and> v \<in> uses g n then
        Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else
        (Mapping.lookup ?p (m,v))) = Mapping.lookup p' (m,v)"
[PROOF STATE]
proof (prove)
using this:
Mapping.lookup (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) n = None
finite (Mapping.keys (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))))
(?n2, ?v2) \<in> Mapping.keys (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) \<Longrightarrow> length (predecessors g ?n2) \<noteq> 1
Mapping.lookup (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) (Entry g, ?v2) \<in> {None, Some []}

goal (1 subgoal):
 1. lookupDef g n ` uses g n = lookup_multimap u' n &&& (\<And>m. m \<noteq> n \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) m) &&& (\<And>m v. (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty)))) (\<alpha>n g)) n \<and> v \<in> uses g n then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) (m, v)) = Mapping.lookup p' (m, v))
[PROOF STEP]
apply-
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Mapping.lookup (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) n = None; finite (Mapping.keys (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty)))); \<And>n v. (n, v) \<in> Mapping.keys (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` uses g n = lookup_multimap u' n
 2. \<And>m. \<lbrakk>m \<noteq> n; Mapping.lookup (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) n = None; finite (Mapping.keys (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty)))); \<And>n v. (n, v) \<in> Mapping.keys (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) m
 3. \<And>m v. \<lbrakk>Mapping.lookup (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) n = None; finite (Mapping.keys (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty)))); \<And>n v. (n, v) \<in> Mapping.keys (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty)))) (\<alpha>n g)) n \<and> v \<in> uses g n then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) (m, v)) = Mapping.lookup p' (m, v)
[PROOF STEP]
apply (rule foldr_aux_1(1)[of "sorted_list_of_set (uses g n)" g n ?u ?p u' p', simplified]; simp add: aux_2_def[symmetric] asm(3)[simplified]; fail)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m. \<lbrakk>m \<noteq> n; Mapping.lookup (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) n = None; finite (Mapping.keys (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty)))); \<And>n v. (n, v) \<in> Mapping.keys (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) m
 2. \<And>m v. \<lbrakk>Mapping.lookup (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) n = None; finite (Mapping.keys (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty)))); \<And>n v. (n, v) \<in> Mapping.keys (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty)))) (\<alpha>n g)) n \<and> v \<in> uses g n then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) (m, v)) = Mapping.lookup p' (m, v)
[PROOF STEP]
apply (rule foldr_aux_1(2)[of "sorted_list_of_set (uses g n)" g n ?u ?p u' p', simplified]; simp add: aux_2_def[symmetric] asm(3)[simplified]; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m v. \<lbrakk>Mapping.lookup (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) n = None; finite (Mapping.keys (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty)))); \<And>n v. (n, v) \<in> Mapping.keys (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty)))) (\<alpha>n g)) n \<and> v \<in> uses g n then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) (m, v)) = Mapping.lookup p' (m, v)
[PROOF STEP]
apply (rule foldr_aux_1(3)[of "sorted_list_of_set (uses g n)" g n ?u ?p u' p', simplified]; simp add: aux_2_def[symmetric] asm(3)[simplified]; fail)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
lookupDef g n ` uses g n = lookup_multimap u' n
?m2 \<noteq> n \<Longrightarrow> Mapping.lookup u' ?m2 = Mapping.lookup (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) ?m2
(if ?m2 \<in> phiDefNodes_aux g ?v2 (filter (\<lambda>n. (n, ?v2) \<notin> Mapping.keys (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty)))) (\<alpha>n g)) n \<and> ?v2 \<in> uses g n then Some (map (\<lambda>m. lookupDef g m ?v2) (predecessors g ?m2)) else Mapping.lookup (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) (?m2, ?v2)) = Mapping.lookup p' (?m2, ?v2)

goal (6 subgoals):
 1. \<And>n u' p'. \<lbrakk>n \<in> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 2. \<And>n u' p'. \<lbrakk>n \<notin> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 3. \<And>n v u' p'. \<lbrakk>set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set []. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
 4. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<in> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 5. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<notin> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 6. \<And>a ns n v u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set (a # ns). n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
lookupDef g n ` uses g n = lookup_multimap u' n
?m2 \<noteq> n \<Longrightarrow> Mapping.lookup u' ?m2 = Mapping.lookup (fst (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) ?m2
(if ?m2 \<in> phiDefNodes_aux g ?v2 (filter (\<lambda>n. (n, ?v2) \<notin> Mapping.keys (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty)))) (\<alpha>n g)) n \<and> ?v2 \<in> uses g n then Some (map (\<lambda>m. lookupDef g m ?v2) (predecessors g ?m2)) else Mapping.lookup (snd (foldr (aux_2 g) ns (Mapping.empty, Mapping.empty))) (?m2, ?v2)) = Mapping.lookup p' (?m2, ?v2)

goal (6 subgoals):
 1. \<And>n u' p'. \<lbrakk>n \<in> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 2. \<And>n u' p'. \<lbrakk>n \<notin> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 3. \<And>n v u' p'. \<lbrakk>set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set []. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
 4. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<in> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 5. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<notin> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 6. \<And>a ns n v u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set (a # ns). n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
[PROOF STEP]
assume 1: "m \<in> set (n#ns)"
[PROOF STATE]
proof (state)
this:
m \<in> set (n # ns)

goal (6 subgoals):
 1. \<And>n u' p'. \<lbrakk>n \<in> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 2. \<And>n u' p'. \<lbrakk>n \<notin> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 3. \<And>n v u' p'. \<lbrakk>set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set []. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
 4. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<in> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 5. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<notin> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 6. \<And>a ns n v u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set (a # ns). n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
[PROOF STEP]
show "uses' g m = lookup_multimap u' m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uses' g m = lookup_multimap u' m
[PROOF STEP]
apply (cases "m = n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. m = n \<Longrightarrow> uses' g m = lookup_multimap u' m
 2. m \<noteq> n \<Longrightarrow> uses' g m = lookup_multimap u' m
[PROOF STEP]
apply (simp add: uses'_def aux_2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<noteq> n \<Longrightarrow> uses' g m = lookup_multimap u' m
[PROOF STEP]
using 1 asm(2)
[PROOF STATE]
proof (prove)
using this:
m \<in> set (n # ns)
distinct (n # ns)

goal (1 subgoal):
 1. m \<noteq> n \<Longrightarrow> uses' g m = lookup_multimap u' m
[PROOF STEP]
apply (auto simp: IH(1) lookup_multimap_def aux_2(2))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
uses' g m = lookup_multimap u' m

goal (5 subgoals):
 1. \<And>n u' p'. \<lbrakk>n \<in> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 2. \<And>n u' p'. \<lbrakk>n \<notin> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 3. \<And>n v u' p'. \<lbrakk>set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set []. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
 4. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<notin> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 5. \<And>a ns n v u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set (a # ns). n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>n u' p'. \<lbrakk>n \<in> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 2. \<And>n u' p'. \<lbrakk>n \<notin> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 3. \<And>n v u' p'. \<lbrakk>set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set []. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
 4. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<notin> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 5. \<And>a ns n v u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set (a # ns). n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
[PROOF STEP]
assume 2: "m \<notin> set (n#ns)"
[PROOF STATE]
proof (state)
this:
m \<notin> set (n # ns)

goal (5 subgoals):
 1. \<And>n u' p'. \<lbrakk>n \<in> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 2. \<And>n u' p'. \<lbrakk>n \<notin> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 3. \<And>n v u' p'. \<lbrakk>set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set []. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
 4. \<And>a ns n u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); n \<notin> set (a # ns); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 5. \<And>a ns n v u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set (a # ns). n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
[PROOF STEP]
thus "Mapping.lookup u' m = None"
[PROOF STATE]
proof (prove)
using this:
m \<notin> set (n # ns)

goal (1 subgoal):
 1. Mapping.lookup u' m = None
[PROOF STEP]
by (simp add: aux_2(2) IH(2))
[PROOF STATE]
proof (state)
this:
Mapping.lookup u' m = None

goal (4 subgoals):
 1. \<And>n u' p'. \<lbrakk>n \<in> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 2. \<And>n u' p'. \<lbrakk>n \<notin> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 3. \<And>n v u' p'. \<lbrakk>set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set []. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
 4. \<And>a ns n v u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set (a # ns). n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>n u' p'. \<lbrakk>n \<in> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 2. \<And>n u' p'. \<lbrakk>n \<notin> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 3. \<And>n v u' p'. \<lbrakk>set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set []. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
 4. \<And>a ns n v u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set (a # ns). n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>n u' p'. \<lbrakk>n \<in> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 2. \<And>n u' p'. \<lbrakk>n \<notin> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 3. \<And>n v u' p'. \<lbrakk>set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set []. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
 4. \<And>a ns n v u' p'. \<lbrakk>\<And>n u' p'. \<lbrakk>n \<in> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n; \<And>n u' p'. \<lbrakk>n \<notin> set ns; set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None; \<And>n v u' p'. \<lbrakk>set ns \<subseteq> set (\<alpha>n g); distinct ns; foldr (aux_2 g) ns (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v); set (a # ns) \<subseteq> set (\<alpha>n g); distinct (a # ns); foldr (aux_2 g) (a # ns) (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set (a # ns). n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
[PROOF STEP]
show "(if \<exists>n \<in> set (n#ns). m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<and> v \<in> uses g n then
        Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else
        None) = Mapping.lookup p' (m,v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if \<exists>n\<in>set (n # ns). m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<and> v \<in> uses g n then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else None) = Mapping.lookup p' (m, v)
[PROOF STEP]
apply (auto simp: aux_2(3)[symmetric] IH(3)[symmetric] keys_dom_lookup dom_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<in> phiDefNodes_aux g v (\<alpha>n g) n; v \<in> uses g n; \<forall>n\<in>set ns. m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<longrightarrow> v \<notin> uses g n\<rbrakk> \<Longrightarrow> m \<in> phiDefNodes_aux g v (filter (\<lambda>n. \<forall>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<longrightarrow> v \<notin> uses g na) (\<alpha>n g)) n
 2. \<lbrakk>m \<notin> phiDefNodes_aux g v (\<alpha>n g) n; \<forall>n\<in>set ns. m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<longrightarrow> v \<notin> uses g n; m \<in> phiDefNodes_aux g v (filter (\<lambda>n. \<forall>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<longrightarrow> v \<notin> uses g na) (\<alpha>n g)) n; v \<in> uses g n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule phiDefNodes_auxE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>v \<in> uses g n; \<forall>n\<in>set ns. m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<longrightarrow> v \<notin> uses g n\<rbrakk> \<Longrightarrow> n \<in> set (\<alpha>n g)
 2. \<And>ns. \<lbrakk>v \<in> uses g n; \<forall>n\<in>set ns. m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<longrightarrow> v \<notin> uses g n; g \<turnstile> m-ns\<rightarrow>n; \<forall>n\<in>set ns. v \<notin> defs g n; length (predecessors g m) \<noteq> 1; unvisitedPath (\<alpha>n g) ns\<rbrakk> \<Longrightarrow> m \<in> phiDefNodes_aux g v (filter (\<lambda>n. \<forall>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<longrightarrow> v \<notin> uses g na) (\<alpha>n g)) n
 3. \<lbrakk>m \<notin> phiDefNodes_aux g v (\<alpha>n g) n; \<forall>n\<in>set ns. m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<longrightarrow> v \<notin> uses g n; m \<in> phiDefNodes_aux g v (filter (\<lambda>n. \<forall>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<longrightarrow> v \<notin> uses g na) (\<alpha>n g)) n; v \<in> uses g n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule uses_in_\<alpha>n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ns. \<lbrakk>v \<in> uses g n; \<forall>n\<in>set ns. m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<longrightarrow> v \<notin> uses g n; g \<turnstile> m-ns\<rightarrow>n; \<forall>n\<in>set ns. v \<notin> defs g n; length (predecessors g m) \<noteq> 1; unvisitedPath (\<alpha>n g) ns\<rbrakk> \<Longrightarrow> m \<in> phiDefNodes_aux g v (filter (\<lambda>n. \<forall>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<longrightarrow> v \<notin> uses g na) (\<alpha>n g)) n
 2. \<lbrakk>m \<notin> phiDefNodes_aux g v (\<alpha>n g) n; \<forall>n\<in>set ns. m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<longrightarrow> v \<notin> uses g n; m \<in> phiDefNodes_aux g v (filter (\<lambda>n. \<forall>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<longrightarrow> v \<notin> uses g na) (\<alpha>n g)) n; v \<in> uses g n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (rule phiDefNodes_auxI)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>ns. \<lbrakk>v \<in> uses g n; \<forall>n\<in>set ns. m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<longrightarrow> v \<notin> uses g n; g \<turnstile> m-ns\<rightarrow>n; \<forall>n\<in>set ns. v \<notin> defs g n; length (predecessors g m) \<noteq> 1; unvisitedPath (\<alpha>n g) ns\<rbrakk> \<Longrightarrow> g \<turnstile> m-?ns173 ns\<rightarrow>n
 2. \<And>ns. \<lbrakk>v \<in> uses g n; \<forall>n\<in>set ns. m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<longrightarrow> v \<notin> uses g n; g \<turnstile> m-ns\<rightarrow>n; \<forall>n\<in>set ns. v \<notin> defs g n; length (predecessors g m) \<noteq> 1; unvisitedPath (\<alpha>n g) ns\<rbrakk> \<Longrightarrow> unvisitedPath (filter (\<lambda>n. \<forall>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<longrightarrow> v \<notin> uses g na) (\<alpha>n g)) (?ns173 ns)
 3. \<And>ns. \<lbrakk>v \<in> uses g n; \<forall>n\<in>set ns. m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<longrightarrow> v \<notin> uses g n; g \<turnstile> m-ns\<rightarrow>n; \<forall>n\<in>set ns. v \<notin> defs g n; length (predecessors g m) \<noteq> 1; unvisitedPath (\<alpha>n g) ns\<rbrakk> \<Longrightarrow> \<forall>n\<in>set (?ns173 ns). v \<notin> defs g n
 4. \<And>ns. \<lbrakk>v \<in> uses g n; \<forall>n\<in>set ns. m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<longrightarrow> v \<notin> uses g n; g \<turnstile> m-ns\<rightarrow>n; \<forall>n\<in>set ns. v \<notin> defs g n; length (predecessors g m) \<noteq> 1; unvisitedPath (\<alpha>n g) ns\<rbrakk> \<Longrightarrow> length (predecessors g m) \<noteq> 1
 5. \<lbrakk>m \<notin> phiDefNodes_aux g v (\<alpha>n g) n; \<forall>n\<in>set ns. m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<longrightarrow> v \<notin> uses g n; m \<in> phiDefNodes_aux g v (filter (\<lambda>n. \<forall>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<longrightarrow> v \<notin> uses g na) (\<alpha>n g)) n; v \<in> uses g n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply auto[4]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ns x na. \<lbrakk>v \<in> uses g n; \<forall>n\<in>set ns. m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<longrightarrow> v \<notin> uses g n; g \<turnstile> m-ns\<rightarrow>n; \<forall>n\<in>set ns. v \<notin> defs g n; length (predecessors g m) \<noteq> Suc 0; x \<in> set ns; distinct ns; set ns \<subseteq> set (\<alpha>n g); na \<in> set ns; x \<in> phiDefNodes_aux g v (\<alpha>n g) na; v \<in> uses g na\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>m \<notin> phiDefNodes_aux g v (\<alpha>n g) n; \<forall>n\<in>set ns. m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<longrightarrow> v \<notin> uses g n; m \<in> phiDefNodes_aux g v (filter (\<lambda>n. \<forall>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<longrightarrow> v \<notin> uses g na) (\<alpha>n g)) n; v \<in> uses g n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule phiDefNodes_aux_redirect; auto simp: uses_in_\<alpha>n; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<notin> phiDefNodes_aux g v (\<alpha>n g) n; \<forall>n\<in>set ns. m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<longrightarrow> v \<notin> uses g n; m \<in> phiDefNodes_aux g v (filter (\<lambda>n. \<forall>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<longrightarrow> v \<notin> uses g na) (\<alpha>n g)) n; v \<in> uses g n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule rev_subsetD)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<notin> phiDefNodes_aux g v (\<alpha>n g) n; \<forall>n\<in>set ns. m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<longrightarrow> v \<notin> uses g n; v \<in> uses g n\<rbrakk> \<Longrightarrow> phiDefNodes_aux g v (filter (\<lambda>n. \<forall>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<longrightarrow> v \<notin> uses g na) (\<alpha>n g)) n \<subseteq> ?B242
 2. \<lbrakk>m \<notin> phiDefNodes_aux g v (\<alpha>n g) n; \<forall>n\<in>set ns. m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<longrightarrow> v \<notin> uses g n; v \<in> uses g n; m \<in> ?B242\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (rule phiDefNodes_aux_unvisited_monotonic)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<notin> phiDefNodes_aux g v (\<alpha>n g) n; \<forall>n\<in>set ns. m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<longrightarrow> v \<notin> uses g n; v \<in> uses g n\<rbrakk> \<Longrightarrow> set (filter (\<lambda>n. \<forall>na\<in>set ns. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<longrightarrow> v \<notin> uses g na) (\<alpha>n g)) \<subseteq> set ?un'245
 2. \<lbrakk>m \<notin> phiDefNodes_aux g v (\<alpha>n g) n; \<forall>n\<in>set ns. m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<longrightarrow> v \<notin> uses g n; v \<in> uses g n; m \<in> phiDefNodes_aux g v ?un'245 n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(if \<exists>n\<in>set (n # ns). m \<in> phiDefNodes_aux g v (\<alpha>n g) n \<and> v \<in> uses g n then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else None) = Mapping.lookup p' (m, v)

goal (3 subgoals):
 1. \<And>n u' p'. \<lbrakk>n \<in> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 2. \<And>n u' p'. \<lbrakk>n \<notin> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 3. \<And>n v u' p'. \<lbrakk>set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set []. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(if \<exists>n\<in>set (n # ns). m \<in> phiDefNodes_aux g ?v4 (\<alpha>n g) n \<and> ?v4 \<in> uses g n then Some (map (\<lambda>m. lookupDef g m ?v4) (predecessors g m)) else None) = Mapping.lookup p' (m, ?v4)

goal (3 subgoals):
 1. \<And>n u' p'. \<lbrakk>n \<in> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> uses' g n = lookup_multimap u' n
 2. \<And>n u' p'. \<lbrakk>n \<notin> set []; set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> Mapping.lookup u' n = None
 3. \<And>n v u' p'. \<lbrakk>set [] \<subseteq> set (\<alpha>n g); distinct []; foldr (aux_2 g) [] (Mapping.empty, Mapping.empty) = (u', p')\<rbrakk> \<Longrightarrow> (if \<exists>na\<in>set []. n \<in> phiDefNodes_aux g v (\<alpha>n g) na \<and> v \<in> uses g na then Some (map (\<lambda>m. lookupDef g m v) (predecessors g n)) else None) = Mapping.lookup p' (n, v)
[PROOF STEP]
qed (auto simp: lookup_empty)