[STATEMENT]
lemma less_prod_Pair_conv:
  "((a\<^sub>1,b\<^sub>1) \<sqsubset>\<^bsub>Product.le r\<^sub>A r\<^sub>B\<^esub> (a\<^sub>2,b\<^sub>2)) =
  (a\<^sub>1 \<sqsubset>\<^bsub>r\<^sub>A\<^esub> a\<^sub>2 & b\<^sub>1 \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> b\<^sub>2 | a\<^sub>1 \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> a\<^sub>2 & b\<^sub>1 \<sqsubset>\<^bsub>r\<^sub>B\<^esub> b\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((a\<^sub>1, b\<^sub>1) \<sqsubset>\<^bsub>Product.le r\<^sub>A r\<^sub>B\<^esub> (a\<^sub>2, b\<^sub>2)) = (a\<^sub>1 \<sqsubset>\<^bsub>r\<^sub>A\<^esub> a\<^sub>2 \<and> b\<^sub>1 \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> b\<^sub>2 \<or> a\<^sub>1 \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> a\<^sub>2 \<and> b\<^sub>1 \<sqsubset>\<^bsub>r\<^sub>B\<^esub> b\<^sub>2)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((a\<^sub>1, b\<^sub>1) \<sqsubset>\<^bsub>Product.le r\<^sub>A r\<^sub>B\<^esub> (a\<^sub>2, b\<^sub>2)) = (a\<^sub>1 \<sqsubset>\<^bsub>r\<^sub>A\<^esub> a\<^sub>2 \<and> b\<^sub>1 \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> b\<^sub>2 \<or> a\<^sub>1 \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> a\<^sub>2 \<and> b\<^sub>1 \<sqsubset>\<^bsub>r\<^sub>B\<^esub> b\<^sub>2)
[PROOF STEP]
apply (unfold lesssub_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((a\<^sub>1, b\<^sub>1) <=(r\<^sub>A,r\<^sub>B) (a\<^sub>2, b\<^sub>2) \<and> (a\<^sub>1, b\<^sub>1) \<noteq> (a\<^sub>2, b\<^sub>2)) = ((a\<^sub>1 \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> a\<^sub>2 \<and> a\<^sub>1 \<noteq> a\<^sub>2) \<and> b\<^sub>1 \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> b\<^sub>2 \<or> a\<^sub>1 \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> a\<^sub>2 \<and> b\<^sub>1 \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> b\<^sub>2 \<and> b\<^sub>1 \<noteq> b\<^sub>2)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a\<^sub>1 \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> a\<^sub>2 \<and> b\<^sub>1 \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> b\<^sub>2 \<and> (a\<^sub>1 = a\<^sub>2 \<longrightarrow> b\<^sub>1 \<noteq> b\<^sub>2)) = (a\<^sub>1 \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> a\<^sub>2 \<and> a\<^sub>1 \<noteq> a\<^sub>2 \<and> b\<^sub>1 \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> b\<^sub>2 \<or> a\<^sub>1 \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> a\<^sub>2 \<and> b\<^sub>1 \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> b\<^sub>2 \<and> b\<^sub>1 \<noteq> b\<^sub>2)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma order_le_prodI [iff]: "(order r\<^sub>A  A & order r\<^sub>B B) \<Longrightarrow> order (Product.le r\<^sub>A r\<^sub>B) (A \<times> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order r\<^sub>A A \<and> order r\<^sub>B B \<Longrightarrow> order (Product.le r\<^sub>A r\<^sub>B) (A \<times> B)
[PROOF STEP]
apply (unfold order_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>x\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<longrightarrow> x = y) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z)) \<and> (\<forall>x\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x) \<and> (\<forall>x\<in>B. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x \<longrightarrow> x = y) \<and> (\<forall>x\<in>B. \<forall>y\<in>B. \<forall>z\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z) \<Longrightarrow> (\<forall>x\<in>A \<times> B. x <=(r\<^sub>A,r\<^sub>B) x) \<and> (\<forall>x\<in>A \<times> B. \<forall>y\<in>A \<times> B. x <=(r\<^sub>A,r\<^sub>B) y \<and> y <=(r\<^sub>A,r\<^sub>B) x \<longrightarrow> x = y) \<and> (\<forall>x\<in>A \<times> B. \<forall>y\<in>A \<times> B. \<forall>z\<in>A \<times> B. x <=(r\<^sub>A,r\<^sub>B) y \<and> y <=(r\<^sub>A,r\<^sub>B) z \<longrightarrow> x <=(r\<^sub>A,r\<^sub>B) z)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>x\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x; \<forall>x\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x; \<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<longrightarrow> x = y; \<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z; \<forall>x\<in>B. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x \<longrightarrow> x = y; \<forall>x\<in>B. \<forall>y\<in>B. \<forall>z\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z; a \<in> A; b \<in> B\<rbrakk> \<Longrightarrow> a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> a
 2. \<And>a b. \<lbrakk>\<forall>x\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x; \<forall>x\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x; \<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<longrightarrow> x = y; \<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z; \<forall>x\<in>B. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x \<longrightarrow> x = y; \<forall>x\<in>B. \<forall>y\<in>B. \<forall>z\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z; a \<in> A; b \<in> B\<rbrakk> \<Longrightarrow> b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> b
 3. \<And>a b aa ba. \<lbrakk>\<forall>x\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x; \<forall>x\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x; \<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<longrightarrow> x = y; \<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z; \<forall>x\<in>B. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x \<longrightarrow> x = y; \<forall>x\<in>B. \<forall>y\<in>B. \<forall>z\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z; a \<in> A; b \<in> B; aa \<in> A; ba \<in> B; a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> aa; b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ba; aa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> a; ba \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> b\<rbrakk> \<Longrightarrow> a = aa
 4. \<And>a b aa ba. \<lbrakk>\<forall>x\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x; \<forall>x\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x; \<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<longrightarrow> x = y; \<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z; \<forall>x\<in>B. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x \<longrightarrow> x = y; \<forall>x\<in>B. \<forall>y\<in>B. \<forall>z\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z; a \<in> A; b \<in> B; aa \<in> A; ba \<in> B; a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> aa; b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ba; aa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> a; ba \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> b\<rbrakk> \<Longrightarrow> b = ba
 5. \<And>a b aa ba ab bb. \<lbrakk>\<forall>x\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x; \<forall>x\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x; \<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<longrightarrow> x = y; \<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z; \<forall>x\<in>B. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x \<longrightarrow> x = y; \<forall>x\<in>B. \<forall>y\<in>B. \<forall>z\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z; a \<in> A; b \<in> B; aa \<in> A; ba \<in> B; ab \<in> A; bb \<in> B; a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> aa; b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ba; aa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> ab; ba \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> bb\<rbrakk> \<Longrightarrow> a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> ab
 6. \<And>a b aa ba ab bb. \<lbrakk>\<forall>x\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x; \<forall>x\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x; \<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<longrightarrow> x = y; \<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z; \<forall>x\<in>B. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x \<longrightarrow> x = y; \<forall>x\<in>B. \<forall>y\<in>B. \<forall>z\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z; a \<in> A; b \<in> B; aa \<in> A; ba \<in> B; ab \<in> A; bb \<in> B; a \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> aa; b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ba; aa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> ab; ba \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> bb\<rbrakk> \<Longrightarrow> b \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> bb
