[STATEMENT]
lemma (in Congruence_Rule) Ang_external_Gr_lemma2 :
  assumes N :
    "Def (Tri (Tr A B C))"
    "Bet_Point (Se B D) A"
  shows "\<not> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
assume W : "Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp)"
[PROOF STATE]
proof (state)
this:
Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from N
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A
[PROOF STEP]
have "\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi A) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi D) add Emp) (Geos (Poi A) add Emp)
[PROOF STEP]
by (simp add:Bet_Point_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi A) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi A) add Emp)
[PROOF STEP]
have P1 : "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi A) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P2 : "Line_on (Li A D) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A D) A
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A D) A

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from N
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A
[PROOF STEP]
have P3 : "Line_on (Li A D) B"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A

goal (1 subgoal):
 1. Line_on (Li A D) B
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li A D) B

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P4 : "Line_on (Li A B) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A B) A
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A B) A

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P5 : "Line_on (Li A B) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A B) B
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A B) B

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from N
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A
[PROOF STEP]
have P6 : "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
[PROOF STEP]
by (simp add:Tri_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P2 P3 P4 P5 P6
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A D) A
Line_on (Li A D) B
Line_on (Li A B) A
Line_on (Li A B) B
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
[PROOF STEP]
have "Eq (Geos (Lin (Li A D)) add Emp) (Geos (Lin (Li A B)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A D) A
Line_on (Li A D) B
Line_on (Li A B) A
Line_on (Li A B) B
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Lin (Li A D)) add Emp) (Geos (Lin (Li A B)) add Emp)
[PROOF STEP]
by (simp add:Line_unique)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li A D)) add Emp) (Geos (Lin (Li A B)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li A D)) add Emp) (Geos (Lin (Li A B)) add Emp)
[PROOF STEP]
have P7 : "Line_on (Li A D) C \<Longrightarrow> Line_on (Li A B) C"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li A D)) add Emp) (Geos (Lin (Li A B)) add Emp)

goal (1 subgoal):
 1. Line_on (Li A D) C \<Longrightarrow> Line_on (Li A B) C
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Line_on (Li A D) C \<Longrightarrow> Line_on (Li A B) C

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from N
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A
[PROOF STEP]
have P8 : "\<not> Line_on (Li A B) C"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A

goal (1 subgoal):
 1. \<not> Line_on (Li A B) C
[PROOF STEP]
by (simp add:Tri_def_Line)
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li A B) C

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P7 P8
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A D) C \<Longrightarrow> Line_on (Li A B) C
\<not> Line_on (Li A B) C
[PROOF STEP]
have P9 : "\<not> Line_on (Li A D) C"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A D) C \<Longrightarrow> Line_on (Li A B) C
\<not> Line_on (Li A B) C

goal (1 subgoal):
 1. \<not> Line_on (Li A D) C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li A D) C

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P1 P9
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)
\<not> Line_on (Li A D) C
[PROOF STEP]
have "Def (Ang (An A D C))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)
\<not> Line_on (Li A D) C

goal (1 subgoal):
 1. Def (Ang (An A D C))
[PROOF STEP]
by (simp add:Ang_sinple_def)
[PROOF STATE]
proof (state)
this:
Def (Ang (An A D C))

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A D C))
[PROOF STEP]
have P10 : "Def (Ang (An C A D))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A D C))

goal (1 subgoal):
 1. Def (Ang (An C A D))
[PROOF STEP]
by (blast intro:Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An C A D))

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P11 : "Cong (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An B C A)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An B C A)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An B C A)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from N
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A
[PROOF STEP]
have P12 : "Def (Ang (An A C B))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A

goal (1 subgoal):
 1. Def (Ang (An A C B))
[PROOF STEP]
by (blast intro:Tri_to_Ang Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An A C B))

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A C B))
[PROOF STEP]
have P13 : "Def (Ang (An B C A))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A C B))

goal (1 subgoal):
 1. Def (Ang (An B C A))
[PROOF STEP]
by (simp add:Ang_def_rev)
[PROOF STATE]
proof (state)
this:
Def (Ang (An B C A))

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from W P10 P11 P12 P13
[PROOF STATE]
proof (chain)
picking this:
Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp)
Def (Ang (An C A D))
Cong (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An B C A)) add Emp)
Def (Ang (An A C B))
Def (Ang (An B C A))
[PROOF STEP]
have P14 : "Gr (Geos (Ang (An B C A)) add Emp) (Geos (Ang (An C A D)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp)
Def (Ang (An C A D))
Cong (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An B C A)) add Emp)
Def (Ang (An A C B))
Def (Ang (An B C A))

goal (1 subgoal):
 1. Gr (Geos (Ang (An B C A)) add Emp) (Geos (Ang (An C A D)) add Emp)
[PROOF STEP]
by (blast intro:Ang_Gr_trans_Eq_Gr Ang_rev)
[PROOF STATE]
proof (state)
this:
Gr (Geos (Ang (An B C A)) add Emp) (Geos (Ang (An C A D)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from N
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A
[PROOF STEP]
have P15 : "\<not> Line_on (Li C A) B"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A

goal (1 subgoal):
 1. \<not> Line_on (Li C A) B
[PROOF STEP]
by (simp add:Tri_def_Line)
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li C A) B

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from N
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A
[PROOF STEP]
have P16 : "\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
[PROOF STEP]
by (simp add:Tri_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P10 P15
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An C A D))
\<not> Line_on (Li C A) B
[PROOF STEP]
have "\<exists>p. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An p C A)) add Emp)
    \<and> Plane_sameside (Li C A) p B"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An C A D))
\<not> Line_on (Li C A) B

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An p C A)) add Emp) \<and> Plane_sameside (Li C A) p B
[PROOF STEP]
by (simp add:Ang_move_sameside)
[PROOF STATE]
proof (state)
this:
\<exists>p. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An p C A)) add Emp) \<and> Plane_sameside (Li C A) p B

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An p C A)) add Emp) \<and> Plane_sameside (Li C A) p B
[PROOF STEP]
obtain B1 :: Point where P17 : "Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An B1 C A)) add Emp)
    \<and> Plane_sameside (Li C A) B1 B"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An p C A)) add Emp) \<and> Plane_sameside (Li C A) p B

goal (1 subgoal):
 1. (\<And>B1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An B1 C A)) add Emp) \<and> Plane_sameside (Li C A) B1 B \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An B1 C A)) add Emp) \<and> Plane_sameside (Li C A) B1 B

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An B1 C A)) add Emp) \<and> Plane_sameside (Li C A) B1 B
[PROOF STEP]
have P18 : "\<not> Line_on (Li C A) B1"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An B1 C A)) add Emp) \<and> Plane_sameside (Li C A) B1 B

goal (1 subgoal):
 1. \<not> Line_on (Li C A) B1
[PROOF STEP]
by (simp add:Plane_sameside_def)
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li C A) B1

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P16 P18
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
\<not> Line_on (Li C A) B1
[PROOF STEP]
have "Def (Ang (An C A B1))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
\<not> Line_on (Li C A) B1

goal (1 subgoal):
 1. Def (Ang (An C A B1))
