[STATEMENT]
lemma pp_arc_expanded:
  "pp_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. pp_arc x = (coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pp_arc x \<Longrightarrow> coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x)
 2. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x) \<Longrightarrow> pp_arc x
[PROOF STEP]
assume 1: "pp_arc x"
[PROOF STATE]
proof (state)
this:
pp_arc x

goal (2 subgoals):
 1. pp_arc x \<Longrightarrow> coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x)
 2. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x) \<Longrightarrow> pp_arc x
[PROOF STEP]
have 2: "x * top * x\<^sup>T \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive (x * top * x\<^sup>T)
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
pp_arc x

goal (1 subgoal):
 1. coreflexive (x * top * x\<^sup>T)
[PROOF STEP]
by (metis comp_associative conv_dist_comp equivalence_top_closed vector_top_closed)
[PROOF STATE]
proof (state)
this:
coreflexive (x * top * x\<^sup>T)

goal (2 subgoals):
 1. pp_arc x \<Longrightarrow> coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x)
 2. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x) \<Longrightarrow> pp_arc x
[PROOF STEP]
have 3: "x\<^sup>T * top * x \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive (x\<^sup>T * top * x)
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
pp_arc x

goal (1 subgoal):
 1. coreflexive (x\<^sup>T * top * x)
[PROOF STEP]
by (metis conv_dist_comp conv_involutive equivalence_top_closed vector_top_closed mult_assoc)
[PROOF STATE]
proof (state)
this:
coreflexive (x\<^sup>T * top * x)

goal (2 subgoals):
 1. pp_arc x \<Longrightarrow> coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x)
 2. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x) \<Longrightarrow> pp_arc x
[PROOF STEP]
have 4: "x\<^sup>T \<le> x\<^sup>T * x * x\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>T \<le> x\<^sup>T * x * x\<^sup>T
[PROOF STEP]
by (metis conv_involutive ex231c)
[PROOF STATE]
proof (state)
this:
x\<^sup>T \<le> x\<^sup>T * x * x\<^sup>T

goal (2 subgoals):
 1. pp_arc x \<Longrightarrow> coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x)
 2. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x) \<Longrightarrow> pp_arc x
[PROOF STEP]
have "top = --(top * x) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. top = - - (top * x) * top
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
pp_arc x

goal (1 subgoal):
 1. top = - - (top * x) * top
[PROOF STEP]
by (metis conv_complement conv_dist_comp conv_involutive equivalence_top_closed)
[PROOF STATE]
proof (state)
this:
top = - - (top * x) * top

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

goal (2 subgoals):
 1. pp_arc x \<Longrightarrow> coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x)
 2. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x) \<Longrightarrow> pp_arc x
[PROOF STEP]
have "... \<le> --(top * x\<^sup>T * top * x) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - - (top * x) * top \<le> - - (top * x\<^sup>T * top * x) * top
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
pp_arc x

goal (1 subgoal):
 1. - - (top * x) * top \<le> - - (top * x\<^sup>T * top * x) * top
[PROOF STEP]
by (metis eq_refl mult_assoc p_comp_pp p_pp_comp)
[PROOF STATE]
proof (state)
this:
- - (top * x) * top \<le> - - (top * x\<^sup>T * top * x) * top

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

goal (2 subgoals):
 1. pp_arc x \<Longrightarrow> coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x)
 2. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x) \<Longrightarrow> pp_arc x
[PROOF STEP]
have "... = (top * --(x * top) \<sqinter> --(top * x\<^sup>T * top * x)) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - - (top * x\<^sup>T * top * x) * top = (top * - - (x * top) \<sqinter> - - (top * x\<^sup>T * top * x)) * top
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
pp_arc x

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

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

goal (2 subgoals):
 1. pp_arc x \<Longrightarrow> coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x)
 2. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x) \<Longrightarrow> pp_arc x
[PROOF STEP]
have "... = top * (--(x * top) \<sqinter> --(top * x\<^sup>T * top * x)) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (top * - - (x * top) \<sqinter> - - (top * x\<^sup>T * top * x)) * top = top * (- - (x * top) \<sqinter> - - (top * x\<^sup>T * top * x)) * top
[PROOF STEP]
by (simp add: covector_complement_closed covector_comp_inf covector_mult_closed)
[PROOF STATE]
proof (state)
this:
(top * - - (x * top) \<sqinter> - - (top * x\<^sup>T * top * x)) * top = top * (- - (x * top) \<sqinter> - - (top * x\<^sup>T * top * x)) * top

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

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

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

goal (2 subgoals):
 1. pp_arc x \<Longrightarrow> coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x)
 2. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x) \<Longrightarrow> pp_arc x
[PROOF STEP]
have "... = top * --(x * top * x\<^sup>T * top * x) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. top * - - (x * top \<sqinter> top * x\<^sup>T * top * x) * top = top * - - (x * top * x\<^sup>T * top * x) * top
[PROOF STEP]
by (metis comp_associative comp_inf_covector inf_top.left_neutral)
[PROOF STATE]
proof (state)
this:
top * - - (x * top \<sqinter> top * x\<^sup>T * top * x) * top = top * - - (x * top * x\<^sup>T * top * x) * top

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

goal (2 subgoals):
 1. pp_arc x \<Longrightarrow> coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x)
 2. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x) \<Longrightarrow> pp_arc x
[PROOF STEP]
have "... \<le> top * --(x * top * x\<^sup>T * x * x\<^sup>T * top * x) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. top * - - (x * top * x\<^sup>T * top * x) * top \<le> top * - - (x * top * x\<^sup>T * x * x\<^sup>T * top * x) * top
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
x\<^sup>T \<le> x\<^sup>T * x * x\<^sup>T

goal (1 subgoal):
 1. top * - - (x * top * x\<^sup>T * top * x) * top \<le> top * - - (x * top * x\<^sup>T * x * x\<^sup>T * top * x) * top
[PROOF STEP]
by (metis comp_associative comp_left_isotone comp_right_isotone pp_isotone)
[PROOF STATE]
proof (state)
this:
top * - - (x * top * x\<^sup>T * top * x) * top \<le> top * - - (x * top * x\<^sup>T * x * x\<^sup>T * top * x) * top

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

goal (2 subgoals):
 1. pp_arc x \<Longrightarrow> coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x)
 2. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x) \<Longrightarrow> pp_arc x
[PROOF STEP]
have "... \<le> top * --(x * x\<^sup>T * top * x) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. top * - - (x * top * x\<^sup>T * x * x\<^sup>T * top * x) * top \<le> top * - - (x * x\<^sup>T * top * x) * top
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
coreflexive (x * top * x\<^sup>T)

goal (1 subgoal):
 1. top * - - (x * top * x\<^sup>T * x * x\<^sup>T * top * x) * top \<le> top * - - (x * x\<^sup>T * top * x) * top
[PROOF STEP]
by (metis comp_associative comp_left_isotone comp_right_isotone pp_isotone comp_left_one)
[PROOF STATE]
proof (state)
this:
top * - - (x * top * x\<^sup>T * x * x\<^sup>T * top * x) * top \<le> top * - - (x * x\<^sup>T * top * x) * top

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

goal (2 subgoals):
 1. pp_arc x \<Longrightarrow> coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x)
 2. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x) \<Longrightarrow> pp_arc x
[PROOF STEP]
have "... \<le> top * --x * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. top * - - (x * x\<^sup>T * top * x) * top \<le> top * - - x * top
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
coreflexive (x\<^sup>T * top * x)

goal (1 subgoal):
 1. top * - - (x * x\<^sup>T * top * x) * top \<le> top * - - x * top
[PROOF STEP]
by (metis comp_associative comp_left_isotone comp_right_isotone pp_isotone comp_right_one)
[PROOF STATE]
proof (state)
this:
top * - - (x * x\<^sup>T * top * x) * top \<le> top * - - x * top

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

goal (1 subgoal):
 1. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x)
[PROOF STEP]
using 2 3 top_le
[PROOF STATE]
proof (prove)
using this:
top \<le> top * - - x * top
coreflexive (x * top * x\<^sup>T)
coreflexive (x\<^sup>T * top * x)
top \<le> ?a \<Longrightarrow> ?a = top

goal (1 subgoal):
 1. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x)

goal (1 subgoal):
 1. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x) \<Longrightarrow> pp_arc x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x) \<Longrightarrow> pp_arc x
[PROOF STEP]
assume "x * top * x\<^sup>T \<le> 1 \<and> x\<^sup>T * top * x \<le> 1 \<and> top * --x * top = top"
[PROOF STATE]
proof (state)
this:
coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x)

goal (1 subgoal):
 1. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x) \<Longrightarrow> pp_arc x
[PROOF STEP]
thus "pp_arc x"
[PROOF STATE]
proof (prove)
using this:
coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x)

goal (1 subgoal):
 1. pp_arc x
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x) \<Longrightarrow> injective (x * top)
 2. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x) \<Longrightarrow> surjective (- - (x * top))
 3. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x) \<Longrightarrow> injective (x\<^sup>T * top)
 4. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x) \<Longrightarrow> surjective (- - (x\<^sup>T * top))
[PROOF STEP]
apply (metis comp_associative conv_dist_comp equivalence_top_closed vector_top_closed)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x) \<Longrightarrow> surjective (- - (x * top))
 2. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x) \<Longrightarrow> injective (x\<^sup>T * top)
 3. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x) \<Longrightarrow> surjective (- - (x\<^sup>T * top))
[PROOF STEP]
apply (metis comp_associative mult_right_isotone top_le pp_comp_semi_commute)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x) \<Longrightarrow> injective (x\<^sup>T * top)
 2. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x) \<Longrightarrow> surjective (- - (x\<^sup>T * top))
