Walnut 1.3 (#1)

Add support for any Ostrowski numeration system based on the given pre-period and period of the continued fraction expansion of a quadratic irrational number.

Author: aseemrb

Command Files/number_system_proof.txt

@@ -0,0 +1,3 @@
+def successor "?msd_ns2 x < y & (Az (z <= x) | (z >= y))":
+eval base "?msd_ns2 Ax,z ((x + 0 = z) <=> (x = z))":
+eval induction "?msd_ns2 Ax,y,z,u,v ($successor(y, u) & $successor(z, v)) => ((x + y = z) <=> (x + u = v))":

Custom Bases/msd_fib.txt

@@ -1,6 +1,8 @@
-{0,1}
+{0, 1} 
+
 0 1
 0 -> 0
 1 -> 1
+
 1 1
 0 -> 0

Custom Bases/msd_fib_addition.txt

@@ -1,156 +1,48 @@
-{0,1} {0,1} {0,1}
-13 1
-0 0 0 -> 13
-0 0 1 -> 5
+{0, 1} {0, 1} {0, 1} 
+
+0 1
+0 0 0 -> 0
+0 0 1 -> 1
+1 0 1 -> 0
+0 1 1 -> 0
+
+1 0
+0 0 0 -> 2
+1 0 0 -> 3
+0 1 0 -> 3
+1 1 0 -> 4
 1 0 1 -> 2
 0 1 1 -> 2
-1 0 0 -> 16
-0 1 0 -> 16
-1 1 0 -> 16
-1 1 1 -> 16
-0 0
-0 0 0 -> 15
+1 1 1 -> 3
+
+2 0
+1 0 0 -> 2
+0 1 0 -> 2
+1 1 0 -> 3
 1 1 1 -> 2
-1 0 0 -> 11
-1 0 1 -> 12
-0 1 0 -> 6
-0 1 1 -> 3
-1 1 0 -> 16
-0 0 1 -> 16
-1 1
-0 0 0 -> 4
-0 0 1 -> 9
-1 0 0 -> 16
-0 1 0 -> 16
-1 1 0 -> 16
-1 0 1 -> 16
-0 1 1 -> 16
-1 1 1 -> 16
-2 1
-0 0 0 -> 13
-1 0 0 -> 16
-0 1 0 -> 16
-1 1 0 -> 16
-0 0 1 -> 16
-1 0 1 -> 16
-0 1 1 -> 16
-1 1 1 -> 16
+
 3 0
-0 0 0 -> 14
-1 0 0 -> 7
-0 1 0 -> 16
-1 1 0 -> 16
-0 0 1 -> 16
-1 0 1 -> 16
-0 1 1 -> 16
-1 1 1 -> 16
-4 0
-0 0 1 -> 2
-0 0 0 -> 16
-1 0 0 -> 16
-0 1 0 -> 16
-1 1 0 -> 16
-1 0 1 -> 16
-0 1 1 -> 16
-1 1 1 -> 16
+0 0 0 -> 1
+1 0 0 -> 0
+0 1 0 -> 0
+1 0 1 -> 1
+0 1 1 -> 1
+1 1 1 -> 0
+
+4 1
+0 0 0 -> 5
+0 0 1 -> 6
+1 0 1 -> 5
+0 1 1 -> 5
+
 5 0
-0 0 0 -> 14
-1 0 0 -> 7
-0 1 0 -> 10
-1 1 0 -> 1
-0 0 1 -> 16
-1 0 1 -> 16
-0 1 1 -> 16
-1 1 1 -> 16
+0 0 1 -> 0
+
 6 1
-0 0 0 -> 13
-0 0 1 -> 5
-1 0 1 -> 2
-1 0 0 -> 16
-0 1 0 -> 16
-1 1 0 -> 16
-0 1 1 -> 16
-1 1 1 -> 16
-7 0
-0 0 0 -> 15
-0 1 0 -> 6
+0 0 0 -> 3
+1 0 0 -> 4
+0 1 0 -> 4
+0 0 1 -> 2
+1 0 1 -> 3
 0 1 1 -> 3
-1 0 0 -> 16
-1 1 0 -> 16
-0 0 1 -> 16
-1 0 1 -> 16
-1 1 1 -> 16
-8 0
-0 0 0 -> 15
-1 0 0 -> 16
-0 1 0 -> 16
-1 1 0 -> 16
-0 0 1 -> 16
-1 0 1 -> 16
-0 1 1 -> 16
-1 1 1 -> 16
-9 1
-0 0 0 -> 0
-1 0 0 -> 1
-0 1 0 -> 1
-1 1 0 -> 16
-0 0 1 -> 16
-1 0 1 -> 16
-0 1 1 -> 16
-1 1 1 -> 16
-10 0
-0 0 0 -> 15
-1 0 0 -> 11
-1 0 1 -> 12
-0 1 0 -> 16
-1 1 0 -> 16
-0 0 1 -> 16
-0 1 1 -> 16
-1 1 1 -> 16
-11 1
-0 0 0 -> 13
-0 0 1 -> 5
-0 1 1 -> 2
-1 0 0 -> 16
-0 1 0 -> 16
-1 1 0 -> 16
-1 0 1 -> 16
-1 1 1 -> 16
-12 0
-0 0 0 -> 14
-0 1 0 -> 10
-1 0 0 -> 16
-1 1 0 -> 16
-0 0 1 -> 16
-1 0 1 -> 16
-0 1 1 -> 16
-1 1 1 -> 16
-14 0
-1 1 0 -> 8
-0 0 0 -> 16
-1 0 0 -> 16
-0 1 0 -> 16
-0 0 1 -> 16
-1 0 1 -> 16
-0 1 1 -> 16
-1 1 1 -> 16
-15 0
-0 0 0 -> 14
-1 1 1 -> 8
-1 0 0 -> 7
-0 1 0 -> 10
-1 1 0 -> 1
-0 0 1 -> 16
-1 0 1 -> 16
-0 1 1 -> 16
-16 0
-0 0 0 -> 16
-1 0 0 -> 16
-0 1 0 -> 16
-1 1 0 -> 16
-0 0 1 -> 16
-1 0 1 -> 16
-0 1 1 -> 16
-1 1 1 -> 16
-
-
+1 1 1 -> 4

Custom Bases/msd_pell.txt

@@ -1,7 +1,9 @@
-{0,1,2}
+{0, 1, 2} 
+
 0 1
 0 -> 0
 1 -> 0
 2 -> 1
+
 1 0
 0 -> 0