[STATEMENT]
lemma (in Congruence_Rule) Tri_AAS_lemma1 :
  assumes
    "Def (Tri (Tr A1 B1 C1))" "Def (Tri (Tr A2 B2 C2))"
    "Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)"
    "Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)"
    "Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)"
  shows
    "Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P1 : "Line_on (Li A2 C2) A2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A2 C2) A2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A2 C2) A2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P2 : "Line_on (Li A2 C2) C2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A2 C2) C2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A2 C2) C2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
[PROOF STEP]
have "\<not> Eq (Geos (Poi C1) add Emp) (Geos (Poi A1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi C1) add Emp) (Geos (Poi A1) add Emp)
[PROOF STEP]
have P3 : "\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi C1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi C1) add Emp) (Geos (Poi A1) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
[PROOF STEP]
have P4 : "\<not> Eq (Geos (Poi C2) add Emp) (Geos (Poi A2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi C2) add Emp) (Geos (Poi A2) add Emp)
[PROOF STEP]
have P5 : "\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi C2) add Emp) (Geos (Poi A2) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P1 P2 P3 P5
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A2 C2) A2
Line_on (Li A2 C2) C2
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi C1) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)
[PROOF STEP]
have "\<exists>p. Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 p)) add Emp)
    \<and> \<not> Bet_Point (Se p C2) A2 \<and> Line_on (Li A2 C2) p \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi p) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A2 C2) A2
Line_on (Li A2 C2) C2
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi C1) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 p)) add Emp) \<and> \<not> Bet_Point (Se p C2) A2 \<and> Line_on (Li A2 C2) p \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
by (simp add:Seg_move_sameside)
[PROOF STATE]
proof (state)
this:
\<exists>p. Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 p)) add Emp) \<and> \<not> Bet_Point (Se p C2) A2 \<and> Line_on (Li A2 C2) p \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi p) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 p)) add Emp) \<and> \<not> Bet_Point (Se p C2) A2 \<and> Line_on (Li A2 C2) p \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
obtain C3 :: Point where P6 : "Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C3)) add Emp)
    \<and> \<not> Bet_Point (Se C3 C2) A2 \<and> Line_on (Li A2 C2) C3 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C3) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 p)) add Emp) \<and> \<not> Bet_Point (Se p C2) A2 \<and> Line_on (Li A2 C2) p \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi p) add Emp)

goal (1 subgoal):
 1. (\<And>C3. Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<and> \<not> Bet_Point (Se C3 C2) A2 \<and> Line_on (Li A2 C2) C3 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C3) add Emp) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<and> \<not> Bet_Point (Se C3 C2) A2 \<and> Line_on (Li A2 C2) C3 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C3) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P6
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<and> \<not> Bet_Point (Se C3 C2) A2 \<and> Line_on (Li A2 C2) C3 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C3) add Emp)
[PROOF STEP]
have P7 : "Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow>
    Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<and> \<not> Bet_Point (Se C3 C2) A2 \<and> Line_on (Li A2 C2) C3 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C3) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev Eq_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms P7
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)
[PROOF STEP]
have P8 : "Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow>
    Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
by (simp add:Tri_SAS)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P6
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<and> \<not> Bet_Point (Se C3 C2) A2 \<and> Line_on (Li A2 C2) C3 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C3) add Emp)
[PROOF STEP]
have "Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C2)) add Emp) \<Longrightarrow>
    Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<and> \<not> Bet_Point (Se C3 C2) A2 \<and> Line_on (Li A2 C2) C3 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C3) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C2)) add Emp) \<Longrightarrow> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev Eq_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C2)) add Emp) \<Longrightarrow> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C2)) add Emp) \<Longrightarrow> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp)
[PROOF STEP]
have P9 : "\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow>
    \<not> Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C2)) add Emp) \<Longrightarrow> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> \<not> Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> \<not> Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P1 P2 P3 P5 P6 P9
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A2 C2) A2
Line_on (Li A2 C2) C2
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi C1) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<and> \<not> Bet_Point (Se C3 C2) A2 \<and> Line_on (Li A2 C2) C3 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C3) add Emp)
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> \<not> Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)
[PROOF STEP]
have P10 : "\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow>
    Bet_Point (Se C2 A2) C3 \<and> \<not> Bet_Point (Se A2 C3) C2
    \<or> \<not> Bet_Point (Se C2 A2) C3 \<and> Bet_Point (Se A2 C3) C2"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A2 C2) A2
Line_on (Li A2 C2) C2
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi C1) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<and> \<not> Bet_Point (Se C3 C2) A2 \<and> Line_on (Li A2 C2) C3 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C3) add Emp)
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> \<not> Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Bet_Point (Se C2 A2) C3 \<and> \<not> Bet_Point (Se A2 C3) C2 \<or> \<not> Bet_Point (Se C2 A2) C3 \<and> Bet_Point (Se A2 C3) C2
[PROOF STEP]
by (simp add:Seg_not_Eq_move)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Bet_Point (Se C2 A2) C3 \<and> \<not> Bet_Point (Se A2 C3) C2 \<or> \<not> Bet_Point (Se C2 A2) C3 \<and> Bet_Point (Se A2 C3) C2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
[PROOF STEP]
have P11 : "Def (Tri (Tr B2 A2 C2))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)

goal (1 subgoal):
 1. Def (Tri (Tr B2 A2 C2))
