[STATEMENT]
lemma lm031:
  "{a. Domain a \<subseteq> N    &   Range a \<in> all_partitions G} =
   (Domain -`(Pow N))  \<inter>  (Range -` (all_partitions G)) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a. Domain a \<subseteq> N \<and> Range a \<in> all_partitions G} = Domain -` Pow N \<inter> Range -` all_partitions G
[PROOF STEP]
by fastforce


[STATEMENT]
lemma cardinalityPreservation:
  assumes "\<forall>X \<in> XX. finite X" "is_non_overlapping XX"
  shows   "card (\<Union> XX) = sum card XX"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (\<Union> XX) = sum card XX
[PROOF STEP]
by (metis assms is_non_overlapping_def card_Union_disjoint disjointI)


[STATEMENT]
lemma map_vec_append: "map_vec f (a @\<^sub>v b) = map_vec f a @\<^sub>v map_vec f b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_vec f (a @\<^sub>v b) = map_vec f a @\<^sub>v map_vec f b
[PROOF STEP]
by (induction a arbitrary: b) (auto)


[STATEMENT]
lemma single_nz_val_carrier: "single_nz_val n i v \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. single_nz_val n i v \<in> carrier_vec n
[PROOF STEP]
by auto


[STATEMENT]
lemma ssubst_sopen_distrib[rule_format]:
  "\<forall>n s p t'. lc t' \<longrightarrow> [x \<rightarrow> t'] {n \<rightarrow> [s,p]} t
   = {n \<rightarrow> [[x \<rightarrow> t']s, [x \<rightarrow> t']p]} [x \<rightarrow> t'] t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n s p t'. lc t' \<longrightarrow> [x \<rightarrow> t'] {n \<rightarrow> [s,p]} t = {n \<rightarrow> [[x \<rightarrow> t'] s,[x \<rightarrow> t'] p]} [x \<rightarrow> t'] t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>n s p t'. lc t' \<longrightarrow> [x \<rightarrow> t'] {n \<rightarrow> [s,p]} t = {n \<rightarrow> [[x \<rightarrow> t'] s,[x \<rightarrow> t'] p]} [x \<rightarrow> t'] t
[PROOF STEP]
have
    "(\<forall>n s p t'. lc t'
       \<longrightarrow> [x \<rightarrow> t'] {n \<rightarrow> [s,p]} t = {n \<rightarrow> [[x \<rightarrow> t']s, [x \<rightarrow> t']p]} [x \<rightarrow> t'] t)
    &(\<forall>n s p t'. lc t'
       \<longrightarrow> ssubst_option x t' (sopen_option n s p u)
           = sopen_option n ([x \<rightarrow> t']s) ([x \<rightarrow> t']p) (ssubst_option x t' u))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>n s p t'. lc t' \<longrightarrow> [x \<rightarrow> t'] {n \<rightarrow> [s,p]} t = {n \<rightarrow> [[x \<rightarrow> t'] s,[x \<rightarrow> t'] p]} [x \<rightarrow> t'] t) \<and> (\<forall>n s p t'. lc t' \<longrightarrow> ssubst_option x t' (sopen_option n s p u) = sopen_option n ([x \<rightarrow> t'] s) ([x \<rightarrow> t'] p) (ssubst_option x t' u))
[PROOF STEP]
by (rule compat_sterm_sterm_option.induct, simp_all split: bVariable.split)
[PROOF STATE]
proof (state)
this:
(\<forall>n s p t'. lc t' \<longrightarrow> [x \<rightarrow> t'] {n \<rightarrow> [s,p]} t = {n \<rightarrow> [[x \<rightarrow> t'] s,[x \<rightarrow> t'] p]} [x \<rightarrow> t'] t) \<and> (\<forall>n s p t'. lc t' \<longrightarrow> ssubst_option x t' (sopen_option n s p u) = sopen_option n ([x \<rightarrow> t'] s) ([x \<rightarrow> t'] p) (ssubst_option x t' u))

goal (1 subgoal):
 1. \<forall>n s p t'. lc t' \<longrightarrow> [x \<rightarrow> t'] {n \<rightarrow> [s,p]} t = {n \<rightarrow> [[x \<rightarrow> t'] s,[x \<rightarrow> t'] p]} [x \<rightarrow> t'] t
[PROOF STEP]
from conjunct1[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<forall>n s p t'. lc t' \<longrightarrow> [x \<rightarrow> t'] {n \<rightarrow> [s,p]} t = {n \<rightarrow> [[x \<rightarrow> t'] s,[x \<rightarrow> t'] p]} [x \<rightarrow> t'] t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>n s p t'. lc t' \<longrightarrow> [x \<rightarrow> t'] {n \<rightarrow> [s,p]} t = {n \<rightarrow> [[x \<rightarrow> t'] s,[x \<rightarrow> t'] p]} [x \<rightarrow> t'] t

goal (1 subgoal):
 1. \<forall>n s p t'. lc t' \<longrightarrow> [x \<rightarrow> t'] {n \<rightarrow> [s,p]} t = {n \<rightarrow> [[x \<rightarrow> t'] s,[x \<rightarrow> t'] p]} [x \<rightarrow> t'] t
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
\<forall>n s p t'. lc t' \<longrightarrow> [x \<rightarrow> t'] {n \<rightarrow> [s,p]} t = {n \<rightarrow> [[x \<rightarrow> t'] s,[x \<rightarrow> t'] p]} [x \<rightarrow> t'] t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rtrancl_beta_UpdL:
  "\<lbrakk> t \<rightarrow>\<^sub>\<beta>\<^sup>* t'; body u \<rbrakk> \<Longrightarrow> Upd t l u \<rightarrow>\<^sub>\<beta>\<^sup>* Upd t' l u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t ->> t'; body u\<rbrakk> \<Longrightarrow> Upd t l u ->> Upd t' l u
[PROOF STEP]
proof (induct t t' rule: rtranclp.induct, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a ->> b; body u \<Longrightarrow> Upd a l u ->> Upd b l u; b -> c; body u\<rbrakk> \<Longrightarrow> Upd a l u ->> Upd c l u
[PROOF STEP]
case (rtrancl_into_rtrancl a b c)
[PROOF STATE]
proof (state)
this:
a ->> b
body u \<Longrightarrow> Upd a l u ->> Upd b l u
b -> c
body u

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a ->> b; body u \<Longrightarrow> Upd a l u ->> Upd b l u; b -> c; body u\<rbrakk> \<Longrightarrow> Upd a l u ->> Upd c l u
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
a ->> b
body u \<Longrightarrow> Upd a l u ->> Upd b l u
b -> c
body u

goal (1 subgoal):
 1. Upd a l u ->> Upd c l u
[PROOF STEP]
proof (auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>a ->> b; Upd a l u ->> Upd b l u; b -> c; body u\<rbrakk> \<Longrightarrow> Upd a l u ->> Upd c l u
[PROOF STEP]
from \<open>b \<rightarrow>\<^sub>\<beta> c\<close> \<open>body u\<close>
[PROOF STATE]
proof (chain)
picking this:
b -> c
body u
[PROOF STEP]
have "Upd b l u \<rightarrow>\<^sub>\<beta> Upd c l u"
[PROOF STATE]
proof (prove)
using this:
b -> c
body u

goal (1 subgoal):
 1. Upd b l u -> Upd c l u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Upd b l u -> Upd c l u

goal (1 subgoal):
 1. \<lbrakk>a ->> b; Upd a l u ->> Upd b l u; b -> c; body u\<rbrakk> \<Longrightarrow> Upd a l u ->> Upd c l u
[PROOF STEP]
with rtrancl_into_rtrancl(2)[OF \<open>body u\<close>]
[PROOF STATE]
proof (chain)
picking this:
Upd a l u ->> Upd b l u
Upd b l u -> Upd c l u
[PROOF STEP]
show "Upd a l u \<rightarrow>\<^sub>\<beta>\<^sup>* Upd c l u"
[PROOF STATE]
proof (prove)
using this:
Upd a l u ->> Upd b l u
Upd b l u -> Upd c l u

goal (1 subgoal):
 1. Upd a l u ->> Upd c l u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Upd a l u ->> Upd c l u

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Upd a l u ->> Upd c l u

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma strand_subst_all_fv_subset:
  assumes "fv t \<subseteq> fv\<^sub>s\<^sub>t S" "(subst_domain \<delta> \<union> range_vars \<delta>) \<inter> bvars\<^sub>s\<^sub>t S = {}"
  shows "fv (t \<cdot> \<delta>) \<subseteq> fv\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fv (t \<cdot> \<delta>) \<subseteq> fv\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
fv t \<subseteq> fv\<^sub>s\<^sub>t S
(subst_domain \<delta> \<union> range_vars \<delta>) \<inter> bvars\<^sub>s\<^sub>t S = {}

goal (1 subgoal):
 1. fv (t \<cdot> \<delta>) \<subseteq> fv\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>)
[PROOF STEP]
by (metis fv_strand_subst' Int_commute subst_apply_fv_subset)


[STATEMENT]
lemma recvOFriend_eqButUID:
assumes "step s a = (ou, s')"
and "reach s"
and "a = COMact (comReceiveCreateOFriend AID cp UID uID') \<or> a = COMact (comReceiveDeleteOFriend AID cp UID uID')"
and "uID' \<notin> UIDs AID'"
shows "eqButUID s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID s s'
[PROOF STEP]
using assms reach_distinct_friends_reqs(4)
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
reach s
a = COMact (comReceiveCreateOFriend AID cp UID uID') \<or> a = COMact (comReceiveDeleteOFriend AID cp UID uID')
uID' \<notin> UIDs AID'
reach ?s \<Longrightarrow> distinct (recvOuterFriendIDs ?s ?uid)

goal (1 subgoal):
 1. eqButUID s s'
[PROOF STEP]
unfolding eqButUID_def eqButUIDf_def
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
reach s
a = COMact (comReceiveCreateOFriend AID cp UID uID') \<or> a = COMact (comReceiveDeleteOFriend AID cp UID uID')
uID' \<notin> UIDs AID'
reach ?s \<Longrightarrow> distinct (recvOuterFriendIDs ?s ?uid)

goal (1 subgoal):
 1. admin s = admin s' \<and> pendingUReqs s = pendingUReqs s' \<and> userReq s = userReq s' \<and> userIDs s = userIDs s' \<and> user s = user s' \<and> pass s = pass s' \<and> pendingFReqs s = pendingFReqs s' \<and> friendReq s = friendReq s' \<and> friendIDs s = friendIDs s' \<and> postIDs s = postIDs s' \<and> admin s = admin s' \<and> post s = post s' \<and> vis s = vis s' \<and> owner s = owner s' \<and> pendingSApiReqs s = pendingSApiReqs s' \<and> sApiReq s = sApiReq s' \<and> serverApiIDs s = serverApiIDs s' \<and> serverPass s = serverPass s' \<and> outerPostIDs s = outerPostIDs s' \<and> outerPost s = outerPost s' \<and> outerVis s = outerVis s' \<and> outerOwner s = outerOwner s' \<and> sentOuterFriendIDs s = sentOuterFriendIDs s' \<and> (\<forall>uid. if uid \<in> UIDs AID' then recvOuterFriendIDs s uid = recvOuterFriendIDs s' uid else eqButUIDl (recvOuterFriendIDs s uid) (recvOuterFriendIDs s' uid)) \<and> pendingCApiReqs s = pendingCApiReqs s' \<and> cApiReq s = cApiReq s' \<and> clientApiIDs s = clientApiIDs s' \<and> clientPass s = clientPass s' \<and> sharedWith s = sharedWith s'
[PROOF STEP]
by (auto simp: com_defs remove1_idem remove1_append)


[STATEMENT]
lemma distinct_mid_unique2: "\<lbrakk>distinct (xs@U@ys); U\<noteq>[]; xs@U@ys = as@U@bs\<rbrakk> \<Longrightarrow> ys = bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct (xs @ U @ ys); U \<noteq> []; xs @ U @ ys = as @ U @ bs\<rbrakk> \<Longrightarrow> ys = bs
[PROOF STEP]
using distinct_mid_unique1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (?xs @ ?U @ ?ys); ?U \<noteq> []; ?xs @ ?U @ ?ys = ?as @ ?U @ ?bs\<rbrakk> \<Longrightarrow> ?as = ?xs

goal (1 subgoal):
 1. \<lbrakk>distinct (xs @ U @ ys); U \<noteq> []; xs @ U @ ys = as @ U @ bs\<rbrakk> \<Longrightarrow> ys = bs
[PROOF STEP]
by blast


[STATEMENT]
lemma nocross_UV_lists_subset:
  "{x. set x = X \<and> distinct x \<and> take 1 x = [r]
     \<and> no_cross_products (create_ldeep x) \<and> (\<forall>xs \<in> Y. sublist xs x)}
  \<subseteq> {x. set x = X \<and> distinct x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. set x = X \<and> distinct x \<and> take 1 x = [r] \<and> no_cross_products (create_ldeep x) \<and> (\<forall>xs\<in>Y. sublist xs x)} \<subseteq> {x. set x = X \<and> distinct x}
[PROOF STEP]
by blast


[STATEMENT]
lemma combine_forward:
  assumes "dom_children (Node r {|(t1,e1)|}) T"
      and "\<forall>v \<in> dverts (Node r {|(t1,e1)|}). forward v"
      and "wf_dlverts (Node r {|(t1,e1)|})"
      and "v \<in> dverts (Node (r@Dtree.root t1) (sucs t1))"
    shows "forward v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. forward v
[PROOF STEP]
proof(cases "v = r @ Dtree.root t1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. v = r @ dtree.root t1 \<Longrightarrow> forward v
 2. v \<noteq> r @ dtree.root t1 \<Longrightarrow> forward v
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
v = r @ dtree.root t1

goal (2 subgoals):
 1. v = r @ dtree.root t1 \<Longrightarrow> forward v
 2. v \<noteq> r @ dtree.root t1 \<Longrightarrow> forward v
[PROOF STEP]
have 0: "(Dtree.root t1) \<in> dverts t1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dtree.root t1 \<in> dverts t1
[PROOF STEP]
by (simp add: dtree.set_sel(1))
[PROOF STATE]
proof (state)
this:
dtree.root t1 \<in> dverts t1

goal (2 subgoals):
 1. v = r @ dtree.root t1 \<Longrightarrow> forward v
 2. v \<noteq> r @ dtree.root t1 \<Longrightarrow> forward v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dtree.root t1 \<in> dverts t1
[PROOF STEP]
have fwd_t1: "forward (Dtree.root t1)"
[PROOF STATE]
proof (prove)
using this:
dtree.root t1 \<in> dverts t1

goal (1 subgoal):
 1. forward (dtree.root t1)
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
dtree.root t1 \<in> dverts t1
Ball (dverts (Node r {|(t1, e1)|})) forward

goal (1 subgoal):
 1. forward (dtree.root t1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
forward (dtree.root t1)

goal (2 subgoals):
 1. v = r @ dtree.root t1 \<Longrightarrow> forward v
 2. v \<noteq> r @ dtree.root t1 \<Longrightarrow> forward v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
forward (dtree.root t1)

goal (2 subgoals):
 1. v = r @ dtree.root t1 \<Longrightarrow> forward v
 2. v \<noteq> r @ dtree.root t1 \<Longrightarrow> forward v
[PROOF STEP]
have "set r \<inter> set (Dtree.root t1) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set r \<inter> set (dtree.root t1) = {}
[PROOF STEP]
using assms(3) 0 lverts_if_in_verts
[PROOF STATE]
proof (prove)
using this:
wf_dlverts (Node r {|(t1, e1)|})
dtree.root t1 \<in> dverts t1
\<lbrakk>?v \<in> dverts ?t; ?x \<in> set ?v\<rbrakk> \<Longrightarrow> ?x \<in> dlverts ?t

goal (1 subgoal):
 1. set r \<inter> set (dtree.root t1) = {}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
set r \<inter> set (dtree.root t1) = {}

goal (2 subgoals):
 1. v = r @ dtree.root t1 \<Longrightarrow> forward v
 2. v \<noteq> r @ dtree.root t1 \<Longrightarrow> forward v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set r \<inter> set (dtree.root t1) = {}

goal (2 subgoals):
 1. v = r @ dtree.root t1 \<Longrightarrow> forward v
 2. v \<noteq> r @ dtree.root t1 \<Longrightarrow> forward v
[PROOF STEP]
have "\<exists>x\<in>set r. \<exists>y\<in>set (Dtree.root t1). x \<rightarrow>\<^bsub>T\<^esub> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>set r. \<exists>y\<in>set (dtree.root t1). x \<rightarrow>\<^bsub>T\<^esub> y
[PROOF STEP]
using assms(1,3) root_arc_if_dom_wfdlverts
[PROOF STATE]
proof (prove)
using this:
dom_children (Node r {|(t1, e1)|}) T
wf_dlverts (Node r {|(t1, e1)|})
\<lbrakk>dom_children (Node ?r ?xs) ?T; ?t1.0 \<in> fst ` fset ?xs; wf_dlverts (Node ?r ?xs)\<rbrakk> \<Longrightarrow> \<exists>x\<in>set ?r. \<exists>y\<in>set (dtree.root ?t1.0). x \<rightarrow>\<^bsub>?T\<^esub> y

goal (1 subgoal):
 1. \<exists>x\<in>set r. \<exists>y\<in>set (dtree.root t1). x \<rightarrow>\<^bsub>T\<^esub> y
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>set r. \<exists>y\<in>set (dtree.root t1). x \<rightarrow>\<^bsub>T\<^esub> y

goal (2 subgoals):
 1. v = r @ dtree.root t1 \<Longrightarrow> forward v
 2. v \<noteq> r @ dtree.root t1 \<Longrightarrow> forward v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
forward (dtree.root t1)
set r \<inter> set (dtree.root t1) = {}
\<exists>x\<in>set r. \<exists>y\<in>set (dtree.root t1). x \<rightarrow>\<^bsub>T\<^esub> y
[PROOF STEP]
have "\<exists>x\<in>set r. x \<rightarrow>\<^bsub>T\<^esub> hd (Dtree.root t1)"
[PROOF STATE]
proof (prove)
using this:
forward (dtree.root t1)
set r \<inter> set (dtree.root t1) = {}
\<exists>x\<in>set r. \<exists>y\<in>set (dtree.root t1). x \<rightarrow>\<^bsub>T\<^esub> y

goal (1 subgoal):
 1. \<exists>x\<in>set r. x \<rightarrow>\<^bsub>T\<^esub> hd (dtree.root t1)
[PROOF STEP]
using forward_arc_to_head
[PROOF STATE]
proof (prove)
using this:
forward (dtree.root t1)
set r \<inter> set (dtree.root t1) = {}
\<exists>x\<in>set r. \<exists>y\<in>set (dtree.root t1). x \<rightarrow>\<^bsub>T\<^esub> y
\<lbrakk>forward ?ys; set ?xs \<inter> set ?ys = {}; ?x \<in> set ?xs; ?y \<in> set ?ys; ?x \<rightarrow>\<^bsub>T\<^esub> ?y\<rbrakk> \<Longrightarrow> ?y = hd ?ys

goal (1 subgoal):
 1. \<exists>x\<in>set r. x \<rightarrow>\<^bsub>T\<^esub> hd (dtree.root t1)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>set r. x \<rightarrow>\<^bsub>T\<^esub> hd (dtree.root t1)

goal (2 subgoals):
 1. v = r @ dtree.root t1 \<Longrightarrow> forward v
 2. v \<noteq> r @ dtree.root t1 \<Longrightarrow> forward v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>set r. x \<rightarrow>\<^bsub>T\<^esub> hd (dtree.root t1)

goal (2 subgoals):
 1. v = r @ dtree.root t1 \<Longrightarrow> forward v
 2. v \<noteq> r @ dtree.root t1 \<Longrightarrow> forward v
[PROOF STEP]
have fwd_r: "forward r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. forward r
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
Ball (dverts (Node r {|(t1, e1)|})) forward

goal (1 subgoal):
 1. forward r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
forward r

goal (2 subgoals):
 1. v = r @ dtree.root t1 \<Longrightarrow> forward v
 2. v \<noteq> r @ dtree.root t1 \<Longrightarrow> forward v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>x\<in>set r. x \<rightarrow>\<^bsub>T\<^esub> hd (dtree.root t1)
forward r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<in>set r. x \<rightarrow>\<^bsub>T\<^esub> hd (dtree.root t1)
forward r

goal (1 subgoal):
 1. forward v
[PROOF STEP]
using forward_app fwd_t1 True
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<in>set r. x \<rightarrow>\<^bsub>T\<^esub> hd (dtree.root t1)
forward r
\<lbrakk>forward ?s1.0; forward ?s2.0; \<exists>x\<in>set ?s1.0. x \<rightarrow>\<^bsub>T\<^esub> hd ?s2.0\<rbrakk> \<Longrightarrow> forward (?s1.0 @ ?s2.0)
forward (dtree.root t1)
v = r @ dtree.root t1

goal (1 subgoal):
 1. forward v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
forward v

goal (1 subgoal):
 1. v \<noteq> r @ dtree.root t1 \<Longrightarrow> forward v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<noteq> r @ dtree.root t1 \<Longrightarrow> forward v
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
v \<noteq> r @ dtree.root t1

goal (1 subgoal):
 1. v \<noteq> r @ dtree.root t1 \<Longrightarrow> forward v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<noteq> r @ dtree.root t1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v \<noteq> r @ dtree.root t1

goal (1 subgoal):
 1. forward v
[PROOF STEP]
using assms(2,4) dverts_suc_subseteq
[PROOF STATE]
proof (prove)
using this:
v \<noteq> r @ dtree.root t1
Ball (dverts (Node r {|(t1, e1)|})) forward
v \<in> dverts (Node (r @ dtree.root t1) (sucs t1))
?x \<in> fst ` fset (sucs ?t) \<Longrightarrow> dverts ?x \<subseteq> dverts ?t

goal (1 subgoal):
 1. forward v
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
forward v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Q_denormalize_full:
  assumes "wf_dlverts t1"
      and "\<forall>v \<in> dverts t1. distinct v"
      and "hd (Dtree.root t1) = root"
      and "max_deg t1 \<le> 1"
      and "\<forall>xs \<in> (dverts t1). seq_conform xs"
      and "dom_children t1 T"
    shows "fwd_sub root (dverts t1) (denormalize (normalize_full t1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fwd_sub root (dverts t1) (denormalize (normalize_full t1))
[PROOF STEP]
using P_denormalize_full[OF assms(1-4)] assms(1,4-6) denormalize_full_sublist_preserv
[PROOF STATE]
proof (prove)
using this:
unique_set_r root (dverts t1) (denormalize (normalize_full t1))
wf_dlverts t1
max_deg t1 \<le> 1
Ball (dverts t1) seq_conform
dom_children t1 T
\<lbrakk>sublist ?xs ?v; ?v \<in> dverts ?t1.0; max_deg ?t1.0 \<le> 1\<rbrakk> \<Longrightarrow> sublist ?xs (denormalize (normalize_full ?t1.0))

goal (1 subgoal):
 1. fwd_sub root (dverts t1) (denormalize (normalize_full t1))
[PROOF STEP]
by (auto dest: denormalize_full_fwd simp: fwd_sub_def)


[STATEMENT]
lemma normalize1_dverts_split:
  "dverts (normalize1 t1)
  = {v \<in> dverts (normalize1 t1). v \<notin> dverts t1} \<union> {v \<in> dverts (normalize1 t1). v \<in> dverts t1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dverts (normalize1 t1) = {v \<in> dverts (normalize1 t1). v \<notin> dverts t1} \<union> {v \<in> dverts (normalize1 t1). v \<in> dverts t1}
[PROOF STEP]
by blast


[STATEMENT]
lemma closed_\<G>\<^sub>F\<^sub>G:
  "closed (\<G>\<^sub>F\<^sub>G \<phi> w) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed (\<G>\<^sub>F\<^sub>G \<phi> w) w
[PROOF STEP]
proof (induction \<phi>)
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. closed (\<G>\<^sub>F\<^sub>G true w) w
 2. closed (\<G>\<^sub>F\<^sub>G false w) w
 3. \<And>x. closed (\<G>\<^sub>F\<^sub>G p(x) w) w
 4. \<And>x. closed (\<G>\<^sub>F\<^sub>G (np(x)) w) w
 5. \<And>\<phi>1 \<phi>2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi>1 w) w; closed (\<G>\<^sub>F\<^sub>G \<phi>2 w) w\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (\<phi>1 and \<phi>2) w) w
 6. \<And>\<phi>1 \<phi>2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi>1 w) w; closed (\<G>\<^sub>F\<^sub>G \<phi>2 w) w\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (\<phi>1 or \<phi>2) w) w
 7. \<And>\<phi>. closed (\<G>\<^sub>F\<^sub>G \<phi> w) w \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (X \<phi>) w) w
 8. \<And>\<phi>. closed (\<G>\<^sub>F\<^sub>G \<phi> w) w \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 9. \<And>\<phi>. closed (\<G>\<^sub>F\<^sub>G \<phi> w) w \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (F \<phi>) w) w
 10. \<And>\<phi>1 \<phi>2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi>1 w) w; closed (\<G>\<^sub>F\<^sub>G \<phi>2 w) w\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (\<phi>1 U \<phi>2) w) w
