[STATEMENT]
lemma (in Congruence_Rule) Tri_week_ASA :
  assumes N :
    "Def (Tri (Tr A B C))"
    "Def (Tri (Tr A1 B1 C1))"
    "Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)"
    "Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C1 A1 B1)) add Emp)"
    "Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) add Emp)"
  shows "\<not>\<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
assume W : "\<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp)"
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P1 : "Line_on (Li B1 C1) B1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B1 C1) B1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B1 C1) B1

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P2 : "Line_on (Li B1 C1) C1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B1 C1) C1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B1 C1) C1

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

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

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

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P1 P2 P3 P4
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B1 C1) B1
Line_on (Li B1 C1) C1
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C1) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
have "\<exists>p. Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp)
    \<and> \<not> Bet_Point (Se p C1) B1 \<and> Line_on (Li B1 C1) p \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi p) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B1 C1) B1
Line_on (Li B1 C1) C1
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C1) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> \<not> Bet_Point (Se p C1) B1 \<and> Line_on (Li B1 C1) p \<and> \<not> Eq (Geos (Poi B1) 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 B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> \<not> Bet_Point (Se p C1) B1 \<and> Line_on (Li B1 C1) p \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi p) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> \<not> Bet_Point (Se p C1) B1 \<and> Line_on (Li B1 C1) p \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
obtain D1 :: Point where P5 : "Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 D1)) add Emp)
    \<and> \<not> Bet_Point (Se D1 C1) B1 \<and> Line_on (Li B1 C1) D1 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> \<not> Bet_Point (Se p C1) B1 \<and> Line_on (Li B1 C1) p \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi p) add Emp)

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from W
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp)
[PROOF STEP]
have P6 : "\<not> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp)

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P5 P6
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 D1)) add Emp) \<and> \<not> Bet_Point (Se D1 C1) B1 \<and> Line_on (Li B1 C1) D1 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D1) add Emp)
\<not> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B C)) add Emp)
[PROOF STEP]
have "\<not> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B1 D1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 D1)) add Emp) \<and> \<not> Bet_Point (Se D1 C1) B1 \<and> Line_on (Li B1 C1) D1 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D1) add Emp)
\<not> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B C)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B1 D1)) add Emp)
[PROOF STEP]
by (simp add:Eq_not_trans)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B1 D1)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B1 D1)) add Emp)
[PROOF STEP]
have P7 : "\<not> Eq (Geos (Poi C1) add Emp) (Geos (Poi D1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B1 D1)) add Emp)

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C1 A1 B1)) add Emp)
Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) add Emp)
[PROOF STEP]
have P8 : "\<not> Line_on (Li B1 C1) A1"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C1 A1 B1)) add Emp)
Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) add Emp)

goal (1 subgoal):
 1. \<not> Line_on (Li B1 C1) A1
[PROOF STEP]
by (simp add:Tri_def_Line)
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li B1 C1) A1

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P5
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 D1)) add Emp) \<and> \<not> Bet_Point (Se D1 C1) B1 \<and> Line_on (Li B1 C1) D1 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D1) add Emp)
[PROOF STEP]
have P9 : "Line_on (Li B1 C1) D1"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 D1)) add Emp) \<and> \<not> Bet_Point (Se D1 C1) B1 \<and> Line_on (Li B1 C1) D1 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D1) add Emp)

