[STATEMENT]
lemma d_cancellation_1: "d x \<le> d y + d x \<cdot> ad y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x \<le> d y + d x \<cdot> ad y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d x \<le> d y + d x \<cdot> ad y
[PROOF STEP]
have a: "d (d x \<cdot> ad y) = ad y \<cdot> d x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (d x \<cdot> ad y) = ad y \<cdot> d x
[PROOF STEP]
using local.a_closure' local.ads_d_def local.am2 local.ans_d_def
[PROOF STATE]
proof (prove)
using this:
ans_d (ad ?x) = ad ?x
d ?x = ad (ad ?x)
ad ?x \<cdot> ad ?y = ad ?y \<cdot> ad ?x
ans_d ?x = ad (ad ?x)

goal (1 subgoal):
 1. d (d x \<cdot> ad y) = ad y \<cdot> d x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d (d x \<cdot> ad y) = ad y \<cdot> d x

goal (1 subgoal):
 1. d x \<le> d y + d x \<cdot> ad y
[PROOF STEP]
hence "d x \<le> d (d x \<cdot> ad y) + d y"
[PROOF STATE]
proof (prove)
using this:
d (d x \<cdot> ad y) = ad y \<cdot> d x

goal (1 subgoal):
 1. d x \<le> d (d x \<cdot> ad y) + d y
[PROOF STEP]
using d_a_galois1 local.a_comm_var local.ads_d_def
[PROOF STATE]
proof (prove)
using this:
d (d x \<cdot> ad y) = ad y \<cdot> d x
(d ?x \<cdot> ad ?y \<le> d ?z) = (d ?x \<le> d ?z + d ?y)
ad ?x \<cdot> ad ?y \<le> ad ?y \<cdot> ad ?x
d ?x = ad (ad ?x)

goal (1 subgoal):
 1. d x \<le> d (d x \<cdot> ad y) + d y
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
d x \<le> d (d x \<cdot> ad y) + d y

goal (1 subgoal):
 1. d x \<le> d y + d x \<cdot> ad y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
d x \<le> d (d x \<cdot> ad y) + d y

goal (1 subgoal):
 1. d x \<le> d y + d x \<cdot> ad y
[PROOF STEP]
using a add_commute local.ads_d_def local.am2
[PROOF STATE]
proof (prove)
using this:
d x \<le> d (d x \<cdot> ad y) + d y
d (d x \<cdot> ad y) = ad y \<cdot> d x
?a + ?b = ?b + ?a
d ?x = ad (ad ?x)
ad ?x \<cdot> ad ?y = ad ?y \<cdot> ad ?x

goal (1 subgoal):
 1. d x \<le> d y + d x \<cdot> ad y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d x \<le> d y + d x \<cdot> ad y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma d_cancellation_2: "(d z + d y) \<cdot> ad y \<le> d z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d z + d y) \<cdot> ad y \<le> d z
[PROOF STEP]
by (simp add: da_shunt1)


[STATEMENT]
lemma a_de_morgan: "ad (ad x \<cdot> ad y) = d (x + y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (ad x \<cdot> ad y) = d (x + y)
[PROOF STEP]
by (simp add: local.ads_d_def)


[STATEMENT]
lemma a_de_morgan_var_3: "ad (d x + d y) = ad x \<cdot> ad y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (d x + d y) = ad x \<cdot> ad y
[PROOF STEP]
using local.a_add_idem local.ads_d_def am_add_op_def
[PROOF STATE]
proof (prove)
using this:
ad ?x \<oplus> ad ?x = ad ?x
d ?x = ad (ad ?x)
?x \<oplus> ?y \<equiv> ad (ad ?x \<cdot> ad ?y)

goal (1 subgoal):
 1. ad (d x + d y) = ad x \<cdot> ad y
[PROOF STEP]
by auto


[STATEMENT]
lemma a_de_morgan_var_4: "ad (d x \<cdot> d y) = ad x + ad y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (d x \<cdot> d y) = ad x + ad y
[PROOF STEP]
using local.a_add_idem local.ads_d_def am_add_op_def
[PROOF STATE]
proof (prove)
using this:
ad ?x \<oplus> ad ?x = ad ?x
d ?x = ad (ad ?x)
?x \<oplus> ?y \<equiv> ad (ad ?x \<cdot> ad ?y)

goal (1 subgoal):
 1. ad (d x \<cdot> d y) = ad x + ad y
[PROOF STEP]
by auto


[STATEMENT]
lemma a_4: "ad x \<le> ad (x \<cdot> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<le> ad (x \<cdot> y)
[PROOF STEP]
using local.a_add_idem local.a_antitone' local.dpdz.domain_1'' am_add_op_def
[PROOF STATE]
proof (prove)
using this:
ad ?x \<oplus> ad ?x = ad ?x
?x \<le> ?y \<Longrightarrow> ad ?y \<le> ad ?x
ad (ad (?x \<cdot> ?y)) \<le> ad (ad ?x)
?x \<oplus> ?y \<equiv> ad (ad ?x \<cdot> ad ?y)

goal (1 subgoal):
 1. ad x \<le> ad (x \<cdot> y)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma a_6: "ad (d x \<cdot> y) = ad x + ad y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (d x \<cdot> y) = ad x + ad y
[PROOF STEP]
using a_de_morgan_var_4 local.ads_d_def
[PROOF STATE]
proof (prove)
using this:
ad (d ?x \<cdot> d ?y) = ad ?x + ad ?y
d ?x = ad (ad ?x)

goal (1 subgoal):
 1. ad (d x \<cdot> y) = ad x + ad y
[PROOF STEP]
by auto


[STATEMENT]
lemma a_7: "d x \<cdot> ad (d y + d z) = d x \<cdot> ad y \<cdot> ad z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x \<cdot> ad (d y + d z) = d x \<cdot> ad y \<cdot> ad z
[PROOF STEP]
using a_de_morgan_var_3 local.mult.semigroup_axioms semigroup.assoc
[PROOF STATE]
proof (prove)
using this:
ad (d ?x + d ?y) = ad ?x \<cdot> ad ?y
semigroup (\<cdot>)
semigroup ?f \<Longrightarrow> ?f (?f ?a ?b) ?c = ?f ?a (?f ?b ?c)

goal (1 subgoal):
 1. d x \<cdot> ad (d y + d z) = d x \<cdot> ad y \<cdot> ad z
[PROOF STEP]
by fastforce


[STATEMENT]
lemma a_d_add_closure [simp]: "d (ad x + ad y) = ad x + ad y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (ad x + ad y) = ad x + ad y
[PROOF STEP]
using local.a_add_idem local.ads_d_def am_add_op_def
[PROOF STATE]
proof (prove)
using this:
ad ?x \<oplus> ad ?x = ad ?x
d ?x = ad (ad ?x)
?x \<oplus> ?y \<equiv> ad (ad ?x \<cdot> ad ?y)

goal (1 subgoal):
 1. d (ad x + ad y) = ad x + ad y
[PROOF STEP]
by auto


[STATEMENT]
lemma d_6 [simp]: "d x + ad x \<cdot> d y = d x + d y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x + ad x \<cdot> d y = d x + d y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d x + ad x \<cdot> d y = d x + d y
[PROOF STEP]
have "ad (ad x \<cdot> (x + ad y)) = d (x + y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (ad x \<cdot> (x + ad y)) = d (x + y)
[PROOF STEP]
by (simp add: distrib_left ads_d_def)
[PROOF STATE]
proof (state)
this:
ad (ad x \<cdot> (x + ad y)) = d (x + y)

goal (1 subgoal):
 1. d x + ad x \<cdot> d y = d x + d y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ad (ad x \<cdot> (x + ad y)) = d (x + y)

goal (1 subgoal):
 1. d x + ad x \<cdot> d y = d x + d y
[PROOF STEP]
by (simp add: local.ads_d_def local.ans_d_def)
[PROOF STATE]
proof (state)
this:
d x + ad x \<cdot> d y = d x + d y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma d_7 [simp]: "ad x + d x \<cdot> ad y = ad x + ad y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x + d x \<cdot> ad y = ad x + ad y
[PROOF STEP]
by (metis a_d_add_closure local.ads_d_def local.ans4 local.s4)


[STATEMENT]
lemma a_mult_add: "ad x \<cdot> (y + x) = ad x \<cdot> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> (y + x) = ad x \<cdot> y
[PROOF STEP]
by (simp add: distrib_left)


[STATEMENT]
lemma kat_2: "y \<cdot> ad z \<le> ad x \<cdot> y \<Longrightarrow> d x \<cdot> y \<cdot> ad z = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<cdot> ad z \<le> ad x \<cdot> y \<Longrightarrow> d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<cdot> ad z \<le> ad x \<cdot> y \<Longrightarrow> d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a)
[PROOF STEP]
assume a: "y \<cdot> ad z \<le> ad x \<cdot> y"
[PROOF STATE]
proof (state)
this:
y \<cdot> ad z \<le> ad x \<cdot> y

goal (1 subgoal):
 1. y \<cdot> ad z \<le> ad x \<cdot> y \<Longrightarrow> d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a)
[PROOF STEP]
hence "d x \<cdot> y \<cdot> ad z \<le> d x \<cdot> ad x \<cdot> y"
[PROOF STATE]
proof (prove)
using this:
y \<cdot> ad z \<le> ad x \<cdot> y

goal (1 subgoal):
 1. d x \<cdot> y \<cdot> ad z \<le> d x \<cdot> ad x \<cdot> y
[PROOF STEP]
using local.mult_isol mult_assoc
[PROOF STATE]
proof (prove)
using this:
y \<cdot> ad z \<le> ad x \<cdot> y
?x \<le> ?y \<Longrightarrow> ?z \<cdot> ?x \<le> ?z \<cdot> ?y
?a \<cdot> ?b \<cdot> ?c = ?a \<cdot> (?b \<cdot> ?c)

goal (1 subgoal):
 1. d x \<cdot> y \<cdot> ad z \<le> d x \<cdot> ad x \<cdot> y
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
d x \<cdot> y \<cdot> ad z \<le> d x \<cdot> ad x \<cdot> y

goal (1 subgoal):
 1. y \<cdot> ad z \<le> ad x \<cdot> y \<Longrightarrow> d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
d x \<cdot> y \<cdot> ad z \<le> d x \<cdot> ad x \<cdot> y

goal (1 subgoal):
 1. d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a)
[PROOF STEP]
using local.join.le_bot ads_d_def
[PROOF STATE]
proof (prove)
using this:
d x \<cdot> y \<cdot> ad z \<le> d x \<cdot> ad x \<cdot> y
?a \<le> (zero_class.zero::'a) \<Longrightarrow> ?a = (zero_class.zero::'a)
d ?x = ad (ad ?x)

goal (1 subgoal):
 1. d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma kat_3: "d x \<cdot> y \<cdot> ad z = 0 \<Longrightarrow> d x \<cdot> y = d x \<cdot> y \<cdot> d z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a) \<Longrightarrow> d x \<cdot> y = d x \<cdot> y \<cdot> d z
[PROOF STEP]
using local.a_zero_def local.ads_d_def local.am_d_def local.kat_3'
[PROOF STATE]
proof (prove)
using this:
a_zero = ad (1::'a)
d ?x = ad (ad ?x)
am_d ?x = ad (ad ?x)
am_d ?x \<cdot> ?y \<cdot> ad ?z = a_zero \<Longrightarrow> am_d ?x \<cdot> ?y = am_d ?x \<cdot> ?y \<cdot> am_d ?z

goal (1 subgoal):
 1. d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a) \<Longrightarrow> d x \<cdot> y = d x \<cdot> y \<cdot> d z
[PROOF STEP]
by auto


[STATEMENT]
lemma kat_4: "d x \<cdot> y = d x \<cdot> y \<cdot> d z \<Longrightarrow> d x \<cdot> y \<le> y \<cdot> d z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x \<cdot> y = d x \<cdot> y \<cdot> d z \<Longrightarrow> d x \<cdot> y \<le> y \<cdot> d z
[PROOF STEP]
using a_subid_aux1 mult_assoc ads_d_def
[PROOF STATE]
proof (prove)
using this:
ad ?x \<cdot> ?y \<le> ?y
?a \<cdot> ?b \<cdot> ?c = ?a \<cdot> (?b \<cdot> ?c)
d ?x = ad (ad ?x)

goal (1 subgoal):
 1. d x \<cdot> y = d x \<cdot> y \<cdot> d z \<Longrightarrow> d x \<cdot> y \<le> y \<cdot> d z
[PROOF STEP]
by auto


[STATEMENT]
lemma kat_2_equiv: "y \<cdot> ad z \<le> ad x \<cdot> y \<longleftrightarrow> d x \<cdot> y \<cdot> ad z = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y \<cdot> ad z \<le> ad x \<cdot> y) = (d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y \<cdot> ad z \<le> ad x \<cdot> y \<Longrightarrow> d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a)
 2. d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a) \<Longrightarrow> y \<cdot> ad z \<le> ad x \<cdot> y
[PROOF STEP]
assume "y \<cdot> ad z \<le> ad x \<cdot> y"
[PROOF STATE]
proof (state)
this:
y \<cdot> ad z \<le> ad x \<cdot> y

goal (2 subgoals):
 1. y \<cdot> ad z \<le> ad x \<cdot> y \<Longrightarrow> d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a)
 2. d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a) \<Longrightarrow> y \<cdot> ad z \<le> ad x \<cdot> y
[PROOF STEP]
thus "d x \<cdot> y \<cdot> ad z = 0"
[PROOF STATE]
proof (prove)
using this:
y \<cdot> ad z \<le> ad x \<cdot> y

goal (1 subgoal):
 1. d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a)
[PROOF STEP]
by (simp add: kat_2)
[PROOF STATE]
proof (state)
this:
d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a)

goal (1 subgoal):
 1. d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a) \<Longrightarrow> y \<cdot> ad z \<le> ad x \<cdot> y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a) \<Longrightarrow> y \<cdot> ad z \<le> ad x \<cdot> y
[PROOF STEP]
assume 1: "d x \<cdot> y \<cdot> ad z = 0"
[PROOF STATE]
proof (state)
this:
d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a)

goal (1 subgoal):
 1. d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a) \<Longrightarrow> y \<cdot> ad z \<le> ad x \<cdot> y
[PROOF STEP]
have "y \<cdot> ad z = (d x + ad x) \<cdot> y \<cdot> ad z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<cdot> ad z = (d x + ad x) \<cdot> y \<cdot> ad z
[PROOF STEP]
by (simp add: local.ads_d_def)
[PROOF STATE]
proof (state)
this:
y \<cdot> ad z = (d x + ad x) \<cdot> y \<cdot> ad z

goal (1 subgoal):
 1. d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a) \<Longrightarrow> y \<cdot> ad z \<le> ad x \<cdot> y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
y \<cdot> ad z = (d x + ad x) \<cdot> y \<cdot> ad z

goal (1 subgoal):
 1. d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a) \<Longrightarrow> y \<cdot> ad z \<le> ad x \<cdot> y
[PROOF STEP]
have "... = d x \<cdot> y \<cdot> ad z + ad x \<cdot> y \<cdot> ad z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d x + ad x) \<cdot> y \<cdot> ad z = d x \<cdot> y \<cdot> ad z + ad x \<cdot> y \<cdot> ad z
[PROOF STEP]
using local.distrib_right
[PROOF STATE]
proof (prove)
using this:
(?a + ?b) \<cdot> ?c = ?a \<cdot> ?c + ?b \<cdot> ?c

goal (1 subgoal):
 1. (d x + ad x) \<cdot> y \<cdot> ad z = d x \<cdot> y \<cdot> ad z + ad x \<cdot> y \<cdot> ad z
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
(d x + ad x) \<cdot> y \<cdot> ad z = d x \<cdot> y \<cdot> ad z + ad x \<cdot> y \<cdot> ad z

