OAI/Analysis/MatrixSigning/Optimization/TerminalWitnessMachine.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W19.TerminalWitnessMachine.inputState line 13
2. def OAI.KS.W19.TerminalWitnessMachine.collected line 18
3. def OAI.KS.W19.TerminalWitnessMachine.copyIndex line 24
4. def OAI.KS.W19.TerminalWitnessMachine.collect line 26
5. def OAI.KS.W19.TerminalWitnessMachine.collectTicks line 29
6. theorem OAI.KS.W19.TerminalWitnessMachine.collect_spec line 36
7. def OAI.KS.W19.TerminalWitnessMachine.coefficient line 54
8. def OAI.KS.W19.TerminalWitnessMachine.scalarTicks line 57
9. theorem OAI.KS.W19.TerminalWitnessMachine.scalar_spec line 61
10. def OAI.KS.W19.TerminalWitnessMachine.program line 80
11. def OAI.KS.W19.TerminalWitnessMachine.outputState line 83
12. def OAI.KS.W19.TerminalWitnessMachine.ticks line 88
13. theorem OAI.KS.W19.TerminalWitnessMachine.full_spec line 91
14. theorem OAI.KS.W19.TerminalWitnessMachine.witness_negative line 111