goal (1 subgoal):
 1. Line_on (Li B1 C1) D1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Line_on (Li B1 C1) D1

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B1 C1) D1
[PROOF STEP]
have P10 : "Eq (Geos (Poi D1) add Emp) (Geos (Poi A1) add Emp) \<Longrightarrow> Line_on (Li B1 C1) A1"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B1 C1) D1

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P8 P10
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B1 C1) A1
Eq (Geos (Poi D1) add Emp) (Geos (Poi A1) add Emp) \<Longrightarrow> Line_on (Li B1 C1) A1
[PROOF STEP]
have P11 : "\<not> Eq (Geos (Poi D1) add Emp) (Geos (Poi A1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B1 C1) A1
Eq (Geos (Poi D1) add Emp) (Geos (Poi A1) add Emp) \<Longrightarrow> Line_on (Li B1 C1) A1

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

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

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P13 : "Line_on (Li A1 B1) B1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A1 B1) B1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A1 B1) B1

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P5
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 D1)) add Emp) \<and> \<not> Bet_Point (Se D1 C1) B1 \<and> Line_on (Li B1 C1) D1 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D1) add Emp)
[PROOF STEP]
have P14 : "\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 D1)) add Emp) \<and> \<not> Bet_Point (Se D1 C1) B1 \<and> Line_on (Li B1 C1) D1 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D1) add Emp)

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from assms P7 P9 P14
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C1 A1 B1)) add Emp)
Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) add Emp)
\<not> Eq (Geos (Poi C1) add Emp) (Geos (Poi D1) add Emp)
Line_on (Li B1 C1) D1
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D1) add Emp)
[PROOF STEP]
have "Def (Tri (Tr A1 B1 D1))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C1 A1 B1)) add Emp)
Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) add Emp)
\<not> Eq (Geos (Poi C1) add Emp) (Geos (Poi D1) add Emp)
Line_on (Li B1 C1) D1
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D1) add Emp)

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 D1))
[PROOF STEP]
have "Def (Tri (Tr D1 B1 A1))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 D1))

goal (1 subgoal):
 1. Def (Tri (Tr D1 B1 A1))
[PROOF STEP]
by (simp add:Tri_def_rev)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr D1 B1 A1))

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr D1 B1 A1))
[PROOF STEP]
have P15 : "Def (Tri (Tr B1 A1 D1))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr D1 B1 A1))

goal (1 subgoal):
 1. Def (Tri (Tr B1 A1 D1))
[PROOF STEP]
by (simp add:Tri_def_trans)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr B1 A1 D1))

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

goal (1 subgoal):
 1. Def (Tri (Tr B A C))
