Theory Congruence

(*<*)
theory Congruence imports Order begin
(*>*)

section‹Congruence›
text‹
Of the equivalence relations for angles, only the transitive law is not included in the axiom, but is mentioned by the theorem.
However, in the proofs before that, there are some scenes where it is regarded as congruence by the congruence relation with the same angle.
Therefore, we add a weak transitive law that ``when two angles are congruent, the same angle as one is congruent with the other".
Also, the uniqueness of the large and small relationship between the two angles and the transitive relation of three or more those have not been proved.
Therefore, each proof regarding these is added to this section.
Furthermore, regarding Theorem 23, the proof is omitted because the ``large and small relationship of line segments", which is treated as a premise, is undefined.
As a result, the proof process of Theorem 24 is different from the existing one.
›

locale Definition_3 = Order_Rule +
  fixes Def :: "Geo_object ⇒ bool"
    and Cong :: "Geo_objects ⇒ Geo_objects ⇒ bool"
    and Gr :: "Geo_objects ⇒ Geo_objects ⇒ bool"
    and Ang_inside :: "Angle ⇒ Point ⇒ bool"
    and Right_angle :: "Angle ⇒ bool"
  assumes Tri_def : "Def (Tri (Tr p1 p2 p3)) ⟷ ¬ Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
        ∧ ¬ Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp) ∧ ¬ Eq (Geos (Poi p3) add Emp) (Geos (Poi p1) add Emp)
        ∧ ¬ Bet_Point (Se p1 p2) p3 ∧ ¬ Bet_Point (Se p2 p3) p1 ∧ ¬ Bet_Point (Se p3 p1) p2
        ∧ ¬ Seg_on_Seg (Se p1 p2) (Se p2 p3) ∧ ¬ Seg_on_Seg (Se p2 p3) (Se p3 p1) ∧ ¬ Seg_on_Seg (Se p3 p1) (Se p1 p2)"
    and Cong_refl [simp,intro] : "Cong obs obs"
    and Ang_def : "Def (Ang (An p1 p2 p3)) ⟷ ¬ Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
        ∧ ¬ Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp) ∧ ¬ Eq (Geos (Poi p3) add Emp) (Geos (Poi p1) add Emp)
        ∧ ¬ Eq (Geos (Lin (Li p2 p1)) add Emp) (Geos (Lin (Li p2 p3)) add Emp)"
    and Ang_rev : "⟦Cong (Geos (ang1) add Emp) (Geos (ang2) add Emp)⟧ ⟹
        Cong (Geos (ang2) add Emp) (Geos (ang1) add Emp)"
    and Ang_roll : "Cong (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p3 p2 p1)) add Emp)
        ∧ Eq (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p3 p2 p1)) add Emp)"
    and Ang_inside_def : "Ang_inside (An p1 p2 p3) p ⟷ Def (Ang (An p1 p2 p3)) ∧ Plane_sameside (Li p2 p1) p3 p ∧ Plane_sameside (Li p2 p3) p1 p"
    and Ang_Point_swap : "⟦Def (Ang (An p1 p2 p3)); Line_on (Li p2 p1) p4; ¬ Bet_Point (Se p1 p4) p2;
        Line_on (Li p2 p3) p5; ¬ Bet_Point (Se p3 p5) p2; ¬ Eq (Geos (Poi p2) add Emp) (Geos (Poi p4) add Emp);
        ¬ Eq (Geos (Poi p2) add Emp) (Geos (Poi p5) add Emp)⟧ ⟹ 
        Eq (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p5)) add Emp) ∧ Def (Ang (An p4 p2 p5))"
    and Ang_Right_angle_def : "Right_angle (An p1 p2 p3) ⟷
        (∃p. Cong (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p1 p2 p)) add Emp)
        ∧ Bet_Point (Se p3 p) p2 ∧ Def (Ang (An p1 p2 p3)) ∧ Def (Ang (An p1 p2 p)))"
    and Tri_Cong_def : "Cong (Geos (Tri (Tr p11 p12 p13)) add Emp) (Geos (Tri (Tr p21 p22 p23)) add Emp) 
        ⟷ Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
        ∧ Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p23)) add Emp)
        ∧ Eq (Geos (Seg (Se p13 p11)) add Emp) (Geos (Seg (Se p23 p21)) add Emp)
        ∧ Cong (Geos (Ang (An p12 p11 p13)) add Emp) (Geos (Ang (An p22 p21 p23)) add Emp)
        ∧ Cong (Geos (Ang (An p13 p12 p11)) add Emp) (Geos (Ang (An p23 p22 p21)) add Emp)
        ∧ Cong (Geos (Ang (An p11 p13 p12)) add Emp) (Geos (Ang (An p21 p23 p22)) add Emp)"
    and Ang_greater_def : "⟦Cong (Geos (Ang an1) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp);
        Plane_sameside (Li p2 p3) p4 p1⟧ ⟹
        Ang_inside (An p1 p2 p3) p4 ⟷ Gr (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang an1) add Emp)"
    and Ang_less_def : "⟦Cong (Geos (Ang an1) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp);
        Plane_sameside (Li p2 p3) p4 p1; ¬ Ang_inside (An p1 p2 p3) p4;
        ¬ Eq (Geos (Lin (Li p2 p1)) add Emp) (Geos (Lin (Li p2 p4)) add Emp)⟧ ⟹ 
        Gr (Geos (Ang an1) add Emp) (Geos (Ang (An p1 p2 p3)) add Emp)"
        
locale Axiom_3 = Definition_3 +
  assumes Seg_add : "⟦Line_on l1 p11; Line_on l1 p12; Line_on l1 p13; ¬ Seg_on_Seg (Se p11 p12) (Se p12 p13);
        Line_on l2 p21; Line_on l2 p22; Line_on l2 p23; ¬ Seg_on_Seg (Se p21 p22) (Se p22 p23);
        Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp);
        Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p23)) add Emp)⟧ ⟹
        Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)"
    and Seg_sub : "⟦Line_on l1 p11; Line_on l1 p12; Line_on l1 p13; ¬ Seg_on_Seg (Se p11 p12) (Se p12 p13);
        Line_on l2 p21; Line_on l2 p22; Line_on l2 p23; ¬ Seg_on_Seg (Se p21 p22) (Se p22 p23);
        Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)⟧ ⟹
        Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
        ∧ Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p23)) add Emp)"
    and Ang_move_sameside : "⟦¬ Line_on (Li p1 p2) p3; Def (Ang a1)⟧ ⟹ ∃p. Cong (Geos (Ang a1) add Emp) (Geos (Ang (An p p1 p2)) add Emp) ∧ Plane_sameside (Li p1 p2) p p3"
    and Ang_move_diffside : "⟦¬ Line_on (Li p1 p2) p3; Def (Ang a1)⟧ ⟹ ∃p. Cong (Geos (Ang a1) add Emp) (Geos (Ang (An p p1 p2)) add Emp) ∧ Plane_diffside (Li p1 p2) p p3"
    and Ang_move_unique : "⟦Cong (Geos (Ang an1) add Emp) (Geos (Ang (An p1 p2 p3)) add Emp);
        Cong (Geos (Ang an1) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp);
        Plane_sameside (Li p2 p3) p1 p4⟧ ⟹
        Eq (Geos (Lin (Li p1 p2)) add Emp) (Geos (Lin (Li p4 p2)) add Emp) ∧ ¬ Bet_Point (Se p1 p4) p2"
    and Tri_week_SAS : "⟦Def (Tri (Tr p11 p12 p13)); Def (Tri (Tr p21 p22 p23));
        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);
        Cong (Geos (Ang (An p12 p11 p13)) add Emp) (Geos (Ang (An p22 p21 p23)) add Emp)⟧
        ⟹ Cong (Geos (Ang (An p13 p12 p11)) add Emp) (Geos (Ang (An p23 p22 p21)) add Emp)"