[PROOF STEP]
by (blast intro:Tri_def_rev Tri_def_trans)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr B2 A2 C2))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P6 P11
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<and> \<not> Bet_Point (Se C3 C2) A2 \<and> Line_on (Li A2 C2) C3 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C3) add Emp)
Def (Tri (Tr B2 A2 C2))
[PROOF STEP]
have "Def (Tri (Tr B2 A2 C3))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<and> \<not> Bet_Point (Se C3 C2) A2 \<and> Line_on (Li A2 C2) C3 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C3) add Emp)
Def (Tri (Tr B2 A2 C2))

goal (1 subgoal):
 1. Def (Tri (Tr B2 A2 C3))
[PROOF STEP]
by (simp add:Tri_def_extension)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr B2 A2 C3))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr B2 A2 C3))
[PROOF STEP]
have P12 : "Def (Tri (Tr A2 B2 C3))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr B2 A2 C3))

goal (1 subgoal):
 1. Def (Tri (Tr A2 B2 C3))
[PROOF STEP]
by (blast intro:Tri_def_rev Tri_def_trans)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr A2 B2 C3))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P11
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr B2 A2 C2))
[PROOF STEP]
have P13 : "Def (Ang (An B2 A2 C2))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr B2 A2 C2))

goal (1 subgoal):
 1. Def (Ang (An B2 A2 C2))
[PROOF STEP]
by (simp add:Tri_to_Ang)
[PROOF STATE]
proof (state)
this:
Def (Ang (An B2 A2 C2))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P14 : "Line_on (Li A2 B2) B2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A2 B2) B2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A2 B2) B2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P15 : "\<not> Bet_Point (Se B2 B2) A2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se B2 B2) A2
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se B2 B2) A2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P6
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<and> \<not> Bet_Point (Se C3 C2) A2 \<and> Line_on (Li A2 C2) C3 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C3) add Emp)
[PROOF STEP]
have P16 : "\<not> Bet_Point (Se C2 C3) A2"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<and> \<not> Bet_Point (Se C3 C2) A2 \<and> Line_on (Li A2 C2) C3 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C3) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
[PROOF STEP]
have P17 : "\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P6 P13 P14 P15 P16 P17
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<and> \<not> Bet_Point (Se C3 C2) A2 \<and> Line_on (Li A2 C2) C3 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C3) add Emp)
Def (Ang (An B2 A2 C2))
Line_on (Li A2 B2) B2
\<not> Bet_Point (Se B2 B2) A2
\<not> Bet_Point (Se C2 C3) A2
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B2) add Emp)
[PROOF STEP]
have P18 :
    "Eq (Geos (Ang (An B2 A2 C2)) add Emp) (Geos (Ang (An B2 A2 C3)) add Emp) \<and> Def (Ang (An B2 A2 C3))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<and> \<not> Bet_Point (Se C3 C2) A2 \<and> Line_on (Li A2 C2) C3 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C3) add Emp)
Def (Ang (An B2 A2 C2))
Line_on (Li A2 B2) B2
\<not> Bet_Point (Se B2 B2) A2
\<not> Bet_Point (Se C2 C3) A2
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B2) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Ang (An B2 A2 C2)) add Emp) (Geos (Ang (An B2 A2 C3)) add Emp) \<and> Def (Ang (An B2 A2 C3))
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An B2 A2 C2)) add Emp) (Geos (Ang (An B2 A2 C3)) add Emp) \<and> Def (Ang (An B2 A2 C3))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms P18
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
Eq (Geos (Ang (An B2 A2 C2)) add Emp) (Geos (Ang (An B2 A2 C3)) add Emp) \<and> Def (Ang (An B2 A2 C3))
[PROOF STEP]
have P19 : "Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C3)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
Eq (Geos (Ang (An B2 A2 C2)) add Emp) (Geos (Ang (An B2 A2 C3)) add Emp) \<and> Def (Ang (An B2 A2 C3))

goal (1 subgoal):
 1. Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C3)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C3)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms P6 P12 P19
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<and> \<not> Bet_Point (Se C3 C2) A2 \<and> Line_on (Li A2 C2) C3 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C3) add Emp)
Def (Tri (Tr A2 B2 C3))
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C3)) add Emp)
[PROOF STEP]
have "Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C3)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<and> \<not> Bet_Point (Se C3 C2) A2 \<and> Line_on (Li A2 C2) C3 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C3) add Emp)
Def (Tri (Tr A2 B2 C3))
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C3)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C3)) add Emp)
[PROOF STEP]
by (simp add:Tri_SAS)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C3)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C3)) add Emp)
[PROOF STEP]
have P20 : "Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C3)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp)
[PROOF STEP]
by (simp add:Tri_Cong_def)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
[PROOF STEP]
have P21 : "Def (Ang (An A1 C1 B1))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)

goal (1 subgoal):
 1. Def (Ang (An A1 C1 B1))
[PROOF STEP]
by (blast intro:Tri_to_Ang Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An A1 C1 B1))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
[PROOF STEP]
have P22 : "Def (Ang (An A2 C2 B2))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)

goal (1 subgoal):
 1. Def (Ang (An A2 C2 B2))
[PROOF STEP]
by (blast intro:Tri_to_Ang Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An A2 C2 B2))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P18
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An B2 A2 C2)) add Emp) (Geos (Ang (An B2 A2 C3)) add Emp) \<and> Def (Ang (An B2 A2 C3))
[PROOF STEP]
have P23 : "Def (Ang (An A2 C3 B2))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An B2 A2 C2)) add Emp) (Geos (Ang (An B2 A2 C3)) add Emp) \<and> Def (Ang (An B2 A2 C3))