[PROOF STEP]
by (blast intro:Tri_def_rev Tri_def_trans)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr B A C))

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

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P5
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 D1)) add Emp) \<and> \<not> Bet_Point (Se D1 C1) B1 \<and> Line_on (Li B1 C1) D1 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D1) add Emp)
[PROOF STEP]
have P18 : "Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 D1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 D1)) add Emp) \<and> \<not> Bet_Point (Se D1 C1) B1 \<and> Line_on (Li B1 C1) D1 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D1) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 D1)) add Emp)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 D1)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P19 : "Line_on (Li B1 A1) A1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B1 A1) A1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B1 A1) A1

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

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr C1 B1 A1))
[PROOF STEP]
have P20 : "Def (Ang (An C1 B1 A1))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr C1 B1 A1))

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P21 : "Line_on (Li B1 A1) A1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B1 A1) A1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B1 A1) A1

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P22 : "\<not> Bet_Point (Se A1 A1) B1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se A1 A1) B1
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se A1 A1) B1

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P5
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 D1)) add Emp) \<and> \<not> Bet_Point (Se D1 C1) B1 \<and> Line_on (Li B1 C1) D1 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D1) add Emp)
[PROOF STEP]
have P23 : "\<not> Bet_Point (Se C1 D1) B1"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 D1)) add Emp) \<and> \<not> Bet_Point (Se D1 C1) B1 \<and> Line_on (Li B1 C1) D1 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D1) add Emp)

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P12
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)
[PROOF STEP]
have P24 : "\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P9 P14 P19 P20 P21 P22 P23 P24
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B1 C1) D1
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D1) add Emp)
Line_on (Li B1 A1) A1
Def (Ang (An C1 B1 A1))
Line_on (Li B1 A1) A1
\<not> Bet_Point (Se A1 A1) B1
\<not> Bet_Point (Se C1 D1) B1
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A1) add Emp)
[PROOF STEP]
have P25 : "Eq (Geos (Ang (An C1 B1 A1)) add Emp) (Geos (Ang (An D1 B1 A1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B1 C1) D1
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D1) add Emp)
Line_on (Li B1 A1) A1
Def (Ang (An C1 B1 A1))
Line_on (Li B1 A1) A1
\<not> Bet_Point (Se A1 A1) B1
\<not> Bet_Point (Se C1 D1) B1
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A1) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Ang (An C1 B1 A1)) add Emp) (Geos (Ang (An D1 B1 A1)) add Emp)
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An C1 B1 A1)) add Emp) (Geos (Ang (An D1 B1 A1)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from assms P25
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C1 A1 B1)) add Emp)
Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) add Emp)
Eq (Geos (Ang (An C1 B1 A1)) add Emp) (Geos (Ang (An D1 B1 A1)) add Emp)
[PROOF STEP]
have P26 : "Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An D1 B1 A1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C1 A1 B1)) add Emp)
Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) add Emp)
Eq (Geos (Ang (An C1 B1 A1)) add Emp) (Geos (Ang (An D1 B1 A1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An D1 B1 A1)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An D1 B1 A1)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P27 : "Eq (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An A B C)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An A B C)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P26 P27
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An D1 B1 A1)) add Emp)
Eq (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
have P28 : "Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An D1 B1 A1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An D1 B1 A1)) add Emp)
Eq (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An A B C)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An D1 B1 A1)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Eq_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An D1 B1 A1)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P29 : "Eq (Geos (Ang (An D1 B1 A1)) add Emp) (Geos (Ang (An A1 B1 D1)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An D1 B1 A1)) add Emp) (Geos (Ang (An A1 B1 D1)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An D1 B1 A1)) add Emp) (Geos (Ang (An A1 B1 D1)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P28 P29
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An D1 B1 A1)) add Emp)
Eq (Geos (Ang (An D1 B1 A1)) add Emp) (Geos (Ang (An A1 B1 D1)) add Emp)
[PROOF STEP]
have P30 : "Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 D1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An D1 B1 A1)) add Emp)
Eq (Geos (Ang (An D1 B1 A1)) add Emp) (Geos (Ang (An A1 B1 D1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 D1)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Eq_rev Ang_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 D1)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P15 P16 P17 P18 P30
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr B1 A1 D1))
Def (Tri (Tr B A C))
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A1)) add Emp)
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 D1)) add Emp)
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 D1)) add Emp)
[PROOF STEP]
have P31 : "Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D1 A1 B1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr B1 A1 D1))
Def (Tri (Tr B A C))
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A1)) add Emp)
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 D1)) add Emp)
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 D1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D1 A1 B1)) add Emp)
[PROOF STEP]
by (simp add:Tri_week_SAS)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D1 A1 B1)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P1 P2 P3 P5 P8 P23
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B1 C1) B1
Line_on (Li B1 C1) C1
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C1) add Emp)
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 D1)) add Emp) \<and> \<not> Bet_Point (Se D1 C1) B1 \<and> Line_on (Li B1 C1) D1 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D1) add Emp)
\<not> Line_on (Li B1 C1) A1
\<not> Bet_Point (Se C1 D1) B1
[PROOF STEP]
have P32 : "Plane_sameside (Li A1 B1) C1 D1 \<or> Eq (Geos (Poi C1) add Emp) (Geos (Poi D1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B1 C1) B1
Line_on (Li B1 C1) C1
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C1) add Emp)
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 D1)) add Emp) \<and> \<not> Bet_Point (Se D1 C1) B1 \<and> Line_on (Li B1 C1) D1 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D1) add Emp)
\<not> Line_on (Li B1 C1) A1
\<not> Bet_Point (Se C1 D1) B1

goal (1 subgoal):
 1. Plane_sameside (Li A1 B1) C1 D1 \<or> Eq (Geos (Poi C1) add Emp) (Geos (Poi D1) add Emp)
[PROOF STEP]
by (simp add:Seg_Plane_sameside)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li A1 B1) C1 D1 \<or> Eq (Geos (Poi C1) add Emp) (Geos (Poi D1) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from assms P31
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C1 A1 B1)) add Emp)
Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) add Emp)
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D1 A1 B1)) add Emp)
[PROOF STEP]
have P33 : "Plane_sameside (Li A1 B1) C1 D1 \<Longrightarrow> Eq (Geos (Lin (Li C1 A1)) add Emp) (Geos (Lin (Li D1 A1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C1 A1 B1)) add Emp)
Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) add Emp)
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D1 A1 B1)) add Emp)

goal (1 subgoal):
 1. Plane_sameside (Li A1 B1) C1 D1 \<Longrightarrow> Eq (Geos (Lin (Li C1 A1)) add Emp) (Geos (Lin (Li D1 A1)) add Emp)
