OAI/GroupTheory/SimpleOvergroups/CommonCompiler.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.retract line 18
  2. abbrev OAI.SimpleFInftyOvergroups.CommonCompiler.Letter line 56
  3. abbrev OAI.SimpleFInftyOvergroups.CommonCompiler.FiniteLetter line 57
  4. abbrev OAI.SimpleFInftyOvergroups.CommonCompiler.includeLetter line 60
  5. theorem OAI.SimpleFInftyOvergroups.CommonCompiler.includeLetter_injective line 63
  6. def OAI.SimpleFInftyOvergroups.CommonCompiler.retractLetter line 67
  7. theorem OAI.SimpleFInftyOvergroups.CommonCompiler.retract_include line 70
  8. theorem OAI.SimpleFInftyOvergroups.CommonCompiler.grade_include_letter line 76
  9. theorem OAI.SimpleFInftyOvergroups.CommonCompiler.grade_include line 81
  10. theorem OAI.SimpleFInftyOvergroups.CommonCompiler.grade_retract_letter line 88
  11. theorem OAI.SimpleFInftyOvergroups.CommonCompiler.grade_retract line 98
  12. abbrev OAI.SimpleFInftyOvergroups.CommonCompiler.includeWord line 104
  13. abbrev OAI.SimpleFInftyOvergroups.CommonCompiler.retractWord line 106
  14. theorem OAI.SimpleFInftyOvergroups.CommonCompiler.retract_include_word line 109
  15. def OAI.SimpleFInftyOvergroups.CommonCompiler.clamp line 119
  16. theorem OAI.SimpleFInftyOvergroups.CommonCompiler.include_retract line 123
  17. theorem OAI.SimpleFInftyOvergroups.CommonCompiler.clamp_words line 131
  18. theorem OAI.SimpleFInftyOvergroups.CommonCompiler.primrec_clamp line 138
  19. theorem OAI.SimpleFInftyOvergroups.CommonCompiler.primrec_letterGrade line 150
  20. theorem OAI.SimpleFInftyOvergroups.CommonCompiler.primrec_grade line 159
  21. def OAI.SimpleFInftyOvergroups.CommonCompiler.service line 172
  22. theorem OAI.SimpleFInftyOvergroups.CommonCompiler.partrec_service line 176
  23. def OAI.SimpleFInftyOvergroups.CommonCompiler.calculus line 182
  24. theorem OAI.SimpleFInftyOvergroups.CommonCompiler.service_full line 196