[STATEMENT]
theorem (in Congruence_Rule) Ang_move_Greater :
  assumes
    "Def (Ang (An h1 o1 k1))" "Def (Ang (An h2 o2 l2))"
    "Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)"
    "Plane_sameside (Li o2 h2) k2 l2"
    "Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)"
    "Plane_sameside (Li o1 h1) k1 l1"
    "Ang_inside (An h2 o2 l2) k2"
  shows
    "\<not> Ang_inside (An h1 o1 k1) l1"
    "\<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Ang_inside (An h1 o1 k1) l1 &&& \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Plane_sameside (Li o2 h2) k2 l2
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Plane_sameside (Li o1 h1) k1 l1
Ang_inside (An h2 o2 l2) k2
[PROOF STEP]
have P1 : "\<not> Line_on (Li o2 h2) k2"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Plane_sameside (Li o2 h2) k2 l2
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Plane_sameside (Li o1 h1) k1 l1
Ang_inside (An h2 o2 l2) k2

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

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Plane_sameside (Li o2 h2) k2 l2
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Plane_sameside (Li o1 h1) k1 l1
Ang_inside (An h2 o2 l2) k2
[PROOF STEP]
have "\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi o2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Plane_sameside (Li o2 h2) k2 l2
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Plane_sameside (Li o1 h1) k1 l1
Ang_inside (An h2 o2 l2) k2

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

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi o2) add Emp)
[PROOF STEP]
have P2 : "\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi o2) add Emp)

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

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from P1 P2
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li o2 h2) k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h2) add Emp)
[PROOF STEP]
have "Def (Ang (An o2 h2 k2))"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li o2 h2) k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h2) add Emp)

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

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An o2 h2 k2))
[PROOF STEP]
have P3 : "Def (Ang (An h2 o2 k2))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An o2 h2 k2))

goal (1 subgoal):
 1. Def (Ang (An h2 o2 k2))
[PROOF STEP]
by (blast intro:Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An h2 o2 k2))

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from assms P3
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Plane_sameside (Li o2 h2) k2 l2
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Plane_sameside (Li o1 h1) k1 l1
Ang_inside (An h2 o2 l2) k2
Def (Ang (An h2 o2 k2))
[PROOF STEP]
have "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<exists>p. Ang_inside (An h2 o2 k2) p
    \<and> Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 p)) add Emp)
    \<and> Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 p)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Plane_sameside (Li o2 h2) k2 l2
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Plane_sameside (Li o1 h1) k1 l1
Ang_inside (An h2 o2 l2) k2
Def (Ang (An h2 o2 k2))

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<exists>p. Ang_inside (An h2 o2 k2) p \<and> Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 p)) add Emp) \<and> Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 p)) add Emp)
[PROOF STEP]
by (simp add:Ang_split)
[PROOF STATE]
proof (state)
this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<exists>p. Ang_inside (An h2 o2 k2) p \<and> Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 p)) add Emp) \<and> Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 p)) add Emp)

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<exists>p. Ang_inside (An h2 o2 k2) p \<and> Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 p)) add Emp) \<and> Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 p)) add Emp)
[PROOF STEP]
obtain l21 :: Point where P4 : "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Ang_inside (An h2 o2 k2) l21
    \<and> Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l21)) add Emp)
    \<and> Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l21)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<exists>p. Ang_inside (An h2 o2 k2) p \<and> Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 p)) add Emp) \<and> Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 p)) add Emp)

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

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Ang_inside (An h2 o2 k2) l21 \<and> Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l21)) add Emp) \<and> Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l21)) add Emp)
[PROOF STEP]
have P5 : "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow>
    Plane_sameside (Li o2 k2) h2 l21 \<and> Plane_sameside (Li o2 h2) k2 l21"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Ang_inside (An h2 o2 k2) l21 \<and> Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l21)) add Emp) \<and> Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l21)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Plane_sameside (Li o2 k2) h2 l21 \<and> Plane_sameside (Li o2 h2) k2 l21
[PROOF STEP]
by (simp add:Ang_inside_def)
[PROOF STATE]
proof (state)
this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Plane_sameside (Li o2 k2) h2 l21 \<and> Plane_sameside (Li o2 h2) k2 l21

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Plane_sameside (Li o2 h2) k2 l2
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Plane_sameside (Li o1 h1) k1 l1
Ang_inside (An h2 o2 l2) k2
[PROOF STEP]
have P6 : "Plane_diffside (Li o2 k2) h2 l2"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Plane_sameside (Li o2 h2) k2 l2
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Plane_sameside (Li o1 h1) k1 l1
Ang_inside (An h2 o2 l2) k2

