OAI/Computability/BinPacking/Search/ExtensionVerifier.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.ExtensionVerifierMachine.frontTapes line 9
  2. def OAI.BinPackingGap.ExtensionVerifierMachine.frontendAccepted line 13
  3. def OAI.BinPackingGap.ExtensionVerifierMachine.frontendExit line 17
  4. def OAI.BinPackingGap.ExtensionVerifierMachine.frontendTapes line 20
  5. theorem OAI.BinPackingGap.ExtensionVerifierMachine.frontTapes_fieldInput line 24
  6. theorem OAI.BinPackingGap.ExtensionVerifierMachine.frontend_of_decoded line 29
  7. def OAI.BinPackingGap.ExtensionVerifierMachine.pairedInputInTime line 37
  8. def OAI.BinPackingGap.ExtensionVerifierMachine.queryShapeInTime line 68
  9. def OAI.BinPackingGap.ExtensionVerifierMachine.queryGateInTime line 92
  10. def OAI.BinPackingGap.ExtensionVerifierMachine.witnessShapeInTime line 111
  11. def OAI.BinPackingGap.ExtensionVerifierMachine.witnessGateInTime line 135
  12. def OAI.BinPackingGap.ExtensionVerifierMachine.frontendInTime line 156
  13. def OAI.BinPackingGap.ExtensionVerifierMachine.extractedTapes line 189
  14. def OAI.BinPackingGap.ExtensionVerifierMachine.validationInput line 194
  15. def OAI.BinPackingGap.ExtensionVerifierMachine.checkedTapes line 200
  16. def OAI.BinPackingGap.ExtensionVerifierMachine.agreementInput line 205
  17. def OAI.BinPackingGap.ExtensionVerifierMachine.capacityInput line 211
  18. def OAI.BinPackingGap.ExtensionVerifierMachine.extractionInTime line 216
  19. def OAI.BinPackingGap.ExtensionVerifierMachine.prepareValidationInTime line 237
  20. def OAI.BinPackingGap.ExtensionVerifierMachine.prepareAgreementInTime line 270
  21. theorem OAI.BinPackingGap.ExtensionVerifierMachine.check_factor line 288
  22. def OAI.BinPackingGap.ExtensionVerifierMachine.canonicalBudget line 296
  23. structure OAI.BinPackingGap.ExtensionVerifierMachine.CanonicalRun line 310
  24. def OAI.BinPackingGap.ExtensionVerifierMachine.canonicalRun line 319
  25. def OAI.BinPackingGap.ExtensionVerifierMachine.canonicalTime line 448
  26. theorem OAI.BinPackingGap.ExtensionVerifierMachine.canonicalBudget_le line 452
  27. def OAI.BinPackingGap.ExtensionVerifierMachine.canonicalInPolynomialTime line 479
  28. def OAI.BinPackingGap.ExtensionVerifierMachine.decisionTime line 491
  29. structure OAI.BinPackingGap.ExtensionVerifierMachine.DecisionRun line 494
  30. def OAI.BinPackingGap.ExtensionVerifierMachine.decisionRun line 501
  31. theorem OAI.BinPackingGap.ExtensionVerifierMachine.initialConfiguration line 548
  32. theorem OAI.BinPackingGap.ExtensionVerifierMachine.finalConfiguration line 555
  33. theorem OAI.BinPackingGap.ExtensionVerifierMachine.initial_mass line 562
  34. def OAI.BinPackingGap.ExtensionVerifierMachine.timePolynomial line 567
  35. def OAI.BinPackingGap.ExtensionVerifierMachine.outputsInTime line 571
  36. def OAI.BinPackingGap.ExtensionVerifierMachine.computableInPolyTime line 606
  37. theorem OAI.BinPackingGap.ExtensionVerifierMachine.computation_finiteAlphabet line 622
  38. def OAI.BinPackingGap.packingExtensionVerifier line 633
  39. theorem OAI.BinPackingGap.packingExtensionVerifier_accepts line 639
  40. theorem OAI.BinPackingGap.packingExtension_inNP line 645
  41. theorem OAI.BinPackingGap.packingExtension_allNone line 650