From 39ba834c446e911ef8c944dd78a8bffbb9e97fb0 Mon Sep 17 00:00:00 2001 From: Yoni Zohar Date: Tue, 19 May 2026 12:14:25 +0300 Subject: [PATCH] suggestion --- Theories/Ints.smt2 | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Theories/Ints.smt2 b/Theories/Ints.smt2 index ebae55c..c4335f1 100644 --- a/Theories/Ints.smt2 +++ b/Theories/Ints.smt2 @@ -65,12 +65,12 @@ - ** as the exponentiation function if the second argument is non-negative. That is (** m n) is m to the power of n. In particular, (= (** 0 0) 1) holds. - If n is strictly smaller than 0, then ** is defined so as to satisfy the formula + If n is strictly smaller than 0 then (= (** 0 n) 0). For any m different than 0, + ** is defined so as to satisfy the formula (= (** m n) (div 1 (** m (- n)))) - So the following holds for all integers n < 0: - - (= (** 0 n) (div 1 0)) + So the following holds for all integers n < 0 and m != 0: - (= (** m n) (** m (- n))) if (= (abs m) 1) - (= (** m n) 0) if (> (abs m) 1)