[STATEMENT]
lemma (in Congruence_Rule) Ang_replace :
  assumes
    "Def (Ang (An A B C))"
    "Def (Ang (An A1 B1 C1))"
    "Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)"
  shows "\<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp)
    \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp)
    \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))"
    and "\<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp)
    \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp)
    \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))"
    and "\<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp)
    \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp)
    \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1
    \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1)) &&& \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p)) &&& \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
 2. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 3. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
[PROOF STEP]
have P1 : "\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)

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

goal (3 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
 2. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 3. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)
[PROOF STEP]
have P2 : "\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)

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

goal (3 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
 2. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 3. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
have P3 : "Line_on (Li B1 A1) A1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B1 A1) A1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B1 A1) A1

goal (3 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
 2. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 3. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
have P4 : "Line_on (Li B1 A1) B1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B1 A1) B1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B1 A1) B1

goal (3 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
 2. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 3. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
[PROOF STEP]
have "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) 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)

goal (3 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
 2. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 3. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
[PROOF STEP]
have P5 : "\<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)

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 (3 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
 2. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 3. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from P2 P3 P4 P5
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A1) add Emp)
Line_on (Li B1 A1) A1
Line_on (Li B1 A1) B1
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)
[PROOF STEP]
have "\<exists>p. Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> \<not> Bet_Point (Se p A1) B1 \<and> Line_on (Li B1 A1) p \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi p) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A1) add Emp)
Line_on (Li B1 A1) A1
Line_on (Li B1 A1) B1
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)

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

goal (3 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
 2. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 3. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> \<not> Bet_Point (Se p A1) B1 \<and> Line_on (Li B1 A1) p \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
obtain A2 :: Point where P6 : "Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Line_on (Li B1 A1) A2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> \<not> Bet_Point (Se p A1) B1 \<and> Line_on (Li B1 A1) p \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi p) add Emp)

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

goal (3 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
 2. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 3. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
[PROOF STEP]
have P7 : "\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)

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

goal (3 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
 2. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 3. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
have P8 : "Line_on (Li B1 C1) B1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B1 C1) B1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B1 C1) B1

goal (3 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
 2. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 3. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
have P9 : "Line_on (Li B1 C1) C1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B1 C1) C1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B1 C1) C1

goal (3 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
 2. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 3. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
[PROOF STEP]
have P10 : "\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)

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

goal (3 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
 2. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 3. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from P7 P8 P9 P10
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C1) add Emp)
Line_on (Li B1 C1) B1
Line_on (Li B1 C1) C1
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
have "\<exists>p. Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> \<not> Bet_Point (Se p C1) B1 \<and> Line_on (Li B1 C1) p \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi p) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C1) add Emp)
Line_on (Li B1 C1) B1
Line_on (Li B1 C1) C1
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)

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

goal (3 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
 2. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 3. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> \<not> Bet_Point (Se p C1) B1 \<and> Line_on (Li B1 C1) p \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
obtain C2 :: Point where P11 : "Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) \<and> \<not> Bet_Point (Se C2 C1) B1 \<and> Line_on (Li B1 C1) C2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> \<not> Bet_Point (Se p C1) B1 \<and> Line_on (Li B1 C1) p \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi p) add Emp)

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

goal (3 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
 2. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 3. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
have P12 : "\<not> Bet_Point (Se C1 C1) B1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se C1 C1) B1
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se C1 C1) B1

goal (3 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
 2. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 3. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from P6
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Line_on (Li B1 A1) A2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)
[PROOF STEP]
have P13 : "\<not> Bet_Point (Se A1 A2) B1"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Line_on (Li B1 A1) A2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)

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

goal (3 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
 2. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 3. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from assms P3 P6 P7 P9 P12 P13
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Line_on (Li B1 A1) A1
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Line_on (Li B1 A1) A2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C1) add Emp)
Line_on (Li B1 C1) C1
\<not> Bet_Point (Se C1 C1) B1
\<not> Bet_Point (Se A1 A2) B1
[PROOF STEP]
have P14 : "Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B1 C1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Line_on (Li B1 A1) A1
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Line_on (Li B1 A1) A2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C1) add Emp)
Line_on (Li B1 C1) C1
\<not> Bet_Point (Se C1 C1) B1
\<not> Bet_Point (Se A1 A2) B1

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

goal (3 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
 2. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 3. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from assms P14
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B1 C1)) add Emp)
[PROOF STEP]
have P15 : "Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B1 C1)) add Emp)

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

goal (3 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
 2. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 3. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
[PROOF STEP]
have P16 : "\<not> Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)

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

goal (3 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
 2. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 3. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from P6
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Line_on (Li B1 A1) A2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)
[PROOF STEP]
have P17 : "Line_on (Li B1 A1) A2"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Line_on (Li B1 A1) A2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)

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

goal (3 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
 2. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 3. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from P6
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Line_on (Li B1 A1) A2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)
[PROOF STEP]
have P18 : "\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Line_on (Li B1 A1) A2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)

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