[PROOF STEP]
by (simp add:Ang_move_unique)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li A1 B1) C1 D1 \<Longrightarrow> Eq (Geos (Lin (Li C1 A1)) add Emp) (Geos (Lin (Li D1 A1)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C1 A1 B1)) add Emp)
Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) 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 A B C))
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C1 A1 B1)) add Emp)
Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) 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. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi C1) add Emp) (Geos (Poi A1) add Emp)
[PROOF STEP]
have P34 : "Eq (Geos (Lin (Li C1 A1)) add Emp) (Geos (Lin (Li A1 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. Eq (Geos (Lin (Li C1 A1)) add Emp) (Geos (Lin (Li A1 C1)) add Emp)
[PROOF STEP]
by (simp add:Line_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li C1 A1)) add Emp) (Geos (Lin (Li A1 C1)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P11
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi D1) add Emp) (Geos (Poi A1) add Emp)
[PROOF STEP]
have P35 : "Eq (Geos (Lin (Li D1 A1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi D1) add Emp) (Geos (Poi A1) add Emp)

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P33 P34 P35
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li A1 B1) C1 D1 \<Longrightarrow> Eq (Geos (Lin (Li C1 A1)) add Emp) (Geos (Lin (Li D1 A1)) add Emp)
Eq (Geos (Lin (Li C1 A1)) add Emp) (Geos (Lin (Li A1 C1)) add Emp)
Eq (Geos (Lin (Li D1 A1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)
[PROOF STEP]
have P36 : "Plane_sameside (Li A1 B1) C1 D1 \<Longrightarrow> Eq (Geos (Lin (Li A1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li A1 B1) C1 D1 \<Longrightarrow> Eq (Geos (Lin (Li C1 A1)) add Emp) (Geos (Lin (Li D1 A1)) add Emp)
Eq (Geos (Lin (Li C1 A1)) add Emp) (Geos (Lin (Li A1 C1)) add Emp)
Eq (Geos (Lin (Li D1 A1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)

goal (1 subgoal):
 1. Plane_sameside (Li A1 B1) C1 D1 \<Longrightarrow> Eq (Geos (Lin (Li A1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)
[PROOF STEP]
by (blast intro:Eq_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li A1 B1) C1 D1 \<Longrightarrow> Eq (Geos (Lin (Li A1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P37 : "Line_on (Li A1 C1) C1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A1 C1) C1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A1 C1) C1

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P38 : "Line_on (Li A1 C1) A1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A1 C1) A1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A1 C1) A1

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P39 : "Line_on (Li A1 D1) D1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A1 D1) D1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A1 D1) D1

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P40 : "Line_on (Li A1 D1) A1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A1 D1) A1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A1 D1) A1

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P37
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A1 C1) C1
[PROOF STEP]
have P41 : "Eq (Geos (Poi C1) add Emp) (Geos (Poi D1) add Emp) \<Longrightarrow> Line_on (Li A1 C1) D1"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A1 C1) C1

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P11 P38 P39 P40 P41
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi D1) add Emp) (Geos (Poi A1) add Emp)
Line_on (Li A1 C1) A1
Line_on (Li A1 D1) D1
Line_on (Li A1 D1) A1
Eq (Geos (Poi C1) add Emp) (Geos (Poi D1) add Emp) \<Longrightarrow> Line_on (Li A1 C1) D1
[PROOF STEP]
have P42 : "Eq (Geos (Poi C1) add Emp) (Geos (Poi D1) add Emp) \<Longrightarrow>
    Eq (Geos (Lin (Li A1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi D1) add Emp) (Geos (Poi A1) add Emp)
Line_on (Li A1 C1) A1
Line_on (Li A1 D1) D1
Line_on (Li A1 D1) A1
Eq (Geos (Poi C1) add Emp) (Geos (Poi D1) add Emp) \<Longrightarrow> Line_on (Li A1 C1) D1

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P32 P36 P42
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li A1 B1) C1 D1 \<or> Eq (Geos (Poi C1) add Emp) (Geos (Poi D1) add Emp)
Plane_sameside (Li A1 B1) C1 D1 \<Longrightarrow> Eq (Geos (Lin (Li A1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)
Eq (Geos (Poi C1) add Emp) (Geos (Poi D1) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li A1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)
[PROOF STEP]
have P43 : "Eq (Geos (Lin (Li A1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li A1 B1) C1 D1 \<or> Eq (Geos (Poi C1) add Emp) (Geos (Poi D1) add Emp)
Plane_sameside (Li A1 B1) C1 D1 \<Longrightarrow> Eq (Geos (Lin (Li A1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)
Eq (Geos (Poi C1) add Emp) (Geos (Poi D1) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li A1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Lin (Li A1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li A1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P2 P7 P9 P37
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B1 C1) C1
\<not> Eq (Geos (Poi C1) add Emp) (Geos (Poi D1) add Emp)
Line_on (Li B1 C1) D1
Line_on (Li A1 C1) C1
[PROOF STEP]
have P44 : "Line_on (Li A1 C1) D1 \<Longrightarrow> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li A1 C1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B1 C1) C1
\<not> Eq (Geos (Poi C1) add Emp) (Geos (Poi D1) add Emp)
Line_on (Li B1 C1) D1
Line_on (Li A1 C1) C1

goal (1 subgoal):
 1. Line_on (Li A1 C1) D1 \<Longrightarrow> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li A1 C1)) add Emp)
[PROOF STEP]
by (simp add:Line_unique)
[PROOF STATE]
proof (state)
this:
Line_on (Li A1 C1) D1 \<Longrightarrow> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li A1 C1)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P1 P44
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B1 C1) B1
Line_on (Li A1 C1) D1 \<Longrightarrow> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li A1 C1)) add Emp)
[PROOF STEP]
have P45 : "Line_on (Li A1 C1) D1 \<Longrightarrow> Line_on (Li A1 C1) B1"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B1 C1) B1
Line_on (Li A1 C1) D1 \<Longrightarrow> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li A1 C1)) add Emp)

