OAI/Analysis/MatrixSigning/Arithmetic/MultiplicationDeterministic.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KS.W03.MultiplicationDeterministic.copy_coinIndependent line 12
2. theorem OAI.KS.W03.MultiplicationDeterministic.frame_coinIndependent line 21
3. theorem OAI.KS.W03.MultiplicationDeterministic.reverse_coinIndependent line 25
4. theorem OAI.KS.W03.MultiplicationDeterministic.adder_coinIndependent line 29
5. theorem OAI.KS.W03.MultiplicationDeterministic.trim_coinIndependent line 33
6. theorem OAI.KS.W03.MultiplicationDeterministic.body_coinIndependent line 37
7. theorem OAI.KS.W03.MultiplicationDeterministic.loop_coinIndependent line 47
8. theorem OAI.KS.W03.MultiplicationDeterministic.initialize_coinIndependent line 50
9. theorem OAI.KS.W03.MultiplicationDeterministic.normalize_coinIndependent line 55
10. theorem OAI.KS.W03.MultiplicationDeterministic.coinIndependent line 60