[STATEMENT]
theorem (in Congruence_Rule) Ang_move_Smaller :
  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"
    "\<not> Ang_inside (An h2 o2 l2) k2"
    "\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)"
  shows "Ang_inside (An h1 o1 k1) l1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
have P1 : "Ang_inside (An l2 o2 h2) k2 \<Longrightarrow> Ang_inside (An h2 o2 l2) k2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ang_inside (An l2 o2 h2) k2 \<Longrightarrow> Ang_inside (An h2 o2 l2) k2
[PROOF STEP]
by (simp add:Ang_inside_def Ang_def_rev)
[PROOF STATE]
proof (state)
this:
Ang_inside (An l2 o2 h2) k2 \<Longrightarrow> Ang_inside (An h2 o2 l2) k2

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
from assms P1
[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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
Ang_inside (An l2 o2 h2) k2 \<Longrightarrow> Ang_inside (An h2 o2 l2) k2
[PROOF STEP]
have P2 : "\<not> Ang_inside (An l2 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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
Ang_inside (An l2 o2 h2) k2 \<Longrightarrow> Ang_inside (An h2 o2 l2) k2

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

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
[PROOF STEP]
have P3 : "\<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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)

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 (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
[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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)

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

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

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
[PROOF STEP]
have P6 : "Def (Ang (An l2 o2 h2))"
[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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)

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

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
from assms P5 P6
[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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
Def (Ang (An k2 o2 h2))
Def (Ang (An l2 o2 h2))
[PROOF STEP]
have P7 : "Ang_inside (An k2 o2 h2) l2 \<and> \<not> Ang_inside (An l2 o2 h2) k2
    \<or> \<not> Ang_inside (An k2 o2 h2) l2 \<and> Ang_inside (An l2 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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
Def (Ang (An k2 o2 h2))
Def (Ang (An l2 o2 h2))

goal (1 subgoal):
 1. Ang_inside (An k2 o2 h2) l2 \<and> \<not> Ang_inside (An l2 o2 h2) k2 \<or> \<not> Ang_inside (An k2 o2 h2) l2 \<and> Ang_inside (An l2 o2 h2) k2
[PROOF STEP]
by (simp add:Ang_inside_case)
[PROOF STATE]
proof (state)
this:
Ang_inside (An k2 o2 h2) l2 \<and> \<not> Ang_inside (An l2 o2 h2) k2 \<or> \<not> Ang_inside (An k2 o2 h2) l2 \<and> Ang_inside (An l2 o2 h2) k2

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
from P2 P7
[PROOF STATE]
proof (chain)
picking this:
\<not> Ang_inside (An l2 o2 h2) k2
Ang_inside (An k2 o2 h2) l2 \<and> \<not> Ang_inside (An l2 o2 h2) k2 \<or> \<not> Ang_inside (An k2 o2 h2) l2 \<and> Ang_inside (An l2 o2 h2) k2
[PROOF STEP]
have "Ang_inside (An k2 o2 h2) l2"
[PROOF STATE]
proof (prove)
using this:
\<not> Ang_inside (An l2 o2 h2) k2
Ang_inside (An k2 o2 h2) l2 \<and> \<not> Ang_inside (An l2 o2 h2) k2 \<or> \<not> Ang_inside (An k2 o2 h2) l2 \<and> Ang_inside (An l2 o2 h2) k2

goal (1 subgoal):
 1. Ang_inside (An k2 o2 h2) l2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Ang_inside (An k2 o2 h2) l2

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An k2 o2 h2) l2
[PROOF STEP]
have P8 : "Ang_inside (An h2 o2 k2) l2"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An k2 o2 h2) l2

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

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
[PROOF STEP]
have P9 : "\<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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)

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. Ang_inside (An h1 o1 k1) l1
[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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
[PROOF STEP]
have "\<not> Eq (Geos (Poi h1) add Emp) (Geos (Poi o1) 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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)

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

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi h1) add Emp) (Geos (Poi o1) add Emp)
[PROOF STEP]
have P10 : "\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi 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. \<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi h1) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi h1) add Emp)

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

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

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
from P5
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An k2 o2 h2))
[PROOF STEP]
have P12 : "Def (Ang (An h2 o2 k2))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An k2 o2 h2))

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 (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
[PROOF STEP]
have P13 : "Cong (Geos (Ang (An h1 o1 l1)) 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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) 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_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. Ang_inside (An h1 o1 k1) l1
[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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
[PROOF STEP]
have P14 : "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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)

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 (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
[PROOF STEP]
have P15 : "Cong (Geos (Ang (An h2 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 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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)

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

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
[PROOF STEP]
have P16 : "Plane_sameside (Li o1 h1) l1 k1"
[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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)

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

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
from P8 P11 P12 P13 P14 P15 P16
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h2 o2 k2) l2
Def (Ang (An h1 o1 l1))
Def (Ang (An h2 o2 k2))
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Plane_sameside (Li o2 h2) l2 k2
Cong (Geos (Ang (An h2 o2 k2)) add Emp) (Geos (Ang (An h1 o1 k1)) add Emp)
Plane_sameside (Li o1 h1) l1 k1
[PROOF STEP]
have P17 : "\<not> Ang_inside (An h1 o1 l1) k1"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h2 o2 k2) l2
Def (Ang (An h1 o1 l1))
Def (Ang (An h2 o2 k2))
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Plane_sameside (Li o2 h2) l2 k2
Cong (Geos (Ang (An h2 o2 k2)) add Emp) (Geos (Ang (An h1 o1 k1)) add Emp)
Plane_sameside (Li o1 h1) l1 k1

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

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
have P18 : "Ang_inside (An l1 o1 h1) k1 \<Longrightarrow> Ang_inside (An h1 o1 l1) k1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ang_inside (An l1 o1 h1) k1 \<Longrightarrow> Ang_inside (An h1 o1 l1) k1
[PROOF STEP]
by (simp add:Ang_inside_def Ang_def_rev)
[PROOF STATE]
proof (state)
this:
Ang_inside (An l1 o1 h1) k1 \<Longrightarrow> Ang_inside (An h1 o1 l1) k1

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
from P17 P18
[PROOF STATE]
proof (chain)
picking this:
\<not> Ang_inside (An h1 o1 l1) k1
Ang_inside (An l1 o1 h1) k1 \<Longrightarrow> Ang_inside (An h1 o1 l1) k1
[PROOF STEP]
have P19 : "\<not> Ang_inside (An l1 o1 h1) k1"
[PROOF STATE]
proof (prove)
using this:
\<not> Ang_inside (An h1 o1 l1) k1
Ang_inside (An l1 o1 h1) k1 \<Longrightarrow> Ang_inside (An h1 o1 l1) k1

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

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
[PROOF STEP]
have P20 : "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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)

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. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
from P11
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h1 o1 l1))
[PROOF STEP]
have P21 : "Def (Ang (An l1 o1 h1))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h1 o1 l1))

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

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
have "Line_on (Li o1 k1) k1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o1 k1) k1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o1 k1) k1

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

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

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
have P23 : "Line_on (Li o1 h1) o1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o1 h1) o1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o1 h1) o1

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
have "Line_on (Li l1 k1) l1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li l1 k1) l1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li l1 k1) l1

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li l1 k1) l1
[PROOF STEP]
have P24 : "Eq (Geos (Lin (Li l1 k1)) 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 l1 k1) l1

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

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
from P9 P24
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li o1 h1) l1
Eq (Geos (Lin (Li l1 k1)) add Emp) (Geos (Lin (Li o1 h1)) add Emp) \<Longrightarrow> Line_on (Li o1 h1) l1
[PROOF STEP]
have P25 : "\<not> Eq (Geos (Lin (Li l1 k1)) add Emp) (Geos (Lin (Li o1 h1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li o1 h1) l1
Eq (Geos (Lin (Li l1 k1)) 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 l1 k1)) add Emp) (Geos (Lin (Li o1 h1)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Lin (Li l1 k1)) add Emp) (Geos (Lin (Li o1 h1)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
from P23 P25
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li o1 h1) o1
\<not> Eq (Geos (Lin (Li l1 k1)) add Emp) (Geos (Lin (Li o1 h1)) add Emp)
[PROOF STEP]
have "Bet_Point (Se l1 k1) o1 \<Longrightarrow> Plane_diffside (Li o1 h1) l1 k1"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li o1 h1) o1
\<not> Eq (Geos (Lin (Li l1 k1)) add Emp) (Geos (Lin (Li o1 h1)) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se l1 k1) o1 \<Longrightarrow> Plane_diffside (Li o1 h1) l1 k1
[PROOF STEP]
by (simp add:Plane_Bet_diffside)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se l1 k1) o1 \<Longrightarrow> Plane_diffside (Li o1 h1) l1 k1

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se l1 k1) o1 \<Longrightarrow> Plane_diffside (Li o1 h1) l1 k1
[PROOF STEP]
have P26 : "Bet_Point (Se l1 k1) o1 \<Longrightarrow> \<not> Plane_sameside (Li o1 h1) l1 k1"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se l1 k1) o1 \<Longrightarrow> Plane_diffside (Li o1 h1) l1 k1