goal (1 subgoal):
 1. d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a) \<Longrightarrow> y \<cdot> ad z \<le> ad x \<cdot> y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(d x + ad x) \<cdot> y \<cdot> ad z = d x \<cdot> y \<cdot> ad z + ad x \<cdot> y \<cdot> ad z

goal (1 subgoal):
 1. d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a) \<Longrightarrow> y \<cdot> ad z \<le> ad x \<cdot> y
[PROOF STEP]
have "... = ad x \<cdot> y \<cdot> ad z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x \<cdot> y \<cdot> ad z + ad x \<cdot> y \<cdot> ad z = ad x \<cdot> y \<cdot> ad z
[PROOF STEP]
using "1"
[PROOF STATE]
proof (prove)
using this:
d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a)

goal (1 subgoal):
 1. d x \<cdot> y \<cdot> ad z + ad x \<cdot> y \<cdot> ad z = ad x \<cdot> y \<cdot> ad z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d x \<cdot> y \<cdot> ad z + ad x \<cdot> y \<cdot> ad z = ad x \<cdot> y \<cdot> ad z

goal (1 subgoal):
 1. d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a) \<Longrightarrow> y \<cdot> ad z \<le> ad x \<cdot> y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d x \<cdot> y \<cdot> ad z + ad x \<cdot> y \<cdot> ad z = ad x \<cdot> y \<cdot> ad z

goal (1 subgoal):
 1. d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a) \<Longrightarrow> y \<cdot> ad z \<le> ad x \<cdot> y
[PROOF STEP]
have "... \<le> ad x \<cdot> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> y \<cdot> ad z \<le> ad x \<cdot> y
[PROOF STEP]
by (simp add: local.a_subid_aux2)
[PROOF STATE]
proof (state)
this:
ad x \<cdot> y \<cdot> ad z \<le> ad x \<cdot> y

goal (1 subgoal):
 1. d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a) \<Longrightarrow> y \<cdot> ad z \<le> ad x \<cdot> y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
y \<cdot> ad z \<le> ad x \<cdot> y
[PROOF STEP]
show "y \<cdot> ad z \<le> ad x \<cdot> y"
[PROOF STATE]
proof (prove)
using this:
y \<cdot> ad z \<le> ad x \<cdot> y

goal (1 subgoal):
 1. y \<cdot> ad z \<le> ad x \<cdot> y
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
y \<cdot> ad z \<le> ad x \<cdot> y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma kat_4_equiv: "d x \<cdot> y = d x \<cdot> y \<cdot> d z \<longleftrightarrow> d x \<cdot> y \<le> y \<cdot> d z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d x \<cdot> y = d x \<cdot> y \<cdot> d z) = (d x \<cdot> y \<le> y \<cdot> d z)
[PROOF STEP]
using local.ads_d_def local.dpdz.d_preserves_equation
[PROOF STATE]
proof (prove)
using this:
d ?x = ad (ad ?x)
(ad (ad ?y) \<cdot> ?x \<le> ?x \<cdot> ad (ad ?z)) = (ad (ad ?y) \<cdot> ?x = ad (ad ?y) \<cdot> ?x \<cdot> ad (ad ?z))

goal (1 subgoal):
 1. (d x \<cdot> y = d x \<cdot> y \<cdot> d z) = (d x \<cdot> y \<le> y \<cdot> d z)
[PROOF STEP]
by auto


[STATEMENT]
lemma kat_3_equiv_opp: "ad z \<cdot> y \<cdot> d x = 0 \<longleftrightarrow> y \<cdot> d x = d z \<cdot> y \<cdot> d x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ad z \<cdot> y \<cdot> d x = (zero_class.zero::'a)) = (y \<cdot> d x = d z \<cdot> y \<cdot> d x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (ad z \<cdot> y \<cdot> d x = (zero_class.zero::'a)) = (y \<cdot> d x = d z \<cdot> y \<cdot> d x)
[PROOF STEP]
have "ad z \<cdot> (y \<cdot> d x) = 0 \<longrightarrow> (ad z \<cdot> y \<cdot> d x = 0) = (y \<cdot> d x = d z \<cdot> y \<cdot> d x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad z \<cdot> (y \<cdot> d x) = (zero_class.zero::'a) \<longrightarrow> (ad z \<cdot> y \<cdot> d x = (zero_class.zero::'a)) = (y \<cdot> d x = d z \<cdot> y \<cdot> d x)
[PROOF STEP]
by (metis (no_types, opaque_lifting) add_commute local.add_zerol local.ads_d_def local.as3 local.distrib_right' local.mult_1_left mult_assoc)
[PROOF STATE]
proof (state)
this:
ad z \<cdot> (y \<cdot> d x) = (zero_class.zero::'a) \<longrightarrow> (ad z \<cdot> y \<cdot> d x = (zero_class.zero::'a)) = (y \<cdot> d x = d z \<cdot> y \<cdot> d x)

