[STATEMENT]
lemma (in Congruence_Rule) Tri_week_SSS_lemma1 :
  assumes
    "Plane_diffside (Li x y) z1 z2"
    "\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)"
    "Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)"
    "Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)"
    "\<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p \<and> Eq (Geos (Poi x) add Emp) (Geos (Poi p) add Emp)"
  shows "Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
\<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p \<and> Eq (Geos (Poi x) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
have P1 : "\<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p
    \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
\<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p \<and> Eq (Geos (Poi x) add Emp) (Geos (Poi p) add Emp)

goal (1 subgoal):
 1. \<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
[PROOF STEP]
by (simp add:Plane_diffside_def)
[PROOF STATE]
proof (state)
this:
\<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
\<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p \<and> Eq (Geos (Poi x) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
obtain pn :: Point where P2 : "Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
\<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p \<and> Eq (Geos (Poi x) add Emp) (Geos (Poi p) add Emp)

goal (1 subgoal):
 1. (\<And>pn. Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from P2
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp)
[PROOF STEP]
have P3 : "Bet_Point (Se z1 z2) pn"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se z1 z2) pn
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Bet_Point (Se z1 z2) pn

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) pn
[PROOF STEP]
have P4 : "Line_on (Li z1 z2) pn"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) pn

goal (1 subgoal):
 1. Line_on (Li z1 z2) pn
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li z1 z2) pn

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from P2 P4
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp)
Line_on (Li z1 z2) pn
[PROOF STEP]
have P5 : "Line_on (Li z1 z2) x"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp)
Line_on (Li z1 z2) pn

goal (1 subgoal):
 1. Line_on (Li z1 z2) x
[PROOF STEP]
by (blast intro:Eq_rev Point_Eq)
[PROOF STATE]
proof (state)
this:
Line_on (Li z1 z2) x

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from assms P3
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
\<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p \<and> Eq (Geos (Poi x) add Emp) (Geos (Poi p) add Emp)
Bet_Point (Se z1 z2) pn
[PROOF STEP]
have P6 : "Bet_Point (Se z1 z2) x"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
\<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p \<and> Eq (Geos (Poi x) add Emp) (Geos (Poi p) add Emp)
Bet_Point (Se z1 z2) pn

goal (1 subgoal):
 1. Bet_Point (Se z1 z2) x
[PROOF STEP]
by (blast intro:Eq_rev Point_Eq)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se z1 z2) x

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
have P7 : "Line_on (Li x y) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li x y) x
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li x y) x

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
have P8 : "Line_on (Li x y) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li x y) y
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li x y) y

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from assms P5 P7 P8
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
\<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p \<and> Eq (Geos (Poi x) add Emp) (Geos (Poi p) add Emp)
Line_on (Li z1 z2) x
Line_on (Li x y) x
Line_on (Li x y) y
[PROOF STEP]
have P9 : "Line_on (Li z1 z2) y \<Longrightarrow> Eq (Geos (Lin (Li z1 z2)) add Emp) (Geos (Lin (Li x y)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
\<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p \<and> Eq (Geos (Poi x) add Emp) (Geos (Poi p) add Emp)
Line_on (Li z1 z2) x
Line_on (Li x y) x
Line_on (Li x y) y

goal (1 subgoal):
 1. Line_on (Li z1 z2) y \<Longrightarrow> Eq (Geos (Lin (Li z1 z2)) add Emp) (Geos (Lin (Li x y)) add Emp)
[PROOF STEP]
by (simp add:Line_unique)
[PROOF STATE]
proof (state)
this:
Line_on (Li z1 z2) y \<Longrightarrow> Eq (Geos (Lin (Li z1 z2)) add Emp) (Geos (Lin (Li x y)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
have P10 : "Line_on (Li z1 z2) z1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li z1 z2) z1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li z1 z2) z1

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from P9 P10
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li z1 z2) y \<Longrightarrow> Eq (Geos (Lin (Li z1 z2)) add Emp) (Geos (Lin (Li x y)) add Emp)
Line_on (Li z1 z2) z1
[PROOF STEP]
have P11 : "Line_on (Li z1 z2) y \<Longrightarrow> Line_on (Li x y) z1"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li z1 z2) y \<Longrightarrow> Eq (Geos (Lin (Li z1 z2)) add Emp) (Geos (Lin (Li x y)) add Emp)
Line_on (Li z1 z2) z1