[PROOF STEP]
case (LTLGlobal \<phi>)
[PROOF STATE]
proof (state)
this:
closed (\<G>\<^sub>F\<^sub>G \<phi> w) w

goal (10 subgoals):
 1. closed (\<G>\<^sub>F\<^sub>G true w) w
 2. closed (\<G>\<^sub>F\<^sub>G false w) w
 3. \<And>x. closed (\<G>\<^sub>F\<^sub>G p(x) w) w
 4. \<And>x. closed (\<G>\<^sub>F\<^sub>G (np(x)) w) w
 5. \<And>\<phi>1 \<phi>2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi>1 w) w; closed (\<G>\<^sub>F\<^sub>G \<phi>2 w) w\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (\<phi>1 and \<phi>2) w) w
 6. \<And>\<phi>1 \<phi>2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi>1 w) w; closed (\<G>\<^sub>F\<^sub>G \<phi>2 w) w\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (\<phi>1 or \<phi>2) w) w
 7. \<And>\<phi>. closed (\<G>\<^sub>F\<^sub>G \<phi> w) w \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (X \<phi>) w) w
 8. \<And>\<phi>. closed (\<G>\<^sub>F\<^sub>G \<phi> w) w \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 9. \<And>\<phi>. closed (\<G>\<^sub>F\<^sub>G \<phi> w) w \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (F \<phi>) w) w
 10. \<And>\<phi>1 \<phi>2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi>1 w) w; closed (\<G>\<^sub>F\<^sub>G \<phi>2 w) w\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (\<phi>1 U \<phi>2) w) w
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
closed (\<G>\<^sub>F\<^sub>G \<phi> w) w