[PROOF STEP]
by (blast intro:Ang_sinple_def Eq_rev)
[PROOF STATE]
proof (state)
this:
Def (Ang (An C A B1))

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An C A B1))
[PROOF STEP]
have P19 : "Def (Ang (An B1 C A))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An C A B1))

goal (1 subgoal):
 1. Def (Ang (An B1 C A))
[PROOF STEP]
by (blast intro:Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An B1 C A))

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from N
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A
[PROOF STEP]
have P20 : "Def (Ang (An A C B))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A

goal (1 subgoal):
 1. Def (Ang (An A C B))
[PROOF STEP]
by (blast intro:Tri_def_rev Tri_def_trans Tri_to_Ang)
[PROOF STATE]
proof (state)
this:
Def (Ang (An A C B))

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P17
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An B1 C A)) add Emp) \<and> Plane_sameside (Li C A) B1 B
[PROOF STEP]
have P21 : "Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An B1 C A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An B1 C A)) add Emp) \<and> Plane_sameside (Li C A) B1 B

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An B1 C A)) add Emp)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An B1 C A)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P17
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An B1 C A)) add Emp) \<and> Plane_sameside (Li C A) B1 B
[PROOF STEP]
have P22 : "Plane_sameside (Li C A) B1 B"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An B1 C A)) add Emp) \<and> Plane_sameside (Li C A) B1 B

goal (1 subgoal):
 1. Plane_sameside (Li C A) B1 B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li C A) B1 B

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P10 P14 P19 P20 P21 P22
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An C A D))
Gr (Geos (Ang (An B C A)) add Emp) (Geos (Ang (An C A D)) add Emp)
Def (Ang (An B1 C A))
Def (Ang (An A C B))
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An B1 C A)) add Emp)
Plane_sameside (Li C A) B1 B
[PROOF STEP]
have "Ang_inside (An B C A) B1"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An C A D))
Gr (Geos (Ang (An B C A)) add Emp) (Geos (Ang (An C A D)) add Emp)
Def (Ang (An B1 C A))
Def (Ang (An A C B))
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An B1 C A)) add Emp)
Plane_sameside (Li C A) B1 B

goal (1 subgoal):
 1. Ang_inside (An B C A) B1
[PROOF STEP]
by (simp add:Ang_greater_def)
[PROOF STATE]
proof (state)
this:
Ang_inside (An B C A) B1

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An B C A) B1
[PROOF STEP]
have "Plane_diffside (Li C B1) B A"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An B C A) B1

goal (1 subgoal):
 1. Plane_diffside (Li C B1) B A
[PROOF STEP]
by (simp add:Ang_inside_Planeside)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li C B1) B A

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li C B1) B A
[PROOF STEP]
have "\<exists>p. Bet_Point (Se B A) p \<and> Line_on (Li C B1) p \<and> \<not> Line_on (Li C B1) B \<and> \<not> Line_on (Li C B1) A"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li C B1) B A

goal (1 subgoal):
 1. \<exists>p. Bet_Point (Se B A) p \<and> Line_on (Li C B1) p \<and> \<not> Line_on (Li C B1) B \<and> \<not> Line_on (Li C B1) A
[PROOF STEP]
by (simp add:Plane_diffside_def)
[PROOF STATE]
proof (state)
this:
\<exists>p. Bet_Point (Se B A) p \<and> Line_on (Li C B1) p \<and> \<not> Line_on (Li C B1) B \<and> \<not> Line_on (Li C B1) A

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Bet_Point (Se B A) p \<and> Line_on (Li C B1) p \<and> \<not> Line_on (Li C B1) B \<and> \<not> Line_on (Li C B1) A
[PROOF STEP]
obtain B2 :: Point where P23 : "Bet_Point (Se B A) B2 \<and> Line_on (Li C B1) B2
    \<and> \<not> Line_on (Li C B1) B \<and> \<not> Line_on (Li C B1) A"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Bet_Point (Se B A) p \<and> Line_on (Li C B1) p \<and> \<not> Line_on (Li C B1) B \<and> \<not> Line_on (Li C B1) A

goal (1 subgoal):
 1. (\<And>B2. Bet_Point (Se B A) B2 \<and> Line_on (Li C B1) B2 \<and> \<not> Line_on (Li C B1) B \<and> \<not> Line_on (Li C B1) A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet_Point (Se B A) B2 \<and> Line_on (Li C B1) B2 \<and> \<not> Line_on (Li C B1) B \<and> \<not> Line_on (Li C B1) A

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se B A) B2 \<and> Line_on (Li C B1) B2 \<and> \<not> Line_on (Li C B1) B \<and> \<not> Line_on (Li C B1) A
[PROOF STEP]
have "Line_on (Li B A) B2"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se B A) B2 \<and> Line_on (Li C B1) B2 \<and> \<not> Line_on (Li C B1) B \<and> \<not> Line_on (Li C B1) A

goal (1 subgoal):
 1. Line_on (Li B A) B2
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li B A) B2

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B A) B2
[PROOF STEP]
have P24 : "Eq (Geos (Poi B2) add Emp) (Geos (Poi C) add Emp) \<Longrightarrow> Line_on (Li B A) C"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B A) B2

goal (1 subgoal):
 1. Eq (Geos (Poi B2) add Emp) (Geos (Poi C) add Emp) \<Longrightarrow> Line_on (Li B A) C
[PROOF STEP]
by (simp add:Point_Eq)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi B2) add Emp) (Geos (Poi C) add Emp) \<Longrightarrow> Line_on (Li B A) C

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from N
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A
[PROOF STEP]
have "Def (Tri (Tr B A C))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A

goal (1 subgoal):
 1. Def (Tri (Tr B A C))
[PROOF STEP]
by (blast intro:Tri_def_rev Tri_def_trans)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr B A C))

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr B A C))
[PROOF STEP]
have P25 : "\<not> Line_on (Li B A) C"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr B A C))

goal (1 subgoal):
 1. \<not> Line_on (Li B A) C
[PROOF STEP]
by (simp add:Tri_def_Line)
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li B A) C

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P24 P25
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Poi B2) add Emp) (Geos (Poi C) add Emp) \<Longrightarrow> Line_on (Li B A) C
\<not> Line_on (Li B A) C
[PROOF STEP]
have P26 : "\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi B2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Poi B2) add Emp) (Geos (Poi C) add Emp) \<Longrightarrow> Line_on (Li B A) C
\<not> Line_on (Li B A) C

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi B2) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi B2) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P23
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se B A) B2 \<and> Line_on (Li C B1) B2 \<and> \<not> Line_on (Li C B1) B \<and> \<not> Line_on (Li C B1) A
[PROOF STEP]
have P27 : "Bet_Point (Se A B) B2"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se B A) B2 \<and> Line_on (Li C B1) B2 \<and> \<not> Line_on (Li C B1) B \<and> \<not> Line_on (Li C B1) A

goal (1 subgoal):
 1. Bet_Point (Se A B) B2
[PROOF STEP]
by (simp add:Bet_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A B) B2

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P28 : "Line_on (Li C A) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li C A) A
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li C A) A

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P5
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A B) B
[PROOF STEP]
have P29 : "Eq (Geos (Lin (Li A B)) add Emp) (Geos (Lin (Li C A)) add Emp) \<Longrightarrow>
    Line_on (Li C A) B"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A B) B

