OAI/Computability/DegreeRigidity/Effective/LocalStage.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.LocalStage.pairProcedure line 13
  2. theorem OAI.TuringRigidity.LocalStage.pairProcedure_recursive line 15
  3. def OAI.TuringRigidity.LocalStage.candidate line 18
  4. theorem OAI.TuringRigidity.LocalStage.candidate_extends line 21
  5. def OAI.TuringRigidity.LocalStage.Changes line 27
  6. def OAI.TuringRigidity.LocalStage.scan line 30
  7. theorem OAI.TuringRigidity.LocalStage.scan_spec line 34
  8. def OAI.TuringRigidity.LocalStage.openProcedure line 49
  9. theorem OAI.TuringRigidity.LocalStage.open_extends line 51
  10. structure OAI.TuringRigidity.LocalStage.State line 55
  11. def OAI.TuringRigidity.LocalStage.generic line 60
  12. def OAI.TuringRigidity.LocalStage.stageAction line 63
  13. def OAI.TuringRigidity.LocalStage.stageWord line 65
  14. def OAI.TuringRigidity.LocalStage.advance line 70
  15. def OAI.TuringRigidity.LocalStage.construction line 75
  16. def OAI.TuringRigidity.LocalStage.conditions line 79
  17. def OAI.TuringRigidity.LocalStage.proposal line 81
  18. theorem OAI.TuringRigidity.LocalStage.action_not_done line 84
  19. theorem OAI.TuringRigidity.LocalStage.accept_action line 87
  20. theorem OAI.TuringRigidity.LocalStage.done_eq line 93
  21. theorem OAI.TuringRigidity.LocalStage.action_eq line 103
  22. theorem OAI.TuringRigidity.LocalStage.seen_eq line 108
  23. theorem OAI.TuringRigidity.LocalStage.active_eq line 116
  24. theorem OAI.TuringRigidity.LocalStage.stage_words line 119
  25. theorem OAI.TuringRigidity.LocalStage.word_growth line 129
  26. theorem OAI.TuringRigidity.LocalStage.length_bound line 135
  27. theorem OAI.TuringRigidity.LocalStage.level_step line 144
  28. theorem OAI.TuringRigidity.LocalStage.surviving_columns line 169
  29. theorem OAI.TuringRigidity.LocalStage.surviving_generic_visit line 176