OAI/Computability/BinPacking/Search/ExtensionPairMachine.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingGap.ExtensionPairMachine.Tape line 9
  2. abbrev OAI.BinPackingGap.ExtensionPairMachine.Label line 10
  3. abbrev OAI.BinPackingGap.ExtensionPairMachine.State line 11
  4. abbrev OAI.BinPackingGap.ExtensionPairMachine.Alphabet line 12
  5. abbrev OAI.BinPackingGap.ExtensionPairMachine.machine line 13
  6. abbrev OAI.BinPackingGap.ExtensionPairMachine.tapes line 14
  7. abbrev OAI.BinPackingGap.ExtensionPairMachine.cfg line 15
  8. abbrev OAI.BinPackingGap.ExtensionPairMachine.pairTrace line 19
  9. abbrev OAI.BinPackingGap.ExtensionPairMachine.pairInTime line 20
  10. abbrev OAI.BinPackingGap.ExtensionPairMachine.pairHaltInTime line 21
  11. theorem OAI.BinPackingGap.ExtensionPairMachine.machine_finiteAlphabet line 23
  12. def OAI.BinPackingGap.ExtensionPairMachine.alphabetFintype line 27
  13. theorem OAI.BinPackingGap.ExtensionPairMachine.update_zero line 30
  14. theorem OAI.BinPackingGap.ExtensionPairMachine.update_one line 36
  15. theorem OAI.BinPackingGap.ExtensionPairMachine.joinTrace line 42
  16. theorem OAI.BinPackingGap.ExtensionPairMachine.countStep_empty line 46
  17. theorem OAI.BinPackingGap.ExtensionPairMachine.copyStep_missing line 56
  18. theorem OAI.BinPackingGap.ExtensionPairMachine.replicate_true_append_cons line 66
  19. theorem OAI.BinPackingGap.ExtensionPairMachine.countRejectTrace line 75
  20. theorem OAI.BinPackingGap.ExtensionPairMachine.copyRejectTrace line 90
  21. def OAI.BinPackingGap.ExtensionPairMachine.noTerminatorInTime line 109
  22. theorem OAI.BinPackingGap.ExtensionPairMachine.truncatedTrace line 122
  23. def OAI.BinPackingGap.ExtensionPairMachine.truncatedInTime line 136
  24. theorem OAI.BinPackingGap.ExtensionPairMachine.headerCases line 145
  25. theorem OAI.BinPackingGap.ExtensionPairMachine.decodePairAux_replicate line 160
  26. theorem OAI.BinPackingGap.ExtensionPairMachine.decodePair_replicate line 166
  27. theorem OAI.BinPackingGap.ExtensionPairMachine.decodePair_frame line 170
  28. theorem OAI.BinPackingGap.ExtensionPairMachine.decodePair_none_iff line 176
  29. theorem OAI.BinPackingGap.ExtensionPairMachine.pairBits_of_decodePair line 194
  30. theorem OAI.BinPackingGap.ExtensionPairMachine.malformedTrace line 215
  31. def OAI.BinPackingGap.ExtensionPairMachine.decodedInTime line 236
  32. structure OAI.BinPackingGap.ExtensionPairMachine.RejectedRun line 249
  33. def OAI.BinPackingGap.ExtensionPairMachine.malformedInTime line 256
  34. def OAI.BinPackingGap.ExtensionPairMachine.splitTime line 272
  35. theorem OAI.BinPackingGap.ExtensionPairMachine.success_steps_le_splitTime line 274
  36. theorem OAI.BinPackingGap.ExtensionPairMachine.rejected_steps_le_splitTime line 280
  37. def OAI.BinPackingGap.ExtensionPairMachine.ExitSpec line 286
  38. structure OAI.BinPackingGap.ExtensionPairMachine.SplitRun line 293
  39. def OAI.BinPackingGap.ExtensionPairMachine.splitInTime line 299