OAI/Computability/MinUncut/PCP/ClauseLookup.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.discardFieldsTrace line 18
  2. inductive OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.Tape line 61
  3. inductive OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.Label line 65
  4. def OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.fieldDestination line 71
  5. def OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.readStart line 72
  6. def OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.readLoop line 73
  7. def OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.skipLabel line 74
  8. def OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.headerLabel line 75
  9. def OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.program line 78
  10. def OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.machine line 95
  11. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.atSkip line 106
  12. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.atReadStart line 110
  13. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.atReadLoop line 114
  14. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.atReadDone line 119
  15. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.discardHeadersTrace line 122
  16. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.discardSixTrace line 134
  17. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.readSixTrace line 144
  18. def OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.scanTapes line 160
  19. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.scanTapes_work line 164
  20. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.scanTapes_index line 168
  21. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.scanTapes_other line 173
  22. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.update_scanTapes_work line 178
  23. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.skipClausesTrace line 185
  24. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.fieldDestination_eq line 233
  25. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.fieldDestination_injective_below line 239
  26. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.readSix_output_field line 245
  27. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.readSix_output_work line 257
  28. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.readSix_output_frame line 265
  29. def OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.outputTapes line 273
  30. def OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.scanSteps line 279
  31. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.scanReadTrace line 285
  32. def OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.lookupSteps line 313
  33. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.lookupWithSplitTrace line 317
  34. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.output_formula line 347
  35. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.output_index line 353
  36. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.output_work line 359
  37. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.output_field line 365
  38. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.output_frame line 372
  39. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.clauseWords_six line 379
  40. def OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.fieldWords line 385
  41. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.output_fieldWords line 389
  42. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.lookupSteps_le_input line 395
  43. def OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.timePolynomial line 414
  44. theorem OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.timePolynomial_eval line 416
  45. def OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.lookupWithSplitInTime line 419
  46. def OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.lookupInTime line 439
  47. def OAI.MinUncutGames.Foundations.Hastad.SourceClauseLookup.machineInTime line 458