[STATEMENT]
lemma (in Congruence_Rule) Ang_not_Gr_lemma1 :
  assumes
    "Def (Ang (An p11 p12 p13))" "Def (Ang (An p21 p22 p23))"
    "Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)"
  shows
    "\<not> 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. \<not> 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. \<not> 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))
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))
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. \<not> 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))
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. \<not> 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 p14 :: Point where P1 : "Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)
    \<and> Plane_sameside (Li p12 p13) p14 p11"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p p11

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

goal (1 subgoal):
 1. \<not> 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 p14 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p14 p11
[PROOF STEP]
have P2 : "Plane_sameside (Li p12 p13) p11 p14"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p14 p11

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

goal (1 subgoal):
 1. \<not> 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 p14
[PROOF STEP]
have P3 : "\<not> Line_on (Li p12 p13) p14"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p12 p13) p11 p14

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

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

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

goal (1 subgoal):
 1. \<not> 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 p14))
[PROOF STEP]
have P5 : "Def (Ang (An p14 p12 p13))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p12 p13 p14))

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

goal (1 subgoal):
 1. \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from assms P1 P5
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
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 p14 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p14 p11
Def (Ang (An p14 p12 p13))
[PROOF STEP]
have P6 : "Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
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 p14 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p14 p11
Def (Ang (An p14 p12 p13))

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

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

goal (1 subgoal):
 1. \<not> 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))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
have P8 : "Def (Ang (An p13 p12 p11))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)

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

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

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

goal (1 subgoal):
 1. \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from P2 P7 P9
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p12 p13) p11 p14
Cong (Geos (Ang (An p13 p12 p11)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
Cong (Geos (Ang (An p13 p12 p11)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)
[PROOF STEP]
have P10 : "Eq (Geos (Lin (Li p11 p12)) add Emp) (Geos (Lin (Li p14 p12)) add Emp) \<and> \<not> Bet_Point (Se p11 p14) p12"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p12 p13) p11 p14
Cong (Geos (Ang (An p13 p12 p11)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
Cong (Geos (Ang (An p13 p12 p11)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)

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

goal (1 subgoal):
 1. \<not> 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 p14 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p14 p11
[PROOF STEP]
have "Ang_inside (An p11 p12 p13) p14 \<longleftrightarrow>
    Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p14 p11

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

goal (1 subgoal):
 1. \<not> 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:
Ang_inside (An p11 p12 p13) p14 = Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
have "Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow>
    Ang_inside (An p11 p12 p13) p14"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An p11 p12 p13) p14 = Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> Ang_inside (An p11 p12 p13) p14
[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) \<Longrightarrow> Ang_inside (An p11 p12 p13) p14

goal (1 subgoal):
 1. \<not> 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:
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> Ang_inside (An p11 p12 p13) p14
[PROOF STEP]
have "Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow>
    Plane_sameside (Li p12 p11) p13 p14"
[PROOF STATE]
proof (prove)
using this:
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> Ang_inside (An p11 p12 p13) p14

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

goal (1 subgoal):
 1. \<not> 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:
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> Plane_sameside (Li p12 p11) p13 p14
[PROOF STEP]
have P11 : "Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow>
    \<not> Line_on (Li p12 p11) p14"
[PROOF STATE]
proof (prove)
using this:
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> Plane_sameside (Li p12 p11) p13 p14

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

goal (1 subgoal):
 1. \<not> 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))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
have "\<not> Eq (Geos (Poi p11) add Emp) (Geos (Poi p12) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
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 p11) add Emp) (Geos (Poi p12) add Emp)
[PROOF STEP]
by (simp add:Ang_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi p11) add Emp) (Geos (Poi p12) add Emp)

goal (1 subgoal):
 1. \<not> 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> Eq (Geos (Poi p11) add Emp) (Geos (Poi p12) add Emp)
[PROOF STEP]
have P12 : "Eq (Geos (Lin (Li p11 p12)) add Emp) (Geos (Lin (Li p12 p11)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi p11) add Emp) (Geos (Poi p12) add Emp)

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

