[STATEMENT]
lemma (in Congruence_Rule) Ang_split_lemma1 :
  assumes N :
    "Def (Ang (An h1 o1 k1))" "Def (Ang (An h2 o2 k2))"
    "Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)"
    "Cong (Geos (Ang (An l1 o1 k1)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp)"
    "Plane_sameside (Li o1 k1) h1 l1"
    "Plane_sameside (Li o2 k2) h2 l2"
    "\<not> Eq (Geos (Lin (Li o1 l1)) add Emp) (Geos (Lin (Li o1 h1)) add Emp)"
  shows
    "\<not> Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp) \<Longrightarrow> False
[PROOF STEP]
assume W : "Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp)"
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P1 : "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 (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from N
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 k2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Cong (Geos (Ang (An l1 o1 k1)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp)
Plane_sameside (Li o1 k1) h1 l1
Plane_sameside (Li o2 k2) h2 l2
\<not> Eq (Geos (Lin (Li o1 l1)) add Emp) (Geos (Lin (Li o1 h1)) add Emp)
[PROOF STEP]
have P2 : "\<not> Line_on (Li o2 k2) h2 \<and> \<not> Line_on (Li o2 k2) l2
    \<and> \<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi l2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 k2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Cong (Geos (Ang (An l1 o1 k1)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp)
Plane_sameside (Li o1 k1) h1 l1
Plane_sameside (Li o2 k2) h2 l2
\<not> Eq (Geos (Lin (Li o1 l1)) add Emp) (Geos (Lin (Li o1 h1)) add Emp)

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

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P1 P2
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li o2 k2) o2
\<not> Line_on (Li o2 k2) h2 \<and> \<not> Line_on (Li o2 k2) l2 \<and> \<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi l2) add Emp)
[PROOF STEP]
have "Bet_Point (Se h2 l2) o2 \<Longrightarrow> (\<exists>p. Bet_Point (Se h2 l2) p
    \<and> Line_on (Li o2 k2) p \<and> \<not> Line_on (Li o2 k2) h2 \<and> \<not> Line_on (Li o2 k2) l2)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li o2 k2) o2
\<not> Line_on (Li o2 k2) h2 \<and> \<not> Line_on (Li o2 k2) l2 \<and> \<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi l2) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se h2 l2) o2 \<Longrightarrow> \<exists>p. Bet_Point (Se h2 l2) p \<and> Line_on (Li o2 k2) p \<and> \<not> Line_on (Li o2 k2) h2 \<and> \<not> Line_on (Li o2 k2) l2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet_Point (Se h2 l2) o2 \<Longrightarrow> \<exists>p. Bet_Point (Se h2 l2) p \<and> Line_on (Li o2 k2) p \<and> \<not> Line_on (Li o2 k2) h2 \<and> \<not> Line_on (Li o2 k2) l2

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se h2 l2) o2 \<Longrightarrow> \<exists>p. Bet_Point (Se h2 l2) p \<and> Line_on (Li o2 k2) p \<and> \<not> Line_on (Li o2 k2) h2 \<and> \<not> Line_on (Li o2 k2) l2
[PROOF STEP]
have "Bet_Point (Se h2 l2) o2 \<Longrightarrow> Plane_diffside (Li o2 k2) h2 l2"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se h2 l2) o2 \<Longrightarrow> \<exists>p. Bet_Point (Se h2 l2) p \<and> Line_on (Li o2 k2) p \<and> \<not> Line_on (Li o2 k2) h2 \<and> \<not> Line_on (Li o2 k2) l2

goal (1 subgoal):
 1. Bet_Point (Se h2 l2) o2 \<Longrightarrow> Plane_diffside (Li o2 k2) h2 l2
