OAI/Computability/DirectedFeedback/Encoding/ExpanderTableWords.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Foundations.PCP.ExpanderTableWords.rotationWords line 58
  2. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableWords.rotationWords_length line 60
  3. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableWords.rotationWords_getElem line 64
  4. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableWords.rotationWords_get line 70
  5. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableWords.rotationWords_getElem? line 76
  6. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableWords.rotationWords_getElem?_none line 82
  7. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableWords.rotationWords_entry_lt line 86
  8. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableWords.rotationWords_lookup line 91
  9. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableWords.rotationWords_row_order line 97
  10. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableWords.decode_rotationWords line 102
  11. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableWords.decoded_lookup line 106
  12. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableWords.decoded_coordinate_lookup line 112
  13. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableWords.encode_rotationWords_length_eq line 119
  14. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableWords.encode_rotationWords_length_le line 123
  15. abbrev OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.Alphabet line 143
  16. abbrev OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.State line 144
  17. def OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.residue line 146
  18. def OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.nextResidue line 149
  19. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.nextResidue_residue line 152
  20. def OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.scanLoop line 158
  21. def OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.emitter line 171
  22. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.scanPushBound line 178
  23. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.emitterPushBound line 184
  24. abbrev OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.tapes line 191
  25. def OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.unaryTapes line 195
  26. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.unaryTapes_source line 200
  27. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.unaryTapes_quotient line 208
  28. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.unaryTapes_remainder line 215
  29. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.unaryTapes_other line 222
  30. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.update_source_inline_MachineFixedDivMod line 230
  31. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.update_quotient_inline_MachineFixedDivMod line 248
  32. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.update_remainder_inline_MachineFixedDivMod line 262
  33. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.scanAux_true line 268
  34. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.scanAux_false line 284
  35. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.scanStep_succ line 297
  36. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.scanStep_zero line 324
  37. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.emitterStep line 347
  38. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.trace_fromCount line 371
  39. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.divModTrace line 408
  40. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.divModFromTapes line 429
  41. def OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.divModInTime line 456
  42. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.scanTrace_fromCount line 480
  43. def OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.emitterWithFinish line 513
  44. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.emitterWithFinishPushBound line 521
  45. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.emitterWithFinishStep line 529
  46. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.divModTraceWithFinish line 555
  47. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedDivMod.divModFromTapesWithFinish line 583
  48. inductive OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.Tape line 624
  49. instance OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.(instance at line 631) line 631
  50. inductive OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.Label line 633
  51. abbrev OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.Ambient line 651
  52. abbrev OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.State line 652
  53. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.divisionStates line 655
  54. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.firstFinish line 662
  55. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.secondFinish line 666
  56. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.affinePlan line 670
  57. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.firstPlan line 675
  58. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.secondPlan line 679
  59. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.outputPlan line 683
  60. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.lookupTape line 687
  61. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.dirtyTape line 694
  62. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.statement line 704
  63. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.program line 769