OAI/GroupTheory/SimpleOvergroups/BoundedContexts.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.display line 12
  2. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.wordCost_pres line 17
  3. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.wordCost_dels line 22
  4. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.wordCost_reverse line 27
  5. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.display_cost line 30
  6. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.display_congr line 36
  7. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.step_zero line 61
  8. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.step_identity line 63
  9. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.step_multiply line 71
  10. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.step_group_pre line 80
  11. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.step_delete_pre line 86
  12. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.step_delete_group line 92
  13. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.display_step line 108
  14. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.run_display_normalize line 153
  15. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.normalize_right_context line 174
  16. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.normalize_context line 191
  17. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.normalize_zero_context line 202
  18. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.normalize_nil_ne_zero line 214