goal (1 subgoal):
 1. Def (Ang (An A2 C3 B2))
[PROOF STEP]
by (blast intro:Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An A2 C3 B2))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms P20 P21 P22 P23
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp)
Def (Ang (An A1 C1 B1))
Def (Ang (An A2 C2 B2))
Def (Ang (An A2 C3 B2))
[PROOF STEP]
have P24 : "Cong (Geos (Ang (An A2 C2 B2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp)
Def (Ang (An A1 C1 B1))
Def (Ang (An A2 C2 B2))
Def (Ang (An A2 C3 B2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An A2 C2 B2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp)
[PROOF STEP]
by (blast intro:Ang_trans Ang_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An A2 C2 B2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P22 P23 P24
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A2 C2 B2))
Def (Ang (An A2 C3 B2))
Cong (Geos (Ang (An A2 C2 B2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp)
[PROOF STEP]
have P25 : "\<not> Gr (Geos (Ang (An A2 C2 B2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp)
    \<and> \<not> Gr (Geos (Ang (An A2 C3 B2)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A2 C2 B2))
Def (Ang (An A2 C3 B2))
Cong (Geos (Ang (An A2 C2 B2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp)

goal (1 subgoal):
 1. \<not> Gr (Geos (Ang (An A2 C2 B2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp) \<and> \<not> Gr (Geos (Ang (An A2 C3 B2)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
[PROOF STEP]
by (simp add:Ang_not_Gr)
[PROOF STATE]
proof (state)
this:
\<not> Gr (Geos (Ang (An A2 C2 B2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp) \<and> \<not> Gr (Geos (Ang (An A2 C3 B2)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
[PROOF STEP]
have P26 : "Def (Tri (Tr B2 C2 A2))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)

goal (1 subgoal):
 1. Def (Tri (Tr B2 C2 A2))
[PROOF STEP]
by (blast intro:Tri_def_trans)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr B2 C2 A2))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P27 : "Bet_Point (Se C2 A2) C3 \<Longrightarrow> \<not> Eq (Geos (Poi C3) add Emp) (Geos (Poi C2) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bet_Point (Se C2 A2) C3 \<Longrightarrow> \<not> Eq (Geos (Poi C3) add Emp) (Geos (Poi C2) add Emp)
[PROOF STEP]
by (simp add:Bet_Point_def)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se C2 A2) C3 \<Longrightarrow> \<not> Eq (Geos (Poi C3) add Emp) (Geos (Poi C2) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P28 : "Bet_Point (Se A2 C3) C2 \<Longrightarrow> \<not> Eq (Geos (Poi C3) add Emp) (Geos (Poi C2) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bet_Point (Se A2 C3) C2 \<Longrightarrow> \<not> Eq (Geos (Poi C3) add Emp) (Geos (Poi C2) add Emp)
[PROOF STEP]
by (simp add:Bet_Point_def)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A2 C3) C2 \<Longrightarrow> \<not> Eq (Geos (Poi C3) add Emp) (Geos (Poi C2) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P10 P27 P28
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Bet_Point (Se C2 A2) C3 \<and> \<not> Bet_Point (Se A2 C3) C2 \<or> \<not> Bet_Point (Se C2 A2) C3 \<and> Bet_Point (Se A2 C3) C2
Bet_Point (Se C2 A2) C3 \<Longrightarrow> \<not> Eq (Geos (Poi C3) add Emp) (Geos (Poi C2) add Emp)
Bet_Point (Se A2 C3) C2 \<Longrightarrow> \<not> Eq (Geos (Poi C3) add Emp) (Geos (Poi C2) add Emp)
[PROOF STEP]
have P29 : "\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow>
    \<not> Eq (Geos (Poi C2) add Emp) (Geos (Poi C3) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Bet_Point (Se C2 A2) C3 \<and> \<not> Bet_Point (Se A2 C3) C2 \<or> \<not> Bet_Point (Se C2 A2) C3 \<and> Bet_Point (Se A2 C3) C2
Bet_Point (Se C2 A2) C3 \<Longrightarrow> \<not> Eq (Geos (Poi C3) add Emp) (Geos (Poi C2) add Emp)
Bet_Point (Se A2 C3) C2 \<Longrightarrow> \<not> Eq (Geos (Poi C3) add Emp) (Geos (Poi C2) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> \<not> Eq (Geos (Poi C2) add Emp) (Geos (Poi C3) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> \<not> Eq (Geos (Poi C2) add Emp) (Geos (Poi C3) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P5 P6
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<and> \<not> Bet_Point (Se C3 C2) A2 \<and> Line_on (Li A2 C2) C3 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C3) add Emp)
[PROOF STEP]
have P30 : "Line_on (Li C2 A2) C3"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<and> \<not> Bet_Point (Se C3 C2) A2 \<and> Line_on (Li A2 C2) C3 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C3) add Emp)

goal (1 subgoal):
 1. Line_on (Li C2 A2) C3
[PROOF STEP]
by (blast intro:Line_rev Line_on_trans)
[PROOF STATE]
proof (state)
this:
Line_on (Li C2 A2) C3

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P26 P29 P30
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr B2 C2 A2))
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> \<not> Eq (Geos (Poi C2) add Emp) (Geos (Poi C3) add Emp)
Line_on (Li C2 A2) C3
[PROOF STEP]
have "\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow>
    Def (Tri (Tr B2 C2 C3))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr B2 C2 A2))
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> \<not> Eq (Geos (Poi C2) add Emp) (Geos (Poi C3) add Emp)
Line_on (Li C2 A2) C3

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Tri (Tr B2 C2 C3))
[PROOF STEP]
by (simp add:Tri_def_extension)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Tri (Tr B2 C2 C3))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Tri (Tr B2 C2 C3))
[PROOF STEP]
have P31 : "\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow>
    Def (Tri (Tr C3 C2 B2))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Tri (Tr B2 C2 C3))

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Tri (Tr C3 C2 B2))
[PROOF STEP]
by (blast intro:Tri_def_rev Tri_def_trans)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Tri (Tr C3 C2 B2))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Tri (Tr C3 C2 B2))
[PROOF STEP]
have P32 : "\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow>
    Bet_Point (Se C2 A2) C3 \<Longrightarrow> Gr (Geos (Ang (An B2 C3 A2)) add Emp) (Geos (Ang (An C3 C2 B2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Tri (Tr C3 C2 B2))

goal (1 subgoal):
 1. \<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se C2 A2) C3\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An B2 C3 A2)) add Emp) (Geos (Ang (An C3 C2 B2)) add Emp)