locale Congruence_Rule = Axiom_3 +
  assumes Ang_weektrans : "⟦Eq (Geos (Ang an1) add Emp) (Geos (Ang an2) add Emp);
        Cong (Geos (Ang an2) add Emp) (Geos (Ang an3) add Emp)⟧ ⟹ Cong (Geos (Ang an1) add Emp) (Geos (Ang an3) add Emp)"

lemma (in Congruence_Rule) Seg_Bet_add : 
  assumes 
    "Bet_Point (Se p11 p13) p12"
    "Bet_Point (Se p21 p23) p22"
    "Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)"
    "Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p23)) add Emp)"
  shows "Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)"
proof -
  from assms have "∃l. Line_on l p11 ∧ Line_on l p13 ∧ Line_on l p12" by (simp add:Line_Bet_exist)
  then obtain l1 :: Line where P1 : "Line_on l1 p11 ∧ Line_on l1 p13 ∧ Line_on l1 p12" by blast
  from assms have "∃l. Line_on l p21 ∧ Line_on l p23 ∧ Line_on l p22" by (simp add:Line_Bet_exist)
  then obtain l2 :: Line where P2 : "Line_on l2 p21 ∧ Line_on l2 p23 ∧ Line_on l2 p22" by blast
  from assms have P3 : "¬ Seg_on_Seg (Se p11 p12) (Se p12 p13)" by (simp add:Seg_Bet_not_on)
  from assms have P4 : "¬ Seg_on_Seg (Se p21 p22) (Se p22 p23)" by (simp add:Seg_Bet_not_on)
  from assms P1 P2 P3 P4 show "Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)" by (blast intro:Seg_add)
qed

lemma (in Congruence_Rule) Tri_sinple_def :
  assumes 
    "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)"
    "¬ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)"
    "¬ Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)"
    "¬ Line_on (Li A B) C"
  shows "Def (Tri (Tr A B C))"
proof -
  have P1 : "Bet_Point (Se A B) C ⟹ Line_on (Li A B) C" by (simp add:Line_Bet_on)
  from assms P1 have P2 : "¬ Bet_Point (Se A B) C" by blast 
  from assms have P3 : "¬ Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)" by (blast intro:Eq_rev)
  from P3 have P4 : "Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li A B)) add Emp)" by (simp add:Line_rev)
  have P5 : "Bet_Point (Se B C) A ⟹ Line_on (Li A B) C" by (simp add:Line_Bet_on)
  from assms P5 have P6 : "¬ Bet_Point (Se B C) A" by blast 
  have P7 : "Bet_Point (Se C A) B ⟹ Line_on (Li A B) C" by (simp add:Line_Bet_on)
  from assms P7 have P8 : "¬ Bet_Point (Se C A) B" by blast 
  have "Seg_on_Seg (Se A B) (Se B C) ⟹ ∃p. Bet_Point (Se A B) p ∧ Bet_Point (Se B C) p" by (simp add:Seg_on_Seg_rule)
  then obtain D :: Point where P9 : "Seg_on_Seg (Se A B) (Se B C) ⟹ Bet_Point (Se A B) D ∧ Bet_Point (Se B C) D" by blast
  have P10 : "Line_on (Li A B) B" by (simp add:Line_on_rule)
  from P9 have P11 : "Seg_on_Seg (Se A B) (Se B C) ⟹ Line_on (Li A B) D" by (simp add:Line_Bet_on)
  have P12 : "Line_on (Li B C) B" by (simp add:Line_on_rule)
  from P9 have P13 : "Seg_on_Seg (Se A B) (Se B C) ⟹ Line_on (Li B C) D" by (simp add:Line_Bet_on)
  from P9 have "Seg_on_Seg (Se A B) (Se B C) ⟹ Bet_Point (Se A B) D" by simp
  then have P14 : "Seg_on_Seg (Se A B) (Se B C) ⟹ ¬ Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)" by (simp add:Bet_Point_def)
  from P10 P11 P12 P13 P14 have P15 : "Seg_on_Seg (Se A B) (Se B C) ⟹ Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li A B)) add Emp)" by (simp add:Line_unique)
  have P16 : "Line_on (Li B C) C" by (simp add:Line_on_rule)
  from P15 P16 have P17 : "Seg_on_Seg (Se A B) (Se B C) ⟹ Line_on (Li A B) C" by (simp add:Line_on_trans)
  from assms P17 have P18 : "¬ Seg_on_Seg (Se A B) (Se B C)" by blast 
  have "Seg_on_Seg (Se B C) (Se C A) ⟹ ∃p. Bet_Point (Se B C) p ∧ Bet_Point (Se C A) p" by (simp add:Seg_on_Seg_rule)
  then obtain E :: Point where P19 : "Seg_on_Seg (Se B C) (Se C A) ⟹ Bet_Point (Se B C) E ∧ Bet_Point (Se C A) E" by blast
  then have P20 : "Seg_on_Seg (Se B C) (Se C A) ⟹ Line_on (Li B C) E" by (simp add:Line_Bet_on)
  have P21 : "Line_on (Li C A) C" by (simp add:Line_on_rule)
  from P19 have P22 : "Seg_on_Seg (Se B C) (Se C A) ⟹ Line_on (Li C A) E" by (simp add:Line_Bet_on)
  from P19 have "Seg_on_Seg (Se B C) (Se C A) ⟹ Bet_Point (Se B C) E" by simp
  then have P23 : "Seg_on_Seg (Se B C) (Se C A) ⟹ ¬ Eq (Geos (Poi C) add Emp) (Geos (Poi E) add Emp)" by (simp add:Bet_Point_def)
  from P16 P20 P21 P22 P23 have P24 : "Seg_on_Seg (Se B C) (Se C A) ⟹ Eq (Geos (Lin (Li C A)) add Emp) (Geos (Lin (Li B C)) add Emp)" by (simp add:Line_unique)
  have P25 : "Line_on (Li C A) A" by (simp add:Line_on_rule)
  from P24 P25 have P26 : "Seg_on_Seg (Se B C) (Se C A) ⟹ Line_on (Li B C) A" by (simp add:Line_on_trans)
  from assms P3 P26 have P27 : "Seg_on_Seg (Se B C) (Se C A) ⟹ Line_on (Li B A) C" by (blast intro:Line_on_rev)
  from P4 P27 have P28 : "Seg_on_Seg (Se B C) (Se C A) ⟹ Line_on (Li A B) C" by (simp add:Line_on_trans)
  from assms P28 have P29 : "¬ Seg_on_Seg (Se B C) (Se C A)" by blast 
  have "Seg_on_Seg (Se C A) (Se A B) ⟹ ∃p. Bet_Point (Se C A) p ∧ Bet_Point (Se A B) p" by (simp add:Seg_on_Seg_rule)
  then obtain F :: Point where P30 : "Seg_on_Seg (Se C A) (Se A B) ⟹ Bet_Point (Se C A) F ∧ Bet_Point (Se A B) F" by blast
  then have P31 : "Seg_on_Seg (Se C A) (Se A B) ⟹ Line_on (Li C A) F" by (simp add:Line_Bet_on)
  have P32 : "Line_on (Li A B) A" by (simp add:Line_on_rule)
  from P30 have P33 : "Seg_on_Seg (Se C A) (Se A B) ⟹ Line_on (Li A B) F" by (simp add:Line_Bet_on)
  from P30 have "Seg_on_Seg (Se C A) (Se A B) ⟹ Bet_Point (Se C A) F" by simp
  then have P34 : "Seg_on_Seg (Se C A) (Se A B) ⟹ ¬ Eq (Geos (Poi A) add Emp) (Geos (Poi F) add Emp)" by (simp add:Bet_Point_def)
  from P25 P31 P32 P33 P34 have P35 : "Seg_on_Seg (Se C A) (Se A B) ⟹ Eq (Geos (Lin (Li C A)) add Emp) (Geos (Lin (Li A B)) add Emp)" by (simp add:Line_unique)
  from P21 P35 have P36 : "Seg_on_Seg (Se C A) (Se A B) ⟹ Line_on (Li A B) C" by (simp add:Line_on_trans)
  from assms P36 have P37 : "¬ Seg_on_Seg (Se C A) (Se A B)" by blast
  from assms P2 P6 P8 P18 P29 P37 show "Def (Tri (Tr A B C))" by (simp add:Tri_def)
