[STATEMENT]
lemma (in Congruence_Rule) Tri_sinple_def :
  assumes
    "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)"
    "\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)"
    "\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)"
    "\<not> Line_on (Li A B) C"
  shows "Def (Tri (Tr A B C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
have P1 : "Bet_Point (Se A B) C \<Longrightarrow> Line_on (Li A B) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bet_Point (Se A B) C \<Longrightarrow> Line_on (Li A B) C
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A B) C \<Longrightarrow> Line_on (Li A B) C

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from assms P1
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
\<not> Line_on (Li A B) C
Bet_Point (Se A B) C \<Longrightarrow> Line_on (Li A B) C
[PROOF STEP]
have P2 : "\<not> Bet_Point (Se A B) C"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
\<not> Line_on (Li A B) C
Bet_Point (Se A B) C \<Longrightarrow> Line_on (Li A B) C

goal (1 subgoal):
 1. \<not> Bet_Point (Se A B) C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se A B) C

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
\<not> Line_on (Li A B) C
[PROOF STEP]
have P3 : "\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
\<not> Line_on (Li A B) C

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

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from P3
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)
[PROOF STEP]
have P4 : "Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li A B)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)

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

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
have P5 : "Bet_Point (Se B C) A \<Longrightarrow> Line_on (Li A B) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bet_Point (Se B C) A \<Longrightarrow> Line_on (Li A B) C
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se B C) A \<Longrightarrow> Line_on (Li A B) C

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from assms P5
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
\<not> Line_on (Li A B) C
Bet_Point (Se B C) A \<Longrightarrow> Line_on (Li A B) C
[PROOF STEP]
have P6 : "\<not> Bet_Point (Se B C) A"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
\<not> Line_on (Li A B) C
Bet_Point (Se B C) A \<Longrightarrow> Line_on (Li A B) C

goal (1 subgoal):
 1. \<not> Bet_Point (Se B C) A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se B C) A

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
have P7 : "Bet_Point (Se C A) B \<Longrightarrow> Line_on (Li A B) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bet_Point (Se C A) B \<Longrightarrow> Line_on (Li A B) C
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se C A) B \<Longrightarrow> Line_on (Li A B) C

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from assms P7
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
\<not> Line_on (Li A B) C
Bet_Point (Se C A) B \<Longrightarrow> Line_on (Li A B) C
[PROOF STEP]
have P8 : "\<not> Bet_Point (Se C A) B"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
\<not> Line_on (Li A B) C
Bet_Point (Se C A) B \<Longrightarrow> Line_on (Li A B) C

goal (1 subgoal):
 1. \<not> Bet_Point (Se C A) B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se C A) B

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
have "Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> \<exists>p. Bet_Point (Se A B) p \<and> Bet_Point (Se B C) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> \<exists>p. Bet_Point (Se A B) p \<and> Bet_Point (Se B C) p
[PROOF STEP]
by (simp add:Seg_on_Seg_rule)
[PROOF STATE]
proof (state)
this:
Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> \<exists>p. Bet_Point (Se A B) p \<and> Bet_Point (Se B C) p

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> \<exists>p. Bet_Point (Se A B) p \<and> Bet_Point (Se B C) p
[PROOF STEP]
obtain D :: Point where P9 : "Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Bet_Point (Se A B) D \<and> Bet_Point (Se B C) D"
[PROOF STATE]
proof (prove)
using this:
Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> \<exists>p. Bet_Point (Se A B) p \<and> Bet_Point (Se B C) p

goal (1 subgoal):
 1. (\<And>D. (Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Bet_Point (Se A B) D \<and> Bet_Point (Se B C) D) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Bet_Point (Se A B) D \<and> Bet_Point (Se B C) D

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
have P10 : "Line_on (Li A B) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A B) B
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A B) B

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from P9
[PROOF STATE]
proof (chain)
picking this:
Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Bet_Point (Se A B) D \<and> Bet_Point (Se B C) D
[PROOF STEP]
have P11 : "Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Line_on (Li A B) D"
[PROOF STATE]
proof (prove)
using this:
Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Bet_Point (Se A B) D \<and> Bet_Point (Se B C) D

goal (1 subgoal):
 1. Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Line_on (Li A B) D
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Line_on (Li A B) D

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
have P12 : "Line_on (Li B C) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B C) B
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B C) B

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from P9
[PROOF STATE]
proof (chain)
picking this:
Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Bet_Point (Se A B) D \<and> Bet_Point (Se B C) D
[PROOF STEP]
have P13 : "Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Line_on (Li B C) D"
[PROOF STATE]
proof (prove)
using this:
Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Bet_Point (Se A B) D \<and> Bet_Point (Se B C) D

goal (1 subgoal):
 1. Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Line_on (Li B C) D
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Line_on (Li B C) D

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from P9
[PROOF STATE]
proof (chain)
picking this:
Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Bet_Point (Se A B) D \<and> Bet_Point (Se B C) D
[PROOF STEP]
have "Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Bet_Point (Se A B) D"
[PROOF STATE]
proof (prove)
using this:
Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Bet_Point (Se A B) D \<and> Bet_Point (Se B C) D

goal (1 subgoal):
 1. Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Bet_Point (Se A B) D
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Bet_Point (Se A B) D

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Bet_Point (Se A B) D
[PROOF STEP]
have P14 : "Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Bet_Point (Se A B) D

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

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from P10 P11 P12 P13 P14
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A B) B
Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Line_on (Li A B) D
Line_on (Li B C) B
Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Line_on (Li B C) D
Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
[PROOF STEP]
have P15 : "Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li A B)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A B) B
Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Line_on (Li A B) D
Line_on (Li B C) B
Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Line_on (Li B C) D
Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)

goal (1 subgoal):
 1. Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li A B)) add Emp)
[PROOF STEP]
by (simp add:Line_unique)
[PROOF STATE]
proof (state)
this:
Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li A B)) add Emp)

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
have P16 : "Line_on (Li B C) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B C) C
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B C) C

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from P15 P16
[PROOF STATE]
proof (chain)
picking this:
Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li A B)) add Emp)
Line_on (Li B C) C
[PROOF STEP]
have P17 : "Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Line_on (Li A B) C"
[PROOF STATE]
proof (prove)
using this:
Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li A B)) add Emp)
Line_on (Li B C) C

goal (1 subgoal):
 1. Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Line_on (Li A B) C
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Line_on (Li A B) C

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from assms P17
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
\<not> Line_on (Li A B) C
Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Line_on (Li A B) C
[PROOF STEP]
have P18 : "\<not> Seg_on_Seg (Se A B) (Se B C)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
\<not> Line_on (Li A B) C
Seg_on_Seg (Se A B) (Se B C) \<Longrightarrow> Line_on (Li A B) C