goal (1 subgoal):
 1. closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
proof (cases "w \<Turnstile> F G \<phi>")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; \<not> w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
w \<Turnstile> F G \<phi>

goal (2 subgoals):
 1. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; \<not> w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
hence "\<forall>\<^sub>\<infinity>i. suffix i w \<Turnstile> \<phi>"
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile> F G \<phi>

goal (1 subgoal):
 1. \<forall>\<^sub>\<infinity>i. suffix i w \<Turnstile> \<phi>
[PROOF STEP]
using LTL_FG_almost_all_suffixes
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile> F G \<phi>
?w \<Turnstile> F G ?\<phi> = (\<forall>\<^sub>\<infinity>i. suffix i ?w \<Turnstile> ?\<phi>)

goal (1 subgoal):
 1. \<forall>\<^sub>\<infinity>i. suffix i w \<Turnstile> \<phi>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>\<infinity>i. suffix i w \<Turnstile> \<phi>

goal (2 subgoals):
 1. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; \<not> w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>\<infinity>i. suffix i w \<Turnstile> \<phi>
[PROOF STEP]
obtain i where "\<forall>j \<ge> i. suffix j w \<Turnstile> \<phi>"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>\<infinity>i. suffix i w \<Turnstile> \<phi>

goal (1 subgoal):
 1. (\<And>i. \<forall>j\<ge>i. suffix j w \<Turnstile> \<phi> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding MOST_nat_le
[PROOF STATE]
proof (prove)
using this:
\<exists>m. \<forall>n\<ge>m. suffix n w \<Turnstile> \<phi>

goal (1 subgoal):
 1. (\<And>i. \<forall>j\<ge>i. suffix j w \<Turnstile> \<phi> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>j\<ge>i. suffix j w \<Turnstile> \<phi>

goal (2 subgoals):
 1. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; \<not> w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>j\<ge>i. suffix j w \<Turnstile> \<phi>

goal (2 subgoals):
 1. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; \<not> w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; \<not> w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
assume "k \<ge> i"
[PROOF STATE]
proof (state)
this:
i \<le> k

goal (2 subgoals):
 1. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; \<not> w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
hence "suffix k w \<Turnstile> \<phi>"
[PROOF STATE]
proof (prove)
using this:
i \<le> k

goal (1 subgoal):
 1. suffix k w \<Turnstile> \<phi>
[PROOF STEP]
using \<open>\<forall>j\<ge>i. suffix j w \<Turnstile> \<phi>\<close>
[PROOF STATE]
proof (prove)
using this:
i \<le> k
\<forall>j\<ge>i. suffix j w \<Turnstile> \<phi>

goal (1 subgoal):
 1. suffix k w \<Turnstile> \<phi>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
suffix k w \<Turnstile> \<phi>

goal (2 subgoals):
 1. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; \<not> w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
hence "\<PP> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} (suffix k w) 0"
[PROOF STATE]
proof (prove)
using this:
suffix k w \<Turnstile> \<phi>

goal (1 subgoal):
 1. \<exists>j. {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} \<Turnstile>\<^sub>P af\<^sub>G \<phi> (prefix j (suffix k w))
[PROOF STEP]
using LTL_FG_suffix
[PROOF STATE]
proof (prove)
using this:
suffix k w \<Turnstile> \<phi>
suffix ?i ?w \<Turnstile> F G ?\<phi> = ?w \<Turnstile> F G ?\<phi>

goal (1 subgoal):
 1. \<exists>j. {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} \<Turnstile>\<^sub>P af\<^sub>G \<phi> (prefix j (suffix k w))
[PROOF STEP]
by (blast dest: ltl_implies_provable[unfolded \<G>\<^sub>F\<^sub>G_alt_def])
[PROOF STATE]
proof (state)
this:
\<exists>j. {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} \<Turnstile>\<^sub>P af\<^sub>G \<phi> (prefix j (suffix k w))

goal (2 subgoals):
 1. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; \<not> w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
hence "\<PP> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w k"
[PROOF STATE]
proof (prove)
using this:
\<exists>j. {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} \<Turnstile>\<^sub>P af\<^sub>G \<phi> (prefix j (suffix k w))

goal (1 subgoal):
 1. \<PP> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w k
[PROOF STEP]
unfolding subsequence_shift
[PROOF STATE]
proof (prove)
using this:
\<exists>j. {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} \<Turnstile>\<^sub>P af\<^sub>G \<phi> (w [k + 0 \<rightarrow> k + j])

goal (1 subgoal):
 1. \<PP> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<PP> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w k

goal (2 subgoals):
 1. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; \<not> w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
i \<le> ?k2 \<Longrightarrow> \<PP> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w ?k2

goal (2 subgoals):
 1. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; \<not> w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
hence "\<PP>\<^sub>\<infinity> \<phi> {G \<psi> | \<psi>. w \<Turnstile> F G \<psi>} w"
[PROOF STATE]
proof (prove)
using this:
i \<le> ?k2 \<Longrightarrow> \<PP> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w ?k2

goal (1 subgoal):
 1. \<PP>\<^sub>\<infinity> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w
[PROOF STEP]
using almost_all_eventually_provable_def[of \<phi> _ w]
[PROOF STATE]
proof (prove)
using this:
i \<le> ?k2 \<Longrightarrow> \<PP> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w ?k2
\<PP>\<^sub>\<infinity> \<phi> ?\<G> w \<equiv> \<forall>\<^sub>\<infinity>i. \<PP> \<phi> ?\<G> w i

goal (1 subgoal):
 1. \<PP>\<^sub>\<infinity> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w
[PROOF STEP]
unfolding MOST_nat_le
[PROOF STATE]
proof (prove)
using this:
i \<le> ?k2 \<Longrightarrow> \<PP> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w ?k2
\<PP>\<^sub>\<infinity> \<phi> ?\<G> w \<equiv> \<exists>m. \<forall>n\<ge>m. \<PP> \<phi> ?\<G> w n

goal (1 subgoal):
 1. \<PP>\<^sub>\<infinity> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<PP>\<^sub>\<infinity> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w

goal (2 subgoals):
 1. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; \<not> w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
hence "\<PP>\<^sub>\<infinity> \<phi> (\<G>\<^sub>F\<^sub>G \<phi> w) w"
[PROOF STATE]
proof (prove)
using this:
\<PP>\<^sub>\<infinity> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w

goal (1 subgoal):
 1. \<PP>\<^sub>\<infinity> \<phi> (\<G>\<^sub>F\<^sub>G \<phi> w) w
[PROOF STEP]
unfolding \<G>\<^sub>F\<^sub>G_alt_def
[PROOF STATE]
proof (prove)
using this:
\<PP>\<^sub>\<infinity> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w

goal (1 subgoal):
 1. \<PP>\<^sub>\<infinity> \<phi> {G \<psi> |\<psi>. G \<psi> \<in> \<^bold>G \<phi> \<and> w \<Turnstile> F G \<psi>} w
[PROOF STEP]
using almost_all_eventually_provable_restrict_to_G
[PROOF STATE]
proof (prove)
using this:
\<PP>\<^sub>\<infinity> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w
\<lbrakk>\<PP>\<^sub>\<infinity> ?\<phi> ?\<G> ?w; Only_G ?\<G>\<rbrakk> \<Longrightarrow> \<PP>\<^sub>\<infinity> ?\<phi> (?\<G> \<inter> \<^bold>G ?\<phi>) ?w

goal (1 subgoal):
 1. \<PP>\<^sub>\<infinity> \<phi> {G \<psi> |\<psi>. G \<psi> \<in> \<^bold>G \<phi> \<and> w \<Turnstile> F G \<psi>} w
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<PP>\<^sub>\<infinity> \<phi> (\<G>\<^sub>F\<^sub>G \<phi> w) w

goal (2 subgoals):
 1. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; \<not> w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<PP>\<^sub>\<infinity> \<phi> (\<G>\<^sub>F\<^sub>G \<phi> w) w

goal (1 subgoal):
 1. closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
using LTLGlobal insert
[PROOF STATE]
proof (prove)
using this:
\<PP>\<^sub>\<infinity> \<phi> (\<G>\<^sub>F\<^sub>G \<phi> w) w
closed (\<G>\<^sub>F\<^sub>G \<phi> w) w
ListMem ?x ?xs \<Longrightarrow> ListMem ?x (?y # ?xs)

goal (1 subgoal):
 1. closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w

goal (1 subgoal):
 1. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; \<not> w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w

goal (9 subgoals):
 1. closed (\<G>\<^sub>F\<^sub>G true w) w
 2. closed (\<G>\<^sub>F\<^sub>G false w) w
 3. \<And>x. closed (\<G>\<^sub>F\<^sub>G p(x) w) w
 4. \<And>x. closed (\<G>\<^sub>F\<^sub>G (np(x)) w) w
 5. \<And>\<phi>1 \<phi>2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi>1 w) w; closed (\<G>\<^sub>F\<^sub>G \<phi>2 w) w\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (\<phi>1 and \<phi>2) w) w
 6. \<And>\<phi>1 \<phi>2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi>1 w) w; closed (\<G>\<^sub>F\<^sub>G \<phi>2 w) w\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (\<phi>1 or \<phi>2) w) w
 7. \<And>\<phi>. closed (\<G>\<^sub>F\<^sub>G \<phi> w) w \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (X \<phi>) w) w
 8. \<And>\<phi>. closed (\<G>\<^sub>F\<^sub>G \<phi> w) w \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (F \<phi>) w) w
 9. \<And>\<phi>1 \<phi>2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi>1 w) w; closed (\<G>\<^sub>F\<^sub>G \<phi>2 w) w\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (\<phi>1 U \<phi>2) w) w