goal (1 subgoal):
 1. \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from P10 P12
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li p11 p12)) add Emp) (Geos (Lin (Li p14 p12)) add Emp) \<and> \<not> Bet_Point (Se p11 p14) p12
Eq (Geos (Lin (Li p11 p12)) add Emp) (Geos (Lin (Li p12 p11)) add Emp)
[PROOF STEP]
have P13 : "Eq (Geos (Lin (Li p14 p12)) add Emp) (Geos (Lin (Li p12 p11)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li p11 p12)) add Emp) (Geos (Lin (Li p14 p12)) add Emp) \<and> \<not> Bet_Point (Se p11 p14) p12
Eq (Geos (Lin (Li p11 p12)) add Emp) (Geos (Lin (Li p12 p11)) add Emp)

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

goal (1 subgoal):
 1. \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
have P14 : "Line_on (Li p14 p12) p14"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p14 p12) p14
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p14 p12) p14

goal (1 subgoal):
 1. \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from P13 P14
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li p14 p12)) add Emp) (Geos (Lin (Li p12 p11)) add Emp)
Line_on (Li p14 p12) p14
[PROOF STEP]
have P15 : "Line_on (Li p12 p11) p14"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li p14 p12)) add Emp) (Geos (Lin (Li p12 p11)) add Emp)
Line_on (Li p14 p12) p14

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

goal (1 subgoal):
 1. \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from P11 P15
[PROOF STATE]
proof (chain)
picking this:
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> \<not> Line_on (Li p12 p11) p14
Line_on (Li p12 p11) p14
[PROOF STEP]
show "\<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> \<not> Line_on (Li p12 p11) p14
Line_on (Li p12 p11) p14

goal (1 subgoal):
 1. \<not> 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:
\<not> 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_Gr :
  assumes
    "Def (Ang (An p11 p12 p13))" "Def (Ang (An p21 p22 p23))"
    "Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)"
  shows
    "\<not> Gr (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)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Gr (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)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> 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))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
show P1 : "\<not> 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))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)

goal (1 subgoal):
 1. \<not> 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_lemma1)
[PROOF STATE]
proof (state)
this:
\<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)

goal (1 subgoal):
 1. \<not> 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))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
have P2 : "Cong (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))
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 p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
by (simp add:Ang_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)

goal (1 subgoal):
 1. \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) 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))
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 p11 p12 p13)) add Emp)
[PROOF STEP]
show "\<not> 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))
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 p11 p12 p13)) add Emp)

goal (1 subgoal):
 1. \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
