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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se C B)) add Emp) (Geos (Seg (Se A p)) add Emp) \<and> \<not> Bet_Point (Se p D) A \<and> Line_on (Li B D) 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 C B)) add Emp) (Geos (Seg (Se A p)) add Emp) \<and> \<not> Bet_Point (Se p D) A \<and> Line_on (Li B D) p \<and> \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi p) add Emp)

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

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P7 : "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. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) 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 : "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. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P9 : "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. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P10 : "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. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) 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 P11 : "\<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. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P7 P8 P9 P10 P11
[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. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) 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 P12 : "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. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) 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 P13 : "\<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. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P12 P13
[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 P14 : "\<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. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P3 P14
[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. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A D C))
[PROOF STEP]
have P15 : "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. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P16 : "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. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P17 : "\<not> Bet_Point (Se C C) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se C C) A
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se C C) A

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> Bet_Point (Se D D1) A
[PROOF STEP]
by (blast intro:Bet_rev)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se D D1) A

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) 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 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. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) 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 P22 : "\<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. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P6 P15 P16 P17 P20 P21 P22
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se C B)) add Emp) (Geos (Seg (Se A D1)) add Emp) \<and> \<not> Bet_Point (Se D1 D) A \<and> Line_on (Li B D) D1 \<and> \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D1) add Emp)
Def (Ang (An C A D))
Line_on (Li A C) C
\<not> Bet_Point (Se C C) A
Line_on (Li A D) D1
\<not> Bet_Point (Se D D1) A
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
have P23 :
    "Eq (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An C A D1)) add Emp)
    \<and> Def (Ang (An C A D1))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se C B)) add Emp) (Geos (Seg (Se A D1)) add Emp) \<and> \<not> Bet_Point (Se D1 D) A \<and> Line_on (Li B D) D1 \<and> \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D1) add Emp)
Def (Ang (An C A D))
Line_on (Li A C) C
\<not> Bet_Point (Se C C) A
Line_on (Li A D) D1
\<not> Bet_Point (Se D D1) A
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)

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

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

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

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

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

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) 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 P27 : "Def (Tri (Tr 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. Def (Tri (Tr C A B))
[PROOF STEP]
by (blast intro:Ang_to_Tri Tri_def_rev Tri_def_trans)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr C A B))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P28 : "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. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P6
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se C B)) add Emp) (Geos (Seg (Se A D1)) add Emp) \<and> \<not> Bet_Point (Se D1 D) A \<and> Line_on (Li B D) D1 \<and> \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D1) add Emp)
[PROOF STEP]
have P29 : "Eq (Geos (Seg (Se A D1)) add Emp) (Geos (Seg (Se C B)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se C B)) add Emp) (Geos (Seg (Se A D1)) add Emp) \<and> \<not> Bet_Point (Se D1 D) A \<and> Line_on (Li B D) D1 \<and> \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D1) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se A D1)) add Emp) (Geos (Seg (Se C B)) add Emp)
[PROOF STEP]
by (simp add:Eq_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se A D1)) add Emp) (Geos (Seg (Se C B)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D1)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> Cong (Geos (Tri (Tr A C D1)) add Emp) (Geos (Tri (Tr C A B)) add Emp)
[PROOF STEP]
by (simp add:Tri_SAS)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An C A D1)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> Cong (Geos (Tri (Tr A C D1)) add Emp) (Geos (Tri (Tr C A B)) add Emp)

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

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) 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 P30 : "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. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from W P15 P23 P25 P30
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)
Def (Ang (An C A D))
Eq (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An C A D1)) add Emp) \<and> Def (Ang (An C A D1))
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An C A D1)) add Emp)
Def (Ang (An A C B))
[PROOF STEP]
have P31 : "Cong (Geos (Ang (An C A D1)) 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)
Def (Ang (An C A D))
Eq (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An C A D1)) add Emp) \<and> Def (Ang (An C A D1))
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An C A D1)) add Emp)
Def (Ang (An A C B))

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P29 P31
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C A D1)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An D1 C A)) add Emp) (Geos (Ang (An B A C)) add Emp)
Cong (Geos (Ang (An C A D1)) add Emp) (Geos (Ang (An A C B)) add Emp)
[PROOF STEP]
have P32 : "Cong (Geos (Ang (An D1 C A)) add Emp) (Geos (Ang (An B A C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C A D1)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An D1 C A)) add Emp) (Geos (Ang (An B A C)) add Emp)
Cong (Geos (Ang (An C A D1)) add Emp) (Geos (Ang (An A C B)) add Emp)

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P15
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An C A D))
[PROOF STEP]
have P37 : "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. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P38 : "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. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P30
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A C B))
[PROOF STEP]
have P39 : "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. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from W P15 P30 P36 P37 P38
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp)
Def (Ang (An C A D))
Def (Ang (An A C B))
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An D A C)) add Emp)
Def (Ang (An D A C))
Cong (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An B C A)) add Emp)
[PROOF STEP]
have P40 : "Cong (Geos (Ang (An D A C)) 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)
Def (Ang (An C A D))
Def (Ang (An A C B))
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An D A C)) add Emp)
Def (Ang (An D A C))
Cong (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An B C A)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P30 P37 P38 P39 P40
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A C B))
Def (Ang (An D A C))
Cong (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An B C A)) add Emp)
Def (Ang (An B C A))
Cong (Geos (Ang (An D A C)) add Emp) (Geos (Ang (An A C B)) add Emp)
[PROOF STEP]
have P41 : "Cong (Geos (Ang (An D A C)) add Emp) (Geos (Ang (An B C A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A C B))
Def (Ang (An D A C))
Cong (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An B C A)) add Emp)
Def (Ang (An B C A))
Cong (Geos (Ang (An D A C)) add Emp) (Geos (Ang (An A C B)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) 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 P42 : "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. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P35 P37 P39 P41 P42
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se B E) C \<and> Line_on (Li B C) E
Def (Ang (An D A C))
Def (Ang (An B C A))
Cong (Geos (Ang (An D A C)) add Emp) (Geos (Ang (An B C A)) add Emp)
Bet_Point (Se D B) A
[PROOF STEP]
have P43 : "Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An A C E)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se B E) C \<and> Line_on (Li B C) E
Def (Ang (An D A C))
Def (Ang (An B C A))
Cong (Geos (Ang (An D A C)) add Emp) (Geos (Ang (An B C A)) add Emp)
Bet_Point (Se D B) A

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P32 P44 P45 P46 P47
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An D1 C A)) add Emp) (Geos (Ang (An B A C)) add Emp)
Cong (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An C A B)) add Emp)
Def (Ang (An B A C))
Def (Ang (An C A B))
Def (Ang (An D1 C A))
[PROOF STEP]
have P48 : "Cong (Geos (Ang (An D1 C A)) add Emp) (Geos (Ang (An C A B)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An D1 C A)) add Emp) (Geos (Ang (An B A C)) add Emp)
Cong (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An C A B)) add Emp)
Def (Ang (An B A C))
Def (Ang (An C A B))
Def (Ang (An D1 C A))

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

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

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

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

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

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

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P16 P34 P50 P51
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A C) C
Line_on (Li B C) C
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi C) add Emp)
Line_on (Li B C) E
[PROOF STEP]
have P52 : "Line_on (Li A C) E \<Longrightarrow>
    Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li A C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A C) C