goal (3 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
 2. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 3. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from P4 P8 P17 P18
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B1 A1) B1
Line_on (Li B1 C1) B1
Line_on (Li B1 A1) A2
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)
[PROOF STEP]
have P19 : "Line_on (Li B1 C1) A2 \<Longrightarrow> Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B1 A1) B1
Line_on (Li B1 C1) B1
Line_on (Li B1 A1) A2
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)

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

goal (3 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
 2. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 3. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from P16 P19
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)
Line_on (Li B1 C1) A2 \<Longrightarrow> Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)
[PROOF STEP]
have P20 : "\<not> Line_on (Li B1 C1) A2"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)
Line_on (Li B1 C1) A2 \<Longrightarrow> Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)

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

goal (3 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
 2. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 3. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from P7 P20
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C1) add Emp)
\<not> Line_on (Li B1 C1) A2
[PROOF STEP]
have "Def (Ang (An B1 C1 A2))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C1) add Emp)
\<not> Line_on (Li B1 C1) A2

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

goal (3 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
 2. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 3. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An B1 C1 A2))
[PROOF STEP]
have P21 : "Def (Ang (An A2 B1 C1))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An B1 C1 A2))

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

goal (3 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
 2. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 3. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from P6 P14 P15 P21
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Line_on (Li B1 A1) A2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)
Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B1 C1)) add Emp)
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C1)) add Emp)
Def (Ang (An A2 B1 C1))
[PROOF STEP]
show "\<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp)
    \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp)
    \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Line_on (Li B1 A1) A2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)
Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B1 C1)) add Emp)
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C1)) add Emp)
Def (Ang (An A2 B1 C1))

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))

goal (2 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 2. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
have P22 : "\<not> Bet_Point (Se A1 A1) B1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se A1 A1) B1
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se A1 A1) B1

goal (2 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 2. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from P11
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) \<and> \<not> Bet_Point (Se C2 C1) B1 \<and> Line_on (Li B1 C1) C2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)
[PROOF STEP]
have P23 : "\<not> Bet_Point (Se C1 C2) B1"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) \<and> \<not> Bet_Point (Se C2 C1) B1 \<and> Line_on (Li B1 C1) C2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)

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

goal (2 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 2. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from assms P2 P3 P7 P11 P22 P23
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A1) add Emp)
Line_on (Li B1 A1) A1
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C1) add Emp)
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) \<and> \<not> Bet_Point (Se C2 C1) B1 \<and> Line_on (Li B1 C1) C2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)
\<not> Bet_Point (Se A1 A1) B1
\<not> Bet_Point (Se C1 C2) B1
[PROOF STEP]
have P24 : "Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A1) add Emp)
Line_on (Li B1 A1) A1
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C1) add Emp)
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) \<and> \<not> Bet_Point (Se C2 C1) B1 \<and> Line_on (Li B1 C1) C2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)
\<not> Bet_Point (Se A1 A1) B1
\<not> Bet_Point (Se C1 C2) B1

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

goal (2 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 2. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from assms P24
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 C2)) add Emp)
[PROOF STEP]
have P25 : "Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 C2)) add Emp)

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

goal (2 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 2. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from P11
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) \<and> \<not> Bet_Point (Se C2 C1) B1 \<and> Line_on (Li B1 C1) C2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)
[PROOF STEP]
have P26 : "Line_on (Li B1 C1) C2"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) \<and> \<not> Bet_Point (Se C2 C1) B1 \<and> Line_on (Li B1 C1) C2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)

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

goal (2 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 2. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from P11
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) \<and> \<not> Bet_Point (Se C2 C1) B1 \<and> Line_on (Li B1 C1) C2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)
[PROOF STEP]
have P27 : "\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) \<and> \<not> Bet_Point (Se C2 C1) B1 \<and> Line_on (Li B1 C1) C2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)

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

goal (2 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 2. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from P4 P8 P26 P27
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B1 A1) B1
Line_on (Li B1 C1) B1
Line_on (Li B1 C1) C2
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)
[PROOF STEP]
have P28 : "Line_on (Li B1 A1) C2 \<Longrightarrow> Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B1 A1) B1
Line_on (Li B1 C1) B1
Line_on (Li B1 C1) C2
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)

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

goal (2 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 2. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from P16 P28
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)
Line_on (Li B1 A1) C2 \<Longrightarrow> Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)
[PROOF STEP]
have P29: "\<not> Line_on (Li B1 A1) C2"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)
Line_on (Li B1 A1) C2 \<Longrightarrow> Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)

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

goal (2 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 2. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from P2 P29
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A1) add Emp)
\<not> Line_on (Li B1 A1) C2
[PROOF STEP]
have "Def (Ang (An B1 A1 C2))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A1) add Emp)
\<not> Line_on (Li B1 A1) C2

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

goal (2 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 2. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An B1 A1 C2))
[PROOF STEP]
have P30 : "Def (Ang (An A1 B1 C2))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An B1 A1 C2))

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