[PROOF STEP]
by (simp add:Ang_external_Gr)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se C2 A2) C3\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An B2 C3 A2)) add Emp) (Geos (Ang (An C3 C2 B2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P33 : "Cong (Geos (Ang (An B2 C3 A2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An B2 C3 A2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An B2 C3 A2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P31
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Tri (Tr C3 C2 B2))
[PROOF STEP]
have P34 : "\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow>
    Def (Ang (An C3 C2 B2))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Tri (Tr C3 C2 B2))

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Ang (An C3 C2 B2))
[PROOF STEP]
by (simp add:Tri_to_Ang)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Ang (An C3 C2 B2))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P23
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A2 C3 B2))
[PROOF STEP]
have P35 : "Def (Ang (An B2 C3 A2))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A2 C3 B2))

goal (1 subgoal):
 1. Def (Ang (An B2 C3 A2))
[PROOF STEP]
by (blast intro:Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An B2 C3 A2))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P23 P32 P33 P34 P35
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A2 C3 B2))
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se C2 A2) C3\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An B2 C3 A2)) add Emp) (Geos (Ang (An C3 C2 B2)) add Emp)
Cong (Geos (Ang (An B2 C3 A2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp)
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Ang (An C3 C2 B2))
Def (Ang (An B2 C3 A2))
[PROOF STEP]
have P36 : "\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow>
    Bet_Point (Se C2 A2) C3 \<Longrightarrow> Gr (Geos (Ang (An A2 C3 B2)) add Emp) (Geos (Ang (An C3 C2 B2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A2 C3 B2))
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se C2 A2) C3\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An B2 C3 A2)) add Emp) (Geos (Ang (An C3 C2 B2)) add Emp)
Cong (Geos (Ang (An B2 C3 A2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp)
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Ang (An C3 C2 B2))
Def (Ang (An B2 C3 A2))

goal (1 subgoal):
 1. \<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se C2 A2) C3\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An A2 C3 B2)) add Emp) (Geos (Ang (An C3 C2 B2)) add Emp)
[PROOF STEP]
by (blast intro:Ang_Gr_trans_Eq_Gr Ang_rev)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se C2 A2) C3\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An A2 C3 B2)) add Emp) (Geos (Ang (An C3 C2 B2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P37 : "Bet_Point (Se C2 A2) C3 \<Longrightarrow> Line_on (Li C2 C3) A2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bet_Point (Se C2 A2) C3 \<Longrightarrow> Line_on (Li C2 C3) A2
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se C2 A2) C3 \<Longrightarrow> Line_on (Li C2 C3) A2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P10
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Bet_Point (Se C2 A2) C3 \<and> \<not> Bet_Point (Se A2 C3) C2 \<or> \<not> Bet_Point (Se C2 A2) C3 \<and> Bet_Point (Se A2 C3) C2
[PROOF STEP]
have P38 : "\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow>
    Bet_Point (Se C2 A2) C3 \<Longrightarrow> \<not> Bet_Point (Se C3 A2) C2"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Bet_Point (Se C2 A2) C3 \<and> \<not> Bet_Point (Se A2 C3) C2 \<or> \<not> Bet_Point (Se C2 A2) C3 \<and> Bet_Point (Se A2 C3) C2

goal (1 subgoal):
 1. \<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se C2 A2) C3\<rbrakk> \<Longrightarrow> \<not> Bet_Point (Se C3 A2) C2
[PROOF STEP]
by (blast intro:Bet_rev)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se C2 A2) C3\<rbrakk> \<Longrightarrow> \<not> Bet_Point (Se C3 A2) C2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P39 : "Line_on (Li C2 B2) B2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li C2 B2) B2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li C2 B2) B2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P40 : "\<not> Bet_Point (Se B2 B2) C2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se B2 B2) C2
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se B2 B2) C2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P13
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An B2 A2 C2))
[PROOF STEP]
have P41 : "\<not> Eq (Geos (Poi C2) add Emp) (Geos (Poi B2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An B2 A2 C2))

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P4 P34 P37 P38 P39 P40 P41
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi C2) add Emp) (Geos (Poi A2) add Emp)
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Ang (An C3 C2 B2))
Bet_Point (Se C2 A2) C3 \<Longrightarrow> Line_on (Li C2 C3) A2
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se C2 A2) C3\<rbrakk> \<Longrightarrow> \<not> Bet_Point (Se C3 A2) C2
Line_on (Li C2 B2) B2
\<not> Bet_Point (Se B2 B2) C2
\<not> Eq (Geos (Poi C2) add Emp) (Geos (Poi B2) add Emp)
[PROOF STEP]
have "\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow>
    Bet_Point (Se C2 A2) C3 \<Longrightarrow> Eq (Geos (Ang (An C3 C2 B2)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
    \<and> Def (Ang (An A2 C2 B2))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi C2) add Emp) (Geos (Poi A2) add Emp)
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Ang (An C3 C2 B2))
Bet_Point (Se C2 A2) C3 \<Longrightarrow> Line_on (Li C2 C3) A2
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se C2 A2) C3\<rbrakk> \<Longrightarrow> \<not> Bet_Point (Se C3 A2) C2
Line_on (Li C2 B2) B2
\<not> Bet_Point (Se B2 B2) C2
\<not> Eq (Geos (Poi C2) add Emp) (Geos (Poi B2) add Emp)