[PROOF STEP]
by (simp add:Plane_diffside_def)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se h2 l2) o2 \<Longrightarrow> Plane_diffside (Li o2 k2) h2 l2

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se h2 l2) o2 \<Longrightarrow> Plane_diffside (Li o2 k2) h2 l2
[PROOF STEP]
have P3 : "Bet_Point (Se h2 l2) o2 \<Longrightarrow> \<not> Plane_sameside (Li o2 k2) h2 l2"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se h2 l2) o2 \<Longrightarrow> Plane_diffside (Li o2 k2) h2 l2

goal (1 subgoal):
 1. Bet_Point (Se h2 l2) o2 \<Longrightarrow> \<not> Plane_sameside (Li o2 k2) h2 l2
[PROOF STEP]
by (simp add:Plane_diffside_not_sameside)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se h2 l2) o2 \<Longrightarrow> \<not> Plane_sameside (Li o2 k2) h2 l2

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

goal (1 subgoal):
 1. \<not> Bet_Point (Se h2 l2) o2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se h2 l2) o2

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P5 : "Line_on (Li o2 l2) l2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o2 l2) l2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o2 l2) l2

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from W P5
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp)
Line_on (Li o2 l2) l2
[PROOF STEP]
have P6 : "Line_on (Li o2 h2) l2"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp)
Line_on (Li o2 l2) l2

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

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P7 : "Line_on (Li o2 k2) k2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o2 k2) k2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o2 k2) k2

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P8 : "\<not> Bet_Point (Se k2 k2) o2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se k2 k2) o2
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se k2 k2) o2

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li o2 k2) o2
[PROOF STEP]
have P9 : "Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp) \<Longrightarrow> Line_on (Li o2 k2) l2"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li o2 k2) o2

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

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P2 P9
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li o2 k2) h2 \<and> \<not> Line_on (Li o2 k2) l2 \<and> \<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi l2) add Emp)
Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp) \<Longrightarrow> Line_on (Li o2 k2) l2
[PROOF STEP]
have P10 : "\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li o2 k2) h2 \<and> \<not> Line_on (Li o2 k2) l2 \<and> \<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi l2) add Emp)
Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp) \<Longrightarrow> Line_on (Li o2 k2) l2

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
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 o2 h2)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from N
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 k2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Cong (Geos (Ang (An l1 o1 k1)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp)
Plane_sameside (Li o1 k1) h1 l1
Plane_sameside (Li o2 k2) h2 l2
\<not> Eq (Geos (Lin (Li o1 l1)) add Emp) (Geos (Lin (Li o1 h1)) add Emp)
[PROOF STEP]
have "Def (Tri (Tr h2 o2 k2))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 k2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Cong (Geos (Ang (An l1 o1 k1)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp)
Plane_sameside (Li o1 k1) h1 l1
Plane_sameside (Li o2 k2) h2 l2
\<not> Eq (Geos (Lin (Li o1 l1)) add Emp) (Geos (Lin (Li o1 h1)) add Emp)

goal (1 subgoal):
 1. Def (Tri (Tr h2 o2 k2))
[PROOF STEP]
by (simp add:Ang_to_Tri)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr h2 o2 k2))

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr h2 o2 k2))
[PROOF STEP]
have P11 : "\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr h2 o2 k2))

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

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from N P4 P6 P7 P8 P10 P11
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 k2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Cong (Geos (Ang (An l1 o1 k1)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp)
Plane_sameside (Li o1 k1) h1 l1
Plane_sameside (Li o2 k2) h2 l2
\<not> Eq (Geos (Lin (Li o1 l1)) add Emp) (Geos (Lin (Li o1 h1)) add Emp)
\<not> Bet_Point (Se h2 l2) o2
Line_on (Li o2 h2) l2
Line_on (Li o2 k2) k2
\<not> Bet_Point (Se k2 k2) o2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k2) add Emp)
[PROOF STEP]
have P12 :
    "Eq (Geos (Ang (An h2 o2 k2)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp) \<and> Def (Ang (An l2 o2 k2))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 k2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Cong (Geos (Ang (An l1 o1 k1)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp)
