[STATEMENT]
lemma foldr_aux_1:
    assumes "set us \<subseteq> uses g n" "Mapping.lookup u n = None" "foldr (aux_1 g n) us (u,p) = (u',p')" (is "foldr ?f _ _ = _")
    assumes "finite (Mapping.keys p)" "\<And>n v. (n,v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1" "\<And>v. Mapping.lookup p (Entry g,v) \<in> {None, Some []}"
    shows "lookupDef g n ` set us = 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> set us 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)
goal (1 subgoal):
 1. lookupDef g n ` set us = 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 (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set us \<subseteq> uses g n
Mapping.lookup u n = None
foldr (aux_1 g n) us (u, p) = (u', p')
finite (Mapping.keys p)
(?n2, ?v2) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g ?n2) \<noteq> 1
Mapping.lookup p (Entry g, ?v2) \<in> {None, Some []}

goal (1 subgoal):
 1. lookupDef g n ` set us = 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 (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v))
[PROOF STEP]
proof (induction us arbitrary: u' p')
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set [] = lookup_multimap u' n
 2. \<And>m u' p'. \<lbrakk>m \<noteq> n; set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 3. \<And>m v u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set [] then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
 4. \<And>a us u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set (a # us) = lookup_multimap u' n
 5. \<And>a us m u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); m \<noteq> n; set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 6. \<And>a us m v u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set (a # us) then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
[PROOF STEP]
case (Cons v us)
[PROOF STATE]
proof (state)
this:
\<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (?u'2, ?p'2); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap ?u'2 n
\<lbrakk>?m2 \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (?u'2, ?p'2); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup ?u'2 ?m2 = Mapping.lookup u ?m2
\<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (?u'2, ?p'2); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if ?m2 \<in> phiDefNodes_aux g ?v2 (filter (\<lambda>n. (n, ?v2) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> ?v2 \<in> set us then Some (map (\<lambda>m. lookupDef g m ?v2) (predecessors g ?m2)) else Mapping.lookup p (?m2, ?v2)) = Mapping.lookup ?p'2 (?m2, ?v2)

goal (6 subgoals):
 1. \<And>u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set [] = lookup_multimap u' n
 2. \<And>m u' p'. \<lbrakk>m \<noteq> n; set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 3. \<And>m v u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set [] then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
 4. \<And>a us u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set (a # us) = lookup_multimap u' n
 5. \<And>a us m u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); m \<noteq> n; set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 6. \<And>a us m v u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set (a # us) then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
[PROOF STEP]
let ?u = "fst (foldr ?f us (u,p))"
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set [] = lookup_multimap u' n
 2. \<And>m u' p'. \<lbrakk>m \<noteq> n; set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 3. \<And>m v u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set [] then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
 4. \<And>a us u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set (a # us) = lookup_multimap u' n
 5. \<And>a us m u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); m \<noteq> n; set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 6. \<And>a us m v u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set (a # us) then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
[PROOF STEP]
let ?p = "snd (foldr ?f us (u,p))"
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set [] = lookup_multimap u' n
 2. \<And>m u' p'. \<lbrakk>m \<noteq> n; set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 3. \<And>m v u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set [] then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
 4. \<And>a us u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set (a # us) = lookup_multimap u' n
 5. \<And>a us m u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); m \<noteq> n; set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 6. \<And>a us m v u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set (a # us) then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set [] = lookup_multimap u' n
 2. \<And>m u' p'. \<lbrakk>m \<noteq> n; set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 3. \<And>m v u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set [] then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
 4. \<And>a us u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set (a # us) = lookup_multimap u' n
 5. \<And>a us m u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); m \<noteq> n; set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 6. \<And>a us m v u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set (a # us) then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
set (v # us) \<subseteq> uses g n
Mapping.lookup u n = None
foldr (aux_1 g n) (v # us) (u, p) = (u', p')
finite (Mapping.keys p)
(?n2, ?v2) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g ?n2) \<noteq> 1
Mapping.lookup p (Entry g, ?v2) \<in> {None, Some []}

goal (6 subgoals):
 1. \<And>u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set [] = lookup_multimap u' n
 2. \<And>m u' p'. \<lbrakk>m \<noteq> n; set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 3. \<And>m v u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set [] then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
 4. \<And>a us u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set (a # us) = lookup_multimap u' n
 5. \<And>a us m u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); m \<noteq> n; set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 6. \<And>a us m v u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set (a # us) then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
[PROOF STEP]
have "n \<in> set (\<alpha>n g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<in> set (\<alpha>n g)
[PROOF STEP]
using 1(1) uses_in_\<alpha>n
[PROOF STATE]
proof (prove)
using this:
set (v # us) \<subseteq> uses g n
?v \<in> uses ?g ?n \<Longrightarrow> ?n \<in> set (\<alpha>n ?g)

goal (1 subgoal):
 1. n \<in> set (\<alpha>n g)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n \<in> set (\<alpha>n g)

goal (6 subgoals):
 1. \<And>u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set [] = lookup_multimap u' n
 2. \<And>m u' p'. \<lbrakk>m \<noteq> n; set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 3. \<And>m v u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set [] then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
 4. \<And>a us u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set (a # us) = lookup_multimap u' n
 5. \<And>a us m u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); m \<noteq> n; set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 6. \<And>a us m v u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set (a # us) then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
[PROOF STEP]
hence "lookupDef g n v = fst (readVariableRecursive g v n ?p)"
[PROOF STATE]
proof (prove)
using this:
n \<in> set (\<alpha>n g)

goal (1 subgoal):
 1. lookupDef g n v = fst (readVariableRecursive g v n (snd (foldr (aux_1 g n) us (u, p))))
[PROOF STEP]
by (rule fst_readVariableRecursive[symmetric])
[PROOF STATE]
proof (state)
this:
lookupDef g n v = fst (readVariableRecursive g v n (snd (foldr (aux_1 g n) us (u, p))))

goal (6 subgoals):
 1. \<And>u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set [] = lookup_multimap u' n
 2. \<And>m u' p'. \<lbrakk>m \<noteq> n; set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 3. \<And>m v u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set [] then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
 4. \<And>a us u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set (a # us) = lookup_multimap u' n
 5. \<And>a us m u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); m \<noteq> n; set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 6. \<And>a us m v u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set (a # us) then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lookupDef g n v = fst (readVariableRecursive g v n (snd (foldr (aux_1 g n) us (u, p))))

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

goal (1 subgoal):
 1. lookupDef g n ` set us = lookup_multimap (fst (foldr (aux_1 g n) us (u, p))) n
[PROOF STEP]
by - (rule Cons(1)[of ?u ?p], auto)
[PROOF STATE]
proof (state)
this:
lookupDef g n ` set us = lookup_multimap (fst (foldr (aux_1 g n) us (u, p))) n

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

goal (1 subgoal):
 1. lookupDef g n ` set (v # us) = lookup_multimap u' n
[PROOF STEP]
using 1(3)
[PROOF STATE]
proof (prove)
using this:
lookupDef g n v = fst (readVariableRecursive g v n (snd (foldr (aux_1 g n) us (u, p))))
lookupDef g n ` set us = lookup_multimap (fst (foldr (aux_1 g n) us (u, p))) n
foldr (aux_1 g n) (v # us) (u, p) = (u', p')

goal (1 subgoal):
 1. lookupDef g n ` set (v # us) = lookup_multimap u' n
[PROOF STEP]
by (auto simp: aux_1_def split_def Let_def lookup_multimap_def lookup_update split: option.splits)
[PROOF STATE]
proof (state)
this:
lookupDef g n ` set (v # us) = lookup_multimap u' n

goal (5 subgoals):
 1. \<And>u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set [] = lookup_multimap u' n
 2. \<And>m u' p'. \<lbrakk>m \<noteq> n; set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 3. \<And>m v u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set [] then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
 4. \<And>a us m u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); m \<noteq> n; set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 5. \<And>a us m v u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set (a # us) then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set [] = lookup_multimap u' n
 2. \<And>m u' p'. \<lbrakk>m \<noteq> n; set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 3. \<And>m v u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set [] then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
 4. \<And>a us m u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); m \<noteq> n; set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 5. \<And>a us m v u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set (a # us) then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
m \<noteq> n
set (v # us) \<subseteq> uses g n
Mapping.lookup u n = None
foldr (aux_1 g n) (v # us) (u, p) = (u', p')
finite (Mapping.keys p)
(?n2, ?v2) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g ?n2) \<noteq> 1
Mapping.lookup p (Entry g, ?v2) \<in> {None, Some []}

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

goal (1 subgoal):
 1. Mapping.lookup (fst (foldr (aux_1 g n) us (u, p))) m = Mapping.lookup u m
[PROOF STEP]
by - (rule Cons(2)[of _ ?u ?p], auto)
[PROOF STATE]
proof (state)
this:
Mapping.lookup (fst (foldr (aux_1 g n) us (u, p))) m = Mapping.lookup u m

goal (5 subgoals):
 1. \<And>u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set [] = lookup_multimap u' n
 2. \<And>m u' p'. \<lbrakk>m \<noteq> n; set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 3. \<And>m v u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set [] then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
 4. \<And>a us m u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); m \<noteq> n; set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 5. \<And>a us m v u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set (a # us) then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
Mapping.lookup (fst (foldr (aux_1 g n) us (u, p))) m = Mapping.lookup u m

goal (1 subgoal):
 1. Mapping.lookup u' m = Mapping.lookup u m
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
Mapping.lookup (fst (foldr (aux_1 g n) us (u, p))) m = Mapping.lookup u m
m \<noteq> n
set (v # us) \<subseteq> uses g n
Mapping.lookup u n = None
foldr (aux_1 g n) (v # us) (u, p) = (u', p')
finite (Mapping.keys p)
(?n2, ?v2) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g ?n2) \<noteq> 1
Mapping.lookup p (Entry g, ?v2) \<in> {None, Some []}

goal (1 subgoal):
 1. Mapping.lookup u' m = Mapping.lookup u m
[PROOF STEP]
by (auto simp: aux_1_def split_def Let_def lookup_multimap_def lookup_update_neq split: option.splits)
[PROOF STATE]
proof (state)
this:
Mapping.lookup u' m = Mapping.lookup u m

goal (4 subgoals):
 1. \<And>u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set [] = lookup_multimap u' n
 2. \<And>m u' p'. \<lbrakk>m \<noteq> n; set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 3. \<And>m v u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set [] then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
 4. \<And>a us m v u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set (a # us) then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set [] = lookup_multimap u' n
 2. \<And>m u' p'. \<lbrakk>m \<noteq> n; set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 3. \<And>m v u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set [] then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
 4. \<And>a us m v u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set (a # us) then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
[PROOF STEP]
case (3 m v' u' p')
[PROOF STATE]
proof (state)
this:
set (v # us) \<subseteq> uses g n
Mapping.lookup u n = None
foldr (aux_1 g n) (v # us) (u, p) = (u', p')
finite (Mapping.keys p)
(?n2, ?v2) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g ?n2) \<noteq> 1
Mapping.lookup p (Entry g, ?v2) \<in> {None, Some []}

goal (4 subgoals):
 1. \<And>u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set [] = lookup_multimap u' n
 2. \<And>m u' p'. \<lbrakk>m \<noteq> n; set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 3. \<And>m v u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set [] then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
 4. \<And>a us m v u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set (a # us) then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
[PROOF STEP]
from 3(1)
[PROOF STATE]
proof (chain)
picking this:
set (v # us) \<subseteq> uses g n
[PROOF STEP]
have[simp]: "\<And>v. v \<in> set us \<Longrightarrow> v \<in> vars g"
[PROOF STATE]
proof (prove)
using this:
set (v # us) \<subseteq> uses g n

goal (1 subgoal):
 1. \<And>v. v \<in> set us \<Longrightarrow> v \<in> vars g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?v2 \<in> set us \<Longrightarrow> ?v2 \<in> vars g

goal (4 subgoals):
 1. \<And>u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set [] = lookup_multimap u' n
 2. \<And>m u' p'. \<lbrakk>m \<noteq> n; set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 3. \<And>m v u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set [] then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
 4. \<And>a us m v u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set (a # us) then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
[PROOF STEP]
from 3
[PROOF STATE]
proof (chain)
picking this:
set (v # us) \<subseteq> uses g n
Mapping.lookup u n = None
foldr (aux_1 g n) (v # us) (u, p) = (u', p')
finite (Mapping.keys p)
(?n2, ?v2) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g ?n2) \<noteq> 1
Mapping.lookup p (Entry g, ?v2) \<in> {None, Some []}
[PROOF STEP]
have IH: "\<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> set us 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:
set (v # us) \<subseteq> uses g n
Mapping.lookup u n = None
foldr (aux_1 g n) (v # us) (u, p) = (u', p')
finite (Mapping.keys p)
(?n2, ?v2) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g ?n2) \<noteq> 1
Mapping.lookup p (Entry g, ?v2) \<in> {None, Some []}

goal (1 subgoal):
 1. \<And>m v'. (if m \<in> phiDefNodes_aux g v' (filter (\<lambda>n. (n, v') \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v' \<in> set us then Some (map (\<lambda>m. lookupDef g m v') (predecessors g m)) else Mapping.lookup p (m, v')) = Mapping.lookup (snd (foldr (aux_1 g n) us (u, p))) (m, v')
[PROOF STEP]
by - (rule Cons(3)[of ?u ?p], auto)
[PROOF STATE]
proof (state)
this:
(if ?m2 \<in> phiDefNodes_aux g ?v'2 (filter (\<lambda>n. (n, ?v'2) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> ?v'2 \<in> set us then Some (map (\<lambda>m. lookupDef g m ?v'2) (predecessors g ?m2)) else Mapping.lookup p (?m2, ?v'2)) = Mapping.lookup (snd (foldr (aux_1 g n) us (u, p))) (?m2, ?v'2)

goal (4 subgoals):
 1. \<And>u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set [] = lookup_multimap u' n
 2. \<And>m u' p'. \<lbrakk>m \<noteq> n; set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 3. \<And>m v u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set [] then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
 4. \<And>a us m v u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set (a # us) then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
[PROOF STEP]
have rVV: "phis'_aux g v {n} ?p = snd (readVariableRecursive g v n ?p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. phis'_aux g v {n} (snd (foldr (aux_1 g n) us (u, p))) = snd (readVariableRecursive g v n (snd (foldr (aux_1 g n) us (u, p))))
[PROOF STEP]
apply (rule snd_readVariableRecursive(1))
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. v \<in> vars g
 2. n \<in> set (\<alpha>n g)
 3. finite (Mapping.keys (snd (foldr (aux_1 g n) us (u, p))))
 4. \<And>na. (na, v) \<in> Mapping.keys (snd (foldr (aux_1 g n) us (u, p))) \<Longrightarrow> length (predecessors g na) \<noteq> 1
 5. Mapping.lookup (snd (foldr (aux_1 g n) us (u, p))) (Entry g, v) \<in> {None, Some []}
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
set (v # us) \<subseteq> uses g n
Mapping.lookup u n = None
foldr (aux_1 g n) (v # us) (u, p) = (u', p')
finite (Mapping.keys p)
(?n2, ?v2) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g ?n2) \<noteq> 1
Mapping.lookup p (Entry g, ?v2) \<in> {None, Some []}

goal (5 subgoals):
 1. v \<in> vars g
 2. n \<in> set (\<alpha>n g)
 3. finite (Mapping.keys (snd (foldr (aux_1 g n) us (u, p))))
 4. \<And>na. (na, v) \<in> Mapping.keys (snd (foldr (aux_1 g n) us (u, p))) \<Longrightarrow> length (predecessors g na) \<noteq> 1
 5. Mapping.lookup (snd (foldr (aux_1 g n) us (u, p))) (Entry g, v) \<in> {None, Some []}
[PROOF STEP]
apply (auto simp: uses_in_\<alpha>n)[2]
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite (Mapping.keys (snd (foldr (aux_1 g n) us (u, p))))
 2. \<And>na. (na, v) \<in> Mapping.keys (snd (foldr (aux_1 g n) us (u, p))) \<Longrightarrow> length (predecessors g na) \<noteq> 1
 3. Mapping.lookup (snd (foldr (aux_1 g n) us (u, p))) (Entry g, v) \<in> {None, Some []}
[PROOF STEP]
apply (rule finite_subset[where B="set (\<alpha>n g) \<times> vars g \<union> Mapping.keys p"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. Mapping.keys (snd (foldr (aux_1 g n) us (u, p))) \<subseteq> set (\<alpha>n g) \<times> vars g \<union> Mapping.keys p
 2. finite (set (\<alpha>n g) \<times> vars g \<union> Mapping.keys p)
 3. \<And>na. (na, v) \<in> Mapping.keys (snd (foldr (aux_1 g n) us (u, p))) \<Longrightarrow> length (predecessors g na) \<noteq> 1
 4. Mapping.lookup (snd (foldr (aux_1 g n) us (u, p))) (Entry g, v) \<in> {None, Some []}
[PROOF STEP]
apply (auto simp: keys_dom_lookup IH[symmetric] split: if_split_asm dest!: phiDefNodes_aux_in_unvisited[THEN subsetD])[1]
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite (set (\<alpha>n g) \<times> vars g \<union> Mapping.keys p)
 2. \<And>na. (na, v) \<in> Mapping.keys (snd (foldr (aux_1 g n) us (u, p))) \<Longrightarrow> length (predecessors g na) \<noteq> 1
 3. Mapping.lookup (snd (foldr (aux_1 g n) us (u, p))) (Entry g, v) \<in> {None, Some []}
[PROOF STEP]
apply (simp add: 3(4))[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na. (na, v) \<in> Mapping.keys (snd (foldr (aux_1 g n) us (u, p))) \<Longrightarrow> length (predecessors g na) \<noteq> 1
 2. Mapping.lookup (snd (foldr (aux_1 g n) us (u, p))) (Entry g, v) \<in> {None, Some []}
[PROOF STEP]
using 3(5-6)
[PROOF STATE]
proof (prove)
using this:
(?n2, ?v2) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g ?n2) \<noteq> 1
Mapping.lookup p (Entry g, ?v2) \<in> {None, Some []}

goal (2 subgoals):
 1. \<And>na. (na, v) \<in> Mapping.keys (snd (foldr (aux_1 g n) us (u, p))) \<Longrightarrow> length (predecessors g na) \<noteq> 1
 2. Mapping.lookup (snd (foldr (aux_1 g n) us (u, p))) (Entry g, v) \<in> {None, Some []}
[PROOF STEP]
apply (auto simp: keys_dom_lookup dom_def IH[symmetric] split: if_split_asm dest!: phiDefNode_aux_is_join_node)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
phis'_aux g v {n} (snd (foldr (aux_1 g n) us (u, p))) = snd (readVariableRecursive g v n (snd (foldr (aux_1 g n) us (u, p))))

goal (4 subgoals):
 1. \<And>u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set [] = lookup_multimap u' n
 2. \<And>m u' p'. \<lbrakk>m \<noteq> n; set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 3. \<And>m v u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set [] then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
 4. \<And>a us m v u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set (a # us) then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
[PROOF STEP]
have a: "m \<in> phiDefNodes_aux g v [n\<leftarrow>\<alpha>n g . (n, v) \<notin> Mapping.keys ?p] n \<Longrightarrow> m \<in> phiDefNodes_aux g v [n\<leftarrow>\<alpha>n g . (n, v) \<notin> Mapping.keys p] n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<in> phiDefNodes_aux g v (filter (\<lambda>na. (na, v) \<notin> Mapping.keys (snd (foldr (aux_1 g n) us (u, p)))) (\<alpha>n g)) n \<Longrightarrow> m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n
[PROOF STEP]
apply (erule rev_subsetD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. phiDefNodes_aux g v (filter (\<lambda>na. (na, v) \<notin> Mapping.keys (snd (foldr (aux_1 g n) us (u, p)))) (\<alpha>n g)) n \<subseteq> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n
[PROOF STEP]
apply (rule phiDefNodes_aux_unvisited_monotonic)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (filter (\<lambda>na. (na, v) \<notin> Mapping.keys (snd (foldr (aux_1 g n) us (u, p)))) (\<alpha>n g)) \<subseteq> set (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g))
[PROOF STEP]
by (auto simp: IH[symmetric] keys_dom_lookup split: if_split_asm)
[PROOF STATE]
proof (state)
this:
m \<in> phiDefNodes_aux g v (filter (\<lambda>na. (na, v) \<notin> Mapping.keys (snd (foldr (aux_1 g n) us (u, p)))) (\<alpha>n g)) n \<Longrightarrow> m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n

goal (4 subgoals):
 1. \<And>u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set [] = lookup_multimap u' n
 2. \<And>m u' p'. \<lbrakk>m \<noteq> n; set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 3. \<And>m v u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set [] then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
 4. \<And>a us m v u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set (a # us) then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
[PROOF STEP]
have b: "v \<notin> set us \<Longrightarrow> [n\<leftarrow>\<alpha>n g . (n, v) \<notin> Mapping.keys ?p] = [n\<leftarrow>\<alpha>n g . (n, v) \<notin> Mapping.keys p]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<notin> set us \<Longrightarrow> filter (\<lambda>na. (na, v) \<notin> Mapping.keys (snd (foldr (aux_1 g n) us (u, p)))) (\<alpha>n g) = filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)
[PROOF STEP]
by (rule arg_cong2[where f=filter], auto simp: keys_dom_lookup IH[symmetric])
[PROOF STATE]
proof (state)
this:
v \<notin> set us \<Longrightarrow> filter (\<lambda>na. (na, v) \<notin> Mapping.keys (snd (foldr (aux_1 g n) us (u, p)))) (\<alpha>n g) = filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)

goal (4 subgoals):
 1. \<And>u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set [] = lookup_multimap u' n
 2. \<And>m u' p'. \<lbrakk>m \<noteq> n; set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 3. \<And>m v u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set [] then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
 4. \<And>a us m v u' p'. \<lbrakk>\<And>u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set us = lookup_multimap u' n; \<And>m u' p'. \<lbrakk>m \<noteq> n; set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m; \<And>m v u' p'. \<lbrakk>set us \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) us (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set us then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v); set (a # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (a # us) (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set (a # us) then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
[PROOF STEP]
from 3
[PROOF STATE]
proof (chain)
picking this:
set (v # us) \<subseteq> uses g n
Mapping.lookup u n = None
foldr (aux_1 g n) (v # us) (u, p) = (u', p')
finite (Mapping.keys p)
(?n2, ?v2) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g ?n2) \<noteq> 1
Mapping.lookup p (Entry g, ?v2) \<in> {None, Some []}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set (v # us) \<subseteq> uses g n
Mapping.lookup u n = None
foldr (aux_1 g n) (v # us) (u, p) = (u', p')
finite (Mapping.keys p)
(?n2, ?v2) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g ?n2) \<noteq> 1
Mapping.lookup p (Entry g, ?v2) \<in> {None, Some []}

goal (1 subgoal):
 1. (if m \<in> phiDefNodes_aux g v' (filter (\<lambda>n. (n, v') \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v' \<in> set (v # us) then Some (map (\<lambda>m. lookupDef g m v') (predecessors g m)) else Mapping.lookup p (m, v')) = Mapping.lookup p' (m, v')
[PROOF STEP]
unfolding aux_1_def
[PROOF STATE]
proof (prove)
using this:
set (v # us) \<subseteq> uses g n
Mapping.lookup u n = None
foldr (\<lambda>a aa. case aa of (uses, phis) \<Rightarrow> let (use, y) = readVariableRecursive g a n phis in (Mapping.update n (insert use (lookup_multimap uses n)) uses, y)) (v # us) (u, p) = (u', p')
finite (Mapping.keys p)
(?n2, ?v2) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g ?n2) \<noteq> 1
Mapping.lookup p (Entry g, ?v2) \<in> {None, Some []}

goal (1 subgoal):
 1. (if m \<in> phiDefNodes_aux g v' (filter (\<lambda>n. (n, v') \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v' \<in> set (v # us) then Some (map (\<lambda>m. lookupDef g m v') (predecessors g m)) else Mapping.lookup p (m, v')) = Mapping.lookup p' (m, v')
[PROOF STEP]
unfolding foldr.foldr_Cons
[PROOF STATE]
proof (prove)
using this:
set (v # us) \<subseteq> uses g n
Mapping.lookup u n = None
((\<lambda>(uses, phis). let (use, y) = readVariableRecursive g v n phis in (Mapping.update n (insert use (lookup_multimap uses n)) uses, y)) \<circ>\<circ>\<circ> foldr) (\<lambda>a (uses, phis). let (use, y) = readVariableRecursive g a n phis in (Mapping.update n (insert use (lookup_multimap uses n)) uses, y)) us (u, p) = (u', p')
finite (Mapping.keys p)
(?n2, ?v2) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g ?n2) \<noteq> 1
Mapping.lookup p (Entry g, ?v2) \<in> {None, Some []}

goal (1 subgoal):
 1. (if m \<in> phiDefNodes_aux g v' (filter (\<lambda>n. (n, v') \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v' \<in> set (v # us) then Some (map (\<lambda>m. lookupDef g m v') (predecessors g m)) else Mapping.lookup p (m, v')) = Mapping.lookup p' (m, v')
[PROOF STEP]
unfolding aux_1_def[symmetric]
[PROOF STATE]
proof (prove)
using this:
set (v # us) \<subseteq> uses g n
Mapping.lookup u n = None
((\<lambda>(uses, phis). let (use, y) = readVariableRecursive g v n phis in (Mapping.update n (insert use (lookup_multimap uses n)) uses, y)) \<circ>\<circ>\<circ> foldr) (aux_1 g n) us (u, p) = (u', p')
finite (Mapping.keys p)
(?n2, ?v2) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g ?n2) \<noteq> 1
Mapping.lookup p (Entry g, ?v2) \<in> {None, Some []}

goal (1 subgoal):
 1. (if m \<in> phiDefNodes_aux g v' (filter (\<lambda>n. (n, v') \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v' \<in> set (v # us) then Some (map (\<lambda>m. lookupDef g m v') (predecessors g m)) else Mapping.lookup p (m, v')) = Mapping.lookup p' (m, v')
[PROOF STEP]
by (auto simp: Let_def split_def IH[symmetric] rVV[symmetric] phis'_aux_def b dest: a uses_in_vars split: if_split_asm)
[PROOF STATE]
proof (state)
this:
(if m \<in> phiDefNodes_aux g v' (filter (\<lambda>n. (n, v') \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v' \<in> set (v # us) then Some (map (\<lambda>m. lookupDef g m v') (predecessors g m)) else Mapping.lookup p (m, v')) = Mapping.lookup p' (m, v')

goal (3 subgoals):
 1. \<And>u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set [] = lookup_multimap u' n
 2. \<And>m u' p'. \<lbrakk>m \<noteq> n; set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 3. \<And>m v u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set [] then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>set (v # us) \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) (v # us) (u, p) = (?u'a4, ?p'a4); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if ?m4 \<in> phiDefNodes_aux g ?v'4 (filter (\<lambda>n. (n, ?v'4) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> ?v'4 \<in> set (v # us) then Some (map (\<lambda>m. lookupDef g m ?v'4) (predecessors g ?m4)) else Mapping.lookup p (?m4, ?v'4)) = Mapping.lookup ?p'a4 (?m4, ?v'4)

goal (3 subgoals):
 1. \<And>u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> lookupDef g n ` set [] = lookup_multimap u' n
 2. \<And>m u' p'. \<lbrakk>m \<noteq> n; set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> Mapping.lookup u' m = Mapping.lookup u m
 3. \<And>m v u' p'. \<lbrakk>set [] \<subseteq> uses g n; Mapping.lookup u n = None; foldr (aux_1 g n) [] (u, p) = (u', p'); finite (Mapping.keys p); \<And>n v. (n, v) \<in> Mapping.keys p \<Longrightarrow> length (predecessors g n) \<noteq> 1; \<And>v. Mapping.lookup p (Entry g, v) \<in> {None, Some []}\<rbrakk> \<Longrightarrow> (if m \<in> phiDefNodes_aux g v (filter (\<lambda>n. (n, v) \<notin> Mapping.keys p) (\<alpha>n g)) n \<and> v \<in> set [] then Some (map (\<lambda>m. lookupDef g m v) (predecessors g m)) else Mapping.lookup p (m, v)) = Mapping.lookup p' (m, v)
[PROOF STEP]
qed (auto simp: lookup_multimap_def)