[STATEMENT]
lemma unwinding_implies_view_partitioned:
shows view_partitioned
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. view_partitioned
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. view_partitioned
[PROOF STEP]
from unwinding_implies_view_partitioned_ind
[PROOF STATE]
proof (chain)
picking this:
view_partitioned_ind
[PROOF STEP]
have view_partitioned_inductive: "view_partitioned_ind"
[PROOF STATE]
proof (prove)
using this:
view_partitioned_ind

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

goal (1 subgoal):
 1. view_partitioned
[PROOF STEP]
have purged_relation: "\<forall> u execs . purged_relation u execs (purge execs u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>u execs. purged_relation u execs (purge execs u)
[PROOF STEP]
by(unfold purged_relation_def, unfold purge_def, auto)
[PROOF STATE]
proof (state)
this:
\<forall>u execs. purged_relation u execs (purge execs u)

goal (1 subgoal):
 1. view_partitioned
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>u execs. purged_relation u execs (purge execs u)

goal (1 subgoal):
 1. view_partitioned
[PROOF STEP]
fix execs s t n u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. view_partitioned
[PROOF STEP]
assume 1: "equivalent_states s t u"
[PROOF STATE]
proof (state)
this:
equivalent_states s t u

goal (1 subgoal):
 1. view_partitioned
[PROOF STEP]
from this view_partitioned_inductive purged_relation
[PROOF STATE]
proof (chain)
picking this:
equivalent_states s t u
view_partitioned_ind
\<forall>u execs. purged_relation u execs (purge execs u)
[PROOF STEP]
have "equivalent_states (run n s execs) (run n t (purge execs u)) u"
[PROOF STATE]
proof (prove)
using this:
equivalent_states s t u
view_partitioned_ind
\<forall>u execs. purged_relation u execs (purge execs u)

goal (1 subgoal):
 1. equivalent_states (run n s execs) (run n t (purge execs u)) u
[PROOF STEP]
unfolding view_partitioned_ind_def
[PROOF STATE]
proof (prove)
using this:
equivalent_states s t u
\<forall>execs1 execs2 s t n u. equivalent_states s t u \<and> purged_relation u execs1 execs2 \<longrightarrow> equivalent_states (run n s execs1) (run n t execs2) u
\<forall>u execs. purged_relation u execs (purge execs u)

goal (1 subgoal):
 1. equivalent_states (run n s execs) (run n t (purge execs u)) u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
equivalent_states (run n s execs) (run n t (purge execs u)) u

goal (1 subgoal):
 1. view_partitioned
[PROOF STEP]
from this ifp_reflexive
[PROOF STATE]
proof (chain)
picking this:
equivalent_states (run n s execs) (run n t (purge execs u)) u
\<forall>u. ifp u u
[PROOF STEP]
have "run n s execs \<parallel> run n t (purge execs u) \<rightharpoonup> (\<lambda>rs rt. vpeq u rs rt \<and> current rs = current rt)"
[PROOF STATE]
proof (prove)
using this:
equivalent_states (run n s execs) (run n t (purge execs u)) u
\<forall>u. ifp u u

goal (1 subgoal):
 1. B2 (run n s execs) (run n t (purge execs u)) (\<lambda>rs rt. vpeq u rs rt \<and> current rs = current rt)
[PROOF STEP]
using r_into_rtranclp
[PROOF STATE]
proof (prove)
using this:
equivalent_states (run n s execs) (run n t (purge execs u)) u
\<forall>u. ifp u u
?r ?x ?y \<Longrightarrow> ?r\<^sup>*\<^sup>* ?x ?y

goal (1 subgoal):
 1. B2 (run n s execs) (run n t (purge execs u)) (\<lambda>rs rt. vpeq u rs rt \<and> current rs = current rt)
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
using this:
equivalent_states (run n s execs) (run n t (purge execs u)) u
\<forall>u. ifp u u
?r ?x ?y \<Longrightarrow> ?r\<^sup>*\<^sup>* ?x ?y

goal (1 subgoal):
 1. B2 (run n s execs) (run n t (purge execs u)) (\<lambda>rs rt. vpeq u rs rt \<and> current rs = current rt)
[PROOF STEP]
by(cases "run n s execs",simp,cases "run n t (purge execs u)",simp,auto)
[PROOF STATE]
proof (state)
this:
B2 (run n s execs) (run n t (purge execs u)) (\<lambda>rs rt. vpeq u rs rt \<and> current rs = current rt)

