---

Step * of Lemma geo-add-length-assoc

∀[e:BasicGeometry]. ∀[x,y,z:Length].  (x + y + z = x + y + z ∈ 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' `z' THEN (GenConcl ⌜a = z ∈ {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 RenameTo `a' `z1'
         THEN (GenConcl ⌜a = z1 ∈ {p:Point| B(OXp)} ⌝⋅ THENA Auto)
         THEN ThinVar `a')
   THEN Auto) }

1
1. e : BasicGeometry
2. x : {p:Point| B(OXp)} 
3. y : {p:Point| B(OXp)} 
4. z : {p:Point| B(OXp)} 
5. x1 : {p:Point| B(OXp)} 
6. y1 : {p:Point| B(OXp)} 
7. z1 : {p:Point| B(OXp)} 
8. x ≡ x1
9. y ≡ y1
10. z ≡ z1
⊢ x + y + z = x1 + y1 + z1 ∈ Length

---

Latex:

---

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


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'  `z'  THEN  (GenConcl  \mkleeneopen{}a  =  z\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  RenameTo  `a'  `z1'
              THEN  (GenConcl  \mkleeneopen{}a  =  z1\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  ThinVar  `a')
  THEN  Auto)

---

Home Index