[PROOF STEP]
qed auto


[STATEMENT]
lemma all_final_exceptD:
  "\<lbrakk> all_final_except s Ts; not_final_thread s t \<rbrakk> \<Longrightarrow> t \<in> Ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>all_final_except s Ts; not_final_thread s t\<rbrakk> \<Longrightarrow> t \<in> Ts
[PROOF STEP]
by(auto simp add: all_final_except_def)


[STATEMENT]
lemma deadlockedAcquire_must_wait:
  "\<And>ln. \<lbrakk> thr s t = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s t); ln $ l > 0; must_wait s t (Inl l) (deadlocked s \<union> final_threads s) \<rbrakk>
  \<Longrightarrow> t \<in> deadlocked s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ln. \<lbrakk>thr s t = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s t); 0 < ln $ l; must_wait s t (Inl l) (deadlocked s \<union> final_threads s)\<rbrakk> \<Longrightarrow> t \<in> deadlocked s
[PROOF STEP]
apply(erule must_wait_elims)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ln la t'. \<lbrakk>thr s t = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s t); 0 < ln $ l; Inl l = Inl la; has_lock (locks s $ la) t'; t' \<noteq> t; t' \<in> deadlocked s \<union> final_threads s\<rbrakk> \<Longrightarrow> t \<in> deadlocked s
 2. \<And>ln t'. \<lbrakk>thr s t = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s t); 0 < ln $ l; Inl l = Inr (Inl t'); not_final_thread s t'; t' \<in> deadlocked s \<union> final_threads s\<rbrakk> \<Longrightarrow> t \<in> deadlocked s
 3. \<And>ln t'. \<lbrakk>thr s t = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s t); 0 < ln $ l; Inl l = Inr (Inr t'); all_final_except s (deadlocked s \<union> final_threads s); t' \<notin> interrupts s\<rbrakk> \<Longrightarrow> t \<in> deadlocked s
[PROOF STEP]
apply(erule (2) deadlockedAcquire)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>ln la t'. \<lbrakk>\<not> waiting (wset s t); 0 < ln $ l; Inl l = Inl la; has_lock (locks s $ la) t'; t' \<noteq> t; t' \<in> deadlocked s \<union> final_threads s\<rbrakk> \<Longrightarrow> has_lock (locks s $ l) (?t'4 ln la t')
 2. \<And>ln la t'. \<lbrakk>\<not> waiting (wset s t); 0 < ln $ l; Inl l = Inl la; has_lock (locks s $ la) t'; t' \<noteq> t; t' \<in> deadlocked s \<union> final_threads s\<rbrakk> \<Longrightarrow> ?t'4 ln la t' \<noteq> t
 3. \<And>ln la t'. \<lbrakk>\<not> waiting (wset s t); 0 < ln $ l; Inl l = Inl la; has_lock (locks s $ la) t'; t' \<noteq> t; t' \<in> deadlocked s \<union> final_threads s\<rbrakk> \<Longrightarrow> ?t'4 ln la t' \<in> deadlocked s \<or> ?t'4 ln la t' \<in> final_threads s
 4. \<And>ln t'. \<lbrakk>thr s t = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s t); 0 < ln $ l; Inl l = Inr (Inl t'); not_final_thread s t'; t' \<in> deadlocked s \<union> final_threads s\<rbrakk> \<Longrightarrow> t \<in> deadlocked s
 5. \<And>ln t'. \<lbrakk>thr s t = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s t); 0 < ln $ l; Inl l = Inr (Inr t'); all_final_except s (deadlocked s \<union> final_threads s); t' \<notin> interrupts s\<rbrakk> \<Longrightarrow> t \<in> deadlocked s
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bouncing_ball_flow:
  fixes h::real
  assumes "g < 0" and "h \<ge> 0"
  shows "g < 0 \<Longrightarrow> h \<ge> 0 \<Longrightarrow>
  \<lceil>\<lambda>s. s$1 = h \<and> s$2 = 0\<rceil> \<le> wp
    (LOOP
      ((x\<acute>= (\<lambda>t. f g) & (\<lambda> s. s$1 \<ge> 0) on (\<lambda>s. UNIV) UNIV @ 0);
      (IF (\<lambda> s. s$1 = 0) THEN (2 ::= (\<lambda>s. - s$2)) ELSE skip))
    INV (\<lambda>s. 0 \<le> s$1 \<and> 2 * g * s$1 = 2 * g * h + s$2 * s$2))
  \<lceil>\<lambda>s. 0 \<le> s$1 \<and> s$1 \<le> h\<rceil>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g < 0; 0 \<le> h\<rbrakk> \<Longrightarrow> \<lceil>\<lambda>s. s $ 1 = h \<and> s $ 2 = 0\<rceil> \<subseteq> wp (LOOP x\<acute>=\<lambda>t. f g & \<lambda>s. 0 \<le> s $ 1 on \<lambda>s. UNIV UNIV @ 0 ; (IF (\<lambda>s. s $ 1 = 0) THEN (2 ::= (\<lambda>s. - s $ 2)) ELSE skip) INV (\<lambda>s. 0 \<le> s $ 1 \<and> 2 \<cdot> g \<cdot> s $ 1 = 2 \<cdot> g \<cdot> h + s $ 2 \<cdot> s $ 2) ) \<lceil>\<lambda>s. 0 \<le> s $ 1 \<and> s $ 1 \<le> h\<rceil>