goal (1 subgoal):
 1. Eq (Geos (Lin (Li A B)) add Emp) (Geos (Lin (Li C A)) add Emp) \<Longrightarrow> Line_on (Li C A) B
[PROOF STEP]
by (simp add: Line_on_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li A B)) add Emp) (Geos (Lin (Li C A)) add Emp) \<Longrightarrow> Line_on (Li C A) B

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P15 P29
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li C A) B
Eq (Geos (Lin (Li A B)) add Emp) (Geos (Lin (Li C A)) add Emp) \<Longrightarrow> Line_on (Li C A) B
[PROOF STEP]
have P30 : "\<not> Eq (Geos (Lin (Li A B)) add Emp) (Geos (Lin (Li C A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li C A) B
Eq (Geos (Lin (Li A B)) add Emp) (Geos (Lin (Li C A)) add Emp) \<Longrightarrow> Line_on (Li C A) B

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li A B)) add Emp) (Geos (Lin (Li C A)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Lin (Li A B)) add Emp) (Geos (Lin (Li C A)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P27 P28 P30
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se A B) B2
Line_on (Li C A) A
\<not> Eq (Geos (Lin (Li A B)) add Emp) (Geos (Lin (Li C A)) add Emp)
[PROOF STEP]
have P31 : "Plane_sameside (Li C A) B B2"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se A B) B2
Line_on (Li C A) A
\<not> Eq (Geos (Lin (Li A B)) add Emp) (Geos (Lin (Li C A)) add Emp)

goal (1 subgoal):
 1. Plane_sameside (Li C A) B B2
[PROOF STEP]
by (simp add:Plane_Bet_sameside Plane_sameside_rev)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li C A) B B2

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P32 : "Line_on (Li C A) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li C A) C
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li C A) C

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have "Line_on (Li B1 B2) B1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B1 B2) B1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B1 B2) B1

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B1 B2) B1
[PROOF STEP]
have P33 : "Eq (Geos (Lin (Li B1 B2)) add Emp) (Geos (Lin (Li C A)) add Emp) \<Longrightarrow>
    Line_on (Li C A) B1"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B1 B2) B1

goal (1 subgoal):
 1. Eq (Geos (Lin (Li B1 B2)) add Emp) (Geos (Lin (Li C A)) add Emp) \<Longrightarrow> Line_on (Li C A) B1
[PROOF STEP]
by (simp add: Line_on_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li B1 B2)) add Emp) (Geos (Lin (Li C A)) add Emp) \<Longrightarrow> Line_on (Li C A) B1

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P18 P33
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li C A) B1
Eq (Geos (Lin (Li B1 B2)) add Emp) (Geos (Lin (Li C A)) add Emp) \<Longrightarrow> Line_on (Li C A) B1
[PROOF STEP]
have P34 : "\<not> Eq (Geos (Lin (Li B1 B2)) add Emp) (Geos (Lin (Li C A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li C A) B1
Eq (Geos (Lin (Li B1 B2)) add Emp) (Geos (Lin (Li C A)) add Emp) \<Longrightarrow> Line_on (Li C A) B1

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li B1 B2)) add Emp) (Geos (Lin (Li C A)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Lin (Li B1 B2)) add Emp) (Geos (Lin (Li C A)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P32 P34
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li C A) C
\<not> Eq (Geos (Lin (Li B1 B2)) add Emp) (Geos (Lin (Li C A)) add Emp)
[PROOF STEP]
have "Bet_Point (Se B1 B2) C \<Longrightarrow> Plane_diffside (Li C A) B1 B2"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li C A) C
\<not> Eq (Geos (Lin (Li B1 B2)) add Emp) (Geos (Lin (Li C A)) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se B1 B2) C \<Longrightarrow> Plane_diffside (Li C A) B1 B2
[PROOF STEP]
by (simp add:Plane_Bet_diffside)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se B1 B2) C \<Longrightarrow> Plane_diffside (Li C A) B1 B2

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se B1 B2) C \<Longrightarrow> Plane_diffside (Li C A) B1 B2
[PROOF STEP]
have P35 : "Bet_Point (Se B1 B2) C \<Longrightarrow> \<not> Plane_sameside (Li C A) B1 B2"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se B1 B2) C \<Longrightarrow> Plane_diffside (Li C A) B1 B2

goal (1 subgoal):
 1. Bet_Point (Se B1 B2) C \<Longrightarrow> \<not> Plane_sameside (Li C A) B1 B2
[PROOF STEP]
by (simp add:Plane_diffside_not_sameside)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se B1 B2) C \<Longrightarrow> \<not> Plane_sameside (Li C A) B1 B2

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P22 P31
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li C A) B1 B
Plane_sameside (Li C A) B B2
[PROOF STEP]
have P36 : "\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi B2) add Emp) \<Longrightarrow>
    Plane_sameside (Li C A) B1 B2"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li C A) B1 B
Plane_sameside (Li C A) B B2

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi B2) add Emp) \<Longrightarrow> Plane_sameside (Li C A) B1 B2
[PROOF STEP]
by (blast intro:Plane_sameside_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi B2) add Emp) \<Longrightarrow> Plane_sameside (Li C A) B1 B2

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P35 P36
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se B1 B2) C \<Longrightarrow> \<not> Plane_sameside (Li C A) B1 B2
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi B2) add Emp) \<Longrightarrow> Plane_sameside (Li C A) B1 B2
[PROOF STEP]
have P37 : "\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi B2) add Emp) \<Longrightarrow>
    \<not> Bet_Point (Se B1 B2) C"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se B1 B2) C \<Longrightarrow> \<not> Plane_sameside (Li C A) B1 B2
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi B2) add Emp) \<Longrightarrow> Plane_sameside (Li C A) B1 B2

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi B2) add Emp) \<Longrightarrow> \<not> Bet_Point (Se B1 B2) C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi B2) add Emp) \<Longrightarrow> \<not> Bet_Point (Se B1 B2) C

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P38 : "Eq (Geos (Poi B1) add Emp) (Geos (Poi B2) add Emp) \<Longrightarrow>
    Bet_Point (Se B1 B2) C \<Longrightarrow> Bet_Point (Se B2 B2) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Eq (Geos (Poi B1) add Emp) (Geos (Poi B2) add Emp); Bet_Point (Se B1 B2) C\<rbrakk> \<Longrightarrow> Bet_Point (Se B2 B2) C
[PROOF STEP]
by (simp add:Bet_Point_Eq)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Eq (Geos (Poi B1) add Emp) (Geos (Poi B2) add Emp); Bet_Point (Se B1 B2) C\<rbrakk> \<Longrightarrow> Bet_Point (Se B2 B2) C

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P39 : "\<not> Bet_Point (Se B2 B2) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se B2 B2) C
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se B2 B2) C

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P38 P39
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>Eq (Geos (Poi B1) add Emp) (Geos (Poi B2) add Emp); Bet_Point (Se B1 B2) C\<rbrakk> \<Longrightarrow> Bet_Point (Se B2 B2) C
\<not> Bet_Point (Se B2 B2) C
[PROOF STEP]
have P40 : "Eq (Geos (Poi B1) add Emp) (Geos (Poi B2) add Emp) \<Longrightarrow>
    \<not> Bet_Point (Se B1 B2) C"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Eq (Geos (Poi B1) add Emp) (Geos (Poi B2) add Emp); Bet_Point (Se B1 B2) C\<rbrakk> \<Longrightarrow> Bet_Point (Se B2 B2) C
