diff options
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)) |