goal (1 subgoal):
 1. (ad z \<cdot> y \<cdot> d x = (zero_class.zero::'a)) = (y \<cdot> d x = d z \<cdot> y \<cdot> d x)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ad z \<cdot> (y \<cdot> d x) = (zero_class.zero::'a) \<longrightarrow> (ad z \<cdot> y \<cdot> d x = (zero_class.zero::'a)) = (y \<cdot> d x = d z \<cdot> y \<cdot> d x)

goal (1 subgoal):
 1. (ad z \<cdot> y \<cdot> d x = (zero_class.zero::'a)) = (y \<cdot> d x = d z \<cdot> y \<cdot> d x)
[PROOF STEP]
by (metis a_4 local.a_add_idem local.a_gla2 local.ads_d_def mult_assoc am_add_op_def)
[PROOF STATE]
proof (state)
this:
(ad z \<cdot> y \<cdot> d x = (zero_class.zero::'a)) = (y \<cdot> d x = d z \<cdot> y \<cdot> d x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma kat_4_equiv_opp: "y \<cdot> d x = d z \<cdot> y \<cdot> d x \<longleftrightarrow> y \<cdot> d x \<le> d z \<cdot> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y \<cdot> d x = d z \<cdot> y \<cdot> d x) = (y \<cdot> d x \<le> d z \<cdot> y)
[PROOF STEP]
using kat_2_equiv kat_3_equiv_opp local.ads_d_def
[PROOF STATE]
proof (prove)
using this:
(?y \<cdot> ad ?z \<le> ad ?x \<cdot> ?y) = (d ?x \<cdot> ?y \<cdot> ad ?z = (zero_class.zero::'a))
(ad ?z \<cdot> ?y \<cdot> d ?x = (zero_class.zero::'a)) = (?y \<cdot> d ?x = d ?z \<cdot> ?y \<cdot> d ?x)
d ?x = ad (ad ?x)

goal (1 subgoal):
 1. (y \<cdot> d x = d z \<cdot> y \<cdot> d x) = (y \<cdot> d x \<le> d z \<cdot> y)
[PROOF STEP]
by auto


[STATEMENT]
lemma fdemodalisation22: "|x\<rangle> y \<le> d z \<longleftrightarrow> ad z \<cdot> x \<cdot> d y = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ( |x\<rangle> y \<le> d z) = (ad z \<cdot> x \<cdot> d y = (zero_class.zero::'a))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ( |x\<rangle> y \<le> d z) = (ad z \<cdot> x \<cdot> d y = (zero_class.zero::'a))
[PROOF STEP]
have "|x\<rangle> y \<le> d z \<longleftrightarrow> d (x \<cdot> y) \<le> d z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ( |x\<rangle> y \<le> d z) = (d (x \<cdot> y) \<le> d z)
[PROOF STEP]
by (simp add: fdia_def ads_d_def)
[PROOF STATE]
proof (state)
this:
( |x\<rangle> y \<le> d z) = (d (x \<cdot> y) \<le> d z)

goal (1 subgoal):
 1. ( |x\<rangle> y \<le> d z) = (ad z \<cdot> x \<cdot> d y = (zero_class.zero::'a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
( |x\<rangle> y \<le> d z) = (d (x \<cdot> y) \<le> d z)

goal (1 subgoal):
 1. ( |x\<rangle> y \<le> d z) = (ad z \<cdot> x \<cdot> d y = (zero_class.zero::'a))
[PROOF STEP]
have "... \<longleftrightarrow> ad z \<cdot> d (x \<cdot> y) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d (x \<cdot> y) \<le> d z) = (ad z \<cdot> d (x \<cdot> y) = (zero_class.zero::'a))
[PROOF STEP]
by (metis add_commute local.a_gla local.ads_d_def local.ans4)
[PROOF STATE]
proof (state)
this:
(d (x \<cdot> y) \<le> d z) = (ad z \<cdot> d (x \<cdot> y) = (zero_class.zero::'a))

goal (1 subgoal):
 1. ( |x\<rangle> y \<le> d z) = (ad z \<cdot> x \<cdot> d y = (zero_class.zero::'a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(d (x \<cdot> y) \<le> d z) = (ad z \<cdot> d (x \<cdot> y) = (zero_class.zero::'a))

goal (1 subgoal):
 1. ( |x\<rangle> y \<le> d z) = (ad z \<cdot> x \<cdot> d y = (zero_class.zero::'a))
[PROOF STEP]
have "... \<longleftrightarrow> ad z \<cdot> x \<cdot> y = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ad z \<cdot> d (x \<cdot> y) = (zero_class.zero::'a)) = (ad z \<cdot> x \<cdot> y = (zero_class.zero::'a))
[PROOF STEP]
using dpdz.dom_weakly_local mult_assoc ads_d_def
[PROOF STATE]
proof (prove)
using this:
(?x \<cdot> ?y = (zero_class.zero::'a)) = (?x \<cdot> ad (ad ?y) = (zero_class.zero::'a))
?a \<cdot> ?b \<cdot> ?c = ?a \<cdot> (?b \<cdot> ?c)
d ?x = ad (ad ?x)

goal (1 subgoal):
 1. (ad z \<cdot> d (x \<cdot> y) = (zero_class.zero::'a)) = (ad z \<cdot> x \<cdot> y = (zero_class.zero::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(ad z \<cdot> d (x \<cdot> y) = (zero_class.zero::'a)) = (ad z \<cdot> x \<cdot> y = (zero_class.zero::'a))

goal (1 subgoal):
 1. ( |x\<rangle> y \<le> d z) = (ad z \<cdot> x \<cdot> d y = (zero_class.zero::'a))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
( |x\<rangle> y \<le> d z) = (ad z \<cdot> x \<cdot> y = (zero_class.zero::'a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
( |x\<rangle> y \<le> d z) = (ad z \<cdot> x \<cdot> y = (zero_class.zero::'a))

goal (1 subgoal):
 1. ( |x\<rangle> y \<le> d z) = (ad z \<cdot> x \<cdot> d y = (zero_class.zero::'a))
[PROOF STEP]
using dpdz.dom_weakly_local ads_d_def
[PROOF STATE]
proof (prove)
using this:
( |x\<rangle> y \<le> d z) = (ad z \<cdot> x \<cdot> y = (zero_class.zero::'a))
(?x \<cdot> ?y = (zero_class.zero::'a)) = (?x \<cdot> ad (ad ?y) = (zero_class.zero::'a))
d ?x = ad (ad ?x)

goal (1 subgoal):
 1. ( |x\<rangle> y \<le> d z) = (ad z \<cdot> x \<cdot> d y = (zero_class.zero::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
( |x\<rangle> y \<le> d z) = (ad z \<cdot> x \<cdot> d y = (zero_class.zero::'a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dia_diff_var: "|x\<rangle> y \<le> |x\<rangle> (d y \<cdot> ad z) + |x\<rangle> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |x\<rangle> y \<le>  |x\<rangle> (d y \<cdot> ad z) +  |x\<rangle> z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  |x\<rangle> y \<le>  |x\<rangle> (d y \<cdot> ad z) +  |x\<rangle> z
[PROOF STEP]
have 1: "|x\<rangle> (d y \<cdot> d z) \<le> |x\<rangle> (1 \<cdot> d z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |x\<rangle> (d y \<cdot> d z) \<le>  |x\<rangle> ((1::'a) \<cdot> d z)
[PROOF STEP]
using dpdz.dom_glb_eq ds.fd_subdist fdia_def ads_d_def
[PROOF STATE]
proof (prove)
using this:
(ad (ad ?x) \<le> ad (ad ?y) \<cdot> ad (ad ?z)) = (ad (ad ?x) \<le> ad (ad ?y) \<and> ad (ad ?x) \<le> ad (ad ?z))
 |?x\<rangle> (ad (ad ?y) \<cdot> ad (ad ?z)) \<le>  |?x\<rangle> ?y \<cdot>  |?x\<rangle> ?z
 |?x\<rangle> ?y = ad (ad (?x \<cdot> ?y))
d ?x = ad (ad ?x)

goal (1 subgoal):
 1.  |x\<rangle> (d y \<cdot> d z) \<le>  |x\<rangle> ((1::'a) \<cdot> d z)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
 |x\<rangle> (d y \<cdot> d z) \<le>  |x\<rangle> ((1::'a) \<cdot> d z)

goal (1 subgoal):
 1.  |x\<rangle> y \<le>  |x\<rangle> (d y \<cdot> ad z) +  |x\<rangle> z
[PROOF STEP]
have "|x\<rangle> y = |x\<rangle> (d y \<cdot> (ad z + d z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |x\<rangle> y =  |x\<rangle> (d y \<cdot> (ad z + d z))
[PROOF STEP]
by (metis as3 add_comm ds.fdia_d_simp mult_1_right ads_d_def)
[PROOF STATE]
proof (state)
this:
 |x\<rangle> y =  |x\<rangle> (d y \<cdot> (ad z + d z))

goal (1 subgoal):
 1.  |x\<rangle> y \<le>  |x\<rangle> (d y \<cdot> ad z) +  |x\<rangle> z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
 |x\<rangle> y =  |x\<rangle> (d y \<cdot> (ad z + d z))

goal (1 subgoal):
 1.  |x\<rangle> y \<le>  |x\<rangle> (d y \<cdot> ad z) +  |x\<rangle> z
[PROOF STEP]
have "... = |x\<rangle> (d y \<cdot> ad z) + |x\<rangle> (d y \<cdot> d z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |x\<rangle> (d y \<cdot> (ad z + d z)) =  |x\<rangle> (d y \<cdot> ad z) +  |x\<rangle> (d y \<cdot> d z)
[PROOF STEP]
by (simp add: local.distrib_left local.ds.fdia_add1)
[PROOF STATE]
proof (state)
this:
 |x\<rangle> (d y \<cdot> (ad z + d z)) =  |x\<rangle> (d y \<cdot> ad z) +  |x\<rangle> (d y \<cdot> d z)

goal (1 subgoal):
 1.  |x\<rangle> y \<le>  |x\<rangle> (d y \<cdot> ad z) +  |x\<rangle> z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
 |x\<rangle> (d y \<cdot> (ad z + d z)) =  |x\<rangle> (d y \<cdot> ad z) +  |x\<rangle> (d y \<cdot> d z)

goal (1 subgoal):
 1.  |x\<rangle> y \<le>  |x\<rangle> (d y \<cdot> ad z) +  |x\<rangle> z
[PROOF STEP]
have "... \<le> |x\<rangle> (d y \<cdot> ad z) + |x\<rangle> (1 \<cdot> d z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |x\<rangle> (d y \<cdot> ad z) +  |x\<rangle> (d y \<cdot> d z) \<le>  |x\<rangle> (d y \<cdot> ad z) +  |x\<rangle> ((1::'a) \<cdot> d z)
[PROOF STEP]
using "1" local.join.sup.mono
[PROOF STATE]
proof (prove)
using this:
 |x\<rangle> (d y \<cdot> d z) \<le>  |x\<rangle> ((1::'a) \<cdot> d z)
\<lbrakk>?c \<le> ?a; ?d \<le> ?b\<rbrakk> \<Longrightarrow> ?c + ?d \<le> ?a + ?b

goal (1 subgoal):
 1.  |x\<rangle> (d y \<cdot> ad z) +  |x\<rangle> (d y \<cdot> d z) \<le>  |x\<rangle> (d y \<cdot> ad z) +  |x\<rangle> ((1::'a) \<cdot> d z)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
 |x\<rangle> (d y \<cdot> ad z) +  |x\<rangle> (d y \<cdot> d z) \<le>  |x\<rangle> (d y \<cdot> ad z) +  |x\<rangle> ((1::'a) \<cdot> d z)

goal (1 subgoal):
 1.  |x\<rangle> y \<le>  |x\<rangle> (d y \<cdot> ad z) +  |x\<rangle> z
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
 |x\<rangle> y \<le>  |x\<rangle> (d y \<cdot> ad z) +  |x\<rangle> ((1::'a) \<cdot> d z)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
 |x\<rangle> y \<le>  |x\<rangle> (d y \<cdot> ad z) +  |x\<rangle> ((1::'a) \<cdot> d z)

goal (1 subgoal):
 1.  |x\<rangle> y \<le>  |x\<rangle> (d y \<cdot> ad z) +  |x\<rangle> z
[PROOF STEP]
by (simp add: fdia_def ads_d_def)
[PROOF STATE]
proof (state)
this:
 |x\<rangle> y \<le>  |x\<rangle> (d y \<cdot> ad z) +  |x\<rangle> z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dia_diff: "|x\<rangle> y \<cdot> ad ( |x\<rangle> z ) \<le> |x\<rangle> (d y \<cdot> ad z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |x\<rangle> y \<cdot> ad ( |x\<rangle> z) \<le>  |x\<rangle> (d y \<cdot> ad z)
[PROOF STEP]
using fdia_def dia_diff_var d_a_galois2 ads_d_def
[PROOF STATE]
proof (prove)
using this:
 |?x\<rangle> ?y = ad (ad (?x \<cdot> ?y))
 |?x\<rangle> ?y \<le>  |?x\<rangle> (d ?y \<cdot> ad ?z) +  |?x\<rangle> ?z
(d ?x \<cdot> d ?y \<le> d ?z) = (d ?x \<le> d ?z + ad ?y)
d ?x = ad (ad ?x)

goal (1 subgoal):
 1.  |x\<rangle> y \<cdot> ad ( |x\<rangle> z) \<le>  |x\<rangle> (d y \<cdot> ad z)
[PROOF STEP]
by metis


[STATEMENT]
lemma fdia_export_2: "ad y \<cdot> |x\<rangle> z = |ad y \<cdot> x\<rangle> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad y \<cdot>  |x\<rangle> z =  |ad y \<cdot> x\<rangle> z
[PROOF STEP]
using local.am_d_def local.d_a_export local.fdia_def mult_assoc
[PROOF STATE]
proof (prove)
using this:
am_d ?x = ad (ad ?x)
am_d (ad ?x \<cdot> ?y) = ad ?x \<cdot> am_d ?y
 |?x\<rangle> ?y = ad (ad (?x \<cdot> ?y))
?a \<cdot> ?b \<cdot> ?c = ?a \<cdot> (?b \<cdot> ?c)

goal (1 subgoal):
 1. ad y \<cdot>  |x\<rangle> z =  |ad y \<cdot> x\<rangle> z
[PROOF STEP]
by auto


[STATEMENT]
lemma fdia_split: "|x\<rangle> y = d z \<cdot> |x\<rangle> y + ad z \<cdot> |x\<rangle> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |x\<rangle> y = d z \<cdot>  |x\<rangle> y + ad z \<cdot>  |x\<rangle> y
[PROOF STEP]
by (metis mult_onel ans3 distrib_right ads_d_def)


[STATEMENT]
lemma fdia_fbox_de_morgan_2: "ad ( |x\<rangle> y) = |x] ad y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad ( |x\<rangle> y) =  |x] ad y
[PROOF STEP]
using fbox_def local.a_closure local.a_loc local.am_d_def local.fdia_def
[PROOF STATE]
proof (prove)
using this:
 |?x] ?y = ad (?x \<cdot> ad ?y)
am_d (ad ?x) = ad ?x
ad (?x \<cdot> am_d ?y) = ad (?x \<cdot> ?y)
am_d ?x = ad (ad ?x)
 |?x\<rangle> ?y = ad (ad (?x \<cdot> ?y))

goal (1 subgoal):
 1. ad ( |x\<rangle> y) =  |x] ad y
[PROOF STEP]
by auto


[STATEMENT]
lemma fbox_simp: "|x] y = |x] d y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |x] y =  |x] d y
[PROOF STEP]
using fbox_def local.a_add_idem local.ads_d_def am_add_op_def
[PROOF STATE]
proof (prove)
using this:
 |?x] ?y = ad (?x \<cdot> ad ?y)
ad ?x \<oplus> ad ?x = ad ?x
d ?x = ad (ad ?x)
?x \<oplus> ?y \<equiv> ad (ad ?x \<cdot> ad ?y)

goal (1 subgoal):
 1.  |x] y =  |x] d y
[PROOF STEP]
by auto


[STATEMENT]
lemma fbox_dom [simp]: "|x] 0 = ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |x] (zero_class.zero::'a) = ad x
[PROOF STEP]
by (simp add: fbox_def)


[STATEMENT]
lemma fbox_add1: "|x] (d y \<cdot> d z) = |x] y \<cdot> |x] z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |x] (d y \<cdot> d z) =  |x] y \<cdot>  |x] z
[PROOF STEP]
using a_de_morgan_var_4 fbox_def local.distrib_left
[PROOF STATE]
proof (prove)
using this:
ad (d ?x \<cdot> d ?y) = ad ?x + ad ?y
 |?x] ?y = ad (?x \<cdot> ad ?y)
?a \<cdot> (?b + ?c) = ?a \<cdot> ?b + ?a \<cdot> ?c

goal (1 subgoal):
 1.  |x] (d y \<cdot> d z) =  |x] y \<cdot>  |x] z
[PROOF STEP]
by auto


[STATEMENT]
lemma fbox_add2: "|x + y] z = |x] z \<cdot> |y] z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |x + y] z =  |x] z \<cdot>  |y] z
[PROOF STEP]
by (simp add: fbox_def)


[STATEMENT]
lemma fbox_mult: "|x \<cdot> y] z = |x] |y] z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |x \<cdot> y] z =  |x]  |y] z
[PROOF STEP]
using fbox_def local.a2_eq' local.apd_d_def mult_assoc
[PROOF STATE]
proof (prove)
using this:
 |?x] ?y = ad (?x \<cdot> ad ?y)
ad (?x \<cdot> apd_d ?y) = ad (?x \<cdot> ?y)
apd_d ?x = ad (ad ?x)
?a \<cdot> ?b \<cdot> ?c = ?a \<cdot> (?b \<cdot> ?c)

goal (1 subgoal):
 1.  |x \<cdot> y] z =  |x]  |y] z
[PROOF STEP]
by auto


[STATEMENT]
lemma fbox_zero [simp]: "|0] x = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |(zero_class.zero::'a)] x = (1::'a)
[PROOF STEP]
by (simp add: fbox_def)


[STATEMENT]
lemma fbox_one [simp]: "|1] x = d x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |(1::'a)] x = d x
[PROOF STEP]
by (simp add: fbox_def ads_d_def)


[STATEMENT]
lemma fbox_iso: "d x \<le> d y \<Longrightarrow> |z] x \<le> |z] y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x \<le> d y \<Longrightarrow>  |z] x \<le>  |z] y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d x \<le> d y \<Longrightarrow>  |z] x \<le>  |z] y
[PROOF STEP]
assume "d x \<le> d y"
[PROOF STATE]
proof (state)
this:
d x \<le> d y

goal (1 subgoal):
 1. d x \<le> d y \<Longrightarrow>  |z] x \<le>  |z] y
[PROOF STEP]
hence "ad y \<le> ad x"
[PROOF STATE]
proof (prove)
using this:
d x \<le> d y

goal (1 subgoal):
 1. ad y \<le> ad x
[PROOF STEP]
using local.a_add_idem local.a_antitone' local.ads_d_def am_add_op_def
[PROOF STATE]
proof (prove)
using this:
d x \<le> d y
ad ?x \<oplus> ad ?x = ad ?x
?x \<le> ?y \<Longrightarrow> ad ?y \<le> ad ?x
d ?x = ad (ad ?x)
?x \<oplus> ?y \<equiv> ad (ad ?x \<cdot> ad ?y)

goal (1 subgoal):
 1. ad y \<le> ad x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ad y \<le> ad x

goal (1 subgoal):
 1. d x \<le> d y \<Longrightarrow>  |z] x \<le>  |z] y
[PROOF STEP]
hence "z \<cdot> ad y \<le> z \<cdot> ad x"
[PROOF STATE]
proof (prove)
using this:
ad y \<le> ad x

goal (1 subgoal):
 1. z \<cdot> ad y \<le> z \<cdot> ad x
[PROOF STEP]
by (simp add: mult_isol)
[PROOF STATE]
proof (state)
this:
z \<cdot> ad y \<le> z \<cdot> ad x

goal (1 subgoal):
 1. d x \<le> d y \<Longrightarrow>  |z] x \<le>  |z] y
[PROOF STEP]
thus "|z] x \<le> |z] y"
[PROOF STATE]
proof (prove)
using this:
z \<cdot> ad y \<le> z \<cdot> ad x

goal (1 subgoal):
 1.  |z] x \<le>  |z] y
[PROOF STEP]
by (simp add: fbox_def a_antitone')
[PROOF STATE]
proof (state)
this:
 |z] x \<le>  |z] y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fbox_antitone_var: "x \<le> y \<Longrightarrow> |y] z \<le> |x] z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow>  |y] z \<le>  |x] z
[PROOF STEP]
by (simp add: fbox_def a_antitone mult_isor)


[STATEMENT]
lemma fbox_subdist_1: "|x] (d y \<cdot> d z) \<le> |x] y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |x] (d y \<cdot> d z) \<le>  |x] y
[PROOF STEP]
using a_de_morgan_var_4 fbox_def local.a_supdist_var local.distrib_left
[PROOF STATE]
proof (prove)
using this:
ad (d ?x \<cdot> d ?y) = ad ?x + ad ?y
 |?x] ?y = ad (?x \<cdot> ad ?y)
ad (?x + ?y) \<le> ad ?x
?a \<cdot> (?b + ?c) = ?a \<cdot> ?b + ?a \<cdot> ?c

goal (1 subgoal):
 1.  |x] (d y \<cdot> d z) \<le>  |x] y
[PROOF STEP]
by force


[STATEMENT]
lemma fbox_subdist_2: "|x] y \<le>|x] (d y + d z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |x] y \<le>  |x] (d y + d z)
[PROOF STEP]
by (simp add: fbox_iso ads_d_def)


[STATEMENT]
lemma fbox_diff_var: "|x] (d y + ad z) \<cdot> |x] z \<le> |x] y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |x] (d y + ad z) \<cdot>  |x] z \<le>  |x] y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  |x] (d y + ad z) \<cdot>  |x] z \<le>  |x] y
[PROOF STEP]
have "ad (ad y) \<cdot> ad (ad z) = ad (ad z + ad y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (ad y) \<cdot> ad (ad z) = ad (ad z + ad y)
[PROOF STEP]
using local.dpdz.dsg4
[PROOF STATE]
proof (prove)
using this:
ad (ad ?x) \<cdot> ad (ad ?y) = ad (ad ?y) \<cdot> ad (ad ?x)

goal (1 subgoal):
 1. ad (ad y) \<cdot> ad (ad z) = ad (ad z + ad y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ad (ad y) \<cdot> ad (ad z) = ad (ad z + ad y)

goal (1 subgoal):
 1.  |x] (d y + ad z) \<cdot>  |x] z \<le>  |x] y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ad (ad y) \<cdot> ad (ad z) = ad (ad z + ad y)
[PROOF STEP]
have "d (d (d y + ad z) \<cdot> d z) \<le> d y"
[PROOF STATE]
proof (prove)
using this:
ad (ad y) \<cdot> ad (ad z) = ad (ad z + ad y)

goal (1 subgoal):
 1. d (d (d y + ad z) \<cdot> d z) \<le> d y
[PROOF STEP]
by (simp add: local.a_subid_aux1' local.ads_d_def)
[PROOF STATE]
proof (state)
this:
d (d (d y + ad z) \<cdot> d z) \<le> d y

goal (1 subgoal):
 1.  |x] (d y + ad z) \<cdot>  |x] z \<le>  |x] y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
d (d (d y + ad z) \<cdot> d z) \<le> d y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
d (d (d y + ad z) \<cdot> d z) \<le> d y

goal (1 subgoal):
 1.  |x] (d y + ad z) \<cdot>  |x] z \<le>  |x] y
[PROOF STEP]
by (metis fbox_add1 fbox_iso)
[PROOF STATE]
proof (state)
this:
 |x] (d y + ad z) \<cdot>  |x] z \<le>  |x] y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fbox_diff: "|x] (d y + ad z) \<le> |x] y + ad ( |x] z )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |x] (d y + ad z) \<le>  |x] y + ad ( |x] z)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  |x] (d y + ad z) \<le>  |x] y + ad ( |x] z)
[PROOF STEP]
have f1: "\<And>a. ad (ad (ad (a::'a))) = ad a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. ad (ad (ad a)) = ad a
[PROOF STEP]
using local.a_closure' local.ans_d_def
[PROOF STATE]
proof (prove)
using this:
ans_d (ad ?x) = ad ?x
ans_d ?x = ad (ad ?x)

goal (1 subgoal):
 1. \<And>a. ad (ad (ad a)) = ad a
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
ad (ad (ad ?a1)) = ad ?a1

goal (1 subgoal):
 1.  |x] (d y + ad z) \<le>  |x] y + ad ( |x] z)
[PROOF STEP]
have f2: "\<And>a aa. ad (ad (a::'a)) + ad aa = ad (ad a \<cdot> aa)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa. ad (ad a) + ad aa = ad (ad a \<cdot> aa)
[PROOF STEP]
using local.ans_d_def
[PROOF STATE]
proof (prove)
using this:
ans_d ?x = ad (ad ?x)

goal (1 subgoal):
 1. \<And>a aa. ad (ad a) + ad aa = ad (ad a \<cdot> aa)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ad (ad ?a1) + ad ?aa1 = ad (ad ?a1 \<cdot> ?aa1)

goal (1 subgoal):
 1.  |x] (d y + ad z) \<le>  |x] y + ad ( |x] z)
[PROOF STEP]
have f3: "\<And>a aa. ad ((a::'a) + aa) = ad (aa + a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa. ad (a + aa) = ad (aa + a)
[PROOF STEP]
by (simp add: local.am2)
[PROOF STATE]
proof (state)
this:
ad (?a1 + ?aa1) = ad (?aa1 + ?a1)

goal (1 subgoal):
 1.  |x] (d y + ad z) \<le>  |x] y + ad ( |x] z)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ad (?a1 + ?aa1) = ad (?aa1 + ?a1)
[PROOF STEP]
have f4: "\<And>a aa. ad (ad (ad (a::'a) \<cdot> aa)) = ad (ad aa + a)"
[PROOF STATE]
proof (prove)
using this:
ad (?a1 + ?aa1) = ad (?aa1 + ?a1)

goal (1 subgoal):
 1. \<And>a aa. ad (ad (ad a \<cdot> aa)) = ad (ad aa + a)
[PROOF STEP]
using f2 f1
[PROOF STATE]
proof (prove)
using this:
ad (?a1 + ?aa1) = ad (?aa1 + ?a1)
ad (ad ?a1) + ad ?aa1 = ad (ad ?a1 \<cdot> ?aa1)
ad (ad (ad ?a1)) = ad ?a1

goal (1 subgoal):
 1. \<And>a aa. ad (ad (ad a \<cdot> aa)) = ad (ad aa + a)
[PROOF STEP]
by (metis (no_types) local.ans4)
[PROOF STATE]
proof (state)
this:
ad (ad (ad ?a1 \<cdot> ?aa1)) = ad (ad ?aa1 + ?a1)

goal (1 subgoal):
 1.  |x] (d y + ad z) \<le>  |x] y + ad ( |x] z)
[PROOF STEP]
have f5: "\<And>a aa ab. ad ((a::'a) \<cdot> (aa + ab)) = ad (a \<cdot> (ab + aa))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa ab. ad (a \<cdot> (aa + ab)) = ad (a \<cdot> (ab + aa))
[PROOF STEP]
using f3 local.distrib_left
[PROOF STATE]
proof (prove)
using this:
ad (?a1 + ?aa1) = ad (?aa1 + ?a1)
?a \<cdot> (?b + ?c) = ?a \<cdot> ?b + ?a \<cdot> ?c

goal (1 subgoal):
 1. \<And>a aa ab. ad (a \<cdot> (aa + ab)) = ad (a \<cdot> (ab + aa))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
ad (?a1 \<cdot> (?aa1 + ?ab1)) = ad (?a1 \<cdot> (?ab1 + ?aa1))

goal (1 subgoal):
 1.  |x] (d y + ad z) \<le>  |x] y + ad ( |x] z)
