[STATEMENT]
lemma \<phi>E:
assumes \<phi>: "\<phi> (Trans s a ou s')" (is "\<phi> ?trn")
and step: "step s a = (ou, s')"
and rs: "reach s"
obtains (Friend) uid p uid' where "a = Cact (cFriend uid p uid')" "ou = outOK" "f ?trn = FrVal True"
                                  "uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1"
                                  "IDsOK s [UID1, UID2] []"
                                  "\<not>friends12 s" "friends12 s'"
      | (Unfriend) uid p uid' where "a = Dact (dFriend uid p uid')" "ou = outOK" "f ?trn = FrVal False"
                                    "uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1"
                                    "IDsOK s [UID1, UID2] []"
                                    "friends12 s" "\<not>friends12 s'"
      | (OpenF) uid p uid' where "a = Cact (cFriend uid p uid')"
                                 "(uid \<in> UIDs \<and> uid' \<in> {UID1,UID2}) \<or> (uid' \<in> UIDs \<and> uid \<in> {UID1,UID2})"
                                 "ou = outOK" "f ?trn = OVal True" "\<not>openByF s" "openByF s'"
                                 "\<not>openByA s" "\<not>openByA s'"
      | (CloseF) uid p uid' where "a = Dact (dFriend uid p uid')"
                                  "(uid \<in> UIDs \<and> uid' \<in> {UID1,UID2}) \<or> (uid' \<in> UIDs \<and> uid \<in> {UID1,UID2})"
                                  "ou = outOK" "f ?trn = OVal False" "openByF s" "\<not>openByF s'"
                                  "\<not>openByA s" "\<not>openByA s'"
      | (CloseA) uid p uid' p' where "a = Cact (cUser uid p uid' p')"
                                     "uid' \<in> {UID1,UID2}" "openByA s" "\<not>openByA s'"
                                     "\<not>openByF s" "\<not>openByF s'"
                                     "ou = outOK" "f ?trn = OVal False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using \<phi>
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s a ou s')

goal (1 subgoal):
 1. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
proof (elim \<phi>.elims disjE conjE)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cFriend uid p uid')) oua s'a; (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)}; oua = outOK\<rbrakk> \<Longrightarrow> thesis
 2. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 3. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)}; oua = outOK\<rbrakk> \<Longrightarrow> thesis
 4. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 5. \<And>sa uid p uid' p' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cUser uid p uid' p')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
fix s1 uid p uid' ou1 s1'
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cFriend uid p uid')) oua s'a; (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)}; oua = outOK\<rbrakk> \<Longrightarrow> thesis
 2. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 3. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)}; oua = outOK\<rbrakk> \<Longrightarrow> thesis
 4. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 5. \<And>sa uid p uid' p' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cUser uid p uid' p')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume "(uid,uid') \<in> {(UID1,UID2), (UID2,UID1)}" and ou: "ou1 = outOK"
     and "?trn = Trans s1 (Cact (cFriend uid p uid')) ou1 s1'"
[PROOF STATE]
proof (state)
this:
(uid, uid') \<in> {(UID1, UID2), (UID2, UID1)}
ou1 = outOK
Trans s a ou s' = Trans s1 (Cact (cFriend uid p uid')) ou1 s1'

goal (5 subgoals):
 1. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cFriend uid p uid')) oua s'a; (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)}; oua = outOK\<rbrakk> \<Longrightarrow> thesis
 2. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 3. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)}; oua = outOK\<rbrakk> \<Longrightarrow> thesis
 4. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 5. \<And>sa uid p uid' p' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cUser uid p uid' p')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(uid, uid') \<in> {(UID1, UID2), (UID2, UID1)}
ou1 = outOK
Trans s a ou s' = Trans s1 (Cact (cFriend uid p uid')) ou1 s1'
[PROOF STEP]
have trn: "a = Cact (cFriend uid p uid')" "s = s1" "s' = s1'" "ou = ou1"
        and uids: "uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1"
