OAI/Computability/DirectedFeedback/Games/TupleBody.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.SlotCount line 13
  2. abbrev OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.QueryCount line 14
  3. abbrev OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.Query line 15
  4. inductive OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.Label line 17
  5. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.selected line 36
  6. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.main line 39
  7. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.framed line 41
  8. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.framedConfiguration line 46
  9. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.framed_stepAux line 55
  10. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.framed_step line 62
  11. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.framedExecution line 77
  12. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.finish line 92
  13. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.drainProgram line 98
  14. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.drainStatement line 102
  15. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.selectState line 107
  16. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.program line 112
  17. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.reset_step line 149
  18. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.resetInTime line 155
  19. structure OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.Ready line 163
  20. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.contextSignature line 189
  21. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.workingState line 192
  22. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.workingState_loader line 197
  23. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.arithmeticMetadata line 201
  24. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.queryMetadata line 207
  25. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.arithmeticState_working line 212
  26. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.queryState_working line 217
  27. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.select_workingState line 222
  28. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.rightValue line 227
  29. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.variableRank line 230
  30. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.leftValue line 233
  31. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.slotBudget line 236
  32. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.preparePhase line 244
  33. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.seedZeroPhase line 267
  34. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.drainPhase line 280
  35. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.clauseRankPhase line 294
  36. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.variableRankPhase line 311
  37. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.rightBasePhase line 332
  38. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.leftBasePhase line 354
  39. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.queryPhase line 379
  40. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.selectPhase line 404
  41. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.loaded_extra line 416
  42. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.Ready.loadedClean line 422
  43. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.loopSnapshot line 430
  44. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.rankSnapshot line 433
  45. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.baseSnapshot line 437
  46. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.slotInTime line 441
  47. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.slotAt line 538
  48. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.prefixBits line 541
  49. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.prefixBudget line 545
  50. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.prefixInTime line 549
  51. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.prefixBits_eq_ofFn line 582
  52. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.prefixBits_eq_tupleBits line 593
  53. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.setupBudget line 604
  54. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.finishBudget line 614
  55. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.bodyBudget line 617
  56. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.setupInTime line 620
  57. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.finishInTime line 689
  58. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.bodyInTime line 748
  59. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBody.machine line 769