[STATEMENT]
theorem (in Congruence_Rule) Ang_bisection :
  assumes
    "Def (Ang (An A B C))"
  shows
    "\<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp)
    \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
have P1 : "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. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
have P2 : "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. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
[PROOF STEP]
have P3 : "\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))

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 (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
[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))

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 (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
[PROOF STEP]
have P4 : "\<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 (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P1 P2 P3 P4
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B C) B
Line_on (Li B C) C
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<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 B p)) add Emp)
    \<and> \<not> Bet_Point (Se p C) B \<and> Line_on (Li B C) p \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi p) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B C) B
Line_on (Li B C) C
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<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 B p)) add Emp) \<and> \<not> Bet_Point (Se p C) B \<and> Line_on (Li B C) p \<and> \<not> Eq (Geos (Poi B) 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 B p)) add Emp) \<and> \<not> Bet_Point (Se p C) B \<and> Line_on (Li B C) p \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi p) add Emp)

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

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

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

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

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

goal (1 subgoal):
 1. Eq (Geos (Poi C2) 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 C2) add Emp) (Geos (Poi A) add Emp) \<Longrightarrow> Line_on (Li B C) A

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
[PROOF STEP]
have P8 : "Def (Tri (Tr A B C))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))

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. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
[PROOF STEP]
have P9 : "\<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. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P7 P9
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Poi C2) add Emp) (Geos (Poi A) add Emp) \<Longrightarrow> Line_on (Li B C) A
\<not> Line_on (Li B C) A
[PROOF STEP]
have P10 : "\<not> Eq (Geos (Poi C2) add Emp) (Geos (Poi A) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Poi C2) add Emp) (Geos (Poi A) add Emp) \<Longrightarrow> Line_on (Li B C) A
\<not> Line_on (Li B C) A

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

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

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se C2 p)) add Emp) (Geos (Seg (Se p A)) add Emp) \<and> Bet_Point (Se C2 A) p
[PROOF STEP]
by (simp add:Seg_bisection)
[PROOF STATE]
proof (state)
this:
\<exists>p. Eq (Geos (Seg (Se C2 p)) add Emp) (Geos (Seg (Se p A)) add Emp) \<and> Bet_Point (Se C2 A) p

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Eq (Geos (Seg (Se C2 p)) add Emp) (Geos (Seg (Se p A)) add Emp) \<and> Bet_Point (Se C2 A) p
[PROOF STEP]
obtain D :: Point where P11 : "Eq (Geos (Seg (Se C2 D)) add Emp) (Geos (Seg (Se D A)) add Emp)
    \<and> Bet_Point (Se C2 A) D"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Eq (Geos (Seg (Se C2 p)) add Emp) (Geos (Seg (Se p A)) add Emp) \<and> Bet_Point (Se C2 A) p

goal (1 subgoal):
 1. (\<And>D. Eq (Geos (Seg (Se C2 D)) add Emp) (Geos (Seg (Se D A)) add Emp) \<and> Bet_Point (Se C2 A) D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se C2 D)) add Emp) (Geos (Seg (Se D A)) add Emp) \<and> Bet_Point (Se C2 A) D

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
have P12 : "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. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P1 P5 P6 P12
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B C) B
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B C2)) add Emp) \<and> \<not> Bet_Point (Se C2 C) B \<and> Line_on (Li B C) C2 \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C2) add Emp)
Line_on (Li B C) C2
Line_on (Li B A) B
[PROOF STEP]
have P13 : "Line_on (Li B A) C2 \<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 C) B
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B C2)) add Emp) \<and> \<not> Bet_Point (Se C2 C) B \<and> Line_on (Li B C) C2 \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C2) add Emp)
Line_on (Li B C) C2
Line_on (Li B A) B

goal (1 subgoal):
 1. Line_on (Li B A) C2 \<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 A) C2 \<Longrightarrow> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
[PROOF STEP]
have P14 : "\<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 (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 (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P13 P14
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B A) C2 \<Longrightarrow> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
\<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
[PROOF STEP]
have P15 : "\<not> Line_on (Li B A) C2"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B A) C2 \<Longrightarrow> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
\<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)

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

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P11
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se C2 D)) add Emp) (Geos (Seg (Se D A)) add Emp) \<and> Bet_Point (Se C2 A) D
[PROOF STEP]
have P16 : "Bet_Point (Se C2 A) D"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se C2 D)) add Emp) (Geos (Seg (Se D A)) add Emp) \<and> Bet_Point (Se C2 A) D

goal (1 subgoal):
 1. Bet_Point (Se C2 A) D
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Bet_Point (Se C2 A) D

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se C2 A) D
[PROOF STEP]
have P17 : "Line_on (Li C2 A) D"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se C2 A) D

