OAI/Analysis/MatrixSigning/Realization/RawMatrixMachine.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CurrentKS.RawMatrixMachine.unary line 11
  2. def OAI.CurrentKS.RawMatrixMachine.extend line 13
  3. def OAI.CurrentKS.RawMatrixMachine.state line 16
  4. def OAI.CurrentKS.RawMatrixMachine.ports line 19
  5. def OAI.CurrentKS.RawMatrixMachine.fields line 20
  6. def OAI.CurrentKS.RawMatrixMachine.popMarker line 21
  7. def OAI.CurrentKS.RawMatrixMachine.copyPorts line 22
  8. def OAI.CurrentKS.RawMatrixMachine.copyCount line 23
  9. def OAI.CurrentKS.RawMatrixMachine.framePorts line 24
  10. def OAI.CurrentKS.RawMatrixMachine.framing line 25
  11. def OAI.CurrentKS.RawMatrixMachine.appendFrame line 26
  12. def OAI.CurrentKS.RawMatrixMachine.body line 27
  13. def OAI.CurrentKS.RawMatrixMachine.scan line 29
  14. def OAI.CurrentKS.RawMatrixMachine.finish line 30
  15. def OAI.CurrentKS.RawMatrixMachine.program line 31
  16. def OAI.CurrentKS.RawMatrixMachine.rawTape line 33
  17. def OAI.CurrentKS.RawMatrixMachine.canonicalTape line 35
  18. lemma OAI.CurrentKS.RawMatrixMachine.extend_port line 38
  19. lemma OAI.CurrentKS.RawMatrixMachine.extend_other line 41
  20. lemma OAI.CurrentKS.RawMatrixMachine.fields_spec line 48
  21. lemma OAI.CurrentKS.RawMatrixMachine.popMarker_spec line 57
  22. lemma OAI.CurrentKS.RawMatrixMachine.copyCount_spec line 66
  23. lemma OAI.CurrentKS.RawMatrixMachine.framing_spec line 76
  24. lemma OAI.CurrentKS.RawMatrixMachine.appendFrame_spec line 84
  25. def OAI.CurrentKS.RawMatrixMachine.bodyTicks line 94
  26. lemma OAI.CurrentKS.RawMatrixMachine.body_spec line 99
  27. lemma OAI.CurrentKS.RawMatrixMachine.bodyTicks_le line 113
  28. lemma OAI.CurrentKS.RawMatrixMachine.scan_trace line 121
  29. lemma OAI.CurrentKS.RawMatrixMachine.finish_spec line 149
  30. theorem OAI.CurrentKS.RawMatrixMachine.program_spec line 160