\<not> Bet_Point (Se B2 B2) C

goal (1 subgoal):
 1. Eq (Geos (Poi B1) add Emp) (Geos (Poi B2) add Emp) \<Longrightarrow> \<not> Bet_Point (Se B1 B2) C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi B1) add Emp) (Geos (Poi B2) add Emp) \<Longrightarrow> \<not> Bet_Point (Se B1 B2) C

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P37 P40
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi B2) add Emp) \<Longrightarrow> \<not> Bet_Point (Se B1 B2) C
Eq (Geos (Poi B1) add Emp) (Geos (Poi B2) add Emp) \<Longrightarrow> \<not> Bet_Point (Se B1 B2) C
[PROOF STEP]
have P41 : "\<not> Bet_Point (Se B1 B2) C"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi B2) add Emp) \<Longrightarrow> \<not> Bet_Point (Se B1 B2) C
Eq (Geos (Poi B1) add Emp) (Geos (Poi B2) add Emp) \<Longrightarrow> \<not> Bet_Point (Se B1 B2) C

goal (1 subgoal):
 1. \<not> Bet_Point (Se B1 B2) C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se B1 B2) C

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P42 : "\<not> Bet_Point (Se A A) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se A A) C
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se A A) C

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P16 P19 P23 P26 P28 P41 P42
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
Def (Ang (An B1 C A))
Bet_Point (Se B A) B2 \<and> Line_on (Li C B1) B2 \<and> \<not> Line_on (Li C B1) B \<and> \<not> Line_on (Li C B1) A
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi B2) add Emp)
Line_on (Li C A) A
\<not> Bet_Point (Se B1 B2) C
\<not> Bet_Point (Se A A) C
[PROOF STEP]
have P43 :
    "Eq (Geos (Ang (An B1 C A)) add Emp) (Geos (Ang (An B2 C A)) add Emp) \<and> Def (Ang (An B2 C A))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
Def (Ang (An B1 C A))
Bet_Point (Se B A) B2 \<and> Line_on (Li C B1) B2 \<and> \<not> Line_on (Li C B1) B \<and> \<not> Line_on (Li C B1) A
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi B2) add Emp)
Line_on (Li C A) A
\<not> Bet_Point (Se B1 B2) C
\<not> Bet_Point (Se A A) C

goal (1 subgoal):
 1. Eq (Geos (Ang (An B1 C A)) add Emp) (Geos (Ang (An B2 C A)) add Emp) \<and> Def (Ang (An B2 C A))
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An B1 C A)) add Emp) (Geos (Ang (An B2 C A)) add Emp) \<and> Def (Ang (An B2 C A))

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P21 P43
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An B1 C A)) add Emp)
Eq (Geos (Ang (An B1 C A)) add Emp) (Geos (Ang (An B2 C A)) add Emp) \<and> Def (Ang (An B2 C A))
[PROOF STEP]
have P44 : "Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An B2 C A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An B1 C A)) add Emp)
Eq (Geos (Ang (An B1 C A)) add Emp) (Geos (Ang (An B2 C A)) add Emp) \<and> Def (Ang (An B2 C A))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An B2 C A)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An B2 C A)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P43
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An B1 C A)) add Emp) (Geos (Ang (An B2 C A)) add Emp) \<and> Def (Ang (An B2 C A))
[PROOF STEP]
have P45 : "Def (Tri (Tr A B2 C))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An B1 C A)) add Emp) (Geos (Ang (An B2 C A)) add Emp) \<and> Def (Ang (An B2 C A))

goal (1 subgoal):
 1. Def (Tri (Tr A B2 C))
[PROOF STEP]
by (blast intro:Ang_to_Tri Tri_def_rev Tri_def_trans)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr A B2 C))

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P27
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se A B) B2
[PROOF STEP]
have P46 : "Bet_Point (Se B A) B2"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se A B) B2

goal (1 subgoal):
 1. Bet_Point (Se B A) B2
[PROOF STEP]
by (simp add:Bet_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se B A) B2

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from N P46
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A
Bet_Point (Se B A) B2
[PROOF STEP]
have P47 : "Bet_Point (Se B2 D) A"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A
Bet_Point (Se B A) B2

goal (1 subgoal):
 1. Bet_Point (Se B2 D) A
[PROOF STEP]
by (blast intro:Bet_swap_134_234)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se B2 D) A

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P45 P47
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B2 C))
Bet_Point (Se B2 D) A
[PROOF STEP]
have P48 : "\<not> Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B2 C))
Bet_Point (Se B2 D) A

goal (1 subgoal):
 1. \<not> Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B2)) add Emp)
[PROOF STEP]
by (simp add:Ang_external_Gr_lemma1)
[PROOF STATE]
proof (state)
this:
\<not> Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B2)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P49 : "Cong (Geos (Ang (An B2 C A)) add Emp) (Geos (Ang (An A C B2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An B2 C A)) add Emp) (Geos (Ang (An A C B2)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An B2 C A)) add Emp) (Geos (Ang (An A C B2)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P43
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An B1 C A)) add Emp) (Geos (Ang (An B2 C A)) add Emp) \<and> Def (Ang (An B2 C A))
[PROOF STEP]
have P50 : "Def (Ang (An A C B2))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An B1 C A)) add Emp) (Geos (Ang (An B2 C A)) add Emp) \<and> Def (Ang (An B2 C A))

goal (1 subgoal):
 1. Def (Ang (An A C B2))
[PROOF STEP]
by (simp add:Ang_def_rev)
[PROOF STATE]
proof (state)
this:
Def (Ang (An A C B2))

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P10 P43 P44 P49 P50
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An C A D))
Eq (Geos (Ang (An B1 C A)) add Emp) (Geos (Ang (An B2 C A)) add Emp) \<and> Def (Ang (An B2 C A))
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An B2 C A)) add Emp)
Cong (Geos (Ang (An B2 C A)) add Emp) (Geos (Ang (An A C B2)) add Emp)
Def (Ang (An A C B2))
[PROOF STEP]
have P51 : "Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An C A D))
Eq (Geos (Ang (An B1 C A)) add Emp) (Geos (Ang (An B2 C A)) add Emp) \<and> Def (Ang (An B2 C A))
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An B2 C A)) add Emp)
Cong (Geos (Ang (An B2 C A)) add Emp) (Geos (Ang (An A C B2)) add Emp)
Def (Ang (An A C B2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B2)) add Emp)
[PROOF STEP]
by (blast intro:Ang_trans Ang_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B2)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P48 P51
[PROOF STATE]
proof (chain)
picking this:
\<not> Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B2)) add Emp)
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B2)) add Emp)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B2)) add Emp)
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B2)) add Emp)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem (in Congruence_Rule) Ang_external_Gr :
  assumes
    "Def (Tri (Tr A B C))"
    "Bet_Point (Se B D) A"
  shows
    "Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)"
    "Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) &&& Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)
 2. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A
[PROOF STEP]
have "\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi A) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi D) add Emp) (Geos (Poi A) add Emp)
[PROOF STEP]
by (simp add:Bet_Point_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi A) add Emp)

