[STATEMENT]
theorem (in Congruence_Rule) Ang_Right_angle_Cong :
  assumes
    "Right_angle (An l1 o1 h1)" "Right_angle (An l2 o2 h2)"
  shows
    "Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Right_angle (An l1 o1 h1)
Right_angle (An l2 o2 h2)
[PROOF STEP]
have "\<exists>p. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 p)) add Emp)
        \<and> Bet_Point (Se h1 p) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 p))"
[PROOF STATE]
proof (prove)
using this:
Right_angle (An l1 o1 h1)
Right_angle (An l2 o2 h2)

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 p)) add Emp) \<and> Bet_Point (Se h1 p) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 p))
[PROOF STEP]
by (simp add:Ang_Right_angle_def)
[PROOF STATE]
proof (state)
this:
\<exists>p. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 p)) add Emp) \<and> Bet_Point (Se h1 p) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 p))

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 p)) add Emp) \<and> Bet_Point (Se h1 p) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 p))
[PROOF STEP]
obtain k1 :: Point where P1 : "Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp)
        \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 p)) add Emp) \<and> Bet_Point (Se h1 p) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 p))

goal (1 subgoal):
 1. (\<And>k1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Right_angle (An l1 o1 h1)
Right_angle (An l2 o2 h2)
[PROOF STEP]
have "\<exists>p. Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l2 o2 p)) add Emp)
        \<and> Bet_Point (Se h2 p) o2 \<and> Def (Ang (An l2 o2 h2)) \<and> Def (Ang (An l2 o2 p))"
[PROOF STATE]
proof (prove)
using this:
Right_angle (An l1 o1 h1)
Right_angle (An l2 o2 h2)

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l2 o2 p)) add Emp) \<and> Bet_Point (Se h2 p) o2 \<and> Def (Ang (An l2 o2 h2)) \<and> Def (Ang (An l2 o2 p))
[PROOF STEP]
by (simp add:Ang_Right_angle_def)
[PROOF STATE]
proof (state)
this:
\<exists>p. Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l2 o2 p)) add Emp) \<and> Bet_Point (Se h2 p) o2 \<and> Def (Ang (An l2 o2 h2)) \<and> Def (Ang (An l2 o2 p))

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l2 o2 p)) add Emp) \<and> Bet_Point (Se h2 p) o2 \<and> Def (Ang (An l2 o2 h2)) \<and> Def (Ang (An l2 o2 p))
[PROOF STEP]
obtain k2 :: Point where P2 : "Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp)
        \<and> Bet_Point (Se h2 k2) o2 \<and> Def (Ang (An l2 o2 h2)) \<and> Def (Ang (An l2 o2 k2))"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l2 o2 p)) add Emp) \<and> Bet_Point (Se h2 p) o2 \<and> Def (Ang (An l2 o2 h2)) \<and> Def (Ang (An l2 o2 p))

goal (1 subgoal):
 1. (\<And>k2. Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp) \<and> Bet_Point (Se h2 k2) o2 \<and> Def (Ang (An l2 o2 h2)) \<and> Def (Ang (An l2 o2 k2)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp) \<and> Bet_Point (Se h2 k2) o2 \<and> Def (Ang (An l2 o2 h2)) \<and> Def (Ang (An l2 o2 k2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))
[PROOF STEP]
have P3 : "\<not> Line_on (Li o1 h1) l1"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P1 P2 P3
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp) \<and> Bet_Point (Se h2 k2) o2 \<and> Def (Ang (An l2 o2 h2)) \<and> Def (Ang (An l2 o2 k2))
\<not> Line_on (Li o1 h1) l1
[PROOF STEP]
have "\<exists>p. Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An p o1 h1)) add Emp)
    \<and> Plane_sameside (Li o1 h1) p l1"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp) \<and> Bet_Point (Se h2 k2) o2 \<and> Def (Ang (An l2 o2 h2)) \<and> Def (Ang (An l2 o2 k2))
