OAI/Analysis/MarkovType/WordReduction.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.step line 13
  2. def OAI.MarkovSuperreflexivity.scanWord line 17
  3. def OAI.MarkovSuperreflexivity.reduceWord line 20
  4. def OAI.MarkovSuperreflexivity.reducedLength line 22
  5. def OAI.MarkovSuperreflexivity.ReducedWord line 24
  6. theorem OAI.MarkovSuperreflexivity.step_nil line 27
  7. theorem OAI.MarkovSuperreflexivity.step_cancel line 29
  8. theorem OAI.MarkovSuperreflexivity.step_keep line 32
  9. theorem OAI.MarkovSuperreflexivity.scanWord_nil line 35
  10. theorem OAI.MarkovSuperreflexivity.scanWord_cons line 37
  11. theorem OAI.MarkovSuperreflexivity.scanWord_append line 40
  12. theorem OAI.MarkovSuperreflexivity.scanWord_append_singleton line 44
  13. theorem OAI.MarkovSuperreflexivity.reduceWord_nil line 48
  14. theorem OAI.MarkovSuperreflexivity.reduceWord_append_singleton line 50
  15. theorem OAI.MarkovSuperreflexivity.reducedWord_nil line 54
  16. theorem OAI.MarkovSuperreflexivity.reducedWord_singleton line 56
  17. theorem OAI.MarkovSuperreflexivity.reducedWord_cons line 59
  18. theorem OAI.MarkovSuperreflexivity.ReducedWord.tail line 63
  19. theorem OAI.MarkovSuperreflexivity.ReducedWord.take line 66
  20. theorem OAI.MarkovSuperreflexivity.ReducedWord.drop line 69
  21. theorem OAI.MarkovSuperreflexivity.ReducedWord.reverse line 72
  22. theorem OAI.MarkovSuperreflexivity.reducedWord_append line 77
  23. theorem OAI.MarkovSuperreflexivity.ReducedWord.append line 82
  24. theorem OAI.MarkovSuperreflexivity.ReducedWord.step line 87
  25. theorem OAI.MarkovSuperreflexivity.reducedWord_scan line 101
  26. theorem OAI.MarkovSuperreflexivity.reducedWord_reduceWord line 109
  27. theorem OAI.MarkovSuperreflexivity.reduceWord_reduced line 112
  28. inductive OAI.MarkovSuperreflexivity.CancelPair line 115
  29. abbrev OAI.MarkovSuperreflexivity.WordReduction line 119
  30. theorem OAI.MarkovSuperreflexivity.scanWord_reachable line 122
  31. theorem OAI.MarkovSuperreflexivity.reduceWord_red line 146
  32. theorem OAI.MarkovSuperreflexivity.ReducedWord.no_cancel line 149
  33. theorem OAI.MarkovSuperreflexivity.ReducedWord.eq_of_reduction line 156
  34. theorem OAI.MarkovSuperreflexivity.reduceWord_of_reduced line 160
  35. theorem OAI.MarkovSuperreflexivity.reduceWord_idem line 163
  36. theorem OAI.MarkovSuperreflexivity.wordReduction_invariant line 167
  37. theorem OAI.MarkovSuperreflexivity.reduceWord_invariant line 176
  38. theorem OAI.MarkovSuperreflexivity.step_length_cons line 181
  39. theorem OAI.MarkovSuperreflexivity.step_length_le line 185
  40. theorem OAI.MarkovSuperreflexivity.step_cancels_iff line 192
  41. theorem OAI.MarkovSuperreflexivity.sum_step_length line 196
  42. theorem OAI.MarkovSuperreflexivity.scanWord_length_le line 207
  43. theorem OAI.MarkovSuperreflexivity.reducedLength_nil line 217
  44. theorem OAI.MarkovSuperreflexivity.reducedLength_le line 219
  45. theorem OAI.MarkovSuperreflexivity.sum_reducedLength_append line 223
  46. theorem OAI.MarkovSuperreflexivity.sum_reducedLength_append_ge line 229