goal (1 subgoal):
 1. Plane_diffside (Li o2 k2) h2 l2
[PROOF STEP]
by (simp add:Ang_inside_Planeside)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li o2 k2) h2 l2

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from P5 P6
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Plane_sameside (Li o2 k2) h2 l21 \<and> Plane_sameside (Li o2 h2) k2 l21
Plane_diffside (Li o2 k2) h2 l2
[PROOF STEP]
have "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow>
    Plane_diffside (Li o2 k2) l21 l2"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Plane_sameside (Li o2 k2) h2 l21 \<and> Plane_sameside (Li o2 h2) k2 l21
Plane_diffside (Li o2 k2) h2 l2

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Plane_diffside (Li o2 k2) l21 l2
[PROOF STEP]
by (blast intro:Plane_trans)
[PROOF STATE]
proof (state)
this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Plane_diffside (Li o2 k2) l21 l2

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Plane_diffside (Li o2 k2) l21 l2
[PROOF STEP]
have "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<exists>p. Bet_Point (Se l21 l2) p \<and> Line_on (Li o2 k2) p
    \<and> \<not> Line_on (Li o2 k2) l21 \<and> \<not> Line_on (Li o2 k2) l2"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Plane_diffside (Li o2 k2) l21 l2

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<exists>p. Bet_Point (Se l21 l2) p \<and> Line_on (Li o2 k2) p \<and> \<not> Line_on (Li o2 k2) l21 \<and> \<not> Line_on (Li o2 k2) l2
[PROOF STEP]
by (simp add:Plane_diffside_def)
[PROOF STATE]
proof (state)
this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<exists>p. Bet_Point (Se l21 l2) p \<and> Line_on (Li o2 k2) p \<and> \<not> Line_on (Li o2 k2) l21 \<and> \<not> Line_on (Li o2 k2) l2

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<exists>p. Bet_Point (Se l21 l2) p \<and> Line_on (Li o2 k2) p \<and> \<not> Line_on (Li o2 k2) l21 \<and> \<not> Line_on (Li o2 k2) l2
[PROOF STEP]
obtain pn :: Point where P7 : "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow>
    Bet_Point (Se l21 l2) pn \<and> Line_on (Li o2 k2) pn
    \<and> \<not> Line_on (Li o2 k2) l21 \<and> \<not> Line_on (Li o2 k2) l2"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<exists>p. Bet_Point (Se l21 l2) p \<and> Line_on (Li o2 k2) p \<and> \<not> Line_on (Li o2 k2) l21 \<and> \<not> Line_on (Li o2 k2) l2