[PROOF STATE]
proof (prove)
using this:
(uid, uid') \<in> {(UID1, UID2), (UID2, UID1)}
ou1 = outOK
Trans s a ou s' = Trans s1 (Cact (cFriend uid p uid')) ou1 s1'

goal (1 subgoal):
 1. ((a = Cact (cFriend uid p uid') &&& s = s1) &&& s' = s1' &&& ou = ou1) &&& uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1
[PROOF STEP]
using UID1_UID2
[PROOF STATE]
proof (prove)
using this:
(uid, uid') \<in> {(UID1, UID2), (UID2, UID1)}
ou1 = outOK
Trans s a ou s' = Trans s1 (Cact (cFriend uid p uid')) ou1 s1'
UID1 \<noteq> UID2

goal (1 subgoal):
 1. ((a = Cact (cFriend uid p uid') &&& s = s1) &&& s' = s1' &&& ou = ou1) &&& uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = Cact (cFriend uid p uid')
s = s1
s' = s1'
ou = ou1
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1

goal (5 subgoals):
 1. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cFriend uid p uid')) oua s'a; (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)}; oua = outOK\<rbrakk> \<Longrightarrow> thesis
 2. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 3. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)}; oua = outOK\<rbrakk> \<Longrightarrow> thesis
 4. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 5. \<And>sa uid p uid' p' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cUser uid p uid' p')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = Cact (cFriend uid p uid')
s = s1
s' = s1'
ou = ou1
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
a = Cact (cFriend uid p uid')
s = s1
s' = s1'
ou = ou1
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using ou uids trn step UID1_UID2_UIDs UID1_UID2 reach_distinct_friends_reqs[OF rs]
[PROOF STATE]
proof (prove)
using this:
a = Cact (cFriend uid p uid')
s = s1
s' = s1'
ou = ou1
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1
ou1 = outOK
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1
a = Cact (cFriend uid p uid')
s = s1
s' = s1'
ou = ou1
step s a = (ou, s')
{UID1, UID2} \<inter> UIDs = {}
UID1 \<noteq> UID2
distinct (friendIDs s ?uid)
distinct (pendingFReqs s ?uid)
?uid' \<in>\<in> pendingFReqs s ?uid \<Longrightarrow> ?uid' \<notin> set (friendIDs s ?uid)
?uid' \<in>\<in> pendingFReqs s ?uid \<Longrightarrow> ?uid \<notin> set (friendIDs s ?uid')

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (intro Friend[of uid p uid']) (auto simp add: c_defs friends12_def)
[PROOF STATE]
proof (state)
this:
thesis

goal (4 subgoals):
 1. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 2. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)}; oua = outOK\<rbrakk> \<Longrightarrow> thesis
 3. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 4. \<And>sa uid p uid' p' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cUser uid p uid' p')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 2. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)}; oua = outOK\<rbrakk> \<Longrightarrow> thesis
 3. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 4. \<And>sa uid p uid' p' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cUser uid p uid' p')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
fix s1 uid p uid' ou1 s1'
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 2. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)}; oua = outOK\<rbrakk> \<Longrightarrow> thesis
 3. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 4. \<And>sa uid p uid' p' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cUser uid p uid' p')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume op: "open s1 \<noteq> open s1'"
     and "?trn = Trans s1 (Cact (cFriend uid p uid')) ou1 s1'"
[PROOF STATE]
proof (state)
this:
open s1 \<noteq> open s1'
Trans s a ou s' = Trans s1 (Cact (cFriend uid p uid')) ou1 s1'

goal (4 subgoals):
 1. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 2. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)}; oua = outOK\<rbrakk> \<Longrightarrow> thesis
 3. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 4. \<And>sa uid p uid' p' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cUser uid p uid' p')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
open s1 \<noteq> open s1'
Trans s a ou s' = Trans s1 (Cact (cFriend uid p uid')) ou1 s1'
[PROOF STEP]
have trn: "a = Cact (cFriend uid p uid')" "s = s1" "s' = s1'" "ou = ou1"
[PROOF STATE]
proof (prove)
using this:
open s1 \<noteq> open s1'
Trans s a ou s' = Trans s1 (Cact (cFriend uid p uid')) ou1 s1'