goal (1 subgoal):
 1. view_partitioned
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
equivalent_states ?s2 ?t2 ?u2 \<Longrightarrow> B2 (run ?n2 ?s2 ?execs2) (run ?n2 ?t2 (purge ?execs2 ?u2)) (\<lambda>rs rt. vpeq ?u2 rs rt \<and> current rs = current rt)

goal (1 subgoal):
 1. view_partitioned
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
equivalent_states ?s2 ?t2 ?u2 \<Longrightarrow> B2 (run ?n2 ?s2 ?execs2) (run ?n2 ?t2 (purge ?execs2 ?u2)) (\<lambda>rs rt. vpeq ?u2 rs rt \<and> current rs = current rt)

goal (1 subgoal):
 1. view_partitioned
[PROOF STEP]
unfolding view_partitioned_def Let_def
[PROOF STATE]
proof (prove)
using this:
equivalent_states ?s2 ?t2 ?u2 \<Longrightarrow> B2 (run ?n2 ?s2 ?execs2) (run ?n2 ?t2 (purge ?execs2 ?u2)) (\<lambda>rs rt. vpeq ?u2 rs rt \<and> current rs = current rt)

goal (1 subgoal):
 1. \<forall>execs ms mt n u. equivalent_states ms mt u \<longrightarrow> B2 (run n ms execs) (run n mt (purge execs u)) (\<lambda>rs rt. vpeq u rs rt \<and> current rs = current rt)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
view_partitioned

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem unwinding_implies_NI_unrelated:
shows NI_unrelated
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NI_unrelated
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. NI_unrelated
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. NI_unrelated
[PROOF STEP]
fix execs a n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. NI_unrelated
[PROOF STEP]
from unwinding_implies_view_partitioned
[PROOF STATE]
proof (chain)
picking this:
view_partitioned
[PROOF STEP]
have vp: view_partitioned
[PROOF STATE]
proof (prove)
using this:
view_partitioned

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

goal (1 subgoal):
 1. NI_unrelated
[PROOF STEP]
from vp and vpeq_reflexive
[PROOF STATE]
proof (chain)
picking this:
view_partitioned
\<forall>a u. vpeq u a a
[PROOF STEP]
have 1: "\<forall> u . (run n (Some s0) execs
                      \<parallel> run n (Some s0) (purge execs u)
                          \<rightharpoonup> (\<lambda>rs rt. vpeq u rs rt \<and> current rs = current rt))"
[PROOF STATE]
proof (prove)
using this:
view_partitioned
\<forall>a u. vpeq u a a

goal (1 subgoal):
 1. \<forall>u. B2 (run n (Some s0) execs) (run n (Some s0) (purge execs u)) (\<lambda>rs rt. vpeq u rs rt \<and> current rs = current rt)
[PROOF STEP]
unfolding view_partitioned_def
[PROOF STATE]
proof (prove)
using this:
\<forall>execs ms mt n u. equivalent_states ms mt u \<longrightarrow> B2 (run n ms execs) (run n mt (purge execs u)) (\<lambda>rs rt. vpeq u rs rt \<and> current rs = current rt)
\<forall>a u. vpeq u a a

goal (1 subgoal):
 1. \<forall>u. B2 (run n (Some s0) execs) (run n (Some s0) (purge execs u)) (\<lambda>rs rt. vpeq u rs rt \<and> current rs = current rt)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>u. B2 (run n (Some s0) execs) (run n (Some s0) (purge execs u)) (\<lambda>rs rt. vpeq u rs rt \<and> current rs = current rt)

goal (1 subgoal):
 1. NI_unrelated
[PROOF STEP]
have "run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (purge execs (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f a = output_f s_f2 a \<and> current s_f = current s_f2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (purge execs (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f a = output_f s_f2 a \<and> current s_f = current s_f2))
[PROOF STEP]
proof(cases "run n (Some s0) execs")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. run n (Some s0) execs = None \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (purge execs (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f a = output_f s_f2 a \<and> current s_f = current s_f2))
 2. \<And>aa. run n (Some s0) execs = Some aa \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (purge execs (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f a = output_f s_f2 a \<and> current s_f = current s_f2))
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
run n (Some s0) execs = None

goal (2 subgoals):
 1. run n (Some s0) execs = None \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (purge execs (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f a = output_f s_f2 a \<and> current s_f = current s_f2))
 2. \<And>aa. run n (Some s0) execs = Some aa \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (purge execs (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f a = output_f s_f2 a \<and> current s_f = current s_f2))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
run n (Some s0) execs = None

goal (1 subgoal):
 1. run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (purge execs (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f a = output_f s_f2 a \<and> current s_f = current s_f2))
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
using this:
run n (Some s0) execs = None