goal (1 subgoal):
 1. \<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se C2 A2) C3\<rbrakk> \<Longrightarrow> Eq (Geos (Ang (An C3 C2 B2)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp) \<and> Def (Ang (An A2 C2 B2))
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se C2 A2) C3\<rbrakk> \<Longrightarrow> Eq (Geos (Ang (An C3 C2 B2)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp) \<and> Def (Ang (An A2 C2 B2))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se C2 A2) C3\<rbrakk> \<Longrightarrow> Eq (Geos (Ang (An C3 C2 B2)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp) \<and> Def (Ang (An A2 C2 B2))
[PROOF STEP]
have P42 : "\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow>
    Bet_Point (Se C2 A2) C3 \<Longrightarrow> Cong (Geos (Ang (An C3 C2 B2)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se C2 A2) C3\<rbrakk> \<Longrightarrow> Eq (Geos (Ang (An C3 C2 B2)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp) \<and> Def (Ang (An A2 C2 B2))

goal (1 subgoal):
 1. \<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se C2 A2) C3\<rbrakk> \<Longrightarrow> Cong (Geos (Ang (An C3 C2 B2)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se C2 A2) C3\<rbrakk> \<Longrightarrow> Cong (Geos (Ang (An C3 C2 B2)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P22 P23 P34 P36 P42
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A2 C2 B2))
Def (Ang (An A2 C3 B2))
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Ang (An C3 C2 B2))
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se C2 A2) C3\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An A2 C3 B2)) add Emp) (Geos (Ang (An C3 C2 B2)) add Emp)
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se C2 A2) C3\<rbrakk> \<Longrightarrow> Cong (Geos (Ang (An C3 C2 B2)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
[PROOF STEP]
have P43 : "\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow>
    Bet_Point (Se C2 A2) C3 \<Longrightarrow> Gr (Geos (Ang (An A2 C3 B2)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A2 C2 B2))
Def (Ang (An A2 C3 B2))
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Ang (An C3 C2 B2))
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se C2 A2) C3\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An A2 C3 B2)) add Emp) (Geos (Ang (An C3 C2 B2)) add Emp)
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se C2 A2) C3\<rbrakk> \<Longrightarrow> Cong (Geos (Ang (An C3 C2 B2)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)

goal (1 subgoal):
 1. \<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se C2 A2) C3\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An A2 C3 B2)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
[PROOF STEP]
by (blast intro:Ang_Gr_trans_Gr_Eq Ang_rev)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se C2 A2) C3\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An A2 C3 B2)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P31
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Tri (Tr C3 C2 B2))
[PROOF STEP]
have "\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow>
    Def (Tri (Tr C2 C3 B2))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Tri (Tr C3 C2 B2))

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Tri (Tr C2 C3 B2))
[PROOF STEP]
by (blast intro:Tri_def_rev Tri_def_trans)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Tri (Tr C2 C3 B2))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Tri (Tr C2 C3 B2))
[PROOF STEP]
have P44 : "\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow>
    Bet_Point (Se A2 C3) C2 \<Longrightarrow> Gr (Geos (Ang (An B2 C2 A2)) add Emp) (Geos (Ang (An C2 C3 B2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Tri (Tr C2 C3 B2))

goal (1 subgoal):
 1. \<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se A2 C3) C2\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An B2 C2 A2)) add Emp) (Geos (Ang (An C2 C3 B2)) add Emp)