goal (1 subgoal):
 1. (a = Cact (cFriend uid p uid') &&& s = s1) &&& s' = s1' &&& ou = ou1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = Cact (cFriend uid p uid')
s = s1
s' = s1'
ou = ou1

goal (4 subgoals):
 1. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 2. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)}; oua = outOK\<rbrakk> \<Longrightarrow> thesis
 3. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 4. \<And>sa uid p uid' p' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cUser uid p uid' p')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = Cact (cFriend uid p uid')
s = s1
s' = s1'
ou = ou1
[PROOF STEP]
have uids: "uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid \<in> {UID1, UID2} \<and> uid' \<in> UIDs" "ou = outOK"
                  "\<not>openByF s1" "openByF s1'" "\<not>openByA s1" "\<not>openByA s1'"
[PROOF STATE]
proof (prove)
using this:
a = Cact (cFriend uid p uid')
s = s1
s' = s1'
ou = ou1

goal (1 subgoal):
 1. (uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid \<in> {UID1, UID2} \<and> uid' \<in> UIDs &&& ou = outOK &&& \<not> openByF s1) &&& openByF s1' &&& \<not> openByA s1 &&& \<not> openByA s1'
[PROOF STEP]
using op step
[PROOF STATE]
proof (prove)
using this:
a = Cact (cFriend uid p uid')
s = s1
s' = s1'
ou = ou1
open s1 \<noteq> open s1'
step s a = (ou, s')

goal (1 subgoal):
 1. (uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid \<in> {UID1, UID2} \<and> uid' \<in> UIDs &&& ou = outOK &&& \<not> openByF s1) &&& openByF s1' &&& \<not> openByA s1 &&& \<not> openByA s1'
[PROOF STEP]
by (auto simp add: c_defs open_def openByA_def openByF_def)
[PROOF STATE]
proof (state)
this:
uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid \<in> {UID1, UID2} \<and> uid' \<in> UIDs
ou = outOK
\<not> openByF s1
openByF s1'
\<not> openByA s1
\<not> openByA s1'

goal (4 subgoals):
 1. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 2. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)}; oua = outOK\<rbrakk> \<Longrightarrow> thesis
 3. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 4. \<And>sa uid p uid' p' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cUser uid p uid' p')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid \<in> {UID1, UID2} \<and> uid' \<in> UIDs
ou = outOK
\<not> openByF s1
openByF s1'
\<not> openByA s1
\<not> openByA s1'
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid \<in> {UID1, UID2} \<and> uid' \<in> UIDs
ou = outOK
\<not> openByF s1
openByF s1'
\<not> openByA s1
\<not> openByA s1'

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using op trn step UID1_UID2_UIDs UID1_UID2
[PROOF STATE]
proof (prove)
using this:
uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid \<in> {UID1, UID2} \<and> uid' \<in> UIDs
ou = outOK
\<not> openByF s1
openByF s1'
\<not> openByA s1
\<not> openByA s1'
open s1 \<noteq> open s1'
a = Cact (cFriend uid p uid')
s = s1
s' = s1'
ou = ou1
step s a = (ou, s')
{UID1, UID2} \<inter> UIDs = {}
UID1 \<noteq> UID2

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

goal (3 subgoals):
 1. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)}; oua = outOK\<rbrakk> \<Longrightarrow> thesis
 2. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 3. \<And>sa uid p uid' p' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cUser uid p uid' p')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)}; oua = outOK\<rbrakk> \<Longrightarrow> thesis
 2. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 3. \<And>sa uid p uid' p' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cUser uid p uid' p')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
fix s1 uid p uid' ou1 s1'
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)}; oua = outOK\<rbrakk> \<Longrightarrow> thesis
 2. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 3. \<And>sa uid p uid' p' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cUser uid p uid' p')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume "(uid,uid') \<in> {(UID1,UID2), (UID2,UID1)}" and ou: "ou1 = outOK"
     and "?trn = Trans s1 (Dact (dFriend uid p uid')) ou1 s1'"
