OAI/GroupTheory/SimpleOvergroups/EffectiveCode.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleFInftyOvergroups.ContextualEncoding.PaddedCode.body line 13
  2. def OAI.SimpleFInftyOvergroups.ContextualEncoding.PaddedCode.code line 16
  3. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.PaddedCode.block_length line 31
  4. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.PaddedCode.descriptor_le_length line 36
  5. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.PaddedCode.cost_padding line 40
  6. def OAI.SimpleFInftyOvergroups.ContextualEncoding.PaddedCode.symbols line 44
  7. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.PaddedCode.mem_symbols_of_encode_le line 46
  8. def OAI.SimpleFInftyOvergroups.ContextualEncoding.PaddedCode.wordsOver line 51
  9. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.PaddedCode.mem_wordsOver line 56
  10. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.PaddedCode.block_length_le_encode line 83
  11. def OAI.SimpleFInftyOvergroups.ContextualEncoding.PaddedCode.words line 93
  12. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.PaddedCode.mem_words line 96
  13. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.PaddedCode.word_cost_bound line 108
  14. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.PaddedCode.primrec_replicate line 116
  15. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.PaddedCode.primrec_block line 120
  16. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.PaddedCode.primrec_encode line 131
  17. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.PaddedCode.primrec_symbols line 135
  18. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.PaddedCode.primrec_wordsOver line 139
  19. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.PaddedCode.primrec_words line 147