goal (1 subgoal):
 1. (\<And>pn. (Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Bet_Point (Se l21 l2) pn \<and> Line_on (Li o2 k2) pn \<and> \<not> Line_on (Li o2 k2) l21 \<and> \<not> Line_on (Li o2 k2) l2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Bet_Point (Se l21 l2) pn \<and> Line_on (Li o2 k2) pn \<and> \<not> Line_on (Li o2 k2) l21 \<and> \<not> Line_on (Li o2 k2) l2

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Bet_Point (Se l21 l2) pn \<and> Line_on (Li o2 k2) pn \<and> \<not> Line_on (Li o2 k2) l21 \<and> \<not> Line_on (Li o2 k2) l2
[PROOF STEP]
have P8 : "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Bet_Point (Se l21 l2) pn"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Bet_Point (Se l21 l2) pn \<and> Line_on (Li o2 k2) pn \<and> \<not> Line_on (Li o2 k2) l21 \<and> \<not> Line_on (Li o2 k2) l2

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Bet_Point (Se l21 l2) pn
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Bet_Point (Se l21 l2) pn

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Bet_Point (Se l21 l2) pn
[PROOF STEP]
have P9 : "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow>
    \<not> Eq (Geos (Poi l21) add Emp) (Geos (Poi l2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Bet_Point (Se l21 l2) pn

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

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Plane_sameside (Li o2 h2) k2 l2
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Plane_sameside (Li o1 h1) k1 l1
Ang_inside (An h2 o2 l2) k2
[PROOF STEP]
have P10 : "Plane_sameside (Li o2 h2) l2 k2"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Plane_sameside (Li o2 h2) k2 l2
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Plane_sameside (Li o1 h1) k1 l1
Ang_inside (An h2 o2 l2) k2

goal (1 subgoal):
 1. Plane_sameside (Li o2 h2) l2 k2
[PROOF STEP]
by (simp add:Plane_sameside_rev)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li o2 h2) l2 k2

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from P5 P9 P10
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Plane_sameside (Li o2 k2) h2 l21 \<and> Plane_sameside (Li o2 h2) k2 l21
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<not> Eq (Geos (Poi l21) add Emp) (Geos (Poi l2) add Emp)
Plane_sameside (Li o2 h2) l2 k2
[PROOF STEP]
have P11 : "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Plane_sameside (Li o2 h2) l2 l21"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Plane_sameside (Li o2 k2) h2 l21 \<and> Plane_sameside (Li o2 h2) k2 l21
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<not> Eq (Geos (Poi l21) add Emp) (Geos (Poi l2) add Emp)
Plane_sameside (Li o2 h2) l2 k2

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Plane_sameside (Li o2 h2) l2 l21
[PROOF STEP]
by (blast intro:Plane_sameside_trans)
[PROOF STATE]
proof (state)
this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Plane_sameside (Li o2 h2) l2 l21

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from P8
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Bet_Point (Se l21 l2) pn
[PROOF STEP]
have P12 : "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow>
    Eq (Geos (Poi pn) add Emp) (Geos (Poi o2) add Emp) \<Longrightarrow> Bet_Point (Se l21 l2) o2"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Bet_Point (Se l21 l2) pn

goal (1 subgoal):
 1. \<lbrakk>Ang_inside (An h1 o1 k1) l1; Eq (Geos (Poi pn) add Emp) (Geos (Poi o2) add Emp)\<rbrakk> \<Longrightarrow> Bet_Point (Se l21 l2) o2
[PROOF STEP]
by (simp add:Point_Eq)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Ang_inside (An h1 o1 k1) l1; Eq (Geos (Poi pn) add Emp) (Geos (Poi o2) add Emp)\<rbrakk> \<Longrightarrow> Bet_Point (Se l21 l2) o2

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
have P13 : "Line_on (Li o2 h2) o2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o2 h2) o2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o2 h2) o2

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
have P14 : "Line_on (Li l21 l2) l2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li l21 l2) l2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li l21 l2) l2

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from P14
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li l21 l2) l2
[PROOF STEP]
have P15 : "Eq (Geos (Lin (Li l21 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp) \<Longrightarrow>
    Line_on (Li o2 h2) l2"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li l21 l2) l2

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

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Plane_sameside (Li o2 h2) k2 l2
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Plane_sameside (Li o1 h1) k1 l1
Ang_inside (An h2 o2 l2) k2
[PROOF STEP]
have "Def (Tri (Tr o2 h2 l2))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Plane_sameside (Li o2 h2) k2 l2
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Plane_sameside (Li o1 h1) k1 l1
Ang_inside (An h2 o2 l2) k2

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

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr o2 h2 l2))
[PROOF STEP]
have P16 : "\<not> Line_on (Li o2 h2) l2"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr o2 h2 l2))

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

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from P15 P16
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li l21 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp) \<Longrightarrow> Line_on (Li o2 h2) l2
\<not> Line_on (Li o2 h2) l2
[PROOF STEP]
have P17 : "\<not> Eq (Geos (Lin (Li l21 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li l21 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp) \<Longrightarrow> Line_on (Li o2 h2) l2
\<not> Line_on (Li o2 h2) l2

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li l21 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Lin (Li l21 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp)

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from P12 P13 P17
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>Ang_inside (An h1 o1 k1) l1; Eq (Geos (Poi pn) add Emp) (Geos (Poi o2) add Emp)\<rbrakk> \<Longrightarrow> Bet_Point (Se l21 l2) o2
Line_on (Li o2 h2) o2
\<not> Eq (Geos (Lin (Li l21 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp)
[PROOF STEP]
have "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow>
    Eq (Geos (Poi pn) add Emp) (Geos (Poi o2) add Emp) \<Longrightarrow>
    Plane_diffside (Li o2 h2) l2 l21"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Ang_inside (An h1 o1 k1) l1; Eq (Geos (Poi pn) add Emp) (Geos (Poi o2) add Emp)\<rbrakk> \<Longrightarrow> Bet_Point (Se l21 l2) o2
Line_on (Li o2 h2) o2
\<not> Eq (Geos (Lin (Li l21 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp)

goal (1 subgoal):
 1. \<lbrakk>Ang_inside (An h1 o1 k1) l1; Eq (Geos (Poi pn) add Emp) (Geos (Poi o2) add Emp)\<rbrakk> \<Longrightarrow> Plane_diffside (Li o2 h2) l2 l21
[PROOF STEP]
by (simp add:Plane_Bet_diffside Plane_diffside_rev)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Ang_inside (An h1 o1 k1) l1; Eq (Geos (Poi pn) add Emp) (Geos (Poi o2) add Emp)\<rbrakk> \<Longrightarrow> Plane_diffside (Li o2 h2) l2 l21

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>Ang_inside (An h1 o1 k1) l1; Eq (Geos (Poi pn) add Emp) (Geos (Poi o2) add Emp)\<rbrakk> \<Longrightarrow> Plane_diffside (Li o2 h2) l2 l21
[PROOF STEP]
have P18 : "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow>
    Eq (Geos (Poi pn) add Emp) (Geos (Poi o2) add Emp) \<Longrightarrow>
    \<not> Plane_sameside (Li o2 h2) l2 l21"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Ang_inside (An h1 o1 k1) l1; Eq (Geos (Poi pn) add Emp) (Geos (Poi o2) add Emp)\<rbrakk> \<Longrightarrow> Plane_diffside (Li o2 h2) l2 l21

goal (1 subgoal):
 1. \<lbrakk>Ang_inside (An h1 o1 k1) l1; Eq (Geos (Poi pn) add Emp) (Geos (Poi o2) add Emp)\<rbrakk> \<Longrightarrow> \<not> Plane_sameside (Li o2 h2) l2 l21
[PROOF STEP]
by (simp add:Plane_diffside_not_sameside)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Ang_inside (An h1 o1 k1) l1; Eq (Geos (Poi pn) add Emp) (Geos (Poi o2) add Emp)\<rbrakk> \<Longrightarrow> \<not> Plane_sameside (Li o2 h2) l2 l21

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from P11 P18
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Plane_sameside (Li o2 h2) l2 l21
\<lbrakk>Ang_inside (An h1 o1 k1) l1; Eq (Geos (Poi pn) add Emp) (Geos (Poi o2) add Emp)\<rbrakk> \<Longrightarrow> \<not> Plane_sameside (Li o2 h2) l2 l21
[PROOF STEP]
have P19 : "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow>
    \<not> Eq (Geos (Poi pn) add Emp) (Geos (Poi o2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Plane_sameside (Li o2 h2) l2 l21
\<lbrakk>Ang_inside (An h1 o1 k1) l1; Eq (Geos (Poi pn) add Emp) (Geos (Poi o2) add Emp)\<rbrakk> \<Longrightarrow> \<not> Plane_sameside (Li o2 h2) l2 l21

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

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
have P20 : "Line_on (Li o2 k2) o2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o2 k2) o2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o2 k2) o2

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from P8
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Bet_Point (Se l21 l2) pn
[PROOF STEP]
have P21 : "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Line_on (Li l21 l2) pn"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Bet_Point (Se l21 l2) pn

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Line_on (Li l21 l2) pn
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Line_on (Li l21 l2) pn

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from P7 P19 P20 P21
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Bet_Point (Se l21 l2) pn \<and> Line_on (Li o2 k2) pn \<and> \<not> Line_on (Li o2 k2) l21 \<and> \<not> Line_on (Li o2 k2) l2
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<not> Eq (Geos (Poi pn) add Emp) (Geos (Poi o2) add Emp)
Line_on (Li o2 k2) o2
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Line_on (Li l21 l2) pn
[PROOF STEP]
have P22 : "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Line_on (Li l21 l2) o2 \<Longrightarrow>
    Eq (Geos (Lin (Li l21 l2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Bet_Point (Se l21 l2) pn \<and> Line_on (Li o2 k2) pn \<and> \<not> Line_on (Li o2 k2) l21 \<and> \<not> Line_on (Li o2 k2) l2
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<not> Eq (Geos (Poi pn) add Emp) (Geos (Poi o2) add Emp)
Line_on (Li o2 k2) o2
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Line_on (Li l21 l2) pn

goal (1 subgoal):
 1. \<lbrakk>Ang_inside (An h1 o1 k1) l1; Line_on (Li l21 l2) o2\<rbrakk> \<Longrightarrow> Eq (Geos (Lin (Li l21 l2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
[PROOF STEP]
by (simp add:Line_unique)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Ang_inside (An h1 o1 k1) l1; Line_on (Li l21 l2) o2\<rbrakk> \<Longrightarrow> Eq (Geos (Lin (Li l21 l2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from P14 P22
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li l21 l2) l2
\<lbrakk>Ang_inside (An h1 o1 k1) l1; Line_on (Li l21 l2) o2\<rbrakk> \<Longrightarrow> Eq (Geos (Lin (Li l21 l2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
[PROOF STEP]
have P23 : "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow>
    Line_on (Li l21 l2) o2 \<Longrightarrow> Line_on (Li o2 k2) l2"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li l21 l2) l2
\<lbrakk>Ang_inside (An h1 o1 k1) l1; Line_on (Li l21 l2) o2\<rbrakk> \<Longrightarrow> Eq (Geos (Lin (Li l21 l2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)

goal (1 subgoal):
 1. \<lbrakk>Ang_inside (An h1 o1 k1) l1; Line_on (Li l21 l2) o2\<rbrakk> \<Longrightarrow> Line_on (Li o2 k2) l2
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Ang_inside (An h1 o1 k1) l1; Line_on (Li l21 l2) o2\<rbrakk> \<Longrightarrow> Line_on (Li o2 k2) l2

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from P7 P23
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Bet_Point (Se l21 l2) pn \<and> Line_on (Li o2 k2) pn \<and> \<not> Line_on (Li o2 k2) l21 \<and> \<not> Line_on (Li o2 k2) l2
\<lbrakk>Ang_inside (An h1 o1 k1) l1; Line_on (Li l21 l2) o2\<rbrakk> \<Longrightarrow> Line_on (Li o2 k2) l2
[PROOF STEP]
have P24 : "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<not> Line_on (Li l21 l2) o2"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Bet_Point (Se l21 l2) pn \<and> Line_on (Li o2 k2) pn \<and> \<not> Line_on (Li o2 k2) l21 \<and> \<not> Line_on (Li o2 k2) l2
\<lbrakk>Ang_inside (An h1 o1 k1) l1; Line_on (Li l21 l2) o2\<rbrakk> \<Longrightarrow> Line_on (Li o2 k2) l2

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<not> Line_on (Li l21 l2) o2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<not> Line_on (Li l21 l2) o2

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from P9 P24
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<not> Eq (Geos (Poi l21) add Emp) (Geos (Poi l2) add Emp)
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<not> Line_on (Li l21 l2) o2
[PROOF STEP]
have "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Def (Ang (An l21 l2 o2))"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<not> Eq (Geos (Poi l21) add Emp) (Geos (Poi l2) add Emp)
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<not> Line_on (Li l21 l2) o2

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Def (Ang (An l21 l2 o2))
[PROOF STEP]
by (simp add:Ang_sinple_def)
[PROOF STATE]
proof (state)
this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Def (Ang (An l21 l2 o2))

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Def (Ang (An l21 l2 o2))
[PROOF STEP]
have P25 : "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Def (Ang (An l21 o2 l2))"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Def (Ang (An l21 l2 o2))

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Def (Ang (An l21 o2 l2))
[PROOF STEP]
by (blast intro:Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Def (Ang (An l21 o2 l2))

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Def (Ang (An l21 o2 l2))
[PROOF STEP]
have P26 : "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow>
    \<not> Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Def (Ang (An l21 o2 l2))

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<not> Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
[PROOF STEP]
by (simp add:Ang_def)
[PROOF STATE]
proof (state)
this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<not> Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
have P27 : "Eq (Geos (Ang (An h2 o2 l21)) add Emp) (Geos (Ang (An l21 o2 h2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An h2 o2 l21)) add Emp) (Geos (Ang (An l21 o2 h2)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An h2 o2 l21)) add Emp) (Geos (Ang (An l21 o2 h2)) add Emp)

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from P4 P27
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Ang_inside (An h2 o2 k2) l21 \<and> Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l21)) add Emp) \<and> Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l21)) add Emp)
Eq (Geos (Ang (An h2 o2 l21)) add Emp) (Geos (Ang (An l21 o2 h2)) add Emp)
[PROOF STEP]
have P28 : "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow>
    Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An l21 o2 h2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Ang_inside (An h2 o2 k2) l21 \<and> Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l21)) add Emp) \<and> Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l21)) add Emp)
Eq (Geos (Ang (An h2 o2 l21)) add Emp) (Geos (Ang (An l21 o2 h2)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An l21 o2 h2)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An l21 o2 h2)) add Emp)

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
have P29 : "Eq (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from assms P29
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Plane_sameside (Li o2 h2) k2 l2
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Plane_sameside (Li o1 h1) k1 l1
Ang_inside (An h2 o2 l2) k2
Eq (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
have P30 : "Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Plane_sameside (Li o2 h2) k2 l2
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Plane_sameside (Li o1 h1) k1 l1
Ang_inside (An h2 o2 l2) k2
Eq (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)

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

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from P11 P28 P30
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Plane_sameside (Li o2 h2) l2 l21
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An l21 o2 h2)) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
have P31 : "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow>
    Eq (Geos (Lin (Li l2 o2)) add Emp) (Geos (Lin (Li l21 o2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Plane_sameside (Li o2 h2) l2 l21
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An l21 o2 h2)) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Eq (Geos (Lin (Li l2 o2)) add Emp) (Geos (Lin (Li l21 o2)) add Emp)
[PROOF STEP]
by (simp add:Ang_move_unique)
[PROOF STATE]
proof (state)
this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Eq (Geos (Lin (Li l2 o2)) add Emp) (Geos (Lin (Li l21 o2)) add Emp)

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from P25
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Def (Ang (An l21 o2 l2))
[PROOF STEP]
have P32 : "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Def (Tri (Tr l21 o2 l2))"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Def (Ang (An l21 o2 l2))

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Def (Tri (Tr l21 o2 l2))
[PROOF STEP]
by (simp add:Ang_to_Tri)
[PROOF STATE]
proof (state)
this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Def (Tri (Tr l21 o2 l2))

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Def (Tri (Tr l21 o2 l2))
[PROOF STEP]
have "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Def (Tri (Tr l21 o2 l2))

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
[PROOF STEP]
by (simp add:Tri_def)
[PROOF STATE]
proof (state)
this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
[PROOF STEP]
have P33 : "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow>
    Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li l2 o2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li l2 o2)) add Emp)
[PROOF STEP]
by (simp add:Line_rev)
[PROOF STATE]
proof (state)
this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li l2 o2)) add Emp)

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from P32
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Def (Tri (Tr l21 o2 l2))
[PROOF STEP]
have "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow>
    \<not> Eq (Geos (Poi l21) add Emp) (Geos (Poi o2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Def (Tri (Tr l21 o2 l2))

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<not> Eq (Geos (Poi l21) add Emp) (Geos (Poi o2) add Emp)
[PROOF STEP]
by (simp add:Tri_def)
[PROOF STATE]
proof (state)
this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<not> Eq (Geos (Poi l21) add Emp) (Geos (Poi o2) add Emp)

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<not> Eq (Geos (Poi l21) add Emp) (Geos (Poi o2) add Emp)
[PROOF STEP]
have P34 : "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow>
    Eq (Geos (Lin (Li l21 o2)) add Emp) (Geos (Lin (Li o2 l21)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<not> Eq (Geos (Poi l21) add Emp) (Geos (Poi o2) add Emp)

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Eq (Geos (Lin (Li l21 o2)) add Emp) (Geos (Lin (Li o2 l21)) add Emp)
[PROOF STEP]
by (simp add:Line_rev)
[PROOF STATE]
proof (state)
this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Eq (Geos (Lin (Li l21 o2)) add Emp) (Geos (Lin (Li o2 l21)) add Emp)

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from P31 P33
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Eq (Geos (Lin (Li l2 o2)) add Emp) (Geos (Lin (Li l21 o2)) add Emp)
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li l2 o2)) add Emp)
[PROOF STEP]
have P35 : "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow>
    Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li l21 o2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Eq (Geos (Lin (Li l2 o2)) add Emp) (Geos (Lin (Li l21 o2)) add Emp)
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li l2 o2)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li l21 o2)) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev Eq_trans)
[PROOF STATE]
proof (state)
this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li l21 o2)) add Emp)

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from P34 P35
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Eq (Geos (Lin (Li l21 o2)) add Emp) (Geos (Lin (Li o2 l21)) add Emp)
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li l21 o2)) add Emp)
[PROOF STEP]
have P36 : "Ang_inside (An h1 o1 k1) l1 \<Longrightarrow>
    Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Eq (Geos (Lin (Li l21 o2)) add Emp) (Geos (Lin (Li o2 l21)) add Emp)
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li l21 o2)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev Eq_trans)
[PROOF STATE]
proof (state)
this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)