\<not> Line_on (Li o1 h1) l1

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An p o1 h1)) add Emp) \<and> Plane_sameside (Li o1 h1) p l1
[PROOF STEP]
by (simp add:Ang_move_sameside)
[PROOF STATE]
proof (state)
this:
\<exists>p. Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An p o1 h1)) add Emp) \<and> Plane_sameside (Li o1 h1) p l1

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An p o1 h1)) add Emp) \<and> Plane_sameside (Li o1 h1) p l1
[PROOF STEP]
obtain l11 :: Point where P4 : "Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)
    \<and> Plane_sameside (Li o1 h1) l11 l1"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An p o1 h1)) add Emp) \<and> Plane_sameside (Li o1 h1) p l1

goal (1 subgoal):
 1. (\<And>l11. Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp) \<and> Plane_sameside (Li o1 h1) l11 l1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp) \<and> Plane_sameside (Li o1 h1) l11 l1

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp) \<and> Plane_sameside (Li o1 h1) l11 l1
[PROOF STEP]
have P5 : "\<not> Line_on (Li o1 h1) l11"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp) \<and> Plane_sameside (Li o1 h1) l11 l1

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))
[PROOF STEP]
have P6 : "\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi h1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P5 P6
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li o1 h1) l11
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi h1) add Emp)
[PROOF STEP]
have "Def (Ang (An o1 h1 l11))"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li o1 h1) l11
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi h1) add Emp)

goal (1 subgoal):
 1. Def (Ang (An o1 h1 l11))
[PROOF STEP]
by (simp add:Ang_sinple_def)
[PROOF STATE]
proof (state)
this:
Def (Ang (An o1 h1 l11))

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An o1 h1 l11))
[PROOF STEP]
have P7 : "Def (Ang (An l11 o1 h1))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An o1 h1 l11))

goal (1 subgoal):
 1. Def (Ang (An l11 o1 h1))
[PROOF STEP]
by (blast intro:Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An l11 o1 h1))

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P2 P4 P7
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp) \<and> Bet_Point (Se h2 k2) o2 \<and> Def (Ang (An l2 o2 h2)) \<and> Def (Ang (An l2 o2 k2))
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp) \<and> Plane_sameside (Li o1 h1) l11 l1
Def (Ang (An l11 o1 h1))
[PROOF STEP]
have P8 : "Cong (Geos (Ang (An l2 o2 k2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp) \<and> Bet_Point (Se h2 k2) o2 \<and> Def (Ang (An l2 o2 h2)) \<and> Def (Ang (An l2 o2 k2))
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp) \<and> Plane_sameside (Li o1 h1) l11 l1
Def (Ang (An l11 o1 h1))

goal (1 subgoal):
 1. Cong (Geos (Ang (An l2 o2 k2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)
[PROOF STEP]
by (blast intro:Ang_rev Ang_trans)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An l2 o2 k2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P2
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp) \<and> Bet_Point (Se h2 k2) o2 \<and> Def (Ang (An l2 o2 h2)) \<and> Def (Ang (An l2 o2 k2))
[PROOF STEP]
have P9 : "Def (Ang (An h2 o2 l2))"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp) \<and> Bet_Point (Se h2 k2) o2 \<and> Def (Ang (An l2 o2 h2)) \<and> Def (Ang (An l2 o2 k2))

goal (1 subgoal):
 1. Def (Ang (An h2 o2 l2))
[PROOF STEP]
by (simp add:Ang_def_rev)
[PROOF STATE]
proof (state)
this:
Def (Ang (An h2 o2 l2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P7
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An l11 o1 h1))
[PROOF STEP]
have P10 : "Def (Ang (An h1 o1 l11))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An l11 o1 h1))

goal (1 subgoal):
 1. Def (Ang (An h1 o1 l11))