qed

lemma (in Congruence_Rule) Tri_def_Line :
  assumes 
    "Def (Tri (Tr A B C))"
  shows "¬ Line_on (Li A B) C ∧ ¬ Line_on (Li B C) A ∧ ¬ Line_on (Li C A) B"
proof -
  from assms have P1 : "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
        ∧ ¬ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) ∧ ¬ Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
        ∧ ¬ Bet_Point (Se A B) C ∧ ¬ Bet_Point (Se B C) A ∧ ¬ Bet_Point (Se C A) B" by (simp add:Tri_def)
  have P2 : "Line_on (Li A B) B" by (simp add:Line_on_rule)
  have P3 : "Line_on (Li A B) A" by (simp add:Line_on_rule)
  from P1 P2 P3 have P4 : "Line_on (Li A B) C ⟹ Bet_Point (Se A C) B ∨ Bet_Point (Se C B) A ∨ Bet_Point (Se B A) C" by (simp add:Bet_case)
  from P1 have P5 : "¬ Bet_Point (Se A C) B" by (blast intro:Bet_rev)
  from P1 have P6 : "¬ Bet_Point (Se C B) A" by (blast intro:Bet_rev)
  from P1 have P7 : "¬ Bet_Point (Se B A) C" by (blast intro:Bet_rev)
  from P4 P5 P6 P7 have P8 : "¬ Line_on (Li A B) C" by blast 
  have P9 : "Line_on (Li B C) B" by (simp add:Line_on_rule)
  have P10 : "Line_on (Li B C) C" by (simp add:Line_on_rule)
  from P1 P9 P10 have P11 : "Line_on (Li B C) A ⟹ Bet_Point (Se A C) B ∨ Bet_Point (Se C B) A ∨ Bet_Point (Se B A) C" by (simp add:Bet_case)
  from P5 P6 P7 P11 have P12 : "¬ Line_on (Li B C) A" by blast 
  have P13 : "Line_on (Li C A) C" by (simp add:Line_on_rule)
  have P14 : "Line_on (Li C A) A" by (simp add:Line_on_rule)
  from P1 P13 P14 have P15 : "Line_on (Li C A) B ⟹ Bet_Point (Se A C) B ∨ Bet_Point (Se C B) A ∨ Bet_Point (Se B A) C" by (simp add:Bet_case)
  from P5 P6 P7 P15 have P16 : "¬ Line_on (Li C A) B" by blast 
  from P8 P12 P16 show "¬ Line_on (Li A B) C ∧ ¬ Line_on (Li B C) A ∧ ¬ Line_on (Li C A) B" by simp
qed

lemma (in Congruence_Rule) Tri_def_trans :
  assumes 
    "Def (Tri (Tr A B C))"
  shows "Def (Tri (Tr B C A))"
proof -
  from assms have P1 : "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
        ∧ ¬ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) ∧ ¬ Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
        ∧ ¬ Bet_Point (Se A B) C ∧ ¬ Bet_Point (Se B C) A ∧ ¬ Bet_Point (Se C A) B" by (simp add:Tri_def)
  from assms have P2 : "¬ Line_on (Li B C) A" by (simp add:Tri_def_Line)
  from P1 P2 show "Def (Tri (Tr B C A))" by (simp add:Tri_sinple_def)
qed

lemma (in Congruence_Rule) Tri_def_rev :
  assumes 
    "Def (Tri (Tr A B C))"
  shows "Def (Tri (Tr C B A))"
proof -
  from assms have P1 : "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
        ∧ ¬ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) ∧ ¬ Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
        ∧ ¬ Bet_Point (Se A B) C ∧ ¬ Bet_Point (Se B C) A ∧ ¬ Bet_Point (Se C A) B" by (simp add:Tri_def)
  from assms have P2 : "¬ Line_on (Li B C) A" by (simp add:Tri_def_Line)
  from P1 have P3 : "Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li C B)) add Emp)" by (simp add:Line_rev)
  from P2 P3 have P4 : "¬ Line_on (Li C B) A" by (simp add:Line_not_on_trans)
  from P1 have P5 : "¬ Eq (Geos (Poi C) add Emp) (Geos (Poi B) add Emp)" by (blast intro:Eq_rev)
  from P1 have P6 : "¬ Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)" by (blast intro:Eq_rev)
  from P1 have P7 : "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)" by (blast intro:Eq_rev)
  from P4 P5 P6 P7 show "Def (Tri (Tr C B A))" by (simp add:Tri_sinple_def)
qed

lemma (in Congruence_Rule) Tri_def_extension :
  assumes 
    "Def (Tri (Tr A B C))"
    "¬ Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)"
    "Line_on (Li B C) D"
  shows "Def (Tri (Tr A B D))"
