OAI/Combinatorics/MatchingCount/Complexity/GuardMachineBase.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.MachineCost.advance line 9
  2. def OAI.MatchingFPRAS.MachineCost.run line 10
  3. lemma OAI.MatchingFPRAS.MachineCost.run_add line 14
  4. lemma OAI.MatchingFPRAS.MachineCost.run_step_eq line 20
  5. def OAI.MatchingFPRAS.MachineCost.statementCost line 26
  6. lemma OAI.MatchingFPRAS.MachineCost.statementCost_pos line 33
  7. theorem OAI.MatchingFPRAS.MachineCost.statement_translation_time line 45
  8. def OAI.MatchingFPRAS.MachineCost.programCost line 93
  9. lemma OAI.MatchingFPRAS.MachineCost.statementCost_le_programCost line 95
  10. lemma OAI.MatchingFPRAS.MachineCost.programCost_pos line 98
  11. theorem OAI.MatchingFPRAS.MachineCost.run_translation_time line 101
  12. def OAI.MatchingFPRAS.PostCompiler.index line 138
  13. def OAI.MatchingFPRAS.PostCompiler.pack line 139
  14. def OAI.MatchingFPRAS.PostCompiler.unpack line 140
  15. lemma OAI.MatchingFPRAS.PostCompiler.unpack_pack line 143
  16. lemma OAI.MatchingFPRAS.PostCompiler.pack_ne_zero line 146
  17. def OAI.MatchingFPRAS.PostCompiler.packState line 148
  18. lemma OAI.MatchingFPRAS.PostCompiler.packState_of_mem line 151
  19. def OAI.MatchingFPRAS.PostCompiler.sealedMachine line 154
  20. abbrev OAI.MatchingFPRAS.PostCompiler.Phase line 159
  21. def OAI.MatchingFPRAS.PostCompiler.perform line 161
  22. def OAI.MatchingFPRAS.PostCompiler.phaseStep line 165
  23. def OAI.MatchingFPRAS.PostCompiler.well line 172
  24. def OAI.MatchingFPRAS.PostCompiler.embed line 173
  25. lemma OAI.MatchingFPRAS.PostCompiler.phaseStep_well line 178
  26. lemma OAI.MatchingFPRAS.PostCompiler.phaseStep_first line 190
  27. lemma OAI.MatchingFPRAS.PostCompiler.embed_step line 200
  28. lemma OAI.MatchingFPRAS.PostCompiler.phaseRun line 213
  29. lemma OAI.MatchingFPRAS.PostCompiler.phaseRun_stops line 223
  30. lemma OAI.MatchingFPRAS.PostCompiler.embed_fold line 235
  31. lemma OAI.MatchingFPRAS.PostCompiler.entry line 244
  32. lemma OAI.MatchingFPRAS.PostCompiler.initial_tick line 251
  33. lemma OAI.MatchingFPRAS.PostCompiler.halted_tick line 258
  34. lemma OAI.MatchingFPRAS.PostCompiler.halted_fold line 264
  35. theorem OAI.MatchingFPRAS.PostCompiler.seal_words line 270
  36. theorem OAI.MatchingFPRAS.PostCompiler.seal_outputs line 290
  37. theorem OAI.MatchingFPRAS.PostCompiler.outputs_extend line 314
  38. theorem OAI.MatchingFPRAS.PostCompiler.words_extend line 328
  39. lemma OAI.MatchingFPRAS.PostCompiler.finite_supported line 347
  40. def OAI.MatchingFPRAS.PostCompiler.compiled line 359
  41. theorem OAI.MatchingFPRAS.PostCompiler.compiled_outputs line 363
  42. theorem OAI.MatchingFPRAS.PostCompiler.compiled_words line 388