OAI/Computability/MinUncut/Search/BlockEnumeration.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncut.Costed.PolyProgram.variableDrop line 13
  2. def OAI.MinUncut.Costed.PolyProgram.expressions line 32
  3. def OAI.MinUncut.Costed.Blocks.block line 41
  4. def OAI.MinUncut.Costed.Blocks.source line 42
  5. def OAI.MinUncut.Costed.Blocks.step line 43
  6. def OAI.MinUncut.Costed.Blocks.extractor line 46
  7. def OAI.MinUncut.Costed.Blocks.stepProgram line 51
  8. lemma OAI.MinUncut.Costed.Blocks.length_block line 63
  9. lemma OAI.MinUncut.Costed.Blocks.source_step line 66
  10. lemma OAI.MinUncut.Costed.Blocks.head_step line 74
  11. lemma OAI.MinUncut.Costed.Blocks.second_step line 75
  12. lemma OAI.MinUncut.Costed.Blocks.iterate_head line 77
  13. lemma OAI.MinUncut.Costed.Blocks.iterate_source line 82
  14. lemma OAI.MinUncut.Costed.Blocks.magnitude_append line 88
  15. lemma OAI.MinUncut.Costed.Blocks.magnitude_step line 93
  16. lemma OAI.MinUncut.Costed.Blocks.iterate_size line 103
  17. def OAI.MinUncut.Costed.Blocks.iterationProgram line 126
  18. lemma OAI.MinUncut.Costed.Blocks.iterate_accumulator line 139
  19. def OAI.MinUncut.Costed.Blocks.enumerate line 154