[STATEMENT]
lemma (in Congruence_Rule) Ang_inside_case :
  assumes
    "Def (Ang (An A B C))"
    "Def (Ang (An D B C))"
    "Plane_sameside (Li B C) A D"
    "\<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B D)) add Emp)"
  shows
    "Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A
    \<or> \<not> Ang_inside (An A B C) D \<and> Ang_inside (An D B C) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A \<or> \<not> Ang_inside (An A B C) D \<and> Ang_inside (An D B C) A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A \<or> \<not> Ang_inside (An A B C) D \<and> Ang_inside (An D B C) A
[PROOF STEP]
have P1 : "Ang_inside (An A B C) D \<Longrightarrow> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ang_inside (An A B C) D \<Longrightarrow> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D
[PROOF STEP]
by (simp add:Ang_inside_def)
[PROOF STATE]
proof (state)
this:
Ang_inside (An A B C) D \<Longrightarrow> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D

goal (1 subgoal):
 1. Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A \<or> \<not> Ang_inside (An A B C) D \<and> Ang_inside (An D B C) A
[PROOF STEP]
have P2 : "Ang_inside (An D B C) A \<Longrightarrow> Plane_sameside (Li B D) C A \<and> Plane_sameside (Li B C) D A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ang_inside (An D B C) A \<Longrightarrow> Plane_sameside (Li B D) C A \<and> Plane_sameside (Li B C) D A
[PROOF STEP]
by (simp add:Ang_inside_def)
[PROOF STATE]
proof (state)
this:
Ang_inside (An D B C) A \<Longrightarrow> Plane_sameside (Li B D) C A \<and> Plane_sameside (Li B C) D A

goal (1 subgoal):
 1. Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A \<or> \<not> Ang_inside (An A B C) D \<and> Ang_inside (An D B C) A
[PROOF STEP]
have P3 : "Ang_inside (An A B C) D \<Longrightarrow> Plane_diffside (Li B D) A C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ang_inside (An A B C) D \<Longrightarrow> Plane_diffside (Li B D) A C
[PROOF STEP]
by (simp add:Ang_inside_Planeside)
[PROOF STATE]
proof (state)
this:
Ang_inside (An A B C) D \<Longrightarrow> Plane_diffside (Li B D) A C

goal (1 subgoal):
 1. Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A \<or> \<not> Ang_inside (An A B C) D \<and> Ang_inside (An D B C) A
[PROOF STEP]
have "Plane_diffside (Li B D) A C \<Longrightarrow> Plane_diffside (Li B D) C A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Plane_diffside (Li B D) A C \<Longrightarrow> Plane_diffside (Li B D) C A
[PROOF STEP]
by (simp add:Plane_diffside_rev)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li B D) A C \<Longrightarrow> Plane_diffside (Li B D) C A

goal (1 subgoal):
 1. Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A \<or> \<not> Ang_inside (An A B C) D \<and> Ang_inside (An D B C) A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li B D) A C \<Longrightarrow> Plane_diffside (Li B D) C A
[PROOF STEP]
have P4 : "Plane_diffside (Li B D) A C \<Longrightarrow> \<not> Plane_sameside (Li B D) C A"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li B D) A C \<Longrightarrow> Plane_diffside (Li B D) C A

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

goal (1 subgoal):
 1. Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A \<or> \<not> Ang_inside (An A B C) D \<and> Ang_inside (An D B C) A
[PROOF STEP]
from P3 P4
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An A B C) D \<Longrightarrow> Plane_diffside (Li B D) A C
Plane_diffside (Li B D) A C \<Longrightarrow> \<not> Plane_sameside (Li B D) C A
[PROOF STEP]
have P5 : "Ang_inside (An A B C) D \<Longrightarrow> \<not> Plane_sameside (Li B D) C A"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An A B C) D \<Longrightarrow> Plane_diffside (Li B D) A C
Plane_diffside (Li B D) A C \<Longrightarrow> \<not> Plane_sameside (Li B D) C A

goal (1 subgoal):
 1. Ang_inside (An A B C) D \<Longrightarrow> \<not> Plane_sameside (Li B D) C A
[PROOF STEP]
by (simp add:Plane_diffside_rev)
[PROOF STATE]
proof (state)
this:
Ang_inside (An A B C) D \<Longrightarrow> \<not> Plane_sameside (Li B D) C A

goal (1 subgoal):
 1. Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A \<or> \<not> Ang_inside (An A B C) D \<and> Ang_inside (An D B C) A
[PROOF STEP]
from P2 P5
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An D B C) A \<Longrightarrow> Plane_sameside (Li B D) C A \<and> Plane_sameside (Li B C) D A
Ang_inside (An A B C) D \<Longrightarrow> \<not> Plane_sameside (Li B D) C A
[PROOF STEP]
have P6 : "Ang_inside (An A B C) D \<and> Ang_inside (An D B C) A \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An D B C) A \<Longrightarrow> Plane_sameside (Li B D) C A \<and> Plane_sameside (Li B C) D A
Ang_inside (An A B C) D \<Longrightarrow> \<not> Plane_sameside (Li B D) C A

goal (1 subgoal):
 1. Ang_inside (An A B C) D \<and> Ang_inside (An D B C) A \<Longrightarrow> False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Ang_inside (An A B C) D \<and> Ang_inside (An D B C) A \<Longrightarrow> False

goal (1 subgoal):
 1. Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A \<or> \<not> Ang_inside (An A B C) D \<and> Ang_inside (An D B C) A
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An D B C))
Plane_sameside (Li B C) A D
\<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B D)) add Emp)
[PROOF STEP]
have P7 : "\<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 D B C))
Plane_sameside (Li B C) A D
\<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B D)) 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 (1 subgoal):
 1. Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A \<or> \<not> Ang_inside (An A B C) D \<and> Ang_inside (An D B C) A
[PROOF STEP]
from assms P7
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An D B C))
Plane_sameside (Li B C) A D
\<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B D)) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
have P8 : "\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An D B C))
Plane_sameside (Li B C) A D
\<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B D)) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)

goal (1 subgoal):
 1. \<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A \<Longrightarrow> False
[PROOF STEP]
by (simp add:Ang_outside_exclusive)
[PROOF STATE]
proof (state)
this:
\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A \<Longrightarrow> False

goal (1 subgoal):
 1. Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A \<or> \<not> Ang_inside (An A B C) D \<and> Ang_inside (An D B C) A
[PROOF STEP]
from P6 P8
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An A B C) D \<and> Ang_inside (An D B C) A \<Longrightarrow> False
\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A \<Longrightarrow> False
[PROOF STEP]
show "Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A
    \<or> \<not> Ang_inside (An A B C) D \<and> Ang_inside (An D B C) A"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An A B C) D \<and> Ang_inside (An D B C) A \<Longrightarrow> False
\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A \<Longrightarrow> False

goal (1 subgoal):
 1. Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A \<or> \<not> Ang_inside (An A B C) D \<and> Ang_inside (An D B C) A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A \<or> \<not> Ang_inside (An A B C) D \<and> Ang_inside (An D B C) A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Congruence_Rule) Plane_sameside_HalfLine :
  assumes
    "Plane_sameside l1 p1 p2"
    "Line_on l1 p3"
    "Line_on (Li p3 p1) p4"
    "\<not> Bet_Point (Se p4 p1) p3"
    "\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)"
    "\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p4) add Emp)"
  shows "Plane_sameside l1 p1 p4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Plane_sameside l1 p1 p4
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Plane_sameside l1 p1 p4
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside l1 p1 p2
Line_on l1 p3
Line_on (Li p3 p1) p4
\<not> Bet_Point (Se p4 p1) p3
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p4) add Emp)
[PROOF STEP]
have P1 : "\<not> Line_on l1 p1 \<and> \<not> Line_on l1 p2
    \<and> \<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside l1 p1 p2
Line_on l1 p3
Line_on (Li p3 p1) p4
\<not> Bet_Point (Se p4 p1) p3
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p4) add Emp)

goal (1 subgoal):
 1. \<not> Line_on l1 p1 \<and> \<not> Line_on l1 p2 \<and> \<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