Line_on (Li B C) C
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi C) add Emp)
Line_on (Li B C) E

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P43 P46 P47 P48 P56
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An A C E)) add Emp)
Def (Ang (An C A B))
Def (Ang (An D1 C A))
Cong (Geos (Ang (An D1 C A)) add Emp) (Geos (Ang (An C A B)) add Emp)
Def (Ang (An A C E))
[PROOF STEP]
have P57 : "Cong (Geos (Ang (An D1 C A)) add Emp) (Geos (Ang (An A C E)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An A C E)) add Emp)
Def (Ang (An C A B))
Def (Ang (An D1 C A))
Cong (Geos (Ang (An D1 C A)) add Emp) (Geos (Ang (An C A B)) add Emp)
Def (Ang (An A C E))

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

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

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

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

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B D) B
[PROOF STEP]
have P61 : "Eq (Geos (Lin (Li B D)) 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 B D) B

goal (1 subgoal):
 1. Eq (Geos (Lin (Li B D)) 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 B D)) add Emp) (Geos (Lin (Li C A)) add Emp) \<Longrightarrow> Line_on (Li C A) B

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) 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 P62 : "\<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. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P61 P62
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li B D)) add Emp) (Geos (Lin (Li C A)) add Emp) \<Longrightarrow> Line_on (Li C A) B
\<not> Line_on (Li C A) B
[PROOF STEP]
have P63 : "\<not> Eq (Geos (Lin (Li B D)) add Emp) (Geos (Lin (Li C A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li B D)) add Emp) (Geos (Lin (Li C A)) add Emp) \<Longrightarrow> Line_on (Li C A) B
\<not> Line_on (Li C A) B

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P1 P2 P3 P66 P67
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B D) A
Line_on (Li B D) D
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)
Line_on (Li B D) D1
\<not> Eq (Geos (Poi D1) add Emp) (Geos (Poi A) add Emp)
[PROOF STEP]
have P68 : "\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi D1) add Emp) \<Longrightarrow>
    Bet_Point (Se D A) D1 \<or> Bet_Point (Se A D1) D \<or> Bet_Point (Se D1 D) A"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B D) A
