[STATEMENT]
lemma (in Congruence_Rule) Ang_Gr_trans_Eq_Gr :
  assumes
    "Def (Ang (An p11 p12 p13))" "Def (Ang (An p21 p22 p23))" "Def (Ang (An p31 p32 p33))"
    "Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)"
    "Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)"
  shows
    "Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
have P1 : "\<not> Line_on (Li p22 p23) p21"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)

goal (1 subgoal):
 1. \<not> Line_on (Li p22 p23) p21
[PROOF STEP]
by (simp add:Ang_to_Tri Tri_def_Line)
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li p22 p23) p21

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms P1
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
\<not> Line_on (Li p22 p23) p21
[PROOF STEP]
have "\<exists>p. Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p p22 p23)) add Emp)
    \<and> Plane_sameside (Li p22 p23) p p21"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
\<not> Line_on (Li p22 p23) p21

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p p22 p23)) add Emp) \<and> Plane_sameside (Li p22 p23) p p21
[PROOF STEP]
by (simp add:Ang_move_sameside)
[PROOF STATE]
proof (state)
this:
\<exists>p. Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p p22 p23)) add Emp) \<and> Plane_sameside (Li p22 p23) p p21

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p p22 p23)) add Emp) \<and> Plane_sameside (Li p22 p23) p p21
[PROOF STEP]
obtain p24 :: Point where P2 : "Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p24 p22 p23)) add Emp)
    \<and> Plane_sameside (Li p22 p23) p24 p21"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p p22 p23)) add Emp) \<and> Plane_sameside (Li p22 p23) p p21

goal (1 subgoal):
 1. (\<And>p24. Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p24 p22 p23)) add Emp) \<and> Plane_sameside (Li p22 p23) p24 p21 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p24 p22 p23)) add Emp) \<and> Plane_sameside (Li p22 p23) p24 p21

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p24 p22 p23)) add Emp) \<and> Plane_sameside (Li p22 p23) p24 p21
[PROOF STEP]
have P3 : "Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p24 p22 p23)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p24 p22 p23)) add Emp) \<and> Plane_sameside (Li p22 p23) p24 p21

goal (1 subgoal):
 1. Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p24 p22 p23)) add Emp)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p24 p22 p23)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P2
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p24 p22 p23)) add Emp) \<and> Plane_sameside (Li p22 p23) p24 p21
[PROOF STEP]
have P4 : "Plane_sameside (Li p22 p23) p24 p21"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p24 p22 p23)) add Emp) \<and> Plane_sameside (Li p22 p23) p24 p21

goal (1 subgoal):
 1. Plane_sameside (Li p22 p23) p24 p21
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li p22 p23) p24 p21

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms P3 P4
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p24 p22 p23)) add Emp)
Plane_sameside (Li p22 p23) p24 p21
[PROOF STEP]
have "Ang_inside (An p21 p22 p23) p24"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p24 p22 p23)) add Emp)
Plane_sameside (Li p22 p23) p24 p21

goal (1 subgoal):
 1. Ang_inside (An p21 p22 p23) p24
[PROOF STEP]
by (simp add:Ang_greater_def)
[PROOF STATE]
proof (state)
this:
Ang_inside (An p21 p22 p23) p24

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An p21 p22 p23) p24
[PROOF STEP]
have P5 : "Ang_inside (An p23 p22 p21) p24"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An p21 p22 p23) p24

goal (1 subgoal):
 1. Ang_inside (An p23 p22 p21) p24
[PROOF STEP]
by (simp add:Ang_inside_def Ang_def_rev)
[PROOF STATE]
proof (state)
this:
Ang_inside (An p23 p22 p21) p24

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
have P6 : "\<not> Line_on (Li p32 p33) p31"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)

goal (1 subgoal):
 1. \<not> Line_on (Li p32 p33) p31
[PROOF STEP]
by (simp add:Ang_to_Tri Tri_def_Line)
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li p32 p33) p31

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms P6
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
\<not> Line_on (Li p32 p33) p31
[PROOF STEP]
have "\<exists>p. Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p p32 p33)) add Emp)
    \<and> Plane_sameside (Li p32 p33) p p31"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
