OAI/Analysis/MatrixSigning/Matrices/PivotReplayLoop.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W17.FixedPSD.historyTape line 10
2. def OAI.KS.W17.FixedPSD.replayGuard line 16
3. def OAI.KS.W17.FixedPSD.restoreAllProgram line 18
4. def OAI.KS.W17.FixedPSD.restoreConfig line 20
5. def OAI.KS.W17.FixedPSD.restoreTicks line 23
6. theorem OAI.KS.W17.FixedPSD.restore_step_empty line 31
7. theorem OAI.KS.W17.FixedPSD.restore_step_nonempty line 43
8. theorem OAI.KS.W17.FixedPSD.run_restoreAll line 58
9. theorem OAI.KS.W17.FixedPSD.restoreAll_spec line 103