OAI/Computability/DegreeRigidity/Effective/FiniteShuffle.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.FiniteShuffle.Agree line 9
  2. theorem OAI.TuringRigidity.FiniteShuffle.Agree.mono line 11
  3. theorem OAI.TuringRigidity.FiniteShuffle.Agree.symm line 14
  4. theorem OAI.TuringRigidity.FiniteShuffle.Agree.trans line 17
  5. def OAI.TuringRigidity.FiniteShuffle.initial line 20
  6. theorem OAI.TuringRigidity.FiniteShuffle.prefix_length line 22
  7. theorem OAI.TuringRigidity.FiniteShuffle.prefix_getD line 25
  8. theorem OAI.TuringRigidity.FiniteShuffle.prefix_default line 29
  9. theorem OAI.TuringRigidity.FiniteShuffle.prefix_agree line 35
  10. def OAI.TuringRigidity.FiniteShuffle.OddBound line 42
  11. theorem OAI.TuringRigidity.FiniteShuffle.count_agree line 44
  12. theorem OAI.TuringRigidity.FiniteShuffle.count_constant line 53
  13. theorem OAI.TuringRigidity.FiniteShuffle.code_agree line 61
  14. theorem OAI.TuringRigidity.FiniteShuffle.code_agree_inserted line 72
  15. def OAI.TuringRigidity.FiniteShuffle.freeze line 85
  16. theorem OAI.TuringRigidity.FiniteShuffle.freeze_bound line 88
  17. theorem OAI.TuringRigidity.FiniteShuffle.agree_of_columns line 92
  18. theorem OAI.TuringRigidity.FiniteShuffle.freeze_agree line 104
  19. def OAI.TuringRigidity.FiniteShuffle.extendEven line 109
  20. theorem OAI.TuringRigidity.FiniteShuffle.extendEven_count line 112
  21. theorem OAI.TuringRigidity.FiniteShuffle.extendEven_agree line 116
  22. theorem OAI.TuringRigidity.FiniteShuffle.extendEven_bound line 121
  23. theorem OAI.TuringRigidity.FiniteShuffle.extendEven_code line 126
  24. theorem OAI.TuringRigidity.FiniteShuffle.initial_prefix line 154
  25. theorem OAI.TuringRigidity.FiniteShuffle.agree_of_prefix line 161
  26. def OAI.TuringRigidity.FiniteShuffle.DenseOpen line 168
  27. theorem OAI.TuringRigidity.FiniteShuffle.odd_null_extension line 171
  28. theorem OAI.TuringRigidity.FiniteShuffle.finite_extension line 190
  29. theorem OAI.TuringRigidity.FiniteShuffle.all_extension line 216