goal (2 subgoals):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)
 2. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi A) add Emp)
[PROOF STEP]
have P1 : "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi A) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)

goal (2 subgoals):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)
 2. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
have P2 : "Line_on (Li A D) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A D) A
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A D) A

goal (2 subgoals):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)
 2. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A
[PROOF STEP]
have P3 : "Line_on (Li A D) B"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A

goal (1 subgoal):
 1. Line_on (Li A D) B
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li A D) B

goal (2 subgoals):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)
 2. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
have P4 : "Line_on (Li A B) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A B) A
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A B) A

goal (2 subgoals):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)
 2. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
have P5 : "Line_on (Li A B) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A B) B
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A B) B

goal (2 subgoals):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)
 2. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A
[PROOF STEP]
have P6 : "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
[PROOF STEP]
by (simp add:Tri_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)

goal (2 subgoals):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)
 2. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from P2 P3 P4 P5 P6
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A D) A
Line_on (Li A D) B
Line_on (Li A B) A
Line_on (Li A B) B
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
[PROOF STEP]
have "Eq (Geos (Lin (Li A D)) add Emp) (Geos (Lin (Li A B)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A D) A
Line_on (Li A D) B
Line_on (Li A B) A
Line_on (Li A B) B
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Lin (Li A D)) add Emp) (Geos (Lin (Li A B)) add Emp)
[PROOF STEP]
by (simp add:Line_unique)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li A D)) add Emp) (Geos (Lin (Li A B)) add Emp)

goal (2 subgoals):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)
 2. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li A D)) add Emp) (Geos (Lin (Li A B)) add Emp)
[PROOF STEP]
have P7 : "Line_on (Li A D) C \<Longrightarrow> Line_on (Li A B) C"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li A D)) add Emp) (Geos (Lin (Li A B)) add Emp)

goal (1 subgoal):
 1. Line_on (Li A D) C \<Longrightarrow> Line_on (Li A B) C
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Line_on (Li A D) C \<Longrightarrow> Line_on (Li A B) C

goal (2 subgoals):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)
 2. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A
[PROOF STEP]
have P8 : "\<not> Line_on (Li A B) C"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A

goal (1 subgoal):
 1. \<not> Line_on (Li A B) C
[PROOF STEP]
by (simp add:Tri_def_Line)
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li A B) C

goal (2 subgoals):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)
 2. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from P7 P8
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A D) C \<Longrightarrow> Line_on (Li A B) C
\<not> Line_on (Li A B) C
[PROOF STEP]
have P9 : "\<not> Line_on (Li A D) C"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A D) C \<Longrightarrow> Line_on (Li A B) C
\<not> Line_on (Li A B) C

goal (1 subgoal):
 1. \<not> Line_on (Li A D) C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li A D) C

goal (2 subgoals):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)
 2. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from P1 P9
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)
\<not> Line_on (Li A D) C
[PROOF STEP]
have "Def (Ang (An A D C))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)
\<not> Line_on (Li A D) C

goal (1 subgoal):
 1. Def (Ang (An A D C))
[PROOF STEP]
by (simp add:Ang_sinple_def)
[PROOF STATE]
proof (state)
this:
Def (Ang (An A D C))

goal (2 subgoals):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)
 2. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A D C))
[PROOF STEP]
have P10 : "Def (Ang (An C A D))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A D C))

goal (1 subgoal):
 1. Def (Ang (An C A D))
[PROOF STEP]
by (blast intro:Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An C A D))

goal (2 subgoals):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)
 2. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A
[PROOF STEP]
have P11 : "Def (Ang (An A C B))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A

goal (1 subgoal):
 1. Def (Ang (An A C B))
[PROOF STEP]
by (simp add:Tri_to_Ang Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An A C B))

goal (2 subgoals):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)
 2. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from P10 P11
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An C A D))
Def (Ang (An A C B))
[PROOF STEP]
have P12 :
    "Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)
    \<or> Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)
    \<or> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An C A D))
Def (Ang (An A C B))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<or> Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<or> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp)
[PROOF STEP]
by (simp add:Ang_relation_case)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<or> Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<or> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp)

goal (2 subgoals):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)
 2. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A
[PROOF STEP]
have P13 : "\<not> Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A

goal (1 subgoal):
 1. \<not> Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)
[PROOF STEP]
by (simp add:Ang_external_Gr_lemma1)
[PROOF STATE]
proof (state)
this:
\<not> Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)

goal (2 subgoals):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)
 2. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A
[PROOF STEP]
have P14 : "\<not> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A

goal (1 subgoal):
 1. \<not> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp)
[PROOF STEP]
by (simp add:Ang_external_Gr_lemma2)
[PROOF STATE]
proof (state)
this:
\<not> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp)

goal (2 subgoals):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)
 2. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from P12 P13 P14
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<or> Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<or> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp)
\<not> Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)
\<not> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp)
[PROOF STEP]
show P15 : "Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<or> Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<or> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp)
\<not> Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)
\<not> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An C A D)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
have P16 : "Line_on (Li C A) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li C A) C
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li C A) C

goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
have P17 : "Line_on (Li C A) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li C A) A
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li C A) A

goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A
[PROOF STEP]
have P18 : "\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
[PROOF STEP]
by (simp add:Tri_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from P16 P17 P18
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li C A) C
Line_on (Li C A) A
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
[PROOF STEP]
have "\<exists>p. Bet_Point (Se C p) A \<and> Line_on (Li C A) p"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li C A) C
Line_on (Li C A) A
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)

goal (1 subgoal):
 1. \<exists>p. Bet_Point (Se C p) A \<and> Line_on (Li C A) p
[PROOF STEP]
by (simp add:Bet_extension)
[PROOF STATE]
proof (state)
this:
\<exists>p. Bet_Point (Se C p) A \<and> Line_on (Li C A) p

goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Bet_Point (Se C p) A \<and> Line_on (Li C A) p
[PROOF STEP]
obtain E :: Point where P19 : "Bet_Point (Se C E) A"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Bet_Point (Se C p) A \<and> Line_on (Li C A) p

goal (1 subgoal):
 1. (\<And>E. Bet_Point (Se C E) A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet_Point (Se C E) A

goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A
[PROOF STEP]
have P20 : "Bet_Point (Se D B) A"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A

goal (1 subgoal):
 1. Bet_Point (Se D B) A
[PROOF STEP]
by (simp add:Bet_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se D B) A

goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from P10 P19 P20
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An C A D))
Bet_Point (Se C E) A
Bet_Point (Se D B) A
[PROOF STEP]
have P21 : "Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An E A B)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An C A D))
Bet_Point (Se C E) A
Bet_Point (Se D B) A

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An E A B)) add Emp)
[PROOF STEP]
by (simp add:Ang_vertical)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An E A B)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
have P22 : "Eq (Geos (Ang (An E A B)) add Emp) (Geos (Ang (An B A E)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An E A B)) add Emp) (Geos (Ang (An B A E)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An E A B)) add Emp) (Geos (Ang (An B A E)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from P21 P22
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An E A B)) add Emp)
Eq (Geos (Ang (An E A B)) add Emp) (Geos (Ang (An B A E)) add Emp)
[PROOF STEP]
have P23 : "Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An B A E)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An E A B)) add Emp)
Eq (Geos (Ang (An E A B)) add Emp) (Geos (Ang (An B A E)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An B A E)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An B A E)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from P19
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se C E) A
[PROOF STEP]
have P24 : "Line_on (Li C E) A"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se C E) A