Line_on (Li B D) D
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)
Line_on (Li B D) D1
\<not> Eq (Geos (Poi D1) add Emp) (Geos (Poi A) add Emp)

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

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

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

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

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P60 P70
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li C A) A
\<not> Eq (Geos (Lin (Li A D)) add Emp) (Geos (Lin (Li C A)) add Emp)
[PROOF STEP]
have P71 : "Bet_Point (Se A D) D1 \<Longrightarrow> Plane_sameside (Li C A) D D1"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li C A) A
\<not> Eq (Geos (Lin (Li A D)) add Emp) (Geos (Lin (Li C A)) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se A D) D1 \<Longrightarrow> Plane_sameside (Li C A) D D1
[PROOF STEP]
by (simp add:Plane_Bet_sameside Plane_sameside_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A D) D1 \<Longrightarrow> Plane_sameside (Li C A) D D1

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P60 P74
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li C A) A
\<not> Eq (Geos (Lin (Li A D1)) add Emp) (Geos (Lin (Li C A)) add Emp)
[PROOF STEP]
have P75 : "Bet_Point (Se A D1) D \<Longrightarrow> Plane_sameside (Li C A) D D1"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li C A) A
\<not> Eq (Geos (Lin (Li A D1)) add Emp) (Geos (Lin (Li C A)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P6 P64 P68 P71 P75
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se C B)) add Emp) (Geos (Seg (Se A D1)) add Emp) \<and> \<not> Bet_Point (Se D1 D) A \<and> Line_on (Li B D) D1 \<and> \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D1) add Emp)
Plane_diffside (Li C A) B D
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi D1) add Emp) \<Longrightarrow> Bet_Point (Se D A) D1 \<or> Bet_Point (Se A D1) D \<or> Bet_Point (Se D1 D) A
Bet_Point (Se A D) D1 \<Longrightarrow> Plane_sameside (Li C A) D D1
Bet_Point (Se A D1) D \<Longrightarrow> Plane_sameside (Li C A) D D1
[PROOF STEP]
have P76 : "\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi D1) add Emp) \<Longrightarrow>
    Plane_diffside (Li C A) B D1"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se C B)) add Emp) (Geos (Seg (Se A D1)) add Emp) \<and> \<not> Bet_Point (Se D1 D) A \<and> Line_on (Li B D) D1 \<and> \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D1) add Emp)
Plane_diffside (Li C A) B D
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi D1) add Emp) \<Longrightarrow> Bet_Point (Se D A) D1 \<or> Bet_Point (Se A D1) D \<or> Bet_Point (Se D1 D) A
Bet_Point (Se A D) D1 \<Longrightarrow> Plane_sameside (Li C A) D D1
Bet_Point (Se A D1) D \<Longrightarrow> Plane_sameside (Li C A) D D1

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi D) add Emp) (Geos (Poi D1) add Emp) \<Longrightarrow> Plane_diffside (Li C A) B D1
[PROOF STEP]
by (blast intro:Plane_trans Plane_diffside_rev Bet_rev)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi D1) add Emp) \<Longrightarrow> Plane_diffside (Li C A) B D1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P65 P76
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Poi D) add Emp) (Geos (Poi D1) add Emp) \<Longrightarrow> Plane_diffside (Li C A) B D1
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi D1) add Emp) \<Longrightarrow> Plane_diffside (Li C A) B D1
[PROOF STEP]
have P77 : "Plane_diffside (Li C A) B D1"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Poi D) add Emp) (Geos (Poi D1) add Emp) \<Longrightarrow> Plane_diffside (Li C A) B D1
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi D1) add Emp) \<Longrightarrow> Plane_diffside (Li C A) B D1

goal (1 subgoal):
 1. Plane_diffside (Li C A) B D1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li C A) B D1

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B E) B
[PROOF STEP]
have P79 : "Eq (Geos (Lin (Li B E)) 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 B E) B

goal (1 subgoal):
 1. Eq (Geos (Lin (Li B E)) 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 B E)) add Emp) (Geos (Lin (Li C A)) add Emp) \<Longrightarrow> Line_on (Li C A) B

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P62 P79
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li C A) B
Eq (Geos (Lin (Li B E)) add Emp) (Geos (Lin (Li C A)) add Emp) \<Longrightarrow> Line_on (Li C A) B
[PROOF STEP]
have P80 : "\<not> Eq (Geos (Lin (Li B E)) 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 B E)) 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 B E)) add Emp) (Geos (Lin (Li C A)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Lin (Li B E)) add Emp) (Geos (Lin (Li C A)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P49 P78 P80
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se B E) C
Line_on (Li C A) C
\<not> Eq (Geos (Lin (Li B E)) add Emp) (Geos (Lin (Li C A)) add Emp)
[PROOF STEP]
have P81 : "Plane_diffside (Li C A) B E"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se B E) C
Line_on (Li C A) C
\<not> Eq (Geos (Lin (Li B E)) add Emp) (Geos (Lin (Li C A)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P51
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B C) E
[PROOF STEP]
have P82 : "Eq (Geos (Poi D1) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> Line_on (Li B C) D1"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B C) E