[PROOF STEP]
by (simp add:Ang_external_Gr Bet_rev)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se A2 C3) C2\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An B2 C2 A2)) add Emp) (Geos (Ang (An C2 C3 B2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P45 : "Cong (Geos (Ang (An B2 C2 A2)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An B2 C2 A2)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An B2 C2 A2)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P26
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr B2 C2 A2))
[PROOF STEP]
have P46 : "Def (Ang (An B2 C2 A2))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr B2 C2 A2))

goal (1 subgoal):
 1. Def (Ang (An B2 C2 A2))
[PROOF STEP]
by (simp add:Tri_to_Ang)
[PROOF STATE]
proof (state)
this:
Def (Ang (An B2 C2 A2))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P34
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Ang (An C3 C2 B2))
[PROOF STEP]
have P47 : "\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow>
    Def (Ang (An C2 C3 B2))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Ang (An C3 C2 B2))

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Ang (An C2 C3 B2))
[PROOF STEP]
by (blast intro:Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Ang (An C2 C3 B2))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P22 P44 P45 P46 P47
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A2 C2 B2))
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se A2 C3) C2\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An B2 C2 A2)) add Emp) (Geos (Ang (An C2 C3 B2)) add Emp)
Cong (Geos (Ang (An B2 C2 A2)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Def (Ang (An B2 C2 A2))
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Ang (An C2 C3 B2))
[PROOF STEP]
have P48 : "\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow>
    Bet_Point (Se A2 C3) C2 \<Longrightarrow> Gr (Geos (Ang (An A2 C2 B2)) add Emp) (Geos (Ang (An C2 C3 B2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A2 C2 B2))
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se A2 C3) C2\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An B2 C2 A2)) add Emp) (Geos (Ang (An C2 C3 B2)) add Emp)
Cong (Geos (Ang (An B2 C2 A2)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Def (Ang (An B2 C2 A2))
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Ang (An C2 C3 B2))

goal (1 subgoal):
 1. \<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se A2 C3) C2\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An A2 C2 B2)) add Emp) (Geos (Ang (An C2 C3 B2)) add Emp)