goal (1 subgoal):
 1. Line_on (Li C E) A
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li C E) A

goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
have P25 : "Line_on (Li C E) E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li C E) E
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li C E) E

goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from P19
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se C E) A
[PROOF STEP]
have P26 : "\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se C E) A

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp)
[PROOF STEP]
by (simp add:Bet_Point_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from P4 P24 P25 P26
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A B) A
Line_on (Li C E) A
Line_on (Li C E) E
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp)
[PROOF STEP]
have P27 : "Line_on (Li A B) E \<Longrightarrow>
    Eq (Geos (Lin (Li C E)) add Emp) (Geos (Lin (Li A B)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A B) A
Line_on (Li C E) A
Line_on (Li C E) E
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp)

goal (1 subgoal):
 1. Line_on (Li A B) E \<Longrightarrow> Eq (Geos (Lin (Li C E)) add Emp) (Geos (Lin (Li A B)) add Emp)
[PROOF STEP]
by (simp add:Line_unique)
[PROOF STATE]
proof (state)
this:
Line_on (Li A B) E \<Longrightarrow> Eq (Geos (Lin (Li C E)) add Emp) (Geos (Lin (Li A B)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
have P28 : "Line_on (Li C E) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li C E) C
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li C E) C

goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from P27 P28
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A B) E \<Longrightarrow> Eq (Geos (Lin (Li C E)) add Emp) (Geos (Lin (Li A B)) add Emp)
Line_on (Li C E) C
[PROOF STEP]
have P29 : "Line_on (Li A B) E \<Longrightarrow> Line_on (Li A B) C"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A B) E \<Longrightarrow> Eq (Geos (Lin (Li C E)) add Emp) (Geos (Lin (Li A B)) add Emp)
Line_on (Li C E) C

goal (1 subgoal):
 1. Line_on (Li A B) E \<Longrightarrow> Line_on (Li A B) C
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Line_on (Li A B) E \<Longrightarrow> Line_on (Li A B) C

goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from P8 P29
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li A B) C
Line_on (Li A B) E \<Longrightarrow> Line_on (Li A B) C
[PROOF STEP]
have P30 : "\<not> Line_on (Li A B) E"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li A B) C
Line_on (Li A B) E \<Longrightarrow> Line_on (Li A B) C

goal (1 subgoal):
 1. \<not> Line_on (Li A B) E
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li A B) E

goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from P6 P30
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Line_on (Li A B) E
[PROOF STEP]
have "Def (Ang (An A B E))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Line_on (Li A B) E

goal (1 subgoal):
 1. Def (Ang (An A B E))
[PROOF STEP]
by (simp add:Ang_sinple_def)
[PROOF STATE]
proof (state)
this:
Def (Ang (An A B E))

goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B E))
[PROOF STEP]
have P31 : "Def (Ang (An B A E))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B E))

goal (1 subgoal):
 1. Def (Ang (An B A E))
[PROOF STEP]
by (blast intro:Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An B A E))

goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from P11
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A C B))
[PROOF STEP]
have P32 : "Def (Tri (Tr A C B))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A C B))

goal (1 subgoal):
 1. Def (Tri (Tr A C B))
[PROOF STEP]
by (simp add:Ang_to_Tri)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr A C B))

goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from P19 P32
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se C E) A
Def (Tri (Tr A C B))
[PROOF STEP]
have P33 : "\<not> Cong (Geos (Ang (An B A E)) add Emp) (Geos (Ang (An A B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se C E) A
Def (Tri (Tr A C B))

goal (1 subgoal):
 1. \<not> Cong (Geos (Ang (An B A E)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
by (simp add:Ang_external_Gr_lemma1)
[PROOF STATE]
proof (state)
this:
\<not> Cong (Geos (Ang (An B A E)) add Emp) (Geos (Ang (An A B C)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from P19 P32
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se C E) A
Def (Tri (Tr A C B))
[PROOF STEP]
have P34 : "\<not> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An B A E)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se C E) A
Def (Tri (Tr A C B))

goal (1 subgoal):
 1. \<not> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An B A E)) add Emp)
[PROOF STEP]
by (simp add:Ang_external_Gr_lemma2)
[PROOF STATE]
proof (state)
this:
\<not> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An B A E)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A
[PROOF STEP]
have P35 : "Def (Ang (An A B C))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B D) A

goal (1 subgoal):
 1. Def (Ang (An A B C))
[PROOF STEP]
by (simp add:Tri_to_Ang)
[PROOF STATE]
proof (state)
this:
Def (Ang (An A B C))

goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from P31 P35
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An B A E))
Def (Ang (An A B C))
[PROOF STEP]
have P36 :
    "Cong (Geos (Ang (An B A E)) add Emp) (Geos (Ang (An A B C)) add Emp)
    \<or> Gr (Geos (Ang (An B A E)) add Emp) (Geos (Ang (An A B C)) add Emp)
    \<or> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An B A E)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An B A E))
Def (Ang (An A B C))

goal (1 subgoal):
 1. Cong (Geos (Ang (An B A E)) add Emp) (Geos (Ang (An A B C)) add Emp) \<or> Gr (Geos (Ang (An B A E)) add Emp) (Geos (Ang (An A B C)) add Emp) \<or> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An B A E)) add Emp)