[PROOF STEP]
apply(rule wp_loopI, simp_all add: local_flow.wp_g_ode_subset[OF local_flow_ball])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>g < 0; 0 \<le> h\<rbrakk> \<Longrightarrow> \<forall>s. 0 \<le> s $ 1 \<and> 2 \<cdot> g \<cdot> s $ 1 = 2 \<cdot> g \<cdot> h + s $ 2 \<cdot> s $ 2 \<longrightarrow> s $ 1 \<le> h
 2. \<lbrakk>g < 0; 0 \<le> h\<rbrakk> \<Longrightarrow> \<forall>s. 0 \<le> s $ 1 \<and> 2 \<cdot> g \<cdot> s $ 1 = 2 \<cdot> g \<cdot> h + s $ 2 \<cdot> s $ 2 \<longrightarrow> (\<forall>t. (\<forall>\<tau>\<le>t. 0 \<le> g \<cdot> \<tau>\<^sup>2 / 2 + s $ 2 \<cdot> \<tau> + s $ 1) \<longrightarrow> (g \<cdot> t\<^sup>2 / 2 + s $ 2 \<cdot> t + s $ 1 = 0 \<longrightarrow> 2 \<cdot> g \<cdot> h + (g \<cdot> t \<cdot> (g \<cdot> t + s $ 2) + s $ 2 \<cdot> (g \<cdot> t + s $ 2)) = 0) \<and> (g \<cdot> t\<^sup>2 / 2 + s $ 2 \<cdot> t + s $ 1 = 0 \<or> 2 \<cdot> g \<cdot> (g \<cdot> t\<^sup>2 / 2 + s $ 2 \<cdot> t + s $ 1) = 2 \<cdot> g \<cdot> h + (g \<cdot> t \<cdot> (g \<cdot> t + s $ 2) + s $ 2 \<cdot> (g \<cdot> t + s $ 2))))
[PROOF STEP]
by (auto simp: bb_real_arith)


[STATEMENT]
lemma irreflclpE [elim!]:
  assumes "r\<^sup>\<noteq>\<^sup>\<noteq> a b"
  obtains "r a b" "a \<noteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>r a b; a \<noteq> b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
r\<^sup>\<noteq>\<^sup>\<noteq> a b

goal (1 subgoal):
 1. (\<lbrakk>r a b; a \<noteq> b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(simp add: irreflclp_def)


[STATEMENT]
lemma torder_on_restrictPI':
  "\<lbrakk> torder_on A r; B = A \<inter> C \<rbrakk> \<Longrightarrow> torder_on B (r |` C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>torder_on A r; B = A \<inter> C\<rbrakk> \<Longrightarrow> torder_on B (r |` C)
[PROOF STEP]
by(simp add: torder_on_restrictPI)


[STATEMENT]
lemma doesnt_modify_annos:
  "doesnt_modify c x \<Longrightarrow> doesnt_modify (c \<otimes> annos) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. doesnt_modify c x \<Longrightarrow> doesnt_modify (c \<otimes> annos) x
[PROOF STEP]
unfolding doesnt_modify_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>mds mem c' mds' mem'. \<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle> \<longrightarrow> mem x = mem' x \<and> dma mem x = dma mem' x \<Longrightarrow> \<forall>mds mem c' mds' mem'. \<langle>c \<otimes> annos, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle> \<longrightarrow> mem x = mem' x \<and> dma mem x = dma mem' x
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>mds mem c' mds' mem'. \<lbrakk>\<forall>mds mem c' mds' mem'. \<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle> \<longrightarrow> mem x = mem' x \<and> dma mem x = dma mem' x; \<langle>c \<otimes> annos, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>\<rbrakk> \<Longrightarrow> mem x = mem' x \<and> dma mem x = dma mem' x
[PROOF STEP]
apply (induct annos)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>mds mem c' mds' mem'. \<lbrakk>\<forall>mds mem c' mds' mem'. \<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle> \<longrightarrow> mem x = mem' x \<and> dma mem x = dma mem' x; \<langle>c \<otimes> [], mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>\<rbrakk> \<Longrightarrow> mem x = mem' x \<and> dma mem x = dma mem' x
 2. \<And>a annos mds mem c' mds' mem'. \<lbrakk>\<And>mds mem c' mds' mem'. \<lbrakk>\<forall>mds mem c' mds' mem'. \<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle> \<longrightarrow> mem x = mem' x \<and> dma mem x = dma mem' x; \<langle>c \<otimes> annos, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>\<rbrakk> \<Longrightarrow> mem x = mem' x \<and> dma mem x = dma mem' x; \<forall>mds mem c' mds' mem'. \<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle> \<longrightarrow> mem x = mem' x \<and> dma mem x = dma mem' x; \<langle>c \<otimes> (a # annos), mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>\<rbrakk> \<Longrightarrow> mem x = mem' x \<and> dma mem x = dma mem' x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a annos mds mem c' mds' mem'. \<lbrakk>\<And>mds mem c' mds' mem'. \<lbrakk>\<forall>mds mem c' mds' mem'. \<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle> \<longrightarrow> mem x = mem' x \<and> dma mem x = dma mem' x; \<langle>c \<otimes> annos, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>\<rbrakk> \<Longrightarrow> mem x = mem' x \<and> dma mem x = dma mem' x; \<forall>mds mem c' mds' mem'. \<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle> \<longrightarrow> mem x = mem' x \<and> dma mem x = dma mem' x; \<langle>c \<otimes> (a # annos), mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>\<rbrakk> \<Longrightarrow> mem x = mem' x \<and> dma mem x = dma mem' x
[PROOF STEP]
by (metis annotate.simps(2) upd_elim)


[STATEMENT]
lemma pull_up_configuration_senior:
  "\<lbrakk>x \<in> configuration q n; y \<in> configuration q n\<rbrakk> \<Longrightarrow> senior x n = senior y n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> configuration q n; y \<in> configuration q n\<rbrakk> \<Longrightarrow> senior x n = senior y n
[PROOF STEP]
by force


[STATEMENT]
lemma state_rank_in_function_set:
  shows "(\<lambda>q. state_rank q t) \<in> {f. (\<forall>x. x \<notin> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x = None) \<and>
      (\<forall>x. x \<in> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x \<in> {None} \<union> Some ` {0..<max_rank})}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>q. state_rank q t) \<in> {f. (\<forall>x. x \<notin> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x = None) \<and> (\<forall>x. x \<in> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x \<in> {None} \<union> Some ` {0..<max_rank})}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>q. state_rank q t) \<in> {f. (\<forall>x. x \<notin> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x = None) \<and> (\<forall>x. x \<in> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x \<in> {None} \<union> Some ` {0..<max_rank})}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>q. state_rank q t) \<in> {f. (\<forall>x. x \<notin> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x = None) \<and> (\<forall>x. x \<in> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x \<in> {None} \<union> Some ` {0..<max_rank})}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>q. state_rank q t) \<in> {f. (\<forall>x. x \<notin> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x = None) \<and> (\<forall>x. x \<in> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x \<in> {None} \<union> Some ` {0..<max_rank})}
[PROOF STEP]
assume "x \<notin> reach \<Sigma> \<delta> q\<^sub>0"
[PROOF STATE]
proof (state)
this:
x \<notin> reach \<Sigma> \<delta> q\<^sub>0

goal (1 subgoal):
 1. (\<lambda>q. state_rank q t) \<in> {f. (\<forall>x. x \<notin> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x = None) \<and> (\<forall>x. x \<in> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x \<in> {None} \<union> Some ` {0..<max_rank})}
[PROOF STEP]
hence "\<And>token. x \<noteq> token_run token t"
[PROOF STATE]
proof (prove)
using this:
x \<notin> reach \<Sigma> \<delta> q\<^sub>0

goal (1 subgoal):
 1. \<And>token. x \<noteq> token_run token t
[PROOF STEP]
unfolding reach_def token_run.simps
[PROOF STATE]
proof (prove)
using this:
x \<notin> {run \<delta> q\<^sub>0 w n |w n. range w \<subseteq> \<Sigma>}

goal (1 subgoal):
 1. \<And>token. x \<noteq> run \<delta> q\<^sub>0 (suffix token w) (t - token)
[PROOF STEP]
using bounded_w
[PROOF STATE]
proof (prove)
using this:
x \<notin> {run \<delta> q\<^sub>0 w n |w n. range w \<subseteq> \<Sigma>}
range w \<subseteq> \<Sigma>

goal (1 subgoal):
 1. \<And>token. x \<noteq> run \<delta> q\<^sub>0 (suffix token w) (t - token)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x \<noteq> token_run ?token t

goal (1 subgoal):
 1. (\<lambda>q. state_rank q t) \<in> {f. (\<forall>x. x \<notin> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x = None) \<and> (\<forall>x. x \<in> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x \<in> {None} \<union> Some ` {0..<max_rank})}
[PROOF STEP]
hence "state_rank x t = None"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> token_run ?token t

goal (1 subgoal):
 1. state_rank x t = None
[PROOF STEP]
using pull_up_configuration_state_rank
[PROOF STATE]
proof (prove)
using this:
x \<noteq> token_run ?token t
configuration ?q ?n = {} \<Longrightarrow> state_rank ?q ?n = None

goal (1 subgoal):
 1. state_rank x t = None
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
state_rank x t = None

goal (1 subgoal):
 1. (\<lambda>q. state_rank q t) \<in> {f. (\<forall>x. x \<notin> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x = None) \<and> (\<forall>x. x \<in> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x \<in> {None} \<union> Some ` {0..<max_rank})}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 \<notin> reach \<Sigma> \<delta> q\<^sub>0 \<Longrightarrow> state_rank ?x2 t = None

goal (1 subgoal):
 1. (\<lambda>q. state_rank q t) \<in> {f. (\<forall>x. x \<notin> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x = None) \<and> (\<forall>x. x \<in> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x \<in> {None} \<union> Some ` {0..<max_rank})}
[PROOF STEP]
with state_rank_range
[PROOF STATE]
proof (chain)
picking this:
state_rank ?q ?n \<in> {None} \<union> Some ` {0..<max_rank}
?x2 \<notin> reach \<Sigma> \<delta> q\<^sub>0 \<Longrightarrow> state_rank ?x2 t = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
state_rank ?q ?n \<in> {None} \<union> Some ` {0..<max_rank}
?x2 \<notin> reach \<Sigma> \<delta> q\<^sub>0 \<Longrightarrow> state_rank ?x2 t = None

goal (1 subgoal):
 1. (\<lambda>q. state_rank q t) \<in> {f. (\<forall>x. x \<notin> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x = None) \<and> (\<forall>x. x \<in> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x \<in> {None} \<union> Some ` {0..<max_rank})}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>q. state_rank q t) \<in> {f. (\<forall>x. x \<notin> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x = None) \<and> (\<forall>x. x \<in> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x \<in> {None} \<union> Some ` {0..<max_rank})}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_Fvars_fmla[simp]:
  fixes A :: fmla
  shows "finite (Fvars A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (Fvars A)
[PROOF STEP]
by (induct A rule: fmla.induct) auto


[STATEMENT]
lemma [synth_rules]: "INTRO_KD (R\<^sup>k) (R\<^sup>k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. INTRO_KD (R\<^sup>k) (R\<^sup>k)
[PROOF STEP]
by simp


[STATEMENT]
lemma "iface_toString ''in: '' (Iface ''+'') = ''''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iface_toString ''in: '' (Iface ''+'') = []
[PROOF STEP]
by eval


[STATEMENT]
lemma modelAppendTautologicalFormula:
fixes
  F :: Formula and F' :: Formula
assumes
  "model valuation F" "\<forall> c. c el F' \<longrightarrow> clauseTautology c"
  "vars valuation \<supseteq> vars F \<union> vars F'"
shows
  "model valuation (F @ F')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. model valuation (F @ F')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
model valuation F
\<forall>c. c el F' \<longrightarrow> clauseTautology c
vars F \<union> vars F' \<subseteq> vars valuation

goal (1 subgoal):
 1. model valuation (F @ F')
[PROOF STEP]
proof (induct F')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>model valuation F; \<forall>c. c el [] \<longrightarrow> clauseTautology c; vars F \<union> vars [] \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ [])
 2. \<And>a F'. \<lbrakk>\<lbrakk>model valuation F; \<forall>c. c el F' \<longrightarrow> clauseTautology c; vars F \<union> vars F' \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ F'); model valuation F; \<forall>c. c el a # F' \<longrightarrow> clauseTautology c; vars F \<union> vars (a # F') \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ a # F')
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
model valuation F
\<forall>c. c el [] \<longrightarrow> clauseTautology c
vars F \<union> vars [] \<subseteq> vars valuation

goal (2 subgoals):
 1. \<lbrakk>model valuation F; \<forall>c. c el [] \<longrightarrow> clauseTautology c; vars F \<union> vars [] \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ [])
 2. \<And>a F'. \<lbrakk>\<lbrakk>model valuation F; \<forall>c. c el F' \<longrightarrow> clauseTautology c; vars F \<union> vars F' \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ F'); model valuation F; \<forall>c. c el a # F' \<longrightarrow> clauseTautology c; vars F \<union> vars (a # F') \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ a # F')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
model valuation F
\<forall>c. c el [] \<longrightarrow> clauseTautology c
vars F \<union> vars [] \<subseteq> vars valuation

goal (1 subgoal):
 1. model valuation (F @ [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
model valuation (F @ [])

goal (1 subgoal):
 1. \<And>a F'. \<lbrakk>\<lbrakk>model valuation F; \<forall>c. c el F' \<longrightarrow> clauseTautology c; vars F \<union> vars F' \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ F'); model valuation F; \<forall>c. c el a # F' \<longrightarrow> clauseTautology c; vars F \<union> vars (a # F') \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ a # F')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a F'. \<lbrakk>\<lbrakk>model valuation F; \<forall>c. c el F' \<longrightarrow> clauseTautology c; vars F \<union> vars F' \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ F'); model valuation F; \<forall>c. c el a # F' \<longrightarrow> clauseTautology c; vars F \<union> vars (a # F') \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ a # F')
[PROOF STEP]
case (Cons c F'')
[PROOF STATE]
proof (state)
this:
\<lbrakk>model valuation F; \<forall>c. c el F'' \<longrightarrow> clauseTautology c; vars F \<union> vars F'' \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ F'')
model valuation F
\<forall>ca. ca el c # F'' \<longrightarrow> clauseTautology ca
vars F \<union> vars (c # F'') \<subseteq> vars valuation

goal (1 subgoal):
 1. \<And>a F'. \<lbrakk>\<lbrakk>model valuation F; \<forall>c. c el F' \<longrightarrow> clauseTautology c; vars F \<union> vars F' \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ F'); model valuation F; \<forall>c. c el a # F' \<longrightarrow> clauseTautology c; vars F \<union> vars (a # F') \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ a # F')
[PROOF STEP]
hence "model valuation (F @ F'')"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>model valuation F; \<forall>c. c el F'' \<longrightarrow> clauseTautology c; vars F \<union> vars F'' \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ F'')
model valuation F
\<forall>ca. ca el c # F'' \<longrightarrow> clauseTautology ca
vars F \<union> vars (c # F'') \<subseteq> vars valuation

goal (1 subgoal):
 1. model valuation (F @ F'')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
model valuation (F @ F'')

goal (1 subgoal):
 1. \<And>a F'. \<lbrakk>\<lbrakk>model valuation F; \<forall>c. c el F' \<longrightarrow> clauseTautology c; vars F \<union> vars F' \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ F'); model valuation F; \<forall>c. c el a # F' \<longrightarrow> clauseTautology c; vars F \<union> vars (a # F') \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ a # F')
[PROOF STEP]
hence "model valuation ((F @ F'') @ [c])"
[PROOF STATE]
proof (prove)
using this:
model valuation (F @ F'')

goal (1 subgoal):
 1. model valuation ((F @ F'') @ [c])
[PROOF STEP]
using Cons(3)
[PROOF STATE]
proof (prove)
using this:
model valuation (F @ F'')
\<forall>ca. ca el c # F'' \<longrightarrow> clauseTautology ca

goal (1 subgoal):
 1. model valuation ((F @ F'') @ [c])
[PROOF STEP]
using Cons(4)
[PROOF STATE]
proof (prove)
using this:
model valuation (F @ F'')
\<forall>ca. ca el c # F'' \<longrightarrow> clauseTautology ca
vars F \<union> vars (c # F'') \<subseteq> vars valuation

goal (1 subgoal):
 1. model valuation ((F @ F'') @ [c])
[PROOF STEP]
using modelAppendTautology[of "valuation" "F @ F''" "c"]
[PROOF STATE]
proof (prove)
using this:
model valuation (F @ F'')
\<forall>ca. ca el c # F'' \<longrightarrow> clauseTautology ca
vars F \<union> vars (c # F'') \<subseteq> vars valuation
\<lbrakk>model valuation (F @ F''); clauseTautology c; vars (F @ F'') \<union> vars c \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation ((F @ F'') @ [c])

goal (1 subgoal):
 1. model valuation ((F @ F'') @ [c])
[PROOF STEP]
using varsAppendFormulae[of "F" "F''"]
[PROOF STATE]
proof (prove)
using this:
model valuation (F @ F'')
\<forall>ca. ca el c # F'' \<longrightarrow> clauseTautology ca
vars F \<union> vars (c # F'') \<subseteq> vars valuation
\<lbrakk>model valuation (F @ F''); clauseTautology c; vars (F @ F'') \<union> vars c \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation ((F @ F'') @ [c])
vars (F @ F'') = vars F \<union> vars F''

goal (1 subgoal):
 1. model valuation ((F @ F'') @ [c])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
model valuation ((F @ F'') @ [c])

goal (1 subgoal):
 1. \<And>a F'. \<lbrakk>\<lbrakk>model valuation F; \<forall>c. c el F' \<longrightarrow> clauseTautology c; vars F \<union> vars F' \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ F'); model valuation F; \<forall>c. c el a # F' \<longrightarrow> clauseTautology c; vars F \<union> vars (a # F') \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ a # F')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
model valuation ((F @ F'') @ [c])

goal (1 subgoal):
 1. model valuation (F @ c # F'')
[PROOF STEP]
by (simp add: formulaTrueAppend)
[PROOF STATE]
proof (state)
this:
model valuation (F @ c # F'')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma len_alt: "len x = (LEAST i. x < 2 ^ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. len x = (LEAST i. x < 2 ^ i)
[PROOF STEP]
proof (rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. len x \<le> (LEAST i. x < 2 ^ i)
 2. (LEAST i. x < 2 ^ i) \<le> len x
[PROOF STEP]
show "len x \<le> (LEAST i. x < 2 ^ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. len x \<le> (LEAST i. x < 2 ^ i)
[PROOF STEP]
unfolding len_le_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < 2 ^ (LEAST i. x < 2 ^ i)
[PROOF STEP]
by (rule LeastI) (rule less_pow2_len)
[PROOF STATE]
proof (state)
this:
len x \<le> (LEAST i. x < 2 ^ i)

goal (1 subgoal):
 1. (LEAST i. x < 2 ^ i) \<le> len x
[PROOF STEP]
qed (auto intro: Least_le)


[STATEMENT]
lemma map_pair_automaton:
  "pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B) =
   fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B)" (is "?Ls = ?Rs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B) = fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B) = fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B)
[PROOF STEP]
let ?ls = "pair_rule \<circ> map_prod (map_ta_rule id f) (map_ta_rule id g)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B) = fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B)
[PROOF STEP]
let ?rs = "map_ta_rule id (\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> pair_rule"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B) = fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B)
[PROOF STEP]
have *: "(\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> lift_Some_None = lift_Some_None \<circ> f"
    "(\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> lift_None_Some = lift_None_Some \<circ> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> lift_Some_None = lift_Some_None \<circ> f &&& (\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> lift_None_Some = lift_None_Some \<circ> g
[PROOF STEP]
by (auto simp: comp_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> lift_Some_None = lift_Some_None \<circ> f
(\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> lift_None_Some = lift_None_Some \<circ> g

goal (1 subgoal):
 1. pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B) = fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B)
[PROOF STEP]
have "?ls x = ?rs x" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pair_rule \<circ> map_prod (map_ta_rule id f) (map_ta_rule id g)) x = (map_ta_rule id (\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> pair_rule) x
[PROOF STEP]
by (cases x) (auto simp: ta_rule.map_sel)
[PROOF STATE]
proof (state)
this:
(pair_rule \<circ> map_prod (map_ta_rule id f) (map_ta_rule id g)) ?x3 = (map_ta_rule id (\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> pair_rule) ?x3

goal (1 subgoal):
 1. pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B) = fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(pair_rule \<circ> map_prod (map_ta_rule id f) (map_ta_rule id g)) ?x3 = (map_ta_rule id (\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> pair_rule) ?x3
[PROOF STEP]
have [simp]: "?ls = ?rs"
[PROOF STATE]
proof (prove)
using this:
(pair_rule \<circ> map_prod (map_ta_rule id f) (map_ta_rule id g)) ?x3 = (map_ta_rule id (\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> pair_rule) ?x3

goal (1 subgoal):
 1. pair_rule \<circ> map_prod (map_ta_rule id f) (map_ta_rule id g) = map_ta_rule id (\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> pair_rule
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pair_rule \<circ> map_prod (map_ta_rule id f) (map_ta_rule id g) = map_ta_rule id (\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> pair_rule

goal (1 subgoal):
 1. pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B) = fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pair_rule \<circ> map_prod (map_ta_rule id f) (map_ta_rule id g) = map_ta_rule id (\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> pair_rule
[PROOF STEP]
have "rules ?Ls = rules ?Rs"
[PROOF STATE]
proof (prove)
using this:
pair_rule \<circ> map_prod (map_ta_rule id f) (map_ta_rule id g) = map_ta_rule id (\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> pair_rule

goal (1 subgoal):
 1. rules (pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B)) = rules (fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B))
[PROOF STEP]
unfolding pair_automaton_def fmap_funs_ta_def
[PROOF STATE]
proof (prove)
using this:
pair_rule \<circ> map_prod (map_ta_rule id f) (map_ta_rule id g) = map_ta_rule id (\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> pair_rule

goal (1 subgoal):
 1. rules (TA (map_ta_rule lift_Some_None lift_Some_None |`| rules (TA (map_ta_rule id f |`| rules A) (eps A)) |\<union>| map_ta_rule lift_None_Some lift_None_Some |`| rules (TA (map_ta_rule id g |`| rules B) (eps B)) |\<union>| pair_rule |`| (rules (TA (map_ta_rule id f |`| rules A) (eps A)) |\<times>| rules (TA (map_ta_rule id g |`| rules B) (eps B)))) (pair_eps (TA (map_ta_rule id f |`| rules A) (eps A)) (TA (map_ta_rule id g |`| rules B) (eps B)) |\<union>| map_both prod.swap |`| pair_eps (TA (map_ta_rule id g |`| rules B) (eps B)) (TA (map_ta_rule id f |`| rules A) (eps A)))) = rules (TA (map_ta_rule id (\<lambda>(a, b). (map_option f a, map_option g b)) |`| rules (TA (map_ta_rule lift_Some_None lift_Some_None |`| rules A |\<union>| map_ta_rule lift_None_Some lift_None_Some |`| rules B |\<union>| pair_rule |`| (rules A |\<times>| rules B)) (pair_eps A B |\<union>| map_both prod.swap |`| pair_eps B A))) (eps (TA (map_ta_rule lift_Some_None lift_Some_None |`| rules A |\<union>| map_ta_rule lift_None_Some lift_None_Some |`| rules B |\<union>| pair_rule |`| (rules A |\<times>| rules B)) (pair_eps A B |\<union>| map_both prod.swap |`| pair_eps B A))))
[PROOF STEP]
by (simp add: fimage_funion map_ta_rule_comp * map_prod_ftimes)
[PROOF STATE]
proof (state)
this:
rules (pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B)) = rules (fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B))

goal (1 subgoal):
 1. pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B) = fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rules (pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B)) = rules (fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B))

