OAI/Analysis/MatrixSigning/Matrices/RowDotModel.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W12.RowDot.vectorTape line 13
  2. def OAI.KS.W12.RowDot.valueTape line 16
  3. def OAI.KS.W12.RowDot.indexedVector line 18
  4. def OAI.KS.W12.RowDot.tailTape line 20
  5. def OAI.KS.W12.RowDot.rowPairs line 22
  6. def OAI.KS.W12.RowDot.Consecutive line 25
  7. theorem OAI.KS.W12.RowDot.consecutive_cons line 28
  8. theorem OAI.KS.W12.RowDot.consecutive_indexedVector line 32
  9. theorem OAI.KS.W12.RowDot.tailTape_indexedVector line 39
  10. theorem OAI.KS.W12.RowDot.tailTape_nil line 47
  11. theorem OAI.KS.W12.RowDot.tailTape_cons line 48
  12. theorem OAI.KS.W12.RowDot.rowPairs_nil line 51
  13. theorem OAI.KS.W12.RowDot.rowPairs_cons line 52
  14. theorem OAI.KS.W12.RowDot.rowPairs_dotValue line 56
  15. def OAI.KS.W12.RowDot.state line 60
  16. def OAI.KS.W12.RowDot.boundary line 65