[STATEMENT]
lemma sync_\<phi>1_\<phi>2:
assumes v1: "validTrans trn1" and r1: "reach (srcOf trn1)"
and v2: "validTrans trn2" and s2: "reach (srcOf trn2)"
and c1: "isCom1 trn1" and c2: "isCom2 trn2"
and sn: "sync trn1 trn2"
shows "\<phi>1 trn1 \<longleftrightarrow> \<phi>2 trn2" (is "?A \<longleftrightarrow> ?B")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi>1 trn1 = \<phi>2 trn2
[PROOF STEP]
proof(cases trn1)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. trn1 = Trans x1 x2 x3 x4 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
[PROOF STEP]
case (Trans s1 a1 ou1 s1')
[PROOF STATE]
proof (state)
this:
trn1 = Trans s1 a1 ou1 s1'

goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. trn1 = Trans x1 x2 x3 x4 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
[PROOF STEP]
note trn1 = Trans
[PROOF STATE]
proof (state)
this:
trn1 = Trans s1 a1 ou1 s1'

goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. trn1 = Trans x1 x2 x3 x4 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
[PROOF STEP]
hence step1: "step s1 a1 = (ou1,s1')"
[PROOF STATE]
proof (prove)
using this:
trn1 = Trans s1 a1 ou1 s1'

goal (1 subgoal):
 1. step s1 a1 = (ou1, s1')
[PROOF STEP]
using v1
[PROOF STATE]
proof (prove)
using this:
trn1 = Trans s1 a1 ou1 s1'
Iss.validTrans trn1

goal (1 subgoal):
 1. step s1 a1 = (ou1, s1')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
step s1 a1 = (ou1, s1')

goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. trn1 = Trans x1 x2 x3 x4 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi>1 trn1 = \<phi>2 trn2
[PROOF STEP]
proof(cases trn2)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. trn2 = Trans x1 x2 x3 x4 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
[PROOF STEP]
case (Trans s2 a2 ou2 s2')
[PROOF STATE]
proof (state)
this:
trn2 = Trans s2 a2 ou2 s2'

goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. trn2 = Trans x1 x2 x3 x4 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
[PROOF STEP]
note trn2 = Trans
[PROOF STATE]
proof (state)
this:
trn2 = Trans s2 a2 ou2 s2'

goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. trn2 = Trans x1 x2 x3 x4 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
[PROOF STEP]
hence step2: "step s2 a2 = (ou2,s2')"
[PROOF STATE]
proof (prove)
using this:
trn2 = Trans s2 a2 ou2 s2'

goal (1 subgoal):
 1. step s2 a2 = (ou2, s2')
[PROOF STEP]
using v2
[PROOF STATE]
proof (prove)
using this:
trn2 = Trans s2 a2 ou2 s2'
Iss.validTrans trn2

goal (1 subgoal):
 1. step s2 a2 = (ou2, s2')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
step s2 a2 = (ou2, s2')

goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. trn2 = Trans x1 x2 x3 x4 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi>1 trn1 = \<phi>2 trn2
[PROOF STEP]
proof(cases a1)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x1. a1 = Sact x1 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 2. \<And>x2. a1 = Cact x2 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 3. \<And>x3. a1 = Dact x3 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 4. \<And>x4. a1 = Uact x4 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 5. \<And>x5. a1 = Ract x5 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 6. \<And>x6. a1 = Lact x6 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 7. \<And>x7. a1 = COMact x7 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
[PROOF STEP]
case (COMact ca1)
[PROOF STATE]
proof (state)
this:
a1 = COMact ca1

goal (7 subgoals):
 1. \<And>x1. a1 = Sact x1 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 2. \<And>x2. a1 = Cact x2 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 3. \<And>x3. a1 = Dact x3 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 4. \<And>x4. a1 = Uact x4 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 5. \<And>x5. a1 = Ract x5 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 6. \<And>x6. a1 = Lact x6 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 7. \<And>x7. a1 = COMact x7 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
[PROOF STEP]
note a1 = COMact
[PROOF STATE]
proof (state)
this:
a1 = COMact ca1

goal (7 subgoals):
 1. \<And>x1. a1 = Sact x1 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 2. \<And>x2. a1 = Cact x2 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 3. \<And>x3. a1 = Dact x3 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 4. \<And>x4. a1 = Uact x4 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 5. \<And>x5. a1 = Ract x5 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 6. \<And>x6. a1 = Lact x6 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 7. \<And>x7. a1 = COMact x7 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi>1 trn1 = \<phi>2 trn2
[PROOF STEP]
proof(cases a2)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x1. a2 = Sact x1 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 2. \<And>x2. a2 = Cact x2 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 3. \<And>x3. a2 = Dact x3 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 4. \<And>x4. a2 = Uact x4 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 5. \<And>x5. a2 = Ract x5 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 6. \<And>x6. a2 = Lact x6 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 7. \<And>x7. a2 = COMact x7 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
[PROOF STEP]
case (COMact ca2)
[PROOF STATE]
proof (state)
this:
a2 = COMact ca2

goal (7 subgoals):
 1. \<And>x1. a2 = Sact x1 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 2. \<And>x2. a2 = Cact x2 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 3. \<And>x3. a2 = Dact x3 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 4. \<And>x4. a2 = Uact x4 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 5. \<And>x5. a2 = Ract x5 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 6. \<And>x6. a2 = Lact x6 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 7. \<And>x7. a2 = COMact x7 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
[PROOF STEP]
note a2 = COMact
[PROOF STATE]
proof (state)
this:
a2 = COMact ca2

goal (7 subgoals):
 1. \<And>x1. a2 = Sact x1 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 2. \<And>x2. a2 = Cact x2 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 3. \<And>x3. a2 = Dact x3 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 4. \<And>x4. a2 = Uact x4 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 5. \<And>x5. a2 = Ract x5 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 6. \<And>x6. a2 = Lact x6 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 7. \<And>x7. a2 = COMact x7 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
[PROOF STEP]
have "?A \<longleftrightarrow> (\<exists>aid1. ca1 =
             (comSendPost (admin s1) (pass s1 (admin s1)) aid1
               PID) \<and>
            ou1 =
            O_sendPost
             (aid1, clientPass s1 aid1, PID, post s1 PID,
              owner s1 PID, vis s1 PID))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi>1 trn1 = (\<exists>aid1. ca1 = comSendPost (admin s1) (pass s1 (admin s1)) aid1 PID \<and> ou1 = O_sendPost (aid1, clientPass s1 aid1, PID, post s1 PID, owner s1 PID, vis s1 PID))
[PROOF STEP]
using c1
[PROOF STATE]
proof (prove)
using this:
isCom1 trn1

goal (1 subgoal):
 1. \<phi>1 trn1 = (\<exists>aid1. ca1 = comSendPost (admin s1) (pass s1 (admin s1)) aid1 PID \<and> ou1 = O_sendPost (aid1, clientPass s1 aid1, PID, post s1 PID, owner s1 PID, vis s1 PID))
[PROOF STEP]
unfolding trn1 Iss.\<phi>_def3[OF step1]
[PROOF STATE]
proof (prove)
using this:
isCom1 (Trans s1 a1 ou1 s1')

goal (1 subgoal):
 1. ((\<exists>pst. a1 = Uact (uPost (owner s1 PID) (pass s1 (owner s1 PID)) PID pst) \<and> ou1 = outOK) \<or> (\<exists>aid. a1 = COMact (comSendPost (admin s1) (pass s1 (admin s1)) aid PID) \<and> ou1 = O_sendPost (aid, clientPass s1 aid, PID, post s1 PID, owner s1 PID, vis s1 PID))) = (\<exists>aid1. ca1 = comSendPost (admin s1) (pass s1 (admin s1)) aid1 PID \<and> ou1 = O_sendPost (aid1, clientPass s1 aid1, PID, post s1 PID, owner s1 PID, vis s1 PID))
[PROOF STEP]
unfolding a1
[PROOF STATE]
proof (prove)
using this:
isCom1 (Trans s1 (COMact ca1) ou1 s1')

goal (1 subgoal):
 1. ((\<exists>pst. COMact ca1 = Uact (uPost (owner s1 PID) (pass s1 (owner s1 PID)) PID pst) \<and> ou1 = outOK) \<or> (\<exists>aid. COMact ca1 = COMact (comSendPost (admin s1) (pass s1 (admin s1)) aid PID) \<and> ou1 = O_sendPost (aid, clientPass s1 aid, PID, post s1 PID, owner s1 PID, vis s1 PID))) = (\<exists>aid1. ca1 = comSendPost (admin s1) (pass s1 (admin s1)) aid1 PID \<and> ou1 = O_sendPost (aid1, clientPass s1 aid1, PID, post s1 PID, owner s1 PID, vis s1 PID))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<phi>1 trn1 = (\<exists>aid1. ca1 = comSendPost (admin s1) (pass s1 (admin s1)) aid1 PID \<and> ou1 = O_sendPost (aid1, clientPass s1 aid1, PID, post s1 PID, owner s1 PID, vis s1 PID))

goal (7 subgoals):
 1. \<And>x1. a2 = Sact x1 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 2. \<And>x2. a2 = Cact x2 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 3. \<And>x3. a2 = Dact x3 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 4. \<And>x4. a2 = Uact x4 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 5. \<And>x5. a2 = Ract x5 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 6. \<And>x6. a2 = Lact x6 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 7. \<And>x7. a2 = COMact x7 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<phi>1 trn1 = (\<exists>aid1. ca1 = comSendPost (admin s1) (pass s1 (admin s1)) aid1 PID \<and> ou1 = O_sendPost (aid1, clientPass s1 aid1, PID, post s1 PID, owner s1 PID, vis s1 PID))

goal (7 subgoals):
 1. \<And>x1. a2 = Sact x1 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 2. \<And>x2. a2 = Cact x2 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 3. \<And>x3. a2 = Dact x3 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 4. \<And>x4. a2 = Uact x4 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 5. \<And>x5. a2 = Ract x5 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 6. \<And>x6. a2 = Lact x6 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 7. \<And>x7. a2 = COMact x7 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
[PROOF STEP]
have "\<dots> \<longleftrightarrow> (\<exists>uid2 pst2 vs2.
        ca2 = comReceivePost AID1 (serverPass s2 AID1) PID pst2 uid2 vs2 \<and> ou2 = outOK)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>aid1. ca1 = comSendPost (admin s1) (pass s1 (admin s1)) aid1 PID \<and> ou1 = O_sendPost (aid1, clientPass s1 aid1, PID, post s1 PID, owner s1 PID, vis s1 PID)) = (\<exists>uid2 pst2 vs2. ca2 = comReceivePost AID1 (serverPass s2 AID1) PID pst2 uid2 vs2 \<and> ou2 = outOK)
[PROOF STEP]
using sn step1 step2
[PROOF STATE]
proof (prove)
using this:
sync trn1 trn2
step s1 a1 = (ou1, s1')
step s2 a2 = (ou2, s2')

goal (1 subgoal):
 1. (\<exists>aid1. ca1 = comSendPost (admin s1) (pass s1 (admin s1)) aid1 PID \<and> ou1 = O_sendPost (aid1, clientPass s1 aid1, PID, post s1 PID, owner s1 PID, vis s1 PID)) = (\<exists>uid2 pst2 vs2. ca2 = comReceivePost AID1 (serverPass s2 AID1) PID pst2 uid2 vs2 \<and> ou2 = outOK)
[PROOF STEP]
unfolding trn1 trn2 a1 a2
[PROOF STATE]
proof (prove)
using this:
sync (Trans s1 (COMact ca1) ou1 s1') (Trans s2 (COMact ca2) ou2 s2')
step s1 (COMact ca1) = (ou1, s1')
step s2 (COMact ca2) = (ou2, s2')

goal (1 subgoal):
 1. (\<exists>aid1. ca1 = comSendPost (admin s1) (pass s1 (admin s1)) aid1 PID \<and> ou1 = O_sendPost (aid1, clientPass s1 aid1, PID, post s1 PID, owner s1 PID, vis s1 PID)) = (\<exists>uid2 pst2 vs2. ca2 = comReceivePost AID1 (serverPass s2 AID1) PID pst2 uid2 vs2 \<and> ou2 = outOK)
[PROOF STEP]
apply(cases ca1)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>sync (Trans s1 (COMact ca1) ou1 s1') (Trans s2 (COMact ca2) ou2 s2'); step s1 (COMact ca1) = (ou1, s1'); step s2 (COMact ca2) = (ou2, s2'); ca1 = comSendServerReq x11 x12 x13 x14\<rbrakk> \<Longrightarrow> (\<exists>aid1. ca1 = comSendPost (admin s1) (pass s1 (admin s1)) aid1 PID \<and> ou1 = O_sendPost (aid1, clientPass s1 aid1, PID, post s1 PID, owner s1 PID, vis s1 PID)) = (\<exists>uid2 pst2 vs2. ca2 = comReceivePost AID1 (serverPass s2 AID1) PID pst2 uid2 vs2 \<and> ou2 = outOK)
 2. \<And>x21 x22. \<lbrakk>sync (Trans s1 (COMact ca1) ou1 s1') (Trans s2 (COMact ca2) ou2 s2'); step s1 (COMact ca1) = (ou1, s1'); step s2 (COMact ca2) = (ou2, s2'); ca1 = comReceiveClientReq x21 x22\<rbrakk> \<Longrightarrow> (\<exists>aid1. ca1 = comSendPost (admin s1) (pass s1 (admin s1)) aid1 PID \<and> ou1 = O_sendPost (aid1, clientPass s1 aid1, PID, post s1 PID, owner s1 PID, vis s1 PID)) = (\<exists>uid2 pst2 vs2. ca2 = comReceivePost AID1 (serverPass s2 AID1) PID pst2 uid2 vs2 \<and> ou2 = outOK)
 3. \<And>x31 x32 x33 x34. \<lbrakk>sync (Trans s1 (COMact ca1) ou1 s1') (Trans s2 (COMact ca2) ou2 s2'); step s1 (COMact ca1) = (ou1, s1'); step s2 (COMact ca2) = (ou2, s2'); ca1 = comConnectClient x31 x32 x33 x34\<rbrakk> \<Longrightarrow> (\<exists>aid1. ca1 = comSendPost (admin s1) (pass s1 (admin s1)) aid1 PID \<and> ou1 = O_sendPost (aid1, clientPass s1 aid1, PID, post s1 PID, owner s1 PID, vis s1 PID)) = (\<exists>uid2 pst2 vs2. ca2 = comReceivePost AID1 (serverPass s2 AID1) PID pst2 uid2 vs2 \<and> ou2 = outOK)
 4. \<And>x41 x42. \<lbrakk>sync (Trans s1 (COMact ca1) ou1 s1') (Trans s2 (COMact ca2) ou2 s2'); step s1 (COMact ca1) = (ou1, s1'); step s2 (COMact ca2) = (ou2, s2'); ca1 = comConnectServer x41 x42\<rbrakk> \<Longrightarrow> (\<exists>aid1. ca1 = comSendPost (admin s1) (pass s1 (admin s1)) aid1 PID \<and> ou1 = O_sendPost (aid1, clientPass s1 aid1, PID, post s1 PID, owner s1 PID, vis s1 PID)) = (\<exists>uid2 pst2 vs2. ca2 = comReceivePost AID1 (serverPass s2 AID1) PID pst2 uid2 vs2 \<and> ou2 = outOK)
 5. \<And>x51 x52 x53 x54 x55 x56. \<lbrakk>sync (Trans s1 (COMact ca1) ou1 s1') (Trans s2 (COMact ca2) ou2 s2'); step s1 (COMact ca1) = (ou1, s1'); step s2 (COMact ca2) = (ou2, s2'); ca1 = comReceivePost x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> (\<exists>aid1. ca1 = comSendPost (admin s1) (pass s1 (admin s1)) aid1 PID \<and> ou1 = O_sendPost (aid1, clientPass s1 aid1, PID, post s1 PID, owner s1 PID, vis s1 PID)) = (\<exists>uid2 pst2 vs2. ca2 = comReceivePost AID1 (serverPass s2 AID1) PID pst2 uid2 vs2 \<and> ou2 = outOK)
 6. \<And>x61 x62 x63 x64. \<lbrakk>sync (Trans s1 (COMact ca1) ou1 s1') (Trans s2 (COMact ca2) ou2 s2'); step s1 (COMact ca1) = (ou1, s1'); step s2 (COMact ca2) = (ou2, s2'); ca1 = comSendPost x61 x62 x63 x64\<rbrakk> \<Longrightarrow> (\<exists>aid1. ca1 = comSendPost (admin s1) (pass s1 (admin s1)) aid1 PID \<and> ou1 = O_sendPost (aid1, clientPass s1 aid1, PID, post s1 PID, owner s1 PID, vis s1 PID)) = (\<exists>uid2 pst2 vs2. ca2 = comReceivePost AID1 (serverPass s2 AID1) PID pst2 uid2 vs2 \<and> ou2 = outOK)
 7. \<And>x71 x72 x73 x74. \<lbrakk>sync (Trans s1 (COMact ca1) ou1 s1') (Trans s2 (COMact ca2) ou2 s2'); step s1 (COMact ca1) = (ou1, s1'); step s2 (COMact ca2) = (ou2, s2'); ca1 = comReceiveCreateOFriend x71 x72 x73 x74\<rbrakk> \<Longrightarrow> (\<exists>aid1. ca1 = comSendPost (admin s1) (pass s1 (admin s1)) aid1 PID \<and> ou1 = O_sendPost (aid1, clientPass s1 aid1, PID, post s1 PID, owner s1 PID, vis s1 PID)) = (\<exists>uid2 pst2 vs2. ca2 = comReceivePost AID1 (serverPass s2 AID1) PID pst2 uid2 vs2 \<and> ou2 = outOK)
 8. \<And>x81 x82 x83 x84. \<lbrakk>sync (Trans s1 (COMact ca1) ou1 s1') (Trans s2 (COMact ca2) ou2 s2'); step s1 (COMact ca1) = (ou1, s1'); step s2 (COMact ca2) = (ou2, s2'); ca1 = comSendCreateOFriend x81 x82 x83 x84\<rbrakk> \<Longrightarrow> (\<exists>aid1. ca1 = comSendPost (admin s1) (pass s1 (admin s1)) aid1 PID \<and> ou1 = O_sendPost (aid1, clientPass s1 aid1, PID, post s1 PID, owner s1 PID, vis s1 PID)) = (\<exists>uid2 pst2 vs2. ca2 = comReceivePost AID1 (serverPass s2 AID1) PID pst2 uid2 vs2 \<and> ou2 = outOK)
 9. \<And>x91 x92 x93 x94. \<lbrakk>sync (Trans s1 (COMact ca1) ou1 s1') (Trans s2 (COMact ca2) ou2 s2'); step s1 (COMact ca1) = (ou1, s1'); step s2 (COMact ca2) = (ou2, s2'); ca1 = comReceiveDeleteOFriend x91 x92 x93 x94\<rbrakk> \<Longrightarrow> (\<exists>aid1. ca1 = comSendPost (admin s1) (pass s1 (admin s1)) aid1 PID \<and> ou1 = O_sendPost (aid1, clientPass s1 aid1, PID, post s1 PID, owner s1 PID, vis s1 PID)) = (\<exists>uid2 pst2 vs2. ca2 = comReceivePost AID1 (serverPass s2 AID1) PID pst2 uid2 vs2 \<and> ou2 = outOK)
 10. \<And>x101 x102 x103 x104. \<lbrakk>sync (Trans s1 (COMact ca1) ou1 s1') (Trans s2 (COMact ca2) ou2 s2'); step s1 (COMact ca1) = (ou1, s1'); step s2 (COMact ca2) = (ou2, s2'); ca1 = comSendDeleteOFriend x101 x102 x103 x104\<rbrakk> \<Longrightarrow> (\<exists>aid1. ca1 = comSendPost (admin s1) (pass s1 (admin s1)) aid1 PID \<and> ou1 = O_sendPost (aid1, clientPass s1 aid1, PID, post s1 PID, owner s1 PID, vis s1 PID)) = (\<exists>uid2 pst2 vs2. ca2 = comReceivePost AID1 (serverPass s2 AID1) PID pst2 uid2 vs2 \<and> ou2 = outOK)
[PROOF STEP]
by (cases ca2, auto simp: all_defs)+
[PROOF STATE]
proof (state)
this:
(\<exists>aid1. ca1 = comSendPost (admin s1) (pass s1 (admin s1)) aid1 PID \<and> ou1 = O_sendPost (aid1, clientPass s1 aid1, PID, post s1 PID, owner s1 PID, vis s1 PID)) = (\<exists>uid2 pst2 vs2. ca2 = comReceivePost AID1 (serverPass s2 AID1) PID pst2 uid2 vs2 \<and> ou2 = outOK)

goal (7 subgoals):
 1. \<And>x1. a2 = Sact x1 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 2. \<And>x2. a2 = Cact x2 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 3. \<And>x3. a2 = Dact x3 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 4. \<And>x4. a2 = Uact x4 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 5. \<And>x5. a2 = Ract x5 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 6. \<And>x6. a2 = Lact x6 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 7. \<And>x7. a2 = COMact x7 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<exists>aid1. ca1 = comSendPost (admin s1) (pass s1 (admin s1)) aid1 PID \<and> ou1 = O_sendPost (aid1, clientPass s1 aid1, PID, post s1 PID, owner s1 PID, vis s1 PID)) = (\<exists>uid2 pst2 vs2. ca2 = comReceivePost AID1 (serverPass s2 AID1) PID pst2 uid2 vs2 \<and> ou2 = outOK)

goal (7 subgoals):
 1. \<And>x1. a2 = Sact x1 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 2. \<And>x2. a2 = Cact x2 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 3. \<And>x3. a2 = Dact x3 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 4. \<And>x4. a2 = Uact x4 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 5. \<And>x5. a2 = Ract x5 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 6. \<And>x6. a2 = Lact x6 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 7. \<And>x7. a2 = COMact x7 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
[PROOF STEP]
have "\<dots> \<longleftrightarrow> ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>uid2 pst2 vs2. ca2 = comReceivePost AID1 (serverPass s2 AID1) PID pst2 uid2 vs2 \<and> ou2 = outOK) = \<phi>2 trn2
[PROOF STEP]
using c2
[PROOF STATE]
proof (prove)
using this:
isCom2 trn2

goal (1 subgoal):
 1. (\<exists>uid2 pst2 vs2. ca2 = comReceivePost AID1 (serverPass s2 AID1) PID pst2 uid2 vs2 \<and> ou2 = outOK) = \<phi>2 trn2
[PROOF STEP]
unfolding trn2 Rcv.\<phi>_def3[OF step2]
[PROOF STATE]
proof (prove)
using this:
isCom2 (Trans s2 a2 ou2 s2')

goal (1 subgoal):
 1. (\<exists>uid2 pst2 vs2. ca2 = comReceivePost AID1 (serverPass s2 AID1) PID pst2 uid2 vs2 \<and> ou2 = outOK) = (\<exists>uid pst vs. a2 = COMact (comReceivePost AID1 (serverPass s2 AID1) PID pst uid vs) \<and> ou2 = outOK)
[PROOF STEP]
unfolding a2
[PROOF STATE]
proof (prove)
using this:
isCom2 (Trans s2 (COMact ca2) ou2 s2')

goal (1 subgoal):
 1. (\<exists>uid2 pst2 vs2. ca2 = comReceivePost AID1 (serverPass s2 AID1) PID pst2 uid2 vs2 \<and> ou2 = outOK) = (\<exists>uid pst vs. COMact ca2 = COMact (comReceivePost AID1 (serverPass s2 AID1) PID pst uid vs) \<and> ou2 = outOK)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<exists>uid2 pst2 vs2. ca2 = comReceivePost AID1 (serverPass s2 AID1) PID pst2 uid2 vs2 \<and> ou2 = outOK) = \<phi>2 trn2

goal (7 subgoals):
 1. \<And>x1. a2 = Sact x1 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 2. \<And>x2. a2 = Cact x2 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 3. \<And>x3. a2 = Dact x3 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 4. \<And>x4. a2 = Uact x4 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 5. \<And>x5. a2 = Ract x5 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 6. \<And>x6. a2 = Lact x6 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 7. \<And>x7. a2 = COMact x7 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<phi>1 trn1 = \<phi>2 trn2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<phi>1 trn1 = \<phi>2 trn2

goal (1 subgoal):
 1. \<phi>1 trn1 = \<phi>2 trn2
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<phi>1 trn1 = \<phi>2 trn2

goal (6 subgoals):
 1. \<And>x1. a2 = Sact x1 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 2. \<And>x2. a2 = Cact x2 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 3. \<And>x3. a2 = Dact x3 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 4. \<And>x4. a2 = Uact x4 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 5. \<And>x5. a2 = Ract x5 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 6. \<And>x6. a2 = Lact x6 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
[PROOF STEP]
qed(insert assms, unfold trn1 trn2, auto)
[PROOF STATE]
proof (state)
this:
\<phi>1 trn1 = \<phi>2 trn2

goal (6 subgoals):
 1. \<And>x1. a1 = Sact x1 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 2. \<And>x2. a1 = Cact x2 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 3. \<And>x3. a1 = Dact x3 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 4. \<And>x4. a1 = Uact x4 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 5. \<And>x5. a1 = Ract x5 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
 6. \<And>x6. a1 = Lact x6 \<Longrightarrow> \<phi>1 trn1 = \<phi>2 trn2
[PROOF STEP]
qed(insert assms, unfold trn1 trn2, auto)
[PROOF STATE]
proof (state)
this:
\<phi>1 trn1 = \<phi>2 trn2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<phi>1 trn1 = \<phi>2 trn2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma textPost_textPost_cong[intro]:
assumes "textPost pst1 = textPost pst2"
and "setTextPost pst1 emptyText = setTextPost pst2 emptyText"
shows "pst1 = pst2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pst1 = pst2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
textPost pst1 = textPost pst2
setTextPost pst1 emptyText = setTextPost pst2 emptyText

goal (1 subgoal):
 1. pst1 = pst2
[PROOF STEP]
by (cases pst1, cases pst2) auto


[STATEMENT]
lemma sync_\<phi>_\<gamma>:
assumes "validTrans trn1" and "reach (srcOf trn1)"
and "validTrans trn2" and "reach (srcOf trn2)"
and "isCom1 trn1" and "isCom2 trn2"
and "\<gamma>1 trn1" and "\<gamma>2 trn2"
and so: "syncO (g1 trn1) (g2 trn2)"
and "\<phi>1 trn1 \<Longrightarrow> \<phi>2 trn2 \<Longrightarrow> syncV (f1 trn1) (f2 trn2)"
shows "sync trn1 trn2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sync trn1 trn2
[PROOF STEP]
proof(cases trn1, cases trn2)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x1a x2a x3a x4a. \<lbrakk>trn1 = Trans x1 x2 x3 x4; trn2 = Trans x1a x2a x3a x4a\<rbrakk> \<Longrightarrow> sync trn1 trn2
[PROOF STEP]
fix s1 a1 ou1 s1' s2 a2 ou2 s2'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x1a x2a x3a x4a. \<lbrakk>trn1 = Trans x1 x2 x3 x4; trn2 = Trans x1a x2a x3a x4a\<rbrakk> \<Longrightarrow> sync trn1 trn2
[PROOF STEP]
assume trn1: "trn1 = Trans s1 a1 ou1 s1'"
  and trn2: "trn2 = Trans s2 a2 ou2 s2'"
[PROOF STATE]
proof (state)
this:
trn1 = Trans s1 a1 ou1 s1'
trn2 = Trans s2 a2 ou2 s2'

goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x1a x2a x3a x4a. \<lbrakk>trn1 = Trans x1 x2 x3 x4; trn2 = Trans x1a x2a x3a x4a\<rbrakk> \<Longrightarrow> sync trn1 trn2
[PROOF STEP]
hence step1: "step s1 a1 = (ou1,s1')" and step2: "step s2 a2 = (ou2,s2')"
[PROOF STATE]
proof (prove)
using this:
trn1 = Trans s1 a1 ou1 s1'
trn2 = Trans s2 a2 ou2 s2'

goal (1 subgoal):
 1. step s1 a1 = (ou1, s1') &&& step s2 a2 = (ou2, s2')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
trn1 = Trans s1 a1 ou1 s1'
trn2 = Trans s2 a2 ou2 s2'
Iss.validTrans trn1
Iss.reach (srcOf trn1)
Iss.validTrans trn2
Iss.reach (srcOf trn2)
isCom1 trn1
isCom2 trn2
\<gamma>1 trn1
\<gamma>2 trn2
syncO (g1 trn1) (g2 trn2)
\<lbrakk>\<phi>1 trn1; \<phi>2 trn2\<rbrakk> \<Longrightarrow> syncV (f1 trn1) (f2 trn2)

goal (1 subgoal):
 1. step s1 a1 = (ou1, s1') &&& step s2 a2 = (ou2, s2')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
step s1 a1 = (ou1, s1')
step s2 a2 = (ou2, s2')

goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x1a x2a x3a x4a. \<lbrakk>trn1 = Trans x1 x2 x3 x4; trn2 = Trans x1a x2a x3a x4a\<rbrakk> \<Longrightarrow> sync trn1 trn2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sync trn1 trn2
[PROOF STEP]
proof(cases a1)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x1. a1 = Sact x1 \<Longrightarrow> sync trn1 trn2
 2. \<And>x2. a1 = Cact x2 \<Longrightarrow> sync trn1 trn2
 3. \<And>x3. a1 = Dact x3 \<Longrightarrow> sync trn1 trn2
 4. \<And>x4. a1 = Uact x4 \<Longrightarrow> sync trn1 trn2
 5. \<And>x5. a1 = Ract x5 \<Longrightarrow> sync trn1 trn2
 6. \<And>x6. a1 = Lact x6 \<Longrightarrow> sync trn1 trn2
 7. \<And>x7. a1 = COMact x7 \<Longrightarrow> sync trn1 trn2
[PROOF STEP]
case (COMact ca1)
[PROOF STATE]
proof (state)
this:
a1 = COMact ca1

goal (7 subgoals):
 1. \<And>x1. a1 = Sact x1 \<Longrightarrow> sync trn1 trn2
 2. \<And>x2. a1 = Cact x2 \<Longrightarrow> sync trn1 trn2
 3. \<And>x3. a1 = Dact x3 \<Longrightarrow> sync trn1 trn2
 4. \<And>x4. a1 = Uact x4 \<Longrightarrow> sync trn1 trn2
 5. \<And>x5. a1 = Ract x5 \<Longrightarrow> sync trn1 trn2
 6. \<And>x6. a1 = Lact x6 \<Longrightarrow> sync trn1 trn2
 7. \<And>x7. a1 = COMact x7 \<Longrightarrow> sync trn1 trn2
[PROOF STEP]
note a1 = COMact
[PROOF STATE]
proof (state)
this:
a1 = COMact ca1

goal (7 subgoals):
 1. \<And>x1. a1 = Sact x1 \<Longrightarrow> sync trn1 trn2
 2. \<And>x2. a1 = Cact x2 \<Longrightarrow> sync trn1 trn2
 3. \<And>x3. a1 = Dact x3 \<Longrightarrow> sync trn1 trn2
 4. \<And>x4. a1 = Uact x4 \<Longrightarrow> sync trn1 trn2
 5. \<And>x5. a1 = Ract x5 \<Longrightarrow> sync trn1 trn2
 6. \<And>x6. a1 = Lact x6 \<Longrightarrow> sync trn1 trn2
 7. \<And>x7. a1 = COMact x7 \<Longrightarrow> sync trn1 trn2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sync trn1 trn2
[PROOF STEP]
proof(cases a2)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x1. a2 = Sact x1 \<Longrightarrow> sync trn1 trn2
 2. \<And>x2. a2 = Cact x2 \<Longrightarrow> sync trn1 trn2
 3. \<And>x3. a2 = Dact x3 \<Longrightarrow> sync trn1 trn2
 4. \<And>x4. a2 = Uact x4 \<Longrightarrow> sync trn1 trn2
 5. \<And>x5. a2 = Ract x5 \<Longrightarrow> sync trn1 trn2
 6. \<And>x6. a2 = Lact x6 \<Longrightarrow> sync trn1 trn2
 7. \<And>x7. a2 = COMact x7 \<Longrightarrow> sync trn1 trn2
[PROOF STEP]
case (COMact ca2)
[PROOF STATE]
proof (state)
this:
a2 = COMact ca2

goal (7 subgoals):
 1. \<And>x1. a2 = Sact x1 \<Longrightarrow> sync trn1 trn2
 2. \<And>x2. a2 = Cact x2 \<Longrightarrow> sync trn1 trn2
 3. \<And>x3. a2 = Dact x3 \<Longrightarrow> sync trn1 trn2
 4. \<And>x4. a2 = Uact x4 \<Longrightarrow> sync trn1 trn2
 5. \<And>x5. a2 = Ract x5 \<Longrightarrow> sync trn1 trn2
 6. \<And>x6. a2 = Lact x6 \<Longrightarrow> sync trn1 trn2
 7. \<And>x7. a2 = COMact x7 \<Longrightarrow> sync trn1 trn2
[PROOF STEP]
note a2 = COMact
[PROOF STATE]
proof (state)
this:
a2 = COMact ca2

goal (7 subgoals):
 1. \<And>x1. a2 = Sact x1 \<Longrightarrow> sync trn1 trn2
 2. \<And>x2. a2 = Cact x2 \<Longrightarrow> sync trn1 trn2
 3. \<And>x3. a2 = Dact x3 \<Longrightarrow> sync trn1 trn2
 4. \<And>x4. a2 = Uact x4 \<Longrightarrow> sync trn1 trn2
 5. \<And>x5. a2 = Ract x5 \<Longrightarrow> sync trn1 trn2
 6. \<And>x6. a2 = Lact x6 \<Longrightarrow> sync trn1 trn2
 7. \<And>x7. a2 = COMact x7 \<Longrightarrow> sync trn1 trn2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sync trn1 trn2
[PROOF STEP]
proof(cases ca1)
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>x11 x12 x13 x14. ca1 = comSendServerReq x11 x12 x13 x14 \<Longrightarrow> sync trn1 trn2
 2. \<And>x21 x22. ca1 = comReceiveClientReq x21 x22 \<Longrightarrow> sync trn1 trn2
 3. \<And>x31 x32 x33 x34. ca1 = comConnectClient x31 x32 x33 x34 \<Longrightarrow> sync trn1 trn2
 4. \<And>x41 x42. ca1 = comConnectServer x41 x42 \<Longrightarrow> sync trn1 trn2
 5. \<And>x51 x52 x53 x54 x55 x56. ca1 = comReceivePost x51 x52 x53 x54 x55 x56 \<Longrightarrow> sync trn1 trn2
 6. \<And>x61 x62 x63 x64. ca1 = comSendPost x61 x62 x63 x64 \<Longrightarrow> sync trn1 trn2
 7. \<And>x71 x72 x73 x74. ca1 = comReceiveCreateOFriend x71 x72 x73 x74 \<Longrightarrow> sync trn1 trn2
 8. \<And>x81 x82 x83 x84. ca1 = comSendCreateOFriend x81 x82 x83 x84 \<Longrightarrow> sync trn1 trn2
 9. \<And>x91 x92 x93 x94. ca1 = comReceiveDeleteOFriend x91 x92 x93 x94 \<Longrightarrow> sync trn1 trn2
 10. \<And>x101 x102 x103 x104. ca1 = comSendDeleteOFriend x101 x102 x103 x104 \<Longrightarrow> sync trn1 trn2
[PROOF STEP]
term comReceivePost
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>x11 x12 x13 x14. ca1 = comSendServerReq x11 x12 x13 x14 \<Longrightarrow> sync trn1 trn2
 2. \<And>x21 x22. ca1 = comReceiveClientReq x21 x22 \<Longrightarrow> sync trn1 trn2
 3. \<And>x31 x32 x33 x34. ca1 = comConnectClient x31 x32 x33 x34 \<Longrightarrow> sync trn1 trn2
 4. \<And>x41 x42. ca1 = comConnectServer x41 x42 \<Longrightarrow> sync trn1 trn2
 5. \<And>x51 x52 x53 x54 x55 x56. ca1 = comReceivePost x51 x52 x53 x54 x55 x56 \<Longrightarrow> sync trn1 trn2
 6. \<And>x61 x62 x63 x64. ca1 = comSendPost x61 x62 x63 x64 \<Longrightarrow> sync trn1 trn2
 7. \<And>x71 x72 x73 x74. ca1 = comReceiveCreateOFriend x71 x72 x73 x74 \<Longrightarrow> sync trn1 trn2
 8. \<And>x81 x82 x83 x84. ca1 = comSendCreateOFriend x81 x82 x83 x84 \<Longrightarrow> sync trn1 trn2
 9. \<And>x91 x92 x93 x94. ca1 = comReceiveDeleteOFriend x91 x92 x93 x94 \<Longrightarrow> sync trn1 trn2
 10. \<And>x101 x102 x103 x104. ca1 = comSendDeleteOFriend x101 x102 x103 x104 \<Longrightarrow> sync trn1 trn2
[PROOF STEP]
case (comSendPost uid1 p1 aid1 pid)
[PROOF STATE]
proof (state)
this:
ca1 = comSendPost uid1 p1 aid1 pid

goal (10 subgoals):
 1. \<And>x11 x12 x13 x14. ca1 = comSendServerReq x11 x12 x13 x14 \<Longrightarrow> sync trn1 trn2
 2. \<And>x21 x22. ca1 = comReceiveClientReq x21 x22 \<Longrightarrow> sync trn1 trn2
 3. \<And>x31 x32 x33 x34. ca1 = comConnectClient x31 x32 x33 x34 \<Longrightarrow> sync trn1 trn2
 4. \<And>x41 x42. ca1 = comConnectServer x41 x42 \<Longrightarrow> sync trn1 trn2
 5. \<And>x51 x52 x53 x54 x55 x56. ca1 = comReceivePost x51 x52 x53 x54 x55 x56 \<Longrightarrow> sync trn1 trn2
 6. \<And>x61 x62 x63 x64. ca1 = comSendPost x61 x62 x63 x64 \<Longrightarrow> sync trn1 trn2
 7. \<And>x71 x72 x73 x74. ca1 = comReceiveCreateOFriend x71 x72 x73 x74 \<Longrightarrow> sync trn1 trn2
 8. \<And>x81 x82 x83 x84. ca1 = comSendCreateOFriend x81 x82 x83 x84 \<Longrightarrow> sync trn1 trn2
 9. \<And>x91 x92 x93 x94. ca1 = comReceiveDeleteOFriend x91 x92 x93 x94 \<Longrightarrow> sync trn1 trn2
 10. \<And>x101 x102 x103 x104. ca1 = comSendDeleteOFriend x101 x102 x103 x104 \<Longrightarrow> sync trn1 trn2
[PROOF STEP]
note ca1 = comSendPost
[PROOF STATE]
proof (state)
this:
ca1 = comSendPost uid1 p1 aid1 pid

goal (10 subgoals):
 1. \<And>x11 x12 x13 x14. ca1 = comSendServerReq x11 x12 x13 x14 \<Longrightarrow> sync trn1 trn2
 2. \<And>x21 x22. ca1 = comReceiveClientReq x21 x22 \<Longrightarrow> sync trn1 trn2
 3. \<And>x31 x32 x33 x34. ca1 = comConnectClient x31 x32 x33 x34 \<Longrightarrow> sync trn1 trn2
 4. \<And>x41 x42. ca1 = comConnectServer x41 x42 \<Longrightarrow> sync trn1 trn2
 5. \<And>x51 x52 x53 x54 x55 x56. ca1 = comReceivePost x51 x52 x53 x54 x55 x56 \<Longrightarrow> sync trn1 trn2
 6. \<And>x61 x62 x63 x64. ca1 = comSendPost x61 x62 x63 x64 \<Longrightarrow> sync trn1 trn2
 7. \<And>x71 x72 x73 x74. ca1 = comReceiveCreateOFriend x71 x72 x73 x74 \<Longrightarrow> sync trn1 trn2
 8. \<And>x81 x82 x83 x84. ca1 = comSendCreateOFriend x81 x82 x83 x84 \<Longrightarrow> sync trn1 trn2
 9. \<And>x91 x92 x93 x94. ca1 = comReceiveDeleteOFriend x91 x92 x93 x94 \<Longrightarrow> sync trn1 trn2
 10. \<And>x101 x102 x103 x104. ca1 = comSendDeleteOFriend x101 x102 x103 x104 \<Longrightarrow> sync trn1 trn2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ca1 = comSendPost uid1 p1 aid1 pid
[PROOF STEP]
obtain pst where p1: "p1 = pass s1 (admin s1)" and
        aid1: "aid1 = AID2" and ou2: "ou2 = outOK" and ou1: "ou1 \<noteq> outErr" and
        ca2: "ca2 = comReceivePost AID1 (serverPass s2 AID1) pid pst (owner s1 pid) (vis s1 pid)"
[PROOF STATE]
proof (prove)
using this:
ca1 = comSendPost uid1 p1 aid1 pid

goal (1 subgoal):
 1. (\<And>pst. \<lbrakk>p1 = pass s1 (admin s1); aid1 = AID2; ou2 = outOK; ou1 \<noteq> outErr; ca2 = comReceivePost AID1 (serverPass s2 AID1) pid pst (owner s1 pid) (vis s1 pid)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using so step1 step2
[PROOF STATE]
proof (prove)
using this:
ca1 = comSendPost uid1 p1 aid1 pid
syncO (g1 trn1) (g2 trn2)
step s1 a1 = (ou1, s1')
step s2 a2 = (ou2, s2')

goal (1 subgoal):
 1. (\<And>pst. \<lbrakk>p1 = pass s1 (admin s1); aid1 = AID2; ou2 = outOK; ou1 \<noteq> outErr; ca2 = comReceivePost AID1 (serverPass s2 AID1) pid pst (owner s1 pid) (vis s1 pid)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding trn1 trn2 a1 a2 ca1
[PROOF STATE]
proof (prove)
using this:
comSendPost uid1 p1 aid1 pid = comSendPost uid1 p1 aid1 pid
syncO (g1 (Trans s1 (COMact (comSendPost uid1 p1 aid1 pid)) ou1 s1')) (g2 (Trans s2 (COMact ca2) ou2 s2'))
step s1 (COMact (comSendPost uid1 p1 aid1 pid)) = (ou1, s1')
step s2 (COMact ca2) = (ou2, s2')

goal (1 subgoal):
 1. (\<And>pst. \<lbrakk>p1 = pass s1 (admin s1); aid1 = AID2; ou2 = outOK; ou1 \<noteq> outErr; ca2 = comReceivePost AID1 (serverPass s2 AID1) pid pst (owner s1 pid) (vis s1 pid)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases ca2, auto simp: all_defs)
[PROOF STATE]
proof (state)
this:
p1 = pass s1 (admin s1)
aid1 = AID2
ou2 = outOK
ou1 \<noteq> outErr
ca2 = comReceivePost AID1 (serverPass s2 AID1) pid pst (owner s1 pid) (vis s1 pid)

goal (10 subgoals):
 1. \<And>x11 x12 x13 x14. ca1 = comSendServerReq x11 x12 x13 x14 \<Longrightarrow> sync trn1 trn2
 2. \<And>x21 x22. ca1 = comReceiveClientReq x21 x22 \<Longrightarrow> sync trn1 trn2
 3. \<And>x31 x32 x33 x34. ca1 = comConnectClient x31 x32 x33 x34 \<Longrightarrow> sync trn1 trn2
 4. \<And>x41 x42. ca1 = comConnectServer x41 x42 \<Longrightarrow> sync trn1 trn2
 5. \<And>x51 x52 x53 x54 x55 x56. ca1 = comReceivePost x51 x52 x53 x54 x55 x56 \<Longrightarrow> sync trn1 trn2
 6. \<And>x61 x62 x63 x64. ca1 = comSendPost x61 x62 x63 x64 \<Longrightarrow> sync trn1 trn2
 7. \<And>x71 x72 x73 x74. ca1 = comReceiveCreateOFriend x71 x72 x73 x74 \<Longrightarrow> sync trn1 trn2
 8. \<And>x81 x82 x83 x84. ca1 = comSendCreateOFriend x81 x82 x83 x84 \<Longrightarrow> sync trn1 trn2
 9. \<And>x91 x92 x93 x94. ca1 = comReceiveDeleteOFriend x91 x92 x93 x94 \<Longrightarrow> sync trn1 trn2
 10. \<And>x101 x102 x103 x104. ca1 = comSendDeleteOFriend x101 x102 x103 x104 \<Longrightarrow> sync trn1 trn2
[PROOF STEP]
have ou1: "ou1 = O_sendPost (AID2,clientPass s1 AID2,pid, post s1 pid, owner s1 pid, vis s1 pid)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ou1 = O_sendPost (AID2, clientPass s1 AID2, pid, post s1 pid, owner s1 pid, vis s1 pid)
[PROOF STEP]
using step1 ou1
[PROOF STATE]
proof (prove)
using this:
step s1 a1 = (ou1, s1')
ou1 \<noteq> outErr

goal (1 subgoal):
 1. ou1 = O_sendPost (AID2, clientPass s1 AID2, pid, post s1 pid, owner s1 pid, vis s1 pid)
[PROOF STEP]
unfolding a1 ca1 aid1
[PROOF STATE]
proof (prove)
using this:
step s1 (COMact (comSendPost uid1 p1 AID2 pid)) = (ou1, s1')
ou1 \<noteq> outErr

goal (1 subgoal):
 1. ou1 = O_sendPost (AID2, clientPass s1 AID2, pid, post s1 pid, owner s1 pid, vis s1 pid)
[PROOF STEP]
by (auto simp: all_defs)
[PROOF STATE]
proof (state)
this:
ou1 = O_sendPost (AID2, clientPass s1 AID2, pid, post s1 pid, owner s1 pid, vis s1 pid)

goal (10 subgoals):
 1. \<And>x11 x12 x13 x14. ca1 = comSendServerReq x11 x12 x13 x14 \<Longrightarrow> sync trn1 trn2
 2. \<And>x21 x22. ca1 = comReceiveClientReq x21 x22 \<Longrightarrow> sync trn1 trn2
 3. \<And>x31 x32 x33 x34. ca1 = comConnectClient x31 x32 x33 x34 \<Longrightarrow> sync trn1 trn2
 4. \<And>x41 x42. ca1 = comConnectServer x41 x42 \<Longrightarrow> sync trn1 trn2
 5. \<And>x51 x52 x53 x54 x55 x56. ca1 = comReceivePost x51 x52 x53 x54 x55 x56 \<Longrightarrow> sync trn1 trn2
 6. \<And>x61 x62 x63 x64. ca1 = comSendPost x61 x62 x63 x64 \<Longrightarrow> sync trn1 trn2
 7. \<And>x71 x72 x73 x74. ca1 = comReceiveCreateOFriend x71 x72 x73 x74 \<Longrightarrow> sync trn1 trn2
 8. \<And>x81 x82 x83 x84. ca1 = comSendCreateOFriend x81 x82 x83 x84 \<Longrightarrow> sync trn1 trn2
 9. \<And>x91 x92 x93 x94. ca1 = comReceiveDeleteOFriend x91 x92 x93 x94 \<Longrightarrow> sync trn1 trn2
 10. \<And>x101 x102 x103 x104. ca1 = comSendDeleteOFriend x101 x102 x103 x104 \<Longrightarrow> sync trn1 trn2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sync trn1 trn2
[PROOF STEP]
proof(cases "pid = PID")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pid = PID \<Longrightarrow> sync trn1 trn2
 2. pid \<noteq> PID \<Longrightarrow> sync trn1 trn2
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
pid \<noteq> PID

goal (2 subgoals):
 1. pid = PID \<Longrightarrow> sync trn1 trn2
 2. pid \<noteq> PID \<Longrightarrow> sync trn1 trn2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
pid \<noteq> PID

goal (1 subgoal):
 1. sync trn1 trn2
[PROOF STEP]
using so step1 step2
[PROOF STATE]
proof (prove)
using this:
pid \<noteq> PID
syncO (g1 trn1) (g2 trn2)
step s1 a1 = (ou1, s1')
step s2 a2 = (ou2, s2')

goal (1 subgoal):
 1. sync trn1 trn2
[PROOF STEP]
unfolding trn1 trn2 a1 a2 ca1 ca2
[PROOF STATE]
proof (prove)
using this:
pid \<noteq> PID
syncO (g1 (Trans s1 (COMact (comSendPost uid1 p1 aid1 pid)) ou1 s1')) (g2 (Trans s2 (COMact (comReceivePost AID1 (serverPass s2 AID1) pid pst (owner s1 pid) (vis s1 pid))) ou2 s2'))
step s1 (COMact (comSendPost uid1 p1 aid1 pid)) = (ou1, s1')
step s2 (COMact (comReceivePost AID1 (serverPass s2 AID1) pid pst (owner s1 pid) (vis s1 pid))) = (ou2, s2')

goal (1 subgoal):
 1. sync (Trans s1 (COMact (comSendPost uid1 p1 aid1 pid)) ou1 s1') (Trans s2 (COMact (comReceivePost AID1 (serverPass s2 AID1) pid pst (owner s1 pid) (vis s1 pid))) ou2 s2')
[PROOF STEP]
by (auto simp: all_defs)
[PROOF STATE]
proof (state)
this:
sync trn1 trn2

goal (1 subgoal):
 1. pid = PID \<Longrightarrow> sync trn1 trn2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pid = PID \<Longrightarrow> sync trn1 trn2
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
pid = PID

goal (1 subgoal):
 1. pid = PID \<Longrightarrow> sync trn1 trn2
[PROOF STEP]
note pid = True
[PROOF STATE]
proof (state)
this:
pid = PID

goal (1 subgoal):
 1. pid = PID \<Longrightarrow> sync trn1 trn2
[PROOF STEP]
hence "\<phi>1 trn1 \<and> \<phi>2 trn2"
[PROOF STATE]
proof (prove)
using this:
pid = PID

goal (1 subgoal):
 1. \<phi>1 trn1 \<and> \<phi>2 trn2
[PROOF STEP]
using ou1 ou2
[PROOF STATE]
proof (prove)
using this:
pid = PID
ou1 = O_sendPost (AID2, clientPass s1 AID2, pid, post s1 pid, owner s1 pid, vis s1 pid)
ou2 = outOK

goal (1 subgoal):
 1. \<phi>1 trn1 \<and> \<phi>2 trn2
[PROOF STEP]
unfolding trn1 trn2 a1 a2 ca1 ca2
[PROOF STATE]
proof (prove)
using this:
pid = PID
ou1 = O_sendPost (AID2, clientPass s1 AID2, pid, post s1 pid, owner s1 pid, vis s1 pid)
ou2 = outOK

goal (1 subgoal):
 1. \<phi>1 (Trans s1 (COMact (comSendPost uid1 p1 aid1 pid)) ou1 s1') \<and> \<phi>2 (Trans s2 (COMact (comReceivePost AID1 (serverPass s2 AID1) pid pst (owner s1 pid) (vis s1 pid))) ou2 s2')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<phi>1 trn1 \<and> \<phi>2 trn2

goal (1 subgoal):
 1. pid = PID \<Longrightarrow> sync trn1 trn2
[PROOF STEP]
hence "syncV (f1 trn1) (f2 trn2)"
[PROOF STATE]
proof (prove)
using this:
\<phi>1 trn1 \<and> \<phi>2 trn2

goal (1 subgoal):
 1. syncV (f1 trn1) (f2 trn2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<phi>1 trn1 \<and> \<phi>2 trn2
Iss.validTrans trn1
Iss.reach (srcOf trn1)
Iss.validTrans trn2
Iss.reach (srcOf trn2)
isCom1 trn1
isCom2 trn2
\<gamma>1 trn1
\<gamma>2 trn2
syncO (g1 trn1) (g2 trn2)
\<lbrakk>\<phi>1 trn1; \<phi>2 trn2\<rbrakk> \<Longrightarrow> syncV (f1 trn1) (f2 trn2)

goal (1 subgoal):
 1. syncV (f1 trn1) (f2 trn2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
syncV (f1 trn1) (f2 trn2)

goal (1 subgoal):
 1. pid = PID \<Longrightarrow> sync trn1 trn2
[PROOF STEP]
hence pst: "pst = post s1 PID"
[PROOF STATE]
proof (prove)
using this:
syncV (f1 trn1) (f2 trn2)

goal (1 subgoal):
 1. pst = post s1 PID
[PROOF STEP]
using pid
[PROOF STATE]
proof (prove)
using this:
syncV (f1 trn1) (f2 trn2)
pid = PID

goal (1 subgoal):
 1. pst = post s1 PID
[PROOF STEP]
unfolding trn1 trn2 a1 a2 ca1 ca2 aid1 ou1
[PROOF STATE]
proof (prove)
using this:
syncV (f1 (Trans s1 (COMact (comSendPost uid1 p1 AID2 pid)) (O_sendPost (AID2, clientPass s1 AID2, pid, post s1 pid, owner s1 pid, vis s1 pid)) s1')) (f2 (Trans s2 (COMact (comReceivePost AID1 (serverPass s2 AID1) pid pst (owner s1 pid) (vis s1 pid))) ou2 s2'))
pid = PID

goal (1 subgoal):
 1. pst = post s1 PID
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pst = post s1 PID

goal (1 subgoal):
 1. pid = PID \<Longrightarrow> sync trn1 trn2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sync trn1 trn2
[PROOF STEP]
unfolding trn1 trn2 a1 a2 ca1 ca2 ou1 ou2 pst pid
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sync (Trans s1 (COMact (comSendPost uid1 p1 aid1 PID)) (O_sendPost (AID2, clientPass s1 AID2, PID, post s1 PID, owner s1 PID, vis s1 PID)) s1') (Trans s2 (COMact (comReceivePost AID1 (serverPass s2 AID1) PID (post s1 PID) (owner s1 PID) (vis s1 PID))) outOK s2')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sync trn1 trn2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sync trn1 trn2

goal (9 subgoals):
 1. \<And>x11 x12 x13 x14. ca1 = comSendServerReq x11 x12 x13 x14 \<Longrightarrow> sync trn1 trn2
 2. \<And>x21 x22. ca1 = comReceiveClientReq x21 x22 \<Longrightarrow> sync trn1 trn2
 3. \<And>x31 x32 x33 x34. ca1 = comConnectClient x31 x32 x33 x34 \<Longrightarrow> sync trn1 trn2
 4. \<And>x41 x42. ca1 = comConnectServer x41 x42 \<Longrightarrow> sync trn1 trn2
 5. \<And>x51 x52 x53 x54 x55 x56. ca1 = comReceivePost x51 x52 x53 x54 x55 x56 \<Longrightarrow> sync trn1 trn2
 6. \<And>x71 x72 x73 x74. ca1 = comReceiveCreateOFriend x71 x72 x73 x74 \<Longrightarrow> sync trn1 trn2
 7. \<And>x81 x82 x83 x84. ca1 = comSendCreateOFriend x81 x82 x83 x84 \<Longrightarrow> sync trn1 trn2
 8. \<And>x91 x92 x93 x94. ca1 = comReceiveDeleteOFriend x91 x92 x93 x94 \<Longrightarrow> sync trn1 trn2
 9. \<And>x101 x102 x103 x104. ca1 = comSendDeleteOFriend x101 x102 x103 x104 \<Longrightarrow> sync trn1 trn2
[PROOF STEP]
qed(insert so step1 step2, unfold trn1 trn2 a1 a2, (cases ca2, auto simp: all_defs)+)
[PROOF STATE]
proof (state)
this:
sync trn1 trn2

goal (6 subgoals):
 1. \<And>x1. a2 = Sact x1 \<Longrightarrow> sync trn1 trn2
 2. \<And>x2. a2 = Cact x2 \<Longrightarrow> sync trn1 trn2
 3. \<And>x3. a2 = Dact x3 \<Longrightarrow> sync trn1 trn2
 4. \<And>x4. a2 = Uact x4 \<Longrightarrow> sync trn1 trn2
 5. \<And>x5. a2 = Ract x5 \<Longrightarrow> sync trn1 trn2
 6. \<And>x6. a2 = Lact x6 \<Longrightarrow> sync trn1 trn2
[PROOF STEP]
qed(insert assms, unfold trn1 trn2, auto)
[PROOF STATE]
proof (state)
this:
sync trn1 trn2

goal (6 subgoals):
 1. \<And>x1. a1 = Sact x1 \<Longrightarrow> sync trn1 trn2
 2. \<And>x2. a1 = Cact x2 \<Longrightarrow> sync trn1 trn2
 3. \<And>x3. a1 = Dact x3 \<Longrightarrow> sync trn1 trn2
 4. \<And>x4. a1 = Uact x4 \<Longrightarrow> sync trn1 trn2
 5. \<And>x5. a1 = Ract x5 \<Longrightarrow> sync trn1 trn2
 6. \<And>x6. a1 = Lact x6 \<Longrightarrow> sync trn1 trn2
[PROOF STEP]
qed(insert assms, unfold trn1 trn2, auto)
[PROOF STATE]
proof (state)
this:
sync trn1 trn2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma isCom1_\<gamma>1:
assumes "validTrans trn1" and "reach (srcOf trn1)" and "isCom1 trn1"
shows "\<gamma>1 trn1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma>1 trn1
[PROOF STEP]
proof(cases trn1)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. trn1 = Trans x1 x2 x3 x4 \<Longrightarrow> \<gamma>1 trn1
[PROOF STEP]
case (Trans s1 a1 ou1 s1')
[PROOF STATE]
proof (state)
this:
trn1 = Trans s1 a1 ou1 s1'

goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. trn1 = Trans x1 x2 x3 x4 \<Longrightarrow> \<gamma>1 trn1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
trn1 = Trans s1 a1 ou1 s1'

goal (1 subgoal):
 1. \<gamma>1 trn1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
trn1 = Trans s1 a1 ou1 s1'
Iss.validTrans trn1
Iss.reach (srcOf trn1)
isCom1 trn1

goal (1 subgoal):
 1. \<gamma>1 trn1
[PROOF STEP]
by (cases a1) auto
[PROOF STATE]
proof (state)
this:
\<gamma>1 trn1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma isCom2_\<gamma>2:
assumes "validTrans trn2" and "reach (srcOf trn2)" and "isCom2 trn2"
shows "\<gamma>2 trn2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma>2 trn2
[PROOF STEP]
proof(cases trn2)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. trn2 = Trans x1 x2 x3 x4 \<Longrightarrow> \<gamma>2 trn2
[PROOF STEP]
case (Trans s2 a2 ou2 s2')
[PROOF STATE]
proof (state)
this:
trn2 = Trans s2 a2 ou2 s2'

goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. trn2 = Trans x1 x2 x3 x4 \<Longrightarrow> \<gamma>2 trn2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
trn2 = Trans s2 a2 ou2 s2'

goal (1 subgoal):
 1. \<gamma>2 trn2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
trn2 = Trans s2 a2 ou2 s2'
Iss.validTrans trn2
Iss.reach (srcOf trn2)
isCom2 trn2

goal (1 subgoal):
 1. \<gamma>2 trn2
[PROOF STEP]
by (cases a2) auto
[PROOF STATE]
proof (state)
this:
\<gamma>2 trn2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma isCom2_V2:
assumes "validTrans trn2" and "reach (srcOf trn2)" and "\<phi>2 trn2"
shows "isCom2 trn2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isCom2 trn2
[PROOF STEP]
proof(cases trn2)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. trn2 = Trans x1 x2 x3 x4 \<Longrightarrow> isCom2 trn2
[PROOF STEP]
case (Trans s2 a2 ou2 s2')
[PROOF STATE]
proof (state)
this:
trn2 = Trans s2 a2 ou2 s2'

goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. trn2 = Trans x1 x2 x3 x4 \<Longrightarrow> isCom2 trn2
[PROOF STEP]
note trn2 = Trans
[PROOF STATE]
proof (state)
this:
trn2 = Trans s2 a2 ou2 s2'

goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. trn2 = Trans x1 x2 x3 x4 \<Longrightarrow> isCom2 trn2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isCom2 trn2
[PROOF STEP]
proof(cases a2)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x1. a2 = Sact x1 \<Longrightarrow> isCom2 trn2
 2. \<And>x2. a2 = Cact x2 \<Longrightarrow> isCom2 trn2
 3. \<And>x3. a2 = Dact x3 \<Longrightarrow> isCom2 trn2
 4. \<And>x4. a2 = Uact x4 \<Longrightarrow> isCom2 trn2
 5. \<And>x5. a2 = Ract x5 \<Longrightarrow> isCom2 trn2
 6. \<And>x6. a2 = Lact x6 \<Longrightarrow> isCom2 trn2
 7. \<And>x7. a2 = COMact x7 \<Longrightarrow> isCom2 trn2
[PROOF STEP]
case (COMact ca2)
[PROOF STATE]
proof (state)
this:
a2 = COMact ca2

goal (7 subgoals):
 1. \<And>x1. a2 = Sact x1 \<Longrightarrow> isCom2 trn2
 2. \<And>x2. a2 = Cact x2 \<Longrightarrow> isCom2 trn2
 3. \<And>x3. a2 = Dact x3 \<Longrightarrow> isCom2 trn2
 4. \<And>x4. a2 = Uact x4 \<Longrightarrow> isCom2 trn2
 5. \<And>x5. a2 = Ract x5 \<Longrightarrow> isCom2 trn2
 6. \<And>x6. a2 = Lact x6 \<Longrightarrow> isCom2 trn2
 7. \<And>x7. a2 = COMact x7 \<Longrightarrow> isCom2 trn2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a2 = COMact ca2

goal (1 subgoal):
 1. isCom2 trn2
[PROOF STEP]
using assms trn2
[PROOF STATE]
proof (prove)
using this:
a2 = COMact ca2
Iss.validTrans trn2
Iss.reach (srcOf trn2)
\<phi>2 trn2
trn2 = Trans s2 a2 ou2 s2'

goal (1 subgoal):
 1. isCom2 trn2
[PROOF STEP]
by (cases ca2) auto
[PROOF STATE]
proof (state)
this:
isCom2 trn2

goal (6 subgoals):
 1. \<And>x1. a2 = Sact x1 \<Longrightarrow> isCom2 trn2
 2. \<And>x2. a2 = Cact x2 \<Longrightarrow> isCom2 trn2
 3. \<And>x3. a2 = Dact x3 \<Longrightarrow> isCom2 trn2
 4. \<And>x4. a2 = Uact x4 \<Longrightarrow> isCom2 trn2
 5. \<And>x5. a2 = Ract x5 \<Longrightarrow> isCom2 trn2
 6. \<And>x6. a2 = Lact x6 \<Longrightarrow> isCom2 trn2
[PROOF STEP]
qed(insert assms trn2, auto)
[PROOF STATE]
proof (state)
this:
isCom2 trn2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem secure: "secure"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. K.secure
[PROOF STEP]
using secure1_secure2_secure[OF Iss.Post_secure Rcv.Post_secure]
[PROOF STATE]
proof (prove)
using this:
K.secure

goal (1 subgoal):
 1. K.secure
[PROOF STEP]
.


[STATEMENT]
theorem C1:  "\<lfloor>\<^bold>\<forall>\<^sup>Ax. Abstract x \<^bold>\<rightarrow> (\<^bold>\<exists>y. Concrete y \<^bold>\<and> x dependsOn y)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lambda>w. \<forall>x. x actualizedAt w \<longrightarrow> Abstract x w \<longrightarrow> (\<exists>xa. (Concrete xa \<^bold>\<and> x dependsOn xa) w)\<rfloor>
[PROOF STEP]
using P3 P4
[PROOF STATE]
proof (prove)
using this:
\<lfloor>\<lambda>w. \<forall>x. ((actualizedAt) x \<^bold>\<rightarrow> Abstract x \<^bold>\<rightarrow> Dependent x) w\<rfloor>
\<lfloor>\<lambda>w. \<forall>x. x actualizedAt w \<longrightarrow> Dependent x w \<longrightarrow> (\<exists>xa. ((actualizedAt) xa \<^bold>\<and> Independent xa \<^bold>\<and> x dependsOn xa) w)\<rfloor>

goal (1 subgoal):
 1. \<lfloor>\<lambda>w. \<forall>x. x actualizedAt w \<longrightarrow> Abstract x w \<longrightarrow> (\<exists>xa. (Concrete xa \<^bold>\<and> x dependsOn xa) w)\<rfloor>
[PROOF STEP]
by blast


[STATEMENT]
theorem C5: "\<lfloor>\<^bold>\<exists>\<^sup>Ax. Concrete x\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>mexistsActB Concrete\<rfloor>
[PROOF STEP]
using P2 P3 P4
[PROOF STATE]
proof (prove)
using this:
\<lfloor>\<lambda>w. \<exists>x. ((actualizedAt) x \<^bold>\<and> Necessary x \<^bold>\<and> Abstract x) w\<rfloor>
\<lfloor>\<lambda>w. \<forall>x. ((actualizedAt) x \<^bold>\<rightarrow> Abstract x \<^bold>\<rightarrow> Dependent x) w\<rfloor>
\<lfloor>\<lambda>w. \<forall>x. x actualizedAt w \<longrightarrow> Dependent x w \<longrightarrow> (\<exists>xa. ((actualizedAt) xa \<^bold>\<and> Independent xa \<^bold>\<and> x dependsOn xa) w)\<rfloor>

goal (1 subgoal):
 1. \<lfloor>mexistsActB Concrete\<rfloor>
[PROOF STEP]
by blast


[STATEMENT]
theorem C7: "\<lfloor>\<^bold>\<forall>\<^sup>Ax. (Necessary x \<^bold>\<and> Abstract x) \<^bold>\<rightarrow> Explained x\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lambda>w. \<forall>x. ((actualizedAt) x \<^bold>\<rightarrow> Necessary x \<^bold>\<and> Abstract x \<^bold>\<rightarrow> Explained x) w\<rfloor>
[PROOF STEP]
using P3 P6
[PROOF STATE]
proof (prove)
using this:
\<lfloor>\<lambda>w. \<forall>x. ((actualizedAt) x \<^bold>\<rightarrow> Abstract x \<^bold>\<rightarrow> Dependent x) w\<rfloor>
\<lfloor>\<lambda>w. \<forall>x. (Dependent x \<^bold>\<rightarrow> Explained x) w\<rfloor>

goal (1 subgoal):
 1. \<lfloor>\<lambda>w. \<forall>x. ((actualizedAt) x \<^bold>\<rightarrow> Necessary x \<^bold>\<and> Abstract x \<^bold>\<rightarrow> Explained x) w\<rfloor>
[PROOF STEP]
by blast


[STATEMENT]
theorem C10:  "\<lfloor>\<^bold>\<exists>\<^sup>Ax. Godlike x\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lambda>w. \<exists>x. ((actualizedAt) x \<^bold>\<and> Godlike x) w\<rfloor>
[PROOF STEP]
nitpick[user_axioms]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lambda>w. \<exists>x. ((actualizedAt) x \<^bold>\<and> Godlike x) w\<rfloor>
[PROOF STEP]
oops


[STATEMENT]
theorem C10:  "\<lfloor>\<^bold>\<exists>\<^sup>Ax. Godlike x\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lambda>w. \<exists>x. ((actualizedAt) x \<^bold>\<and> Godlike x) w\<rfloor>
[PROOF STEP]
nitpick[user_axioms]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lambda>w. \<exists>x. ((actualizedAt) x \<^bold>\<and> Godlike x) w\<rfloor>
[PROOF STEP]
oops \<comment> \<open>Countermodel found\<close>


[STATEMENT]
lemma True
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True
[PROOF STEP]
nitpick[satisfy, user_axioms]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True
[PROOF STEP]
oops \<comment> \<open>Model found: axioms are consistent\<close>


[STATEMENT]
lemma "\<lfloor>\<^bold>\<forall>x. E! x\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>mforallB E!\<rfloor>
[PROOF STEP]
nitpick[user_axioms]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>mforallB E!\<rfloor>
[PROOF STEP]
oops \<comment> \<open>Countermodel found: necessitism is not valid\<close>


[STATEMENT]
lemma "\<lfloor>\<phi> \<^bold>\<rightarrow> \<^bold>\<box>\<phi>\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<phi> \<^bold>\<rightarrow> \<^bold>\<box>\<phi>\<rfloor>
[PROOF STEP]
nitpick[user_axioms]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<phi> \<^bold>\<rightarrow> \<^bold>\<box>\<phi>\<rfloor>
[PROOF STEP]
oops \<comment> \<open>Countermodel found: modal collapse is not valid\<close>


[STATEMENT]
theorem C10:  "\<lfloor>\<^bold>\<exists>\<^sup>Ax. Godlike x\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lambda>w. \<exists>x. ((actualizedAt) x \<^bold>\<and> Godlike x) w\<rfloor>
[PROOF STEP]
using Existence_def Necessary_def
    abstractness_essential concrete_exist P2 C1 B_axiom
[PROOF STATE]
proof (prove)
using this:
E! ?x \<equiv> \<lambda>w. \<exists>x. x actualizedAt w \<and> x = ?x
Necessary ?x \<equiv> \<^bold>\<box>E! ?x
\<lfloor>\<lambda>w. \<forall>x. (Abstract x \<^bold>\<rightarrow> \<^bold>\<box>Abstract x) w\<rfloor>
\<lfloor>\<lambda>w. \<forall>x. (Concrete x \<^bold>\<rightarrow> E! x) w\<rfloor>
\<lfloor>\<lambda>w. \<exists>x. ((actualizedAt) x \<^bold>\<and> Necessary x \<^bold>\<and> Abstract x) w\<rfloor>
\<lfloor>\<lambda>w. \<forall>x. x actualizedAt w \<longrightarrow> Abstract x w \<longrightarrow> (\<exists>xa. (Concrete xa \<^bold>\<and> x dependsOn xa) w)\<rfloor>
universal (\<lambda>x y. x r y \<longrightarrow> y r x)

goal (1 subgoal):
 1. \<lfloor>\<lambda>w. \<exists>x. ((actualizedAt) x \<^bold>\<and> Godlike x) w\<rfloor>
[PROOF STEP]
by meson


[STATEMENT]
lemma gen_lower_bound_increasing:
  fixes a :: real
  assumes "a \<le> x"
      and "\<And>y. a \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> ((\<lambda>x. fl x - f x) has_real_derivative g y) (at y)"
      and "\<And>y. a \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> g y \<le> 0"
      and "fl a = f a"
    shows "fl x \<le> f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fl x \<le> f x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fl x \<le> f x
[PROOF STEP]
have "fl x - f x \<le> fl a - f a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fl x - f x \<le> fl a - f a
[PROOF STEP]
apply (rule DERIV_nonpos_imp_nonincreasing [where f = "\<lambda>x. fl x - f x"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<le> x
 2. \<And>xa. \<lbrakk>a \<le> xa; xa \<le> x\<rbrakk> \<Longrightarrow> \<exists>y. ((\<lambda>x. fl x - f x) has_real_derivative y) (at xa) \<and> y \<le> 0
[PROOF STEP]
apply (rule assms)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>a \<le> xa; xa \<le> x\<rbrakk> \<Longrightarrow> \<exists>y. ((\<lambda>x. fl x - f x) has_real_derivative y) (at xa) \<and> y \<le> 0
[PROOF STEP]
apply (intro allI impI exI conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>a \<le> xa; xa \<le> x\<rbrakk> \<Longrightarrow> ((\<lambda>x. fl x - f x) has_real_derivative ?y3 xa) (at xa)
 2. \<And>xa. \<lbrakk>a \<le> xa; xa \<le> x\<rbrakk> \<Longrightarrow> ?y3 xa \<le> 0
[PROOF STEP]
apply (rule assms | simp)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
fl x - f x \<le> fl a - f a

goal (1 subgoal):
 1. fl x \<le> f x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fl x - f x \<le> fl a - f a

goal (1 subgoal):
 1. fl x \<le> f x
[PROOF STEP]
have "... = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fl a - f a = 0
[PROOF STEP]
by (simp add: assms)
[PROOF STATE]
proof (state)
this:
fl a - f a = 0

goal (1 subgoal):
 1. fl x \<le> f x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
fl x - f x \<le> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fl x - f x \<le> 0

goal (1 subgoal):
 1. fl x \<le> f x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fl x \<le> f x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gen_lower_bound_decreasing:
  fixes a :: real
  assumes "x \<le> a"
      and "\<And>y. x \<le> y \<Longrightarrow> y \<le> a \<Longrightarrow> ((\<lambda>x. fl x - f x) has_real_derivative g y) (at y)"
      and "\<And>y. x \<le> y \<Longrightarrow> y \<le> a \<Longrightarrow> g y \<ge> 0"
      and "fl a = f a"
    shows "fl x \<le> f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fl x \<le> f x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fl x \<le> f x
[PROOF STEP]
have "fl (- (-x)) \<le> f (- (-x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fl (- (- x)) \<le> f (- (- x))
[PROOF STEP]
apply (rule gen_lower_bound_increasing [of "-a" "-x" _ _ "\<lambda>u. - g (-u)"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. - a \<le> - x
 2. \<And>y. \<lbrakk>- a \<le> y; y \<le> - x\<rbrakk> \<Longrightarrow> ((\<lambda>x. fl (- x) - f (- x)) has_real_derivative - g (- y)) (at y)
 3. \<And>y. \<lbrakk>- a \<le> y; y \<le> - x\<rbrakk> \<Longrightarrow> - g (- y) \<le> 0
 4. fl (- (- a)) = f (- (- a))
[PROOF STEP]
apply (auto simp: assms)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>- a \<le> y; y \<le> - x\<rbrakk> \<Longrightarrow> ((\<lambda>x. fl (- x) - f (- x)) has_real_derivative - g (- y)) (at y)
[PROOF STEP]
apply (subst DERIV_mirror [symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>- a \<le> y; y \<le> - x\<rbrakk> \<Longrightarrow> ((\<lambda>a. fl a - f a) has_real_derivative g (- y)) (at (- y))
[PROOF STEP]
apply (simp add: assms)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
fl (- (- x)) \<le> f (- (- x))

goal (1 subgoal):
 1. fl x \<le> f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fl (- (- x)) \<le> f (- (- x))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fl (- (- x)) \<le> f (- (- x))

goal (1 subgoal):
 1. fl x \<le> f x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fl x \<le> f x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gen_upper_bound_increasing:
  fixes a :: real
  assumes "a \<le> x"
      and "\<And>y. a \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> ((\<lambda>x. fu x - f x) has_real_derivative g y) (at y)"
      and "\<And>y. a \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> g y \<ge> 0"
      and "fu a = f a"
    shows "f x \<le> fu x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x \<le> fu x
[PROOF STEP]
apply (rule gen_lower_bound_increasing [of a x f fu  "\<lambda>u. - g u"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. a \<le> x
 2. \<And>y. \<lbrakk>a \<le> y; y \<le> x\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x - fu x) has_real_derivative - g y) (at y)
 3. \<And>y. \<lbrakk>a \<le> y; y \<le> x\<rbrakk> \<Longrightarrow> - g y \<le> 0
 4. f a = fu a
[PROOF STEP]
using assms DERIV_minus [where f = "\<lambda>x. fu x - f x"]
[PROOF STATE]
proof (prove)
using this:
a \<le> x
\<lbrakk>a \<le> ?y; ?y \<le> x\<rbrakk> \<Longrightarrow> ((\<lambda>x. fu x - f x) has_real_derivative g ?y) (at ?y)
\<lbrakk>a \<le> ?y; ?y \<le> x\<rbrakk> \<Longrightarrow> 0 \<le> g ?y
fu a = f a
((\<lambda>x. fu x - f x) has_real_derivative ?D) (at ?x within ?s) \<Longrightarrow> ((\<lambda>x. - (fu x - f x)) has_real_derivative - ?D) (at ?x within ?s)

goal (4 subgoals):
 1. a \<le> x
 2. \<And>y. \<lbrakk>a \<le> y; y \<le> x\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x - fu x) has_real_derivative - g y) (at y)
 3. \<And>y. \<lbrakk>a \<le> y; y \<le> x\<rbrakk> \<Longrightarrow> - g y \<le> 0
 4. f a = fu a
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma gen_upper_bound_decreasing:
  fixes a :: real
  assumes "x \<le> a"
      and "\<And>y. x \<le> y \<Longrightarrow> y \<le> a \<Longrightarrow> ((\<lambda>x. fu x - f x) has_real_derivative g y) (at y)"
      and "\<And>y. x \<le> y \<Longrightarrow> y \<le> a \<Longrightarrow> g y \<le> 0"
      and "fu a = f a"
    shows "f x \<le> fu x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x \<le> fu x
[PROOF STEP]
apply (rule gen_lower_bound_decreasing [of x a _ _  "\<lambda>u. - g u"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. x \<le> a
 2. \<And>y. \<lbrakk>x \<le> y; y \<le> a\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x - fu x) has_real_derivative - g y) (at y)
 3. \<And>y. \<lbrakk>x \<le> y; y \<le> a\<rbrakk> \<Longrightarrow> 0 \<le> - g y
 4. f a = fu a
[PROOF STEP]
using assms DERIV_minus [where f = "\<lambda>x. fu x - f x"]
[PROOF STATE]
proof (prove)
using this:
x \<le> a
\<lbrakk>x \<le> ?y; ?y \<le> a\<rbrakk> \<Longrightarrow> ((\<lambda>x. fu x - f x) has_real_derivative g ?y) (at ?y)
\<lbrakk>x \<le> ?y; ?y \<le> a\<rbrakk> \<Longrightarrow> g ?y \<le> 0
fu a = f a
((\<lambda>x. fu x - f x) has_real_derivative ?D) (at ?x within ?s) \<Longrightarrow> ((\<lambda>x. - (fu x - f x)) has_real_derivative - ?D) (at ?x within ?s)

goal (4 subgoals):
 1. x \<le> a
 2. \<And>y. \<lbrakk>x \<le> y; y \<le> a\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x - fu x) has_real_derivative - g y) (at y)
 3. \<And>y. \<lbrakk>x \<le> y; y \<le> a\<rbrakk> \<Longrightarrow> 0 \<le> - g y
 4. f a = fu a
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma open_domain[intro, simp]: "open (domain c)"
  and open_codomain[intro, simp]: "open (codomain c)"
  and chart_homeomorphism: "homeomorphism (domain c) (codomain c) c (inv_chart c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (domain c) &&& open (codomain c) &&& homeomorphism (domain c) (codomain c) (apply_chart c) (inv_chart c)
[PROOF STEP]
by (transfer, auto)+


[STATEMENT]
lemma at_within_domain: "at x within domain c = at x" if "x \<in> domain c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. at x within domain c = at x
[PROOF STEP]
by (rule at_within_open[OF that open_domain])


[STATEMENT]
lemma at_within_codomain: "at x within codomain c = at x" if "x \<in> codomain c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. at x within codomain c = at x
[PROOF STEP]
by (rule at_within_open[OF that open_codomain])


[STATEMENT]
lemma chart_eqI: "c = d"
  if "domain c = domain d"
    "codomain c = codomain d"
    "\<And>x. c x = d x"
    "\<And>x. inv_chart c x = inv_chart  d x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c = d
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
domain c = domain d
codomain c = codomain d
apply_chart c ?x = apply_chart d ?x
inv_chart c ?x = inv_chart d ?x

goal (1 subgoal):
 1. c = d
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma continuous_apply_chart: "continuous (at x within X) c" if "x \<in> domain c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous (at x within X) (apply_chart c)
[PROOF STEP]
apply (rule continuous_at_imp_continuous_within)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isCont (apply_chart c) x
[PROOF STEP]
using continuous_on_domain[of c] that at_within_domain[OF that]
[PROOF STATE]
proof (prove)
using this:
continuous_on (domain c) (apply_chart c)
x \<in> domain c
at x within domain c = at x

goal (1 subgoal):
 1. isCont (apply_chart c) x
[PROOF STEP]
by (auto simp: continuous_on_eq_continuous_within)


[STATEMENT]
lemma continuous_inv_chart: "continuous (at x within X) (inv_chart c)" if "x \<in> codomain c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous (at x within X) (inv_chart c)
[PROOF STEP]
apply (rule continuous_at_imp_continuous_within)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isCont (inv_chart c) x
[PROOF STEP]
using continuous_on_codomain[of c] that at_within_codomain[OF that]
[PROOF STATE]
proof (prove)
using this:
continuous_on (codomain c) (inv_chart c)
x \<in> codomain c
at x within codomain c = at x

goal (1 subgoal):
 1. isCont (inv_chart c) x
[PROOF STEP]
by (auto simp: continuous_on_eq_continuous_within)


[STATEMENT]
lemma continuous_within_compose2':
  "continuous (at (f x) within t) g \<Longrightarrow> f ` s \<subseteq> t \<Longrightarrow>
    continuous (at x within s) f \<Longrightarrow>
    continuous (at x within s) (\<lambda>x. g (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>continuous (at (f x) within t) g; f ` s \<subseteq> t; continuous (at x within s) f\<rbrakk> \<Longrightarrow> continuous (at x within s) (\<lambda>x. g (f x))
[PROOF STEP]
by (simp add: continuous_within_compose2 continuous_within_subset)


[STATEMENT]
lemma continuous_on_chart_inv:
  assumes "continuous_on s (apply_chart c o f)"
    "f ` s \<subseteq> domain c"
  shows "continuous_on s f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on s f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. continuous_on s f
[PROOF STEP]
have "continuous_on s (inv_chart c o apply_chart c o f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on s (inv_chart c \<circ> apply_chart c \<circ> f)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
continuous_on s (apply_chart c \<circ> f)
f ` s \<subseteq> domain c

goal (1 subgoal):
 1. continuous_on s (inv_chart c \<circ> apply_chart c \<circ> f)
[PROOF STEP]
by (auto intro!: continuous_on_chart(2))
[PROOF STATE]
proof (state)
this:
continuous_on s (inv_chart c \<circ> apply_chart c \<circ> f)

goal (1 subgoal):
 1. continuous_on s f
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
continuous_on s (inv_chart c \<circ> apply_chart c \<circ> f)

goal (1 subgoal):
 1. continuous_on s f
[PROOF STEP]
have "\<And>x. x \<in> s \<Longrightarrow> (inv_chart c o apply_chart c o f) x = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> s \<Longrightarrow> (inv_chart c \<circ> apply_chart c \<circ> f) x = f x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
continuous_on s (apply_chart c \<circ> f)
f ` s \<subseteq> domain c

goal (1 subgoal):
 1. \<And>x. x \<in> s \<Longrightarrow> (inv_chart c \<circ> apply_chart c \<circ> f) x = f x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x \<in> s \<Longrightarrow> (inv_chart c \<circ> apply_chart c \<circ> f) ?x = f ?x

goal (1 subgoal):
 1. continuous_on s f
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
continuous_on s (inv_chart c \<circ> apply_chart c \<circ> f)
?x \<in> s \<Longrightarrow> (inv_chart c \<circ> apply_chart c \<circ> f) ?x = f ?x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
continuous_on s (inv_chart c \<circ> apply_chart c \<circ> f)
?x \<in> s \<Longrightarrow> (inv_chart c \<circ> apply_chart c \<circ> f) ?x = f ?x

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma continuous_on_chart_inv':
  assumes "continuous_on (apply_chart c ` s) (f o inv_chart c)"
    "s \<subseteq> domain c"
  shows "continuous_on s f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on s f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. continuous_on s f
[PROOF STEP]
have "continuous_on s (apply_chart c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on s (apply_chart c)
[PROOF STEP]
using assms continuous_on_domain continuous_on_subset
[PROOF STATE]
proof (prove)
using this:
continuous_on (apply_chart c ` s) (f \<circ> inv_chart c)
s \<subseteq> domain c
continuous_on (domain ?c) (apply_chart ?c)
\<lbrakk>continuous_on ?s ?f; ?t \<subseteq> ?s\<rbrakk> \<Longrightarrow> continuous_on ?t ?f

goal (1 subgoal):
 1. continuous_on s (apply_chart c)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
continuous_on s (apply_chart c)

goal (1 subgoal):
 1. continuous_on s f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
continuous_on s (apply_chart c)
[PROOF STEP]
have "continuous_on s (f o inv_chart c o apply_chart c)"
[PROOF STATE]
proof (prove)
using this:
continuous_on s (apply_chart c)

goal (1 subgoal):
 1. continuous_on s (f \<circ> inv_chart c \<circ> apply_chart c)
[PROOF STEP]
apply (rule continuous_on_compose)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on (apply_chart c ` s) (f \<circ> inv_chart c)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
continuous_on (apply_chart c ` s) (f \<circ> inv_chart c)
s \<subseteq> domain c

goal (1 subgoal):
 1. continuous_on (apply_chart c ` s) (f \<circ> inv_chart c)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
continuous_on s (f \<circ> inv_chart c \<circ> apply_chart c)

goal (1 subgoal):
 1. continuous_on s f
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
continuous_on s (f \<circ> inv_chart c \<circ> apply_chart c)

goal (1 subgoal):
 1. continuous_on s f
[PROOF STEP]
have "(f o inv_chart c o apply_chart c) x = f x" if "x \<in> s" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<circ> inv_chart c \<circ> apply_chart c) x = f x
[PROOF STEP]
using assms that
[PROOF STATE]
proof (prove)
using this:
continuous_on (apply_chart c ` s) (f \<circ> inv_chart c)
s \<subseteq> domain c
x \<in> s

goal (1 subgoal):
 1. (f \<circ> inv_chart c \<circ> apply_chart c) x = f x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x \<in> s \<Longrightarrow> (f \<circ> inv_chart c \<circ> apply_chart c) ?x = f ?x

goal (1 subgoal):
 1. continuous_on s f
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
continuous_on s (f \<circ> inv_chart c \<circ> apply_chart c)
?x \<in> s \<Longrightarrow> (f \<circ> inv_chart c \<circ> apply_chart c) ?x = f ?x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
continuous_on s (f \<circ> inv_chart c \<circ> apply_chart c)
?x \<in> s \<Longrightarrow> (f \<circ> inv_chart c \<circ> apply_chart c) ?x = f ?x

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inj_on_apply_chart: "inj_on (apply_chart f) (domain f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (apply_chart f) (domain f)
[PROOF STEP]
by (auto simp: intro!: inj_on_inverseI[where g="inv_chart f"])


[STATEMENT]
lemma apply_chart_Int: "f ` (X \<inter> Y) = f ` X \<inter> f ` Y" if "X \<subseteq> domain f" "Y \<subseteq> domain f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_chart f ` (X \<inter> Y) = apply_chart f ` X \<inter> apply_chart f ` Y
[PROOF STEP]
using inj_on_apply_chart that
[PROOF STATE]
proof (prove)
using this:
inj_on (apply_chart ?f) (domain ?f)
X \<subseteq> domain f
Y \<subseteq> domain f

goal (1 subgoal):
 1. apply_chart f ` (X \<inter> Y) = apply_chart f ` X \<inter> apply_chart f ` Y
[PROOF STEP]
by (rule inj_on_image_Int)


[STATEMENT]
lemma chart_image_eq_vimage: "c ` X = inv_chart c -` X \<inter> codomain c"
  if "X \<subseteq> domain c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_chart c ` X = inv_chart c -` X \<inter> codomain c
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> domain c

goal (1 subgoal):
 1. apply_chart c ` X = inv_chart c -` X \<inter> codomain c
[PROOF STEP]
by force


[STATEMENT]
lemma open_chart_image[simp, intro]: "open (c ` X)"
  if "open X" "X \<subseteq> domain c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (apply_chart c ` X)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. open (apply_chart c ` X)
[PROOF STEP]
have "c ` X = inv_chart c -` X \<inter> codomain c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_chart c ` X = inv_chart c -` X \<inter> codomain c
[PROOF STEP]
using that(2)
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> domain c

goal (1 subgoal):
 1. apply_chart c ` X = inv_chart c -` X \<inter> codomain c
[PROOF STEP]
by (rule chart_image_eq_vimage)
[PROOF STATE]
proof (state)
this:
apply_chart c ` X = inv_chart c -` X \<inter> codomain c

goal (1 subgoal):
 1. open (apply_chart c ` X)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
apply_chart c ` X = inv_chart c -` X \<inter> codomain c

goal (1 subgoal):
 1. open (apply_chart c ` X)
[PROOF STEP]
have "open \<dots>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (inv_chart c -` X \<inter> codomain c)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
open X
X \<subseteq> domain c

goal (1 subgoal):
 1. open (inv_chart c -` X \<inter> codomain c)
[PROOF STEP]
by (metis continuous_on_codomain continuous_on_open_vimage open_codomain)
[PROOF STATE]
proof (state)
this:
open (inv_chart c -` X \<inter> codomain c)

goal (1 subgoal):
 1. open (apply_chart c ` X)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
open (apply_chart c ` X)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
open (apply_chart c ` X)

goal (1 subgoal):
 1. open (apply_chart c ` X)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
open (apply_chart c ` X)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma open_inv_chart_image[simp, intro]: "open (inv_chart c ` X)"
  if "open X" "X \<subseteq> codomain c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (inv_chart c ` X)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. open (inv_chart c ` X)
[PROOF STEP]
have "inv_chart c ` X = c -` X \<inter> domain c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_chart c ` X = apply_chart c -` X \<inter> domain c
[PROOF STEP]
using that(2)
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> codomain c

goal (1 subgoal):
 1. inv_chart c ` X = apply_chart c -` X \<inter> domain c
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>X \<subseteq> codomain c; x \<in> domain c; apply_chart c x \<in> X\<rbrakk> \<Longrightarrow> x \<in> inv_chart c ` X
[PROOF STEP]
using image_iff
[PROOF STATE]
proof (prove)
using this:
(?z \<in> ?f ` ?A) = (\<exists>x\<in>?A. ?z = ?f x)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>X \<subseteq> codomain c; x \<in> domain c; apply_chart c x \<in> X\<rbrakk> \<Longrightarrow> x \<in> inv_chart c ` X
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
inv_chart c ` X = apply_chart c -` X \<inter> domain c

goal (1 subgoal):
 1. open (inv_chart c ` X)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
inv_chart c ` X = apply_chart c -` X \<inter> domain c

goal (1 subgoal):
 1. open (inv_chart c ` X)
[PROOF STEP]
have "open \<dots>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (apply_chart c -` X \<inter> domain c)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
open X
X \<subseteq> codomain c

goal (1 subgoal):
 1. open (apply_chart c -` X \<inter> domain c)
[PROOF STEP]
by (metis continuous_on_domain continuous_on_open_vimage open_domain)
[PROOF STATE]
proof (state)
this:
open (apply_chart c -` X \<inter> domain c)

goal (1 subgoal):
 1. open (inv_chart c ` X)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
open (inv_chart c ` X)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
open (inv_chart c ` X)

goal (1 subgoal):
 1. open (inv_chart c ` X)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
open (inv_chart c ` X)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma homeomorphism_UNIV_imp_open_map:
  "homeomorphism UNIV UNIV p p' \<Longrightarrow> open f' \<Longrightarrow> open (p ` f')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>homeomorphism UNIV UNIV p p'; open f'\<rbrakk> \<Longrightarrow> open (p ` f')
[PROOF STEP]
by (auto dest: homeomorphism_imp_open_map[where U=f'])


[STATEMENT]
lemma homeomorphism_restrict:
  "homeomorphism (a \<inter> s) (b \<inter> f' -` s) f f'" if "homeomorphism a b f f'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. homeomorphism (a \<inter> s) (b \<inter> f' -` s) f f'
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
homeomorphism a b f f'

goal (1 subgoal):
 1. homeomorphism (a \<inter> s) (b \<inter> f' -` s) f f'
[PROOF STEP]
by (fastforce simp: homeomorphism_def intro: continuous_on_subset intro!: imageI)


[STATEMENT]
lemma restrict_chart_restrict_chart:
  "restrict_chart X (restrict_chart Y c) = restrict_chart (X \<inter> Y) c"
  if "open X" "open Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict_chart X (restrict_chart Y c) = restrict_chart (X \<inter> Y) c
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
open X
open Y

goal (1 subgoal):
 1. restrict_chart X (restrict_chart Y c) = restrict_chart (X \<inter> Y) c
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma domain_restrict_chart[simp]: "open S \<Longrightarrow> domain (restrict_chart S c) = domain c \<inter> S"
  and domain_restrict_chart_if: "domain (restrict_chart S c) = (if open S then domain c \<inter> S else {})"
  and codomain_restrict_chart[simp]: "open S \<Longrightarrow> codomain (restrict_chart S c) = codomain c \<inter> inv_chart c -` S"
  and codomain_restrict_chart_if: "codomain (restrict_chart S c) = (if open S then codomain c \<inter> inv_chart c -` S else {})"
  and apply_chart_restrict_chart[simp]: "apply_chart (restrict_chart S c) = apply_chart c"
  and inv_chart_restrict_chart[simp]: "inv_chart (restrict_chart S c) = inv_chart c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((open S \<Longrightarrow> domain (restrict_chart S c) = domain c \<inter> S) &&& domain (restrict_chart S c) = (if open S then domain c \<inter> S else {}) &&& (open S \<Longrightarrow> codomain (restrict_chart S c) = codomain c \<inter> inv_chart c -` S)) &&& codomain (restrict_chart S c) = (if open S then codomain c \<inter> inv_chart c -` S else {}) &&& apply_chart (restrict_chart S c) = apply_chart c &&& inv_chart (restrict_chart S c) = inv_chart c
[PROOF STEP]
by (transfer, auto)+


[STATEMENT]
lemma compose_chart_apply_chart[simp]: "apply_chart (compose_chart p p' c) = p o apply_chart c"
  and compose_chart_inv_chart[simp]: "inv_chart (compose_chart p p' c) = inv_chart c o p'"
  and domain_compose_chart[simp]: "domain (compose_chart p p' c) = domain c"
  and codomain_compose_chart[simp]: "codomain (compose_chart p p' c) = p ` codomain c"
  if "homeomorphism UNIV UNIV p p'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (apply_chart (compose_chart p p' c) = p \<circ> apply_chart c &&& inv_chart (compose_chart p p' c) = inv_chart c \<circ> p') &&& domain (compose_chart p p' c) = domain c &&& codomain (compose_chart p p' c) = p ` codomain c
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
homeomorphism UNIV UNIV p p'

goal (1 subgoal):
 1. (apply_chart (compose_chart p p' c) = p \<circ> apply_chart c &&& inv_chart (compose_chart p p' c) = inv_chart c \<circ> p') &&& domain (compose_chart p p' c) = domain c &&& codomain (compose_chart p p' c) = p ` codomain c
[PROOF STEP]
by (transfer, auto)+


[STATEMENT]
lemma freess_cons[simp]: "freess (x # xs) = frees x |\<union>| freess xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freess (x # xs) = frees x |\<union>| freess xs
[PROOF STEP]
unfolding freess_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ffUnion \<circ> fset_of_list \<circ> map frees) (x # xs) = frees x |\<union>| (ffUnion \<circ> fset_of_list \<circ> map frees) xs
[PROOF STEP]
by simp


[STATEMENT]
lemma freess_single: "freess [x] = frees x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freess [x] = frees x
[PROOF STEP]
unfolding freess_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ffUnion \<circ> fset_of_list \<circ> map frees) [x] = frees x
[PROOF STEP]
by simp


[STATEMENT]
lemma freess_empty[simp]: "freess [] = {||}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freess [] = {||}
[PROOF STEP]
unfolding freess_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ffUnion \<circ> fset_of_list \<circ> map frees) [] = {||}
[PROOF STEP]
by simp


[STATEMENT]
lemma freess_app[simp]: "freess (xs @ ys) = freess xs |\<union>| freess ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freess (xs @ ys) = freess xs |\<union>| freess ys
[PROOF STEP]
unfolding freess_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ffUnion \<circ> fset_of_list \<circ> map frees) (xs @ ys) = (ffUnion \<circ> fset_of_list \<circ> map frees) xs |\<union>| (ffUnion \<circ> fset_of_list \<circ> map frees) ys
[PROOF STEP]
by simp


[STATEMENT]
lemma freess_subset: "set xs \<subseteq> set ys \<Longrightarrow> freess xs |\<subseteq>| freess ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set xs \<subseteq> set ys \<Longrightarrow> freess xs |\<subseteq>| freess ys
[PROOF STEP]
unfolding freess_def comp_apply
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set xs \<subseteq> set ys \<Longrightarrow> ffUnion (fset_of_list (map frees xs)) |\<subseteq>| ffUnion (fset_of_list (map frees ys))
[PROOF STEP]
by (intro ffunion_mono fset_of_list_subset) auto


[STATEMENT]
lemma app_size1: "size u\<^sub>1 < size (app u\<^sub>1 u\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size u\<^sub>1 < size (app u\<^sub>1 u\<^sub>2)
[PROOF STEP]
by simp


[STATEMENT]
lemma app_size2: "size u\<^sub>2 < size (app u\<^sub>1 u\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size u\<^sub>2 < size (app u\<^sub>1 u\<^sub>2)
[PROOF STEP]
by simp


[STATEMENT]
lemma unx_some_lemmas:
  "unapp u = Some x \<Longrightarrow> unconst u = None"
  "unapp u = Some x \<Longrightarrow> unfree u = None"
  "unconst u = Some y \<Longrightarrow> unapp u = None"
  "unconst u = Some y \<Longrightarrow> unfree u = None"
  "unfree u = Some z \<Longrightarrow> unconst u = None"
  "unfree u = Some z \<Longrightarrow> unapp u = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((unapp u = Some x \<Longrightarrow> unconst u = None) &&& (unapp u = Some x \<Longrightarrow> unfree u = None) &&& (unconst u = Some y \<Longrightarrow> unapp u = None)) &&& (unconst u = Some y \<Longrightarrow> unfree u = None) &&& (unfree u = Some z \<Longrightarrow> unconst u = None) &&& (unfree u = Some z \<Longrightarrow> unapp u = None)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unapp u = Some x \<Longrightarrow> unconst u = None
[PROOF STEP]
by (metis app_unapp const_unconst app_const_distinct not_None_eq surj_pair)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. unapp u = Some x \<Longrightarrow> unfree u = None
 2. unconst u = Some y \<Longrightarrow> unapp u = None
 3. unconst u = Some y \<Longrightarrow> unfree u = None
 4. unfree u = Some z \<Longrightarrow> unconst u = None
 5. unfree u = Some z \<Longrightarrow> unapp u = None
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unapp u = Some x \<Longrightarrow> unfree u = None
[PROOF STEP]
by (metis app_free_distinct app_unapp free_unfree option.exhaust surj_pair)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. unconst u = Some y \<Longrightarrow> unapp u = None
 2. unconst u = Some y \<Longrightarrow> unfree u = None
 3. unfree u = Some z \<Longrightarrow> unconst u = None
 4. unfree u = Some z \<Longrightarrow> unapp u = None
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unconst u = Some y \<Longrightarrow> unapp u = None
[PROOF STEP]
by (metis app_unapp const_unconst app_const_distinct old.prod.exhaust option.distinct(1) option.expand option.sel)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. unconst u = Some y \<Longrightarrow> unfree u = None
 2. unfree u = Some z \<Longrightarrow> unconst u = None
 3. unfree u = Some z \<Longrightarrow> unapp u = None
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unconst u = Some y \<Longrightarrow> unfree u = None
[PROOF STEP]
by (metis const_unconst free_const_distinct free_unfree option.exhaust)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. unfree u = Some z \<Longrightarrow> unconst u = None
 2. unfree u = Some z \<Longrightarrow> unapp u = None
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unfree u = Some z \<Longrightarrow> unconst u = None
[PROOF STEP]
by (metis const_unconst free_const_distinct free_unfree option.exhaust)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unfree u = Some z \<Longrightarrow> unapp u = None
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unfree u = Some z \<Longrightarrow> unapp u = None
[PROOF STEP]
by (metis app_free_distinct app_unapp free_unfree not_Some_eq surj_pair)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma unx_none_simps[simp]:
  "unapp (const name) = None"
  "unapp (free name) = None"
  "unconst (app t u) = None"
  "unconst (free name) = None"
  "unfree (const name) = None"
  "unfree (app t u) = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (unapp (const name) = None &&& unapp (free name) = None &&& unconst (app t u) = None) &&& unconst (free name) = None &&& unfree (const name) = None &&& unfree (app t u) = None
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unapp (const name) = None
[PROOF STEP]
by (metis app_unapp app_const_distinct not_None_eq surj_pair)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. unapp (free name) = None
 2. unconst (app t u) = None
 3. unconst (free name) = None
 4. unfree (const name) = None
 5. unfree (app t u) = None
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unapp (free name) = None
[PROOF STEP]
by (metis app_free_distinct app_unapp option.exhaust surj_pair)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. unconst (app t u) = None
 2. unconst (free name) = None
 3. unfree (const name) = None
 4. unfree (app t u) = None
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unconst (app t u) = None
[PROOF STEP]
by (metis const_unconst app_const_distinct option.distinct(1) option.expand option.sel)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. unconst (free name) = None
 2. unfree (const name) = None
 3. unfree (app t u) = None
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unconst (free name) = None
[PROOF STEP]
by (metis const_unconst free_const_distinct option.exhaust)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. unfree (const name) = None
 2. unfree (app t u) = None
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unfree (const name) = None
[PROOF STEP]
by (metis free_const_distinct free_unfree option.exhaust)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unfree (app t u) = None
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unfree (app t u) = None
[PROOF STEP]
by (metis app_free_distinct free_unfree not_Some_eq)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma term_cases:
  obtains (free) name where "t = free name"
        | (const) name where "t = const name"
        | (app) u\<^sub>1 u\<^sub>2 where "t = app u\<^sub>1 u\<^sub>2"
        | (other) "unfree t = None" "unapp t = None" "unconst t = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> thesis; \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (cases "unfree t")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> thesis; \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> thesis; unfree t = None\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> thesis; \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> thesis; unfree t = Some a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (cases "unconst t")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> thesis; \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> thesis; unfree t = None; unconst t = None\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> thesis; \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> thesis; unfree t = None; unconst t = Some a\<rbrakk> \<Longrightarrow> thesis
 3. \<And>a. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> thesis; \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> thesis; unfree t = Some a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (cases "unapp t")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> thesis; \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> thesis; unfree t = None; unconst t = None; unapp t = None\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> thesis; \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> thesis; unfree t = None; unconst t = None; unapp t = Some a\<rbrakk> \<Longrightarrow> thesis
 3. \<And>a. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> thesis; \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> thesis; unfree t = None; unconst t = Some a\<rbrakk> \<Longrightarrow> thesis
 4. \<And>a. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> thesis; \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> thesis; unfree t = Some a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> thesis; \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> thesis; unfree t = None; unconst t = None; unapp t = None\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> thesis; \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> thesis; unfree t = None; unconst t = None; unapp t = Some a\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> thesis; \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> thesis; unfree t = None; unconst t = Some a\<rbrakk> \<Longrightarrow> thesis
 3. \<And>a. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> thesis; \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> thesis; unfree t = Some a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> thesis; \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> thesis; unfree t = None; unconst t = None; unapp t = Some x\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (cases x) auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> thesis; \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> thesis; unfree t = None; unconst t = Some a\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> thesis; \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> thesis; unfree t = Some a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> thesis; \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> thesis; unfree t = None; unconst t = Some a_\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> thesis; \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> thesis; unfree t = Some a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> thesis; \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> thesis; unfree t = Some a_\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_const_simps[simp]:
  "is_const (const name)"
  "\<not> is_const (app t u)"
  "\<not> is_const (free name)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_const (const name) &&& \<not> is_const (app t u) &&& \<not> is_const (free name)
[PROOF STEP]
unfolding is_const_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unconst (const name) \<noteq> None &&& \<not> unconst (app t u) \<noteq> None &&& \<not> unconst (free name) \<noteq> None
[PROOF STEP]
by simp+


[STATEMENT]
lemma const_name_simps[simp]:
  "const_name (const name) = name"
  "is_const t \<Longrightarrow> const (const_name t) = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. const_name (const name) = name &&& (is_const t \<Longrightarrow> const (const_name t) = t)
[PROOF STEP]
unfolding const_name_def is_const_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case unconst (const name) of Some name \<Rightarrow> name) = name &&& (unconst t \<noteq> None \<Longrightarrow> const (case unconst t of Some name \<Rightarrow> name) = t)
[PROOF STEP]
by auto


[STATEMENT]
lemma is_free_simps[simp]:
  "is_free (free name)"
  "\<not> is_free (const name)"
  "\<not> is_free (app t u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_free (free name) &&& \<not> is_free (const name) &&& \<not> is_free (app t u)
[PROOF STEP]
unfolding is_free_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unfree (free name) \<noteq> None &&& \<not> unfree (const name) \<noteq> None &&& \<not> unfree (app t u) \<noteq> None
[PROOF STEP]
by simp+


[STATEMENT]
lemma free_name_simps[simp]:
  "free_name (free name) = name"
  "is_free t \<Longrightarrow> free (free_name t) = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. free_name (free name) = name &&& (is_free t \<Longrightarrow> free (free_name t) = t)
[PROOF STEP]
unfolding free_name_def is_free_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case unfree (free name) of Some name \<Rightarrow> name) = name &&& (unfree t \<noteq> None \<Longrightarrow> free (case unfree t of Some name \<Rightarrow> name) = t)
[PROOF STEP]
by auto


[STATEMENT]
lemma app_simps[simp]:
  "\<not> is_app (const name)"
  "\<not> is_app (free name)"
  "is_app (app t u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_app (const name) &&& \<not> is_app (free name) &&& is_app (app t u)
[PROOF STEP]
unfolding is_app_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> unapp (const name) \<noteq> None &&& \<not> unapp (free name) \<noteq> None &&& unapp (app t u) \<noteq> None
[PROOF STEP]
by simp+