From a31c56c0051818cf8e952d0919eeefa05342e9f8 Mon Sep 17 00:00:00 2001 From: Masaya Tojo 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