OAI/Computability/DirectedFeedback/Games/Target.lean

GitHub source file

112 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.DFVSGames.Foundations.Target.Literal line 9
  2. def OAI.DFVSGames.Foundations.Target.Literal.eval line 14
  3. abbrev OAI.DFVSGames.Foundations.Target.Clause line 17
  4. def OAI.DFVSGames.Foundations.Target.Clause.eval line 19
  5. structure OAI.DFVSGames.Foundations.Target.Formula line 22
  6. def OAI.DFVSGames.Foundations.Target.Formula.Satisfiable line 26
  7. structure OAI.DFVSGames.Foundations.Target.PermutationTable line 30
  8. theorem OAI.DFVSGames.Foundations.Target.PermutationTable.images_injective line 36
  9. theorem OAI.DFVSGames.Foundations.Target.PermutationTable.images_surjective line 41
  10. structure OAI.DFVSGames.Foundations.Target.Constraint line 45
  11. def OAI.DFVSGames.Foundations.Target.Constraint.satisfied line 50
  12. structure OAI.DFVSGames.Foundations.Target.Instance line 54
  13. def OAI.DFVSGames.Foundations.Target.countSatisfied line 59
  14. theorem OAI.DFVSGames.Foundations.Target.countSatisfied_le_length line 65
  15. theorem OAI.DFVSGames.Foundations.Target.Instance.constraintCount_positive line 74
  16. structure OAI.DFVSGames.Foundations.Target.RationalError line 80
  17. def OAI.DFVSGames.Foundations.Target.CompleteAt line 87
  18. def OAI.DFVSGames.Foundations.Target.SoundAt line 93
  19. structure OAI.DFVSGames.Foundations.Target.SemanticGapReduction line 98
  20. def OAI.DFVSGames.Foundations.Complexity.encodeWord line 112
  21. def OAI.DFVSGames.Foundations.Complexity.encodeWords line 114
  22. def OAI.DFVSGames.Foundations.Complexity.decodeWordsAux line 118
  23. def OAI.DFVSGames.Foundations.Complexity.decodeWords line 124
  24. theorem OAI.DFVSGames.Foundations.Complexity.decodeWordsAux_word line 126
  25. theorem OAI.DFVSGames.Foundations.Complexity.decodeWords_encodeWords line 136
  26. theorem OAI.DFVSGames.Foundations.Complexity.encodeWords_injective line 144
  27. theorem OAI.DFVSGames.Foundations.Complexity.encodeWord_length line 149
  28. theorem OAI.DFVSGames.Foundations.Complexity.encodeWords_append line 152
  29. theorem OAI.DFVSGames.Foundations.Complexity.encodeWords_length line 158
  30. theorem OAI.DFVSGames.Foundations.Complexity.encodeWords_length_le line 164
  31. def OAI.DFVSGames.Foundations.Complexity.literalWords line 178
  32. def OAI.DFVSGames.Foundations.Complexity.clauseWords line 181
  33. def OAI.DFVSGames.Foundations.Complexity.formulaWords line 184
  34. def OAI.DFVSGames.Foundations.Complexity.formulaBits line 187
  35. theorem OAI.DFVSGames.Foundations.Complexity.literalWords_length line 189
  36. theorem OAI.DFVSGames.Foundations.Complexity.clauseWords_length line 192
  37. theorem OAI.DFVSGames.Foundations.Complexity.clausesWords_length line 195
  38. theorem OAI.DFVSGames.Foundations.Complexity.formulaWords_length line 204
  39. theorem OAI.DFVSGames.Foundations.Complexity.literalBits_length_le line 209
  40. theorem OAI.DFVSGames.Foundations.Complexity.clauseBits_length_le line 214
  41. theorem OAI.DFVSGames.Foundations.Complexity.clausesBits_length_le line 222
  42. theorem OAI.DFVSGames.Foundations.Complexity.formulaBits_length_le line 232
  43. abbrev OAI.DFVSGames.Foundations.Hastad.SourceMachine.Alphabet line 251
  44. def OAI.DFVSGames.Foundations.Hastad.SourceMachine.fieldLoop line 253
  45. def OAI.DFVSGames.Foundations.Hastad.SourceMachine.fieldStart line 261
  46. def OAI.DFVSGames.Foundations.Hastad.SourceMachine.fieldTapes line 265
  47. theorem OAI.DFVSGames.Foundations.Hastad.SourceMachine.fieldTapes_source line 269
  48. theorem OAI.DFVSGames.Foundations.Hastad.SourceMachine.fieldTapes_destination line 274
  49. theorem OAI.DFVSGames.Foundations.Hastad.SourceMachine.fieldTapes_self line 279
  50. theorem OAI.DFVSGames.Foundations.Hastad.SourceMachine.fieldTapes_other line 283
  51. theorem OAI.DFVSGames.Foundations.Hastad.SourceMachine.update_field_source_inline_SourceMachine line 289
  52. theorem OAI.DFVSGames.Foundations.Hastad.SourceMachine.update_field_destination_inline_SourceMachine line 300
  53. theorem OAI.DFVSGames.Foundations.Hastad.SourceMachine.fieldStep_delimiter line 306
  54. theorem OAI.DFVSGames.Foundations.Hastad.SourceMachine.fieldStep_true line 320
  55. theorem OAI.DFVSGames.Foundations.Hastad.SourceMachine.fieldLoopTrace line 334
  56. theorem OAI.DFVSGames.Foundations.Hastad.SourceMachine.fieldStartStep line 366
  57. def OAI.DFVSGames.Foundations.Hastad.SourceMachine.fieldInTime line 380
  58. def OAI.DFVSGames.Foundations.Hastad.SourceMachine.afterField line 410
  59. def OAI.DFVSGames.Foundations.Hastad.SourceMachine.fieldNext line 414
  60. def OAI.DFVSGames.Foundations.Hastad.SourceMachine.fourTapes line 421
  61. theorem OAI.DFVSGames.Foundations.Hastad.SourceMachine.fourTapes_source line 428
  62. theorem OAI.DFVSGames.Foundations.Hastad.SourceMachine.fourTapes_other line 434
  63. theorem OAI.DFVSGames.Foundations.Hastad.SourceMachine.fourField_time_eq_length line 440
  64. def OAI.DFVSGames.Foundations.Hastad.SourceMachine.fourFieldsInTime line 445
  65. def OAI.DFVSGames.Foundations.Hastad.SourceMachine.fieldDestination line 489
  66. theorem OAI.DFVSGames.Foundations.Hastad.SourceMachine.fourTapes_concrete line 491
  67. def OAI.DFVSGames.Foundations.Hastad.SourceMachine.groupingProgram line 503
  68. def OAI.DFVSGames.Foundations.Hastad.SourceMachine.groupingMachine line 510
  69. def OAI.DFVSGames.Foundations.Hastad.SourceMachine.groupingMachineInTime line 521
  70. abbrev OAI.DFVSGames.Foundations.Complexity.MachineDrain.Alphabet line 545
  71. def OAI.DFVSGames.Foundations.Complexity.MachineDrain.drain line 547
  72. theorem OAI.DFVSGames.Foundations.Complexity.MachineDrain.drainTrace line 554
  73. def OAI.DFVSGames.Foundations.Complexity.MachineDrain.drainInTime line 575
  74. def OAI.DFVSGames.Foundations.Complexity.MachineFiniteSequence.Label line 600
  75. instance OAI.DFVSGames.Foundations.Complexity.MachineFiniteSequence.labelFintype line 604
  76. instance OAI.DFVSGames.Foundations.Complexity.MachineFiniteSequence.labelDecidableEq line 612
  77. def OAI.DFVSGames.Foundations.Complexity.MachineFiniteSequence.entry line 623
  78. def OAI.DFVSGames.Foundations.Complexity.MachineFiniteSequence.instruction line 630
  79. def OAI.DFVSGames.Foundations.Complexity.MachineFiniteSequence.resultOf line 641
  80. def OAI.DFVSGames.Foundations.Complexity.MachineFiniteSequence.steps line 645
  81. theorem OAI.DFVSGames.Foundations.Complexity.MachineFiniteSequence.trace line 651
  82. abbrev OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.Alphabet line 698
  83. abbrev OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.Tapes line 699
  84. abbrev OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.LocalLabel line 700
  85. abbrev OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.Label line 701
  86. abbrev OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.Data line 702
  87. def OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.entry line 704
  88. def OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.localInstruction line 707
  89. def OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.instruction line 711
  90. def OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.result line 716
  91. def OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.cost line 719
  92. def OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.finalTapes line 721
  93. def OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.finalRegister line 725
  94. theorem OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.finalRegister_none line 730
  95. def OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.steps line 733
  96. theorem OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.sequence_result line 738
  97. theorem OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.sequence_steps line 748
  98. theorem OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.finalTapes_apply line 755
  99. theorem OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.finalTapes_mem line 766
  100. theorem OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.finalTapes_not_mem line 769
  101. def OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.lengthSum line 772
  102. theorem OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.lengthSum_mono line 776
  103. theorem OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.steps_le line 785
  104. theorem OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.steps_le_uniform line 801
  105. theorem OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.trace line 816
  106. def OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.execution line 837
  107. def OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.workTapes line 849
  108. theorem OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.mem_workTapes line 852
  109. theorem OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.workTapes_length_le line 859
  110. def OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.haltTapes line 864
  111. theorem OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.finalTapes_workTapes line 867
  112. theorem OAI.DFVSGames.Foundations.Complexity.MachineDrainMany.cleanupTrace line 877