proof -
  from assms have P1 : "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)" by (simp add:Tri_def)
  from assms have P2 : "¬ Line_on (Li B C) A" by (simp add:Tri_def_Line)
  from assms have P3 : "Eq (Geos (Poi D) add Emp) (Geos (Poi A) add Emp) ⟹ Line_on (Li B C) A" by (simp add:Point_Eq)
  from P2 P3 have P4 : "¬ Eq (Geos (Poi D) add Emp) (Geos (Poi A) add Emp)" by blast
  from assms have P5 : "¬ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)" by (simp add:Tri_def)
  from assms P5 have P6 : "Line_on (Li B D) C" by (simp add:Line_on_rev)
  have P7 : "Line_on (Li B D) B" by (simp add:Line_on_rule)
  have P8 : "Line_on (Li B C) B" by (simp add:Line_on_rule)
  have P9 : "Line_on (Li B C) C" by (simp add:Line_on_rule)
  from P5 P6 P7 P8 P9 have "Eq (Geos (Lin (Li B D)) add Emp) (Geos (Lin (Li B C)) add Emp)" by (simp add:Line_unique)
  then have P10 : "Line_on (Li B D) A ⟹ Line_on (Li B C) A" by (simp add:Line_on_trans)
  from P2 P10 have P11 : "¬ Line_on (Li B D) A" by blast
  from assms P1 P4 P11 have "Def (Tri (Tr B D A))" by (simp add:Tri_sinple_def)
  thus "Def (Tri (Tr A B D))" by (simp add:Tri_def_trans)
qed

lemma (in Congruence_Rule) Ang_to_Tri : 
  assumes 
    "Def (Ang (An A B C))"
  shows "Def (Tri (Tr A B C))"
proof -
  from assms have P1 : "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
    ∧ ¬ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) ∧ ¬ Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
    ∧ ¬ Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)" by (simp add:Ang_def)
  have P2 : "Line_on (Li B A) B" by (simp add:Line_on_rule)
  have P3 : "Line_on (Li B C) B" by (simp add:Line_on_rule)
  have P4 : "Line_on (Li B C) C" by (simp add:Line_on_rule)
  from P1 have P5 : "¬ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)" by simp
  from P1 have "Eq (Geos (Lin (Li A B)) add Emp) (Geos (Lin (Li B A)) add Emp)" by (simp add:Line_rev)
  then have P6 : "Line_on (Li A B) C ⟹ Line_on (Li B A) C" by (simp add:Line_on_trans)
  from P2 P3 P4 P5 P6 have P7 : "Line_on (Li A B) C ⟹ Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)" by (simp add:Line_unique)
  from P1 P7 have P8 : "¬ Line_on (Li A B) C" by blast
  from P1 P8 show "Def (Tri (Tr A B C))" by (simp add:Tri_sinple_def)
qed

lemma (in Congruence_Rule) Ang_sinple_def : 
  assumes 
    "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)"
    "¬ Line_on (Li A B) C"
  shows "Def (Ang (An A B C))"
proof -
  from assms have P1 : "Eq (Geos (Lin (Li A B)) add Emp) (Geos (Lin (Li B A)) add Emp)" by (simp add:Line_rev)
  from assms P1 have P2 : "¬ Line_on (Li B A) C" by (simp add:Line_not_on_trans)
  have "Line_on (Li B A) B" by (simp add:Line_on_rule)
  then have P3 : "Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) ⟹ Line_on (Li B A) C" by (simp add:Point_Eq)
  from P2 P3 have P4 : "¬ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)" by blast
  have "Line_on (Li B A) A" by (simp add:Line_on_rule)
  then have P5 : "Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp) ⟹ Line_on (Li B A) C" by (simp add:Point_Eq)
  from P2 P5 have P6 : "¬ Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)" by (blast intro:Eq_rev)
  have "Line_on (Li B C) C" by (simp add:Line_on_rule)
  then have P7 : "Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li B A)) add Emp) ⟹ Line_on (Li B A) C" by (simp add:Line_on_trans)
  from P2 P7 have P8 : "¬ Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)" by (blast intro:Eq_rev)
  from assms P4 P6 P8 show "Def (Ang (An A B C))" by (simp add:Ang_def)
qed

lemma (in Congruence_Rule) Tri_to_Ang : 
  assumes
    "Def (Tri (Tr A B C))"
  shows "Def (Ang (An A B C))"
proof -
  from assms have P1 : "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
    ∧ ¬ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) ∧ ¬ Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)" by (simp add:Tri_def)
  from assms have P2 : "¬ Line_on (Li A B) C" by (simp add:Tri_def_Line)
  from P1 P2 show "Def (Ang (An A B C))" by (simp add:Ang_sinple_def)
qed

lemma (in Congruence_Rule) Ang_def_rev : 
  assumes 
    "Def (Ang (An A B C))"
  shows "Def (Ang (An C B A))"
proof -
  from assms have P1 : "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
    ∧ ¬ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) ∧ ¬ Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
    ∧ ¬ Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)" by (simp add:Ang_def)
  have P2 : "Line_on (Li B A) A" by (simp add:Line_on_rule)
  have P3 : "Line_on (Li B A) B" by (simp add:Line_on_rule)
  have P4 : "Line_on (Li B C) B" by (simp add:Line_on_rule)
  from P1 have P5 : "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)" by simp
  from P2 P3 P4 P5 have P6 : "Line_on (Li B C) A ⟹ Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)" by (simp add:Line_unique)
  from P1 P6 have P7 : "¬ Line_on (Li B C) A" by blast
  from P1 have P8 : "Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li C B)) add Emp)" by (simp add:Line_rev)
  from P7 P8 have P9 : "¬ Line_on (Li C B) A" by (simp add:Line_not_on_trans)
  from P1 have P10 : "¬ Eq (Geos (Poi C) add Emp) (Geos (Poi B) add Emp)" by (blast intro:Eq_rev)
  from P9 P10 show "Def (Ang (An C B A))" by (simp add:Ang_sinple_def)
qed

lemma (in Congruence_Rule) Ang_def_inv : 
  assumes 
    "Def (Ang (An A B C))"
  shows "Def (Ang (An A C B))"
proof -
  from assms have P1 : "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
    ∧ ¬ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) ∧ ¬ Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
    ∧ ¬ Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)" by (simp add:Ang_def)
  have P2 : "Line_on (Li B A) A" by (simp add:Line_on_rule)
  have P3 : "Line_on (Li B A) B" by (simp add:Line_on_rule)
  have P4 : "Line_on (Li B C) B" by (simp add:Line_on_rule)
  from P1 have P5 : "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)" by simp
  from P2 P3 P4 P5 have P6 : "Line_on (Li B C) A ⟹ Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)" by (simp add:Line_unique)
  from P1 P6 have P7 : "¬ Line_on (Li B C) A" by blast
  have P8 : "Line_on (Li A C) C" by (simp add:Line_on_rule)
  have P9 : "Line_on (Li B C) C" by (simp add:Line_on_rule)
  from P1 P4 P8 P9 have P10 : "Line_on (Li A C) B ⟹ Eq (Geos (Lin (Li A C)) add Emp) (Geos (Lin (Li B C)) add Emp)" by (simp add:Line_unique)
  have P11 : "Line_on (Li A C) A" by (simp add:Line_on_rule)  
  from P10 P11 have P12 : "Line_on (Li A C) B ⟹ Line_on (Li B C) A" by (simp add:Line_on_trans)
  from P7 P12 have P13 : "¬ Line_on (Li A C) B" by blast
  from P1 have P14 : "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)" by (blast intro:Eq_rev)
  from P13 P14 show "Def (Ang (An A C B))" by (simp add:Ang_sinple_def)
qed

lemma (in Congruence_Rule) Ang_def_extension : 
  assumes 
    "Def (Ang (An A B C))"
    "¬ Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)"
    "Line_on (Li B C) D"
  shows "Def (Ang (An A B D))"
