[STATEMENT]
lemma ss422iv:
  assumes "is_p_fun y"
      and "x \<le> y"
      and "y;1 \<le> x;1"
    shows "x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
have "y \<le> (x;1)\<cdot>y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<le> x ; 1 \<cdot> y
[PROOF STEP]
using assms(3) le_infI maddux_20 order_trans
[PROOF STATE]
proof (prove)
using this:
y ; 1 \<le> x ; 1
\<lbrakk>?x \<le> ?a; ?x \<le> ?b\<rbrakk> \<Longrightarrow> ?x \<le> ?a \<cdot> ?b
?x \<le> ?x ; 1
\<lbrakk>?x \<le> ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x \<le> ?z

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

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

goal (1 subgoal):
 1. x = y
[PROOF STEP]
have "... \<le> x;x\<^sup>T;y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x ; 1 \<cdot> y \<le> x ; x\<^sup>T ; y
[PROOF STEP]
by (metis inf_top_left modular_1_var comp_assoc)
[PROOF STATE]
proof (state)
this:
x ; 1 \<cdot> y \<le> x ; x\<^sup>T ; y

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

goal (1 subgoal):
 1. x = y
[PROOF STEP]
have "... \<le> x;y\<^sup>T;y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x ; x\<^sup>T ; y \<le> x ; y\<^sup>T ; y
[PROOF STEP]
using assms(2) conv_iso mult_double_iso
[PROOF STATE]
proof (prove)
using this:
x \<le> y
(?x \<le> ?y) = (?x\<^sup>T \<le> ?y\<^sup>T)
?x \<le> ?y \<Longrightarrow> ?w ; ?x ; ?z \<le> ?w ; ?y ; ?z

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

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

goal (1 subgoal):
 1. x = y
[PROOF STEP]
have "... \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x ; y\<^sup>T ; y \<le> x
[PROOF STEP]
using assms(1) comp_assoc is_p_fun_def mult_isol mult_1_right
[PROOF STATE]
proof (prove)
using this:
is_p_fun y
?x ; ?y ; ?z = ?x ; (?y ; ?z)
is_p_fun ?x \<equiv> ?x\<^sup>T ; ?x \<le> 1'
?x \<le> ?y \<Longrightarrow> ?z ; ?x \<le> ?z ; ?y
?a ; 1' = ?a

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

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

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by (simp add: assms(2) order.antisym)
[PROOF STATE]
proof (state)
this:
x = y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ss423bij:
  assumes "bijective x"
    shows "y ; x\<^sup>T \<le> z \<longleftrightarrow> y \<le> z ; x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y ; x\<^sup>T \<le> z) = (y \<le> z ; x)
[PROOF STEP]
by (simp add: assms is_map_def p_fun_inj ss423 total_sur)


[STATEMENT]
lemma inj_distr:
  assumes "is_inj z"
    shows "(x\<cdot>y);z = (x;z)\<cdot>(y;z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<cdot> y) ; z = x ; z \<cdot> y ; z
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (x \<cdot> y) ; z \<le> x ; z \<cdot> y ; z
 2. x ; z \<cdot> y ; z \<le> (x \<cdot> y) ; z
[PROOF STEP]
using mult_subdistr_var
[PROOF STATE]
proof (prove)
using this:
(?x \<cdot> ?y) ; ?z \<le> ?x ; ?z \<cdot> ?y ; ?z

goal (2 subgoals):
 1. (x \<cdot> y) ; z \<le> x ; z \<cdot> y ; z
 2. x ; z \<cdot> y ; z \<le> (x \<cdot> y) ; z
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x ; z \<cdot> y ; z \<le> (x \<cdot> y) ; z
[PROOF STEP]
using assms conv_iso inj_p_fun p_fun_distl
[PROOF STATE]
proof (prove)
using this:
is_inj z
(?x \<le> ?y) = (?x\<^sup>T \<le> ?y\<^sup>T)
is_inj ?x = is_p_fun (?x\<^sup>T)
is_p_fun ?x \<Longrightarrow> ?x ; (?y \<cdot> ?z) = ?x ; ?y \<cdot> ?x ; ?z

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


[STATEMENT]
lemma test_converse:
  "x \<cdot> 1' = x\<^sup>T \<cdot> 1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<cdot> 1' = x\<^sup>T \<cdot> 1'
[PROOF STEP]
by (metis conv_e conv_times inf_le2 is_test_def test_eq_conv)


[STATEMENT]
lemma injective_down_closed:
  assumes "is_inj x"
      and "y \<le> x"
    shows "is_inj y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_inj y
[PROOF STEP]
by (meson assms conv_iso dual_order.trans is_inj_def mult_isol_var)


[STATEMENT]
lemma injective_sup:
  assumes "is_inj t"
      and "e;t\<^sup>T \<le> 1'"
      and "is_inj e"
    shows "is_inj (t + e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_inj (t + e)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_inj (t + e)
[PROOF STEP]
have 1: "t;e\<^sup>T \<le> 1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t ; e\<^sup>T \<le> 1'
[PROOF STEP]
using assms(2) conv_contrav conv_e conv_invol conv_iso
[PROOF STATE]
proof (prove)
using this:
e ; t\<^sup>T \<le> 1'
(?x ; ?y)\<^sup>T = ?y\<^sup>T ; ?x\<^sup>T
1'\<^sup>T = 1'
(?x\<^sup>T)\<^sup>T = ?x
(?x \<le> ?y) = (?x\<^sup>T \<le> ?y\<^sup>T)

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

goal (1 subgoal):
 1. is_inj (t + e)
