[STATEMENT]
lemma (in Congruence_Rule) Tri_Seg_diagonal :
  assumes
    "Def (Tri (Tr A B C))"
    "Bet_Point (Se B C) D"
    "Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C D)) add Emp)"
  shows
    "Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An A B C)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Gr (Geos (Ang (An B A C)) 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 C) D
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C D)) add Emp)
[PROOF STEP]
have P1 : "\<not> Line_on (Li A B) C"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B C) D
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C D)) add Emp)

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 B A C)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
have "Line_on (Li A C) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A C) C
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A C) C

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

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

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

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An B A C)) 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 C) D
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C D)) add Emp)
[PROOF STEP]
have P4 : "\<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 C) D
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C D)) add Emp)

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 B A C)) 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 C) D
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C D)) add Emp)
[PROOF STEP]
have "\<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 C) D
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C D)) add Emp)

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 B A C)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
[PROOF STEP]
have P5 : "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from P6 P7 P8
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An B A C) D
Plane_sameside (Li A C) D B
Cong (Geos (Ang (An D A C)) add Emp) (Geos (Ang (An D A C)) add Emp)
[PROOF STEP]
have P9 : "Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An D A C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An B A C) D
Plane_sameside (Li A C) D B
Cong (Geos (Ang (An D A C)) add Emp) (Geos (Ang (An D A C)) add Emp)

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An B A C)) 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 C) D
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C D)) add Emp)
[PROOF STEP]
have P10 : "\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi D) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B C) D
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C D)) add Emp)

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An B A C)) 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 C) D
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C D)) add Emp)
[PROOF STEP]
have P11 : "Line_on (Li C B) D"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B C) D
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C D)) add Emp)

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An B A C)) 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 C) D
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C D)) add Emp)
[PROOF STEP]
have P12 : "Def (Tri (Tr A C B))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B C) D
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C D)) add Emp)

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

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

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

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

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
have P14 : "Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C A)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C A)) add Emp)
[PROOF STEP]
by (simp add:Seg_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C A)) add Emp)

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

goal (1 subgoal):
 1. Eq (Geos (Seg (Se C A)) add Emp) (Geos (Seg (Se C D)) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev Eq_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se C A)) add Emp) (Geos (Seg (Se C D)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from P13 P15
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr C A D))
Eq (Geos (Seg (Se C A)) add Emp) (Geos (Seg (Se C D)) add Emp)
[PROOF STEP]
have P16 : "Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An C D A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr C A D))
Eq (Geos (Seg (Se C A)) add Emp) (Geos (Seg (Se C D)) add Emp)

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An B A C)) 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 C) D
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C D)) add Emp)
[PROOF STEP]
have "\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi B) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B C) D
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C D)) add Emp)

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An B A C)) 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 B) add Emp)
[PROOF STEP]
have P17 : "\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi B) add Emp)

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An B A C)) 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 C) D
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C D)) add Emp)
[PROOF STEP]
have P18 : "Line_on (Li B C) D"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B C) D
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C D)) add Emp)

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

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

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

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

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

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

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An B A C)) 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 C) D
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C D)) add Emp)
[PROOF STEP]
have P21 : "Def (Ang (An A B C))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B C) D
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C D)) add Emp)

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 B A C)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
have P22 : "Line_on (Li B A) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B A) A
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B A) A

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An B A C)) 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 C) D
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C D)) add Emp)
[PROOF STEP]
have P24 : "Line_on (Li B C) D"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B C) D
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C D)) add Emp)

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An B A C)) 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 C) D
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C D)) add Emp)
[PROOF STEP]
have "Inv (Bet_Point (Se C D) B)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B C) D
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C D)) add Emp)

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

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

goal (1 subgoal):
 1. \<not> Bet_Point (Se C D) B
[PROOF STEP]
by (simp add:Inv_def)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se C D) B

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

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from P17 P21 P22 P23 P24 P25 P26
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
Def (Ang (An A B C))
Line_on (Li B A) A
\<not> Bet_Point (Se A A) B
Line_on (Li B C) D
\<not> Bet_Point (Se C D) B
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)
[PROOF STEP]
have P27 :
      "Eq (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A B D)) add Emp) \<and> Def (Ang (An A B D))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