proof -
  from assms have P1 : "Def (Tri (Tr A B C))" by (simp add:Ang_to_Tri)
  from assms P1 have "Def (Tri (Tr A B D))" by (simp add:Tri_def_extension)
  thus "Def (Ang (An A B D))" by (simp add:Tri_to_Ang)
qed

lemma (in Congruence_Rule) Bet_end_Point :
  shows "¬ Bet_Point (Se p1 p1) p2"
proof 
  assume W : "Bet_Point (Se p1 p1) p2"
  then have P1 : "¬ Eq (Geos (Poi p1) add Emp) (Geos (Poi p1) add Emp)" by (simp add:Bet_Point_def del:Eq_refl)
  have P2 : "Eq (Geos (Poi p1) add Emp) (Geos (Poi p1) add Emp)" by simp
  from P1 P2 show False by blast
qed

lemma (in Congruence_Rule) Seg_Plane_sameside :
  assumes 
    "Line_on l1 A"
    "Line_on l1 B"
    "Line_on l1 C"
    "¬ Line_on l1 D"
    "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)"
    "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)"
    "¬ Bet_Point (Se B C) A"
  shows "Plane_sameside (Li D A) B C ∨ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)"
proof -
  have "Line_on (Li D A) D" by (simp add:Line_on_rule)
  then have P1 : "Eq (Geos (Lin (Li D A)) add Emp) (Geos (Lin l1) add Emp) ⟹ Line_on l1 D" by (simp add:Line_on_trans)
  from assms P1 have P2 : "¬ Eq (Geos (Lin (Li D A)) add Emp) (Geos (Lin l1) add Emp)" by blast
  have "Plane_diffside (Li D A) B C ⟹ ∃p. Bet_Point (Se B C) p ∧ Line_on (Li D A) p ∧ ¬ Line_on (Li D A) B ∧ ¬ Line_on (Li D A) C" by (simp add:Plane_diffside_def)
  then obtain E :: Point where P3 : "Plane_diffside (Li D A) B C ⟹ Bet_Point (Se B C) E ∧ Line_on (Li D A) E" by blast
  then have P4 : "Plane_diffside (Li D A) B C ⟹ Line_on (Li B C) E" by (simp add:Line_Bet_on)
  have P5 : "Line_on (Li B C) B" by (simp add:Line_on_rule)
  have P6 : "Line_on (Li B C) C" by (simp add:Line_on_rule)
  from assms P5 P6 have P7 : "¬ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) ⟹ Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin l1) add Emp)" by (simp add:Line_unique)
  from P4 P7 have P8 : "Plane_diffside (Li D A) B C ⟹ ¬ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) ⟹ 
    Line_on l1 E" by (simp add:Line_on_trans)
  have P9 : "Line_on (Li D A) A" by (simp add:Line_on_rule)
  from assms P2 P3 P8 P9 have P10 : "Plane_diffside (Li D A) B C ⟹ ¬ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) ⟹ 
    Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp)" by (simp add:Line_unique_Point)
  from P3 have P11 : "Plane_diffside (Li D A) B C ⟹ Bet_Point (Se B C) E" by simp
  from P10 P11 have P12 : "Plane_diffside (Li D A) B C ⟹ ¬ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) ⟹
    Bet_Point (Se B C) A" by (simp add:Point_Eq)
  from assms P12 have "¬ Plane_diffside (Li D A) B C ∨ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)" by blast
  then have P13 : "¬ Plane_diffside (Li D A) B C ∧ ¬ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) 
    ∨ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)" by blast
  from assms P9 have P14 : "Line_on (Li D A) B ⟹ Eq (Geos (Lin (Li D A)) add Emp) (Geos (Lin l1) add Emp)" by (simp add:Line_unique)
  from P2 P14 have P15 : "¬ Line_on (Li D A) B" by blast
  from assms P9 have P16 : "Line_on (Li D A) C ⟹ Eq (Geos (Lin (Li D A)) add Emp) (Geos (Lin l1) add Emp)" by (simp add:Line_unique)
  from P2 P16 have P17 : "¬ Line_on (Li D A) C" by blast
  from P15 P17 have P18 : "¬ Plane_diffside (Li D A) B C ∧ ¬ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) ⟹
    Plane_sameside (Li D A) B C" by (simp add:Plane_not_diffside_sameside)
  from P13 P18 show "Plane_sameside (Li D A) B C ∨ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)" by blast
qed

lemma (in Congruence_Rule) Seg_move_unique :
  assumes 
    "Line_on l1 A"
    "Line_on l1 B"
    "Line_on l1 C"
    "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)"
    "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)"
    "Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)"
    "¬ Bet_Point (Se B C) A"
  shows "Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)"