goal (1 subgoal):
 1. \<not> Seg_on_Seg (Se A B) (Se B C)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Seg_on_Seg (Se A B) (Se B C)

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
have "Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> \<exists>p. Bet_Point (Se B C) p \<and> Bet_Point (Se C A) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> \<exists>p. Bet_Point (Se B C) p \<and> Bet_Point (Se C A) p
[PROOF STEP]
by (simp add:Seg_on_Seg_rule)
[PROOF STATE]
proof (state)
this:
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> \<exists>p. Bet_Point (Se B C) p \<and> Bet_Point (Se C A) p

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> \<exists>p. Bet_Point (Se B C) p \<and> Bet_Point (Se C A) p
[PROOF STEP]
obtain E :: Point where P19 : "Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Bet_Point (Se B C) E \<and> Bet_Point (Se C A) E"
[PROOF STATE]
proof (prove)
using this:
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> \<exists>p. Bet_Point (Se B C) p \<and> Bet_Point (Se C A) p

goal (1 subgoal):
 1. (\<And>E. (Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Bet_Point (Se B C) E \<and> Bet_Point (Se C A) E) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Bet_Point (Se B C) E \<and> Bet_Point (Se C A) E

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Bet_Point (Se B C) E \<and> Bet_Point (Se C A) E
[PROOF STEP]
have P20 : "Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Line_on (Li B C) E"
[PROOF STATE]
proof (prove)
using this:
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Bet_Point (Se B C) E \<and> Bet_Point (Se C A) E

goal (1 subgoal):
 1. Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Line_on (Li B C) E
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Line_on (Li B C) E

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
have P21 : "Line_on (Li C A) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li C A) C
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li C A) C

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from P19
[PROOF STATE]
proof (chain)
picking this:
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Bet_Point (Se B C) E \<and> Bet_Point (Se C A) E
[PROOF STEP]
have P22 : "Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Line_on (Li C A) E"
[PROOF STATE]
proof (prove)
using this:
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Bet_Point (Se B C) E \<and> Bet_Point (Se C A) E

goal (1 subgoal):
 1. Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Line_on (Li C A) E
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Line_on (Li C A) E

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from P19
[PROOF STATE]
proof (chain)
picking this:
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Bet_Point (Se B C) E \<and> Bet_Point (Se C A) E
[PROOF STEP]
have "Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Bet_Point (Se B C) E"
[PROOF STATE]
proof (prove)
using this:
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Bet_Point (Se B C) E \<and> Bet_Point (Se C A) E

goal (1 subgoal):
 1. Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Bet_Point (Se B C) E
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Bet_Point (Se B C) E

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Bet_Point (Se B C) E
[PROOF STEP]
have P23 : "Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi E) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Bet_Point (Se B C) E

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

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from P16 P20 P21 P22 P23
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B C) C
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Line_on (Li B C) E
Line_on (Li C A) C
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Line_on (Li C A) E
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi E) add Emp)
[PROOF STEP]
have P24 : "Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Eq (Geos (Lin (Li C A)) add Emp) (Geos (Lin (Li B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B C) C
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Line_on (Li B C) E
Line_on (Li C A) C
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Line_on (Li C A) E
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi E) add Emp)

goal (1 subgoal):
 1. Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Eq (Geos (Lin (Li C A)) add Emp) (Geos (Lin (Li B C)) add Emp)
[PROOF STEP]
by (simp add:Line_unique)
[PROOF STATE]
proof (state)
this:
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Eq (Geos (Lin (Li C A)) add Emp) (Geos (Lin (Li B C)) add Emp)

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
have P25 : "Line_on (Li C A) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li C A) A
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li C A) A

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from P24 P25
[PROOF STATE]
proof (chain)
picking this:
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Eq (Geos (Lin (Li C A)) add Emp) (Geos (Lin (Li B C)) add Emp)
Line_on (Li C A) A
[PROOF STEP]
have P26 : "Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Line_on (Li B C) A"
[PROOF STATE]
proof (prove)
using this:
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Eq (Geos (Lin (Li C A)) add Emp) (Geos (Lin (Li B C)) add Emp)
Line_on (Li C A) A

goal (1 subgoal):
 1. Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Line_on (Li B C) A
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Line_on (Li B C) A

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from assms P3 P26
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
\<not> Line_on (Li A B) C
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Line_on (Li B C) A
[PROOF STEP]
have P27 : "Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Line_on (Li B A) C"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
\<not> Line_on (Li A B) C
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Line_on (Li B C) A

goal (1 subgoal):
 1. Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Line_on (Li B A) C
[PROOF STEP]
by (blast intro:Line_on_rev)
[PROOF STATE]
proof (state)
this:
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Line_on (Li B A) C

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from P4 P27
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li A B)) add Emp)
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Line_on (Li B A) C
[PROOF STEP]
have P28 : "Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Line_on (Li A B) C"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li A B)) add Emp)
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Line_on (Li B A) C

goal (1 subgoal):
 1. Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Line_on (Li A B) C
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Line_on (Li A B) C

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from assms P28
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
\<not> Line_on (Li A B) C
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Line_on (Li A B) C
[PROOF STEP]
have P29 : "\<not> Seg_on_Seg (Se B C) (Se C A)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
\<not> Line_on (Li A B) C
Seg_on_Seg (Se B C) (Se C A) \<Longrightarrow> Line_on (Li A B) C

goal (1 subgoal):
 1. \<not> Seg_on_Seg (Se B C) (Se C A)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Seg_on_Seg (Se B C) (Se C A)

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
have "Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> \<exists>p. Bet_Point (Se C A) p \<and> Bet_Point (Se A B) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> \<exists>p. Bet_Point (Se C A) p \<and> Bet_Point (Se A B) p
[PROOF STEP]
by (simp add:Seg_on_Seg_rule)
[PROOF STATE]
proof (state)
this:
Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> \<exists>p. Bet_Point (Se C A) p \<and> Bet_Point (Se A B) p

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> \<exists>p. Bet_Point (Se C A) p \<and> Bet_Point (Se A B) p
[PROOF STEP]
obtain F :: Point where P30 : "Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Bet_Point (Se C A) F \<and> Bet_Point (Se A B) F"
[PROOF STATE]
proof (prove)
using this:
Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> \<exists>p. Bet_Point (Se C A) p \<and> Bet_Point (Se A B) p