[PROOF STEP]
by (simp add:Ang_relation_case)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An B A E)) add Emp) (Geos (Ang (An A B C)) add Emp) \<or> Gr (Geos (Ang (An B A E)) add Emp) (Geos (Ang (An A B C)) add Emp) \<or> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An B A E)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from P33 P34 P36
[PROOF STATE]
proof (chain)
picking this:
\<not> Cong (Geos (Ang (An B A E)) add Emp) (Geos (Ang (An A B C)) add Emp)
\<not> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An B A E)) add Emp)
Cong (Geos (Ang (An B A E)) add Emp) (Geos (Ang (An A B C)) add Emp) \<or> Gr (Geos (Ang (An B A E)) add Emp) (Geos (Ang (An A B C)) add Emp) \<or> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An B A E)) add Emp)
[PROOF STEP]
have P37 : "Gr (Geos (Ang (An B A E)) add Emp) (Geos (Ang (An A B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Cong (Geos (Ang (An B A E)) add Emp) (Geos (Ang (An A B C)) add Emp)
\<not> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An B A E)) add Emp)
Cong (Geos (Ang (An B A E)) add Emp) (Geos (Ang (An A B C)) add Emp) \<or> Gr (Geos (Ang (An B A E)) add Emp) (Geos (Ang (An A B C)) add Emp) \<or> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An B A E)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An B A E)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Gr (Geos (Ang (An B A E)) add Emp) (Geos (Ang (An A B C)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from P10 P23 P31 P35 P37
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An C A D))
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An B A E)) add Emp)
Def (Ang (An B A E))
Def (Ang (An A B C))
Gr (Geos (Ang (An B A E)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
show "Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An C A D))
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An B A E)) add Emp)
Def (Ang (An B A E))
Def (Ang (An A B C))
Gr (Geos (Ang (An B A E)) add Emp) (Geos (Ang (An A B C)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
by (blast intro:Ang_Gr_trans_Eq_Gr)
[PROOF STATE]
proof (state)
this:
Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Congruence_Rule) Seg_not_Eq_move :
  assumes
    "\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)"
    "\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B2) add Emp)"
    "\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B3) add Emp)"
    "Line_on l1 A2" "Line_on l1 B2" "Line_on l1 B3"
    "\<not> Bet_Point (Se B3 B2) A2"
    "Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B3)) add Emp)"
    "\<not> Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)"
  shows
    "Bet_Point (Se B2 A2) B3 \<and> \<not> Bet_Point (Se A2 B3) B2
    \<or> \<not> Bet_Point (Se B2 A2) B3 \<and> Bet_Point (Se A2 B3) B2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bet_Point (Se B2 A2) B3 \<and> \<not> Bet_Point (Se A2 B3) B2 \<or> \<not> Bet_Point (Se B2 A2) B3 \<and> Bet_Point (Se A2 B3) B2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Bet_Point (Se B2 A2) B3 \<and> \<not> Bet_Point (Se A2 B3) B2 \<or> \<not> Bet_Point (Se B2 A2) B3 \<and> Bet_Point (Se A2 B3) B2
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B2) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B3) add Emp)
Line_on l1 A2
Line_on l1 B2
Line_on l1 B3
\<not> Bet_Point (Se B3 B2) A2
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B3)) add Emp)
\<not> Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
[PROOF STEP]
have P1 : "Eq (Geos (Seg (Se A2 B2)) add Emp) (Geos (Seg (Se A2 B3)) add Emp) \<Longrightarrow>
    Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B2) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B3) add Emp)
Line_on l1 A2
Line_on l1 B2
Line_on l1 B3
\<not> Bet_Point (Se B3 B2) A2
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B3)) add Emp)
\<not> Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se A2 B2)) add Emp) (Geos (Seg (Se A2 B3)) add Emp) \<Longrightarrow> Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
[PROOF STEP]
by (blast intro:Eq_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se A2 B2)) add Emp) (Geos (Seg (Se A2 B3)) add Emp) \<Longrightarrow> Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se B2 A2) B3 \<and> \<not> Bet_Point (Se A2 B3) B2 \<or> \<not> Bet_Point (Se B2 A2) B3 \<and> Bet_Point (Se A2 B3) B2
[PROOF STEP]
from assms P1
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B2) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B3) add Emp)
Line_on l1 A2
Line_on l1 B2
Line_on l1 B3
\<not> Bet_Point (Se B3 B2) A2
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B3)) add Emp)
\<not> Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Eq (Geos (Seg (Se A2 B2)) add Emp) (Geos (Seg (Se A2 B3)) add Emp) \<Longrightarrow> Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
[PROOF STEP]
have "\<not> Eq (Geos (Seg (Se A2 B2)) add Emp) (Geos (Seg (Se A2 B3)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B2) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B3) add Emp)
Line_on l1 A2
Line_on l1 B2
Line_on l1 B3
\<not> Bet_Point (Se B3 B2) A2
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B3)) add Emp)
\<not> Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Eq (Geos (Seg (Se A2 B2)) add Emp) (Geos (Seg (Se A2 B3)) add Emp) \<Longrightarrow> Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se A2 B2)) add Emp) (Geos (Seg (Se A2 B3)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Seg (Se A2 B2)) add Emp) (Geos (Seg (Se A2 B3)) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se B2 A2) B3 \<and> \<not> Bet_Point (Se A2 B3) B2 \<or> \<not> Bet_Point (Se B2 A2) B3 \<and> Bet_Point (Se A2 B3) B2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Seg (Se A2 B2)) add Emp) (Geos (Seg (Se A2 B3)) add Emp)
[PROOF STEP]
have P2 : "\<not> Eq (Geos (Poi B2) add Emp) (Geos (Poi B3) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Seg (Se A2 B2)) add Emp) (Geos (Seg (Se A2 B3)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi B2) add Emp) (Geos (Poi B3) add Emp)
[PROOF STEP]
by (simp add:Seg_not_Eq_Point)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi B2) add Emp) (Geos (Poi B3) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se B2 A2) B3 \<and> \<not> Bet_Point (Se A2 B3) B2 \<or> \<not> Bet_Point (Se B2 A2) B3 \<and> Bet_Point (Se A2 B3) B2
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B2) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B3) add Emp)
Line_on l1 A2
Line_on l1 B2
Line_on l1 B3
\<not> Bet_Point (Se B3 B2) A2
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B3)) add Emp)
\<not> Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
[PROOF STEP]
have P3 : "\<not> Eq (Geos (Poi B3) add Emp) (Geos (Poi A2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B2) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B3) add Emp)
Line_on l1 A2
Line_on l1 B2
Line_on l1 B3
\<not> Bet_Point (Se B3 B2) A2
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B3)) add Emp)
\<not> Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi B3) add Emp) (Geos (Poi A2) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi B3) add Emp) (Geos (Poi A2) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se B2 A2) B3 \<and> \<not> Bet_Point (Se A2 B3) B2 \<or> \<not> Bet_Point (Se B2 A2) B3 \<and> Bet_Point (Se A2 B3) B2
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B2) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B3) add Emp)
Line_on l1 A2
Line_on l1 B2
Line_on l1 B3
\<not> Bet_Point (Se B3 B2) A2
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B3)) add Emp)
\<not> Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
[PROOF STEP]
have P4 : "Line_on l1 A2"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B2) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B3) add Emp)
Line_on l1 A2
Line_on l1 B2
Line_on l1 B3
\<not> Bet_Point (Se B3 B2) A2
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B3)) add Emp)
\<not> Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)

goal (1 subgoal):
 1. Line_on l1 A2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Line_on l1 A2

goal (1 subgoal):
 1. Bet_Point (Se B2 A2) B3 \<and> \<not> Bet_Point (Se A2 B3) B2 \<or> \<not> Bet_Point (Se B2 A2) B3 \<and> Bet_Point (Se A2 B3) B2
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B2) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B3) add Emp)
Line_on l1 A2
Line_on l1 B2
Line_on l1 B3
\<not> Bet_Point (Se B3 B2) A2
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B3)) add Emp)
\<not> Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
[PROOF STEP]
have P5 : "Line_on l1 B2"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B2) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B3) add Emp)
Line_on l1 A2
Line_on l1 B2
Line_on l1 B3
\<not> Bet_Point (Se B3 B2) A2
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B3)) add Emp)
\<not> Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)

goal (1 subgoal):
 1. Line_on l1 B2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Line_on l1 B2

goal (1 subgoal):
 1. Bet_Point (Se B2 A2) B3 \<and> \<not> Bet_Point (Se A2 B3) B2 \<or> \<not> Bet_Point (Se B2 A2) B3 \<and> Bet_Point (Se A2 B3) B2
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B2) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B3) add Emp)
Line_on l1 A2
Line_on l1 B2
Line_on l1 B3
\<not> Bet_Point (Se B3 B2) A2
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B3)) add Emp)
\<not> Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
[PROOF STEP]
have P6 : "Line_on l1 B3"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B2) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B3) add Emp)
Line_on l1 A2
Line_on l1 B2
Line_on l1 B3
\<not> Bet_Point (Se B3 B2) A2
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B3)) add Emp)
\<not> Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)