goal (1 subgoal):
 1. Line_on (Li A1 C1) D1 \<Longrightarrow> Line_on (Li A1 C1) B1
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Line_on (Li A1 C1) D1 \<Longrightarrow> Line_on (Li A1 C1) B1

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

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr C1 B1 A1))
[PROOF STEP]
have P46 : "\<not> Line_on (Li A1 C1) B1"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr C1 B1 A1))

goal (1 subgoal):
 1. \<not> Line_on (Li A1 C1) B1
[PROOF STEP]
by (simp add:Tri_def_Line)
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li A1 C1) B1

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P45 P46
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A1 C1) D1 \<Longrightarrow> Line_on (Li A1 C1) B1
\<not> Line_on (Li A1 C1) B1
[PROOF STEP]
have P47 : "\<not> Line_on (Li A1 C1) D1"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A1 C1) D1 \<Longrightarrow> Line_on (Li A1 C1) B1
\<not> Line_on (Li A1 C1) B1

goal (1 subgoal):
 1. \<not> Line_on (Li A1 C1) D1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li A1 C1) D1

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P48 : "Line_on (Li A1 D1) D1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A1 D1) D1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A1 D1) D1

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P47 P48
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li A1 C1) D1
Line_on (Li A1 D1) D1
[PROOF STEP]
have P49 : "\<not> Eq (Geos (Lin (Li A1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li A1 C1) D1
Line_on (Li A1 D1) D1

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

goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from P43 P49
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li A1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)
\<not> Eq (Geos (Lin (Li A1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li A1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)
\<not> Eq (Geos (Lin (Li A1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem (in Congruence_Rule) Tri_SAS:
  assumes
    "Def (Tri (Tr A B C))"
    "Def (Tri (Tr A1 B1 C1))"
    "Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)"
    "Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se A1 C1)) add Emp)"
    "Cong (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An B1 A1 C1)) add Emp)"
  shows "Cong (Geos (Tri (Tr A B C)) add Emp) (Geos (Tri (Tr A1 B1 C1)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A B C)) add Emp) (Geos (Tri (Tr A1 B1 C1)) add Emp)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A B C)) add Emp) (Geos (Tri (Tr A1 B1 C1)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se A1 C1)) add Emp)
Cong (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An B1 A1 C1)) add Emp)
[PROOF STEP]
have P1 : "Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se A1 C1)) add Emp)
Cong (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An B1 A1 C1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) add Emp)
[PROOF STEP]
by (simp add:Tri_week_SAS)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A B C)) add Emp) (Geos (Tri (Tr A1 B1 C1)) add Emp)
[PROOF STEP]
have P3 : "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 A B C)) add Emp) (Geos (Tri (Tr A1 B1 C1)) add Emp)
[PROOF STEP]
from assms P2
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se A1 C1)) add Emp)
Cong (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An B1 A1 C1)) add Emp)
Eq (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An C A B)) add Emp)
[PROOF STEP]
have P4 : "Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An B1 A1 C1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se A1 C1)) add Emp)
Cong (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An B1 A1 C1)) add Emp)
Eq (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An C A B)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A B C)) add Emp) (Geos (Tri (Tr A1 B1 C1)) add Emp)
[PROOF STEP]
from P3 P4
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An C1 A1 B1)) add Emp) (Geos (Ang (An B1 A1 C1)) add Emp)
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An B1 A1 C1)) add Emp)
[PROOF STEP]
have P5 : "Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C1 A1 B1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An C1 A1 B1)) add Emp) (Geos (Ang (An B1 A1 C1)) add Emp)
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An B1 A1 C1)) add Emp)

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

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

