377e7822fee078c0d86c79a39e1286b330e4ba6e8a7d288a0d297bd51e9235df  Audit.lean
7e47aa6513dd7639ce5f01a165445ca037bd4da6bb36356b606fff46808ea29f  CheckInterfaces.lean
747948035ee55af8b53b6fca34c88efde40f0be32b292b0fd4fced5cd4933f03  DecodeExtensions.lean
1c36583a82e0266418991db6e316e119b880ffa37246c1cfc07fc84a35f10c74  DumpTable.lean
35da82c8f58a081f49dd301d852dba9f33a384f1f934cf1dd8c2f568cdb0499b  ExportCompiler.lean
7d6cde87d39c3844f123e5996da0148414f0bb1bc2957e6c15ba284bd5e1aeca  ExportExtensions.lean
53e0afba1a31eb2eae1e80adb643697c75b2ef341cfeeff595ee75baf1888bbf  ExportFast.lean
6cdf86b08f37a7295d9a9238de8660ba94dc549912892e0eab917d1ee0bfe5ff  ExportWalkthrough.lean
d3f3252ab42a7eb1dc5e3aae8236b6a71aa24d6f798d455ed567b54573d205e5  PROOF_MAP.md
7b53231ff8151a9680f197b4fb60f1294619f31de0b60e7b5296a319c884525b  README.md
944bafe7c5c19190e7be01eac907ec68514097834ce90c09a66fe437b5dd57a2  U21/BiTag.lean
b0362350fdac593fd428d670c38dfb0d8c428d1f6a1f7407227e1d7e822f49d3  U21/BiTagSimulation.lean
3d0eb02b819bfb7e7539c73fb8237d5eaa908a4698ab55cc48ae328e7e24db0c  U21/BlankNormalization.lean
eb38b3857bc9def7642c7249a39fc56dc9ecd9af70bc45f3e0732948e6147725  U21/CertifiedLayout.lean
83f3b03b8d142e215e98b8fa35d9998e698282a6832f36246e66134ed25e6570  U21/Circular.lean
888249b37a85287115ae4edce965c0a2b3e7902be2be2a21002c89b52cb43b93  U21/Complexity/BiTag.lean
a37bba4b2e3c1cc9f35179975cfd961b2f980dd6b4fcc79d6202aaa822804a1a  U21/Complexity/Bounds.lean
bb73c18f163bcc9ef33cf05fc920481eb35254b3661112cc46fd2e181aeb0577  U21/Complexity/Circular.lean
1cd586aca1c62029114e1fd9238f409591356762f58f4bafc911be6b84dcab21  U21/Complexity/Hardware.lean
19c1f8a969d4deb9ff50b32308608e8275ad2e925f9ab03bae896de07e8e9790  U21/Complexity/Layouts.lean
7b15ae85d620235a9f08e95e382ebe86a333c809115318c7af5908472a2b79a9  U21/Complexity/Ordinary.lean
77b6a4f7ab640b71dbf392621f78ab3c7ee6d2a4d9c5b412017ace41b679c66c  U21/Complexity/PackedBiTag.lean
e7eaadea6edc79544b7eb4c1163a96868dd801b597636e17f2fcd08c7521cf5a  U21/Complexity/PackedBounds.lean
429fdfb6bc2182a2d8132580f5f6a5cd897f64ecce9ba818edcc93ad8adee15b  U21/Complexity/PackedHardware.lean
3092257a9060c488ac184d2222900fb833759a8b5313d3a2c3006d3075b4872f  U21/Complexity/Sharpness.lean
a2893d59d64772bc73cb3e34bb45be7d553c51b13f7a09dd09b8677f9852c75d  U21/Complexity/Standard.lean
c322244f1c07575e54203f16e990a451612c7a241a9126fbabfbcbe4e6b1bac6  U21/Complexity/Trace.lean
a9216b967a176b7ffd506f3262f5cf6b2af44f63c8f6485077aca8e7fc7bb70a  U21/Complexity/Universality.lean
47f9bcb451b1c15f1b885b94202dd2d08e3a07d5e90b623f8ef17e2f43c00603  U21/ControlPermutation.lean
c0fe54448a4246c925ec1adc949c074df8c8d202a1dfaa7587bb88954a6297e6  U21/Copy.lean
fe9de8a9c067f19a4fe76f82019caad96e444ae10a4725f216b3371a13113f64  U21/Dispatch.lean
a098a299ca41c05d6f36bed5b8da6334d42cda293f5610be610786c46b6b265d  U21/Examples.lean
7c39af31485ed3f647a3d5e3bb8d014488f2e88f74d6e302e7ad0c1eb7d2e6b7  U21/Execution.lean
6a231bfded7f5ebca7955fb4039ecea68df94c762477ebe14442df5aa71d59c9  U21/ExtensionExamples.lean
dd7c2b9619028eaf1dbc2357aebba048912625b9be2d6980d03cb89c118789ef  U21/FastControls.lean
22c2c6fd381582e0d6a6ab77267f32c8447cfc52df6934a22194d94fbe0bd159  U21/FastLayout.lean
e01a58e8fb94b72345ba613a5beca00dad1acb03cf106fdcbcd9dee64e52e26c  U21/FastOrdinary.lean
3fdb0c82600f434fa3161e7b309e18e5ef046ffc63abacc3fa3d1184020b9bb0  U21/FrontierExamples.lean
86e4706f65ad4479683b6a0c18b1458cc3988bef9ebd7b77389d5be478e7d3e6  U21/Indexing.lean
4b5804359a5ee05247c742230b4d80d01f7981a628d6bcbd0121825c419e583f  U21/LayoutSearch.lean
3772fc437044aed8b37af42fd4f8ff983c7665c5075108fa6e433316200125d7  U21/Machine.lean
e065a336813b66485826abdd8409ca64a9bac727b003c572f7a9f02c6d7171c3  U21/Macro.lean
a207930e6e22e3b4b5a0f53c597fbe4fa1e3cd3d25e7f5235d8219ff74c73478  U21/OptimizedOutput.lean
3a88010cda7e9d0685f8f383696f2911b916d4f5c627964060bc825653689aca  U21/OptimizedUniversality.lean
9a42aa842c244beee07a4885c3329a383c82fdfa43a370f2dcdd65e2d43277aa  U21/Ordinary.lean
1b33b23c8d93cf23c78ec02955ab1c25ebd52dd086701539bafb3c791fd1fa21  U21/OrdinarySimulation.lean
4e336152b4b945488b3444411725c07721733f803d1da3f4024b3fa329b85883  U21/OrdinaryTape.lean
95ec6039bb45c299a193a5b1afb3dd40d784d4f000bd43bdfb21f5e4be916962  U21/OutputCorrectness.lean
f37fa9e8494a0775a346d3b862f9cacace7486f615ea7e794931e37fb808c53f  U21/OutputExecution.lean
c6384b24cfec462776d7242fa82d5333bcc7154a62178637ccfd52fd4e095fa4  U21/OutputObservation.lean
1aa5f9b9a4fadda6a75e52f6b69f1d7196f5a6949082e6e4719b1f3aaae6f16c  U21/OutputSource.lean
a33e6721de624e78f1134f9b556c0ff9616e19c1bfe339a8d70794863c0bd164  U21/OutputWords.lean
4322a90bd91577161e5eefc279ce4915952a88bccc2ec3bc262c77bbdf374441  U21/PackedAccounting.lean
56793e3cf14600680d7cb13b12ab80775c7b98eeb22b3aa5e83399d88c192fc7  U21/PackedEncoding.lean
1a14152c4023d573ba431deed532ab5a66ecc1085f7300a60399edbe41741f5a  U21/PackedMinimum.lean
f552b7bea8b3c82d870f73010590b0cf45630d14b2c9bd69a8a0fe03b55a40cb  U21/PackedOutput.lean
4edf496e3a87daccc1c5d560580131b41d9334d3438341ebf446e7ed71f15783  U21/PackedRecovery.lean
aa6474edd1b4b3463fa0af4b0a8395082e1bb72dffd3760495c50be350c2b686  U21/PackedSimulation.lean
a06556c252a0713cb5859891f8bd1009ab6911083832361d3ca8b66456f6e4e3  U21/PackedSize.lean
4ec931017dbc028db61c2977b712beb7e9975b5a427659415fc5ea3fb6795b39  U21/PackedSlots.lean
d23ee6c714cbd0abceddb2ecf48d98c79a4a905a4eb979ce59941c4046882032  U21/PackedUniversality.lean
5daa78a3c06e49ab6e0859556d74dd71b070b9e57ab74991bd59c554b35301c2  U21/PermutationCompiler.lean
3377e42b914cfca554d7e981ae54b858db400f7f0a953f888b6547e5f25ac671  U21/PermutedOutput.lean
227ee1a32e3a73c998b93e8a3abc0a889c27549acf12b9cdba0956f816afdeb2  U21/Printing.lean
c8578aced930353988e55f9d90a51fed30d47d9e91d569dac192617d66ca7093  U21/Production.lean
eeeb639ddd583e0bb2c8ccfbae284554872e3157a0d4f0b10b700a942068717b  U21/ProgramRecovery.lean
6a71bba68f0ad44f68e44a022a46aaeec185fb1898665b32dd74426f363a49e1  U21/RecoveredSlots.lean
6ed0fe403b59dbffdd52fad530b23229d9dc0f80c142125a6d717ca93b67e6dd  U21/RecoveredTable.lean
6dde6eb95dc75211f21de03e451265f63bab5eef1a48712b8dfc6ce2718050da  U21/RefereeBridge.lean
c379bd7f93f8dc6525a740fc1c1815bc85eccc86ce404d7a106761d6c2329e28  U21/Relabel.lean
bd14fa73cff96b8c5fb281f077b8b78463f5635c085cced65dbc30f67ed37c28  U21/Restoration.lean
87f23420d71a3fdc285d045de66bc97f8621add5bcd69b2e57ee02c52e35f5d3  U21/RoleOrders.lean
b535a80ee9652366503983c37a28299cc517de06e943b31c3682a745fd6bd297  U21/RunWords.lean
1523e0ea33ac8a2e99bd6dbce7e5879a57c1b4e7437f9a89a491458bc705d32e  U21/RuntimeOutput.lean
90456ea53cb465cf4c47e292f25c79fbf96e5e871dadf19329afc4cb40a91a61  U21/Slots.lean
1201809a2e483630512d07c954a2b54f71b1648ecbb05c96a23fdb85696b6ac3  U21/StructuralRoles.lean
434ca4b28ceaf934e7fe81c3692d3bed62ba3fea2c40b7fbcb1c2c3b404200b5  U21/Tape.lean
42d113fed3d1d7fe3ffc7e65f3c2e1bf9f290570a2bf46cbf9b09d8c42bc4efa  U21/TimeBoundsExamples.lean
9b83d925e37ae958b35d99db5957850cb2551b1fd4dcb5873fa3937b9ee2da94  U21/Universality.lean
edbef1acbebc512b036c6151e372e90fa73bb9cdefc9e5dbc342a2d158c16fc5  U21/Walkthrough.lean
4e7925108a4746ba59da2fc729d05b25a3418931f801233f12f23f64356a8b9a  U21/WeightedAccounting.lean
d713190bb2366872cbe6e88f854bbc457189532fc25fc964e5c972210d06d324  U21/WeightedOrder.lean
8b61c07766339bb2d00d444913ee2edf07675bf3002839e7876c10f0dfc02a95  U21.lean
5da77db984b616485db39accf035321b9c350f3bc5b654be80559f35a9c56260  compiler_check.py
f93c871a715c56701dda00eefb4417c9355028d03b44c897130cf7f375f44457  extension_check.py
ba07692c61499609053e50706a9f2c7081e82630fba427f27b6e0044adbbc2de  fast_check.py
9ecfe89e39abb358d27fb6de73fd1d948d7e0df71e6fcbdab1000530d8a40eda  lake-manifest.json
e583109ac301526fea7c6c3633ccc2459fe289fc6a463e02addd662c464a8b54  lakefile.toml
2bdc48adfa58d0017e538a0ad117c5d73d35deec879978f909406a80c8037273  lean-toolchain
dbb7e783df74cbea649e7e8ee3acf8245d19106ccaaa17f88deebed0322550c1  reference/python_backend/SOURCE_HASHES.json
13a8750d5733d6aaaf92f24b5522fbf9b475465d407074b02120a66d51bb7eb4  reference/python_backend/core.py
53a00e9b399c96c7ef8763c64b989917cd9e51eeac28fe7fb2962b82799e782a  reference/python_backend/optimize.py
929d03e2f2e7b5b9a0d0491946c473f340d89661681426092c05d4e291449449  reference/python_backend/packed.py
87535f7a39f79e8b3911ad0ca4c9e16c84290bd726a0ad7e75688d61a1161bd7  reference/python_backend/packed_layout.py
a46a15b92e8c26ea0e34bfde7b7cfc52b4787b9a244ecea84df07aad3179289f  reference/python_backend/slice_opt.py
182cc4c85d3aae382c190a214ad38a0fa904c708fdc9570a31e96708d05b813f  reference/transition-table.json
98f13a75ee27b7b4b8f5825c273ccbd5759d2d6e6a70aac91d578d91c95f281a  verify.py
79e8f8c94ac7b6621a407cb33c2dc10b444ada8f28772f47fb186a2f1c8c60a5  walkthrough_check.py
