Step
*
of Lemma
eu-cong3-to-conga
∀e:EuclideanPlane. ∀a,b,c,d,E,f:Point.
((∃a',c',d',f':Point. (out(b a'a) ∧ out(b c'c) ∧ out(E d'd) ∧ out(E f'f) ∧ Cong3(a'bc',d'Ef')))
⇒ abc = dEf)
BY
{ RepeatFor 8 ((D 0 THENA Auto))
THEN RepeatFor 8 (D (-1)⋅) }
1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. E : Point
7. f : Point
8. a' : Point
9. c' : Point
10. d' : Point
11. f' : Point
12. out(b a'a)
13. out(b c'c)
14. out(E d'd)
15. out(E f'f)
16. Cong3(a'bc',d'Ef')
⊢ abc = dEf
Latex:
Latex:
\mforall{}e:EuclideanPlane. \mforall{}a,b,c,d,E,f:Point.
((\mexists{}a',c',d',f':Point. (out(b a'a) \mwedge{} out(b c'c) \mwedge{} out(E d'd) \mwedge{} out(E f'f) \mwedge{} Cong3(a'bc',d'Ef')))
{}\mRightarrow{} abc = dEf)
By
Latex:
RepeatFor 8 ((D 0 THENA Auto))
THEN RepeatFor 8 (D (-1)\mcdot{})
Home
Index