[STATEMENT]
lemma act_sup_distr: "\<alpha> (x \<squnion> y) p = (\<alpha> x p) \<squnion> (\<alpha> y p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> (x \<squnion> y) p = \<alpha> x p \<squnion> \<alpha> y p
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<alpha> (x \<squnion> y) p = \<alpha> x p \<squnion> \<alpha> y p
[PROOF STEP]
have "\<alpha> (x \<squnion> y) p  = \<alpha> (\<Squnion>{x,y}) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> (x \<squnion> y) p = \<alpha> (\<Squnion>{x, y}) p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<alpha> (x \<squnion> y) p = \<alpha> (\<Squnion>{x, y}) p

goal (1 subgoal):
 1. \<alpha> (x \<squnion> y) p = \<alpha> x p \<squnion> \<alpha> y p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<alpha> (x \<squnion> y) p = \<alpha> (\<Squnion>{x, y}) p

goal (1 subgoal):
 1. \<alpha> (x \<squnion> y) p = \<alpha> x p \<squnion> \<alpha> y p
[PROOF STEP]
have "... = \<Squnion>{\<alpha> v p |v. v \<in> {x,y}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> (\<Squnion>{x, y}) p = \<Squnion>{\<alpha> v p |v. v \<in> {x, y}}
[PROOF STEP]
by (rule act3)
[PROOF STATE]
proof (state)
this:
\<alpha> (\<Squnion>{x, y}) p = \<Squnion>{\<alpha> v p |v. v \<in> {x, y}}

goal (1 subgoal):
 1. \<alpha> (x \<squnion> y) p = \<alpha> x p \<squnion> \<alpha> y p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<alpha> (\<Squnion>{x, y}) p = \<Squnion>{\<alpha> v p |v. v \<in> {x, y}}

goal (1 subgoal):
 1. \<alpha> (x \<squnion> y) p = \<alpha> x p \<squnion> \<alpha> y p
[PROOF STEP]
have "... = \<Squnion>{v. v = \<alpha> x p \<or> v = \<alpha> y p}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion>{\<alpha> v p |v. v \<in> {x, y}} = \<Squnion>{v. v = \<alpha> x p \<or> v = \<alpha> y p}
[PROOF STEP]
by (metis empty_iff insert_iff)
[PROOF STATE]
proof (state)
this:
\<Squnion>{\<alpha> v p |v. v \<in> {x, y}} = \<Squnion>{v. v = \<alpha> x p \<or> v = \<alpha> y p}

goal (1 subgoal):
 1. \<alpha> (x \<squnion> y) p = \<alpha> x p \<squnion> \<alpha> y p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<alpha> (x \<squnion> y) p = \<Squnion>{v. v = \<alpha> x p \<or> v = \<alpha> y p}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<alpha> (x \<squnion> y) p = \<Squnion>{v. v = \<alpha> x p \<or> v = \<alpha> y p}

goal (1 subgoal):
 1. \<alpha> (x \<squnion> y) p = \<alpha> x p \<squnion> \<alpha> y p
[PROOF STEP]
by (metis Collect_disj_eq Sup_insert ccpo_Sup_singleton insert_def singleton_conv)
[PROOF STATE]
proof (state)
this:
\<alpha> (x \<squnion> y) p = \<alpha> x p \<squnion> \<alpha> y p

goal:
No subgoals!
[PROOF STEP]
qed