[PROOF STEP]
have f6: "\<And>a aa. ad (ad (ad (a::'a) + aa)) = ad (ad aa \<cdot> a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa. ad (ad (ad a + aa)) = ad (ad aa \<cdot> a)
[PROOF STEP]
using f3 f1
[PROOF STATE]
proof (prove)
using this:
ad (?a1 + ?aa1) = ad (?aa1 + ?a1)
ad (ad (ad ?a1)) = ad ?a1

goal (1 subgoal):
 1. \<And>a aa. ad (ad (ad a + aa)) = ad (ad aa \<cdot> a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ad (ad (ad ?a1 + ?aa1)) = ad (ad ?aa1 \<cdot> ?a1)

goal (1 subgoal):
 1.  |x] (d y + ad z) \<le>  |x] y + ad ( |x] z)
[PROOF STEP]
have "ad (x \<cdot> ad (y + ad z)) \<le> ad (ad (x \<cdot> ad z) \<cdot> (x \<cdot> ad y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (x \<cdot> ad (y + ad z)) \<le> ad (ad (x \<cdot> ad z) \<cdot> (x \<cdot> ad y))
[PROOF STEP]
using f5 f2 f1
[PROOF STATE]
proof (prove)
using this:
ad (?a1 \<cdot> (?aa1 + ?ab1)) = ad (?a1 \<cdot> (?ab1 + ?aa1))
ad (ad ?a1) + ad ?aa1 = ad (ad ?a1 \<cdot> ?aa1)
ad (ad (ad ?a1)) = ad ?a1

goal (1 subgoal):
 1. ad (x \<cdot> ad (y + ad z)) \<le> ad (ad (x \<cdot> ad z) \<cdot> (x \<cdot> ad y))
[PROOF STEP]
by (metis (no_types) a_mult_add fbox_def fbox_subdist_1 local.a_gla2 local.ads_d_def local.ans4 local.distrib_left local.gla_1 mult_assoc)
[PROOF STATE]
proof (state)
this:
ad (x \<cdot> ad (y + ad z)) \<le> ad (ad (x \<cdot> ad z) \<cdot> (x \<cdot> ad y))

goal (1 subgoal):
 1.  |x] (d y + ad z) \<le>  |x] y + ad ( |x] z)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ad (x \<cdot> ad (y + ad z)) \<le> ad (ad (x \<cdot> ad z) \<cdot> (x \<cdot> ad y))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ad (x \<cdot> ad (y + ad z)) \<le> ad (ad (x \<cdot> ad z) \<cdot> (x \<cdot> ad y))

goal (1 subgoal):
 1.  |x] (d y + ad z) \<le>  |x] y + ad ( |x] z)
[PROOF STEP]
using f6 f4 f3 f1
[PROOF STATE]
proof (prove)
using this:
ad (x \<cdot> ad (y + ad z)) \<le> ad (ad (x \<cdot> ad z) \<cdot> (x \<cdot> ad y))
ad (ad (ad ?a1 + ?aa1)) = ad (ad ?aa1 \<cdot> ?a1)
ad (ad (ad ?a1 \<cdot> ?aa1)) = ad (ad ?aa1 + ?a1)
ad (?a1 + ?aa1) = ad (?aa1 + ?a1)
ad (ad (ad ?a1)) = ad ?a1

goal (1 subgoal):
 1.  |x] (d y + ad z) \<le>  |x] y + ad ( |x] z)
[PROOF STEP]
by (simp add: fbox_def local.ads_d_def)
[PROOF STATE]
proof (state)
this:
 |x] (d y + ad z) \<le>  |x] y + ad ( |x] z)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma kat_1: "d x \<cdot> y \<le> y \<cdot> d z \<Longrightarrow> y \<cdot> ad z \<le> ad x \<cdot> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x \<cdot> y \<le> y \<cdot> d z \<Longrightarrow> y \<cdot> ad z \<le> ad x \<cdot> y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d x \<cdot> y \<le> y \<cdot> d z \<Longrightarrow> y \<cdot> ad z \<le> ad x \<cdot> y
[PROOF STEP]
assume a: "d x \<cdot> y \<le> y \<cdot> d z"
[PROOF STATE]
proof (state)
this:
d x \<cdot> y \<le> y \<cdot> d z

goal (1 subgoal):
 1. d x \<cdot> y \<le> y \<cdot> d z \<Longrightarrow> y \<cdot> ad z \<le> ad x \<cdot> y
[PROOF STEP]
have "y \<cdot> ad z = d x \<cdot> y \<cdot> ad z + ad x \<cdot> y \<cdot> ad z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<cdot> ad z = d x \<cdot> y \<cdot> ad z + ad x \<cdot> y \<cdot> ad z
[PROOF STEP]
by (metis local.ads_d_def local.as3 local.distrib_right local.mult_1_left)
[PROOF STATE]
proof (state)
this:
y \<cdot> ad z = d x \<cdot> y \<cdot> ad z + ad x \<cdot> y \<cdot> ad z

goal (1 subgoal):
 1. d x \<cdot> y \<le> y \<cdot> d z \<Longrightarrow> y \<cdot> ad z \<le> ad x \<cdot> y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
y \<cdot> ad z = d x \<cdot> y \<cdot> ad z + ad x \<cdot> y \<cdot> ad z

goal (1 subgoal):
 1. d x \<cdot> y \<le> y \<cdot> d z \<Longrightarrow> y \<cdot> ad z \<le> ad x \<cdot> y
[PROOF STEP]
have "... \<le> y \<cdot> (d z \<cdot> ad z) + ad x \<cdot> y \<cdot> ad z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x \<cdot> y \<cdot> ad z + ad x \<cdot> y \<cdot> ad z \<le> y \<cdot> (d z \<cdot> ad z) + ad x \<cdot> y \<cdot> ad z
[PROOF STEP]
by (metis a add_iso mult_isor mult_assoc)
[PROOF STATE]
proof (state)
this:
d x \<cdot> y \<cdot> ad z + ad x \<cdot> y \<cdot> ad z \<le> y \<cdot> (d z \<cdot> ad z) + ad x \<cdot> y \<cdot> ad z

goal (1 subgoal):
 1. d x \<cdot> y \<le> y \<cdot> d z \<Longrightarrow> y \<cdot> ad z \<le> ad x \<cdot> y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d x \<cdot> y \<cdot> ad z + ad x \<cdot> y \<cdot> ad z \<le> y \<cdot> (d z \<cdot> ad z) + ad x \<cdot> y \<cdot> ad z

goal (1 subgoal):
 1. d x \<cdot> y \<le> y \<cdot> d z \<Longrightarrow> y \<cdot> ad z \<le> ad x \<cdot> y
[PROOF STEP]
have "... = ad x \<cdot> y \<cdot> ad z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<cdot> (d z \<cdot> ad z) + ad x \<cdot> y \<cdot> ad z = ad x \<cdot> y \<cdot> ad z
[PROOF STEP]
by (simp add: ads_d_def)
[PROOF STATE]
proof (state)
this:
y \<cdot> (d z \<cdot> ad z) + ad x \<cdot> y \<cdot> ad z = ad x \<cdot> y \<cdot> ad z

goal (1 subgoal):
 1. d x \<cdot> y \<le> y \<cdot> d z \<Longrightarrow> y \<cdot> ad z \<le> ad x \<cdot> y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
y \<cdot> ad z \<le> ad x \<cdot> y \<cdot> ad z
[PROOF STEP]
show "y \<cdot> ad z \<le> ad x \<cdot> y"
[PROOF STATE]
proof (prove)
using this:
y \<cdot> ad z \<le> ad x \<cdot> y \<cdot> ad z

goal (1 subgoal):
 1. y \<cdot> ad z \<le> ad x \<cdot> y
[PROOF STEP]
using local.a_subid_aux2 local.dual_order.trans
[PROOF STATE]
proof (prove)
using this:
y \<cdot> ad z \<le> ad x \<cdot> y \<cdot> ad z
?x \<cdot> ad ?y \<le> ?x
\<lbrakk>?b \<le> ?a; ?c \<le> ?b\<rbrakk> \<Longrightarrow> ?c \<le> ?a

goal (1 subgoal):
 1. y \<cdot> ad z \<le> ad x \<cdot> y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<cdot> ad z \<le> ad x \<cdot> y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma kat_1_equiv: "d x \<cdot> y \<le> y \<cdot> d z \<longleftrightarrow> y \<cdot> ad z \<le> ad x \<cdot> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d x \<cdot> y \<le> y \<cdot> d z) = (y \<cdot> ad z \<le> ad x \<cdot> y)
[PROOF STEP]
using kat_1 kat_2 kat_3 kat_4
[PROOF STATE]
proof (prove)
using this:
d ?x \<cdot> ?y \<le> ?y \<cdot> d ?z \<Longrightarrow> ?y \<cdot> ad ?z \<le> ad ?x \<cdot> ?y
?y \<cdot> ad ?z \<le> ad ?x \<cdot> ?y \<Longrightarrow> d ?x \<cdot> ?y \<cdot> ad ?z = (zero_class.zero::'a)
d ?x \<cdot> ?y \<cdot> ad ?z = (zero_class.zero::'a) \<Longrightarrow> d ?x \<cdot> ?y = d ?x \<cdot> ?y \<cdot> d ?z
d ?x \<cdot> ?y = d ?x \<cdot> ?y \<cdot> d ?z \<Longrightarrow> d ?x \<cdot> ?y \<le> ?y \<cdot> d ?z

goal (1 subgoal):
 1. (d x \<cdot> y \<le> y \<cdot> d z) = (y \<cdot> ad z \<le> ad x \<cdot> y)
[PROOF STEP]
by blast


[STATEMENT]
lemma kat_3_equiv': "d x \<cdot> y \<cdot> ad z = 0 \<longleftrightarrow> d x \<cdot> y = d x \<cdot> y \<cdot> d z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d x \<cdot> y \<cdot> ad z = (zero_class.zero::'a)) = (d x \<cdot> y = d x \<cdot> y \<cdot> d z)
[PROOF STEP]
by (simp add: kat_1_equiv local.kat_2_equiv local.kat_4_equiv)


[STATEMENT]
lemma kat_1_equiv_opp: "y \<cdot> d x \<le> d z \<cdot> y \<longleftrightarrow> ad z \<cdot> y \<le> y \<cdot> ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y \<cdot> d x \<le> d z \<cdot> y) = (ad z \<cdot> y \<le> y \<cdot> ad x)
[PROOF STEP]
by (metis kat_1_equiv local.a_closure' local.ads_d_def local.ans_d_def)


[STATEMENT]
lemma kat_2_equiv_opp: "ad z \<cdot> y \<le> y \<cdot> ad x \<longleftrightarrow> ad z \<cdot> y \<cdot> d x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ad z \<cdot> y \<le> y \<cdot> ad x) = (ad z \<cdot> y \<cdot> d x = (zero_class.zero::'a))
[PROOF STEP]
by (simp add: kat_1_equiv_opp local.kat_3_equiv_opp local.kat_4_equiv_opp)


[STATEMENT]
lemma fbox_one_1 [simp]: "|x] 1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |x] (1::'a) = (1::'a)
[PROOF STEP]
by (simp add: fbox_def)


[STATEMENT]
lemma fbox_demodalisation3: "d y \<le> |x] d z \<longleftrightarrow> d y \<cdot> x \<le> x \<cdot> d z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d y \<le>  |x] d z) = (d y \<cdot> x \<le> x \<cdot> d z)
[PROOF STEP]
by (simp add: fbox_def a_gla kat_2_equiv_opp mult_assoc ads_d_def)


[STATEMENT]
lemma fbox_star_unfold [simp]: "|1] z \<cdot> |x] |x\<^sup>\<star>] z = |x\<^sup>\<star>] z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |(1::'a)] z \<cdot>  |x]  |x\<^sup>\<star>] z =  |x\<^sup>\<star>] z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  |(1::'a)] z \<cdot>  |x]  |x\<^sup>\<star>] z =  |x\<^sup>\<star>] z
[PROOF STEP]
have "ad (ad z + x \<cdot> (x\<^sup>\<star> \<cdot> ad z)) = ad (x\<^sup>\<star> \<cdot> ad z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (ad z + x \<cdot> (x\<^sup>\<star> \<cdot> ad z)) = ad (x\<^sup>\<star> \<cdot> ad z)
[PROOF STEP]
using local.conway.dagger_unfoldl_distr mult_assoc
[PROOF STATE]
proof (prove)
using this:
?y + ?x \<cdot> ?x\<^sup>\<star> \<cdot> ?y = ?x\<^sup>\<star> \<cdot> ?y
?a \<cdot> ?b \<cdot> ?c = ?a \<cdot> (?b \<cdot> ?c)

goal (1 subgoal):
 1. ad (ad z + x \<cdot> (x\<^sup>\<star> \<cdot> ad z)) = ad (x\<^sup>\<star> \<cdot> ad z)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ad (ad z + x \<cdot> (x\<^sup>\<star> \<cdot> ad z)) = ad (x\<^sup>\<star> \<cdot> ad z)

goal (1 subgoal):
 1.  |(1::'a)] z \<cdot>  |x]  |x\<^sup>\<star>] z =  |x\<^sup>\<star>] z
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ad (ad z + x \<cdot> (x\<^sup>\<star> \<cdot> ad z)) = ad (x\<^sup>\<star> \<cdot> ad z)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ad (ad z + x \<cdot> (x\<^sup>\<star> \<cdot> ad z)) = ad (x\<^sup>\<star> \<cdot> ad z)

goal (1 subgoal):
 1.  |(1::'a)] z \<cdot>  |x]  |x\<^sup>\<star>] z =  |x\<^sup>\<star>] z
[PROOF STEP]
using local.a_closure' local.ans_d_def local.fbox_def local.fdia_def local.fdia_fbox_de_morgan_2
[PROOF STATE]
proof (prove)
using this:
ad (ad z + x \<cdot> (x\<^sup>\<star> \<cdot> ad z)) = ad (x\<^sup>\<star> \<cdot> ad z)
ans_d (ad ?x) = ad ?x
ans_d ?x = ad (ad ?x)
 |?x] ?y = ad (?x \<cdot> ad ?y)
 |?x\<rangle> ?y = ad (ad (?x \<cdot> ?y))
ad ( |?x\<rangle> ?y) =  |?x] ad ?y

goal (1 subgoal):
 1.  |(1::'a)] z \<cdot>  |x]  |x\<^sup>\<star>] z =  |x\<^sup>\<star>] z
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
 |(1::'a)] z \<cdot>  |x]  |x\<^sup>\<star>] z =  |x\<^sup>\<star>] z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fbox_star_unfold_var [simp]: "d z \<cdot> |x] |x\<^sup>\<star>] z = |x\<^sup>\<star>] z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d z \<cdot>  |x]  |x\<^sup>\<star>] z =  |x\<^sup>\<star>] z
[PROOF STEP]
using fbox_star_unfold
[PROOF STATE]
proof (prove)
using this:
 |(1::'a)] ?z \<cdot>  |?x]  |?x\<^sup>\<star>] ?z =  |?x\<^sup>\<star>] ?z

goal (1 subgoal):
 1. d z \<cdot>  |x]  |x\<^sup>\<star>] z =  |x\<^sup>\<star>] z
[PROOF STEP]
by auto


[STATEMENT]
lemma fbox_star_unfoldr [simp]: "|1] z \<cdot> |x\<^sup>\<star>] |x] z = |x\<^sup>\<star>] z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |(1::'a)] z \<cdot>  |x\<^sup>\<star>]  |x] z =  |x\<^sup>\<star>] z
[PROOF STEP]
by (metis fbox_star_unfold fbox_mult star_slide_var)


[STATEMENT]
lemma fbox_star_unfoldr_var [simp]: "d z \<cdot> |x\<^sup>\<star>] |x] z = |x\<^sup>\<star>] z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d z \<cdot>  |x\<^sup>\<star>]  |x] z =  |x\<^sup>\<star>] z
[PROOF STEP]
using fbox_star_unfoldr
[PROOF STATE]
proof (prove)
using this:
 |(1::'a)] ?z \<cdot>  |?x\<^sup>\<star>]  |?x] ?z =  |?x\<^sup>\<star>] ?z

goal (1 subgoal):
 1. d z \<cdot>  |x\<^sup>\<star>]  |x] z =  |x\<^sup>\<star>] z