goal (1 subgoal):
 1. Line_on l1 B3
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Line_on l1 B3

goal (1 subgoal):
 1. Bet_Point (Se B2 A2) B3 \<and> \<not> Bet_Point (Se A2 B3) B2 \<or> \<not> Bet_Point (Se B2 A2) B3 \<and> Bet_Point (Se A2 B3) B2
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B2) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B3) add Emp)
Line_on l1 A2
Line_on l1 B2
Line_on l1 B3
\<not> Bet_Point (Se B3 B2) A2
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B3)) add Emp)
\<not> Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
[PROOF STEP]
have P7 : "\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B2) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B3) add Emp)
Line_on l1 A2
Line_on l1 B2
Line_on l1 B3
\<not> Bet_Point (Se B3 B2) A2
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B3)) add Emp)
\<not> Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B2) add Emp)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B2) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se B2 A2) B3 \<and> \<not> Bet_Point (Se A2 B3) B2 \<or> \<not> Bet_Point (Se B2 A2) B3 \<and> Bet_Point (Se A2 B3) B2
[PROOF STEP]
from P2 P3 P4 P5 P6 P7
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi B2) add Emp) (Geos (Poi B3) add Emp)
\<not> Eq (Geos (Poi B3) add Emp) (Geos (Poi A2) add Emp)
Line_on l1 A2
Line_on l1 B2
Line_on l1 B3
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B2) add Emp)
[PROOF STEP]
have "Bet_Point (Se A2 B3) B2 \<or> Bet_Point (Se B3 B2) A2 \<or> Bet_Point (Se B2 A2) B3"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi B2) add Emp) (Geos (Poi B3) add Emp)
\<not> Eq (Geos (Poi B3) add Emp) (Geos (Poi A2) add Emp)
Line_on l1 A2
Line_on l1 B2
Line_on l1 B3
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B2) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se A2 B3) B2 \<or> Bet_Point (Se B3 B2) A2 \<or> Bet_Point (Se B2 A2) B3
[PROOF STEP]
by (simp add:Bet_case)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A2 B3) B2 \<or> Bet_Point (Se B3 B2) A2 \<or> Bet_Point (Se B2 A2) B3

goal (1 subgoal):
 1. Bet_Point (Se B2 A2) B3 \<and> \<not> Bet_Point (Se A2 B3) B2 \<or> \<not> Bet_Point (Se B2 A2) B3 \<and> Bet_Point (Se A2 B3) B2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se A2 B3) B2 \<or> Bet_Point (Se B3 B2) A2 \<or> Bet_Point (Se B2 A2) B3
[PROOF STEP]
have P8 :
    "Bet_Point (Se A2 B3) B2 \<and> \<not> Bet_Point (Se B3 B2) A2 \<and> \<not> Bet_Point (Se B2 A2) B3
    \<or> \<not> Bet_Point (Se A2 B3) B2 \<and> Bet_Point (Se B3 B2) A2 \<and> \<not> Bet_Point (Se B2 A2) B3
    \<or> \<not> Bet_Point (Se A2 B3) B2 \<and> \<not> Bet_Point (Se B3 B2) A2 \<and> Bet_Point (Se B2 A2) B3"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se A2 B3) B2 \<or> Bet_Point (Se B3 B2) A2 \<or> Bet_Point (Se B2 A2) B3

goal (1 subgoal):
 1. Bet_Point (Se A2 B3) B2 \<and> \<not> Bet_Point (Se B3 B2) A2 \<and> \<not> Bet_Point (Se B2 A2) B3 \<or> \<not> Bet_Point (Se A2 B3) B2 \<and> Bet_Point (Se B3 B2) A2 \<and> \<not> Bet_Point (Se B2 A2) B3 \<or> \<not> Bet_Point (Se A2 B3) B2 \<and> \<not> Bet_Point (Se B3 B2) A2 \<and> Bet_Point (Se B2 A2) B3
[PROOF STEP]
by (simp add:Bet_case_fact)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A2 B3) B2 \<and> \<not> Bet_Point (Se B3 B2) A2 \<and> \<not> Bet_Point (Se B2 A2) B3 \<or> \<not> Bet_Point (Se A2 B3) B2 \<and> Bet_Point (Se B3 B2) A2 \<and> \<not> Bet_Point (Se B2 A2) B3 \<or> \<not> Bet_Point (Se A2 B3) B2 \<and> \<not> Bet_Point (Se B3 B2) A2 \<and> Bet_Point (Se B2 A2) B3

goal (1 subgoal):
 1. Bet_Point (Se B2 A2) B3 \<and> \<not> Bet_Point (Se A2 B3) B2 \<or> \<not> Bet_Point (Se B2 A2) B3 \<and> Bet_Point (Se A2 B3) B2
[PROOF STEP]
from assms P8
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B2) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B3) add Emp)
Line_on l1 A2
Line_on l1 B2
Line_on l1 B3
\<not> Bet_Point (Se B3 B2) A2
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B3)) add Emp)
\<not> Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Bet_Point (Se A2 B3) B2 \<and> \<not> Bet_Point (Se B3 B2) A2 \<and> \<not> Bet_Point (Se B2 A2) B3 \<or> \<not> Bet_Point (Se A2 B3) B2 \<and> Bet_Point (Se B3 B2) A2 \<and> \<not> Bet_Point (Se B2 A2) B3 \<or> \<not> Bet_Point (Se A2 B3) B2 \<and> \<not> Bet_Point (Se B3 B2) A2 \<and> Bet_Point (Se B2 A2) B3
[PROOF STEP]
show "Bet_Point (Se B2 A2) B3 \<and> \<not> Bet_Point (Se A2 B3) B2
    \<or> \<not> Bet_Point (Se B2 A2) B3 \<and> Bet_Point (Se A2 B3) B2"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B2) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B3) add Emp)
Line_on l1 A2
Line_on l1 B2
Line_on l1 B3
\<not> Bet_Point (Se B3 B2) A2
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B3)) add Emp)
\<not> Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Bet_Point (Se A2 B3) B2 \<and> \<not> Bet_Point (Se B3 B2) A2 \<and> \<not> Bet_Point (Se B2 A2) B3 \<or> \<not> Bet_Point (Se A2 B3) B2 \<and> Bet_Point (Se B3 B2) A2 \<and> \<not> Bet_Point (Se B2 A2) B3 \<or> \<not> Bet_Point (Se A2 B3) B2 \<and> \<not> Bet_Point (Se B3 B2) A2 \<and> Bet_Point (Se B2 A2) B3

goal (1 subgoal):
 1. Bet_Point (Se B2 A2) B3 \<and> \<not> Bet_Point (Se A2 B3) B2 \<or> \<not> Bet_Point (Se B2 A2) B3 \<and> Bet_Point (Se A2 B3) B2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet_Point (Se B2 A2) B3 \<and> \<not> Bet_Point (Se A2 B3) B2 \<or> \<not> Bet_Point (Se B2 A2) B3 \<and> Bet_Point (Se A2 B3) B2

goal:
No subgoals!
[PROOF STEP]
qed