goal (1 subgoal):
 1. Bet_Point (Se l1 k1) o1 \<Longrightarrow> \<not> Plane_sameside (Li o1 h1) l1 k1
[PROOF STEP]
by (simp add:Plane_diffside_not_sameside)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se l1 k1) o1 \<Longrightarrow> \<not> Plane_sameside (Li o1 h1) l1 k1

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
from P16 P26
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li o1 h1) l1 k1
Bet_Point (Se l1 k1) o1 \<Longrightarrow> \<not> Plane_sameside (Li o1 h1) l1 k1
[PROOF STEP]
have P27 : "\<not> Bet_Point (Se l1 k1) o1"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li o1 h1) l1 k1
Bet_Point (Se l1 k1) o1 \<Longrightarrow> \<not> Plane_sameside (Li o1 h1) l1 k1

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

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
have P28 : "Line_on (Li o1 h1) h1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o1 h1) h1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o1 h1) h1

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
have P29 : "\<not> Bet_Point (Se h1 h1) o1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se h1 h1) o1
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se h1 h1) o1

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
[PROOF STEP]
have P30 : "\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi k1) 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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)

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

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
from P10 P21 P22 P27 P28 P29 P30
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi h1) add Emp)
Def (Ang (An l1 o1 h1))
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Line_on (Li o1 l1) k1
\<not> Bet_Point (Se l1 k1) o1
Line_on (Li o1 h1) h1
\<not> Bet_Point (Se h1 h1) o1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi k1) add Emp)
[PROOF STEP]
have P31 : "Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow>
    Eq (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An k1 o1 h1)) add Emp) \<and> Def (Ang (An k1 o1 h1))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi h1) add Emp)