goal (1 subgoal):
 1. Line_on (Li C2 A) D
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li C2 A) D

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
have P18 : "Line_on (Li C2 A) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li C2 A) A
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li C2 A) A

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
have P19 : "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. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P16
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se C2 A) D
[PROOF STEP]
have P20 : "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se C2 A) D

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

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P17 P18 P19 P20
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li C2 A) D
Line_on (Li C2 A) A
Line_on (Li B A) A
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)
[PROOF STEP]
have P21 : "Line_on (Li B A) D \<Longrightarrow>
    Eq (Geos (Lin (Li C2 A)) add Emp) (Geos (Lin (Li B A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li C2 A) D
Line_on (Li C2 A) A
Line_on (Li B A) A
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)

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

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
have P22 : "Line_on (Li C2 A) C2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li C2 A) C2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li C2 A) C2

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P21 P22
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B A) D \<Longrightarrow> Eq (Geos (Lin (Li C2 A)) add Emp) (Geos (Lin (Li B A)) add Emp)
Line_on (Li C2 A) C2
[PROOF STEP]
have P23 : "Line_on (Li B A) D \<Longrightarrow> Line_on (Li B A) C2"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B A) D \<Longrightarrow> Eq (Geos (Lin (Li C2 A)) add Emp) (Geos (Lin (Li B A)) add Emp)
Line_on (Li C2 A) C2

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

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P15 P23
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B A) C2
Line_on (Li B A) D \<Longrightarrow> Line_on (Li B A) C2
[PROOF STEP]
have P24 : "\<not> Line_on (Li B A) D"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B A) C2
Line_on (Li B A) D \<Longrightarrow> Line_on (Li B A) C2

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

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P4 P24
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)
\<not> Line_on (Li B A) D
[PROOF STEP]
have "Def (Ang (An B A D))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)
\<not> Line_on (Li B A) D

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

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An B A D))
[PROOF STEP]
have P25 : "Def (Tri (Tr A B D))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An B A D))

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

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P4 P15
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)
\<not> Line_on (Li B A) C2
[PROOF STEP]
have P26 : "Def (Ang (An B A C2))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)
\<not> Line_on (Li B A) C2

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

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An B A C2))
[PROOF STEP]
have "Def (Tri (Tr C2 B A))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An B A C2))

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

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr C2 B A))
[PROOF STEP]
have P27 : "\<not> Line_on (Li C2 B) A"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr C2 B A))

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

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
have P28 : "Line_on (Li C2 B) C2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li C2 B) C2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li C2 B) C2

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P16
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se C2 A) D
[PROOF STEP]
have P29 : "\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi C2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se C2 A) D

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

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P17 P22 P28 P29
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li C2 A) D
Line_on (Li C2 A) C2
Line_on (Li C2 B) C2
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi C2) add Emp)
[PROOF STEP]
have P30 : "Line_on (Li C2 B) D \<Longrightarrow>
    Eq (Geos (Lin (Li C2 A)) add Emp) (Geos (Lin (Li C2 B)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li C2 A) D
Line_on (Li C2 A) C2
Line_on (Li C2 B) C2
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi C2) add Emp)

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

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P18 P30
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li C2 A) A
Line_on (Li C2 B) D \<Longrightarrow> Eq (Geos (Lin (Li C2 A)) add Emp) (Geos (Lin (Li C2 B)) add Emp)
[PROOF STEP]
have P31 : "Line_on (Li C2 B) D \<Longrightarrow> Line_on (Li C2 B) A"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li C2 A) A
Line_on (Li C2 B) D \<Longrightarrow> Eq (Geos (Lin (Li C2 A)) add Emp) (Geos (Lin (Li C2 B)) add Emp)

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

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P27 P31
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li C2 B) A
Line_on (Li C2 B) D \<Longrightarrow> Line_on (Li C2 B) A
[PROOF STEP]
have P32 : "\<not> Line_on (Li C2 B) D"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li C2 B) A
Line_on (Li C2 B) D \<Longrightarrow> Line_on (Li C2 B) A

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

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

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

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P32 P33
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li C2 B) D
\<not> Eq (Geos (Poi C2) add Emp) (Geos (Poi B) add Emp)
[PROOF STEP]
have "Def (Ang (An C2 B D))"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li C2 B) D
\<not> Eq (Geos (Poi C2) add Emp) (Geos (Poi B) add Emp)

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

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An C2 B D))
[PROOF STEP]
have P34 : "Def (Tri (Tr C2 B D))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An C2 B D))

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

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
have P35 : "Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se A B)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se A B)) add Emp)
[PROOF STEP]
by (simp add:Seg_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se A B)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
have P36 : "Eq (Geos (Seg (Se B C2)) add Emp) (Geos (Seg (Se C2 B)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Seg (Se B C2)) add Emp) (Geos (Seg (Se C2 B)) add Emp)
[PROOF STEP]
by (simp add:Seg_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se B C2)) add Emp) (Geos (Seg (Se C2 B)) add Emp)

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

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

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P35 P36 P37
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se A B)) add Emp)
Eq (Geos (Seg (Se B C2)) add Emp) (Geos (Seg (Se C2 B)) add Emp)
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B C2)) add Emp)
[PROOF STEP]
have P38 : "Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se C2 B)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se A B)) add Emp)
Eq (Geos (Seg (Se B C2)) add Emp) (Geos (Seg (Se C2 B)) add Emp)
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B C2)) add Emp)

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

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
have P39 : "Eq (Geos (Seg (Se C2 D)) add Emp) (Geos (Seg (Se D C2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Seg (Se C2 D)) add Emp) (Geos (Seg (Se D C2)) add Emp)
[PROOF STEP]
by (simp add:Seg_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se C2 D)) add Emp) (Geos (Seg (Se D C2)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P11 P39
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se C2 D)) add Emp) (Geos (Seg (Se D A)) add Emp) \<and> Bet_Point (Se C2 A) D
Eq (Geos (Seg (Se C2 D)) add Emp) (Geos (Seg (Se D C2)) add Emp)
[PROOF STEP]
have P40 : "Eq (Geos (Seg (Se D A)) add Emp) (Geos (Seg (Se D C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se C2 D)) add Emp) (Geos (Seg (Se D A)) add Emp) \<and> Bet_Point (Se C2 A) D
Eq (Geos (Seg (Se C2 D)) add Emp) (Geos (Seg (Se D C2)) add Emp)

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

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P25 P34 P38 P40
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B D))
Def (Tri (Tr C2 B D))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se C2 B)) add Emp)
Eq (Geos (Seg (Se D A)) add Emp) (Geos (Seg (Se D C2)) add Emp)
[PROOF STEP]
have "Cong (Geos (Tri (Tr A B D)) add Emp) (Geos (Tri (Tr C2 B D)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B D))
Def (Tri (Tr C2 B D))
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se C2 B)) add Emp)
Eq (Geos (Seg (Se D A)) add Emp) (Geos (Seg (Se D C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A B D)) add Emp) (Geos (Tri (Tr C2 B D)) add Emp)
[PROOF STEP]
by (simp add:Tri_SSS)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Tri (Tr A B D)) add Emp) (Geos (Tri (Tr C2 B D)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Tri (Tr A B D)) add Emp) (Geos (Tri (Tr C2 B D)) add Emp)
[PROOF STEP]
have P41 : "Cong (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An D B C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Tri (Tr A B D)) add Emp) (Geos (Tri (Tr C2 B D)) add Emp)

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

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
have P42 : "Eq (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An A B D)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An A B D)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An A B D)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P41 P42
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An D B C2)) add Emp)
Eq (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An A B D)) add Emp)
[PROOF STEP]
have P43 : "Cong (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An D B C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An D B C2)) add Emp)
Eq (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An A B D)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An D B 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 D)) add Emp) (Geos (Ang (An D B C2)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P34
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr C2 B D))
[PROOF STEP]
have P44 : "Def (Ang (An D B C2))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr C2 B D))

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

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
have P45 : "Line_on (Li B D) D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B D) D
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B D) D

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
have P46 : "\<not> Bet_Point (Se D D) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se D D) B
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se D D) B

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P33
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi C2) add Emp) (Geos (Poi B) add Emp)
[PROOF STEP]
have P47 : "\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi C2) add Emp) (Geos (Poi B) add Emp)

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

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P3 P6 P47
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
Line_on (Li B C) C2
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C2) add Emp)
[PROOF STEP]
have P48 : "Line_on (Li B C2) C"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
Line_on (Li B C) C2
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C2) add Emp)

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

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P34
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr C2 B D))
[PROOF STEP]
have P49 : "\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr C2 B D))

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

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P3 P5 P44 P45 P46 P48 P49
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B C2)) add Emp) \<and> \<not> Bet_Point (Se C2 C) B \<and> Line_on (Li B C) C2 \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C2) add Emp)
Def (Ang (An D B C2))
Line_on (Li B D) D
\<not> Bet_Point (Se D D) B
Line_on (Li B C2) C
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
[PROOF STEP]
have P50 : "Eq (Geos (Ang (An D B C2)) add Emp) (Geos (Ang (An D B C)) add Emp)
    \<and> Def (Ang (An D B C))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B C2)) add Emp) \<and> \<not> Bet_Point (Se C2 C) B \<and> Line_on (Li B C) C2 \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C2) add Emp)
Def (Ang (An D B C2))
Line_on (Li B D) D
\<not> Bet_Point (Se D D) B
Line_on (Li B C2) C
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)

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

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P43 P50
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An D B C2)) add Emp)
Eq (Geos (Ang (An D B C2)) add Emp) (Geos (Ang (An D B C)) add Emp) \<and> Def (Ang (An D B C))
[PROOF STEP]
have P51 : "Cong (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An D B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An D B C2)) add Emp)
Eq (Geos (Ang (An D B C2)) add Emp) (Geos (Ang (An D B C)) add Emp) \<and> Def (Ang (An D B C))

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

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P25
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B D))
[PROOF STEP]
have P52 : "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 (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P26
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An B A C2))
[PROOF STEP]
have P53 : "Def (Ang (An A B C2))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An B A C2))

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

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C2))
[PROOF STEP]
have P54 : "\<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C2))

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

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P16
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se C2 A) D
[PROOF STEP]
have P55 : "Bet_Point (Se A C2) D"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se C2 A) D

goal (1 subgoal):
 1. Bet_Point (Se A C2) D
