OAI/Analysis/MatrixSigning/Machines/CopyInput.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W29.CopyInput.reverseEntry line 9
2. def OAI.KS.W29.CopyInput.copyEntry line 13
3. def OAI.KS.W29.CopyInput.tableEntry line 17
4. def OAI.KS.W29.CopyInput.machine line 21
5. def OAI.KS.W29.CopyInput.cfg line 24
6. theorem OAI.KS.W29.CopyInput.table_lookup line 27
7. theorem OAI.KS.W29.CopyInput.reverse_step line 50
8. theorem OAI.KS.W29.CopyInput.reverse_done line 60
9. theorem OAI.KS.W29.CopyInput.copy_step line 69
10. theorem OAI.KS.W29.CopyInput.copy_done line 79
11. theorem OAI.KS.W29.CopyInput.run_reverse line 88
12. theorem OAI.KS.W29.CopyInput.run_copy line 106
13. theorem OAI.KS.W29.CopyInput.run_copy_input line 124
14. theorem OAI.KS.W29.CopyInput.split_copy_fuel line 135
15. theorem OAI.KS.W29.CopyInput.run_eq_copy line 173
16. theorem OAI.KS.W29.CopyInput.haltsWithin line 181
17. theorem OAI.KS.W29.CopyInput.output_eq line 187
18. theorem OAI.KS.W29.CopyInput.haltsWithin_polynomialFuel line 193