[PROOF STEP]
have "(t + e);(t + e)\<^sup>T = t;t\<^sup>T + t;e\<^sup>T + e;t\<^sup>T + e;e\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t + e) ; (t + e)\<^sup>T = t ; t\<^sup>T + t ; e\<^sup>T + e ; t\<^sup>T + e ; e\<^sup>T
[PROOF STEP]
by (metis conv_add distrib_left distrib_right' sup_assoc)
[PROOF STATE]
proof (state)
this:
(t + e) ; (t + e)\<^sup>T = t ; t\<^sup>T + t ; e\<^sup>T + e ; t\<^sup>T + e ; e\<^sup>T

goal (1 subgoal):
 1. is_inj (t + e)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(t + e) ; (t + e)\<^sup>T = t ; t\<^sup>T + t ; e\<^sup>T + e ; t\<^sup>T + e ; e\<^sup>T

goal (1 subgoal):
 1. is_inj (t + e)
[PROOF STEP]
have "... \<le> 1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t ; t\<^sup>T + t ; e\<^sup>T + e ; t\<^sup>T + e ; e\<^sup>T \<le> 1'
[PROOF STEP]
using 1 assms
[PROOF STATE]
proof (prove)
using this:
t ; e\<^sup>T \<le> 1'
is_inj t
e ; t\<^sup>T \<le> 1'
is_inj e

goal (1 subgoal):
 1. t ; t\<^sup>T + t ; e\<^sup>T + e ; t\<^sup>T + e ; e\<^sup>T \<le> 1'
[PROOF STEP]
by (simp add: is_inj_def le_supI)
[PROOF STATE]
proof (state)
this:
t ; t\<^sup>T + t ; e\<^sup>T + e ; t\<^sup>T + e ; e\<^sup>T \<le> 1'

goal (1 subgoal):
 1. is_inj (t + e)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(t + e) ; (t + e)\<^sup>T \<le> 1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(t + e) ; (t + e)\<^sup>T \<le> 1'

goal (1 subgoal):
 1. is_inj (t + e)
[PROOF STEP]
unfolding is_inj_def
[PROOF STATE]
proof (prove)
using this:
(t + e) ; (t + e)\<^sup>T \<le> 1'

goal (1 subgoal):
 1. (t + e) ; (t + e)\<^sup>T \<le> 1'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
is_inj (t + e)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vector_meet_comp:
  assumes "is_vector v"
      and "is_vector w"
    shows "v;w\<^sup>T = v\<cdot>w\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v ; w\<^sup>T = v \<cdot> w\<^sup>T
[PROOF STEP]
by (metis assms conv_contrav conv_one inf_top_right is_vector_def vector_1)


[STATEMENT]
lemma vector_meet_comp':
  assumes "is_vector v"
    shows "v;v\<^sup>T = v\<cdot>v\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v ; v\<^sup>T = v \<cdot> v\<^sup>T
[PROOF STEP]
using assms vector_meet_comp
[PROOF STATE]
proof (prove)
using this:
is_vector v
\<lbrakk>is_vector ?v; is_vector ?w\<rbrakk> \<Longrightarrow> ?v ; ?w\<^sup>T = ?v \<cdot> ?w\<^sup>T

goal (1 subgoal):
 1. v ; v\<^sup>T = v \<cdot> v\<^sup>T
[PROOF STEP]
by blast


[STATEMENT]
lemma vector_meet_comp_x:
  "x;1;x\<^sup>T = x;1\<cdot>1;x\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x ; 1 ; x\<^sup>T = x ; 1 \<cdot> 1 ; x\<^sup>T
[PROOF STEP]
by (metis comp_assoc inf_top.right_neutral is_vector_def one_idem_mult vector_1)


[STATEMENT]
lemma vector_meet_comp_x':
  "x;1;x = x;1\<cdot>1;x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x ; 1 ; x = x ; 1 \<cdot> 1 ; x
[PROOF STEP]
by (metis inf_commute inf_top.right_neutral ra_1)


[STATEMENT]
lemma vector_prop1:
  assumes "is_vector v"
    shows "-v\<^sup>T;v = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - v\<^sup>T ; v = 0
[PROOF STEP]
by (metis assms compl_inf_bot inf_top.right_neutral one_compl one_idem_mult vector_2)


[STATEMENT]
lemma ee:
  assumes "is_vector v"
      and "e \<le> v;-v\<^sup>T"
    shows "e;e = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e ; e = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. e ; e = 0
[PROOF STEP]
have "e;v \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e ; v \<le> 0
[PROOF STEP]
by (metis assms annir mult_isor vector_prop1 comp_assoc)
[PROOF STATE]
proof (state)
this:
e ; v \<le> 0

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

goal (1 subgoal):
 1. e ; e = 0
[PROOF STEP]
by (metis assms(2) annil order.antisym bot_least comp_assoc mult_isol)
[PROOF STATE]
proof (state)
this:
e ; e = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma et:
  assumes "is_vector v"
      and "e \<le> v;-v\<^sup>T"
      and "t \<le> v;v\<^sup>T"
    shows "e;t = 0"
      and "e;t\<^sup>T = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e ; t = 0 &&& e ; t\<^sup>T = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. e ; t = 0
 2. e ; t\<^sup>T = 0
[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]
by (metis assms(2-3) mult_isol_var comp_assoc)
[PROOF STATE]
proof (state)
this:
e ; t \<le> v ; - v\<^sup>T ; v ; v\<^sup>T

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

goal (1 subgoal):
 1. e ; t = 0
[PROOF STEP]
by (simp add: assms(1) comp_assoc le_bot vector_prop1)
[PROOF STATE]
proof (state)
this:
e ; t = 0

goal (1 subgoal):
 1. e ; t\<^sup>T = 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. e ; t\<^sup>T = 0
[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_iso
[PROOF STATE]
proof (prove)
using this:
t \<le> v ; v\<^sup>T
(?x \<le> ?y) = (?x\<^sup>T \<le> ?y\<^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 = 0
[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) mult_isol_var comp_assoc)
[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 = 0
[PROOF STEP]
thus "e;t\<^sup>T = 0"
[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 = 0
[PROOF STEP]
by (simp add: assms(1) comp_assoc le_bot vector_prop1)
[PROOF STATE]
proof (state)
this:
e ; t\<^sup>T = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma point_swap:
  assumes "point p"
      and "point q"
    shows "p \<le> x;q \<longleftrightarrow> q \<le> x\<^sup>T;p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<le> x ; q) = (q \<le> x\<^sup>T ; p)
[PROOF STEP]
by (metis assms conv_invol inj_sur_semi_swap point_def)


[STATEMENT]
lemma singleton_injective:
  assumes "singleton x"
    shows "is_inj x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_inj x
[PROOF STEP]
using assms injective_down_closed maddux_20
[PROOF STATE]
proof (prove)
using this:
singleton x
\<lbrakk>is_inj ?x; ?y \<le> ?x\<rbrakk> \<Longrightarrow> is_inj ?y
?x \<le> ?x ; 1

goal (1 subgoal):
 1. is_inj x
[PROOF STEP]
by blast


[STATEMENT]
lemma injective_inv:
  assumes "is_vector v"
      and "singleton e"
      and "e \<le> v;-v\<^sup>T"
      and "t \<le> v;v\<^sup>T"
      and "is_inj t"
    shows "is_inj (t + e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_inj (t + e)
[PROOF STEP]
by (metis assms singleton_injective injective_sup bot_least et(2))


[STATEMENT]
lemma singleton_is_point:
  assumes "singleton p"
    shows "point (p;1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. point (p ; 1)
[PROOF STEP]
by (simp add: assms comp_assoc is_vector_def point_def)


[STATEMENT]
lemma singleton_transp:
  assumes "singleton p"
    shows "singleton (p\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. singleton (p\<^sup>T)
[PROOF STEP]
by (simp add: assms)


[STATEMENT]
lemma point_to_singleton:
  assumes "singleton p"
    shows "singleton (1'\<cdot>p;p\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. singleton (1' \<cdot> p ; p\<^sup>T)
[PROOF STEP]
using assms dom_def_aux_var dom_one is_vector_def point_def
[PROOF STATE]
proof (prove)
using this:
singleton p
d ?x = 1' \<cdot> ?x ; ?x\<^sup>T
?x ; 1 = d ?x ; 1
is_vector ?x \<equiv> ?x = ?x ; 1
point ?x \<equiv> is_vector ?x \<and> bijective ?x

goal (1 subgoal):
 1. singleton (1' \<cdot> p ; p\<^sup>T)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma singleton_singletonT:
  assumes "singleton p"
    shows "p;p\<^sup>T \<le> 1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p ; p\<^sup>T \<le> 1'
[PROOF STEP]
using assms singleton_injective is_inj_def
[PROOF STATE]
proof (prove)
using this:
singleton p
singleton ?x \<Longrightarrow> is_inj ?x
is_inj ?x \<equiv> ?x ; ?x\<^sup>T \<le> 1'

goal (1 subgoal):
 1. p ; p\<^sup>T \<le> 1'
[PROOF STEP]
by blast


[STATEMENT]
lemma regressively_finite_minimum:
  "regressively_finite R \<Longrightarrow> is_vector v \<Longrightarrow> v \<noteq> 0 \<Longrightarrow> minimum R v \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>regressively_finite R; is_vector v; v \<noteq> 0\<rbrakk> \<Longrightarrow> minimum R v \<noteq> 0
[PROOF STEP]
using galois_aux2
[PROOF STATE]
proof (prove)
using this:
(?x \<cdot> - ?y = 0) = (?x \<le> ?y)

goal (1 subgoal):
 1. \<lbrakk>regressively_finite R; is_vector v; v \<noteq> 0\<rbrakk> \<Longrightarrow> minimum R v \<noteq> 0
[PROOF STEP]
by blast


[STATEMENT]
lemma regressively_finite_irreflexive:
  assumes "regressively_finite x"
    shows "x \<le> -1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> - 1'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<le> - 1'
[PROOF STEP]
have 1: "is_vector ((x\<^sup>T \<cdot> 1');1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_vector ((x\<^sup>T \<cdot> 1') ; 1)
[PROOF STEP]
by (simp add: is_vector_def mult_assoc)
[PROOF STATE]
proof (state)
this:
is_vector ((x\<^sup>T \<cdot> 1') ; 1)

goal (1 subgoal):
 1. x \<le> - 1'
[PROOF STEP]
have "(x\<^sup>T \<cdot> 1');1 = (x\<^sup>T \<cdot> 1');(x\<^sup>T \<cdot> 1');1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x\<^sup>T \<cdot> 1') ; 1 = (x\<^sup>T \<cdot> 1') ; (x\<^sup>T \<cdot> 1') ; 1
[PROOF STEP]
by (simp add: is_test_def test_comp_eq_mult)
[PROOF STATE]
proof (state)
this:
(x\<^sup>T \<cdot> 1') ; 1 = (x\<^sup>T \<cdot> 1') ; (x\<^sup>T \<cdot> 1') ; 1

goal (1 subgoal):
 1. x \<le> - 1'
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
is_vector ((x\<^sup>T \<cdot> 1') ; 1)
(x\<^sup>T \<cdot> 1') ; 1 = (x\<^sup>T \<cdot> 1') ; (x\<^sup>T \<cdot> 1') ; 1
[PROOF STEP]
have "(x\<^sup>T \<cdot> 1');1 = 0"
[PROOF STATE]
proof (prove)
using this:
is_vector ((x\<^sup>T \<cdot> 1') ; 1)
(x\<^sup>T \<cdot> 1') ; 1 = (x\<^sup>T \<cdot> 1') ; (x\<^sup>T \<cdot> 1') ; 1

goal (1 subgoal):
 1. (x\<^sup>T \<cdot> 1') ; 1 = 0
[PROOF STEP]
by (metis assms comp_assoc mult_subdistr)
[PROOF STATE]
proof (state)
this:
(x\<^sup>T \<cdot> 1') ; 1 = 0

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

goal (1 subgoal):
 1. x \<le> - 1'
[PROOF STEP]
by (metis conv_e conv_invol conv_times conv_zero galois_aux ss_p18)
[PROOF STATE]
proof (state)
this:
x \<le> - 1'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma point_equations:
  assumes "is_point p"
  shows "p;1=p"
    and "1;p=1"
    and "p\<^sup>T;1=1"
    and "1;p\<^sup>T=p\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p ; 1 = p &&& 1 ; p = 1) &&& p\<^sup>T ; 1 = 1 &&& 1 ; p\<^sup>T = p\<^sup>T
[PROOF STEP]
apply (metis assms is_point_def is_vector_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. 1 ; p = 1
 2. p\<^sup>T ; 1 = 1
 3. 1 ; p\<^sup>T = p\<^sup>T
[PROOF STEP]
using assms is_point_def is_vector_def tarski vector_comp
[PROOF STATE]
proof (prove)
using this:
is_point p
is_point ?x \<equiv> is_vector ?x \<and> is_inj ?x \<and> ?x \<noteq> 0
is_vector ?x \<equiv> ?x = ?x ; 1
(?x \<noteq> 0) = (1 ; ?x ; 1 = 1)
\<lbrakk>is_vector ?x; is_vector ?y\<rbrakk> \<Longrightarrow> is_vector (?x ; ?y)

goal (3 subgoals):
 1. 1 ; p = 1
 2. p\<^sup>T ; 1 = 1
 3. 1 ; p\<^sup>T = p\<^sup>T
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. p\<^sup>T ; 1 = 1
 2. 1 ; p\<^sup>T = p\<^sup>T
[PROOF STEP]
apply (metis assms conv_contrav conv_one conv_zero is_point_def is_vector_def tarski)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 ; p\<^sup>T = p\<^sup>T
[PROOF STEP]
by (metis assms conv_contrav conv_one is_point_def is_vector_def)


[STATEMENT]
lemma point_singleton:
  assumes "is_point p"
      and "is_vector v"
      and "v \<noteq> 0"
      and "v \<le> p"
    shows "v = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v = p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v = p
[PROOF STEP]
have "1;v = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 ; v = 1
[PROOF STEP]
using assms(2,3) comp_assoc is_vector_def tarski
[PROOF STATE]
proof (prove)
using this:
is_vector v
v \<noteq> 0
?x ; ?y ; ?z = ?x ; (?y ; ?z)
is_vector ?x \<equiv> ?x = ?x ; 1
(?x \<noteq> 0) = (1 ; ?x ; 1 = 1)

goal (1 subgoal):
 1. 1 ; v = 1
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
1 ; v = 1

goal (1 subgoal):
 1. v = p
[PROOF STEP]
hence "p = 1;v \<cdot> p"
[PROOF STATE]
proof (prove)
using this:
1 ; v = 1

goal (1 subgoal):
 1. p = 1 ; v \<cdot> p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p = 1 ; v \<cdot> p

goal (1 subgoal):
 1. v = p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
p = 1 ; v \<cdot> p

goal (1 subgoal):
 1. v = p
[PROOF STEP]
have "... \<le> (1 \<cdot> p;v\<^sup>T);(v \<cdot> 1\<^sup>T;p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 ; v \<cdot> p \<le> (1 \<cdot> p ; v\<^sup>T) ; (v \<cdot> 1\<^sup>T ; p)
[PROOF STEP]
using dedekind
[PROOF STATE]
proof (prove)
using this:
?x ; ?y \<cdot> ?z \<le> (?x \<cdot> ?z ; ?y\<^sup>T) ; (?y \<cdot> ?x\<^sup>T ; ?z)

goal (1 subgoal):
 1. 1 ; v \<cdot> p \<le> (1 \<cdot> p ; v\<^sup>T) ; (v \<cdot> 1\<^sup>T ; p)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
1 ; v \<cdot> p \<le> (1 \<cdot> p ; v\<^sup>T) ; (v \<cdot> 1\<^sup>T ; p)

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

goal (1 subgoal):
 1. v = p
[PROOF STEP]
have "... \<le> p;v\<^sup>T;v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 \<cdot> p ; v\<^sup>T) ; (v \<cdot> 1\<^sup>T ; p) \<le> p ; v\<^sup>T ; v
[PROOF STEP]
by (simp add: mult_subdistl)
[PROOF STATE]
proof (state)
this:
(1 \<cdot> p ; v\<^sup>T) ; (v \<cdot> 1\<^sup>T ; p) \<le> p ; v\<^sup>T ; v

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

goal (1 subgoal):
 1. v = p
[PROOF STEP]
have "... \<le> p;p\<^sup>T;v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p ; v\<^sup>T ; v \<le> p ; p\<^sup>T ; v
[PROOF STEP]
using assms(4) conv_iso mult_double_iso
[PROOF STATE]
proof (prove)
using this:
v \<le> p
(?x \<le> ?y) = (?x\<^sup>T \<le> ?y\<^sup>T)
?x \<le> ?y \<Longrightarrow> ?w ; ?x ; ?z \<le> ?w ; ?y ; ?z

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

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

goal (1 subgoal):
 1. v = p
[PROOF STEP]
have "... \<le> v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p ; p\<^sup>T ; v \<le> v
[PROOF STEP]
by (metis assms(1) is_inj_def is_point_def mult_isor mult_onel)
[PROOF STATE]
proof (state)
this:
p ; p\<^sup>T ; v \<le> v

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

goal (1 subgoal):
 1. v = p
[PROOF STEP]
using assms(4)
[PROOF STATE]
proof (prove)
using this:
p \<le> v
v \<le> p

goal (1 subgoal):
 1. v = p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v = p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma point_not_equal_aux:
  assumes "is_point p"
      and "is_point q"
    shows "p\<noteq>q \<longleftrightarrow> p \<cdot> -q \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<noteq> q) = (p \<cdot> - q \<noteq> 0)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p \<noteq> q \<Longrightarrow> p \<cdot> - q \<noteq> 0
 2. p \<cdot> - q \<noteq> 0 \<Longrightarrow> p \<noteq> q
[PROOF STEP]
show "p \<noteq> q \<Longrightarrow> p \<cdot> - q \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<noteq> q \<Longrightarrow> p \<cdot> - q \<noteq> 0
[PROOF STEP]
proof (rule contrapos_nn)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p \<noteq> q \<Longrightarrow> \<not> ?Q
 2. \<lbrakk>p \<noteq> q; p \<cdot> - q = 0\<rbrakk> \<Longrightarrow> ?Q
[PROOF STEP]
assume "p \<cdot> -q = 0"
[PROOF STATE]
proof (state)
this:
p \<cdot> - q = 0

goal (2 subgoals):
 1. p \<noteq> q \<Longrightarrow> \<not> ?Q
 2. \<lbrakk>p \<noteq> q; p \<cdot> - q = 0\<rbrakk> \<Longrightarrow> ?Q
[PROOF STEP]
thus "p = q"
[PROOF STATE]
proof (prove)
using this:
p \<cdot> - q = 0

goal (1 subgoal):
 1. p = q
[PROOF STEP]
using assms galois_aux2 is_point_def point_singleton
[PROOF STATE]
proof (prove)
using this:
p \<cdot> - q = 0
is_point p
is_point q
(?x \<cdot> - ?y = 0) = (?x \<le> ?y)
is_point ?x \<equiv> is_vector ?x \<and> is_inj ?x \<and> ?x \<noteq> 0
\<lbrakk>is_point ?p; is_vector ?v; ?v \<noteq> 0; ?v \<le> ?p\<rbrakk> \<Longrightarrow> ?v = ?p

goal (1 subgoal):
 1. p = q
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
p = q

goal (1 subgoal):
 1. p \<noteq> q \<Longrightarrow> p \<noteq> q
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
p \<noteq> q \<Longrightarrow> p \<cdot> - q \<noteq> 0

goal (1 subgoal):
 1. p \<cdot> - q \<noteq> 0 \<Longrightarrow> p \<noteq> q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<cdot> - q \<noteq> 0 \<Longrightarrow> p \<noteq> q
[PROOF STEP]
show "p \<cdot> - q \<noteq> 0 \<Longrightarrow> p \<noteq> q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<cdot> - q \<noteq> 0 \<Longrightarrow> p \<noteq> q
[PROOF STEP]
using inf_compl_bot
[PROOF STATE]
proof (prove)
using this:
?x \<cdot> - ?x = 0

goal (1 subgoal):
 1. p \<cdot> - q \<noteq> 0 \<Longrightarrow> p \<noteq> q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<cdot> - q \<noteq> 0 \<Longrightarrow> p \<noteq> q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma point_not_equal:
  assumes "is_point p"
      and "is_point q"
    shows "p\<noteq>q \<longleftrightarrow> p\<le>-q"
      and "p\<le>-q \<longleftrightarrow> p;q\<^sup>T \<le> -1'"
      and "p;q\<^sup>T \<le> -1' \<longleftrightarrow> p\<^sup>T;q \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<noteq> q) = (p \<le> - q) &&& (p \<le> - q) = (p ; q\<^sup>T \<le> - 1') &&& (p ; q\<^sup>T \<le> - 1') = (p\<^sup>T ; q \<le> 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. (p \<noteq> q) = (p \<le> - q)
 2. (p \<le> - q) = (p ; q\<^sup>T \<le> - 1')
 3. (p ; q\<^sup>T \<le> - 1') = (p\<^sup>T ; q \<le> 0)
[PROOF STEP]
have "p \<noteq> q \<Longrightarrow> p \<le> - q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<noteq> q \<Longrightarrow> p \<le> - q
[PROOF STEP]
by (metis assms point_not_equal_aux is_point_def vector_compl vector_mult point_singleton
              inf.orderI inf.cobounded1)
[PROOF STATE]
proof (state)
this:
p \<noteq> q \<Longrightarrow> p \<le> - q

goal (3 subgoals):
 1. (p \<noteq> q) = (p \<le> - q)
 2. (p \<le> - q) = (p ; q\<^sup>T \<le> - 1')
 3. (p ; q\<^sup>T \<le> - 1') = (p\<^sup>T ; q \<le> 0)
[PROOF STEP]
thus "p\<noteq>q \<longleftrightarrow> p\<le>-q"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> q \<Longrightarrow> p \<le> - q

goal (1 subgoal):
 1. (p \<noteq> q) = (p \<le> - q)
[PROOF STEP]
by (metis assms(1) galois_aux inf.orderE is_point_def order.refl)
[PROOF STATE]
proof (state)
this:
(p \<noteq> q) = (p \<le> - q)

goal (2 subgoals):
 1. (p \<le> - q) = (p ; q\<^sup>T \<le> - 1')
 2. (p ; q\<^sup>T \<le> - 1') = (p\<^sup>T ; q \<le> 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (p \<le> - q) = (p ; q\<^sup>T \<le> - 1')
 2. (p ; q\<^sup>T \<le> - 1') = (p\<^sup>T ; q \<le> 0)
[PROOF STEP]
show "(p \<le> - q) = (p ; q\<^sup>T \<le> - 1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<le> - q) = (p ; q\<^sup>T \<le> - 1')
[PROOF STEP]
by (simp add: conv_galois_2)
[PROOF STATE]
proof (state)
this:
(p \<le> - q) = (p ; q\<^sup>T \<le> - 1')

goal (1 subgoal):
 1. (p ; q\<^sup>T \<le> - 1') = (p\<^sup>T ; q \<le> 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (p ; q\<^sup>T \<le> - 1') = (p\<^sup>T ; q \<le> 0)
[PROOF STEP]
show "(p ; q\<^sup>T \<le> - 1') = (p\<^sup>T ; q \<le> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p ; q\<^sup>T \<le> - 1') = (p\<^sup>T ; q \<le> 0)
[PROOF STEP]
by (metis assms(2) compl_bot_eq conv_galois_2 galois_aux maddux_141 mult_1_right
              point_equations(4))
[PROOF STATE]
proof (state)
this:
(p ; q\<^sup>T \<le> - 1') = (p\<^sup>T ; q \<le> 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma point_is_point:
  "point x \<longleftrightarrow> is_point x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. point x = is_point x
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. point x \<Longrightarrow> is_point x
 2. is_point x \<Longrightarrow> point x
[PROOF STEP]
apply (simp add: is_point_def point_def surj_one tarski)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_point x \<Longrightarrow> point x
[PROOF STEP]
using is_point_def is_vector_def mult_assoc point_def sur_def_var1 tarski
[PROOF STATE]
proof (prove)
using this:
is_point ?x \<equiv> is_vector ?x \<and> is_inj ?x \<and> ?x \<noteq> 0
is_vector ?x \<equiv> ?x = ?x ; 1
?a ; ?b ; ?c = ?a ; (?b ; ?c)
point ?x \<equiv> is_vector ?x \<and> bijective ?x
is_sur ?x = (1 ; ?x = 1)
(?x \<noteq> 0) = (1 ; ?x ; 1 = 1)

goal (1 subgoal):
 1. is_point x \<Longrightarrow> point x
[PROOF STEP]
by fastforce


[STATEMENT]
lemma point_in_vector_or_complement:
  assumes "point p"
      and "is_vector v"
    shows "p \<le> v \<or> p \<le> -v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<le> v \<or> p \<le> - v
[PROOF STEP]
proof (cases "p \<le> -v")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p \<le> - v \<Longrightarrow> p \<le> v \<or> p \<le> - v
 2. \<not> p \<le> - v \<Longrightarrow> p \<le> v \<or> p \<le> - v
[PROOF STEP]
assume "p \<le> -v"
[PROOF STATE]
proof (state)
this:
p \<le> - v

goal (2 subgoals):
 1. p \<le> - v \<Longrightarrow> p \<le> v \<or> p \<le> - v
 2. \<not> p \<le> - v \<Longrightarrow> p \<le> v \<or> p \<le> - v
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<le> - v

goal (1 subgoal):
 1. p \<le> v \<or> p \<le> - v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p \<le> v \<or> p \<le> - v

goal (1 subgoal):
 1. \<not> p \<le> - v \<Longrightarrow> p \<le> v \<or> p \<le> - v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> p \<le> - v \<Longrightarrow> p \<le> v \<or> p \<le> - v
[PROOF STEP]
assume "\<not>(p \<le> -v)"
[PROOF STATE]
proof (state)
this:
\<not> p \<le> - v

goal (1 subgoal):
 1. \<not> p \<le> - v \<Longrightarrow> p \<le> v \<or> p \<le> - v
[PROOF STEP]
hence "p\<cdot>v \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<not> p \<le> - v

goal (1 subgoal):
 1. p \<cdot> v \<noteq> 0
[PROOF STEP]
by (simp add: galois_aux)
[PROOF STATE]
proof (state)
this:
p \<cdot> v \<noteq> 0

goal (1 subgoal):
 1. \<not> p \<le> - v \<Longrightarrow> p \<le> v \<or> p \<le> - v
[PROOF STEP]
hence "1;(p\<cdot>v) = 1"
[PROOF STATE]
proof (prove)
using this:
p \<cdot> v \<noteq> 0

goal (1 subgoal):
 1. 1 ; (p \<cdot> v) = 1
[PROOF STEP]
using assms comp_assoc is_vector_def point_def tarski vector_mult
[PROOF STATE]
proof (prove)
using this:
p \<cdot> v \<noteq> 0
point p
is_vector v
?x ; ?y ; ?z = ?x ; (?y ; ?z)
is_vector ?x \<equiv> ?x = ?x ; 1
point ?x \<equiv> is_vector ?x \<and> bijective ?x
(?x \<noteq> 0) = (1 ; ?x ; 1 = 1)
\<lbrakk>is_vector ?x; is_vector ?y\<rbrakk> \<Longrightarrow> is_vector (?x \<cdot> ?y)

goal (1 subgoal):
 1. 1 ; (p \<cdot> v) = 1
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
1 ; (p \<cdot> v) = 1

goal (1 subgoal):
 1. \<not> p \<le> - v \<Longrightarrow> p \<le> v \<or> p \<le> - v
[PROOF STEP]
hence "p \<le> p;(p\<cdot>v)\<^sup>T;(p\<cdot>v)"
[PROOF STATE]
proof (prove)
using this:
1 ; (p \<cdot> v) = 1

goal (1 subgoal):
 1. p \<le> p ; (p \<cdot> v)\<^sup>T ; (p \<cdot> v)
[PROOF STEP]
by (metis inf_top.left_neutral modular_2_var)
[PROOF STATE]
proof (state)
this:
p \<le> p ; (p \<cdot> v)\<^sup>T ; (p \<cdot> v)

goal (1 subgoal):
 1. \<not> p \<le> - v \<Longrightarrow> p \<le> v \<or> p \<le> - v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
p \<le> p ; (p \<cdot> v)\<^sup>T ; (p \<cdot> v)

goal (1 subgoal):
 1. \<not> p \<le> - v \<Longrightarrow> p \<le> v \<or> p \<le> - v
[PROOF STEP]
have "... \<le> p;p\<^sup>T;v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p ; (p \<cdot> v)\<^sup>T ; (p \<cdot> v) \<le> p ; p\<^sup>T ; v
[PROOF STEP]
by (simp add: mult_isol_var)
[PROOF STATE]
proof (state)
this:
p ; (p \<cdot> v)\<^sup>T ; (p \<cdot> v) \<le> p ; p\<^sup>T ; v

goal (1 subgoal):
 1. \<not> p \<le> - v \<Longrightarrow> p \<le> v \<or> p \<le> - v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
p ; (p \<cdot> v)\<^sup>T ; (p \<cdot> v) \<le> p ; p\<^sup>T ; v

goal (1 subgoal):
 1. \<not> p \<le> - v \<Longrightarrow> p \<le> v \<or> p \<le> - v
[PROOF STEP]
have "... \<le> v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p ; p\<^sup>T ; v \<le> v
[PROOF STEP]
using assms(1) comp_assoc point_def ss423conv
[PROOF STATE]
proof (prove)
using this:
point p
?x ; ?y ; ?z = ?x ; (?y ; ?z)
point ?x \<equiv> is_vector ?x \<and> bijective ?x
bijective ?x \<Longrightarrow> (?x ; ?y \<le> ?z) = (?y \<le> ?x\<^sup>T ; ?z)

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

goal (1 subgoal):
 1. \<not> p \<le> - v \<Longrightarrow> p \<le> v \<or> p \<le> - v
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
p \<le> v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<le> v

goal (1 subgoal):
 1. p \<le> v \<or> p \<le> - v
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
p \<le> v \<or> p \<le> - v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma point_in_vector_or_complement_iff:
  assumes "point p"
      and "is_vector v"
    shows "p \<le> v \<longleftrightarrow> \<not>(p \<le> -v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<le> v) = (\<not> p \<le> - v)
[PROOF STEP]
by (metis assms annir compl_top_eq galois_aux inf.orderE one_compl point_def ss423conv tarski
          top_greatest point_in_vector_or_complement)


[STATEMENT]
lemma different_points_consequences:
  assumes "point p"
      and "point q"
      and "p\<noteq>q"
    shows "p\<^sup>T;-q=1"
      and "-q\<^sup>T;p=1"
      and "-(p\<^sup>T;-q)=0"
      and "-(-q\<^sup>T;p)=0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p\<^sup>T ; - q = 1 &&& - q\<^sup>T ; p = 1) &&& - (p\<^sup>T ; - q) = 0 &&& - (- q\<^sup>T ; p) = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. p\<^sup>T ; - q = 1
 2. - q\<^sup>T ; p = 1
 3. - (p\<^sup>T ; - q) = 0
 4. - (- q\<^sup>T ; p) = 0
[PROOF STEP]
have "p \<le> -q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<le> - q
[PROOF STEP]
by (metis assms compl_le_swap1 inf.absorb1 inf.absorb2 point_def point_in_vector_or_complement)
[PROOF STATE]
proof (state)
this:
p \<le> - q

goal (4 subgoals):
 1. p\<^sup>T ; - q = 1
 2. - q\<^sup>T ; p = 1
 3. - (p\<^sup>T ; - q) = 0
 4. - (- q\<^sup>T ; p) = 0
[PROOF STEP]
thus 1: "p\<^sup>T;-q=1"
[PROOF STATE]
proof (prove)
using this:
p \<le> - q

goal (1 subgoal):
 1. p\<^sup>T ; - q = 1
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
p \<le> - q
point p

goal (1 subgoal):
 1. p\<^sup>T ; - q = 1
[PROOF STEP]
by (metis is_vector_def point_def ss423conv top_le)
[PROOF STATE]
proof (state)
this:
p\<^sup>T ; - q = 1

goal (3 subgoals):
 1. - q\<^sup>T ; p = 1
 2. - (p\<^sup>T ; - q) = 0
 3. - (- q\<^sup>T ; p) = 0
[PROOF STEP]
thus 2: "-q\<^sup>T;p=1"
[PROOF STATE]
proof (prove)
using this:
p\<^sup>T ; - q = 1

goal (1 subgoal):
 1. - q\<^sup>T ; p = 1
[PROOF STEP]
using conv_compl conv_one
[PROOF STATE]
proof (prove)
using this:
p\<^sup>T ; - q = 1
(- ?x)\<^sup>T = - ?x\<^sup>T
1\<^sup>T = 1

goal (1 subgoal):
 1. - q\<^sup>T ; p = 1
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
- q\<^sup>T ; p = 1

goal (2 subgoals):
 1. - (p\<^sup>T ; - q) = 0
 2. - (- q\<^sup>T ; p) = 0
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
p\<^sup>T ; - q = 1
[PROOF STEP]
show "-(p\<^sup>T;-q)=0"
[PROOF STATE]
proof (prove)
using this:
p\<^sup>T ; - q = 1

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

goal (1 subgoal):
 1. - (- q\<^sup>T ; p) = 0
[PROOF STEP]
from 2
[PROOF STATE]
proof (chain)
picking this:
- q\<^sup>T ; p = 1
[PROOF STEP]
show "-(-q\<^sup>T;p)=0"
[PROOF STATE]
proof (prove)
using this:
- q\<^sup>T ; p = 1

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma singleton_pq:
  assumes "point p"
      and "point q"
    shows "singleton (p;q\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. singleton (p ; q\<^sup>T)
[PROOF STEP]
using assms comp_assoc point_def point_equations(1,3) point_is_point
[PROOF STATE]
proof (prove)
using this:
point p
point q
?x ; ?y ; ?z = ?x ; (?y ; ?z)
point ?x \<equiv> is_vector ?x \<and> bijective ?x
is_point ?p \<Longrightarrow> ?p ; 1 = ?p
is_point ?p \<Longrightarrow> ?p\<^sup>T ; 1 = 1
point ?x = is_point ?x

goal (1 subgoal):
 1. singleton (p ; q\<^sup>T)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma singleton_equal_aux:
  assumes "singleton p"
      and "singleton q"
      and "q\<le>p"
    shows "p \<le> q;1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<le> q ; 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<le> q ; 1
[PROOF STEP]
have pLp: "p;1;p\<^sup>T \<le>1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p ; 1 ; p\<^sup>T \<le> 1'
[PROOF STEP]
by (simp add: assms(1) maddux_21 ss423conv)
[PROOF STATE]
proof (state)
this:
p ; 1 ; p\<^sup>T \<le> 1'

goal (1 subgoal):
 1. p \<le> q ; 1
[PROOF STEP]
have "p = 1;(q\<^sup>T;q;1) \<cdot> p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = 1 ; (q\<^sup>T ; q ; 1) \<cdot> p
[PROOF STEP]
using tarski
[PROOF STATE]
proof (prove)
using this:
(?x \<noteq> 0) = (1 ; ?x ; 1 = 1)

goal (1 subgoal):
 1. p = 1 ; (q\<^sup>T ; q ; 1) \<cdot> p
[PROOF STEP]
by (metis assms(2) annir singleton_injective inf.commute inf_top.right_neutral inj_triple
              mult_assoc surj_one)
[PROOF STATE]
proof (state)
this:
p = 1 ; (q\<^sup>T ; q ; 1) \<cdot> p

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

goal (1 subgoal):
 1. p \<le> q ; 1
[PROOF STEP]
have "... \<le> (1 \<cdot> p;(q\<^sup>T;q;1)\<^sup>T);(q\<^sup>T;q;1 \<cdot> 1;p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 ; (q\<^sup>T ; q ; 1) \<cdot> p \<le> (1 \<cdot> p ; (q\<^sup>T ; q ; 1)\<^sup>T) ; (q\<^sup>T ; q ; 1 \<cdot> 1 ; p)
[PROOF STEP]
using dedekind
[PROOF STATE]
proof (prove)
using this:
?x ; ?y \<cdot> ?z \<le> (?x \<cdot> ?z ; ?y\<^sup>T) ; (?y \<cdot> ?x\<^sup>T ; ?z)

goal (1 subgoal):
 1. 1 ; (q\<^sup>T ; q ; 1) \<cdot> p \<le> (1 \<cdot> p ; (q\<^sup>T ; q ; 1)\<^sup>T) ; (q\<^sup>T ; q ; 1 \<cdot> 1 ; p)
[PROOF STEP]
by (metis conv_one)
[PROOF STATE]
proof (state)
this:
1 ; (q\<^sup>T ; q ; 1) \<cdot> p \<le> (1 \<cdot> p ; (q\<^sup>T ; q ; 1)\<^sup>T) ; (q\<^sup>T ; q ; 1 \<cdot> 1 ; p)

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

goal (1 subgoal):
 1. p \<le> q ; 1
[PROOF STEP]
have "... \<le> p;1;q\<^sup>T;q;q\<^sup>T;q;1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 \<cdot> p ; (q\<^sup>T ; q ; 1)\<^sup>T) ; (q\<^sup>T ; q ; 1 \<cdot> 1 ; p) \<le> p ; 1 ; q\<^sup>T ; q ; q\<^sup>T ; q ; 1
[PROOF STEP]
by (simp add: comp_assoc mult_isol)
[PROOF STATE]
proof (state)
this:
(1 \<cdot> p ; (q\<^sup>T ; q ; 1)\<^sup>T) ; (q\<^sup>T ; q ; 1 \<cdot> 1 ; p) \<le> p ; 1 ; q\<^sup>T ; q ; q\<^sup>T ; q ; 1

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

goal (1 subgoal):
 1. p \<le> q ; 1
[PROOF STEP]
have "... \<le> p;1;p\<^sup>T;q;q\<^sup>T;q;1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p ; 1 ; q\<^sup>T ; q ; q\<^sup>T ; q ; 1 \<le> p ; 1 ; p\<^sup>T ; q ; q\<^sup>T ; q ; 1
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
q \<le> p

goal (1 subgoal):
 1. p ; 1 ; q\<^sup>T ; q ; q\<^sup>T ; q ; 1 \<le> p ; 1 ; p\<^sup>T ; q ; q\<^sup>T ; q ; 1
[PROOF STEP]
by (metis comp_assoc conv_iso mult_double_iso)
[PROOF STATE]
proof (state)
this:
p ; 1 ; q\<^sup>T ; q ; q\<^sup>T ; q ; 1 \<le> p ; 1 ; p\<^sup>T ; q ; q\<^sup>T ; q ; 1

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

goal (1 subgoal):
 1. p \<le> q ; 1
[PROOF STEP]
have "... \<le> 1';q;q\<^sup>T;q;1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p ; 1 ; p\<^sup>T ; q ; q\<^sup>T ; q ; 1 \<le> 1' ; q ; q\<^sup>T ; q ; 1
[PROOF STEP]
using pLp
[PROOF STATE]
proof (prove)
using this:
p ; 1 ; p\<^sup>T \<le> 1'

goal (1 subgoal):
 1. p ; 1 ; p\<^sup>T ; q ; q\<^sup>T ; q ; 1 \<le> 1' ; q ; q\<^sup>T ; q ; 1
[PROOF STEP]
using mult_isor
[PROOF STATE]
proof (prove)
using this:
p ; 1 ; p\<^sup>T \<le> 1'
?x \<le> ?y \<Longrightarrow> ?x ; ?z \<le> ?y ; ?z

goal (1 subgoal):
 1. p ; 1 ; p\<^sup>T ; q ; q\<^sup>T ; q ; 1 \<le> 1' ; q ; q\<^sup>T ; q ; 1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p ; 1 ; p\<^sup>T ; q ; q\<^sup>T ; q ; 1 \<le> 1' ; q ; q\<^sup>T ; q ; 1

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

goal (1 subgoal):
 1. p \<le> q ; 1
[PROOF STEP]
have "... \<le> q;1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1' ; q ; q\<^sup>T ; q ; 1 \<le> q ; 1
[PROOF STEP]
using assms(2) singleton_singletonT
[PROOF STATE]
proof (prove)
using this:
singleton q
singleton ?p \<Longrightarrow> ?p ; ?p\<^sup>T \<le> 1'

goal (1 subgoal):
 1. 1' ; q ; q\<^sup>T ; q ; 1 \<le> q ; 1
[PROOF STEP]
by (simp add: comp_assoc mult_isol)
[PROOF STATE]
proof (state)
this:
1' ; q ; q\<^sup>T ; q ; 1 \<le> q ; 1

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

goal (1 subgoal):
 1. p \<le> q ; 1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
p \<le> q ; 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma singleton_equal:
 assumes "singleton p"
     and "singleton q"
     and "q\<le>p"
   shows "q=p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q = p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. q = p
[PROOF STEP]
have p1: "p \<le> q;1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<le> q ; 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
singleton p
singleton q
q \<le> p

goal (1 subgoal):
 1. p \<le> q ; 1
[PROOF STEP]
by (rule singleton_equal_aux)
[PROOF STATE]
proof (state)
this:
p \<le> q ; 1

goal (1 subgoal):
 1. q = p
[PROOF STEP]
have "p\<^sup>T \<le> q\<^sup>T;1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p\<^sup>T \<le> q\<^sup>T ; 1
[PROOF STEP]
using assms singleton_equal_aux singleton_transp conv_iso
[PROOF STATE]
proof (prove)
using this:
singleton p
singleton q
q \<le> p
\<lbrakk>singleton ?p; singleton ?q; ?q \<le> ?p\<rbrakk> \<Longrightarrow> ?p \<le> ?q ; 1
singleton ?p \<Longrightarrow> singleton (?p\<^sup>T)
(?x \<le> ?y) = (?x\<^sup>T \<le> ?y\<^sup>T)

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

goal (1 subgoal):
 1. q = p
[PROOF STEP]
hence p2: "p \<le> 1;q"
[PROOF STATE]
proof (prove)
using this:
p\<^sup>T \<le> q\<^sup>T ; 1

goal (1 subgoal):
 1. p \<le> 1 ; q
[PROOF STEP]
using conv_iso
[PROOF STATE]
proof (prove)
using this:
p\<^sup>T \<le> q\<^sup>T ; 1
(?x \<le> ?y) = (?x\<^sup>T \<le> ?y\<^sup>T)

goal (1 subgoal):
 1. p \<le> 1 ; q
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
p \<le> 1 ; q

goal (1 subgoal):
 1. q = p
[PROOF STEP]
have "p \<le> q;1 \<cdot> 1;q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<le> q ; 1 \<cdot> 1 ; q
[PROOF STEP]
using p1 p2 inf.boundedI
[PROOF STATE]
proof (prove)
using this:
p \<le> q ; 1
p \<le> 1 ; q
\<lbrakk>?a \<le> ?b; ?a \<le> ?c\<rbrakk> \<Longrightarrow> ?a \<le> ?b \<cdot> ?c

goal (1 subgoal):
 1. p \<le> q ; 1 \<cdot> 1 ; q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<le> q ; 1 \<cdot> 1 ; q

goal (1 subgoal):
 1. q = p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
p \<le> q ; 1 \<cdot> 1 ; q

goal (1 subgoal):
 1. q = p
[PROOF STEP]
have "... \<le> (q \<cdot> 1;q;1);(1 \<cdot> q\<^sup>T;1;q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q ; 1 \<cdot> 1 ; q \<le> (q \<cdot> 1 ; q ; 1) ; (1 \<cdot> q\<^sup>T ; 1 ; q)
[PROOF STEP]
using dedekind
[PROOF STATE]
proof (prove)
using this:
?x ; ?y \<cdot> ?z \<le> (?x \<cdot> ?z ; ?y\<^sup>T) ; (?y \<cdot> ?x\<^sup>T ; ?z)

goal (1 subgoal):
 1. q ; 1 \<cdot> 1 ; q \<le> (q \<cdot> 1 ; q ; 1) ; (1 \<cdot> q\<^sup>T ; 1 ; q)
[PROOF STEP]
by (metis comp_assoc conv_one)
[PROOF STATE]
proof (state)
this:
q ; 1 \<cdot> 1 ; q \<le> (q \<cdot> 1 ; q ; 1) ; (1 \<cdot> q\<^sup>T ; 1 ; q)

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

goal (1 subgoal):
 1. q = p
[PROOF STEP]
have "... \<le> q;q\<^sup>T;1;q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (q \<cdot> 1 ; q ; 1) ; (1 \<cdot> q\<^sup>T ; 1 ; q) \<le> q ; q\<^sup>T ; 1 ; q
[PROOF STEP]
by (simp add: mult_isor comp_assoc)
[PROOF STATE]
proof (state)
this:
(q \<cdot> 1 ; q ; 1) ; (1 \<cdot> q\<^sup>T ; 1 ; q) \<le> q ; q\<^sup>T ; 1 ; q

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

goal (1 subgoal):
 1. q = p
[PROOF STEP]
have "... \<le> q;1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q ; q\<^sup>T ; 1 ; q \<le> q ; 1'
[PROOF STEP]
by (metis assms(2) conv_contrav conv_invol conv_one is_inj_def mult_assoc mult_isol
              one_idem_mult)
[PROOF STATE]
proof (state)
this:
q ; q\<^sup>T ; 1 ; q \<le> q ; 1'

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

goal (1 subgoal):
 1. q = p
[PROOF STEP]
have "... \<le> q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q ; 1' \<le> q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
q ; 1' \<le> q

goal (1 subgoal):
 1. q = p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
p \<le> q
[PROOF STEP]
have "p \<le> q"
[PROOF STATE]
proof (prove)
using this:
p \<le> q

goal (1 subgoal):
 1. p \<le> q
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
p \<le> q

goal (1 subgoal):
 1. q = p
[PROOF STEP]
thus "q=p"
[PROOF STATE]
proof (prove)
using this:
p \<le> q

goal (1 subgoal):
 1. q = p
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
p \<le> q
q \<le> p

goal (1 subgoal):
 1. q = p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
q = p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma singleton_nonsplit:
  assumes "singleton p"
      and "x\<le>p"
    shows "x=0 \<or> x=p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = 0 \<or> x = p
[PROOF STEP]
proof (cases "x=0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = 0 \<Longrightarrow> x = 0 \<or> x = p
 2. x \<noteq> 0 \<Longrightarrow> x = 0 \<or> x = p
[PROOF STEP]
assume "x=0"
[PROOF STATE]
proof (state)
this:
x = 0

goal (2 subgoals):
 1. x = 0 \<Longrightarrow> x = 0 \<or> x = p
 2. x \<noteq> 0 \<Longrightarrow> x = 0 \<or> x = p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x = 0

goal (1 subgoal):
 1. x = 0 \<or> x = p
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
x = 0 \<or> x = p

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> x = 0 \<or> x = p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> x = 0 \<or> x = p
[PROOF STEP]
assume 1: "x\<noteq>0"
[PROOF STATE]
proof (state)
this:
x \<noteq> 0

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> x = 0 \<or> x = p
[PROOF STEP]
have "singleton x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. singleton x
[PROOF STEP]
proof (safe)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. is_inj (x ; 1)
 2. is_sur (x ; 1)
 3. is_inj (x\<^sup>T ; 1)
 4. is_sur (x\<^sup>T ; 1)
[PROOF STEP]
show "is_inj (x;1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_inj (x ; 1)
[PROOF STEP]
using assms injective_down_closed mult_isor
[PROOF STATE]
proof (prove)
using this:
singleton p
x \<le> p
\<lbrakk>is_inj ?x; ?y \<le> ?x\<rbrakk> \<Longrightarrow> is_inj ?y
?x \<le> ?y \<Longrightarrow> ?x ; ?z \<le> ?y ; ?z

goal (1 subgoal):
 1. is_inj (x ; 1)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_inj (x ; 1)

goal (3 subgoals):
 1. is_sur (x ; 1)
 2. is_inj (x\<^sup>T ; 1)
 3. is_sur (x\<^sup>T ; 1)
[PROOF STEP]
show "is_inj (x\<^sup>T;1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_inj (x\<^sup>T ; 1)
[PROOF STEP]
using assms conv_iso injective_down_closed mult_isol_var
[PROOF STATE]
proof (prove)
using this:
singleton p
x \<le> p
(?x \<le> ?y) = (?x\<^sup>T \<le> ?y\<^sup>T)
\<lbrakk>is_inj ?x; ?y \<le> ?x\<rbrakk> \<Longrightarrow> is_inj ?y
\<lbrakk>?u \<le> ?x; ?v \<le> ?y\<rbrakk> \<Longrightarrow> ?u ; ?v \<le> ?x ; ?y

goal (1 subgoal):
 1. is_inj (x\<^sup>T ; 1)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_inj (x\<^sup>T ; 1)

goal (2 subgoals):
 1. is_sur (x ; 1)
 2. is_sur (x\<^sup>T ; 1)
[PROOF STEP]
show "is_sur (x;1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_sur (x ; 1)
[PROOF STEP]
using 1 comp_assoc sur_def_var1 tarski
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0
?x ; ?y ; ?z = ?x ; (?y ; ?z)
is_sur ?x = (1 ; ?x = 1)
(?x \<noteq> 0) = (1 ; ?x ; 1 = 1)

goal (1 subgoal):
 1. is_sur (x ; 1)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
is_sur (x ; 1)

goal (1 subgoal):
 1. is_sur (x\<^sup>T ; 1)
[PROOF STEP]
thus "is_sur (x\<^sup>T;1)"
[PROOF STATE]
proof (prove)
using this:
is_sur (x ; 1)

goal (1 subgoal):
 1. is_sur (x\<^sup>T ; 1)
[PROOF STEP]
by (metis conv_contrav conv_one mult.semigroup_axioms sur_def_var1 semigroup.assoc)
[PROOF STATE]
proof (state)
this:
is_sur (x\<^sup>T ; 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
singleton x

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> x = 0 \<or> x = p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
singleton x

goal (1 subgoal):
 1. x = 0 \<or> x = p
[PROOF STEP]
using assms singleton_equal
[PROOF STATE]
proof (prove)
using this:
singleton x
singleton p
x \<le> p
\<lbrakk>singleton ?p; singleton ?q; ?q \<le> ?p\<rbrakk> \<Longrightarrow> ?q = ?p

goal (1 subgoal):
 1. x = 0 \<or> x = p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x = 0 \<or> x = p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma singleton_nonzero:
  assumes "singleton p"
    shows "p\<noteq>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<noteq> 0
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p = 0 \<Longrightarrow> False
[PROOF STEP]
assume "p = 0"
[PROOF STATE]
proof (state)
this:
p = 0

goal (1 subgoal):
 1. p = 0 \<Longrightarrow> False
[PROOF STEP]
hence "point 0"
[PROOF STATE]
proof (prove)
using this:
p = 0

goal (1 subgoal):
 1. point 0
[PROOF STEP]
using assms singleton_is_point
[PROOF STATE]
proof (prove)
using this:
p = 0
singleton p
singleton ?p \<Longrightarrow> point (?p ; 1)

goal (1 subgoal):
 1. point 0
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
point 0

goal (1 subgoal):
 1. p = 0 \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
point 0

goal (1 subgoal):
 1. False
[PROOF STEP]
by (simp add: is_point_def point_is_point)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma singleton_sum:
  assumes "singleton p"
    shows "p \<le> x+y \<longleftrightarrow> (p\<le>x \<or> p\<le>y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<le> x + y) = (p \<le> x \<or> p \<le> y)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p \<le> x + y \<Longrightarrow> p \<le> x \<or> p \<le> y
 2. p \<le> x \<or> p \<le> y \<Longrightarrow> p \<le> x + y
[PROOF STEP]
show "p \<le> x + y \<Longrightarrow> p \<le> x \<or> p \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<le> x + y \<Longrightarrow> p \<le> x \<or> p \<le> y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<le> x + y \<Longrightarrow> p \<le> x \<or> p \<le> y
[PROOF STEP]
assume as: "p \<le> x + y"
[PROOF STATE]
proof (state)
this:
p \<le> x + y

goal (1 subgoal):
 1. p \<le> x + y \<Longrightarrow> p \<le> x \<or> p \<le> y
[PROOF STEP]
show "p \<le> x \<or> p \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<le> x \<or> p \<le> y
[PROOF STEP]
proof (cases "p\<le>x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p \<le> x \<Longrightarrow> p \<le> x \<or> p \<le> y
 2. \<not> p \<le> x \<Longrightarrow> p \<le> x \<or> p \<le> y
[PROOF STEP]
assume "p\<le>x"
[PROOF STATE]
proof (state)
this:
p \<le> x

goal (2 subgoals):
 1. p \<le> x \<Longrightarrow> p \<le> x \<or> p \<le> y
 2. \<not> p \<le> x \<Longrightarrow> p \<le> x \<or> p \<le> y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<le> x

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

goal (1 subgoal):
 1. \<not> p \<le> x \<Longrightarrow> p \<le> x \<or> p \<le> y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> p \<le> x \<Longrightarrow> p \<le> x \<or> p \<le> y
[PROOF STEP]
assume a:"\<not>(p\<le>x)"
[PROOF STATE]
proof (state)
this:
\<not> p \<le> x

goal (1 subgoal):
 1. \<not> p \<le> x \<Longrightarrow> p \<le> x \<or> p \<le> y
[PROOF STEP]
hence "p\<cdot>x \<noteq> p"
[PROOF STATE]
proof (prove)
using this:
\<not> p \<le> x

goal (1 subgoal):
 1. p \<cdot> x \<noteq> p
[PROOF STEP]
using a inf.orderI
[PROOF STATE]
proof (prove)
using this:
\<not> p \<le> x
\<not> p \<le> x
?a = ?a \<cdot> ?b \<Longrightarrow> ?a \<le> ?b

goal (1 subgoal):
 1. p \<cdot> x \<noteq> p
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
p \<cdot> x \<noteq> p

goal (1 subgoal):
 1. \<not> p \<le> x \<Longrightarrow> p \<le> x \<or> p \<le> y
[PROOF STEP]
hence "p \<le> -x"
[PROOF STATE]
proof (prove)
using this:
p \<cdot> x \<noteq> p

goal (1 subgoal):
 1. p \<le> - x
[PROOF STEP]
using assms singleton_nonsplit galois_aux inf_le1
[PROOF STATE]
proof (prove)
using this:
p \<cdot> x \<noteq> p
singleton p
\<lbrakk>singleton ?p; ?x \<le> ?p\<rbrakk> \<Longrightarrow> ?x = 0 \<or> ?x = ?p
(?x \<cdot> ?y = 0) = (?x \<le> - ?y)
?x \<cdot> ?y \<le> ?x

goal (1 subgoal):
 1. p \<le> - x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<le> - x

goal (1 subgoal):
 1. \<not> p \<le> x \<Longrightarrow> p \<le> x \<or> p \<le> y
[PROOF STEP]
hence "p\<le>y"
[PROOF STATE]
proof (prove)
using this:
p \<le> - x

goal (1 subgoal):
 1. p \<le> y
[PROOF STEP]
using as
[PROOF STATE]
proof (prove)
using this:
p \<le> - x
p \<le> x + y

goal (1 subgoal):
 1. p \<le> y
[PROOF STEP]
by (metis galois_1 inf.orderE)
[PROOF STATE]
proof (state)
this:
p \<le> y

goal (1 subgoal):
 1. \<not> p \<le> x \<Longrightarrow> p \<le> x \<or> p \<le> y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<le> y

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
p \<le> x \<or> p \<le> y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
p \<le> x + y \<Longrightarrow> p \<le> x \<or> p \<le> y

goal (1 subgoal):
 1. p \<le> x \<or> p \<le> y \<Longrightarrow> p \<le> x + y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<le> x \<or> p \<le> y \<Longrightarrow> p \<le> x + y
[PROOF STEP]
show "p \<le> x \<or> p \<le> y \<Longrightarrow> p \<le> x + y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<le> x \<or> p \<le> y \<Longrightarrow> p \<le> x + y
[PROOF STEP]
using sup.coboundedI1 sup.coboundedI2
[PROOF STATE]
proof (prove)
using this:
?c \<le> ?a \<Longrightarrow> ?c \<le> ?a + ?b
?c \<le> ?b \<Longrightarrow> ?c \<le> ?a + ?b

goal (1 subgoal):
 1. p \<le> x \<or> p \<le> y \<Longrightarrow> p \<le> x + y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<le> x \<or> p \<le> y \<Longrightarrow> p \<le> x + y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma singleton_iff:
 "singleton x \<longleftrightarrow> x \<noteq> 0 \<and> x\<^sup>T;1;x + x;1;x\<^sup>T \<le> 1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. singleton x = (x \<noteq> 0 \<and> x\<^sup>T ; 1 ; x + x ; 1 ; x\<^sup>T \<le> 1')
[PROOF STEP]
by (smt comp_assoc conv_contrav conv_invol conv_one is_inj_def le_sup_iff one_idem_mult
        sur_def_var1 tarski)


[STATEMENT]
lemma singleton_not_atom_in_relation_algebra_tarski:
 assumes "p\<noteq>0"
     and "\<forall>x . x\<le>p \<longrightarrow> x=0 \<or> x=p"
   shows "singleton p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. singleton p
[PROOF STEP]
nitpick [expect=genuine]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. singleton p
[PROOF STEP]
oops


[STATEMENT]
lemma point_exists:
  "\<exists>x . point x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. point x
[PROOF STEP]
by (metis (full_types) order.eq_iff is_inj_def is_sur_def is_vector_def point_axiom point_def)


[STATEMENT]
lemma point_below_vector:
  assumes "is_vector v"
      and "v \<noteq> 0"
    shows "\<exists>x . point x \<and> x \<le> v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. point x \<and> x \<le> v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. point x \<and> x \<le> v
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
v \<noteq> 0
[PROOF STEP]
obtain y and z where 1: "point y \<and> point z \<and> y;z\<^sup>T \<le> v"
[PROOF STATE]
proof (prove)
using this:
v \<noteq> 0

goal (1 subgoal):
 1. (\<And>y z. point y \<and> point z \<and> y ; z\<^sup>T \<le> v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using point_axiom
[PROOF STATE]
proof (prove)
using this:
v \<noteq> 0
?x \<noteq> 0 \<longrightarrow> (\<exists>y z. point y \<and> point z \<and> y ; z\<^sup>T \<le> ?x)

goal (1 subgoal):
 1. (\<And>y z. point y \<and> point z \<and> y ; z\<^sup>T \<le> v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
point y \<and> point z \<and> y ; z\<^sup>T \<le> v

goal (1 subgoal):
 1. \<exists>x. point x \<and> x \<le> v
[PROOF STEP]
have "z\<^sup>T;1 = (1;z)\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z\<^sup>T ; 1 = (1 ; z)\<^sup>T
[PROOF STEP]
using conv_contrav conv_one
[PROOF STATE]
proof (prove)
using this:
(?x ; ?y)\<^sup>T = ?y\<^sup>T ; ?x\<^sup>T
1\<^sup>T = 1

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

goal (1 subgoal):
 1. \<exists>x. point x \<and> x \<le> v
[PROOF STEP]
hence "y;(1;z)\<^sup>T \<le> v"
[PROOF STATE]
proof (prove)
using this:
z\<^sup>T ; 1 = (1 ; z)\<^sup>T

goal (1 subgoal):
 1. y ; (1 ; z)\<^sup>T \<le> v
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
z\<^sup>T ; 1 = (1 ; z)\<^sup>T
point y \<and> point z \<and> y ; z\<^sup>T \<le> v

goal (1 subgoal):
 1. y ; (1 ; z)\<^sup>T \<le> v
[PROOF STEP]
by (metis assms(1) comp_assoc is_vector_def mult_isor)
[PROOF STATE]
proof (state)
this:
y ; (1 ; z)\<^sup>T \<le> v

goal (1 subgoal):
 1. \<exists>x. point x \<and> x \<le> v
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
y ; (1 ; z)\<^sup>T \<le> v

goal (1 subgoal):
 1. \<exists>x. point x \<and> x \<le> v
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
y ; (1 ; z)\<^sup>T \<le> v
point y \<and> point z \<and> y ; z\<^sup>T \<le> v

goal (1 subgoal):
 1. \<exists>x. point x \<and> x \<le> v
[PROOF STEP]
by (metis conv_one is_vector_def point_def sur_def_var1)
[PROOF STATE]
proof (state)
this:
\<exists>x. point x \<and> x \<le> v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma atom_is_singleton:
  assumes "p\<noteq>0"
      and "\<forall>x . x\<le>p \<longrightarrow> x=0 \<or> x=p"
    shows "singleton p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. singleton p
[PROOF STEP]
by (metis assms singleton_nonzero singleton_pq point_axiom)


[STATEMENT]
lemma singleton_iff_atom:
  "singleton p \<longleftrightarrow> p\<noteq>0 \<and> (\<forall>x . x\<le>p \<longrightarrow> x=0 \<or> x=p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. singleton p = (p \<noteq> 0 \<and> (\<forall>x\<le>p. x = 0 \<or> x = p))
[PROOF STEP]
using singleton_nonsplit singleton_nonzero atom_is_singleton
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>singleton ?p; ?x \<le> ?p\<rbrakk> \<Longrightarrow> ?x = 0 \<or> ?x = ?p
singleton ?p \<Longrightarrow> ?p \<noteq> 0
\<lbrakk>?p \<noteq> 0; \<forall>x\<le>?p. x = 0 \<or> x = ?p\<rbrakk> \<Longrightarrow> singleton ?p

goal (1 subgoal):
 1. singleton p = (p \<noteq> 0 \<and> (\<forall>x\<le>p. x = 0 \<or> x = p))
[PROOF STEP]
by blast


[STATEMENT]
lemma maddux_tarski:
  assumes "x\<noteq>0"
  shows "\<exists>y . y\<noteq>0 \<and> y\<le>x \<and> is_p_fun y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y. y \<noteq> 0 \<and> y \<le> x \<and> is_p_fun y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>y. y \<noteq> 0 \<and> y \<le> x \<and> is_p_fun y
[PROOF STEP]
obtain p q where 1: "point p \<and> point q \<and> p;q\<^sup>T \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p q. point p \<and> point q \<and> p ; q\<^sup>T \<le> x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms point_axiom
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0
?x \<noteq> 0 \<longrightarrow> (\<exists>y z. point y \<and> point z \<and> y ; z\<^sup>T \<le> ?x)

goal (1 subgoal):
 1. (\<And>p q. point p \<and> point q \<and> p ; q\<^sup>T \<le> x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
point p \<and> point q \<and> p ; q\<^sup>T \<le> x

goal (1 subgoal):
 1. \<exists>y. y \<noteq> 0 \<and> y \<le> x \<and> is_p_fun y
[PROOF STEP]
hence 2: "p;q\<^sup>T\<noteq>0"
[PROOF STATE]
proof (prove)
using this:
point p \<and> point q \<and> p ; q\<^sup>T \<le> x

goal (1 subgoal):
 1. p ; q\<^sup>T \<noteq> 0
[PROOF STEP]
by (simp add: singleton_nonzero singleton_pq)
[PROOF STATE]
proof (state)
this:
p ; q\<^sup>T \<noteq> 0

goal (1 subgoal):
 1. \<exists>y. y \<noteq> 0 \<and> y \<le> x \<and> is_p_fun y
[PROOF STEP]
have "is_p_fun (p;q\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_p_fun (p ; q\<^sup>T)
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
point p \<and> point q \<and> p ; q\<^sup>T \<le> x

goal (1 subgoal):
 1. is_p_fun (p ; q\<^sup>T)
[PROOF STEP]
by (meson singleton_singletonT singleton_pq singleton_transp is_inj_def p_fun_inj)
[PROOF STATE]
proof (state)
this:
is_p_fun (p ; q\<^sup>T)

goal (1 subgoal):
 1. \<exists>y. y \<noteq> 0 \<and> y \<le> x \<and> is_p_fun y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
is_p_fun (p ; q\<^sup>T)

goal (1 subgoal):
 1. \<exists>y. y \<noteq> 0 \<and> y \<le> x \<and> is_p_fun y
[PROOF STEP]
using 1 2
[PROOF STATE]
proof (prove)
using this:
is_p_fun (p ; q\<^sup>T)
point p \<and> point q \<and> p ; q\<^sup>T \<le> x
p ; q\<^sup>T \<noteq> 0

goal (1 subgoal):
 1. \<exists>y. y \<noteq> 0 \<and> y \<le> x \<and> is_p_fun y
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>y. y \<noteq> 0 \<and> y \<le> x \<and> is_p_fun y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma intermediate_point_theorem:
  assumes "point p"
      and "point r"
    shows "p \<le> x;y;r \<longleftrightarrow> (\<exists>q . point q \<and> p \<le> x;q \<and> q \<le> y;r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<le> x ; y ; r) = (\<exists>q. point q \<and> p \<le> x ; q \<and> q \<le> y ; r)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p \<le> x ; y ; r \<Longrightarrow> \<exists>q. point q \<and> p \<le> x ; q \<and> q \<le> y ; r
 2. \<exists>q. point q \<and> p \<le> x ; q \<and> q \<le> y ; r \<Longrightarrow> p \<le> x ; y ; r
[PROOF STEP]
assume 1: "p \<le> x;y;r"
[PROOF STATE]
proof (state)
this:
p \<le> x ; y ; r

goal (2 subgoals):
 1. p \<le> x ; y ; r \<Longrightarrow> \<exists>q. point q \<and> p \<le> x ; q \<and> q \<le> y ; r
 2. \<exists>q. point q \<and> p \<le> x ; q \<and> q \<le> y ; r \<Longrightarrow> p \<le> x ; y ; r
[PROOF STEP]
let ?v = "x\<^sup>T;p \<cdot> y;r"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p \<le> x ; y ; r \<Longrightarrow> \<exists>q. point q \<and> p \<le> x ; q \<and> q \<le> y ; r
 2. \<exists>q. point q \<and> p \<le> x ; q \<and> q \<le> y ; r \<Longrightarrow> p \<le> x ; y ; r
[PROOF STEP]
have 2: "is_vector ?v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_vector (x\<^sup>T ; p \<cdot> y ; r)
[PROOF STEP]
using assms comp_assoc is_vector_def point_def vector_mult
[PROOF STATE]
proof (prove)
using this:
point p
point r
?x ; ?y ; ?z = ?x ; (?y ; ?z)
is_vector ?x \<equiv> ?x = ?x ; 1
point ?x \<equiv> is_vector ?x \<and> bijective ?x
\<lbrakk>is_vector ?x; is_vector ?y\<rbrakk> \<Longrightarrow> is_vector (?x \<cdot> ?y)

goal (1 subgoal):
 1. is_vector (x\<^sup>T ; p \<cdot> y ; r)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
is_vector (x\<^sup>T ; p \<cdot> y ; r)

goal (2 subgoals):
 1. p \<le> x ; y ; r \<Longrightarrow> \<exists>q. point q \<and> p \<le> x ; q \<and> q \<le> y ; r
 2. \<exists>q. point q \<and> p \<le> x ; q \<and> q \<le> y ; r \<Longrightarrow> p \<le> x ; y ; r
[PROOF STEP]
have "?v \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>T ; p \<cdot> y ; r \<noteq> 0
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
p \<le> x ; y ; r

goal (1 subgoal):
 1. x\<^sup>T ; p \<cdot> y ; r \<noteq> 0
[PROOF STEP]
by (metis assms(1) inf.absorb2 is_point_def maddux_141 point_is_point mult.assoc)
[PROOF STATE]
proof (state)
this:
x\<^sup>T ; p \<cdot> y ; r \<noteq> 0

goal (2 subgoals):
 1. p \<le> x ; y ; r \<Longrightarrow> \<exists>q. point q \<and> p \<le> x ; q \<and> q \<le> y ; r
 2. \<exists>q. point q \<and> p \<le> x ; q \<and> q \<le> y ; r \<Longrightarrow> p \<le> x ; y ; r
[PROOF STEP]
hence "\<exists>q . point q \<and> q \<le> ?v"
[PROOF STATE]
proof (prove)
using this:
x\<^sup>T ; p \<cdot> y ; r \<noteq> 0

goal (1 subgoal):
 1. \<exists>q. point q \<and> q \<le> x\<^sup>T ; p \<cdot> y ; r
[PROOF STEP]
using 2 point_below_vector
[PROOF STATE]
proof (prove)
using this:
x\<^sup>T ; p \<cdot> y ; r \<noteq> 0
is_vector (x\<^sup>T ; p \<cdot> y ; r)
\<lbrakk>is_vector ?v; ?v \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>x. point x \<and> x \<le> ?v

goal (1 subgoal):
 1. \<exists>q. point q \<and> q \<le> x\<^sup>T ; p \<cdot> y ; r
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>q. point q \<and> q \<le> x\<^sup>T ; p \<cdot> y ; r

goal (2 subgoals):
 1. p \<le> x ; y ; r \<Longrightarrow> \<exists>q. point q \<and> p \<le> x ; q \<and> q \<le> y ; r
 2. \<exists>q. point q \<and> p \<le> x ; q \<and> q \<le> y ; r \<Longrightarrow> p \<le> x ; y ; r
[PROOF STEP]
thus "\<exists>q . point q \<and> p \<le> x;q \<and> q \<le> y;r"
[PROOF STATE]
proof (prove)
using this:
\<exists>q. point q \<and> q \<le> x\<^sup>T ; p \<cdot> y ; r

goal (1 subgoal):
 1. \<exists>q. point q \<and> p \<le> x ; q \<and> q \<le> y ; r
[PROOF STEP]
using assms(1) point_swap
[PROOF STATE]
proof (prove)
using this:
\<exists>q. point q \<and> q \<le> x\<^sup>T ; p \<cdot> y ; r
point p
\<lbrakk>point ?p; point ?q\<rbrakk> \<Longrightarrow> (?p \<le> ?x ; ?q) = (?q \<le> ?x\<^sup>T ; ?p)

goal (1 subgoal):
 1. \<exists>q. point q \<and> p \<le> x ; q \<and> q \<le> y ; r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>q. point q \<and> p \<le> x ; q \<and> q \<le> y ; r

goal (1 subgoal):
 1. \<exists>q. point q \<and> p \<le> x ; q \<and> q \<le> y ; r \<Longrightarrow> p \<le> x ; y ; r
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>q. point q \<and> p \<le> x ; q \<and> q \<le> y ; r \<Longrightarrow> p \<le> x ; y ; r
[PROOF STEP]
assume "\<exists>q . point q \<and> p \<le> x;q \<and> q \<le> y;r"
[PROOF STATE]
proof (state)
this:
\<exists>q. point q \<and> p \<le> x ; q \<and> q \<le> y ; r

goal (1 subgoal):
 1. \<exists>q. point q \<and> p \<le> x ; q \<and> q \<le> y ; r \<Longrightarrow> p \<le> x ; y ; r
[PROOF STEP]
thus "p \<le> x;y;r"
[PROOF STATE]
proof (prove)
using this:
\<exists>q. point q \<and> p \<le> x ; q \<and> q \<le> y ; r

goal (1 subgoal):
 1. p \<le> x ; y ; r
[PROOF STEP]
using comp_assoc mult_isol order_trans
[PROOF STATE]
proof (prove)
using this:
\<exists>q. point q \<and> p \<le> x ; q \<and> q \<le> y ; r
?x ; ?y ; ?z = ?x ; (?y ; ?z)
?x \<le> ?y \<Longrightarrow> ?z ; ?x \<le> ?z ; ?y
\<lbrakk>?x \<le> ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x \<le> ?z

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unfoldl_inductl_implies_unfoldr:
  assumes "\<And>x. 1' + x;(rtc x) \<le> rtc x"
      and "\<And>x y z. x+y;z \<le> z \<Longrightarrow> rtc(y);x \<le> z"
    shows "1' + rtc(x);x \<le> rtc x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1' + rtc x ; x \<le> rtc x
[PROOF STEP]
by (metis assms le_sup_iff mult_oner order.trans subdistl_eq sup_absorb2 sup_ge1)


[STATEMENT]
lemma star_transpose_swap:
  assumes "\<And>x. 1' + x;(rtc x) \<le> rtc x"
      and "\<And>x y z. x+y;z \<le> z \<Longrightarrow> rtc(y);x \<le> z"
    shows "rtc(x\<^sup>T) = (rtc x)\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rtc (x\<^sup>T) = rtc x\<^sup>T
[PROOF STEP]
apply(simp only: order.eq_iff; rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. rtc (x\<^sup>T) \<le> rtc x\<^sup>T
 2. rtc x\<^sup>T \<le> rtc (x\<^sup>T)
[PROOF STEP]
apply (metis assms conv_add conv_contrav conv_e conv_iso mult_1_right
             unfoldl_inductl_implies_unfoldr )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rtc x\<^sup>T \<le> rtc (x\<^sup>T)
[PROOF STEP]
by (metis assms conv_add conv_contrav conv_e conv_invol conv_iso mult_1_right
          unfoldl_inductl_implies_unfoldr)


[STATEMENT]
lemma unfoldl_inductl_implies_inductr:
  assumes "\<And>x. 1' + x;(rtc x) \<le> rtc x"
      and "\<And>x y z. x+y;z \<le> z \<Longrightarrow> rtc(y);x \<le> z"
    shows "x+z;y \<le> z \<Longrightarrow> x;rtc(y) \<le> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x + z ; y \<le> z \<Longrightarrow> x ; rtc y \<le> z
[PROOF STEP]
by (metis assms conv_add conv_contrav conv_iso star_transpose_swap)


[STATEMENT]
lemma star_denest_10:
  assumes "x;y=0"
    shows "(x+y)\<^sup>\<star> = y;y\<^sup>\<star>;x\<^sup>\<star>+x\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x + y)\<^sup>\<star> = y\<^sup>+ ; x\<^sup>\<star> + x\<^sup>\<star>
[PROOF STEP]
using assms bubble_sort sup.commute
[PROOF STATE]
proof (prove)
using this:
x ; y = 0
?y ; ?x \<le> ?x ; ?y \<Longrightarrow> (?x + ?y)\<^sup>\<star> = ?x\<^sup>\<star> ; ?y\<^sup>\<star>
?a + ?b = ?b + ?a

goal (1 subgoal):
 1. (x + y)\<^sup>\<star> = y\<^sup>+ ; x\<^sup>\<star> + x\<^sup>\<star>
[PROOF STEP]
by auto


[STATEMENT]
lemma star_star_plus:
  "x\<^sup>\<star> + y\<^sup>\<star> = x\<^sup>+ + y\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<star> + y\<^sup>\<star> = x\<^sup>+ + y\<^sup>\<star>
[PROOF STEP]
by (metis (full_types) sup.left_commute star_plus_one star_unfoldl_eq sup.commute)


[STATEMENT]
lemma cancel_separate:
  assumes "x ; y \<le> 1'"
  shows "x\<^sup>\<star> ; y\<^sup>\<star> \<le> x\<^sup>\<star> + y\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<star> ; y\<^sup>\<star> \<le> x\<^sup>\<star> + y\<^sup>\<star>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x\<^sup>\<star> ; y\<^sup>\<star> \<le> x\<^sup>\<star> + y\<^sup>\<star>
[PROOF STEP]
have "x ; y\<^sup>\<star> = x + x ; y ; y\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x ; y\<^sup>\<star> = x + x ; y ; y\<^sup>\<star>
[PROOF STEP]
by (metis comp_assoc conway.dagger_unfoldl_distr distrib_left mult_oner)
[PROOF STATE]
proof (state)
this:
x ; y\<^sup>\<star> = x + x ; y ; y\<^sup>\<star>

goal (1 subgoal):
 1. x\<^sup>\<star> ; y\<^sup>\<star> \<le> x\<^sup>\<star> + y\<^sup>\<star>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x ; y\<^sup>\<star> = x + x ; y ; y\<^sup>\<star>

goal (1 subgoal):
 1. x\<^sup>\<star> ; y\<^sup>\<star> \<le> x\<^sup>\<star> + y\<^sup>\<star>
[PROOF STEP]
have "... \<le> x + y\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x + x ; y ; y\<^sup>\<star> \<le> x + y\<^sup>\<star>
[PROOF STEP]
by (metis assms join_isol star_invol star_plus_one star_subdist_var_2 sup.absorb2 sup.assoc)
[PROOF STATE]
proof (state)
this:
x + x ; y ; y\<^sup>\<star> \<le> x + y\<^sup>\<star>

goal (1 subgoal):
 1. x\<^sup>\<star> ; y\<^sup>\<star> \<le> x\<^sup>\<star> + y\<^sup>\<star>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x + x ; y ; y\<^sup>\<star> \<le> x + y\<^sup>\<star>

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

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

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

goal (1 subgoal):
 1. x ; (x\<^sup>\<star> + y\<^sup>\<star>) \<le> x\<^sup>\<star> + y\<^sup>\<star>
[PROOF STEP]
by (simp add: distrib_left le_supI1)
[PROOF STATE]
proof (state)
this:
x ; (x\<^sup>\<star> + y\<^sup>\<star>) \<le> x\<^sup>\<star> + y\<^sup>\<star>

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

goal (1 subgoal):
 1. x\<^sup>\<star> ; y\<^sup>\<star> \<le> x\<^sup>\<star> + y\<^sup>\<star>
[PROOF STEP]
by (simp add: rtc_inductl)
[PROOF STATE]
proof (state)
this:
x\<^sup>\<star> ; y\<^sup>\<star> \<le> x\<^sup>\<star> + y\<^sup>\<star>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cancel_separate_inj_converse:
  assumes "is_inj x"
    shows "x\<^sup>\<star> ; x\<^sup>T\<^sup>\<star> = x\<^sup>\<star> + x\<^sup>T\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<star> ; x\<^sup>T\<^sup>\<star> = x\<^sup>\<star> + x\<^sup>T\<^sup>\<star>
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x\<^sup>\<star> ; x\<^sup>T\<^sup>\<star> \<le> x\<^sup>\<star> + x\<^sup>T\<^sup>\<star>
 2. x\<^sup>\<star> + x\<^sup>T\<^sup>\<star> \<le> x\<^sup>\<star> ; x\<^sup>T\<^sup>\<star>
[PROOF STEP]
using assms cancel_separate is_inj_def
[PROOF STATE]
proof (prove)
using this:
is_inj x
?x ; ?y \<le> 1' \<Longrightarrow> ?x\<^sup>\<star> ; ?y\<^sup>\<star> \<le> ?x\<^sup>\<star> + ?y\<^sup>\<star>
is_inj ?x \<equiv> ?x ; ?x\<^sup>T \<le> 1'

goal (2 subgoals):
 1. x\<^sup>\<star> ; x\<^sup>T\<^sup>\<star> \<le> x\<^sup>\<star> + x\<^sup>T\<^sup>\<star>
 2. x\<^sup>\<star> + x\<^sup>T\<^sup>\<star> \<le> x\<^sup>\<star> ; x\<^sup>T\<^sup>\<star>
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<star> + x\<^sup>T\<^sup>\<star> \<le> x\<^sup>\<star> ; x\<^sup>T\<^sup>\<star>
[PROOF STEP]
by (metis conway.dagger_unfoldl_distr le_supI mult_1_right mult_isol sup.cobounded1)


[STATEMENT]
lemma cancel_separate_p_fun_converse:
  assumes "is_p_fun x"
    shows "x\<^sup>T\<^sup>\<star> ; x\<^sup>\<star> = x\<^sup>\<star> + x\<^sup>T\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>T\<^sup>\<star> ; x\<^sup>\<star> = x\<^sup>\<star> + x\<^sup>T\<^sup>\<star>
[PROOF STEP]
using sup_commute assms cancel_separate_inj_converse p_fun_inj
[PROOF STATE]
proof (prove)
using this:
?x + ?y = ?y + ?x
is_p_fun x
is_inj ?x \<Longrightarrow> ?x\<^sup>\<star> ; ?x\<^sup>T\<^sup>\<star> = ?x\<^sup>\<star> + ?x\<^sup>T\<^sup>\<star>
is_p_fun ?x = is_inj (?x\<^sup>T)

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


[STATEMENT]
lemma cancel_separate_converse_idempotent:
  assumes "is_inj x"
      and "is_p_fun x"
    shows "(x\<^sup>\<star> + x\<^sup>T\<^sup>\<star>);(x\<^sup>\<star> + x\<^sup>T\<^sup>\<star>) = x\<^sup>\<star> + x\<^sup>T\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x\<^sup>\<star> + x\<^sup>T\<^sup>\<star>) ; (x\<^sup>\<star> + x\<^sup>T\<^sup>\<star>) = x\<^sup>\<star> + x\<^sup>T\<^sup>\<star>
[PROOF STEP]
by (metis assms cancel_separate cancel_separate_p_fun_converse church_rosser_equiv is_inj_def
          star_denest_var_6)


[STATEMENT]
lemma triple_star:
  assumes "is_inj x"
      and "is_p_fun x"
    shows "x\<^sup>\<star>;x\<^sup>T\<^sup>\<star>;x\<^sup>\<star> = x\<^sup>\<star> + x\<^sup>T\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<star> ; x\<^sup>T\<^sup>\<star> ; x\<^sup>\<star> = x\<^sup>\<star> + x\<^sup>T\<^sup>\<star>
[PROOF STEP]
by (simp add: assms cancel_separate_inj_converse cancel_separate_p_fun_converse)


[STATEMENT]
lemma inj_xxts:
  assumes "is_inj x"
    shows "x;x\<^sup>T\<^sup>\<star> \<le> x\<^sup>\<star> + x\<^sup>T\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x ; x\<^sup>T\<^sup>\<star> \<le> x\<^sup>\<star> + x\<^sup>T\<^sup>\<star>
[PROOF STEP]
by (metis assms cancel_separate_inj_converse distrib_right less_eq_def star_ext)


[STATEMENT]
lemma top_plus:
  "1;x\<^sup>+ = 1;x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 ; x\<^sup>+ = 1 ; x
[PROOF STEP]
by (metis comp_assoc conway.dagger_unfoldr_distr star_denest_var_2 star_ext star_slide_var
           sup_top_left top_unique)


[STATEMENT]
lemma plus_conv:
  "(x\<^sup>+)\<^sup>T = x\<^sup>T\<^sup>+"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x\<^sup>+)\<^sup>T = x\<^sup>T\<^sup>+
[PROOF STEP]
by (simp add: star_conv star_slide_var)


[STATEMENT]
lemma inj_implies_step_forwards_backwards:
  assumes "is_inj x"
    shows "x\<^sup>\<star>;(x\<^sup>+\<cdot>1');1 \<le> x\<^sup>T;1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<star> ; (x\<^sup>+ \<cdot> 1') ; 1 \<le> x\<^sup>T ; 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x\<^sup>\<star> ; (x\<^sup>+ \<cdot> 1') ; 1 \<le> x\<^sup>T ; 1
[PROOF STEP]
have "(x\<^sup>+\<cdot>1');1 \<le> (x\<^sup>\<star>\<cdot>x\<^sup>T);(x\<cdot>(x\<^sup>\<star>)\<^sup>T);1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x\<^sup>+ \<cdot> 1') ; 1 \<le> (x\<^sup>\<star> \<cdot> x\<^sup>T) ; (x \<cdot> (x\<^sup>\<star>)\<^sup>T) ; 1
[PROOF STEP]
by (metis conv_contrav conv_e dedekind mult_1_right mult_isor star_slide_var)
[PROOF STATE]
proof (state)
this:
(x\<^sup>+ \<cdot> 1') ; 1 \<le> (x\<^sup>\<star> \<cdot> x\<^sup>T) ; (x \<cdot> (x\<^sup>\<star>)\<^sup>T) ; 1

goal (1 subgoal):
 1. x\<^sup>\<star> ; (x\<^sup>+ \<cdot> 1') ; 1 \<le> x\<^sup>T ; 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x\<^sup>+ \<cdot> 1') ; 1 \<le> (x\<^sup>\<star> \<cdot> x\<^sup>T) ; (x \<cdot> (x\<^sup>\<star>)\<^sup>T) ; 1

goal (1 subgoal):
 1. x\<^sup>\<star> ; (x\<^sup>+ \<cdot> 1') ; 1 \<le> x\<^sup>T ; 1
[PROOF STEP]
have "... \<le> (x\<^sup>\<star>\<cdot>x\<^sup>T);1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x\<^sup>\<star> \<cdot> x\<^sup>T) ; (x \<cdot> (x\<^sup>\<star>)\<^sup>T) ; 1 \<le> (x\<^sup>\<star> \<cdot> x\<^sup>T) ; 1
[PROOF STEP]
by (simp add: comp_assoc mult_isol)
[PROOF STATE]
proof (state)
this:
(x\<^sup>\<star> \<cdot> x\<^sup>T) ; (x \<cdot> (x\<^sup>\<star>)\<^sup>T) ; 1 \<le> (x\<^sup>\<star> \<cdot> x\<^sup>T) ; 1

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

goal (1 subgoal):
 1. (x\<^sup>+ \<cdot> 1') ; 1 \<le> (x\<^sup>\<star> \<cdot> x\<^sup>T) ; 1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(x\<^sup>+ \<cdot> 1') ; 1 \<le> (x\<^sup>\<star> \<cdot> x\<^sup>T) ; 1

goal (1 subgoal):
 1. x\<^sup>\<star> ; (x\<^sup>+ \<cdot> 1') ; 1 \<le> x\<^sup>T ; 1
[PROOF STEP]
have "x;(x\<^sup>\<star>\<cdot>x\<^sup>T);1 \<le> (x\<^sup>+\<cdot>x;x\<^sup>T);1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x ; (x\<^sup>\<star> \<cdot> x\<^sup>T) ; 1 \<le> (x\<^sup>+ \<cdot> x ; x\<^sup>T) ; 1
[PROOF STEP]
by (metis inf_idem meet_interchange mult_isor)
[PROOF STATE]
proof (state)
this:
x ; (x\<^sup>\<star> \<cdot> x\<^sup>T) ; 1 \<le> (x\<^sup>+ \<cdot> x ; x\<^sup>T) ; 1

goal (1 subgoal):
 1. x\<^sup>\<star> ; (x\<^sup>+ \<cdot> 1') ; 1 \<le> x\<^sup>T ; 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x ; (x\<^sup>\<star> \<cdot> x\<^sup>T) ; 1 \<le> (x\<^sup>+ \<cdot> x ; x\<^sup>T) ; 1

goal (1 subgoal):
 1. x\<^sup>\<star> ; (x\<^sup>+ \<cdot> 1') ; 1 \<le> x\<^sup>T ; 1
[PROOF STEP]
have "... \<le> (x\<^sup>+\<cdot>1');1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x\<^sup>+ \<cdot> x ; x\<^sup>T) ; 1 \<le> (x\<^sup>+ \<cdot> 1') ; 1
[PROOF STEP]
using assms is_inj_def meet_isor mult_isor
[PROOF STATE]
proof (prove)
using this:
is_inj x
is_inj ?x \<equiv> ?x ; ?x\<^sup>T \<le> 1'
?x \<le> ?y \<Longrightarrow> ?z \<cdot> ?x \<le> ?z \<cdot> ?y
?x \<le> ?y \<Longrightarrow> ?x ; ?z \<le> ?y ; ?z

goal (1 subgoal):
 1. (x\<^sup>+ \<cdot> x ; x\<^sup>T) ; 1 \<le> (x\<^sup>+ \<cdot> 1') ; 1
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(x\<^sup>+ \<cdot> x ; x\<^sup>T) ; 1 \<le> (x\<^sup>+ \<cdot> 1') ; 1

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

goal (1 subgoal):
 1. x ; (x\<^sup>\<star> \<cdot> x\<^sup>T) ; 1 \<le> (x\<^sup>\<star> \<cdot> x\<^sup>T) ; 1
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
x ; (x\<^sup>\<star> \<cdot> x\<^sup>T) ; 1 \<le> (x\<^sup>+ \<cdot> 1') ; 1
(x\<^sup>+ \<cdot> 1') ; 1 \<le> (x\<^sup>\<star> \<cdot> x\<^sup>T) ; 1

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

goal (1 subgoal):
 1. x\<^sup>\<star> ; (x\<^sup>+ \<cdot> 1') ; 1 \<le> x\<^sup>T ; 1
[PROOF STEP]
hence "x\<^sup>\<star>;(x\<^sup>+\<cdot>1');1 \<le> (x\<^sup>\<star>\<cdot>x\<^sup>T);1"
[PROOF STATE]
proof (prove)
using this:
x ; (x\<^sup>\<star> \<cdot> x\<^sup>T) ; 1 \<le> (x\<^sup>\<star> \<cdot> x\<^sup>T) ; 1

goal (1 subgoal):
 1. x\<^sup>\<star> ; (x\<^sup>+ \<cdot> 1') ; 1 \<le> (x\<^sup>\<star> \<cdot> x\<^sup>T) ; 1
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
x ; (x\<^sup>\<star> \<cdot> x\<^sup>T) ; 1 \<le> (x\<^sup>\<star> \<cdot> x\<^sup>T) ; 1
(x\<^sup>+ \<cdot> 1') ; 1 \<le> (x\<^sup>\<star> \<cdot> x\<^sup>T) ; 1

goal (1 subgoal):
 1. x\<^sup>\<star> ; (x\<^sup>+ \<cdot> 1') ; 1 \<le> (x\<^sup>\<star> \<cdot> x\<^sup>T) ; 1
[PROOF STEP]
by (simp add: comp_assoc rtc_inductl)
[PROOF STATE]
proof (state)
this:
x\<^sup>\<star> ; (x\<^sup>+ \<cdot> 1') ; 1 \<le> (x\<^sup>\<star> \<cdot> x\<^sup>T) ; 1

goal (1 subgoal):
 1. x\<^sup>\<star> ; (x\<^sup>+ \<cdot> 1') ; 1 \<le> x\<^sup>T ; 1
[PROOF STEP]
thus "x\<^sup>\<star>;(x\<^sup>+\<cdot>1');1 \<le> x\<^sup>T;1"
[PROOF STATE]
proof (prove)
using this:
x\<^sup>\<star> ; (x\<^sup>+ \<cdot> 1') ; 1 \<le> (x\<^sup>\<star> \<cdot> x\<^sup>T) ; 1

goal (1 subgoal):
 1. x\<^sup>\<star> ; (x\<^sup>+ \<cdot> 1') ; 1 \<le> x\<^sup>T ; 1
[PROOF STEP]
using inf.cobounded2 mult_isor order_trans
[PROOF STATE]
proof (prove)
using this:
x\<^sup>\<star> ; (x\<^sup>+ \<cdot> 1') ; 1 \<le> (x\<^sup>\<star> \<cdot> x\<^sup>T) ; 1
?a \<cdot> ?b \<le> ?b
?x \<le> ?y \<Longrightarrow> ?x ; ?z \<le> ?y ; ?z
\<lbrakk>?x \<le> ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x \<le> ?z

goal (1 subgoal):
 1. x\<^sup>\<star> ; (x\<^sup>+ \<cdot> 1') ; 1 \<le> x\<^sup>T ; 1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x\<^sup>\<star> ; (x\<^sup>+ \<cdot> 1') ; 1 \<le> x\<^sup>T ; 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma acyclic_inv:
  assumes "is_acyclic t"
      and "is_vector v"
      and "e \<le> v;-v\<^sup>T"
      and "t \<le> v;v\<^sup>T"
    shows "is_acyclic (t + e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
have "t\<^sup>+;e \<le> t\<^sup>+;v;-v\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t\<^sup>+ ; e \<le> t\<^sup>+ ; v ; - v\<^sup>T
[PROOF STEP]
by (simp add: assms(3) mult_assoc mult_isol)
[PROOF STATE]
proof (state)
this:
t\<^sup>+ ; e \<le> t\<^sup>+ ; v ; - v\<^sup>T

goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
t\<^sup>+ ; e \<le> t\<^sup>+ ; v ; - v\<^sup>T

goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
have "... \<le> v;v\<^sup>T;t\<^sup>\<star>;v;-v\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t\<^sup>+ ; v ; - v\<^sup>T \<le> v ; v\<^sup>T ; t\<^sup>\<star> ; v ; - v\<^sup>T
[PROOF STEP]
by (simp add: assms(4) mult_isor)
[PROOF STATE]
proof (state)
this:
t\<^sup>+ ; v ; - v\<^sup>T \<le> v ; v\<^sup>T ; t\<^sup>\<star> ; v ; - v\<^sup>T

goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
t\<^sup>+ ; v ; - v\<^sup>T \<le> v ; v\<^sup>T ; t\<^sup>\<star> ; v ; - v\<^sup>T

goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
have "... \<le> v;-v\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v ; v\<^sup>T ; t\<^sup>\<star> ; v ; - v\<^sup>T \<le> v ; - v\<^sup>T
[PROOF STEP]
by (metis assms(2) mult_double_iso top_greatest is_vector_def mult_assoc)
[PROOF STATE]
proof (state)
this:
v ; v\<^sup>T ; t\<^sup>\<star> ; v ; - v\<^sup>T \<le> v ; - v\<^sup>T

goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
v ; v\<^sup>T ; t\<^sup>\<star> ; v ; - v\<^sup>T \<le> v ; - v\<^sup>T

goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
have "... \<le> -1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v ; - v\<^sup>T \<le> - 1'
[PROOF STEP]
by (simp add: conv_galois_1)
[PROOF STATE]
proof (state)
this:
v ; - v\<^sup>T \<le> - 1'

goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
t\<^sup>+ ; e \<le> - 1'
[PROOF STEP]
have 1: "t\<^sup>+;e \<le> -1'"
[PROOF STATE]
proof (prove)
using this:
t\<^sup>+ ; e \<le> - 1'

goal (1 subgoal):
 1. t\<^sup>+ ; e \<le> - 1'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
t\<^sup>+ ; e \<le> - 1'

goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
have "e \<le> v;-v\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e \<le> v ; - v\<^sup>T
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
e \<le> v ; - v\<^sup>T

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

goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
e \<le> v ; - v\<^sup>T

goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
have "... \<le> -1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v ; - v\<^sup>T \<le> - 1'
[PROOF STEP]
by (simp add: conv_galois_1)
[PROOF STATE]
proof (state)
this:
v ; - v\<^sup>T \<le> - 1'

goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
e \<le> - 1'
[PROOF STEP]
have 2: "t\<^sup>+;e + e \<le> -1'"
[PROOF STATE]
proof (prove)
using this:
e \<le> - 1'

goal (1 subgoal):
 1. t\<^sup>+ ; e + e \<le> - 1'
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
e \<le> - 1'
t\<^sup>+ ; e \<le> - 1'

goal (1 subgoal):
 1. t\<^sup>+ ; e + e \<le> - 1'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t\<^sup>+ ; e + e \<le> - 1'

goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
have 3: "e;t\<^sup>\<star> = e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e ; t\<^sup>\<star> = e
[PROOF STEP]
by (metis assms(2-4) et(1) independence2)
[PROOF STATE]
proof (state)
this:
e ; t\<^sup>\<star> = e

goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
have 4: "e\<^sup>\<star> = 1' + e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e\<^sup>\<star> = 1' + e
[PROOF STEP]
using assms(2-3) ee boffa_var bot_least
[PROOF STATE]
proof (prove)
using this:
is_vector v
e \<le> v ; - v\<^sup>T
\<lbrakk>is_vector ?v; ?e \<le> ?v ; - ?v\<^sup>T\<rbrakk> \<Longrightarrow> ?e ; ?e = 0
transitive ?x \<Longrightarrow> ?x\<^sup>\<star> = 1' + ?x
0 \<le> ?a

goal (1 subgoal):
 1. e\<^sup>\<star> = 1' + e
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
e\<^sup>\<star> = 1' + e

goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
have "(t + e)\<^sup>+ = (t + e);t\<^sup>\<star>;(e;t\<^sup>\<star>)\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t + e)\<^sup>+ = (t + e) ; t\<^sup>\<star> ; (e ; t\<^sup>\<star>)\<^sup>\<star>
[PROOF STEP]
by (simp add: comp_assoc)
[PROOF STATE]
proof (state)
this:
(t + e)\<^sup>+ = (t + e) ; t\<^sup>\<star> ; (e ; t\<^sup>\<star>)\<^sup>\<star>

goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(t + e)\<^sup>+ = (t + e) ; t\<^sup>\<star> ; (e ; t\<^sup>\<star>)\<^sup>\<star>

goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
have "... = (t + e);t\<^sup>\<star>;(1' + e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t + e) ; t\<^sup>\<star> ; (e ; t\<^sup>\<star>)\<^sup>\<star> = (t + e) ; t\<^sup>\<star> ; (1' + e)
[PROOF STEP]
using 3 4
[PROOF STATE]
proof (prove)
using this:
e ; t\<^sup>\<star> = e
e\<^sup>\<star> = 1' + e

goal (1 subgoal):
 1. (t + e) ; t\<^sup>\<star> ; (e ; t\<^sup>\<star>)\<^sup>\<star> = (t + e) ; t\<^sup>\<star> ; (1' + e)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(t + e) ; t\<^sup>\<star> ; (e ; t\<^sup>\<star>)\<^sup>\<star> = (t + e) ; t\<^sup>\<star> ; (1' + e)

goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(t + e) ; t\<^sup>\<star> ; (e ; t\<^sup>\<star>)\<^sup>\<star> = (t + e) ; t\<^sup>\<star> ; (1' + e)

goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
have "... = t\<^sup>+;(1' + e) + e;t\<^sup>\<star>;(1' + e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t + e) ; t\<^sup>\<star> ; (1' + e) = t\<^sup>+ ; (1' + e) + e ; t\<^sup>\<star> ; (1' + e)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(t + e) ; t\<^sup>\<star> ; (1' + e) = t\<^sup>+ ; (1' + e) + e ; t\<^sup>\<star> ; (1' + e)

goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(t + e) ; t\<^sup>\<star> ; (1' + e) = t\<^sup>+ ; (1' + e) + e ; t\<^sup>\<star> ; (1' + e)

goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
have "... = t\<^sup>+;(1' + e) + e;(1' + e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t\<^sup>+ ; (1' + e) + e ; t\<^sup>\<star> ; (1' + e) = t\<^sup>+ ; (1' + e) + e ; (1' + e)
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
e ; t\<^sup>\<star> = e

goal (1 subgoal):
 1. t\<^sup>+ ; (1' + e) + e ; t\<^sup>\<star> ; (1' + e) = t\<^sup>+ ; (1' + e) + e ; (1' + e)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t\<^sup>+ ; (1' + e) + e ; t\<^sup>\<star> ; (1' + e) = t\<^sup>+ ; (1' + e) + e ; (1' + e)

goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
t\<^sup>+ ; (1' + e) + e ; t\<^sup>\<star> ; (1' + e) = t\<^sup>+ ; (1' + e) + e ; (1' + e)

goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
have "... = t\<^sup>+;(1' + e) + e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t\<^sup>+ ; (1' + e) + e ; (1' + e) = t\<^sup>+ ; (1' + e) + e
[PROOF STEP]
using 4 assms(2-3) ee independence2
[PROOF STATE]
proof (prove)
using this:
e\<^sup>\<star> = 1' + e
is_vector v
e \<le> v ; - v\<^sup>T
\<lbrakk>is_vector ?v; ?e \<le> ?v ; - ?v\<^sup>T\<rbrakk> \<Longrightarrow> ?e ; ?e = 0
?x ; ?y = 0 \<Longrightarrow> ?x ; ?y\<^sup>\<star> = ?x

goal (1 subgoal):
 1. t\<^sup>+ ; (1' + e) + e ; (1' + e) = t\<^sup>+ ; (1' + e) + e
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
t\<^sup>+ ; (1' + e) + e ; (1' + e) = t\<^sup>+ ; (1' + e) + e

goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
t\<^sup>+ ; (1' + e) + e ; (1' + e) = t\<^sup>+ ; (1' + e) + e

goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
have "... = t\<^sup>+ + t\<^sup>+;e + e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t\<^sup>+ ; (1' + e) + e = t\<^sup>+ + t\<^sup>+ ; e + e
[PROOF STEP]
by (simp add: distrib_left)
[PROOF STATE]
proof (state)
this:
t\<^sup>+ ; (1' + e) + e = t\<^sup>+ + t\<^sup>+ ; e + e

goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
t\<^sup>+ ; (1' + e) + e = t\<^sup>+ + t\<^sup>+ ; e + e

goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
have "... \<le> -1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t\<^sup>+ + t\<^sup>+ ; e + e \<le> - 1'
[PROOF STEP]
using assms(1) 2
[PROOF STATE]
proof (prove)
using this:
is_acyclic t
t\<^sup>+ ; e + e \<le> - 1'

goal (1 subgoal):
 1. t\<^sup>+ + t\<^sup>+ ; e + e \<le> - 1'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t\<^sup>+ + t\<^sup>+ ; e + e \<le> - 1'

goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
is_acyclic (t + e)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_acyclic (t + e)

goal (1 subgoal):
 1. is_acyclic (t + e)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
is_acyclic (t + e)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma acyclic_single_step:
  assumes "is_acyclic x"
    shows "x \<le> -1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> - 1'
[PROOF STEP]
by (metis assms dual_order.trans mult_isol mult_oner star_ref)


[STATEMENT]
lemma acyclic_reachable_points:
  assumes "is_point p"
      and "is_point q"
      and "p \<le> x;q"
      and "is_acyclic x"
    shows "p\<noteq>q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<noteq> q
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p = q \<Longrightarrow> False
[PROOF STEP]
assume "p=q"
[PROOF STATE]
proof (state)
this:
p = q

goal (1 subgoal):
 1. p = q \<Longrightarrow> False
[PROOF STEP]
hence "p \<le> x;q \<cdot> q"
[PROOF STATE]
proof (prove)
using this:
p = q

goal (1 subgoal):
 1. p \<le> x ; q \<cdot> q
[PROOF STEP]
by (simp add: assms(3) order.eq_iff inf.absorb2)
[PROOF STATE]
proof (state)
this:
p \<le> x ; q \<cdot> q

goal (1 subgoal):
 1. p = q \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
p \<le> x ; q \<cdot> q

goal (1 subgoal):
 1. p = q \<Longrightarrow> False
[PROOF STEP]
have "... = (x \<cdot> 1');q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x ; q \<cdot> q = (x \<cdot> 1') ; q
[PROOF STEP]
using assms(2) inj_distr is_point_def
[PROOF STATE]
proof (prove)
using this:
is_point q
is_inj ?z \<Longrightarrow> (?x \<cdot> ?y) ; ?z = ?x ; ?z \<cdot> ?y ; ?z
is_point ?x \<equiv> is_vector ?x \<and> is_inj ?x \<and> ?x \<noteq> 0

goal (1 subgoal):
 1. x ; q \<cdot> q = (x \<cdot> 1') ; q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x ; q \<cdot> q = (x \<cdot> 1') ; q

goal (1 subgoal):
 1. p = q \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x ; q \<cdot> q = (x \<cdot> 1') ; q

goal (1 subgoal):
 1. p = q \<Longrightarrow> False
[PROOF STEP]
have "... \<le> (-1' \<cdot> 1');q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<cdot> 1') ; q \<le> (- 1' \<cdot> 1') ; q
[PROOF STEP]
using acyclic_single_step assms(4)
[PROOF STATE]
proof (prove)
using this:
is_acyclic ?x \<Longrightarrow> ?x \<le> - 1'
is_acyclic x

goal (1 subgoal):
 1. (x \<cdot> 1') ; q \<le> (- 1' \<cdot> 1') ; q
[PROOF STEP]
by (metis abel_semigroup.commute inf.abel_semigroup_axioms
          meet_isor mult_isor)
[PROOF STATE]
proof (state)
this:
(x \<cdot> 1') ; q \<le> (- 1' \<cdot> 1') ; q

goal (1 subgoal):
 1. p = q \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x \<cdot> 1') ; q \<le> (- 1' \<cdot> 1') ; q

goal (1 subgoal):
 1. p = q \<Longrightarrow> False
[PROOF STEP]
have "... = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- 1' \<cdot> 1') ; q = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(- 1' \<cdot> 1') ; q = 0

goal (1 subgoal):
 1. p = q \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
p \<le> 0
[PROOF STEP]
have "p \<le> 0"
[PROOF STATE]
proof (prove)
using this:
p \<le> 0

goal (1 subgoal):
 1. p \<le> 0
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
p \<le> 0

goal (1 subgoal):
 1. p = q \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
p \<le> 0

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms(1) bot_unique is_point_def
[PROOF STATE]
proof (prove)
using this:
p \<le> 0
is_point p
(?a \<le> 0) = (?a = 0)
is_point ?x \<equiv> is_vector ?x \<and> is_inj ?x \<and> ?x \<noteq> 0

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma acyclic_trans:
 assumes "is_acyclic x"
   shows "x \<le> -(x\<^sup>T\<^sup>+)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> - x\<^sup>T\<^sup>+
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<le> - x\<^sup>T\<^sup>+
[PROOF STEP]
have "\<exists>c\<ge>x. c \<le> - (x\<^sup>+)\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c\<ge>x. c \<le> - (x\<^sup>+)\<^sup>T
[PROOF STEP]
by (metis assms compl_mono conv_galois_2 conv_iso double_compl mult_onel star_1l)
[PROOF STATE]
proof (state)
this:
\<exists>c\<ge>x. c \<le> - (x\<^sup>+)\<^sup>T

goal (1 subgoal):
 1. x \<le> - x\<^sup>T\<^sup>+
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>c\<ge>x. c \<le> - (x\<^sup>+)\<^sup>T

goal (1 subgoal):
 1. x \<le> - x\<^sup>T\<^sup>+
[PROOF STEP]
by (metis dual_order.trans plus_conv)
[PROOF STATE]
proof (state)
this:
x \<le> - x\<^sup>T\<^sup>+

goal:
No subgoals!
[PROOF STEP]
qed