[PROOF STEP]
apply (metis conv_dist_comp coreflexive_symmetric vector_conv_covector vector_top_closed mult_assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x) \<and> times_top_class.total (top * - - x) \<Longrightarrow> surjective (- - (x\<^sup>T * top))
[PROOF STEP]
by (metis conv_complement conv_dist_comp equivalence_top_closed inf.orderE inf_top.left_neutral mult_right_isotone pp_comp_semi_commute)
[PROOF STATE]
proof (state)
this:
pp_arc x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma N_comp:
  "N x * y = -(-x * top) \<sqinter> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N x * y = - (- x * top) \<sqinter> y
[PROOF STEP]
by (simp add: vector_mult_closed vector_complement_closed vector_inf_one_comp)


[STATEMENT]
lemma N_comp_top [simp]:
  "N x * top = -(-x * top)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N x * top = - (- x * top)
[PROOF STEP]
by (simp add: N_comp)


[STATEMENT]
lemma vector_N_pp:
  "vector x \<Longrightarrow> N x = --x \<sqinter> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector x \<Longrightarrow> N x = - x '
[PROOF STEP]
by (simp add: vector_complement_closed)


[STATEMENT]
lemma N_vector_pp [simp]:
  "N (x * top) = --(x * top) \<sqinter> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N (x * top) = - (x * top) '
[PROOF STEP]
by (simp add: comp_associative vector_complement_closed)


[STATEMENT]
lemma N_vector_top_pp [simp]:
  "N (x * top) * top = --(x * top)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N (x * top) * top = - - (x * top)
[PROOF STEP]
by (metis N_comp_top comp_associative vector_top_closed vector_complement_closed)


[STATEMENT]
lemma N_below_inf_one_pp:
  "N x \<le> --x \<sqinter> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N x \<le> - x '
[PROOF STEP]
using inf.sup_left_isotone p_antitone top_right_mult_increasing
[PROOF STATE]
proof (prove)
using this:
?y \<le> ?x \<Longrightarrow> ?y \<sqinter> ?z \<le> ?x \<sqinter> ?z
?x \<le> ?y \<Longrightarrow> - ?y \<le> - ?x
?x \<le> ?x * top

goal (1 subgoal):
 1. N x \<le> - x '
[PROOF STEP]
by auto


[STATEMENT]
lemma N_below_pp:
  "N x \<le> --x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N x \<le> - - x
[PROOF STEP]
using N_below_inf_one_pp
[PROOF STATE]
proof (prove)
using this:
N ?x \<le> - ?x '

goal (1 subgoal):
 1. N x \<le> - - x
[PROOF STEP]
by auto


[STATEMENT]
lemma N_comp_N:
  "N x * N y = -(-x * top) \<sqinter> -(-y * top) \<sqinter> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N x * N y = - (- x * top) \<sqinter> - (- y * top) \<sqinter> (1::'a)
[PROOF STEP]
by (simp add: N_comp inf.mult_assoc)


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


[STATEMENT]
lemma N_top [simp]:
  "N top = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N top = (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma n_split_omega_mult_pp:
  "xs * --xo = xo \<Longrightarrow> vector xo \<Longrightarrow> N top * xo = xs * N xo * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs * - - xo = xo; vector xo\<rbrakk> \<Longrightarrow> N top * xo = xs * N xo * top
[PROOF STEP]
by (metis N_top N_vector_top_pp comp_associative comp_left_one)


[STATEMENT]
lemma ee:
  assumes "vector v"
      and "e \<le> v * -v\<^sup>T"
    shows "e * e = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e * e = bot
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. e * e = bot
[PROOF STEP]
have "e * v \<le> bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e * v \<le> bot
[PROOF STEP]
by (metis assms covector_vector_comp comp_associative mult_left_isotone mult_right_zero)
[PROOF STATE]
proof (state)
this:
e * v \<le> bot

goal (1 subgoal):
 1. e * e = bot
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
e * v \<le> bot

goal (1 subgoal):
 1. e * e = bot
[PROOF STEP]
by (metis assms(2) bot_unique comp_associative mult_right_isotone semiring.mult_not_zero)
[PROOF STATE]
proof (state)
this:
e * e = bot

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma et:
  assumes "vector v"
      and "e \<le> v * -v\<^sup>T"
      and "t \<le> v * v\<^sup>T"
    shows "e * t = bot"
      and "e * t\<^sup>T = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e * t = bot &&& e * t\<^sup>T = bot
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. e * t = bot
 2. e * t\<^sup>T = bot
[PROOF STEP]
have "e * t \<le> v * -v\<^sup>T * v * v\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e * t \<le> v * - v\<^sup>T * v * v\<^sup>T
[PROOF STEP]
using assms(2-3) comp_isotone mult_assoc
[PROOF STATE]
proof (prove)
using this:
e \<le> v * - v\<^sup>T
t \<le> v * v\<^sup>T
\<lbrakk>?x \<le> ?y; ?w \<le> ?z\<rbrakk> \<Longrightarrow> ?x * ?w \<le> ?y * ?z
?a * ?b * ?c = ?a * (?b * ?c)

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

goal (2 subgoals):
 1. e * t = bot
 2. e * t\<^sup>T = bot
[PROOF STEP]
thus "e * t = bot"
[PROOF STATE]
proof (prove)
using this:
e * t \<le> v * - v\<^sup>T * v * v\<^sup>T

goal (1 subgoal):
 1. e * t = bot
[PROOF STEP]
by (simp add: assms(1) covector_vector_comp le_bot mult_assoc)
[PROOF STATE]
proof (state)
this:
e * t = bot

goal (1 subgoal):
 1. e * t\<^sup>T = bot
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. e * t\<^sup>T = bot
[PROOF STEP]
have "t\<^sup>T \<le> v * v\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t\<^sup>T \<le> v * v\<^sup>T
[PROOF STEP]
using assms(3) conv_order conv_dist_comp
[PROOF STATE]
proof (prove)
using this:
t \<le> v * v\<^sup>T
(?x \<le> ?y) = (?x\<^sup>T \<le> ?y\<^sup>T)
(?x * ?y)\<^sup>T = ?y\<^sup>T * ?x\<^sup>T

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

goal (1 subgoal):
 1. e * t\<^sup>T = bot
[PROOF STEP]
hence "e * t\<^sup>T \<le> v * -v\<^sup>T * v * v\<^sup>T"
[PROOF STATE]
proof (prove)
using this:
t\<^sup>T \<le> v * v\<^sup>T

goal (1 subgoal):
 1. e * t\<^sup>T \<le> v * - v\<^sup>T * v * v\<^sup>T
[PROOF STEP]
by (metis assms(2) comp_associative comp_isotone)
[PROOF STATE]
proof (state)
this:
e * t\<^sup>T \<le> v * - v\<^sup>T * v * v\<^sup>T

goal (1 subgoal):
 1. e * t\<^sup>T = bot
[PROOF STEP]
thus "e * t\<^sup>T = bot"
[PROOF STATE]
proof (prove)
using this:
e * t\<^sup>T \<le> v * - v\<^sup>T * v * v\<^sup>T

goal (1 subgoal):
 1. e * t\<^sup>T = bot
[PROOF STEP]
by (simp add: assms(1) covector_vector_comp le_bot mult_assoc)
[PROOF STATE]
proof (state)
this:
e * t\<^sup>T = bot

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ve_dist:
  assumes "e \<le> v * -v\<^sup>T"
      and "vector v"
      and "arc e"
    shows "(v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T = v * v\<^sup>T \<squnion> v * v\<^sup>T * e \<squnion> e\<^sup>T * v * v\<^sup>T \<squnion> e\<^sup>T * e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T = v * v\<^sup>T \<squnion> v * v\<^sup>T * e \<squnion> e\<^sup>T * v * v\<^sup>T \<squnion> e\<^sup>T * e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T = v * v\<^sup>T \<squnion> v * v\<^sup>T * e \<squnion> e\<^sup>T * v * v\<^sup>T \<squnion> e\<^sup>T * e
[PROOF STEP]
have "e \<le> v * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e \<le> v * top
[PROOF STEP]
using assms(1) comp_right_isotone dual_order.trans top_greatest
[PROOF STATE]
proof (prove)
using this:
e \<le> v * - v\<^sup>T
?x \<le> ?y \<Longrightarrow> ?z * ?x \<le> ?z * ?y
\<lbrakk>?b \<le> ?a; ?c \<le> ?b\<rbrakk> \<Longrightarrow> ?c \<le> ?a
?x \<le> top

goal (1 subgoal):
 1. e \<le> v * top
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
e \<le> v * top

