OAI/Computability/WeisfeilerLeman/RAMBounds.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.WLTime.TypedStack.Code.HaltState line 9
  2. def OAI.WLTime.TypedStack.Code.haltTransition line 10
  3. def OAI.WLTime.TypedStack.Code.haltMachine line 14
  4. theorem OAI.WLTime.TypedStack.Code.haltMachine_run line 20
  5. def OAI.WLTime.TypedStack.Code.haltOneTape line 27
  6. theorem OAI.WLTime.TypedStack.Code.haltOneTape_correct line 29
  7. def OAI.WLTime.RAMAlphabet.budgetConstant line 43
  8. theorem OAI.WLTime.RAMAlphabet.budget_bound line 44
  9. theorem OAI.WLTime.TypedStack.Code.Exec.of_decEq line 80
  10. abbrev OAI.WLTime.RAMConsumer.Reg line 91
  11. abbrev OAI.WLTime.RAMConsumer.Letter line 92
  12. def OAI.WLTime.RAMConsumer.prelude line 95
  13. def OAI.WLTime.RAMConsumer.code line 98
  14. def OAI.WLTime.RAMConsumer.answer line 100
  15. theorem OAI.WLTime.RAMConsumer.prefix_exec line 102
  16. theorem OAI.WLTime.RAMConsumer.code_exec line 130
  17. def OAI.WLTime.RAMConsumer.oneTape line 153
  18. theorem OAI.WLTime.RAMConsumer.correct line 155
  19. theorem OAI.WLTime.RAMConsumer.code_size line 171
  20. def OAI.WLTime.OneTape.Symbolic.RAMWriter.consumer line 183
  21. def OAI.WLTime.OneTape.Symbolic.RAMWriter.consumerFactor line 185
  22. theorem OAI.WLTime.OneTape.Symbolic.RAMWriter.correct line 186
  23. def OAI.WLTime.OneTape.Symbolic.RAMWriter.tapesBound line 209
  24. def OAI.WLTime.OneTape.Symbolic.RAMWriter.alphabetBound line 210
  25. def OAI.WLTime.OneTape.Symbolic.RAMWriter.ramSize line 211
  26. theorem OAI.WLTime.OneTape.Symbolic.RAMWriter.ramSize_spec line 212
  27. def OAI.WLTime.OneTape.Symbolic.RAMWriter.statesBound line 214
  28. theorem OAI.WLTime.OneTape.Symbolic.RAMWriter.consumer_alphabet line 216
  29. theorem OAI.WLTime.OneTape.Symbolic.RAMWriter.consumer_states line 231
  30. theorem OAI.WLTime.Numeric.ram_consumer_small line 276
  31. def OAI.WLTime.OneTape.Symbolic.RAMWriter.widthFactor line 314
  32. theorem OAI.WLTime.OneTape.Symbolic.RAMWriter.width_small line 315
  33. theorem OAI.WLTime.OneTape.Symbolic.RAMWriter.word_cost_small line 328
  34. theorem OAI.WLTime.OneTape.Symbolic.RAMWriter.designation_small line 341
  35. theorem OAI.WLTime.diagonal_graph_contradiction line 375
  36. theorem OAI.WLTime.ram_decides_pair line 408
  37. theorem OAI.WLTime.ram_pointwise line 437