[PROOF STEP]
by (simp add:Bet_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A C2) D

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P4 P5 P54 P55
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B C2)) add Emp) \<and> \<not> Bet_Point (Se C2 C) B \<and> Line_on (Li B C) C2 \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C2) add Emp)
\<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C2)) add Emp)
Bet_Point (Se A C2) D
[PROOF STEP]
have P56 : "Ang_inside (An A B C2) D"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B C2)) add Emp) \<and> \<not> Bet_Point (Se C2 C) B \<and> Line_on (Li B C) C2 \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C2) add Emp)
\<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C2)) add Emp)
Bet_Point (Se A C2) D

goal (1 subgoal):
 1. Ang_inside (An A B C2) D
[PROOF STEP]
by (simp add:Ang_inside_Bet_Point)
[PROOF STATE]
proof (state)
this:
Ang_inside (An A B C2) D

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
have P57 : "\<not> Bet_Point (Se A A) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se A A) B
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se A A) B

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P3 P4 P5 P6 P19 P53 P56 P57
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B C2)) add Emp) \<and> \<not> Bet_Point (Se C2 C) B \<and> Line_on (Li B C) C2 \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C2) add Emp)
Line_on (Li B C) C2
Line_on (Li B A) A
Def (Ang (An A B C2))
Ang_inside (An A B C2) D
\<not> Bet_Point (Se A A) B
[PROOF STEP]
have P58 : "Ang_inside (An A B C) D"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)
Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B C2)) add Emp) \<and> \<not> Bet_Point (Se C2 C) B \<and> Line_on (Li B C) C2 \<and> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C2) add Emp)
Line_on (Li B C) C2
Line_on (Li B A) A
Def (Ang (An A B C2))
Ang_inside (An A B C2) D
\<not> Bet_Point (Se A A) B

goal (1 subgoal):
 1. Ang_inside (An A B C) D
[PROOF STEP]
by (simp add:Ang_inside_trans)
[PROOF STATE]
proof (state)
this:
Ang_inside (An A B C) D

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
from P50 P51 P52 P58
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An D B C2)) add Emp) (Geos (Ang (An D B C)) add Emp) \<and> Def (Ang (An D B C))
Cong (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An D B C)) add Emp)
Def (Ang (An A B D))
Ang_inside (An A B C) D
[PROOF STEP]
show "\<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp)
    \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An D B C2)) add Emp) (Geos (Ang (An D B C)) add Emp) \<and> Def (Ang (An D B C))
Cong (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An D B C)) add Emp)
Def (Ang (An A B D))
Ang_inside (An A B C) D

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>p. Cong (Geos (Ang (An A B p)) add Emp) (Geos (Ang (An p B C)) add Emp) \<and> Ang_inside (An A B C) p \<and> Def (Ang (An A B p)) \<and> Def (Ang (An p B C))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proper_implies_part: "PP x y \<Longrightarrow> P x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PP x y \<Longrightarrow> P x y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. PP x y \<Longrightarrow> P x y
[PROOF STEP]
assume "PP x y"
[PROOF STATE]
proof (state)
this:
PP x y

goal (1 subgoal):
 1. PP x y \<Longrightarrow> P x y
[PROOF STEP]
with nip_eq
[PROOF STATE]
proof (chain)
picking this:
PP ?x ?y = (P ?x ?y \<and> ?x \<noteq> ?y)
PP x y
[PROOF STEP]
have "P x y \<and> x \<noteq> y"
[PROOF STATE]
proof (prove)
using this:
PP ?x ?y = (P ?x ?y \<and> ?x \<noteq> ?y)
PP x y

goal (1 subgoal):
 1. P x y \<and> x \<noteq> y
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
P x y \<and> x \<noteq> y

goal (1 subgoal):
 1. PP x y \<Longrightarrow> P x y
[PROOF STEP]
thus "P x y"
[PROOF STATE]
proof (prove)
using this:
P x y \<and> x \<noteq> y

goal (1 subgoal):
 1. P x y
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
P x y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proper_implies_distinct: "PP x y \<Longrightarrow> x \<noteq> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PP x y \<Longrightarrow> x \<noteq> y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. PP x y \<Longrightarrow> x \<noteq> y
[PROOF STEP]
assume "PP x y"
[PROOF STATE]
proof (state)
this:
PP x y

goal (1 subgoal):
 1. PP x y \<Longrightarrow> x \<noteq> y
[PROOF STEP]
with nip_eq
[PROOF STATE]
proof (chain)
picking this:
PP ?x ?y = (P ?x ?y \<and> ?x \<noteq> ?y)
PP x y
[PROOF STEP]
have "P x y \<and> x \<noteq> y"
[PROOF STATE]
proof (prove)
using this:
PP ?x ?y = (P ?x ?y \<and> ?x \<noteq> ?y)
PP x y

goal (1 subgoal):
 1. P x y \<and> x \<noteq> y
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
P x y \<and> x \<noteq> y

goal (1 subgoal):
 1. PP x y \<Longrightarrow> x \<noteq> y
[PROOF STEP]
thus "x \<noteq> y"
[PROOF STATE]
proof (prove)
using this:
P x y \<and> x \<noteq> y

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proper_implies_not_part: "PP x y \<Longrightarrow> \<not> P y x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PP x y \<Longrightarrow> \<not> P y x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. PP x y \<Longrightarrow> \<not> P y x
[PROOF STEP]
assume "PP x y"
[PROOF STATE]
proof (state)
this:
PP x y

goal (1 subgoal):
 1. PP x y \<Longrightarrow> \<not> P y x
[PROOF STEP]
hence "P x y"
[PROOF STATE]
proof (prove)
using this:
PP x y

goal (1 subgoal):
 1. P x y
[PROOF STEP]
by (rule proper_implies_part)
[PROOF STATE]
proof (state)
this:
P x y

goal (1 subgoal):
 1. PP x y \<Longrightarrow> \<not> P y x
[PROOF STEP]
show "\<not> P y x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> P y x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P y x \<Longrightarrow> False
[PROOF STEP]
from \<open>PP x y\<close>
[PROOF STATE]
proof (chain)
picking this:
PP x y
[PROOF STEP]
have "x \<noteq> y"
[PROOF STATE]
proof (prove)
using this:
PP x y

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
by (rule proper_implies_distinct)
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal (1 subgoal):
 1. P y x \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal (1 subgoal):
 1. P y x \<Longrightarrow> False
[PROOF STEP]
assume "P y x"
[PROOF STATE]
proof (state)
this:
P y x

goal (1 subgoal):
 1. P y x \<Longrightarrow> False
[PROOF STEP]
with \<open>P x y\<close>
[PROOF STATE]
proof (chain)
picking this:
P x y
P y x
[PROOF STEP]
have "x = y"
[PROOF STATE]
proof (prove)
using this:
P x y
P y x

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by (rule part_antisymmetry)
[PROOF STATE]
proof (state)
this:
x = y

goal (1 subgoal):
 1. P y x \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> y
x = y
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
x = y

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> P y x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proper_part_asymmetry: "PP x y \<Longrightarrow> \<not> PP y x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PP x y \<Longrightarrow> \<not> PP y x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. PP x y \<Longrightarrow> \<not> PP y x
[PROOF STEP]
assume "PP x y"
[PROOF STATE]
proof (state)
this:
PP x y

goal (1 subgoal):
 1. PP x y \<Longrightarrow> \<not> PP y x
[PROOF STEP]
hence "P x y"
[PROOF STATE]
proof (prove)
using this:
PP x y

goal (1 subgoal):
 1. P x y
[PROOF STEP]
by (rule proper_implies_part)
[PROOF STATE]
proof (state)
this:
P x y

goal (1 subgoal):
 1. PP x y \<Longrightarrow> \<not> PP y x
