[STATEMENT]
lemma eqButUID_step_\<phi>:
assumes ss1: "eqButUID s s1"
and rs: "reach s" and rs1: "reach s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
and a: "a \<noteq> Cact (cFriend UID1 (pass s UID1) UID2) \<and> a \<noteq> Cact (cFriend UID2 (pass s UID2) UID1) \<and>
        a \<noteq> Dact (dFriend UID1 (pass s UID1) UID2) \<and> a \<noteq> Dact (dFriend UID2 (pass s UID2) UID1)"
shows "\<phi> (Trans s a ou s') = \<phi> (Trans s1 a ou1 s1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (Trans s a ou s') = \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<phi> (Trans s a ou s') \<Longrightarrow> \<phi> (Trans s1 a ou1 s1')
 2. \<phi> (Trans s1 a ou1 s1') \<Longrightarrow> \<phi> (Trans s a ou s')
[PROOF STEP]
assume "\<phi> (Trans s a ou s')"
[PROOF STATE]
proof (state)
this:
\<phi> (Trans s a ou s')

goal (2 subgoals):
 1. \<phi> (Trans s a ou s') \<Longrightarrow> \<phi> (Trans s1 a ou1 s1')
 2. \<phi> (Trans s1 a ou1 s1') \<Longrightarrow> \<phi> (Trans s a ou s')
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
eqButUID s s1
reach s
reach s1
step s a = (ou, s')
step s1 a = (ou1, s1')
a \<noteq> Cact (cFriend UID1 (pass s UID1) UID2) \<and> a \<noteq> Cact (cFriend UID2 (pass s UID2) UID1) \<and> a \<noteq> Dact (dFriend UID1 (pass s UID1) UID2) \<and> a \<noteq> Dact (dFriend UID2 (pass s UID2) UID1)
\<phi> (Trans s a ou s')
[PROOF STEP]
show "\<phi> (Trans s1 a ou1 s1')"
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1
reach s
reach s1
step s a = (ou, s')
step s1 a = (ou1, s1')
a \<noteq> Cact (cFriend UID1 (pass s UID1) UID2) \<and> a \<noteq> Cact (cFriend UID2 (pass s UID2) UID1) \<and> a \<noteq> Dact (dFriend UID1 (pass s UID1) UID2) \<and> a \<noteq> Dact (dFriend UID2 (pass s UID2) UID1)
\<phi> (Trans s a ou s')

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
by (rule eqButUID_step_\<phi>_imp)
[PROOF STATE]
proof (state)
this:
\<phi> (Trans s1 a ou1 s1')

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1') \<Longrightarrow> \<phi> (Trans s a ou s')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1') \<Longrightarrow> \<phi> (Trans s a ou s')
[PROOF STEP]
assume "\<phi> (Trans s1 a ou1 s1')"
[PROOF STATE]
proof (state)
this:
\<phi> (Trans s1 a ou1 s1')

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1') \<Longrightarrow> \<phi> (Trans s a ou s')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<phi> (Trans s1 a ou1 s1')

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1') \<Longrightarrow> \<phi> (Trans s a ou s')
[PROOF STEP]
have "eqButUID s1 s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID s1 s
[PROOF STEP]
using ss1
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1

goal (1 subgoal):
 1. eqButUID s1 s
[PROOF STEP]
by (rule eqButUID_sym)
[PROOF STATE]
proof (state)
this:
eqButUID s1 s

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1') \<Longrightarrow> \<phi> (Trans s a ou s')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eqButUID s1 s

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1') \<Longrightarrow> \<phi> (Trans s a ou s')
[PROOF STEP]
have "a \<noteq> Cact (cFriend UID1 (pass s1 UID1) UID2) \<and>
                 a \<noteq> Cact (cFriend UID2 (pass s1 UID2) UID1) \<and>
                 a \<noteq> Dact (dFriend UID1 (pass s1 UID1) UID2) \<and>
                 a \<noteq> Dact (dFriend UID2 (pass s1 UID2) UID1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> Cact (cFriend UID1 (pass s1 UID1) UID2) \<and> a \<noteq> Cact (cFriend UID2 (pass s1 UID2) UID1) \<and> a \<noteq> Dact (dFriend UID1 (pass s1 UID1) UID2) \<and> a \<noteq> Dact (dFriend UID2 (pass s1 UID2) UID1)
[PROOF STEP]
using a ss1
[PROOF STATE]
proof (prove)
using this:
a \<noteq> Cact (cFriend UID1 (pass s UID1) UID2) \<and> a \<noteq> Cact (cFriend UID2 (pass s UID2) UID1) \<and> a \<noteq> Dact (dFriend UID1 (pass s UID1) UID2) \<and> a \<noteq> Dact (dFriend UID2 (pass s UID2) UID1)
eqButUID s s1

goal (1 subgoal):
 1. a \<noteq> Cact (cFriend UID1 (pass s1 UID1) UID2) \<and> a \<noteq> Cact (cFriend UID2 (pass s1 UID2) UID1) \<and> a \<noteq> Dact (dFriend UID1 (pass s1 UID1) UID2) \<and> a \<noteq> Dact (dFriend UID2 (pass s1 UID2) UID1)
[PROOF STEP]
unfolding eqButUID_def
[PROOF STATE]
proof (prove)
using this:
a \<noteq> Cact (cFriend UID1 (pass s UID1) UID2) \<and> a \<noteq> Cact (cFriend UID2 (pass s UID2) UID1) \<and> a \<noteq> Dact (dFriend UID1 (pass s UID1) UID2) \<and> a \<noteq> Dact (dFriend UID2 (pass s UID2) UID1)
admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> owner s = owner s1 \<and> vis s = vis s1

goal (1 subgoal):
 1. a \<noteq> Cact (cFriend UID1 (pass s1 UID1) UID2) \<and> a \<noteq> Cact (cFriend UID2 (pass s1 UID2) UID1) \<and> a \<noteq> Dact (dFriend UID1 (pass s1 UID1) UID2) \<and> a \<noteq> Dact (dFriend UID2 (pass s1 UID2) UID1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<noteq> Cact (cFriend UID1 (pass s1 UID1) UID2) \<and> a \<noteq> Cact (cFriend UID2 (pass s1 UID2) UID1) \<and> a \<noteq> Dact (dFriend UID1 (pass s1 UID1) UID2) \<and> a \<noteq> Dact (dFriend UID2 (pass s1 UID2) UID1)

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1') \<Longrightarrow> \<phi> (Trans s a ou s')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<phi> (Trans s1 a ou1 s1')
eqButUID s1 s
a \<noteq> Cact (cFriend UID1 (pass s1 UID1) UID2) \<and> a \<noteq> Cact (cFriend UID2 (pass s1 UID2) UID1) \<and> a \<noteq> Dact (dFriend UID1 (pass s1 UID1) UID2) \<and> a \<noteq> Dact (dFriend UID2 (pass s1 UID2) UID1)
[PROOF STEP]
show "\<phi> (Trans s a ou s')"
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s1 a ou1 s1')
eqButUID s1 s
a \<noteq> Cact (cFriend UID1 (pass s1 UID1) UID2) \<and> a \<noteq> Cact (cFriend UID2 (pass s1 UID2) UID1) \<and> a \<noteq> Dact (dFriend UID1 (pass s1 UID1) UID2) \<and> a \<noteq> Dact (dFriend UID2 (pass s1 UID2) UID1)

goal (1 subgoal):
 1. \<phi> (Trans s a ou s')
[PROOF STEP]
using rs rs1 step step1
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s1 a ou1 s1')
eqButUID s1 s
a \<noteq> Cact (cFriend UID1 (pass s1 UID1) UID2) \<and> a \<noteq> Cact (cFriend UID2 (pass s1 UID2) UID1) \<and> a \<noteq> Dact (dFriend UID1 (pass s1 UID1) UID2) \<and> a \<noteq> Dact (dFriend UID2 (pass s1 UID2) UID1)
reach s
reach s1
step s a = (ou, s')
step s1 a = (ou1, s1')

goal (1 subgoal):
 1. \<phi> (Trans s a ou s')
[PROOF STEP]
by (intro eqButUID_step_\<phi>_imp[of s1 s])
[PROOF STATE]
proof (state)
this:
\<phi> (Trans s a ou s')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma createFriend_sym: "createFriend s uid p uid' = createFriend s uid' p' uid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. createFriend s uid p uid' = createFriend s uid' p' uid
[PROOF STEP]
unfolding c_defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let fr = friendIDs s; pfr = pendingFReqs s in s\<lparr>friendIDs := fr(uid := fr uid ## uid', uid' := fr uid' ## uid), pendingFReqs := pfr(uid := remove1 uid' (pfr uid), uid' := remove1 uid (pfr uid')), friendReq := fun_upd2 (fun_upd2 (friendReq s) uid' uid emptyReq) uid uid' emptyReq\<rparr>) = (let fr = friendIDs s; pfr = pendingFReqs s in s\<lparr>friendIDs := fr(uid' := fr uid' ## uid, uid := fr uid ## uid'), pendingFReqs := pfr(uid' := remove1 uid (pfr uid'), uid := remove1 uid' (pfr uid)), friendReq := fun_upd2 (fun_upd2 (friendReq s) uid uid' emptyReq) uid' uid emptyReq\<rparr>)
[PROOF STEP]
by (cases "uid = uid'") (auto simp: fun_upd2_comm fun_upd_twist)


[STATEMENT]
lemma deleteFriend_sym: "deleteFriend s uid p uid' = deleteFriend s uid' p' uid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deleteFriend s uid p uid' = deleteFriend s uid' p' uid
[PROOF STEP]
unfolding d_defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let fr = friendIDs s in s\<lparr>friendIDs := fr(uid := removeAll uid' (fr uid), uid' := removeAll uid (fr uid'))\<rparr>) = (let fr = friendIDs s in s\<lparr>friendIDs := fr(uid' := removeAll uid (fr uid'), uid := removeAll uid' (fr uid))\<rparr>)
[PROOF STEP]
by (cases "uid = uid'") (auto simp: fun_upd_twist)


[STATEMENT]
lemma createFriendReq_createFriend_absorb:
assumes "e_createFriendReq s uid' p uid req"
shows "createFriend (createFriendReq s uid' p1 uid req) uid p2 uid' = createFriend s uid p3 uid'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. createFriend (createFriendReq s uid' p1 uid req) uid p2 uid' = createFriend s uid p3 uid'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
e_createFriendReq s uid' p uid req

goal (1 subgoal):
 1. createFriend (createFriendReq s uid' p1 uid req) uid p2 uid' = createFriend s uid p3 uid'
[PROOF STEP]
unfolding c_defs
[PROOF STATE]
proof (prove)
using this:
IDsOK s [uid', uid] [] \<and> pass s uid' = p \<and> uid' \<notin> set (pendingFReqs s uid) \<and> uid' \<notin> set (friendIDs s uid)

goal (1 subgoal):
 1. (let fr = friendIDs (let pfr = pendingFReqs s in s\<lparr>pendingFReqs := pfr(uid := pfr uid ## uid'), friendReq := fun_upd2 (friendReq s) uid' uid req\<rparr>); pfr = pendingFReqs (let pfr = pendingFReqs s in s\<lparr>pendingFReqs := pfr(uid := pfr uid ## uid'), friendReq := fun_upd2 (friendReq s) uid' uid req\<rparr>) in (let pfr = pendingFReqs s in s\<lparr>pendingFReqs := pfr(uid := pfr uid ## uid'), friendReq := fun_upd2 (friendReq s) uid' uid req\<rparr>)\<lparr>friendIDs := fr(uid := fr uid ## uid', uid' := fr uid' ## uid), pendingFReqs := pfr(uid := remove1 uid' (pfr uid), uid' := remove1 uid (pfr uid')), friendReq := fun_upd2 (fun_upd2 (friendReq (let pfr = pendingFReqs s in s\<lparr>pendingFReqs := pfr(uid := pfr uid ## uid'), friendReq := fun_upd2 (friendReq s) uid' uid req\<rparr>)) uid' uid emptyReq) uid uid' emptyReq\<rparr>) = (let fr = friendIDs s; pfr = pendingFReqs s in s\<lparr>friendIDs := fr(uid := fr uid ## uid', uid' := fr uid' ## uid), pendingFReqs := pfr(uid := remove1 uid' (pfr uid), uid' := remove1 uid (pfr uid')), friendReq := fun_upd2 (fun_upd2 (friendReq s) uid' uid emptyReq) uid uid' emptyReq\<rparr>)
[PROOF STEP]
by (auto simp: remove1_idem remove1_append fun_upd2_absorb)


[STATEMENT]
lemma eqButUID_deleteFriend12_friendIDs_eq:
assumes ss1: "eqButUID s s1"
and rs: "reach s" and rs1: "reach s1"
shows "friendIDs (deleteFriend s UID1 p UID2) = friendIDs (deleteFriend s1 UID1 p' UID2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. friendIDs (deleteFriend s UID1 p UID2) = friendIDs (deleteFriend s1 UID1 p' UID2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. friendIDs (deleteFriend s UID1 p UID2) = friendIDs (deleteFriend s1 UID1 p' UID2)
[PROOF STEP]
have "distinct (friendIDs s UID1)" "distinct (friendIDs s UID2)"
       "distinct (friendIDs s1 UID1)" "distinct (friendIDs s1 UID2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (distinct (friendIDs s UID1) &&& distinct (friendIDs s UID2)) &&& distinct (friendIDs s1 UID1) &&& distinct (friendIDs s1 UID2)
[PROOF STEP]
using rs rs1
[PROOF STATE]
proof (prove)
using this:
reach s
reach s1

goal (1 subgoal):
 1. (distinct (friendIDs s UID1) &&& distinct (friendIDs s UID2)) &&& distinct (friendIDs s1 UID1) &&& distinct (friendIDs s1 UID2)
[PROOF STEP]
by (auto intro: reach_distinct_friends_reqs)
[PROOF STATE]
proof (state)
this:
distinct (friendIDs s UID1)
distinct (friendIDs s UID2)
distinct (friendIDs s1 UID1)
distinct (friendIDs s1 UID2)

goal (1 subgoal):
 1. friendIDs (deleteFriend s UID1 p UID2) = friendIDs (deleteFriend s1 UID1 p' UID2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct (friendIDs s UID1)
distinct (friendIDs s UID2)
distinct (friendIDs s1 UID1)
distinct (friendIDs s1 UID2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
distinct (friendIDs s UID1)
distinct (friendIDs s UID2)
distinct (friendIDs s1 UID1)
distinct (friendIDs s1 UID2)

goal (1 subgoal):
 1. friendIDs (deleteFriend s UID1 p UID2) = friendIDs (deleteFriend s1 UID1 p' UID2)
[PROOF STEP]
using ss1
[PROOF STATE]
proof (prove)
using this:
distinct (friendIDs s UID1)
distinct (friendIDs s UID2)
distinct (friendIDs s1 UID1)
distinct (friendIDs s1 UID2)
eqButUID s s1

goal (1 subgoal):
 1. friendIDs (deleteFriend s UID1 p UID2) = friendIDs (deleteFriend s1 UID1 p' UID2)
[PROOF STEP]
unfolding eqButUID_def eqButUIDf_def
[PROOF STATE]
proof (prove)
using this:
distinct (friendIDs s UID1)
distinct (friendIDs s UID2)
distinct (friendIDs s1 UID1)
distinct (friendIDs s1 UID2)
admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> (eqButUIDl UID2 (pendingFReqs s UID1) (pendingFReqs s1 UID1) \<and> eqButUIDl UID1 (pendingFReqs s UID2) (pendingFReqs s1 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> pendingFReqs s uid = pendingFReqs s1 uid)) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> (eqButUIDl UID2 (friendIDs s UID1) (friendIDs s1 UID1) \<and> eqButUIDl UID1 (friendIDs s UID2) (friendIDs s1 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> friendIDs s uid = friendIDs s1 uid)) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> owner s = owner s1 \<and> vis s = vis s1

goal (1 subgoal):
 1. friendIDs (deleteFriend s UID1 p UID2) = friendIDs (deleteFriend s1 UID1 p' UID2)
[PROOF STEP]
unfolding d_defs
[PROOF STATE]
proof (prove)
using this:
distinct (friendIDs s UID1)
distinct (friendIDs s UID2)
distinct (friendIDs s1 UID1)
distinct (friendIDs s1 UID2)
admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> (eqButUIDl UID2 (pendingFReqs s UID1) (pendingFReqs s1 UID1) \<and> eqButUIDl UID1 (pendingFReqs s UID2) (pendingFReqs s1 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> pendingFReqs s uid = pendingFReqs s1 uid)) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> (eqButUIDl UID2 (friendIDs s UID1) (friendIDs s1 UID1) \<and> eqButUIDl UID1 (friendIDs s UID2) (friendIDs s1 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> friendIDs s uid = friendIDs s1 uid)) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> owner s = owner s1 \<and> vis s = vis s1

goal (1 subgoal):
 1. friendIDs (let fr = friendIDs s in s\<lparr>friendIDs := fr(UID1 := removeAll UID2 (fr UID1), UID2 := removeAll UID1 (fr UID2))\<rparr>) = friendIDs (let fr = friendIDs s1 in s1\<lparr>friendIDs := fr(UID1 := removeAll UID2 (fr UID1), UID2 := removeAll UID1 (fr UID2))\<rparr>)
[PROOF STEP]
by (auto simp: distinct_remove1_removeAll)
[PROOF STATE]
proof (state)
this:
friendIDs (deleteFriend s UID1 p UID2) = friendIDs (deleteFriend s1 UID1 p' UID2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eqButUID_createFriend12_friendIDs_eq:
assumes ss1: "eqButUID s s1"
and rs: "reach s" and rs1: "reach s1"
and f12: "\<not>friends12 s" "\<not>friends12 s1"
shows "friendIDs (createFriend s UID1 p UID2) = friendIDs (createFriend s1 UID1 p' UID2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. friendIDs (createFriend s UID1 p UID2) = friendIDs (createFriend s1 UID1 p' UID2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. friendIDs (createFriend s UID1 p UID2) = friendIDs (createFriend s1 UID1 p' UID2)
[PROOF STEP]
have f12': "UID1 \<notin> set (friendIDs s UID2)" "UID2 \<notin> set (friendIDs s UID1)"
             "UID1 \<notin> set (friendIDs s1 UID2)" "UID2 \<notin> set (friendIDs s1 UID1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (UID1 \<notin> set (friendIDs s UID2) &&& UID2 \<notin> set (friendIDs s UID1)) &&& UID1 \<notin> set (friendIDs s1 UID2) &&& UID2 \<notin> set (friendIDs s1 UID1)
[PROOF STEP]
using f12 rs rs1 reach_friendIDs_symmetric
[PROOF STATE]
proof (prove)
using this:
\<not> friends12 s
\<not> friends12 s1
reach s
reach s1
reach ?s \<Longrightarrow> (?uID1.0 \<in>\<in> friendIDs ?s ?uID2.0) = (?uID2.0 \<in>\<in> friendIDs ?s ?uID1.0)

goal (1 subgoal):
 1. (UID1 \<notin> set (friendIDs s UID2) &&& UID2 \<notin> set (friendIDs s UID1)) &&& UID1 \<notin> set (friendIDs s1 UID2) &&& UID2 \<notin> set (friendIDs s1 UID1)
[PROOF STEP]
unfolding friends12_def
[PROOF STATE]
proof (prove)
using this:
\<not> (UID1 \<in>\<in> friendIDs s UID2 \<and> UID2 \<in>\<in> friendIDs s UID1)
\<not> (UID1 \<in>\<in> friendIDs s1 UID2 \<and> UID2 \<in>\<in> friendIDs s1 UID1)
reach s
reach s1
reach ?s \<Longrightarrow> (?uID1.0 \<in>\<in> friendIDs ?s ?uID2.0) = (?uID2.0 \<in>\<in> friendIDs ?s ?uID1.0)

goal (1 subgoal):
 1. (UID1 \<notin> set (friendIDs s UID2) &&& UID2 \<notin> set (friendIDs s UID1)) &&& UID1 \<notin> set (friendIDs s1 UID2) &&& UID2 \<notin> set (friendIDs s1 UID1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
UID1 \<notin> set (friendIDs s UID2)
UID2 \<notin> set (friendIDs s UID1)
UID1 \<notin> set (friendIDs s1 UID2)
UID2 \<notin> set (friendIDs s1 UID1)

goal (1 subgoal):
 1. friendIDs (createFriend s UID1 p UID2) = friendIDs (createFriend s1 UID1 p' UID2)
[PROOF STEP]
have "friendIDs s = friendIDs s1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. friendIDs s = friendIDs s1
[PROOF STEP]
proof (intro ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. friendIDs s x = friendIDs s1 x
[PROOF STEP]
fix uid
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. friendIDs s x = friendIDs s1 x
[PROOF STEP]
show "friendIDs s uid = friendIDs s1 uid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. friendIDs s uid = friendIDs s1 uid
[PROOF STEP]
using ss1 f12'
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1
UID1 \<notin> set (friendIDs s UID2)
UID2 \<notin> set (friendIDs s UID1)
UID1 \<notin> set (friendIDs s1 UID2)
UID2 \<notin> set (friendIDs s1 UID1)

goal (1 subgoal):
 1. friendIDs s uid = friendIDs s1 uid
[PROOF STEP]
unfolding eqButUID_def eqButUIDf_def
[PROOF STATE]
proof (prove)
using this:
admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> (eqButUIDl UID2 (pendingFReqs s UID1) (pendingFReqs s1 UID1) \<and> eqButUIDl UID1 (pendingFReqs s UID2) (pendingFReqs s1 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> pendingFReqs s uid = pendingFReqs s1 uid)) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> (eqButUIDl UID2 (friendIDs s UID1) (friendIDs s1 UID1) \<and> eqButUIDl UID1 (friendIDs s UID2) (friendIDs s1 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> friendIDs s uid = friendIDs s1 uid)) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> owner s = owner s1 \<and> vis s = vis s1
UID1 \<notin> set (friendIDs s UID2)
UID2 \<notin> set (friendIDs s UID1)
UID1 \<notin> set (friendIDs s1 UID2)
UID2 \<notin> set (friendIDs s1 UID1)

goal (1 subgoal):
 1. friendIDs s uid = friendIDs s1 uid
[PROOF STEP]
by (cases "uid = UID1 \<or> uid = UID2") (auto simp: remove1_idem)
[PROOF STATE]
proof (state)
this:
friendIDs s uid = friendIDs s1 uid

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
friendIDs s = friendIDs s1

goal (1 subgoal):
 1. friendIDs (createFriend s UID1 p UID2) = friendIDs (createFriend s1 UID1 p' UID2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
friendIDs s = friendIDs s1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
friendIDs s = friendIDs s1

goal (1 subgoal):
 1. friendIDs (createFriend s UID1 p UID2) = friendIDs (createFriend s1 UID1 p' UID2)
[PROOF STEP]
by (auto simp: c_defs)
[PROOF STATE]
proof (state)
this:
friendIDs (createFriend s UID1 p UID2) = friendIDs (createFriend s1 UID1 p' UID2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "test (do {
  node \<leftarrow> Node_insertBefore_document . createTextNode(''Foo'');
  tmp0 \<leftarrow> Node_insertBefore_document . createTextNode(''fail'');
  assert_throws(HierarchyRequestError, node . insertBefore(tmp0, None))
}) Node_insertBefore_heap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test (Heap_Error_Monad.bind Node_insertBefore_document . createTextNode(''Foo'') (\<lambda>node. Heap_Error_Monad.bind Node_insertBefore_document . createTextNode(''fail'') (\<lambda>tmp0. assert_throws(HierarchyRequestError, node . insertBefore(tmp0, None))))) Node_insertBefore_heap
[PROOF STEP]
by eval


[STATEMENT]
lemma "test (do {
  tmp1 \<leftarrow> Node_insertBefore_document . body;
  tmp2 \<leftarrow> Node_insertBefore_document . getElementById(''log'');
  tmp0 \<leftarrow> Node_insertBefore_document . body;
  assert_throws(HierarchyRequestError, tmp0 . insertBefore(tmp1, tmp2));
  tmp4 \<leftarrow> Node_insertBefore_document . documentElement;
  tmp5 \<leftarrow> Node_insertBefore_document . getElementById(''log'');
  tmp3 \<leftarrow> Node_insertBefore_document . body;
  assert_throws(HierarchyRequestError, tmp3 . insertBefore(tmp4, tmp5))
}) Node_insertBefore_heap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test (Heap_Error_Monad.bind Node_insertBefore_document . body (\<lambda>tmp1. Heap_Error_Monad.bind Node_insertBefore_document . getElementById(''log'') (\<lambda>tmp2. Heap_Error_Monad.bind Node_insertBefore_document . body (\<lambda>tmp0. Heap_Error_Monad.bind assert_throws(HierarchyRequestError, tmp0 . insertBefore(tmp1, tmp2)) (\<lambda>_. Heap_Error_Monad.bind Node_insertBefore_document . documentElement (\<lambda>tmp4. Heap_Error_Monad.bind Node_insertBefore_document . getElementById(''log'') (\<lambda>tmp5. Heap_Error_Monad.bind Node_insertBefore_document . body (\<lambda>tmp3. assert_throws(HierarchyRequestError, tmp3 . insertBefore(tmp4, tmp5)))))))))) Node_insertBefore_heap
[PROOF STEP]
by eval


[STATEMENT]
lemma "test (do {
  a \<leftarrow> Node_insertBefore_document . createElement(''div'');
  b \<leftarrow> Node_insertBefore_document . createElement(''div'');
  c \<leftarrow> Node_insertBefore_document . createElement(''div'');
  assert_throws(NotFoundError, a . insertBefore(b, c))
}) Node_insertBefore_heap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test (Heap_Error_Monad.bind Node_insertBefore_document . createElement(''div'') (\<lambda>a. Heap_Error_Monad.bind Node_insertBefore_document . createElement(''div'') (\<lambda>b. Heap_Error_Monad.bind Node_insertBefore_document . createElement(''div'') (\<lambda>c. assert_throws(NotFoundError, a . insertBefore(b, c)))))) Node_insertBefore_heap
[PROOF STEP]
by eval


[STATEMENT]
lemma "test (do {
  doc \<leftarrow> createDocument(''title'');
  doc2 \<leftarrow> createDocument(''title2'');
  tmp0 \<leftarrow> doc . documentElement;
  assert_throws(HierarchyRequestError, doc . insertBefore(doc2, tmp0));
  tmp1 \<leftarrow> doc . createTextNode(''text'');
  tmp2 \<leftarrow> doc . documentElement;
  assert_throws(HierarchyRequestError, doc . insertBefore(tmp1, tmp2))
}) Node_insertBefore_heap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test (Heap_Error_Monad.bind createDocument(''title'') (\<lambda>doc. Heap_Error_Monad.bind createDocument(''title2'') (\<lambda>doc2. Heap_Error_Monad.bind doc . documentElement (\<lambda>tmp0. Heap_Error_Monad.bind assert_throws(HierarchyRequestError, doc . insertBefore(doc2, tmp0)) (\<lambda>_. Heap_Error_Monad.bind doc . createTextNode(''text'') (\<lambda>tmp1. Heap_Error_Monad.bind doc . documentElement (\<lambda>tmp2. assert_throws(HierarchyRequestError, doc . insertBefore(tmp1, tmp2))))))))) Node_insertBefore_heap
[PROOF STEP]
by eval


[STATEMENT]
lemma "test (do {
  a \<leftarrow> Node_insertBefore_document . createElement(''div'');
  b \<leftarrow> Node_insertBefore_document . createElement(''div'');
  c \<leftarrow> Node_insertBefore_document . createElement(''div'');
  a . appendChild(b);
  a . appendChild(c);
  tmp0 \<leftarrow> a . childNodes;
  assert_array_equals(tmp0, [b, c]);
  tmp1 \<leftarrow> a . insertBefore(b, b);
  assert_equals(tmp1, b);
  tmp2 \<leftarrow> a . childNodes;
  assert_array_equals(tmp2, [b, c]);
  tmp3 \<leftarrow> a . insertBefore(c, c);
  assert_equals(tmp3, c);
  tmp4 \<leftarrow> a . childNodes;
  assert_array_equals(tmp4, [b, c])
}) Node_insertBefore_heap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test (Heap_Error_Monad.bind Node_insertBefore_document . createElement(''div'') (\<lambda>a. Heap_Error_Monad.bind Node_insertBefore_document . createElement(''div'') (\<lambda>b. Heap_Error_Monad.bind Node_insertBefore_document . createElement(''div'') (\<lambda>c. Heap_Error_Monad.bind a . appendChild(b) (\<lambda>_. Heap_Error_Monad.bind a . appendChild(c) (\<lambda>_. Heap_Error_Monad.bind a . childNodes (\<lambda>tmp0. Heap_Error_Monad.bind assert_array_equals(tmp0, [b, c]) (\<lambda>_. Heap_Error_Monad.bind a . insertBefore(b, b) (\<lambda>tmp1. Heap_Error_Monad.bind assert_array_equals(tmp1, b) (\<lambda>_. Heap_Error_Monad.bind a . childNodes (\<lambda>tmp2. Heap_Error_Monad.bind assert_array_equals(tmp2, [b, c]) (\<lambda>_. Heap_Error_Monad.bind a . insertBefore(c, c) (\<lambda>tmp3. Heap_Error_Monad.bind assert_array_equals(tmp3, c) (\<lambda>_. Heap_Error_Monad.bind a . childNodes (\<lambda>tmp4. assert_array_equals(tmp4, [b, c])))))))))))))))) Node_insertBefore_heap
[PROOF STEP]
by eval


[STATEMENT]
lemma hypext_logistic:
  "(*h* logistic) x = hyp_logistic x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* logistic) x = hyp_logistic x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (*h* logistic) x = hyp_logistic x
[PROOF STEP]
have "(*h* (\<lambda>x. exp (- x) + 1)) x = (*h* exp) (- x) + of_comp 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* (\<lambda>x. exp (- x) + 1)) x = (*h* exp) (- x) + of_comp 1
[PROOF STEP]
by (simp add: hypext_compose hypext_uminus hypext_fun_cadd twice_field_differentiable_at_compose)
[PROOF STATE]
proof (state)
this:
(*h* (\<lambda>x. exp (- x) + 1)) x = (*h* exp) (- x) + of_comp 1

goal (1 subgoal):
 1. (*h* logistic) x = hyp_logistic x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(*h* (\<lambda>x. exp (- x) + 1)) x = (*h* exp) (- x) + of_comp 1
[PROOF STEP]
have "(*h* (\<lambda>x. 1 + exp (- x))) x = 1 + (*h* exp) (- x)"
[PROOF STATE]
proof (prove)
using this:
(*h* (\<lambda>x. exp (- x) + 1)) x = (*h* exp) (- x) + of_comp 1

goal (1 subgoal):
 1. (*h* (\<lambda>x. 1 + exp (- x))) x = 1 + (*h* exp) (- x)
[PROOF STEP]
by (simp add: one_hyperdual_def add.commute)
[PROOF STATE]
proof (state)
this:
(*h* (\<lambda>x. 1 + exp (- x))) x = 1 + (*h* exp) (- x)

goal (1 subgoal):
 1. (*h* logistic) x = hyp_logistic x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(*h* (\<lambda>x. 1 + exp (- x))) x = 1 + (*h* exp) (- x)

goal (1 subgoal):
 1. (*h* logistic) x = hyp_logistic x
[PROOF STEP]
have "1 + exp (- Base x) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + exp (- Base x) \<noteq> 0
[PROOF STEP]
by (metis exp_ge_zero add_eq_0_iff neg_0_le_iff_le not_one_le_zero)
[PROOF STATE]
proof (state)
this:
1 + exp (- Base x) \<noteq> 0

goal (1 subgoal):
 1. (*h* logistic) x = hyp_logistic x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 + exp (- Base x) \<noteq> 0

goal (1 subgoal):
 1. (*h* logistic) x = hyp_logistic x
[PROOF STEP]
have "(\<lambda>x. 1 + exp (- x)) twice_field_differentiable_at Base x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. 1 + exp (- x)) twice_field_differentiable_at Base x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. 1 + exp (- x)) twice_field_differentiable_at Base x
[PROOF STEP]
have "(\<lambda>x. exp (- x)) twice_field_differentiable_at Base x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. exp (- x)) twice_field_differentiable_at Base x
[PROOF STEP]
by (simp add: twice_field_differentiable_at_compose)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. exp (- x)) twice_field_differentiable_at Base x

goal (1 subgoal):
 1. (\<lambda>x. 1 + exp (- x)) twice_field_differentiable_at Base x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. exp (- x)) twice_field_differentiable_at Base x
[PROOF STEP]
have "(\<lambda>x. exp (- x) + 1) twice_field_differentiable_at Base x"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. exp (- x)) twice_field_differentiable_at Base x

goal (1 subgoal):
 1. (\<lambda>x. exp (- x) + 1) twice_field_differentiable_at Base x
[PROOF STEP]
using twice_field_differentiable_at_compose[of "\<lambda>x. exp (- x)" "Base x" "\<lambda>x. x + 1"]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. exp (- x)) twice_field_differentiable_at Base x
\<lbrakk>(\<lambda>x. exp (- x)) twice_field_differentiable_at Base x; (\<lambda>x. x + 1) twice_field_differentiable_at exp (- Base x)\<rbrakk> \<Longrightarrow> (\<lambda>x. exp (- x) + 1) twice_field_differentiable_at Base x

goal (1 subgoal):
 1. (\<lambda>x. exp (- x) + 1) twice_field_differentiable_at Base x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>x. exp (- x) + 1) twice_field_differentiable_at Base x

goal (1 subgoal):
 1. (\<lambda>x. 1 + exp (- x)) twice_field_differentiable_at Base x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. exp (- x) + 1) twice_field_differentiable_at Base x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. exp (- x) + 1) twice_field_differentiable_at Base x

goal (1 subgoal):
 1. (\<lambda>x. 1 + exp (- x)) twice_field_differentiable_at Base x
[PROOF STEP]
by (simp add: add.commute)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. 1 + exp (- x)) twice_field_differentiable_at Base x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>x. 1 + exp (- x)) twice_field_differentiable_at Base x

goal (1 subgoal):
 1. (*h* logistic) x = hyp_logistic x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(*h* (\<lambda>x. 1 + exp (- x))) x = 1 + (*h* exp) (- x)
1 + exp (- Base x) \<noteq> 0
(\<lambda>x. 1 + exp (- x)) twice_field_differentiable_at Base x
[PROOF STEP]
have "(*h* (\<lambda>x. inverse (1 + exp (- x)))) x = inverse (1 + (*h* exp) (- x))"
[PROOF STATE]
proof (prove)
using this:
(*h* (\<lambda>x. 1 + exp (- x))) x = 1 + (*h* exp) (- x)
1 + exp (- Base x) \<noteq> 0
(\<lambda>x. 1 + exp (- x)) twice_field_differentiable_at Base x

goal (1 subgoal):
 1. (*h* (\<lambda>x. inverse (1 + exp (- x)))) x = inverse (1 + (*h* exp) (- x))
[PROOF STEP]
by (simp add: hypext_fun_inverse)
[PROOF STATE]
proof (state)
this:
(*h* (\<lambda>x. inverse (1 + exp (- x)))) x = inverse (1 + (*h* exp) (- x))

goal (1 subgoal):
 1. (*h* logistic) x = hyp_logistic x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(*h* (\<lambda>x. inverse (1 + exp (- x)))) x = inverse (1 + (*h* exp) (- x))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(*h* (\<lambda>x. inverse (1 + exp (- x)))) x = inverse (1 + (*h* exp) (- x))

goal (1 subgoal):
 1. (*h* logistic) x = hyp_logistic x
[PROOF STEP]
unfolding logistic_def hyp_logistic_def
[PROOF STATE]
proof (prove)
using this:
(*h* (\<lambda>x. inverse (1 + exp (- x)))) x = inverse (1 + (*h* exp) (- x))

goal (1 subgoal):
 1. (*h* (\<lambda>x. inverse (1 + exp (- x)))) x = inverse (1 + (*h* exp) (- x))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(*h* logistic) x = hyp_logistic x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "Eps1 (hyp_logistic (\<beta> x)) = deriv logistic x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eps1 (hyp_logistic (\<beta> x)) = deriv logistic x
[PROOF STEP]
by (metis Eps1_hypext hypext_logistic)


[STATEMENT]
lemma "First (autodiff logistic x) = exp (- x) / (1 + exp (- x)) ^ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. First (autodiff logistic x) = exp (- x) / (1 + exp (- x))\<^sup>2
[PROOF STEP]
(* Move to hyperdual variant: *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. First (autodiff logistic x) = exp (- x) / (1 + exp (- x))\<^sup>2
[PROOF STEP]
apply (simp only: autodiff.simps hyperdual_to_derivs.simps derivs.sel hypext_logistic)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eps1 (hyp_logistic (\<beta> x)) = exp (- x) / (1 + exp (- x))\<^sup>2
[PROOF STEP]
(* Unfold extensions of functions that have a hyperdual variant (all except exp): *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eps1 (hyp_logistic (\<beta> x)) = exp (- x) / (1 + exp (- x))\<^sup>2
[PROOF STEP]
apply (simp only: hyp_logistic_def inverse_hyperdual.code hyperdual.sel)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - Eps1 (1 + (*h* exp) (- \<beta> x)) / (Base (1 + (*h* exp) (- \<beta> x)))\<^sup>2 = exp (- x) / (1 + exp (- x))\<^sup>2
[PROOF STEP]
(* Finish by expanding the extension of exp and hyperdual computations: *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - Eps1 (1 + (*h* exp) (- \<beta> x)) / (Base (1 + (*h* exp) (- \<beta> x)))\<^sup>2 = exp (- x) / (1 + exp (- x))\<^sup>2
[PROOF STEP]
apply (simp add: hyperdualx_def hypext_exp_Hyperdual hyperdual_bases)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma "Second (autodiff logistic x) = deriv (deriv logistic) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Second (autodiff logistic x) = deriv (deriv logistic) x
[PROOF STEP]
by (rule autodiff_extract_second)


[STATEMENT]
lemma "Second (autodiff logistic x) = ((exp (- x) - 1) * exp (- x)) / ((1 + exp (- x)) ^ 3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Second (autodiff logistic x) = (exp (- x) - 1) * exp (- x) / (1 + exp (- x)) ^ 3
[PROOF STEP]
(* Move to hyperdual variant: *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Second (autodiff logistic x) = (exp (- x) - 1) * exp (- x) / (1 + exp (- x)) ^ 3
[PROOF STEP]
apply (simp only: autodiff.simps hyperdual_to_derivs.simps derivs.sel hypext_logistic)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eps12 (hyp_logistic (\<beta> x)) = (exp (- x) - 1) * exp (- x) / (1 + exp (- x)) ^ 3
[PROOF STEP]
(* Unfold extensions of functions that have a hyperdual variant (all except exp): *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eps12 (hyp_logistic (\<beta> x)) = (exp (- x) - 1) * exp (- x) / (1 + exp (- x)) ^ 3
[PROOF STEP]
apply (simp only: hyp_logistic_def inverse_hyperdual.code hyperdual.sel)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * (Eps1 (1 + (*h* exp) (- \<beta> x)) * Eps2 (1 + (*h* exp) (- \<beta> x)) / Base (1 + (*h* exp) (- \<beta> x)) ^ 3) - Eps12 (1 + (*h* exp) (- \<beta> x)) / (Base (1 + (*h* exp) (- \<beta> x)))\<^sup>2 = (exp (- x) - 1) * exp (- x) / (1 + exp (- x)) ^ 3
[PROOF STEP]
(* Finish by expanding the extension of exp and hyperdual computations: *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * (Eps1 (1 + (*h* exp) (- \<beta> x)) * Eps2 (1 + (*h* exp) (- \<beta> x)) / Base (1 + (*h* exp) (- \<beta> x)) ^ 3) - Eps12 (1 + (*h* exp) (- \<beta> x)) / (Base (1 + (*h* exp) (- \<beta> x)))\<^sup>2 = (exp (- x) - 1) * exp (- x) / (1 + exp (- x)) ^ 3
[PROOF STEP]
apply (simp add: hyperdualx_def hypext_exp_Hyperdual hyperdual_bases)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * (exp (- x) * exp (- x)) / (1 + exp (- x)) ^ 3 - exp (- x) / (1 + exp (- x))\<^sup>2 = (exp (- x) - 1) * exp (- x) / (1 + exp (- x)) ^ 3
[PROOF STEP]
(* Simplify the resulting expression: *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * (exp (- x) * exp (- x)) / (1 + exp (- x)) ^ 3 - exp (- x) / (1 + exp (- x))\<^sup>2 = (exp (- x) - 1) * exp (- x) / (1 + exp (- x)) ^ 3
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 2 * (exp (- x) * exp (- x)) / (1 + exp (- x)) ^ 3 - exp (- x) / (1 + exp (- x))\<^sup>2 = (exp (- x) - 1) * exp (- x) / (1 + exp (- x)) ^ 3
[PROOF STEP]
have
    "2 * (exp (- x) * exp (- x)) / (1 + exp (- x)) ^ 3 - exp (- x) / (1 + exp (- x)) ^ 2 =
     (2 * exp (- x) / (1 + exp (- x)) ^ 3 - 1 / (1 + exp (- x)) ^ 2) * exp (- x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * (exp (- x) * exp (- x)) / (1 + exp (- x)) ^ 3 - exp (- x) / (1 + exp (- x))\<^sup>2 = (2 * exp (- x) / (1 + exp (- x)) ^ 3 - 1 / (1 + exp (- x))\<^sup>2) * exp (- x)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
2 * (exp (- x) * exp (- x)) / (1 + exp (- x)) ^ 3 - exp (- x) / (1 + exp (- x))\<^sup>2 = (2 * exp (- x) / (1 + exp (- x)) ^ 3 - 1 / (1 + exp (- x))\<^sup>2) * exp (- x)

goal (1 subgoal):
 1. 2 * (exp (- x) * exp (- x)) / (1 + exp (- x)) ^ 3 - exp (- x) / (1 + exp (- x))\<^sup>2 = (exp (- x) - 1) * exp (- x) / (1 + exp (- x)) ^ 3
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 * (exp (- x) * exp (- x)) / (1 + exp (- x)) ^ 3 - exp (- x) / (1 + exp (- x))\<^sup>2 = (2 * exp (- x) / (1 + exp (- x)) ^ 3 - 1 / (1 + exp (- x))\<^sup>2) * exp (- x)

goal (1 subgoal):
 1. 2 * (exp (- x) * exp (- x)) / (1 + exp (- x)) ^ 3 - exp (- x) / (1 + exp (- x))\<^sup>2 = (exp (- x) - 1) * exp (- x) / (1 + exp (- x)) ^ 3
[PROOF STEP]
have "... = (2 * exp (- x) / (1 + exp (- x)) ^ 3 - (1 + exp (- x)) / (1 + exp (- x)) ^ 3) * exp (- x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (2 * exp (- x) / (1 + exp (- x)) ^ 3 - 1 / (1 + exp (- x))\<^sup>2) * exp (- x) = (2 * exp (- x) / (1 + exp (- x)) ^ 3 - (1 + exp (- x)) / (1 + exp (- x)) ^ 3) * exp (- x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (2 * exp (- x) / (1 + exp (- x)) ^ 3 - 1 / (1 + exp (- x))\<^sup>2) * exp (- x) = (2 * exp (- x) / (1 + exp (- x)) ^ 3 - (1 + exp (- x)) / (1 + exp (- x)) ^ 3) * exp (- x)
[PROOF STEP]
have "inverse ((1 + exp (- x)) ^ 2) = inverse (1 + exp (- x)) ^ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse ((1 + exp (- x))\<^sup>2) = (inverse (1 + exp (- x)))\<^sup>2
[PROOF STEP]
by (simp add: power_inverse)
[PROOF STATE]
proof (state)
this:
inverse ((1 + exp (- x))\<^sup>2) = (inverse (1 + exp (- x)))\<^sup>2

goal (1 subgoal):
 1. (2 * exp (- x) / (1 + exp (- x)) ^ 3 - 1 / (1 + exp (- x))\<^sup>2) * exp (- x) = (2 * exp (- x) / (1 + exp (- x)) ^ 3 - (1 + exp (- x)) / (1 + exp (- x)) ^ 3) * exp (- x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
inverse ((1 + exp (- x))\<^sup>2) = (inverse (1 + exp (- x)))\<^sup>2

goal (1 subgoal):
 1. (2 * exp (- x) / (1 + exp (- x)) ^ 3 - 1 / (1 + exp (- x))\<^sup>2) * exp (- x) = (2 * exp (- x) / (1 + exp (- x)) ^ 3 - (1 + exp (- x)) / (1 + exp (- x)) ^ 3) * exp (- x)
[PROOF STEP]
have "... = (1 + exp (- x)) * inverse (1 + exp (- x)) * inverse (1 + exp (- x)) ^ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inverse (1 + exp (- x)))\<^sup>2 = (1 + exp (- x)) * inverse (1 + exp (- x)) * (inverse (1 + exp (- x)))\<^sup>2
[PROOF STEP]
by (simp add: inverse_eq_divide)
[PROOF STATE]
proof (state)
this:
(inverse (1 + exp (- x)))\<^sup>2 = (1 + exp (- x)) * inverse (1 + exp (- x)) * (inverse (1 + exp (- x)))\<^sup>2

goal (1 subgoal):
 1. (2 * exp (- x) / (1 + exp (- x)) ^ 3 - 1 / (1 + exp (- x))\<^sup>2) * exp (- x) = (2 * exp (- x) / (1 + exp (- x)) ^ 3 - (1 + exp (- x)) / (1 + exp (- x)) ^ 3) * exp (- x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(inverse (1 + exp (- x)))\<^sup>2 = (1 + exp (- x)) * inverse (1 + exp (- x)) * (inverse (1 + exp (- x)))\<^sup>2

goal (1 subgoal):
 1. (2 * exp (- x) / (1 + exp (- x)) ^ 3 - 1 / (1 + exp (- x))\<^sup>2) * exp (- x) = (2 * exp (- x) / (1 + exp (- x)) ^ 3 - (1 + exp (- x)) / (1 + exp (- x)) ^ 3) * exp (- x)
[PROOF STEP]
have "... = (1 + exp (- x)) * inverse (1 + exp (- x)) ^ 3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 + exp (- x)) * inverse (1 + exp (- x)) * (inverse (1 + exp (- x)))\<^sup>2 = (1 + exp (- x)) * inverse (1 + exp (- x)) ^ 3
[PROOF STEP]
by (simp add: power2_eq_square power3_eq_cube)
[PROOF STATE]
proof (state)
this:
(1 + exp (- x)) * inverse (1 + exp (- x)) * (inverse (1 + exp (- x)))\<^sup>2 = (1 + exp (- x)) * inverse (1 + exp (- x)) ^ 3

goal (1 subgoal):
 1. (2 * exp (- x) / (1 + exp (- x)) ^ 3 - 1 / (1 + exp (- x))\<^sup>2) * exp (- x) = (2 * exp (- x) / (1 + exp (- x)) ^ 3 - (1 + exp (- x)) / (1 + exp (- x)) ^ 3) * exp (- x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
inverse ((1 + exp (- x))\<^sup>2) = (1 + exp (- x)) * inverse (1 + exp (- x)) ^ 3
[PROOF STEP]
have "inverse ((1 + exp (- x)) ^ 2) = (1 + exp (- x)) * inverse ((1 + exp (- x)) ^ 3)"
[PROOF STATE]
proof (prove)
using this:
inverse ((1 + exp (- x))\<^sup>2) = (1 + exp (- x)) * inverse (1 + exp (- x)) ^ 3

goal (1 subgoal):
 1. inverse ((1 + exp (- x))\<^sup>2) = (1 + exp (- x)) * inverse ((1 + exp (- x)) ^ 3)
[PROOF STEP]
by (simp add: power_inverse)
[PROOF STATE]
proof (state)
this:
inverse ((1 + exp (- x))\<^sup>2) = (1 + exp (- x)) * inverse ((1 + exp (- x)) ^ 3)

goal (1 subgoal):
 1. (2 * exp (- x) / (1 + exp (- x)) ^ 3 - 1 / (1 + exp (- x))\<^sup>2) * exp (- x) = (2 * exp (- x) / (1 + exp (- x)) ^ 3 - (1 + exp (- x)) / (1 + exp (- x)) ^ 3) * exp (- x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inverse ((1 + exp (- x))\<^sup>2) = (1 + exp (- x)) * inverse ((1 + exp (- x)) ^ 3)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inverse ((1 + exp (- x))\<^sup>2) = (1 + exp (- x)) * inverse ((1 + exp (- x)) ^ 3)

goal (1 subgoal):
 1. (2 * exp (- x) / (1 + exp (- x)) ^ 3 - 1 / (1 + exp (- x))\<^sup>2) * exp (- x) = (2 * exp (- x) / (1 + exp (- x)) ^ 3 - (1 + exp (- x)) / (1 + exp (- x)) ^ 3) * exp (- x)
[PROOF STEP]
by (simp add: inverse_eq_divide)
[PROOF STATE]
proof (state)
this:
(2 * exp (- x) / (1 + exp (- x)) ^ 3 - 1 / (1 + exp (- x))\<^sup>2) * exp (- x) = (2 * exp (- x) / (1 + exp (- x)) ^ 3 - (1 + exp (- x)) / (1 + exp (- x)) ^ 3) * exp (- x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(2 * exp (- x) / (1 + exp (- x)) ^ 3 - 1 / (1 + exp (- x))\<^sup>2) * exp (- x) = (2 * exp (- x) / (1 + exp (- x)) ^ 3 - (1 + exp (- x)) / (1 + exp (- x)) ^ 3) * exp (- x)

goal (1 subgoal):
 1. 2 * (exp (- x) * exp (- x)) / (1 + exp (- x)) ^ 3 - exp (- x) / (1 + exp (- x))\<^sup>2 = (exp (- x) - 1) * exp (- x) / (1 + exp (- x)) ^ 3
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(2 * exp (- x) / (1 + exp (- x)) ^ 3 - 1 / (1 + exp (- x))\<^sup>2) * exp (- x) = (2 * exp (- x) / (1 + exp (- x)) ^ 3 - (1 + exp (- x)) / (1 + exp (- x)) ^ 3) * exp (- x)

goal (1 subgoal):
 1. 2 * (exp (- x) * exp (- x)) / (1 + exp (- x)) ^ 3 - exp (- x) / (1 + exp (- x))\<^sup>2 = (exp (- x) - 1) * exp (- x) / (1 + exp (- x)) ^ 3
[PROOF STEP]
have "... = (2 * exp (- x) - (1 + exp (- x))) / (1 + exp (- x)) ^ 3 * exp (- x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (2 * exp (- x) / (1 + exp (- x)) ^ 3 - (1 + exp (- x)) / (1 + exp (- x)) ^ 3) * exp (- x) = (2 * exp (- x) - (1 + exp (- x))) / (1 + exp (- x)) ^ 3 * exp (- x)
[PROOF STEP]
by (metis diff_divide_distrib)
[PROOF STATE]
proof (state)
this:
(2 * exp (- x) / (1 + exp (- x)) ^ 3 - (1 + exp (- x)) / (1 + exp (- x)) ^ 3) * exp (- x) = (2 * exp (- x) - (1 + exp (- x))) / (1 + exp (- x)) ^ 3 * exp (- x)

goal (1 subgoal):
 1. 2 * (exp (- x) * exp (- x)) / (1 + exp (- x)) ^ 3 - exp (- x) / (1 + exp (- x))\<^sup>2 = (exp (- x) - 1) * exp (- x) / (1 + exp (- x)) ^ 3
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
2 * (exp (- x) * exp (- x)) / (1 + exp (- x)) ^ 3 - exp (- x) / (1 + exp (- x))\<^sup>2 = (2 * exp (- x) - (1 + exp (- x))) / (1 + exp (- x)) ^ 3 * exp (- x)
[PROOF STEP]
show
    "2 * (exp (- x) * exp (- x)) / (1 + exp (- x)) ^ 3 - exp (- x) / (1 + exp (- x))\<^sup>2 =
     (exp (- x) - 1) * exp (- x) / (1 + exp (- x)) ^ 3"
[PROOF STATE]
proof (prove)
using this:
2 * (exp (- x) * exp (- x)) / (1 + exp (- x)) ^ 3 - exp (- x) / (1 + exp (- x))\<^sup>2 = (2 * exp (- x) - (1 + exp (- x))) / (1 + exp (- x)) ^ 3 * exp (- x)

goal (1 subgoal):
 1. 2 * (exp (- x) * exp (- x)) / (1 + exp (- x)) ^ 3 - exp (- x) / (1 + exp (- x))\<^sup>2 = (exp (- x) - 1) * exp (- x) / (1 + exp (- x)) ^ 3
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
2 * (exp (- x) * exp (- x)) / (1 + exp (- x)) ^ 3 - exp (- x) / (1 + exp (- x))\<^sup>2 = (exp (- x) - 1) * exp (- x) / (1 + exp (- x)) ^ 3

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma initial_invariant:
  shows "atomic_step_invariant s0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atomic_step_invariant s0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. atomic_step_invariant s0
[PROOF STEP]
have "sp_subset s0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sp_subset s0
[PROOF STEP]
unfolding sp_subset_def s0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>p1 p2. sp_impl_subj_subj \<lparr>sp_impl_subj_subj = Policy.sp_spec_subj_subj, sp_impl_subj_obj = Policy.sp_spec_subj_obj, current = initial_current, obj = initial_obj, thread = \<lambda>_. \<lparr>ev_counter = 0\<rparr>\<rparr> p1 p2 \<longrightarrow> Policy.sp_spec_subj_subj p1 p2) \<and> (\<forall>p1 p2 m. sp_impl_subj_obj \<lparr>sp_impl_subj_subj = Policy.sp_spec_subj_subj, sp_impl_subj_obj = Policy.sp_spec_subj_obj, current = initial_current, obj = initial_obj, thread = \<lambda>_. \<lparr>ev_counter = 0\<rparr>\<rparr> p1 p2 m \<longrightarrow> Policy.sp_spec_subj_obj p1 p2 m)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sp_subset s0

goal (1 subgoal):
 1. atomic_step_invariant s0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
sp_subset s0

goal (1 subgoal):
 1. atomic_step_invariant s0
[PROOF STEP]
unfolding atomic_step_invariant_def
[PROOF STATE]
proof (prove)
using this:
sp_subset s0

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rstate_invariant:
  shows "atomic_step_invariant (\<down>s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atomic_step_invariant \<down> s
[PROOF STEP]
unfolding rep_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atomic_step_invariant (Rep_rstate_t s)
[PROOF STEP]
by (metis Rep_rstate_t mem_Collect_eq)


[STATEMENT]
lemma rstate_down_up[simp]:
  shows "(\<up>\<down>s) = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<up> \<down> s = s
[PROOF STEP]
unfolding rep_def abs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_rstate_t (Rep_rstate_t s) = s
[PROOF STEP]
using Rep_rstate_t_inverse
[PROOF STATE]
proof (prove)
using this:
Abs_rstate_t (Rep_rstate_t ?x) = ?x

goal (1 subgoal):
 1. Abs_rstate_t (Rep_rstate_t s) = s
[PROOF STEP]
by auto


[STATEMENT]
lemma rstate_up_down[simp]:
  assumes "atomic_step_invariant s"
  shows "(\<down>\<up>s) = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<down> \<up> s = s
[PROOF STEP]
using assms Abs_rstate_t_inverse
[PROOF STATE]
proof (prove)
using this:
atomic_step_invariant s
?y \<in> {s. atomic_step_invariant s} \<Longrightarrow> Rep_rstate_t (Abs_rstate_t ?y) = ?y

goal (1 subgoal):
 1. \<down> \<up> s = s
[PROOF STEP]
unfolding rep_def abs_def
[PROOF STATE]
proof (prove)
using this:
atomic_step_invariant s
?y \<in> {s. atomic_step_invariant s} \<Longrightarrow> Rep_rstate_t (Abs_rstate_t ?y) = ?y

goal (1 subgoal):
 1. Rep_rstate_t (Abs_rstate_t s) = s
[PROOF STEP]
by auto


[STATEMENT]
lemma inst_vpeq_rel:
  shows rvpeq_refl: "rvpeq u s s"
    and rvpeq_sym: "rvpeq u s1 s2 \<Longrightarrow> rvpeq u s2 s1"
    and rvpeq_trans: "\<lbrakk> rvpeq u s1 s2; rvpeq u s2 s3 \<rbrakk> \<Longrightarrow> rvpeq u s1 s3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rvpeq u s s &&& (rvpeq u s1 s2 \<Longrightarrow> rvpeq u s2 s1) &&& (\<lbrakk>rvpeq u s1 s2; rvpeq u s2 s3\<rbrakk> \<Longrightarrow> rvpeq u s1 s3)
[PROOF STEP]
unfolding rvpeq_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vpeq (Step.partition u) \<down> s \<down> s &&& (vpeq (Step.partition u) \<down> s1 \<down> s2 \<Longrightarrow> vpeq (Step.partition u) \<down> s2 \<down> s1) &&& (\<lbrakk>vpeq (Step.partition u) \<down> s1 \<down> s2; vpeq (Step.partition u) \<down> s2 \<down> s3\<rbrakk> \<Longrightarrow> vpeq (Step.partition u) \<down> s1 \<down> s3)
[PROOF STEP]
using vpeq_rel
[PROOF STATE]
proof (prove)
using this:
vpeq ?u ?s ?s
vpeq ?u ?s ?t \<Longrightarrow> vpeq ?u ?t ?s
\<lbrakk>vpeq ?u ?s1.0 ?s2.0; vpeq ?u ?s2.0 ?s3.0\<rbrakk> \<Longrightarrow> vpeq ?u ?s1.0 ?s3.0

goal (1 subgoal):
 1. vpeq (Step.partition u) \<down> s \<down> s &&& (vpeq (Step.partition u) \<down> s1 \<down> s2 \<Longrightarrow> vpeq (Step.partition u) \<down> s2 \<down> s1) &&& (\<lbrakk>vpeq (Step.partition u) \<down> s1 \<down> s2; vpeq (Step.partition u) \<down> s2 \<down> s3\<rbrakk> \<Longrightarrow> vpeq (Step.partition u) \<down> s1 \<down> s3)
[PROOF STEP]
by metis+


[STATEMENT]
lemma inst_ifp_refl:
  shows "\<forall> u . rifp u u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>u. rifp u u
[PROOF STEP]
unfolding rifp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>u. Policy.ifp (Step.partition u) (Step.partition u)
[PROOF STEP]
using Policy_properties.ifp_reflexive
[PROOF STATE]
proof (prove)
using this:
\<forall>p. Policy.ifp p p

goal (1 subgoal):
 1. \<forall>u. Policy.ifp (Step.partition u) (Step.partition u)
[PROOF STEP]
by fast


[STATEMENT]
lemma inst_step_atomicity [simp]:
  shows "\<forall> s a . rcurrent (rstep s a) = rcurrent s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s a. rcurrent (rstep s a) = rcurrent s
[PROOF STEP]
unfolding rstep_def rcurrent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s a. current \<down> \<up> atomic_step \<down> s a = current \<down> s
[PROOF STEP]
using atomic_step_does_not_change_current_thread rstate_up_down rstate_invariant atomic_step_preserves_invariants
[PROOF STATE]
proof (prove)
using this:
current (atomic_step ?s ?ipt) = current ?s
atomic_step_invariant ?s \<Longrightarrow> \<down> \<up> ?s = ?s
atomic_step_invariant \<down> ?s
atomic_step_invariant ?s \<Longrightarrow> atomic_step_invariant (atomic_step ?s ?a)

goal (1 subgoal):
 1. \<forall>s a. current \<down> \<up> atomic_step \<down> s a = current \<down> s
[PROOF STEP]
by auto


[STATEMENT]
lemma inst_weakly_step_consistent:
  assumes "rvpeq u s t"
      and "rvpeq (rcurrent s) s t"
      and "rcurrent s = rcurrent t"
      and "rprecondition s (rcurrent s) a"
      and "rprecondition t (rcurrent t) a"
    shows "rvpeq u (rstep s a) (rstep t a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rvpeq u (rstep s a) (rstep t a)
[PROOF STEP]
using assms atomic_step_weakly_step_consistent rstate_invariant atomic_step_preserves_invariants
[PROOF STATE]
proof (prove)
using this:
rvpeq u s t
rvpeq (rcurrent s) s t
rcurrent s = rcurrent t
rprecondition s (rcurrent s) a
rprecondition t (rcurrent t) a
\<lbrakk>vpeq ?u ?s1.0 ?s2.0; vpeq (Step.partition (current ?s1.0)) ?s1.0 ?s2.0; atomic_step_invariant ?s1.0; atomic_step_invariant ?s2.0; atomic_step_precondition ?s1.0 (current ?s1.0) ?ipt; atomic_step_precondition ?s2.0 (current ?s2.0) ?ipt; current ?s1.0 = current ?s2.0\<rbrakk> \<Longrightarrow> vpeq ?u (atomic_step ?s1.0 ?ipt) (atomic_step ?s2.0 ?ipt)
atomic_step_invariant \<down> ?s
atomic_step_invariant ?s \<Longrightarrow> atomic_step_invariant (atomic_step ?s ?a)

goal (1 subgoal):
 1. rvpeq u (rstep s a) (rstep t a)
[PROOF STEP]
unfolding rcurrent_def rstep_def rvpeq_def rprecondition_def
[PROOF STATE]
proof (prove)
using this:
vpeq (Step.partition u) \<down> s \<down> t
vpeq (Step.partition (current \<down> s)) \<down> s \<down> t
current \<down> s = current \<down> t
atomic_step_precondition \<down> s (current \<down> s) a
atomic_step_precondition \<down> t (current \<down> t) a
\<lbrakk>vpeq ?u ?s1.0 ?s2.0; vpeq (Step.partition (current ?s1.0)) ?s1.0 ?s2.0; atomic_step_invariant ?s1.0; atomic_step_invariant ?s2.0; atomic_step_precondition ?s1.0 (current ?s1.0) ?ipt; atomic_step_precondition ?s2.0 (current ?s2.0) ?ipt; current ?s1.0 = current ?s2.0\<rbrakk> \<Longrightarrow> vpeq ?u (atomic_step ?s1.0 ?ipt) (atomic_step ?s2.0 ?ipt)
atomic_step_invariant \<down> ?s
atomic_step_invariant ?s \<Longrightarrow> atomic_step_invariant (atomic_step ?s ?a)

goal (1 subgoal):
 1. vpeq (Step.partition u) \<down> \<up> atomic_step \<down> s a \<down> \<up> atomic_step \<down> t a
[PROOF STEP]
by auto


[STATEMENT]
lemma inst_local_respect:
  assumes not_ifp: "\<not>rifp (rcurrent s) u"
      and prec: "rprecondition s (rcurrent s) a"
    shows "rvpeq u s (rstep s a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rvpeq u s (rstep s a)
[PROOF STEP]
using assms atomic_step_respects_policy rstate_invariant atomic_step_preserves_invariants
[PROOF STATE]
proof (prove)
using this:
\<not> rifp (rcurrent s) u
rprecondition s (rcurrent s) a
\<lbrakk>\<not> Policy.ifp (Step.partition (current ?s)) ?u; atomic_step_invariant ?s; atomic_step_precondition ?s (current ?s) ?ipt\<rbrakk> \<Longrightarrow> vpeq ?u ?s (atomic_step ?s ?ipt)
atomic_step_invariant \<down> ?s
atomic_step_invariant ?s \<Longrightarrow> atomic_step_invariant (atomic_step ?s ?a)

goal (1 subgoal):
 1. rvpeq u s (rstep s a)
[PROOF STEP]
unfolding rifp_def rprecondition_def rvpeq_def rstep_def rcurrent_def
[PROOF STATE]
proof (prove)
using this:
\<not> Policy.ifp (Step.partition (current \<down> s)) (Step.partition u)
atomic_step_precondition \<down> s (current \<down> s) a
\<lbrakk>\<not> Policy.ifp (Step.partition (current ?s)) ?u; atomic_step_invariant ?s; atomic_step_precondition ?s (current ?s) ?ipt\<rbrakk> \<Longrightarrow> vpeq ?u ?s (atomic_step ?s ?ipt)
atomic_step_invariant \<down> ?s
atomic_step_invariant ?s \<Longrightarrow> atomic_step_invariant (atomic_step ?s ?a)

goal (1 subgoal):
 1. vpeq (Step.partition u) \<down> s \<down> \<up> atomic_step \<down> s a
[PROOF STEP]
by auto


[STATEMENT]
lemma inst_output_consistency:
  assumes rvpeq: "rvpeq (rcurrent s) s t"
  and     current_eq: "rcurrent s = rcurrent t"
  shows   "routput_f s a = routput_f t a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. routput_f s a = routput_f t a
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. routput_f s a = routput_f t a
[PROOF STEP]
have "\<forall> a s t. rvpeq (rcurrent s) s t \<and> rcurrent s = rcurrent t \<longrightarrow> routput_f s a = routput_f t a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a s t. rvpeq (rcurrent s) s t \<and> rcurrent s = rcurrent t \<longrightarrow> routput_f s a = routput_f t a
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>a s t. rvpeq (rcurrent s) s t \<and> rcurrent s = rcurrent t \<longrightarrow> routput_f s a = routput_f t a
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>a s t. rvpeq (rcurrent s) s t \<and> rcurrent s = rcurrent t \<longrightarrow> routput_f s a = routput_f t a
[PROOF STEP]
fix a :: raction_t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>a s t. rvpeq (rcurrent s) s t \<and> rcurrent s = rcurrent t \<longrightarrow> routput_f s a = routput_f t a
[PROOF STEP]
fix s t :: rstate_t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>a s t. rvpeq (rcurrent s) s t \<and> rcurrent s = rcurrent t \<longrightarrow> routput_f s a = routput_f t a
[PROOF STEP]
fix p :: page_t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>a s t. rvpeq (rcurrent s) s t \<and> rcurrent s = rcurrent t \<longrightarrow> routput_f s a = routput_f t a
[PROOF STEP]
assume 1: "rvpeq (rcurrent s) s t"
           and 2: "rcurrent s = rcurrent t"
[PROOF STATE]
proof (state)
this:
rvpeq (rcurrent s) s t
rcurrent s = rcurrent t

goal (1 subgoal):
 1. \<forall>a s t. rvpeq (rcurrent s) s t \<and> rcurrent s = rcurrent t \<longrightarrow> routput_f s a = routput_f t a
[PROOF STEP]
let ?part = "partition (rcurrent s)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>a s t. rvpeq (rcurrent s) s t \<and> rcurrent s = rcurrent t \<longrightarrow> routput_f s a = routput_f t a
[PROOF STEP]
have "routput_f s a p = routput_f t a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. routput_f s a p = routput_f t a p
[PROOF STEP]
proof (cases "Policy.sp_spec_subj_obj ?part (PAGE p) READ"
                 rule: case_split [case_names Allowed Denied])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Policy.sp_spec_subj_obj (Step.partition (rcurrent s)) (PAGE p) READ \<Longrightarrow> routput_f s a p = routput_f t a p
 2. \<not> Policy.sp_spec_subj_obj (Step.partition (rcurrent s)) (PAGE p) READ \<Longrightarrow> routput_f s a p = routput_f t a p
[PROOF STEP]
case Allowed
[PROOF STATE]
proof (state)
this:
Policy.sp_spec_subj_obj (Step.partition (rcurrent s)) (PAGE p) READ

goal (2 subgoals):
 1. Policy.sp_spec_subj_obj (Step.partition (rcurrent s)) (PAGE p) READ \<Longrightarrow> routput_f s a p = routput_f t a p
 2. \<not> Policy.sp_spec_subj_obj (Step.partition (rcurrent s)) (PAGE p) READ \<Longrightarrow> routput_f s a p = routput_f t a p
[PROOF STEP]
have 5: "obj (\<down>s) (PAGE p) = obj (\<down>t) (PAGE p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obj \<down> s (PAGE p) = obj \<down> t (PAGE p)
[PROOF STEP]
using 1 Allowed
[PROOF STATE]
proof (prove)
using this:
rvpeq (rcurrent s) s t
Policy.sp_spec_subj_obj (Step.partition (rcurrent s)) (PAGE p) READ

goal (1 subgoal):
 1. obj \<down> s (PAGE p) = obj \<down> t (PAGE p)
[PROOF STEP]
unfolding rvpeq_def vpeq_def vpeq_obj_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>obj_id. Policy.sp_spec_subj_obj (Step.partition (rcurrent s)) obj_id READ \<longrightarrow> obj \<down> s obj_id = obj \<down> t obj_id) \<and> vpeq_subj_subj (Step.partition (rcurrent s)) \<down> s \<down> t \<and> vpeq_subj_obj (Step.partition (rcurrent s)) \<down> s \<down> t \<and> vpeq_local (Step.partition (rcurrent s)) \<down> s \<down> t
Policy.sp_spec_subj_obj (Step.partition (rcurrent s)) (PAGE p) READ

goal (1 subgoal):
 1. obj \<down> s (PAGE p) = obj \<down> t (PAGE p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
obj \<down> s (PAGE p) = obj \<down> t (PAGE p)

goal (2 subgoals):
 1. Policy.sp_spec_subj_obj (Step.partition (rcurrent s)) (PAGE p) READ \<Longrightarrow> routput_f s a p = routput_f t a p
 2. \<not> Policy.sp_spec_subj_obj (Step.partition (rcurrent s)) (PAGE p) READ \<Longrightarrow> routput_f s a p = routput_f t a p
[PROOF STEP]
have 6: "sp_impl_subj_obj (\<down>s) ?part (PAGE p) READ = sp_impl_subj_obj (\<down>t) ?part (PAGE p) READ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sp_impl_subj_obj \<down> s (Step.partition (rcurrent s)) (PAGE p) READ = sp_impl_subj_obj \<down> t (Step.partition (rcurrent s)) (PAGE p) READ
[PROOF STEP]
using 1 2 Allowed
[PROOF STATE]
proof (prove)
using this:
rvpeq (rcurrent s) s t
rcurrent s = rcurrent t
Policy.sp_spec_subj_obj (Step.partition (rcurrent s)) (PAGE p) READ

goal (1 subgoal):
 1. sp_impl_subj_obj \<down> s (Step.partition (rcurrent s)) (PAGE p) READ = sp_impl_subj_obj \<down> t (Step.partition (rcurrent s)) (PAGE p) READ
[PROOF STEP]
unfolding rvpeq_def vpeq_def vpeq_subj_obj_def
[PROOF STATE]
proof (prove)
using this:
vpeq_obj (Step.partition (rcurrent s)) \<down> s \<down> t \<and> vpeq_subj_subj (Step.partition (rcurrent s)) \<down> s \<down> t \<and> (\<forall>ob m p1. (Policy.sp_spec_subj_obj (Step.partition (rcurrent s)) ob m \<longrightarrow> sp_impl_subj_obj \<down> s (Step.partition (rcurrent s)) ob m = sp_impl_subj_obj \<down> t (Step.partition (rcurrent s)) ob m) \<and> (Policy.sp_spec_subj_obj p1 ob PROVIDE \<and> (Policy.sp_spec_subj_obj (Step.partition (rcurrent s)) ob READ \<or> Policy.sp_spec_subj_obj (Step.partition (rcurrent s)) ob WRITE) \<longrightarrow> sp_impl_subj_obj \<down> s p1 ob PROVIDE = sp_impl_subj_obj \<down> t p1 ob PROVIDE)) \<and> vpeq_local (Step.partition (rcurrent s)) \<down> s \<down> t
rcurrent s = rcurrent t
Policy.sp_spec_subj_obj (Step.partition (rcurrent s)) (PAGE p) READ

goal (1 subgoal):
 1. sp_impl_subj_obj \<down> s (Step.partition (rcurrent s)) (PAGE p) READ = sp_impl_subj_obj \<down> t (Step.partition (rcurrent s)) (PAGE p) READ
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sp_impl_subj_obj \<down> s (Step.partition (rcurrent s)) (PAGE p) READ = sp_impl_subj_obj \<down> t (Step.partition (rcurrent s)) (PAGE p) READ

goal (2 subgoals):
 1. Policy.sp_spec_subj_obj (Step.partition (rcurrent s)) (PAGE p) READ \<Longrightarrow> routput_f s a p = routput_f t a p
 2. \<not> Policy.sp_spec_subj_obj (Step.partition (rcurrent s)) (PAGE p) READ \<Longrightarrow> routput_f s a p = routput_f t a p
[PROOF STEP]
show "routput_f s a p = routput_f t a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. routput_f s a p = routput_f t a p
[PROOF STEP]
unfolding routput_f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if sp_impl_subj_obj \<down> s (Step.partition (rcurrent s)) (PAGE p) READ then VALUE (obj \<down> s (PAGE p)) else EXCEPTION) = (if sp_impl_subj_obj \<down> t (Step.partition (rcurrent t)) (PAGE p) READ then VALUE (obj \<down> t (PAGE p)) else EXCEPTION)
[PROOF STEP]
using 2 5 6
[PROOF STATE]
proof (prove)
using this:
rcurrent s = rcurrent t
obj \<down> s (PAGE p) = obj \<down> t (PAGE p)
sp_impl_subj_obj \<down> s (Step.partition (rcurrent s)) (PAGE p) READ = sp_impl_subj_obj \<down> t (Step.partition (rcurrent s)) (PAGE p) READ

goal (1 subgoal):
 1. (if sp_impl_subj_obj \<down> s (Step.partition (rcurrent s)) (PAGE p) READ then VALUE (obj \<down> s (PAGE p)) else EXCEPTION) = (if sp_impl_subj_obj \<down> t (Step.partition (rcurrent t)) (PAGE p) READ then VALUE (obj \<down> t (PAGE p)) else EXCEPTION)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
routput_f s a p = routput_f t a p

goal (1 subgoal):
 1. \<not> Policy.sp_spec_subj_obj (Step.partition (rcurrent s)) (PAGE p) READ \<Longrightarrow> routput_f s a p = routput_f t a p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Policy.sp_spec_subj_obj (Step.partition (rcurrent s)) (PAGE p) READ \<Longrightarrow> routput_f s a p = routput_f t a p
[PROOF STEP]
case Denied
[PROOF STATE]
proof (state)
this:
\<not> Policy.sp_spec_subj_obj (Step.partition (rcurrent s)) (PAGE p) READ

goal (1 subgoal):
 1. \<not> Policy.sp_spec_subj_obj (Step.partition (rcurrent s)) (PAGE p) READ \<Longrightarrow> routput_f s a p = routput_f t a p
[PROOF STEP]
hence "sp_impl_subj_obj (\<down>s) ?part (PAGE p) READ = False"
                and "sp_impl_subj_obj (\<down>t) ?part (PAGE p) READ = False"
[PROOF STATE]
proof (prove)
using this:
\<not> Policy.sp_spec_subj_obj (Step.partition (rcurrent s)) (PAGE p) READ

goal (1 subgoal):
 1. sp_impl_subj_obj \<down> s (Step.partition (rcurrent s)) (PAGE p) READ = False &&& sp_impl_subj_obj \<down> t (Step.partition (rcurrent s)) (PAGE p) READ = False
[PROOF STEP]
using rstate_invariant
[PROOF STATE]
proof (prove)
using this:
\<not> Policy.sp_spec_subj_obj (Step.partition (rcurrent s)) (PAGE p) READ
atomic_step_invariant \<down> ?s

goal (1 subgoal):
 1. sp_impl_subj_obj \<down> s (Step.partition (rcurrent s)) (PAGE p) READ = False &&& sp_impl_subj_obj \<down> t (Step.partition (rcurrent s)) (PAGE p) READ = False
[PROOF STEP]
unfolding atomic_step_invariant_def sp_subset_def
[PROOF STATE]
proof (prove)
using this:
\<not> Policy.sp_spec_subj_obj (Step.partition (rcurrent s)) (PAGE p) READ
(\<forall>p1 p2. sp_impl_subj_subj \<down> ?s p1 p2 \<longrightarrow> Policy.sp_spec_subj_subj p1 p2) \<and> (\<forall>p1 p2 m. sp_impl_subj_obj \<down> ?s p1 p2 m \<longrightarrow> Policy.sp_spec_subj_obj p1 p2 m)

goal (1 subgoal):
 1. sp_impl_subj_obj \<down> s (Step.partition (rcurrent s)) (PAGE p) READ = False &&& sp_impl_subj_obj \<down> t (Step.partition (rcurrent s)) (PAGE p) READ = False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sp_impl_subj_obj \<down> s (Step.partition (rcurrent s)) (PAGE p) READ = False
sp_impl_subj_obj \<down> t (Step.partition (rcurrent s)) (PAGE p) READ = False

goal (1 subgoal):
 1. \<not> Policy.sp_spec_subj_obj (Step.partition (rcurrent s)) (PAGE p) READ \<Longrightarrow> routput_f s a p = routput_f t a p
[PROOF STEP]
thus "routput_f s a p = routput_f t a p"
[PROOF STATE]
proof (prove)
using this:
sp_impl_subj_obj \<down> s (Step.partition (rcurrent s)) (PAGE p) READ = False
sp_impl_subj_obj \<down> t (Step.partition (rcurrent s)) (PAGE p) READ = False

goal (1 subgoal):
 1. routput_f s a p = routput_f t a p
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
sp_impl_subj_obj \<down> s (Step.partition (rcurrent s)) (PAGE p) READ = False
sp_impl_subj_obj \<down> t (Step.partition (rcurrent s)) (PAGE p) READ = False
rcurrent s = rcurrent t

goal (1 subgoal):
 1. routput_f s a p = routput_f t a p
[PROOF STEP]
unfolding routput_f_def
[PROOF STATE]
proof (prove)
using this:
sp_impl_subj_obj \<down> s (Step.partition (rcurrent s)) (PAGE p) READ = False
sp_impl_subj_obj \<down> t (Step.partition (rcurrent s)) (PAGE p) READ = False
rcurrent s = rcurrent t

goal (1 subgoal):
 1. (if sp_impl_subj_obj \<down> s (Step.partition (rcurrent s)) (PAGE p) READ then VALUE (obj \<down> s (PAGE p)) else EXCEPTION) = (if sp_impl_subj_obj \<down> t (Step.partition (rcurrent t)) (PAGE p) READ then VALUE (obj \<down> t (PAGE p)) else EXCEPTION)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
routput_f s a p = routput_f t a p

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
routput_f s a p = routput_f t a p

goal (1 subgoal):
 1. \<forall>a s t. rvpeq (rcurrent s) s t \<and> rcurrent s = rcurrent t \<longrightarrow> routput_f s a = routput_f t a
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>rvpeq (rcurrent ?sa2) ?sa2 ?ta2; rcurrent ?sa2 = rcurrent ?ta2\<rbrakk> \<Longrightarrow> routput_f ?sa2 ?aa2 ?p2 = routput_f ?ta2 ?aa2 ?p2

goal (1 subgoal):
 1. \<forall>a s t. rvpeq (rcurrent s) s t \<and> rcurrent s = rcurrent t \<longrightarrow> routput_f s a = routput_f t a
[PROOF STEP]
thus "\<forall> a s t. rvpeq (rcurrent s) s t \<and> rcurrent s = rcurrent t \<longrightarrow> routput_f s a = routput_f t a"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>rvpeq (rcurrent ?sa2) ?sa2 ?ta2; rcurrent ?sa2 = rcurrent ?ta2\<rbrakk> \<Longrightarrow> routput_f ?sa2 ?aa2 ?p2 = routput_f ?ta2 ?aa2 ?p2

goal (1 subgoal):
 1. \<forall>a s t. rvpeq (rcurrent s) s t \<and> rcurrent s = rcurrent t \<longrightarrow> routput_f s a = routput_f t a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>a s t. rvpeq (rcurrent s) s t \<and> rcurrent s = rcurrent t \<longrightarrow> routput_f s a = routput_f t a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>a s t. rvpeq (rcurrent s) s t \<and> rcurrent s = rcurrent t \<longrightarrow> routput_f s a = routput_f t a

goal (1 subgoal):
 1. routput_f s a = routput_f t a
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>a s t. rvpeq (rcurrent s) s t \<and> rcurrent s = rcurrent t \<longrightarrow> routput_f s a = routput_f t a

goal (1 subgoal):
 1. routput_f s a = routput_f t a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>a s t. rvpeq (rcurrent s) s t \<and> rcurrent s = rcurrent t \<longrightarrow> routput_f s a = routput_f t a
rvpeq (rcurrent s) s t
rcurrent s = rcurrent t

goal (1 subgoal):
 1. routput_f s a = routput_f t a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
routput_f s a = routput_f t a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inst_cswitch_independent_of_state:
  assumes "rcurrent s = rcurrent t"
  shows "rcurrent (rcswitch n s) = rcurrent (rcswitch n t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rcurrent (rcswitch n s) = rcurrent (rcswitch n t)
[PROOF STEP]
using rstate_invariant cswitch_preserves_invariants
[PROOF STATE]
proof (prove)
using this:
atomic_step_invariant \<down> ?s
atomic_step_invariant ?s \<Longrightarrow> atomic_step_invariant (?s\<lparr>current := ?new_current\<rparr>)

goal (1 subgoal):
 1. rcurrent (rcswitch n s) = rcurrent (rcswitch n t)
[PROOF STEP]
unfolding rcurrent_def rcswitch_def
[PROOF STATE]
proof (prove)
using this:
atomic_step_invariant \<down> ?s
atomic_step_invariant ?s \<Longrightarrow> atomic_step_invariant (?s\<lparr>current := ?new_current\<rparr>)

goal (1 subgoal):
 1. current \<down> \<up> \<down> s\<lparr>current := Eps rinvariant\<rparr> = current \<down> \<up> \<down> t\<lparr>current := Eps rinvariant\<rparr>
[PROOF STEP]
by simp


[STATEMENT]
lemma prec_first_IPC_action:
assumes "is_SK_IPC aseq"
  shows "rprecondition s d (hd aseq)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rprecondition s d (hd aseq)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_SK_IPC aseq

goal (1 subgoal):
 1. rprecondition s d (hd aseq)
[PROOF STEP]
unfolding is_SK_IPC_def rprecondition_def atomic_step_precondition_def
[PROOF STATE]
proof (prove)
using this:
\<exists>dir partner page. aseq = [SK_IPC dir PREP partner page, SK_IPC dir WAIT partner page, SK_IPC dir (BUF (Eps rinvariant)) partner page]

goal (1 subgoal):
 1. case hd aseq of SK_IPC dir PREP partner page \<Rightarrow> True | SK_IPC dir WAIT partner page \<Rightarrow> ipc_precondition d dir partner page \<down> s | SK_IPC dir (BUF page') partner page \<Rightarrow> ipc_precondition d dir partner page \<down> s \<and> ipc_precondition partner (opposite_ipc_direction dir) d page' \<down> s | SK_EV_WAIT ev_wait_stage_t x \<Rightarrow> rinvariant x | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> True | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> ev_signal_precondition d partner \<down> s | NONE \<Rightarrow> True
[PROOF STEP]
by auto


[STATEMENT]
lemma prec_first_EV_WAIT_action:
assumes "is_SK_EV_WAIT aseq"
  shows "rprecondition s d (hd aseq)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rprecondition s d (hd aseq)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_SK_EV_WAIT aseq

goal (1 subgoal):
 1. rprecondition s d (hd aseq)
[PROOF STEP]
unfolding is_SK_EV_WAIT_def rprecondition_def atomic_step_precondition_def
[PROOF STATE]
proof (prove)
using this:
\<exists>consume. aseq = [SK_EV_WAIT EV_PREP consume, SK_EV_WAIT EV_WAIT consume, SK_EV_WAIT EV_FINISH consume]

goal (1 subgoal):
 1. case hd aseq of SK_IPC dir PREP partner page \<Rightarrow> True | SK_IPC dir WAIT partner page \<Rightarrow> ipc_precondition d dir partner page \<down> s | SK_IPC dir (BUF page') partner page \<Rightarrow> ipc_precondition d dir partner page \<down> s \<and> ipc_precondition partner (opposite_ipc_direction dir) d page' \<down> s | SK_EV_WAIT ev_wait_stage_t x \<Rightarrow> rinvariant x | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> True | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> ev_signal_precondition d partner \<down> s | NONE \<Rightarrow> True
[PROOF STEP]
by auto


[STATEMENT]
lemma prec_first_EV_SIGNAL_action:
assumes "is_SK_EV_SIGNAL aseq"
  shows "rprecondition s d (hd aseq)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rprecondition s d (hd aseq)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_SK_EV_SIGNAL aseq

goal (1 subgoal):
 1. rprecondition s d (hd aseq)
[PROOF STEP]
unfolding is_SK_EV_SIGNAL_def rprecondition_def atomic_step_precondition_def
          ev_signal_precondition_def
[PROOF STATE]
proof (prove)
using this:
\<exists>partner. aseq = [SK_EV_SIGNAL EV_SIGNAL_PREP partner, SK_EV_SIGNAL EV_SIGNAL_FINISH partner]

goal (1 subgoal):
 1. case hd aseq of SK_IPC dir PREP partner page \<Rightarrow> True | SK_IPC dir WAIT partner page \<Rightarrow> ipc_precondition d dir partner page \<down> s | SK_IPC dir (BUF page') partner page \<Rightarrow> ipc_precondition d dir partner page \<down> s \<and> ipc_precondition partner (opposite_ipc_direction dir) d page' \<down> s | SK_EV_WAIT ev_wait_stage_t x \<Rightarrow> rinvariant x | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> True | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> sp_impl_subj_subj \<down> s (Step.partition d) (Step.partition partner) | NONE \<Rightarrow> True
[PROOF STEP]
by auto


[STATEMENT]
lemma prec_after_IPC_step:
assumes prec: "rprecondition s (rcurrent s) (aseq ! n)"
    and n_bound: "Suc n < length aseq"
    and IPC: "is_SK_IPC aseq"
    and not_aborting: "\<not>raborting s (rcurrent s) (aseq ! n)"
    and not_waiting: "\<not>rwaiting s (rcurrent s) (aseq ! n)"
shows "rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
fix dir partner page
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
let ?page' = "(SOME page' . True)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
assume IPC: "aseq = [SK_IPC dir PREP partner page,SK_IPC dir WAIT partner page,SK_IPC dir (BUF ?page') partner page]"
[PROOF STATE]
proof (state)
this:
aseq = [SK_IPC dir PREP partner page, SK_IPC dir WAIT partner page, SK_IPC dir (BUF (Eps rinvariant)) partner page]

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
aseq = [SK_IPC dir PREP partner page, SK_IPC dir WAIT partner page, SK_IPC dir (BUF (Eps rinvariant)) partner page]

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
assume 0: "n=0"
[PROOF STATE]
proof (state)
this:
n = 0

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
from 0 IPC prec not_aborting
[PROOF STATE]
proof (chain)
picking this:
n = 0
aseq = [SK_IPC dir PREP partner page, SK_IPC dir WAIT partner page, SK_IPC dir (BUF (Eps rinvariant)) partner page]
rprecondition s (rcurrent s) (aseq ! n)
\<not> raborting s (rcurrent s) (aseq ! n)
[PROOF STEP]
have ?thesis
[PROOF STATE]
proof (prove)
using this:
n = 0
aseq = [SK_IPC dir PREP partner page, SK_IPC dir WAIT partner page, SK_IPC dir (BUF (Eps rinvariant)) partner page]
rprecondition s (rcurrent s) (aseq ! n)
\<not> raborting s (rcurrent s) (aseq ! n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
unfolding rprecondition_def atomic_step_precondition_def rstep_def rcurrent_def atomic_step_def atomic_step_ipc_def aborting_def
[PROOF STATE]
proof (prove)
using this:
n = 0
aseq = [SK_IPC dir PREP partner page, SK_IPC dir WAIT partner page, SK_IPC dir (BUF (Eps rinvariant)) partner page]
case aseq ! n of SK_IPC dir PREP partner page \<Rightarrow> True | SK_IPC dir WAIT partner page \<Rightarrow> ipc_precondition (current \<down> s) dir partner page \<down> s | SK_IPC dir (BUF page') partner page \<Rightarrow> ipc_precondition (current \<down> s) dir partner page \<down> s \<and> ipc_precondition partner (opposite_ipc_direction dir) (current \<down> s) page' \<down> s | SK_EV_WAIT ev_wait_stage_t x \<Rightarrow> rinvariant x | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> True | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> ev_signal_precondition (current \<down> s) partner \<down> s | NONE \<Rightarrow> True
\<not> (case aseq ! n of SK_IPC dir PREP partner page \<Rightarrow> \<not> ipc_precondition (current \<down> s) dir partner page \<down> s | SK_IPC dir _ partner page \<Rightarrow> False | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> \<not> ev_signal_precondition (current \<down> s) partner \<down> s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> False | _ \<Rightarrow> False)

goal (1 subgoal):
 1. case aseq ! Suc n of SK_IPC dir PREP partner page \<Rightarrow> True | SK_IPC dir WAIT partner page \<Rightarrow> ipc_precondition (current \<down> s) dir partner page \<down> \<up> case aseq ! n of SK_IPC SEND (BUF page') partner page \<Rightarrow> set_object_value (PAGE page') (obj \<down> s (PAGE page)) \<down> s | SK_IPC RECV (BUF page') partner page \<Rightarrow> \<down> s | SK_IPC dir _ partner page \<Rightarrow> \<down> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ALL \<Rightarrow> atomic_step_ev_wait_all (current \<down> s) \<down> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ONE \<Rightarrow> atomic_step_ev_wait_one (current \<down> s) \<down> s | SK_EV_WAIT _ consume \<Rightarrow> \<down> s | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> \<down> s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> atomic_step_ev_signal (current \<down> s) partner \<down> s | NONE \<Rightarrow> \<down> s | SK_IPC dir (BUF page') partner page \<Rightarrow> ipc_precondition (current \<down> s) dir partner page \<down> \<up> case aseq ! n of SK_IPC SEND (BUF page') partner page \<Rightarrow> set_object_value (PAGE page') (obj \<down> s (PAGE page)) \<down> s | SK_IPC RECV (BUF page') partner page \<Rightarrow> \<down> s | SK_IPC dir _ partner page \<Rightarrow> \<down> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ALL \<Rightarrow> atomic_step_ev_wait_all (current \<down> s) \<down> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ONE \<Rightarrow> atomic_step_ev_wait_one (current \<down> s) \<down> s | SK_EV_WAIT _ consume \<Rightarrow> \<down> s | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> \<down> s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> atomic_step_ev_signal (current \<down> s) partner \<down> s | NONE \<Rightarrow> \<down> s \<and> ipc_precondition partner (opposite_ipc_direction dir) (current \<down> s) page' \<down> \<up> case aseq ! n of SK_IPC SEND (BUF page') partner page \<Rightarrow> set_object_value (PAGE page') (obj \<down> s (PAGE page)) \<down> s | SK_IPC RECV (BUF page') partner page \<Rightarrow> \<down> s | SK_IPC dir _ partner page \<Rightarrow> \<down> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ALL \<Rightarrow> atomic_step_ev_wait_all (current \<down> s) \<down> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ONE \<Rightarrow> atomic_step_ev_wait_one (current \<down> s) \<down> s | SK_EV_WAIT _ consume \<Rightarrow> \<down> s | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> \<down> s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> atomic_step_ev_signal (current \<down> s) partner \<down> s | NONE \<Rightarrow> \<down> s | SK_EV_WAIT ev_wait_stage_t x \<Rightarrow> rinvariant x | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> True | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> ev_signal_precondition (current \<down> s) partner \<down> \<up> case aseq ! n of SK_IPC SEND (BUF page') partner page \<Rightarrow> set_object_value (PAGE page') (obj \<down> s (PAGE page)) \<down> s | SK_IPC RECV (BUF page') partner page \<Rightarrow> \<down> s | SK_IPC dir _ partner page \<Rightarrow> \<down> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ALL \<Rightarrow> atomic_step_ev_wait_all (current \<down> s) \<down> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ONE \<Rightarrow> atomic_step_ev_wait_one (current \<down> s) \<down> s | SK_EV_WAIT _ consume \<Rightarrow> \<down> s | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> \<down> s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> atomic_step_ev_signal (current \<down> s) partner \<down> s | NONE \<Rightarrow> \<down> s | NONE \<Rightarrow> True
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
n = 0 \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n = 0 \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
n = 0 \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
assume 1: "n=1"
[PROOF STATE]
proof (state)
this:
n = 1

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
from 1 IPC prec not_waiting
[PROOF STATE]
proof (chain)
picking this:
n = 1
aseq = [SK_IPC dir PREP partner page, SK_IPC dir WAIT partner page, SK_IPC dir (BUF (Eps rinvariant)) partner page]
rprecondition s (rcurrent s) (aseq ! n)
\<not> rwaiting s (rcurrent s) (aseq ! n)
[PROOF STEP]
have ?thesis
[PROOF STATE]
proof (prove)
using this:
n = 1
aseq = [SK_IPC dir PREP partner page, SK_IPC dir WAIT partner page, SK_IPC dir (BUF (Eps rinvariant)) partner page]
rprecondition s (rcurrent s) (aseq ! n)
\<not> rwaiting s (rcurrent s) (aseq ! n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
unfolding rprecondition_def atomic_step_precondition_def rstep_def rcurrent_def atomic_step_def atomic_step_ipc_def waiting_def
[PROOF STATE]
proof (prove)
using this:
n = 1
aseq = [SK_IPC dir PREP partner page, SK_IPC dir WAIT partner page, SK_IPC dir (BUF (Eps rinvariant)) partner page]
case aseq ! n of SK_IPC dir PREP partner page \<Rightarrow> True | SK_IPC dir WAIT partner page \<Rightarrow> ipc_precondition (current \<down> s) dir partner page \<down> s | SK_IPC dir (BUF page') partner page \<Rightarrow> ipc_precondition (current \<down> s) dir partner page \<down> s \<and> ipc_precondition partner (opposite_ipc_direction dir) (current \<down> s) page' \<down> s | SK_EV_WAIT ev_wait_stage_t x \<Rightarrow> rinvariant x | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> True | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> ev_signal_precondition (current \<down> s) partner \<down> s | NONE \<Rightarrow> True
\<not> (case aseq ! n of SK_IPC dir WAIT partner page \<Rightarrow> \<not> ipc_precondition partner (opposite_ipc_direction dir) (current \<down> s) (Eps rinvariant) \<down> s | SK_IPC dir _ partner page \<Rightarrow> False | SK_EV_WAIT EV_WAIT x \<Rightarrow> ev_counter (thread \<down> s (current \<down> s)) = 0 | SK_EV_WAIT _ x \<Rightarrow> False | _ \<Rightarrow> False)

goal (1 subgoal):
 1. case aseq ! Suc n of SK_IPC dir PREP partner page \<Rightarrow> True | SK_IPC dir WAIT partner page \<Rightarrow> ipc_precondition (current \<down> s) dir partner page \<down> \<up> case aseq ! n of SK_IPC SEND (BUF page') partner page \<Rightarrow> set_object_value (PAGE page') (obj \<down> s (PAGE page)) \<down> s | SK_IPC RECV (BUF page') partner page \<Rightarrow> \<down> s | SK_IPC dir _ partner page \<Rightarrow> \<down> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ALL \<Rightarrow> atomic_step_ev_wait_all (current \<down> s) \<down> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ONE \<Rightarrow> atomic_step_ev_wait_one (current \<down> s) \<down> s | SK_EV_WAIT _ consume \<Rightarrow> \<down> s | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> \<down> s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> atomic_step_ev_signal (current \<down> s) partner \<down> s | NONE \<Rightarrow> \<down> s | SK_IPC dir (BUF page') partner page \<Rightarrow> ipc_precondition (current \<down> s) dir partner page \<down> \<up> case aseq ! n of SK_IPC SEND (BUF page') partner page \<Rightarrow> set_object_value (PAGE page') (obj \<down> s (PAGE page)) \<down> s | SK_IPC RECV (BUF page') partner page \<Rightarrow> \<down> s | SK_IPC dir _ partner page \<Rightarrow> \<down> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ALL \<Rightarrow> atomic_step_ev_wait_all (current \<down> s) \<down> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ONE \<Rightarrow> atomic_step_ev_wait_one (current \<down> s) \<down> s | SK_EV_WAIT _ consume \<Rightarrow> \<down> s | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> \<down> s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> atomic_step_ev_signal (current \<down> s) partner \<down> s | NONE \<Rightarrow> \<down> s \<and> ipc_precondition partner (opposite_ipc_direction dir) (current \<down> s) page' \<down> \<up> case aseq ! n of SK_IPC SEND (BUF page') partner page \<Rightarrow> set_object_value (PAGE page') (obj \<down> s (PAGE page)) \<down> s | SK_IPC RECV (BUF page') partner page \<Rightarrow> \<down> s | SK_IPC dir _ partner page \<Rightarrow> \<down> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ALL \<Rightarrow> atomic_step_ev_wait_all (current \<down> s) \<down> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ONE \<Rightarrow> atomic_step_ev_wait_one (current \<down> s) \<down> s | SK_EV_WAIT _ consume \<Rightarrow> \<down> s | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> \<down> s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> atomic_step_ev_signal (current \<down> s) partner \<down> s | NONE \<Rightarrow> \<down> s | SK_EV_WAIT ev_wait_stage_t x \<Rightarrow> rinvariant x | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> True | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> ev_signal_precondition (current \<down> s) partner \<down> \<up> case aseq ! n of SK_IPC SEND (BUF page') partner page \<Rightarrow> set_object_value (PAGE page') (obj \<down> s (PAGE page)) \<down> s | SK_IPC RECV (BUF page') partner page \<Rightarrow> \<down> s | SK_IPC dir _ partner page \<Rightarrow> \<down> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ALL \<Rightarrow> atomic_step_ev_wait_all (current \<down> s) \<down> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ONE \<Rightarrow> atomic_step_ev_wait_one (current \<down> s) \<down> s | SK_EV_WAIT _ consume \<Rightarrow> \<down> s | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> \<down> s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> atomic_step_ev_signal (current \<down> s) partner \<down> s | NONE \<Rightarrow> \<down> s | NONE \<Rightarrow> True
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
n = 1 \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n = 1 \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
from IPC
[PROOF STATE]
proof (chain)
picking this:
aseq = [SK_IPC dir PREP partner page, SK_IPC dir WAIT partner page, SK_IPC dir (BUF (Eps rinvariant)) partner page]
[PROOF STEP]
have "length aseq = 3"
[PROOF STATE]
proof (prove)
using this:
aseq = [SK_IPC dir PREP partner page, SK_IPC dir WAIT partner page, SK_IPC dir (BUF (Eps rinvariant)) partner page]

goal (1 subgoal):
 1. length aseq = 3
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length aseq = 3

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n = 0 \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
n = 1 \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
length aseq = 3
[PROOF STEP]
have ?thesis
[PROOF STATE]
proof (prove)
using this:
n = 0 \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
n = 1 \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
length aseq = 3

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
using n_bound
[PROOF STATE]
proof (prove)
using this:
n = 0 \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
n = 1 \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
length aseq = 3
Suc n < length aseq

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
aseq = [SK_IPC ?dir2 PREP ?partner2 ?page2, SK_IPC ?dir2 WAIT ?partner2 ?page2, SK_IPC ?dir2 (BUF (Eps rinvariant)) ?partner2 ?page2] \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
aseq = [SK_IPC ?dir2 PREP ?partner2 ?page2, SK_IPC ?dir2 WAIT ?partner2 ?page2, SK_IPC ?dir2 (BUF (Eps rinvariant)) ?partner2 ?page2] \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
using IPC
[PROOF STATE]
proof (prove)
using this:
aseq = [SK_IPC ?dir2 PREP ?partner2 ?page2, SK_IPC ?dir2 WAIT ?partner2 ?page2, SK_IPC ?dir2 (BUF (Eps rinvariant)) ?partner2 ?page2] \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
is_SK_IPC aseq

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
unfolding is_SK_IPC_def
[PROOF STATE]
proof (prove)
using this:
aseq = [SK_IPC ?dir2 PREP ?partner2 ?page2, SK_IPC ?dir2 WAIT ?partner2 ?page2, SK_IPC ?dir2 (BUF (Eps rinvariant)) ?partner2 ?page2] \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
\<exists>dir partner page. aseq = [SK_IPC dir PREP partner page, SK_IPC dir WAIT partner page, SK_IPC dir (BUF (Eps rinvariant)) partner page]

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal:
No subgoals!
[PROOF STEP]
qed