OAI/Analysis/FreeWords/ColoredExpansion.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.KKLocalPatching.Colored.Cell line 13
  2. def OAI.KKLocalPatching.Colored.old line 15
  3. def OAI.KKLocalPatching.Colored.changes line 17
  4. def OAI.KKLocalPatching.Colored.erase line 22
  5. theorem OAI.KKLocalPatching.Colored.erase_old line 24
  6. theorem OAI.KKLocalPatching.Colored.changes_length line 27
  7. theorem OAI.KKLocalPatching.Colored.erase_of_mem_changes line 34
  8. theorem OAI.KKLocalPatching.Colored.true_of_mem_changes line 46
  9. def OAI.KKLocalPatching.Colored.value line 57
  10. theorem OAI.KKLocalPatching.Colored.value_nil line 60
  11. theorem OAI.KKLocalPatching.Colored.value_cons line 62
  12. theorem OAI.KKLocalPatching.Colored.value_old line 65
  13. theorem OAI.KKLocalPatching.Colored.value_append line 69
  14. theorem OAI.KKLocalPatching.Colored.expansion line 73