proof -
  have "∃p q r. ¬ Line_on l1 p ∧ ¬ Line_on l1 q ∧ ¬ Line_on l1 r
        ∧ ¬ Eq (Geos (Poi p) add Emp) (Geos (Poi q) add Emp) ∧ ¬ Eq (Geos (Poi q) add Emp) (Geos (Poi r) add Emp)
        ∧ ¬ Eq (Geos (Poi r) add Emp) (Geos (Poi p) add Emp)" by (blast intro:Line_not_on_exist)
  then obtain D :: Point where P1 : "¬ Line_on l1 D" by blast
  have P2 : "Line_on (Li A D) D" by (simp add:Line_on_rule)
  have P3 : "Line_on (Li A B) A" by (simp add:Line_on_rule)
  have P4 : "Line_on (Li A B) B" by (simp add:Line_on_rule)
  from assms P3 P4 have P5 : "Eq (Geos (Lin l1) add Emp) (Geos (Lin (Li A B)) add Emp)" by (simp add:Line_unique)
  from assms P5 have P6 : "Line_on (Li A B) C" by (simp add:Line_on_trans)
  from P1 P5 have P7 : "¬ Line_on (Li A B) D" by (simp add:Line_not_on_trans)
  from assms P7 have "Def (Ang (An A B D))" by (simp add:Ang_sinple_def)
  then have P8 : "Def (Ang (An D A B))" by (blast intro:Ang_def_rev Ang_def_inv)
  then have "¬ Eq (Geos (Poi D) add Emp) (Geos (Poi A) add Emp)" by (simp add:Ang_def)
  then have P9 : "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)" by (blast intro:Eq_rev)
  have P10 : "¬ Bet_Point (Se D D) A" by (simp add:Bet_end_Point)
  from assms P2 P6 P8 P9 P10 have "Eq (Geos (Ang (An D A B)) add Emp) (Geos (Ang (An D A C)) add Emp)" by (simp add:Ang_Point_swap)
  then have P11 : "Cong (Geos (Ang (An D A B)) add Emp) (Geos (Ang (An D A C)) add Emp)" by (simp add:Ang_weektrans)
  from assms P7 have "Def (Tri (Tr A B D))" by (blast intro:Ang_sinple_def Ang_to_Tri)
  then have "Def (Tri (Tr D B A))" by (simp add:Tri_def_rev)
  then have P12 : "Def (Tri (Tr A D B))" by (simp add:Tri_def_trans)
  have P13 : "Line_on (Li A C) A" by (simp add:Line_on_rule)
  have P14 : "Line_on (Li A C) C" by (simp add:Line_on_rule)
  from assms P13 P14 have P15 : "Eq (Geos (Lin l1) add Emp) (Geos (Lin (Li A C)) add Emp)" by (simp add:Line_unique)
  from P1 P15 have P16 : "¬ Line_on (Li A C) D" by (simp add:Line_not_on_trans)
  from assms P16 have "Def (Tri (Tr A C D))" by (blast intro:Ang_sinple_def Ang_to_Tri)
  then have "Def (Tri (Tr D C A))" by (simp add:Tri_def_rev)
  then have P17 : "Def (Tri (Tr A D C))" by (simp add:Tri_def_trans)
  from assms P11 P12 P17 have P18 : "Cong (Geos (Ang (An B D A)) add Emp) (Geos (Ang (An C D A)) add Emp)" by (simp add:Tri_week_SAS)
  have P19 : "Cong (Geos (Ang (An A D B)) add Emp) (Geos (Ang (An B D A)) add Emp)" by (simp add:Ang_roll)
  have P20 : "Eq (Geos (Ang (An B D A)) add Emp) (Geos (Ang (An A D B)) add Emp)" by (simp add:Ang_roll)
  from P18 P20 have P21 : "Cong (Geos (Ang (An A D B)) add Emp) (Geos (Ang (An C D A)) add Emp)" by (blast intro:Ang_weektrans Eq_rev)
  from assms P1 have P22 : "Plane_sameside (Li D A) B C ∨ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)" by (simp add:Seg_Plane_sameside)
  from P19 P21 have P23 : "Plane_sameside (Li D A) B C ⟹ Eq (Geos (Lin (Li B D)) add Emp) (Geos (Lin (Li C D)) add Emp)" by (simp add:Ang_move_unique)
  have P24 : "Line_on (Li B D) B" by (simp add:Line_on_rule)
  from P23 P24 have P25 : "Plane_sameside (Li D A) B C ⟹ Line_on (Li C D) B" by (simp add:Line_on_trans)
  have P26 : "Line_on (Li B C) B" by (simp add:Line_on_rule)
  have P27 : "Line_on (Li B C) C" by (simp add:Line_on_rule)
  have P28 : "Line_on (Li C D) C" by (simp add:Line_on_rule)
  from P25 P26 P27 P28 have P29 : "Plane_sameside (Li D A) B C ⟹ ¬ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) ⟹
    Eq (Geos (Lin (Li C D)) add Emp) (Geos (Lin (Li B C)) add Emp)" by (simp add:Line_unique)
  have P30 : "Line_on (Li C D) D" by (simp add:Line_on_rule)
  from P29 P30 have P31 : "Plane_sameside (Li D A) B C ⟹ ¬ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) ⟹
    Line_on (Li B C) D" by (simp add:Line_on_trans)
  from assms P26 P27 have P32 : "¬ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) ⟹ Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin l1) add Emp)" by (simp add:Line_unique)
  from P31 P32 have P33 : "Plane_sameside (Li D A) B C ⟹ ¬ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) ⟹
    Line_on l1 D" by (simp add:Line_on_trans)
  from P1 P33 have P34 : "Plane_sameside (Li D A) B C ⟹ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)" by blast
  from P22 P34 show "Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)" by blast
qed

lemma (in Congruence_Rule) Seg_not_Eq_Point :
  assumes 
    "¬ Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)"
  shows "¬ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)"
proof -
  have P1 : "Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) ⟹ 
    Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)" by (simp add:Seg_Point_Eq)
  from assms P1 show "¬ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)" by blast
qed

lemma (in Congruence_Rule) Ang_replace : 
  assumes 
    "Def (Ang (An A B C))"
    "Def (Ang (An A1 B1 C1))"
    "Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)"
  shows "∃p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp)
    ∧ Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp)
    ∧ Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) ∧ Line_on (Li B1 A1) p ∧ ¬ Bet_Point (Se p A1) B1 ∧ Def (Ang (An p B1 C1))"
    and "∃p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp)
    ∧ Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp)
    ∧ Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) ∧ Line_on (Li B1 C1) p ∧ ¬ Bet_Point (Se p C1) B1 ∧ Def (Ang (An A1 B1 p))"
    and "∃p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp)
    ∧ Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp) 
    ∧ Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) ∧ Line_on (Li B1 A1) p ∧ ¬ Bet_Point (Se p A1) B1
    ∧ Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) ∧ Line_on (Li B1 C1) q ∧ ¬ Bet_Point (Se q C1) B1 ∧ Def (Ang (An p B1 q))"
