From a31c56c0051818cf8e952d0919eeefa05342e9f8 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Fri, 6 Aug 2021 00:40:02 +0900
Subject: peano: Rename theorems.
---
peano.lisp | 37 +++++++++++++++----------------------
1 file changed, 15 insertions(+), 22 deletions(-)
diff --git a/peano.lisp b/peano.lisp
index 791e04e..c25fbf3 100644
--- a/peano.lisp
+++ b/peano.lisp
@@ -68,32 +68,25 @@
(equal (nat+ nil x)
x)))
-(defthm nat+-cancellative-1-1-1
- (implies (and (consp x)
- (nat? x)
- (nat? k))
- (not (equal (nat+ x k)
- k))))
+(defthm nat+-left-not-zp
+ (implies (and (nat? x)
+ (not (z? x))
+ (nat? y))
+ (not (equal (nat+ x y)
+ y))))
-(defthm nat+-cancellative-1-1
- (implies (and (consp x)
- (nat? x)
- (nat? k))
- (not (equal (nat+ k x)
- k)))
+(defthm nat+-right-not-zp
+ (implies (and (nat? x)
+ (nat? y)
+ (not (z? y)))
+ (not (equal (nat+ x y)
+ x)))
:hints (("Goal" :in-theory (disable nat+-commutative)
:use ((:instance nat+-commutative
- (x x)
- (y k))))))
-
-(defthm nat+-cancellative-1
- (implies (and (consp x)
- (nat? x)
- (nat? k))
- (not (equal (nat+ k x)
- k))))
+ (x x)
+ (y y))))))
-(defthm nat+-cancellative
+(defthm nat+-left-cancellative
(implies (and (nat? x)
(nat? y)
(nat? k))
--
cgit v1.2.3