---

Step * of Lemma sq_stable__rv-sep-ext

∀rv:InnerProductSpace. ∀x,y:Point.  SqStable(x # y)
BY
{ Extract of Obid: sq_stable__rv-sep
  normalizes to:
  
  λrv,x,y,_. case rv."+sep" -y -y x y 
                  case rv."#or" -y + x 0 -y + x 
                       case rv."#or" x + -y 0 -y + x 
                            let _,p = rv."positive" x - y 
                            in p ((((rlessw(r0^2;||x - y||^2) * 20) + 1) * 20) + 1)
                        of inl(_) =>
                        Ax
                        | inr(b) =>
                        case rv."#or" 0 -y + x 0 b of inl(_) => Ax | inr(a) => a
                   of inl(_) =>
                   Ax
                   | inr(b) =>
                   case rv."#or" 0 -y + x -y + y b of inl(_) => Ax | inr(a) => a
             of inl(_) =>
             Ax
             | inr(a) =>
             a
  
  not unfolding  rv-0 rv-add rv-minus rv-sub rsqrt rlessw rnexp rv-norm rmul int-to-real record-select
  finishing with Auto }

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}x,y:Point.    SqStable(x  \#  y)


By

---

Latex:
Extract  of  Obid:  sq\_stable\_\_rv-sep
normalizes  to:

\mlambda{}rv,x,y,$_{}$.  case  rv."+sep"  -y  -y  x  y 
                              case  rv."\#or"  -y  +  x  0  -y  +  x 
                                        case  rv."\#or"  x  +  -y  0  -y  +  x 
                                                  let  $_{}$,p  =  rv."positive"  x  -  y 
                                                  in  p  ((((rlessw(r0\^{}2;||x  -  y||\^{}2)  *  20)  +  1)  *  20)  +  1)
                                          of  inl($_{}$)  =>
                                          Ax
                                          |  inr(b)  =>
                                          case  rv."\#or"  0  -y  +  x  0  b  of  inl($_{}$)  =>  Ax  |  inr(a)  =>  \000Ca
                                of  inl($_{}$)  =>
                                Ax
                                |  inr(b)  =>
                                case  rv."\#or"  0  -y  +  x  -y  +  y  b  of  inl($_{}$)  =>  Ax  |  inr(a)  =>  \000Ca
                    of  inl($_{}$)  =>
                    Ax
                    |  inr(a)  =>
                    a

not  unfolding    rv-0  rv-add  rv-minus  rv-sub  rsqrt  rlessw  rnexp  rv-norm  rmul  int-to-real  record-select
finishing  with  Auto

---

Home Index