goal (2 subgoals):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
 2. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from P11 P24 P25 P30
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) \<and> \<not> Bet_Point (Se C2 C1) B1 \<and> Line_on (Li B1 C1) C2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)
Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 C2)) add Emp)
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C2)) add Emp)
Def (Ang (An A1 B1 C2))
[PROOF STEP]
show "\<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp)
    \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp)
    \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) \<and> \<not> Bet_Point (Se C2 C1) B1 \<and> Line_on (Li B1 C1) C2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)
Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 C2)) add Emp)
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C2)) add Emp)
Def (Ang (An A1 B1 C2))

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A1 B1 p))

goal (1 subgoal):
 1. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from assms P6 P11 P13 P17 P23 P26
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Line_on (Li B1 A1) A2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) \<and> \<not> Bet_Point (Se C2 C1) B1 \<and> Line_on (Li B1 C1) C2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)
\<not> Bet_Point (Se A1 A2) B1
Line_on (Li B1 A1) A2
\<not> Bet_Point (Se C1 C2) B1
Line_on (Li B1 C1) C2
[PROOF STEP]
have P31 : "Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B1 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Line_on (Li B1 A1) A2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) \<and> \<not> Bet_Point (Se C2 C1) B1 \<and> Line_on (Li B1 C1) C2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)
\<not> Bet_Point (Se A1 A2) B1
Line_on (Li B1 A1) A2
\<not> Bet_Point (Se C1 C2) B1
Line_on (Li B1 C1) C2

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

goal (1 subgoal):
 1. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from assms P31
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B1 C2)) add Emp)
[PROOF STEP]
have P32 : "Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B1 C2)) add Emp)

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

goal (1 subgoal):
 1. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
have P33 : "Line_on (Li B1 C2) B1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B1 C2) B1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B1 C2) B1

goal (1 subgoal):
 1. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
have P34 : "Line_on (Li B1 C2) C2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B1 C2) C2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B1 C2) C2

goal (1 subgoal):
 1. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from P8 P26 P27 P33 P34
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B1 C1) B1
Line_on (Li B1 C1) C2
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)
Line_on (Li B1 C2) B1
Line_on (Li B1 C2) C2
[PROOF STEP]
have "Eq (Geos (Lin (Li B1 C2)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B1 C1) B1
Line_on (Li B1 C1) C2
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)
Line_on (Li B1 C2) B1
Line_on (Li B1 C2) C2

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

goal (1 subgoal):
 1. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li B1 C2)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)
[PROOF STEP]
have P35 : "Line_on (Li B1 C2) A2 \<Longrightarrow> Line_on (Li B1 C1) A2"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li B1 C2)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)

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

goal (1 subgoal):
 1. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from P20 P35
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B1 C1) A2
Line_on (Li B1 C2) A2 \<Longrightarrow> Line_on (Li B1 C1) A2
[PROOF STEP]
have P36 : "\<not> Line_on (Li B1 C2) A2"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B1 C1) A2
Line_on (Li B1 C2) A2 \<Longrightarrow> Line_on (Li B1 C1) A2

goal (1 subgoal):
 1. \<not> Line_on (Li B1 C2) A2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li B1 C2) A2

goal (1 subgoal):
 1. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from P11 P36
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) \<and> \<not> Bet_Point (Se C2 C1) B1 \<and> Line_on (Li B1 C1) C2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)
\<not> Line_on (Li B1 C2) A2
[PROOF STEP]
have "Def (Ang (An B1 C2 A2))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) \<and> \<not> Bet_Point (Se C2 C1) B1 \<and> Line_on (Li B1 C1) C2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)
\<not> Line_on (Li B1 C2) A2

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

goal (1 subgoal):
 1. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An B1 C2 A2))
[PROOF STEP]
have P37 : "Def (Ang (An A2 B1 C2))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An B1 C2 A2))

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

goal (1 subgoal):
 1. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
from P6 P11 P21 P30 P31 P32 P37
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Line_on (Li B1 A1) A2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) \<and> \<not> Bet_Point (Se C2 C1) B1 \<and> Line_on (Li B1 C1) C2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)
Def (Ang (An A2 B1 C1))
Def (Ang (An A1 B1 C2))
Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B1 C2)) add Emp)
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C2)) add Emp)
Def (Ang (An A2 B1 C2))
[PROOF STEP]
show "\<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp)
    \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp)
    \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1
    \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Line_on (Li B1 A1) A2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)
Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) \<and> \<not> Bet_Point (Se C2 C1) B1 \<and> Line_on (Li B1 C1) C2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)
Def (Ang (An A2 B1 C1))
Def (Ang (An A1 B1 C2))
Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B1 C2)) add Emp)
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C2)) add Emp)
Def (Ang (An A2 B1 C2))

goal (1 subgoal):
 1. \<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) \<and> Line_on (Li B1 C1) q \<and> \<not> Bet_Point (Se q C1) B1 \<and> Def (Ang (An p B1 q))

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

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

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr C B A))
[PROOF STEP]
have P3 : "Def (Tri (Tr A C B))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr C B A))

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

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

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

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed