---

Step * 1 1 1 of Lemma eu-conga-to-cong3


1. E : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. ¬(a = b ∈ Point)
9. ¬(c = b ∈ Point)
10. ¬(d = e ∈ Point)
11. ¬(f = e ∈ Point)
12. a' : Point
13. c' : Point
14. d' : Point
15. f' : Point
16. b_a_a' ∧ b_c_c' ∧ e_d_d' ∧ e_f_f' ∧ ba'=ed' ∧ bc'=ef' ∧ a'c'=d'f'
⊢ out(b a'a) ∧ out(b cc') ∧ out(e d'd) ∧ out(e ff') ∧ Cong3(a'bc',d'ef')
BY
{ Auto
THEN Try (Unfold `eu-out` 0 THEN Auto) }

1
1. E : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. ¬(a = b ∈ Point)
9. ¬(c = b ∈ Point)
10. ¬(d = e ∈ Point)
11. ¬(f = e ∈ Point)
12. a' : Point
13. c' : Point
14. d' : Point
15. f' : Point
16. b_a_a'
17. b_c_c'
18. e_d_d'
19. e_f_f'
20. ba'=ed'
21. bc'=ef'
22. a'c'=d'f'
23. out(b a'a)
24. out(b cc')
25. out(e d'd)
26. out(e ff')
⊢ Cong3(a'bc',d'ef')

---

Latex:

---

Latex:

1.  E  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  e  :  Point
7.  f  :  Point
8.  \mneg{}(a  =  b)
9.  \mneg{}(c  =  b)
10.  \mneg{}(d  =  e)
11.  \mneg{}(f  =  e)
12.  a'  :  Point
13.  c'  :  Point
14.  d'  :  Point
15.  f'  :  Point
16.  b\_a\_a'  \mwedge{}  b\_c\_c'  \mwedge{}  e\_d\_d'  \mwedge{}  e\_f\_f'  \mwedge{}  ba'=ed'  \mwedge{}  bc'=ef'  \mwedge{}  a'c'=d'f'
\mvdash{}  out(b  a'a)  \mwedge{}  out(b  cc')  \mwedge{}  out(e  d'd)  \mwedge{}  out(e  ff')  \mwedge{}  Cong3(a'bc',d'ef')


By

---

Latex:
Auto
THEN  Try  (Unfold  `eu-out`  0  THEN  Auto)

---

Home Index