---

Step * of Lemma geo-add-length-comm

∀[e:BasicGeometry]. ∀[x,y:Length].  (x + y = y + x ∈ Length)
BY
{ (Auto
   THEN ∀h:hyp. (UnfoldTop `geo-length-type` h THEN (D h THENA Auto)) 
   THEN ∀h:hyp. (UnfoldTop `geo-eq` h THEN FoldTop `geo-eq` h THEN MoveToConcl h) 
   THEN (RenameTo `a' `x' THEN (GenConcl ⌜a = x ∈ {p:Point| B(OXp)} ⌝⋅ THENA Auto) THEN ThinVar `a')
   THEN RenameTo `a' `y'
   THEN (GenConcl ⌜a = y ∈ {p:Point| B(OXp)} ⌝⋅ THENA Auto)
   THEN ThinVar `a'
   THEN RenameTo `a' `x1'
   THEN (GenConcl ⌜a = x1 ∈ {p:Point| B(OXp)} ⌝⋅ THENA Auto)
   THEN ThinVar `a'
   THEN RenameTo `a' `y1'
   THEN (GenConcl ⌜a = y1 ∈ {p:Point| B(OXp)} ⌝⋅ THENA Auto)
   THEN ThinVar `a'
   THEN Auto
   THEN Unfold `geo-add-length` 0
   THEN GeneralizeGeoExtends [`a';`b']
   THEN DSetVars
   THEN EqTypeCD
   THEN Auto) }

1
1. e : BasicGeometry
2. x : Point
3. B(OXx)
4. y : Point
5. B(OXy)
6. x1 : Point
7. B(OXx1)
8. y1 : Point
9. B(OXy1)
10. x ≡ x1
11. y ≡ y1
12. a : Point
13. B(Oxa)
14. xa ≅ Xy
15. xa ≅ Xy
16. B(Oxa)
17. b : Point
18. B(Oy1b)
19. y1b ≅ Xx1
20. y1b ≅ Xx1
21. B(Oy1b)
⊢ a ≡ b

---

Latex:

---

Latex:
\mforall{}[e:BasicGeometry].  \mforall{}[x,y:Length].    (x  +  y  =  y  +  x)


By

---

Latex:
(Auto
  THEN  \mforall{}h:hyp.  (UnfoldTop  `geo-length-type`  h  THEN  (D  h  THENA  Auto)) 
  THEN  \mforall{}h:hyp.  (UnfoldTop  `geo-eq`  h  THEN  FoldTop  `geo-eq`  h  THEN  MoveToConcl  h) 
  THEN  (RenameTo  `a'  `x'  THEN  (GenConcl  \mkleeneopen{}a  =  x\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ThinVar  `a')
  THEN  RenameTo  `a'  `y'
  THEN  (GenConcl  \mkleeneopen{}a  =  y\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `a'
  THEN  RenameTo  `a'  `x1'
  THEN  (GenConcl  \mkleeneopen{}a  =  x1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `a'
  THEN  RenameTo  `a'  `y1'
  THEN  (GenConcl  \mkleeneopen{}a  =  y1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `a'
  THEN  Auto
  THEN  Unfold  `geo-add-length`  0
  THEN  GeneralizeGeoExtends  [`a';`b']
  THEN  DSetVars
  THEN  EqTypeCD
  THEN  Auto)

---

Home Index