[PROOF STEP]
by (simp add:Ang_def_rev)
[PROOF STATE]
proof (state)
this:
Def (Ang (An h1 o1 l11))

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
have P11 : "Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
have P12 : "Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An h1 o1 l11)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An h1 o1 l11)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An h1 o1 l11)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P2 P4 P7 P9 P11
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp) \<and> Bet_Point (Se h2 k2) o2 \<and> Def (Ang (An l2 o2 h2)) \<and> Def (Ang (An l2 o2 k2))
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp) \<and> Plane_sameside (Li o1 h1) l11 l1
Def (Ang (An l11 o1 h1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
[PROOF STEP]
have P13 : "Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp) \<and> Bet_Point (Se h2 k2) o2 \<and> Def (Ang (An l2 o2 h2)) \<and> Def (Ang (An l2 o2 k2))
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp) \<and> Plane_sameside (Li o1 h1) l11 l1
Def (Ang (An l11 o1 h1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)
[PROOF STEP]
by (blast intro:Ang_rev Ang_trans)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P7 P9 P10 P12 P13
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An l11 o1 h1))
Def (Ang (An h2 o2 l2))
Def (Ang (An h1 o1 l11))
Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An h1 o1 l11)) add Emp)
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)
[PROOF STEP]
have P14 : "Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l11)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An l11 o1 h1))
Def (Ang (An h2 o2 l2))
Def (Ang (An h1 o1 l11))
Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An h1 o1 l11)) add Emp)
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l11)) add Emp)
[PROOF STEP]
by (blast intro:Ang_rev Ang_trans)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l11)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P1 P2 P9 P10 P14
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp) \<and> Bet_Point (Se h2 k2) o2 \<and> Def (Ang (An l2 o2 h2)) \<and> Def (Ang (An l2 o2 k2))
Def (Ang (An h2 o2 l2))
Def (Ang (An h1 o1 l11))
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l11)) add Emp)
[PROOF STEP]
have P15 : "Cong (Geos (Ang (An l2 o2 k2)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp) \<and> Bet_Point (Se h2 k2) o2 \<and> Def (Ang (An l2 o2 h2)) \<and> Def (Ang (An l2 o2 k2))
Def (Ang (An h2 o2 l2))
Def (Ang (An h1 o1 l11))
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l11)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An l2 o2 k2)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)
[PROOF STEP]
by (simp add:Ang_complementary)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An l2 o2 k2)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P1 P4 P7
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp) \<and> Plane_sameside (Li o1 h1) l11 l1
Def (Ang (An l11 o1 h1))
[PROOF STEP]
have P16 : "Eq (Geos (Lin (Li o1 l11)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l1 o1 h1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp) \<and> Plane_sameside (Li o1 h1) l11 l1
Def (Ang (An l11 o1 h1))

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o1 l11)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l1 o1 h1)) add Emp)
[PROOF STEP]
by (simp add:Ang_move_unique_inv)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li o1 l11)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l1 o1 h1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P1 P2 P4 P7 P16
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp) \<and> Bet_Point (Se h2 k2) o2 \<and> Def (Ang (An l2 o2 h2)) \<and> Def (Ang (An l2 o2 k2))
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp) \<and> Plane_sameside (Li o1 h1) l11 l1
Def (Ang (An l11 o1 h1))
Eq (Geos (Lin (Li o1 l11)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l1 o1 h1)) add Emp)
[PROOF STEP]
have "Eq (Geos (Lin (Li o1 l11)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp) \<and> Bet_Point (Se h2 k2) o2 \<and> Def (Ang (An l2 o2 h2)) \<and> Def (Ang (An l2 o2 k2))
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp) \<and> Plane_sameside (Li o1 h1) l11 l1
Def (Ang (An l11 o1 h1))
Eq (Geos (Lin (Li o1 l11)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l1 o1 h1)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o1 l11)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
by (blast intro:Ang_trans Ang_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li o1 l11)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li o1 l11)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
have P17 : "\<not> Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp) \<Longrightarrow>
    \<not> Eq (Geos (Lin (Li o1 l11)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li o1 l11)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)