goal (1 subgoal):
 1. (\<And>F. (Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Bet_Point (Se C A) F \<and> Bet_Point (Se A B) F) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Bet_Point (Se C A) F \<and> Bet_Point (Se A B) F

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Bet_Point (Se C A) F \<and> Bet_Point (Se A B) F
[PROOF STEP]
have P31 : "Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Line_on (Li C A) F"
[PROOF STATE]
proof (prove)
using this:
Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Bet_Point (Se C A) F \<and> Bet_Point (Se A B) F

goal (1 subgoal):
 1. Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Line_on (Li C A) F
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Line_on (Li C A) F

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
have P32 : "Line_on (Li A B) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A B) A
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A B) A

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from P30
[PROOF STATE]
proof (chain)
picking this:
Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Bet_Point (Se C A) F \<and> Bet_Point (Se A B) F
[PROOF STEP]
have P33 : "Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Line_on (Li A B) F"
[PROOF STATE]
proof (prove)
using this:
Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Bet_Point (Se C A) F \<and> Bet_Point (Se A B) F

goal (1 subgoal):
 1. Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Line_on (Li A B) F
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Line_on (Li A B) F

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from P30
[PROOF STATE]
proof (chain)
picking this:
Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Bet_Point (Se C A) F \<and> Bet_Point (Se A B) F
[PROOF STEP]
have "Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Bet_Point (Se C A) F"
[PROOF STATE]
proof (prove)
using this:
Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Bet_Point (Se C A) F \<and> Bet_Point (Se A B) F

goal (1 subgoal):
 1. Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Bet_Point (Se C A) F
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Bet_Point (Se C A) F

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Bet_Point (Se C A) F
[PROOF STEP]
have P34 : "Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi F) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Bet_Point (Se C A) F

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

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from P25 P31 P32 P33 P34
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li C A) A
Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Line_on (Li C A) F
Line_on (Li A B) A
Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Line_on (Li A B) F
Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi F) add Emp)
[PROOF STEP]
have P35 : "Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Eq (Geos (Lin (Li C A)) add Emp) (Geos (Lin (Li A B)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li C A) A
Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Line_on (Li C A) F
Line_on (Li A B) A
Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Line_on (Li A B) F
Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi F) add Emp)

goal (1 subgoal):
 1. Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Eq (Geos (Lin (Li C A)) add Emp) (Geos (Lin (Li A B)) add Emp)
[PROOF STEP]
by (simp add:Line_unique)
[PROOF STATE]
proof (state)
this:
Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Eq (Geos (Lin (Li C A)) add Emp) (Geos (Lin (Li A B)) add Emp)

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from P21 P35
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li C A) C
Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Eq (Geos (Lin (Li C A)) add Emp) (Geos (Lin (Li A B)) add Emp)
[PROOF STEP]
have P36 : "Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Line_on (Li A B) C"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li C A) C
Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Eq (Geos (Lin (Li C A)) add Emp) (Geos (Lin (Li A B)) add Emp)

goal (1 subgoal):
 1. Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Line_on (Li A B) C
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Line_on (Li A B) C

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from assms P36
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
\<not> Line_on (Li A B) C
Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Line_on (Li A B) C
[PROOF STEP]
have P37 : "\<not> Seg_on_Seg (Se C A) (Se A B)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
\<not> Line_on (Li A B) C
Seg_on_Seg (Se C A) (Se A B) \<Longrightarrow> Line_on (Li A B) C

goal (1 subgoal):
 1. \<not> Seg_on_Seg (Se C A) (Se A B)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Seg_on_Seg (Se C A) (Se A B)

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from assms P2 P6 P8 P18 P29 P37
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
\<not> Line_on (Li A B) C
\<not> Bet_Point (Se A B) C
\<not> Bet_Point (Se B C) A
\<not> Bet_Point (Se C A) B
\<not> Seg_on_Seg (Se A B) (Se B C)
\<not> Seg_on_Seg (Se B C) (Se C A)
\<not> Seg_on_Seg (Se C A) (Se A B)
[PROOF STEP]
show "Def (Tri (Tr A B C))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
\<not> Line_on (Li A B) C
\<not> Bet_Point (Se A B) C
\<not> Bet_Point (Se B C) A
\<not> Bet_Point (Se C A) B
\<not> Seg_on_Seg (Se A B) (Se B C)
\<not> Seg_on_Seg (Se B C) (Se C A)
\<not> Seg_on_Seg (Se C A) (Se A B)

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
by (simp add:Tri_def)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr A B C))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Congruence_Rule) Tri_def_Line :
  assumes
    "Def (Tri (Tr A B C))"
  shows "\<not> Line_on (Li A B) C \<and> \<not> Line_on (Li B C) A \<and> \<not> Line_on (Li C A) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Line_on (Li A B) C \<and> \<not> Line_on (Li B C) A \<and> \<not> Line_on (Li C A) B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Line_on (Li A B) C \<and> \<not> Line_on (Li B C) A \<and> \<not> Line_on (Li C A) B
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
[PROOF STEP]
have P1 : "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
        \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
        \<and> \<not> Bet_Point (Se A B) C \<and> \<not> Bet_Point (Se B C) A \<and> \<not> Bet_Point (Se C A) B"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))

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

goal (1 subgoal):
 1. \<not> Line_on (Li A B) C \<and> \<not> Line_on (Li B C) A \<and> \<not> Line_on (Li C A) B
[PROOF STEP]
have P2 : "Line_on (Li A B) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A B) B
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A B) B

goal (1 subgoal):
 1. \<not> Line_on (Li A B) C \<and> \<not> Line_on (Li B C) A \<and> \<not> Line_on (Li C A) B
[PROOF STEP]
have P3 : "Line_on (Li A B) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A B) A
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A B) A

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

goal (1 subgoal):
 1. Line_on (Li A B) C \<Longrightarrow> Bet_Point (Se A C) B \<or> Bet_Point (Se C B) A \<or> Bet_Point (Se B A) C
[PROOF STEP]
by (simp add:Bet_case)
[PROOF STATE]
proof (state)
this:
Line_on (Li A B) C \<Longrightarrow> Bet_Point (Se A C) B \<or> Bet_Point (Se C B) A \<or> Bet_Point (Se B A) C

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

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

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

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

goal (1 subgoal):
 1. \<not> Line_on (Li A B) C \<and> \<not> Line_on (Li B C) A \<and> \<not> Line_on (Li C A) B
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Bet_Point (Se A B) C \<and> \<not> Bet_Point (Se B C) A \<and> \<not> Bet_Point (Se C A) B
[PROOF STEP]
have P7 : "\<not> Bet_Point (Se B A) C"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Bet_Point (Se A B) C \<and> \<not> Bet_Point (Se B C) A \<and> \<not> Bet_Point (Se C A) B

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

goal (1 subgoal):
 1. \<not> Line_on (Li A B) C \<and> \<not> Line_on (Li B C) A \<and> \<not> Line_on (Li C A) B