[PROOF STEP]
by auto


[STATEMENT]
lemma fbox_star_induct_var: "d y \<le> |x] y \<Longrightarrow> d y \<le> |x\<^sup>\<star>] y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d y \<le>  |x] y \<Longrightarrow> d y \<le>  |x\<^sup>\<star>] y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d y \<le>  |x] y \<Longrightarrow> d y \<le>  |x\<^sup>\<star>] y
[PROOF STEP]
assume a1: "d y \<le> |x] y"
[PROOF STATE]
proof (state)
this:
d y \<le>  |x] y

goal (1 subgoal):
 1. d y \<le>  |x] y \<Longrightarrow> d y \<le>  |x\<^sup>\<star>] y
[PROOF STEP]
have "\<And>a. ad (ad (ad (a::'a))) = ad a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. ad (ad (ad a)) = ad a
[PROOF STEP]
using local.a_closure' local.ans_d_def
[PROOF STATE]
proof (prove)
using this:
ans_d (ad ?x) = ad ?x
ans_d ?x = ad (ad ?x)

goal (1 subgoal):
 1. \<And>a. ad (ad (ad a)) = ad a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ad (ad (ad ?a1)) = ad ?a1

goal (1 subgoal):
 1. d y \<le>  |x] y \<Longrightarrow> d y \<le>  |x\<^sup>\<star>] y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ad (ad (ad ?a1)) = ad ?a1
[PROOF STEP]
have "ad (ad (x\<^sup>\<star> \<cdot> ad y)) \<le> ad y"
[PROOF STATE]
proof (prove)
using this:
ad (ad (ad ?a1)) = ad ?a1

goal (1 subgoal):
 1. ad (ad (x\<^sup>\<star> \<cdot> ad y)) \<le> ad y
[PROOF STEP]
using a1
[PROOF STATE]
proof (prove)
using this:
ad (ad (ad ?a1)) = ad ?a1
d y \<le>  |x] y

goal (1 subgoal):
 1. ad (ad (x\<^sup>\<star> \<cdot> ad y)) \<le> ad y
[PROOF STEP]
by (metis dka.fdia_star_induct local.a_export' local.ads_d_def local.ans4 local.ans_d_def local.eq_refl local.fbox_def local.fdia_def local.meet_ord_def)
[PROOF STATE]
proof (state)
this:
ad (ad (x\<^sup>\<star> \<cdot> ad y)) \<le> ad y

goal (1 subgoal):
 1. d y \<le>  |x] y \<Longrightarrow> d y \<le>  |x\<^sup>\<star>] y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ad (ad (x\<^sup>\<star> \<cdot> ad y)) \<le> ad y
[PROOF STEP]
have "ad (ad y + ad (x\<^sup>\<star> \<cdot> ad y)) = zero_class.zero"
[PROOF STATE]
proof (prove)
using this:
ad (ad (x\<^sup>\<star> \<cdot> ad y)) \<le> ad y

goal (1 subgoal):
 1. ad (ad y + ad (x\<^sup>\<star> \<cdot> ad y)) = (zero_class.zero::'a)
[PROOF STEP]
by (metis (no_types) add_commute local.a_2_var local.ads_d_def local.ans4)
[PROOF STATE]
proof (state)
this:
ad (ad y + ad (x\<^sup>\<star> \<cdot> ad y)) = (zero_class.zero::'a)

goal (1 subgoal):
 1. d y \<le>  |x] y \<Longrightarrow> d y \<le>  |x\<^sup>\<star>] y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ad (ad y + ad (x\<^sup>\<star> \<cdot> ad y)) = (zero_class.zero::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ad (ad y + ad (x\<^sup>\<star> \<cdot> ad y)) = (zero_class.zero::'a)

goal (1 subgoal):
 1. d y \<le>  |x\<^sup>\<star>] y
[PROOF STEP]
using local.a_2_var local.ads_d_def local.fbox_def
[PROOF STATE]
proof (prove)
using this:
ad (ad y + ad (x\<^sup>\<star> \<cdot> ad y)) = (zero_class.zero::'a)
(ad ?x \<cdot> d ?y = (zero_class.zero::'a)) = (ad ?x \<le> ad ?y)
d ?x = ad (ad ?x)
 |?x] ?y = ad (?x \<cdot> ad ?y)

goal (1 subgoal):
 1. d y \<le>  |x\<^sup>\<star>] y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d y \<le>  |x\<^sup>\<star>] y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fbox_star_induct: "d y \<le> d z \<cdot> |x] y \<Longrightarrow> d y \<le> |x\<^sup>\<star>] z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d y \<le> d z \<cdot>  |x] y \<Longrightarrow> d y \<le>  |x\<^sup>\<star>] z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d y \<le> d z \<cdot>  |x] y \<Longrightarrow> d y \<le>  |x\<^sup>\<star>] z
[PROOF STEP]
assume a1: "d y \<le> d z \<cdot> |x] y"
[PROOF STATE]
proof (state)
this:
d y \<le> d z \<cdot>  |x] y

goal (1 subgoal):
 1. d y \<le> d z \<cdot>  |x] y \<Longrightarrow> d y \<le>  |x\<^sup>\<star>] z
[PROOF STEP]
hence a: "d y \<le> d z" and "d y \<le> |x] y"
[PROOF STATE]
proof (prove)
using this:
d y \<le> d z \<cdot>  |x] y

goal (1 subgoal):
 1. d y \<le> d z &&& d y \<le>  |x] y
[PROOF STEP]
apply (metis local.a_subid_aux2 local.dual_order.trans local.fbox_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d y \<le>  |x] y
[PROOF STEP]
using a1 dka.dom_subid_aux2 local.dual_order.trans
[PROOF STATE]
proof (prove)
using this:
d y \<le> d z \<cdot>  |x] y
d ?x \<cdot> ?y \<le> ?y
\<lbrakk>?b \<le> ?a; ?c \<le> ?b\<rbrakk> \<Longrightarrow> ?c \<le> ?a

goal (1 subgoal):
 1. d y \<le>  |x] y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
d y \<le> d z
d y \<le>  |x] y

goal (1 subgoal):
 1. d y \<le> d z \<cdot>  |x] y \<Longrightarrow> d y \<le>  |x\<^sup>\<star>] z
[PROOF STEP]
hence "d y \<le> |x\<^sup>\<star>] y"
[PROOF STATE]
proof (prove)
using this:
d y \<le> d z
d y \<le>  |x] y

goal (1 subgoal):
 1. d y \<le>  |x\<^sup>\<star>] y
[PROOF STEP]
using fbox_star_induct_var
[PROOF STATE]
proof (prove)
using this:
d y \<le> d z
d y \<le>  |x] y
d ?y \<le>  |?x] ?y \<Longrightarrow> d ?y \<le>  |?x\<^sup>\<star>] ?y

goal (1 subgoal):
 1. d y \<le>  |x\<^sup>\<star>] y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
d y \<le>  |x\<^sup>\<star>] y

goal (1 subgoal):
 1. d y \<le> d z \<cdot>  |x] y \<Longrightarrow> d y \<le>  |x\<^sup>\<star>] z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
d y \<le>  |x\<^sup>\<star>] y

goal (1 subgoal):
 1. d y \<le>  |x\<^sup>\<star>] z
[PROOF STEP]
using a local.fbox_iso local.order.trans
[PROOF STATE]
proof (prove)
using this:
d y \<le>  |x\<^sup>\<star>] y
d y \<le> d z
d ?x \<le> d ?y \<Longrightarrow>  |?z] ?x \<le>  |?z] ?y
\<lbrakk>?a \<le> ?b; ?b \<le> ?c\<rbrakk> \<Longrightarrow> ?a \<le> ?c

goal (1 subgoal):
 1. d y \<le>  |x\<^sup>\<star>] z
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
d y \<le>  |x\<^sup>\<star>] z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fbox_star_induct_eq: "d z \<cdot> |x] y = d y \<Longrightarrow> d y \<le> |x\<^sup>\<star>] z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d z \<cdot>  |x] y = d y \<Longrightarrow> d y \<le>  |x\<^sup>\<star>] z
[PROOF STEP]
by (simp add: fbox_star_induct)


[STATEMENT]
lemma fbox_export_1: "ad y + |x] y = |d y \<cdot> x] y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad y +  |x] y =  |d y \<cdot> x] y
[PROOF STEP]
by (simp add: local.a_6 local.fbox_def mult_assoc)


[STATEMENT]
lemma fbox_export_2: "d y + |x] y = |ad y \<cdot> x] y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d y +  |x] y =  |ad y \<cdot> x] y
[PROOF STEP]
by (simp add: local.ads_d_def local.ans_d_def local.fbox_def mult_assoc)


[STATEMENT]
lemma "d p \<le> |(d t \<cdot> x)\<^sup>\<star> \<cdot> ad t] (d q \<cdot> ad t) \<Longrightarrow> d p \<le> |d t \<cdot> x] d q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d p \<le>  |(d t \<cdot> x)\<^sup>\<star> \<cdot> ad t] (d q \<cdot> ad t) \<Longrightarrow> d p \<le>  |d t \<cdot> x] d q
[PROOF STEP]
(*nitpick [expect=genuine]*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d p \<le>  |(d t \<cdot> x)\<^sup>\<star> \<cdot> ad t] (d q \<cdot> ad t) \<Longrightarrow> d p \<le>  |d t \<cdot> x] d q
[PROOF STEP]
oops


[STATEMENT]
lemma minimal:
  assumes "x \<in> A" and "P x"
  shows "\<exists>y \<in> A. size y \<le> size x \<and> P y \<and> (\<forall>z \<in> A. size z < size y \<longrightarrow> \<not> P z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y\<in>A. size y \<le> size x \<and> P y \<and> (\<forall>z\<in>A. size z < size y \<longrightarrow> \<not> P z)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> A
P x

goal (1 subgoal):
 1. \<exists>y\<in>A. size y \<le> size x \<and> P y \<and> (\<forall>z\<in>A. size z < size y \<longrightarrow> \<not> P z)
[PROOF STEP]
proof (induction x taking: size rule: measure_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>y. size y < size x \<longrightarrow> y \<in> A \<longrightarrow> P y \<longrightarrow> (\<exists>ya\<in>A. size ya \<le> size y \<and> P ya \<and> (\<forall>z\<in>A. size z < size ya \<longrightarrow> \<not> P z)); x \<in> A; P x\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. size y \<le> size x \<and> P y \<and> (\<forall>z\<in>A. size z < size y \<longrightarrow> \<not> P z)
[PROOF STEP]
case (1 x)
[PROOF STATE]
proof (state)
this:
\<forall>y. size y < size x \<longrightarrow> y \<in> A \<longrightarrow> P y \<longrightarrow> (\<exists>ya\<in>A. size ya \<le> size y \<and> P ya \<and> (\<forall>z\<in>A. size z < size ya \<longrightarrow> \<not> P z))
x \<in> A
P x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>y. size y < size x \<longrightarrow> y \<in> A \<longrightarrow> P y \<longrightarrow> (\<exists>ya\<in>A. size ya \<le> size y \<and> P ya \<and> (\<forall>z\<in>A. size z < size ya \<longrightarrow> \<not> P z)); x \<in> A; P x\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. size y \<le> size x \<and> P y \<and> (\<forall>z\<in>A. size z < size y \<longrightarrow> \<not> P z)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>y. size y < size x \<longrightarrow> y \<in> A \<longrightarrow> P y \<longrightarrow> (\<exists>ya\<in>A. size ya \<le> size y \<and> P ya \<and> (\<forall>z\<in>A. size z < size ya \<longrightarrow> \<not> P z))
x \<in> A
P x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>y. size y < size x \<longrightarrow> y \<in> A \<longrightarrow> P y \<longrightarrow> (\<exists>ya\<in>A. size ya \<le> size y \<and> P ya \<and> (\<forall>z\<in>A. size z < size ya \<longrightarrow> \<not> P z))
x \<in> A
P x

goal (1 subgoal):
 1. \<exists>y\<in>A. size y \<le> size x \<and> P y \<and> (\<forall>z\<in>A. size z < size y \<longrightarrow> \<not> P z)
[PROOF STEP]
proof (cases "\<forall>y \<in> A. size y < size x \<longrightarrow> \<not> P y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<forall>y. size y < size x \<longrightarrow> y \<in> A \<longrightarrow> P y \<longrightarrow> (\<exists>ya\<in>A. size ya \<le> size y \<and> P ya \<and> (\<forall>z\<in>A. size z < size ya \<longrightarrow> \<not> P z)); x \<in> A; P x; \<forall>y\<in>A. size y < size x \<longrightarrow> \<not> P y\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. size y \<le> size x \<and> P y \<and> (\<forall>z\<in>A. size z < size y \<longrightarrow> \<not> P z)
 2. \<lbrakk>\<forall>y. size y < size x \<longrightarrow> y \<in> A \<longrightarrow> P y \<longrightarrow> (\<exists>ya\<in>A. size ya \<le> size y \<and> P ya \<and> (\<forall>z\<in>A. size z < size ya \<longrightarrow> \<not> P z)); x \<in> A; P x; \<not> (\<forall>y\<in>A. size y < size x \<longrightarrow> \<not> P y)\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. size y \<le> size x \<and> P y \<and> (\<forall>z\<in>A. size z < size y \<longrightarrow> \<not> P z)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>A. size y < size x \<longrightarrow> \<not> P y

goal (2 subgoals):
 1. \<lbrakk>\<forall>y. size y < size x \<longrightarrow> y \<in> A \<longrightarrow> P y \<longrightarrow> (\<exists>ya\<in>A. size ya \<le> size y \<and> P ya \<and> (\<forall>z\<in>A. size z < size ya \<longrightarrow> \<not> P z)); x \<in> A; P x; \<forall>y\<in>A. size y < size x \<longrightarrow> \<not> P y\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. size y \<le> size x \<and> P y \<and> (\<forall>z\<in>A. size z < size y \<longrightarrow> \<not> P z)
 2. \<lbrakk>\<forall>y. size y < size x \<longrightarrow> y \<in> A \<longrightarrow> P y \<longrightarrow> (\<exists>ya\<in>A. size ya \<le> size y \<and> P ya \<and> (\<forall>z\<in>A. size z < size ya \<longrightarrow> \<not> P z)); x \<in> A; P x; \<not> (\<forall>y\<in>A. size y < size x \<longrightarrow> \<not> P y)\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. size y \<le> size x \<and> P y \<and> (\<forall>z\<in>A. size z < size y \<longrightarrow> \<not> P z)
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
\<forall>y. size y < size x \<longrightarrow> y \<in> A \<longrightarrow> P y \<longrightarrow> (\<exists>ya\<in>A. size ya \<le> size y \<and> P ya \<and> (\<forall>z\<in>A. size z < size ya \<longrightarrow> \<not> P z))
x \<in> A
P x
\<forall>y\<in>A. size y < size x \<longrightarrow> \<not> P y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>y. size y < size x \<longrightarrow> y \<in> A \<longrightarrow> P y \<longrightarrow> (\<exists>ya\<in>A. size ya \<le> size y \<and> P ya \<and> (\<forall>z\<in>A. size z < size ya \<longrightarrow> \<not> P z))
x \<in> A
P x
\<forall>y\<in>A. size y < size x \<longrightarrow> \<not> P y

goal (1 subgoal):
 1. \<exists>y\<in>A. size y \<le> size x \<and> P y \<and> (\<forall>z\<in>A. size z < size y \<longrightarrow> \<not> P z)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>A. size y \<le> size x \<and> P y \<and> (\<forall>z\<in>A. size z < size y \<longrightarrow> \<not> P z)

goal (1 subgoal):
 1. \<lbrakk>\<forall>y. size y < size x \<longrightarrow> y \<in> A \<longrightarrow> P y \<longrightarrow> (\<exists>ya\<in>A. size ya \<le> size y \<and> P ya \<and> (\<forall>z\<in>A. size z < size ya \<longrightarrow> \<not> P z)); x \<in> A; P x; \<not> (\<forall>y\<in>A. size y < size x \<longrightarrow> \<not> P y)\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. size y \<le> size x \<and> P y \<and> (\<forall>z\<in>A. size z < size y \<longrightarrow> \<not> P z)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<forall>y. size y < size x \<longrightarrow> y \<in> A \<longrightarrow> P y \<longrightarrow> (\<exists>ya\<in>A. size ya \<le> size y \<and> P ya \<and> (\<forall>z\<in>A. size z < size ya \<longrightarrow> \<not> P z)); x \<in> A; P x; \<not> (\<forall>y\<in>A. size y < size x \<longrightarrow> \<not> P y)\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. size y \<le> size x \<and> P y \<and> (\<forall>z\<in>A. size z < size y \<longrightarrow> \<not> P z)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>y\<in>A. size y < size x \<longrightarrow> \<not> P y)

goal (1 subgoal):
 1. \<lbrakk>\<forall>y. size y < size x \<longrightarrow> y \<in> A \<longrightarrow> P y \<longrightarrow> (\<exists>ya\<in>A. size ya \<le> size y \<and> P ya \<and> (\<forall>z\<in>A. size z < size ya \<longrightarrow> \<not> P z)); x \<in> A; P x; \<not> (\<forall>y\<in>A. size y < size x \<longrightarrow> \<not> P y)\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. size y \<le> size x \<and> P y \<and> (\<forall>z\<in>A. size z < size y \<longrightarrow> \<not> P z)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>y\<in>A. size y < size x \<longrightarrow> \<not> P y)
