OAI/Analysis/MatrixSigning/Matrices/PivotControllerLoop.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W17.FixedPSD.controllerGuard line 9
2. def OAI.KS.W17.FixedPSD.controllerProgram line 14
3. def OAI.KS.W17.FixedPSD.controllerConfig line 16
4. theorem OAI.KS.W17.FixedPSD.controller_step_clear line 19
5. theorem OAI.KS.W17.FixedPSD.controller_step_empty line 31
6. theorem OAI.KS.W17.FixedPSD.controller_run_clear line 44
7. theorem OAI.KS.W17.FixedPSD.controller_step_finished line 59
8. theorem OAI.KS.W17.FixedPSD.controller_step_call line 74
9. def OAI.KS.W17.FixedPSD.localBits line 93
10. def OAI.KS.W17.FixedPSD.controllerTicks line 95
11. theorem OAI.KS.W17.FixedPSD.controllerTicks_descend line 114
12. theorem OAI.KS.W17.FixedPSD.vectorTape_nonempty line 122