Plane_sameside (Li o1 k1) h1 l1
Plane_sameside (Li o2 k2) h2 l2
\<not> Eq (Geos (Lin (Li o1 l1)) add Emp) (Geos (Lin (Li o1 h1)) add Emp)
\<not> Bet_Point (Se h2 l2) o2
Line_on (Li o2 h2) l2
Line_on (Li o2 k2) k2
\<not> Bet_Point (Se k2 k2) o2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k2) add Emp)

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. Def (Tri (Tr h1 o1 k1))
[PROOF STEP]
by (simp add:Ang_to_Tri)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr h1 o1 k1))

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

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

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

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

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

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

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P18 : "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. Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li o1 k1) o1
[PROOF STEP]
have P19 : "Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp) \<Longrightarrow> Line_on (Li o1 k1) l1"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li o1 k1) o1

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

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P17 P19
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li o1 k1) h1 \<and> \<not> Line_on (Li o1 k1) l1 \<and> \<not> Eq (Geos (Poi h1) add Emp) (Geos (Poi l1) add Emp)
Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp) \<Longrightarrow> Line_on (Li o1 k1) l1
[PROOF STEP]
have "\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li o1 k1) h1 \<and> \<not> Line_on (Li o1 k1) l1 \<and> \<not> Eq (Geos (Poi h1) add Emp) (Geos (Poi l1) add Emp)
Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp) \<Longrightarrow> Line_on (Li o1 k1) l1

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

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

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

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P15 P16
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li h1 o1)) add Emp) (Geos (Lin (Li l1 o1)) add Emp) \<and> \<not> Bet_Point (Se h1 l1) o1
Eq (Geos (Lin (Li h1 o1)) add Emp) (Geos (Lin (Li o1 h1)) add Emp)
[PROOF STEP]
have P21 : "Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li l1 o1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li h1 o1)) add Emp) (Geos (Lin (Li l1 o1)) add Emp) \<and> \<not> Bet_Point (Se h1 l1) o1
Eq (Geos (Lin (Li h1 o1)) add Emp) (Geos (Lin (Li o1 h1)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li l1 o1)) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev Eq_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li l1 o1)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P20 P21
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li o1 l1)) add Emp) (Geos (Lin (Li l1 o1)) add Emp)
Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li l1 o1)) add Emp)
[PROOF STEP]
have P22 : "Eq (Geos (Lin (Li o1 l1)) add Emp) (Geos (Lin (Li o1 h1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li o1 l1)) add Emp) (Geos (Lin (Li l1 o1)) add Emp)
Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li l1 o1)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o1 l1)) add Emp) (Geos (Lin (Li o1 h1)) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev Eq_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li o1 l1)) add Emp) (Geos (Lin (Li o1 h1)) add Emp)

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem (in Congruence_Rule) Ang_split :
  assumes
    "Def (Ang (An h1 o1 k1))" "Def (Ang (An h2 o2 k2))"
    "Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)"
    "Ang_inside (An h1 o1 k1) l1"
  shows
    "\<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)
goal (1 subgoal):
 1. \<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]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<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]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 k2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
have P1 : "Plane_sameside (Li o1 h1) k1 l1 \<and> Plane_sameside (Li o1 k1) h1 l1"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 k2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Ang_inside (An h1 o1 k1) l1

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

goal (1 subgoal):
 1. \<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]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 k2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
have P2 : "\<not> Line_on (Li o2 k2) h2"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 k2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Ang_inside (An h1 o1 k1) l1

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

goal (1 subgoal):
 1. \<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]
from P1
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li o1 h1) k1 l1 \<and> Plane_sameside (Li o1 k1) h1 l1
[PROOF STEP]
have P3 : "\<not> Line_on (Li o1 k1) l1"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li o1 h1) k1 l1 \<and> Plane_sameside (Li o1 k1) h1 l1

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

goal (1 subgoal):
 1. \<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]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 k2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
have P4 : "Def (Tri (Tr h1 o1 k1))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 k2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Ang_inside (An h1 o1 k1) l1

goal (1 subgoal):
 1. Def (Tri (Tr h1 o1 k1))