[PROOF STEP]
from \<open>PP x y\<close>
[PROOF STATE]
proof (chain)
picking this:
PP x y
[PROOF STEP]
have "x \<noteq> y"
[PROOF STATE]
proof (prove)
using this:
PP x y

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
by (rule proper_implies_distinct)
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal (1 subgoal):
 1. PP x y \<Longrightarrow> \<not> PP y x
[PROOF STEP]
show "\<not> PP y x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> PP y x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. PP y x \<Longrightarrow> False
[PROOF STEP]
assume "PP y x"
[PROOF STATE]
proof (state)
this:
PP y x

goal (1 subgoal):
 1. PP y x \<Longrightarrow> False
[PROOF STEP]
hence "P y x"
[PROOF STATE]
proof (prove)
using this:
PP y x

goal (1 subgoal):
 1. P y x
[PROOF STEP]
by (rule proper_implies_part)
[PROOF STATE]
proof (state)
this:
P y x

goal (1 subgoal):
 1. PP y x \<Longrightarrow> False
[PROOF STEP]
with \<open>P x y\<close>
[PROOF STATE]
proof (chain)
picking this:
P x y
P y x
[PROOF STEP]
have "x = y"
[PROOF STATE]
proof (prove)
using this:
P x y
P y x

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by (rule part_antisymmetry)
[PROOF STATE]
proof (state)
this:
x = y

goal (1 subgoal):
 1. PP y x \<Longrightarrow> False
[PROOF STEP]
with \<open>x \<noteq> y\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> y
x = y
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
x = y

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> PP y x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proper_implies_overlap: "PP x y \<Longrightarrow> O x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PP x y \<Longrightarrow> O x y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. PP x y \<Longrightarrow> O x y
[PROOF STEP]
assume "PP x y"
[PROOF STATE]
proof (state)
this:
PP x y

goal (1 subgoal):
 1. PP x y \<Longrightarrow> O x y
[PROOF STEP]
hence "P x y"
[PROOF STATE]
proof (prove)
using this:
PP x y

goal (1 subgoal):
 1. P x y
[PROOF STEP]
by (rule proper_implies_part)
[PROOF STATE]
proof (state)
this:
P x y

goal (1 subgoal):
 1. PP x y \<Longrightarrow> O x y
[PROOF STEP]
thus "O x y"
[PROOF STATE]
proof (prove)
using this:
P x y

goal (1 subgoal):
 1. O x y
[PROOF STEP]
by (rule part_implies_overlap)
[PROOF STATE]
proof (state)
this:
O x y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proper_part_irreflexivity: "\<not> PP x x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> PP x x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. PP x x \<Longrightarrow> False
[PROOF STEP]
assume "PP x x"
[PROOF STATE]
proof (state)
this:
PP x x

goal (1 subgoal):
 1. PP x x \<Longrightarrow> False
[PROOF STEP]
hence "\<not> PP x x"
[PROOF STATE]
proof (prove)
using this:
PP x x

goal (1 subgoal):
 1. \<not> PP x x
[PROOF STEP]
by (rule proper_part_asymmetry)
[PROOF STATE]
proof (state)
this:
\<not> PP x x

goal (1 subgoal):
 1. PP x x \<Longrightarrow> False
[PROOF STEP]
thus "False"
[PROOF STATE]
proof (prove)
using this:
\<not> PP x x

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>PP x x\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> PP x x
PP x x

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma splits_at_combine: "splits_at \<delta> i \<alpha> N \<beta> \<Longrightarrow> \<delta> = \<alpha> @ [N] @ \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. splits_at \<delta> i \<alpha> N \<beta> \<Longrightarrow> \<delta> = \<alpha> @ [N] @ \<beta>
[PROOF STEP]
by (simp add: id_take_nth_drop splits_at_def)


[STATEMENT]
lemma splits_at_combine_dest: "Derives1 a i r b \<Longrightarrow> splits_at a i \<alpha> N \<beta> \<Longrightarrow> b = \<alpha> @ (snd r) @ \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Derives1 a i r b; splits_at a i \<alpha> N \<beta>\<rbrakk> \<Longrightarrow> b = \<alpha> @ snd r @ \<beta>
[PROOF STEP]
by (metis (no_types, lifting) Derives1_drop Derives1_split append_assoc append_eq_conv_conj
      length_append splits_at_def)


[STATEMENT]
lemma Derives1_nonterminal:
  assumes "Derives1 a i r b"
  assumes "splits_at a i \<alpha> N \<beta>"
  shows "fst r = N \<and> is_nonterminal N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst r = N \<and> is_nonterminal N
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fst r = N \<and> is_nonterminal N
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Derives1 a i r b
splits_at a i \<alpha> N \<beta>
[PROOF STEP]
have fst: "fst r = N"
[PROOF STATE]
proof (prove)
using this:
Derives1 a i r b
splits_at a i \<alpha> N \<beta>

goal (1 subgoal):
 1. fst r = N
[PROOF STEP]
by (metis Derives1_split append_Cons nth_append_length splits_at_def)
[PROOF STATE]
proof (state)
this:
fst r = N

goal (1 subgoal):
 1. fst r = N \<and> is_nonterminal N
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst r = N
[PROOF STEP]
have "is_nonterminal N"
[PROOF STATE]
proof (prove)
using this:
fst r = N

goal (1 subgoal):
 1. is_nonterminal N
[PROOF STEP]
by (metis Derives1_def assms(1) prod.collapse rule_nonterminal_type)
[PROOF STATE]
proof (state)
this:
is_nonterminal N

goal (1 subgoal):
 1. fst r = N \<and> is_nonterminal N
[PROOF STEP]
with fst
[PROOF STATE]
proof (chain)
picking this:
fst r = N
is_nonterminal N
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fst r = N
is_nonterminal N

goal (1 subgoal):
 1. fst r = N \<and> is_nonterminal N
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst r = N \<and> is_nonterminal N

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma splits_at_ex: "Derives1 \<delta> i r s \<Longrightarrow> \<exists> \<alpha> N \<beta>. splits_at \<delta> i \<alpha> N \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Derives1 \<delta> i r s \<Longrightarrow> \<exists>\<alpha> N \<beta>. splits_at \<delta> i \<alpha> N \<beta>
[PROOF STEP]
by (simp add: Derives1_bound splits_at_def)


[STATEMENT]
lemma splits_at_\<alpha>: "Derives1 \<delta> i r s \<Longrightarrow> splits_at \<delta> i \<alpha> N \<beta> \<Longrightarrow>
  \<alpha> = take i \<delta> \<and> \<alpha> = take i s \<and> length \<alpha> = i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Derives1 \<delta> i r s; splits_at \<delta> i \<alpha> N \<beta>\<rbrakk> \<Longrightarrow> \<alpha> = take i \<delta> \<and> \<alpha> = take i s \<and> length \<alpha> = i
[PROOF STEP]
by (metis Derives1_split append_eq_conv_conj splits_at_def)


[STATEMENT]
lemma LeftDerives1_splits_at_is_word: "LeftDerives1 \<delta> i r s \<Longrightarrow> splits_at \<delta> i \<alpha> N \<beta> \<Longrightarrow> is_word \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>LeftDerives1 \<delta> i r s; splits_at \<delta> i \<alpha> N \<beta>\<rbrakk> \<Longrightarrow> is_word \<alpha>
[PROOF STEP]
by (metis LeftDerives1_def leftmost_def splits_at_def)


[STATEMENT]
lemma splits_at_\<beta>: "Derives1 \<delta> i r s \<Longrightarrow> splits_at \<delta> i \<alpha> N \<beta> \<Longrightarrow>
  \<beta> = drop (Suc i) \<delta> \<and> \<beta> = drop (i + length (snd r)) s \<and> length \<beta> = length \<delta> - i - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Derives1 \<delta> i r s; splits_at \<delta> i \<alpha> N \<beta>\<rbrakk> \<Longrightarrow> \<beta> = drop (Suc i) \<delta> \<and> \<beta> = drop (i + length (snd r)) s \<and> length \<beta> = length \<delta> - i - 1