by (simp add:Ang_not_Gr_lemma1)
[PROOF STATE]
proof (state)
this:
\<not> 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_Gr_not_Eq_rev :
  assumes
    "Def (Ang (An p11 p12 p13))" "Def (Ang (An p21 p22 p23))"
    "Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)"
  shows
    "\<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)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<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)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> 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))
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))
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 (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> 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))
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 (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> 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 p14 :: Point where P1 : "Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)
    \<and> Plane_sameside (Li p12 p13) p14 p11"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p p11

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

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> 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 p14 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p14 p11
[PROOF STEP]
have P2 : "Plane_sameside (Li p12 p13) p11 p14"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p14 p11

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

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> 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 p14
[PROOF STEP]
have P3 : "\<not> Line_on (Li p12 p13) p14"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p12 p13) p11 p14

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

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> 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))
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) 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))
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 (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from P3 P4
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li p12 p13) p14
\<not> Eq (Geos (Poi p12) add Emp) (Geos (Poi p13) add Emp)
[PROOF STEP]
have "Def (Ang (An p12 p13 p14))"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li p12 p13) p14
\<not> Eq (Geos (Poi p12) add Emp) (Geos (Poi p13) add Emp)

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

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> 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 p14))
[PROOF STEP]
have P5 : "Def (Ang (An p14 p12 p13))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p12 p13 p14))

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

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> 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))
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
have "\<not> Line_on (Li p22 p23) p21"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
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 p22 p23) p21
[PROOF STEP]
by (simp add:Ang_to_Tri Tri_def_Line)
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li p22 p23) p21

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> 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 p22 p23) p21
[PROOF STEP]
have "\<exists>p. Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p p22 p23)) add Emp)
    \<and> Plane_sameside (Li p22 p23) p p21"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li p22 p23) p21

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

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> 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 p11 p12 p13)) add Emp) (Geos (Ang (An p p22 p23)) add Emp) \<and> Plane_sameside (Li p22 p23) p p21
[PROOF STEP]
obtain p24 :: Point where P6 : "Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p24 p22 p23)) add Emp)
    \<and> Plane_sameside (Li p22 p23) p24 p21"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p p22 p23)) add Emp) \<and> Plane_sameside (Li p22 p23) p p21

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

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> 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:
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p24 p22 p23)) add Emp) \<and> Plane_sameside (Li p22 p23) p24 p21
[PROOF STEP]
have P7 : "\<not> Line_on (Li p22 p23) p24"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p24 p22 p23)) add Emp) \<and> Plane_sameside (Li p22 p23) p24 p21

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

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> 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))
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
have P8 : "\<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p23) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
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 p22) add Emp) (Geos (Poi p23) add Emp)
[PROOF STEP]
by (simp add:Ang_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p23) add Emp)

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

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

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> 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 p22 p23 p24))
[PROOF STEP]
have P9 : "Def (Ang (An p24 p22 p23))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p22 p23 p24))

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

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from P6
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p24 p22 p23)) add Emp) \<and> Plane_sameside (Li p22 p23) p24 p21
[PROOF STEP]
have P10 : "Plane_sameside (Li p22 p23) p21 p24"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p24 p22 p23)) add Emp) \<and> Plane_sameside (Li p22 p23) p24 p21

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

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> 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))
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
have P11 : "Def (Ang (An p13 p12 p11))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)

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

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> 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))
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
have P12 : "Def (Ang (An p23 p22 p21))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)

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

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

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

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

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

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
have P15 : "Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p13 p12 p11)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p13 p12 p11)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p13 p12 p11)) add Emp)

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
have P16 : "Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p23 p22 p21)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p23 p22 p21)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p23 p22 p21)) add Emp)

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
have P17 : "Cong (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p13 p12 p14)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p13 p12 p14)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p13 p12 p14)) add Emp)

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
have P18 : "Cong (Geos (Ang (An p24 p22 p23)) add Emp) (Geos (Ang (An p23 p22 p24)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An p24 p22 p23)) add Emp) (Geos (Ang (An p23 p22 p24)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p24 p22 p23)) add Emp) (Geos (Ang (An p23 p22 p24)) add Emp)

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from assms P6 P9 P11 P15
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p24 p22 p23)) add Emp) \<and> Plane_sameside (Li p22 p23) p24 p21
Def (Ang (An p24 p22 p23))
Def (Ang (An p13 p12 p11))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p13 p12 p11)) add Emp)
[PROOF STEP]
have P19 :
    "Cong (Geos (Ang (An p13 p12 p11)) add Emp) (Geos (Ang (An p24 p22 p23)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p24 p22 p23)) add Emp) \<and> Plane_sameside (Li p22 p23) p24 p21
Def (Ang (An p24 p22 p23))
Def (Ang (An p13 p12 p11))
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p13 p12 p11)) add Emp)

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

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from P9 P11 P14 P18 P19
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p24 p22 p23))
Def (Ang (An p13 p12 p11))
Def (Ang (An p23 p22 p24))
Cong (Geos (Ang (An p24 p22 p23)) add Emp) (Geos (Ang (An p23 p22 p24)) add Emp)
Cong (Geos (Ang (An p13 p12 p11)) add Emp) (Geos (Ang (An p24 p22 p23)) add Emp)
[PROOF STEP]
have P20 :
    "Cong (Geos (Ang (An p13 p12 p11)) add Emp) (Geos (Ang (An p23 p22 p24)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p24 p22 p23))
