OAI/Computability/BinPacking/Computation/FinalCNFRowTrace.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Buffer line 11
  2. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.readUnarySlots line 17
  3. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.unaryBits line 28
  4. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.unaryBits_eq_encodeWords line 31
  5. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.unaryBits_length_le line 38
  6. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.statementPushBound_readUnarySlots line 48
  7. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.stepAux_readUnarySlots line 59
  8. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.stepAux_readUnaryAll line 83
  9. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.unaryBlockMapAt line 96
  10. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.stepAux_unaryBlockMapAt line 104
  11. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.step_unaryBlockMapAt line 119
  12. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.unaryBlockInTime line 132
  13. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.unaryBits_relation line 149
  14. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.readerStateEquiv line 160
  15. abbrev OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.State line 171
  16. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.readRelationAt line 173
  17. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.stepAux_readRelationAt line 178
  18. inductive OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.Tape line 199
  19. abbrev OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.Tape.enumList line 204
  20. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.Tape.enumList_getElem?_ctorIdx_eq line 207
  21. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.Tape.enumList_nodup line 211
  22. instance OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.(instance at line 213) line 213
  23. abbrev OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.Ambient line 217
  24. abbrev OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.Plan line 218
  25. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.values line 220
  26. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan line 223
  27. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan_length line 227
  28. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan_bits line 230
  29. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.source line 238
  30. inductive OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.Label line 241
  31. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.guard line 253
  32. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.program line 260
  33. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.machine line 307
  34. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles line 318
  35. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_injective line 322
  36. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.headPhaseInTime line 325
  37. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.workingTapes line 341
  38. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.workingTapes_operands line 354
  39. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.update_working_input line 361
  40. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.update_working_tail line 368
  41. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.update_working_head line 375
  42. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.update_working_accumulator line 382
  43. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.update_working_rowIndex line 389
  44. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.source_ne_scratch line 397
  45. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.source_ne_accumulator line 400
  46. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.headerFrame line 414
  47. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.headerInputTapes line 426
  48. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes line 429
  49. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes_input line 434
  50. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes_archive line 437
  51. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes_accumulator line 440
  52. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes_rowIndex line 444
  53. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.headerTimePolynomial line 447
  54. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.headerTimePolynomial_eval line 450
  55. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.headerInTime line 454
  56. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.tableRowsBits line 583
  57. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.tableBits_header_rows line 586
  58. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.tableHeaderInTime line 592
  59. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.headerInput_configuration line 603
  60. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.initializedTableHeaderInTime line 611
  61. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.endpointTapes line 624
  62. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.endpointsInTime line 630
  63. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.relationInTime line 655
  64. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.emitInTime line 669
  65. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.finishTapes line 686
  66. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.finishInTime line 691