[STATEMENT]
lemma linear_sup_closed:
  "linear x \<Longrightarrow> linear (x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linear x \<Longrightarrow> linear (x \<squnion> y)
[PROOF STEP]
by (metis conv_dist_sup sup_assoc sup_commute sup_top_right)


[STATEMENT]
lemma linear_reflexive:
  "linear x \<Longrightarrow> reflexive x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linear x \<Longrightarrow> reflexive x
[PROOF STEP]
by (metis one_inf_conv inf.distrib_left inf.cobounded2 inf.orderE reflexive_top_closed sup.idem)


[STATEMENT]
lemma linear_conv_closed:
  "linear x \<Longrightarrow> linear (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linear x \<Longrightarrow> linear (x\<^sup>T)
[PROOF STEP]
by (simp add: sup_commute)


[STATEMENT]
lemma linear_comp_closed:
  assumes "linear x"
      and "linear y"
    shows "linear (x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linear (x * y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. linear (x * y)
[PROOF STEP]
have "reflexive y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reflexive y
[PROOF STEP]
by (simp add: assms(2) linear_reflexive)
[PROOF STATE]
proof (state)
this:
reflexive y

goal (1 subgoal):
 1. linear (x * y)
[PROOF STEP]
hence "x \<squnion> x\<^sup>T \<le> x * y \<squnion> y\<^sup>T * x\<^sup>T"
[PROOF STATE]
proof (prove)
using this:
reflexive y

goal (1 subgoal):
 1. x \<squnion> x\<^sup>T \<le> x * y \<squnion> y\<^sup>T * x\<^sup>T
[PROOF STEP]
by (metis case_split_left case_split_right le_supI sup.cobounded1 sup.cobounded2 sup.idem reflexive_conv_closed)
[PROOF STATE]
proof (state)
this:
x \<squnion> x\<^sup>T \<le> x * y \<squnion> y\<^sup>T * x\<^sup>T

goal (1 subgoal):
 1. linear (x * y)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<squnion> x\<^sup>T \<le> x * y \<squnion> y\<^sup>T * x\<^sup>T

goal (1 subgoal):
 1. linear (x * y)