[PROOF STEP]
apply blast+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma order_le_prodE: "A \<noteq> {} \<Longrightarrow> B \<noteq> {} \<Longrightarrow> order (Product.le r\<^sub>A r\<^sub>B) (A \<times> B) \<Longrightarrow> (order r\<^sub>A  A & order r\<^sub>B B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; B \<noteq> {}; order (Product.le r\<^sub>A r\<^sub>B) (A \<times> B)\<rbrakk> \<Longrightarrow> order r\<^sub>A A \<and> order r\<^sub>B B
[PROOF STEP]
apply (unfold order_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; B \<noteq> {}; (\<forall>x\<in>A \<times> B. x <=(r\<^sub>A,r\<^sub>B) x) \<and> (\<forall>x\<in>A \<times> B. \<forall>y\<in>A \<times> B. x <=(r\<^sub>A,r\<^sub>B) y \<and> y <=(r\<^sub>A,r\<^sub>B) x \<longrightarrow> x = y) \<and> (\<forall>x\<in>A \<times> B. \<forall>y\<in>A \<times> B. \<forall>z\<in>A \<times> B. x <=(r\<^sub>A,r\<^sub>B) y \<and> y <=(r\<^sub>A,r\<^sub>B) z \<longrightarrow> x <=(r\<^sub>A,r\<^sub>B) z)\<rbrakk> \<Longrightarrow> ((\<forall>x\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<longrightarrow> x = y) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z)) \<and> (\<forall>x\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x) \<and> (\<forall>x\<in>B. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x \<longrightarrow> x = y) \<and> (\<forall>x\<in>B. \<forall>y\<in>B. \<forall>z\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; B \<noteq> {}; (\<forall>x\<in>A. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y) \<and> (\<forall>x\<in>A. \<forall>y\<in>B. \<forall>xa\<in>A. \<forall>ya\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xa \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya \<and> xa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<and> ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<longrightarrow> x = xa \<and> y = ya) \<and> (\<forall>x\<in>A. \<forall>y\<in>B. \<forall>xa\<in>A. \<forall>ya\<in>B. \<forall>xb\<in>A. \<forall>yb\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xa \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya \<and> xa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb \<and> ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> yb \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> yb)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<longrightarrow> x = y) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z) \<and> (\<forall>x\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x) \<and> (\<forall>x\<in>B. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x \<longrightarrow> x = y) \<and> (\<forall>x\<in>B. \<forall>y\<in>B. \<forall>z\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x xa xb. \<lbrakk>\<forall>x\<in>A. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y; \<forall>x\<in>A. \<forall>y\<in>B. \<forall>xa\<in>A. \<forall>ya\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xa \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya \<and> xa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<and> ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<longrightarrow> x = xa \<and> y = ya; \<forall>x\<in>A. \<forall>y\<in>B. \<forall>xa\<in>A. \<forall>ya\<in>B. \<forall>xb\<in>A. \<forall>yb\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xa \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya \<and> xa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb \<and> ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> yb \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> yb; x \<in> A; x \<notin> {}; xa \<in> B; xa \<notin> {}; xb \<in> A\<rbrakk> \<Longrightarrow> xb \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb
 2. \<And>x xa xb y. \<lbrakk>\<forall>x\<in>A. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y; \<forall>x\<in>A. \<forall>y\<in>B. \<forall>xa\<in>A. \<forall>ya\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xa \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya \<and> xa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<and> ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<longrightarrow> x = xa \<and> y = ya; \<forall>x\<in>A. \<forall>y\<in>B. \<forall>xa\<in>A. \<forall>ya\<in>B. \<forall>xb\<in>A. \<forall>yb\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xa \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya \<and> xa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb \<and> ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> yb \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> yb; x \<in> A; x \<notin> {}; xa \<in> B; xa \<notin> {}; xb \<in> A; y \<in> A; xb \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y; y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb\<rbrakk> \<Longrightarrow> xb = y
 3. \<And>x xa xb y z. \<lbrakk>\<forall>x\<in>A. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y; \<forall>x\<in>A. \<forall>y\<in>B. \<forall>xa\<in>A. \<forall>ya\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xa \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya \<and> xa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<and> ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<longrightarrow> x = xa \<and> y = ya; \<forall>x\<in>A. \<forall>y\<in>B. \<forall>xa\<in>A. \<forall>ya\<in>B. \<forall>xb\<in>A. \<forall>yb\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xa \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya \<and> xa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb \<and> ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> yb \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> yb; x \<in> A; x \<notin> {}; xa \<in> B; xa \<notin> {}; xb \<in> A; y \<in> A; z \<in> A; xb \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y; y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z\<rbrakk> \<Longrightarrow> xb \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z
 4. \<And>x xa xb. \<lbrakk>\<forall>x\<in>A. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y; \<forall>x\<in>A. \<forall>y\<in>B. \<forall>xa\<in>A. \<forall>ya\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xa \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya \<and> xa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<and> ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<longrightarrow> x = xa \<and> y = ya; \<forall>x\<in>A. \<forall>y\<in>B. \<forall>xa\<in>A. \<forall>ya\<in>B. \<forall>xb\<in>A. \<forall>yb\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xa \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya \<and> xa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb \<and> ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> yb \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> yb; x \<in> A; x \<notin> {}; xa \<in> B; xa \<notin> {}; xb \<in> B\<rbrakk> \<Longrightarrow> xb \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> xb
 5. \<And>x xa xb y. \<lbrakk>\<forall>x\<in>A. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y; \<forall>x\<in>A. \<forall>y\<in>B. \<forall>xa\<in>A. \<forall>ya\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xa \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya \<and> xa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<and> ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<longrightarrow> x = xa \<and> y = ya; \<forall>x\<in>A. \<forall>y\<in>B. \<forall>xa\<in>A. \<forall>ya\<in>B. \<forall>xb\<in>A. \<forall>yb\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xa \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya \<and> xa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb \<and> ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> yb \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> yb; x \<in> A; x \<notin> {}; xa \<in> B; xa \<notin> {}; xb \<in> B; y \<in> B; xb \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y; y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> xb\<rbrakk> \<Longrightarrow> xb = y
 6. \<And>x xa xb y z. \<lbrakk>\<forall>x\<in>A. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y; \<forall>x\<in>A. \<forall>y\<in>B. \<forall>xa\<in>A. \<forall>ya\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xa \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya \<and> xa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<and> ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<longrightarrow> x = xa \<and> y = ya; \<forall>x\<in>A. \<forall>y\<in>B. \<forall>xa\<in>A. \<forall>ya\<in>B. \<forall>xb\<in>A. \<forall>yb\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xa \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya \<and> xa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb \<and> ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> yb \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> yb; x \<in> A; x \<notin> {}; xa \<in> B; xa \<notin> {}; xb \<in> B; y \<in> B; z \<in> B; xb \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y; y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z\<rbrakk> \<Longrightarrow> xb \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z
[PROOF STEP]
apply blast+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma order_le_prod [iff]: "A \<noteq> {} \<Longrightarrow> B \<noteq> {} \<Longrightarrow> order(Product.le r\<^sub>A r\<^sub>B) (A \<times> B) = (order r\<^sub>A A & order r\<^sub>B B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; B \<noteq> {}\<rbrakk> \<Longrightarrow> order (Product.le r\<^sub>A r\<^sub>B) (A \<times> B) = (order r\<^sub>A A \<and> order r\<^sub>B B)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; B \<noteq> {}\<rbrakk> \<Longrightarrow> order (Product.le r\<^sub>A r\<^sub>B) (A \<times> B) = (order r\<^sub>A A \<and> order r\<^sub>B B)
[PROOF STEP]
apply (unfold order_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; B \<noteq> {}\<rbrakk> \<Longrightarrow> ((\<forall>x\<in>A \<times> B. x <=(r\<^sub>A,r\<^sub>B) x) \<and> (\<forall>x\<in>A \<times> B. \<forall>y\<in>A \<times> B. x <=(r\<^sub>A,r\<^sub>B) y \<and> y <=(r\<^sub>A,r\<^sub>B) x \<longrightarrow> x = y) \<and> (\<forall>x\<in>A \<times> B. \<forall>y\<in>A \<times> B. \<forall>z\<in>A \<times> B. x <=(r\<^sub>A,r\<^sub>B) y \<and> y <=(r\<^sub>A,r\<^sub>B) z \<longrightarrow> x <=(r\<^sub>A,r\<^sub>B) z)) = (((\<forall>x\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<longrightarrow> x = y) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z)) \<and> (\<forall>x\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x) \<and> (\<forall>x\<in>B. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x \<longrightarrow> x = y) \<and> (\<forall>x\<in>B. \<forall>y\<in>B. \<forall>z\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; B \<noteq> {}\<rbrakk> \<Longrightarrow> ((\<forall>x\<in>A. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y) \<and> (\<forall>x\<in>A. \<forall>y\<in>B. \<forall>xa\<in>A. \<forall>ya\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xa \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya \<and> xa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<and> ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<longrightarrow> x = xa \<and> y = ya) \<and> (\<forall>x\<in>A. \<forall>y\<in>B. \<forall>xa\<in>A. \<forall>ya\<in>B. \<forall>xb\<in>A. \<forall>yb\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xa \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya \<and> xa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb \<and> ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> yb \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> yb)) = ((\<forall>x\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<longrightarrow> x = y) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z) \<and> (\<forall>x\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x) \<and> (\<forall>x\<in>B. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x \<longrightarrow> x = y) \<and> (\<forall>x\<in>B. \<forall>y\<in>B. \<forall>z\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z))
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (12 subgoals):
 1. \<And>x xa xb. \<lbrakk>x \<in> A; x \<notin> {}; xa \<in> B; xa \<notin> {}; \<forall>x\<in>A. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y; \<forall>x\<in>A. \<forall>y\<in>B. \<forall>xa\<in>A. \<forall>ya\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xa \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya \<and> xa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<and> ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<longrightarrow> x = xa \<and> y = ya; \<forall>x\<in>A. \<forall>y\<in>B. \<forall>xa\<in>A. \<forall>ya\<in>B. \<forall>xb\<in>A. \<forall>yb\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xa \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya \<and> xa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb \<and> ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> yb \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> yb; xb \<in> A\<rbrakk> \<Longrightarrow> xb \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb
 2. \<And>x xa xb y. \<lbrakk>x \<in> A; x \<notin> {}; xa \<in> B; xa \<notin> {}; \<forall>x\<in>A. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y; \<forall>x\<in>A. \<forall>y\<in>B. \<forall>xa\<in>A. \<forall>ya\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xa \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya \<and> xa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<and> ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<longrightarrow> x = xa \<and> y = ya; \<forall>x\<in>A. \<forall>y\<in>B. \<forall>xa\<in>A. \<forall>ya\<in>B. \<forall>xb\<in>A. \<forall>yb\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xa \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya \<and> xa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb \<and> ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> yb \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> yb; xb \<in> A; y \<in> A; xb \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y; y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb\<rbrakk> \<Longrightarrow> xb = y
 3. \<And>x xa xb y z. \<lbrakk>x \<in> A; x \<notin> {}; xa \<in> B; xa \<notin> {}; \<forall>x\<in>A. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y; \<forall>x\<in>A. \<forall>y\<in>B. \<forall>xa\<in>A. \<forall>ya\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xa \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya \<and> xa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<and> ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<longrightarrow> x = xa \<and> y = ya; \<forall>x\<in>A. \<forall>y\<in>B. \<forall>xa\<in>A. \<forall>ya\<in>B. \<forall>xb\<in>A. \<forall>yb\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xa \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya \<and> xa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb \<and> ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> yb \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> yb; xb \<in> A; y \<in> A; z \<in> A; xb \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y; y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z\<rbrakk> \<Longrightarrow> xb \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z
 4. \<And>x xa xb. \<lbrakk>x \<in> A; x \<notin> {}; xa \<in> B; xa \<notin> {}; \<forall>x\<in>A. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y; \<forall>x\<in>A. \<forall>y\<in>B. \<forall>xa\<in>A. \<forall>ya\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xa \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya \<and> xa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<and> ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<longrightarrow> x = xa \<and> y = ya; \<forall>x\<in>A. \<forall>y\<in>B. \<forall>xa\<in>A. \<forall>ya\<in>B. \<forall>xb\<in>A. \<forall>yb\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xa \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya \<and> xa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb \<and> ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> yb \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> yb; xb \<in> B\<rbrakk> \<Longrightarrow> xb \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> xb
 5. \<And>x xa xb y. \<lbrakk>x \<in> A; x \<notin> {}; xa \<in> B; xa \<notin> {}; \<forall>x\<in>A. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y; \<forall>x\<in>A. \<forall>y\<in>B. \<forall>xa\<in>A. \<forall>ya\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xa \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya \<and> xa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<and> ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<longrightarrow> x = xa \<and> y = ya; \<forall>x\<in>A. \<forall>y\<in>B. \<forall>xa\<in>A. \<forall>ya\<in>B. \<forall>xb\<in>A. \<forall>yb\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xa \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya \<and> xa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb \<and> ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> yb \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> yb; xb \<in> B; y \<in> B; xb \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y; y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> xb\<rbrakk> \<Longrightarrow> xb = y
 6. \<And>x xa xb y z. \<lbrakk>x \<in> A; x \<notin> {}; xa \<in> B; xa \<notin> {}; \<forall>x\<in>A. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y; \<forall>x\<in>A. \<forall>y\<in>B. \<forall>xa\<in>A. \<forall>ya\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xa \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya \<and> xa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<and> ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<longrightarrow> x = xa \<and> y = ya; \<forall>x\<in>A. \<forall>y\<in>B. \<forall>xa\<in>A. \<forall>ya\<in>B. \<forall>xb\<in>A. \<forall>yb\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xa \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya \<and> xa \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb \<and> ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> yb \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> yb; xb \<in> B; y \<in> B; z \<in> B; xb \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y; y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z\<rbrakk> \<Longrightarrow> xb \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z
 7. \<And>x xa xb y. \<lbrakk>x \<in> A; x \<notin> {}; xa \<in> B; xa \<notin> {}; \<forall>x\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x; \<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<longrightarrow> x = y; \<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z; \<forall>x\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x; \<forall>x\<in>B. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x \<longrightarrow> x = y; \<forall>x\<in>B. \<forall>y\<in>B. \<forall>z\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z; xb \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> xb \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb
 8. \<And>x xa xb y. \<lbrakk>x \<in> A; x \<notin> {}; xa \<in> B; xa \<notin> {}; \<forall>x\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x; \<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<longrightarrow> x = y; \<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z; \<forall>x\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x; \<forall>x\<in>B. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x \<longrightarrow> x = y; \<forall>x\<in>B. \<forall>y\<in>B. \<forall>z\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z; xb \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y
 9. \<And>x xa xb y xc ya. \<lbrakk>x \<in> A; x \<notin> {}; xa \<in> B; xa \<notin> {}; \<forall>x\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x; \<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<longrightarrow> x = y; \<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z; \<forall>x\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x; \<forall>x\<in>B. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x \<longrightarrow> x = y; \<forall>x\<in>B. \<forall>y\<in>B. \<forall>z\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z; xb \<in> A; y \<in> B; xc \<in> A; ya \<in> B; xb \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xc; y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya; xc \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb; ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y\<rbrakk> \<Longrightarrow> xb = xc
 10. \<And>x xa xb y xc ya. \<lbrakk>x \<in> A; x \<notin> {}; xa \<in> B; xa \<notin> {}; \<forall>x\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x; \<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> x \<longrightarrow> x = y; \<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> z; \<forall>x\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x; \<forall>x\<in>B. \<forall>y\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> x \<longrightarrow> x = y; \<forall>x\<in>B. \<forall>y\<in>B. \<forall>z\<in>B. x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> z; xb \<in> A; y \<in> B; xc \<in> A; ya \<in> B; xb \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xc; y \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> ya; xc \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> xb; ya \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> y\<rbrakk> \<Longrightarrow> y = ya
A total of 12 subgoals...
[PROOF STEP]
apply blast+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma acc_le_prodI [intro!]:
  "\<lbrakk> acc r\<^sub>A; acc r\<^sub>B \<rbrakk> \<Longrightarrow> acc(Product.le r\<^sub>A r\<^sub>B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>acc r\<^sub>A; acc r\<^sub>B\<rbrakk> \<Longrightarrow> acc (Product.le r\<^sub>A r\<^sub>B)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>acc r\<^sub>A; acc r\<^sub>B\<rbrakk> \<Longrightarrow> acc (Product.le r\<^sub>A r\<^sub>B)
[PROOF STEP]
apply (unfold acc_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>r\<^sub>A\<^esub> y}; wf {(y, x). x \<sqsubset>\<^bsub>r\<^sub>B\<^esub> y}\<rbrakk> \<Longrightarrow> wf {(y, x). x \<sqsubset>\<^bsub>Product.le r\<^sub>A r\<^sub>B\<^esub> y}
[PROOF STEP]
apply (rule wf_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>r\<^sub>A\<^esub> y}; wf {(y, x). x \<sqsubset>\<^bsub>r\<^sub>B\<^esub> y}\<rbrakk> \<Longrightarrow> wf ?r
 2. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>r\<^sub>A\<^esub> y}; wf {(y, x). x \<sqsubset>\<^bsub>r\<^sub>B\<^esub> y}\<rbrakk> \<Longrightarrow> {(y, x). x \<sqsubset>\<^bsub>Product.le r\<^sub>A r\<^sub>B\<^esub> y} \<subseteq> ?r
[PROOF STEP]
apply (erule wf_lex_prod)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. wf {(y, x). x \<sqsubset>\<^bsub>r\<^sub>B\<^esub> y} \<Longrightarrow> wf ?rb3
 2. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>r\<^sub>A\<^esub> y}; wf {(y, x). x \<sqsubset>\<^bsub>r\<^sub>B\<^esub> y}\<rbrakk> \<Longrightarrow> {(y, x). x \<sqsubset>\<^bsub>Product.le r\<^sub>A r\<^sub>B\<^esub> y} \<subseteq> {(y, x). x \<sqsubset>\<^bsub>r\<^sub>A\<^esub> y} <*lex*> ?rb3
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>r\<^sub>A\<^esub> y}; wf {(y, x). x \<sqsubset>\<^bsub>r\<^sub>B\<^esub> y}\<rbrakk> \<Longrightarrow> {(y, x). x \<sqsubset>\<^bsub>Product.le r\<^sub>A r\<^sub>B\<^esub> y} \<subseteq> {(y, x). x \<sqsubset>\<^bsub>r\<^sub>A\<^esub> y} <*lex*> {(y, x). x \<sqsubset>\<^bsub>r\<^sub>B\<^esub> y}
[PROOF STEP]
apply (auto simp add: lesssub_def less_prod_Pair_conv lex_prod_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma closed_lift2_sup:
  "\<lbrakk> closed (err A) (lift2 f); closed (err B) (lift2 g) \<rbrakk> \<Longrightarrow>
  closed (err(A\<times>B)) (lift2(sup f g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>closed (err A) (lift2 f); closed (err B) (lift2 g)\<rbrakk> \<Longrightarrow> closed (err (A \<times> B)) (lift2 (Product.sup f g))
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>closed (err A) (lift2 f); closed (err B) (lift2 g)\<rbrakk> \<Longrightarrow> closed (err (A \<times> B)) (lift2 (Product.sup f g))
[PROOF STEP]
apply (unfold closed_def plussub_def lift2_def err_def' sup_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>insert Err {x. \<exists>y\<in>A. x = OK y}. \<forall>y\<in>insert Err {x. \<exists>y\<in>A. x = OK y}. (case x of Err \<Rightarrow> Err | OK x \<Rightarrow> case y of Err \<Rightarrow> Err | OK xa \<Rightarrow> f x xa) \<in> insert Err {x. \<exists>y\<in>A. x = OK y}; \<forall>x\<in>insert Err {x. \<exists>y\<in>B. x = OK y}. \<forall>y\<in>insert Err {x. \<exists>y\<in>B. x = OK y}. (case x of Err \<Rightarrow> Err | OK x \<Rightarrow> case y of Err \<Rightarrow> Err | OK xa \<Rightarrow> g x xa) \<in> insert Err {x. \<exists>y\<in>B. x = OK y}\<rbrakk> \<Longrightarrow> \<forall>x\<in>insert Err {x. \<exists>y\<in>A \<times> B. x = OK y}. \<forall>y\<in>insert Err {x. \<exists>y\<in>A \<times> B. x = OK y}. (case x of Err \<Rightarrow> Err | OK x \<Rightarrow> case y of Err \<Rightarrow> Err | OK xa \<Rightarrow> (case x of (a\<^sub>1, b\<^sub>1) \<Rightarrow> \<lambda>(a\<^sub>2, b\<^sub>2). Err.sup Pair (f a\<^sub>1 a\<^sub>2) (g b\<^sub>1 b\<^sub>2)) xa) \<in> insert Err {x. \<exists>y\<in>A \<times> B. x = OK y}
[PROOF STEP]
apply (simp split: err.split)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>y\<in>A. \<forall>ya\<in>A. f y ya = Err \<or> (\<exists>yb\<in>A. f y ya = OK yb); \<forall>y\<in>B. \<forall>ya\<in>B. g y ya = Err \<or> (\<exists>yb\<in>B. g y ya = OK yb)\<rbrakk> \<Longrightarrow> \<forall>a b. a \<in> A \<and> b \<in> B \<longrightarrow> (\<forall>aa ba. aa \<in> A \<and> ba \<in> B \<longrightarrow> f a aa = Err \<or> g b ba = Err \<or> (\<exists>x\<in>A. f a aa = OK x) \<and> (\<exists>y\<in>B. g b ba = OK y))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma unfold_plussub_lift2: "e\<^sub>1 \<squnion>\<^bsub>lift2 f\<^esub> e\<^sub>2 = lift2 f e\<^sub>1 e\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e\<^sub>1 \<squnion>\<^bsub>lift2 f\<^esub> e\<^sub>2 = lift2 f e\<^sub>1 e\<^sub>2
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e\<^sub>1 \<squnion>\<^bsub>lift2 f\<^esub> e\<^sub>2 = lift2 f e\<^sub>1 e\<^sub>2
[PROOF STEP]
by (simp add: plussub_def)


[STATEMENT]
lemma plus_eq_Err_conv [simp]:
  assumes "x\<in>A"  "y\<in>A"  "semilat(err A, Err.le r, lift2 f)"
  shows "(x \<squnion>\<^sub>f y = Err) = (\<not>(\<exists>z\<in>A. x \<sqsubseteq>\<^sub>r z \<and> y \<sqsubseteq>\<^sub>r z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<squnion>\<^bsub>f\<^esub> y = Err) = (\<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z))
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<squnion>\<^bsub>f\<^esub> y = Err) = (\<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x \<squnion>\<^bsub>f\<^esub> y = Err) = (\<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z))
[PROOF STEP]
have plus_le_conv2:
    "\<And>r f z. \<lbrakk> z \<in> err A; semilat (err A, r, f); OK x \<in> err A; OK y \<in> err A;
                 OK x \<squnion>\<^sub>f OK y \<sqsubseteq>\<^sub>r z\<rbrakk> \<Longrightarrow> OK x \<sqsubseteq>\<^sub>r z \<and> OK y \<sqsubseteq>\<^sub>r z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r f z. \<lbrakk>z \<in> err A; semilat (err A, r, f); OK x \<in> err A; OK y \<in> err A; OK x \<squnion>\<^bsub>f\<^esub> OK y \<sqsubseteq>\<^bsub>r\<^esub> z\<rbrakk> \<Longrightarrow> OK x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> OK y \<sqsubseteq>\<^bsub>r\<^esub> z
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r f z. \<lbrakk>z \<in> err A; semilat (err A, r, f); OK x \<in> err A; OK y \<in> err A; OK x \<squnion>\<^bsub>f\<^esub> OK y \<sqsubseteq>\<^bsub>r\<^esub> z\<rbrakk> \<Longrightarrow> OK x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> OK y \<sqsubseteq>\<^bsub>r\<^esub> z
[PROOF STEP]
by (rule Semilat.plus_le_conv [OF Semilat.intro, THEN iffD1])
[PROOF STATE]
proof (state)
this:
\<lbrakk>?z \<in> err A; semilat (err A, ?r, ?f); OK x \<in> err A; OK y \<in> err A; OK x \<squnion>\<^bsub>?f\<^esub> OK y \<sqsubseteq>\<^bsub>?r\<^esub> ?z\<rbrakk> \<Longrightarrow> OK x \<sqsubseteq>\<^bsub>?r\<^esub> ?z \<and> OK y \<sqsubseteq>\<^bsub>?r\<^esub> ?z

goal (1 subgoal):
 1. (x \<squnion>\<^bsub>f\<^esub> y = Err) = (\<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z))
[PROOF STEP]
(*>*)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?z \<in> err A; semilat (err A, ?r, ?f); OK x \<in> err A; OK y \<in> err A; OK x \<squnion>\<^bsub>?f\<^esub> OK y \<sqsubseteq>\<^bsub>?r\<^esub> ?z\<rbrakk> \<Longrightarrow> OK x \<sqsubseteq>\<^bsub>?r\<^esub> ?z \<and> OK y \<sqsubseteq>\<^bsub>?r\<^esub> ?z

goal (1 subgoal):
 1. (x \<squnion>\<^bsub>f\<^esub> y = Err) = (\<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x \<in> A
y \<in> A
semilat (err A, Err.le r, lift2 f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> A
y \<in> A
semilat (err A, Err.le r, lift2 f)

goal (1 subgoal):
 1. (x \<squnion>\<^bsub>f\<^esub> y = Err) = (\<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z))
[PROOF STEP]
apply (rule_tac iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); x \<squnion>\<^bsub>f\<^esub> y = Err\<rbrakk> \<Longrightarrow> \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z)
 2. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z)\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; x \<sqsubseteq>\<^bsub>r\<^esub> z; y \<sqsubseteq>\<^bsub>r\<^esub> z\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z)\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