goal (1 subgoal):
 1. \<not> \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp)
[PROOF STEP]
by (simp add:Tri_week_ASA)
[PROOF STATE]
proof (state)
this:
\<not> \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp)

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

goal (1 subgoal):
 1. Eq (Geos (Seg (Se C A)) add Emp) (Geos (Seg (Se C1 A1)) add Emp)
[PROOF STEP]
by (blast intro:Seg_rev Eq_rev Eq_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se C A)) add Emp) (Geos (Seg (Se C1 A1)) add Emp)

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

goal (1 subgoal):
 1. Def (Tri (Tr A C B))
[PROOF STEP]
by (blast intro:Tri_def_rev Tri_def_trans)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr A C B))

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

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A B C)) add Emp) (Geos (Tri (Tr A1 B1 C1)) add Emp)
[PROOF STEP]
from assms P5 P8 P9
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se A1 C1)) add Emp)
Cong (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An B1 A1 C1)) add Emp)
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C1 A1 B1)) add Emp)
Def (Tri (Tr A C B))
Def (Tri (Tr A1 C1 B1))
[PROOF STEP]
have P10 : "Cong (Geos (Ang (An B C A)) add Emp) (Geos (Ang (An B1 C1 A1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se A1 C1)) add Emp)
Cong (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An B1 A1 C1)) add Emp)
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C1 A1 B1)) add Emp)
Def (Tri (Tr A C B))
Def (Tri (Tr A1 C1 B1))

goal (1 subgoal):
 1. Cong (Geos (Ang (An B C A)) add Emp) (Geos (Ang (An B1 C1 A1)) add Emp)
[PROOF STEP]
by (simp add:Tri_week_SAS)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An B C A)) add Emp) (Geos (Ang (An B1 C1 A1)) add Emp)

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

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A B C)) add Emp) (Geos (Tri (Tr A1 B1 C1)) add Emp)
[PROOF STEP]
from P10 P11
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An B C A)) add Emp) (Geos (Ang (An B1 C1 A1)) add Emp)
Eq (Geos (Ang (An B C A)) add Emp) (Geos (Ang (An A C B)) add Emp)
[PROOF STEP]
have P13 : "Cong (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An B1 C1 A1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An B C A)) add Emp) (Geos (Ang (An B1 C1 A1)) add Emp)
Eq (Geos (Ang (An B C A)) add Emp) (Geos (Ang (An A C B)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A B C)) add Emp) (Geos (Tri (Tr A1 B1 C1)) add Emp)
[PROOF STEP]
from P10 P12 P13
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An B C A)) add Emp) (Geos (Ang (An B1 C1 A1)) add Emp)
Eq (Geos (Ang (An B1 C1 A1)) add Emp) (Geos (Ang (An A1 C1 B1)) add Emp)
Cong (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An B1 C1 A1)) add Emp)
[PROOF STEP]
have P14 : "Cong (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An A1 C1 B1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An B C A)) add Emp) (Geos (Ang (An B1 C1 A1)) add Emp)
Eq (Geos (Ang (An B1 C1 A1)) add Emp) (Geos (Ang (An A1 C1 B1)) add Emp)
Cong (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An B1 C1 A1)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A B C)) add Emp) (Geos (Tri (Tr A1 B1 C1)) add Emp)
[PROOF STEP]
from assms P1 P6 P7 P14
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se A1 C1)) add Emp)
Cong (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An B1 A1 C1)) add Emp)
Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) add Emp)
\<not> \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp)
Eq (Geos (Seg (Se C A)) add Emp) (Geos (Seg (Se C1 A1)) add Emp)
Cong (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An A1 C1 B1)) add Emp)
[PROOF STEP]
show "Cong (Geos (Tri (Tr A B C)) add Emp) (Geos (Tri (Tr A1 B1 C1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se A1 C1)) add Emp)
Cong (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An B1 A1 C1)) add Emp)
Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) add Emp)
\<not> \<not> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp)
Eq (Geos (Seg (Se C A)) add Emp) (Geos (Seg (Se C1 A1)) add Emp)
Cong (Geos (Ang (An A C B)) add Emp) (Geos (Ang (An A1 C1 B1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A B C)) add Emp) (Geos (Tri (Tr A1 B1 C1)) add Emp)
[PROOF STEP]
by (simp add:Tri_Cong_def)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Tri (Tr A B C)) add Emp) (Geos (Tri (Tr A1 B1 C1)) add Emp)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem (in Congruence_Rule) Tri_ASA:
  assumes
    "Def (Tri (Tr A B C))"
    "Def (Tri (Tr A1 B1 C1))"
    "Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)"
    "Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) add Emp)"
    "Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C1 A1 B1)) add Emp)"
  shows "Cong (Geos (Tri (Tr A B C)) add Emp) (Geos (Tri (Tr A1 B1 C1)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A B C)) add Emp) (Geos (Tri (Tr A1 B1 C1)) add Emp)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A B C)) add Emp) (Geos (Tri (Tr A1 B1 C1)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)
Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) add Emp)
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C1 A1 B1)) add Emp)
[PROOF STEP]
have P1 : "Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)
Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) add Emp)
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C1 A1 B1)) add Emp)

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

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