[PROOF STEP]
by (simp add:Plane_sameside_def)
[PROOF STATE]
proof (state)
this:
\<not> Line_on l1 p1 \<and> \<not> Line_on l1 p2 \<and> \<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)

goal (1 subgoal):
 1. Plane_sameside l1 p1 p4
[PROOF STEP]
have "Plane_diffside l1 p1 p4 \<Longrightarrow>
    \<exists>p. Bet_Point (Se p1 p4) p \<and> Line_on l1 p \<and> \<not> Line_on l1 p1 \<and> \<not> Line_on l1 p4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Plane_diffside l1 p1 p4 \<Longrightarrow> \<exists>p. Bet_Point (Se p1 p4) p \<and> Line_on l1 p \<and> \<not> Line_on l1 p1 \<and> \<not> Line_on l1 p4
[PROOF STEP]
by (simp add:Plane_diffside_def)
[PROOF STATE]
proof (state)
this:
Plane_diffside l1 p1 p4 \<Longrightarrow> \<exists>p. Bet_Point (Se p1 p4) p \<and> Line_on l1 p \<and> \<not> Line_on l1 p1 \<and> \<not> Line_on l1 p4

goal (1 subgoal):
 1. Plane_sameside l1 p1 p4
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside l1 p1 p4 \<Longrightarrow> \<exists>p. Bet_Point (Se p1 p4) p \<and> Line_on l1 p \<and> \<not> Line_on l1 p1 \<and> \<not> Line_on l1 p4
[PROOF STEP]
obtain p5 :: Point where P2 : "Plane_diffside l1 p1 p4 \<Longrightarrow>
    Bet_Point (Se p1 p4) p5 \<and> Line_on l1 p5 \<and> \<not> Line_on l1 p4"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside l1 p1 p4 \<Longrightarrow> \<exists>p. Bet_Point (Se p1 p4) p \<and> Line_on l1 p \<and> \<not> Line_on l1 p1 \<and> \<not> Line_on l1 p4

goal (1 subgoal):
 1. (\<And>p5. (Plane_diffside l1 p1 p4 \<Longrightarrow> Bet_Point (Se p1 p4) p5 \<and> Line_on l1 p5 \<and> \<not> Line_on l1 p4) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Plane_diffside l1 p1 p4 \<Longrightarrow> Bet_Point (Se p1 p4) p5 \<and> Line_on l1 p5 \<and> \<not> Line_on l1 p4

goal (1 subgoal):
 1. Plane_sameside l1 p1 p4
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside l1 p1 p2
Line_on l1 p3
Line_on (Li p3 p1) p4
\<not> Bet_Point (Se p4 p1) p3
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p4) add Emp)
[PROOF STEP]
have P3 : "Eq (Geos (Poi p3) add Emp) (Geos (Poi p1) add Emp) \<Longrightarrow> Line_on l1 p1"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside l1 p1 p2
Line_on l1 p3
Line_on (Li p3 p1) p4
\<not> Bet_Point (Se p4 p1) p3
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p4) add Emp)

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

goal (1 subgoal):
 1. Plane_sameside l1 p1 p4
[PROOF STEP]
from P1 P3
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on l1 p1 \<and> \<not> Line_on l1 p2 \<and> \<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
Eq (Geos (Poi p3) add Emp) (Geos (Poi p1) add Emp) \<Longrightarrow> Line_on l1 p1
[PROOF STEP]
have P4 : "\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on l1 p1 \<and> \<not> Line_on l1 p2 \<and> \<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
Eq (Geos (Poi p3) add Emp) (Geos (Poi p1) add Emp) \<Longrightarrow> Line_on l1 p1

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

goal (1 subgoal):
 1. Plane_sameside l1 p1 p4
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p1) add Emp)
[PROOF STEP]
have P5 : "Eq (Geos (Lin (Li p3 p1)) add Emp) (Geos (Lin (Li p1 p3)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p1) add Emp)

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

goal (1 subgoal):
 1. Plane_sameside l1 p1 p4
[PROOF STEP]
from assms P5
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside l1 p1 p2
Line_on l1 p3
Line_on (Li p3 p1) p4
\<not> Bet_Point (Se p4 p1) p3
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p4) add Emp)
Eq (Geos (Lin (Li p3 p1)) add Emp) (Geos (Lin (Li p1 p3)) add Emp)
[PROOF STEP]
have P6 : "Line_on (Li p1 p3) p4"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside l1 p1 p2
Line_on l1 p3
Line_on (Li p3 p1) p4
\<not> Bet_Point (Se p4 p1) p3
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p4) add Emp)
Eq (Geos (Lin (Li p3 p1)) add Emp) (Geos (Lin (Li p1 p3)) add Emp)

goal (1 subgoal):
 1. Line_on (Li p1 p3) p4
[PROOF STEP]
by (simp add:Line_rev Line_on_trans)
[PROOF STATE]
proof (state)
this:
Line_on (Li p1 p3) p4

goal (1 subgoal):
 1. Plane_sameside l1 p1 p4
[PROOF STEP]
from P4
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p1) add Emp)
[PROOF STEP]
have P7 : "\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p3) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p1) add Emp)

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

goal (1 subgoal):
 1. Plane_sameside l1 p1 p4
[PROOF STEP]
from assms P6 P7
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside l1 p1 p2
Line_on l1 p3
Line_on (Li p3 p1) p4
\<not> Bet_Point (Se p4 p1) p3
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p4) add Emp)
Line_on (Li p1 p3) p4
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p3) add Emp)
[PROOF STEP]
have P8 : "Line_on (Li p1 p4) p3"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside l1 p1 p2
Line_on l1 p3
Line_on (Li p3 p1) p4
\<not> Bet_Point (Se p4 p1) p3
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p4) add Emp)
Line_on (Li p1 p3) p4
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p3) add Emp)

goal (1 subgoal):
 1. Line_on (Li p1 p4) p3
[PROOF STEP]
by (simp add:Line_on_rev)
[PROOF STATE]
proof (state)
this:
Line_on (Li p1 p4) p3

goal (1 subgoal):
 1. Plane_sameside l1 p1 p4
[PROOF STEP]
from P2
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside l1 p1 p4 \<Longrightarrow> Bet_Point (Se p1 p4) p5 \<and> Line_on l1 p5 \<and> \<not> Line_on l1 p4
[PROOF STEP]
have P9 : "Plane_diffside l1 p1 p4 \<Longrightarrow> Line_on (Li p1 p4) p5"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside l1 p1 p4 \<Longrightarrow> Bet_Point (Se p1 p4) p5 \<and> Line_on l1 p5 \<and> \<not> Line_on l1 p4

goal (1 subgoal):
 1. Plane_diffside l1 p1 p4 \<Longrightarrow> Line_on (Li p1 p4) p5
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Plane_diffside l1 p1 p4 \<Longrightarrow> Line_on (Li p1 p4) p5

goal (1 subgoal):
 1. Plane_sameside l1 p1 p4
[PROOF STEP]
from assms P2 P8 P9
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside l1 p1 p2
Line_on l1 p3
Line_on (Li p3 p1) p4
\<not> Bet_Point (Se p4 p1) p3
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p4) add Emp)
Plane_diffside l1 p1 p4 \<Longrightarrow> Bet_Point (Se p1 p4) p5 \<and> Line_on l1 p5 \<and> \<not> Line_on l1 p4
Line_on (Li p1 p4) p3
Plane_diffside l1 p1 p4 \<Longrightarrow> Line_on (Li p1 p4) p5
[PROOF STEP]
have P10 : "Plane_diffside l1 p1 p4 \<Longrightarrow> \<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p5) add Emp) \<Longrightarrow>
    Eq (Geos (Lin (Li p1 p4)) add Emp) (Geos (Lin l1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside l1 p1 p2
Line_on l1 p3
Line_on (Li p3 p1) p4
\<not> Bet_Point (Se p4 p1) p3
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p4) add Emp)
Plane_diffside l1 p1 p4 \<Longrightarrow> Bet_Point (Se p1 p4) p5 \<and> Line_on l1 p5 \<and> \<not> Line_on l1 p4
Line_on (Li p1 p4) p3
Plane_diffside l1 p1 p4 \<Longrightarrow> Line_on (Li p1 p4) p5