[PROOF STEP]
from P4 P5 P6 P7
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A B) C \<Longrightarrow> Bet_Point (Se A C) B \<or> Bet_Point (Se C B) A \<or> Bet_Point (Se B A) C
\<not> Bet_Point (Se A C) B
\<not> Bet_Point (Se C B) A
\<not> Bet_Point (Se B A) C
[PROOF STEP]
have P8 : "\<not> Line_on (Li A B) C"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A B) C \<Longrightarrow> Bet_Point (Se A C) B \<or> Bet_Point (Se C B) A \<or> Bet_Point (Se B A) C
\<not> Bet_Point (Se A C) B
\<not> Bet_Point (Se C B) A
\<not> Bet_Point (Se B A) C

goal (1 subgoal):
 1. \<not> Line_on (Li A B) C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li A B) C

goal (1 subgoal):
 1. \<not> Line_on (Li A B) C \<and> \<not> Line_on (Li B C) A \<and> \<not> Line_on (Li C A) B
[PROOF STEP]
have P9 : "Line_on (Li B C) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B C) B
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B C) B

goal (1 subgoal):
 1. \<not> Line_on (Li A B) C \<and> \<not> Line_on (Li B C) A \<and> \<not> Line_on (Li C A) B
[PROOF STEP]
have P10 : "Line_on (Li B C) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B C) C
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B C) C

goal (1 subgoal):
 1. \<not> Line_on (Li A B) C \<and> \<not> Line_on (Li B C) A \<and> \<not> Line_on (Li C A) B
[PROOF STEP]
from P1 P9 P10
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Bet_Point (Se A B) C \<and> \<not> Bet_Point (Se B C) A \<and> \<not> Bet_Point (Se C A) B
Line_on (Li B C) B
Line_on (Li B C) C
[PROOF STEP]
have P11 : "Line_on (Li B C) A \<Longrightarrow> Bet_Point (Se A C) B \<or> Bet_Point (Se C B) A \<or> Bet_Point (Se B A) C"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Bet_Point (Se A B) C \<and> \<not> Bet_Point (Se B C) A \<and> \<not> Bet_Point (Se C A) B
Line_on (Li B C) B
Line_on (Li B C) C

goal (1 subgoal):
 1. Line_on (Li B C) A \<Longrightarrow> Bet_Point (Se A C) B \<or> Bet_Point (Se C B) A \<or> Bet_Point (Se B A) C
[PROOF STEP]
by (simp add:Bet_case)
[PROOF STATE]
proof (state)
this:
Line_on (Li B C) A \<Longrightarrow> Bet_Point (Se A C) B \<or> Bet_Point (Se C B) A \<or> Bet_Point (Se B A) C

goal (1 subgoal):
 1. \<not> Line_on (Li A B) C \<and> \<not> Line_on (Li B C) A \<and> \<not> Line_on (Li C A) B
[PROOF STEP]
from P5 P6 P7 P11
[PROOF STATE]
proof (chain)
picking this:
\<not> Bet_Point (Se A C) B
\<not> Bet_Point (Se C B) A
\<not> Bet_Point (Se B A) C
Line_on (Li B C) A \<Longrightarrow> Bet_Point (Se A C) B \<or> Bet_Point (Se C B) A \<or> Bet_Point (Se B A) C
[PROOF STEP]
have P12 : "\<not> Line_on (Li B C) A"
[PROOF STATE]
proof (prove)
using this:
\<not> Bet_Point (Se A C) B
\<not> Bet_Point (Se C B) A
\<not> Bet_Point (Se B A) C
Line_on (Li B C) A \<Longrightarrow> Bet_Point (Se A C) B \<or> Bet_Point (Se C B) A \<or> Bet_Point (Se B A) C

goal (1 subgoal):
 1. \<not> Line_on (Li B C) A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li B C) A

goal (1 subgoal):
 1. \<not> Line_on (Li A B) C \<and> \<not> Line_on (Li B C) A \<and> \<not> Line_on (Li C A) B
[PROOF STEP]
have P13 : "Line_on (Li C A) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li C A) C
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li C A) C

goal (1 subgoal):
 1. \<not> Line_on (Li A B) C \<and> \<not> Line_on (Li B C) A \<and> \<not> Line_on (Li C A) B
[PROOF STEP]
have P14 : "Line_on (Li C A) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li C A) A
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li C A) A

goal (1 subgoal):
 1. \<not> Line_on (Li A B) C \<and> \<not> Line_on (Li B C) A \<and> \<not> Line_on (Li C A) B
[PROOF STEP]
from P1 P13 P14
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Bet_Point (Se A B) C \<and> \<not> Bet_Point (Se B C) A \<and> \<not> Bet_Point (Se C A) B
Line_on (Li C A) C
Line_on (Li C A) A
[PROOF STEP]
have P15 : "Line_on (Li C A) B \<Longrightarrow> Bet_Point (Se A C) B \<or> Bet_Point (Se C B) A \<or> Bet_Point (Se B A) C"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Bet_Point (Se A B) C \<and> \<not> Bet_Point (Se B C) A \<and> \<not> Bet_Point (Se C A) B
Line_on (Li C A) C
Line_on (Li C A) A

goal (1 subgoal):
 1. Line_on (Li C A) B \<Longrightarrow> Bet_Point (Se A C) B \<or> Bet_Point (Se C B) A \<or> Bet_Point (Se B A) C
[PROOF STEP]
by (simp add:Bet_case)
[PROOF STATE]
proof (state)
this:
Line_on (Li C A) B \<Longrightarrow> Bet_Point (Se A C) B \<or> Bet_Point (Se C B) A \<or> Bet_Point (Se B A) C

goal (1 subgoal):
 1. \<not> Line_on (Li A B) C \<and> \<not> Line_on (Li B C) A \<and> \<not> Line_on (Li C A) B
[PROOF STEP]
from P5 P6 P7 P15
[PROOF STATE]
proof (chain)
picking this:
\<not> Bet_Point (Se A C) B
\<not> Bet_Point (Se C B) A
\<not> Bet_Point (Se B A) C
Line_on (Li C A) B \<Longrightarrow> Bet_Point (Se A C) B \<or> Bet_Point (Se C B) A \<or> Bet_Point (Se B A) C
[PROOF STEP]
have P16 : "\<not> Line_on (Li C A) B"
[PROOF STATE]
proof (prove)
using this:
\<not> Bet_Point (Se A C) B
\<not> Bet_Point (Se C B) A
\<not> Bet_Point (Se B A) C
Line_on (Li C A) B \<Longrightarrow> Bet_Point (Se A C) B \<or> Bet_Point (Se C B) A \<or> Bet_Point (Se B A) C

goal (1 subgoal):
 1. \<not> Line_on (Li C A) B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li C A) B

goal (1 subgoal):
 1. \<not> Line_on (Li A B) C \<and> \<not> Line_on (Li B C) A \<and> \<not> Line_on (Li C A) B