goal (2 subgoals):
 1. \<not> Ang_inside (An h1 o1 k1) l1
 2. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from P26 P36
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<not> Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
[PROOF STEP]
show "\<not> Ang_inside (An h1 o1 k1) l1"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> \<not> Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
Ang_inside (An h1 o1 k1) l1 \<Longrightarrow> Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Plane_sameside (Li o2 h2) k2 l2
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Plane_sameside (Li o1 h1) k1 l1
Ang_inside (An h2 o2 l2) k2
[PROOF STEP]
have P37 : "Def (Ang (An k1 o1 h1))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Plane_sameside (Li o2 h2) k2 l2
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Plane_sameside (Li o1 h1) k1 l1
Ang_inside (An h2 o2 l2) k2

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

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

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from P37
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An k1 o1 h1))
[PROOF STEP]
have P39 : "\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi h1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An k1 o1 h1))

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. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from P38 P39
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li o1 h1) l1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi h1) add Emp)
[PROOF STEP]
have "Def (Ang (An o1 h1 l1))"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li o1 h1) l1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi h1) add Emp)

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An o1 h1 l1))
[PROOF STEP]
have P40 : "Def (Ang (An l1 o1 h1))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An o1 h1 l1))

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from assms P37 P40
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Plane_sameside (Li o2 h2) k2 l2
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Plane_sameside (Li o1 h1) k1 l1
Ang_inside (An h2 o2 l2) k2
Def (Ang (An k1 o1 h1))
Def (Ang (An l1 o1 h1))
[PROOF STEP]
have P41 : "Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An k1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 h1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Plane_sameside (Li o2 h2) k2 l2
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Plane_sameside (Li o1 h1) k1 l1
Ang_inside (An h2 o2 l2) k2
Def (Ang (An k1 o1 h1))
Def (Ang (An l1 o1 h1))

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An k1 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 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An k1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 h1)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
have P42 : "Cong (Geos (Ang (An k1 o1 h1)) add Emp) (Geos (Ang (An h1 o1 k1)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An k1 o1 h1)) add Emp) (Geos (Ang (An h1 o1 k1)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An k1 o1 h1)) add Emp) (Geos (Ang (An h1 o1 k1)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from assms P37 P40 P41 P42
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Plane_sameside (Li o2 h2) k2 l2
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Plane_sameside (Li o1 h1) k1 l1
Ang_inside (An h2 o2 l2) k2
Def (Ang (An k1 o1 h1))
Def (Ang (An l1 o1 h1))
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An k1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 h1)) add Emp)
Cong (Geos (Ang (An k1 o1 h1)) add Emp) (Geos (Ang (An h1 o1 k1)) add Emp)
[PROOF STEP]
have P43 : "Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An l1 o1 h1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Plane_sameside (Li o2 h2) k2 l2
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Plane_sameside (Li o1 h1) k1 l1
Ang_inside (An h2 o2 l2) k2
Def (Ang (An k1 o1 h1))
Def (Ang (An l1 o1 h1))
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An k1 o1 h1)) add Emp) (Geos (Ang (An l1 o1 h1)) add Emp)
Cong (Geos (Ang (An k1 o1 h1)) add Emp) (Geos (Ang (An h1 o1 k1)) add Emp)

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
have P44 : "Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from P40
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An l1 o1 h1))
[PROOF STEP]
have P45 : "Def (Ang (An h1 o1 l1))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An l1 o1 h1))

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from assms P40 P43 P44 P45
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Plane_sameside (Li o2 h2) k2 l2
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Plane_sameside (Li o1 h1) k1 l1
Ang_inside (An h2 o2 l2) k2
Def (Ang (An l1 o1 h1))
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An l1 o1 h1)) add Emp)
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Def (Ang (An h1 o1 l1))
[PROOF STEP]
have P46 : "Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Plane_sameside (Li o2 h2) k2 l2
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Plane_sameside (Li o1 h1) k1 l1
Ang_inside (An h2 o2 l2) k2
Def (Ang (An l1 o1 h1))
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An l1 o1 h1)) add Emp)
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Def (Ang (An h1 o1 l1))

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from assms P45 P46
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Plane_sameside (Li o2 h2) k2 l2
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Plane_sameside (Li o1 h1) k1 l1
Ang_inside (An h2 o2 l2) k2
Def (Ang (An h1 o1 l1))
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
[PROOF STEP]
have P47 : "Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Plane_sameside (Li o2 h2) k2 l2
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Plane_sameside (Li o1 h1) k1 l1
Ang_inside (An h2 o2 l2) k2
Def (Ang (An h1 o1 l1))
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from assms P3 P47
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Plane_sameside (Li o2 h2) k2 l2
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Plane_sameside (Li o1 h1) k1 l1
Ang_inside (An h2 o2 l2) k2
Def (Ang (An h2 o2 k2))
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
[PROOF STEP]
have P48 : "Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An h2 o2 k2)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Plane_sameside (Li o2 h2) k2 l2
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Plane_sameside (Li o1 h1) k1 l1
Ang_inside (An h2 o2 l2) k2
Def (Ang (An h2 o2 k2))
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from P29 P48
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An h2 o2 k2)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
[PROOF STEP]
have P49 : "Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An h2 o2 k2)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An h2 o2 k2)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
have P50 : "Cong (Geos (Ang (An h2 o2 k2)) add Emp) (Geos (Ang (An k2 o2 h2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An h2 o2 k2)) add Emp) (Geos (Ang (An k2 o2 h2)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An h2 o2 k2)) add Emp) (Geos (Ang (An k2 o2 h2)) add Emp)

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

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li k2 o2)) add Emp) (Geos (Lin (Li l2 o2)) add Emp) \<and> \<not> Bet_Point (Se k2 l2) o2
[PROOF STEP]
by (simp add:Ang_move_unique)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li k2 o2)) add Emp) (Geos (Lin (Li l2 o2)) add Emp) \<and> \<not> Bet_Point (Se k2 l2) o2

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Plane_sameside (Li o2 h2) k2 l2
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Plane_sameside (Li o1 h1) k1 l1
Ang_inside (An h2 o2 l2) k2
[PROOF STEP]
have "Def (Ang (An h2 o2 l2)) \<and> Plane_sameside (Li o2 h2) l2 k2
    \<and> Plane_sameside (Li o2 l2) h2 k2"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Plane_sameside (Li o2 h2) k2 l2