goal (1 subgoal):
 1. \<lbrakk>Plane_diffside l1 p1 p4; \<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p5) add Emp)\<rbrakk> \<Longrightarrow> Eq (Geos (Lin (Li p1 p4)) add Emp) (Geos (Lin l1) add Emp)
[PROOF STEP]
by (simp add:Line_unique)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Plane_diffside l1 p1 p4; \<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p5) add Emp)\<rbrakk> \<Longrightarrow> Eq (Geos (Lin (Li p1 p4)) add Emp) (Geos (Lin l1) add Emp)

goal (1 subgoal):
 1. Plane_sameside l1 p1 p4
[PROOF STEP]
have P11 : "Line_on (Li p1 p4) p1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p1 p4) p1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p1 p4) p1

goal (1 subgoal):
 1. Plane_sameside l1 p1 p4
[PROOF STEP]
from P10 P11
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>Plane_diffside l1 p1 p4; \<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p5) add Emp)\<rbrakk> \<Longrightarrow> Eq (Geos (Lin (Li p1 p4)) add Emp) (Geos (Lin l1) add Emp)
Line_on (Li p1 p4) p1
[PROOF STEP]
have P12 : "Plane_diffside l1 p1 p4 \<Longrightarrow> \<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p5) add Emp) \<Longrightarrow>
    Line_on l1 p1"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Plane_diffside l1 p1 p4; \<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p5) add Emp)\<rbrakk> \<Longrightarrow> Eq (Geos (Lin (Li p1 p4)) add Emp) (Geos (Lin l1) add Emp)
Line_on (Li p1 p4) p1

goal (1 subgoal):
 1. \<lbrakk>Plane_diffside l1 p1 p4; \<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p5) add Emp)\<rbrakk> \<Longrightarrow> Line_on l1 p1
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Plane_diffside l1 p1 p4; \<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p5) add Emp)\<rbrakk> \<Longrightarrow> Line_on l1 p1

goal (1 subgoal):
 1. Plane_sameside l1 p1 p4
[PROOF STEP]
from P1 P12
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on l1 p1 \<and> \<not> Line_on l1 p2 \<and> \<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
\<lbrakk>Plane_diffside l1 p1 p4; \<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p5) add Emp)\<rbrakk> \<Longrightarrow> Line_on l1 p1
[PROOF STEP]
have P13 : "Plane_diffside l1 p1 p4 \<Longrightarrow> Eq (Geos (Poi p5) add Emp) (Geos (Poi p3) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on l1 p1 \<and> \<not> Line_on l1 p2 \<and> \<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
\<lbrakk>Plane_diffside l1 p1 p4; \<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p5) add Emp)\<rbrakk> \<Longrightarrow> Line_on l1 p1

goal (1 subgoal):
 1. Plane_diffside l1 p1 p4 \<Longrightarrow> Eq (Geos (Poi p5) add Emp) (Geos (Poi p3) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev)
[PROOF STATE]
proof (state)
this:
Plane_diffside l1 p1 p4 \<Longrightarrow> Eq (Geos (Poi p5) add Emp) (Geos (Poi p3) add Emp)

goal (1 subgoal):
 1. Plane_sameside l1 p1 p4
[PROOF STEP]
from P2
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside l1 p1 p4 \<Longrightarrow> Bet_Point (Se p1 p4) p5 \<and> Line_on l1 p5 \<and> \<not> Line_on l1 p4
[PROOF STEP]
have P14 : "Plane_diffside l1 p1 p4 \<Longrightarrow> Bet_Point (Se p1 p4) p5"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside l1 p1 p4 \<Longrightarrow> Bet_Point (Se p1 p4) p5 \<and> Line_on l1 p5 \<and> \<not> Line_on l1 p4

goal (1 subgoal):
 1. Plane_diffside l1 p1 p4 \<Longrightarrow> Bet_Point (Se p1 p4) p5
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Plane_diffside l1 p1 p4 \<Longrightarrow> Bet_Point (Se p1 p4) p5

goal (1 subgoal):
 1. Plane_sameside l1 p1 p4
[PROOF STEP]
from P13 P14
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside l1 p1 p4 \<Longrightarrow> Eq (Geos (Poi p5) add Emp) (Geos (Poi p3) add Emp)
Plane_diffside l1 p1 p4 \<Longrightarrow> Bet_Point (Se p1 p4) p5
[PROOF STEP]
have "Plane_diffside l1 p1 p4 \<Longrightarrow> Bet_Point (Se p1 p4) p3"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside l1 p1 p4 \<Longrightarrow> Eq (Geos (Poi p5) add Emp) (Geos (Poi p3) add Emp)
Plane_diffside l1 p1 p4 \<Longrightarrow> Bet_Point (Se p1 p4) p5

goal (1 subgoal):
 1. Plane_diffside l1 p1 p4 \<Longrightarrow> Bet_Point (Se p1 p4) p3
[PROOF STEP]
by (simp add:Point_Eq)
[PROOF STATE]
proof (state)
this:
Plane_diffside l1 p1 p4 \<Longrightarrow> Bet_Point (Se p1 p4) p3

goal (1 subgoal):
 1. Plane_sameside l1 p1 p4
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside l1 p1 p4 \<Longrightarrow> Bet_Point (Se p1 p4) p3
[PROOF STEP]
have P15 : "Plane_diffside l1 p1 p4 \<Longrightarrow> Bet_Point (Se p4 p1) p3"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside l1 p1 p4 \<Longrightarrow> Bet_Point (Se p1 p4) p3

goal (1 subgoal):
 1. Plane_diffside l1 p1 p4 \<Longrightarrow> Bet_Point (Se p4 p1) p3
[PROOF STEP]
by (simp add:Bet_rev)
[PROOF STATE]
proof (state)
this:
Plane_diffside l1 p1 p4 \<Longrightarrow> Bet_Point (Se p4 p1) p3

goal (1 subgoal):
 1. Plane_sameside l1 p1 p4
[PROOF STEP]
from assms P15
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside l1 p1 p2
Line_on l1 p3
Line_on (Li p3 p1) p4
\<not> Bet_Point (Se p4 p1) p3
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p4) add Emp)
Plane_diffside l1 p1 p4 \<Longrightarrow> Bet_Point (Se p4 p1) p3
[PROOF STEP]
have P16 : "\<not> Plane_diffside l1 p1 p4"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside l1 p1 p2
Line_on l1 p3
Line_on (Li p3 p1) p4
\<not> Bet_Point (Se p4 p1) p3
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p4) add Emp)
Plane_diffside l1 p1 p4 \<Longrightarrow> Bet_Point (Se p4 p1) p3

goal (1 subgoal):
 1. \<not> Plane_diffside l1 p1 p4
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Plane_diffside l1 p1 p4

goal (1 subgoal):
 1. Plane_sameside l1 p1 p4
[PROOF STEP]
have P17 : "Line_on (Li p3 p1) p3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p3 p1) p3
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p3 p1) p3

goal (1 subgoal):
 1. Plane_sameside l1 p1 p4
[PROOF STEP]
from assms P17
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside l1 p1 p2
Line_on l1 p3
Line_on (Li p3 p1) p4
\<not> Bet_Point (Se p4 p1) p3
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p4) add Emp)
Line_on (Li p3 p1) p3
[PROOF STEP]
have P18 : "Line_on l1 p4 \<Longrightarrow>
    Eq (Geos (Lin (Li p3 p1)) add Emp) (Geos (Lin l1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside l1 p1 p2
Line_on l1 p3
Line_on (Li p3 p1) p4
\<not> Bet_Point (Se p4 p1) p3
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p4) add Emp)
Line_on (Li p3 p1) p3

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

goal (1 subgoal):
 1. Plane_sameside l1 p1 p4
[PROOF STEP]
have P19 : "Line_on (Li p3 p1) p1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p3 p1) p1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p3 p1) p1

goal (1 subgoal):
 1. Plane_sameside l1 p1 p4