proof -
  from assms have P1 : "¬ Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)" by (simp add:Ang_def)
  then have P2 : "¬ Eq (Geos (Poi B1) add Emp) (Geos (Poi A1) add Emp)" by (blast intro:Eq_rev)
  have P3 : "Line_on (Li B1 A1) A1" by (simp add:Line_on_rule)
  have P4 : "Line_on (Li B1 A1) B1" by (simp add:Line_on_rule)
  from assms have "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)" by (simp add:Ang_def)
  then have P5 : "¬ Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)" by (blast intro:Eq_rev)
  from P2 P3 P4 P5 have "∃p. Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) ∧ ¬ Bet_Point (Se p A1) B1 ∧ Line_on (Li B1 A1) p ∧ ¬ Eq (Geos (Poi B1) add Emp) (Geos (Poi p) add Emp)" by (simp add:Seg_move_sameside)
  then obtain A2 :: Point where P6 : "Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) ∧ ¬ Bet_Point (Se A2 A1) B1 ∧ Line_on (Li B1 A1) A2 ∧ ¬ Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)" by blast
  from assms have P7 : "¬ Eq (Geos (Poi B1) add Emp) (Geos (Poi C1) add Emp)" by (simp add:Ang_def)
  have P8 : "Line_on (Li B1 C1) B1" by (simp add:Line_on_rule)
  have P9 : "Line_on (Li B1 C1) C1" by (simp add:Line_on_rule)
  from assms have P10 : "¬ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)" by (simp add:Ang_def)
  from P7 P8 P9 P10 have "∃p. Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) ∧ ¬ Bet_Point (Se p C1) B1 ∧ Line_on (Li B1 C1) p ∧ ¬ Eq (Geos (Poi B1) add Emp) (Geos (Poi p) add Emp)" by (simp add:Seg_move_sameside)
  then obtain C2 :: Point where P11 : "Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) ∧ ¬ Bet_Point (Se C2 C1) B1 ∧ Line_on (Li B1 C1) C2 ∧ ¬ Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)" by blast
  have P12 : "¬ Bet_Point (Se C1 C1) B1" by (simp add:Bet_end_Point)
  from P6 have P13 : "¬ Bet_Point (Se A1 A2) B1" by (blast intro:Bet_rev)
  from assms P3 P6 P7 P9 P12 P13 have P14 : "Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B1 C1)) add Emp)" by (simp add:Ang_Point_swap)
  from assms P14 have P15 : "Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C1)) add Emp)" by (blast intro:Ang_weektrans Ang_rev Eq_rev)
  from assms have P16 : "¬ Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)" by (simp add:Ang_def)
  from P6 have P17 : "Line_on (Li B1 A1) A2" by simp
  from P6 have P18 : "¬ Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)" by simp
  from P4 P8 P17 P18 have P19 : "Line_on (Li B1 C1) A2 ⟹ Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)" by (simp add:Line_unique)
  from P16 P19 have P20 : "¬ Line_on (Li B1 C1) A2" by blast
  from P7 P20 have "Def (Ang (An B1 C1 A2))" by (simp add:Ang_sinple_def)
  then have P21 : "Def (Ang (An A2 B1 C1))" by (blast intro:Ang_def_rev Ang_def_inv)
  from P6 P14 P15 P21 show "∃p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp)
    ∧ Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp)
    ∧ Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) ∧ Line_on (Li B1 A1) p ∧ ¬ Bet_Point (Se p A1) B1 ∧ Def (Ang (An p B1 C1))" by blast
  have P22 : "¬ Bet_Point (Se A1 A1) B1" by (simp add:Bet_end_Point)
  from P11 have P23 : "¬ Bet_Point (Se C1 C2) B1" by (blast intro:Bet_rev)
  from assms P2 P3 P7 P11 P22 P23 have P24 : "Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 C2)) add Emp)" by (simp add:Ang_Point_swap)
  from assms P24 have P25 : "Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C2)) add Emp)" by (blast intro:Ang_weektrans Ang_rev Eq_rev)
  from P11 have P26 : "Line_on (Li B1 C1) C2" by simp
  from P11 have P27 : "¬ Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)" by simp
  from P4 P8 P26 P27 have P28 : "Line_on (Li B1 A1) C2 ⟹ Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)" by (simp add:Line_unique)
  from P16 P28 have P29: "¬ Line_on (Li B1 A1) C2" by blast
  from P2 P29 have "Def (Ang (An B1 A1 C2))" by (simp add:Ang_sinple_def)
  then have P30 : "Def (Ang (An A1 B1 C2))" by (blast intro:Ang_def_rev Ang_def_inv)
  from P11 P24 P25 P30 show "∃p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp)
    ∧ Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A1 B1 p)) add Emp) 
    ∧ Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) ∧ Line_on (Li B1 C1) p ∧ ¬ Bet_Point (Se p C1) B1 ∧ Def (Ang (An A1 B1 p))" by blast
  from assms P6 P11 P13 P17 P23 P26 have P31 : "Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B1 C2)) add Emp)" by (simp add:Ang_Point_swap)
  from assms P31 have P32 : "Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C2)) add Emp)" by (blast intro:Ang_weektrans Ang_rev Eq_rev)
  have P33 : "Line_on (Li B1 C2) B1" by (simp add:Line_on_rule)
  have P34 : "Line_on (Li B1 C2) C2" by (simp add:Line_on_rule)
  from P8 P26 P27 P33 P34 have "Eq (Geos (Lin (Li B1 C2)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)" by (simp add:Line_unique)
  then have P35 : "Line_on (Li B1 C2) A2 ⟹ Line_on (Li B1 C1) A2" by (simp add:Line_on_trans)
  from P20 P35 have P36 : "¬ Line_on (Li B1 C2) A2" by blast
  from P11 P36 have "Def (Ang (An B1 C2 A2))" by (simp add:Ang_sinple_def)
  then have P37 : "Def (Ang (An A2 B1 C2))" by (blast intro:Ang_def_rev Ang_def_inv)
  from P6 P11 P21 P30 P31 P32 P37 show "∃p q. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 q)) add Emp)
    ∧ Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 q)) add Emp)
    ∧ Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) ∧ Line_on (Li B1 A1) p ∧ ¬ Bet_Point (Se p A1) B1
    ∧ Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 q)) add Emp) ∧ Line_on (Li B1 C1) q ∧ ¬ Bet_Point (Se q C1) B1 ∧ Def (Ang (An p B1 q))"
  by blast
qed

text‹Theorem11›

theorem (in Congruence_Rule) Tri_isosceles: 
  assumes 
    "Def (Tri (Tr A B C))"
    "Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)"
  shows "Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp)"
proof -
  from assms have P1 : "Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se A B)) add Emp)" by (simp add:Eq_rev)
  have P2 : "Cong (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An C A B)) add Emp)" by (simp add:Ang_roll)
  from assms have "Def (Tri (Tr C B A))" by (simp add:Tri_def_rev)
  then have P3 : "Def (Tri (Tr A C B))" by (simp add:Tri_def_trans)
  from assms P1 P2 P3 have P4 : "Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An B C A)) add Emp)" by (simp add:Tri_week_SAS)
  have P5 : "Eq (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An A B C)) add Emp)" by (simp add:Ang_roll)
  from P4 P5 have P6 : "Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An B C A)) add Emp)" by (blast intro:Ang_weektrans Eq_rev)
  have P7 : "Eq (Geos (Ang (An B C A)) add Emp) (Geos (Ang (An A C B)) add Emp)" by (simp add:Ang_roll)
  from P6 P7 show "Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A C B)) add Emp)" by (blast intro:Ang_weektrans Eq_rev Ang_rev)
qed

lemma (in Congruence_Rule) Tri_week_ASA :
  assumes N :
    "Def (Tri (Tr A B C))"
    "Def (Tri (Tr A1 B1 C1))"
    "Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)"
    "Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C1 A1 B1)) add Emp)"
    "Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) add Emp)"
  shows "¬¬ Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp)"