goal (1 subgoal):
 1. case run n (Some s0) execs of None \<Rightarrow> True | Some aa \<Rightarrow> case run n (Some s0) (purge execs (current aa)) of None \<Rightarrow> True | Some ab \<Rightarrow> output_f aa a = output_f ab a \<and> current aa = current ab
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (purge execs (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f a = output_f s_f2 a \<and> current s_f = current s_f2))

goal (1 subgoal):
 1. \<And>aa. run n (Some s0) execs = Some aa \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (purge execs (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f a = output_f s_f2 a \<and> current s_f = current s_f2))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa. run n (Some s0) execs = Some aa \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (purge execs (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f a = output_f s_f2 a \<and> current s_f = current s_f2))
[PROOF STEP]
case (Some rs)
[PROOF STATE]
proof (state)
this:
run n (Some s0) execs = Some rs

goal (1 subgoal):
 1. \<And>aa. run n (Some s0) execs = Some aa \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (purge execs (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f a = output_f s_f2 a \<and> current s_f = current s_f2))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
run n (Some s0) execs = Some rs

goal (1 subgoal):
 1. run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (purge execs (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f a = output_f s_f2 a \<and> current s_f = current s_f2))
[PROOF STEP]
proof(cases "run n (Some s0) (purge execs (current rs))")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>run n (Some s0) execs = Some rs; run n (Some s0) (purge execs (current rs)) = None\<rbrakk> \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (purge execs (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f a = output_f s_f2 a \<and> current s_f = current s_f2))
 2. \<And>aa. \<lbrakk>run n (Some s0) execs = Some rs; run n (Some s0) (purge execs (current rs)) = Some aa\<rbrakk> \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (purge execs (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f a = output_f s_f2 a \<and> current s_f = current s_f2))
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
run n (Some s0) (purge execs (current rs)) = None

goal (2 subgoals):
 1. \<lbrakk>run n (Some s0) execs = Some rs; run n (Some s0) (purge execs (current rs)) = None\<rbrakk> \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (purge execs (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f a = output_f s_f2 a \<and> current s_f = current s_f2))
 2. \<And>aa. \<lbrakk>run n (Some s0) execs = Some rs; run n (Some s0) (purge execs (current rs)) = Some aa\<rbrakk> \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (purge execs (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f a = output_f s_f2 a \<and> current s_f = current s_f2))
[PROOF STEP]
from Some this
[PROOF STATE]
proof (chain)
picking this:
run n (Some s0) execs = Some rs
run n (Some s0) (purge execs (current rs)) = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
run n (Some s0) execs = Some rs
run n (Some s0) (purge execs (current rs)) = None

goal (1 subgoal):
 1. run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (purge execs (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f a = output_f s_f2 a \<and> current s_f = current s_f2))
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
using this:
run n (Some s0) execs = Some rs
run n (Some s0) (purge execs (current rs)) = None

goal (1 subgoal):
 1. case run n (Some s0) execs of None \<Rightarrow> True | Some aa \<Rightarrow> case run n (Some s0) (purge execs (current aa)) of None \<Rightarrow> True | Some ab \<Rightarrow> output_f aa a = output_f ab a \<and> current aa = current ab
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (purge execs (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f a = output_f s_f2 a \<and> current s_f = current s_f2))

goal (1 subgoal):
 1. \<And>aa. \<lbrakk>run n (Some s0) execs = Some rs; run n (Some s0) (purge execs (current rs)) = Some aa\<rbrakk> \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (purge execs (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f a = output_f s_f2 a \<and> current s_f = current s_f2))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>run n (Some s0) execs = Some rs; run n (Some s0) (purge execs (current rs)) = Some aa\<rbrakk> \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (purge execs (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f a = output_f s_f2 a \<and> current s_f = current s_f2))
[PROOF STEP]
case (Some rt)
[PROOF STATE]
proof (state)
this:
run n (Some s0) (purge execs (current rs)) = Some rt

goal (1 subgoal):
 1. \<And>aa. \<lbrakk>run n (Some s0) execs = Some rs; run n (Some s0) (purge execs (current rs)) = Some aa\<rbrakk> \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (purge execs (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f a = output_f s_f2 a \<and> current s_f = current s_f2))