[PROOF STEP]
from P18 P19
[PROOF STATE]
proof (chain)
picking this:
Line_on l1 p4 \<Longrightarrow> Eq (Geos (Lin (Li p3 p1)) add Emp) (Geos (Lin l1) add Emp)
Line_on (Li p3 p1) p1
[PROOF STEP]
have P20 : "Line_on l1 p4 \<Longrightarrow> Line_on l1 p1"
[PROOF STATE]
proof (prove)
using this:
Line_on l1 p4 \<Longrightarrow> Eq (Geos (Lin (Li p3 p1)) add Emp) (Geos (Lin l1) add Emp)
Line_on (Li p3 p1) p1

goal (1 subgoal):
 1. Line_on l1 p4 \<Longrightarrow> Line_on l1 p1
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Line_on l1 p4 \<Longrightarrow> Line_on l1 p1

goal (1 subgoal):
 1. Plane_sameside l1 p1 p4
[PROOF STEP]
from P1 P20
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on l1 p1 \<and> \<not> Line_on l1 p2 \<and> \<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
Line_on l1 p4 \<Longrightarrow> Line_on l1 p1
[PROOF STEP]
have P21 : "\<not> Line_on l1 p4"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on l1 p1 \<and> \<not> Line_on l1 p2 \<and> \<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
Line_on l1 p4 \<Longrightarrow> Line_on l1 p1

goal (1 subgoal):
 1. \<not> Line_on l1 p4
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on l1 p4

goal (1 subgoal):
 1. Plane_sameside l1 p1 p4
[PROOF STEP]
from assms P1 P16 P21
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside l1 p1 p2
Line_on l1 p3
Line_on (Li p3 p1) p4
\<not> Bet_Point (Se p4 p1) p3
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p4) add Emp)
\<not> Line_on l1 p1 \<and> \<not> Line_on l1 p2 \<and> \<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
\<not> Plane_diffside l1 p1 p4
\<not> Line_on l1 p4
[PROOF STEP]
show "Plane_sameside l1 p1 p4"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside l1 p1 p2
Line_on l1 p3
Line_on (Li p3 p1) p4
\<not> Bet_Point (Se p4 p1) p3
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p4) add Emp)
\<not> Line_on l1 p1 \<and> \<not> Line_on l1 p2 \<and> \<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
\<not> Plane_diffside l1 p1 p4
\<not> Line_on l1 p4

goal (1 subgoal):
 1. Plane_sameside l1 p1 p4
[PROOF STEP]
by (simp add:Plane_not_diffside_sameside)
[PROOF STATE]
proof (state)
this:
Plane_sameside l1 p1 p4

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Congruence_Rule) Plane_Bet_sameside_rev :
  assumes
    "Plane_sameside l1 p1 p3"
    "Line_on l1 p2"
    "\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)"
    "\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)"
    "\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p1) add Emp)"
    "Line_on l2 p1" "Line_on l2 p2" "Line_on l2 p3"
    "\<not> Eq (Geos (Lin l1) add Emp) (Geos (Lin l2) add Emp)"
  shows "Bet_Point (Se p3 p2) p1 \<or> Bet_Point (Se p2 p1) p3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bet_Point (Se p3 p2) p1 \<or> Bet_Point (Se p2 p1) p3
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Bet_Point (Se p3 p2) p1 \<or> Bet_Point (Se p2 p1) p3
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside l1 p1 p3
Line_on l1 p2
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p1) add Emp)
Line_on l2 p1
Line_on l2 p2
Line_on l2 p3
\<not> Eq (Geos (Lin l1) add Emp) (Geos (Lin l2) add Emp)
[PROOF STEP]
have P1 : "Bet_Point (Se p1 p3) p2 \<or> Bet_Point (Se p3 p2) p1 \<or> Bet_Point (Se p2 p1) p3"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside l1 p1 p3
Line_on l1 p2
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p1) add Emp)
Line_on l2 p1
Line_on l2 p2
Line_on l2 p3
\<not> Eq (Geos (Lin l1) add Emp) (Geos (Lin l2) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se p1 p3) p2 \<or> Bet_Point (Se p3 p2) p1 \<or> Bet_Point (Se p2 p1) p3
[PROOF STEP]
by (simp add:Bet_case)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p1 p3) p2 \<or> Bet_Point (Se p3 p2) p1 \<or> Bet_Point (Se p2 p1) p3

goal (1 subgoal):
 1. Bet_Point (Se p3 p2) p1 \<or> Bet_Point (Se p2 p1) p3
[PROOF STEP]
have P2 : "Line_on (Li p1 p3) p1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p1 p3) p1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p1 p3) p1

goal (1 subgoal):
 1. Bet_Point (Se p3 p2) p1 \<or> Bet_Point (Se p2 p1) p3
[PROOF STEP]
have P3 : "Line_on (Li p1 p3) p3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p1 p3) p3
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p1 p3) p3

goal (1 subgoal):
 1. Bet_Point (Se p3 p2) p1 \<or> Bet_Point (Se p2 p1) p3
[PROOF STEP]
from assms P2 P3
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside l1 p1 p3
Line_on l1 p2
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p1) add Emp)
Line_on l2 p1
Line_on l2 p2
Line_on l2 p3
\<not> Eq (Geos (Lin l1) add Emp) (Geos (Lin l2) add Emp)
Line_on (Li p1 p3) p1
Line_on (Li p1 p3) p3
[PROOF STEP]
have P4 : " Eq (Geos (Lin l2) add Emp) (Geos (Lin (Li p1 p3)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside l1 p1 p3
Line_on l1 p2
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p1) add Emp)
Line_on l2 p1
Line_on l2 p2
Line_on l2 p3
\<not> Eq (Geos (Lin l1) add Emp) (Geos (Lin l2) add Emp)
Line_on (Li p1 p3) p1
Line_on (Li p1 p3) p3

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

goal (1 subgoal):
 1. Bet_Point (Se p3 p2) p1 \<or> Bet_Point (Se p2 p1) p3
[PROOF STEP]
from assms P4
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside l1 p1 p3
Line_on l1 p2
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p1) add Emp)
Line_on l2 p1
Line_on l2 p2
Line_on l2 p3
\<not> Eq (Geos (Lin l1) add Emp) (Geos (Lin l2) add Emp)
Eq (Geos (Lin l2) add Emp) (Geos (Lin (Li p1 p3)) add Emp)
[PROOF STEP]
have "\<not> Eq (Geos (Lin l1) add Emp) (Geos (Lin (Li p1 p3)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside l1 p1 p3
Line_on l1 p2
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p1) add Emp)
Line_on l2 p1
Line_on l2 p2
Line_on l2 p3
\<not> Eq (Geos (Lin l1) add Emp) (Geos (Lin l2) add Emp)
Eq (Geos (Lin l2) add Emp) (Geos (Lin (Li p1 p3)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin l1) add Emp) (Geos (Lin (Li p1 p3)) add Emp)
[PROOF STEP]
by (blast intro:Eq_trans)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Lin l1) add Emp) (Geos (Lin (Li p1 p3)) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se p3 p2) p1 \<or> Bet_Point (Se p2 p1) p3
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Lin l1) add Emp) (Geos (Lin (Li p1 p3)) add Emp)
[PROOF STEP]
have P6 : "\<not> Eq (Geos (Lin (Li p1 p3)) add Emp) (Geos (Lin l1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Lin l1) add Emp) (Geos (Lin (Li p1 p3)) add Emp)

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

goal (1 subgoal):
 1. Bet_Point (Se p3 p2) p1 \<or> Bet_Point (Se p2 p1) p3