\<not> Line_on (Li p32 p33) p31

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p p32 p33)) add Emp) \<and> Plane_sameside (Li p32 p33) p p31
[PROOF STEP]
by (simp add:Ang_move_sameside)
[PROOF STATE]
proof (state)
this:
\<exists>p. Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p p32 p33)) add Emp) \<and> Plane_sameside (Li p32 p33) p p31

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p p32 p33)) add Emp) \<and> Plane_sameside (Li p32 p33) p p31
[PROOF STEP]
obtain p34 :: Point where P7 : "Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p34 p32 p33)) add Emp)
    \<and> Plane_sameside (Li p32 p33) p34 p31"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p p32 p33)) add Emp) \<and> Plane_sameside (Li p32 p33) p p31

goal (1 subgoal):
 1. (\<And>p34. Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p34 p32 p33)) add Emp) \<and> Plane_sameside (Li p32 p33) p34 p31 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p34 p32 p33)) add Emp) \<and> Plane_sameside (Li p32 p33) p34 p31

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p34 p32 p33)) add Emp) \<and> Plane_sameside (Li p32 p33) p34 p31
[PROOF STEP]
have P8 : "Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p34 p32 p33)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p34 p32 p33)) add Emp) \<and> Plane_sameside (Li p32 p33) p34 p31

goal (1 subgoal):
 1. Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p34 p32 p33)) add Emp)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p34 p32 p33)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P7
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p34 p32 p33)) add Emp) \<and> Plane_sameside (Li p32 p33) p34 p31
[PROOF STEP]
have P9 : "Plane_sameside (Li p32 p33) p34 p31"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p34 p32 p33)) add Emp) \<and> Plane_sameside (Li p32 p33) p34 p31

goal (1 subgoal):
 1. Plane_sameside (Li p32 p33) p34 p31
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li p32 p33) p34 p31

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
have P10 : "Def (Ang (An p33 p32 p31))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)

goal (1 subgoal):
 1. Def (Ang (An p33 p32 p31))
[PROOF STEP]
by (blast intro:Ang_def_rev)
[PROOF STATE]
proof (state)
this:
Def (Ang (An p33 p32 p31))

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
have P11 : "Def (Ang (An p23 p22 p21))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)

goal (1 subgoal):
 1. Def (Ang (An p23 p22 p21))
[PROOF STEP]
by (blast intro:Ang_def_rev)
[PROOF STATE]
proof (state)
this:
Def (Ang (An p23 p22 p21))

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P4
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p22 p23) p24 p21
[PROOF STEP]
have P12 : "\<not> Line_on (Li p22 p23) p24"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p22 p23) p24 p21

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
have P13 : "\<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p23) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P12 P13
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li p22 p23) p24
\<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p23) add Emp)
[PROOF STEP]
have "Def (Ang (An p22 p23 p24))"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li p22 p23) p24
\<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p23) add Emp)

goal (1 subgoal):
 1. Def (Ang (An p22 p23 p24))
[PROOF STEP]
by (simp add:Ang_sinple_def)
[PROOF STATE]
proof (state)
this:
Def (Ang (An p22 p23 p24))

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p22 p23 p24))
[PROOF STEP]
have P14 : "Def (Ang (An p24 p22 p23))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p22 p23 p24))

goal (1 subgoal):
 1. Def (Ang (An p24 p22 p23))
[PROOF STEP]
by (blast intro:Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An p24 p22 p23))

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p24 p22 p23))
[PROOF STEP]
have P15 : "Def (Ang (An p23 p22 p24))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p24 p22 p23))

goal (1 subgoal):
 1. Def (Ang (An p23 p22 p24))
