From e614d3f3644f7c88b4b3ecd615b43c963ad83b56 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Wed, 31 Dec 2025 13:48:20 +0100
Subject: [PATCH 1/2] Pos.lp: fix definition of multiplication

---
 Pos.lp | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

diff --git a/Pos.lp b/Pos.lp
index 55fa402..7d8aa61 100644
--- a/Pos.lp
+++ b/Pos.lp
@@ -557,24 +557,24 @@ end;
 
 symbol mul : ℙ → ℙ → ℙ;
 
-rule mul (I $x) $y ↪ add $x (O (mul $x $y))
+rule mul (I $x) $y ↪ add $y (O (mul $x $y))
 with mul (O $x) $y ↪ O (mul $x $y)
 with mul H      $y ↪ $y;
 
 // shortcuts
 
-symbol _1 ≔ H;
-symbol _2 ≔ O H;
-symbol _3 ≔ I H;
-symbol _4 ≔ O (O H);
-symbol _5 ≔ I (O H);
-symbol _6 ≔ O (I H);
-symbol _7 ≔ I (I H);
-symbol _8 ≔ O (O (O H));
-symbol _9 ≔ I (O (O H));
-symbol _10 ≔ O (I (O H));
-
-// enable printing of natural numbers in decimal notation
+symbol _1 ≔ H; assert ⊢ val _1 ≡ 1;
+symbol _2 ≔ O H; assert ⊢ val _2 ≡ 2;
+symbol _3 ≔ I H; assert ⊢ val _3 ≡ 3;
+symbol _4 ≔ O (O H); assert ⊢ val _4 ≡ 4;
+symbol _5 ≔ I (O H); assert ⊢ val _5 ≡ 5;
+symbol _6 ≔ O (I H); assert ⊢ val _6 ≡ 6;
+symbol _7 ≔ I (I H); assert ⊢ val _7 ≡ 7;
+symbol _8 ≔ O (O (O H)); assert ⊢ val _8 ≡ 8;
+symbol _9 ≔ I (O (O H)); assert ⊢ val _9 ≡ 9;
+symbol _10 ≔ O (I (O H)); assert ⊢ val _10 ≡ 10;
+
+// enable printing of positive numbers in decimal notation
 
 builtin "pos_one" ≔ H;
 builtin "pos_double" ≔ O;

From eb4f236cf7ce8419bac102d141586ea9583b9df3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Wed, 31 Dec 2025 13:54:14 +0100
Subject: [PATCH 2/2] wip

---
 Nat.lp | 10 +++++-----
 Pos.lp | 12 ++++++------
 2 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/Nat.lp b/Nat.lp
index 6953e55..05ee851 100644
--- a/Nat.lp
+++ b/Nat.lp
@@ -1766,6 +1766,11 @@ begin
   { assume n h; rewrite factS n; apply leq_pmulr (n +1) (n !) (fact_gt0 n) }
 end;
 
+// enable printing of natural numbers in decimal notation
+
+builtin "nat_zero" ≔ _0;
+builtin "nat_succ" ≔ +1;
+
 // shortcuts
 
 symbol _1 ≔ _0 +1;
@@ -1779,11 +1784,6 @@ symbol _8 ≔ _7 +1;
 symbol _9 ≔ _8 +1;
 symbol _10 ≔ _9 +1;
 
-// enable printing of natural numbers in decimal notation
-
-builtin "nat_zero" ≔ _0;
-builtin "nat_succ" ≔ +1;
-
 // enable parsing of natural numbers in decimal notation
 
 builtin "0"  ≔ _0;
diff --git a/Pos.lp b/Pos.lp
index 7d8aa61..89b7294 100644
--- a/Pos.lp
+++ b/Pos.lp
@@ -561,6 +561,12 @@ rule mul (I $x) $y ↪ add $y (O (mul $x $y))
 with mul (O $x) $y ↪ O (mul $x $y)
 with mul H      $y ↪ $y;
 
+// enable printing of positive numbers in decimal notation
+
+builtin "pos_one" ≔ H;
+builtin "pos_double" ≔ O;
+builtin "pos_succ_double" ≔ I;
+
 // shortcuts
 
 symbol _1 ≔ H; assert ⊢ val _1 ≡ 1;
@@ -573,9 +579,3 @@ symbol _7 ≔ I (I H); assert ⊢ val _7 ≡ 7;
 symbol _8 ≔ O (O (O H)); assert ⊢ val _8 ≡ 8;
 symbol _9 ≔ I (O (O H)); assert ⊢ val _9 ≡ 9;
 symbol _10 ≔ O (I (O H)); assert ⊢ val _10 ≡ 10;
-
-// enable printing of positive numbers in decimal notation
-
-builtin "pos_one" ≔ H;
-builtin "pos_double" ≔ O;
-builtin "pos_succ_double" ≔ I;