[PROOF STEP]
from P8 P12 P16
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li A B) C
\<not> Line_on (Li B C) A
\<not> Line_on (Li C A) B
[PROOF STEP]
show "\<not> Line_on (Li A B) C \<and> \<not> Line_on (Li B C) A \<and> \<not> Line_on (Li C A) B"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li A B) C
\<not> Line_on (Li B C) A
\<not> Line_on (Li C A) B

goal (1 subgoal):
 1. \<not> Line_on (Li A B) C \<and> \<not> Line_on (Li B C) A \<and> \<not> Line_on (Li C A) B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li A B) C \<and> \<not> Line_on (Li B C) A \<and> \<not> Line_on (Li C A) B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Congruence_Rule) Tri_def_trans :
  assumes
    "Def (Tri (Tr A B C))"
  shows "Def (Tri (Tr B C A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Def (Tri (Tr B C A))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Def (Tri (Tr B C A))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
[PROOF STEP]
have P1 : "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
        \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
        \<and> \<not> Bet_Point (Se A B) C \<and> \<not> Bet_Point (Se B C) A \<and> \<not> Bet_Point (Se C A) B"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))

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

goal (1 subgoal):
 1. Def (Tri (Tr B C A))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
[PROOF STEP]
have P2 : "\<not> Line_on (Li B C) A"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))

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

goal (1 subgoal):
 1. Def (Tri (Tr B C A))
[PROOF STEP]
from P1 P2
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Bet_Point (Se A B) C \<and> \<not> Bet_Point (Se B C) A \<and> \<not> Bet_Point (Se C A) B
\<not> Line_on (Li B C) A
[PROOF STEP]
show "Def (Tri (Tr B C A))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Bet_Point (Se A B) C \<and> \<not> Bet_Point (Se B C) A \<and> \<not> Bet_Point (Se C A) B
\<not> Line_on (Li B C) A

goal (1 subgoal):
 1. Def (Tri (Tr B C A))
[PROOF STEP]
by (simp add:Tri_sinple_def)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr B C A))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Congruence_Rule) Tri_def_rev :
  assumes
    "Def (Tri (Tr A B C))"
  shows "Def (Tri (Tr C B A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Def (Tri (Tr C B A))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Def (Tri (Tr C B A))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
[PROOF STEP]
have P1 : "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
        \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
        \<and> \<not> Bet_Point (Se A B) C \<and> \<not> Bet_Point (Se B C) A \<and> \<not> Bet_Point (Se C A) B"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))

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

goal (1 subgoal):
 1. Def (Tri (Tr C B A))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
[PROOF STEP]
have P2 : "\<not> Line_on (Li B C) A"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))

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

goal (1 subgoal):
 1. Def (Tri (Tr C B A))
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Bet_Point (Se A B) C \<and> \<not> Bet_Point (Se B C) A \<and> \<not> Bet_Point (Se C A) B
[PROOF STEP]
have P3 : "Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li C B)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Bet_Point (Se A B) C \<and> \<not> Bet_Point (Se B C) A \<and> \<not> Bet_Point (Se C A) B

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

goal (1 subgoal):
 1. Def (Tri (Tr C B A))
[PROOF STEP]
from P2 P3
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B C) A
Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li C B)) add Emp)
[PROOF STEP]
have P4 : "\<not> Line_on (Li C B) A"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B C) A
Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li C B)) add Emp)

goal (1 subgoal):
 1. \<not> Line_on (Li C B) A
[PROOF STEP]
by (simp add:Line_not_on_trans)
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li C B) A

goal (1 subgoal):
 1. Def (Tri (Tr C B A))
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Bet_Point (Se A B) C \<and> \<not> Bet_Point (Se B C) A \<and> \<not> Bet_Point (Se C A) B
[PROOF STEP]
have P5 : "\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi B) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Bet_Point (Se A B) C \<and> \<not> Bet_Point (Se B C) A \<and> \<not> Bet_Point (Se C A) B

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

goal (1 subgoal):
 1. Def (Tri (Tr C B A))
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Bet_Point (Se A B) C \<and> \<not> Bet_Point (Se B C) A \<and> \<not> Bet_Point (Se C A) B
[PROOF STEP]
have P6 : "\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Bet_Point (Se A B) C \<and> \<not> Bet_Point (Se B C) A \<and> \<not> Bet_Point (Se C A) B

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

goal (1 subgoal):
 1. Def (Tri (Tr C B A))
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Bet_Point (Se A B) C \<and> \<not> Bet_Point (Se B C) A \<and> \<not> Bet_Point (Se C A) B
[PROOF STEP]
have P7 : "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Bet_Point (Se A B) C \<and> \<not> Bet_Point (Se B C) A \<and> \<not> Bet_Point (Se C A) B

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

goal (1 subgoal):
 1. Def (Tri (Tr C B A))
[PROOF STEP]
from P4 P5 P6 P7
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li C B) A
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
show "Def (Tri (Tr C B A))"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li C B) A
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)

goal (1 subgoal):
 1. Def (Tri (Tr C B A))
[PROOF STEP]
by (simp add:Tri_sinple_def)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr C B A))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Congruence_Rule) Tri_def_extension :
  assumes
    "Def (Tri (Tr A B C))"
    "\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)"
    "Line_on (Li B C) D"
  shows "Def (Tri (Tr A B D))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Def (Tri (Tr A B D))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Def (Tri (Tr A B D))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
Line_on (Li B C) D
[PROOF STEP]
have P1 : "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
Line_on (Li B C) D

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

goal (1 subgoal):
 1. Def (Tri (Tr A B D))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
Line_on (Li B C) D
[PROOF STEP]
have P2 : "\<not> Line_on (Li B C) A"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
Line_on (Li B C) D

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

goal (1 subgoal):
 1. Def (Tri (Tr A B D))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
Line_on (Li B C) D
[PROOF STEP]
have P3 : "Eq (Geos (Poi D) add Emp) (Geos (Poi A) add Emp) \<Longrightarrow> Line_on (Li B C) A"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
Line_on (Li B C) D

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

goal (1 subgoal):
 1. Def (Tri (Tr A B D))
[PROOF STEP]
from P2 P3
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B C) A
Eq (Geos (Poi D) add Emp) (Geos (Poi A) add Emp) \<Longrightarrow> Line_on (Li B C) A
[PROOF STEP]
have P4 : "\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi A) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B C) A
Eq (Geos (Poi D) add Emp) (Geos (Poi A) add Emp) \<Longrightarrow> Line_on (Li B C) A

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

goal (1 subgoal):
 1. Def (Tri (Tr A B D))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
Line_on (Li B C) D
[PROOF STEP]
have P5 : "\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
Line_on (Li B C) D

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. Def (Tri (Tr A B D))
[PROOF STEP]
from assms P5
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
Line_on (Li B C) D
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
have P6 : "Line_on (Li B D) C"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
Line_on (Li B C) D
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)