goal (1 subgoal):
 1. Line_on (Li z1 z2) y \<Longrightarrow> Line_on (Li x y) z1
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Line_on (Li z1 z2) y \<Longrightarrow> Line_on (Li x y) z1

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from P1 P11
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Line_on (Li z1 z2) y \<Longrightarrow> Line_on (Li x y) z1
[PROOF STEP]
have P12 : "\<not> Line_on (Li z1 z2) y"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Line_on (Li z1 z2) y \<Longrightarrow> Line_on (Li x y) z1

goal (1 subgoal):
 1. \<not> Line_on (Li z1 z2) y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li z1 z2) y

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from P3
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) pn
[PROOF STEP]
have P13 : "\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi z2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) pn

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from P8
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li x y) y
[PROOF STEP]
have P14 : "Eq (Geos (Poi z2) add Emp) (Geos (Poi y) add Emp) \<Longrightarrow> Line_on (Li x y) z2"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li x y) y

goal (1 subgoal):
 1. Eq (Geos (Poi z2) add Emp) (Geos (Poi y) add Emp) \<Longrightarrow> Line_on (Li x y) z2
[PROOF STEP]
by (blast intro:Eq_rev Point_Eq)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi z2) add Emp) (Geos (Poi y) add Emp) \<Longrightarrow> Line_on (Li x y) z2

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from P1 P14
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Eq (Geos (Poi z2) add Emp) (Geos (Poi y) add Emp) \<Longrightarrow> Line_on (Li x y) z2
[PROOF STEP]
have P15 : "\<not> Eq (Geos (Poi z2) add Emp) (Geos (Poi y) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Eq (Geos (Poi z2) add Emp) (Geos (Poi y) add Emp) \<Longrightarrow> Line_on (Li x y) z2

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from P8
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li x y) y
[PROOF STEP]
have P16 : "Eq (Geos (Poi y) add Emp) (Geos (Poi z1) add Emp) \<Longrightarrow> Line_on (Li x y) z1"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li x y) y

goal (1 subgoal):
 1. Eq (Geos (Poi y) add Emp) (Geos (Poi z1) add Emp) \<Longrightarrow> Line_on (Li x y) z1
[PROOF STEP]
by (blast intro:Eq_rev Point_Eq)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi y) add Emp) (Geos (Poi z1) add Emp) \<Longrightarrow> Line_on (Li x y) z1

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from P1 P16
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Eq (Geos (Poi y) add Emp) (Geos (Poi z1) add Emp) \<Longrightarrow> Line_on (Li x y) z1
[PROOF STEP]
have P17 : "\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi z1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Eq (Geos (Poi y) add Emp) (Geos (Poi z1) add Emp) \<Longrightarrow> Line_on (Li x y) z1

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from P12 P13
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li z1 z2) y
\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi z2) add Emp)
[PROOF STEP]
have P18 : "Def (Tri (Tr z1 z2 y))"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li z1 z2) y
\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi z2) add Emp)

goal (1 subgoal):
 1. Def (Tri (Tr z1 z2 y))
[PROOF STEP]
by (simp add:Ang_sinple_def Ang_to_Tri)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr z1 z2 y))

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr z1 z2 y))
[PROOF STEP]
have P19 : "Def (Tri (Tr y z1 z2))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr z1 z2 y))

goal (1 subgoal):
 1. Def (Tri (Tr y z1 z2))
[PROOF STEP]
by (blast intro:Tri_def_trans)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr y z1 z2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from assms P19
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
\<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p \<and> Eq (Geos (Poi x) add Emp) (Geos (Poi p) add Emp)
Def (Tri (Tr y z1 z2))
[PROOF STEP]
have P20 : "Cong (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An y z2 z1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
\<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p \<and> Eq (Geos (Poi x) add Emp) (Geos (Poi p) add Emp)
Def (Tri (Tr y z1 z2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An y z2 z1)) add Emp)
[PROOF STEP]
by (simp add:Tri_isosceles)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An y z2 z1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from P18
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr z1 z2 y))
[PROOF STEP]
have P21 : "Def (Ang (An z1 z2 y))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr z1 z2 y))

