OAI/Computability/Superstring/WalkOutput.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Superstring.WalkCode.letter line 8
  2. def OAI.Superstring.WalkCode.output line 9
  3. theorem OAI.Superstring.WalkCode.output_nil line 10
  4. theorem OAI.Superstring.WalkCode.output_singleton line 11
  5. theorem OAI.Superstring.WalkCode.output_cons_cons line 12
  6. theorem OAI.Superstring.WalkCode.length_letter line 14
  7. theorem OAI.Superstring.WalkCode.length_output line 16
  8. theorem OAI.Superstring.WalkCode.letter_up line 21
  9. theorem OAI.Superstring.WalkCode.letter_down line 23
  10. theorem OAI.Superstring.WalkCode.visited_output line 25
  11. theorem OAI.Superstring.WalkCode.rooted_output line 40
  12. theorem OAI.Superstring.WalkCode.poly_letter line 51
  13. theorem OAI.Superstring.WalkCode.poly_output line 54
  14. theorem OAI.Superstring.CollectionCode.Model.tour_spec_general line 65
  15. theorem OAI.Superstring.CollectionCode.Model.charge_sum line 75
  16. def OAI.Superstring.ThreadArray.environment line 92
  17. theorem OAI.Superstring.ThreadArray.environment_rows line 95
  18. theorem OAI.Superstring.ThreadArray.environment_stride line 97
  19. theorem OAI.Superstring.ThreadArray.environment_data line 99
  20. def OAI.Superstring.ThreadArray.model line 104
  21. theorem OAI.Superstring.ThreadArray.poly_environment line 137
  22. abbrev OAI.Superstring.Executable.code line 148
  23. def OAI.Superstring.Executable.context line 149
  24. def OAI.Superstring.Executable.solve line 151
  25. theorem OAI.Superstring.Executable.poly_code line 152
  26. theorem OAI.Superstring.Executable.poly_context line 153
  27. theorem OAI.Superstring.Executable.poly_solve line 155
  28. theorem OAI.Superstring.Executable.represents line 161
  29. theorem OAI.Superstring.Executable.vertices_eq line 165
  30. theorem OAI.Superstring.Executable.length_vertices line 171
  31. theorem OAI.Superstring.Executable.closed line 178
  32. theorem OAI.Superstring.Executable.histogram line 181
  33. theorem OAI.Superstring.Executable.supply line 186
  34. theorem OAI.Superstring.Executable.solve_spec line 191