[PROOF STEP]
by (simp add:Ang_to_Tri)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr h1 o1 k1))

goal (1 subgoal):
 1. \<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]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr h1 o1 k1))
[PROOF STEP]
have P5 : "\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi k1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr h1 o1 k1))

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

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

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

goal (1 subgoal):
 1. \<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]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An o1 k1 l1))
[PROOF STEP]
have P6 : "Def (Ang (An k1 o1 l1))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An o1 k1 l1))

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

goal (1 subgoal):
 1. \<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]
from P2 P6
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li o2 k2) h2
Def (Ang (An k1 o1 l1))
[PROOF STEP]
have "\<exists>p. Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An p o2 k2)) add Emp)
    \<and> Plane_sameside (Li o2 k2) p h2"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li o2 k2) h2
Def (Ang (An k1 o1 l1))

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

goal (1 subgoal):
 1. \<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]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An p o2 k2)) add Emp) \<and> Plane_sameside (Li o2 k2) p h2
[PROOF STEP]
obtain l2 :: Point where P7 : "Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp)
    \<and> Plane_sameside (Li o2 k2) l2 h2"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An p o2 k2)) add Emp) \<and> Plane_sameside (Li o2 k2) p h2

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

goal (1 subgoal):
 1. \<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]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 k2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
have "Def (Tri (Tr h2 o2 k2))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 k2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Ang_inside (An h1 o1 k1) l1

goal (1 subgoal):
 1. Def (Tri (Tr h2 o2 k2))
[PROOF STEP]
by (simp add:Ang_to_Tri)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr h2 o2 k2))

goal (1 subgoal):
 1. \<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]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr h2 o2 k2))
[PROOF STEP]
have P8 : "\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr h2 o2 k2))

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

goal (1 subgoal):
 1. \<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]
have P9 : "Eq (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp)

goal (1 subgoal):
 1. \<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]
from P7 P9
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp) \<and> Plane_sameside (Li o2 k2) l2 h2
Eq (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp)
[PROOF STEP]
have P10 : "Cong (Geos (Ang (An l1 o1 k1)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp) \<and> Plane_sameside (Li o2 k2) l2 h2
Eq (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An l1 o1 k1)) add Emp)

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

goal (1 subgoal):
 1. \<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]
from P1
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li o1 h1) k1 l1 \<and> Plane_sameside (Li o1 k1) h1 l1
[PROOF STEP]
have P11 : "\<not> Line_on_Seg (Li o1 h1) (Se k1 l1) \<and> \<not> Line_on (Li o1 h1) k1
    \<and> \<not> Line_on (Li o1 h1) l1 \<and> \<not> Eq (Geos (Poi k1) add Emp) (Geos (Poi l1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li o1 h1) k1 l1 \<and> Plane_sameside (Li o1 k1) h1 l1

goal (1 subgoal):
 1. \<not> Line_on_Seg (Li o1 h1) (Se k1 l1) \<and> \<not> Line_on (Li o1 h1) k1 \<and> \<not> Line_on (Li o1 h1) l1 \<and> \<not> Eq (Geos (Poi k1) add Emp) (Geos (Poi l1) add Emp)
[PROOF STEP]
by (simp add:Plane_sameside_def)
[PROOF STATE]
proof (state)
this:
\<not> Line_on_Seg (Li o1 h1) (Se k1 l1) \<and> \<not> Line_on (Li o1 h1) k1 \<and> \<not> Line_on (Li o1 h1) l1 \<and> \<not> Eq (Geos (Poi k1) add Emp) (Geos (Poi l1) add Emp)

goal (1 subgoal):
 1. \<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]
have "Line_on (Li o1 l1) l1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o1 l1) l1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o1 l1) l1

goal (1 subgoal):
 1. \<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]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li o1 l1) l1
[PROOF STEP]
have P12 : "Eq (Geos (Lin (Li o1 l1)) add Emp) (Geos (Lin (Li o1 h1)) add Emp) \<Longrightarrow> Line_on (Li o1 h1) l1"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li o1 l1) l1

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

