OAI/GroupTheory/SimpleOvergroups/ContextualTables.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SimpleFInftyOvergroups.ContextualEncoding.FiniteSearch line 12
  2. def OAI.SimpleFInftyOvergroups.ContextualEncoding.PaddedCode.search line 18
  3. def OAI.SimpleFInftyOvergroups.ContextualEncoding.EncodedCanonical.candidates line 26
  4. def OAI.SimpleFInftyOvergroups.ContextualEncoding.EncodedCanonical.least line 29
  5. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.EncodedCanonical.least_mem line 33
  6. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.EncodedCanonical.least_length line 36
  7. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.EncodedCanonical.least_class line 39
  8. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.EncodedCanonical.least_min line 42
  9. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.EncodedCanonical.least_lt_or_eq line 46
  10. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.EncodedCanonical.least_global_min line 53
  11. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.EncodedCanonical.least_congr line 62
  12. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.EncodedCanonical.least_idem line 68
  13. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.EncodedCanonical.least_nil line 71
  14. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.EncodedCanonical.eq_least_iff line 76
  15. def OAI.SimpleFInftyOvergroups.ContextualEncoding.CodeTable.output line 94
  16. def OAI.SimpleFInftyOvergroups.ContextualEncoding.CodeTable.table line 97
  17. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.CodeTable.mem_table line 103
  18. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.CodeTable.output_congr line 111
  19. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.CodeTable.output_nil line 114
  20. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.CodeTable.whole_steps line 117
  21. def OAI.SimpleFInftyOvergroups.ContextualEncoding.CodeTable.Contextual line 127
  22. def OAI.SimpleFInftyOvergroups.ContextualEncoding.CodeTable.ZeroIdeal line 131
  23. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.CodeTable.branch_normalizes line 134
  24. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.CodeTable.occurrence_normalizes line 156
  25. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.CodeTable.critical_containment line 166
  26. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.CodeTable.critical_overlap line 179
  27. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.CodeTable.decreasing line 201
  28. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.CodeTable.stable line 216