OAI/Analysis/MatrixSigning/Arithmetic/ComplexScalarNodes.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.KS.W15.ComplexMachine.Registers line 12
2. def OAI.KS.W15.ComplexMachine.corePorts line 14
3. def OAI.KS.W15.ComplexMachine.mulPorts line 16
4. theorem OAI.KS.W15.ComplexMachine.corePorts_apply line 19
5. theorem OAI.KS.W15.ComplexMachine.mulPorts_apply line 22
6. def OAI.KS.W15.ComplexMachine.CoreEmpty line 25
7. theorem OAI.KS.W15.ComplexMachine.coreEmpty_apply line 27
8. theorem OAI.KS.W15.ComplexMachine.stored_ne_core line 32
9. def OAI.KS.W15.ComplexMachine.pairProgram line 39
10. def OAI.KS.W15.ComplexMachine.pairTicks line 45
11. theorem OAI.KS.W15.ComplexMachine.pair_spec line 47
12. def OAI.KS.W15.ComplexMachine.mulProgram line 75
13. def OAI.KS.W15.ComplexMachine.addProgram line 76
14. def OAI.KS.W15.ComplexMachine.scalarAfter line 78
15. theorem OAI.KS.W15.ComplexMachine.scalar_multiplication_spec line 81
16. theorem OAI.KS.W15.ComplexMachine.scalar_addition_spec line 96
17. def OAI.KS.W15.ComplexMachine.storeProgram line 113
18. theorem OAI.KS.W15.ComplexMachine.store_spec line 115
19. def OAI.KS.W15.ComplexMachine.mulNode line 130
20. def OAI.KS.W15.ComplexMachine.addNode line 132
21. def OAI.KS.W15.ComplexMachine.mulNodeTicks line 135
22. def OAI.KS.W15.ComplexMachine.addNodeTicks line 138
23. theorem OAI.KS.W15.ComplexMachine.mulNode_spec line 142
24. theorem OAI.KS.W15.ComplexMachine.addNode_spec line 153
25. theorem OAI.KS.W15.ComplexMachine.coreEmpty_update line 164