[PROOF STEP]
obtain y where "y \<in> A" and "size y < size x" and "P y"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>y\<in>A. size y < size x \<longrightarrow> \<not> P y)

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> A; size y < size x; P y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<in> A
size y < size x
P y

goal (1 subgoal):
 1. \<lbrakk>\<forall>y. size y < size x \<longrightarrow> y \<in> A \<longrightarrow> P y \<longrightarrow> (\<exists>ya\<in>A. size ya \<le> size y \<and> P ya \<and> (\<forall>z\<in>A. size z < size ya \<longrightarrow> \<not> P z)); x \<in> A; P x; \<not> (\<forall>y\<in>A. size y < size x \<longrightarrow> \<not> P y)\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. size y \<le> size x \<and> P y \<and> (\<forall>z\<in>A. size z < size y \<longrightarrow> \<not> P z)
[PROOF STEP]
with "1.IH"
[PROOF STATE]
proof (chain)
picking this:
\<forall>y. size y < size x \<longrightarrow> y \<in> A \<longrightarrow> P y \<longrightarrow> (\<exists>ya\<in>A. size ya \<le> size y \<and> P ya \<and> (\<forall>z\<in>A. size z < size ya \<longrightarrow> \<not> P z))
y \<in> A
size y < size x
P y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>y. size y < size x \<longrightarrow> y \<in> A \<longrightarrow> P y \<longrightarrow> (\<exists>ya\<in>A. size ya \<le> size y \<and> P ya \<and> (\<forall>z\<in>A. size z < size ya \<longrightarrow> \<not> P z))
y \<in> A
size y < size x
P y

goal (1 subgoal):
 1. \<exists>y\<in>A. size y \<le> size x \<and> P y \<and> (\<forall>z\<in>A. size z < size y \<longrightarrow> \<not> P z)
[PROOF STEP]
by (fastforce elim!: order_trans)
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>A. size y \<le> size x \<and> P y \<and> (\<forall>z\<in>A. size z < size y \<longrightarrow> \<not> P z)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>A. size y \<le> size x \<and> P y \<and> (\<forall>z\<in>A. size z < size y \<longrightarrow> \<not> P z)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma less_not_eq [simp]:
  "x \<in> A \<Longrightarrow> size x < size y \<Longrightarrow> x = y \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> A; size x < size y; x = y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by simp


[STATEMENT]
lemma BAD_iff [iff]:
  "f \<in> BAD P \<longleftrightarrow> (\<forall>i. f i \<in> A) \<and> bad P f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<in> BAD P) = ((\<forall>i. f i \<in> A) \<and> bad P f)
[PROOF STEP]
by (auto simp: BAD_def)