goal (1 subgoal):
 1. Eq (Geos (Poi D1) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> Line_on (Li B C) D1
[PROOF STEP]
by (blast intro:Eq_rev Point_Eq)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi D1) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> Line_on (Li B C) D1

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

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

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

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

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

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P8 P20 P33 P82 P83
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A D) B
Line_on (Li A D) D1
Line_on (Li B C) B
Eq (Geos (Poi D1) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> Line_on (Li B C) D1
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D1) add Emp)
[PROOF STEP]
have P84 : "Eq (Geos (Poi D1) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow>
    Eq (Geos (Lin (Li A D)) add Emp) (Geos (Lin (Li B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A D) B
Line_on (Li A D) D1
Line_on (Li B C) B
Eq (Geos (Poi D1) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> Line_on (Li B C) D1
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D1) add Emp)

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

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

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

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

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

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P77 P81 P87
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li C A) B D1
Plane_diffside (Li C A) B E
\<not> Eq (Geos (Poi D1) add Emp) (Geos (Poi E) add Emp)
[PROOF STEP]
have P88 : "Plane_sameside (Li C A) D1 E"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li C A) B D1
Plane_diffside (Li C A) B E
\<not> Eq (Geos (Poi D1) add Emp) (Geos (Poi E) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P58 P59 P88
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A C E)) add Emp) (Geos (Ang (An D1 C A)) add Emp)
Cong (Geos (Ang (An A C E)) add Emp) (Geos (Ang (An E C A)) add Emp)
Plane_sameside (Li C A) D1 E
[PROOF STEP]
have P89 : "Eq (Geos (Lin (Li D1 C)) add Emp) (Geos (Lin (Li E C)) add Emp) \<and> \<not> Bet_Point (Se D1 E) C"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A C E)) add Emp) (Geos (Ang (An D1 C A)) add Emp)
Cong (Geos (Ang (An A C E)) add Emp) (Geos (Ang (An E C A)) add Emp)
Plane_sameside (Li C A) D1 E

goal (1 subgoal):
 1. Eq (Geos (Lin (Li D1 C)) add Emp) (Geos (Lin (Li E C)) add Emp) \<and> \<not> Bet_Point (Se D1 E) C
[PROOF STEP]
by (simp add:Ang_move_unique)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li D1 C)) add Emp) (Geos (Lin (Li E C)) add Emp) \<and> \<not> Bet_Point (Se D1 E) C

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P49
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se B E) C
[PROOF STEP]
have P90 : "Line_on (Li E C) B"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se B E) C

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P89 P90
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li D1 C)) add Emp) (Geos (Lin (Li E C)) add Emp) \<and> \<not> Bet_Point (Se D1 E) C
Line_on (Li E C) B
[PROOF STEP]
have P91 : "Line_on (Li D1 C) B"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li D1 C)) add Emp) (Geos (Lin (Li E C)) add Emp) \<and> \<not> Bet_Point (Se D1 E) C
Line_on (Li E C) B

goal (1 subgoal):
 1. Line_on (Li D1 C) B
[PROOF STEP]
by (blast intro:Eq_rev Line_on_trans)
[PROOF STATE]
proof (state)
this:
Line_on (Li D1 C) B

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P8 P20 P83 P91 P92
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A D) B
Line_on (Li A D) D1
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D1) add Emp)
Line_on (Li D1 C) B
Line_on (Li D1 C) D1
[PROOF STEP]
have P93 : "Eq (Geos (Lin (Li A D)) add Emp) (Geos (Lin (Li D1 C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A D) B
Line_on (Li A D) D1
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D1) add Emp)
Line_on (Li D1 C) B
Line_on (Li D1 C) D1

goal (1 subgoal):
 1. Eq (Geos (Lin (Li A D)) add Emp) (Geos (Lin (Li D1 C)) 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 D1 C)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An A C B)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P89 P93
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li D1 C)) add Emp) (Geos (Lin (Li E C)) add Emp) \<and> \<not> Bet_Point (Se D1 E) C
Eq (Geos (Lin (Li A D)) add Emp) (Geos (Lin (Li D1 C)) add Emp)
[PROOF STEP]
have P94 : "Eq (Geos (Lin (Li A D)) add Emp) (Geos (Lin (Li E C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li D1 C)) add Emp) (Geos (Lin (Li E C)) add Emp) \<and> \<not> Bet_Point (Se D1 E) C
Eq (Geos (Lin (Li A D)) add Emp) (Geos (Lin (Li D1 C)) add Emp)

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

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

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

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed