二分木に要素を挿入した後にその要素を探すと必ず挿入された要素が見つかる定理を追加した。これは #ACL2 的にも自明だったらしく一瞬で証明できた。https://gitlab.com/tojoqk/practice-acl2/-/commit/722c82b0120964966e04927800c9e54f48954be5
二分木に要素を挿入した後にその要素を探すと必ず挿入された要素が見つかる定理を追加した。これは #ACL2 的にも自明だったらしく一瞬で証明できた。https://gitlab.com/tojoqk/practice-acl2/-/commit/722c82b0120964966e04927800c9e54f48954be5
senooken JP Social is a social network, courtesy of senooken. It runs on GNU social, version 2.0.2-beta0, available under the GNU Affero General Public License.
All senooken JP Social content and data are available under the Creative Commons Attribution 3.0 license.