Def (Ang (An l1 o1 h1))
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Line_on (Li o1 l1) k1
\<not> Bet_Point (Se l1 k1) o1
Line_on (Li o1 h1) h1
\<not> Bet_Point (Se h1 h1) o1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi k1) add Emp)

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

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
have P32 : "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. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
from P31 P32
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Eq (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An k1 o1 h1)) add Emp) \<and> Def (Ang (An k1 o1 h1))
Eq (Geos (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An h1 o1 l1)) add Emp)
[PROOF STEP]
have P33 : "Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow>
    Eq (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An k1 o1 h1)) 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 (Ang (An l1 o1 h1)) add Emp) (Geos (Ang (An k1 o1 h1)) add Emp) \<and> Def (Ang (An k1 o1 h1))
Eq (Geos (Ang (An l1 o1 h1)) 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> Eq (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An k1 o1 h1)) add Emp)
[PROOF STEP]
by (blast intro:Eq_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Eq (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An k1 o1 h1)) add Emp)

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

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
from P33 P34
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Eq (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An k1 o1 h1)) add Emp)
Eq (Geos (Ang (An k1 o1 h1)) add Emp) (Geos (Ang (An h1 o1 k1)) add Emp)
[PROOF STEP]
have P35 : "Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow>
    Eq (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h1 o1 k1)) 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 (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An k1 o1 h1)) add Emp)