Def (Ang (An A B C))
Line_on (Li B A) A
\<not> Bet_Point (Se A A) B
Line_on (Li B C) D
\<not> Bet_Point (Se C D) B
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)

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

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

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

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

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

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A D C)) 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 A D C)) add Emp)

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

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

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

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

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

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from P20 P31 P32 P33 P34
[PROOF STATE]
proof (chain)
picking this:
Gr (Geos (Ang (An A D C)) add Emp) (Geos (Ang (An D B A)) add Emp)
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A D C)) add Emp)
Def (Ang (An C A D))
Def (Ang (An A D C))
Def (Ang (An D B A))
[PROOF STEP]
have P35 : "Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An D B A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Gr (Geos (Ang (An A D C)) add Emp) (Geos (Ang (An D B A)) add Emp)
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A D C)) add Emp)
Def (Ang (An C A D))
Def (Ang (An A D C))
Def (Ang (An D B A))

goal (1 subgoal):
 1. Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An D B A)) 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 D B A)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from P21 P29 P32 P34 P35
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An D B A)) add Emp)
Def (Ang (An C A D))
Def (Ang (An D B A))
Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An D B A)) add Emp)
[PROOF STEP]
have P36 : "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 A B C))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An D B A)) add Emp)
Def (Ang (An C A D))
Def (Ang (An D B A))
Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An D B 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]
by (blast intro:Ang_Gr_trans_Gr_Eq Ang_rev)
[PROOF STATE]
proof (state)
this:
Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)

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

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

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An B A C)) 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 C) D
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C D)) add Emp)
[PROOF STEP]
have P39 : "Def (Ang (An B A C))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se B C) D
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C D)) add Emp)

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from P9 P32 P37 P38 P39
[PROOF STATE]
proof (chain)
picking this:
Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An D A C)) add Emp)
Def (Ang (An C A D))
Cong (Geos (Ang (An D A C)) add Emp) (Geos (Ang (An C A D)) add Emp)
Def (Ang (An D A C))
Def (Ang (An B A C))
[PROOF STEP]
have P40 : "Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An C A D)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An D A C)) add Emp)
Def (Ang (An C A D))
Cong (Geos (Ang (An D A C)) add Emp) (Geos (Ang (An C A D)) add Emp)
Def (Ang (An D A C))
Def (Ang (An B A C))

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
from P21 P32 P36 P39 P40
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An C A D))
Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
Def (Ang (An B A C))
Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An C A D)) add Emp)
[PROOF STEP]
show "Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An A B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An C A D))
Gr (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A B C)) add Emp)
Def (Ang (An B A C))
Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An C A D)) add Emp)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Congruence_Rule) Tri_Bet_Ang_Gr :
  assumes
    "Def (Tri (Tr A B C))"
    "Bet_Point (Se A C) D"
    "Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)"
  shows
    "Gr (Geos (Ang (An A D B)) add Emp) (Geos (Ang (An A B D)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gr (Geos (Ang (An A D B)) add Emp) (Geos (Ang (An A B D)) add Emp)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Gr (Geos (Ang (An A D B)) add Emp) (Geos (Ang (An A B D)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Bet_Point (Se A C) D
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)
[PROOF STEP]
have P1 : "Cong (Geos (Ang (An A B C)) 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 A C) D
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> Bet_Point (Se D A) C
[PROOF STEP]
by (simp add:Inv_def)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se D A) C

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

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

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
[PROOF STEP]
by (simp add:Bet_Point_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 D B)) add Emp) (Geos (Ang (An A B D)) add Emp)
[PROOF STEP]
from P5
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr D C B))
[PROOF STEP]
have P14 : "\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi B) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr D C B))

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An A D B)) add Emp) (Geos (Ang (An A B D)) add Emp)
[PROOF STEP]
from P8 P9 P10 P11 P12 P13 P14
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An D C B))
Line_on (Li C D) A
\<not> Bet_Point (Se D A) C
Line_on (Li C B) B
\<not> Bet_Point (Se B B) C
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi B) add Emp)
[PROOF STEP]
have P15 : "Eq (Geos (Ang (An D C B)) add Emp) (Geos (Ang (An A C B)) add Emp)
    \<and> Def (Ang (An A C B))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An D C B))