[PROOF STEP]
by (blast intro:Ang_def_rev)
[PROOF STATE]
proof (state)
this:
Def (Ang (An p23 p22 p24))

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
have P16 : "Cong (Geos (Ang (An p24 p22 p23)) add Emp) (Geos (Ang (An p23 p22 p24)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An p24 p22 p23)) add Emp) (Geos (Ang (An p23 p22 p24)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p24 p22 p23)) add Emp) (Geos (Ang (An p23 p22 p24)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms P3 P14 P15 P16
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p24 p22 p23)) add Emp)
Def (Ang (An p24 p22 p23))
Def (Ang (An p23 p22 p24))
Cong (Geos (Ang (An p24 p22 p23)) add Emp) (Geos (Ang (An p23 p22 p24)) add Emp)
[PROOF STEP]
have P17 :
    "Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p23 p22 p24)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p24 p22 p23)) add Emp)
Def (Ang (An p24 p22 p23))
Def (Ang (An p23 p22 p24))
Cong (Geos (Ang (An p24 p22 p23)) add Emp) (Geos (Ang (An p23 p22 p24)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p23 p22 p24)) add Emp)
[PROOF STEP]
by (blast intro:Ang_trans Ang_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p23 p22 p24)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
have P18 : "Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p33 p32 p31)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p33 p32 p31)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p33 p32 p31)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms P10 P15 P17 P18
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Def (Ang (An p33 p32 p31))
Def (Ang (An p23 p22 p24))
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p23 p22 p24)) add Emp)
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p33 p32 p31)) add Emp)
[PROOF STEP]
have P19 :
    "Cong (Geos (Ang (An p33 p32 p31)) add Emp) (Geos (Ang (An p23 p22 p24)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Def (Ang (An p33 p32 p31))
Def (Ang (An p23 p22 p24))
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p23 p22 p24)) add Emp)
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p33 p32 p31)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An p33 p32 p31)) add Emp) (Geos (Ang (An p23 p22 p24)) add Emp)
[PROOF STEP]
by (blast intro:Ang_trans Ang_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p33 p32 p31)) add Emp) (Geos (Ang (An p23 p22 p24)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P9
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p32 p33) p34 p31
[PROOF STEP]
have P20 : "\<not> Line_on (Li p32 p33) p34"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p32 p33) p34 p31

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
have P21 : "\<not> Eq (Geos (Poi p32) add Emp) (Geos (Poi p33) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P20 P21
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li p32 p33) p34
\<not> Eq (Geos (Poi p32) add Emp) (Geos (Poi p33) add Emp)
[PROOF STEP]
have "Def (Ang (An p32 p33 p34))"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li p32 p33) p34
\<not> Eq (Geos (Poi p32) add Emp) (Geos (Poi p33) add Emp)

goal (1 subgoal):
 1. Def (Ang (An p32 p33 p34))
[PROOF STEP]
by (simp add:Ang_sinple_def)
[PROOF STATE]
proof (state)
this:
Def (Ang (An p32 p33 p34))

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p32 p33 p34))
[PROOF STEP]
have P22 : "Def (Ang (An p34 p32 p33))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p32 p33 p34))

goal (1 subgoal):
 1. Def (Ang (An p34 p32 p33))
[PROOF STEP]
by (blast intro:Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An p34 p32 p33))

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p34 p32 p33))
[PROOF STEP]
have P23 : "Def (Ang (An p33 p32 p34))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p34 p32 p33))

goal (1 subgoal):
 1. Def (Ang (An p33 p32 p34))
[PROOF STEP]
by (blast intro:Ang_def_rev)
[PROOF STATE]
proof (state)
this:
Def (Ang (An p33 p32 p34))

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
have P24 : "Cong (Geos (Ang (An p34 p32 p33)) add Emp) (Geos (Ang (An p33 p32 p34)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An p34 p32 p33)) add Emp) (Geos (Ang (An p33 p32 p34)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p34 p32 p33)) add Emp) (Geos (Ang (An p33 p32 p34)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms P8 P22 P23 P24
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p34 p32 p33)) add Emp)
Def (Ang (An p34 p32 p33))
Def (Ang (An p33 p32 p34))
Cong (Geos (Ang (An p34 p32 p33)) add Emp) (Geos (Ang (An p33 p32 p34)) add Emp)
[PROOF STEP]
have P25 :
    "Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p33 p32 p34)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p34 p32 p33)) add Emp)
