OAI/Analysis/MatrixSigning/Arithmetic/MultiplicationMachine.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W03.MultiplicationMachine.program line 15
2. def OAI.KS.W03.MultiplicationMachine.machine line 19
3. def OAI.KS.W03.MultiplicationMachine.exactBudget line 21
4. theorem OAI.KS.W03.MultiplicationMachine.full_spec line 25
5. theorem OAI.KS.W03.MultiplicationMachine.stack_count line 38
6. theorem OAI.KS.W03.MultiplicationMachine.state_count line 39
7. theorem OAI.KS.W03.MultiplicationMachine.input_port line 40
8. theorem OAI.KS.W03.MultiplicationMachine.output_port line 41
9. theorem OAI.KS.W03.MultiplicationMachine.exactBudget_le line 43
10. theorem OAI.KS.W03.MultiplicationMachine.exactBudget_le_input_polynomial line 50
11. theorem OAI.KS.W03.MultiplicationMachine.init_eq line 59
12. theorem OAI.KS.W03.MultiplicationMachine.run_input line 68
13. theorem OAI.KS.W03.MultiplicationMachine.output_correct line 75
14. theorem OAI.KS.W03.MultiplicationMachine.halts_input_polynomial line 83
15. theorem OAI.KS.W03.MultiplicationMachine.uniform_multiplication line 92