OAI/MathematicalPhysics/NavierStokes/BalancedTransport/RecorderSimulation.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BalancedTransport.Recorder.inverse_base_pos line 9
  2. theorem OAI.BalancedTransport.Recorder.inverse_base_le_one line 12
  3. theorem OAI.BalancedTransport.Recorder.digit_unit_bound line 16
  4. def OAI.BalancedTransport.Recorder.Configuration.stacks line 21
  5. def OAI.BalancedTransport.Recorder.Configuration.code line 32
  6. def OAI.BalancedTransport.Recorder.Instruction.fullMap line 35
  7. theorem OAI.BalancedTransport.Recorder.Instruction.fullMap_code line 40
  8. theorem OAI.BalancedTransport.Recorder.Instruction.source_code_mem line 54
  9. theorem OAI.BalancedTransport.Recorder.compiled_boxes_disjoint line 66
  10. theorem OAI.BalancedTransport.Recorder.prefix_halfWidth line 88
  11. theorem OAI.BalancedTransport.Recorder.nonhalt_box_guard line 96
  12. theorem OAI.BalancedTransport.Recorder.Row.sourceControl_ne_halt line 108
  13. theorem OAI.BalancedTransport.Recorder.source_box_guard line 112
  14. theorem OAI.BalancedTransport.Recorder.code_mem_observer_iff line 117
  15. structure OAI.BalancedTransport.Recorder.Checkpoint line 148
  16. def OAI.BalancedTransport.Recorder.Checkpoint.expand line 163
  17. def OAI.BalancedTransport.Recorder.Checkpoint.next line 168
  18. def OAI.BalancedTransport.Recorder.Checkpoint.WorkStep line 181
  19. theorem OAI.BalancedTransport.Recorder.Checkpoint.next_exec line 184
  20. theorem OAI.BalancedTransport.Recorder.Checkpoint.work_execution line 207
  21. theorem OAI.BalancedTransport.Recorder.no_step_from_halt line 225
  22. theorem OAI.BalancedTransport.Recorder.Exec.cancel_to_terminal line 239
  23. theorem OAI.BalancedTransport.Recorder.Checkpoint.halt_reflection line 262
  24. theorem OAI.BalancedTransport.Recorder.Checkpoint.halting_iff line 277
  25. def OAI.BalancedTransport.Coding.rationalWord line 294
  26. theorem OAI.BalancedTransport.Coding.rationalWord_cast line 298
  27. theorem OAI.BalancedTransport.Coding.stream_const line 312
  28. def OAI.BalancedTransport.Coding.rationalTailCode line 326
  29. theorem OAI.BalancedTransport.Coding.rationalTailCode_cast line 329
  30. def OAI.BalancedTransport.Recorder.Checkpoint.initial line 343
  31. theorem OAI.BalancedTransport.Recorder.Checkpoint.initial_work_block line 346
  32. theorem OAI.BalancedTransport.Recorder.Checkpoint.base_gt_one line 362
  33. def OAI.BalancedTransport.Recorder.Checkpoint.rationalInitial line 367
  34. theorem OAI.BalancedTransport.Recorder.Checkpoint.rationalInitial_cast line 373