goal (1 subgoal):
 1. Def (Ang (An z1 z2 y))
[PROOF STEP]
by (simp add:Tri_to_Ang)
[PROOF STATE]
proof (state)
this:
Def (Ang (An z1 z2 y))

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from P6
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) x
[PROOF STEP]
have P22 : "Line_on (Li z2 z1) x"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) x

goal (1 subgoal):
 1. Line_on (Li z2 z1) x
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li z2 z1) x

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from P6
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) x
[PROOF STEP]
have P23 : "Inv (Bet_Point (Se z2 x) z1) \<and> Inv (Bet_Point (Se x z1) z2)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) x

goal (1 subgoal):
 1. Inv (Bet_Point (Se z2 x) z1) \<and> Inv (Bet_Point (Se x z1) z2)
[PROOF STEP]
by (simp add:Bet_iff)
[PROOF STATE]
proof (state)
this:
Inv (Bet_Point (Se z2 x) z1) \<and> Inv (Bet_Point (Se x z1) z2)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Inv (Bet_Point (Se z2 x) z1) \<and> Inv (Bet_Point (Se x z1) z2)
[PROOF STEP]
have "\<not> Bet_Point (Se x z1) z2"
[PROOF STATE]
proof (prove)
using this:
Inv (Bet_Point (Se z2 x) z1) \<and> Inv (Bet_Point (Se x z1) z2)

goal (1 subgoal):
 1. \<not> Bet_Point (Se x z1) z2
[PROOF STEP]
by (simp add:Inv_def)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se x z1) z2

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Bet_Point (Se x z1) z2
[PROOF STEP]
have P24 : "\<not> Bet_Point (Se z1 x) z2"
[PROOF STATE]
proof (prove)
using this:
\<not> Bet_Point (Se x z1) z2

goal (1 subgoal):
 1. \<not> Bet_Point (Se z1 x) z2
[PROOF STEP]
by (blast intro:Bet_rev)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se z1 x) z2

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
have P25 : "Line_on (Li z2 y) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li z2 y) y
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li z2 y) y

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
have P26 : "\<not> Bet_Point (Se y y) z2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se y y) z2
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se y y) z2

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from P6
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) x
[PROOF STEP]
have P27 : "\<not> Eq (Geos (Poi z2) add Emp) (Geos (Poi x) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) x

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from P15 P21 P22 P24 P25 P26 P27
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi z2) add Emp) (Geos (Poi y) add Emp)
Def (Ang (An z1 z2 y))
Line_on (Li z2 z1) x
\<not> Bet_Point (Se z1 x) z2
Line_on (Li z2 y) y
\<not> Bet_Point (Se y y) z2
\<not> Eq (Geos (Poi z2) add Emp) (Geos (Poi x) add Emp)
[PROOF STEP]
have P28 :
    "Eq (Geos (Ang (An z1 z2 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp) \<and> Def (Ang (An x z2 y))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi z2) add Emp) (Geos (Poi y) add Emp)
Def (Ang (An z1 z2 y))
Line_on (Li z2 z1) x
\<not> Bet_Point (Se z1 x) z2
Line_on (Li z2 y) y
\<not> Bet_Point (Se y y) z2
\<not> Eq (Geos (Poi z2) add Emp) (Geos (Poi x) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Ang (An z1 z2 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp) \<and> Def (Ang (An x z2 y))
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An z1 z2 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp) \<and> Def (Ang (An x z2 y))

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
have P29 : "Eq (Geos (Ang (An y z2 z1)) add Emp) (Geos (Ang (An z1 z2 y)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An y z2 z1)) add Emp) (Geos (Ang (An z1 z2 y)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An y z2 z1)) add Emp) (Geos (Ang (An z1 z2 y)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from P20 P29
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An y z2 z1)) add Emp)
Eq (Geos (Ang (An y z2 z1)) add Emp) (Geos (Ang (An z1 z2 y)) add Emp)
[PROOF STEP]
have P30 : "Cong (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An z1 z2 y)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An y z2 z1)) add Emp)
Eq (Geos (Ang (An y z2 z1)) add Emp) (Geos (Ang (An z1 z2 y)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An z1 z2 y)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An z1 z2 y)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from P28 P30
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An z1 z2 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp) \<and> Def (Ang (An x z2 y))
Cong (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An z1 z2 y)) add Emp)
[PROOF STEP]
have P31 : "Cong (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An x z2 y)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An z1 z2 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp) \<and> Def (Ang (An x z2 y))
Cong (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An z1 z2 y)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An x z2 y)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from P19
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr y z1 z2))
[PROOF STEP]
have P32 : "Def (Ang (An z2 z1 y))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr y z1 z2))