Eq (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> Eq (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h1 o1 k1)) add Emp)
[PROOF STEP]
by (blast intro:Eq_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Eq (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h1 o1 k1)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
from assms P35
[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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Eq (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h1 o1 k1)) add Emp)
[PROOF STEP]
have P36 : "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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Eq (Geos (Ang (An h1 o1 l1)) 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 h2 o2 l2)) 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 h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
have P37 : "Eq (Geos (Ang (An h2 o2 k2)) add Emp) (Geos (Ang (An k2 o2 h2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (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:
Eq (Geos (Ang (An h2 o2 k2)) add Emp) (Geos (Ang (An k2 o2 h2)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
from assms P37
[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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
Eq (Geos (Ang (An h2 o2 k2)) add Emp) (Geos (Ang (An k2 o2 h2)) add Emp)
[PROOF STEP]
have P38 : "Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An k2 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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
Eq (Geos (Ang (An h2 o2 k2)) add Emp) (Geos (Ang (An k2 o2 h2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An k2 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 k1)) add Emp) (Geos (Ang (An k2 o2 h2)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
have P39 : "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 (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
from P36 P39
[PROOF STATE]
proof (chain)
picking 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)
Eq (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)
[PROOF STEP]
have P40 : "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 l2 o2 h2)) add Emp)"
[PROOF STATE]
proof (prove)
using 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)
Eq (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An l2 o2 h2)) 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 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 h1 o1 k1)) add Emp) (Geos (Ang (An l2 o2 h2)) add Emp)

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

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

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

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

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
from P41 P42
[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 k2)) add Emp) (Geos (Lin (Li k2 o2)) add Emp)
[PROOF STEP]
have P43 : "Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow>
    Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li l2 o2)) 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 k2)) add Emp) (Geos (Lin (Li k2 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 o2 k2)) add Emp) (Geos (Lin (Li l2 o2)) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev 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 o2 k2)) add Emp) (Geos (Lin (Li l2 o2)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
[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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)

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. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
[PROOF STEP]
have P44 : "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. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
from P43 P44
[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 o2 k2)) add Emp) (Geos (Lin (Li l2 o2)) add Emp)
Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li l2 o2)) add Emp)
[PROOF STEP]
have P45 : "Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow>
    Eq (Geos (Lin (Li o2 k2)) 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 o2 k2)) add Emp) (Geos (Lin (Li l2 o2)) add Emp)
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 o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev 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 o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
from assms 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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
[PROOF STEP]
have P46 : "\<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li 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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li o2 k2)) 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]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
from assms P20 P21 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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
Def (Ang (An k1 o1 h1))
Def (Ang (An l1 o1 h1))
\<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
have P47 : "Ang_inside (An k1 o1 h1) l1 \<and> \<not> Ang_inside (An l1 o1 h1) k1
    \<or> \<not> Ang_inside (An k1 o1 h1) l1 \<and> Ang_inside (An l1 o1 h1) k1"
[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
\<not> Ang_inside (An h2 o2 l2) k2
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
Def (Ang (An k1 o1 h1))
Def (Ang (An l1 o1 h1))
\<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)

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

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
from P19 P47
[PROOF STATE]
proof (chain)
picking this:
\<not> Ang_inside (An l1 o1 h1) k1
Ang_inside (An k1 o1 h1) l1 \<and> \<not> Ang_inside (An l1 o1 h1) k1 \<or> \<not> Ang_inside (An k1 o1 h1) l1 \<and> Ang_inside (An l1 o1 h1) k1
[PROOF STEP]
have "Ang_inside (An k1 o1 h1) l1"
[PROOF STATE]
proof (prove)
using this:
\<not> Ang_inside (An l1 o1 h1) k1
Ang_inside (An k1 o1 h1) l1 \<and> \<not> Ang_inside (An l1 o1 h1) k1 \<or> \<not> Ang_inside (An k1 o1 h1) l1 \<and> Ang_inside (An l1 o1 h1) k1

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

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
thus "Ang_inside (An h1 o1 k1) l1"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An k1 o1 h1) l1

goal (1 subgoal):
 1. Ang_inside (An h1 o1 k1) l1
