58b8180c07e0b90e4e021728efa4757f18edd04b5cbdb259908b171fea023c41  ./NOTE.md
f72fe78cd7e7a5fecdfe9f56bedcdd0117f7601169d726f59837dbbf114125a4  ./README.md
57d92cdf96a6066f6874e90dfc5a4f45b298ce764b5da2560ddcf8ea15b4df31  ./lean/BoundedLob.lean
0db63c69a1d90f2e08e1da244c1d1d0edc373e1557d75a8e9267e6891dca6fa8  ./lean/BoundedLob/Agents.lean
8862c252b2394216f84b6a1ed93ccccf5090c95806cfc17a3b2bd6f565976416  ./lean/BoundedLob/Basic.lean
09f1e87ea6e864d7ad24560064fae664135d2f951b1d3a6f436160b3673af1b6  ./lean/BoundedLob/Engine.lean
7e7aa4aa3dae48412dd15a9148279888a172547cc3a8db6cf09de652e2eac2de  ./lean/BoundedLob/Explicit.lean
50d8c806c7adf0ef6ef10287003068583eb8f5d11180e47b047b9bee133a2e53  ./lean/BoundedLob/Model.lean
853c346b0c11e508c354f0648c20ec3cca531f5f968b0f8389b32250af420c18  ./lean/BoundedLob/Numerals.lean
3afd0b74b33ff0155b2b2c5a454bdbd45f36b5fa05f9626c0c79abef4d5ded6d  ./lean/BoundedLob/Poly.lean
8f15b1a5186b50094a124cb8f1ac17df93b62f94af1a5adc9bdf5b45eb99beec  ./lean/BoundedLob/Separation.lean
3ac3b97fec4109ef90333b13e37141c20896bc23ede85dae0532d5eb0a69ccd5  ./lean/BoundedLob/Unbounded.lean
e7237aca9e68ad0ac51ecaddcf0e452e74ced165d2a8184be6e0bb842aaad7e1  ./lean/Check.lean
ef27e37c70b70f4444535444dda9fb02607bf05682e909635b59b9b5821ef9a9  ./lean/README.md
99433750d519e3aee6dd99a73d91dfb1211f97a3fe96388dc2938a3fd1701131  ./lean/lake-manifest.json
1d4294eb81d708c1165d848dc839952f95c45fe20d6ea99c702d008c3dd8dcfb  ./lean/lakefile.toml
8733782dc070a99b312039cda424f601b80f3be6f6f512627da5ba25adc27632  ./lean/lean-toolchain
45afbf6ecdc1d11c2f50e4d11101c1a77eeca176745c766f2856145d204f4caa  ./proofs/A1-A3.md
10d405ccd7752befe7890ad93f501803216f8bd11ffb15992afbd1d073fcf2e2  ./proofs/A4-A5.md
1dcbf0507a041f0a5303d86413ededa65c40a1c5a4541b7d15cf74f95badadc8  ./proofs/A6-A7.md
934ffc5ab7965be4a7d93fddd5379a9e739e4ab17331ad1e1b57a520af3eb440  ./proofs/ASSUMPTIONS.md
d32bad25ee0b241f4206163ba2f6a07c5bfc37d4e5878e100a15f021e7e6cb95  ./proofs/SEPARATION.md
1ea01bababafa9b6549421fe72b32ad1ddd4e5b8f822cc170c7f6c3082f69d7d  ./proofs/UPPER-ASM1.md
015f13d8dd1aeb2f310fc811a524e8d37fe7e78bedcd5cd891f4bc6e5e7cca9d  ./proofs/UPPER-THETA.md
58c6f15e6555251f86abeed4e63cb5a2a75f89740633f870675ddf96e0d308e9  ./proofs/UPPER.md
0adf2905c95d47d6f3e9d60bee02217dfd917c57a06f39d1312c94fa2590bbd6  ./proofs/check/artifacts/a4check/a4check.py
bb16c29b311ff3150034ae746fd5cd22576d7a41a2bfa6b3e15ad65614c23824  ./proofs/check/artifacts/a4check/post.py
ef1a17aba38198d1b56d10180201e93bea37c90012974b277e9f2302cab5c420  ./proofs/check/artifacts/a4check/ptr.py
eb1542ab4a18ad4f0122fab21a316f701a2634cc02ebe761b13fbbc0688be366  ./proofs/check/artifacts/a4check/synth.py
88bc05a71b9bf08ca8ae97e19a0fc2140388473621b16c0a292ad4bb7d13babd  ./proofs/check/artifacts/g1recheck-20261010T195345Z/g1k.py
4b4f5e378c09390333a4c14ff6f09788b1bc6c76562eb32e02e894ed81c77e2e  ./proofs/check/artifacts/g1recheck-full-20261010T1955Z/res.json
d4b4eecebe805b46f023b7896ea2c9c152a20167c724b837891def09009e2291  ./proofs/check/artifacts/treecheck-20261010T213259Z/out/stdout.host.txt
c4738ac5c4226112f22002361fb800b747435df2fe22a0b0dcde3a57d73323c2  ./proofs/check/artifacts/treecheck-20261010T213259Z/out2/stdout.host.txt
9819b348600683d5ab670c6d67b189a97ef6edc207b04e5756ff5d1a1f16171c  ./proofs/check/artifacts/treecheck-20261010T213259Z/out3/stdout.host.txt
33035d8a64c9a42aa0983dd5a1e3b08ede4ff5b79c919cf8059ce2ed71013bbc  ./proofs/check/artifacts/treecheck-20261010T213259Z/s/treecheck.py
9fc43a8d90cf26a73d91fbe275e5369245b01bfbc72144e4f75cbd3f1fc6ee49  ./proofs/check/artifacts/treecheck-20261010T213259Z/s/treecheck2.py
c8538270accf88f38415c8712af9f5b5ad1ec10524461b4432252ed1c41aa1c9  ./proofs/check/artifacts/treecheck-20261010T213259Z/s/treecheck3.py
57fd2ab04993936924ddc99c3f70bd60f8039219adf32181050b4cefd1b15ded  ./proofs/check/artifacts/treecheck-20261010T213259Z/s/treecheck_defs.py
4c6ecd9cfa15e0a87b4646f0671eb6ec2f988bad26920f80cbacb786b1e29181  ./proofs/check/upper/T-EXEC.md
d5d7163fdf1e94f5768b440a207ab450b69d3017f2e13ebd2b7af6f8e7d3e644  ./proofs/check/upper/T-exec/README.md
a694c489034342aa756e520675dd02be88a579cf72bedb3883673d767b7878dc  ./proofs/check/upper/T-exec/gen.py
3dcac04d24f0238c385fcead332c74b682413fb322cba7cf9580738c72007f9d  ./proofs/check/upper/T-exec/lba.py
af38ca62bbb9dff751cfe822f11cb84744ae8f21878132866bc01078453f63ab  ./proofs/check/upper/T-exec/mxl.py
eb3ec9e13ce9b01abbb7f9f10e120831a291a4d9b46787a6c534ad1a75e40c01  ./proofs/check/upper/T-exec/nat.py
afee5f8e27e30fd29a6103263e161af29ec88632bce4c7414a353b1ede977577  ./proofs/check/upper/T-exec/out/full-20261011T175310Z/res.json
f828bc4627fc17cc913d63afa7afe0fda49abeeca262bda0f9b5891fb682c028  ./proofs/check/upper/T-exec/out/full-20261011T175310Z/run.log
ae44218a1fd137582c1a4cfc5b0fe6ff93b75cc86d392874d58c7e2f1ec913b3  ./proofs/check/upper/T-exec/report.py
e386acdc26d5a968aac79c362325d17a08054658ebfefba0625ab27bfec58d2c  ./proofs/check/upper/T-exec/run.py
637601ac6df2b9d270f9a06a398e802c1aa4ba17190ba67af084c98c279fc140  ./proofs/check/upper/T-exec/tr.py
5e37c47d8b9627cc1201267ac500b34ae41ee0b8876e548dcf804b32a68f8910  ./proofs/check/upper/T-exec/zcheck.py
35756a8918a8097e8cf8f3fb18d7adbc4f8af84b54a4248c71704a343f0e1119  ./supplement-g1/G1.md
a66eb1f5b5fb0f92ef6ee779500fbafdc1c16ec69e3b1e07e55a2efe944e5be9  ./supplement-g1/out3/code.sha256
92a9ad39722953a8c951cca7b5f740c846d2b40247f2ea96e167b0d44d2e0d01  ./supplement-g1/out3/res.json
dc77214e5adad5ec6110a0b3e1a0f95f1baf71dcf81bb0f7fa2d0b9f5ec4f458  ./supplement-g1/out3/run.log
81eac4ecbe59f7e6c879adda6f5f4ba666821e08f6bb2eb2f8b3cfd1a91cfedc  ./supplement-g1/tau/gen.py
fa75ed7c4e301e74208e6c608a74415ef7a34b9400fbceb1f1d7da4a1ac256d6  ./supplement-g1/tau/hilbert.py
6ff1203e1c7708682f75c5316ae81df1cd466ec3b394485656f0df481d040c10  ./supplement-g1/tau/lk.py
c5c72ace319c9b779360837bfe793d119d7af35741a2d476304e61098ff08417  ./supplement-g1/tau/run_tests.py
d3bb7731ce1a1c450b08b7569a2a4fa6e1509c1d33400174229ae8f6139d9b8a  ./supplement-g1/tau/syntax.py
3cbcb05f227036b7995ec7a978f3a57224978aab664c5f489928e2e2eef6dd94  ./supplement-g1/tau/tau.py