goal (1 subgoal):
 1. Def (Ang (An z2 z1 y))
[PROOF STEP]
by (blast intro:Tri_to_Ang Tri_def_rev)
[PROOF STATE]
proof (state)
this:
Def (Ang (An z2 z1 y))

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from P6
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) x
[PROOF STEP]
have P33 : "Line_on (Li z1 z2) x"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) x

goal (1 subgoal):
 1. Line_on (Li z1 z2) x
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li z1 z2) x

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from P23
[PROOF STATE]
proof (chain)
picking this:
Inv (Bet_Point (Se z2 x) z1) \<and> Inv (Bet_Point (Se x z1) z2)
[PROOF STEP]
have P34 : "\<not> Bet_Point (Se z2 x) z1"
[PROOF STATE]
proof (prove)
using this:
Inv (Bet_Point (Se z2 x) z1) \<and> Inv (Bet_Point (Se x z1) z2)

goal (1 subgoal):
 1. \<not> Bet_Point (Se z2 x) z1
[PROOF STEP]
by (simp add:Inv_def)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se z2 x) z1

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
have P35 : "Line_on (Li z1 y) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li z1 y) y
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li z1 y) y

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
have P36 : "\<not> Bet_Point (Se y y) z1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se y y) z1
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se y y) z1

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from P6
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) x
[PROOF STEP]
have "\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi z1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) x

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi z1) add Emp)
[PROOF STEP]
have P37 : "\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi x) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi z1) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from P17
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi z1) add Emp)
[PROOF STEP]
have P38 : "\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi y) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi z1) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from P32 P33 P34 P35 P36 P37 P38
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An z2 z1 y))
Line_on (Li z1 z2) x
\<not> Bet_Point (Se z2 x) z1
Line_on (Li z1 y) y
\<not> Bet_Point (Se y y) z1
\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi x) add Emp)
\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi y) add Emp)
[PROOF STEP]
have P39 :
    "Eq (Geos (Ang (An z2 z1 y)) add Emp) (Geos (Ang (An x z1 y)) add Emp) \<and> Def (Ang (An x z1 y))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An z2 z1 y))
Line_on (Li z1 z2) x
\<not> Bet_Point (Se z2 x) z1
Line_on (Li z1 y) y
\<not> Bet_Point (Se y y) z1
\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi x) add Emp)
\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi y) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Ang (An z2 z1 y)) add Emp) (Geos (Ang (An x z1 y)) add Emp) \<and> Def (Ang (An x z1 y))
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An z2 z1 y)) add Emp) (Geos (Ang (An x z1 y)) add Emp) \<and> Def (Ang (An x z1 y))

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
have P40 : "Eq (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An z2 z1 y)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An z2 z1 y)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An z2 z1 y)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from P31 P40
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
Eq (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An z2 z1 y)) add Emp)
[PROOF STEP]
have P41 : "Cong (Geos (Ang (An z2 z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
Eq (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An z2 z1 y)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An z2 z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An z2 z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
from P39 P41
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An z2 z1 y)) add Emp) (Geos (Ang (An x z1 y)) add Emp) \<and> Def (Ang (An x z1 y))
Cong (Geos (Ang (An z2 z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
show "Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An z2 z1 y)) add Emp) (Geos (Ang (An x z1 y)) add Emp) \<and> Def (Ang (An x z1 y))
Cong (Geos (Ang (An z2 z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)

goal:
No subgoals!
[PROOF STEP]
qed