[PROOF STEP]
apply (drule OK_le_err_OK [THEN iffD2])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; y \<sqsubseteq>\<^bsub>r\<^esub> z; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z)\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
[PROOF STEP]
apply (drule OK_le_err_OK [THEN iffD2])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z)\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
[PROOF STEP]
apply (drule Semilat.lub[OF Semilat.intro, of _ _ _ "OK x" _ "OK y"])
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> ?z13 z
 2. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> ?z13 z
 3. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> OK x \<in> err A
 4. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> OK y \<in> err A
 5. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> ?z13 z \<in> err A
 6. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK x \<squnion>\<^bsub>lift2 f\<^esub> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> ?z13 z\<rbrakk> \<Longrightarrow> False
 7. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z)\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z
 2. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> OK x \<in> err A
 3. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> OK y \<in> err A
 4. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> OK z \<in> err A
 5. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK x \<squnion>\<^bsub>lift2 f\<^esub> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> False
 6. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z)\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> OK x \<in> err A
 2. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> OK y \<in> err A
 3. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> OK z \<in> err A
 4. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK x \<squnion>\<^bsub>lift2 f\<^esub> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> False
 5. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z)\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> OK y \<in> err A
 2. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> OK z \<in> err A
 3. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK x \<squnion>\<^bsub>lift2 f\<^esub> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z)\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> OK z \<in> err A
 2. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK x \<squnion>\<^bsub>lift2 f\<^esub> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z)\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK x \<squnion>\<^bsub>lift2 f\<^esub> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z)\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z)\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
