OAI/Computability/WeisfeilerLeman/Consumer.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.WLTime.TMStack.execution_halted line 11
  2. theorem OAI.WLTime.TMStack.simulate line 19
  3. def OAI.WLTime.TMStack.initialTapes line 52
  4. theorem OAI.WLTime.TMStack.initial_relative line 55
  5. theorem OAI.WLTime.TMStack.initial_store line 75
  6. theorem OAI.WLTime.TMStack.machine_correct line 84
  7. def OAI.WLTime.TMStack.oneTape line 99
  8. theorem OAI.WLTime.TMStack.oneTape_correct line 101
  9. def OAI.WLTime.TMConsumer.decode line 120
  10. theorem OAI.WLTime.TMConsumer.decode_symbol line 121
  11. def OAI.WLTime.TMConsumer.boolInput line 123
  12. abbrev OAI.WLTime.TMConsumer.Reg line 124
  13. def OAI.WLTime.TMConsumer.tmInput line 125
  14. def OAI.WLTime.TMConsumer.prelude line 126
  15. abbrev OAI.WLTime.TMConsumer.State line 129
  16. instance OAI.WLTime.TMConsumer.(instance at line 130) line 130
  17. def OAI.WLTime.TMConsumer.transition line 132
  18. def OAI.WLTime.TMConsumer.machine line 136
  19. theorem OAI.WLTime.TMConsumer.prefix_exec line 143
  20. theorem OAI.WLTime.TMConsumer.machine_initial line 182
  21. theorem OAI.WLTime.TMConsumer.machine_correct line 192
  22. def OAI.WLTime.TMConsumer.oneTape line 210
  23. theorem OAI.WLTime.TMConsumer.oneTape_correct line 212
  24. abbrev OAI.WLTime.StackMachine.Machine.ControlCode line 234
  25. def OAI.WLTime.StackMachine.Machine.controlCode line 235
  26. def OAI.WLTime.StackMachine.Machine.decodeControl line 250
  27. theorem OAI.WLTime.StackMachine.Machine.decode_control line 267
  28. theorem OAI.WLTime.StackMachine.Machine.control_bound line 271
  29. theorem OAI.WLTime.StackMachine.Machine.compile_states_bound line 281
  30. theorem OAI.WLTime.StackMachine.Machine.compile_symbols line 284
  31. theorem OAI.WLTime.TypedStack.Code.mapLetters_controlSize line 292
  32. theorem OAI.WLTime.OneTape.Symbolic.FullWriter.consumer_bound line 299
  33. theorem OAI.WLTime.OneTape.Symbolic.FullWriter.card_reg line 318
  34. theorem OAI.WLTime.OneTape.Symbolic.FullWriter.encodeNat_length line 320
  35. def OAI.WLTime.OneTape.Symbolic.FullWriter.scratchBound line 324
  36. theorem OAI.WLTime.OneTape.Symbolic.FullWriter.scratch_le line 326
  37. def OAI.WLTime.OneTape.Symbolic.FullWriter.syntaxBound line 330
  38. theorem OAI.WLTime.OneTape.Symbolic.FullWriter.syntax_le line 334
  39. def OAI.WLTime.OneTape.Symbolic.FullWriter.consumer line 344
  40. theorem OAI.WLTime.OneTape.Symbolic.FullWriter.code_correct line 347
  41. def OAI.WLTime.OneTape.Symbolic.FullWriter.consumerFactor line 361
  42. theorem OAI.WLTime.OneTape.Symbolic.FullWriter.consumer_correct line 362
  43. theorem OAI.WLTime.OneTape.Symbolic.FullWriter.input_length line 376
  44. theorem OAI.WLTime.TMConsumer.prelude_size line 393
  45. theorem OAI.WLTime.TMConsumer.state_card line 398