OAI/Analysis/MatrixSigning/Matrices/PivotTerminalMachine.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W17.FixedPSD.unitTerminal line 13
2. def OAI.KS.W17.FixedPSD.sparseTerminal line 15
3. def OAI.KS.W17.FixedPSD.terminalSelect line 18
4. def OAI.KS.W17.FixedPSD.terminalProgram line 20
5. def OAI.KS.W17.FixedPSD.terminalState line 22
6. def OAI.KS.W17.FixedPSD.unitTicks line 25
7. theorem OAI.KS.W17.FixedPSD.unitTerminal_spec line 30
8. theorem OAI.KS.W17.FixedPSD.sparseTerminal_spec line 44
9. theorem OAI.KS.W17.FixedPSD.terminal_unit_case line 67
10. theorem OAI.KS.W17.FixedPSD.terminal_sparse_case line 75
11. theorem OAI.KS.W17.FixedPSD.terminal_negative_spec line 87
12. theorem OAI.KS.W17.FixedPSD.terminal_sparse_spec line 99
13. def OAI.KS.W17.FixedPSD.finishTerminal line 115
14. theorem OAI.KS.W17.FixedPSD.finishTerminal_spec line 118