OAI/Analysis/MatrixSigning/Machines/FixedCopyRestore.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KS.W01.FixedCopy.activeFor_append line 10
2. theorem OAI.KS.W01.FixedCopy.reverse_active line 17
3. theorem OAI.KS.W01.FixedCopy.restore_active line 33
4. theorem OAI.KS.W01.FixedCopy.copy_haltsAfter line 54
5. def OAI.KS.W01.FixedCopy.machine line 75
6. def OAI.KS.W01.FixedCopy.program line 78
7. theorem OAI.KS.W01.FixedCopy.config_ext line 81
8. theorem OAI.KS.W01.FixedCopy.project_start line 89
9. theorem OAI.KS.W01.FixedCopy.run_copy_restore line 100
10. theorem OAI.KS.W01.FixedCopy.haltsAfter line 135
11. theorem OAI.KS.W01.FixedCopy.haltsFromWithin line 145
12. theorem OAI.KS.W01.FixedCopy.haltsFromWithin_polynomial line 153