Line_on (Li C D) A
\<not> Bet_Point (Se D A) C
Line_on (Li C B) B
\<not> Bet_Point (Se B B) C
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi B) add Emp)

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An A D B)) add Emp) (Geos (Ang (An A B D)) add Emp)
[PROOF STEP]
from P1 P15
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp)
Eq (Geos (Ang (An D C B)) add Emp) (Geos (Ang (An A C B)) add Emp) \<and> Def (Ang (An A C B))
[PROOF STEP]
have P16 : "Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An D C B)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp)
Eq (Geos (Ang (An D C B)) add Emp) (Geos (Ang (An A C B)) add Emp) \<and> Def (Ang (An A C B))

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

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An A D B)) add Emp) (Geos (Ang (An A B D)) add Emp)
[PROOF STEP]
from P2
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr B C A))
[PROOF STEP]
have P18 : "Def (Tri (Tr B A C))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr B C 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 D B)) add Emp) (Geos (Ang (An A B D)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Bet_Point (Se A C) D
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)
[PROOF STEP]
have P19 : "Line_on (Li A C) D"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Bet_Point (Se A C) D
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)

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

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)
[PROOF STEP]
by (simp add:Bet_Point_def)
[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 D B)) add Emp) (Geos (Ang (An A B D)) add Emp)
[PROOF STEP]
from P18 P19 P20
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr B A C))
Line_on (Li A C) D
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)
[PROOF STEP]
have "Def (Tri (Tr B A D))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr B A C))
Line_on (Li A C) D
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)

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

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

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

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

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

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

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

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

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 A D B)) add Emp) (Geos (Ang (An A B D)) add Emp)
[PROOF STEP]
from P8 P16 P22 P23 P24
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An D C B))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An D C B)) add Emp)
Def (Ang (An A D B))
Gr (Geos (Ang (An A D B)) add Emp) (Geos (Ang (An D C B)) add Emp)
Def (Ang (An A B C))
[PROOF STEP]
have P25 : "Gr (Geos (Ang (An A D B)) add Emp) (Geos (Ang (An A B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An D C B))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An D C B)) add Emp)
Def (Ang (An A D B))
Gr (Geos (Ang (An A D B)) add Emp) (Geos (Ang (An D C B)) add Emp)
Def (Ang (An A B C))

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

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

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

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

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An A D B)) add Emp) (Geos (Ang (An A B D)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Bet_Point (Se A C) D
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)
[PROOF STEP]
have "\<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 A C) D
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)

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 D B)) add Emp) (Geos (Ang (An A B D)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
[PROOF STEP]
have P27 : "\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An A D B)) add Emp) (Geos (Ang (An A B D)) add Emp)
[PROOF STEP]
from P29 P30 P31
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An C B A) D
Plane_sameside (Li B A) D C
Cong (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An D B A)) add Emp)
[PROOF STEP]
have P32 : "Gr (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An D B A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An C B A) D
Plane_sameside (Li B A) D C
Cong (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An D B A)) add Emp)

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

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

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

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

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

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An A D B)) add Emp) (Geos (Ang (An A B D)) add Emp)
[PROOF STEP]
from P24 P32 P33 P34 P35
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Gr (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An D B A)) add Emp)
Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An A B C)) add Emp)
Def (Ang (An C B A))
Def (Ang (An D B A))
[PROOF STEP]
have P36 : "Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An D B A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Gr (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An D B A)) add Emp)
Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An A B C)) add Emp)
Def (Ang (An C B A))
Def (Ang (An D B A))

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

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

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

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An A D B)) add Emp) (Geos (Ang (An A B D)) add Emp)
[PROOF STEP]
from P24 P35 P36 P37 P38
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An D B A))
Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An D B A)) add Emp)
Cong (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An A B D)) add Emp)
Def (Ang (An A B D))
[PROOF STEP]
have P39 : "Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A B D)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An D B A))
Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An D B A)) add Emp)
Cong (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An A B D)) add Emp)
Def (Ang (An A B D))

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An A D B)) add Emp) (Geos (Ang (An A B D)) add Emp)
[PROOF STEP]
from P22 P24 P25 P38 P39
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A D B))
Def (Ang (An A B C))
Gr (Geos (Ang (An A D B)) add Emp) (Geos (Ang (An A B C)) add Emp)
Def (Ang (An A B D))
Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A B D)) add Emp)
[PROOF STEP]
show "Gr (Geos (Ang (An A D B)) add Emp) (Geos (Ang (An A B D)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A D B))
Def (Ang (An A B C))
Gr (Geos (Ang (An A D B)) add Emp) (Geos (Ang (An A B C)) add Emp)
Def (Ang (An A B D))
Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A B D)) add Emp)

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

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P1 : "Line_on (Li A C) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A C) A
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A C) A

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

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

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. \<not> Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from N
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp)
[PROOF STEP]
have "\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp)

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. \<not> Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
[PROOF STEP]
have P4 : "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P1 P2 P3 P4
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A C) A
Line_on (Li A C) C
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
have "\<exists>p. Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A p)) add Emp)
    \<and> \<not> Bet_Point (Se p C) A \<and> Line_on (Li A C) p \<and> \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi p) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A C) A
