acl2-theorems.git/peano.lisp, branch master
Proofs with acl2
http://git.tojo.tokyo/acl2-theorems.git/atom?h=master
2021-09-09T13:53:19Z
Add `(in-package "ACL2")` lines.
2021-09-09T13:53:19Z
Masaya Tojo
masaya@tojo.tokyo
2021-09-09T13:53:04Z
urn:sha1:5163a157c4f9b552db220efaa753f210518817fe
peano: Add nat< function.
2021-08-07T06:13:20Z
Masaya Tojo
masaya@tojo.tokyo
2021-08-07T06:13:20Z
urn:sha1:3d0dc785b63534feb515d3b8eb8dbb25abbfaced
peano: Change nat's expression.
2021-08-06T16:02:01Z
Masaya Tojo
masaya@tojo.tokyo
2021-08-06T16:02:01Z
urn:sha1:b60a5fa9bfd8570bb5878492db85a9814f71e028
peano: associativity-of-nat*: Unuse nat*-commutative.
2021-08-05T16:21:24Z
Masaya Tojo
masaya@tojo.tokyo
2021-08-05T16:21:24Z
urn:sha1:12132a24ad279fd3c1443cb79d52f897acaa49a7
peano: Add nat* function and theorems.
2021-08-05T16:16:56Z
Masaya Tojo
masaya@tojo.tokyo
2021-08-05T16:16:56Z
urn:sha1:80ff85f0f558e31a5aff784b2d38547c870f9d95
peano: Remove unnecessary hypothesis.
2021-08-05T15:54:14Z
Masaya Tojo
masaya@tojo.tokyo
2021-08-05T15:54:14Z
urn:sha1:ab711cc5ce71ee2feaa4e88a0b9af113c2d67e3d
peano: Add nat+-right-cancellative theorem.
2021-08-05T15:42:10Z
Masaya Tojo
masaya@tojo.tokyo
2021-08-05T15:42:10Z
urn:sha1:e00735e48932889c2f78ecbcd84554aeaf913179
peano: Rename theorems.
2021-08-05T15:40:02Z
Masaya Tojo
masaya@tojo.tokyo
2021-08-05T15:40:02Z
urn:sha1:a31c56c0051818cf8e952d0919eeefa05342e9f8
peano: Add peano.lisp file.
2021-08-04T16:44:28Z
Masaya Tojo
masaya@tojo.tokyo
2021-08-04T16:44:28Z
urn:sha1:85492c48d8a09ef6c8f8f332866cff34013ef0eb