[PROOF STEP]
apply (case_tac "x \<squnion>\<^sub>f y")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = Err\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
 2. \<And>x2. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK x2\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK x2\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
[PROOF STEP]
apply (rename_tac "z")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
[PROOF STEP]
apply (subgoal_tac "OK z: err A")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
 2. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z\<rbrakk> \<Longrightarrow> OK z \<in> err A
[PROOF STEP]
apply (frule plus_le_conv2)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A\<rbrakk> \<Longrightarrow> semilat (err A, ?r22 z, ?f22 z)
 2. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A\<rbrakk> \<Longrightarrow> OK x \<in> err A
 3. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A\<rbrakk> \<Longrightarrow> OK y \<in> err A
 4. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A\<rbrakk> \<Longrightarrow> OK x \<squnion>\<^bsub>?f22 z\<^esub> OK y \<sqsubseteq>\<^bsub>?r22 z\<^esub> OK z
 5. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A; OK x \<sqsubseteq>\<^bsub>?r22 z\<^esub> OK z \<and> OK y \<sqsubseteq>\<^bsub>?r22 z\<^esub> OK z\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
 6. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z\<rbrakk> \<Longrightarrow> OK z \<in> err A
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A\<rbrakk> \<Longrightarrow> OK x \<in> err A
 2. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A\<rbrakk> \<Longrightarrow> OK y \<in> err A
 3. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A\<rbrakk> \<Longrightarrow> OK x \<squnion>\<^bsub>lift2 f\<^esub> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z
 4. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z \<and> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
 5. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z\<rbrakk> \<Longrightarrow> OK z \<in> err A
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A\<rbrakk> \<Longrightarrow> OK y \<in> err A
 2. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A\<rbrakk> \<Longrightarrow> OK x \<squnion>\<^bsub>lift2 f\<^esub> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z
 3. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z \<and> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
 4. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z\<rbrakk> \<Longrightarrow> OK z \<in> err A
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A\<rbrakk> \<Longrightarrow> OK x \<squnion>\<^bsub>lift2 f\<^esub> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z
 2. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z \<and> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
 3. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z\<rbrakk> \<Longrightarrow> OK z \<in> err A
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<forall>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<longrightarrow> \<not> y \<sqsubseteq>\<^bsub>r\<^esub> z; x \<squnion>\<^bsub>f\<^esub> y = OK z; z \<in> A\<rbrakk> \<Longrightarrow> z \<sqsubseteq>\<^bsub>r\<^esub> z
 2. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z \<and> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
 3. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z\<rbrakk> \<Longrightarrow> OK z \<in> err A