goal (1 subgoal):
 1. \<not> Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp) \<Longrightarrow> \<not> Eq (Geos (Lin (Li o1 l11)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp) \<Longrightarrow> \<not> Eq (Geos (Lin (Li o1 l11)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P1 P4 P7 P17
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp) \<and> Plane_sameside (Li o1 h1) l11 l1
Def (Ang (An l11 o1 h1))
\<not> Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp) \<Longrightarrow> \<not> Eq (Geos (Lin (Li o1 l11)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
have P18 : "\<not> Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp) \<Longrightarrow>
    Ang_inside (An l11 o1 h1) l1 \<and> \<not> Ang_inside (An l1 o1 h1) l11
    \<or> \<not> Ang_inside (An l11 o1 h1) l1 \<and> Ang_inside (An l1 o1 h1) l11"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp) \<and> Plane_sameside (Li o1 h1) l11 l1
Def (Ang (An l11 o1 h1))
\<not> Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp) \<Longrightarrow> \<not> Eq (Geos (Lin (Li o1 l11)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)

goal (1 subgoal):
 1. \<not> Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp) \<Longrightarrow> Ang_inside (An l11 o1 h1) l1 \<and> \<not> Ang_inside (An l1 o1 h1) l11 \<or> \<not> Ang_inside (An l11 o1 h1) l1 \<and> Ang_inside (An l1 o1 h1) l11
[PROOF STEP]
by (simp add:Ang_inside_case)
[PROOF STATE]
proof (state)
this:
\<not> Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp) \<Longrightarrow> Ang_inside (An l11 o1 h1) l1 \<and> \<not> Ang_inside (An l1 o1 h1) l11 \<or> \<not> Ang_inside (An l11 o1 h1) l1 \<and> Ang_inside (An l1 o1 h1) l11

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P4
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp) \<and> Plane_sameside (Li o1 h1) l11 l1
[PROOF STEP]
have P19 : "Plane_sameside (Li o1 h1) l1 l11"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp) \<and> Plane_sameside (Li o1 h1) l11 l1

goal (1 subgoal):
 1. Plane_sameside (Li o1 h1) l1 l11
[PROOF STEP]
by (simp add:Plane_sameside_rev)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li o1 h1) l1 l11

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
have P20 : "Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 h1)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 h1)) add Emp)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 h1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P19 P20
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li o1 h1) l1 l11
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 h1)) add Emp)
[PROOF STEP]
have P21 : "Ang_inside (An l11 o1 h1) l1 \<Longrightarrow>
    Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l1 o1 h1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li o1 h1) l1 l11
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 h1)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An l11 o1 h1) l1 \<Longrightarrow> Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l1 o1 h1)) add Emp)
[PROOF STEP]
by (simp add:Ang_greater_def)
[PROOF STATE]
proof (state)
this:
Ang_inside (An l11 o1 h1) l1 \<Longrightarrow> Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l1 o1 h1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))
[PROOF STEP]
have P22 : "Line_on (Li o1 h1) k1"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))

goal (1 subgoal):
 1. Line_on (Li o1 h1) k1
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li o1 h1) k1

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
have P23 : "Line_on (Li o1 h1) o1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o1 h1) o1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o1 h1) o1

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
have P24 : "Line_on (Li o1 k1) k1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o1 k1) k1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o1 k1) k1

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
have P25 : "Line_on (Li o1 k1) o1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o1 k1) o1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o1 k1) o1

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))
[PROOF STEP]
have P26 : "Bet_Point (Se h1 k1) o1"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))

goal (1 subgoal):
 1. Bet_Point (Se h1 k1) o1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Bet_Point (Se h1 k1) o1

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se h1 k1) o1
[PROOF STEP]
have P27 : "\<not> Eq (Geos (Poi k1) add Emp) (Geos (Poi o1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se h1 k1) o1

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P22 P23 P24 P25 P27
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li o1 h1) k1
Line_on (Li o1 h1) o1
Line_on (Li o1 k1) k1
Line_on (Li o1 k1) o1
\<not> Eq (Geos (Poi k1) add Emp) (Geos (Poi o1) add Emp)
[PROOF STEP]
have P28 : "Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li o1 h1) k1
Line_on (Li o1 h1) o1
Line_on (Li o1 k1) k1
Line_on (Li o1 k1) o1
\<not> Eq (Geos (Poi k1) add Emp) (Geos (Poi o1) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P19 P28
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li o1 h1) l1 l11
Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
[PROOF STEP]
have P29 : "Plane_sameside (Li o1 k1) l1 l11"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li o1 h1) l1 l11
Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)

goal (1 subgoal):
 1. Plane_sameside (Li o1 k1) l1 l11
[PROOF STEP]
by (simp add:Plane_Line_trans)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li o1 k1) l1 l11

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li o1 k1) l1 l11
[PROOF STEP]
have P30 : "Plane_sameside (Li o1 k1) l11 l1"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li o1 k1) l1 l11

goal (1 subgoal):
 1. Plane_sameside (Li o1 k1) l11 l1
[PROOF STEP]
by (simp add:Plane_sameside_rev)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li o1 k1) l11 l1

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li o1 k1) l11 l1
[PROOF STEP]
have P31 : "\<not> Line_on (Li o1 k1) l11"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li o1 k1) l11 l1

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))
[PROOF STEP]
have P32 : "\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi k1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P31 P32
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li o1 k1) l11
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi k1) add Emp)
[PROOF STEP]
have "Def (Ang (An o1 k1 l11))"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li o1 k1) l11
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi k1) add Emp)

goal (1 subgoal):
 1. Def (Ang (An o1 k1 l11))
[PROOF STEP]
by (simp add:Ang_sinple_def)
[PROOF STATE]
proof (state)
this:
Def (Ang (An o1 k1 l11))

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An o1 k1 l11))
[PROOF STEP]
have P33 : "Def (Ang (An l11 o1 k1))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An o1 k1 l11))

goal (1 subgoal):
 1. Def (Ang (An l11 o1 k1))
[PROOF STEP]
by (blast intro:Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An l11 o1 k1))

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P2 P7 P8 P15 P33
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp) \<and> Bet_Point (Se h2 k2) o2 \<and> Def (Ang (An l2 o2 h2)) \<and> Def (Ang (An l2 o2 k2))
Def (Ang (An l11 o1 h1))
Cong (Geos (Ang (An l2 o2 k2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)
Cong (Geos (Ang (An l2 o2 k2)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)
Def (Ang (An l11 o1 k1))
[PROOF STEP]
have P34 : "Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp) \<and> Bet_Point (Se h2 k2) o2 \<and> Def (Ang (An l2 o2 h2)) \<and> Def (Ang (An l2 o2 k2))
Def (Ang (An l11 o1 h1))
Cong (Geos (Ang (An l2 o2 k2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)
Cong (Geos (Ang (An l2 o2 k2)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)
Def (Ang (An l11 o1 k1))

goal (1 subgoal):
 1. Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)
[PROOF STEP]
by (blast intro:Ang_rev Ang_trans)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))
[PROOF STEP]
have P35 : "Def (Ang (An l1 o1 h1))"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))

goal (1 subgoal):
 1. Def (Ang (An l1 o1 h1))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Def (Ang (An l1 o1 h1))

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P26 P35
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se h1 k1) o1
Def (Ang (An l1 o1 h1))
[PROOF STEP]
have P36 : "Ang_inside (An l11 o1 h1) l1 \<Longrightarrow> Ang_inside (An l1 o1 k1) l11"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se h1 k1) o1
Def (Ang (An l1 o1 h1))

goal (1 subgoal):
 1. Ang_inside (An l11 o1 h1) l1 \<Longrightarrow> Ang_inside (An l1 o1 k1) l11
[PROOF STEP]
by (simp add:Ang_complementary_inside)
[PROOF STATE]
proof (state)
this:
Ang_inside (An l11 o1 h1) l1 \<Longrightarrow> Ang_inside (An l1 o1 k1) l11

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
have P37 : "Cong (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P30 P36 P37
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li o1 k1) l11 l1
Ang_inside (An l11 o1 h1) l1 \<Longrightarrow> Ang_inside (An l1 o1 k1) l11
Cong (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)
[PROOF STEP]
have P38 : "Ang_inside (An l11 o1 h1) l1 \<Longrightarrow>
    Gr (Geos (Ang (An l1 o1 k1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li o1 k1) l11 l1
Ang_inside (An l11 o1 h1) l1 \<Longrightarrow> Ang_inside (An l1 o1 k1) l11
Cong (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An l11 o1 h1) l1 \<Longrightarrow> Gr (Geos (Ang (An l1 o1 k1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)
[PROOF STEP]
by (simp add:Ang_greater_def)
[PROOF STATE]
proof (state)
this:
Ang_inside (An l11 o1 h1) l1 \<Longrightarrow> Gr (Geos (Ang (An l1 o1 k1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P1 P7 P21
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))
Def (Ang (An l11 o1 h1))
Ang_inside (An l11 o1 h1) l1 \<Longrightarrow> Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l1 o1 h1)) add Emp)
[PROOF STEP]
have P39 : "Ang_inside (An l11 o1 h1) l1 \<Longrightarrow>
    Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))
Def (Ang (An l11 o1 h1))
Ang_inside (An l11 o1 h1) l1 \<Longrightarrow> Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l1 o1 h1)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An l11 o1 h1) l1 \<Longrightarrow> Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp)
[PROOF STEP]
by (blast intro:Ang_Gr_trans_Gr_Eq)
[PROOF STATE]
proof (state)
this:
Ang_inside (An l11 o1 h1) l1 \<Longrightarrow> Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P1 P7 P33 P38 P39
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))
Def (Ang (An l11 o1 h1))
Def (Ang (An l11 o1 k1))
Ang_inside (An l11 o1 h1) l1 \<Longrightarrow> Gr (Geos (Ang (An l1 o1 k1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)
Ang_inside (An l11 o1 h1) l1 \<Longrightarrow> Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp)
[PROOF STEP]
have P40 : "Ang_inside (An l11 o1 h1) l1 \<Longrightarrow>
    Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))
Def (Ang (An l11 o1 h1))
Def (Ang (An l11 o1 k1))
Ang_inside (An l11 o1 h1) l1 \<Longrightarrow> Gr (Geos (Ang (An l1 o1 k1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)
Ang_inside (An l11 o1 h1) l1 \<Longrightarrow> Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An l11 o1 h1) l1 \<Longrightarrow> Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)
[PROOF STEP]
by (blast intro:Ang_Gr_trans_Gr_Gr)
[PROOF STATE]
proof (state)
this:
Ang_inside (An l11 o1 h1) l1 \<Longrightarrow> Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P7 P33
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An l11 o1 h1))
Def (Ang (An l11 o1 k1))
[PROOF STEP]
have P41 :
    "Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)
    \<and> \<not> Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)
    \<and> \<not> Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)
    \<or> \<not> Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)
    \<and> Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)
    \<and> \<not> Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)
    \<or> \<not> Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)
    \<and> \<not> Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)
    \<and> Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An l11 o1 h1))
Def (Ang (An l11 o1 k1))

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P40 P41
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An l11 o1 h1) l1 \<Longrightarrow> Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)
Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp) \<and> \<not> Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp) \<and> \<not> Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp) \<or> \<not> Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp) \<and> Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp) \<and> \<not> Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp) \<or> \<not> Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp) \<and> \<not> Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp) \<and> Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)
[PROOF STEP]
have P42 : "Ang_inside (An l11 o1 h1) l1 \<Longrightarrow>
    \<not> Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An l11 o1 h1) l1 \<Longrightarrow> Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)
Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp) \<and> \<not> Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp) \<and> \<not> Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp) \<or> \<not> Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp) \<and> Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp) \<and> \<not> Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp) \<or> \<not> Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp) \<and> \<not> Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp) \<and> Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An l11 o1 h1) l1 \<Longrightarrow> \<not> Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Ang_inside (An l11 o1 h1) l1 \<Longrightarrow> \<not> Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P34 P42
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)
Ang_inside (An l11 o1 h1) l1 \<Longrightarrow> \<not> Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)
[PROOF STEP]
have P43 : "\<not> Ang_inside (An l11 o1 h1) l1"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)
Ang_inside (An l11 o1 h1) l1 \<Longrightarrow> \<not> Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)

goal (1 subgoal):
 1. \<not> Ang_inside (An l11 o1 h1) l1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Ang_inside (An l11 o1 h1) l1

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
have P44 : "Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P4 P44
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp) \<and> Plane_sameside (Li o1 h1) l11 l1
Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)
[PROOF STEP]
have P45 : "Ang_inside (An l1 o1 h1) l11 \<Longrightarrow>
    Gr (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp) \<and> Plane_sameside (Li o1 h1) l11 l1
Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An l1 o1 h1) l11 \<Longrightarrow> Gr (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)
[PROOF STEP]
by (simp add:Ang_greater_def)
[PROOF STATE]
proof (state)
this:
Ang_inside (An l1 o1 h1) l11 \<Longrightarrow> Gr (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P1 P7
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))
Def (Ang (An l11 o1 h1))
[PROOF STEP]
have P46 : "Ang_inside (An l1 o1 h1) l11 \<Longrightarrow> Ang_inside (An l11 o1 k1) l1"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))
Def (Ang (An l11 o1 h1))

goal (1 subgoal):
 1. Ang_inside (An l1 o1 h1) l11 \<Longrightarrow> Ang_inside (An l11 o1 k1) l1
[PROOF STEP]
by (simp add:Ang_complementary_inside)
[PROOF STATE]
proof (state)
this:
Ang_inside (An l1 o1 h1) l11 \<Longrightarrow> Ang_inside (An l11 o1 k1) l1

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
have P47 : "Cong (Geos (Ang (An l1 o1 k1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 k1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An l1 o1 k1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P29 P46 P47
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li o1 k1) l1 l11
Ang_inside (An l1 o1 h1) l11 \<Longrightarrow> Ang_inside (An l11 o1 k1) l1
Cong (Geos (Ang (An l1 o1 k1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp)
[PROOF STEP]
have P48 : "Ang_inside (An l1 o1 h1) l11 \<Longrightarrow>
    Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li o1 k1) l1 l11
Ang_inside (An l1 o1 h1) l11 \<Longrightarrow> Ang_inside (An l11 o1 k1) l1
Cong (Geos (Ang (An l1 o1 k1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An l1 o1 h1) l11 \<Longrightarrow> Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp)
[PROOF STEP]
by (simp add:Ang_greater_def)
[PROOF STATE]
proof (state)
this:
Ang_inside (An l1 o1 h1) l11 \<Longrightarrow> Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P1 P33 P48
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))
Def (Ang (An l11 o1 k1))
Ang_inside (An l1 o1 h1) l11 \<Longrightarrow> Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp)
[PROOF STEP]
have P49 : "Ang_inside (An l1 o1 h1) l11 \<Longrightarrow>
    Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l1 o1 h1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))