goal (1 subgoal):
 1. \<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]
from P11 P12
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on_Seg (Li o1 h1) (Se k1 l1) \<and> \<not> Line_on (Li o1 h1) k1 \<and> \<not> Line_on (Li o1 h1) l1 \<and> \<not> Eq (Geos (Poi k1) add Emp) (Geos (Poi l1) add Emp)
Eq (Geos (Lin (Li o1 l1)) add Emp) (Geos (Lin (Li o1 h1)) add Emp) \<Longrightarrow> Line_on (Li o1 h1) l1
[PROOF STEP]
have P13 : "\<not> Eq (Geos (Lin (Li o1 l1)) add Emp) (Geos (Lin (Li o1 h1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on_Seg (Li o1 h1) (Se k1 l1) \<and> \<not> Line_on (Li o1 h1) k1 \<and> \<not> Line_on (Li o1 h1) l1 \<and> \<not> Eq (Geos (Poi k1) add Emp) (Geos (Poi l1) add Emp)
Eq (Geos (Lin (Li o1 l1)) add Emp) (Geos (Lin (Li o1 h1)) add Emp) \<Longrightarrow> Line_on (Li o1 h1) l1

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

goal (1 subgoal):
 1. \<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]
from P7
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp) \<and> Plane_sameside (Li o2 k2) l2 h2
[PROOF STEP]
have P14 : "Plane_sameside (Li o2 k2) h2 l2"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp) \<and> Plane_sameside (Li o2 k2) l2 h2

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

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

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

goal (1 subgoal):
 1. \<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]
from P1
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li o1 h1) k1 l1 \<and> Plane_sameside (Li o1 k1) h1 l1
[PROOF STEP]
have P16 :  "Plane_sameside (Li o1 k1) l1 h1"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li o1 h1) k1 l1 \<and> Plane_sameside (Li o1 k1) h1 l1

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

goal (1 subgoal):
 1. \<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]
from P7
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp) \<and> Plane_sameside (Li o2 k2) l2 h2
[PROOF STEP]
have P17 : "Plane_sameside (Li o2 k2) l2 h2"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp) \<and> Plane_sameside (Li o2 k2) l2 h2

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

goal (1 subgoal):
 1. \<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]
from assms P5 P8 P10 P13 P15 P16 P17
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 k2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Ang_inside (An h1 o1 k1) l1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi k1) add Emp)
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k2) add Emp)
Cong (Geos (Ang (An l1 o1 k1)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 l1)) add Emp) (Geos (Lin (Li o1 h1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp)
Plane_sameside (Li o1 k1) l1 h1
Plane_sameside (Li o2 k2) l2 h2
[PROOF STEP]
have P18 :
    "Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
    \<and> Ang_inside (An h2 o2 k2) l2"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 k2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Ang_inside (An h1 o1 k1) l1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi k1) add Emp)
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k2) add Emp)
Cong (Geos (Ang (An l1 o1 k1)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 l1)) add Emp) (Geos (Lin (Li o1 h1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp)
Plane_sameside (Li o1 k1) l1 h1
Plane_sameside (Li o2 k2) l2 h2

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

goal (1 subgoal):
 1. \<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]
have P19 : "Eq (Geos (Ang (An l2 o2 k2)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An l2 o2 k2)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An l2 o2 k2)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)

goal (1 subgoal):
 1. \<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]
from P7 P19
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp) \<and> Plane_sameside (Li o2 k2) l2 h2
Eq (Geos (Ang (An l2 o2 k2)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
[PROOF STEP]
have P20 : "Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An l2 o2 k2)) add Emp) \<and> Plane_sameside (Li o2 k2) l2 h2
Eq (Geos (Ang (An l2 o2 k2)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)

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

goal (1 subgoal):
 1. \<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]
have P21 : "Eq (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (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:
Eq (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)

goal (1 subgoal):
 1. \<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]
have P22 : "Eq (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (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:
Eq (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)

goal (1 subgoal):
 1. \<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]