[PROOF STEP]
from assms P6
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside l1 p1 p3
Line_on l1 p2
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p1) add Emp)
Line_on l2 p1
Line_on l2 p2
Line_on l2 p3
\<not> Eq (Geos (Lin l1) add Emp) (Geos (Lin l2) add Emp)
\<not> Eq (Geos (Lin (Li p1 p3)) add Emp) (Geos (Lin l1) add Emp)
[PROOF STEP]
have "Bet_Point (Se p1 p3) p2 \<Longrightarrow> Plane_diffside l1 p1 p3"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside l1 p1 p3
Line_on l1 p2
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p1) add Emp)
Line_on l2 p1
Line_on l2 p2
Line_on l2 p3
\<not> Eq (Geos (Lin l1) add Emp) (Geos (Lin l2) add Emp)
\<not> Eq (Geos (Lin (Li p1 p3)) add Emp) (Geos (Lin l1) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se p1 p3) p2 \<Longrightarrow> Plane_diffside l1 p1 p3
[PROOF STEP]
by (simp add:Plane_Bet_diffside)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p1 p3) p2 \<Longrightarrow> Plane_diffside l1 p1 p3

goal (1 subgoal):
 1. Bet_Point (Se p3 p2) p1 \<or> Bet_Point (Se p2 p1) p3
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p1 p3) p2 \<Longrightarrow> Plane_diffside l1 p1 p3
[PROOF STEP]
have P7 : "Bet_Point (Se p1 p3) p2 \<Longrightarrow> \<not> Plane_sameside l1 p1 p3"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p1 p3) p2 \<Longrightarrow> Plane_diffside l1 p1 p3

goal (1 subgoal):
 1. Bet_Point (Se p1 p3) p2 \<Longrightarrow> \<not> Plane_sameside l1 p1 p3
[PROOF STEP]
by (simp add:Plane_diffside_not_sameside)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p1 p3) p2 \<Longrightarrow> \<not> Plane_sameside l1 p1 p3

goal (1 subgoal):
 1. Bet_Point (Se p3 p2) p1 \<or> Bet_Point (Se p2 p1) p3
[PROOF STEP]
from assms P7
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside l1 p1 p3
Line_on l1 p2
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p1) add Emp)
Line_on l2 p1
Line_on l2 p2
Line_on l2 p3
\<not> Eq (Geos (Lin l1) add Emp) (Geos (Lin l2) add Emp)
Bet_Point (Se p1 p3) p2 \<Longrightarrow> \<not> Plane_sameside l1 p1 p3
[PROOF STEP]
have P8 : "\<not> Bet_Point (Se p1 p3) p2"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside l1 p1 p3
Line_on l1 p2
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p1) add Emp)
Line_on l2 p1
Line_on l2 p2
Line_on l2 p3
\<not> Eq (Geos (Lin l1) add Emp) (Geos (Lin l2) add Emp)
Bet_Point (Se p1 p3) p2 \<Longrightarrow> \<not> Plane_sameside l1 p1 p3

goal (1 subgoal):
 1. \<not> Bet_Point (Se p1 p3) p2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se p1 p3) p2

goal (1 subgoal):
 1. Bet_Point (Se p3 p2) p1 \<or> Bet_Point (Se p2 p1) p3
[PROOF STEP]
from P1 P8
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p1 p3) p2 \<or> Bet_Point (Se p3 p2) p1 \<or> Bet_Point (Se p2 p1) p3
\<not> Bet_Point (Se p1 p3) p2
[PROOF STEP]
show "Bet_Point (Se p3 p2) p1 \<or> Bet_Point (Se p2 p1) p3"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p1 p3) p2 \<or> Bet_Point (Se p3 p2) p1 \<or> Bet_Point (Se p2 p1) p3
\<not> Bet_Point (Se p1 p3) p2

goal (1 subgoal):
 1. Bet_Point (Se p3 p2) p1 \<or> Bet_Point (Se p2 p1) p3
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p3 p2) p1 \<or> Bet_Point (Se p2 p1) p3

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Congruence_Rule) Seg_Bet_relation :
  assumes N :
    "Bet_Point (Se p1 p2) p3"
  shows "\<not> Eq (Geos (Seg (Se p1 p2)) add Emp) (Geos (Seg (Se p1 p3)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Eq (Geos (Seg (Se p1 p2)) add Emp) (Geos (Seg (Se p1 p3)) add Emp)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Eq (Geos (Seg (Se p1 p2)) add Emp) (Geos (Seg (Se p1 p3)) add Emp) \<Longrightarrow> False
[PROOF STEP]
assume W : "Eq (Geos (Seg (Se p1 p2)) add Emp) (Geos (Seg (Se p1 p3)) add Emp)"
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se p1 p2)) add Emp) (Geos (Seg (Se p1 p3)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se p1 p2)) add Emp) (Geos (Seg (Se p1 p3)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from N
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p1 p2) p3
[PROOF STEP]
have "Inv (Bet_Point (Se p2 p3) p1) \<and> Inv (Bet_Point (Se p3 p1) p2)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p1 p2) p3

goal (1 subgoal):
 1. Inv (Bet_Point (Se p2 p3) p1) \<and> Inv (Bet_Point (Se p3 p1) p2)
[PROOF STEP]
by (simp add:Bet_iff)
[PROOF STATE]
proof (state)
this:
Inv (Bet_Point (Se p2 p3) p1) \<and> Inv (Bet_Point (Se p3 p1) p2)

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

goal (1 subgoal):
 1. \<not> Bet_Point (Se p2 p3) p1
[PROOF STEP]
by (simp add:Inv_def)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se p2 p3) p1

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

goal (1 subgoal):
 1. Eq (Geos (Seg (Se p1 p2)) add Emp) (Geos (Seg (Se p1 p3)) add Emp) \<Longrightarrow> False
[PROOF STEP]
have P3 : "Line_on (Li p1 p2) p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p1 p2) p2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p1 p2) p2

goal (1 subgoal):
 1. Eq (Geos (Seg (Se p1 p2)) add Emp) (Geos (Seg (Se p1 p3)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from N
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p1 p2) p3
[PROOF STEP]
have P4 : "Line_on (Li p1 p2) p3"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p1 p2) p3

goal (1 subgoal):
 1. Line_on (Li p1 p2) p3
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li p1 p2) p3

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

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

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

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

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

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

goal (1 subgoal):
 1. Eq (Geos (Seg (Se p1 p2)) add Emp) (Geos (Seg (Se p1 p3)) add Emp) \<Longrightarrow> False
[PROOF STEP]
from W P1 P2 P3 P4 P5 P6
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se p1 p2)) add Emp) (Geos (Seg (Se p1 p3)) add Emp)
\<not> Bet_Point (Se p2 p3) p1
Line_on (Li p1 p2) p1
Line_on (Li p1 p2) p2
Line_on (Li p1 p2) p3
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p3) add Emp)
[PROOF STEP]
have P7 : "Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se p1 p2)) add Emp) (Geos (Seg (Se p1 p3)) add Emp)
\<not> Bet_Point (Se p2 p3) p1
Line_on (Li p1 p2) p1
Line_on (Li p1 p2) p2
Line_on (Li p1 p2) p3
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p3) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)
[PROOF STEP]
by (blast intro:Seg_move_unique)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Congruence_Rule) Seg_Bet_move_lemma1 :
  assumes
    "Bet_Point (Se p11 p13) p12"
    "Line_on l1 p21" "Line_on l1 p22" "Line_on l1 p23"
    "\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)"
    "\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)"
    "Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)"
    "Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)"
    "\<not> Bet_Point (Se p22 p23) p21"
  shows "Bet_Point (Se p21 p23) p22"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p22
Line_on l1 p23
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Bet_Point (Se p22 p23) p21
[PROOF STEP]
have P1 : "\<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p21) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p22
Line_on l1 p23
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Bet_Point (Se p22 p23) p21

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

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p22
Line_on l1 p23
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Bet_Point (Se p22 p23) p21
[PROOF STEP]
have "\<not> Eq (Geos (Poi p12) add Emp) (Geos (Poi p11) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p22
Line_on l1 p23
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Bet_Point (Se p22 p23) p21

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

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi p12) add Emp) (Geos (Poi p11) add Emp)
[PROOF STEP]
have P2 : "\<not> Eq (Geos (Poi p11) add Emp) (Geos (Poi p12) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi p12) add Emp) (Geos (Poi p11) add Emp)

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

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
from assms P1 P2
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p22
Line_on l1 p23
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Bet_Point (Se p22 p23) p21
\<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p21) add Emp)
\<not> Eq (Geos (Poi p11) add Emp) (Geos (Poi p12) add Emp)
[PROOF STEP]
have "\<exists>p. Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p22 p)) add Emp)
    \<and> \<not> Bet_Point (Se p p21) p22 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p22
