OAI/Computability/DegreeRigidity/Representation/CommonIdeal.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.CommonIdeal.bit line 10
  2. def OAI.TuringRigidity.CommonIdeal.table line 12
  3. def OAI.TuringRigidity.CommonIdeal.run line 14
  4. def OAI.TuringRigidity.CommonIdeal.Extends line 17
  5. theorem OAI.TuringRigidity.CommonIdeal.table_mono line 20
  6. theorem OAI.TuringRigidity.CommonIdeal.table_total line 31
  7. theorem OAI.TuringRigidity.CommonIdeal.run_mono line 46
  8. theorem OAI.TuringRigidity.CommonIdeal.run_total line 56
  9. def OAI.TuringRigidity.CommonIdeal.initialWord line 67
  10. theorem OAI.TuringRigidity.CommonIdeal.prefix_length line 69
  11. theorem OAI.TuringRigidity.CommonIdeal.prefix_getD line 72
  12. theorem OAI.TuringRigidity.CommonIdeal.extends_prefix line 76
  13. theorem OAI.TuringRigidity.CommonIdeal.prefix_mono line 80
  14. theorem OAI.TuringRigidity.CommonIdeal.table_prefix line 86
  15. theorem OAI.TuringRigidity.CommonIdeal.run_approximates line 91
  16. theorem OAI.TuringRigidity.CommonIdeal.prefix_of_extends line 105
  17. theorem OAI.TuringRigidity.CommonIdeal.run_finite_extension line 113
  18. def OAI.TuringRigidity.CommonIdeal.Disagree line 121
  19. def OAI.TuringRigidity.CommonIdeal.Agree line 124
  20. def OAI.TuringRigidity.CommonIdeal.Requirement line 128
  21. theorem OAI.TuringRigidity.CommonIdeal.requirement_dense line 131
  22. theorem OAI.TuringRigidity.CommonIdeal.requirement_mono line 142
  23. theorem OAI.TuringRigidity.CommonIdeal.agree_of_common_output line 149
  24. theorem OAI.TuringRigidity.CommonIdeal.agreeing_search_sound line 162
  25. theorem OAI.TuringRigidity.CommonIdeal.agreeing_search_complete line 171