from P18 P21
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp) \<and> Ang_inside (An h2 o2 k2) l2
Eq (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
[PROOF STEP]
have P23 : "Cong (Geos (Ang (An h1 o1 l1)) 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 l2 o2 h2)) add Emp) \<and> Ang_inside (An h2 o2 k2) l2
Eq (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An h1 o1 l1)) 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 (1 subgoal):
 1. \<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]
from P22 P23
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
have P24 : "Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An l2 o2 h2)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) 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 h2 o2 l2)) 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 h2 o2 l2)) add Emp)

goal (1 subgoal):
 1. \<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]
from P18 P20 P24
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp) \<and> Ang_inside (An h2 o2 k2) l2
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
[PROOF STEP]
show "\<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:
Cong (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp) \<and> Ang_inside (An h2 o2 k2) l2
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)

goal (1 subgoal):
 1. \<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 blast
[PROOF STATE]
proof (state)
this:
\<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:
No subgoals!
[PROOF STEP]
qed


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

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

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li o2 h2) k2 l21 \<and> Plane_sameside (Li o2 k2) h2 l21
[PROOF STEP]
have P1 : "Plane_sameside (Li o2 k2) l21 h2"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li o2 h2) k2 l21 \<and> Plane_sameside (Li o2 k2) h2 l21

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

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

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

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)
[PROOF STEP]
from P1 P2
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li o2 k2) l21 h2
Plane_sameside (Li o2 h2) k2 l22 \<and> Plane_sameside (Li o2 k2) h2 l22
[PROOF STEP]
have P3 : "\<not> Eq (Geos (Poi l22) add Emp) (Geos (Poi l21) add Emp) \<Longrightarrow>
    Plane_sameside (Li o2 k2) l21 l22"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li o2 k2) l21 h2