goal (1 subgoal):
 1. (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T = v * v\<^sup>T \<squnion> v * v\<^sup>T * e \<squnion> e\<^sup>T * v * v\<^sup>T \<squnion> e\<^sup>T * e
[PROOF STEP]
hence "v * top * e = v * top * (v * top \<sqinter> e)"
[PROOF STATE]
proof (prove)
using this:
e \<le> v * top

goal (1 subgoal):
 1. v * top * e = v * top * (v * top \<sqinter> e)
[PROOF STEP]
by (simp add: inf.absorb2)
[PROOF STATE]
proof (state)
this:
v * top * e = v * top * (v * top \<sqinter> e)

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

goal (1 subgoal):
 1. (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T = v * v\<^sup>T \<squnion> v * v\<^sup>T * e \<squnion> e\<^sup>T * v * v\<^sup>T \<squnion> e\<^sup>T * e
[PROOF STEP]
have "... = (v * top \<sqinter> top * v\<^sup>T) * e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v * top * (v * top \<sqinter> e) = (v * top \<sqinter> top * v\<^sup>T) * e
[PROOF STEP]
using assms(2) covector_inf_comp_3 vector_conv_covector
[PROOF STATE]
proof (prove)
using this:
vector v
vector ?x \<Longrightarrow> (?y \<sqinter> ?x\<^sup>T) * ?z = ?y * (?x \<sqinter> ?z)
vector ?v = covector (?v\<^sup>T)

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

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

goal (1 subgoal):
 1. (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T = v * v\<^sup>T \<squnion> v * v\<^sup>T * e \<squnion> e\<^sup>T * v * v\<^sup>T \<squnion> e\<^sup>T * e
[PROOF STEP]
have "... = v * top * v\<^sup>T * e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v * top \<sqinter> top * v\<^sup>T) * e = v * top * v\<^sup>T * e
[PROOF STEP]
by (metis assms(2) inf_top_right vector_inf_comp)
[PROOF STATE]
proof (state)
this:
(v * top \<sqinter> top * v\<^sup>T) * e = v * top * v\<^sup>T * e

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

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

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

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

goal (1 subgoal):
 1. (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T = v * v\<^sup>T \<squnion> v * v\<^sup>T * e \<squnion> e\<^sup>T * v * v\<^sup>T \<squnion> e\<^sup>T * e
[PROOF STEP]
have "e\<^sup>T * top * e \<le> e\<^sup>T * top * e * e\<^sup>T * e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e\<^sup>T * top * e \<le> e\<^sup>T * top * e * e\<^sup>T * e
[PROOF STEP]
using ex231c comp_associative mult_right_isotone
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?x * ?x\<^sup>T * ?x
?x * ?y * ?z = ?x * (?y * ?z)
?x \<le> ?y \<Longrightarrow> ?z * ?x \<le> ?z * ?y

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

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

goal (1 subgoal):
 1. (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T = v * v\<^sup>T \<squnion> v * v\<^sup>T * e \<squnion> e\<^sup>T * v * v\<^sup>T \<squnion> e\<^sup>T * e
[PROOF STEP]
have "... \<le> e\<^sup>T * e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e\<^sup>T * top * e * e\<^sup>T * e \<le> e\<^sup>T * e
[PROOF STEP]
by (metis assms(3) coreflexive_comp_top_inf le_infE mult_semi_associative point_injective)
[PROOF STATE]
proof (state)
this:
e\<^sup>T * top * e * e\<^sup>T * e \<le> e\<^sup>T * e

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

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

goal (1 subgoal):
 1. (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T = v * v\<^sup>T \<squnion> v * v\<^sup>T * e \<squnion> e\<^sup>T * v * v\<^sup>T \<squnion> e\<^sup>T * e
[PROOF STEP]
have "(v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T = (v \<squnion> e\<^sup>T * top) * (v\<^sup>T \<squnion> top * e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T = (v \<squnion> e\<^sup>T * top) * (v\<^sup>T \<squnion> top * e)
[PROOF STEP]
by (simp add: conv_dist_comp conv_dist_sup)
[PROOF STATE]
proof (state)
this:
(v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T = (v \<squnion> e\<^sup>T * top) * (v\<^sup>T \<squnion> top * e)

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

goal (1 subgoal):
 1. (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T = v * v\<^sup>T \<squnion> v * v\<^sup>T * e \<squnion> e\<^sup>T * v * v\<^sup>T \<squnion> e\<^sup>T * e
[PROOF STEP]
have "... = v * v\<^sup>T \<squnion> v * top * e \<squnion> e\<^sup>T * top * v\<^sup>T \<squnion> e\<^sup>T * top * top * e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v \<squnion> e\<^sup>T * top) * (v\<^sup>T \<squnion> top * e) = v * v\<^sup>T \<squnion> v * top * e \<squnion> e\<^sup>T * top * v\<^sup>T \<squnion> e\<^sup>T * top * top * e
[PROOF STEP]
by (metis semiring.distrib_left semiring.distrib_right sup_assoc mult_assoc)
[PROOF STATE]
proof (state)
this:
(v \<squnion> e\<^sup>T * top) * (v\<^sup>T \<squnion> top * e) = v * v\<^sup>T \<squnion> v * top * e \<squnion> e\<^sup>T * top * v\<^sup>T \<squnion> e\<^sup>T * top * top * e

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

goal (1 subgoal):
 1. (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T = v * v\<^sup>T \<squnion> v * v\<^sup>T * e \<squnion> e\<^sup>T * v * v\<^sup>T \<squnion> e\<^sup>T * e
[PROOF STEP]
have "... = v * v\<^sup>T \<squnion> v * top * e \<squnion> (v * top * e)\<^sup>T \<squnion> e\<^sup>T * top * e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v * v\<^sup>T \<squnion> v * top * e \<squnion> e\<^sup>T * top * v\<^sup>T \<squnion> e\<^sup>T * top * top * e = v * v\<^sup>T \<squnion> v * top * e \<squnion> (v * top * e)\<^sup>T \<squnion> e\<^sup>T * top * e
[PROOF STEP]
by (simp add: comp_associative conv_dist_comp)
[PROOF STATE]
proof (state)
this:
v * v\<^sup>T \<squnion> v * top * e \<squnion> e\<^sup>T * top * v\<^sup>T \<squnion> e\<^sup>T * top * top * e = v * v\<^sup>T \<squnion> v * top * e \<squnion> (v * top * e)\<^sup>T \<squnion> e\<^sup>T * top * e

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

goal (1 subgoal):
 1. (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T = v * v\<^sup>T \<squnion> v * v\<^sup>T * e \<squnion> e\<^sup>T * v * v\<^sup>T \<squnion> e\<^sup>T * e
[PROOF STEP]
have "... = v * v\<^sup>T \<squnion> v * v\<^sup>T * e \<squnion> (v * v\<^sup>T * e)\<^sup>T \<squnion> e\<^sup>T * e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v * v\<^sup>T \<squnion> v * top * e \<squnion> (v * top * e)\<^sup>T \<squnion> e\<^sup>T * top * e = v * v\<^sup>T \<squnion> v * v\<^sup>T * e \<squnion> (v * v\<^sup>T * e)\<^sup>T \<squnion> e\<^sup>T * e
[PROOF STEP]
using 1 2
[PROOF STATE]
proof (prove)
using this:
v * top * e = v * v\<^sup>T * e
e\<^sup>T * top * e = e\<^sup>T * e

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

goal (1 subgoal):
 1. (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T = v * v\<^sup>T \<squnion> v * v\<^sup>T * e \<squnion> e\<^sup>T * v * v\<^sup>T \<squnion> e\<^sup>T * e
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T = v * v\<^sup>T \<squnion> v * v\<^sup>T * e \<squnion> (v * v\<^sup>T * e)\<^sup>T \<squnion> e\<^sup>T * e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T = v * v\<^sup>T \<squnion> v * v\<^sup>T * e \<squnion> (v * v\<^sup>T * e)\<^sup>T \<squnion> e\<^sup>T * e

goal (1 subgoal):
 1. (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T = v * v\<^sup>T \<squnion> v * v\<^sup>T * e \<squnion> e\<^sup>T * v * v\<^sup>T \<squnion> e\<^sup>T * e
[PROOF STEP]
by (simp add: comp_associative conv_dist_comp)
[PROOF STATE]
proof (state)
this:
(v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T = v * v\<^sup>T \<squnion> v * v\<^sup>T * e \<squnion> e\<^sup>T * v * v\<^sup>T \<squnion> e\<^sup>T * e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ev:
  "vector v \<Longrightarrow> e \<le> v * -v\<^sup>T \<Longrightarrow> e * v = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vector v; e \<le> v * - v\<^sup>T\<rbrakk> \<Longrightarrow> e * v = bot
[PROOF STEP]
by (metis covector_vector_comp order.antisym bot_least comp_associative mult_left_isotone mult_right_zero)


[STATEMENT]
lemma vTeT:
  "vector v \<Longrightarrow> e \<le> v * -v\<^sup>T \<Longrightarrow> v\<^sup>T * e\<^sup>T = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vector v; e \<le> v * - v\<^sup>T\<rbrakk> \<Longrightarrow> v\<^sup>T * e\<^sup>T = bot
[PROOF STEP]
using conv_bot ev conv_dist_comp
[PROOF STATE]
proof (prove)
using this:
symmetric bot
\<lbrakk>vector ?v; ?e \<le> ?v * - ?v\<^sup>T\<rbrakk> \<Longrightarrow> ?e * ?v = bot
(?x * ?y)\<^sup>T = ?y\<^sup>T * ?x\<^sup>T

goal (1 subgoal):
 1. \<lbrakk>vector v; e \<le> v * - v\<^sup>T\<rbrakk> \<Longrightarrow> v\<^sup>T * e\<^sup>T = bot
[PROOF STEP]
by fastforce


[STATEMENT]
lemma prim_subgraph_inv:
  assumes "e \<le> v * -v\<^sup>T \<sqinter> g"
      and "t \<le> v * v\<^sup>T \<sqinter> g"
    shows "t \<squnion> e \<le> ((v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T) \<sqinter> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<squnion> e \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g
[PROOF STEP]
proof (rule sup_least)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g
 2. e \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g
[PROOF STEP]
have "t \<le> ((v \<squnion> e\<^sup>T * top) * v\<^sup>T) \<sqinter> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<le> (v \<squnion> e\<^sup>T * top) * v\<^sup>T \<sqinter> g
[PROOF STEP]
using assms(2) le_supI1 mult_right_dist_sup
[PROOF STATE]
proof (prove)
using this:
t \<le> v * v\<^sup>T \<sqinter> g
?x \<le> ?a \<Longrightarrow> ?x \<le> ?a \<squnion> ?b
(?x \<squnion> ?y) * ?z = ?x * ?z \<squnion> ?y * ?z

goal (1 subgoal):
 1. t \<le> (v \<squnion> e\<^sup>T * top) * v\<^sup>T \<sqinter> g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<le> (v \<squnion> e\<^sup>T * top) * v\<^sup>T \<sqinter> g

goal (2 subgoals):
 1. t \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g
 2. e \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
t \<le> (v \<squnion> e\<^sup>T * top) * v\<^sup>T \<sqinter> g

goal (2 subgoals):
 1. t \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g
 2. e \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g
[PROOF STEP]
have "... \<le> ((v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T) \<sqinter> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v \<squnion> e\<^sup>T * top) * v\<^sup>T \<sqinter> g \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g
[PROOF STEP]
using comp_right_isotone conv_dist_sup inf.sup_left_isotone
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> ?z * ?x \<le> ?z * ?y
(?x \<squnion> ?y)\<^sup>T = ?x\<^sup>T \<squnion> ?y\<^sup>T
?y \<le> ?x \<Longrightarrow> ?y \<sqinter> ?z \<le> ?x \<sqinter> ?z

goal (1 subgoal):
 1. (v \<squnion> e\<^sup>T * top) * v\<^sup>T \<sqinter> g \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(v \<squnion> e\<^sup>T * top) * v\<^sup>T \<sqinter> g \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g

goal (2 subgoals):
 1. t \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g
 2. e \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
t \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g
[PROOF STEP]
show "t \<le> ((v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T) \<sqinter> g"
[PROOF STATE]
proof (prove)
using this:
t \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g

goal (1 subgoal):
 1. t \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
t \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g

goal (1 subgoal):
 1. e \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. e \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g
[PROOF STEP]
have "e \<le> v * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e \<le> v * top
[PROOF STEP]
by (meson assms(1) inf.boundedE mult_right_isotone order.trans top.extremum)
[PROOF STATE]
proof (state)
this:
e \<le> v * top

goal (1 subgoal):
 1. e \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g
[PROOF STEP]
hence "e \<le> v * top \<sqinter> top * e"
[PROOF STATE]
proof (prove)
using this:
e \<le> v * top

goal (1 subgoal):
 1. e \<le> v * top \<sqinter> top * e
[PROOF STEP]
by (simp add: top_left_mult_increasing)
[PROOF STATE]
proof (state)
this:
e \<le> v * top \<sqinter> top * e

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

goal (1 subgoal):
 1. e \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g
[PROOF STEP]
have "... = v * top * e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v * top \<sqinter> top * e = v * top * e
[PROOF STEP]
by (metis inf_top_right vector_export_comp)
[PROOF STATE]
proof (state)
this:
v * top \<sqinter> top * e = v * top * e

goal (1 subgoal):
 1. e \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
e \<le> v * top * e
[PROOF STEP]
have "e \<le> v * top * e \<sqinter> g"
[PROOF STATE]
proof (prove)
using this:
e \<le> v * top * e

goal (1 subgoal):
 1. e \<le> v * top * e \<sqinter> g
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
e \<le> v * top * e
e \<le> v * - v\<^sup>T \<sqinter> g

goal (1 subgoal):
 1. e \<le> v * top * e \<sqinter> g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e \<le> v * top * e \<sqinter> g

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

goal (1 subgoal):
 1. e \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g
[PROOF STEP]
have "... = v * (e\<^sup>T * top)\<^sup>T \<sqinter> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v * top * e \<sqinter> g = v * (e\<^sup>T * top)\<^sup>T \<sqinter> g
[PROOF STEP]
by (simp add: comp_associative conv_dist_comp)
[PROOF STATE]
proof (state)
this:
v * top * e \<sqinter> g = v * (e\<^sup>T * top)\<^sup>T \<sqinter> g

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

goal (1 subgoal):
 1. e \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g
[PROOF STEP]
have "... \<le> v * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v * (e\<^sup>T * top)\<^sup>T \<sqinter> g \<le> v * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g
[PROOF STEP]
by (simp add: conv_dist_sup mult_left_dist_sup sup.assoc sup.orderI)
[PROOF STATE]
proof (state)
this:
v * (e\<^sup>T * top)\<^sup>T \<sqinter> g \<le> v * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g

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

goal (1 subgoal):
 1. e \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g
[PROOF STEP]
have "... \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g
[PROOF STEP]
using inf.sup_left_isotone mult_right_sub_dist_sup_left
[PROOF STATE]
proof (prove)
using this:
?y \<le> ?x \<Longrightarrow> ?y \<sqinter> ?z \<le> ?x \<sqinter> ?z
?x * ?z \<le> (?x \<squnion> ?y) * ?z

goal (1 subgoal):
 1. v * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g

goal (1 subgoal):
 1. e \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
e \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g
[PROOF STEP]
show "e \<le> ((v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T) \<sqinter> g"
[PROOF STATE]
proof (prove)
using this:
e \<le> (v \<squnion> e\<^sup>T * top) * (v \<squnion> e\<^sup>T * top)\<^sup>T \<sqinter> g

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma triple_schroeder_p:
  "x * y * z \<le> -w \<longleftrightarrow> x\<^sup>T * w * z\<^sup>T \<le> -y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * y * z \<le> - w) = (x\<^sup>T * w * z\<^sup>T \<le> - y)
[PROOF STEP]
using mult_assoc p_antitone_iff schroeder_3_p schroeder_4_p
[PROOF STATE]
proof (prove)
using this:
?a * ?b * ?c = ?a * (?b * ?c)
(?x \<le> - ?y) = (?y \<le> - ?x)
(?x * ?y \<le> - ?z) = (?x\<^sup>T * ?z \<le> - ?y)
(?x * ?y \<le> - ?z) = (?z * ?y\<^sup>T \<le> - ?x)

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


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

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


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

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


[STATEMENT]
lemma vector_conv_compl:
  "vector v \<Longrightarrow> top * -v\<^sup>T = -v\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector v \<Longrightarrow> covector (- v\<^sup>T)
[PROOF STEP]
by (simp add: covector_complement_closed vector_conv_covector)


[STATEMENT]
lemma comp_commute_below_diversity:
  "x * y \<le> -1 \<longleftrightarrow> y * x \<le> -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. irreflexive (x * y) = irreflexive (y * x)
[PROOF STEP]
by (metis comp_right_one conv_dist_comp conv_one schroeder_3_p schroeder_4_p)


[STATEMENT]
lemma comp_univalent_below_complement:
  "univalent x \<Longrightarrow> x * -y \<le> -(x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univalent x \<Longrightarrow> x * - y \<le> - (x * y)
[PROOF STEP]
by (metis p_inf pseudo_complement semiring.mult_zero_right univalent_comp_left_dist_inf)


[STATEMENT]
lemma comp_bijective_complement:
  "bijective y \<Longrightarrow> -x * y = -(x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bijective y \<Longrightarrow> - x * y = - (x * y)
[PROOF STEP]
using comp_injective_below_complement complement_conv_sub order.antisym shunt_bijective
[PROOF STATE]
proof (prove)
using this:
injective ?y \<Longrightarrow> - ?x * ?y \<le> - (?x * ?y)
- (?y * ?x) * ?x\<^sup>T \<le> - ?y
\<lbrakk>?a \<le> ?b; ?b \<le> ?a\<rbrakk> \<Longrightarrow> ?a = ?b
bijective ?z \<Longrightarrow> (?x \<le> ?y * ?z) = (?x * ?z\<^sup>T \<le> ?y)

goal (1 subgoal):
 1. bijective y \<Longrightarrow> - x * y = - (x * y)
[PROOF STEP]
by blast


[STATEMENT]
lemma comp_mapping_complement:
  "mapping x \<Longrightarrow> x * -y = -(x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mapping x \<Longrightarrow> x * - y = - (x * y)
[PROOF STEP]
by (metis (full_types) comp_bijective_complement conv_complement conv_dist_comp conv_involutive total_conv_surjective)


[STATEMENT]
lemma kruskal_injective_inv:
  assumes "injective f"
      and "covector q"
      and "q * f\<^sup>T \<le> q"
      and "e \<le> q"
      and "q * f\<^sup>T \<le> -e"
      and "injective e"
      and "q\<^sup>T * q \<sqinter> f\<^sup>T * f \<le> 1"
    shows "injective ((f \<sqinter> -q) \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. injective (f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. injective (f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e)
[PROOF STEP]
have 1: "(f \<sqinter> -q) * (f \<sqinter> -q)\<^sup>T \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. injective (f \<sqinter> - q)
[PROOF STEP]
by (simp add: assms(1) injective_inf_closed)
[PROOF STATE]
proof (state)
this:
injective (f \<sqinter> - q)

goal (1 subgoal):
 1. injective (f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e)
[PROOF STEP]
have 2: "(f \<sqinter> -q) * (f \<sqinter> q) \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive ((f \<sqinter> - q) * (f \<sqinter> q))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. coreflexive ((f \<sqinter> - q) * (f \<sqinter> q))
[PROOF STEP]
have 21: "bot = q * f\<^sup>T \<sqinter> - q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bot = q * f\<^sup>T \<sqinter> - q
[PROOF STEP]
by (metis assms(3) inf.sup_monoid.add_assoc inf.sup_right_divisibility inf_import_p inf_p)
[PROOF STATE]
proof (state)
this:
bot = q * f\<^sup>T \<sqinter> - q

goal (1 subgoal):
 1. coreflexive ((f \<sqinter> - q) * (f \<sqinter> q))
[PROOF STEP]
have "(f \<sqinter> -q) * (f \<sqinter> q) \<le> -q * f \<sqinter> q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<sqinter> - q) * (f \<sqinter> q) \<le> - q * f \<sqinter> q
[PROOF STEP]
by (metis assms(2) comp_inf_covector comp_isotone inf.cobounded2 inf.left_idem)
[PROOF STATE]
proof (state)
this:
(f \<sqinter> - q) * (f \<sqinter> q) \<le> - q * f \<sqinter> q

goal (1 subgoal):
 1. coreflexive ((f \<sqinter> - q) * (f \<sqinter> q))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(f \<sqinter> - q) * (f \<sqinter> q) \<le> - q * f \<sqinter> q

goal (1 subgoal):
 1. coreflexive ((f \<sqinter> - q) * (f \<sqinter> q))
[PROOF STEP]
have "... = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - q * f \<sqinter> q = bot
[PROOF STEP]
using 21 schroeder_2
[PROOF STATE]
proof (prove)
using this:
bot = q * f\<^sup>T \<sqinter> - q
(?x * ?y \<sqinter> ?z = bot) = (?z * ?y\<^sup>T \<sqinter> ?x = bot)

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

goal (1 subgoal):
 1. coreflexive ((f \<sqinter> - q) * (f \<sqinter> q))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(f \<sqinter> - q) * (f \<sqinter> q) \<le> bot
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(f \<sqinter> - q) * (f \<sqinter> q) \<le> bot

goal (1 subgoal):
 1. coreflexive ((f \<sqinter> - q) * (f \<sqinter> q))
[PROOF STEP]
by (simp add: bot_unique)
[PROOF STATE]
proof (state)
this:
coreflexive ((f \<sqinter> - q) * (f \<sqinter> q))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
coreflexive ((f \<sqinter> - q) * (f \<sqinter> q))

goal (1 subgoal):
 1. injective (f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e)
[PROOF STEP]
have 3: "(f \<sqinter> -q) * e\<^sup>T \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive ((f \<sqinter> - q) * e\<^sup>T)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. coreflexive ((f \<sqinter> - q) * e\<^sup>T)
[PROOF STEP]
have "(f \<sqinter> -q) * e\<^sup>T \<le> -q * e\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<sqinter> - q) * e\<^sup>T \<le> - q * e\<^sup>T
[PROOF STEP]
by (simp add: mult_left_isotone)
[PROOF STATE]
proof (state)
this:
(f \<sqinter> - q) * e\<^sup>T \<le> - q * e\<^sup>T

goal (1 subgoal):
 1. coreflexive ((f \<sqinter> - q) * e\<^sup>T)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(f \<sqinter> - q) * e\<^sup>T \<le> - q * e\<^sup>T

goal (1 subgoal):
 1. coreflexive ((f \<sqinter> - q) * e\<^sup>T)
[PROOF STEP]
have "... = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - q * e\<^sup>T = bot
[PROOF STEP]
by (metis assms(2,4) bot_unique conv_bot conv_complement covector_complement_closed p_antitone p_bot regular_closed_bot schroeder_5_p)
[PROOF STATE]
proof (state)
this:
- q * e\<^sup>T = bot

goal (1 subgoal):
 1. coreflexive ((f \<sqinter> - q) * e\<^sup>T)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(f \<sqinter> - q) * e\<^sup>T \<le> bot
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(f \<sqinter> - q) * e\<^sup>T \<le> bot

goal (1 subgoal):
 1. coreflexive ((f \<sqinter> - q) * e\<^sup>T)
[PROOF STEP]
by (simp add: bot_unique)
[PROOF STATE]
proof (state)
this:
coreflexive ((f \<sqinter> - q) * e\<^sup>T)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
coreflexive ((f \<sqinter> - q) * e\<^sup>T)

goal (1 subgoal):
 1. injective (f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e)
[PROOF STEP]
have 4: "(f \<sqinter> q)\<^sup>T * (f \<sqinter> -q)\<^sup>T \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive ((f \<sqinter> q)\<^sup>T * (f \<sqinter> - q)\<^sup>T)
[PROOF STEP]
using 2 conv_dist_comp conv_isotone
[PROOF STATE]
proof (prove)
using this:
coreflexive ((f \<sqinter> - q) * (f \<sqinter> q))
(?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. coreflexive ((f \<sqinter> q)\<^sup>T * (f \<sqinter> - q)\<^sup>T)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
coreflexive ((f \<sqinter> q)\<^sup>T * (f \<sqinter> - q)\<^sup>T)

goal (1 subgoal):
 1. injective (f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e)
[PROOF STEP]
have 5: "(f \<sqinter> q)\<^sup>T * (f \<sqinter> q) \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univalent (f \<sqinter> q)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. univalent (f \<sqinter> q)
[PROOF STEP]
have "(f \<sqinter> q)\<^sup>T * (f \<sqinter> q) \<le> q\<^sup>T * q \<sqinter> f\<^sup>T * f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<sqinter> q)\<^sup>T * (f \<sqinter> q) \<le> q\<^sup>T * q \<sqinter> f\<^sup>T * f
[PROOF STEP]
by (simp add: conv_isotone mult_isotone)
[PROOF STATE]
proof (state)
this:
(f \<sqinter> q)\<^sup>T * (f \<sqinter> q) \<le> q\<^sup>T * q \<sqinter> f\<^sup>T * f

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

goal (1 subgoal):
 1. univalent (f \<sqinter> q)
[PROOF STEP]
have "... \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive (q\<^sup>T * q \<sqinter> f\<^sup>T * f)
[PROOF STEP]
by (simp add: assms(7))
[PROOF STATE]
proof (state)
this:
coreflexive (q\<^sup>T * q \<sqinter> f\<^sup>T * f)

goal (1 subgoal):
 1. univalent (f \<sqinter> q)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
univalent (f \<sqinter> q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
univalent (f \<sqinter> q)

goal (1 subgoal):
 1. univalent (f \<sqinter> q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
univalent (f \<sqinter> q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
univalent (f \<sqinter> q)

goal (1 subgoal):
 1. injective (f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e)
[PROOF STEP]
have 6: "(f \<sqinter> q)\<^sup>T * e\<^sup>T \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive ((f \<sqinter> q)\<^sup>T * e\<^sup>T)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. coreflexive ((f \<sqinter> q)\<^sup>T * e\<^sup>T)
[PROOF STEP]
have "f\<^sup>T * e\<^sup>T \<le> -q\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f\<^sup>T * e\<^sup>T \<le> - q\<^sup>T
[PROOF STEP]
using assms(5) schroeder_5_p
[PROOF STATE]
proof (prove)
using this:
q * f\<^sup>T \<le> - e
(?x * ?y \<le> - ?z) = (?y * ?z\<^sup>T \<le> - ?x\<^sup>T)

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

goal (1 subgoal):
 1. coreflexive ((f \<sqinter> q)\<^sup>T * e\<^sup>T)
[PROOF STEP]
hence "(f \<sqinter> q)\<^sup>T * e\<^sup>T = bot"
[PROOF STATE]
proof (prove)
using this:
f\<^sup>T * e\<^sup>T \<le> - q\<^sup>T

goal (1 subgoal):
 1. (f \<sqinter> q)\<^sup>T * e\<^sup>T = bot
[PROOF STEP]
by (metis assms(2,5) conv_bot conv_dist_comp covector_comp_inf inf.absorb1 inf.cobounded2 inf.sup_monoid.add_commute inf_left_commute inf_p schroeder_4_p)
[PROOF STATE]
proof (state)
this:
(f \<sqinter> q)\<^sup>T * e\<^sup>T = bot

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

goal (1 subgoal):
 1. coreflexive ((f \<sqinter> q)\<^sup>T * e\<^sup>T)
[PROOF STEP]
by (simp add: bot_unique)
[PROOF STATE]
proof (state)
this:
coreflexive ((f \<sqinter> q)\<^sup>T * e\<^sup>T)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
coreflexive ((f \<sqinter> q)\<^sup>T * e\<^sup>T)

goal (1 subgoal):
 1. injective (f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e)
[PROOF STEP]
have 7: "e * (f \<sqinter> -q)\<^sup>T \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive (e * (f \<sqinter> - q)\<^sup>T)
[PROOF STEP]
using 3 conv_dist_comp coreflexive_symmetric
[PROOF STATE]
proof (prove)
using this:
coreflexive ((f \<sqinter> - q) * e\<^sup>T)
(?x * ?y)\<^sup>T = ?y\<^sup>T * ?x\<^sup>T
coreflexive ?x \<Longrightarrow> symmetric ?x

goal (1 subgoal):
 1. coreflexive (e * (f \<sqinter> - q)\<^sup>T)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
coreflexive (e * (f \<sqinter> - q)\<^sup>T)

goal (1 subgoal):
 1. injective (f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e)
[PROOF STEP]
have 8: "e * (f \<sqinter> q) \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive (e * (f \<sqinter> q))
[PROOF STEP]
using 6 conv_dist_comp coreflexive_symmetric
[PROOF STATE]
proof (prove)
using this:
coreflexive ((f \<sqinter> q)\<^sup>T * e\<^sup>T)
(?x * ?y)\<^sup>T = ?y\<^sup>T * ?x\<^sup>T
coreflexive ?x \<Longrightarrow> symmetric ?x

goal (1 subgoal):
 1. coreflexive (e * (f \<sqinter> q))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
coreflexive (e * (f \<sqinter> q))

goal (1 subgoal):
 1. injective (f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e)
[PROOF STEP]
have 9: "e * e\<^sup>T \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. injective e
[PROOF STEP]
by (simp add: assms(6))
[PROOF STATE]
proof (state)
this:
injective e

goal (1 subgoal):
 1. injective (f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e)
[PROOF STEP]
have "((f \<sqinter> -q) \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e) * ((f \<sqinter> -q) \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e)\<^sup>T = (f \<sqinter> -q) * (f \<sqinter> -q)\<^sup>T \<squnion> (f \<sqinter> -q) * (f \<sqinter> q) \<squnion> (f \<sqinter> -q) * e\<^sup>T \<squnion> (f \<sqinter> q)\<^sup>T * (f \<sqinter> -q)\<^sup>T \<squnion> (f \<sqinter> q)\<^sup>T * (f \<sqinter> q) \<squnion> (f \<sqinter> q)\<^sup>T * e\<^sup>T \<squnion> e * (f \<sqinter> -q)\<^sup>T \<squnion> e * (f \<sqinter> q) \<squnion> e * e\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e) * (f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e)\<^sup>T = (f \<sqinter> - q) * (f \<sqinter> - q)\<^sup>T \<squnion> (f \<sqinter> - q) * (f \<sqinter> q) \<squnion> (f \<sqinter> - q) * e\<^sup>T \<squnion> (f \<sqinter> q)\<^sup>T * (f \<sqinter> - q)\<^sup>T \<squnion> (f \<sqinter> q)\<^sup>T * (f \<sqinter> q) \<squnion> (f \<sqinter> q)\<^sup>T * e\<^sup>T \<squnion> e * (f \<sqinter> - q)\<^sup>T \<squnion> e * (f \<sqinter> q) \<squnion> e * e\<^sup>T
[PROOF STEP]
using comp_left_dist_sup comp_right_dist_sup conv_dist_sup sup.assoc
[PROOF STATE]
proof (prove)
using this:
?x * ?y \<squnion> ?x * ?z = ?x * (?y \<squnion> ?z)
(?x \<squnion> ?y) * ?z = ?x * ?z \<squnion> ?y * ?z
(?x \<squnion> ?y)\<^sup>T = ?x\<^sup>T \<squnion> ?y\<^sup>T
?a \<squnion> ?b \<squnion> ?c = ?a \<squnion> (?b \<squnion> ?c)

goal (1 subgoal):
 1. (f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e) * (f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e)\<^sup>T = (f \<sqinter> - q) * (f \<sqinter> - q)\<^sup>T \<squnion> (f \<sqinter> - q) * (f \<sqinter> q) \<squnion> (f \<sqinter> - q) * e\<^sup>T \<squnion> (f \<sqinter> q)\<^sup>T * (f \<sqinter> - q)\<^sup>T \<squnion> (f \<sqinter> q)\<^sup>T * (f \<sqinter> q) \<squnion> (f \<sqinter> q)\<^sup>T * e\<^sup>T \<squnion> e * (f \<sqinter> - q)\<^sup>T \<squnion> e * (f \<sqinter> q) \<squnion> e * e\<^sup>T
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e) * (f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e)\<^sup>T = (f \<sqinter> - q) * (f \<sqinter> - q)\<^sup>T \<squnion> (f \<sqinter> - q) * (f \<sqinter> q) \<squnion> (f \<sqinter> - q) * e\<^sup>T \<squnion> (f \<sqinter> q)\<^sup>T * (f \<sqinter> - q)\<^sup>T \<squnion> (f \<sqinter> q)\<^sup>T * (f \<sqinter> q) \<squnion> (f \<sqinter> q)\<^sup>T * e\<^sup>T \<squnion> e * (f \<sqinter> - q)\<^sup>T \<squnion> e * (f \<sqinter> q) \<squnion> e * e\<^sup>T

goal (1 subgoal):
 1. injective (f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e) * (f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e)\<^sup>T = (f \<sqinter> - q) * (f \<sqinter> - q)\<^sup>T \<squnion> (f \<sqinter> - q) * (f \<sqinter> q) \<squnion> (f \<sqinter> - q) * e\<^sup>T \<squnion> (f \<sqinter> q)\<^sup>T * (f \<sqinter> - q)\<^sup>T \<squnion> (f \<sqinter> q)\<^sup>T * (f \<sqinter> q) \<squnion> (f \<sqinter> q)\<^sup>T * e\<^sup>T \<squnion> e * (f \<sqinter> - q)\<^sup>T \<squnion> e * (f \<sqinter> q) \<squnion> e * e\<^sup>T

goal (1 subgoal):
 1. injective (f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e)
[PROOF STEP]
have "... \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive ((f \<sqinter> - q) * (f \<sqinter> - q)\<^sup>T \<squnion> (f \<sqinter> - q) * (f \<sqinter> q) \<squnion> (f \<sqinter> - q) * e\<^sup>T \<squnion> (f \<sqinter> q)\<^sup>T * (f \<sqinter> - q)\<^sup>T \<squnion> (f \<sqinter> q)\<^sup>T * (f \<sqinter> q) \<squnion> (f \<sqinter> q)\<^sup>T * e\<^sup>T \<squnion> e * (f \<sqinter> - q)\<^sup>T \<squnion> e * (f \<sqinter> q) \<squnion> e * e\<^sup>T)
[PROOF STEP]
using 1 2 3 4 5 6 7 8 9
[PROOF STATE]
proof (prove)
using this:
injective (f \<sqinter> - q)
coreflexive ((f \<sqinter> - q) * (f \<sqinter> q))
coreflexive ((f \<sqinter> - q) * e\<^sup>T)
coreflexive ((f \<sqinter> q)\<^sup>T * (f \<sqinter> - q)\<^sup>T)
univalent (f \<sqinter> q)
coreflexive ((f \<sqinter> q)\<^sup>T * e\<^sup>T)
coreflexive (e * (f \<sqinter> - q)\<^sup>T)
coreflexive (e * (f \<sqinter> q))
injective e

goal (1 subgoal):
 1. coreflexive ((f \<sqinter> - q) * (f \<sqinter> - q)\<^sup>T \<squnion> (f \<sqinter> - q) * (f \<sqinter> q) \<squnion> (f \<sqinter> - q) * e\<^sup>T \<squnion> (f \<sqinter> q)\<^sup>T * (f \<sqinter> - q)\<^sup>T \<squnion> (f \<sqinter> q)\<^sup>T * (f \<sqinter> q) \<squnion> (f \<sqinter> q)\<^sup>T * e\<^sup>T \<squnion> e * (f \<sqinter> - q)\<^sup>T \<squnion> e * (f \<sqinter> q) \<squnion> e * e\<^sup>T)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
coreflexive ((f \<sqinter> - q) * (f \<sqinter> - q)\<^sup>T \<squnion> (f \<sqinter> - q) * (f \<sqinter> q) \<squnion> (f \<sqinter> - q) * e\<^sup>T \<squnion> (f \<sqinter> q)\<^sup>T * (f \<sqinter> - q)\<^sup>T \<squnion> (f \<sqinter> q)\<^sup>T * (f \<sqinter> q) \<squnion> (f \<sqinter> q)\<^sup>T * e\<^sup>T \<squnion> e * (f \<sqinter> - q)\<^sup>T \<squnion> e * (f \<sqinter> q) \<squnion> e * e\<^sup>T)

goal (1 subgoal):
 1. injective (f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
injective (f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
injective (f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e)

goal (1 subgoal):
 1. injective (f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
injective (f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma kruskal_exchange_injective_inv_1:
  assumes "injective f"
      and "covector q"
      and "q * f\<^sup>T \<le> q"
      and "q\<^sup>T * q \<sqinter> f\<^sup>T * f \<le> 1"
    shows "injective ((f \<sqinter> -q) \<squnion> (f \<sqinter> q)\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. injective (f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T)
[PROOF STEP]
using kruskal_injective_inv[where e=bot]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>injective ?f; covector ?q; ?q * ?f\<^sup>T \<le> ?q; bot \<le> ?q; ?q * ?f\<^sup>T \<le> - bot; injective bot; coreflexive (?q\<^sup>T * ?q \<sqinter> ?f\<^sup>T * ?f)\<rbrakk> \<Longrightarrow> injective (?f \<sqinter> - ?q \<squnion> (?f \<sqinter> ?q)\<^sup>T \<squnion> bot)

goal (1 subgoal):
 1. injective (f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T)
[PROOF STEP]
by (simp add: assms)


[STATEMENT]
lemma kruskal_exchange_acyclic_inv_3:
  assumes "injective w"
      and "d \<le> w"
    shows "(w \<sqinter> -d) * d\<^sup>T * top = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w \<sqinter> - d) * d\<^sup>T * top = bot
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (w \<sqinter> - d) * d\<^sup>T * top = bot
[PROOF STEP]
have "(w \<sqinter> -d) * d\<^sup>T * top = (w \<sqinter> -d \<sqinter> (d\<^sup>T * top)\<^sup>T) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w \<sqinter> - d) * d\<^sup>T * top = (w \<sqinter> - d \<sqinter> (d\<^sup>T * top)\<^sup>T) * top
[PROOF STEP]
by (simp add: comp_associative comp_inf_vector_1 conv_dist_comp)
[PROOF STATE]
proof (state)
this:
(w \<sqinter> - d) * d\<^sup>T * top = (w \<sqinter> - d \<sqinter> (d\<^sup>T * top)\<^sup>T) * top

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

goal (1 subgoal):
 1. (w \<sqinter> - d) * d\<^sup>T * top = bot
[PROOF STEP]
have "... = (w \<sqinter> top * d \<sqinter> -d) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w \<sqinter> - d \<sqinter> (d\<^sup>T * top)\<^sup>T) * top = (w \<sqinter> top * d \<sqinter> - d) * top
[PROOF STEP]
by (simp add: conv_dist_comp inf_commute inf_left_commute)
[PROOF STATE]
proof (state)
this:
(w \<sqinter> - d \<sqinter> (d\<^sup>T * top)\<^sup>T) * top = (w \<sqinter> top * d \<sqinter> - d) * top

goal (1 subgoal):
 1. (w \<sqinter> - d) * d\<^sup>T * top = bot
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(w \<sqinter> - d) * d\<^sup>T * top = (w \<sqinter> top * d \<sqinter> - d) * top
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(w \<sqinter> - d) * d\<^sup>T * top = (w \<sqinter> top * d \<sqinter> - d) * top

goal (1 subgoal):
 1. (w \<sqinter> - d) * d\<^sup>T * top = bot
[PROOF STEP]
using assms epm_3
[PROOF STATE]
proof (prove)
using this:
(w \<sqinter> - d) * d\<^sup>T * top = (w \<sqinter> top * d \<sqinter> - d) * top
injective w
d \<le> w
\<lbrakk>?e \<le> ?w; injective ?w\<rbrakk> \<Longrightarrow> ?e = ?w \<sqinter> top * ?e

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma kruskal_subgraph_inv:
  assumes "f \<le> --(-h \<sqinter> g)"
      and "e \<le> --g"
      and "symmetric h"
      and "symmetric g"
    shows "(f \<sqinter> -q) \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e \<le> --(-(h \<sqinter> -e \<sqinter> -e\<^sup>T) \<sqinter> g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e \<le> - - (- (h \<sqinter> - e \<sqinter> - e\<^sup>T) \<sqinter> g)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e \<le> - - (- (h \<sqinter> - e \<sqinter> - e\<^sup>T) \<sqinter> g)
[PROOF STEP]
let ?f = "(f \<sqinter> -q) \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e \<le> - - (- (h \<sqinter> - e \<sqinter> - e\<^sup>T) \<sqinter> g)
[PROOF STEP]
let ?h = "h \<sqinter> -e \<sqinter> -e\<^sup>T"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e \<le> - - (- (h \<sqinter> - e \<sqinter> - e\<^sup>T) \<sqinter> g)
[PROOF STEP]
have 1: "f \<sqinter> -q \<le> -h \<sqinter> --g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<sqinter> - q \<le> - h \<sqinter> - - g
[PROOF STEP]
using assms(1) inf.coboundedI1
[PROOF STATE]
proof (prove)
using this:
f \<le> - - (- h \<sqinter> g)
?a \<le> ?c \<Longrightarrow> ?a \<sqinter> ?b \<le> ?c

goal (1 subgoal):
 1. f \<sqinter> - q \<le> - h \<sqinter> - - g
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f \<sqinter> - q \<le> - h \<sqinter> - - g

goal (1 subgoal):
 1. f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e \<le> - - (- (h \<sqinter> - e \<sqinter> - e\<^sup>T) \<sqinter> g)
[PROOF STEP]
have "(f \<sqinter> q)\<^sup>T \<le> (-h \<sqinter> --g)\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<sqinter> q)\<^sup>T \<le> (- h \<sqinter> - - g)\<^sup>T
[PROOF STEP]
using assms(1) inf.coboundedI1 conv_isotone
[PROOF STATE]
proof (prove)
using this:
f \<le> - - (- h \<sqinter> g)
?a \<le> ?c \<Longrightarrow> ?a \<sqinter> ?b \<le> ?c
?x \<le> ?y \<Longrightarrow> ?x\<^sup>T \<le> ?y\<^sup>T

goal (1 subgoal):
 1. (f \<sqinter> q)\<^sup>T \<le> (- h \<sqinter> - - g)\<^sup>T
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(f \<sqinter> q)\<^sup>T \<le> (- h \<sqinter> - - g)\<^sup>T

goal (1 subgoal):
 1. f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e \<le> - - (- (h \<sqinter> - e \<sqinter> - e\<^sup>T) \<sqinter> g)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(f \<sqinter> q)\<^sup>T \<le> (- h \<sqinter> - - g)\<^sup>T

goal (1 subgoal):
 1. f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e \<le> - - (- (h \<sqinter> - e \<sqinter> - e\<^sup>T) \<sqinter> g)
[PROOF STEP]
have "... = -h \<sqinter> --g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symmetric (- h \<sqinter> - - g)
[PROOF STEP]
using assms(3,4) conv_complement conv_dist_inf
[PROOF STATE]
proof (prove)
using this:
symmetric h
symmetric g
(- ?x)\<^sup>T = - ?x\<^sup>T
(?x \<sqinter> ?y)\<^sup>T = ?x\<^sup>T \<sqinter> ?y\<^sup>T

goal (1 subgoal):
 1. symmetric (- h \<sqinter> - - g)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
symmetric (- h \<sqinter> - - g)

goal (1 subgoal):
 1. f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e \<le> - - (- (h \<sqinter> - e \<sqinter> - e\<^sup>T) \<sqinter> g)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(f \<sqinter> q)\<^sup>T \<le> - h \<sqinter> - - g
[PROOF STEP]
have "?f \<le> (-h \<sqinter> --g) \<squnion> (e \<sqinter> --g)"
[PROOF STATE]
proof (prove)
using this:
(f \<sqinter> q)\<^sup>T \<le> - h \<sqinter> - - g

goal (1 subgoal):
 1. f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e \<le> - h \<sqinter> - - g \<squnion> e \<sqinter> - - g
[PROOF STEP]
using 1 assms(2) inf.absorb1 semiring.add_right_mono
[PROOF STATE]
proof (prove)
using this:
(f \<sqinter> q)\<^sup>T \<le> - h \<sqinter> - - g
f \<sqinter> - q \<le> - h \<sqinter> - - g
e \<le> - - g
?a \<le> ?b \<Longrightarrow> ?a \<sqinter> ?b = ?a
?a \<le> ?b \<Longrightarrow> ?a \<squnion> ?c \<le> ?b \<squnion> ?c

goal (1 subgoal):
 1. f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e \<le> - h \<sqinter> - - g \<squnion> e \<sqinter> - - g
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e \<le> - h \<sqinter> - - g \<squnion> e \<sqinter> - - g

goal (1 subgoal):
 1. f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e \<le> - - (- (h \<sqinter> - e \<sqinter> - e\<^sup>T) \<sqinter> g)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e \<le> - h \<sqinter> - - g \<squnion> e \<sqinter> - - g

goal (1 subgoal):
 1. f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e \<le> - - (- (h \<sqinter> - e \<sqinter> - e\<^sup>T) \<sqinter> g)
[PROOF STEP]
have "... \<le> (-h \<squnion> --e) \<sqinter> --g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - h \<sqinter> - - g \<squnion> e \<sqinter> - - g \<le> (- h \<squnion> - - e) \<sqinter> - - g
[PROOF STEP]
by (simp add: inf.coboundedI1 le_supI2 pp_increasing)
[PROOF STATE]
proof (state)
this:
- h \<sqinter> - - g \<squnion> e \<sqinter> - - g \<le> (- h \<squnion> - - e) \<sqinter> - - g

goal (1 subgoal):
 1. f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e \<le> - - (- (h \<sqinter> - e \<sqinter> - e\<^sup>T) \<sqinter> g)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- h \<sqinter> - - g \<squnion> e \<sqinter> - - g \<le> (- h \<squnion> - - e) \<sqinter> - - g

goal (1 subgoal):
 1. f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e \<le> - - (- (h \<sqinter> - e \<sqinter> - e\<^sup>T) \<sqinter> g)
[PROOF STEP]
have "... \<le> -?h \<sqinter> --g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- h \<squnion> - - e) \<sqinter> - - g \<le> - (h \<sqinter> - e \<sqinter> - e\<^sup>T) \<sqinter> - - g
[PROOF STEP]
using inf.sup_left_isotone order_trans p_antitone_inf p_supdist_inf
[PROOF STATE]
proof (prove)
using this:
?y \<le> ?x \<Longrightarrow> ?y \<sqinter> ?z \<le> ?x \<sqinter> ?z
\<lbrakk>?x \<le> ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x \<le> ?z
- ?x \<le> - (?x \<sqinter> ?y)
- ?x \<squnion> - ?y \<le> - (?x \<sqinter> ?y)

goal (1 subgoal):
 1. (- h \<squnion> - - e) \<sqinter> - - g \<le> - (h \<sqinter> - e \<sqinter> - e\<^sup>T) \<sqinter> - - g
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(- h \<squnion> - - e) \<sqinter> - - g \<le> - (h \<sqinter> - e \<sqinter> - e\<^sup>T) \<sqinter> - - g

goal (1 subgoal):
 1. f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e \<le> - - (- (h \<sqinter> - e \<sqinter> - e\<^sup>T) \<sqinter> g)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e \<le> - (h \<sqinter> - e \<sqinter> - e\<^sup>T) \<sqinter> - - g
[PROOF STEP]
show "?f \<le> --(-?h \<sqinter> g)"
[PROOF STATE]
proof (prove)
using this:
f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e \<le> - (h \<sqinter> - e \<sqinter> - e\<^sup>T) \<sqinter> - - g

goal (1 subgoal):
 1. f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e \<le> - - (- (h \<sqinter> - e \<sqinter> - e\<^sup>T) \<sqinter> g)
[PROOF STEP]
using inf_pp_semi_commute order_lesseq_imp
[PROOF STATE]
proof (prove)
using this:
f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e \<le> - (h \<sqinter> - e \<sqinter> - e\<^sup>T) \<sqinter> - - g
?x \<sqinter> - - ?y \<le> - - (?x \<sqinter> ?y)
(\<forall>z\<ge>?x. ?y \<le> z) = (?y \<le> ?x)

goal (1 subgoal):
 1. f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e \<le> - - (- (h \<sqinter> - e \<sqinter> - e\<^sup>T) \<sqinter> g)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<sqinter> - q \<squnion> (f \<sqinter> q)\<^sup>T \<squnion> e \<le> - - (- (h \<sqinter> - e \<sqinter> - e\<^sup>T) \<sqinter> g)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma antisymmetric_inf_diversity:
  "antisymmetric x \<Longrightarrow> x \<sqinter> -1 = x \<sqinter> -x\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. antisymmetric x \<Longrightarrow> x \<sqinter> - (1::'a) = x \<sqinter> - x\<^sup>T
[PROOF STEP]
by (smt (verit, del_insts) inf.orderE inf.sup_monoid.add_assoc inf.sup_monoid.add_commute inf_import_p one_inf_conv)


[STATEMENT]
lemma conv_complement_0_p [simp]:
  "(-x)\<^sup>T \<squnion> (--x)\<^sup>T = top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- x)\<^sup>T \<squnion> (- - x)\<^sup>T = top
[PROOF STEP]
by (metis conv_top conv_dist_sup stone)


[STATEMENT]
lemma theorem24xxiv_pp:
  "-(x * y) \<squnion> --(x * z) = -(x * (y \<sqinter> -z)) \<squnion> --(x * z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (x * y) \<squnion> - - (x * z) = - (x * (y \<sqinter> - z)) \<squnion> - - (x * z)
[PROOF STEP]
by (metis p_dist_inf theorem24xxiii)


[STATEMENT]
lemma asymmetric_linear:
  "asymmetric x \<longleftrightarrow> linear (-x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. asymmetric x = linear (- x)
[PROOF STEP]
by (metis conv_complement inf.distrib_left inf_p maddux_3_11_pp p_bot p_dist_inf)


[STATEMENT]
lemma strict_linear_asymmetric:
  "strict_linear x \<Longrightarrow> antisymmetric (-x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strict_linear x \<Longrightarrow> antisymmetric (- x)
[PROOF STEP]
by (metis conv_complement eq_refl p_dist_sup pp_one)


[STATEMENT]
lemma regular_complement_top:
  "regular x \<Longrightarrow> x \<squnion> -x = top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. regular x \<Longrightarrow> x \<squnion> - x = top
[PROOF STEP]
by (metis stone)


[STATEMENT]
lemma regular_mult_closed:
  "regular x \<Longrightarrow> regular y \<Longrightarrow> regular (x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>regular x; regular y\<rbrakk> \<Longrightarrow> regular (x * y)
[PROOF STEP]
by (simp add: pp_dist_comp)


[STATEMENT]
lemma regular_one_closed:
  "regular 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. regular (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma pp_total:
  "total (--x) \<longleftrightarrow> -(x*top) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. times_top_class.total (- - x) = dense (x * top)
[PROOF STEP]
by (simp add: dense_pp pp_dist_comp)


[STATEMENT]
lemma pp_surjective:
  "surjective (--x) \<longleftrightarrow> -(top*x) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surjective (- - x) = dense (top * x)
[PROOF STEP]
by (metis p_bot p_comp_pp p_top pp_dist_comp)


[STATEMENT]
lemma bijective_regular:
  "bijective x \<Longrightarrow> regular x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bijective x \<Longrightarrow> regular x
[PROOF STEP]
by (metis comp_bijective_complement mult_left_one regular_one_closed)


[STATEMENT]
lemma mapping_regular:
  "mapping x \<Longrightarrow> regular x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mapping x \<Longrightarrow> regular x
[PROOF STEP]
by (metis bijective_regular conv_complement conv_involutive total_conv_surjective)


[STATEMENT]
lemma arc_regular:
  assumes "arc x"
    shows "regular x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. regular x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. regular x
[PROOF STEP]
have "--x \<le> --(x * top \<sqinter> top * x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - - x \<le> - - (x * top \<sqinter> top * x)
[PROOF STEP]
by (simp add: pp_isotone top_left_mult_increasing top_right_mult_increasing)
[PROOF STATE]
proof (state)
this:
- - x \<le> - - (x * top \<sqinter> top * x)

goal (1 subgoal):
 1. regular x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- - x \<le> - - (x * top \<sqinter> top * x)

goal (1 subgoal):
 1. regular x
[PROOF STEP]
have "... = --(x * top) \<sqinter> --(top * x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - - (x * top \<sqinter> top * x) = - - (x * top) \<sqinter> - - (top * x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- - (x * top \<sqinter> top * x) = - - (x * top) \<sqinter> - - (top * x)

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

goal (1 subgoal):
 1. regular x
[PROOF STEP]
have "... = x * top \<sqinter> top * x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - - (x * top) \<sqinter> - - (top * x) = x * top \<sqinter> top * x
[PROOF STEP]
by (metis assms bijective_regular conv_top conv_dist_comp conv_involutive mapping_regular)
[PROOF STATE]
proof (state)
this:
- - (x * top) \<sqinter> - - (top * x) = x * top \<sqinter> top * x

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

goal (1 subgoal):
 1. regular x
[PROOF STEP]
have "... \<le> x * x\<^sup>T * top * x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * top \<sqinter> top * x \<le> x * x\<^sup>T * top * x
[PROOF STEP]
by (metis comp_associative dedekind_1 inf.commute inf_top.right_neutral)
[PROOF STATE]
proof (state)
this:
x * top \<sqinter> top * x \<le> x * x\<^sup>T * top * x

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

goal (1 subgoal):
 1. regular x
[PROOF STEP]
have "... \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * x\<^sup>T * top * x \<le> x
[PROOF STEP]
by (metis assms comp_right_one conv_top comp_associative conv_dist_comp conv_involutive mult_right_isotone vector_top_closed)
[PROOF STATE]
proof (state)
this:
x * x\<^sup>T * top * x \<le> x

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

goal (1 subgoal):
 1. regular x
[PROOF STEP]
by (simp add: order.antisym pp_increasing)
[PROOF STATE]
proof (state)
this:
regular x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma times_inf [simp]:
  "x * y = x \<sqinter> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y = x \<sqinter> y
[PROOF STEP]
by simp


[STATEMENT]
lemma times_dense:
  "x \<noteq> bot \<Longrightarrow> y \<noteq> bot \<Longrightarrow> x * y \<noteq> bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> bot; y \<noteq> bot\<rbrakk> \<Longrightarrow> x * y \<noteq> bot
[PROOF STEP]
using inf_dense min_inf times_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<noteq> bot; ?y \<noteq> bot\<rbrakk> \<Longrightarrow> ?x \<sqinter> ?y \<noteq> bot
min ?x ?y = ?x \<sqinter> ?y
?x * ?y = min ?x ?y

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> bot; y \<noteq> bot\<rbrakk> \<Longrightarrow> x * y \<noteq> bot
[PROOF STEP]
by presburger


[STATEMENT]
lemma conv_complement_0 [simp]:
  "x\<^sup>T \<squnion> (-x)\<^sup>T = top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>T \<squnion> (- x)\<^sup>T = top
[PROOF STEP]
by (simp add: conv_complement)


[STATEMENT]
lemma schroeder_3:
  "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]
by (simp add: schroeder_3_p)


[STATEMENT]
lemma schroeder_4:
  "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]
by (simp add: schroeder_4_p)


[STATEMENT]
lemma theorem24xxiv:
  "-(x * y) \<squnion> (x * z) = -(x * (y \<sqinter> -z)) \<squnion> (x * z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (x * y) \<squnion> x * z = - (x * (y \<sqinter> - z)) \<squnion> x * z
[PROOF STEP]
using theorem24xxiv_pp
[PROOF STATE]
proof (prove)
using this:
- (?x * ?y) \<squnion> - - (?x * ?z) = - (?x * (?y \<sqinter> - ?z)) \<squnion> - - (?x * ?z)

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


[STATEMENT]
lemma vector_N:
  "vector x \<Longrightarrow> N(x) = x \<sqinter> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector x \<Longrightarrow> N x = x \<sqinter> (1::'a)
[PROOF STEP]
by (simp add: vector_N_pp)


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


[STATEMENT]
lemma N_vector_top [simp]:
  "N(x * top) * top = x * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N (x * top) * top = x * top
[PROOF STEP]
using N_vector_top_pp
[PROOF STATE]
proof (prove)
using this:
N (?x * top) * top = - - (?x * top)

goal (1 subgoal):
 1. N (x * top) * top = x * top
[PROOF STEP]
by simp


[STATEMENT]
lemma N_below_inf_one:
  "N(x) \<le> x \<sqinter> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N x \<le> x \<sqinter> (1::'a)
[PROOF STEP]
using N_below_inf_one_pp
[PROOF STATE]
proof (prove)
using this:
N ?x \<le> - ?x '

goal (1 subgoal):
 1. N x \<le> x \<sqinter> (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma N_below:
  "N(x) \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N x \<le> x
[PROOF STEP]
using N_below_pp
[PROOF STATE]
proof (prove)
using this:
N ?x \<le> - - ?x

goal (1 subgoal):
 1. N x \<le> x
[PROOF STEP]
by simp


[STATEMENT]
lemma n_split_omega_mult:
  "xs * xo = xo \<Longrightarrow> xo * top = xo \<Longrightarrow> N(top) * xo = xs * N(xo) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs * xo = xo; vector xo\<rbrakk> \<Longrightarrow> N top * xo = xs * N xo * top
[PROOF STEP]
using n_split_omega_mult_pp
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?xs * - - ?xo = ?xo; vector ?xo\<rbrakk> \<Longrightarrow> N top * ?xo = ?xs * N ?xo * top

goal (1 subgoal):
 1. \<lbrakk>xs * xo = xo; vector xo\<rbrakk> \<Longrightarrow> N top * xo = xs * N xo * top
[PROOF STEP]
by simp


[STATEMENT]
lemma complement_vector:
  "vector v \<longleftrightarrow> vector (-v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector v = vector (- v)
[PROOF STEP]
using vector_complement_closed
[PROOF STATE]
proof (prove)
using this:
vector ?x \<Longrightarrow> vector (- ?x)

goal (1 subgoal):
 1. vector v = vector (- v)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma complement_covector:
  "covector v \<longleftrightarrow> covector (-v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. covector v = covector (- v)
[PROOF STEP]
using covector_complement_closed
[PROOF STATE]
proof (prove)
using this:
covector ?x \<Longrightarrow> covector (- ?x)

goal (1 subgoal):
 1. covector v = covector (- v)
[PROOF STEP]
by force


[STATEMENT]
lemma triple_schroeder:
  "x * y * z \<le> w \<longleftrightarrow> x\<^sup>T * -w * z\<^sup>T \<le> -y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * y * z \<le> w) = (x\<^sup>T * - w * z\<^sup>T \<le> - y)
[PROOF STEP]
by (simp add: triple_schroeder_p)


[STATEMENT]
lemma schroeder_5:
  "x * y \<le> z \<longleftrightarrow> y * -z\<^sup>T \<le> -x\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * y \<le> z) = (y * - z\<^sup>T \<le> - x\<^sup>T)
[PROOF STEP]
by (simp add: conv_complement schroeder_5_p)


[STATEMENT]
lemma schroeder_6:
  "x * y \<le> z \<longleftrightarrow> -z\<^sup>T * x \<le> -y\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * y \<le> z) = (- z\<^sup>T * x \<le> - y\<^sup>T)
[PROOF STEP]
by (simp add: conv_complement schroeder_5_p)