---

Step * of Lemma rv-sep-iff-ext

∀rv:InnerProductSpace. ∀x,y:Point.  (x # y ⇐⇒ x - y # 0)
BY
{ Extract of Obid: rv-sep-iff
  normalizes to:
  
  λrv,x,y. <λs.case rv."+sep" x - y 0 y y 
                    case rv."#or" x y x - y + y s
                     of inl(_) =>
                     Ax
                     | inr(a) =>
                     case rv."#or" y x - y + y 0 + y a of inl(_) => Ax | inr(x) => x
                of inl(x) =>
                x
                | inr(_) =>
                Ax
           , λs.case rv."+sep" -y -y x y 
                     case rv."#or" -y + x 0 -y + x 
                          case rv."#or" x + -y 0 -y + x s
                           of inl(_) =>
                           Ax
                           | inr(a) =>
                           case rv."#or" 0 -y + x 0 a of inl(_) => Ax | inr(x) => x
                      of inl(_) =>
                      Ax
                      | inr(a) =>
                      case rv."#or" 0 -y + x -y + y a of inl(_) => Ax | inr(x) => x
                 of inl(_) =>
                 Ax
                 | inr(x) =>
                 x
           >
  
  not unfolding  rv-0 rv-add rv-sub rv-minus record-select
  finishing with Auto }

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}x,y:Point.    (x  \#  y  \mLeftarrow{}{}\mRightarrow{}  x  -  y  \#  0)


By

---

Latex:
Extract  of  Obid:  rv-sep-iff
normalizes  to:

\mlambda{}rv,x,y.  <\mlambda{}s.case  rv."+sep"  x  -  y  0  y  y 
                                    case  rv."\#or"  x  y  x  -  y  +  y  s
                                      of  inl($_{}$)  =>
                                      Ax
                                      |  inr(a)  =>
                                      case  rv."\#or"  y  x  -  y  +  y  0  +  y  a  of  inl($_{}$)  =>  Ax  |  inr(x\000C)  =>  x
                            of  inl(x)  =>
                            x
                            |  inr($_{}$)  =>
                            Ax
                  ,  \mlambda{}s.case  rv."+sep"  -y  -y  x  y 
                                      case  rv."\#or"  -y  +  x  0  -y  +  x 
                                                case  rv."\#or"  x  +  -y  0  -y  +  x  s
                                                  of  inl($_{}$)  =>
                                                  Ax
                                                  |  inr(a)  =>
                                                  case  rv."\#or"  0  -y  +  x  0  a  of  inl($_{}$)  =>  Ax  |  inr(x)\000C  =>  x
                                        of  inl($_{}$)  =>
                                        Ax
                                        |  inr(a)  =>
                                        case  rv."\#or"  0  -y  +  x  -y  +  y  a  of  inl($_{}$)  =>  Ax  |  inr(x)\000C  =>  x
                              of  inl($_{}$)  =>
                              Ax
                              |  inr(x)  =>
                              x
                  >

not  unfolding    rv-0  rv-add  rv-sub  rv-minus  record-select
finishing  with  Auto

---

Home Index