[PROOF STEP]
by (metis Derives1_drop Suc_eq_plus1 diff_diff_left length_drop splits_at_def)


[STATEMENT]
lemma Derives1_prefix:
  assumes ab: "Derives1 \<delta> i r (a@b)"
  assumes split: "splits_at \<delta> i \<alpha> N \<beta>"
  shows "is_prefix \<alpha> a \<or> is_prefix a \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_prefix \<alpha> a \<or> is_prefix a \<alpha>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_prefix \<alpha> a \<or> is_prefix a \<alpha>
[PROOF STEP]
have take: "\<alpha> = take i (a@b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> = take i (a @ b)
[PROOF STEP]
using ab split splits_at_\<alpha>
[PROOF STATE]
proof (prove)
using this:
Derives1 \<delta> i r (a @ b)
splits_at \<delta> i \<alpha> N \<beta>
\<lbrakk>Derives1 ?\<delta> ?i ?r ?s; splits_at ?\<delta> ?i ?\<alpha> ?N ?\<beta>\<rbrakk> \<Longrightarrow> ?\<alpha> = take ?i ?\<delta> \<and> ?\<alpha> = take ?i ?s \<and> length ?\<alpha> = ?i

goal (1 subgoal):
 1. \<alpha> = take i (a @ b)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<alpha> = take i (a @ b)

goal (1 subgoal):
 1. is_prefix \<alpha> a \<or> is_prefix a \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_prefix \<alpha> a \<or> is_prefix a \<alpha>
[PROOF STEP]
proof (cases "i \<le> length a")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i \<le> length a \<Longrightarrow> is_prefix \<alpha> a \<or> is_prefix a \<alpha>
 2. \<not> i \<le> length a \<Longrightarrow> is_prefix \<alpha> a \<or> is_prefix a \<alpha>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i \<le> length a

goal (2 subgoals):
 1. i \<le> length a \<Longrightarrow> is_prefix \<alpha> a \<or> is_prefix a \<alpha>
 2. \<not> i \<le> length a \<Longrightarrow> is_prefix \<alpha> a \<or> is_prefix a \<alpha>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<le> length a
[PROOF STEP]
have "\<alpha> = take i a"
[PROOF STATE]
proof (prove)
using this:
i \<le> length a

goal (1 subgoal):
 1. \<alpha> = take i a
[PROOF STEP]
by (simp add: take)
[PROOF STATE]
proof (state)
this:
\<alpha> = take i a

goal (2 subgoals):
 1. i \<le> length a \<Longrightarrow> is_prefix \<alpha> a \<or> is_prefix a \<alpha>
 2. \<not> i \<le> length a \<Longrightarrow> is_prefix \<alpha> a \<or> is_prefix a \<alpha>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<alpha> = take i a
[PROOF STEP]
have "is_prefix \<alpha> a"
[PROOF STATE]
proof (prove)
using this:
\<alpha> = take i a

goal (1 subgoal):
 1. is_prefix \<alpha> a
[PROOF STEP]
by (metis append_take_drop_id is_prefix_def)
[PROOF STATE]
proof (state)
this:
is_prefix \<alpha> a

goal (2 subgoals):
 1. i \<le> length a \<Longrightarrow> is_prefix \<alpha> a \<or> is_prefix a \<alpha>
 2. \<not> i \<le> length a \<Longrightarrow> is_prefix \<alpha> a \<or> is_prefix a \<alpha>
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
i \<le> length a
is_prefix \<alpha> a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<le> length a
is_prefix \<alpha> a

goal (1 subgoal):
 1. is_prefix \<alpha> a \<or> is_prefix a \<alpha>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_prefix \<alpha> a \<or> is_prefix a \<alpha>

goal (1 subgoal):
 1. \<not> i \<le> length a \<Longrightarrow> is_prefix \<alpha> a \<or> is_prefix a \<alpha>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> i \<le> length a \<Longrightarrow> is_prefix \<alpha> a \<or> is_prefix a \<alpha>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> i \<le> length a

goal (1 subgoal):
 1. \<not> i \<le> length a \<Longrightarrow> is_prefix \<alpha> a \<or> is_prefix a \<alpha>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> i \<le> length a
[PROOF STEP]
have "is_prefix a \<alpha>"
[PROOF STATE]
proof (prove)
using this:
\<not> i \<le> length a

goal (1 subgoal):
 1. is_prefix a \<alpha>
[PROOF STEP]
by (simp add: is_prefix_def nat_le_linear take)
[PROOF STATE]
proof (state)
this:
is_prefix a \<alpha>

goal (1 subgoal):
 1. \<not> i \<le> length a \<Longrightarrow> is_prefix \<alpha> a \<or> is_prefix a \<alpha>
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
\<not> i \<le> length a
is_prefix a \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> i \<le> length a
is_prefix a \<alpha>

goal (1 subgoal):
 1. is_prefix \<alpha> a \<or> is_prefix a \<alpha>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_prefix \<alpha> a \<or> is_prefix a \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_prefix \<alpha> a \<or> is_prefix a \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Derives1_suffix:
  assumes ab: "Derives1 \<delta> i r (a@b)"
  assumes split: "splits_at \<delta> i \<alpha> N \<beta>"
  shows "is_suffix \<beta> b \<or> is_suffix b \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_suffix \<beta> b \<or> is_suffix b \<beta>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_suffix \<beta> b \<or> is_suffix b \<beta>
[PROOF STEP]
have drop1: "\<beta> = drop (i + length (snd r)) (a@b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<beta> = drop (i + length (snd r)) (a @ b)
[PROOF STEP]
using ab split splits_at_\<beta>
[PROOF STATE]
proof (prove)
using this:
Derives1 \<delta> i r (a @ b)
splits_at \<delta> i \<alpha> N \<beta>
\<lbrakk>Derives1 ?\<delta> ?i ?r ?s; splits_at ?\<delta> ?i ?\<alpha> ?N ?\<beta>\<rbrakk> \<Longrightarrow> ?\<beta> = drop (Suc ?i) ?\<delta> \<and> ?\<beta> = drop (?i + length (snd ?r)) ?s \<and> length ?\<beta> = length ?\<delta> - ?i - 1

goal (1 subgoal):
 1. \<beta> = drop (i + length (snd r)) (a @ b)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<beta> = drop (i + length (snd r)) (a @ b)

goal (1 subgoal):
 1. is_suffix \<beta> b \<or> is_suffix b \<beta>
[PROOF STEP]
have drop2: "b = drop (length a) (a@b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b = drop (length a) (a @ b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b = drop (length a) (a @ b)

goal (1 subgoal):
 1. is_suffix \<beta> b \<or> is_suffix b \<beta>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_suffix \<beta> b \<or> is_suffix b \<beta>
[PROOF STEP]
proof (cases "(i + length (snd r)) \<le> length a")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i + length (snd r) \<le> length a \<Longrightarrow> is_suffix \<beta> b \<or> is_suffix b \<beta>
 2. \<not> i + length (snd r) \<le> length a \<Longrightarrow> is_suffix \<beta> b \<or> is_suffix b \<beta>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i + length (snd r) \<le> length a

goal (2 subgoals):
 1. i + length (snd r) \<le> length a \<Longrightarrow> is_suffix \<beta> b \<or> is_suffix b \<beta>
 2. \<not> i + length (snd r) \<le> length a \<Longrightarrow> is_suffix \<beta> b \<or> is_suffix b \<beta>
