OAI/Analysis/MatrixSigning/Realization/FramedMapRoutine.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CurrentKS.FramedMapRoutine.source line 14
  2. abbrev OAI.CurrentKS.FramedMapRoutine.accumulator line 15
  3. abbrev OAI.CurrentKS.FramedMapRoutine.work line 16
  4. abbrev OAI.CurrentKS.FramedMapRoutine.scratch line 17
  5. def OAI.CurrentKS.FramedMapRoutine.state line 19
  6. def OAI.CurrentKS.FramedMapRoutine.ports line 22
  7. def OAI.CurrentKS.FramedMapRoutine.decodePorts line 23
  8. def OAI.CurrentKS.FramedMapRoutine.framePorts line 25
  9. lemma OAI.CurrentKS.FramedMapRoutine.decodePorts_0 line 28
  10. lemma OAI.CurrentKS.FramedMapRoutine.decodePorts_1 line 29
  11. lemma OAI.CurrentKS.FramedMapRoutine.decodePorts_2 line 30
  12. lemma OAI.CurrentKS.FramedMapRoutine.framePorts_0 line 31
  13. lemma OAI.CurrentKS.FramedMapRoutine.framePorts_1 line 32
  14. lemma OAI.CurrentKS.FramedMapRoutine.framePorts_2 line 33
  15. def OAI.CurrentKS.FramedMapRoutine.decode line 35
  16. def OAI.CurrentKS.FramedMapRoutine.frame line 36
  17. def OAI.CurrentKS.FramedMapRoutine.append line 37
  18. def OAI.CurrentKS.FramedMapRoutine.body line 38
  19. def OAI.CurrentKS.FramedMapRoutine.scan line 41
  20. def OAI.CurrentKS.FramedMapRoutine.setup line 43
  21. def OAI.CurrentKS.FramedMapRoutine.finish line 44
  22. def OAI.CurrentKS.FramedMapRoutine.program line 46
  23. def OAI.CurrentKS.FramedMapRoutine.tape line 49
  24. lemma OAI.CurrentKS.FramedMapRoutine.state_ports line 51
  25. lemma OAI.CurrentKS.FramedMapRoutine.state_other line 57
  26. lemma OAI.CurrentKS.FramedMapRoutine.element_spec line 62
  27. lemma OAI.CurrentKS.FramedMapRoutine.decode_spec line 68
  28. lemma OAI.CurrentKS.FramedMapRoutine.frame_spec line 77
  29. lemma OAI.CurrentKS.FramedMapRoutine.append_spec line 86
  30. def OAI.CurrentKS.FramedMapRoutine.bodyTicks line 97
  31. lemma OAI.CurrentKS.FramedMapRoutine.body_spec line 101
  32. def OAI.CurrentKS.FramedMapRoutine.scanTicks line 111
  33. lemma OAI.CurrentKS.FramedMapRoutine.scan_trace line 114
  34. lemma OAI.CurrentKS.FramedMapRoutine.setup_spec line 138
  35. lemma OAI.CurrentKS.FramedMapRoutine.finish_spec line 149
  36. def OAI.CurrentKS.FramedMapRoutine.ticks line 160
  37. def OAI.CurrentKS.FramedMapRoutine.routine line 163