goal (1 subgoal):
 1. Def (Tri (Tr B A C))
[PROOF STEP]
by (blast intro:Tri_def_rev Tri_def_trans)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr B A C))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A B C)) add Emp) (Geos (Tri (Tr A1 B1 C1)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)
Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) add Emp)
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C1 A1 B1)) add Emp)
[PROOF STEP]
have P3 : "Def (Tri (Tr B1 A1 C1))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)
Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) add Emp)
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C1 A1 B1)) 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 A B C)) add Emp) (Geos (Tri (Tr A1 B1 C1)) add Emp)
[PROOF STEP]
from assms P1 P2 P3
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)
Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) add Emp)
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C1 A1 B1)) add Emp)
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A1)) add Emp)
Def (Tri (Tr B A C))
Def (Tri (Tr B1 A1 C1))
[PROOF STEP]
have P4 : "\<not>\<not> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se A1 C1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)
Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) add Emp)
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C1 A1 B1)) add Emp)
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A1)) add Emp)
Def (Tri (Tr B A C))
Def (Tri (Tr B1 A1 C1))

goal (1 subgoal):
 1. \<not> \<not> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se A1 C1)) add Emp)
[PROOF STEP]
by (simp add:Tri_week_ASA)
[PROOF STATE]
proof (state)
this:
\<not> \<not> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se A1 C1)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A B C)) add Emp) (Geos (Tri (Tr A1 B1 C1)) add Emp)
[PROOF STEP]
have P6 : "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 A B C)) add Emp) (Geos (Tri (Tr A1 B1 C1)) add Emp)
[PROOF STEP]
from assms P5
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)
Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) add Emp)
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C1 A1 B1)) add Emp)
Eq (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An B A C)) add Emp)
[PROOF STEP]
have P7 : "Cong (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An C1 A1 B1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)
Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) add Emp)
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C1 A1 B1)) add Emp)
Eq (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An B A C)) add Emp)

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

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

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A B C)) add Emp) (Geos (Tri (Tr A1 B1 C1)) add Emp)
[PROOF STEP]
from assms P1 P4 P8
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)
Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) add Emp)
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C1 A1 B1)) add Emp)
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A1)) add Emp)
\<not> \<not> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se A1 C1)) add Emp)
Cong (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An B1 A1 C1)) add Emp)
[PROOF STEP]
show "Cong (Geos (Tri (Tr A B C)) add Emp) (Geos (Tri (Tr A1 B1 C1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)
Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) add Emp)
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C1 A1 B1)) add Emp)
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A1)) add Emp)
\<not> \<not> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se A1 C1)) add Emp)
Cong (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An B1 A1 C1)) add Emp)

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

goal:
No subgoals!
[PROOF STEP]
qed