diff --git a/interval.tal b/interval.tal index 25e5470..4598cb7 100644 --- a/interval.tal +++ b/interval.tal @@ -13,6 +13,25 @@ @iv-not-positive ( x** -> x<0^ ) NIP2 #0000 !x16-lteq @iv-not-negative ( x** -> x<0^ ) POP2 #0000 !x16-gteq +( +x / [-a, +b] -> [ -x/a, +x/b] ) +( -x / [-a, +b] -> [ -x/b, +x/a] ) +( +x / [-a, 0] -> [-256x, -x/a] ) +( -x / [-a, 0] -> [ x/a, 256x] ) +( +x / [ 0, +b] -> [ x/b, 256x] ) +( -x / [ 0, +b] -> [-256x, -x/b] ) +( +x / [+a, +b] -> [ x/b, x/a] ) +( -x / [+a, +b] -> [ -x/a, -x/b] ) +( +x / [-a, -b] -> [ -x/a, -x/b] ) +( -x / [-a, -b] -> [ x/b, x/a] ) +( x / [ 0, 0] -> error ) + +( 0 / y -> [0, 0] ) +( +x / [-a, -b] -> [-x/b, -x/a] ) +( +x / [+a, +b] -> [+x/b, +x/a] ) +( -x / [-a, -b] -> [+x/a, +x/b] ) +( -x / [+a, +b] -> [-x/b, -x/a] ) + + @iv-crosses-zero ( x** -> bool^ ) #0000 SWP2 OVR2 x16-lteq ( x0* 0* x1<0^ ) ?&no !x16-lt ( x0<0^ )