diff options
| author | Masaya Tojo <masaya@tojo.tokyo> | 2021-08-06 00:40:02 +0900 |
|---|---|---|
| committer | Masaya Tojo <masaya@tojo.tokyo> | 2021-08-06 00:40:02 +0900 |
| commit | a31c56c0051818cf8e952d0919eeefa05342e9f8 (patch) | |
| tree | 6143753ade23684c772f7278302ccce0b45b2327 /peano.lisp | |
| parent | 85492c48d8a09ef6c8f8f332866cff34013ef0eb (diff) | |
peano: Rename theorems.
Diffstat (limited to 'peano.lisp')
| -rw-r--r-- | peano.lisp | 37 |
1 files changed, 15 insertions, 22 deletions
@@ -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)) |