From 79871fe479dbffc99dbd360f0d39728427101da8 Mon Sep 17 00:00:00 2001
From: d6 <d_m@plastic-idolatry.com>
Date: Fri, 5 May 2023 14:05:28 -0400
Subject: [PATCH] interval div notes

---
 interval.tal | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

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^ )