[PROOF STEP]
with drop1 drop2
[PROOF STATE]
proof (chain)
picking this:
\<beta> = drop (i + length (snd r)) (a @ b)
b = drop (length a) (a @ b)
i + length (snd r) \<le> length a
[PROOF STEP]
have "is_suffix b \<beta>"
[PROOF STATE]
proof (prove)
using this:
\<beta> = drop (i + length (snd r)) (a @ b)
b = drop (length a) (a @ b)
i + length (snd r) \<le> length a

goal (1 subgoal):
 1. is_suffix b \<beta>
[PROOF STEP]
by (simp add: is_suffix_def)
[PROOF STATE]
proof (state)
this:
is_suffix b \<beta>

goal (2 subgoals):
 1. i + length (snd r) \<le> length a \<Longrightarrow> is_suffix \<beta> b \<or> is_suffix b \<beta>
 2. \<not> i + length (snd r) \<le> length a \<Longrightarrow> is_suffix \<beta> b \<or> is_suffix b \<beta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_suffix b \<beta>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_suffix b \<beta>

goal (1 subgoal):
 1. is_suffix \<beta> b \<or> is_suffix b \<beta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_suffix \<beta> b \<or> is_suffix b \<beta>

goal (1 subgoal):
 1. \<not> i + length (snd r) \<le> length a \<Longrightarrow> is_suffix \<beta> b \<or> is_suffix b \<beta>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> i + length (snd r) \<le> length a \<Longrightarrow> is_suffix \<beta> b \<or> is_suffix b \<beta>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> i + length (snd r) \<le> length a

goal (1 subgoal):
 1. \<not> i + length (snd r) \<le> length a \<Longrightarrow> is_suffix \<beta> b \<or> is_suffix b \<beta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> i + length (snd r) \<le> length a
[PROOF STEP]
have "length a \<le> (i + length (snd r))"
[PROOF STATE]
proof (prove)
using this:
\<not> i + length (snd r) \<le> length a

goal (1 subgoal):
 1. length a \<le> i + length (snd r)
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
length a \<le> i + length (snd r)

goal (1 subgoal):
 1. \<not> i + length (snd r) \<le> length a \<Longrightarrow> is_suffix \<beta> b \<or> is_suffix b \<beta>
[PROOF STEP]
with drop1 drop2
[PROOF STATE]
proof (chain)
picking this:
\<beta> = drop (i + length (snd r)) (a @ b)
b = drop (length a) (a @ b)
length a \<le> i + length (snd r)
[PROOF STEP]
have "is_suffix \<beta> b"
[PROOF STATE]
proof (prove)
using this:
\<beta> = drop (i + length (snd r)) (a @ b)
b = drop (length a) (a @ b)
length a \<le> i + length (snd r)

goal (1 subgoal):
 1. is_suffix \<beta> b
[PROOF STEP]
by (metis append_Nil append_take_drop_id drop_append drop_eq_Nil is_suffix_def)
[PROOF STATE]
proof (state)
this:
is_suffix \<beta> b

goal (1 subgoal):
 1. \<not> i + length (snd r) \<le> length a \<Longrightarrow> is_suffix \<beta> b \<or> is_suffix b \<beta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_suffix \<beta> b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_suffix \<beta> b

goal (1 subgoal):
 1. is_suffix \<beta> b \<or> is_suffix b \<beta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_suffix \<beta> b \<or> is_suffix b \<beta>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_suffix \<beta> b \<or> is_suffix b \<beta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Derives1_skip_prefix:
  "length a \<le> i \<Longrightarrow> Derives1 (a@b) i r (a@c) \<Longrightarrow> Derives1 b (i - length a) r c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length a \<le> i; Derives1 (a @ b) i r (a @ c)\<rbrakk> \<Longrightarrow> Derives1 b (i - length a) r c
[PROOF STEP]
apply (auto simp add: Derives1_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y N \<alpha>. \<lbrakk>length a \<le> length x; a @ b = x @ N # y; a @ c = x @ \<alpha> @ y; is_sentence x; is_sentence y; (N, \<alpha>) \<in> \<RR>; i = length x; r = (N, \<alpha>)\<rbrakk> \<Longrightarrow> \<exists>xa y. b = xa @ N # y \<and> c = xa @ \<alpha> @ y \<and> is_sentence xa \<and> is_sentence y \<and> length x - length a = length xa
[PROOF STEP]
by (metis append_eq_append_conv_if is_sentence_concat is_sentence_cons is_symbol_def
    length_drop rule_nonterminal_type)


[STATEMENT]
lemma cancel_suffix:
  assumes "a @ c = b @ d"
  assumes "length c \<le> length d"
  shows "a = b @ (take (length d - length c) d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = b @ take (length d - length c) d
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a = b @ take (length d - length c) d
[PROOF STEP]
have "a @ c = (b @ take (length d - length c) d) @ drop (length d - length c) d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a @ c = (b @ take (length d - length c) d) @ drop (length d - length c) d
[PROOF STEP]
by (metis append_assoc append_take_drop_id assms(1))
[PROOF STATE]
proof (state)
this:
a @ c = (b @ take (length d - length c) d) @ drop (length d - length c) d

goal (1 subgoal):
 1. a = b @ take (length d - length c) d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a @ c = (b @ take (length d - length c) d) @ drop (length d - length c) d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a @ c = (b @ take (length d - length c) d) @ drop (length d - length c) d

goal (1 subgoal):
 1. a = b @ take (length d - length c) d
[PROOF STEP]
by (metis append_eq_append_conv assms(2) diff_diff_cancel length_drop)
[PROOF STATE]
proof (state)
this:
a = b @ take (length d - length c) d

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_sentence_take:
  "is_sentence y \<Longrightarrow> is_sentence (take n y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_sentence y \<Longrightarrow> is_sentence (take n y)
[PROOF STEP]
by (metis append_take_drop_id is_sentence_concat)


[STATEMENT]
lemma Derives1_skip_suffix:
  assumes i: "i < length a"
  assumes D: "Derives1 (a@c) i r (b@c)"
  shows "Derives1 a i r b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Derives1 a i r b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Derives1 a i r b
[PROOF STEP]
note Derives1_def[where u="a@c" and v="b@c" and i=i and r=r]
[PROOF STATE]
proof (state)
this:
Derives1 (a @ c) i r (b @ c) = (\<exists>x y N \<alpha>. a @ c = x @ [N] @ y \<and> b @ c = x @ \<alpha> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>) \<in> \<RR> \<and> r = (N, \<alpha>) \<and> i = length x)

goal (1 subgoal):
 1. Derives1 a i r b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Derives1 (a @ c) i r (b @ c) = (\<exists>x y N \<alpha>. a @ c = x @ [N] @ y \<and> b @ c = x @ \<alpha> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>) \<in> \<RR> \<and> r = (N, \<alpha>) \<and> i = length x)
[PROOF STEP]
have "\<exists>x y N \<alpha>.
    a @ c = x @ [N] @ y \<and>
    b @ c = x @ \<alpha> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>) \<in> \<RR> \<and> r = (N, \<alpha>) \<and> i = length x"
[PROOF STATE]
proof (prove)
using this:
Derives1 (a @ c) i r (b @ c) = (\<exists>x y N \<alpha>. a @ c = x @ [N] @ y \<and> b @ c = x @ \<alpha> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>) \<in> \<RR> \<and> r = (N, \<alpha>) \<and> i = length x)

