theory EgTop

lemma "\<forall>c.
  \<not>(communicates_on c client_untrusted \<and> communicates_on c store_untrusted)" unfolding communicates_on_def client_untrusted_def Client_untrusted_def
            store_untrusted_def Store_untrusted_def apply clarsimp unfolding UserStep_def ArbitraryRequest_def ArbitraryResponse_def apply clarsimp apply (case_tac c, clarsimp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>c. \<not> (communicates_on c client_untrusted \<and> communicates_on c store_untrusted) proof (prove)
goal (1 subgoal):
 1. \<forall>c. \<not> ((sends_on c LOOP UserStep \<squnion> ArbitraryRequest (case Client_l of Client_l \<Rightarrow> one) \<squnion> ArbitraryResponse (case Client_l of Client_l \<Rightarrow> one) \<or> receives_on c LOOP UserStep \<squnion> ArbitraryRequest (case Client_l of Client_l \<Rightarrow> one) \<squnion> ArbitraryResponse (case Client_l of Client_l \<Rightarrow> one)) \<and> (sends_on c LOOP UserStep \<squnion> ArbitraryRequest (case Store_l of Store_l \<Rightarrow> two) \<squnion> ArbitraryResponse (case Store_l of Store_l \<Rightarrow> two) \<or> receives_on c LOOP UserStep \<squnion> ArbitraryRequest (case Store_l of Store_l \<Rightarrow> two) \<squnion> ArbitraryResponse (case Store_l of Store_l \<Rightarrow> two))) proof (prove)
goal (1 subgoal):
 1. \<And>c. sends_on c UserStep \<or> sends_on c (ArbitraryRequest two) \<or> sends_on c (ArbitraryResponse two) \<or> receives_on c UserStep \<or> receives_on c (ArbitraryRequest two) \<or> receives_on c (ArbitraryResponse two) \<Longrightarrow> \<not> sends_on c UserStep \<and> \<not> sends_on c (ArbitraryRequest one) \<and> \<not> sends_on c (ArbitraryResponse one) \<and> \<not> receives_on c UserStep \<and> \<not> receives_on c (ArbitraryRequest one) \<and> \<not> receives_on c (ArbitraryResponse one) proof (prove)
goal (1 subgoal):
 1. \<And>c. sends_on c (LocalOp internal) \<or> sends_on c (Request (\<lambda>_. {x. q_channel x = two}) (\<lambda>_ _. UNIV\<^sub>c)) \<or> sends_on c (Response (\<lambda>_ _. {(s', \<beta>). s' \<in> UNIV\<^sub>c \<and> a_channel \<beta> = two})) \<or> receives_on c (LocalOp internal) \<or> receives_on c (Request (\<lambda>_. {x. q_channel x = two}) (\<lambda>_ _. UNIV\<^sub>c)) \<or> receives_on c (Response (\<lambda>_ _. {(s', \<beta>). s' \<in> UNIV\<^sub>c \<and> a_channel \<beta> = two})) \<Longrightarrow> \<not> sends_on c (LocalOp internal) \<and> \<not> sends_on c (Request (\<lambda>_. {x. q_channel x = one}) (\<lambda>_ _. UNIV\<^sub>c)) \<and> \<not> sends_on c (Response (\<lambda>_ _. {(s', \<beta>). s' \<in> UNIV\<^sub>c \<and> a_channel \<beta> = one})) \<and> \<not> receives_on c (LocalOp internal) \<and> \<not> receives_on c (Request (\<lambda>_. {x. q_channel x = one}) (\<lambda>_ _. UNIV\<^sub>c)) \<and> \<not> receives_on c (Response (\<lambda>_ _. {(s', \<beta>). s' \<in> UNIV\<^sub>c \<and> a_channel \<beta> = one})) proof (prove)
goal (1 subgoal):
 1. \<And>c. (\<exists>q. q_channel q = two) \<and> two = c \<or> (\<exists>x. x \<in> UNIV\<^sub>c) \<and> (\<exists>y. a_channel y = two) \<and> two = c \<Longrightarrow> ((\<forall>q. q_channel q \<noteq> one) \<or> one \<noteq> c) \<and> (UNIV\<^sub>c = {} \<or> (\<forall>y. a_channel y \<noteq> one) \<or> one \<noteq> c) proof (prove)
goal:
No subgoals!