Def (Ang (An p34 p32 p33))
Def (Ang (An p33 p32 p34))
Cong (Geos (Ang (An p34 p32 p33)) add Emp) (Geos (Ang (An p33 p32 p34)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p33 p32 p34)) add Emp)
[PROOF STEP]
by (blast intro:Ang_trans Ang_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p33 p32 p34)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
have P26 : "Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p23 p22 p21)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p23 p22 p21)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p23 p22 p21)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms P11 P23 P25 P26
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Def (Ang (An p23 p22 p21))
Def (Ang (An p33 p32 p34))
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p33 p32 p34)) add Emp)
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p23 p22 p21)) add Emp)
[PROOF STEP]
have P27 :
    "Cong (Geos (Ang (An p23 p22 p21)) add Emp) (Geos (Ang (An p33 p32 p34)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Def (Ang (An p23 p22 p21))
Def (Ang (An p33 p32 p34))
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p33 p32 p34)) add Emp)
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p23 p22 p21)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An p23 p22 p21)) add Emp) (Geos (Ang (An p33 p32 p34)) add Emp)
[PROOF STEP]
by (blast intro:Ang_trans Ang_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p23 p22 p21)) add Emp) (Geos (Ang (An p33 p32 p34)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P9
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p32 p33) p34 p31
[PROOF STEP]
have P28 : "Plane_sameside (Li p32 p33) p31 p34"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p32 p33) p34 p31

goal (1 subgoal):
 1. Plane_sameside (Li p32 p33) p31 p34
[PROOF STEP]
by (simp add:Plane_sameside_rev)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li p32 p33) p31 p34

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P4 P5 P10 P11 P19 P27 P28
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p22 p23) p24 p21
Ang_inside (An p23 p22 p21) p24
Def (Ang (An p33 p32 p31))
Def (Ang (An p23 p22 p21))
Cong (Geos (Ang (An p33 p32 p31)) add Emp) (Geos (Ang (An p23 p22 p24)) add Emp)
Cong (Geos (Ang (An p23 p22 p21)) add Emp) (Geos (Ang (An p33 p32 p34)) add Emp)
Plane_sameside (Li p32 p33) p31 p34
[PROOF STEP]
have P29 : "\<not> Ang_inside (An p33 p32 p31) p34
    \<and> \<not> Eq (Geos (Lin (Li p32 p31)) add Emp) (Geos (Lin (Li p32 p34)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p22 p23) p24 p21
Ang_inside (An p23 p22 p21) p24
Def (Ang (An p33 p32 p31))
Def (Ang (An p23 p22 p21))
Cong (Geos (Ang (An p33 p32 p31)) add Emp) (Geos (Ang (An p23 p22 p24)) add Emp)
Cong (Geos (Ang (An p23 p22 p21)) add Emp) (Geos (Ang (An p33 p32 p34)) add Emp)
Plane_sameside (Li p32 p33) p31 p34

goal (1 subgoal):
 1. \<not> Ang_inside (An p33 p32 p31) p34 \<and> \<not> Eq (Geos (Lin (Li p32 p31)) add Emp) (Geos (Lin (Li p32 p34)) add Emp)
[PROOF STEP]
by (simp add:Ang_move_Greater)
[PROOF STATE]
proof (state)
this:
\<not> Ang_inside (An p33 p32 p31) p34 \<and> \<not> Eq (Geos (Lin (Li p32 p31)) add Emp) (Geos (Lin (Li p32 p34)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
have P30 : "Ang_inside (An p31 p32 p33) p34 \<Longrightarrow> Ang_inside (An p33 p32 p31) p34"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ang_inside (An p31 p32 p33) p34 \<Longrightarrow> Ang_inside (An p33 p32 p31) p34
[PROOF STEP]
by (simp add:Ang_inside_def Ang_def_rev)
[PROOF STATE]
proof (state)
this:
Ang_inside (An p31 p32 p33) p34 \<Longrightarrow> Ang_inside (An p33 p32 p31) p34

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P29 P30
[PROOF STATE]
proof (chain)
picking this:
\<not> Ang_inside (An p33 p32 p31) p34 \<and> \<not> Eq (Geos (Lin (Li p32 p31)) add Emp) (Geos (Lin (Li p32 p34)) add Emp)
Ang_inside (An p31 p32 p33) p34 \<Longrightarrow> Ang_inside (An p33 p32 p31) p34
[PROOF STEP]
have P31 : "\<not> Ang_inside (An p31 p32 p33) p34"
[PROOF STATE]
proof (prove)
using this:
\<not> Ang_inside (An p33 p32 p31) p34 \<and> \<not> Eq (Geos (Lin (Li p32 p31)) add Emp) (Geos (Lin (Li p32 p34)) add Emp)
Ang_inside (An p31 p32 p33) p34 \<Longrightarrow> Ang_inside (An p33 p32 p31) p34

goal (1 subgoal):
 1. \<not> Ang_inside (An p31 p32 p33) p34
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Ang_inside (An p31 p32 p33) p34

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms P8 P22
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p34 p32 p33)) add Emp)
Def (Ang (An p34 p32 p33))
[PROOF STEP]
have P32 : "Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p34 p32 p33)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p34 p32 p33)) add Emp)
Def (Ang (An p34 p32 p33))