Def (Ang (An l11 o1 k1))
Ang_inside (An l1 o1 h1) l11 \<Longrightarrow> Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An l1 o1 h1) l11 \<Longrightarrow> Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l1 o1 h1)) add Emp)
[PROOF STEP]
by (blast intro:Ang_Gr_trans_Gr_Eq Ang_rev)
[PROOF STATE]
proof (state)
this:
Ang_inside (An l1 o1 h1) l11 \<Longrightarrow> Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l1 o1 h1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P1 P7 P33 P45 P49
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))
Def (Ang (An l11 o1 h1))
Def (Ang (An l11 o1 k1))
Ang_inside (An l1 o1 h1) l11 \<Longrightarrow> Gr (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)
Ang_inside (An l1 o1 h1) l11 \<Longrightarrow> Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l1 o1 h1)) add Emp)
[PROOF STEP]
have P50 : "Ang_inside (An l1 o1 h1) l11 \<Longrightarrow>
    Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp) \<and> Bet_Point (Se h1 k1) o1 \<and> Def (Ang (An l1 o1 h1)) \<and> Def (Ang (An l1 o1 k1))
Def (Ang (An l11 o1 h1))
Def (Ang (An l11 o1 k1))
Ang_inside (An l1 o1 h1) l11 \<Longrightarrow> Gr (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)
Ang_inside (An l1 o1 h1) l11 \<Longrightarrow> Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l1 o1 h1)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An l1 o1 h1) l11 \<Longrightarrow> Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)
[PROOF STEP]
by (blast intro:Ang_Gr_trans_Gr_Gr)
[PROOF STATE]
proof (state)
this:
Ang_inside (An l1 o1 h1) l11 \<Longrightarrow> Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P41 P50
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp) \<and> \<not> Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp) \<and> \<not> Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp) \<or> \<not> Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp) \<and> Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp) \<and> \<not> Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp) \<or> \<not> Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp) \<and> \<not> Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp) \<and> Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)
Ang_inside (An l1 o1 h1) l11 \<Longrightarrow> Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)
[PROOF STEP]
have P51 : "Ang_inside (An l1 o1 h1) l11 \<Longrightarrow>
    \<not> Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp) \<and> \<not> Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp) \<and> \<not> Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp) \<or> \<not> Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp) \<and> Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp) \<and> \<not> Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp) \<or> \<not> Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp) \<and> \<not> Gr (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp) \<and> Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)
Ang_inside (An l1 o1 h1) l11 \<Longrightarrow> Gr (Geos (Ang (An l11 o1 k1)) add Emp) (Geos (Ang (An l11 o1 h1)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An l1 o1 h1) l11 \<Longrightarrow> \<not> Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Ang_inside (An l1 o1 h1) l11 \<Longrightarrow> \<not> Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P34 P51
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)
Ang_inside (An l1 o1 h1) l11 \<Longrightarrow> \<not> Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)
[PROOF STEP]
have P52 : "\<not> Ang_inside (An l1 o1 h1) l11"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)
Ang_inside (An l1 o1 h1) l11 \<Longrightarrow> \<not> Cong (Geos (Ang (An l11 o1 h1)) add Emp) (Geos (Ang (An l11 o1 k1)) add Emp)

goal (1 subgoal):
 1. \<not> Ang_inside (An l1 o1 h1) l11
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Ang_inside (An l1 o1 h1) l11

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
from P18 P43 P52
[PROOF STATE]
proof (chain)
picking this:
\<not> Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp) \<Longrightarrow> Ang_inside (An l11 o1 h1) l1 \<and> \<not> Ang_inside (An l1 o1 h1) l11 \<or> \<not> Ang_inside (An l11 o1 h1) l1 \<and> Ang_inside (An l1 o1 h1) l11
\<not> Ang_inside (An l11 o1 h1) l1
\<not> Ang_inside (An l1 o1 h1) l11
[PROOF STEP]
show "Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp) \<Longrightarrow> Ang_inside (An l11 o1 h1) l1 \<and> \<not> Ang_inside (An l1 o1 h1) l11 \<or> \<not> Ang_inside (An l11 o1 h1) l1 \<and> Ang_inside (An l1 o1 h1) l11
\<not> Ang_inside (An l11 o1 h1) l1
\<not> Ang_inside (An l1 o1 h1) l11

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)

goal:
No subgoals!
[PROOF STEP]
qed