OAI/Analysis/MatrixSigning/Machines/FixedCompare.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W28.FixedCompare.program line 12
2. def OAI.KS.W28.FixedCompare.after line 15
3. theorem OAI.KS.W28.FixedCompare.after_left line 20
4. theorem OAI.KS.W28.FixedCompare.after_right line 24
5. theorem OAI.KS.W28.FixedCompare.after_result line 28
6. theorem OAI.KS.W28.FixedCompare.after_other line 33
7. theorem OAI.KS.W28.FixedCompare.compare_spec line 38
8. theorem OAI.KS.W28.FixedCompare.compare_spec_linear line 65