[PROOF STEP]
from \<open>run n (Some s0) execs = Some rs\<close> Some 1[THEN spec,where x="current rs"]
[PROOF STATE]
proof (chain)
picking this:
run n (Some s0) execs = Some rs
run n (Some s0) (purge execs (current rs)) = Some rt
B2 (run n (Some s0) execs) (run n (Some s0) (purge execs (current rs))) (\<lambda>rsa rt. vpeq (current rs) rsa rt \<and> current rsa = current rt)
[PROOF STEP]
have vpeq: "vpeq (current rs) rs rt \<and> current rs = current rt"
[PROOF STATE]
proof (prove)
using this:
run n (Some s0) execs = Some rs
run n (Some s0) (purge execs (current rs)) = Some rt
B2 (run n (Some s0) execs) (run n (Some s0) (purge execs (current rs))) (\<lambda>rsa rt. vpeq (current rs) rsa rt \<and> current rsa = current rt)

goal (1 subgoal):
 1. vpeq (current rs) rs rt \<and> current rs = current rt
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
using this:
run n (Some s0) execs = Some rs
run n (Some s0) (purge execs (current rs)) = Some rt
B2 (run n (Some s0) execs) (run n (Some s0) (purge execs (current rs))) (\<lambda>rsa rt. vpeq (current rs) rsa rt \<and> current rsa = current rt)

goal (1 subgoal):
 1. vpeq (current rs) rs rt \<and> current rs = current rt
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vpeq (current rs) rs rt \<and> current rs = current rt

goal (1 subgoal):
 1. \<And>aa. \<lbrakk>run n (Some s0) execs = Some rs; run n (Some s0) (purge execs (current rs)) = Some aa\<rbrakk> \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (purge execs (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f a = output_f s_f2 a \<and> current s_f = current s_f2))
[PROOF STEP]
from this output_consistent
[PROOF STATE]
proof (chain)
picking this:
vpeq (current rs) rs rt \<and> current rs = current rt
\<forall>a s t. vpeq (current s) s t \<and> current s = current t \<longrightarrow> output_f s a = output_f t a
[PROOF STEP]
have "output_f rs a = output_f rt a"
[PROOF STATE]
proof (prove)
using this:
vpeq (current rs) rs rt \<and> current rs = current rt
\<forall>a s t. vpeq (current s) s t \<and> current s = current t \<longrightarrow> output_f s a = output_f t a

goal (1 subgoal):
 1. output_f rs a = output_f rt a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
output_f rs a = output_f rt a

goal (1 subgoal):
 1. \<And>aa. \<lbrakk>run n (Some s0) execs = Some rs; run n (Some s0) (purge execs (current rs)) = Some aa\<rbrakk> \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (purge execs (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f a = output_f s_f2 a \<and> current s_f = current s_f2))
[PROOF STEP]
from this vpeq \<open>run n (Some s0) execs = Some rs\<close> Some
[PROOF STATE]
proof (chain)
picking this:
output_f rs a = output_f rt a
vpeq (current rs) rs rt \<and> current rs = current rt
run n (Some s0) execs = Some rs
run n (Some s0) (purge execs (current rs)) = Some rt
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
output_f rs a = output_f rt a
vpeq (current rs) rs rt \<and> current rs = current rt
run n (Some s0) execs = Some rs
run n (Some s0) (purge execs (current rs)) = Some rt

goal (1 subgoal):
 1. run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (purge execs (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f a = output_f s_f2 a \<and> current s_f = current s_f2))
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
using this:
output_f rs a = output_f rt a
vpeq (current rs) rs rt \<and> current rs = current rt
run n (Some s0) execs = Some rs
run n (Some s0) (purge execs (current rs)) = Some rt

goal (1 subgoal):
 1. case run n (Some s0) execs of None \<Rightarrow> True | Some aa \<Rightarrow> case run n (Some s0) (purge execs (current aa)) of None \<Rightarrow> True | Some ab \<Rightarrow> output_f aa a = output_f ab a \<and> current aa = current ab
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (purge execs (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f a = output_f s_f2 a \<and> current s_f = current s_f2))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (purge execs (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f a = output_f s_f2 a \<and> current s_f = current s_f2))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (purge execs (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f a = output_f s_f2 a \<and> current s_f = current s_f2))