[PROOF STEP]
apply (blast dest: Semilat.orderI [OF Semilat.intro] order_refl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z \<and> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
 2. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z\<rbrakk> \<Longrightarrow> OK z \<in> err A
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z\<rbrakk> \<Longrightarrow> OK z \<in> err A
[PROOF STEP]
apply (erule subst)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z)\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y \<in> err A
[PROOF STEP]
apply (unfold semilat_def err_def' closed_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; case (insert Err {x. \<exists>y\<in>A. x = OK y}, Err.le r, lift2 f) of (A, r, f) \<Rightarrow> order r A \<and> (\<forall>x\<in>A. \<forall>y\<in>A. x \<squnion>\<^bsub>f\<^esub> y \<in> A) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> x \<squnion>\<^bsub>f\<^esub> y) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. y \<sqsubseteq>\<^bsub>r\<^esub> x \<squnion>\<^bsub>f\<^esub> y) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z \<longrightarrow> x \<squnion>\<^bsub>f\<^esub> y \<sqsubseteq>\<^bsub>r\<^esub> z); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z)\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y \<in> insert Err {x. \<exists>y\<in>A. x = OK y}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(x \<squnion>\<^bsub>f\<^esub> y = Err) = (\<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z))

goal:
No subgoals!
[PROOF STEP]
qed