goal (1 subgoal):
 1. Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p34 p32 p33)) add Emp)
[PROOF STEP]
by (blast intro:Ang_trans Ang_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p34 p32 p33)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P9 P29 P31 P32
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p32 p33) p34 p31
\<not> Ang_inside (An p33 p32 p31) p34 \<and> \<not> Eq (Geos (Lin (Li p32 p31)) add Emp) (Geos (Lin (Li p32 p34)) add Emp)
\<not> Ang_inside (An p31 p32 p33) p34
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p34 p32 p33)) add Emp)
[PROOF STEP]
show "Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p32 p33) p34 p31
\<not> Ang_inside (An p33 p32 p31) p34 \<and> \<not> Eq (Geos (Lin (Li p32 p31)) add Emp) (Geos (Lin (Li p32 p34)) add Emp)
\<not> Ang_inside (An p31 p32 p33) p34
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p34 p32 p33)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
by (simp add:Ang_less_def)
[PROOF STATE]
proof (state)
this:
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Congruence_Rule) Ang_Gr_trans_Gr_Eq :
  assumes
    "Def (Ang (An p11 p12 p13))" "Def (Ang (An p21 p22 p23))" "Def (Ang (An p31 p32 p33))"
    "Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)"
    "Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)"
  shows
    "Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
have P1 : "\<not> Line_on (Li p12 p13) p11"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)

goal (1 subgoal):
 1. \<not> Line_on (Li p12 p13) p11
[PROOF STEP]
by (simp add:Ang_to_Tri Tri_def_Line)
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li p12 p13) p11

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms P1
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
\<not> Line_on (Li p12 p13) p11
[PROOF STEP]
have "\<exists>p. Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p p12 p13)) add Emp)
    \<and> Plane_sameside (Li p12 p13) p p11"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
\<not> Line_on (Li p12 p13) p11

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p p11
[PROOF STEP]
by (simp add:Ang_move_sameside)
[PROOF STATE]
proof (state)
this:
\<exists>p. Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p p11

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p p11
[PROOF STEP]
obtain p14 :: Point where P2 : "Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)
    \<and> Plane_sameside (Li p12 p13) p14 p11"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p p11

goal (1 subgoal):
 1. (\<And>p14. Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p14 p11 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p14 p11

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p14 p11
[PROOF STEP]
have P3 : "Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p14 p11

goal (1 subgoal):
 1. Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P2
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p14 p11
[PROOF STEP]
have P4 : "Plane_sameside (Li p12 p13) p14 p11"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p14 p11

goal (1 subgoal):
 1. Plane_sameside (Li p12 p13) p14 p11
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li p12 p13) p14 p11

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P3 P4
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)
Plane_sameside (Li p12 p13) p14 p11
[PROOF STEP]
have P5 : "Ang_inside (An p11 p12 p13) p14 \<longleftrightarrow>
    Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)
