OAI/Analysis/MatrixSigning/Arithmetic/GCDMachine.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W30.GCDMachine.clearQuotient line 13
2. def OAI.KS.W30.GCDMachine.advanceDividend line 14
3. def OAI.KS.W30.GCDMachine.reverseRemainder line 15
4. def OAI.KS.W30.GCDMachine.remainderPorts line 16
5. def OAI.KS.W30.GCDMachine.trimRemainder line 17
6. def OAI.KS.W30.GCDMachine.cleanup line 18
7. def OAI.KS.W30.GCDMachine.body line 20
8. def OAI.KS.W30.GCDMachine.guard line 22
9. def OAI.KS.W30.GCDMachine.loop line 24
10. def OAI.KS.W30.GCDMachine.finish line 26
11. def OAI.KS.W30.GCDMachine.program line 27
12. def OAI.KS.W30.GCDMachine.state line 29
13. theorem OAI.KS.W30.GCDMachine.clearQuotient_spec line 32
14. theorem OAI.KS.W30.GCDMachine.advanceDividend_spec line 46
15. theorem OAI.KS.W30.GCDMachine.reverseRemainder_spec line 60
16. theorem OAI.KS.W30.GCDMachine.trimRemainder_start line 74
17. theorem OAI.KS.W30.GCDMachine.trimRemainder_spec line 84
18. theorem OAI.KS.W30.GCDMachine.cleanup_spec line 101
19. theorem OAI.KS.W30.GCDMachine.loop_table_length line 112