Line_on l1 p23
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Bet_Point (Se p22 p23) p21
\<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p21) add Emp)
\<not> Eq (Geos (Poi p11) add Emp) (Geos (Poi p12) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p22 p)) add Emp) \<and> \<not> Bet_Point (Se p p21) p22 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p22) 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 p11 p12)) add Emp) (Geos (Seg (Se p22 p)) add Emp) \<and> \<not> Bet_Point (Se p p21) p22 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p22 p)) add Emp) \<and> \<not> Bet_Point (Se p p21) p22 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
obtain p211 :: Point where P3 : "Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p22 p211)) add Emp)
    \<and> \<not> Bet_Point (Se p211 p21) p22 \<and> Line_on l1 p211 \<and> \<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p211) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p22 p)) add Emp) \<and> \<not> Bet_Point (Se p p21) p22 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p) add Emp)

goal (1 subgoal):
 1. (\<And>p211. Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p22 p211)) add Emp) \<and> \<not> Bet_Point (Se p211 p21) p22 \<and> Line_on l1 p211 \<and> \<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p211) add Emp) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p22 p211)) add Emp) \<and> \<not> Bet_Point (Se p211 p21) p22 \<and> Line_on l1 p211 \<and> \<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p211) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p22
Line_on l1 p23
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Bet_Point (Se p22 p23) p21
[PROOF STEP]
have "\<not> Eq (Geos (Poi p13) add Emp) (Geos (Poi p12) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p22
Line_on l1 p23
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Bet_Point (Se p22 p23) p21

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

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi p13) add Emp) (Geos (Poi p12) add Emp)
[PROOF STEP]
have P4 : "\<not> Eq (Geos (Poi p12) add Emp) (Geos (Poi p13) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi p13) add Emp) (Geos (Poi p12) add Emp)

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

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
from assms P3 P4
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p22
Line_on l1 p23
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Bet_Point (Se p22 p23) p21
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p22 p211)) add Emp) \<and> \<not> Bet_Point (Se p211 p21) p22 \<and> Line_on l1 p211 \<and> \<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p211) add Emp)
\<not> Eq (Geos (Poi p12) add Emp) (Geos (Poi p13) add Emp)
[PROOF STEP]
have "\<exists>p. Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p)) add Emp)
    \<and> Bet_Point (Se p p211) p22 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p22
Line_on l1 p23
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Bet_Point (Se p22 p23) p21
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p22 p211)) add Emp) \<and> \<not> Bet_Point (Se p211 p21) p22 \<and> Line_on l1 p211 \<and> \<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p211) add Emp)
\<not> Eq (Geos (Poi p12) add Emp) (Geos (Poi p13) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p)) add Emp) \<and> Bet_Point (Se p p211) p22 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
by (simp add:Seg_move_diffside)
[PROOF STATE]
proof (state)
this:
\<exists>p. Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p)) add Emp) \<and> Bet_Point (Se p p211) p22 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p)) add Emp) \<and> Bet_Point (Se p p211) p22 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
obtain p231 :: Point where P5 : "Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p231)) add Emp)
    \<and> Bet_Point (Se p231 p211) p22 \<and> Line_on l1 p231 \<and> \<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p231) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p)) add Emp) \<and> Bet_Point (Se p p211) p22 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p) add Emp)

goal (1 subgoal):
 1. (\<And>p231. Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p231)) add Emp) \<and> Bet_Point (Se p231 p211) p22 \<and> Line_on l1 p231 \<and> \<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p231) add Emp) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p231)) add Emp) \<and> Bet_Point (Se p231 p211) p22 \<and> Line_on l1 p231 \<and> \<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p231) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
have P6 : "Eq (Geos (Seg (Se p21 p22)) add Emp) (Geos (Seg (Se p22 p21)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Seg (Se p21 p22)) add Emp) (Geos (Seg (Se p22 p21)) add Emp)
[PROOF STEP]
by (simp add:Seg_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se p21 p22)) add Emp) (Geos (Seg (Se p22 p21)) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p22
Line_on l1 p23
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Bet_Point (Se p22 p23) p21
[PROOF STEP]
have P7 : "Eq (Geos (Seg (Se p21 p22)) add Emp) (Geos (Seg (Se p11 p12)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p22
Line_on l1 p23
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Bet_Point (Se p22 p23) p21

goal (1 subgoal):
 1. Eq (Geos (Seg (Se p21 p22)) add Emp) (Geos (Seg (Se p11 p12)) add Emp)
[PROOF STEP]
by (simp add:Eq_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se p21 p22)) add Emp) (Geos (Seg (Se p11 p12)) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
from P3 P7
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p22 p211)) add Emp) \<and> \<not> Bet_Point (Se p211 p21) p22 \<and> Line_on l1 p211 \<and> \<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p211) add Emp)
Eq (Geos (Seg (Se p21 p22)) add Emp) (Geos (Seg (Se p11 p12)) add Emp)
[PROOF STEP]
have P8 : "Eq (Geos (Seg (Se p22 p211)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p22 p211)) add Emp) \<and> \<not> Bet_Point (Se p211 p21) p22 \<and> Line_on l1 p211 \<and> \<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p211) add Emp)
Eq (Geos (Seg (Se p21 p22)) add Emp) (Geos (Seg (Se p11 p12)) add Emp)

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

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
from P6 P8
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se p21 p22)) add Emp) (Geos (Seg (Se p22 p21)) add Emp)
Eq (Geos (Seg (Se p22 p211)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
[PROOF STEP]
have P9 : "Eq (Geos (Seg (Se p22 p211)) add Emp) (Geos (Seg (Se p22 p21)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se p21 p22)) add Emp) (Geos (Seg (Se p22 p21)) add Emp)
Eq (Geos (Seg (Se p22 p211)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se p22 p211)) add Emp) (Geos (Seg (Se p22 p21)) add Emp)
[PROOF STEP]
by (blast intro:Eq_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se p22 p211)) add Emp) (Geos (Seg (Se p22 p21)) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
from assms P1 P3 P9
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p22
Line_on l1 p23
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Bet_Point (Se p22 p23) p21
\<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p21) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p22 p211)) add Emp) \<and> \<not> Bet_Point (Se p211 p21) p22 \<and> Line_on l1 p211 \<and> \<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p211) add Emp)
Eq (Geos (Seg (Se p22 p211)) add Emp) (Geos (Seg (Se p22 p21)) add Emp)
[PROOF STEP]
have P10 : "Eq (Geos (Poi p211) add Emp) (Geos (Poi p21) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p22
Line_on l1 p23
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Bet_Point (Se p22 p23) p21
\<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p21) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p22 p211)) add Emp) \<and> \<not> Bet_Point (Se p211 p21) p22 \<and> Line_on l1 p211 \<and> \<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p211) add Emp)
Eq (Geos (Seg (Se p22 p211)) add Emp) (Geos (Seg (Se p22 p21)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Poi p211) add Emp) (Geos (Poi p21) add Emp)
[PROOF STEP]
by (blast intro:Seg_move_unique)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi p211) add Emp) (Geos (Poi p21) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
from P5
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p231)) add Emp) \<and> Bet_Point (Se p231 p211) p22 \<and> Line_on l1 p231 \<and> \<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p231) add Emp)
[PROOF STEP]
have P11 : "Bet_Point (Se p211 p231) p22"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p231)) add Emp) \<and> Bet_Point (Se p231 p211) p22 \<and> Line_on l1 p231 \<and> \<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p231) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se p211 p231) p22
[PROOF STEP]
by (simp add:Bet_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p211 p231) p22

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
from P10 P11
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Poi p211) add Emp) (Geos (Poi p21) add Emp)
Bet_Point (Se p211 p231) p22
[PROOF STEP]
have P12 : "Bet_Point (Se p21 p231) p22"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Poi p211) add Emp) (Geos (Poi p21) add Emp)
Bet_Point (Se p211 p231) p22

