OAI/Computability/DegreeRigidity/Effective/GuardedStage.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.GuardedStage.pairProcedure line 13
  2. theorem OAI.TuringRigidity.GuardedStage.pairProcedure_recursive line 15
  3. def OAI.TuringRigidity.GuardedStage.candidate line 19
  4. theorem OAI.TuringRigidity.GuardedStage.candidate_extends line 22
  5. def OAI.TuringRigidity.GuardedStage.Changes line 28
  6. def OAI.TuringRigidity.GuardedStage.scan line 31
  7. theorem OAI.TuringRigidity.GuardedStage.scan_spec line 35
  8. def OAI.TuringRigidity.GuardedStage.openProcedure line 50
  9. theorem OAI.TuringRigidity.GuardedStage.open_extends line 53
  10. structure OAI.TuringRigidity.GuardedStage.State line 58
  11. def OAI.TuringRigidity.GuardedStage.generic line 63
  12. def OAI.TuringRigidity.GuardedStage.stageAction line 66
  13. def OAI.TuringRigidity.GuardedStage.stageWord line 68
  14. def OAI.TuringRigidity.GuardedStage.advance line 73
  15. def OAI.TuringRigidity.GuardedStage.construction line 78
  16. def OAI.TuringRigidity.GuardedStage.conditions line 82
  17. def OAI.TuringRigidity.GuardedStage.proposal line 84
  18. theorem OAI.TuringRigidity.GuardedStage.action_not_done line 87
  19. theorem OAI.TuringRigidity.GuardedStage.accept_action line 90
  20. theorem OAI.TuringRigidity.GuardedStage.done_eq line 96
  21. theorem OAI.TuringRigidity.GuardedStage.action_eq line 106
  22. theorem OAI.TuringRigidity.GuardedStage.seen_eq line 111
  23. theorem OAI.TuringRigidity.GuardedStage.active_eq line 119
  24. theorem OAI.TuringRigidity.GuardedStage.stage_words line 122
  25. theorem OAI.TuringRigidity.GuardedStage.word_growth line 132
  26. theorem OAI.TuringRigidity.GuardedStage.length_bound line 138
  27. theorem OAI.TuringRigidity.GuardedStage.level_step line 147
  28. theorem OAI.TuringRigidity.GuardedStage.surviving_columns line 172
  29. theorem OAI.TuringRigidity.GuardedStage.surviving_generic_visit line 179