Def (Ang (An p13 p12 p11))
Def (Ang (An p23 p22 p24))
Cong (Geos (Ang (An p24 p22 p23)) add Emp) (Geos (Ang (An p23 p22 p24)) add Emp)
Cong (Geos (Ang (An p13 p12 p11)) add Emp) (Geos (Ang (An p24 p22 p23)) add Emp)

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

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from assms P1 P5 P12 P16
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
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 p14 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p14 p11
Def (Ang (An p14 p12 p13))
Def (Ang (An p23 p22 p21))
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p23 p22 p21)) add Emp)
[PROOF STEP]
have P21 :
    "Cong (Geos (Ang (An p23 p22 p21)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
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 p14 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p14 p11
Def (Ang (An p14 p12 p13))
Def (Ang (An p23 p22 p21))
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p23 p22 p21)) add Emp)

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

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from P5 P12 P13 P17 P21
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p14 p12 p13))
Def (Ang (An p23 p22 p21))
Def (Ang (An p13 p12 p14))
Cong (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p13 p12 p14)) add Emp)
Cong (Geos (Ang (An p23 p22 p21)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)
[PROOF STEP]
have P22 :
    "Cong (Geos (Ang (An p23 p22 p21)) add Emp) (Geos (Ang (An p13 p12 p14)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p14 p12 p13))
Def (Ang (An p23 p22 p21))
Def (Ang (An p13 p12 p14))
Cong (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p13 p12 p14)) add Emp)
Cong (Geos (Ang (An p23 p22 p21)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)

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

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from P6
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p24 p22 p23)) add Emp) \<and> Plane_sameside (Li p22 p23) p24 p21
[PROOF STEP]
have P23 : "Ang_inside (An p21 p22 p23) p24 \<longleftrightarrow>
    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 p11 p12 p13)) add Emp) (Geos (Ang (An p24 p22 p23)) add Emp) \<and> Plane_sameside (Li p22 p23) p24 p21

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

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from assms P23
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
Ang_inside (An p21 p22 p23) p24 = Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
have P24 : "Ang_inside (An p21 p22 p23) p24"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
Ang_inside (An p21 p22 p23) p24 = Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)

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

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from P12 P24
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p23 p22 p21))
Ang_inside (An p21 p22 p23) p24
[PROOF STEP]
have P25 : "Ang_inside (An p23 p22 p21) p24"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p23 p22 p21))
Ang_inside (An p21 p22 p23) p24

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

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from P2 P6 P11 P12 P20 P22 P25
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p12 p13) p11 p14
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p24 p22 p23)) add Emp) \<and> Plane_sameside (Li p22 p23) p24 p21
Def (Ang (An p13 p12 p11))
Def (Ang (An p23 p22 p21))
Cong (Geos (Ang (An p13 p12 p11)) add Emp) (Geos (Ang (An p23 p22 p24)) add Emp)
Cong (Geos (Ang (An p23 p22 p21)) add Emp) (Geos (Ang (An p13 p12 p14)) add Emp)
Ang_inside (An p23 p22 p21) p24
[PROOF STEP]
have P26 : "\<not> Ang_inside (An p13 p12 p11) p14
    \<and> \<not> Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p14)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p12 p13) p11 p14
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p24 p22 p23)) add Emp) \<and> Plane_sameside (Li p22 p23) p24 p21
Def (Ang (An p13 p12 p11))
Def (Ang (An p23 p22 p21))
Cong (Geos (Ang (An p13 p12 p11)) add Emp) (Geos (Ang (An p23 p22 p24)) add Emp)
Cong (Geos (Ang (An p23 p22 p21)) add Emp) (Geos (Ang (An p13 p12 p14)) add Emp)
Ang_inside (An p23 p22 p21) p24

goal (1 subgoal):
 1. \<not> Ang_inside (An p13 p12 p11) p14 \<and> \<not> Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p14)) add Emp)
[PROOF STEP]
by (simp add:Ang_move_Greater)
[PROOF STATE]
proof (state)
this:
\<not> Ang_inside (An p13 p12 p11) p14 \<and> \<not> Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p14)) add Emp)

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> 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 p14 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p14 p11
[PROOF STEP]
have "Ang_inside (An p11 p12 p13) p14 \<longleftrightarrow>
    Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p14 p11

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

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> 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:
Ang_inside (An p11 p12 p13) p14 = Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
have P27 : "Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow>
    Ang_inside (An p11 p12 p13) p14"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An p11 p12 p13) p14 = Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> Ang_inside (An p11 p12 p13) p14