[STATEMENT]
lemma geseq_iff:
  "(f, g) \<in> geseq \<longleftrightarrow>
    f \<in> SEQ A \<and> g \<in> SEQ A \<and> (f = g \<or> (\<exists>i. size (g i) < size (f i) \<and> (\<forall>j < i. f j = g j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((f, g) \<in> geseq) = (f \<in> SEQ A \<and> g \<in> SEQ A \<and> (f = g \<or> (\<exists>i. size (g i) < size (f i) \<and> (\<forall>j<i. f j = g j))))
[PROOF STEP]
by (auto simp: geseq_def)


[STATEMENT]
lemma gseq_iff:
  "(f, g) \<in> gseq \<longleftrightarrow> f \<in> SEQ A \<and> g \<in> SEQ A \<and> (\<exists>i. size (g i) < size (f i) \<and> (\<forall>j < i. f j = g j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((f, g) \<in> gseq) = (f \<in> SEQ A \<and> g \<in> SEQ A \<and> (\<exists>i. size (g i) < size (f i) \<and> (\<forall>j<i. f j = g j)))
[PROOF STEP]
by (auto simp: gseq_def)


[STATEMENT]
lemma geseqE:
  assumes "(f, g) \<in> geseq"
    and "\<lbrakk>\<forall>i. f i \<in> A; \<forall>i. g i \<in> A; f = g\<rbrakk> \<Longrightarrow> Q"
    and "\<And>i. \<lbrakk>\<forall>i. f i \<in> A; \<forall>i. g i \<in> A; size (g i) < size (f i); \<forall>j < i. f j = g j\<rbrakk> \<Longrightarrow> Q"
  shows "Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> geseq
\<lbrakk>\<forall>i. f i \<in> A; \<forall>i. g i \<in> A; f = g\<rbrakk> \<Longrightarrow> Q
\<lbrakk>\<forall>i. f i \<in> A; \<forall>i. g i \<in> A; size (g ?i) < size (f ?i); \<forall>j<?i. f j = g j\<rbrakk> \<Longrightarrow> Q

goal (1 subgoal):
 1. Q
[PROOF STEP]
by (auto simp: geseq_iff)


[STATEMENT]
lemma gseqE:
  assumes "(f, g) \<in> gseq"
    and "\<And>i. \<lbrakk>\<forall>i. f i \<in> A; \<forall>i. g i \<in> A; size (g i) < size (f i); \<forall>j < i. f j = g j\<rbrakk> \<Longrightarrow> Q"
  shows "Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> gseq
\<lbrakk>\<forall>i. f i \<in> A; \<forall>i. g i \<in> A; size (g ?i) < size (f ?i); \<forall>j<?i. f j = g j\<rbrakk> \<Longrightarrow> Q

goal (1 subgoal):
 1. Q
[PROOF STEP]
by (auto simp: gseq_iff)


[STATEMENT]
lemma eq_upto_BAD_mem:
  assumes "f \<in> eq_upto (BAD P) g i"
  shows "f j \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f j \<in> A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f \<in> eq_upto (BAD P) g i

goal (1 subgoal):
 1. f j \<in> A
[PROOF STEP]
by (auto)


[STATEMENT]
lemma eq_upto_BAD_non_empty:
  "eq_upto (BAD P) lb i \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_upto (BAD P) lb i \<noteq> {}
[PROOF STEP]
using eq_upto_lexmin_non_empty [of "BAD P"] and BAD_ex
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>BAD P \<subseteq> SEQ A; BAD P \<noteq> {}\<rbrakk> \<Longrightarrow> eq_upto (BAD P) lb ?i \<noteq> {}
h \<in> BAD P

goal (1 subgoal):
 1. eq_upto (BAD P) lb i \<noteq> {}
[PROOF STEP]
by auto


[STATEMENT]
lemma non_empty_ith:
  shows "ith (eq_upto (BAD P) lb i) i \<subseteq> A"
  and "ith (eq_upto (BAD P) lb i) i \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ith (eq_upto (BAD P) lb i) i \<subseteq> A &&& ith (eq_upto (BAD P) lb i) i \<noteq> {}
[PROOF STEP]
using eq_upto_BAD_non_empty [of i]
[PROOF STATE]
proof (prove)
using this:
eq_upto (BAD P) lb i \<noteq> {}

goal (1 subgoal):
 1. ith (eq_upto (BAD P) lb i) i \<subseteq> A &&& ith (eq_upto (BAD P) lb i) i \<noteq> {}
[PROOF STEP]
by auto


[STATEMENT]
lemma lb_BAD:
  "lb \<in> BAD P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lb \<in> BAD P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lb \<in> BAD P
[PROOF STEP]
have *: "\<And>j. lb j \<in> ith (eq_upto (BAD P) lb j) j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. lb j \<in> ith (eq_upto (BAD P) lb j) j
[PROOF STEP]
by (rule lb_mem)
[PROOF STATE]
proof (state)
this:
lb ?j \<in> ith (eq_upto (BAD P) lb ?j) ?j

goal (1 subgoal):
 1. lb \<in> BAD P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lb ?j \<in> ith (eq_upto (BAD P) lb ?j) ?j
[PROOF STEP]
have "\<forall>i. lb i \<in> A"
[PROOF STATE]
proof (prove)
using this:
lb ?j \<in> ith (eq_upto (BAD P) lb ?j) ?j

goal (1 subgoal):
 1. \<forall>i. lb i \<in> A
[PROOF STEP]
by (auto simp: ith_conv) (metis eq_upto_BAD_mem)
[PROOF STATE]
proof (state)
this:
\<forall>i. lb i \<in> A

goal (1 subgoal):
 1. lb \<in> BAD P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>i. lb i \<in> A

goal (1 subgoal):
 1. lb \<in> BAD P
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>i. lb i \<in> A

goal (1 subgoal):
 1. lb \<in> BAD P
[PROOF STEP]
assume "good P lb"
[PROOF STATE]
proof (state)
this:
good P lb

goal (1 subgoal):
 1. lb \<in> BAD P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
good P lb
[PROOF STEP]
obtain i j where "i < j" and "P (lb i) (lb j)"
[PROOF STATE]
proof (prove)
using this:
good P lb

goal (1 subgoal):
 1. (\<And>i j. \<lbrakk>i < j; P (lb i) (lb j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: good_def)
[PROOF STATE]
proof (state)
this:
i < j
P (lb i) (lb j)

goal (1 subgoal):
 1. lb \<in> BAD P
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
lb ?j \<in> ith (eq_upto (BAD P) lb ?j) ?j
[PROOF STEP]
have "lb j \<in> ith (eq_upto (BAD P) lb j) j"
[PROOF STATE]
proof (prove)
using this:
lb ?j \<in> ith (eq_upto (BAD P) lb ?j) ?j

goal (1 subgoal):
 1. lb j \<in> ith (eq_upto (BAD P) lb j) j
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
lb j \<in> ith (eq_upto (BAD P) lb j) j

goal (1 subgoal):
 1. lb \<in> BAD P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lb j \<in> ith (eq_upto (BAD P) lb j) j
[PROOF STEP]
obtain g where "g \<in> eq_upto (BAD P) lb j" and "g j = lb j"
[PROOF STATE]
proof (prove)
using this:
lb j \<in> ith (eq_upto (BAD P) lb j) j

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> eq_upto (BAD P) lb j; g j = lb j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
g \<in> eq_upto (BAD P) lb j
g j = lb j

goal (1 subgoal):
 1. lb \<in> BAD P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
g \<in> eq_upto (BAD P) lb j
g j = lb j
[PROOF STEP]
have "\<forall>k \<le> j. g k = lb k"
[PROOF STATE]
proof (prove)
using this:
g \<in> eq_upto (BAD P) lb j
g j = lb j

goal (1 subgoal):
 1. \<forall>k\<le>j. g k = lb k
[PROOF STEP]
by (auto simp: order_le_less)
[PROOF STATE]
proof (state)
this:
\<forall>k\<le>j. g k = lb k

goal (1 subgoal):
 1. lb \<in> BAD P
[PROOF STEP]
with \<open>i < j\<close> and \<open>P (lb i) (lb j)\<close>
[PROOF STATE]
proof (chain)
picking this:
i < j
P (lb i) (lb j)
\<forall>k\<le>j. g k = lb k
[PROOF STEP]
have "P (g i) (g j)"
[PROOF STATE]
proof (prove)
using this:
i < j
P (lb i) (lb j)
\<forall>k\<le>j. g k = lb k

goal (1 subgoal):
 1. P (g i) (g j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P (g i) (g j)

goal (1 subgoal):
 1. lb \<in> BAD P
[PROOF STEP]
with \<open>i < j\<close>
[PROOF STATE]
proof (chain)
picking this:
i < j
P (g i) (g j)
[PROOF STEP]
have "good P g"
[PROOF STATE]
proof (prove)
using this:
i < j
P (g i) (g j)

goal (1 subgoal):
 1. good P g
[PROOF STEP]
by (auto simp: good_def)
[PROOF STATE]
proof (state)
this:
good P g

goal (1 subgoal):
 1. lb \<in> BAD P
[PROOF STEP]
with \<open>g \<in> eq_upto (BAD P) lb j\<close>
[PROOF STATE]
proof (chain)
picking this:
g \<in> eq_upto (BAD P) lb j
good P g
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
g \<in> eq_upto (BAD P) lb j
good P g

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

goal (1 subgoal):
 1. lb \<in> BAD P
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
good P lb \<Longrightarrow> False

goal (1 subgoal):
 1. lb \<in> BAD P
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. lb i \<in> A
good P lb \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>i. lb i \<in> A
good P lb \<Longrightarrow> False

goal (1 subgoal):
 1. lb \<in> BAD P
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
lb \<in> BAD P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lb_lower_bound:
  "\<forall>g. (lb, g) \<in> gseq \<longrightarrow> g \<notin> BAD P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>g. (lb, g) \<in> gseq \<longrightarrow> g \<notin> BAD P
[PROOF STEP]
proof (intro allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>g. (lb, g) \<in> gseq \<Longrightarrow> g \<notin> BAD P
[PROOF STEP]
fix g
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>g. (lb, g) \<in> gseq \<Longrightarrow> g \<notin> BAD P
[PROOF STEP]
assume "(lb, g) \<in> gseq"
[PROOF STATE]
proof (state)
this:
(lb, g) \<in> gseq

goal (1 subgoal):
 1. \<And>g. (lb, g) \<in> gseq \<Longrightarrow> g \<notin> BAD P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(lb, g) \<in> gseq
[PROOF STEP]
obtain i where "g i \<in> A" and "size (g i) < size (lb i)"
    and "\<forall>j < i. lb j = g j"
[PROOF STATE]
proof (prove)
using this:
(lb, g) \<in> gseq

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>g i \<in> A; size (g i) < size (lb i); \<forall>j<i. lb j = g j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: gseq_iff)
[PROOF STATE]
proof (state)
this:
g i \<in> A
size (g i) < size (lb i)
\<forall>j<i. lb j = g j

goal (1 subgoal):
 1. \<And>g. (lb, g) \<in> gseq \<Longrightarrow> g \<notin> BAD P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
g i \<in> A
size (g i) < size (lb i)
\<forall>j<i. lb j = g j

goal (1 subgoal):
 1. \<And>g. (lb, g) \<in> gseq \<Longrightarrow> g \<notin> BAD P
[PROOF STEP]
with lb_minimal
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?y \<in> A; size ?y < size (lb ?i)\<rbrakk> \<Longrightarrow> ?y \<notin> ith (eq_upto (BAD P) lb ?i) ?i
g i \<in> A
size (g i) < size (lb i)
\<forall>j<i. lb j = g j
[PROOF STEP]
have "g i \<notin> ith (eq_upto (BAD P) lb i) i"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y \<in> A; size ?y < size (lb ?i)\<rbrakk> \<Longrightarrow> ?y \<notin> ith (eq_upto (BAD P) lb ?i) ?i
g i \<in> A
size (g i) < size (lb i)
\<forall>j<i. lb j = g j

goal (1 subgoal):
 1. g i \<notin> ith (eq_upto (BAD P) lb i) i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g i \<notin> ith (eq_upto (BAD P) lb i) i

goal (1 subgoal):
 1. \<And>g. (lb, g) \<in> gseq \<Longrightarrow> g \<notin> BAD P
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
g i \<in> A
size (g i) < size (lb i)
\<forall>j<i. lb j = g j
g i \<notin> ith (eq_upto (BAD P) lb i) i
[PROOF STEP]
show "g \<notin> BAD P"
[PROOF STATE]
proof (prove)
using this:
g i \<in> A
size (g i) < size (lb i)
\<forall>j<i. lb j = g j
g i \<notin> ith (eq_upto (BAD P) lb i) i

goal (1 subgoal):
 1. g \<notin> BAD P
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
g \<notin> BAD P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lower_bound_ex:
  "\<exists>f \<in> BAD P. \<forall>g. (f, g) \<in> gseq \<longrightarrow> g \<notin> BAD P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f\<in>BAD P. \<forall>g. (f, g) \<in> gseq \<longrightarrow> g \<notin> BAD P
[PROOF STEP]
using lb_BAD and lb_lower_bound
[PROOF STATE]
proof (prove)
using this:
lb \<in> BAD P
\<forall>g. (lb, g) \<in> gseq \<longrightarrow> g \<notin> BAD P

goal (1 subgoal):
 1. \<exists>f\<in>BAD P. \<forall>g. (f, g) \<in> gseq \<longrightarrow> g \<notin> BAD P
[PROOF STEP]
by blast


[STATEMENT]
lemma gseq_conv:
  "(f, g) \<in> gseq \<longleftrightarrow> f \<noteq> g \<and> (f, g) \<in> geseq"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((f, g) \<in> gseq) = (f \<noteq> g \<and> (f, g) \<in> geseq)
[PROOF STEP]
by (auto simp: gseq_def geseq_def dest: less_not_eq)


[STATEMENT]
lemma mbs:
  "\<exists>f \<in> BAD P. \<forall>g. (f, g) \<in> gseq \<longrightarrow> good P g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f\<in>BAD P. \<forall>g. (f, g) \<in> gseq \<longrightarrow> good P g
[PROOF STEP]
using lower_bound_ex
[PROOF STATE]
proof (prove)
using this:
\<exists>f\<in>BAD P. \<forall>g. (f, g) \<in> gseq \<longrightarrow> g \<notin> BAD P

goal (1 subgoal):
 1. \<exists>f\<in>BAD P. \<forall>g. (f, g) \<in> gseq \<longrightarrow> good P g
[PROOF STEP]
by (auto simp: gseq_conv geseq_iff)


[STATEMENT]
lemma ICdual:  "\<I> \<^bold>\<equiv> \<C>\<^sup>d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I> \<^bold>\<equiv> \<C>\<^sup>d
[PROOF STEP]
by (simp add: Cl_br_def Int_br_def dual_def equal_op_def conn)


[STATEMENT]
lemma ICdual': "\<C> \<^bold>\<equiv> \<I>\<^sup>d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<C> \<^bold>\<equiv> \<I>\<^sup>d
[PROOF STEP]
by (simp add: Cl_br_def Int_br_def dual_def equal_op_def conn)


[STATEMENT]
lemma FI_rel: "Br_1 \<B> \<Longrightarrow> \<F> \<^bold>\<equiv> \<F>\<^sub>I \<I>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Br_1 \<B> \<Longrightarrow> \<F> \<^bold>\<equiv> \<F>\<^sub>I \<I>
[PROOF STEP]
using Fr_br_def Fr_int_def Int_br_def equal_op_def
[PROOF STATE]
proof (prove)
using this:
\<F>\<^sub>B ?\<B> \<equiv> \<lambda>A. ?\<B> A \<^bold>\<or> ?\<B> (\<^bold>\<midarrow>A)
\<F>\<^sub>I ?\<I> \<equiv> ?\<I>\<^sup>c \<^bold>\<sqinter> ?\<I>\<^sup>d
\<I>\<^sub>B ?\<B> \<equiv> \<lambda>A. A \<^bold>\<leftharpoonup> ?\<B> A
?\<phi> \<^bold>\<equiv> ?\<psi> \<equiv> \<forall>X w. ?\<phi> X w = ?\<psi> X w

goal (1 subgoal):
 1. Br_1 \<B> \<Longrightarrow> \<F> \<^bold>\<equiv> \<F>\<^sub>I \<I>
[PROOF STEP]
by (smt Br_5b_def PB5b dual_def conn)


[STATEMENT]
lemma IF_rel: "Br_1 \<B> \<Longrightarrow> \<I> \<^bold>\<equiv> \<I>\<^sub>F \<F>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Br_1 \<B> \<Longrightarrow> \<I> \<^bold>\<equiv> \<I>\<^sub>F \<F>
[PROOF STEP]
using Br_5b_def Fr_br_def Int_br_def Int_fr_def PB5b
[PROOF STATE]
proof (prove)
using this:
Br_5b ?\<phi> \<equiv> \<forall>A. contains A (?\<phi> A)
\<F>\<^sub>B ?\<B> \<equiv> \<lambda>A. ?\<B> A \<^bold>\<or> ?\<B> (\<^bold>\<midarrow>A)
\<I>\<^sub>B ?\<B> \<equiv> \<lambda>A. A \<^bold>\<leftharpoonup> ?\<B> A
\<I>\<^sub>F ?\<F> \<equiv> \<lambda>A. A \<^bold>\<leftharpoonup> ?\<F> A
Br_1 ?\<phi> \<Longrightarrow> Br_5b ?\<phi>

goal (1 subgoal):
 1. Br_1 \<B> \<Longrightarrow> \<I> \<^bold>\<equiv> \<I>\<^sub>F \<F>
[PROOF STEP]
unfolding equal_op_def conn
[PROOF STATE]
proof (prove)
using this:
Br_5b ?\<phi> \<equiv> \<forall>A. contains A (?\<phi> A)
\<F>\<^sub>B ?\<B> \<equiv> \<lambda>A w. ?\<B> A w \<or> ?\<B> (\<lambda>w. \<not> A w) w
\<I>\<^sub>B ?\<B> \<equiv> \<lambda>A w. A w \<and> \<not> ?\<B> A w
\<I>\<^sub>F ?\<F> \<equiv> \<lambda>A w. A w \<and> \<not> ?\<F> A w
Br_1 ?\<phi> \<Longrightarrow> Br_5b ?\<phi>

goal (1 subgoal):
 1. Br_1 \<B> \<Longrightarrow> \<forall>X w. \<I> X w = \<I>\<^sub>F \<F> X w
[PROOF STEP]
by fastforce


[STATEMENT]
lemma FC_rel: "Br_1 \<B> \<Longrightarrow> \<F> \<^bold>\<equiv> \<F>\<^sub>C \<C>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Br_1 \<B> \<Longrightarrow> \<F> \<^bold>\<equiv> \<F>\<^sub>C \<C>
[PROOF STEP]
using Br_5b_def Cl_br_def Fr_br_def Fr_cl_def PB5b
[PROOF STATE]
proof (prove)
using this:
Br_5b ?\<phi> \<equiv> \<forall>A. contains A (?\<phi> A)
\<C>\<^sub>B ?\<B> \<equiv> \<lambda>A. A \<^bold>\<or> ?\<B> (\<^bold>\<midarrow>A)
\<F>\<^sub>B ?\<B> \<equiv> \<lambda>A. ?\<B> A \<^bold>\<or> ?\<B> (\<^bold>\<midarrow>A)
\<F>\<^sub>C ?\<C> \<equiv> \<lambda>A. ?\<C> A \<^bold>\<and> ?\<C> (\<^bold>\<midarrow>A)
Br_1 ?\<phi> \<Longrightarrow> Br_5b ?\<phi>

goal (1 subgoal):
 1. Br_1 \<B> \<Longrightarrow> \<F> \<^bold>\<equiv> \<F>\<^sub>C \<C>
[PROOF STEP]
unfolding equal_op_def conn
[PROOF STATE]
proof (prove)
using this:
Br_5b ?\<phi> \<equiv> \<forall>A. contains A (?\<phi> A)
\<C>\<^sub>B ?\<B> \<equiv> \<lambda>A w. A w \<or> ?\<B> (\<lambda>w. \<not> A w) w
\<F>\<^sub>B ?\<B> \<equiv> \<lambda>A w. ?\<B> A w \<or> ?\<B> (\<lambda>w. \<not> A w) w
\<F>\<^sub>C ?\<C> \<equiv> \<lambda>A w. ?\<C> A w \<and> ?\<C> (\<lambda>w. \<not> A w) w
Br_1 ?\<phi> \<Longrightarrow> Br_5b ?\<phi>

goal (1 subgoal):
 1. Br_1 \<B> \<Longrightarrow> \<forall>X w. \<F> X w = \<F>\<^sub>C \<C> X w
[PROOF STEP]
by fastforce


[STATEMENT]
lemma CF_rel: "Br_1 \<B> \<Longrightarrow> \<C> \<^bold>\<equiv> \<C>\<^sub>F \<F>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Br_1 \<B> \<Longrightarrow> \<C> \<^bold>\<equiv> \<C>\<^sub>F \<F>
[PROOF STEP]
using Br_5b_def Cl_br_def Cl_fr_def Fr_br_def PB5b
[PROOF STATE]
proof (prove)
using this:
Br_5b ?\<phi> \<equiv> \<forall>A. contains A (?\<phi> A)
\<C>\<^sub>B ?\<B> \<equiv> \<lambda>A. A \<^bold>\<or> ?\<B> (\<^bold>\<midarrow>A)
\<C>\<^sub>F ?\<F> \<equiv> \<lambda>A. A \<^bold>\<or> ?\<F> A
\<F>\<^sub>B ?\<B> \<equiv> \<lambda>A. ?\<B> A \<^bold>\<or> ?\<B> (\<^bold>\<midarrow>A)
Br_1 ?\<phi> \<Longrightarrow> Br_5b ?\<phi>

goal (1 subgoal):
 1. Br_1 \<B> \<Longrightarrow> \<C> \<^bold>\<equiv> \<C>\<^sub>F \<F>
[PROOF STEP]
unfolding equal_op_def conn
[PROOF STATE]
proof (prove)
using this:
Br_5b ?\<phi> \<equiv> \<forall>A. contains A (?\<phi> A)
\<C>\<^sub>B ?\<B> \<equiv> \<lambda>A w. A w \<or> ?\<B> (\<lambda>w. \<not> A w) w
\<C>\<^sub>F ?\<F> \<equiv> \<lambda>A w. A w \<or> ?\<F> A w
\<F>\<^sub>B ?\<B> \<equiv> \<lambda>A w. ?\<B> A w \<or> ?\<B> (\<lambda>w. \<not> A w) w
Br_1 ?\<phi> \<Longrightarrow> Br_5b ?\<phi>

goal (1 subgoal):
 1. Br_1 \<B> \<Longrightarrow> \<forall>X w. \<C> X w = \<C>\<^sub>F \<F> X w
[PROOF STEP]
by fastforce


[STATEMENT]
lemma BC_rel: "Br_1 \<B> \<Longrightarrow> \<B> \<^bold>\<equiv> \<B>\<^sub>C \<C>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Br_1 \<B> \<Longrightarrow> \<B> \<^bold>\<equiv> \<B>\<^sub>C \<C>
[PROOF STEP]
using BI_BC_rel BI_rel ICdual' eq_ext'
[PROOF STATE]
proof (prove)
using this:
\<B>\<^sub>I ?\<phi> = \<B>\<^sub>C ?\<phi>\<^sup>d
Br_1 \<B> \<Longrightarrow> \<B> \<^bold>\<equiv> \<B>\<^sub>I \<I>
\<C> \<^bold>\<equiv> \<I>\<^sup>d
?a \<^bold>\<equiv> ?b \<Longrightarrow> ?a = ?b

goal (1 subgoal):
 1. Br_1 \<B> \<Longrightarrow> \<B> \<^bold>\<equiv> \<B>\<^sub>C \<C>
[PROOF STEP]
by fastforce


[STATEMENT]
lemma BF_rel: "Br_1 \<B> \<Longrightarrow> \<B> \<^bold>\<equiv> \<B>\<^sub>F \<F>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Br_1 \<B> \<Longrightarrow> \<B> \<^bold>\<equiv> \<B>\<^sub>F \<F>
[PROOF STEP]
by (smt BI_rel Br_fr_def Br_int_def IF_rel Int_fr_def diff_def equal_op_def meet_def)


[STATEMENT]
lemma fp1: "Br_1 \<B> \<Longrightarrow> \<I>\<^sup>f\<^sup>p \<^bold>\<equiv> \<B>\<^sup>c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Br_1 \<B> \<Longrightarrow> \<I>\<^sup>f\<^sup>p \<^bold>\<equiv> \<B>\<^sup>c
[PROOF STEP]
using Br_5b_def Int_br_def PB5b
[PROOF STATE]
proof (prove)
using this:
Br_5b ?\<phi> \<equiv> \<forall>A. contains A (?\<phi> A)
\<I>\<^sub>B ?\<B> \<equiv> \<lambda>A. A \<^bold>\<leftharpoonup> ?\<B> A
Br_1 ?\<phi> \<Longrightarrow> Br_5b ?\<phi>

goal (1 subgoal):
 1. Br_1 \<B> \<Longrightarrow> \<I>\<^sup>f\<^sup>p \<^bold>\<equiv> \<B>\<^sup>c
[PROOF STEP]
unfolding equal_op_def conn
[PROOF STATE]
proof (prove)
using this:
Br_5b ?\<phi> \<equiv> \<forall>A. contains A (?\<phi> A)
\<I>\<^sub>B ?\<B> \<equiv> \<lambda>A w. A w \<and> \<not> ?\<B> A w
Br_1 ?\<phi> \<Longrightarrow> Br_5b ?\<phi>

goal (1 subgoal):
 1. Br_1 \<B> \<Longrightarrow> \<forall>X w. (\<I> X w = X w) = (\<not> \<B> X w)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma fp2: "Br_1 \<B> \<Longrightarrow> \<B>\<^sup>f\<^sup>p \<^bold>\<equiv> \<I>\<^sup>c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Br_1 \<B> \<Longrightarrow> \<B>\<^sup>f\<^sup>p \<^bold>\<equiv> \<I>\<^sup>c
[PROOF STEP]
using Br_5b_def Int_br_def PB5b conn equal_op_def
[PROOF STATE]
proof (prove)
using this:
Br_5b ?\<phi> \<equiv> \<forall>A. contains A (?\<phi> A)
\<I>\<^sub>B ?\<B> \<equiv> \<lambda>A. A \<^bold>\<leftharpoonup> ?\<B> A
Br_1 ?\<phi> \<Longrightarrow> Br_5b ?\<phi>
?A \<^bold>\<and> ?B \<equiv> \<lambda>w. ?A w \<and> ?B w
?A \<^bold>\<or> ?B \<equiv> \<lambda>w. ?A w \<or> ?B w
\<^bold>\<top> \<equiv> \<lambda>w. True
\<^bold>\<bottom> \<equiv> \<lambda>w. False
?A \<^bold>\<rightarrow> ?B \<equiv> \<lambda>w. ?B w \<longleftarrow> ?A w
?A \<^bold>\<leftrightarrow> ?B \<equiv> \<lambda>w. ?A w = ?B w
?A \<^bold>\<leftharpoonup> ?B \<equiv> \<lambda>w. ?A w \<and> \<not> ?B w
\<^bold>\<midarrow>?A \<equiv> \<lambda>w. \<not> ?A w
?\<phi> \<^bold>\<equiv> ?\<psi> \<equiv> \<forall>X w. ?\<phi> X w = ?\<psi> X w

goal (1 subgoal):
 1. Br_1 \<B> \<Longrightarrow> \<B>\<^sup>f\<^sup>p \<^bold>\<equiv> \<I>\<^sup>c
[PROOF STEP]
by fastforce


[STATEMENT]
lemma fp3: "Br_1 \<B> \<Longrightarrow> \<C>\<^sup>f\<^sup>p \<^bold>\<equiv> \<B>\<^sup>d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Br_1 \<B> \<Longrightarrow> \<C>\<^sup>f\<^sup>p \<^bold>\<equiv> \<B>\<^sup>d
[PROOF STEP]
using Br_5c_def Cl_br_def PB5c dual_def
[PROOF STATE]
proof (prove)
using this:
Br_5c ?\<phi> \<equiv> \<forall>A. contains (?\<phi>\<^sup>d A) A
\<C>\<^sub>B ?\<B> \<equiv> \<lambda>A. A \<^bold>\<or> ?\<B> (\<^bold>\<midarrow>A)
Br_1 ?\<phi> \<Longrightarrow> Br_5c ?\<phi>
?\<phi>\<^sup>d \<equiv> \<lambda>X. ?\<phi>\<^sup>c (\<^bold>\<midarrow>X)

goal (1 subgoal):
 1. Br_1 \<B> \<Longrightarrow> \<C>\<^sup>f\<^sup>p \<^bold>\<equiv> \<B>\<^sup>d
[PROOF STEP]
unfolding equal_op_def conn
[PROOF STATE]
proof (prove)
using this:
Br_5c ?\<phi> \<equiv> \<forall>A. contains (?\<phi>\<^sup>d A) A
\<C>\<^sub>B ?\<B> \<equiv> \<lambda>A w. A w \<or> ?\<B> (\<lambda>w. \<not> A w) w
Br_1 ?\<phi> \<Longrightarrow> Br_5c ?\<phi>
?\<phi>\<^sup>d \<equiv> \<lambda>X w. \<not> ?\<phi> (\<lambda>w. \<not> X w) w

goal (1 subgoal):
 1. Br_1 \<B> \<Longrightarrow> \<forall>X w. (\<C> X w = X w) = \<B>\<^sup>d X w
[PROOF STEP]
by fastforce


[STATEMENT]
lemma fp4: "Br_1 \<B> \<Longrightarrow> (\<B>\<^sup>d)\<^sup>f\<^sup>p \<^bold>\<equiv> \<C>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Br_1 \<B> \<Longrightarrow> \<B>\<^sup>d\<^sup>f\<^sup>p \<^bold>\<equiv> \<C>
[PROOF STEP]
by (smt dimp_def equal_op_def fp3)


[STATEMENT]
lemma fp5: "Br_1 \<B> \<Longrightarrow> \<F>\<^sup>f\<^sup>p \<^bold>\<equiv> \<B> \<^bold>\<squnion> (\<C>\<^sup>c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Br_1 \<B> \<Longrightarrow> \<F>\<^sup>f\<^sup>p \<^bold>\<equiv> \<B> \<^bold>\<squnion> \<C>\<^sup>c
[PROOF STEP]
by (smt Br_5b_def Cl_br_def Fr_br_def PB5b equal_op_def conn)


[STATEMENT]
lemma Int_Open: "Br_1 \<B> \<Longrightarrow> Br_3 \<B> \<Longrightarrow> \<forall>A. Op(\<I> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Br_1 \<B>; Br_3 \<B>\<rbrakk> \<Longrightarrow> \<forall>A w. \<I> (\<I> A) w = \<I> A w
[PROOF STEP]
using IB4 IDEM_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Br_1 ?\<phi>; Br_3 ?\<phi>\<rbrakk> \<Longrightarrow> Br_6 (\<I>\<^sub>B ?\<phi>)
Br_6 ?\<phi> \<equiv> \<forall>A w. ?\<phi> A w = ?\<phi> (?\<phi> A) w

goal (1 subgoal):
 1. \<lbrakk>Br_1 \<B>; Br_3 \<B>\<rbrakk> \<Longrightarrow> \<forall>A w. \<I> (\<I> A) w = \<I> A w
[PROOF STEP]
by blast


[STATEMENT]
lemma Cl_Closed: "Br_1 \<B> \<Longrightarrow> Br_3 \<B> \<Longrightarrow> \<forall>A. Cl(\<C> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Br_1 \<B>; Br_3 \<B>\<rbrakk> \<Longrightarrow> \<forall>A w. \<C> (\<C> A) w = \<C> A w
[PROOF STEP]
using CB4 IDEM_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Br_1 ?\<phi>; Br_3 ?\<phi>\<rbrakk> \<Longrightarrow> Br_6 (\<C>\<^sub>B ?\<phi>)
Br_6 ?\<phi> \<equiv> \<forall>A w. ?\<phi> A w = ?\<phi> (?\<phi> A) w

goal (1 subgoal):
 1. \<lbrakk>Br_1 \<B>; Br_3 \<B>\<rbrakk> \<Longrightarrow> \<forall>A w. \<C> (\<C> A) w = \<C> A w
[PROOF STEP]
by blast


[STATEMENT]
lemma Br_Border: "Br_1 \<B> \<Longrightarrow> \<forall>A. Br(\<B> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Br_1 \<B> \<Longrightarrow> \<forall>A w. \<B> (\<B> A) w = \<B> A w
[PROOF STEP]
using IDEM_def PB6
[PROOF STATE]
proof (prove)
using this:
Br_6 ?\<phi> \<equiv> \<forall>A w. ?\<phi> A w = ?\<phi> (?\<phi> A) w
Br_1 ?\<phi> \<Longrightarrow> Br_6 ?\<phi>

goal (1 subgoal):
 1. Br_1 \<B> \<Longrightarrow> \<forall>A w. \<B> (\<B> A) w = \<B> A w
[PROOF STEP]
by blast


[STATEMENT]
lemma "\<BB> \<B> \<Longrightarrow> \<forall>A. Fr(\<F> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<BB> \<B> \<Longrightarrow> \<forall>A w. \<F> (\<F> A) w = \<F> A w
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<BB> \<B> \<Longrightarrow> \<forall>A w. \<F> (\<F> A) w = \<F> A w
[PROOF STEP]
oops


[STATEMENT]
lemma OpCldual: "\<forall>A. Cl A \<longleftrightarrow> Op(\<^bold>\<midarrow>A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A. (\<forall>w. \<C> A w = A w) = (\<forall>w. \<I> (\<^bold>\<midarrow>A) w = (\<^bold>\<midarrow>A) w)
[PROOF STEP]
using Cl_br_def Int_br_def conn
[PROOF STATE]
proof (prove)
using this:
\<C>\<^sub>B ?\<B> \<equiv> \<lambda>A. A \<^bold>\<or> ?\<B> (\<^bold>\<midarrow>A)
\<I>\<^sub>B ?\<B> \<equiv> \<lambda>A. A \<^bold>\<leftharpoonup> ?\<B> A
?A \<^bold>\<and> ?B \<equiv> \<lambda>w. ?A w \<and> ?B w
?A \<^bold>\<or> ?B \<equiv> \<lambda>w. ?A w \<or> ?B w
\<^bold>\<top> \<equiv> \<lambda>w. True
\<^bold>\<bottom> \<equiv> \<lambda>w. False
?A \<^bold>\<rightarrow> ?B \<equiv> \<lambda>w. ?B w \<longleftarrow> ?A w
?A \<^bold>\<leftrightarrow> ?B \<equiv> \<lambda>w. ?A w = ?B w
?A \<^bold>\<leftharpoonup> ?B \<equiv> \<lambda>w. ?A w \<and> \<not> ?B w
\<^bold>\<midarrow>?A \<equiv> \<lambda>w. \<not> ?A w

goal (1 subgoal):
 1. \<forall>A. (\<forall>w. \<C> A w = A w) = (\<forall>w. \<I> (\<^bold>\<midarrow>A) w = (\<^bold>\<midarrow>A) w)
[PROOF STEP]
by auto


[STATEMENT]
lemma ClOpdual: "\<forall>A. Op A \<longleftrightarrow> Cl(\<^bold>\<midarrow>A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A. (\<forall>w. \<I> A w = A w) = (\<forall>w. \<C> (\<^bold>\<midarrow>A) w = (\<^bold>\<midarrow>A) w)
[PROOF STEP]
using Cl_br_def Int_br_def conn
[PROOF STATE]
proof (prove)
using this:
\<C>\<^sub>B ?\<B> \<equiv> \<lambda>A. A \<^bold>\<or> ?\<B> (\<^bold>\<midarrow>A)
\<I>\<^sub>B ?\<B> \<equiv> \<lambda>A. A \<^bold>\<leftharpoonup> ?\<B> A
?A \<^bold>\<and> ?B \<equiv> \<lambda>w. ?A w \<and> ?B w
?A \<^bold>\<or> ?B \<equiv> \<lambda>w. ?A w \<or> ?B w
\<^bold>\<top> \<equiv> \<lambda>w. True
\<^bold>\<bottom> \<equiv> \<lambda>w. False
?A \<^bold>\<rightarrow> ?B \<equiv> \<lambda>w. ?B w \<longleftarrow> ?A w
?A \<^bold>\<leftrightarrow> ?B \<equiv> \<lambda>w. ?A w = ?B w
?A \<^bold>\<leftharpoonup> ?B \<equiv> \<lambda>w. ?A w \<and> \<not> ?B w
\<^bold>\<midarrow>?A \<equiv> \<lambda>w. \<not> ?A w

goal (1 subgoal):
 1. \<forall>A. (\<forall>w. \<I> A w = A w) = (\<forall>w. \<C> (\<^bold>\<midarrow>A) w = (\<^bold>\<midarrow>A) w)
[PROOF STEP]
by auto


[STATEMENT]
lemma Fr_ClBr: "Br_1 \<B> \<Longrightarrow> \<forall>A. Fr(A) = (Cl(A) \<and> Br(A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Br_1 \<B> \<Longrightarrow> \<forall>A. (\<forall>w. \<F> A w = A w) = ((\<forall>w. \<C> A w = A w) \<and> (\<forall>w. \<B> A w = A w))
[PROOF STEP]
by (metis BF_rel Br_fr_def CF_rel Cl_fr_def eq_ext' join_def meet_def)


[STATEMENT]
lemma Cl_F: "Br_1 \<B> \<Longrightarrow> Br_3 \<B> \<Longrightarrow> \<forall>A. Cl(\<F> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Br_1 \<B>; Br_3 \<B>\<rbrakk> \<Longrightarrow> \<forall>A w. \<C> (\<F> A) w = \<F> A w
[PROOF STEP]
by (metis CF_rel Cl_fr_def FB4 Fr_4_def eq_ext' join_def)


[STATEMENT]
lemma small_ordinal_arrs[simp]:
  "small {[a, b]\<^sub>\<circ> | a b. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> a \<le> b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small {[a, b]\<^sub>\<circ> |a b. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b}
[PROOF STEP]
by (rule down[where x=\<open>A \<times>\<^sub>\<bullet> A\<close>]) auto


[STATEMENT]
lemma ordinal_arrsI[cat_ordinal_cs_intros]:
  assumes "x = [a, b]\<^sub>\<circ>" and "a \<in>\<^sub>\<circ> A" and "b \<in>\<^sub>\<circ> A" and "a \<le> b"
  shows "x \<in>\<^sub>\<circ> ordinal_arrs A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>\<circ> ordinal_arrs A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x = [a, b]\<^sub>\<circ>
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b

goal (1 subgoal):
 1. x \<in>\<^sub>\<circ> ordinal_arrs A
[PROOF STEP]
unfolding ordinal_arrs_def
[PROOF STATE]
proof (prove)
using this:
x = [a, b]\<^sub>\<circ>
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b

goal (1 subgoal):
 1. x \<in>\<^sub>\<circ> ZFC_in_HOL.set {[a, b]\<^sub>\<circ> |a b. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b}
[PROOF STEP]
by auto


[STATEMENT]
lemma ordinal_arrsD[dest]:
  assumes "[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> ordinal_arrs A"
  shows "a \<in>\<^sub>\<circ> A" and "b \<in>\<^sub>\<circ> A" and "a \<le> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> A &&& b \<in>\<^sub>\<circ> A &&& a \<subseteq>\<^sub>\<circ> b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> ordinal_arrs A

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> A &&& b \<in>\<^sub>\<circ> A &&& a \<subseteq>\<^sub>\<circ> b
[PROOF STEP]
unfolding ordinal_arrs_def
[PROOF STATE]
proof (prove)
using this:
[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> ZFC_in_HOL.set {[a, b]\<^sub>\<circ> |a b. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b}

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> A &&& b \<in>\<^sub>\<circ> A &&& a \<subseteq>\<^sub>\<circ> b
[PROOF STEP]
by auto


[STATEMENT]
lemma ordinal_arrsE[elim]:
  assumes "x \<in>\<^sub>\<circ> ordinal_arrs A"
  obtains a b where "a \<in>\<^sub>\<circ> A" and "b \<in>\<^sub>\<circ> A" and "a \<le> b" and "x = [a, b]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>a \<in>\<^sub>\<circ> A; b \<in>\<^sub>\<circ> A; a \<subseteq>\<^sub>\<circ> b; x = [a, b]\<^sub>\<circ>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> ordinal_arrs A

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>a \<in>\<^sub>\<circ> A; b \<in>\<^sub>\<circ> A; a \<subseteq>\<^sub>\<circ> b; x = [a, b]\<^sub>\<circ>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding ordinal_arrs_def
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> ZFC_in_HOL.set {[a, b]\<^sub>\<circ> |a b. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b}

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>a \<in>\<^sub>\<circ> A; b \<in>\<^sub>\<circ> A; a \<subseteq>\<^sub>\<circ> b; x = [a, b]\<^sub>\<circ>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp


[STATEMENT]
lemma small_ordinal_composable[simp]:
  "small
    {
      [[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> | a b c.
        a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<le> b \<and> b \<le> c
    }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}
[PROOF STEP]
by (rule down[where x=\<open>(A \<times>\<^sub>\<bullet> A) \<times>\<^sub>\<bullet> (A \<times>\<^sub>\<bullet> A)\<close>]) auto