goal (1 subgoal):
 1. Line_on (Li B D) C
[PROOF STEP]
by (simp add:Line_on_rev)
[PROOF STATE]
proof (state)
this:
Line_on (Li B D) C

goal (1 subgoal):
 1. Def (Tri (Tr A B D))
[PROOF STEP]
have P7 : "Line_on (Li B D) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B D) B
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B D) B

goal (1 subgoal):
 1. Def (Tri (Tr A B D))
[PROOF STEP]
have P8 : "Line_on (Li B C) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B C) B
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B C) B

goal (1 subgoal):
 1. Def (Tri (Tr A B D))
[PROOF STEP]
have P9 : "Line_on (Li B C) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B C) C
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B C) C

goal (1 subgoal):
 1. Def (Tri (Tr A B D))
[PROOF STEP]
from P5 P6 P7 P8 P9
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
Line_on (Li B D) C
Line_on (Li B D) B
Line_on (Li B C) B
Line_on (Li B C) C
[PROOF STEP]
have "Eq (Geos (Lin (Li B D)) add Emp) (Geos (Lin (Li B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
Line_on (Li B D) C
Line_on (Li B D) B
Line_on (Li B C) B
Line_on (Li B C) C

goal (1 subgoal):
 1. Eq (Geos (Lin (Li B D)) add Emp) (Geos (Lin (Li B C)) add Emp)
[PROOF STEP]
by (simp add:Line_unique)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li B D)) add Emp) (Geos (Lin (Li B C)) add Emp)

goal (1 subgoal):
 1. Def (Tri (Tr A B D))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li B D)) add Emp) (Geos (Lin (Li B C)) add Emp)
[PROOF STEP]
have P10 : "Line_on (Li B D) A \<Longrightarrow> Line_on (Li B C) A"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li B D)) add Emp) (Geos (Lin (Li B C)) add Emp)

goal (1 subgoal):
 1. Line_on (Li B D) A \<Longrightarrow> Line_on (Li B C) A
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Line_on (Li B D) A \<Longrightarrow> Line_on (Li B C) A

goal (1 subgoal):
 1. Def (Tri (Tr A B D))
[PROOF STEP]
from P2 P10
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B C) A
Line_on (Li B D) A \<Longrightarrow> Line_on (Li B C) A
[PROOF STEP]
have P11 : "\<not> Line_on (Li B D) A"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B C) A
Line_on (Li B D) A \<Longrightarrow> Line_on (Li B C) A

goal (1 subgoal):
 1. \<not> Line_on (Li B D) A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li B D) A

goal (1 subgoal):
 1. Def (Tri (Tr A B D))
[PROOF STEP]
from assms P1 P4 P11
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
Line_on (Li B C) D
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi A) add Emp)
\<not> Line_on (Li B D) A
[PROOF STEP]
have "Def (Tri (Tr B D A))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
Line_on (Li B C) D
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi A) add Emp)
\<not> Line_on (Li B D) A

goal (1 subgoal):
 1. Def (Tri (Tr B D A))
[PROOF STEP]
by (simp add:Tri_sinple_def)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr B D A))

goal (1 subgoal):
 1. Def (Tri (Tr A B D))
[PROOF STEP]
thus "Def (Tri (Tr A B D))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr B D A))

goal (1 subgoal):
 1. Def (Tri (Tr A B D))
[PROOF STEP]
by (simp add:Tri_def_trans)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr A B D))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Congruence_Rule) Ang_to_Tri :
  assumes
    "Def (Ang (An A B C))"
  shows "Def (Tri (Tr A B C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
[PROOF STEP]
have P1 : "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
    \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
    \<and> \<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))

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

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
have P2 : "Line_on (Li B A) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B A) B
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B A) B

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
have P3 : "Line_on (Li B C) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B C) B
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B C) B

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
have P4 : "Line_on (Li B C) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B C) C
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B C) C

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
[PROOF STEP]
have P5 : "\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)

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

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
[PROOF STEP]
have "Eq (Geos (Lin (Li A B)) add Emp) (Geos (Lin (Li B A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)

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

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li A B)) add Emp) (Geos (Lin (Li B A)) add Emp)
[PROOF STEP]
have P6 : "Line_on (Li A B) C \<Longrightarrow> Line_on (Li B A) C"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li A B)) add Emp) (Geos (Lin (Li B A)) add Emp)

goal (1 subgoal):
 1. Line_on (Li A B) C \<Longrightarrow> Line_on (Li B A) C
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Line_on (Li A B) C \<Longrightarrow> Line_on (Li B A) C

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from P2 P3 P4 P5 P6
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B A) B
Line_on (Li B C) B
Line_on (Li B C) C
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
Line_on (Li A B) C \<Longrightarrow> Line_on (Li B A) C
[PROOF STEP]
have P7 : "Line_on (Li A B) C \<Longrightarrow> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B A) B
Line_on (Li B C) B
Line_on (Li B C) C
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
Line_on (Li A B) C \<Longrightarrow> Line_on (Li B A) C

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

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from P1 P7
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
Line_on (Li A B) C \<Longrightarrow> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
[PROOF STEP]
have P8 : "\<not> Line_on (Li A B) C"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
Line_on (Li A B) C \<Longrightarrow> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)

goal (1 subgoal):
 1. \<not> Line_on (Li A B) C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li A B) C

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
from P1 P8
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
\<not> Line_on (Li A B) C
[PROOF STEP]
show "Def (Tri (Tr A B C))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
\<not> Line_on (Li A B) C

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
by (simp add:Tri_sinple_def)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr A B C))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Congruence_Rule) Ang_sinple_def :
  assumes
    "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)"
    "\<not> Line_on (Li A B) C"
  shows "Def (Ang (An A B C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Def (Ang (An A B C))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Def (Ang (An A B C))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Line_on (Li A B) C
[PROOF STEP]
have P1 : "Eq (Geos (Lin (Li A B)) add Emp) (Geos (Lin (Li B A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Line_on (Li A B) C

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

goal (1 subgoal):
 1. Def (Ang (An A B C))
[PROOF STEP]
from assms P1
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Line_on (Li A B) C
Eq (Geos (Lin (Li A B)) add Emp) (Geos (Lin (Li B A)) add Emp)
[PROOF STEP]
have P2 : "\<not> Line_on (Li B A) C"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Line_on (Li A B) C
Eq (Geos (Lin (Li A B)) add Emp) (Geos (Lin (Li B A)) add Emp)

goal (1 subgoal):
 1. \<not> Line_on (Li B A) C
[PROOF STEP]
by (simp add:Line_not_on_trans)
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li B A) C

goal (1 subgoal):
 1. Def (Ang (An A B C))