[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) \<Longrightarrow> Ang_inside (An p11 p12 p13) p14

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from P11 P27
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p13 p12 p11))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> Ang_inside (An p11 p12 p13) p14
[PROOF STEP]
have P28 : "Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow>
    Ang_inside (An p13 p12 p11) p14"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p13 p12 p11))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> Ang_inside (An p11 p12 p13) p14

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

goal (2 subgoals):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
 2. \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from P26 P28
[PROOF STATE]
proof (chain)
picking this:
\<not> Ang_inside (An p13 p12 p11) p14 \<and> \<not> Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p14)) add Emp)
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> Ang_inside (An p13 p12 p11) p14
[PROOF STEP]
show "\<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Ang_inside (An p13 p12 p11) p14 \<and> \<not> Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p14)) add Emp)
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> Ang_inside (An p13 p12 p11) p14

goal (1 subgoal):
 1. \<not> 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:
\<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)

goal (1 subgoal):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from assms P1 P5
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
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 p14 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p14 p11
Def (Ang (An p14 p12 p13))
[PROOF STEP]
have P29 : "Cong (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 p14 p12 p13)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
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 p14 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p14 p11
Def (Ang (An p14 p12 p13))

goal (1 subgoal):
 1. Cong (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 p14 p12 p13)) add Emp)
[PROOF STEP]
by (blast intro:Ang_rev Ang_trans)
[PROOF STATE]
proof (state)
this:
Cong (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 p14 p12 p13)) add Emp)

goal (1 subgoal):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
have P30 : "Cong (Geos (Ang (An p13 p12 p11)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An p13 p12 p11)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p13 p12 p11)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)

goal (1 subgoal):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from assms P5 P11 P29 P30
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
Def (Ang (An p14 p12 p13))
Def (Ang (An p13 p12 p11))
Cong (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 p14 p12 p13)) add Emp)
Cong (Geos (Ang (An p13 p12 p11)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
have P31 : "Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An p13 p12 p11)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
Def (Ang (An p14 p12 p13))
Def (Ang (An p13 p12 p11))
Cong (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 p14 p12 p13)) add Emp)
Cong (Geos (Ang (An p13 p12 p11)) 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) \<Longrightarrow> Cong (Geos (Ang (An p13 p12 p11)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)
[PROOF STEP]
by (blast intro:Ang_rev Ang_trans)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p13 p12 p11)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)

goal (1 subgoal):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from P2 P30 P31
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p12 p13) p11 p14
Cong (Geos (Ang (An p13 p12 p11)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p13 p12 p11)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)
[PROOF STEP]
have P32 : "Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow>
    Eq (Geos (Lin (Li p11 p12)) add Emp) (Geos (Lin (Li p14 p12)) add Emp) \<and> \<not> Bet_Point (Se p11 p14) p12"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p12 p13) p11 p14
Cong (Geos (Ang (An p13 p12 p11)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p13 p12 p11)) add Emp) (Geos (Ang (An p14 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) \<Longrightarrow> Eq (Geos (Lin (Li p11 p12)) add Emp) (Geos (Lin (Li p14 p12)) add Emp) \<and> \<not> Bet_Point (Se p11 p14) p12
[PROOF STEP]
by (simp add:Ang_move_unique)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li p11 p12)) add Emp) (Geos (Lin (Li p14 p12)) add Emp) \<and> \<not> Bet_Point (Se p11 p14) p12

goal (1 subgoal):
 1. \<not> Cong (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))
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
have "\<not> Eq (Geos (Poi p11) add Emp) (Geos (Poi p12) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
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 p11) add Emp) (Geos (Poi p12) add Emp)
[PROOF STEP]
by (simp add:Ang_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi p11) add Emp) (Geos (Poi p12) add Emp)

