OAI/MathematicalPhysics/NavierStokes/BalancedTransport/RecorderRules.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.BalancedTransport.Recorder.Machine line 8
  2. inductive OAI.BalancedTransport.Recorder.Record line 13
  3. inductive OAI.BalancedTransport.Recorder.Letter line 20
  4. inductive OAI.BalancedTransport.Recorder.Control line 27
  5. structure OAI.BalancedTransport.Recorder.Configuration line 34
  6. structure OAI.BalancedTransport.Recorder.Tails line 40
  7. structure OAI.BalancedTransport.Recorder.Instruction line 45
  8. def OAI.BalancedTransport.Recorder.Instruction.source line 63
  9. def OAI.BalancedTransport.Recorder.Instruction.target line 67
  10. def OAI.BalancedTransport.Recorder.Instruction.sourceTails line 71
  11. def OAI.BalancedTransport.Recorder.Instruction.targetTails line 76
  12. theorem OAI.BalancedTransport.Recorder.Instruction.sourceTails_source line 81
  13. theorem OAI.BalancedTransport.Recorder.Instruction.targetTails_target line 86
  14. def OAI.BalancedTransport.Recorder.Instruction.Balanced line 91
  15. inductive OAI.BalancedTransport.Recorder.Row line 102
  16. def OAI.BalancedTransport.Recorder.Row.valid line 123
  17. def OAI.BalancedTransport.Recorder.Row.instruction line 129
  18. theorem OAI.BalancedTransport.Recorder.Row.balanced line 155
  19. def OAI.BalancedTransport.Recorder.sourceRow line 168
  20. def OAI.BalancedTransport.Recorder.targetRow line 207
  21. theorem OAI.BalancedTransport.Recorder.sourceRow_source line 231
  22. theorem OAI.BalancedTransport.Recorder.targetRow_target line 240
  23. theorem OAI.BalancedTransport.Recorder.source_separation line 246
  24. theorem OAI.BalancedTransport.Recorder.target_separation line 257
  25. def OAI.BalancedTransport.Recorder.Step line 272
  26. theorem OAI.BalancedTransport.Recorder.step_deterministic line 284
  27. theorem OAI.BalancedTransport.Recorder.step_injective line 293
  28. instance OAI.BalancedTransport.Recorder.(instance at line 300) line 300
  29. def OAI.BalancedTransport.Recorder.table line 304
  30. theorem OAI.BalancedTransport.Recorder.mem_table line 309
  31. inductive OAI.BalancedTransport.Recorder.Exec line 320
  32. theorem OAI.BalancedTransport.Recorder.row_step line 334
  33. theorem OAI.BalancedTransport.Recorder.outward_scan line 338
  34. theorem OAI.BalancedTransport.Recorder.returning_scan line 351