OAI/Computability/MinUncut/Estimates/ReversePrefixProgram.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncut.Costed.prefixStep line 9
  2. def OAI.MinUncut.Costed.prefixStepProgram line 12
  3. lemma OAI.MinUncut.Costed.prefixStep_safe line 15
  4. def OAI.MinUncut.Costed.reversePrefixProgram line 25
  5. lemma OAI.MinUncut.Costed.prefixStep_iter line 30
  6. lemma OAI.MinUncut.Costed.reversePrefix_spec line 55
  7. def OAI.MinUncut.Costed.Blocks.emitted line 64
  8. def OAI.MinUncut.Costed.Blocks.retained line 66
  9. lemma OAI.MinUncut.Costed.Blocks.block_reverse line 69
  10. lemma OAI.MinUncut.Costed.Blocks.enumerate_reverse line 72
  11. lemma OAI.MinUncut.Costed.Blocks.length_emitted line 75
  12. def OAI.MinUncut.Costed.Blocks.forward line 80