---

Step * 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))
∧ (¬(c = b ∈ Point))
∧ (¬(d = e ∈ Point))
∧ (¬(f = e ∈ Point))
∧ (∃a',c',x',z':Point. (b_a_a' ∧ b_c_c' ∧ e_d_x' ∧ e_f_z' ∧ ba'=ex' ∧ bc'=ez' ∧ a'c'=x'z'))
⊢ ∃a',c',d',f':Point. (out(b a'a) ∧ out(b cc') ∧ out(e d'd) ∧ out(e ff') ∧ Cong3(a'bc',d'ef'))
BY
{ RepeatFor 8 ((D (-1) THENA Auto))
THEN RenameVar `d\'' (-3)⋅
THEN RenameVar `f\'' (-2)⋅
THEN (InstConcl [⌜a'⌝;⌜c'⌝;⌜d'⌝;⌜f'⌝]⋅ THENA 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' ∧ 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')

---

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))
\mwedge{}  (\mneg{}(c  =  b))
\mwedge{}  (\mneg{}(d  =  e))
\mwedge{}  (\mneg{}(f  =  e))
\mwedge{}  (\mexists{}a',c',x',z':Point.  (b\_a\_a'  \mwedge{}  b\_c\_c'  \mwedge{}  e\_d\_x'  \mwedge{}  e\_f\_z'  \mwedge{}  ba'=ex'  \mwedge{}  bc'=ez'  \mwedge{}  a'c'=x'z'))
\mvdash{}  \mexists{}a',c',d',f':Point.  (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:
RepeatFor  8  ((D  (-1)  THENA  Auto))
THEN  RenameVar  `d\mbackslash{}''  (-3)\mcdot{}
THEN  RenameVar  `f\mbackslash{}''  (-2)\mcdot{}
THEN  (InstConcl  [\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{};\mkleeneopen{}f'\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index