[PROOF STEP]
have "Line_on (Li B A) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B A) B
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B A) B

goal (1 subgoal):
 1. Def (Ang (An A B C))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B A) B
[PROOF STEP]
have P3 : "Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<Longrightarrow> Line_on (Li B A) C"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B A) B

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

goal (1 subgoal):
 1. Def (Ang (An A B C))
[PROOF STEP]
from P2 P3
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B A) C
Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<Longrightarrow> Line_on (Li B A) C
[PROOF STEP]
have P4 : "\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B A) C
Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<Longrightarrow> Line_on (Li B A) C

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

goal (1 subgoal):
 1. Def (Ang (An A B C))
[PROOF STEP]
have "Line_on (Li B A) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B A) A
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B A) A

goal (1 subgoal):
 1. Def (Ang (An A B C))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B A) A
[PROOF STEP]
have P5 : "Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp) \<Longrightarrow> Line_on (Li B A) C"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B A) A

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

goal (1 subgoal):
 1. Def (Ang (An A B C))
[PROOF STEP]
from P2 P5
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B A) C
Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp) \<Longrightarrow> Line_on (Li B A) C
[PROOF STEP]
have P6 : "\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B A) C
Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp) \<Longrightarrow> Line_on (Li B A) C

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

goal (1 subgoal):
 1. Def (Ang (An A B C))
[PROOF STEP]
have "Line_on (Li B C) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B C) C
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B C) C

goal (1 subgoal):
 1. Def (Ang (An A B C))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B C) C
[PROOF STEP]
have P7 : "Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li B A)) add Emp) \<Longrightarrow> Line_on (Li B A) C"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B C) C

goal (1 subgoal):
 1. Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li B A)) add Emp) \<Longrightarrow> Line_on (Li B A) C
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li B A)) add Emp) \<Longrightarrow> Line_on (Li B A) C

goal (1 subgoal):
 1. Def (Ang (An A B C))
[PROOF STEP]
from P2 P7
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B A) C
Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li B A)) add Emp) \<Longrightarrow> Line_on (Li B A) C
[PROOF STEP]
have P8 : "\<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B A) C
Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li B A)) add Emp) \<Longrightarrow> Line_on (Li B A) C

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

goal (1 subgoal):
 1. Def (Ang (An A B C))
[PROOF STEP]
from assms P4 P6 P8
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Line_on (Li A B) C
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
\<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
[PROOF STEP]
show "Def (Ang (An A B C))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Line_on (Li A B) C
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
\<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)

goal (1 subgoal):
 1. Def (Ang (An A B C))
[PROOF STEP]
by (simp add:Ang_def)
[PROOF STATE]
proof (state)
this:
Def (Ang (An A B C))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Congruence_Rule) Tri_to_Ang :
  assumes
    "Def (Tri (Tr A B C))"
  shows "Def (Ang (An A B C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Def (Ang (An A B C))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Def (Ang (An A B C))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
[PROOF STEP]
have P1 : "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
    \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))

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

goal (1 subgoal):
 1. Def (Ang (An A B C))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
[PROOF STEP]
have P2 : "\<not> Line_on (Li A B) C"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))

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

goal (1 subgoal):
 1. Def (Ang (An A B C))
[PROOF STEP]
from P1 P2
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
\<not> Line_on (Li A B) C
[PROOF STEP]
show "Def (Ang (An A B C))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
\<not> Line_on (Li A B) C

goal (1 subgoal):
 1. Def (Ang (An A B C))
[PROOF STEP]
by (simp add:Ang_sinple_def)
[PROOF STATE]
proof (state)
this:
Def (Ang (An A B C))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Congruence_Rule) Ang_def_rev :
  assumes
    "Def (Ang (An A B C))"
  shows "Def (Ang (An C B A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Def (Ang (An C B A))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Def (Ang (An C B A))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
[PROOF STEP]
have P1 : "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
    \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
    \<and> \<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))

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

goal (1 subgoal):
 1. Def (Ang (An C B A))
[PROOF STEP]
have P2 : "Line_on (Li B A) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B A) A
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B A) A

goal (1 subgoal):
 1. Def (Ang (An C B A))
[PROOF STEP]
have P3 : "Line_on (Li B A) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B A) B
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B A) B

goal (1 subgoal):
 1. Def (Ang (An C B A))
[PROOF STEP]
have P4 : "Line_on (Li B C) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B C) B
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B C) B

goal (1 subgoal):
 1. Def (Ang (An C B A))
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
[PROOF STEP]
have P5 : "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)

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

goal (1 subgoal):
 1. Def (Ang (An C B A))
[PROOF STEP]
from P2 P3 P4 P5
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B A) A
Line_on (Li B A) B
Line_on (Li B C) B
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
[PROOF STEP]
have P6 : "Line_on (Li B C) A \<Longrightarrow> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B A) A
Line_on (Li B A) B
Line_on (Li B C) B
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)

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

goal (1 subgoal):
 1. Def (Ang (An C B A))
[PROOF STEP]
from P1 P6
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
Line_on (Li B C) A \<Longrightarrow> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
[PROOF STEP]
have P7 : "\<not> Line_on (Li B C) A"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
Line_on (Li B C) A \<Longrightarrow> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)

goal (1 subgoal):
 1. \<not> Line_on (Li B C) A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li B C) A

goal (1 subgoal):
 1. Def (Ang (An C B A))
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
[PROOF STEP]
have P8 : "Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li C B)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)

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

goal (1 subgoal):
 1. Def (Ang (An C B A))
[PROOF STEP]
from P7 P8
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B C) A
Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li C B)) add Emp)
[PROOF STEP]
have P9 : "\<not> Line_on (Li C B) A"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B C) A
Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li C B)) add Emp)

goal (1 subgoal):
 1. \<not> Line_on (Li C B) A
[PROOF STEP]
by (simp add:Line_not_on_trans)
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li C B) A

goal (1 subgoal):
 1. Def (Ang (An C B A))
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
[PROOF STEP]
have P10 : "\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi B) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)

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

goal (1 subgoal):
 1. Def (Ang (An C B A))
[PROOF STEP]
from P9 P10
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li C B) A
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi B) add Emp)
[PROOF STEP]
show "Def (Ang (An C B A))"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li C B) A
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi B) add Emp)

goal (1 subgoal):
 1. Def (Ang (An C B A))
[PROOF STEP]
by (simp add:Ang_sinple_def)
[PROOF STATE]
proof (state)
this:
Def (Ang (An C B A))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Congruence_Rule) Ang_def_inv :
  assumes
    "Def (Ang (An A B C))"
  shows "Def (Ang (An A C B))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Def (Ang (An A C B))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Def (Ang (An A C B))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
[PROOF STEP]
have P1 : "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
    \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
    \<and> \<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))

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

