OAI/Analysis/MatrixSigning/Arithmetic/EncodedDivision.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W19.EncodedDivision.program line 10
2. def OAI.KS.W19.EncodedDivision.machine line 11
3. def OAI.KS.W19.EncodedDivision.resultPair line 13
4. theorem OAI.KS.W19.EncodedDivision.input_spec line 15
5. theorem OAI.KS.W19.EncodedDivision.run_spec line 23
6. theorem OAI.KS.W19.EncodedDivision.fuel_quadratic line 33
7. theorem OAI.KS.W19.EncodedDivision.run_polynomial line 45
8. theorem OAI.KS.W19.EncodedDivision.output_polynomial line 52
9. theorem OAI.KS.W19.EncodedDivision.natural_output_correct line 60
10. theorem OAI.KS.W19.EncodedDivision.haltsWithin_polynomial line 73