Public
- Public
- Network
- Groups
- Popular
- People

Conversation

Notices

きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 13-Aug-2021 17:03:43 JST きゅーけー

ACL2 で n 個の要素からなるリストの長さが n より大きいときに必ず重複が存在することを鳩の巣の原理によって証明できた！
鳩の巣の原理自体は ACL が自動証明してくれたんだけど、それをリストの問題に適用するのが大変だった。
source: https://git.tojo.tokyo/acl2-theorems.git/tree/pigenhole.lisp?id=b420ce87ceae55123e1780a7eddec7eea5388ab7CI: https://ci.tojo.tokyo/jobs/acl2-verify/260
In conversation Friday, 13-Aug-2021 17:03:43 JST from mastodon.tojo.tokyo permalink
Attachments
1. Untitled attachment
2. No result found on File_thumbnail lookup.
  
  Laminar

Feeds