Line_on (Li A C) C
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)

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

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

goal (1 subgoal):
 1. (\<And>D. Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A D)) add Emp) \<and> \<not> Bet_Point (Se D C) A \<and> Line_on (Li A C) D \<and> \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A D)) add Emp) \<and> \<not> Bet_Point (Se D C) A \<and> Line_on (Li A C) D \<and> \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from W P1 P2 P3 P4 P5
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)
Line_on (Li A C) A
Line_on (Li A C) C
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A D)) add Emp) \<and> \<not> Bet_Point (Se D C) A \<and> Line_on (Li A C) D \<and> \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)
[PROOF STEP]
have P6 : "Bet_Point (Se C A) D \<and> \<not> Bet_Point (Se A D) C
    \<or> \<not> Bet_Point (Se C A) D \<and> Bet_Point (Se A D) C"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)
Line_on (Li A C) A
Line_on (Li A C) C
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A D)) add Emp) \<and> \<not> Bet_Point (Se D C) A \<and> Line_on (Li A C) D \<and> \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se C A) D \<and> \<not> Bet_Point (Se A D) C \<or> \<not> Bet_Point (Se C A) D \<and> Bet_Point (Se A D) C
[PROOF STEP]
by (simp add:Seg_not_Eq_move)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se C A) D \<and> \<not> Bet_Point (Se A D) C \<or> \<not> Bet_Point (Se C A) D \<and> Bet_Point (Se A D) C

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

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P8 : "Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se B A)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se B A)) add Emp)
[PROOF STEP]
by (simp add:Seg_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se B A)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P5 P8
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A D)) add Emp) \<and> \<not> Bet_Point (Se D C) A \<and> Line_on (Li A C) D \<and> \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se B A)) add Emp)
[PROOF STEP]
have P9 : "Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se A D)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A D)) add Emp) \<and> \<not> Bet_Point (Se D C) A \<and> Line_on (Li A C) D \<and> \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se B A)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se A D)) add Emp)
[PROOF STEP]
by (blast intro:Eq_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se A D)) add Emp)

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

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

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

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

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. \<not> Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
[PROOF STEP]
have P13 : "Def (Ang (An C B A))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P12 P14 P15 P16 P17
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An B C A))
Bet_Point (Se C A) D \<Longrightarrow> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An B C A)) add Emp)
Def (Ang (An A C B))
Cong (Geos (Ang (An B C A)) add Emp) (Geos (Ang (An A C B)) add Emp)
[PROOF STEP]
have P18 : "Bet_Point (Se C A) D \<Longrightarrow>
    Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An B C A))