Plane_sameside (Li o2 h2) k2 l22 \<and> Plane_sameside (Li o2 k2) h2 l22

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi l22) add Emp) (Geos (Poi l21) add Emp) \<Longrightarrow> Plane_sameside (Li o2 k2) l21 l22
[PROOF STEP]
by (simp add:Plane_sameside_trans)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi l22) add Emp) (Geos (Poi l21) add Emp) \<Longrightarrow> Plane_sameside (Li o2 k2) l21 l22

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)
[PROOF STEP]
have P4 : "Eq (Geos (Ang (An k2 o2 l21)) add Emp) (Geos (Ang (An l21 o2 k2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An k2 o2 l21)) add Emp) (Geos (Ang (An l21 o2 k2)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An k2 o2 l21)) add Emp) (Geos (Ang (An l21 o2 k2)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)
[PROOF STEP]
from assms P4
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 k2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Ang_inside (An h1 o1 k1) l1
Ang_inside (An h2 o2 k2) l21
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l21)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l21)) add Emp)
Ang_inside (An h2 o2 k2) l22
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l22)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l22)) add Emp)
Eq (Geos (Ang (An k2 o2 l21)) add Emp) (Geos (Ang (An l21 o2 k2)) add Emp)
[PROOF STEP]
have P5 : "Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An l21 o2 k2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 k2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Ang_inside (An h1 o1 k1) l1
Ang_inside (An h2 o2 k2) l21
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l21)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l21)) add Emp)
Ang_inside (An h2 o2 k2) l22
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l22)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l22)) add Emp)
Eq (Geos (Ang (An k2 o2 l21)) add Emp) (Geos (Ang (An l21 o2 k2)) add Emp)

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

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)
[PROOF STEP]
have P6 : "Eq (Geos (Ang (An k2 o2 l22)) add Emp) (Geos (Ang (An l22 o2 k2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An k2 o2 l22)) add Emp) (Geos (Ang (An l22 o2 k2)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An k2 o2 l22)) add Emp) (Geos (Ang (An l22 o2 k2)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)
[PROOF STEP]
from assms P6
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 k2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Ang_inside (An h1 o1 k1) l1
Ang_inside (An h2 o2 k2) l21
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l21)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l21)) add Emp)
Ang_inside (An h2 o2 k2) l22
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l22)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l22)) add Emp)
Eq (Geos (Ang (An k2 o2 l22)) add Emp) (Geos (Ang (An l22 o2 k2)) add Emp)
[PROOF STEP]
have P7 : "Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An l22 o2 k2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h1 o1 k1))
Def (Ang (An h2 o2 k2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Ang_inside (An h1 o1 k1) l1
Ang_inside (An h2 o2 k2) l21
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l21)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l21)) add Emp)
Ang_inside (An h2 o2 k2) l22
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l22)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l22)) add Emp)
Eq (Geos (Ang (An k2 o2 l22)) add Emp) (Geos (Ang (An l22 o2 k2)) add Emp)

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

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)
[PROOF STEP]
from P3 P5 P7
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi l22) add Emp) (Geos (Poi l21) add Emp) \<Longrightarrow> Plane_sameside (Li o2 k2) l21 l22
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An l21 o2 k2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An l22 o2 k2)) add Emp)
[PROOF STEP]
have P8 : "\<not> Eq (Geos (Poi l22) add Emp) (Geos (Poi l21) add Emp) \<Longrightarrow>
    Eq (Geos (Lin (Li l21 o2)) add Emp) (Geos (Lin (Li l22 o2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi l22) add Emp) (Geos (Poi l21) add Emp) \<Longrightarrow> Plane_sameside (Li o2 k2) l21 l22
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An l21 o2 k2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An l22 o2 k2)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi l22) add Emp) (Geos (Poi l21) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li l21 o2)) add Emp) (Geos (Lin (Li l22 o2)) add Emp)
[PROOF STEP]
by (simp add:Ang_move_unique)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi l22) add Emp) (Geos (Poi l21) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li l21 o2)) add Emp) (Geos (Lin (Li l22 o2)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)
[PROOF STEP]
have P9 : "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 (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li o2 k2) l21 h2
[PROOF STEP]
have P10 : "\<not> Line_on (Li o2 k2) l21"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li o2 k2) l21 h2

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

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)
[PROOF STEP]
from P9
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li o2 k2) o2
[PROOF STEP]
have P11 : "Eq (Geos (Poi o2) add Emp) (Geos (Poi l21) add Emp) \<Longrightarrow> Line_on (Li o2 k2) l21"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li o2 k2) o2

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

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)
[PROOF STEP]
from P10 P11
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li o2 k2) l21
Eq (Geos (Poi o2) add Emp) (Geos (Poi l21) add Emp) \<Longrightarrow> Line_on (Li o2 k2) l21
[PROOF STEP]
have P12 : "\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l21) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li o2 k2) l21
Eq (Geos (Poi o2) add Emp) (Geos (Poi l21) add Emp) \<Longrightarrow> Line_on (Li o2 k2) l21

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

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

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

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)
[PROOF STEP]
from P2
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li o2 h2) k2 l22 \<and> Plane_sameside (Li o2 k2) h2 l22
[PROOF STEP]
have P14 : "\<not> Line_on (Li o2 k2) l22"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li o2 h2) k2 l22 \<and> Plane_sameside (Li o2 k2) h2 l22

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

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)
[PROOF STEP]
from P9
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li o2 k2) o2
[PROOF STEP]
have P15 : "Eq (Geos (Poi o2) add Emp) (Geos (Poi l22) add Emp) \<Longrightarrow> Line_on (Li o2 k2) l22"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li o2 k2) o2

goal (1 subgoal):
 1. Eq (Geos (Poi o2) add Emp) (Geos (Poi l22) add Emp) \<Longrightarrow> Line_on (Li o2 k2) l22
