OAI/Analysis/MatrixSigning/Machines/BinaryStackMoves.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W04.BinaryStackMoves.clearDispatch line 15
2. def OAI.KS.W04.BinaryStackMoves.clearMachine line 20
3. def OAI.KS.W04.BinaryStackMoves.clearProgram line 21
4. def OAI.KS.W04.BinaryStackMoves.oneConfig line 24
5. theorem OAI.KS.W04.BinaryStackMoves.config_ext line 28
6. theorem OAI.KS.W04.BinaryStackMoves.clear_step_cons line 34
7. theorem OAI.KS.W04.BinaryStackMoves.clear_step_nil line 48
8. theorem OAI.KS.W04.BinaryStackMoves.run_clear line 61
9. theorem OAI.KS.W04.BinaryStackMoves.clear_active line 82
10. theorem OAI.KS.W04.BinaryStackMoves.clear_haltsAfter line 104
11. def OAI.KS.W04.BinaryStackMoves.moveDispatch line 111
12. def OAI.KS.W04.BinaryStackMoves.moveMachine line 117
13. def OAI.KS.W04.BinaryStackMoves.moveProgram line 119
14. def OAI.KS.W04.BinaryStackMoves.twoConfig line 122
15. theorem OAI.KS.W04.BinaryStackMoves.move_step_cons line 126
16. theorem OAI.KS.W04.BinaryStackMoves.move_step_nil line 140
17. theorem OAI.KS.W04.BinaryStackMoves.run_move line 154
18. theorem OAI.KS.W04.BinaryStackMoves.move_active line 177
19. theorem OAI.KS.W04.BinaryStackMoves.move_haltsAfter line 201
20. theorem OAI.KS.W04.BinaryStackMoves.oneConfig_original line 209
21. theorem OAI.KS.W04.BinaryStackMoves.twoConfig_original line 216
22. theorem OAI.KS.W04.BinaryStackMoves.run_clear_stacks line 225
23. theorem OAI.KS.W04.BinaryStackMoves.run_move_stacks line 232
24. theorem OAI.KS.W04.BinaryStackMoves.clear_haltsAfter_stacks line 241
25. theorem OAI.KS.W04.BinaryStackMoves.move_haltsAfter_stacks line 248
26. theorem OAI.KS.W04.BinaryStackMoves.clear_linear_time line 256
27. theorem OAI.KS.W04.BinaryStackMoves.move_linear_time line 262
28. theorem OAI.KS.W04.BinaryStackMoves.move_output line 269
29. theorem OAI.KS.W04.BinaryStackMoves.clear_table_length line 286
30. theorem OAI.KS.W04.BinaryStackMoves.move_table_length line 289