Bet_Point (Se C A) D \<Longrightarrow> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An B C A)) add Emp)
Def (Ang (An A C B))
Cong (Geos (Ang (An B C A)) add Emp) (Geos (Ang (An A C B)) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se C A) D \<Longrightarrow> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp)
[PROOF STEP]
by (blast intro:Ang_Gr_trans_Gr_Eq Ang_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se C A) D \<Longrightarrow> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P12 P16
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A C B))
[PROOF STEP]
have P19 : "Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp)
    \<and> \<not> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp)
    \<and> \<not> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An A B C)) add Emp)
    \<or> \<not> Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp)
    \<and> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp)
    \<and> \<not> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An A B C)) add Emp)
    \<or> \<not> Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp)
    \<and> \<not> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp)
    \<and> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An A B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A C B))

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P18 P19
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se C A) D \<Longrightarrow> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp)
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp) \<and> \<not> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp) \<and> \<not> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An A B C)) add Emp) \<or> \<not> Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp) \<and> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp) \<and> \<not> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An A B C)) add Emp) \<or> \<not> Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp) \<and> \<not> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp) \<and> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
have P20 : "Bet_Point (Se C A) D \<Longrightarrow>
    \<not> Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se C A) D \<Longrightarrow> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp)
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp) \<and> \<not> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp) \<and> \<not> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An A B C)) add Emp) \<or> \<not> Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp) \<and> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp) \<and> \<not> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An A B C)) add Emp) \<or> \<not> Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp) \<and> \<not> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp) \<and> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An A B C)) add Emp)

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

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

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. \<not> Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P5 P21
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A D)) add Emp) \<and> \<not> Bet_Point (Se D C) A \<and> Line_on (Li A C) D \<and> \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)
Def (Tri (Tr B A C))
[PROOF STEP]
have "Def (Tri (Tr B A D))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A D)) add Emp) \<and> \<not> Bet_Point (Se D C) A \<and> Line_on (Li A C) D \<and> \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)
Def (Tri (Tr B A C))

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr B A D))
[PROOF STEP]
have P22 : "Def (Tri (Tr A B D))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr B A D))

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

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

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P19 P23
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp) \<and> \<not> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp) \<and> \<not> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An A B C)) add Emp) \<or> \<not> Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp) \<and> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp) \<and> \<not> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An A B C)) add Emp) \<or> \<not> Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp) \<and> \<not> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp) \<and> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An A B C)) add Emp)
Bet_Point (Se A D) C \<Longrightarrow> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
have P24 : "Bet_Point (Se A D) C \<Longrightarrow>
    \<not> Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp) \<and> \<not> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp) \<and> \<not> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An A B C)) add Emp) \<or> \<not> Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp) \<and> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp) \<and> \<not> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An A B C)) add Emp) \<or> \<not> Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp) \<and> \<not> Gr (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp) \<and> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An A B C)) add Emp)
Bet_Point (Se A D) C \<Longrightarrow> Gr (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An A B C)) add Emp)

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from assms P6 P20 P24
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp)
Bet_Point (Se C A) D \<and> \<not> Bet_Point (Se A D) C \<or> \<not> Bet_Point (Se C A) D \<and> Bet_Point (Se A D) C
Bet_Point (Se C A) D \<Longrightarrow> \<not> Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp)
Bet_Point (Se A D) C \<Longrightarrow> \<not> Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp)
Bet_Point (Se C A) D \<and> \<not> Bet_Point (Se A D) C \<or> \<not> Bet_Point (Se C A) D \<and> Bet_Point (Se A D) C
Bet_Point (Se C A) D \<Longrightarrow> \<not> Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp)
Bet_Point (Se A D) C \<Longrightarrow> \<not> Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp)

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

goal:
No subgoals!
[PROOF STEP]
qed