[PROOF STEP]
by (blast intro:Ang_Gr_trans_Eq_Gr Ang_rev)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se A2 C3) C2\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An A2 C2 B2)) add Emp) (Geos (Ang (An C2 C3 B2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P49 : "Bet_Point (Se A2 C3) C2 \<Longrightarrow> Line_on (Li C3 C2) A2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bet_Point (Se A2 C3) C2 \<Longrightarrow> Line_on (Li C3 C2) A2
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A2 C3) C2 \<Longrightarrow> Line_on (Li C3 C2) A2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P10
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Bet_Point (Se C2 A2) C3 \<and> \<not> Bet_Point (Se A2 C3) C2 \<or> \<not> Bet_Point (Se C2 A2) C3 \<and> Bet_Point (Se A2 C3) C2
[PROOF STEP]
have P50 : "\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow>
    Bet_Point (Se A2 C3) C2 \<Longrightarrow> \<not> Bet_Point (Se C2 A2) C3"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Bet_Point (Se C2 A2) C3 \<and> \<not> Bet_Point (Se A2 C3) C2 \<or> \<not> Bet_Point (Se C2 A2) C3 \<and> Bet_Point (Se A2 C3) C2

goal (1 subgoal):
 1. \<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se A2 C3) C2\<rbrakk> \<Longrightarrow> \<not> Bet_Point (Se C2 A2) C3
[PROOF STEP]
by (blast intro:Bet_rev)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se A2 C3) C2\<rbrakk> \<Longrightarrow> \<not> Bet_Point (Se C2 A2) C3

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P51 : "Line_on (Li C3 B2) B2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li C3 B2) B2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li C3 B2) B2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P52 : "\<not> Bet_Point (Se B2 B2) C3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se B2 B2) C3
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se B2 B2) C3

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P6
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<and> \<not> Bet_Point (Se C3 C2) A2 \<and> Line_on (Li A2 C2) C3 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C3) add Emp)
[PROOF STEP]
have P53 : "\<not> Eq (Geos (Poi C3) add Emp) (Geos (Poi A2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<and> \<not> Bet_Point (Se C3 C2) A2 \<and> Line_on (Li A2 C2) C3 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C3) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P47
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Ang (An C2 C3 B2))
[PROOF STEP]
have P54 : "\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow>
    \<not> Eq (Geos (Poi C3) add Emp) (Geos (Poi B2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Ang (An C2 C3 B2))

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> \<not> Eq (Geos (Poi C3) add Emp) (Geos (Poi B2) add Emp)
[PROOF STEP]
by (simp add:Ang_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> \<not> Eq (Geos (Poi C3) add Emp) (Geos (Poi B2) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P47 P49 P50 P51 P52 P53 P54
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Ang (An C2 C3 B2))
Bet_Point (Se A2 C3) C2 \<Longrightarrow> Line_on (Li C3 C2) A2
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se A2 C3) C2\<rbrakk> \<Longrightarrow> \<not> Bet_Point (Se C2 A2) C3
Line_on (Li C3 B2) B2
\<not> Bet_Point (Se B2 B2) C3
\<not> Eq (Geos (Poi C3) add Emp) (Geos (Poi A2) add Emp)
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> \<not> Eq (Geos (Poi C3) add Emp) (Geos (Poi B2) add Emp)
[PROOF STEP]
have "\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow>
    Bet_Point (Se A2 C3) C2 \<Longrightarrow> Eq (Geos (Ang (An C2 C3 B2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp)
    \<and> Def (Ang (An A2 C3 B2))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Ang (An C2 C3 B2))
Bet_Point (Se A2 C3) C2 \<Longrightarrow> Line_on (Li C3 C2) A2
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se A2 C3) C2\<rbrakk> \<Longrightarrow> \<not> Bet_Point (Se C2 A2) C3
Line_on (Li C3 B2) B2
\<not> Bet_Point (Se B2 B2) C3
\<not> Eq (Geos (Poi C3) add Emp) (Geos (Poi A2) add Emp)
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> \<not> Eq (Geos (Poi C3) add Emp) (Geos (Poi B2) add Emp)

goal (1 subgoal):
 1. \<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se A2 C3) C2\<rbrakk> \<Longrightarrow> Eq (Geos (Ang (An C2 C3 B2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp) \<and> Def (Ang (An A2 C3 B2))
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se A2 C3) C2\<rbrakk> \<Longrightarrow> Eq (Geos (Ang (An C2 C3 B2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp) \<and> Def (Ang (An A2 C3 B2))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se A2 C3) C2\<rbrakk> \<Longrightarrow> Eq (Geos (Ang (An C2 C3 B2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp) \<and> Def (Ang (An A2 C3 B2))
[PROOF STEP]
have P55 : "\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow>
    Bet_Point (Se A2 C3) C2 \<Longrightarrow> Cong (Geos (Ang (An C2 C3 B2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se A2 C3) C2\<rbrakk> \<Longrightarrow> Eq (Geos (Ang (An C2 C3 B2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp) \<and> Def (Ang (An A2 C3 B2))

goal (1 subgoal):
 1. \<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se A2 C3) C2\<rbrakk> \<Longrightarrow> Cong (Geos (Ang (An C2 C3 B2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se A2 C3) C2\<rbrakk> \<Longrightarrow> Cong (Geos (Ang (An C2 C3 B2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P22 P23 P47 P48 P55
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A2 C2 B2))
Def (Ang (An A2 C3 B2))
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Ang (An C2 C3 B2))
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se A2 C3) C2\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An A2 C2 B2)) add Emp) (Geos (Ang (An C2 C3 B2)) add Emp)
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se A2 C3) C2\<rbrakk> \<Longrightarrow> Cong (Geos (Ang (An C2 C3 B2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp)
[PROOF STEP]
have P56 : "\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow>
    Bet_Point (Se A2 C3) C2 \<Longrightarrow> Gr (Geos (Ang (An A2 C2 B2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A2 C2 B2))
Def (Ang (An A2 C3 B2))
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Def (Ang (An C2 C3 B2))
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se A2 C3) C2\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An A2 C2 B2)) add Emp) (Geos (Ang (An C2 C3 B2)) add Emp)
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se A2 C3) C2\<rbrakk> \<Longrightarrow> Cong (Geos (Ang (An C2 C3 B2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp)

goal (1 subgoal):
 1. \<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se A2 C3) C2\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An A2 C2 B2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp)
[PROOF STEP]
by (blast intro:Ang_Gr_trans_Gr_Eq Ang_rev)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se A2 C3) C2\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An A2 C2 B2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P10 P25 P43 P56
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Bet_Point (Se C2 A2) C3 \<and> \<not> Bet_Point (Se A2 C3) C2 \<or> \<not> Bet_Point (Se C2 A2) C3 \<and> Bet_Point (Se A2 C3) C2
\<not> Gr (Geos (Ang (An A2 C2 B2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp) \<and> \<not> Gr (Geos (Ang (An A2 C3 B2)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se C2 A2) C3\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An A2 C3 B2)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se A2 C3) C2\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An A2 C2 B2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp)
[PROOF STEP]
have P57 : "Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Bet_Point (Se C2 A2) C3 \<and> \<not> Bet_Point (Se A2 C3) C2 \<or> \<not> Bet_Point (Se C2 A2) C3 \<and> Bet_Point (Se A2 C3) C2
\<not> Gr (Geos (Ang (An A2 C2 B2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp) \<and> \<not> Gr (Geos (Ang (An A2 C3 B2)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se C2 A2) C3\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An A2 C3 B2)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
\<lbrakk>\<not> Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp); Bet_Point (Se A2 C3) C2\<rbrakk> \<Longrightarrow> Gr (Geos (Ang (An A2 C2 B2)) add Emp) (Geos (Ang (An A2 C3 B2)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P8 P57
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp)
[PROOF STEP]
show "Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp) \<Longrightarrow> Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
Eq (Geos (Seg (Se A2 C2)) add Emp) (Geos (Seg (Se A2 C3)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem (in Congruence_Rule) Tri_AAS :
  assumes
    "Def (Tri (Tr A1 B1 C1))" "Def (Tri (Tr A2 B2 C2))"
    "Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)"
    "Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)"
    "Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp)
    \<or> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)"
  shows
    "Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<or> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
[PROOF STEP]
have P1 : "Def (Tri (Tr B1 A1 C1))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<or> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)

goal (1 subgoal):
 1. Def (Tri (Tr B1 A1 C1))
[PROOF STEP]
by (blast intro:Tri_def_rev Tri_def_trans)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr B1 A1 C1))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<or> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
[PROOF STEP]
have P2 : "Def (Tri (Tr B2 A2 C2))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<or> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)

goal (1 subgoal):
 1. Def (Tri (Tr B2 A2 C2))
[PROOF STEP]
by (blast intro:Tri_def_rev Tri_def_trans)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr B2 A2 C2))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P3 : "Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se B1 A1)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se B1 A1)) add Emp)
[PROOF STEP]
by (simp add:Seg_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se B1 A1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P4 : "Eq (Geos (Seg (Se A2 B2)) add Emp) (Geos (Seg (Se B2 A2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Seg (Se A2 B2)) add Emp) (Geos (Seg (Se B2 A2)) add Emp)
[PROOF STEP]
by (simp add:Seg_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se A2 B2)) add Emp) (Geos (Seg (Se B2 A2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms P3 P4
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<or> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se B1 A1)) add Emp)
Eq (Geos (Seg (Se A2 B2)) add Emp) (Geos (Seg (Se B2 A2)) add Emp)
[PROOF STEP]
have P5 : "Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B2 A2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<or> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se B1 A1)) add Emp)
Eq (Geos (Seg (Se A2 B2)) add Emp) (Geos (Seg (Se B2 A2)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B2 A2)) add Emp)
[PROOF STEP]
by (blast intro:Eq_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B2 A2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P6 : "Eq (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An B1 C1 A1)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An B1 C1 A1)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An B1 C1 A1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms P6
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<or> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
Eq (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An B1 C1 A1)) add Emp)
[PROOF STEP]
have P7 : "Cong (Geos (Ang (An B1 C1 A1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<or> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
Eq (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An B1 C1 A1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An B1 C1 A1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An B1 C1 A1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P8 : "Eq (Geos (Ang (An A2 C2 B2)) add Emp) (Geos (Ang (An B2 C2 A2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An A2 C2 B2)) add Emp) (Geos (Ang (An B2 C2 A2)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An A2 C2 B2)) add Emp) (Geos (Ang (An B2 C2 A2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P7 P8
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An B1 C1 A1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Eq (Geos (Ang (An A2 C2 B2)) add Emp) (Geos (Ang (An B2 C2 A2)) add Emp)
[PROOF STEP]
have P9 : "Cong (Geos (Ang (An B1 C1 A1)) add Emp) (Geos (Ang (An B2 C2 A2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An B1 C1 A1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Eq (Geos (Ang (An A2 C2 B2)) add Emp) (Geos (Ang (An B2 C2 A2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An B1 C1 A1)) add Emp) (Geos (Ang (An B2 C2 A2)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An B1 C1 A1)) add Emp) (Geos (Ang (An B2 C2 A2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P1 P2 P5 P9
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr B1 A1 C1))
Def (Tri (Tr B2 A2 C2))
Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B2 A2)) add Emp)
Cong (Geos (Ang (An B1 C1 A1)) add Emp) (Geos (Ang (An B2 C2 A2)) add Emp)
[PROOF STEP]
have "Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<Longrightarrow>
    Cong (Geos (Tri (Tr B1 A1 C1)) add Emp) (Geos (Tri (Tr B2 A2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr B1 A1 C1))
Def (Tri (Tr B2 A2 C2))
Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B2 A2)) add Emp)
Cong (Geos (Ang (An B1 C1 A1)) add Emp) (Geos (Ang (An B2 C2 A2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<Longrightarrow> Cong (Geos (Tri (Tr B1 A1 C1)) add Emp) (Geos (Tri (Tr B2 A2 C2)) add Emp)
[PROOF STEP]
by (simp add:Tri_AAS_lemma1)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<Longrightarrow> Cong (Geos (Tri (Tr B1 A1 C1)) add Emp) (Geos (Tri (Tr B2 A2 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<Longrightarrow> Cong (Geos (Tri (Tr B1 A1 C1)) add Emp) (Geos (Tri (Tr B2 A2 C2)) add Emp)
[PROOF STEP]
have P10 : "Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An C1 A1 B1)) add Emp) (Geos (Ang (An C2 A2 B2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<Longrightarrow> Cong (Geos (Tri (Tr B1 A1 C1)) add Emp) (Geos (Tri (Tr B2 A2 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An C1 A1 B1)) add Emp) (Geos (Ang (An C2 A2 B2)) add Emp)
[PROOF STEP]
by (simp add:Tri_Cong_def)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An C1 A1 B1)) add Emp) (Geos (Ang (An C2 A2 B2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P11 : "Eq (Geos (Ang (An C1 A1 B1)) add Emp) (Geos (Ang (An B1 A1 C1)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An C1 A1 B1)) add Emp) (Geos (Ang (An B1 A1 C1)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An C1 A1 B1)) add Emp) (Geos (Ang (An B1 A1 C1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P10 P11
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An C1 A1 B1)) add Emp) (Geos (Ang (An C2 A2 B2)) add Emp)
Eq (Geos (Ang (An C1 A1 B1)) add Emp) (Geos (Ang (An B1 A1 C1)) add Emp)
[PROOF STEP]
have P12 : "Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An C2 A2 B2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An C1 A1 B1)) add Emp) (Geos (Ang (An C2 A2 B2)) add Emp)
Eq (Geos (Ang (An C1 A1 B1)) add Emp) (Geos (Ang (An B1 A1 C1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An C2 A2 B2)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An C2 A2 B2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P13 : "Eq (Geos (Ang (An C2 A2 B2)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An C2 A2 B2)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An C2 A2 B2)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P12 P13
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An C2 A2 B2)) add Emp)
Eq (Geos (Ang (An C2 A2 B2)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
[PROOF STEP]
have "Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An C2 A2 B2)) add Emp)
Eq (Geos (Ang (An C2 A2 B2)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
[PROOF STEP]
have P14 : "Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp)
    \<or> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<or> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<or> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<or> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
[PROOF STEP]
have P15 : "Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp) \<Longrightarrow>
    Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<or> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp) \<Longrightarrow> Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
by (simp add:Tri_AAS_lemma1)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp) \<Longrightarrow> Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms P14 P15
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<or> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<or> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp) \<Longrightarrow> Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
show "Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Cong (Geos (Ang (An A1 C1 B1)) add Emp) (Geos (Ang (An A2 C2 B2)) add Emp)
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<or> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp) \<or> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp) \<Longrightarrow> Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp) \<Longrightarrow> Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)

goal:
No subgoals!
[PROOF STEP]
qed