OAI/GroupTheory/SimpleOvergroups/ContextualCompiler.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.Sigma line 18
  2. def OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.rel line 20
  3. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.wf_rel line 27
  4. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.primrec_shortlex line 29
  5. def OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.raw line 33
  6. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.raw_encode line 36
  7. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.partrec_raw line 40
  8. abbrev OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.terminalAlphabet line 44
  9. abbrev OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.terminalMachine line 46
  10. structure OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.Family line 49
  11. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.exists_family line 65
  12. def OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.family line 75
  13. abbrev OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.Syntax line 85
  14. abbrev OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.Acting line 86
  15. abbrev OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.Points line 87
  16. abbrev OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.ops line 92
  17. abbrev OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.Symbols line 95
  18. abbrev OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.Keys line 101
  19. def OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.cost line 117
  20. def OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.code line 122
  21. def OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.search line 123
  22. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.primrec_cost line 126
  23. def OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.normal line 138
  24. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.partrec_normal line 141
  25. def OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.test line 144
  26. def OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.tables line 150
  27. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.partrec_test line 154
  28. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.partrec_tables line 163
  29. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.exists_fixed_point line 170
  30. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.certificate line 188
  31. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.all_budgets line 210
  32. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.Source.exists_total_fixed_point line 220