goal (1 subgoal):
 1. pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B) = fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B)
[PROOF STEP]
have "eps ?Ls = eps ?Rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eps (pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B)) = eps (fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B))
[PROOF STEP]
unfolding pair_automaton_def fmap_funs_ta_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eps (TA (map_ta_rule lift_Some_None lift_Some_None |`| rules (TA (map_ta_rule id f |`| rules A) (eps A)) |\<union>| map_ta_rule lift_None_Some lift_None_Some |`| rules (TA (map_ta_rule id g |`| rules B) (eps B)) |\<union>| pair_rule |`| (rules (TA (map_ta_rule id f |`| rules A) (eps A)) |\<times>| rules (TA (map_ta_rule id g |`| rules B) (eps B)))) (pair_eps (TA (map_ta_rule id f |`| rules A) (eps A)) (TA (map_ta_rule id g |`| rules B) (eps B)) |\<union>| map_both prod.swap |`| pair_eps (TA (map_ta_rule id g |`| rules B) (eps B)) (TA (map_ta_rule id f |`| rules A) (eps A)))) = eps (TA (map_ta_rule id (\<lambda>(a, b). (map_option f a, map_option g b)) |`| rules (TA (map_ta_rule lift_Some_None lift_Some_None |`| rules A |\<union>| map_ta_rule lift_None_Some lift_None_Some |`| rules B |\<union>| pair_rule |`| (rules A |\<times>| rules B)) (pair_eps A B |\<union>| map_both prod.swap |`| pair_eps B A))) (eps (TA (map_ta_rule lift_Some_None lift_Some_None |`| rules A |\<union>| map_ta_rule lift_None_Some lift_None_Some |`| rules B |\<union>| pair_rule |`| (rules A |\<times>| rules B)) (pair_eps A B |\<union>| map_both prod.swap |`| pair_eps B A))))
[PROOF STEP]
by (simp add: fimage_funion \<Q>_def)
[PROOF STATE]
proof (state)
this:
eps (pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B)) = eps (fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B))

goal (1 subgoal):
 1. pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B) = fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rules (pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B)) = rules (fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B))
eps (pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B)) = eps (fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
rules (pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B)) = rules (fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B))
eps (pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B)) = eps (fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B))

goal (1 subgoal):
 1. pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B) = fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B)
[PROOF STEP]
by (intro TA_equalityI) simp
[PROOF STATE]
proof (state)
this:
pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B) = fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stut_fun3: "\<lbrakk>STUTINV X;STUTINV Y;STUTINV Z\<rbrakk> \<Longrightarrow> STUTINV (f <X,Y,Z>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>STUTINV X; STUTINV Y; STUTINV Z\<rbrakk> \<Longrightarrow> STUTINV f<X, Y, Z>
[PROOF STEP]
by (simp add: stutinv_def)


[STATEMENT]
lemma Nonce_Exp: "Nonce X \<noteq> Exp  X' Y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Nonce X \<noteq> Exp X' Y'
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma Aenc_Pair: "Aenc X Y \<noteq> Pair  X' Y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Aenc X Y \<noteq> Messages.Pair X' Y'
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma init_mapstate_Some_aodv_init [elim]:
  assumes "s \<in> init (pnet np p)"
      and "netmap s i = Some v"
    shows "v \<in> init (np i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> init (np i)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
s \<in> init (pnet np p)
netmap s i = Some v

goal (1 subgoal):
 1. v \<in> init (np i)
[PROOF STEP]
proof (induction p arbitrary: s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ia R s. \<lbrakk>s \<in> init (pnet np \<langle>ia; R\<rangle>); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
 2. \<And>p1 p2 s. \<lbrakk>\<And>s. \<lbrakk>s \<in> init (pnet np p1); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); \<And>s. \<lbrakk>s \<in> init (pnet np p2); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); s \<in> init (pnet np (p1 \<parallel> p2)); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
fix ii R s
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ia R s. \<lbrakk>s \<in> init (pnet np \<langle>ia; R\<rangle>); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
 2. \<And>p1 p2 s. \<lbrakk>\<And>s. \<lbrakk>s \<in> init (pnet np p1); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); \<And>s. \<lbrakk>s \<in> init (pnet np p2); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); s \<in> init (pnet np (p1 \<parallel> p2)); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
assume "s \<in> init (pnet np \<langle>ii; R\<rangle>)"
       and "netmap s i = Some v"
[PROOF STATE]
proof (state)
this:
s \<in> init (pnet np \<langle>ii; R\<rangle>)
netmap s i = Some v

goal (2 subgoals):
 1. \<And>ia R s. \<lbrakk>s \<in> init (pnet np \<langle>ia; R\<rangle>); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
 2. \<And>p1 p2 s. \<lbrakk>\<And>s. \<lbrakk>s \<in> init (pnet np p1); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); \<And>s. \<lbrakk>s \<in> init (pnet np p2); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); s \<in> init (pnet np (p1 \<parallel> p2)); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
from this(1)
[PROOF STATE]
proof (chain)
picking this:
s \<in> init (pnet np \<langle>ii; R\<rangle>)
[PROOF STEP]
obtain ns where s: "s = NodeS ii ns R"
      and ns: "ns \<in> init (np ii)"
[PROOF STATE]
proof (prove)
using this:
s \<in> init (pnet np \<langle>ii; R\<rangle>)

goal (1 subgoal):
 1. (\<And>ns. \<lbrakk>s = NodeS ii ns R; ns \<in> init (np ii)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
s = NodeS ii ns R
ns \<in> init (np ii)

goal (2 subgoals):
 1. \<And>ia R s. \<lbrakk>s \<in> init (pnet np \<langle>ia; R\<rangle>); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
 2. \<And>p1 p2 s. \<lbrakk>\<And>s. \<lbrakk>s \<in> init (pnet np p1); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); \<And>s. \<lbrakk>s \<in> init (pnet np p2); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); s \<in> init (pnet np (p1 \<parallel> p2)); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
from s and \<open>netmap s i = Some v\<close>
[PROOF STATE]
proof (chain)
picking this:
s = NodeS ii ns R
netmap s i = Some v
[PROOF STEP]
have "i = ii"
[PROOF STATE]
proof (prove)
using this:
s = NodeS ii ns R
netmap s i = Some v

goal (1 subgoal):
 1. i = ii
[PROOF STEP]
by simp (metis domI domIff)
[PROOF STATE]
proof (state)
this:
i = ii

goal (2 subgoals):
 1. \<And>ia R s. \<lbrakk>s \<in> init (pnet np \<langle>ia; R\<rangle>); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
 2. \<And>p1 p2 s. \<lbrakk>\<And>s. \<lbrakk>s \<in> init (pnet np p1); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); \<And>s. \<lbrakk>s \<in> init (pnet np p2); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); s \<in> init (pnet np (p1 \<parallel> p2)); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
with s ns
[PROOF STATE]
proof (chain)
picking this:
s = NodeS ii ns R
ns \<in> init (np ii)
i = ii
[PROOF STEP]
show "v \<in> init (np i)"
[PROOF STATE]
proof (prove)
using this:
s = NodeS ii ns R
ns \<in> init (np ii)
i = ii

goal (1 subgoal):
 1. v \<in> init (np i)
[PROOF STEP]
using \<open>netmap s i = Some v\<close>
[PROOF STATE]
proof (prove)
using this:
s = NodeS ii ns R
ns \<in> init (np ii)
i = ii
netmap s i = Some v

goal (1 subgoal):
 1. v \<in> init (np i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v \<in> init (np i)

goal (1 subgoal):
 1. \<And>p1 p2 s. \<lbrakk>\<And>s. \<lbrakk>s \<in> init (pnet np p1); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); \<And>s. \<lbrakk>s \<in> init (pnet np p2); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); s \<in> init (pnet np (p1 \<parallel> p2)); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p1 p2 s. \<lbrakk>\<And>s. \<lbrakk>s \<in> init (pnet np p1); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); \<And>s. \<lbrakk>s \<in> init (pnet np p2); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); s \<in> init (pnet np (p1 \<parallel> p2)); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
fix p1 p2 s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p1 p2 s. \<lbrakk>\<And>s. \<lbrakk>s \<in> init (pnet np p1); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); \<And>s. \<lbrakk>s \<in> init (pnet np p2); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); s \<in> init (pnet np (p1 \<parallel> p2)); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
assume IH1: "\<And>s. s \<in> init (pnet np p1) \<Longrightarrow> netmap s i = Some v \<Longrightarrow> v \<in> init (np i)"
       and IH2: "\<And>s. s \<in> init (pnet np p2) \<Longrightarrow> netmap s i = Some v \<Longrightarrow> v \<in> init (np i)"
       and "s \<in> init (pnet np (p1 \<parallel> p2))"
       and "netmap s i = Some v"
[PROOF STATE]
proof (state)
this:
\<lbrakk>?s \<in> init (pnet np p1); netmap ?s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
\<lbrakk>?s \<in> init (pnet np p2); netmap ?s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
s \<in> init (pnet np (p1 \<parallel> p2))
netmap s i = Some v

goal (1 subgoal):
 1. \<And>p1 p2 s. \<lbrakk>\<And>s. \<lbrakk>s \<in> init (pnet np p1); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); \<And>s. \<lbrakk>s \<in> init (pnet np p2); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); s \<in> init (pnet np (p1 \<parallel> p2)); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
from this(3)
[PROOF STATE]
proof (chain)
picking this:
s \<in> init (pnet np (p1 \<parallel> p2))
[PROOF STEP]
obtain s1 s2 where "s = SubnetS s1 s2"
                                and "s1 \<in> init (pnet np p1)"
                                and "s2 \<in> init (pnet np p2)"
[PROOF STATE]
proof (prove)
using this:
s \<in> init (pnet np (p1 \<parallel> p2))

goal (1 subgoal):
 1. (\<And>s1 s2. \<lbrakk>s = SubnetS s1 s2; s1 \<in> init (pnet np p1); s2 \<in> init (pnet np p2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s = SubnetS s1 s2
s1 \<in> init (pnet np p1)
s2 \<in> init (pnet np p2)

goal (1 subgoal):
 1. \<And>p1 p2 s. \<lbrakk>\<And>s. \<lbrakk>s \<in> init (pnet np p1); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); \<And>s. \<lbrakk>s \<in> init (pnet np p2); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); s \<in> init (pnet np (p1 \<parallel> p2)); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
from this(1) and \<open>netmap s i = Some v\<close>
[PROOF STATE]
proof (chain)
picking this:
s = SubnetS s1 s2
netmap s i = Some v
[PROOF STEP]
have "netmap s1 i = Some v \<or> netmap s2 i = Some v"
[PROOF STATE]
proof (prove)
using this:
s = SubnetS s1 s2
netmap s i = Some v

goal (1 subgoal):
 1. netmap s1 i = Some v \<or> netmap s2 i = Some v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
netmap s1 i = Some v \<or> netmap s2 i = Some v

goal (1 subgoal):
 1. \<And>p1 p2 s. \<lbrakk>\<And>s. \<lbrakk>s \<in> init (pnet np p1); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); \<And>s. \<lbrakk>s \<in> init (pnet np p2); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); s \<in> init (pnet np (p1 \<parallel> p2)); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
thus "v \<in> init (np i)"
[PROOF STATE]
proof (prove)
using this:
netmap s1 i = Some v \<or> netmap s2 i = Some v

goal (1 subgoal):
 1. v \<in> init (np i)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. netmap s1 i = Some v \<Longrightarrow> v \<in> init (np i)
 2. netmap s2 i = Some v \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
assume "netmap s1 i = Some v"
[PROOF STATE]
proof (state)
this:
netmap s1 i = Some v

goal (2 subgoals):
 1. netmap s1 i = Some v \<Longrightarrow> v \<in> init (np i)
 2. netmap s2 i = Some v \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
with \<open>s1 \<in> init (pnet np p1)\<close>
[PROOF STATE]
proof (chain)
picking this:
s1 \<in> init (pnet np p1)
netmap s1 i = Some v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s1 \<in> init (pnet np p1)
netmap s1 i = Some v

goal (1 subgoal):
 1. v \<in> init (np i)
[PROOF STEP]
by (rule IH1)
[PROOF STATE]
proof (state)
this:
v \<in> init (np i)

goal (1 subgoal):
 1. netmap s2 i = Some v \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. netmap s2 i = Some v \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
assume "netmap s2 i = Some v"
[PROOF STATE]
proof (state)
this:
netmap s2 i = Some v

goal (1 subgoal):
 1. netmap s2 i = Some v \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
with \<open>s2 \<in> init (pnet np p2)\<close>
[PROOF STATE]
proof (chain)
picking this:
s2 \<in> init (pnet np p2)
netmap s2 i = Some v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s2 \<in> init (pnet np p2)
netmap s2 i = Some v

goal (1 subgoal):
 1. v \<in> init (np i)
[PROOF STEP]
by (rule IH2)
[PROOF STATE]
proof (state)
this:
v \<in> init (np i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
v \<in> init (np i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma one_before_two_2:
  "alw (\<lambda>x. statename (shd (stl x)) = Some 2 \<longrightarrow> statename (shd x) = Some 1) (make_full_observation drinks (Some 2) r [r $ 1] x2a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alw (\<lambda>x. state_eq (Some 2) (stl x) \<longrightarrow> state_eq (Some 1) x) (make_full_observation drinks (Some 2) r [r $ 1] x2a)
[PROOF STEP]
proof(coinduction)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>xs. make_full_observation drinks (Some 2) r [r $ 1] x2a = xs \<and> (state_eq (Some 2) (stl xs) \<longrightarrow> state_eq (Some 1) xs) \<and> (stl xs = make_full_observation drinks (Some 2) r [r $ 1] x2a \<or> alw (\<lambda>x. state_eq (Some 2) (stl x) \<longrightarrow> state_eq (Some 1) x) (stl xs))
[PROOF STEP]
case alw
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. \<exists>xs. make_full_observation drinks (Some 2) r [r $ 1] x2a = xs \<and> (state_eq (Some 2) (stl xs) \<longrightarrow> state_eq (Some 1) xs) \<and> (stl xs = make_full_observation drinks (Some 2) r [r $ 1] x2a \<or> alw (\<lambda>x. state_eq (Some 2) (stl x) \<longrightarrow> state_eq (Some 1) x) (stl xs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>xs. make_full_observation drinks (Some 2) r [r $ 1] x2a = xs \<and> (state_eq (Some 2) (stl xs) \<longrightarrow> state_eq (Some 1) xs) \<and> (stl xs = make_full_observation drinks (Some 2) r [r $ 1] x2a \<or> alw (\<lambda>x. state_eq (Some 2) (stl x) \<longrightarrow> state_eq (Some 1) x) (stl xs))
[PROOF STEP]
apply (simp add: drinks_step_2_none)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. make_full_observation drinks None r [] (stl x2a) = make_full_observation drinks (Some 2) r [r $ 1] x2a \<or> alw (\<lambda>x. state_eq (Some 2) (stl x) \<longrightarrow> state_eq (Some 1) x) (make_full_observation drinks None r [] (stl x2a))
[PROOF STEP]
by (metis (mono_tags, lifting) alw_mono nxt.simps once_none_nxt_always_none option.distinct(1))
[PROOF STATE]
proof (state)
this:
\<exists>xs. make_full_observation drinks (Some 2) r [r $ 1] x2a = xs \<and> (state_eq (Some 2) (stl xs) \<longrightarrow> state_eq (Some 1) xs) \<and> (stl xs = make_full_observation drinks (Some 2) r [r $ 1] x2a \<or> alw (\<lambda>x. state_eq (Some 2) (stl x) \<longrightarrow> state_eq (Some 1) x) (stl xs))

goal:
No subgoals!
[PROOF STEP]
qed