OAI/GroupTheory/SimpleOvergroups/VariableCode.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SimpleFInftyOvergroups.ContextualEncoding.DelimiterCode line 9
  2. def OAI.SimpleFInftyOvergroups.ContextualEncoding.DelimiterCode.block line 21
  3. def OAI.SimpleFInftyOvergroups.ContextualEncoding.DelimiterCode.encode line 22
  4. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.DelimiterCode.block_length line 24
  5. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.DelimiterCode.encode_nil line 26
  6. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.DelimiterCode.encode_cons line 27
  7. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.DelimiterCode.encode_append line 29
  8. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.DelimiterCode.length_le_encode line 32
  9. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.DelimiterCode.encode_eq_nil line 37
  10. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.DelimiterCode.split_at_stop line 45
  11. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.DelimiterCode.block_cancel line 66
  12. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.DelimiterCode.prefix_decode line 73
  13. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.DelimiterCode.encode_injective line 86
  14. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.DelimiterCode.split_past_avoiding line 92
  15. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.DelimiterCode.tail_avoids line 106
  16. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.DelimiterCode.marker_alignment line 109
  17. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.DelimiterCode.occurrence_decode line 127
  18. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.DelimiterCode.overlap_decode line 142
  19. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.DelimiterCode.encode_avoids line 161
  20. def OAI.SimpleFInftyOvergroups.ContextualEncoding.DelimiterCode.cost line 170
  21. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.DelimiterCode.cost_nil line 171
  22. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.DelimiterCode.cost_cons line 172
  23. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.DelimiterCode.cost_append line 174
  24. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.DelimiterCode.cost_bound line 177
  25. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.DelimiterCode.cost_le_quota line 187
  26. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.strict_dependency line 195