[PROOF STEP]
by (simp add: assms(1) conv_dist_comp top_le)
[PROOF STATE]
proof (state)
this:
linear (x * y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma equivalence_one_closed:
  "equivalence 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (coreflexive (1::'a) \<and> transitive (1::'a)) \<and> symmetric (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma equivalence_top_closed:
  "equivalence top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equivalence top
[PROOF STEP]
by simp


[STATEMENT]
lemma equivalence_inf_closed:
  "equivalence x \<Longrightarrow> equivalence y \<Longrightarrow> equivalence (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equivalence x; equivalence y\<rbrakk> \<Longrightarrow> equivalence (x \<sqinter> y)
[PROOF STEP]
using conv_dist_inf preorder_inf_closed
[PROOF STATE]
proof (prove)
using this:
(?x \<sqinter> ?y)\<^sup>T = ?x\<^sup>T \<sqinter> ?y\<^sup>T
\<lbrakk>preorder ?x; preorder ?y\<rbrakk> \<Longrightarrow> preorder (?x \<sqinter> ?y)

goal (1 subgoal):
 1. \<lbrakk>equivalence x; equivalence y\<rbrakk> \<Longrightarrow> equivalence (x \<sqinter> y)
[PROOF STEP]
by auto


[STATEMENT]
lemma equivalence_conv_closed:
  "equivalence x \<Longrightarrow> equivalence (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equivalence x \<Longrightarrow> equivalence (x\<^sup>T)
[PROOF STEP]
by simp


[STATEMENT]
lemma order_one_closed:
  "order 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (coreflexive (1::'a) \<and> transitive (1::'a)) \<and> antisymmetric (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma order_inf_closed:
  "order x \<Longrightarrow> order y \<Longrightarrow> order (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>order x; order y\<rbrakk> \<Longrightarrow> order (x \<sqinter> y)
[PROOF STEP]
using antisymmetric_inf_closed transitive_inf_closed
[PROOF STATE]
proof (prove)
using this:
antisymmetric ?x \<Longrightarrow> antisymmetric (?x \<sqinter> ?y)
\<lbrakk>transitive ?x; transitive ?y\<rbrakk> \<Longrightarrow> transitive (?x \<sqinter> ?y)

goal (1 subgoal):
 1. \<lbrakk>order x; order y\<rbrakk> \<Longrightarrow> order (x \<sqinter> y)
[PROOF STEP]
by auto


[STATEMENT]
lemma order_conv_closed:
  "order x \<Longrightarrow> order (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order x \<Longrightarrow> order (x\<^sup>T)
[PROOF STEP]
by (simp add: inf_commute reflexive_conv_closed transitive_conv_closed)


[STATEMENT]
lemma linear_order_conv_closed:
  "linear_order x \<Longrightarrow> linear_order (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_distrib_allegory_signature_class.linear_order x \<Longrightarrow> bounded_distrib_allegory_signature_class.linear_order (x\<^sup>T)
[PROOF STEP]
using equivalence_top_closed conv_dist_sup inf_commute reflexive_conv_closed transitive_conv_closed
[PROOF STATE]
proof (prove)
using this:
equivalence top
(?x \<squnion> ?y)\<^sup>T = ?x\<^sup>T \<squnion> ?y\<^sup>T
?x \<sqinter> ?y = ?y \<sqinter> ?x
reflexive ?x \<Longrightarrow> reflexive (?x\<^sup>T)
transitive ?x \<Longrightarrow> transitive (?x\<^sup>T)

goal (1 subgoal):
 1. bounded_distrib_allegory_signature_class.linear_order x \<Longrightarrow> bounded_distrib_allegory_signature_class.linear_order (x\<^sup>T)
[PROOF STEP]
by force


[STATEMENT]
lemma equivalence_comp_dist_inf:
  "equivalence x \<Longrightarrow> x * y \<sqinter> x * z = x * (y \<sqinter> x * z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equivalence x \<Longrightarrow> x * y \<sqinter> x * z = x * (y \<sqinter> x * z)
[PROOF STEP]
by (metis order.antisym comp_right_subdist_inf dedekind_1 order.eq_iff inf.absorb1 inf.absorb2 mult_1_right mult_assoc)


[STATEMENT]
lemma coreflexive_comp_top_inf:
  "coreflexive x \<Longrightarrow> x * top \<sqinter> y = x * y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive x \<Longrightarrow> x * top \<sqinter> y = x * y
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. coreflexive x \<Longrightarrow> x * top \<sqinter> y \<le> x * y
 2. coreflexive x \<Longrightarrow> x * y \<le> x * top \<sqinter> y
[PROOF STEP]
apply (metis comp_left_isotone comp_left_one coreflexive_symmetric dedekind_1 inf_top_left order_trans)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive x \<Longrightarrow> x * y \<le> x * top \<sqinter> y
[PROOF STEP]
using comp_left_isotone comp_right_isotone
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> ?x * ?z \<le> ?y * ?z
?x \<le> ?y \<Longrightarrow> ?z * ?x \<le> ?z * ?y

goal (1 subgoal):
 1. coreflexive x \<Longrightarrow> x * y \<le> x * top \<sqinter> y
[PROOF STEP]
by fastforce


[STATEMENT]
lemma coreflexive_comp_top_inf_one:
  "coreflexive x \<Longrightarrow> x * top \<sqinter> 1 = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive x \<Longrightarrow> x * top \<sqinter> (1::'a) = x
[PROOF STEP]
by (simp add: coreflexive_comp_top_inf)


[STATEMENT]
lemma coreflexive_comp_inf:
  "coreflexive x \<Longrightarrow> coreflexive y \<Longrightarrow> x * y = x \<sqinter> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>coreflexive x; coreflexive y\<rbrakk> \<Longrightarrow> x * y = x \<sqinter> y
[PROOF STEP]
by (metis (full_types) coreflexive_comp_top_inf coreflexive_comp_top_inf_one inf.mult_assoc inf.absorb2)


[STATEMENT]
lemma coreflexive_comp_inf_comp:
  assumes "coreflexive x"
      and "coreflexive y"
    shows "(x * z) \<sqinter> (y * z) = (x \<sqinter> y) * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * z \<sqinter> y * z = (x \<sqinter> y) * z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x * z \<sqinter> y * z = (x \<sqinter> y) * z
[PROOF STEP]
have "(x * z) \<sqinter> (y * z) = x * top \<sqinter> z \<sqinter> y * top \<sqinter> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * z \<sqinter> y * z = x * top \<sqinter> z \<sqinter> y * top \<sqinter> z
[PROOF STEP]
using assms coreflexive_comp_top_inf inf_assoc
[PROOF STATE]
proof (prove)
using this:
coreflexive x
coreflexive y
coreflexive ?x \<Longrightarrow> ?x * top \<sqinter> ?y = ?x * ?y
?x \<sqinter> ?y \<sqinter> ?z = ?x \<sqinter> (?y \<sqinter> ?z)

goal (1 subgoal):
 1. x * z \<sqinter> y * z = x * top \<sqinter> z \<sqinter> y * top \<sqinter> z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x * z \<sqinter> y * z = x * top \<sqinter> z \<sqinter> y * top \<sqinter> z

goal (1 subgoal):
 1. x * z \<sqinter> y * z = (x \<sqinter> y) * z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x * z \<sqinter> y * z = x * top \<sqinter> z \<sqinter> y * top \<sqinter> z

goal (1 subgoal):
 1. x * z \<sqinter> y * z = (x \<sqinter> y) * z
[PROOF STEP]
have "... = x * top \<sqinter> y * top \<sqinter> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * top \<sqinter> z \<sqinter> y * top \<sqinter> z = x * top \<sqinter> y * top \<sqinter> z
[PROOF STEP]
by (simp add: inf.commute inf.left_commute)
[PROOF STATE]
proof (state)
this:
x * top \<sqinter> z \<sqinter> y * top \<sqinter> z = x * top \<sqinter> y * top \<sqinter> z

goal (1 subgoal):
 1. x * z \<sqinter> y * z = (x \<sqinter> y) * z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x * top \<sqinter> z \<sqinter> y * top \<sqinter> z = x * top \<sqinter> y * top \<sqinter> z

goal (1 subgoal):
 1. x * z \<sqinter> y * z = (x \<sqinter> y) * z
[PROOF STEP]
have "... = (x \<sqinter> y) * top \<sqinter> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * top \<sqinter> y * top \<sqinter> z = (x \<sqinter> y) * top \<sqinter> z
[PROOF STEP]
by (metis assms coreflexive_comp_inf coreflexive_comp_top_inf mult_assoc)
[PROOF STATE]
proof (state)
this:
x * top \<sqinter> y * top \<sqinter> z = (x \<sqinter> y) * top \<sqinter> z

goal (1 subgoal):
 1. x * z \<sqinter> y * z = (x \<sqinter> y) * z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x * top \<sqinter> y * top \<sqinter> z = (x \<sqinter> y) * top \<sqinter> z

goal (1 subgoal):
 1. x * z \<sqinter> y * z = (x \<sqinter> y) * z
[PROOF STEP]
have "... = (x \<sqinter> y) * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqinter> y) * top \<sqinter> z = (x \<sqinter> y) * z
[PROOF STEP]
by (simp add: assms(1) coreflexive_comp_top_inf coreflexive_inf_closed)
[PROOF STATE]
proof (state)
this:
(x \<sqinter> y) * top \<sqinter> z = (x \<sqinter> y) * z

goal (1 subgoal):
 1. x * z \<sqinter> y * z = (x \<sqinter> y) * z
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x * z \<sqinter> y * z = (x \<sqinter> y) * z
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x * z \<sqinter> y * z = (x \<sqinter> y) * z

goal (1 subgoal):
 1. x * z \<sqinter> y * z = (x \<sqinter> y) * z
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x * z \<sqinter> y * z = (x \<sqinter> y) * z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma test_comp_test_inf:
  "(x \<sqinter> 1) * y * (z \<sqinter> 1) = (x \<sqinter> 1) * y \<sqinter> y * (z \<sqinter> 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqinter> (1::'a)) * y * (z \<sqinter> (1::'a)) = (x \<sqinter> (1::'a)) * y \<sqinter> y * (z \<sqinter> (1::'a))
[PROOF STEP]
by (smt comp_right_one comp_right_subdist_inf coreflexive_comp_top_inf inf.left_commute inf.orderE inf_le2 mult_assoc)


[STATEMENT]
lemma test_comp_test_top:
  "y \<sqinter> (x \<sqinter> 1) * top * (z \<sqinter> 1) = (x \<sqinter> 1) * y * (z \<sqinter> 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<sqinter> (x \<sqinter> (1::'a)) * top * (z \<sqinter> (1::'a)) = (x \<sqinter> (1::'a)) * y * (z \<sqinter> (1::'a))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<sqinter> (x \<sqinter> (1::'a)) * top * (z \<sqinter> (1::'a)) = (x \<sqinter> (1::'a)) * y * (z \<sqinter> (1::'a))
[PROOF STEP]
have "\<forall>u v . (v \<sqinter> u\<^sup>T)\<^sup>T = v\<^sup>T \<sqinter> u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>u v. (v \<sqinter> u\<^sup>T)\<^sup>T = v\<^sup>T \<sqinter> u
[PROOF STEP]
using conv_dist_inf
[PROOF STATE]
proof (prove)
using this:
(?x \<sqinter> ?y)\<^sup>T = ?x\<^sup>T \<sqinter> ?y\<^sup>T

goal (1 subgoal):
 1. \<forall>u v. (v \<sqinter> u\<^sup>T)\<^sup>T = v\<^sup>T \<sqinter> u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>u v. (v \<sqinter> u\<^sup>T)\<^sup>T = v\<^sup>T \<sqinter> u

goal (1 subgoal):
 1. y \<sqinter> (x \<sqinter> (1::'a)) * top * (z \<sqinter> (1::'a)) = (x \<sqinter> (1::'a)) * y * (z \<sqinter> (1::'a))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>u v. (v \<sqinter> u\<^sup>T)\<^sup>T = v\<^sup>T \<sqinter> u

goal (1 subgoal):
 1. y \<sqinter> (x \<sqinter> (1::'a)) * top * (z \<sqinter> (1::'a)) = (x \<sqinter> (1::'a)) * y * (z \<sqinter> (1::'a))
[PROOF STEP]
by (smt conv_dist_comp conv_involutive coreflexive_comp_top_inf inf.cobounded2 inf.left_commute inf.sup_monoid.add_commute symmetric_one_closed mult_assoc symmetric_top_closed)
[PROOF STATE]
proof (state)
this:
y \<sqinter> (x \<sqinter> (1::'a)) * top * (z \<sqinter> (1::'a)) = (x \<sqinter> (1::'a)) * y * (z \<sqinter> (1::'a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma coreflexive_idempotent:
  "coreflexive x \<Longrightarrow> idempotent x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive x \<Longrightarrow> idempotent x
[PROOF STEP]
by (simp add: coreflexive_comp_inf)


[STATEMENT]
lemma coreflexive_univalent:
  "coreflexive x \<Longrightarrow> univalent x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive x \<Longrightarrow> univalent x
[PROOF STEP]
by (simp add: coreflexive_idempotent coreflexive_symmetric)


[STATEMENT]
lemma coreflexive_injective:
  "coreflexive x \<Longrightarrow> injective x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive x \<Longrightarrow> injective x
[PROOF STEP]
by (simp add: coreflexive_idempotent coreflexive_symmetric)


[STATEMENT]
lemma coreflexive_commutative:
  "coreflexive x \<Longrightarrow> coreflexive y \<Longrightarrow> x * y = y * x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>coreflexive x; coreflexive y\<rbrakk> \<Longrightarrow> x * y = y * x
[PROOF STEP]
by (simp add: coreflexive_comp_inf inf.commute)


[STATEMENT]
lemma coreflexive_dedekind:
  "coreflexive x \<Longrightarrow> coreflexive y \<Longrightarrow> coreflexive z \<Longrightarrow> x * y \<sqinter> z \<le> x * (y \<sqinter> x * z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>coreflexive x; coreflexive y; coreflexive z\<rbrakk> \<Longrightarrow> x * y \<sqinter> z \<le> x * (y \<sqinter> x * z)
[PROOF STEP]
by (simp add: coreflexive_comp_inf inf.coboundedI1 inf.left_commute)


[STATEMENT]
lemma dedekind_eq:
  "x * y \<sqinter> z = (x \<sqinter> (z * y\<^sup>T)) * (y \<sqinter> (x\<^sup>T * z)) \<sqinter> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y \<sqinter> z = (x \<sqinter> z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z
[PROOF STEP]
proof (rule order.antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x * y \<sqinter> z \<le> (x \<sqinter> z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z
 2. (x \<sqinter> z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z \<le> x * y \<sqinter> z
[PROOF STEP]
have "x * y \<sqinter> z \<le> x * (y \<sqinter> (x\<^sup>T * z)) \<sqinter> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y \<sqinter> z \<le> x * (y \<sqinter> x\<^sup>T * z) \<sqinter> z
[PROOF STEP]
by (simp add: dedekind_1)
[PROOF STATE]
proof (state)
this:
x * y \<sqinter> z \<le> x * (y \<sqinter> x\<^sup>T * z) \<sqinter> z

goal (2 subgoals):
 1. x * y \<sqinter> z \<le> (x \<sqinter> z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z
 2. (x \<sqinter> z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z \<le> x * y \<sqinter> z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x * y \<sqinter> z \<le> x * (y \<sqinter> x\<^sup>T * z) \<sqinter> z

goal (2 subgoals):
 1. x * y \<sqinter> z \<le> (x \<sqinter> z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z
 2. (x \<sqinter> z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z \<le> x * y \<sqinter> z
[PROOF STEP]
have "... \<le> (x \<sqinter> (z * (y \<sqinter> (x\<^sup>T * z))\<^sup>T)) * (y \<sqinter> (x\<^sup>T * z)) \<sqinter> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * (y \<sqinter> x\<^sup>T * z) \<sqinter> z \<le> (x \<sqinter> z * (y \<sqinter> x\<^sup>T * z)\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z
[PROOF STEP]
by (simp add: dedekind_2)
[PROOF STATE]
proof (state)
this:
x * (y \<sqinter> x\<^sup>T * z) \<sqinter> z \<le> (x \<sqinter> z * (y \<sqinter> x\<^sup>T * z)\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z

goal (2 subgoals):
 1. x * y \<sqinter> z \<le> (x \<sqinter> z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z
 2. (x \<sqinter> z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z \<le> x * y \<sqinter> z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x * (y \<sqinter> x\<^sup>T * z) \<sqinter> z \<le> (x \<sqinter> z * (y \<sqinter> x\<^sup>T * z)\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z

goal (2 subgoals):
 1. x * y \<sqinter> z \<le> (x \<sqinter> z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z
 2. (x \<sqinter> z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z \<le> x * y \<sqinter> z
[PROOF STEP]
have "... \<le> (x \<sqinter> (z * y\<^sup>T)) * (y \<sqinter> (x\<^sup>T * z)) \<sqinter> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqinter> z * (y \<sqinter> x\<^sup>T * z)\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z \<le> (x \<sqinter> z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z
[PROOF STEP]
by (metis comp_left_isotone comp_right_isotone inf_mono conv_order inf.cobounded1 order_refl)
[PROOF STATE]
proof (state)
this:
(x \<sqinter> z * (y \<sqinter> x\<^sup>T * z)\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z \<le> (x \<sqinter> z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z

goal (2 subgoals):
 1. x * y \<sqinter> z \<le> (x \<sqinter> z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z
 2. (x \<sqinter> z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z \<le> x * y \<sqinter> z
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x * y \<sqinter> z \<le> (x \<sqinter> z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z
[PROOF STEP]
show "x * y \<sqinter> z \<le> (x \<sqinter> (z * y\<^sup>T)) * (y \<sqinter> (x\<^sup>T * z)) \<sqinter> z"
[PROOF STATE]
proof (prove)
using this:
x * y \<sqinter> z \<le> (x \<sqinter> z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z

goal (1 subgoal):
 1. x * y \<sqinter> z \<le> (x \<sqinter> z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x * y \<sqinter> z \<le> (x \<sqinter> z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z

goal (1 subgoal):
 1. (x \<sqinter> z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z \<le> x * y \<sqinter> z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x \<sqinter> z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z \<le> x * y \<sqinter> z
[PROOF STEP]
show "(x \<sqinter> (z * y\<^sup>T)) * (y \<sqinter> (x\<^sup>T * z)) \<sqinter> z \<le> x * y \<sqinter> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqinter> z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z \<le> x * y \<sqinter> z
[PROOF STEP]
using comp_isotone inf.sup_left_isotone
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<le> ?y; ?w \<le> ?z\<rbrakk> \<Longrightarrow> ?x * ?w \<le> ?y * ?z
?y \<le> ?x \<Longrightarrow> ?y \<sqinter> ?z \<le> ?x \<sqinter> ?z

goal (1 subgoal):
 1. (x \<sqinter> z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z \<le> x * y \<sqinter> z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x \<sqinter> z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * z) \<sqinter> z \<le> x * y \<sqinter> z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dedekind:
  "x * y \<sqinter> z \<le> (x \<sqinter> (z * y\<^sup>T)) * (y \<sqinter> (x\<^sup>T * z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y \<sqinter> z \<le> (x \<sqinter> z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * z)
[PROOF STEP]
by (metis dedekind_eq inf.cobounded1)


[STATEMENT]
lemma vector_export_comp:
  "(x * top \<sqinter> y) * z = x * top \<sqinter> y * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * top \<sqinter> y) * z = x * top \<sqinter> y * z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x * top \<sqinter> y) * z = x * top \<sqinter> y * z
[PROOF STEP]
have "vector (x * top)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector (x * top)
[PROOF STEP]
by (simp add: comp_associative)
[PROOF STATE]
proof (state)
this:
vector (x * top)

goal (1 subgoal):
 1. (x * top \<sqinter> y) * z = x * top \<sqinter> y * z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
vector (x * top)

goal (1 subgoal):
 1. (x * top \<sqinter> y) * z = x * top \<sqinter> y * z
[PROOF STEP]
by (simp add: vector_inf_comp)
[PROOF STATE]
proof (state)
this:
(x * top \<sqinter> y) * z = x * top \<sqinter> y * z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vector_export_comp_unit:
  "(x * top \<sqinter> 1) * y = x * top \<sqinter> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * top \<sqinter> (1::'a)) * y = x * top \<sqinter> y
[PROOF STEP]
by (simp add: vector_export_comp)


[STATEMENT]
lemma ex231a [simp]:
  "(1 \<sqinter> x * x\<^sup>T) * x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((1::'a) \<sqinter> x * x\<^sup>T) * x = x
[PROOF STEP]
by (metis inf.cobounded1 inf.idem inf_right_idem comp_left_one conv_one coreflexive_comp_top_inf dedekind_eq)


[STATEMENT]
lemma ex231b [simp]:
  "x * (1 \<sqinter> x\<^sup>T * x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * ((1::'a) \<sqinter> x\<^sup>T * x) = x
[PROOF STEP]
by (metis conv_dist_comp conv_dist_inf conv_involutive conv_one ex231a)


[STATEMENT]
lemma ex231c:
  "x \<le> x * x\<^sup>T * x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> x * x\<^sup>T * x
[PROOF STEP]
by (metis comp_left_isotone ex231a inf_le2)


[STATEMENT]
lemma ex231d:
  "x \<le> x * top * x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> x * top * x
[PROOF STEP]
by (metis comp_left_isotone comp_right_isotone top_greatest order_trans ex231c)


[STATEMENT]
lemma ex231e [simp]:
  "x * top * x * top = x * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * top * x * top = x * top
[PROOF STEP]
by (metis ex231d order.antisym comp_associative mult_right_isotone top.extremum)


[STATEMENT]
lemma arc_injective:
  "arc x \<Longrightarrow> injective x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arc x \<Longrightarrow> injective x
[PROOF STEP]
by (metis conv_dist_inf conv_involutive inf.absorb2 top_right_mult_increasing univalent_inf_closed)


[STATEMENT]
lemma arc_conv_closed:
  "arc x \<Longrightarrow> arc (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arc x \<Longrightarrow> arc (x\<^sup>T)
[PROOF STEP]
by simp


[STATEMENT]
lemma arc_univalent:
  "arc x \<Longrightarrow> univalent x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arc x \<Longrightarrow> univalent x
[PROOF STEP]
using arc_conv_closed arc_injective univalent_conv_injective
[PROOF STATE]
proof (prove)
using this:
arc ?x \<Longrightarrow> arc (?x\<^sup>T)
arc ?x \<Longrightarrow> injective ?x
univalent ?x = injective (?x\<^sup>T)

goal (1 subgoal):
 1. arc x \<Longrightarrow> univalent x
[PROOF STEP]
by blast


[STATEMENT]
lemma injective_codomain:
  assumes "injective x"
  shows "x * (x \<sqinter> 1) = x \<sqinter> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * (x \<sqinter> (1::'a)) = x \<sqinter> (1::'a)
[PROOF STEP]
proof (rule order.antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x * (x \<sqinter> (1::'a)) \<le> x \<sqinter> (1::'a)
 2. x \<sqinter> (1::'a) \<le> x * (x \<sqinter> (1::'a))
[PROOF STEP]
show "x * (x \<sqinter> 1) \<le> x \<sqinter> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * (x \<sqinter> (1::'a)) \<le> x \<sqinter> (1::'a)
[PROOF STEP]
by (metis assms comp_right_one dual_order.trans inf.boundedI inf.cobounded1 inf.sup_monoid.add_commute mult_right_isotone one_inf_conv)
[PROOF STATE]
proof (state)
this:
x * (x \<sqinter> (1::'a)) \<le> x \<sqinter> (1::'a)

goal (1 subgoal):
 1. x \<sqinter> (1::'a) \<le> x * (x \<sqinter> (1::'a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<sqinter> (1::'a) \<le> x * (x \<sqinter> (1::'a))
[PROOF STEP]
show "x \<sqinter> 1 \<le> x * (x \<sqinter> 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqinter> (1::'a) \<le> x * (x \<sqinter> (1::'a))
[PROOF STEP]
by (metis coreflexive_idempotent inf.cobounded1 inf.cobounded2 mult_left_isotone)
[PROOF STATE]
proof (state)
this:
x \<sqinter> (1::'a) \<le> x * (x \<sqinter> (1::'a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma injective_sup:
  assumes "injective t"
      and "e * t\<^sup>T \<le> 1"
      and "injective e"
    shows "injective (t \<squnion> e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. injective (t \<squnion> e)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. injective (t \<squnion> e)
[PROOF STEP]
have "(t \<squnion> e) * (t \<squnion> e)\<^sup>T = t * t\<^sup>T \<squnion> t * e\<^sup>T \<squnion> e * t\<^sup>T \<squnion> e * e\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t \<squnion> e) * (t \<squnion> e)\<^sup>T = t * t\<^sup>T \<squnion> t * e\<^sup>T \<squnion> e * t\<^sup>T \<squnion> e * e\<^sup>T
[PROOF STEP]
by (simp add: comp_left_dist_sup conv_dist_sup semiring.distrib_right sup.assoc)
[PROOF STATE]
proof (state)
this:
(t \<squnion> e) * (t \<squnion> e)\<^sup>T = t * t\<^sup>T \<squnion> t * e\<^sup>T \<squnion> e * t\<^sup>T \<squnion> e * e\<^sup>T

goal (1 subgoal):
 1. injective (t \<squnion> e)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(t \<squnion> e) * (t \<squnion> e)\<^sup>T = t * t\<^sup>T \<squnion> t * e\<^sup>T \<squnion> e * t\<^sup>T \<squnion> e * e\<^sup>T

goal (1 subgoal):
 1. injective (t \<squnion> e)
[PROOF STEP]
using assms coreflexive_symmetric conv_dist_comp
[PROOF STATE]
proof (prove)
using this:
(t \<squnion> e) * (t \<squnion> e)\<^sup>T = t * t\<^sup>T \<squnion> t * e\<^sup>T \<squnion> e * t\<^sup>T \<squnion> e * e\<^sup>T
injective t
coreflexive (e * t\<^sup>T)
injective e
coreflexive ?x \<Longrightarrow> symmetric ?x
(?x * ?y)\<^sup>T = ?y\<^sup>T * ?x\<^sup>T

goal (1 subgoal):
 1. injective (t \<squnion> e)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
injective (t \<squnion> e)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma injective_inv:
  "injective t \<Longrightarrow> e * t\<^sup>T = bot \<Longrightarrow> arc e \<Longrightarrow> injective (t \<squnion> e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>injective t; e * t\<^sup>T = bot; arc e\<rbrakk> \<Longrightarrow> injective (t \<squnion> e)
[PROOF STEP]
using arc_injective injective_sup bot_least
[PROOF STATE]
proof (prove)
using this:
arc ?x \<Longrightarrow> injective ?x
\<lbrakk>injective ?t; coreflexive (?e * ?t\<^sup>T); injective ?e\<rbrakk> \<Longrightarrow> injective (?t \<squnion> ?e)
bot \<le> ?a

goal (1 subgoal):
 1. \<lbrakk>injective t; e * t\<^sup>T = bot; arc e\<rbrakk> \<Longrightarrow> injective (t \<squnion> e)
[PROOF STEP]
by blast


[STATEMENT]
lemma univalent_sup:
  "univalent t \<Longrightarrow> e\<^sup>T * t \<le> 1 \<Longrightarrow> univalent e \<Longrightarrow> univalent (t \<squnion> e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>univalent t; coreflexive (e\<^sup>T * t); univalent e\<rbrakk> \<Longrightarrow> univalent (t \<squnion> e)
[PROOF STEP]
by (metis injective_sup conv_dist_sup conv_involutive)


[STATEMENT]
lemma point_injective:
  "arc x \<Longrightarrow> x\<^sup>T * top * x \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arc x \<Longrightarrow> coreflexive (x\<^sup>T * top * x)
[PROOF STEP]
by (metis conv_top comp_associative conv_dist_comp conv_involutive vector_top_closed)


[STATEMENT]
lemma vv_transitive:
  "vector v \<Longrightarrow> (v * v\<^sup>T) * (v * v\<^sup>T) \<le> v * v\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector v \<Longrightarrow> transitive (v * v\<^sup>T)
[PROOF STEP]
by (metis comp_associative comp_left_isotone comp_right_isotone top_greatest)


[STATEMENT]
lemma epm_3:
  assumes "e \<le> w"
      and "injective w"
    shows "e = w \<sqinter> top * e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e = w \<sqinter> top * e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. e = w \<sqinter> top * e
[PROOF STEP]
have "w \<sqinter> top * e \<le> w * e\<^sup>T * e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<sqinter> top * e \<le> w * e\<^sup>T * e
[PROOF STEP]
by (metis (no_types, lifting) inf.absorb2 top.extremum dedekind_2 inf.commute)
[PROOF STATE]
proof (state)
this:
w \<sqinter> top * e \<le> w * e\<^sup>T * e

goal (1 subgoal):
 1. e = w \<sqinter> top * e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
w \<sqinter> top * e \<le> w * e\<^sup>T * e

goal (1 subgoal):
 1. e = w \<sqinter> top * e
[PROOF STEP]
have "... \<le> w * w\<^sup>T * e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w * e\<^sup>T * e \<le> w * w\<^sup>T * e
[PROOF STEP]
by (simp add: assms(1) conv_isotone mult_left_isotone mult_right_isotone)
[PROOF STATE]
proof (state)
this:
w * e\<^sup>T * e \<le> w * w\<^sup>T * e

goal (1 subgoal):
 1. e = w \<sqinter> top * e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
w * e\<^sup>T * e \<le> w * w\<^sup>T * e

goal (1 subgoal):
 1. e = w \<sqinter> top * e
[PROOF STEP]
have "... \<le> e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w * w\<^sup>T * e \<le> e
[PROOF STEP]
using assms(2) coreflexive_comp_top_inf inf.sup_right_divisibility
[PROOF STATE]
proof (prove)
using this:
injective w
coreflexive ?x \<Longrightarrow> ?x * top \<sqinter> ?y = ?x * ?y
(?y \<le> ?x) = (\<exists>z. z \<sqinter> ?x = ?y)

goal (1 subgoal):
 1. w * w\<^sup>T * e \<le> e
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
w * w\<^sup>T * e \<le> e

goal (1 subgoal):
 1. e = w \<sqinter> top * e
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
w \<sqinter> top * e \<le> e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
w \<sqinter> top * e \<le> e

goal (1 subgoal):
 1. e = w \<sqinter> top * e
[PROOF STEP]
by (simp add: assms(1) top_left_mult_increasing order.antisym)
[PROOF STATE]
proof (state)
this:
e = w \<sqinter> top * e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma comp_inf_vector:
  "x * (y \<sqinter> z * top) = (x \<sqinter> top * z\<^sup>T) * y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * (y \<sqinter> z * top) = (x \<sqinter> top * z\<^sup>T) * y
[PROOF STEP]
by (metis conv_top covector_inf_comp_3 comp_associative conv_dist_comp inf.commute vector_top_closed)


[STATEMENT]
lemma inf_vector_comp:
  "(x \<sqinter> y * top) * z = y * top \<sqinter> x * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqinter> y * top) * z = y * top \<sqinter> x * z
[PROOF STEP]
using inf.commute vector_export_comp
[PROOF STATE]
proof (prove)
using this:
?a \<sqinter> ?b = ?b \<sqinter> ?a
(?x * top \<sqinter> ?y) * ?z = ?x * top \<sqinter> ?y * ?z

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


[STATEMENT]
lemma comp_inf_covector:
  "x * (y \<sqinter> top * z) = x * y \<sqinter> top * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * (y \<sqinter> top * z) = x * y \<sqinter> top * z
[PROOF STEP]
by (simp add: covector_comp_inf covector_mult_closed)


[STATEMENT]
lemma univalent_comp_left_dist_inf:
  assumes "univalent x"
    shows "x * (y \<sqinter> z) = x * y \<sqinter> x * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * (y \<sqinter> z) = x * y \<sqinter> x * z
[PROOF STEP]
proof (rule order.antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x * (y \<sqinter> z) \<le> x * y \<sqinter> x * z
 2. x * y \<sqinter> x * z \<le> x * (y \<sqinter> z)
[PROOF STEP]
show "x * (y \<sqinter> z) \<le> x * y \<sqinter> x * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * (y \<sqinter> z) \<le> x * y \<sqinter> x * z
[PROOF STEP]
by (simp add: comp_right_isotone)
[PROOF STATE]
proof (state)
this:
x * (y \<sqinter> z) \<le> x * y \<sqinter> x * z

goal (1 subgoal):
 1. x * y \<sqinter> x * z \<le> x * (y \<sqinter> z)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x * y \<sqinter> x * z \<le> x * (y \<sqinter> z)
[PROOF STEP]
have "x * y \<sqinter> x * z \<le> (x \<sqinter> x * z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * x * z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y \<sqinter> x * z \<le> (x \<sqinter> x * z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * x * z)
[PROOF STEP]
by (metis comp_associative dedekind)
[PROOF STATE]
proof (state)
this:
x * y \<sqinter> x * z \<le> (x \<sqinter> x * z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * x * z)

goal (1 subgoal):
 1. x * y \<sqinter> x * z \<le> x * (y \<sqinter> z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x * y \<sqinter> x * z \<le> (x \<sqinter> x * z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * x * z)

goal (1 subgoal):
 1. x * y \<sqinter> x * z \<le> x * (y \<sqinter> z)
[PROOF STEP]
have "... \<le> x * (y \<sqinter> x\<^sup>T * x * z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqinter> x * z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * x * z) \<le> x * (y \<sqinter> x\<^sup>T * x * z)
[PROOF STEP]
by (simp add: comp_left_isotone)
[PROOF STATE]
proof (state)
this:
(x \<sqinter> x * z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * x * z) \<le> x * (y \<sqinter> x\<^sup>T * x * z)

goal (1 subgoal):
 1. x * y \<sqinter> x * z \<le> x * (y \<sqinter> z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x \<sqinter> x * z * y\<^sup>T) * (y \<sqinter> x\<^sup>T * x * z) \<le> x * (y \<sqinter> x\<^sup>T * x * z)

goal (1 subgoal):
 1. x * y \<sqinter> x * z \<le> x * (y \<sqinter> z)
[PROOF STEP]
have "... \<le> x * (y \<sqinter> 1 * z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * (y \<sqinter> x\<^sup>T * x * z) \<le> x * (y \<sqinter> (1::'a) * z)
[PROOF STEP]
using assms comp_left_isotone comp_right_isotone inf.sup_right_isotone
[PROOF STATE]
proof (prove)
using this:
univalent x
?x \<le> ?y \<Longrightarrow> ?x * ?z \<le> ?y * ?z
?x \<le> ?y \<Longrightarrow> ?z * ?x \<le> ?z * ?y
?y \<le> ?x \<Longrightarrow> ?z \<sqinter> ?y \<le> ?z \<sqinter> ?x

goal (1 subgoal):
 1. x * (y \<sqinter> x\<^sup>T * x * z) \<le> x * (y \<sqinter> (1::'a) * z)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x * (y \<sqinter> x\<^sup>T * x * z) \<le> x * (y \<sqinter> (1::'a) * z)

goal (1 subgoal):
 1. x * y \<sqinter> x * z \<le> x * (y \<sqinter> z)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x * y \<sqinter> x * z \<le> x * (y \<sqinter> (1::'a) * z)
[PROOF STEP]
show "x * y \<sqinter> x * z \<le> x * (y \<sqinter> z)"
[PROOF STATE]
proof (prove)
using this:
x * y \<sqinter> x * z \<le> x * (y \<sqinter> (1::'a) * z)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma injective_comp_right_dist_inf:
  "injective z \<Longrightarrow> (x \<sqinter> y) * z = x * z \<sqinter> y * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. injective z \<Longrightarrow> (x \<sqinter> y) * z = x * z \<sqinter> y * z
[PROOF STEP]
by (metis univalent_comp_left_dist_inf conv_dist_comp conv_involutive conv_dist_inf)


[STATEMENT]
lemma vector_covector:
  "vector v \<Longrightarrow> vector w \<Longrightarrow> v \<sqinter> w\<^sup>T = v * w\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vector v; vector w\<rbrakk> \<Longrightarrow> v \<sqinter> w\<^sup>T = v * w\<^sup>T
[PROOF STEP]
by (metis covector_comp_inf inf_top_left vector_conv_covector)


[STATEMENT]
lemma comp_inf_vector_1:
  "(x \<sqinter> top * y) * z = x * (z \<sqinter> (top * y)\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqinter> top * y) * z = x * (z \<sqinter> (top * y)\<^sup>T)
[PROOF STEP]
by (simp add: comp_inf_vector conv_dist_comp)


[STATEMENT]
lemma shunt_bijective:
  assumes "bijective z"
    shows "x \<le> y * z \<longleftrightarrow> x * z\<^sup>T \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<le> y * z) = (x * z\<^sup>T \<le> y)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<le> y * z \<Longrightarrow> x * z\<^sup>T \<le> y
 2. x * z\<^sup>T \<le> y \<Longrightarrow> x \<le> y * z
[PROOF STEP]
assume "x \<le> y * z"
[PROOF STATE]
proof (state)
this:
x \<le> y * z

goal (2 subgoals):
 1. x \<le> y * z \<Longrightarrow> x * z\<^sup>T \<le> y
 2. x * z\<^sup>T \<le> y \<Longrightarrow> x \<le> y * z
[PROOF STEP]
hence "x * z\<^sup>T \<le> y * z * z\<^sup>T"
[PROOF STATE]
proof (prove)
using this:
x \<le> y * z

goal (1 subgoal):
 1. x * z\<^sup>T \<le> y * z * z\<^sup>T
[PROOF STEP]
by (simp add: mult_left_isotone)
[PROOF STATE]
proof (state)
this:
x * z\<^sup>T \<le> y * z * z\<^sup>T

goal (2 subgoals):
 1. x \<le> y * z \<Longrightarrow> x * z\<^sup>T \<le> y
 2. x * z\<^sup>T \<le> y \<Longrightarrow> x \<le> y * z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x * z\<^sup>T \<le> y * z * z\<^sup>T

goal (2 subgoals):
 1. x \<le> y * z \<Longrightarrow> x * z\<^sup>T \<le> y
 2. x * z\<^sup>T \<le> y \<Longrightarrow> x \<le> y * z
[PROOF STEP]
have "... \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y * z * z\<^sup>T \<le> y
[PROOF STEP]
using assms comp_associative mult_right_isotone
[PROOF STATE]
proof (prove)
using this:
bijective z
?x * ?y * ?z = ?x * (?y * ?z)
?x \<le> ?y \<Longrightarrow> ?z * ?x \<le> ?z * ?y

goal (1 subgoal):
 1. y * z * z\<^sup>T \<le> y
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
y * z * z\<^sup>T \<le> y

goal (2 subgoals):
 1. x \<le> y * z \<Longrightarrow> x * z\<^sup>T \<le> y
 2. x * z\<^sup>T \<le> y \<Longrightarrow> x \<le> y * z
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x * z\<^sup>T \<le> y
[PROOF STEP]
show "x * z\<^sup>T \<le> y"
[PROOF STATE]
proof (prove)
using this:
x * z\<^sup>T \<le> y

goal (1 subgoal):
 1. x * z\<^sup>T \<le> y
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x * z\<^sup>T \<le> y

goal (1 subgoal):
 1. x * z\<^sup>T \<le> y \<Longrightarrow> x \<le> y * z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x * z\<^sup>T \<le> y \<Longrightarrow> x \<le> y * z
[PROOF STEP]
assume 1: "x * z\<^sup>T \<le> y"
[PROOF STATE]
proof (state)
this:
x * z\<^sup>T \<le> y

goal (1 subgoal):
 1. x * z\<^sup>T \<le> y \<Longrightarrow> x \<le> y * z
[PROOF STEP]
have "x = x \<sqinter> top * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = x \<sqinter> top * z
[PROOF STEP]
by (simp add: assms)
[PROOF STATE]
proof (state)
this:
x = x \<sqinter> top * z

goal (1 subgoal):
 1. x * z\<^sup>T \<le> y \<Longrightarrow> x \<le> y * z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x = x \<sqinter> top * z

goal (1 subgoal):
 1. x * z\<^sup>T \<le> y \<Longrightarrow> x \<le> y * z
[PROOF STEP]
have "... \<le> x * z\<^sup>T * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqinter> top * z \<le> x * z\<^sup>T * z
[PROOF STEP]
by (metis dedekind_2 inf_commute inf_top.right_neutral)
[PROOF STATE]
proof (state)
this:
x \<sqinter> top * z \<le> x * z\<^sup>T * z

goal (1 subgoal):
 1. x * z\<^sup>T \<le> y \<Longrightarrow> x \<le> y * z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<sqinter> top * z \<le> x * z\<^sup>T * z

goal (1 subgoal):
 1. x * z\<^sup>T \<le> y \<Longrightarrow> x \<le> y * z
[PROOF STEP]
have "... \<le> y * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * z\<^sup>T * z \<le> y * z
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
x * z\<^sup>T \<le> y

goal (1 subgoal):
 1. x * z\<^sup>T * z \<le> y * z
[PROOF STEP]
by (simp add: mult_left_isotone)
[PROOF STATE]
proof (state)
this:
x * z\<^sup>T * z \<le> y * z

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma shunt_mapping:
  "mapping z \<Longrightarrow> x \<le> z * y \<longleftrightarrow> z\<^sup>T * x \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mapping z \<Longrightarrow> (x \<le> z * y) = (z\<^sup>T * x \<le> y)
[PROOF STEP]
by (metis shunt_bijective mapping_conv_bijective conv_order conv_dist_comp conv_involutive)


[STATEMENT]
lemma bijective_reverse:
  assumes "bijective p"
      and "bijective q"
    shows "p \<le> r * q \<longleftrightarrow> q \<le> r\<^sup>T * p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<le> r * q) = (q \<le> r\<^sup>T * p)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (p \<le> r * q) = (q \<le> r\<^sup>T * p)
[PROOF STEP]
have "p \<le> r * q \<longleftrightarrow> p * q\<^sup>T \<le> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<le> r * q) = (p * q\<^sup>T \<le> r)
[PROOF STEP]
by (simp add: assms(2) shunt_bijective)
[PROOF STATE]
proof (state)
this:
(p \<le> r * q) = (p * q\<^sup>T \<le> r)

goal (1 subgoal):
 1. (p \<le> r * q) = (q \<le> r\<^sup>T * p)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(p \<le> r * q) = (p * q\<^sup>T \<le> r)

goal (1 subgoal):
 1. (p \<le> r * q) = (q \<le> r\<^sup>T * p)
[PROOF STEP]
have "... \<longleftrightarrow> q\<^sup>T \<le> p\<^sup>T * r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p * q\<^sup>T \<le> r) = (q\<^sup>T \<le> p\<^sup>T * r)
[PROOF STEP]
by (metis assms(1) conv_dist_comp conv_involutive conv_order shunt_bijective)
[PROOF STATE]
proof (state)
this:
(p * q\<^sup>T \<le> r) = (q\<^sup>T \<le> p\<^sup>T * r)

goal (1 subgoal):
 1. (p \<le> r * q) = (q \<le> r\<^sup>T * p)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(p * q\<^sup>T \<le> r) = (q\<^sup>T \<le> p\<^sup>T * r)

goal (1 subgoal):
 1. (p \<le> r * q) = (q \<le> r\<^sup>T * p)
[PROOF STEP]
have "... \<longleftrightarrow> q \<le> r\<^sup>T * p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (q\<^sup>T \<le> p\<^sup>T * r) = (q \<le> r\<^sup>T * p)
[PROOF STEP]
using conv_dist_comp conv_isotone
[PROOF STATE]
proof (prove)
using this:
(?x * ?y)\<^sup>T = ?y\<^sup>T * ?x\<^sup>T
?x \<le> ?y \<Longrightarrow> ?x\<^sup>T \<le> ?y\<^sup>T

goal (1 subgoal):
 1. (q\<^sup>T \<le> p\<^sup>T * r) = (q \<le> r\<^sup>T * p)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(q\<^sup>T \<le> p\<^sup>T * r) = (q \<le> r\<^sup>T * p)

goal (1 subgoal):
 1. (p \<le> r * q) = (q \<le> r\<^sup>T * p)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(p \<le> r * q) = (q \<le> r\<^sup>T * p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(p \<le> r * q) = (q \<le> r\<^sup>T * p)

goal (1 subgoal):
 1. (p \<le> r * q) = (q \<le> r\<^sup>T * p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(p \<le> r * q) = (q \<le> r\<^sup>T * p)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arc_expanded:
  "arc x \<longleftrightarrow> x * top * x\<^sup>T \<le> 1 \<and> x\<^sup>T * top * x \<le> 1 \<and> top * x * top = top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arc x = (coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * x))
[PROOF STEP]
by (metis conv_top comp_associative conv_dist_comp conv_involutive vector_top_closed)


[STATEMENT]
lemma arc_top_arc:
  assumes "arc x"
    shows "x * top * x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * top * x = x
[PROOF STEP]
by (metis assms epm_3 top_right_mult_increasing vector_inf_comp vector_mult_closed vector_top_closed)


[STATEMENT]
lemma arc_top_edge:
  assumes "arc x"
    shows "x\<^sup>T * top * x = x\<^sup>T * x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>T * top * x = x\<^sup>T * x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x\<^sup>T * top * x = x\<^sup>T * x
[PROOF STEP]
have "x\<^sup>T = x\<^sup>T * top \<sqinter> top * x\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>T = x\<^sup>T * top \<sqinter> top * x\<^sup>T
[PROOF STEP]
using assms epm_3 top_right_mult_increasing
[PROOF STATE]
proof (prove)
using this:
arc x
\<lbrakk>?e \<le> ?w; injective ?w\<rbrakk> \<Longrightarrow> ?e = ?w \<sqinter> top * ?e
?x \<le> ?x * top

goal (1 subgoal):
 1. x\<^sup>T = x\<^sup>T * top \<sqinter> top * x\<^sup>T
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x\<^sup>T = x\<^sup>T * top \<sqinter> top * x\<^sup>T

goal (1 subgoal):
 1. x\<^sup>T * top * x = x\<^sup>T * x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x\<^sup>T = x\<^sup>T * top \<sqinter> top * x\<^sup>T

goal (1 subgoal):
 1. x\<^sup>T * top * x = x\<^sup>T * x
[PROOF STEP]
by (metis comp_inf_vector_1 conv_dist_comp conv_involutive conv_top inf.absorb1 top_right_mult_increasing)
[PROOF STATE]
proof (state)
this:
x\<^sup>T * top * x = x\<^sup>T * x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arc_eq_1:
  assumes "arc x"
    shows "x = x * x\<^sup>T * x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = x * x\<^sup>T * x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = x * x\<^sup>T * x
[PROOF STEP]
have "x * x\<^sup>T * x \<le> x * top * x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * x\<^sup>T * x \<le> x * top * x
[PROOF STEP]
by (simp add: mult_left_isotone mult_right_isotone)
[PROOF STATE]
proof (state)
this:
x * x\<^sup>T * x \<le> x * top * x

goal (1 subgoal):
 1. x = x * x\<^sup>T * x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x * x\<^sup>T * x \<le> x * top * x

goal (1 subgoal):
 1. x = x * x\<^sup>T * x
[PROOF STEP]
have "... \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * top * x \<le> x
[PROOF STEP]
by (simp add: assms arc_top_arc)
[PROOF STATE]
proof (state)
this:
x * top * x \<le> x

goal (1 subgoal):
 1. x = x * x\<^sup>T * x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x * x\<^sup>T * x \<le> x
[PROOF STEP]
have "x * x\<^sup>T * x \<le> x"
[PROOF STATE]
proof (prove)
using this:
x * x\<^sup>T * x \<le> x

goal (1 subgoal):
 1. x * x\<^sup>T * x \<le> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x * x\<^sup>T * x \<le> x

goal (1 subgoal):
 1. x = x * x\<^sup>T * x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x * x\<^sup>T * x \<le> x

goal (1 subgoal):
 1. x = x * x\<^sup>T * x
[PROOF STEP]
by (simp add: order.antisym ex231c)
[PROOF STATE]
proof (state)
this:
x = x * x\<^sup>T * x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arc_eq_2:
  assumes "arc x"
    shows "x\<^sup>T = x\<^sup>T * x * x\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>T = x\<^sup>T * x * x\<^sup>T
[PROOF STEP]
using arc_eq_1 assms conv_involutive
[PROOF STATE]
proof (prove)
using this:
arc ?x \<Longrightarrow> ?x = ?x * ?x\<^sup>T * ?x
arc x
?x\<^sup>T\<^sup>T = ?x

goal (1 subgoal):
 1. x\<^sup>T = x\<^sup>T * x * x\<^sup>T
[PROOF STEP]
by fastforce


[STATEMENT]
lemma points_arc:
  "point x \<Longrightarrow> point y \<Longrightarrow> arc (x * y\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>point x; point y\<rbrakk> \<Longrightarrow> arc (x * y\<^sup>T)
[PROOF STEP]
by (metis comp_associative conv_dist_comp conv_involutive equivalence_top_closed)


[STATEMENT]
lemma point_arc:
  "point x \<Longrightarrow> arc (x * x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. point x \<Longrightarrow> arc (x * x\<^sup>T)
[PROOF STEP]
by (simp add: points_arc)


[STATEMENT]
lemma arc_expanded_1:
  "arc e \<Longrightarrow> e * x * e\<^sup>T \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arc e \<Longrightarrow> coreflexive (e * x * e\<^sup>T)
[PROOF STEP]
by (meson arc_expanded order_trans top_greatest mult_left_isotone mult_right_isotone)


[STATEMENT]
lemma arc_expanded_2:
  "arc e \<Longrightarrow> e\<^sup>T * x * e \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arc e \<Longrightarrow> coreflexive (e\<^sup>T * x * e)
[PROOF STEP]
by (meson arc_expanded order_trans top_greatest mult_left_isotone mult_right_isotone)


[STATEMENT]
lemma point_conv_comp:
  "point x \<Longrightarrow> x\<^sup>T * x = top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. point x \<Longrightarrow> x\<^sup>T * x = top
[PROOF STEP]
using order_eq_iff shunt_bijective top_greatest vector_conv_covector
[PROOF STATE]
proof (prove)
using this:
(?x = ?y) = (?x \<le> ?y \<and> ?y \<le> ?x)
bijective ?z \<Longrightarrow> (?x \<le> ?y * ?z) = (?x * ?z\<^sup>T \<le> ?y)
?x \<le> top
vector ?v = covector (?v\<^sup>T)

goal (1 subgoal):
 1. point x \<Longrightarrow> x\<^sup>T * x = top
[PROOF STEP]
by blast


[STATEMENT]
lemma point_antisymmetric:
  "point x \<Longrightarrow> antisymmetric x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. point x \<Longrightarrow> antisymmetric x
[PROOF STEP]
by (simp add: vector_covector)


[STATEMENT]
lemma mapping_inf_point_arc:
  assumes "mapping x"
      and "point y"
    shows "arc (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arc (x \<sqinter> y)
[PROOF STEP]
proof (unfold arc_expanded, intro conjI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. coreflexive ((x \<sqinter> y) * top * (x \<sqinter> y)\<^sup>T)
 2. coreflexive ((x \<sqinter> y)\<^sup>T * top * (x \<sqinter> y))
 3. times_top_class.total (top * (x \<sqinter> y))
[PROOF STEP]
show "(x \<sqinter> y) * top * (x \<sqinter> y)\<^sup>T \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive ((x \<sqinter> y) * top * (x \<sqinter> y)\<^sup>T)
[PROOF STEP]
by (metis assms conv_dist_comp covector_conv_vector inf.orderE inf.sup_monoid.add_commute surjective_conv_total top.extremum top_right_mult_increasing vector_export_comp)
[PROOF STATE]
proof (state)
this:
coreflexive ((x \<sqinter> y) * top * (x \<sqinter> y)\<^sup>T)

goal (2 subgoals):
 1. coreflexive ((x \<sqinter> y)\<^sup>T * top * (x \<sqinter> y))
 2. times_top_class.total (top * (x \<sqinter> y))
[PROOF STEP]
have "(x \<sqinter> y)\<^sup>T * top * (x \<sqinter> y) = x\<^sup>T * y * (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqinter> y)\<^sup>T * top * (x \<sqinter> y) = x\<^sup>T * y * (x \<sqinter> y)
[PROOF STEP]
by (simp add: assms(2) conv_dist_inf covector_inf_comp_3)
[PROOF STATE]
proof (state)
this:
(x \<sqinter> y)\<^sup>T * top * (x \<sqinter> y) = x\<^sup>T * y * (x \<sqinter> y)

goal (2 subgoals):
 1. coreflexive ((x \<sqinter> y)\<^sup>T * top * (x \<sqinter> y))
 2. times_top_class.total (top * (x \<sqinter> y))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x \<sqinter> y)\<^sup>T * top * (x \<sqinter> y) = x\<^sup>T * y * (x \<sqinter> y)

goal (2 subgoals):
 1. coreflexive ((x \<sqinter> y)\<^sup>T * top * (x \<sqinter> y))
 2. times_top_class.total (top * (x \<sqinter> y))
[PROOF STEP]
have "... = x\<^sup>T * (y \<sqinter> y\<^sup>T) * x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>T * y * (x \<sqinter> y) = x\<^sup>T * (y \<sqinter> y\<^sup>T) * x
[PROOF STEP]
by (simp add: assms(2) comp_associative covector_inf_comp_3 inf.sup_monoid.add_commute)
[PROOF STATE]
proof (state)
this:
x\<^sup>T * y * (x \<sqinter> y) = x\<^sup>T * (y \<sqinter> y\<^sup>T) * x

goal (2 subgoals):
 1. coreflexive ((x \<sqinter> y)\<^sup>T * top * (x \<sqinter> y))
 2. times_top_class.total (top * (x \<sqinter> y))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x\<^sup>T * y * (x \<sqinter> y) = x\<^sup>T * (y \<sqinter> y\<^sup>T) * x

goal (2 subgoals):
 1. coreflexive ((x \<sqinter> y)\<^sup>T * top * (x \<sqinter> y))
 2. times_top_class.total (top * (x \<sqinter> y))
[PROOF STEP]
have "... \<le> x\<^sup>T * x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>T * (y \<sqinter> y\<^sup>T) * x \<le> x\<^sup>T * x
[PROOF STEP]
by (metis assms(2) comp_right_one mult_left_isotone mult_right_isotone vector_covector)
[PROOF STATE]
proof (state)
this:
x\<^sup>T * (y \<sqinter> y\<^sup>T) * x \<le> x\<^sup>T * x

goal (2 subgoals):
 1. coreflexive ((x \<sqinter> y)\<^sup>T * top * (x \<sqinter> y))
 2. times_top_class.total (top * (x \<sqinter> y))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x\<^sup>T * (y \<sqinter> y\<^sup>T) * x \<le> x\<^sup>T * x

goal (2 subgoals):
 1. coreflexive ((x \<sqinter> y)\<^sup>T * top * (x \<sqinter> y))
 2. times_top_class.total (top * (x \<sqinter> y))
[PROOF STEP]
have "... \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univalent x
[PROOF STEP]
by (simp add: assms(1))
[PROOF STATE]
proof (state)
this:
univalent x

goal (2 subgoals):
 1. coreflexive ((x \<sqinter> y)\<^sup>T * top * (x \<sqinter> y))
 2. times_top_class.total (top * (x \<sqinter> y))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
coreflexive ((x \<sqinter> y)\<^sup>T * top * (x \<sqinter> y))
[PROOF STEP]
show "(x \<sqinter> y)\<^sup>T * top * (x \<sqinter> y) \<le> 1"
[PROOF STATE]
proof (prove)
using this:
coreflexive ((x \<sqinter> y)\<^sup>T * top * (x \<sqinter> y))

goal (1 subgoal):
 1. coreflexive ((x \<sqinter> y)\<^sup>T * top * (x \<sqinter> y))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
coreflexive ((x \<sqinter> y)\<^sup>T * top * (x \<sqinter> y))

goal (1 subgoal):
 1. times_top_class.total (top * (x \<sqinter> y))
[PROOF STEP]
show "top * (x \<sqinter> y) * top = top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. times_top_class.total (top * (x \<sqinter> y))
[PROOF STEP]
by (metis assms inf_top_right inf_vector_comp mult_assoc)
[PROOF STATE]
proof (state)
this:
times_top_class.total (top * (x \<sqinter> y))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma conv_complement_1:
  "-(x\<^sup>T) \<squnion> (-x)\<^sup>T = (-x)\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - x\<^sup>T \<squnion> (- x)\<^sup>T = (- x)\<^sup>T
[PROOF STEP]
by (metis conv_dist_inf conv_order bot_least conv_involutive pseudo_complement sup.absorb2 sup.cobounded2)


[STATEMENT]
lemma conv_complement:
  "(-x)\<^sup>T = -(x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- x)\<^sup>T = - x\<^sup>T
[PROOF STEP]
by (metis conv_complement_1 conv_dist_sup conv_involutive sup_commute)


[STATEMENT]
lemma conv_complement_sub_inf [simp]:
  "x\<^sup>T * -(x * y) \<sqinter> y = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>T * - (x * y) \<sqinter> y = bot
[PROOF STEP]
by (metis comp_left_zero conv_dist_comp conv_involutive dedekind_1 inf_import_p inf_p inf_right_idem ppp pseudo_complement regular_closed_bot)


[STATEMENT]
lemma conv_complement_sub_leq:
  "x\<^sup>T * -(x * y) \<le> -y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>T * - (x * y) \<le> - y
[PROOF STEP]
using pseudo_complement conv_complement_sub_inf
[PROOF STATE]
proof (prove)
using this:
(?x \<sqinter> ?y = bot) = (?x \<le> - ?y)
?x\<^sup>T * - (?x * ?y) \<sqinter> ?y = bot

goal (1 subgoal):
 1. x\<^sup>T * - (x * y) \<le> - y
[PROOF STEP]
by blast


[STATEMENT]
lemma conv_complement_sub [simp]:
  "x\<^sup>T * -(x * y) \<squnion> -y = -y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>T * - (x * y) \<squnion> - y = - y
[PROOF STEP]
by (simp add: conv_complement_sub_leq sup.absorb2)


[STATEMENT]
lemma complement_conv_sub:
  "-(y * x) * x\<^sup>T \<le> -y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (y * x) * x\<^sup>T \<le> - y
[PROOF STEP]
by (metis conv_complement conv_complement_sub_leq conv_order conv_dist_comp)


[STATEMENT]
lemma schroeder_3_p:
  "x * y \<le> -z \<longleftrightarrow> x\<^sup>T * z \<le> -y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * y \<le> - z) = (x\<^sup>T * z \<le> - y)
[PROOF STEP]
using pseudo_complement schroeder_1
[PROOF STATE]
proof (prove)
using this:
(?x \<sqinter> ?y = bot) = (?x \<le> - ?y)
(?x * ?y \<sqinter> ?z = bot) = (?x\<^sup>T * ?z \<sqinter> ?y = bot)

goal (1 subgoal):
 1. (x * y \<le> - z) = (x\<^sup>T * z \<le> - y)
[PROOF STEP]
by auto


[STATEMENT]
lemma schroeder_4_p:
  "x * y \<le> -z \<longleftrightarrow> z * y\<^sup>T \<le> -x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * y \<le> - z) = (z * y\<^sup>T \<le> - x)
[PROOF STEP]
using pseudo_complement schroeder_2
[PROOF STATE]
proof (prove)
using this:
(?x \<sqinter> ?y = bot) = (?x \<le> - ?y)
(?x * ?y \<sqinter> ?z = bot) = (?z * ?y\<^sup>T \<sqinter> ?x = bot)

goal (1 subgoal):
 1. (x * y \<le> - z) = (z * y\<^sup>T \<le> - x)
[PROOF STEP]
by auto


[STATEMENT]
lemma comp_pp_semi_commute:
  "x * --y \<le> --(x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * - - y \<le> - - (x * y)
[PROOF STEP]
using conv_complement_sub_leq schroeder_3_p
[PROOF STATE]
proof (prove)
using this:
?x\<^sup>T * - (?x * ?y) \<le> - ?y
(?x * ?y \<le> - ?z) = (?x\<^sup>T * ?z \<le> - ?y)

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


[STATEMENT]
lemma p_comp_pp [simp]:
  "-(x * --y) = -(x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (x * - - y) = - (x * y)
[PROOF STEP]
using comp_pp_semi_commute comp_right_isotone order.eq_iff p_antitone pp_increasing
[PROOF STATE]
proof (prove)
using this:
?x * - - ?y \<le> - - (?x * ?y)
?x \<le> ?y \<Longrightarrow> ?z * ?x \<le> ?z * ?y
(?a = ?b) = (?a \<le> ?b \<and> ?b \<le> ?a)
?x \<le> ?y \<Longrightarrow> - ?y \<le> - ?x
?x \<le> - - ?x

goal (1 subgoal):
 1. - (x * - - y) = - (x * y)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma pp_comp_semi_commute:
  "--x * y \<le> --(x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - - x * y \<le> - - (x * y)
[PROOF STEP]
using complement_conv_sub schroeder_4_p
[PROOF STATE]
proof (prove)
using this:
- (?y * ?x) * ?x\<^sup>T \<le> - ?y
(?x * ?y \<le> - ?z) = (?z * ?y\<^sup>T \<le> - ?x)

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


[STATEMENT]
lemma p_pp_comp [simp]:
  "-(--x * y) = -(x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (- - x * y) = - (x * y)
[PROOF STEP]
using pp_comp_semi_commute comp_left_isotone order.eq_iff p_antitone pp_increasing
[PROOF STATE]
proof (prove)
using this:
- - ?x * ?y \<le> - - (?x * ?y)
?x \<le> ?y \<Longrightarrow> ?x * ?z \<le> ?y * ?z
(?a = ?b) = (?a \<le> ?b \<and> ?b \<le> ?a)
?x \<le> ?y \<Longrightarrow> - ?y \<le> - ?x
?x \<le> - - ?x

goal (1 subgoal):
 1. - (- - x * y) = - (x * y)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma pp_comp_subdist:
  "--x * --y \<le> --(x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - - x * - - y \<le> - - (x * y)
[PROOF STEP]
by (simp add: p_antitone_iff)


[STATEMENT]
lemma theorem24xxiii:
  "x * y \<sqinter> -(x * z) = x * (y \<sqinter> -z) \<sqinter> -(x * z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y \<sqinter> - (x * z) = x * (y \<sqinter> - z) \<sqinter> - (x * z)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x * y \<sqinter> - (x * z) = x * (y \<sqinter> - z) \<sqinter> - (x * z)
[PROOF STEP]
have "x * y \<sqinter> -(x * z) \<le> x * (y \<sqinter> (x\<^sup>T * -(x * z)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y \<sqinter> - (x * z) \<le> x * (y \<sqinter> x\<^sup>T * - (x * z))
[PROOF STEP]
by (simp add: dedekind_1)
[PROOF STATE]
proof (state)
this:
x * y \<sqinter> - (x * z) \<le> x * (y \<sqinter> x\<^sup>T * - (x * z))

goal (1 subgoal):
 1. x * y \<sqinter> - (x * z) = x * (y \<sqinter> - z) \<sqinter> - (x * z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x * y \<sqinter> - (x * z) \<le> x * (y \<sqinter> x\<^sup>T * - (x * z))

goal (1 subgoal):
 1. x * y \<sqinter> - (x * z) = x * (y \<sqinter> - z) \<sqinter> - (x * z)
[PROOF STEP]
have "... \<le> x * (y \<sqinter> -z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * (y \<sqinter> x\<^sup>T * - (x * z)) \<le> x * (y \<sqinter> - z)
[PROOF STEP]
using comp_right_isotone conv_complement_sub_leq inf.sup_right_isotone
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> ?z * ?x \<le> ?z * ?y
?x\<^sup>T * - (?x * ?y) \<le> - ?y
?y \<le> ?x \<Longrightarrow> ?z \<sqinter> ?y \<le> ?z \<sqinter> ?x

goal (1 subgoal):
 1. x * (y \<sqinter> x\<^sup>T * - (x * z)) \<le> x * (y \<sqinter> - z)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x * (y \<sqinter> x\<^sup>T * - (x * z)) \<le> x * (y \<sqinter> - z)

goal (1 subgoal):
 1. x * y \<sqinter> - (x * z) = x * (y \<sqinter> - z) \<sqinter> - (x * z)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x * y \<sqinter> - (x * z) \<le> x * (y \<sqinter> - z)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x * y \<sqinter> - (x * z) \<le> x * (y \<sqinter> - z)

goal (1 subgoal):
 1. x * y \<sqinter> - (x * z) = x * (y \<sqinter> - z) \<sqinter> - (x * z)
[PROOF STEP]
using comp_right_subdist_inf order.antisym inf.coboundedI2 inf.commute
[PROOF STATE]
proof (prove)
using this:
x * y \<sqinter> - (x * z) \<le> x * (y \<sqinter> - z)
?x * (?y \<sqinter> ?z) \<le> ?x * ?y \<sqinter> ?x * ?z
\<lbrakk>?a \<le> ?b; ?b \<le> ?a\<rbrakk> \<Longrightarrow> ?a = ?b
?b \<le> ?c \<Longrightarrow> ?a \<sqinter> ?b \<le> ?c
?a \<sqinter> ?b = ?b \<sqinter> ?a

goal (1 subgoal):
 1. x * y \<sqinter> - (x * z) = x * (y \<sqinter> - z) \<sqinter> - (x * z)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x * y \<sqinter> - (x * z) = x * (y \<sqinter> - z) \<sqinter> - (x * z)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vector_complement_closed:
  "vector x \<Longrightarrow> vector (-x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector x \<Longrightarrow> vector (- x)
[PROOF STEP]
by (metis complement_conv_sub conv_top order.eq_iff top_right_mult_increasing)


[STATEMENT]
lemma covector_complement_closed:
  "covector x \<Longrightarrow> covector (-x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. covector x \<Longrightarrow> covector (- x)
[PROOF STEP]
by (metis conv_complement_sub_leq conv_top order.eq_iff top_left_mult_increasing)


[STATEMENT]
lemma covector_vector_comp:
  "vector v \<Longrightarrow> -v\<^sup>T * v = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector v \<Longrightarrow> - v\<^sup>T * v = bot
[PROOF STEP]
by (metis conv_bot conv_complement conv_complement_sub_inf conv_dist_comp conv_involutive inf_top.right_neutral)


[STATEMENT]
lemma irreflexive_bot_closed:
  "irreflexive bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. irreflexive bot
[PROOF STEP]
by simp


[STATEMENT]
lemma irreflexive_inf_closed:
  "irreflexive x \<Longrightarrow> irreflexive (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. irreflexive x \<Longrightarrow> irreflexive (x \<sqinter> y)
[PROOF STEP]
by (simp add: le_infI1)


[STATEMENT]
lemma irreflexive_sup_closed:
  "irreflexive x \<Longrightarrow> irreflexive y \<Longrightarrow> irreflexive (x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>irreflexive x; irreflexive y\<rbrakk> \<Longrightarrow> irreflexive (x \<squnion> y)
[PROOF STEP]
by simp


[STATEMENT]
lemma irreflexive_conv_closed:
  "irreflexive x \<Longrightarrow> irreflexive (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. irreflexive x \<Longrightarrow> irreflexive (x\<^sup>T)
[PROOF STEP]
using conv_complement conv_isotone
[PROOF STATE]
proof (prove)
using this:
(- ?x)\<^sup>T = - ?x\<^sup>T
?x \<le> ?y \<Longrightarrow> ?x\<^sup>T \<le> ?y\<^sup>T

goal (1 subgoal):
 1. irreflexive x \<Longrightarrow> irreflexive (x\<^sup>T)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma reflexive_complement_irreflexive:
  "reflexive x \<Longrightarrow> irreflexive (-x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reflexive x \<Longrightarrow> irreflexive (- x)
[PROOF STEP]
by (simp add: p_antitone)


[STATEMENT]
lemma irreflexive_complement_reflexive:
  "irreflexive x \<longleftrightarrow> reflexive (-x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. irreflexive x = reflexive (- x)
[PROOF STEP]
by (simp add: p_antitone_iff)


[STATEMENT]
lemma symmetric_complement_closed:
  "symmetric x \<Longrightarrow> symmetric (-x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symmetric x \<Longrightarrow> symmetric (- x)
[PROOF STEP]
by (simp add: conv_complement)


[STATEMENT]
lemma asymmetric_irreflexive:
  "asymmetric x \<Longrightarrow> irreflexive x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. asymmetric x \<Longrightarrow> irreflexive x
[PROOF STEP]
by (metis inf.mult_not_zero inf.left_commute inf.right_idem inf.sup_monoid.add_commute pseudo_complement one_inf_conv)


[STATEMENT]
lemma linear_asymmetric:
  "linear x \<Longrightarrow> asymmetric (-x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linear x \<Longrightarrow> asymmetric (- x)
[PROOF STEP]
using conv_complement p_top
[PROOF STATE]
proof (prove)
using this:
(- ?x)\<^sup>T = - ?x\<^sup>T
dense top

goal (1 subgoal):
 1. linear x \<Longrightarrow> asymmetric (- x)
[PROOF STEP]
by force


[STATEMENT]
lemma strict_linear_sup_closed:
  "strict_linear x \<Longrightarrow> strict_linear y \<Longrightarrow> strict_linear (x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>strict_linear x; strict_linear y\<rbrakk> \<Longrightarrow> strict_linear (x \<squnion> y)
[PROOF STEP]
by (metis (mono_tags, opaque_lifting) conv_dist_sup sup.right_idem sup_assoc sup_commute)


[STATEMENT]
lemma strict_linear_irreflexive:
  "strict_linear x \<Longrightarrow> irreflexive x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strict_linear x \<Longrightarrow> irreflexive x
[PROOF STEP]
using sup_left_divisibility
[PROOF STATE]
proof (prove)
using this:
(?x \<le> ?y) = (\<exists>z. ?x \<squnion> z = ?y)

goal (1 subgoal):
 1. strict_linear x \<Longrightarrow> irreflexive x
[PROOF STEP]
by blast


[STATEMENT]
lemma strict_linear_conv_closed:
  "strict_linear x \<Longrightarrow> strict_linear (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strict_linear x \<Longrightarrow> strict_linear (x\<^sup>T)
[PROOF STEP]
by (simp add: sup_commute)


[STATEMENT]
lemma strict_order_var:
  "strict_order x \<longleftrightarrow> asymmetric x \<and> transitive x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strict_order x = (asymmetric x \<and> transitive x)
[PROOF STEP]
by (metis asymmetric_irreflexive comp_right_one irreflexive_conv_closed conv_dist_comp dual_order.trans pseudo_complement schroeder_3_p)


[STATEMENT]
lemma strict_order_bot_closed:
  "strict_order bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strict_order bot
[PROOF STEP]
by simp


[STATEMENT]
lemma strict_order_inf_closed:
  "strict_order x \<Longrightarrow> strict_order y \<Longrightarrow> strict_order (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>strict_order x; strict_order y\<rbrakk> \<Longrightarrow> strict_order (x \<sqinter> y)
[PROOF STEP]
using inf.coboundedI1 transitive_inf_closed
[PROOF STATE]
proof (prove)
using this:
?a \<le> ?c \<Longrightarrow> ?a \<sqinter> ?b \<le> ?c
\<lbrakk>transitive ?x; transitive ?y\<rbrakk> \<Longrightarrow> transitive (?x \<sqinter> ?y)

goal (1 subgoal):
 1. \<lbrakk>strict_order x; strict_order y\<rbrakk> \<Longrightarrow> strict_order (x \<sqinter> y)
[PROOF STEP]
by auto


[STATEMENT]
lemma strict_order_conv_closed:
  "strict_order x \<Longrightarrow> strict_order (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strict_order x \<Longrightarrow> strict_order (x\<^sup>T)
[PROOF STEP]
using irreflexive_conv_closed transitive_conv_closed
[PROOF STATE]
proof (prove)
using this:
irreflexive ?x \<Longrightarrow> irreflexive (?x\<^sup>T)
transitive ?x \<Longrightarrow> transitive (?x\<^sup>T)

goal (1 subgoal):
 1. strict_order x \<Longrightarrow> strict_order (x\<^sup>T)
[PROOF STEP]
by blast


[STATEMENT]
lemma order_strict_order:
  assumes "order x"
  shows "strict_order (x \<sqinter> -1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strict_order (x \<sqinter> - (1::'a))
[PROOF STEP]
proof (rule conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. irreflexive (x \<sqinter> - (1::'a))
 2. transitive (x \<sqinter> - (1::'a))
[PROOF STEP]
show 1: "irreflexive (x \<sqinter> -1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. irreflexive (x \<sqinter> - (1::'a))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
irreflexive (x \<sqinter> - (1::'a))

goal (1 subgoal):
 1. transitive (x \<sqinter> - (1::'a))
[PROOF STEP]
have "antisymmetric (x \<sqinter> -1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. antisymmetric (x \<sqinter> - (1::'a))
[PROOF STEP]
using antisymmetric_inf_closed assms
[PROOF STATE]
proof (prove)
using this:
antisymmetric ?x \<Longrightarrow> antisymmetric (?x \<sqinter> ?y)
order x

goal (1 subgoal):
 1. antisymmetric (x \<sqinter> - (1::'a))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
antisymmetric (x \<sqinter> - (1::'a))

goal (1 subgoal):
 1. transitive (x \<sqinter> - (1::'a))
[PROOF STEP]
hence "(x \<sqinter> -1) * (x \<sqinter> -1) \<sqinter> 1 \<le> (x \<sqinter> -1 \<sqinter> (x \<sqinter> -1)\<^sup>T) * (x \<sqinter> -1 \<sqinter> (x \<sqinter> -1)\<^sup>T)"
[PROOF STATE]
proof (prove)
using this:
antisymmetric (x \<sqinter> - (1::'a))

goal (1 subgoal):
 1. (x \<sqinter> - (1::'a)) * (x \<sqinter> - (1::'a)) \<sqinter> (1::'a) \<le> (x \<sqinter> - (1::'a) \<sqinter> (x \<sqinter> - (1::'a))\<^sup>T) * (x \<sqinter> - (1::'a) \<sqinter> (x \<sqinter> - (1::'a))\<^sup>T)
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
antisymmetric (x \<sqinter> - (1::'a))
irreflexive (x \<sqinter> - (1::'a))

goal (1 subgoal):
 1. (x \<sqinter> - (1::'a)) * (x \<sqinter> - (1::'a)) \<sqinter> (1::'a) \<le> (x \<sqinter> - (1::'a) \<sqinter> (x \<sqinter> - (1::'a))\<^sup>T) * (x \<sqinter> - (1::'a) \<sqinter> (x \<sqinter> - (1::'a))\<^sup>T)
[PROOF STEP]
by (metis (no_types) coreflexive_symmetric irreflexive_inf_closed coreflexive_transitive dedekind_1 inf_idem mult_1_right semiring.mult_not_zero strict_order_var)
[PROOF STATE]
proof (state)
this:
(x \<sqinter> - (1::'a)) * (x \<sqinter> - (1::'a)) \<sqinter> (1::'a) \<le> (x \<sqinter> - (1::'a) \<sqinter> (x \<sqinter> - (1::'a))\<^sup>T) * (x \<sqinter> - (1::'a) \<sqinter> (x \<sqinter> - (1::'a))\<^sup>T)

goal (1 subgoal):
 1. transitive (x \<sqinter> - (1::'a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x \<sqinter> - (1::'a)) * (x \<sqinter> - (1::'a)) \<sqinter> (1::'a) \<le> (x \<sqinter> - (1::'a) \<sqinter> (x \<sqinter> - (1::'a))\<^sup>T) * (x \<sqinter> - (1::'a) \<sqinter> (x \<sqinter> - (1::'a))\<^sup>T)

goal (1 subgoal):
 1. transitive (x \<sqinter> - (1::'a))
[PROOF STEP]
have "... = (x \<sqinter> x\<^sup>T \<sqinter> -1) * (x \<sqinter> x\<^sup>T \<sqinter> -1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqinter> - (1::'a) \<sqinter> (x \<sqinter> - (1::'a))\<^sup>T) * (x \<sqinter> - (1::'a) \<sqinter> (x \<sqinter> - (1::'a))\<^sup>T) = (x \<sqinter> x\<^sup>T \<sqinter> - (1::'a)) * (x \<sqinter> x\<^sup>T \<sqinter> - (1::'a))
[PROOF STEP]
by (simp add: conv_complement conv_dist_inf inf.absorb2 inf.sup_monoid.add_assoc)
[PROOF STATE]
proof (state)
this:
(x \<sqinter> - (1::'a) \<sqinter> (x \<sqinter> - (1::'a))\<^sup>T) * (x \<sqinter> - (1::'a) \<sqinter> (x \<sqinter> - (1::'a))\<^sup>T) = (x \<sqinter> x\<^sup>T \<sqinter> - (1::'a)) * (x \<sqinter> x\<^sup>T \<sqinter> - (1::'a))

goal (1 subgoal):
 1. transitive (x \<sqinter> - (1::'a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x \<sqinter> - (1::'a) \<sqinter> (x \<sqinter> - (1::'a))\<^sup>T) * (x \<sqinter> - (1::'a) \<sqinter> (x \<sqinter> - (1::'a))\<^sup>T) = (x \<sqinter> x\<^sup>T \<sqinter> - (1::'a)) * (x \<sqinter> x\<^sup>T \<sqinter> - (1::'a))

goal (1 subgoal):
 1. transitive (x \<sqinter> - (1::'a))
[PROOF STEP]
have "... = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqinter> x\<^sup>T \<sqinter> - (1::'a)) * (x \<sqinter> x\<^sup>T \<sqinter> - (1::'a)) = bot
[PROOF STEP]
using assms order.antisym reflexive_conv_closed
[PROOF STATE]
proof (prove)
using this:
order x
\<lbrakk>?a \<le> ?b; ?b \<le> ?a\<rbrakk> \<Longrightarrow> ?a = ?b
reflexive ?x \<Longrightarrow> reflexive (?x\<^sup>T)

goal (1 subgoal):
 1. (x \<sqinter> x\<^sup>T \<sqinter> - (1::'a)) * (x \<sqinter> x\<^sup>T \<sqinter> - (1::'a)) = bot
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(x \<sqinter> x\<^sup>T \<sqinter> - (1::'a)) * (x \<sqinter> x\<^sup>T \<sqinter> - (1::'a)) = bot

goal (1 subgoal):
 1. transitive (x \<sqinter> - (1::'a))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(x \<sqinter> - (1::'a)) * (x \<sqinter> - (1::'a)) \<sqinter> (1::'a) \<le> bot
[PROOF STEP]
have "(x \<sqinter> -1) * (x \<sqinter> -1) \<le> -1"
[PROOF STATE]
proof (prove)
using this:
(x \<sqinter> - (1::'a)) * (x \<sqinter> - (1::'a)) \<sqinter> (1::'a) \<le> bot

goal (1 subgoal):
 1. irreflexive ((x \<sqinter> - (1::'a)) * (x \<sqinter> - (1::'a)))
[PROOF STEP]
using le_bot pseudo_complement
[PROOF STATE]
proof (prove)
using this:
(x \<sqinter> - (1::'a)) * (x \<sqinter> - (1::'a)) \<sqinter> (1::'a) \<le> bot
?a \<le> bot \<Longrightarrow> ?a = bot
(?x \<sqinter> ?y = bot) = (?x \<le> - ?y)

goal (1 subgoal):
 1. irreflexive ((x \<sqinter> - (1::'a)) * (x \<sqinter> - (1::'a)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
irreflexive ((x \<sqinter> - (1::'a)) * (x \<sqinter> - (1::'a)))

goal (1 subgoal):
 1. transitive (x \<sqinter> - (1::'a))
[PROOF STEP]
thus "transitive (x \<sqinter> -1)"
[PROOF STATE]
proof (prove)
using this:
irreflexive ((x \<sqinter> - (1::'a)) * (x \<sqinter> - (1::'a)))

goal (1 subgoal):
 1. transitive (x \<sqinter> - (1::'a))
[PROOF STEP]
by (meson assms comp_isotone inf.boundedI inf.cobounded1 inf.order_lesseq_imp)
[PROOF STATE]
proof (state)
this:
transitive (x \<sqinter> - (1::'a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma strict_order_order:
  "strict_order x \<Longrightarrow> order (x \<squnion> 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strict_order x \<Longrightarrow> order (x \<squnion> (1::'a))
[PROOF STEP]
apply (unfold strict_order_var, intro conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. asymmetric x \<and> transitive x \<Longrightarrow> reflexive (x \<squnion> (1::'a))
 2. asymmetric x \<and> transitive x \<Longrightarrow> transitive (x \<squnion> (1::'a))
 3. asymmetric x \<and> transitive x \<Longrightarrow> antisymmetric (x \<squnion> (1::'a))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. asymmetric x \<and> transitive x \<Longrightarrow> transitive (x \<squnion> (1::'a))
 2. asymmetric x \<and> transitive x \<Longrightarrow> antisymmetric (x \<squnion> (1::'a))
[PROOF STEP]
apply (simp add: mult_left_dist_sup mult_right_dist_sup sup.absorb2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. asymmetric x \<and> transitive x \<Longrightarrow> antisymmetric (x \<squnion> (1::'a))
[PROOF STEP]
using conv_dist_sup coreflexive_bot_closed sup.absorb2 sup_inf_distrib2
[PROOF STATE]
proof (prove)
using this:
(?x \<squnion> ?y)\<^sup>T = ?x\<^sup>T \<squnion> ?y\<^sup>T
coreflexive bot
?a \<le> ?b \<Longrightarrow> ?a \<squnion> ?b = ?b
?y \<sqinter> ?z \<squnion> ?x = (?y \<squnion> ?x) \<sqinter> (?z \<squnion> ?x)

goal (1 subgoal):
 1. asymmetric x \<and> transitive x \<Longrightarrow> antisymmetric (x \<squnion> (1::'a))
[PROOF STEP]
by fastforce


[STATEMENT]
lemma linear_strict_order_conv_closed:
  "linear_strict_order x \<Longrightarrow> linear_strict_order (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linear_strict_order x \<Longrightarrow> linear_strict_order (x\<^sup>T)
[PROOF STEP]
by (simp add: irreflexive_conv_closed sup_monoid.add_commute transitive_conv_closed)


[STATEMENT]
lemma linear_order_strict_order:
  "linear_order x \<Longrightarrow> linear_strict_order (x \<sqinter> -1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_distrib_allegory_signature_class.linear_order x \<Longrightarrow> linear_strict_order (x \<sqinter> - (1::'a))
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. bounded_distrib_allegory_signature_class.linear_order x \<Longrightarrow> strict_order (x \<sqinter> - (1::'a))
 2. bounded_distrib_allegory_signature_class.linear_order x \<Longrightarrow> strict_linear (x \<sqinter> - (1::'a))
[PROOF STEP]
using order_strict_order
[PROOF STATE]
proof (prove)
using this:
order ?x \<Longrightarrow> strict_order (?x \<sqinter> - (1::'a))

goal (2 subgoals):
 1. bounded_distrib_allegory_signature_class.linear_order x \<Longrightarrow> strict_order (x \<sqinter> - (1::'a))
 2. bounded_distrib_allegory_signature_class.linear_order x \<Longrightarrow> strict_linear (x \<sqinter> - (1::'a))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_distrib_allegory_signature_class.linear_order x \<Longrightarrow> strict_linear (x \<sqinter> - (1::'a))
[PROOF STEP]
by (metis conv_complement conv_dist_inf coreflexive_symmetric order.eq_iff inf.absorb2 inf.distrib_left inf.sup_monoid.add_commute top.extremum)


[STATEMENT]
lemma regular_conv_closed:
  "regular x \<Longrightarrow> regular (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. regular x \<Longrightarrow> regular (x\<^sup>T)
[PROOF STEP]
by (metis conv_complement)


[STATEMENT]
lemma equivalence_comp_left_complement:
  "equivalence x \<Longrightarrow> x * -x = -x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equivalence x \<Longrightarrow> x * - x = - x
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. equivalence x \<Longrightarrow> x * - x \<le> - x
 2. equivalence x \<Longrightarrow> - x \<le> x * - x
[PROOF STEP]
apply (metis conv_complement_sub_leq preorder_idempotent)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equivalence x \<Longrightarrow> - x \<le> x * - x
[PROOF STEP]
using mult_left_isotone
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> ?x * ?z \<le> ?y * ?z

goal (1 subgoal):
 1. equivalence x \<Longrightarrow> - x \<le> x * - x
[PROOF STEP]
by fastforce


[STATEMENT]
lemma equivalence_comp_right_complement:
  "equivalence x \<Longrightarrow> -x * x = -x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equivalence x \<Longrightarrow> - x * x = - x
[PROOF STEP]
by (metis equivalence_comp_left_complement conv_complement conv_dist_comp)


[STATEMENT]
lemma coreflexive_comp_top_coreflexive_complement:
  "coreflexive x \<Longrightarrow> (x * top)' = x '"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive x \<Longrightarrow> (x * top) ' = x '
[PROOF STEP]
by (metis coreflexive_comp_top_inf_one inf.commute inf_import_p)


[STATEMENT]
lemma coreflexive_comp_inf_complement:
  "coreflexive x \<Longrightarrow> (x * y) \<sqinter> -z = (x * y) \<sqinter> -(x * z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive x \<Longrightarrow> x * y \<sqinter> - z = x * y \<sqinter> - (x * z)
[PROOF STEP]
by (metis coreflexive_comp_top_inf inf.sup_relative_same_increasing inf_import_p inf_le1)


[STATEMENT]
lemma double_coreflexive_complement:
  "x '' = (-x)'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x ' ' = - x '
[PROOF STEP]
using inf.sup_monoid.add_commute inf_import_p
[PROOF STATE]
proof (prove)
using this:
?a \<sqinter> ?b = ?b \<sqinter> ?a
?x \<sqinter> - (?x \<sqinter> ?y) = ?x \<sqinter> - ?y

goal (1 subgoal):
 1. x ' ' = - x '
[PROOF STEP]
by auto


[STATEMENT]
lemma coreflexive_pp_dist_comp:
  assumes "coreflexive x"
      and "coreflexive y"
    shows "(x * y)'' = x '' * y ''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * y) ' ' = x ' ' * y ' '
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x * y) ' ' = x ' ' * y ' '
[PROOF STEP]
have "(x * y)'' = --(x * y) \<sqinter> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * y) ' ' = - (x * y) '
[PROOF STEP]
by (simp add: double_coreflexive_complement)
[PROOF STATE]
proof (state)
this:
(x * y) ' ' = - (x * y) '

goal (1 subgoal):
 1. (x * y) ' ' = x ' ' * y ' '
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x * y) ' ' = - (x * y) '

goal (1 subgoal):
 1. (x * y) ' ' = x ' ' * y ' '
[PROOF STEP]
have "... = --x \<sqinter> --y \<sqinter> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (x * y) ' = - - x \<sqinter> - - y \<sqinter> (1::'a)
[PROOF STEP]
by (simp add: assms coreflexive_comp_inf)
[PROOF STATE]
proof (state)
this:
- (x * y) ' = - - x \<sqinter> - - y \<sqinter> (1::'a)

goal (1 subgoal):
 1. (x * y) ' ' = x ' ' * y ' '
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- (x * y) ' = - - x \<sqinter> - - y \<sqinter> (1::'a)

goal (1 subgoal):
 1. (x * y) ' ' = x ' ' * y ' '
[PROOF STEP]
have "... = (--x \<sqinter> 1) * (--y \<sqinter> 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - - x \<sqinter> - - y \<sqinter> (1::'a) = - x ' * - y '
[PROOF STEP]
by (simp add: coreflexive_comp_inf inf.left_commute inf.sup_monoid.add_assoc)
[PROOF STATE]
proof (state)
this:
- - x \<sqinter> - - y \<sqinter> (1::'a) = - x ' * - y '

goal (1 subgoal):
 1. (x * y) ' ' = x ' ' * y ' '
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- - x \<sqinter> - - y \<sqinter> (1::'a) = - x ' * - y '

goal (1 subgoal):
 1. (x * y) ' ' = x ' ' * y ' '
[PROOF STEP]
have "... = x '' * y ''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - x ' * - y ' = x ' ' * y ' '
[PROOF STEP]
by (simp add: double_coreflexive_complement)
[PROOF STATE]
proof (state)
this:
- x ' * - y ' = x ' ' * y ' '

goal (1 subgoal):
 1. (x * y) ' ' = x ' ' * y ' '
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(x * y) ' ' = x ' ' * y ' '
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(x * y) ' ' = x ' ' * y ' '

goal (1 subgoal):
 1. (x * y) ' ' = x ' ' * y ' '
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(x * y) ' ' = x ' ' * y ' '

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma coreflexive_pseudo_complement:
  "coreflexive x \<Longrightarrow> x \<sqinter> y = bot \<longleftrightarrow> x \<le> y '"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive x \<Longrightarrow> (x \<sqinter> y = bot) = (x \<le> y ')
[PROOF STEP]
by (simp add: pseudo_complement)


[STATEMENT]
lemma pp_bijective_conv_mapping:
  "pp_bijective x \<longleftrightarrow> pp_mapping (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pp_bijective x = pp_mapping (x\<^sup>T)
[PROOF STEP]
by (simp add: conv_complement surjective_conv_total)