[PROOF STEP]
by (simp add:Point_Eq)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi o2) add Emp) (Geos (Poi l22) add Emp) \<Longrightarrow> Line_on (Li o2 k2) l22

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)
[PROOF STEP]
from P14 P15
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li o2 k2) l22
Eq (Geos (Poi o2) add Emp) (Geos (Poi l22) add Emp) \<Longrightarrow> Line_on (Li o2 k2) l22
[PROOF STEP]
have "\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l22) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li o2 k2) l22
Eq (Geos (Poi o2) add Emp) (Geos (Poi l22) add Emp) \<Longrightarrow> Line_on (Li o2 k2) l22

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

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

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

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)
[PROOF STEP]
from P8 P13
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi l22) add Emp) (Geos (Poi l21) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li l21 o2)) add Emp) (Geos (Lin (Li l22 o2)) add Emp)
Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li l21 o2)) add Emp)
[PROOF STEP]
have P17 : "\<not> Eq (Geos (Poi l22) add Emp) (Geos (Poi l21) add Emp) \<Longrightarrow>
    Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li l22 o2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi l22) add Emp) (Geos (Poi l21) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li l21 o2)) add Emp) (Geos (Lin (Li l22 o2)) add Emp)
Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li l21 o2)) add Emp)

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

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)
[PROOF STEP]
from P16 P17
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li o2 l22)) add Emp) (Geos (Lin (Li l22 o2)) add Emp)
\<not> Eq (Geos (Poi l22) add Emp) (Geos (Poi l21) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li l22 o2)) add Emp)
[PROOF STEP]
have P18 : "\<not> Eq (Geos (Poi l22) add Emp) (Geos (Poi l21) add Emp) \<Longrightarrow>
    Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li o2 l22)) add Emp) (Geos (Lin (Li l22 o2)) add Emp)
\<not> Eq (Geos (Poi l22) add Emp) (Geos (Poi l21) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li l22 o2)) add Emp)

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

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)
[PROOF STEP]
have P19 : "Line_on (Li o2 l21) o2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o2 l21) o2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o2 l21) o2

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)
[PROOF STEP]
have P20 : "Line_on (Li o2 l21) l21"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o2 l21) l21
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o2 l21) l21

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)
[PROOF STEP]
have P21 : "Line_on (Li o2 l22) o2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o2 l22) o2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o2 l22) o2

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)
[PROOF STEP]
have "Line_on (Li o2 l22) l22"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o2 l22) l22
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o2 l22) l22

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li o2 l22) l22
[PROOF STEP]
have P22 : "Eq (Geos (Poi l22) add Emp) (Geos (Poi l21) add Emp) \<Longrightarrow> Line_on (Li o2 l22) l21"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li o2 l22) l22

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

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)
[PROOF STEP]
from P12 P19 P20 P21 P22
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l21) add Emp)
Line_on (Li o2 l21) o2
Line_on (Li o2 l21) l21
Line_on (Li o2 l22) o2
Eq (Geos (Poi l22) add Emp) (Geos (Poi l21) add Emp) \<Longrightarrow> Line_on (Li o2 l22) l21
[PROOF STEP]
have P23 : "Eq (Geos (Poi l22) add Emp) (Geos (Poi l21) add Emp) \<Longrightarrow>
    Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l21) add Emp)
Line_on (Li o2 l21) o2
Line_on (Li o2 l21) l21
Line_on (Li o2 l22) o2
Eq (Geos (Poi l22) add Emp) (Geos (Poi l21) add Emp) \<Longrightarrow> Line_on (Li o2 l22) l21

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

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)
[PROOF STEP]
from P18 P23
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi l22) add Emp) (Geos (Poi l21) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)
Eq (Geos (Poi l22) add Emp) (Geos (Poi l21) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)
[PROOF STEP]
show "Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi l22) add Emp) (Geos (Poi l21) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)
Eq (Geos (Poi l22) add Emp) (Geos (Poi l21) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li o2 l21)) add Emp) (Geos (Lin (Li o2 l22)) add Emp)

goal:
No subgoals!
[PROOF STEP]
qed