[PROOF STATE]
proof (state)
this:
(uid, uid') \<in> {(UID1, UID2), (UID2, UID1)}
ou1 = outOK
Trans s a ou s' = Trans s1 (Dact (dFriend uid p uid')) ou1 s1'

goal (3 subgoals):
 1. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)}; oua = outOK\<rbrakk> \<Longrightarrow> thesis
 2. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 3. \<And>sa uid p uid' p' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cUser uid p uid' p')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(uid, uid') \<in> {(UID1, UID2), (UID2, UID1)}
ou1 = outOK
Trans s a ou s' = Trans s1 (Dact (dFriend uid p uid')) ou1 s1'
[PROOF STEP]
have trn: "a = Dact (dFriend uid p uid')" "s = s1" "s' = s1'" "ou = ou1"
        and uids: "uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1"
[PROOF STATE]
proof (prove)
using this:
(uid, uid') \<in> {(UID1, UID2), (UID2, UID1)}
ou1 = outOK
Trans s a ou s' = Trans s1 (Dact (dFriend uid p uid')) ou1 s1'

goal (1 subgoal):
 1. ((a = Dact (dFriend uid p uid') &&& s = s1) &&& s' = s1' &&& ou = ou1) &&& uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1
[PROOF STEP]
using UID1_UID2
[PROOF STATE]
proof (prove)
using this:
(uid, uid') \<in> {(UID1, UID2), (UID2, UID1)}
ou1 = outOK
Trans s a ou s' = Trans s1 (Dact (dFriend uid p uid')) ou1 s1'
UID1 \<noteq> UID2

goal (1 subgoal):
 1. ((a = Dact (dFriend uid p uid') &&& s = s1) &&& s' = s1' &&& ou = ou1) &&& uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = Dact (dFriend uid p uid')
s = s1
s' = s1'
ou = ou1
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1

goal (3 subgoals):
 1. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)}; oua = outOK\<rbrakk> \<Longrightarrow> thesis
 2. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 3. \<And>sa uid p uid' p' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cUser uid p uid' p')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = Dact (dFriend uid p uid')
s = s1
s' = s1'
ou = ou1
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
a = Dact (dFriend uid p uid')
s = s1
s' = s1'
ou = ou1
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using step ou reach_friendIDs_symmetric[OF rs]
[PROOF STATE]
proof (prove)
using this:
a = Dact (dFriend uid p uid')
s = s1
s' = s1'
ou = ou1
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1
step s a = (ou, s')
ou1 = outOK
(?uID1.0 \<in>\<in> friendIDs s ?uID2.0) = (?uID2.0 \<in>\<in> friendIDs s ?uID1.0)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (intro Unfriend) (auto simp: d_defs friends12_def)
[PROOF STATE]
proof (state)
this:
thesis

goal (2 subgoals):
 1. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 2. \<And>sa uid p uid' p' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cUser uid p uid' p')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 2. \<And>sa uid p uid' p' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cUser uid p uid' p')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
fix s1 uid p uid' ou1 s1'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 2. \<And>sa uid p uid' p' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cUser uid p uid' p')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume op: "open s1 \<noteq> open s1'"
     and "?trn = Trans s1 (Dact (dFriend uid p uid')) ou1 s1'"
[PROOF STATE]
proof (state)
this:
open s1 \<noteq> open s1'
Trans s a ou s' = Trans s1 (Dact (dFriend uid p uid')) ou1 s1'

goal (2 subgoals):
 1. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 2. \<And>sa uid p uid' p' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cUser uid p uid' p')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
open s1 \<noteq> open s1'
Trans s a ou s' = Trans s1 (Dact (dFriend uid p uid')) ou1 s1'
[PROOF STEP]
have trn: "a = Dact (dFriend uid p uid')" "s = s1" "s' = s1'" "ou = ou1"
[PROOF STATE]
proof (prove)
using this:
open s1 \<noteq> open s1'
Trans s a ou s' = Trans s1 (Dact (dFriend uid p uid')) ou1 s1'

