OAI/GroupTheory/SimpleOvergroups/BoundedForms.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SimpleFInftyOvergroups.BoundedEncoding.WithBound line 9
  2. def OAI.SimpleFInftyOvergroups.BoundedEncoding.WithBound.key line 16
  3. abbrev OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.GLabel line 23
  4. abbrev OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.XLabel line 24
  5. def OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.identity line 26
  6. def OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.multiply line 27
  7. def OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.inverse line 29
  8. def OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.act line 30
  9. inductive OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.Letter line 33
  10. def OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.Letter.cost line 40
  11. def OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.Letter.key line 45
  12. abbrev OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.Form line 52
  13. def OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.Form.cost line 55
  14. def OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.Form.key line 59
  15. def OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.wordCost line 63
  16. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.wordCost_nil line 65
  17. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.wordCost_cons line 66
  18. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.wordCost_append line 68
  19. def OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.step line 73
  20. def OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.run line 82
  21. def OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.normalize line 85
  22. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.run_nil line 87
  23. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.run_cons line 88
  24. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.run_append line 90
  25. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.step_none line 93
  26. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.run_none line 94
  27. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.step_cost line 99
  28. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.run_cost line 116
  29. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.normalize_cost line 124
  30. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.step_congr line 128
  31. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.run_congr line 187
  32. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.normalize_left_context line 209