Plane_sameside (Li p12 p13) p14 p11

goal (1 subgoal):
 1. Ang_inside (An p11 p12 p13) p14 = Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
by (simp add:Ang_greater_def)
[PROOF STATE]
proof (state)
this:
Ang_inside (An p11 p12 p13) p14 = Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms P5
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Ang_inside (An p11 p12 p13) p14 = Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
have P6 : "Ang_inside (An p11 p12 p13) p14"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Ang_inside (An p11 p12 p13) p14 = Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An p11 p12 p13) p14
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Ang_inside (An p11 p12 p13) p14

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P4
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p12 p13) p14 p11
[PROOF STEP]
have P7 : "\<not> Line_on (Li p12 p13) p14"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p12 p13) p14 p11

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
have P8 : "\<not> Eq (Geos (Poi p12) add Emp) (Geos (Poi p13) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P7 P8
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li p12 p13) p14
\<not> Eq (Geos (Poi p12) add Emp) (Geos (Poi p13) add Emp)
[PROOF STEP]
have "Def (Ang (An p12 p13 p14))"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li p12 p13) p14
\<not> Eq (Geos (Poi p12) add Emp) (Geos (Poi p13) add Emp)

goal (1 subgoal):
 1. Def (Ang (An p12 p13 p14))
[PROOF STEP]
by (simp add:Ang_sinple_def)
[PROOF STATE]
proof (state)
this:
Def (Ang (An p12 p13 p14))

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p12 p13 p14))
[PROOF STEP]
have P9 : "Def (Ang (An p14 p12 p13))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p12 p13 p14))

goal (1 subgoal):
 1. Def (Ang (An p14 p12 p13))
[PROOF STEP]
by (blast intro:Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An p14 p12 p13))

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms P3 P9
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)
Def (Ang (An p14 p12 p13))
[PROOF STEP]
have P10 : "Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)
Def (Ang (An p14 p12 p13))

goal (1 subgoal):
 1. Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)
[PROOF STEP]
by (blast intro:Ang_trans Ang_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P4 P10
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p12 p13) p14 p11
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)
[PROOF STEP]
have P11 : "Ang_inside (An p11 p12 p13) p14 \<longleftrightarrow>
    Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p12 p13) p14 p11
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An p11 p12 p13) p14 = Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
by (simp add:Ang_greater_def)
[PROOF STATE]
proof (state)
this:
Ang_inside (An p11 p12 p13) p14 = Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P6 P11
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An p11 p12 p13) p14
Ang_inside (An p11 p12 p13) p14 = Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
show "Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An p11 p12 p13) p14
Ang_inside (An p11 p12 p13) p14 = Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Congruence_Rule) Ang_Eq_Point :
  assumes
    "Def (Ang (An p1 p2 p3))"
    "Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)"
  shows
    "Eq (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp) \<and> Def (Ang (An p4 p2 p3))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp) \<and> Def (Ang (An p4 p2 p3))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Eq (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp) \<and> Def (Ang (An p4 p2 p3))
[PROOF STEP]
have "Line_on (Li p2 p1) p1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p2 p1) p1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p2 p1) p1

goal (1 subgoal):
 1. Eq (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp) \<and> Def (Ang (An p4 p2 p3))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p2 p1) p1
[PROOF STEP]
have P1 : "Line_on (Li p2 p1) p4"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p2 p1) p1

goal (1 subgoal):
 1. Line_on (Li p2 p1) p4
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p2 p1) p1
Def (Ang (An p1 p2 p3))
Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)

goal (1 subgoal):
 1. Line_on (Li p2 p1) p4
[PROOF STEP]
by (simp add:Point_Eq)
[PROOF STATE]
proof (state)
this:
Line_on (Li p2 p1) p4

goal (1 subgoal):
 1. Eq (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp) \<and> Def (Ang (An p4 p2 p3))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p1 p2 p3))
Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)
[PROOF STEP]
have P2 : "Bet_Point (Se p1 p4) p2 \<Longrightarrow> Bet_Point (Se p4 p4) p2"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p1 p2 p3))
Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se p1 p4) p2 \<Longrightarrow> Bet_Point (Se p4 p4) p2
[PROOF STEP]
by (simp add:Bet_Point_Eq)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p1 p4) p2 \<Longrightarrow> Bet_Point (Se p4 p4) p2

