OAI/Computability/Scheduling/StateBounds.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ThreeMachine.Algorithm.tableOf_length line 10
  2. theorem OAI.ThreeMachine.Algorithm.states_length line 13
  3. theorem OAI.ThreeMachine.Algorithm.markings_length line 20
  4. theorem OAI.ThreeMachine.Algorithm.layers_length line 25
  5. def OAI.ThreeMachine.StackCompiler.BlockSmall line 37
  6. def OAI.ThreeMachine.StackCompiler.TableSmall line 40
  7. def OAI.ThreeMachine.StackCompiler.MarksSmall line 42
  8. theorem OAI.ThreeMachine.StackCompiler.blockSmall_of_good line 44
  9. theorem OAI.ThreeMachine.StackCompiler.layers_small line 48
  10. theorem OAI.ThreeMachine.StackCompiler.markings_small line 53
  11. theorem OAI.ThreeMachine.StackCompiler.volume_table_le line 60
  12. theorem OAI.ThreeMachine.StackCompiler.volume_marks_le line 71
  13. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeTable line 85
  14. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeMarks line 91
  15. theorem OAI.ThreeMachine.StackCompiler.Poly.lengthTriples line 97
  16. theorem OAI.ThreeMachine.StackCompiler.Poly.lengthAlphabet line 103
  17. theorem OAI.ThreeMachine.StackCompiler.Poly.lengthFamily line 109
  18. theorem OAI.ThreeMachine.StackCompiler.volume_block_bound line 125
  19. theorem OAI.ThreeMachine.StackCompiler.volume_advance_le line 132
  20. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeSmallBlock line 148
  21. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeSmallLookup line 153
  22. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeAdvance line 162
  23. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeTryAdvance line 168
  24. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_append_le line 192
  25. theorem OAI.ThreeMachine.StackCompiler.Realizer.time_zero line 202
  26. theorem OAI.ThreeMachine.StackCompiler.Realizer.time_nil line 203
  27. theorem OAI.ThreeMachine.StackCompiler.Realizer.time_cons line 204
  28. theorem OAI.ThreeMachine.StackCompiler.Realizer.time_reverse_le line 205
  29. theorem OAI.ThreeMachine.StackCompiler.Realizer.volume_range_le line 209
  30. theorem OAI.ThreeMachine.StackCompiler.Realizer.time_rangeStep_le line 218
  31. theorem OAI.ThreeMachine.StackCompiler.Realizer.time_range_le line 226
  32. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_orD_le line 244
  33. abbrev OAI.ThreeMachine.StackCompiler.Poly.IterPool line 260
  34. theorem OAI.ThreeMachine.StackCompiler.Poly.iterateTime line 261
  35. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeFirstResult line 285
  36. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeOptionOr line 298
  37. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeStateList line 311
  38. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeSetList line 318
  39. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeExpandBody line 325