goal (1 subgoal):
 1. Bet_Point (Se p21 p231) p22
[PROOF STEP]
by (simp add:Bet_Point_Eq)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p21 p231) p22

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
have P13 : "Line_on (Li p11 p12) p11"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p11 p12) p11
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p11 p12) p11

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
have P14 : "Line_on (Li p11 p12) p12"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p11 p12) p12
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p11 p12) p12

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p22
Line_on l1 p23
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Bet_Point (Se p22 p23) p21
[PROOF STEP]
have P15 : "Line_on (Li p11 p12) p13"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p22
Line_on l1 p23
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Bet_Point (Se p22 p23) p21

goal (1 subgoal):
 1. Line_on (Li p11 p12) p13
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li p11 p12) p13

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p22
Line_on l1 p23
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Bet_Point (Se p22 p23) p21
[PROOF STEP]
have P16 : "\<not> Seg_on_Seg (Se p11 p12) (Se p12 p13)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p22
Line_on l1 p23
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Bet_Point (Se p22 p23) p21

goal (1 subgoal):
 1. \<not> Seg_on_Seg (Se p11 p12) (Se p12 p13)
[PROOF STEP]
by (simp add:Seg_Bet_not_on)
[PROOF STATE]
proof (state)
this:
\<not> Seg_on_Seg (Se p11 p12) (Se p12 p13)

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
from P12
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p21 p231) p22
[PROOF STEP]
have P17 : "\<not> Seg_on_Seg (Se p21 p22) (Se p22 p231)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p21 p231) p22

goal (1 subgoal):
 1. \<not> Seg_on_Seg (Se p21 p22) (Se p22 p231)
[PROOF STEP]
by (simp add:Seg_Bet_not_on)
[PROOF STATE]
proof (state)
this:
\<not> Seg_on_Seg (Se p21 p22) (Se p22 p231)

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
from assms P5 P13 P14 P15 P16 P17
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p22
Line_on l1 p23
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Bet_Point (Se p22 p23) p21
Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p231)) add Emp) \<and> Bet_Point (Se p231 p211) p22 \<and> Line_on l1 p231 \<and> \<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p231) add Emp)
Line_on (Li p11 p12) p11
Line_on (Li p11 p12) p12
Line_on (Li p11 p12) p13
\<not> Seg_on_Seg (Se p11 p12) (Se p12 p13)
\<not> Seg_on_Seg (Se p21 p22) (Se p22 p231)
[PROOF STEP]
have P18 : "Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p231)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p22
Line_on l1 p23
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Bet_Point (Se p22 p23) p21
Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p231)) add Emp) \<and> Bet_Point (Se p231 p211) p22 \<and> Line_on l1 p231 \<and> \<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p231) add Emp)
Line_on (Li p11 p12) p11
Line_on (Li p11 p12) p12
Line_on (Li p11 p12) p13
\<not> Seg_on_Seg (Se p11 p12) (Se p12 p13)
\<not> Seg_on_Seg (Se p21 p22) (Se p22 p231)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p231)) add Emp)
[PROOF STEP]
by (simp add:Seg_add)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p231)) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
from assms P18
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p22
Line_on l1 p23
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Bet_Point (Se p22 p23) p21
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p231)) add Emp)
[PROOF STEP]
have P19 : "Eq (Geos (Seg (Se p21 p231)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p22
Line_on l1 p23
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Bet_Point (Se p22 p23) p21
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p231)) add Emp)

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

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
from P12
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p21 p231) p22
[PROOF STEP]
have P20 : "\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p231) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p21 p231) p22

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

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
from P12
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p21 p231) p22
[PROOF STEP]
have P21 : "Bet_Point (Se p231 p21) p22"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p21 p231) p22

goal (1 subgoal):
 1. Bet_Point (Se p231 p21) p22
[PROOF STEP]
by (simp add:Bet_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p231 p21) p22

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
from P21
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p231 p21) p22
[PROOF STEP]
have P22 : "Bet_Point (Se p231 p23) p21 \<Longrightarrow> Bet_Point (Se p22 p23) p21"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p231 p21) p22

goal (1 subgoal):
 1. Bet_Point (Se p231 p23) p21 \<Longrightarrow> Bet_Point (Se p22 p23) p21
[PROOF STEP]
by (blast intro:Bet_swap_134_234)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p231 p23) p21 \<Longrightarrow> Bet_Point (Se p22 p23) p21

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
from assms P22
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p22
Line_on l1 p23
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Bet_Point (Se p22 p23) p21
Bet_Point (Se p231 p23) p21 \<Longrightarrow> Bet_Point (Se p22 p23) p21
[PROOF STEP]
have P23 : "\<not> Bet_Point (Se p231 p23) p21"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p22
Line_on l1 p23
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Bet_Point (Se p22 p23) p21
Bet_Point (Se p231 p23) p21 \<Longrightarrow> Bet_Point (Se p22 p23) p21

goal (1 subgoal):
 1. \<not> Bet_Point (Se p231 p23) p21
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se p231 p23) p21

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
from assms P5 P19 P20 P23
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p22
Line_on l1 p23
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Bet_Point (Se p22 p23) p21
Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p231)) add Emp) \<and> Bet_Point (Se p231 p211) p22 \<and> Line_on l1 p231 \<and> \<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p231) add Emp)
Eq (Geos (Seg (Se p21 p231)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p231) add Emp)
\<not> Bet_Point (Se p231 p23) p21
[PROOF STEP]
have P24 : "Eq (Geos (Poi p231) add Emp) (Geos (Poi p23) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p22
Line_on l1 p23
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Bet_Point (Se p22 p23) p21
Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p231)) add Emp) \<and> Bet_Point (Se p231 p211) p22 \<and> Line_on l1 p231 \<and> \<not> Eq (Geos (Poi p22) add Emp) (Geos (Poi p231) add Emp)
Eq (Geos (Seg (Se p21 p231)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p231) add Emp)
\<not> Bet_Point (Se p231 p23) p21

goal (1 subgoal):
 1. Eq (Geos (Poi p231) add Emp) (Geos (Poi p23) add Emp)
[PROOF STEP]
by (blast intro:Seg_move_unique)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi p231) add Emp) (Geos (Poi p23) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
from P21 P24
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p231 p21) p22
Eq (Geos (Poi p231) add Emp) (Geos (Poi p23) add Emp)
[PROOF STEP]
have "Bet_Point (Se p23 p21) p22"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p231 p21) p22
Eq (Geos (Poi p231) add Emp) (Geos (Poi p23) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se p23 p21) p22
[PROOF STEP]
by (simp add:Bet_Point_Eq)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p23 p21) p22

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
thus "Bet_Point (Se p21 p23) p22"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p23 p21) p22

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
by (simp add:Bet_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p21 p23) p22

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Congruence_Rule) Seg_Bet_move_sameside :
  assumes
    "Bet_Point (Se p11 p13) p12"
    "Line_on l1 p21" "Line_on l1 p4"
    "\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p4) add Emp)"
  shows "\<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q
    \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp)
    \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp)
    \<and> \<not> Bet_Point (Se p p4) p21 \<and> \<not> Bet_Point (Se q p4) p21"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> \<not> Bet_Point (Se p p4) p21 \<and> \<not> Bet_Point (Se q p4) p21
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> \<not> Bet_Point (Se p p4) p21 \<and> \<not> Bet_Point (Se q p4) p21
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p4
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p4) add Emp)
[PROOF STEP]
have "\<not> Eq (Geos (Poi p12) add Emp) (Geos (Poi p11) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p4
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p4) add Emp)

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

goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> \<not> Bet_Point (Se p p4) p21 \<and> \<not> Bet_Point (Se q p4) p21
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi p12) add Emp) (Geos (Poi p11) add Emp)
[PROOF STEP]
have P1 : "\<not> Eq (Geos (Poi p11) add Emp) (Geos (Poi p12) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi p12) add Emp) (Geos (Poi p11) add Emp)

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

goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> \<not> Bet_Point (Se p p4) p21 \<and> \<not> Bet_Point (Se q p4) p21
[PROOF STEP]
from assms P1
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p4
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p4) add Emp)
\<not> Eq (Geos (Poi p11) add Emp) (Geos (Poi p12) add Emp)
[PROOF STEP]
have "\<exists>p. Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp)
    \<and> \<not> Bet_Point (Se p p4) p21 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p4
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p4) add Emp)
\<not> Eq (Geos (Poi p11) add Emp) (Geos (Poi p12) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> \<not> Bet_Point (Se p p4) p21 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p21) 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 p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> \<not> Bet_Point (Se p p4) p21 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p) add Emp)

goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> \<not> Bet_Point (Se p p4) p21 \<and> \<not> Bet_Point (Se q p4) p21
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> \<not> Bet_Point (Se p p4) p21 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
obtain p22 :: Point where P2 : "Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
    \<and> \<not> Bet_Point (Se p22 p4) p21 \<and> Line_on l1 p22 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> \<not> Bet_Point (Se p p4) p21 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p) add Emp)

goal (1 subgoal):
 1. (\<And>p22. Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp) \<and> \<not> Bet_Point (Se p22 p4) p21 \<and> Line_on l1 p22 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp) \<and> \<not> Bet_Point (Se p22 p4) p21 \<and> Line_on l1 p22 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)

goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> \<not> Bet_Point (Se p p4) p21 \<and> \<not> Bet_Point (Se q p4) p21
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p4
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p4) add Emp)
[PROOF STEP]
have P3 : "\<not> Eq (Geos (Poi p11) add Emp) (Geos (Poi p13) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p4
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p4) add Emp)

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

goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> \<not> Bet_Point (Se p p4) p21 \<and> \<not> Bet_Point (Se q p4) p21
[PROOF STEP]
from assms P2 P3
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p4
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p4) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp) \<and> \<not> Bet_Point (Se p22 p4) p21 \<and> Line_on l1 p22 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p11) add Emp) (Geos (Poi p13) add Emp)
[PROOF STEP]
have "\<exists>p. Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p)) add Emp)
    \<and> \<not> Bet_Point (Se p p22) p21 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p4
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p4) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp) \<and> \<not> Bet_Point (Se p22 p4) p21 \<and> Line_on l1 p22 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p11) add Emp) (Geos (Poi p13) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> \<not> Bet_Point (Se p p22) p21 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p21) 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 p11 p13)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> \<not> Bet_Point (Se p p22) p21 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p) add Emp)

goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> \<not> Bet_Point (Se p p4) p21 \<and> \<not> Bet_Point (Se q p4) p21
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> \<not> Bet_Point (Se p p22) p21 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
obtain p23 :: Point where P4 : "Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
    \<and> \<not> Bet_Point (Se p23 p22) p21 \<and> Line_on l1 p23 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> \<not> Bet_Point (Se p p22) p21 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p) add Emp)

goal (1 subgoal):
 1. (\<And>p23. Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp) \<and> \<not> Bet_Point (Se p23 p22) p21 \<and> Line_on l1 p23 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp) \<and> \<not> Bet_Point (Se p23 p22) p21 \<and> Line_on l1 p23 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)

goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> \<not> Bet_Point (Se p p4) p21 \<and> \<not> Bet_Point (Se q p4) p21
[PROOF STEP]
from P4
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp) \<and> \<not> Bet_Point (Se p23 p22) p21 \<and> Line_on l1 p23 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
[PROOF STEP]
have "\<not> Bet_Point (Se p23 p22) p21"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp) \<and> \<not> Bet_Point (Se p23 p22) p21 \<and> Line_on l1 p23 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)

goal (1 subgoal):
 1. \<not> Bet_Point (Se p23 p22) p21
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se p23 p22) p21

goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> \<not> Bet_Point (Se p p4) p21 \<and> \<not> Bet_Point (Se q p4) p21
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Bet_Point (Se p23 p22) p21
[PROOF STEP]
have P5 : "\<not> Bet_Point (Se p22 p23) p21"
[PROOF STATE]
proof (prove)
using this:
\<not> Bet_Point (Se p23 p22) p21

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

goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> \<not> Bet_Point (Se p p4) p21 \<and> \<not> Bet_Point (Se q p4) p21
[PROOF STEP]
from assms P2 P4 P5
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p4
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p4) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp) \<and> \<not> Bet_Point (Se p22 p4) p21 \<and> Line_on l1 p22 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp) \<and> \<not> Bet_Point (Se p23 p22) p21 \<and> Line_on l1 p23 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
\<not> Bet_Point (Se p22 p23) p21
[PROOF STEP]
have P6 : "Bet_Point (Se p21 p23) p22"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p4
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p4) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp) \<and> \<not> Bet_Point (Se p22 p4) p21 \<and> Line_on l1 p22 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp) \<and> \<not> Bet_Point (Se p23 p22) p21 \<and> Line_on l1 p23 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
\<not> Bet_Point (Se p22 p23) p21

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
by (blast intro:Seg_Bet_move_lemma1)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p21 p23) p22

goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> \<not> Bet_Point (Se p p4) p21 \<and> \<not> Bet_Point (Se q p4) p21
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p21 p23) p22
[PROOF STEP]
have P7 : "Bet_Point (Se p23 p21) p22"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p21 p23) p22

goal (1 subgoal):
 1. Bet_Point (Se p23 p21) p22
[PROOF STEP]
by (simp add:Bet_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p23 p21) p22

goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> \<not> Bet_Point (Se p p4) p21 \<and> \<not> Bet_Point (Se q p4) p21
[PROOF STEP]
from P7
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p23 p21) p22
[PROOF STEP]
have P8 : "Bet_Point (Se p23 p4) p21 \<Longrightarrow> Bet_Point (Se p22 p4) p21"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p23 p21) p22

goal (1 subgoal):
 1. Bet_Point (Se p23 p4) p21 \<Longrightarrow> Bet_Point (Se p22 p4) p21
[PROOF STEP]
by (blast intro:Bet_swap_134_234)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p23 p4) p21 \<Longrightarrow> Bet_Point (Se p22 p4) p21

goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> \<not> Bet_Point (Se p p4) p21 \<and> \<not> Bet_Point (Se q p4) p21
[PROOF STEP]
from P2 P8
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp) \<and> \<not> Bet_Point (Se p22 p4) p21 \<and> Line_on l1 p22 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
Bet_Point (Se p23 p4) p21 \<Longrightarrow> Bet_Point (Se p22 p4) p21
[PROOF STEP]
have P9 : "\<not> Bet_Point (Se p23 p4) p21"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp) \<and> \<not> Bet_Point (Se p22 p4) p21 \<and> Line_on l1 p22 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
Bet_Point (Se p23 p4) p21 \<Longrightarrow> Bet_Point (Se p22 p4) p21

goal (1 subgoal):
 1. \<not> Bet_Point (Se p23 p4) p21
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se p23 p4) p21

goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> \<not> Bet_Point (Se p p4) p21 \<and> \<not> Bet_Point (Se q p4) p21
[PROOF STEP]
from P2 P4 P6 P9
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp) \<and> \<not> Bet_Point (Se p22 p4) p21 \<and> Line_on l1 p22 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp) \<and> \<not> Bet_Point (Se p23 p22) p21 \<and> Line_on l1 p23 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Bet_Point (Se p21 p23) p22
\<not> Bet_Point (Se p23 p4) p21
[PROOF STEP]
show "\<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q
    \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp)
    \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp)
    \<and> \<not> Bet_Point (Se p p4) p21 \<and> \<not> Bet_Point (Se q p4) p21"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp) \<and> \<not> Bet_Point (Se p22 p4) p21 \<and> Line_on l1 p22 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp) \<and> \<not> Bet_Point (Se p23 p22) p21 \<and> Line_on l1 p23 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Bet_Point (Se p21 p23) p22
\<not> Bet_Point (Se p23 p4) p21

goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> \<not> Bet_Point (Se p p4) p21 \<and> \<not> Bet_Point (Se q p4) p21
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> \<not> Bet_Point (Se p p4) p21 \<and> \<not> Bet_Point (Se q p4) p21

goal:
No subgoals!
[PROOF STEP]
qed