goal (1 subgoal):
 1. Eq (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp) \<and> Def (Ang (An p4 p2 p3))
[PROOF STEP]
have P3 : "\<not> Bet_Point (Se p4 p4) p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se p4 p4) p2
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se p4 p4) p2

goal (1 subgoal):
 1. Eq (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp) \<and> Def (Ang (An p4 p2 p3))
[PROOF STEP]
from P2 P3
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p1 p4) p2 \<Longrightarrow> Bet_Point (Se p4 p4) p2
\<not> Bet_Point (Se p4 p4) p2
[PROOF STEP]
have P4 : "\<not> Bet_Point (Se p1 p4) p2"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p1 p4) p2 \<Longrightarrow> Bet_Point (Se p4 p4) p2
\<not> Bet_Point (Se p4 p4) p2

goal (1 subgoal):
 1. \<not> Bet_Point (Se p1 p4) p2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se p1 p4) p2

goal (1 subgoal):
 1. Eq (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp) \<and> Def (Ang (An p4 p2 p3))
[PROOF STEP]
have P5 : "Line_on (Li p2 p3) p3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p2 p3) p3
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p2 p3) p3

goal (1 subgoal):
 1. Eq (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp) \<and> Def (Ang (An p4 p2 p3))
[PROOF STEP]
have P6 : "\<not> Bet_Point (Se p3 p3) p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se p3 p3) p2
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se p3 p3) p2

goal (1 subgoal):
 1. Eq (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp) \<and> Def (Ang (An p4 p2 p3))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p1 p2 p3))
Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)
[PROOF STEP]
have P7 : "\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p1 p2 p3))
Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)

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

goal (1 subgoal):
 1. Eq (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp) \<and> Def (Ang (An p4 p2 p3))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p1 p2 p3))
Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)
[PROOF STEP]
have P8 : "Eq (Geos (Poi p2) add Emp) (Geos (Poi p4) add Emp) \<Longrightarrow>
    Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p1 p2 p3))
Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Poi p2) add Emp) (Geos (Poi p4) add Emp) \<Longrightarrow> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
[PROOF STEP]
by (blast intro:Eq_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi p2) add Emp) (Geos (Poi p4) add Emp) \<Longrightarrow> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp) \<and> Def (Ang (An p4 p2 p3))
[PROOF STEP]
from P7 P8
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
Eq (Geos (Poi p2) add Emp) (Geos (Poi p4) add Emp) \<Longrightarrow> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
[PROOF STEP]
have P9 : "\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p4) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
Eq (Geos (Poi p2) add Emp) (Geos (Poi p4) add Emp) \<Longrightarrow> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)

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

goal (1 subgoal):
 1. Eq (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp) \<and> Def (Ang (An p4 p2 p3))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p1 p2 p3))
Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)
[PROOF STEP]
have P10 : "\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p1 p2 p3))
Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)

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

goal (1 subgoal):
 1. Eq (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp) \<and> Def (Ang (An p4 p2 p3))
[PROOF STEP]
from assms P1 P4 P5 P6 P9 P10
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p1 p2 p3))
Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)
Line_on (Li p2 p1) p4
\<not> Bet_Point (Se p1 p4) p2
Line_on (Li p2 p3) p3
\<not> Bet_Point (Se p3 p3) p2
\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p4) add Emp)
\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)
[PROOF STEP]
show
    "Eq (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp) \<and> Def (Ang (An p4 p2 p3))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p1 p2 p3))
Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)
Line_on (Li p2 p1) p4
\<not> Bet_Point (Se p1 p4) p2
Line_on (Li p2 p3) p3
\<not> Bet_Point (Se p3 p3) p2
\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p4) add Emp)
\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp) \<and> Def (Ang (An p4 p2 p3))
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp) \<and> Def (Ang (An p4 p2 p3))

goal:
No subgoals!
[PROOF STEP]
qed