[STATEMENT]
lemma compatible_up[simp]: "compatible (up\<cdot>x) (up\<cdot>y) \<longleftrightarrow> compatible x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compatible (up\<cdot>x) (up\<cdot>y) = compatible x y
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. compatible (up\<cdot>x) (up\<cdot>y) \<Longrightarrow> compatible x y
 2. compatible x y \<Longrightarrow> compatible (up\<cdot>x) (up\<cdot>y)
[PROOF STEP]
assume "compatible (up\<cdot>x) (up\<cdot>y)"
[PROOF STATE]
proof (state)
this:
compatible (up\<cdot>x) (up\<cdot>y)

goal (2 subgoals):
 1. compatible (up\<cdot>x) (up\<cdot>y) \<Longrightarrow> compatible x y
 2. compatible x y \<Longrightarrow> compatible (up\<cdot>x) (up\<cdot>y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
compatible (up\<cdot>x) (up\<cdot>y)
[PROOF STEP]
obtain z' where z': "{up\<cdot>x,up\<cdot>y} <<| z'"
[PROOF STATE]
proof (prove)
using this:
compatible (up\<cdot>x) (up\<cdot>y)

goal (1 subgoal):
 1. (\<And>z'. {up\<cdot>x, up\<cdot>y} <<| z' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding compatible_def
[PROOF STATE]
proof (prove)
using this:
Ex ((<<|) {up\<cdot>x, up\<cdot>y})

goal (1 subgoal):
 1. (\<And>z'. {up\<cdot>x, up\<cdot>y} <<| z' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{up\<cdot>x, up\<cdot>y} <<| z'

goal (2 subgoals):
 1. compatible (up\<cdot>x) (up\<cdot>y) \<Longrightarrow> compatible x y
 2. compatible x y \<Longrightarrow> compatible (up\<cdot>x) (up\<cdot>y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{up\<cdot>x, up\<cdot>y} <<| z'
[PROOF STEP]
obtain z where  "{up\<cdot>x,up\<cdot>y} <<| up\<cdot>z"
[PROOF STATE]
proof (prove)
using this:
{up\<cdot>x, up\<cdot>y} <<| z'

goal (1 subgoal):
 1. (\<And>z. {up\<cdot>x, up\<cdot>y} <<| up\<cdot>z \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases z') auto
[PROOF STATE]
proof (state)
this:
{up\<cdot>x, up\<cdot>y} <<| up\<cdot>z

goal (2 subgoals):
 1. compatible (up\<cdot>x) (up\<cdot>y) \<Longrightarrow> compatible x y
 2. compatible x y \<Longrightarrow> compatible (up\<cdot>x) (up\<cdot>y)
[PROOF STEP]
hence "{x,y} <<| z"
[PROOF STATE]
proof (prove)
using this:
{up\<cdot>x, up\<cdot>y} <<| up\<cdot>z

goal (1 subgoal):
 1. {x, y} <<| z
[PROOF STEP]
unfolding is_lub_def
[PROOF STATE]
proof (prove)
using this:
{up\<cdot>x, up\<cdot>y} <| up\<cdot>z \<and> (\<forall>u. {up\<cdot>x, up\<cdot>y} <| u \<longrightarrow> up\<cdot>z \<sqsubseteq> u)

goal (1 subgoal):
 1. {x, y} <| z \<and> (\<forall>u. {x, y} <| u \<longrightarrow> z \<sqsubseteq> u)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>u. \<lbrakk>x \<sqsubseteq> z; y \<sqsubseteq> z; \<forall>u. up\<cdot>x \<sqsubseteq> u \<and> up\<cdot>y \<sqsubseteq> u \<longrightarrow> up\<cdot>z \<sqsubseteq> u; x \<sqsubseteq> u; y \<sqsubseteq> u\<rbrakk> \<Longrightarrow> z \<sqsubseteq> u
[PROOF STEP]
by (metis up_below)
[PROOF STATE]
proof (state)
this:
{x, y} <<| z

goal (2 subgoals):
 1. compatible (up\<cdot>x) (up\<cdot>y) \<Longrightarrow> compatible x y
 2. compatible x y \<Longrightarrow> compatible (up\<cdot>x) (up\<cdot>y)
[PROOF STEP]
thus "compatible x y"
[PROOF STATE]
proof (prove)
using this:
{x, y} <<| z

goal (1 subgoal):
 1. compatible x y
[PROOF STEP]
unfolding compatible_def
[PROOF STATE]
proof (prove)
using this:
{x, y} <<| z

goal (1 subgoal):
 1. Ex ((<<|) {x, y})
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
compatible x y

goal (1 subgoal):
 1. compatible x y \<Longrightarrow> compatible (up\<cdot>x) (up\<cdot>y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. compatible x y \<Longrightarrow> compatible (up\<cdot>x) (up\<cdot>y)
[PROOF STEP]
assume "compatible x y"
[PROOF STATE]
proof (state)
this:
compatible x y

goal (1 subgoal):
 1. compatible x y \<Longrightarrow> compatible (up\<cdot>x) (up\<cdot>y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
compatible x y
[PROOF STEP]
obtain z where z: "{x,y} <<| z"
[PROOF STATE]
proof (prove)
using this:
compatible x y

goal (1 subgoal):
 1. (\<And>z. {x, y} <<| z \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding compatible_def
[PROOF STATE]
proof (prove)
using this:
Ex ((<<|) {x, y})

goal (1 subgoal):
 1. (\<And>z. {x, y} <<| z \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x, y} <<| z

goal (1 subgoal):
 1. compatible x y \<Longrightarrow> compatible (up\<cdot>x) (up\<cdot>y)
[PROOF STEP]
hence  "{up\<cdot>x,up\<cdot>y} <<| up\<cdot>z"
[PROOF STATE]
proof (prove)
using this:
{x, y} <<| z

goal (1 subgoal):
 1. {up\<cdot>x, up\<cdot>y} <<| up\<cdot>z
[PROOF STEP]
unfolding is_lub_def
[PROOF STATE]
proof (prove)
using this:
{x, y} <| z \<and> (\<forall>u. {x, y} <| u \<longrightarrow> z \<sqsubseteq> u)

goal (1 subgoal):
 1. {up\<cdot>x, up\<cdot>y} <| up\<cdot>z \<and> (\<forall>u. {up\<cdot>x, up\<cdot>y} <| u \<longrightarrow> up\<cdot>z \<sqsubseteq> u)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>u. \<lbrakk>x \<sqsubseteq> z; y \<sqsubseteq> z; \<forall>u. x \<sqsubseteq> u \<and> y \<sqsubseteq> u \<longrightarrow> z \<sqsubseteq> u; up\<cdot>x \<sqsubseteq> u; up\<cdot>y \<sqsubseteq> u\<rbrakk> \<Longrightarrow> up\<cdot>z \<sqsubseteq> u
[PROOF STEP]
by (metis not_up_less_UU upE up_below)
[PROOF STATE]
proof (state)
this:
{up\<cdot>x, up\<cdot>y} <<| up\<cdot>z

goal (1 subgoal):
 1. compatible x y \<Longrightarrow> compatible (up\<cdot>x) (up\<cdot>y)
[PROOF STEP]
thus "compatible (up\<cdot>x) (up\<cdot>y)"
[PROOF STATE]
proof (prove)
using this:
{up\<cdot>x, up\<cdot>y} <<| up\<cdot>z

goal (1 subgoal):
 1. compatible (up\<cdot>x) (up\<cdot>y)
[PROOF STEP]
unfolding compatible_def
[PROOF STATE]
proof (prove)
using this:
{up\<cdot>x, up\<cdot>y} <<| up\<cdot>z

goal (1 subgoal):
 1. Ex ((<<|) {up\<cdot>x, up\<cdot>y})
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
compatible (up\<cdot>x) (up\<cdot>y)

goal:
No subgoals!
[PROOF STEP]
qed