goal (1 subgoal):
 1. NI_unrelated
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
run ?n2 (Some s0) ?execs2 \<rightharpoonup> (\<lambda>s_f. run ?n2 (Some s0) (purge ?execs2 (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f ?a2 = output_f s_f2 ?a2 \<and> current s_f = current s_f2))

goal (1 subgoal):
 1. NI_unrelated
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
run ?n2 (Some s0) ?execs2 \<rightharpoonup> (\<lambda>s_f. run ?n2 (Some s0) (purge ?execs2 (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f ?a2 = output_f s_f2 ?a2 \<and> current s_f = current s_f2))

goal (1 subgoal):
 1. NI_unrelated
[PROOF STEP]
unfolding NI_unrelated_def
[PROOF STATE]
proof (prove)
using this:
run ?n2 (Some s0) ?execs2 \<rightharpoonup> (\<lambda>s_f. run ?n2 (Some s0) (purge ?execs2 (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f ?a2 = output_f s_f2 ?a2 \<and> current s_f = current s_f2))

goal (1 subgoal):
 1. \<forall>execs a n. run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (purge execs (current s_f)) \<rightharpoonup> (\<lambda>s_f2. output_f s_f a = output_f s_f2 a \<and> current s_f = current s_f2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
NI_unrelated

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vpeq_involved_domains:
assumes ifp_curr: "ifp (current s) u"
    and not_intermediary_curr: "\<not>intermediary (current s) u"
    and no_gateway_comm: "does_not_communicate_with_gateway u execs"
    and vpeq_s_t: "\<forall> v . ifp v u \<and> \<not>intermediary v u \<longrightarrow> vpeq v s t'"
    and prec_s: "precondition (next_state s execs) (next_action s execs)"
  shows "\<forall> d \<in> involved (next_action s execs) . vpeq d s t'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>d\<in>involved (next_action s execs). vpeq d s t'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>d\<in>involved (next_action s execs). vpeq d s t'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>d\<in>involved (next_action s execs). vpeq d s t'
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>d\<in>involved (next_action s execs). vpeq d s t'
[PROOF STEP]
assume involved: "v \<in> involved (next_action s execs)"
[PROOF STATE]
proof (state)
this:
v \<in> involved (next_action s execs)

goal (1 subgoal):
 1. \<forall>d\<in>involved (next_action s execs). vpeq d s t'
[PROOF STEP]
from this prec_s involved_ifp[THEN spec,THEN spec,where x1="next_state s execs" and x="next_action s execs"]
[PROOF STATE]
proof (chain)
picking this:
v \<in> involved (next_action s execs)
precondition (next_state s execs) (next_action s execs)
\<forall>d\<in>involved (next_action s execs). kprecondition (next_state s execs) (the (next_action s execs)) \<longrightarrow> ifp d (current (next_state s execs))
[PROOF STEP]
have ifp_v_curr: "ifp v (current s)"
[PROOF STATE]
proof (prove)
using this:
v \<in> involved (next_action s execs)
precondition (next_state s execs) (next_action s execs)
\<forall>d\<in>involved (next_action s execs). kprecondition (next_state s execs) (the (next_action s execs)) \<longrightarrow> ifp d (current (next_state s execs))

goal (1 subgoal):
 1. ifp v (current s)
[PROOF STEP]
using current_next_state
[PROOF STATE]
proof (prove)
using this:
v \<in> involved (next_action s execs)
precondition (next_state s execs) (next_action s execs)
\<forall>d\<in>involved (next_action s execs). kprecondition (next_state s execs) (the (next_action s execs)) \<longrightarrow> ifp d (current (next_state s execs))
\<forall>s execs. current (next_state s execs) = current s

goal (1 subgoal):
 1. ifp v (current s)
[PROOF STEP]
unfolding involved_def precondition_def B_def
[PROOF STATE]
proof (prove)
using this:
v \<in> (case next_action s execs of None \<Rightarrow> {} | Some a \<Rightarrow> kinvolved a)
case next_action s execs of None \<Rightarrow> True | Some a \<Rightarrow> kprecondition (next_state s execs) a
\<forall>d\<in>case next_action s execs of None \<Rightarrow> {} | Some a \<Rightarrow> kinvolved a. kprecondition (next_state s execs) (the (next_action s execs)) \<longrightarrow> ifp d (current (next_state s execs))
\<forall>s execs. current (next_state s execs) = current s

goal (1 subgoal):
 1. ifp v (current s)
[PROOF STEP]
by(cases "next_action s execs",auto)
[PROOF STATE]
proof (state)
this:
ifp v (current s)

goal (1 subgoal):
 1. \<forall>d\<in>involved (next_action s execs). vpeq d s t'
[PROOF STEP]
have "vpeq v s t'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vpeq v s t'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vpeq v s t'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vpeq v s t'
[PROOF STEP]
assume "ifp v u \<and> \<not>intermediary v u"
[PROOF STATE]
proof (state)
this:
ifp v u \<and> \<not> intermediary v u

goal (1 subgoal):
 1. vpeq v s t'
[PROOF STEP]
from this vpeq_s_t
[PROOF STATE]
proof (chain)
picking this:
ifp v u \<and> \<not> intermediary v u
\<forall>v. ifp v u \<and> \<not> intermediary v u \<longrightarrow> vpeq v s t'
[PROOF STEP]
have "vpeq v s t'"
[PROOF STATE]
proof (prove)
using this:
ifp v u \<and> \<not> intermediary v u
\<forall>v. ifp v u \<and> \<not> intermediary v u \<longrightarrow> vpeq v s t'

goal (1 subgoal):
 1. vpeq v s t'
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
vpeq v s t'

goal (1 subgoal):
 1. vpeq v s t'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
ifp v u \<and> \<not> intermediary v u \<Longrightarrow> vpeq v s t'

goal (1 subgoal):
 1. vpeq v s t'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ifp v u \<and> \<not> intermediary v u \<Longrightarrow> vpeq v s t'

goal (1 subgoal):
 1. vpeq v s t'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
ifp v u \<and> \<not> intermediary v u \<Longrightarrow> vpeq v s t'

goal (1 subgoal):
 1. vpeq v s t'
[PROOF STEP]
assume not_intermediary_v: "intermediary v u"
[PROOF STATE]
proof (state)
this:
intermediary v u

goal (1 subgoal):
 1. vpeq v s t'
[PROOF STEP]
from ifp_curr not_intermediary_curr ifp_v_curr not_intermediary_v
[PROOF STATE]
proof (chain)
picking this:
ifp (current s) u
\<not> intermediary (current s) u
ifp v (current s)
intermediary v u
[PROOF STEP]
have curr_is_u: "current s = u"
[PROOF STATE]
proof (prove)
using this:
ifp (current s) u
\<not> intermediary (current s) u
ifp v (current s)
intermediary v u

goal (1 subgoal):
 1. current s = u
[PROOF STEP]
using rtranclp_trans r_into_rtranclp
[PROOF STATE]
proof (prove)
using this:
ifp (current s) u
\<not> intermediary (current s) u
ifp v (current s)
intermediary v u
\<lbrakk>?r\<^sup>*\<^sup>* ?x ?y; ?r\<^sup>*\<^sup>* ?y ?z\<rbrakk> \<Longrightarrow> ?r\<^sup>*\<^sup>* ?x ?z
?r ?x ?y \<Longrightarrow> ?r\<^sup>*\<^sup>* ?x ?y

goal (1 subgoal):
 1. current s = u
[PROOF STEP]
by (metis intermediary_def)
[PROOF STATE]
proof (state)
this:
current s = u

goal (1 subgoal):
 1. vpeq v s t'
[PROOF STEP]
from curr_is_u next_action_from_execs[THEN spec,THEN spec,where x=execs and x1=s] not_intermediary_v involved
         no_gateway_comm[unfolded does_not_communicate_with_gateway_def,THEN spec,where x="the (next_action s execs)"]
[PROOF STATE]
proof (chain)
picking this:
current s = u
next_action s execs \<rightharpoonup> (\<lambda>a. a \<in> actions_in_execution (execs (current s)))
intermediary v u
v \<in> involved (next_action s execs)
the (next_action s execs) \<in> actions_in_execution (execs u) \<longrightarrow> (\<forall>v. intermediary v u \<longrightarrow> v \<notin> involved (Some (the (next_action s execs))))
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
current s = u
next_action s execs \<rightharpoonup> (\<lambda>a. a \<in> actions_in_execution (execs (current s)))
intermediary v u
v \<in> involved (next_action s execs)
the (next_action s execs) \<in> actions_in_execution (execs u) \<longrightarrow> (\<forall>v. intermediary v u \<longrightarrow> v \<notin> involved (Some (the (next_action s execs))))

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding involved_def B_def
[PROOF STATE]
proof (prove)
using this:
current s = u
case next_action s execs of None \<Rightarrow> True | Some a \<Rightarrow> a \<in> actions_in_execution (execs (current s))
intermediary v u
v \<in> (case next_action s execs of None \<Rightarrow> {} | Some a \<Rightarrow> kinvolved a)
the (next_action s execs) \<in> actions_in_execution (execs u) \<longrightarrow> (\<forall>v. intermediary v u \<longrightarrow> v \<notin> (case Some (the (next_action s execs)) of None \<Rightarrow> {} | Some a \<Rightarrow> kinvolved a))

goal (1 subgoal):
 1. False
[PROOF STEP]
by (cases "next_action s execs",auto)
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. vpeq v s t'
[PROOF STEP]
hence "vpeq v s t'"
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. vpeq v s t'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vpeq v s t'

goal (1 subgoal):
 1. vpeq v s t'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
intermediary v u \<Longrightarrow> vpeq v s t'

goal (1 subgoal):
 1. vpeq v s t'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
intermediary v u \<Longrightarrow> vpeq v s t'

goal (1 subgoal):
 1. vpeq v s t'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
intermediary v u \<Longrightarrow> vpeq v s t'

goal (1 subgoal):
 1. vpeq v s t'
[PROOF STEP]
assume intermediary_v: "\<not> ifp v u"
[PROOF STATE]
proof (state)
this:
\<not> ifp v u

goal (1 subgoal):
 1. vpeq v s t'
[PROOF STEP]
from ifp_curr not_intermediary_curr ifp_v_curr intermediary_v
[PROOF STATE]
proof (chain)
picking this:
ifp (current s) u
\<not> intermediary (current s) u
ifp v (current s)
\<not> ifp v u
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
using this:
ifp (current s) u
\<not> intermediary (current s) u
ifp v (current s)
\<not> ifp v u

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding intermediary_def
[PROOF STATE]
proof (prove)
using this:
ifp (current s) u
\<nexists>v. ifp\<^sup>*\<^sup>* v (current s) \<and> ifp (current s) u \<and> \<not> ifp v u \<and> current s \<noteq> u
ifp v (current s)
\<not> ifp v u

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

goal (1 subgoal):
 1. vpeq v s t'
[PROOF STEP]
hence "vpeq v s t'"
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. vpeq v s t'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vpeq v s t'

goal (1 subgoal):
 1. vpeq v s t'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> ifp v u \<Longrightarrow> vpeq v s t'

goal (1 subgoal):
 1. vpeq v s t'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ifp v u \<and> \<not> intermediary v u \<Longrightarrow> vpeq v s t'
intermediary v u \<Longrightarrow> vpeq v s t'
\<not> ifp v u \<Longrightarrow> vpeq v s t'
[PROOF STEP]
show "vpeq v s t'"
[PROOF STATE]
proof (prove)
using this:
ifp v u \<and> \<not> intermediary v u \<Longrightarrow> vpeq v s t'
intermediary v u \<Longrightarrow> vpeq v s t'
\<not> ifp v u \<Longrightarrow> vpeq v s t'

goal (1 subgoal):
 1. vpeq v s t'
[PROOF STEP]
unfolding intermediary_def
[PROOF STATE]
proof (prove)
using this:
ifp v u \<and> (\<nexists>va. ifp\<^sup>*\<^sup>* va v \<and> ifp v u \<and> \<not> ifp va u \<and> v \<noteq> u) \<Longrightarrow> vpeq v s t'
\<exists>va. ifp\<^sup>*\<^sup>* va v \<and> ifp v u \<and> \<not> ifp va u \<and> v \<noteq> u \<Longrightarrow> vpeq v s t'
\<not> ifp v u \<Longrightarrow> vpeq v s t'

goal (1 subgoal):
 1. vpeq v s t'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vpeq v s t'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vpeq v s t'

goal (1 subgoal):
 1. \<forall>d\<in>involved (next_action s execs). vpeq d s t'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?v2 \<in> involved (next_action s execs) \<Longrightarrow> vpeq ?v2 s t'

goal (1 subgoal):
 1. \<forall>d\<in>involved (next_action s execs). vpeq d s t'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?v2 \<in> involved (next_action s execs) \<Longrightarrow> vpeq ?v2 s t'

goal (1 subgoal):
 1. \<forall>d\<in>involved (next_action s execs). vpeq d s t'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>d\<in>involved (next_action s execs). vpeq d s t'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ipurge_l_removes_gateway_communications:
shows "does_not_communicate_with_gateway u (ipurge_l execs u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. does_not_communicate_with_gateway u (ipurge_l execs u)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. does_not_communicate_with_gateway u (ipurge_l execs u)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. does_not_communicate_with_gateway u (ipurge_l execs u)
[PROOF STEP]
fix aseq u execs a v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. does_not_communicate_with_gateway u (ipurge_l execs u)
[PROOF STEP]
assume 1: "aseq \<in> set (remove_gateway_communications u (execs u))"
[PROOF STATE]
proof (state)
this:
aseq \<in> set (remove_gateway_communications u (execs u))

goal (1 subgoal):
 1. does_not_communicate_with_gateway u (ipurge_l execs u)
[PROOF STEP]
assume 2: "a \<in> set aseq"
[PROOF STATE]
proof (state)
this:
a \<in> set aseq

goal (1 subgoal):
 1. does_not_communicate_with_gateway u (ipurge_l execs u)
[PROOF STEP]
assume 3: "intermediary v u"
[PROOF STATE]
proof (state)
this:
intermediary v u

goal (1 subgoal):
 1. does_not_communicate_with_gateway u (ipurge_l execs u)
[PROOF STEP]
have 4: "v \<notin> involved (Some a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<notin> involved (Some a)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<notin> involved (Some a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<notin> involved (Some a)
[PROOF STEP]
fix a::'action_t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<notin> involved (Some a__)
[PROOF STEP]
fix aseq u exec v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v__ \<notin> involved (Some a__)
[PROOF STEP]
have "aseq \<in> set (remove_gateway_communications u exec) \<and> a \<in> set aseq \<and> intermediary v u \<longrightarrow> v \<notin> involved (Some a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aseq \<in> set (remove_gateway_communications u exec) \<and> a \<in> set aseq \<and> intermediary v u \<longrightarrow> v \<notin> involved (Some a)
[PROOF STEP]
by(induct exec,auto)
[PROOF STATE]
proof (state)
this:
aseq \<in> set (remove_gateway_communications u exec) \<and> a \<in> set aseq \<and> intermediary v u \<longrightarrow> v \<notin> involved (Some a)

goal (1 subgoal):
 1. v__ \<notin> involved (Some a__)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?aseqa2 \<in> set (remove_gateway_communications ?ub2 ?exec2) \<and> ?aa2 \<in> set ?aseqa2 \<and> intermediary ?va2 ?ub2 \<longrightarrow> ?va2 \<notin> involved (Some ?aa2)

goal (1 subgoal):
 1. v \<notin> involved (Some a)
[PROOF STEP]
from 1 2 3 this
[PROOF STATE]
proof (chain)
picking this:
aseq \<in> set (remove_gateway_communications u (execs u))
a \<in> set aseq
intermediary v u
?aseqa2 \<in> set (remove_gateway_communications ?ub2 ?exec2) \<and> ?aa2 \<in> set ?aseqa2 \<and> intermediary ?va2 ?ub2 \<longrightarrow> ?va2 \<notin> involved (Some ?aa2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
aseq \<in> set (remove_gateway_communications u (execs u))
a \<in> set aseq
intermediary v u
?aseqa2 \<in> set (remove_gateway_communications ?ub2 ?exec2) \<and> ?aa2 \<in> set ?aseqa2 \<and> intermediary ?va2 ?ub2 \<longrightarrow> ?va2 \<notin> involved (Some ?aa2)

goal (1 subgoal):
 1. v \<notin> involved (Some a)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
v \<notin> involved (Some a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
v \<notin> involved (Some a)

goal (1 subgoal):
 1. does_not_communicate_with_gateway u (ipurge_l execs u)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?aseq2 \<in> set (remove_gateway_communications ?ua2 (?execsa2 ?ua2)); ?a2 \<in> set ?aseq2; intermediary ?v2 ?ua2\<rbrakk> \<Longrightarrow> ?v2 \<notin> involved (Some ?a2)

goal (1 subgoal):
 1. does_not_communicate_with_gateway u (ipurge_l execs u)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?aseq2 \<in> set (remove_gateway_communications ?ua2 (?execsa2 ?ua2)); ?a2 \<in> set ?aseq2; intermediary ?v2 ?ua2\<rbrakk> \<Longrightarrow> ?v2 \<notin> involved (Some ?a2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?aseq2 \<in> set (remove_gateway_communications ?ua2 (?execsa2 ?ua2)); ?a2 \<in> set ?aseq2; intermediary ?v2 ?ua2\<rbrakk> \<Longrightarrow> ?v2 \<notin> involved (Some ?a2)

goal (1 subgoal):
 1. does_not_communicate_with_gateway u (ipurge_l execs u)
[PROOF STEP]
unfolding does_not_communicate_with_gateway_def ipurge_l_def actions_in_execution_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?aseq2 \<in> set (remove_gateway_communications ?ua2 (?execsa2 ?ua2)); ?a2 \<in> set ?aseq2; intermediary ?v2 ?ua2\<rbrakk> \<Longrightarrow> ?v2 \<notin> involved (Some ?a2)

goal (1 subgoal):
 1. \<forall>a. a \<in> {a. \<exists>aseq\<in>set (if intermediary u u then [] else if u = u then remove_gateway_communications u (execs u) else execs u). a \<in> set aseq} \<longrightarrow> (\<forall>v. intermediary v u \<longrightarrow> v \<notin> involved (Some a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
does_not_communicate_with_gateway u (ipurge_l execs u)

goal:
No subgoals!
[PROOF STEP]
qed