---

Step * of Lemma Euclid-drop-perp-ext

No Annotations
∀e:EuclideanPlane. ∀a:Point. ∀b:{b:Point| a # b} . ∀c:{c:Point| c # ab} .  (∃p:Point [(Colinear(a;b;p) ∧ ab  ⊥p pc)])
BY
{ Extract of Obid: Euclid-drop-perp
  not unfolding  geo-SCO geo-M geo-SCS geo-SS geo-CC sympoint 
  finishing with (RepUR ``let midpoint-construction`` 0 THEN Auto)
  normalizes to:
  
  λe,a,b,c. if M(a;b;c)
           then let a' = SymmetricPoint(a;c) in
                 let x = SCO(b;a;c;a') in
                 let y = SCS(b;a;c;a') in
                 let u = CC(x;y;y;x) in
                 let v = CC(y;x;x;y) in
                 if M(u;v;c) then Mid(x;y) else Mid(y;x) fi 
           else let b' = SymmetricPoint(b;c) in
                 let x = SCO(a;b;c;b') in
                 let y = SCS(a;b;c;b') in
                 let u = CC(x;y;y;x) in
                 let v = CC(y;x;x;y) in
                 if M(u;v;c) then Mid(x;y) else Mid(y;x) fi 
           fi  }

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a:Point.  \mforall{}b:\{b:Point|  a  \#  b\}  .  \mforall{}c:\{c:Point|  c  \#  ab\}  .
    (\mexists{}p:Point  [(Colinear(a;b;p)  \mwedge{}  ab    \mbot{}p  pc)])


By

---

Latex:
Extract  of  Obid:  Euclid-drop-perp
not  unfolding    geo-SCO  geo-M  geo-SCS  geo-SS  geo-CC  sympoint 
finishing  with  (RepUR  ``let  midpoint-construction``  0  THEN  Auto)
normalizes  to:

\mlambda{}e,a,b,c.  if  M(a;b;c)
                  then  let  a'  =  SymmetricPoint(a;c)  in
                              let  x  =  SCO(b;a;c;a')  in
                              let  y  =  SCS(b;a;c;a')  in
                              let  u  =  CC(x;y;y;x)  in
                              let  v  =  CC(y;x;x;y)  in
                              if  M(u;v;c)  then  Mid(x;y)  else  Mid(y;x)  fi 
                  else  let  b'  =  SymmetricPoint(b;c)  in
                              let  x  =  SCO(a;b;c;b')  in
                              let  y  =  SCS(a;b;c;b')  in
                              let  u  =  CC(x;y;y;x)  in
                              let  v  =  CC(y;x;x;y)  in
                              if  M(u;v;c)  then  Mid(x;y)  else  Mid(y;x)  fi 
                  fi 

---

Home Index