OAI/GroupTheory/SimpleOvergroups/NamedActions.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Operations line 9
  2. abbrev OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Letter line 21
  3. abbrev OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Form line 22
  4. abbrev OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Result line 23
  5. def OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Operations.letterCost line 28
  6. def OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Operations.wordCost line 33
  7. def OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Operations.formCost line 35
  8. def OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Operations.formKey line 39
  9. def OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Operations.plan line 42
  10. def OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Operations.totalStep line 54
  11. def OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Operations.totalRun line 57
  12. def OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Operations.totalNormalize line 60
  13. def OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Operations.totalTest line 63
  14. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Operations.totalRun_nil line 66
  15. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Operations.totalRun_cons line 67
  16. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Operations.wordCost_nil line 69
  17. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Operations.wordCost_cons line 70
  18. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Operations.wordCost_append line 72
  19. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Operations.totalStep_none line 74
  20. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Operations.totalStep_cost line 77
  21. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Operations.totalRun_cost line 94
  22. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Operations.totalNormalize_cost line 101
  23. structure OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Interpretation line 107
  24. def OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Interpretation.gkey line 122
  25. def OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Interpretation.xkey line 123
  26. def OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Interpretation.letter line 125
  27. def OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Interpretation.form line 131
  28. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Interpretation.letter_cost line 134
  29. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Interpretation.form_cost line 142
  30. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Interpretation.word_cost line 148
  31. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Interpretation.form_key line 151
  32. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Interpretation.totalStep line 158
  33. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Interpretation.totalRun line 179
  34. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Interpretation.totalNormalize line 185
  35. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Interpretation.totalTest line 192
  36. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Interpretation.totalTest_context line 197
  37. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Interpretation.totalTest_zero_context line 206
  38. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.NamedAction.Interpretation.totalTest_nil line 213