goal (1 subgoal):
 1. (a = Dact (dFriend uid p uid') &&& s = s1) &&& s' = s1' &&& ou = ou1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = Dact (dFriend uid p uid')
s = s1
s' = s1'
ou = ou1

goal (2 subgoals):
 1. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 2. \<And>sa uid p uid' p' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cUser uid p uid' p')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = Dact (dFriend uid p uid')
s = s1
s' = s1'
ou = ou1
[PROOF STEP]
have uids: "uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid \<in> {UID1, UID2} \<and> uid' \<in> UIDs" "ou = outOK"
                  "openByF s1" "\<not>openByF s1'" "\<not>openByA s1" "\<not>openByA s1'"
[PROOF STATE]
proof (prove)
using this:
a = Dact (dFriend uid p uid')
s = s1
s' = s1'
ou = ou1

goal (1 subgoal):
 1. (uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid \<in> {UID1, UID2} \<and> uid' \<in> UIDs &&& ou = outOK &&& openByF s1) &&& \<not> openByF s1' &&& \<not> openByA s1 &&& \<not> openByA s1'
[PROOF STEP]
using op step
[PROOF STATE]
proof (prove)
using this:
a = Dact (dFriend uid p uid')
s = s1
s' = s1'
ou = ou1
open s1 \<noteq> open s1'
step s a = (ou, s')

goal (1 subgoal):
 1. (uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid \<in> {UID1, UID2} \<and> uid' \<in> UIDs &&& ou = outOK &&& openByF s1) &&& \<not> openByF s1' &&& \<not> openByA s1 &&& \<not> openByA s1'
[PROOF STEP]
by (auto simp add: d_defs open_def openByA_def openByF_def)
[PROOF STATE]
proof (state)
this:
uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid \<in> {UID1, UID2} \<and> uid' \<in> UIDs
ou = outOK
openByF s1
\<not> openByF s1'
\<not> openByA s1
\<not> openByA s1'

goal (2 subgoals):
 1. \<And>sa uid p uid' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Dact (dFriend uid p uid')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
 2. \<And>sa uid p uid' p' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cUser uid p uid' p')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid \<in> {UID1, UID2} \<and> uid' \<in> UIDs
ou = outOK
openByF s1
\<not> openByF s1'
\<not> openByA s1
\<not> openByA s1'
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid \<in> {UID1, UID2} \<and> uid' \<in> UIDs
ou = outOK
openByF s1
\<not> openByF s1'
\<not> openByA s1
\<not> openByA s1'

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using op trn step UID1_UID2_UIDs UID1_UID2
[PROOF STATE]
proof (prove)
using this:
uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid \<in> {UID1, UID2} \<and> uid' \<in> UIDs
ou = outOK
openByF s1
\<not> openByF s1'
\<not> openByA s1
\<not> openByA s1'
open s1 \<noteq> open s1'
a = Dact (dFriend uid p uid')
s = s1
s' = s1'
ou = ou1
step s a = (ou, s')
{UID1, UID2} \<inter> UIDs = {}
UID1 \<noteq> UID2

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

goal (1 subgoal):
 1. \<And>sa uid p uid' p' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cUser uid p uid' p')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>sa uid p uid' p' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cUser uid p uid' p')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
fix s1 uid p uid' p' ou1 s1'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>sa uid p uid' p' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cUser uid p uid' p')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume op: "open s1 \<noteq> open s1'"
     and "?trn = Trans s1 (Cact (cUser uid p uid' p')) ou1 s1'"
[PROOF STATE]
proof (state)
this:
open s1 \<noteq> open s1'
Trans s a ou s' = Trans s1 (Cact (cUser uid p uid' p')) ou1 s1'

goal (1 subgoal):
 1. \<And>sa uid p uid' p' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cUser uid p uid' p')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
open s1 \<noteq> open s1'
Trans s a ou s' = Trans s1 (Cact (cUser uid p uid' p')) ou1 s1'
[PROOF STEP]
have trn: "a = Cact (cUser uid p uid' p')" "s = s1" "s' = s1'" "ou = ou1"
[PROOF STATE]
proof (prove)
using this:
open s1 \<noteq> open s1'
Trans s a ou s' = Trans s1 (Cact (cUser uid p uid' p')) ou1 s1'

goal (1 subgoal):
 1. (a = Cact (cUser uid p uid' p') &&& s = s1) &&& s' = s1' &&& ou = ou1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = Cact (cUser uid p uid' p')
s = s1
s' = s1'
ou = ou1

goal (1 subgoal):
 1. \<And>sa uid p uid' p' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cUser uid p uid' p')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = Cact (cUser uid p uid' p')
s = s1
s' = s1'
ou = ou1
[PROOF STEP]
have uids: "uid' = UID2 \<or> uid' = UID1" "ou = outOK"
                  "\<not>openByF s1" "\<not>openByF s1'" "openByA s1" "\<not>openByA s1'"
[PROOF STATE]
proof (prove)
using this:
a = Cact (cUser uid p uid' p')
s = s1
s' = s1'
ou = ou1

goal (1 subgoal):
 1. (uid' = UID2 \<or> uid' = UID1 &&& ou = outOK &&& \<not> openByF s1) &&& \<not> openByF s1' &&& openByA s1 &&& \<not> openByA s1'
[PROOF STEP]
using op step
[PROOF STATE]
proof (prove)
using this:
a = Cact (cUser uid p uid' p')
s = s1
s' = s1'
ou = ou1
open s1 \<noteq> open s1'
step s a = (ou, s')

goal (1 subgoal):
 1. (uid' = UID2 \<or> uid' = UID1 &&& ou = outOK &&& \<not> openByF s1) &&& \<not> openByF s1' &&& openByA s1 &&& \<not> openByA s1'
[PROOF STEP]
by (auto simp add: c_defs open_def openByF_def openByA_def)
[PROOF STATE]
proof (state)
this:
uid' = UID2 \<or> uid' = UID1
ou = outOK
\<not> openByF s1
\<not> openByF s1'
openByA s1
\<not> openByA s1'

goal (1 subgoal):
 1. \<And>sa uid p uid' p' oua s'a. \<lbrakk>\<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal True; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; \<not> friends12 s; friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; f (Trans s a ou s') = FrVal False; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; IDsOK s [UID1, UID2] []; friends12 s; \<not> friends12 s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal True; \<not> openByF s; openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); uid \<in> UIDs \<and> uid' \<in> {UID1, UID2} \<or> uid' \<in> UIDs \<and> uid \<in> {UID1, UID2}; ou = outOK; f (Trans s a ou s') = OVal False; openByF s; \<not> openByF s'; \<not> openByA s; \<not> openByA s'\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid' p'. \<lbrakk>a = Cact (cUser uid p uid' p'); uid' \<in> {UID1, UID2}; openByA s; \<not> openByA s'; \<not> openByF s; \<not> openByF s'; ou = outOK; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; Trans s a ou s' = Trans sa (Cact (cUser uid p uid' p')) oua s'a; open sa \<noteq> open s'a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
uid' = UID2 \<or> uid' = UID1
ou = outOK
\<not> openByF s1
\<not> openByF s1'
openByA s1
\<not> openByA s1'
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
uid' = UID2 \<or> uid' = UID1
ou = outOK
\<not> openByF s1
\<not> openByF s1'
openByA s1
\<not> openByA s1'

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using trn step UID1_UID2_UIDs UID1_UID2
[PROOF STATE]
proof (prove)
using this:
uid' = UID2 \<or> uid' = UID1
ou = outOK
\<not> openByF s1
\<not> openByF s1'
openByA s1
\<not> openByA s1'
a = Cact (cUser uid p uid' p')
s = s1
s' = s1'
ou = ou1
step s a = (ou, s')
{UID1, UID2} \<inter> UIDs = {}
UID1 \<noteq> UID2

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

goal:
No subgoals!
[PROOF STEP]
qed