goal (1 subgoal):
 1. \<not> Cong (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> Eq (Geos (Poi p11) add Emp) (Geos (Poi p12) add Emp)
[PROOF STEP]
have P33 : "Eq (Geos (Lin (Li p11 p12)) add Emp) (Geos (Lin (Li p12 p11)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi p11) add Emp) (Geos (Poi p12) add Emp)

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

goal (1 subgoal):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from P32 P33
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li p11 p12)) add Emp) (Geos (Lin (Li p14 p12)) add Emp) \<and> \<not> Bet_Point (Se p11 p14) p12
Eq (Geos (Lin (Li p11 p12)) add Emp) (Geos (Lin (Li p12 p11)) add Emp)
[PROOF STEP]
have P34 : "Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow>
    Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p14 p12)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li p11 p12)) add Emp) (Geos (Lin (Li p14 p12)) add Emp) \<and> \<not> Bet_Point (Se p11 p14) p12
Eq (Geos (Lin (Li p11 p12)) add Emp) (Geos (Lin (Li p12 p11)) add Emp)

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

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

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

goal (1 subgoal):
 1. \<not> Cong (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> Eq (Geos (Poi p14) add Emp) (Geos (Poi p12) add Emp)
[PROOF STEP]
have P35 : "Eq (Geos (Lin (Li p14 p12)) add Emp) (Geos (Lin (Li p12 p14)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi p14) add Emp) (Geos (Poi p12) add Emp)

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

goal (1 subgoal):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from P34 P35
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p14 p12)) add Emp)
Eq (Geos (Lin (Li p14 p12)) add Emp) (Geos (Lin (Li p12 p14)) add Emp)
[PROOF STEP]
have P36 : "Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow>
    Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p14)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p14 p12)) add Emp)
Eq (Geos (Lin (Li p14 p12)) add Emp) (Geos (Lin (Li p12 p14)) add Emp)

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

goal (1 subgoal):
 1. \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
from P26 P36
[PROOF STATE]
proof (chain)
picking this:
\<not> Ang_inside (An p13 p12 p11) p14 \<and> \<not> Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p14)) add Emp)
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p14)) add Emp)
[PROOF STEP]
show "\<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Ang_inside (An p13 p12 p11) p14 \<and> \<not> Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p14)) add Emp)
Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li p12 p11)) add Emp) (Geos (Lin (Li p12 p14)) add Emp)

goal (1 subgoal):
 1. \<not> 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:
\<not> Cong (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_relation_case_fact :
  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)
    \<and> \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
    \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
    \<or> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
    \<and> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
    \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
    \<or> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
    \<and> \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
    \<and> 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) \<and> \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<or> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<or> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> 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) \<and> \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<or> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<or> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> 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 : "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:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))

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 (simp add:Ang_relation_case)
[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 (1 subgoal):
 1. Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<or> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<or> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> 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 P2 : "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)
    \<and> \<not> 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. 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) \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
by (simp add:Ang_not_Gr)
[PROOF STATE]
proof (state)
this:
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) \<and> \<not> 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) \<and> \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<or> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<or> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> 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 P3 : "Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<Longrightarrow>
    \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
    \<and> \<not> 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. Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<Longrightarrow> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
by (simp add:Ang_Gr_not_Eq_rev)
[PROOF STATE]
proof (state)
this:
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<Longrightarrow> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> 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) \<and> \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<or> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<or> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> 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 "Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow>
    \<not> Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
    \<and> \<not> 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. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> \<not> Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
by (simp add:Ang_Gr_not_Eq_rev)
[PROOF STATE]
proof (state)
this:
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> \<not> Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<and> \<not> 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) \<and> \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<or> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<or> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> 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:
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> \<not> Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
have P4 : "Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow>
    \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
    \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> \<not> Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<and> \<not> 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) \<Longrightarrow> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
by (blast intro:Ang_rev)
[PROOF STATE]
proof (state)
this:
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> 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) \<and> \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<or> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<or> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
from P1 P2 P3 P4
[PROOF STATE]
proof (chain)
picking 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)
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) \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<Longrightarrow> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
show "Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
    \<and> \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
    \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
    \<or> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
    \<and> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
    \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
    \<or> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
    \<and> \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
    \<and> 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 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)
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) \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<Longrightarrow> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<Longrightarrow> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> 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) \<and> \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<or> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<or> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> 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) \<and> \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<or> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp) \<or> \<not> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> \<not> Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp) \<and> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)

goal:
No subgoals!
[PROOF STEP]
qed