goal (1 subgoal):
 1. Def (Ang (An A C B))
[PROOF STEP]
have P2 : "Line_on (Li B A) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B A) A
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B A) A

goal (1 subgoal):
 1. Def (Ang (An A C B))
[PROOF STEP]
have P3 : "Line_on (Li B A) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B A) B
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B A) B

goal (1 subgoal):
 1. Def (Ang (An A C B))
[PROOF STEP]
have P4 : "Line_on (Li B C) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B C) B
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B C) B

goal (1 subgoal):
 1. Def (Ang (An A C B))
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
[PROOF STEP]
have P5 : "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)

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

goal (1 subgoal):
 1. Def (Ang (An A C B))
[PROOF STEP]
from P2 P3 P4 P5
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B A) A
Line_on (Li B A) B
Line_on (Li B C) B
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
[PROOF STEP]
have P6 : "Line_on (Li B C) A \<Longrightarrow> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B A) A
Line_on (Li B A) B
Line_on (Li B C) B
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)

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

goal (1 subgoal):
 1. Def (Ang (An A C B))
[PROOF STEP]
from P1 P6
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
Line_on (Li B C) A \<Longrightarrow> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
[PROOF STEP]
have P7 : "\<not> Line_on (Li B C) A"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
Line_on (Li B C) A \<Longrightarrow> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)

goal (1 subgoal):
 1. \<not> Line_on (Li B C) A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li B C) A

goal (1 subgoal):
 1. Def (Ang (An A C B))
[PROOF STEP]
have P8 : "Line_on (Li A C) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A C) C
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A C) C

goal (1 subgoal):
 1. Def (Ang (An A C B))
[PROOF STEP]
have P9 : "Line_on (Li B C) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B C) C
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B C) C

goal (1 subgoal):
 1. Def (Ang (An A C B))
[PROOF STEP]
from P1 P4 P8 P9
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
Line_on (Li B C) B
Line_on (Li A C) C
Line_on (Li B C) C
[PROOF STEP]
have P10 : "Line_on (Li A C) B \<Longrightarrow> Eq (Geos (Lin (Li A C)) add Emp) (Geos (Lin (Li B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
Line_on (Li B C) B
Line_on (Li A C) C
Line_on (Li B C) C

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

goal (1 subgoal):
 1. Def (Ang (An A C B))
[PROOF STEP]
have P11 : "Line_on (Li A C) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A C) A
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A C) A

goal (1 subgoal):
 1. Def (Ang (An A C B))
[PROOF STEP]
from P10 P11
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A C) B \<Longrightarrow> Eq (Geos (Lin (Li A C)) add Emp) (Geos (Lin (Li B C)) add Emp)
Line_on (Li A C) A
[PROOF STEP]
have P12 : "Line_on (Li A C) B \<Longrightarrow> Line_on (Li B C) A"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A C) B \<Longrightarrow> Eq (Geos (Lin (Li A C)) add Emp) (Geos (Lin (Li B C)) add Emp)
Line_on (Li A C) A

goal (1 subgoal):
 1. Line_on (Li A C) B \<Longrightarrow> Line_on (Li B C) A
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Line_on (Li A C) B \<Longrightarrow> Line_on (Li B C) A

goal (1 subgoal):
 1. Def (Ang (An A C B))
[PROOF STEP]
from P7 P12
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B C) A
Line_on (Li A C) B \<Longrightarrow> Line_on (Li B C) A
[PROOF STEP]
have P13 : "\<not> Line_on (Li A C) B"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B C) A
Line_on (Li A C) B \<Longrightarrow> Line_on (Li B C) A

goal (1 subgoal):
 1. \<not> Line_on (Li A C) B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li A C) B

goal (1 subgoal):
 1. Def (Ang (An A C B))
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
[PROOF STEP]
have P14 : "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp) \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<and> \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp) \<and> \<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)

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

goal (1 subgoal):
 1. Def (Ang (An A C B))
[PROOF STEP]
from P13 P14
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li A C) B
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
show "Def (Ang (An A C B))"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li A C) B
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)

goal (1 subgoal):
 1. Def (Ang (An A C B))
[PROOF STEP]
by (simp add:Ang_sinple_def)
[PROOF STATE]
proof (state)
this:
Def (Ang (An A C B))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Congruence_Rule) Ang_def_extension :
  assumes
    "Def (Ang (An A B C))"
    "\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)"
    "Line_on (Li B C) D"
  shows "Def (Ang (An A B D))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Def (Ang (An A B D))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Def (Ang (An A B D))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
Line_on (Li B C) D
[PROOF STEP]
have P1 : "Def (Tri (Tr A B C))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
Line_on (Li B C) D

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
by (simp add:Ang_to_Tri)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr A B C))

goal (1 subgoal):
 1. Def (Ang (An A B D))
[PROOF STEP]
from assms P1
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
Line_on (Li B C) D
Def (Tri (Tr A B C))
[PROOF STEP]
have "Def (Tri (Tr A B D))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
Line_on (Li B C) D
Def (Tri (Tr A B C))

goal (1 subgoal):
 1. Def (Tri (Tr A B D))
[PROOF STEP]
by (simp add:Tri_def_extension)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr A B D))

goal (1 subgoal):
 1. Def (Ang (An A B D))
[PROOF STEP]
thus "Def (Ang (An A B D))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B D))

goal (1 subgoal):
 1. Def (Ang (An A B D))
[PROOF STEP]
by (simp add:Tri_to_Ang)
[PROOF STATE]
proof (state)
this:
Def (Ang (An A B D))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Congruence_Rule) Bet_end_Point :
  shows "\<not> Bet_Point (Se p1 p1) p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se p1 p1) p2
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Bet_Point (Se p1 p1) p2 \<Longrightarrow> False
[PROOF STEP]
assume W : "Bet_Point (Se p1 p1) p2"
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p1 p1) p2

goal (1 subgoal):
 1. Bet_Point (Se p1 p1) p2 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p1 p1) p2
[PROOF STEP]
have P1 : "\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p1 p1) p2

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

goal (1 subgoal):
 1. Bet_Point (Se p1 p1) p2 \<Longrightarrow> False
[PROOF STEP]
have P2 : "Eq (Geos (Poi p1) add Emp) (Geos (Poi p1) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Poi p1) add Emp) (Geos (Poi p1) add Emp)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi p1) add Emp) (Geos (Poi p1) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se p1 p1) p2 \<Longrightarrow> False
[PROOF STEP]
from P1 P2
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p1) add Emp)
Eq (Geos (Poi p1) add Emp) (Geos (Poi p1) add Emp)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p1) add Emp)
Eq (Geos (Poi p1) add Emp) (Geos (Poi p1) add Emp)

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

goal:
No subgoals!
[PROOF STEP]
qed