[PROOF STEP]
by (simp add:Ang_inside_def Ang_def_rev)
[PROOF STATE]
proof (state)
this:
Ang_inside (An h1 o1 k1) l1

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

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

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

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

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from assms P1
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
\<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p4 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p4 p11
[PROOF STEP]
have P2 : "\<not> Ang_inside (An p11 p12 p13) p4 \<and> \<not> Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp) \<Longrightarrow>
    Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
\<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p4 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p4 p11

goal (1 subgoal):
 1. \<not> Ang_inside (An p11 p12 p13) p4 \<and> \<not> Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp) \<Longrightarrow> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
by (blast intro:Ang_less_def)
[PROOF STATE]
proof (state)
this:
\<not> Ang_inside (An p11 p12 p13) p4 \<and> \<not> Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp) \<Longrightarrow> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from assms P2
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
\<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
\<not> Ang_inside (An p11 p12 p13) p4 \<and> \<not> Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp) \<Longrightarrow> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
have P3 : "Ang_inside (An p11 p12 p13) p4 \<or> Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
\<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
\<not> Ang_inside (An p11 p12 p13) p4 \<and> \<not> Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp) \<Longrightarrow> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An p11 p12 p13) p4 \<or> Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Ang_inside (An p11 p12 p13) p4 \<or> Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp)

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

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p12 p13) p11 p4
[PROOF STEP]
have P5 : "\<not> Line_on (Li p12 p13) p4"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p12 p13) p11 p4

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

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

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

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

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p12 p13 p4))
[PROOF STEP]
have P7 : "Def (Ang (An p4 p12 p13))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p12 p13 p4))

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from assms P4 P7
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
\<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
Plane_sameside (Li p12 p13) p11 p4
Def (Ang (An p4 p12 p13))
[PROOF STEP]
have P8 : "Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p4 p12 p13)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
\<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
Plane_sameside (Li p12 p13) p11 p4
Def (Ang (An p4 p12 p13))

goal (1 subgoal):
 1. Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p4 p12 p13)) add Emp)
[PROOF STEP]
by (simp add:Ang_move_unique_inv)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p4 p12 p13)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from assms P1 P7 P8
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
\<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p4 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p4 p11
Def (Ang (An p4 p12 p13))
Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p4 p12 p13)) add Emp)
[PROOF STEP]
have P9 : "Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
\<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p4 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p4 p11
Def (Ang (An p4 p12 p13))
Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p4 p12 p13)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
by (blast intro:Ang_trans Ang_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p4 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p4 p11
[PROOF STEP]
have P10 : "Ang_inside (An p11 p12 p13) p4 \<longleftrightarrow>
    Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p4 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p4 p11

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from P3 P9 P10
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An p11 p12 p13) p4 \<or> Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp)
Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Ang_inside (An p11 p12 p13) p4 = Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
show "Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
    \<or> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An p11 p12 p13) p4 \<or> Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp)
Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Ang_inside (An p11 p12 p13) p4 = Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p12 p13) p11 p4
[PROOF STEP]
have P3 : "\<not> Line_on (Li p12 p13) p4"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p12 p13) p11 p4

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

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

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
from P3 P4
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li p12 p13) p4
\<not> Eq (Geos (Poi p12) add Emp) (Geos (Poi p13) add Emp)
[PROOF STEP]
have "Def (Ang (An p12 p13 p4))"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li p12 p13) p4
\<not> Eq (Geos (Poi p12) add Emp) (Geos (Poi p13) add Emp)

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p12 p13 p4))
[PROOF STEP]
have P5 : "Def (Ang (An p4 p12 p13))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p12 p13 p4))

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
from assms P2 P5
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
\<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Plane_sameside (Li p12 p13) p11 p4
Def (Ang (An p4 p12 p13))
[PROOF STEP]
have P6 : "Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p4 p12 p13)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
\<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Plane_sameside (Li p12 p13) p11 p4
Def (Ang (An p4 p12 p13))

goal (1 subgoal):
 1. Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p4 p12 p13)) add Emp)
[PROOF STEP]
by (simp add:Ang_move_unique_inv)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p4 p12 p13)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
from assms P1 P5 P6
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
\<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p4 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p4 p11
Def (Ang (An p4 p12 p13))
Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p4 p12 p13)) add Emp)
[PROOF STEP]
have P7 : "Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
\<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p4 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p4 p11
Def (Ang (An p4 p12 p13))
Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p4 p12 p13)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
by (blast intro:Ang_trans Ang_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)

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

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
from assms P2 P5 P8
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
\<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Plane_sameside (Li p12 p13) p11 p4
Def (Ang (An p4 p12 p13))
\<not> Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp)
[PROOF STEP]
have P9 : "Ang_inside (An p11 p12 p13) p4 \<and> \<not> Ang_inside (An p4 p12 p13) p11
    \<or> \<not> Ang_inside (An p11 p12 p13) p4 \<and> Ang_inside (An p4 p12 p13) p11"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
\<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Plane_sameside (Li p12 p13) p11 p4
Def (Ang (An p4 p12 p13))
\<not> Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An p11 p12 p13) p4 \<and> \<not> Ang_inside (An p4 p12 p13) p11 \<or> \<not> Ang_inside (An p11 p12 p13) p4 \<and> Ang_inside (An p4 p12 p13) p11
[PROOF STEP]
by (simp add:Ang_inside_case)
[PROOF STATE]
proof (state)
this:
Ang_inside (An p11 p12 p13) p4 \<and> \<not> Ang_inside (An p4 p12 p13) p11 \<or> \<not> Ang_inside (An p11 p12 p13) p4 \<and> Ang_inside (An p4 p12 p13) p11

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p4 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p4 p11
[PROOF STEP]
have P10 : "Ang_inside (An p11 p12 p13) p4 \<longleftrightarrow>
    Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p4 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p4 p11

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
from P1 P8
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p4 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p4 p11
\<not> Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp)
[PROOF STEP]
have P11 : "\<not> Ang_inside (An p11 p12 p13) p4 \<Longrightarrow>
    Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p4 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p4 p11
\<not> Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p4)) add Emp)

goal (1 subgoal):
 1. \<not> Ang_inside (An p11 p12 p13) p4 \<Longrightarrow> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
by (blast intro:Ang_less_def)
[PROOF STATE]
proof (state)
this:
\<not> Ang_inside (An p11 p12 p13) p4 \<Longrightarrow> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
from P9 P10 P11
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An p11 p12 p13) p4 \<and> \<not> Ang_inside (An p4 p12 p13) p11 \<or> \<not> Ang_inside (An p11 p12 p13) p4 \<and> Ang_inside (An p4 p12 p13) p11
Ang_inside (An p11 p12 p13) p4 = Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
\<not> Ang_inside (An p11 p12 p13) p4 \<Longrightarrow> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
show "Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
    \<or> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An p11 p12 p13) p4 \<and> \<not> Ang_inside (An p4 p12 p13) p11 \<or> \<not> Ang_inside (An p11 p12 p13) p4 \<and> Ang_inside (An p4 p12 p13) p11
Ang_inside (An p11 p12 p13) p4 = Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
\<not> Ang_inside (An p11 p12 p13) p4 \<Longrightarrow> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
by (simp add:Ang_not_Eq_Gr)
[PROOF STATE]
proof (state)
this:
\<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
have P2 : "\<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow>
    \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow>
    Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)

goal (1 subgoal):
 1. \<lbrakk>\<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp); \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp); \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
\<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
have P3 : "\<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow>
    \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<Longrightarrow>
    Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)

goal (1 subgoal):
 1. \<lbrakk>\<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp); \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp); \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)

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

goal (1 subgoal):
 1. \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
by (simp add:Ang_not_Gr_Eq_rev)
[PROOF STATE]
proof (state)
this:
\<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
have P4 : "\<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<Longrightarrow>
    \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)

goal (1 subgoal):
 1. \<lbrakk>\<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp); \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)\<rbrakk> \<Longrightarrow> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp); \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)\<rbrakk> \<Longrightarrow> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
from P2 P3 P4
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp); \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
\<lbrakk>\<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp); \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
\<lbrakk>\<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp); \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)\<rbrakk> \<Longrightarrow> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
show "Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
    \<or> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
    \<or> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp); \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
\<lbrakk>\<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp); \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
\<lbrakk>\<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp); \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)\<rbrakk> \<Longrightarrow> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<or> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)

goal:
No subgoals!
[PROOF STEP]
qed