goal (1 subgoal):
 1. \<exists>x y N \<alpha>. a @ c = x @ [N] @ y \<and> b @ c = x @ \<alpha> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>) \<in> \<RR> \<and> r = (N, \<alpha>) \<and> i = length x
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
Derives1 (a @ c) i r (b @ c) = (\<exists>x y N \<alpha>. a @ c = x @ [N] @ y \<and> b @ c = x @ \<alpha> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>) \<in> \<RR> \<and> r = (N, \<alpha>) \<and> i = length x)
Derives1 (a @ c) i r (b @ c)

goal (1 subgoal):
 1. \<exists>x y N \<alpha>. a @ c = x @ [N] @ y \<and> b @ c = x @ \<alpha> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>) \<in> \<RR> \<and> r = (N, \<alpha>) \<and> i = length x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>x y N \<alpha>. a @ c = x @ [N] @ y \<and> b @ c = x @ \<alpha> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>) \<in> \<RR> \<and> r = (N, \<alpha>) \<and> i = length x

goal (1 subgoal):
 1. Derives1 a i r b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x y N \<alpha>. a @ c = x @ [N] @ y \<and> b @ c = x @ \<alpha> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>) \<in> \<RR> \<and> r = (N, \<alpha>) \<and> i = length x
[PROOF STEP]
obtain x y N \<alpha> where split:
    "a @ c = x @ [N] @ y \<and>
     b @ c = x @ \<alpha> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>) \<in> \<RR> \<and> r = (N, \<alpha>) \<and> i = length x"
[PROOF STATE]
proof (prove)
using this:
\<exists>x y N \<alpha>. a @ c = x @ [N] @ y \<and> b @ c = x @ \<alpha> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>) \<in> \<RR> \<and> r = (N, \<alpha>) \<and> i = length x

goal (1 subgoal):
 1. (\<And>x N y \<alpha>. a @ c = x @ [N] @ y \<and> b @ c = x @ \<alpha> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>) \<in> \<RR> \<and> r = (N, \<alpha>) \<and> i = length x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a @ c = x @ [N] @ y \<and> b @ c = x @ \<alpha> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>) \<in> \<RR> \<and> r = (N, \<alpha>) \<and> i = length x

goal (1 subgoal):
 1. Derives1 a i r b
[PROOF STEP]
from split
[PROOF STATE]
proof (chain)
picking this:
a @ c = x @ [N] @ y \<and> b @ c = x @ \<alpha> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>) \<in> \<RR> \<and> r = (N, \<alpha>) \<and> i = length x
[PROOF STEP]
have "length (a@c) = length (x @ [N] @ y)"
[PROOF STATE]
proof (prove)
using this:
a @ c = x @ [N] @ y \<and> b @ c = x @ \<alpha> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>) \<in> \<RR> \<and> r = (N, \<alpha>) \<and> i = length x

goal (1 subgoal):
 1. length (a @ c) = length (x @ [N] @ y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (a @ c) = length (x @ [N] @ y)

goal (1 subgoal):
 1. Derives1 a i r b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (a @ c) = length (x @ [N] @ y)
[PROOF STEP]
have "length a + length c = length x + length y + 1"
[PROOF STATE]
proof (prove)
using this:
length (a @ c) = length (x @ [N] @ y)

goal (1 subgoal):
 1. length a + length c = length x + length y + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length a + length c = length x + length y + 1

goal (1 subgoal):
 1. Derives1 a i r b
[PROOF STEP]
with split
[PROOF STATE]
proof (chain)
picking this:
a @ c = x @ [N] @ y \<and> b @ c = x @ \<alpha> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>) \<in> \<RR> \<and> r = (N, \<alpha>) \<and> i = length x
length a + length c = length x + length y + 1
[PROOF STEP]
have "length a + length c = i + length y + 1"
[PROOF STATE]
proof (prove)
using this:
a @ c = x @ [N] @ y \<and> b @ c = x @ \<alpha> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>) \<in> \<RR> \<and> r = (N, \<alpha>) \<and> i = length x
length a + length c = length x + length y + 1

goal (1 subgoal):
 1. length a + length c = i + length y + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length a + length c = i + length y + 1

goal (1 subgoal):
 1. Derives1 a i r b
[PROOF STEP]
with i
[PROOF STATE]
proof (chain)
picking this:
i < length a
length a + length c = i + length y + 1
[PROOF STEP]
have len_c_y: "length c \<le> length y"
[PROOF STATE]
proof (prove)
using this:
i < length a
length a + length c = i + length y + 1

goal (1 subgoal):
 1. length c \<le> length y
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
length c \<le> length y

goal (1 subgoal):
 1. Derives1 a i r b
[PROOF STEP]
let ?y = "take (length y - length c) y"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Derives1 a i r b
[PROOF STEP]
from split
[PROOF STATE]
proof (chain)
picking this:
a @ c = x @ [N] @ y \<and> b @ c = x @ \<alpha> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>) \<in> \<RR> \<and> r = (N, \<alpha>) \<and> i = length x
[PROOF STEP]
have ac: "a @ c = (x @ [N]) @ y"
[PROOF STATE]
proof (prove)
using this:
a @ c = x @ [N] @ y \<and> b @ c = x @ \<alpha> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>) \<in> \<RR> \<and> r = (N, \<alpha>) \<and> i = length x

goal (1 subgoal):
 1. a @ c = (x @ [N]) @ y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a @ c = (x @ [N]) @ y

goal (1 subgoal):
 1. Derives1 a i r b
[PROOF STEP]
note cancel_suffix[where a=a and c = c and b = "x@[N]" and d = "y", OF ac len_c_y]
[PROOF STATE]
proof (state)
this:
a = (x @ [N]) @ take (length y - length c) y

goal (1 subgoal):
 1. Derives1 a i r b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = (x @ [N]) @ take (length y - length c) y
[PROOF STEP]
have a: "a = x @ [N] @ ?y"
[PROOF STATE]
proof (prove)
using this:
a = (x @ [N]) @ take (length y - length c) y

goal (1 subgoal):
 1. a = x @ [N] @ take (length y - length c) y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = x @ [N] @ take (length y - length c) y

goal (1 subgoal):
 1. Derives1 a i r b
[PROOF STEP]
from split
[PROOF STATE]
proof (chain)
picking this:
a @ c = x @ [N] @ y \<and> b @ c = x @ \<alpha> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>) \<in> \<RR> \<and> r = (N, \<alpha>) \<and> i = length x
[PROOF STEP]
have bc: "b @ c = (x @ \<alpha>) @ y"
[PROOF STATE]
proof (prove)
using this:
a @ c = x @ [N] @ y \<and> b @ c = x @ \<alpha> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>) \<in> \<RR> \<and> r = (N, \<alpha>) \<and> i = length x

goal (1 subgoal):
 1. b @ c = (x @ \<alpha>) @ y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b @ c = (x @ \<alpha>) @ y

goal (1 subgoal):
 1. Derives1 a i r b
[PROOF STEP]
note cancel_suffix[where a=b and c = c and b = "x@\<alpha>" and d = "y", OF bc len_c_y]
[PROOF STATE]
proof (state)
this:
b = (x @ \<alpha>) @ take (length y - length c) y

goal (1 subgoal):
 1. Derives1 a i r b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b = (x @ \<alpha>) @ take (length y - length c) y
[PROOF STEP]
have b: "b = x @ \<alpha> @ ?y"
[PROOF STATE]
proof (prove)
using this:
b = (x @ \<alpha>) @ take (length y - length c) y

goal (1 subgoal):
 1. b = x @ \<alpha> @ take (length y - length c) y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b = x @ \<alpha> @ take (length y - length c) y

goal (1 subgoal):
 1. Derives1 a i r b