Cong (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
Plane_sameside (Li o1 h1) k1 l1
Ang_inside (An h2 o2 l2) k2

goal (1 subgoal):
 1. Def (Ang (An h2 o2 l2)) \<and> Plane_sameside (Li o2 h2) l2 k2 \<and> Plane_sameside (Li o2 l2) h2 k2
[PROOF STEP]
by (simp add:Ang_inside_def)
[PROOF STATE]
proof (state)
this:
Def (Ang (An h2 o2 l2)) \<and> Plane_sameside (Li o2 h2) l2 k2 \<and> Plane_sameside (Li o2 l2) h2 k2

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h2 o2 l2)) \<and> Plane_sameside (Li o2 h2) l2 k2 \<and> Plane_sameside (Li o2 l2) h2 k2
[PROOF STEP]
have P52 : "\<not> Line_on (Li o2 l2) k2"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h2 o2 l2)) \<and> Plane_sameside (Li o2 h2) l2 k2 \<and> Plane_sameside (Li o2 l2) h2 k2

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

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

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
[PROOF STEP]
have P53 : "Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li l2 o2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li l2 o2)) add Emp)
[PROOF STEP]
by (simp add:Line_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li l2 o2)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from P51 P53
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li k2 o2)) add Emp) (Geos (Lin (Li l2 o2)) add Emp) \<and> \<not> Bet_Point (Se k2 l2) o2
Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li l2 o2)) add Emp)
[PROOF STEP]
have P54 : "Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow>
    Eq (Geos (Lin (Li k2 o2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li k2 o2)) add Emp) (Geos (Lin (Li l2 o2)) add Emp) \<and> \<not> Bet_Point (Se k2 l2) o2
Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li l2 o2)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li k2 o2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
[PROOF STEP]
by (blast intro:Eq_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li k2 o2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
have P55 : "Line_on (Li k2 o2) k2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li k2 o2) k2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li k2 o2) k2

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from P54 P55
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li k2 o2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
Line_on (Li k2 o2) k2
[PROOF STEP]
have P56 : "Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow>
    Line_on (Li o2 l2) k2"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li k2 o2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
Line_on (Li k2 o2) k2

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Line_on (Li o2 l2) k2
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Line_on (Li o2 l2) k2

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
from P52 P56
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li o2 l2) k2
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Line_on (Li o2 l2) k2
[PROOF STEP]
show "\<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li o2 l2) k2
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Line_on (Li o2 l2) k2

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

goal:
No subgoals!
[PROOF STEP]
qed