OAI/Analysis/MatrixSigning/Machines/SignedFloorMachine.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W19.SignedFloorMachine.naturalPorts line 13
  2. def OAI.KS.W19.SignedFloorMachine.canonPorts line 15
  3. def OAI.KS.W19.SignedFloorMachine.outputPorts line 16
  4. def OAI.KS.W19.SignedFloorMachine.stripDispatch line 18
  5. def OAI.KS.W19.SignedFloorMachine.strip line 23
  6. def OAI.KS.W19.SignedFloorMachine.divide line 24
  7. def OAI.KS.W19.SignedFloorMachine.canon line 25
  8. def OAI.KS.W19.SignedFloorMachine.emit line 26
  9. def OAI.KS.W19.SignedFloorMachine.finish line 27
  10. def OAI.KS.W19.SignedFloorMachine.tailProgram line 28
  11. def OAI.KS.W19.SignedFloorMachine.program line 29
  12. def OAI.KS.W19.SignedFloorMachine.machine line 30
  13. def OAI.KS.W19.SignedFloorMachine.«stacks» line 32
  14. theorem OAI.KS.W19.SignedFloorMachine.strip_spec line 35
  15. theorem OAI.KS.W19.SignedFloorMachine.divide_spec line 49
  16. theorem OAI.KS.W19.SignedFloorMachine.canon_spec line 68
  17. theorem OAI.KS.W19.SignedFloorMachine.emit_spec line 80
  18. theorem OAI.KS.W19.SignedFloorMachine.finish_spec line 93
  19. theorem OAI.KS.W19.SignedFloorMachine.program_spec line 101
  20. theorem OAI.KS.W19.SignedFloorMachine.fuel_quadratic line 110
  21. theorem OAI.KS.W19.SignedFloorMachine.run_signed_payload line 120
  22. theorem OAI.KS.W19.SignedFloorMachine.output_floor line 135
  23. theorem OAI.KS.W19.SignedFloorMachine.haltsWithin_polynomial line 145