[PROOF STEP]
from split len_c_y a b
[PROOF STATE]
proof (chain)
picking this:
a @ c = x @ [N] @ y \<and> b @ c = x @ \<alpha> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>) \<in> \<RR> \<and> r = (N, \<alpha>) \<and> i = length x
length c \<le> length y
a = x @ [N] @ take (length y - length c) y
b = x @ \<alpha> @ take (length y - length c) y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a @ c = x @ [N] @ y \<and> b @ c = x @ \<alpha> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>) \<in> \<RR> \<and> r = (N, \<alpha>) \<and> i = length x
length c \<le> length y
a = x @ [N] @ take (length y - length c) y
b = x @ \<alpha> @ take (length y - length c) y

goal (1 subgoal):
 1. Derives1 a i r b
[PROOF STEP]
apply (simp only: Derives1_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x @ [N] @ take (length y - length c) y) @ c = x @ [N] @ y \<and> (x @ \<alpha> @ take (length y - length c) y) @ c = x @ \<alpha> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>) \<in> \<RR> \<and> r = (N, \<alpha>) \<and> i = length x; length c \<le> length y; a = x @ [N] @ take (length y - length c) y; b = x @ \<alpha> @ take (length y - length c) y\<rbrakk> \<Longrightarrow> \<exists>xa ya Na \<alpha>'. x @ [N] @ take (length y - length c) y = xa @ [Na] @ ya \<and> x @ \<alpha> @ take (length y - length c) y = xa @ \<alpha>' @ ya \<and> is_sentence xa \<and> is_sentence ya \<and> (Na, \<alpha>') \<in> \<RR> \<and> (N, \<alpha>) = (Na, \<alpha>') \<and> length x = length xa
[PROOF STEP]
apply (rule_tac x=x in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x @ [N] @ take (length y - length c) y) @ c = x @ [N] @ y \<and> (x @ \<alpha> @ take (length y - length c) y) @ c = x @ \<alpha> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>) \<in> \<RR> \<and> r = (N, \<alpha>) \<and> i = length x; length c \<le> length y; a = x @ [N] @ take (length y - length c) y; b = x @ \<alpha> @ take (length y - length c) y\<rbrakk> \<Longrightarrow> \<exists>ya Na \<alpha>'. x @ [N] @ take (length y - length c) y = x @ [Na] @ ya \<and> x @ \<alpha> @ take (length y - length c) y = x @ \<alpha>' @ ya \<and> is_sentence x \<and> is_sentence ya \<and> (Na, \<alpha>') \<in> \<RR> \<and> (N, \<alpha>) = (Na, \<alpha>') \<and> length x = length x
[PROOF STEP]
apply (rule_tac x="?y" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x @ [N] @ take (length y - length c) y) @ c = x @ [N] @ y \<and> (x @ \<alpha> @ take (length y - length c) y) @ c = x @ \<alpha> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>) \<in> \<RR> \<and> r = (N, \<alpha>) \<and> i = length x; length c \<le> length y; a = x @ [N] @ take (length y - length c) y; b = x @ \<alpha> @ take (length y - length c) y\<rbrakk> \<Longrightarrow> \<exists>Na \<alpha>'. x @ [N] @ take (length y - length c) y = x @ [Na] @ take (length y - length c) y \<and> x @ \<alpha> @ take (length y - length c) y = x @ \<alpha>' @ take (length y - length c) y \<and> is_sentence x \<and> is_sentence (take (length y - length c) y) \<and> (Na, \<alpha>') \<in> \<RR> \<and> (N, \<alpha>) = (Na, \<alpha>') \<and> length x = length x
[PROOF STEP]
apply (rule_tac x="N" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x @ [N] @ take (length y - length c) y) @ c = x @ [N] @ y \<and> (x @ \<alpha> @ take (length y - length c) y) @ c = x @ \<alpha> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>) \<in> \<RR> \<and> r = (N, \<alpha>) \<and> i = length x; length c \<le> length y; a = x @ [N] @ take (length y - length c) y; b = x @ \<alpha> @ take (length y - length c) y\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. x @ [N] @ take (length y - length c) y = x @ [N] @ take (length y - length c) y \<and> x @ \<alpha> @ take (length y - length c) y = x @ \<alpha>' @ take (length y - length c) y \<and> is_sentence x \<and> is_sentence (take (length y - length c) y) \<and> (N, \<alpha>') \<in> \<RR> \<and> (N, \<alpha>) = (N, \<alpha>') \<and> length x = length x
[PROOF STEP]
apply (rule_tac x="\<alpha>" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x @ [N] @ take (length y - length c) y) @ c = x @ [N] @ y \<and> (x @ \<alpha> @ take (length y - length c) y) @ c = x @ \<alpha> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>) \<in> \<RR> \<and> r = (N, \<alpha>) \<and> i = length x; length c \<le> length y; a = x @ [N] @ take (length y - length c) y; b = x @ \<alpha> @ take (length y - length c) y\<rbrakk> \<Longrightarrow> x @ [N] @ take (length y - length c) y = x @ [N] @ take (length y - length c) y \<and> x @ \<alpha> @ take (length y - length c) y = x @ \<alpha> @ take (length y - length c) y \<and> is_sentence x \<and> is_sentence (take (length y - length c) y) \<and> (N, \<alpha>) \<in> \<RR> \<and> (N, \<alpha>) = (N, \<alpha>) \<and> length x = length x
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length c \<le> length y; a = x @ N # take (length y - length c) y; b = x @ \<alpha> @ take (length y - length c) y; take (length y - length c) y @ c = y; is_sentence x; is_sentence y; (N, \<alpha>) \<in> \<RR>; r = (N, \<alpha>); i = length x\<rbrakk> \<Longrightarrow> is_sentence (take (length y - length c) y)
[PROOF STEP]
by (rule is_sentence_take)
[PROOF STATE]
proof (state)
this:
Derives1 a i r b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma drop_cancel_suffix: "a@c = drop n (b@c) \<Longrightarrow> a = drop n b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a @ c = drop n (b @ c) \<Longrightarrow> a = drop n b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a @ c = drop n (b @ c) \<Longrightarrow> a = drop n b
[PROOF STEP]
assume a1: "a @ c = drop n (b @ c)"
[PROOF STATE]
proof (state)
this:
a @ c = drop n (b @ c)

goal (1 subgoal):
 1. a @ c = drop n (b @ c) \<Longrightarrow> a = drop n b
[PROOF STEP]
have "length (drop n b) = length b + length c - n - length c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (drop n b) = length b + length c - n - length c
[PROOF STEP]
by (metis add_diff_cancel_right' diff_commute length_drop)
[PROOF STATE]
proof (state)
this:
length (drop n b) = length b + length c - n - length c

goal (1 subgoal):
 1. a @ c = drop n (b @ c) \<Longrightarrow> a = drop n b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (drop n b) = length b + length c - n - length c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length (drop n b) = length b + length c - n - length c

goal (1 subgoal):
 1. a = drop n b
[PROOF STEP]
using a1
[PROOF STATE]
proof (prove)
using this:
length (drop n b) = length b + length c - n - length c
a @ c = drop n (b @ c)

goal (1 subgoal):
 1. a = drop n b
[PROOF STEP]
by (metis add_diff_cancel_right' append_eq_append_conv drop_append
      length_append length_drop)
[PROOF STATE]
proof (state)
this:
a = drop n b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma drop_keep_last: "u \<noteq> [] \<Longrightarrow> u = drop n (a@[X]) \<Longrightarrow> u = drop n a @ [X]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>u \<noteq> []; u = drop n (a @ [X])\<rbrakk> \<Longrightarrow> u = drop n a @ [X]
[PROOF STEP]
by (metis append_take_drop_id drop_butlast last_appendR snoc_eq_iff_butlast)