OAI/Analysis/MatrixSigning/Arithmetic/ZeroPaddedRow.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W12.RowDot.literalDispatch line 11
2. def OAI.KS.W12.RowDot.literalPush line 14
3. theorem OAI.KS.W12.RowDot.literalPush_spec line 17
4. def OAI.KS.W12.RowDot.zeroFrame line 40
5. def OAI.KS.W12.RowDot.prependZero line 42
6. theorem OAI.KS.W12.RowDot.prependZero_spec line 49
7. theorem OAI.KS.W12.RowDot.vectorTape_cons line 73
8. def OAI.KS.W12.RowDot.zeroPadded line 77
9. def OAI.KS.W12.RowDot.copyZeroPadded line 79
10. theorem OAI.KS.W12.RowDot.copyZeroPadded_spec line 82
11. theorem OAI.KS.W12.RowDot.zeroPadded_row_dot line 96
12. theorem OAI.KS.W12.RowDot.zeroPadded_polynomial_spec line 101