proof 
  assume W : "¬ Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp)"
  have P1 : "Line_on (Li B1 C1) B1" by (simp add:Line_on_rule)
  have P2 : "Line_on (Li B1 C1) C1" by (simp add:Line_on_rule)
  from assms have P3 : "¬ Eq (Geos (Poi B1) add Emp) (Geos (Poi C1) add Emp)" by (simp add:Tri_def)
  from assms have P4 : "¬ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)" by (simp add:Tri_def)
  from P1 P2 P3 P4 have "∃p. Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) 
    ∧ ¬ Bet_Point (Se p C1) B1 ∧ Line_on (Li B1 C1) p ∧ ¬ Eq (Geos (Poi B1) add Emp) (Geos (Poi p) add Emp)" by (simp add:Seg_move_sameside)
  then obtain D1 :: Point where P5 : "Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 D1)) add Emp) 
    ∧ ¬ Bet_Point (Se D1 C1) B1 ∧ Line_on (Li B1 C1) D1 ∧ ¬ Eq (Geos (Poi B1) add Emp) (Geos (Poi D1) add Emp)" by blast
  from W have P6 : "¬ Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B C)) add Emp)" by (blast intro:Eq_rev)
  from P5 P6 have "¬ Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B1 D1)) add Emp)" by (simp add:Eq_not_trans)
  then have P7 : "¬ Eq (Geos (Poi C1) add Emp) (Geos (Poi D1) add Emp)" by (simp add:Seg_not_Eq_Point)
  from assms have P8 : "¬ Line_on (Li B1 C1) A1" by (simp add:Tri_def_Line)
  from P5 have P9 : "Line_on (Li B1 C1) D1" by simp
  then have P10 : "Eq (Geos (Poi D1) add Emp) (Geos (Poi A1) add Emp) ⟹ Line_on (Li B1 C1) A1" by (simp add:Point_Eq)
  from P8 P10 have P11 : "¬ Eq (Geos (Poi D1) add Emp) (Geos (Poi A1) add Emp)" by blast
  from assms have P12 : "¬ Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)" by (simp add:Tri_def)
  have P13 : "Line_on (Li A1 B1) B1" by (simp add:Line_on_rule)
  from P5 have P14 : "¬ Eq (Geos (Poi B1) add Emp) (Geos (Poi D1) add Emp)" by simp
  from assms P7 P9 P14 have "Def (Tri (Tr A1 B1 D1))" by (blast intro:Tri_def_extension)
  then have "Def (Tri (Tr D1 B1 A1))" by (simp add:Tri_def_rev)
  then have P15 : "Def (Tri (Tr B1 A1 D1))" by (simp add:Tri_def_trans)
  from assms have P16 : "Def (Tri (Tr B A C))" by (blast intro:Tri_def_rev Tri_def_trans)
  from assms have P17 : "Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A1)) add Emp)" by (blast intro:Seg_rev Eq_trans)
  from P5 have P18 : "Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 D1)) add Emp)" by simp
  have P19 : "Line_on (Li B1 A1) A1" by (simp add:Line_on_rule)
  from assms have "Def (Tri (Tr C1 B1 A1))" by (simp add:Tri_def_rev)
  then have P20 : "Def (Ang (An C1 B1 A1))" by (simp add:Tri_to_Ang)
  have P21 : "Line_on (Li B1 A1) A1" by (simp add:Line_on_rule)
  have P22 : "¬ Bet_Point (Se A1 A1) B1" by (simp add:Bet_end_Point)
  from P5 have P23 : "¬ Bet_Point (Se C1 D1) B1" by (blast intro:Bet_rev)
  from P12 have P24 : "¬ Eq (Geos (Poi B1) add Emp) (Geos (Poi A1) add Emp)" by (blast intro:Eq_rev)
  from P9 P14 P19 P20 P21 P22 P23 P24 have P25 : "Eq (Geos (Ang (An C1 B1 A1)) add Emp) (Geos (Ang (An D1 B1 A1)) add Emp)" by (simp add:Ang_Point_swap)
  from assms P25 have P26 : "Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An D1 B1 A1)) add Emp)" by (blast intro:Ang_weektrans Ang_rev Eq_rev)
  have P27 : "Eq (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An A B C)) add Emp)" by (simp add:Ang_roll)
  from P26 P27 have P28 : "Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An D1 B1 A1)) add Emp)" by (blast intro:Ang_weektrans Eq_rev)
  have P29 : "Eq (Geos (Ang (An D1 B1 A1)) add Emp) (Geos (Ang (An A1 B1 D1)) add Emp)" by (simp add:Ang_roll)  
  from P28 P29 have P30 : "Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 D1)) add Emp)" by (blast intro:Ang_weektrans Eq_rev Ang_rev)
  from P15 P16 P17 P18 P30 have P31 : "Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D1 A1 B1)) add Emp)" by (simp add:Tri_week_SAS)
  from P1 P2 P3 P5 P8 P23 have P32 : "Plane_sameside (Li A1 B1) C1 D1 ∨ Eq (Geos (Poi C1) add Emp) (Geos (Poi D1) add Emp)" by (simp add:Seg_Plane_sameside)
  from assms P31 have P33 : "Plane_sameside (Li A1 B1) C1 D1 ⟹ Eq (Geos (Lin (Li C1 A1)) add Emp) (Geos (Lin (Li D1 A1)) add Emp)" by (simp add:Ang_move_unique)
  from assms have "¬ Eq (Geos (Poi C1) add Emp) (Geos (Poi A1) add Emp)" by (simp add:Tri_def)
  then have P34 : "Eq (Geos (Lin (Li C1 A1)) add Emp) (Geos (Lin (Li A1 C1)) add Emp)" by (simp add:Line_rev)
  from P11 have P35 : "Eq (Geos (Lin (Li D1 A1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)" by (simp add:Line_rev)
  from P33 P34 P35 have P36 : "Plane_sameside (Li A1 B1) C1 D1 ⟹ Eq (Geos (Lin (Li A1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)" by (blast intro:Eq_trans Eq_rev)
  have P37 : "Line_on (Li A1 C1) C1" by (simp add:Line_on_rule)
  have P38 : "Line_on (Li A1 C1) A1" by (simp add:Line_on_rule)
  have P39 : "Line_on (Li A1 D1) D1" by (simp add:Line_on_rule)
  have P40 : "Line_on (Li A1 D1) A1" by (simp add:Line_on_rule)
  from P37 have P41 : "Eq (Geos (Poi C1) add Emp) (Geos (Poi D1) add Emp) ⟹ Line_on (Li A1 C1) D1" by (simp add:Point_Eq)
  from P11 P38 P39 P40 P41 have P42 : "Eq (Geos (Poi C1) add Emp) (Geos (Poi D1) add Emp) ⟹
    Eq (Geos (Lin (Li A1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)" by (simp add:Line_unique)
  from P32 P36 P42 have P43 : "Eq (Geos (Lin (Li A1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)" by blast
  from P2 P7 P9 P37 have P44 : "Line_on (Li A1 C1) D1 ⟹ Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li A1 C1)) add Emp)" by (simp add:Line_unique)
  from P1 P44 have P45 : "Line_on (Li A1 C1) D1 ⟹ Line_on (Li A1 C1) B1" by (simp add:Line_on_trans)
  from assms have "Def (Tri (Tr C1 B1 A1))" by (simp add:Tri_def_rev)
  then have P46 : "¬ Line_on (Li A1 C1) B1" by (simp add:Tri_def_Line)
  from P45 P46 have P47 : "¬ Line_on (Li A1 C1) D1" by blast
  have P48 : "Line_on (Li A1 D1) D1" by (simp add:Line_on_rule)
  from P47 P48 have P49 : "¬ Eq (Geos (Lin (Li A1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)" by (simp add:Line_not_on_Eq)
  from P43 P49 show False by blast
qed

text‹Theorem12›

theorem (in Congruence_Rule) Tri_SAS: 
  assumes 
    "Def (Tri (Tr A B C))"
    "Def (Tri (Tr A1 B1 C1))"
    "Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A1 B1)) add Emp)"
    "Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se A1 C1)) add Emp)"
    "Cong (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An B1 A1 C1)) add Emp)"
  shows "Cong (Geos (Tri (Tr A B C)) add Emp) (Geos (Tri (Tr A1 B1 C1)) add Emp)"
proof -
  from assms have P1 : "Cong (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An C1 B1 A1)) add Emp)" by (simp add:Tri_week_SAS)
  have P2 : "Eq (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An C A B)) add Emp)" by (simp add:Ang_roll)
  have P3 : "Eq (Geos (Ang (An C1 A1 B1)) add Emp) (Geos (Ang (An B1 A1 C1)) add Emp)" by (simp add:Ang_roll)
  from assms P2 have P4 : "Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An B1 A1 C1)) add Emp)" by (blast intro:Ang_weektrans Eq_rev)
  from P3 P4 have P5 : "Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C1 A1 B1)) add Emp)" by (blast intro:Ang_weektrans Ang_rev Eq_rev)
  from assms P1 P5 have P6 : "¬¬ Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C1)) add Emp)" by (simp add:Tri_week_ASA)
  from assms have P7 : "Eq (Geos (Seg (Se C A)) add Emp) (Geos (Seg (Se C1 A1)) add Emp)" by (blast intro:Seg_rev Eq_rev Eq_trans)
  from assms have P8 : "Def (Tri (Tr A C B))" by (