OAI/Computability/DirectedFeedback/Encoding/CanonicalWordTemplate.lean

GitHub source file

138 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.DFVSGames.Reduction.CanonicalWordTemplate.Token line 56
  2. def OAI.DFVSGames.Reduction.CanonicalWordTemplate.evalToken line 62
  3. def OAI.DFVSGames.Reduction.CanonicalWordTemplate.evalTemplate line 67
  4. def OAI.DFVSGames.Reduction.CanonicalWordTemplate.isVariable line 71
  5. def OAI.DFVSGames.Reduction.CanonicalWordTemplate.variableTokens line 76
  6. def OAI.DFVSGames.Reduction.CanonicalWordTemplate.blankTemplate line 78
  7. def OAI.DFVSGames.Reduction.CanonicalWordTemplate.singleTemplate line 82
  8. def OAI.DFVSGames.Reduction.CanonicalWordTemplate.fullTemplate line 87
  9. def OAI.DFVSGames.Reduction.CanonicalWordTemplate.template line 93
  10. theorem OAI.DFVSGames.Reduction.CanonicalWordTemplate.blankTemplate_length line 100
  11. theorem OAI.DFVSGames.Reduction.CanonicalWordTemplate.singleTemplate_length line 102
  12. theorem OAI.DFVSGames.Reduction.CanonicalWordTemplate.fullTemplate_length line 105
  13. theorem OAI.DFVSGames.Reduction.CanonicalWordTemplate.template_length line 108
  14. theorem OAI.DFVSGames.Reduction.CanonicalWordTemplate.evalTemplate_length line 113
  15. theorem OAI.DFVSGames.Reduction.CanonicalWordTemplate.eval_blankTemplate line 117
  16. theorem OAI.DFVSGames.Reduction.CanonicalWordTemplate.eval_singleTemplate line 121
  17. theorem OAI.DFVSGames.Reduction.CanonicalWordTemplate.eval_fullTemplate line 127
  18. theorem OAI.DFVSGames.Reduction.CanonicalWordTemplate.eval_template line 133
  19. theorem OAI.DFVSGames.Reduction.CanonicalWordTemplate.variableTokens_blankTemplate line 140
  20. theorem OAI.DFVSGames.Reduction.CanonicalWordTemplate.variableTokens_singleTemplate line 142
  21. theorem OAI.DFVSGames.Reduction.CanonicalWordTemplate.variableTokens_fullTemplate line 146
  22. theorem OAI.DFVSGames.Reduction.CanonicalWordTemplate.variableTokens_template line 150
  23. theorem OAI.DFVSGames.Reduction.CanonicalWordTemplate.variableTokens_template_length_le_one line 160
  24. theorem OAI.DFVSGames.Reduction.CanonicalWordTemplate.name_mem_variableTokens_iff line 165
  25. theorem OAI.DFVSGames.Reduction.CanonicalWordTemplate.occurrence_mem_variableTokens_iff line 173
  26. theorem OAI.DFVSGames.Reduction.CanonicalWordTemplate.flatMap_encodeWord line 179
  27. theorem OAI.DFVSGames.Reduction.CanonicalWordTemplate.template_bits line 188
  28. inductive OAI.DFVSGames.Reduction.CanonicalBodyTemplate.Token line 208
  29. def OAI.DFVSGames.Reduction.CanonicalBodyTemplate.evalToken line 213
  30. def OAI.DFVSGames.Reduction.CanonicalBodyTemplate.evalTemplate line 217
  31. def OAI.DFVSGames.Reduction.CanonicalBodyTemplate.nameField line 220
  32. def OAI.DFVSGames.Reduction.CanonicalBodyTemplate.recordFields line 222
  33. theorem OAI.DFVSGames.Reduction.CanonicalBodyTemplate.recordFields_name line 225
  34. theorem OAI.DFVSGames.Reduction.CanonicalBodyTemplate.recordFields_occurrence line 229
  35. def OAI.DFVSGames.Reduction.CanonicalBodyTemplate.sourceFields line 232
  36. def OAI.DFVSGames.Reduction.CanonicalBodyTemplate.liftToken line 236
  37. def OAI.DFVSGames.Reduction.CanonicalBodyTemplate.liftRecord line 241
  38. theorem OAI.DFVSGames.Reduction.CanonicalBodyTemplate.liftRecord_length line 244
  39. theorem OAI.DFVSGames.Reduction.CanonicalBodyTemplate.eval_liftToken line 247
  40. theorem OAI.DFVSGames.Reduction.CanonicalBodyTemplate.eval_liftRecord line 253
  41. def OAI.DFVSGames.Reduction.CanonicalBodyTemplate.recordsList line 261
  42. theorem OAI.DFVSGames.Reduction.CanonicalBodyTemplate.recordsList_length line 265
  43. theorem OAI.DFVSGames.Reduction.CanonicalBodyTemplate.eval_recordsList line 275
  44. def OAI.DFVSGames.Reduction.CanonicalBodyTemplate.ambientShift line 293
  45. def OAI.DFVSGames.Reduction.CanonicalBodyTemplate.alphabetOffset line 297
  46. def OAI.DFVSGames.Reduction.CanonicalBodyTemplate.template line 301
  47. theorem OAI.DFVSGames.Reduction.CanonicalBodyTemplate.template_length line 305
  48. theorem OAI.DFVSGames.Reduction.CanonicalBodyTemplate.eval_data line 310
  49. theorem OAI.DFVSGames.Reduction.CanonicalBodyTemplate.alphabetOffset_data line 324
  50. theorem OAI.DFVSGames.Reduction.CanonicalBodyTemplate.eval_canonical line 330
  51. theorem OAI.DFVSGames.Reduction.CanonicalBodyTemplate.alphabetOffset_canonical line 340
  52. def OAI.DFVSGames.Reduction.CanonicalBodyTemplate.coefficientTriples line 347
  53. theorem OAI.DFVSGames.Reduction.CanonicalBodyTemplate.fromCoefficients_hBasis line 351
  54. theorem OAI.DFVSGames.Reduction.CanonicalBodyTemplate.standardTriple_fromCoefficients line 356
  55. theorem OAI.DFVSGames.Reduction.CanonicalBodyTemplate.eval_actualQuery line 367
  56. theorem OAI.DFVSGames.Reduction.CanonicalBodyTemplate.alphabetOffset_actualQuery line 375
  57. theorem OAI.DFVSGames.Reduction.CanonicalBodyTemplate.eval_fromCoefficients line 381
  58. theorem OAI.DFVSGames.Reduction.CanonicalBodyTemplate.alphabetOffset_fromCoefficients line 390
  59. theorem OAI.DFVSGames.Reduction.CanonicalBodyTemplate.actualEdge_permutation line 398
  60. theorem OAI.DFVSGames.Reduction.CanonicalBodyTemplate.flatMap_encodeWord line 409
  61. theorem OAI.DFVSGames.Reduction.CanonicalBodyTemplate.actualQuery_bits line 418
  62. def OAI.DFVSGames.Reduction.CanonicalBodyMachine.fieldEquiv line 438
  63. def OAI.DFVSGames.Reduction.CanonicalBodyMachine.fieldIndex line 441
  64. theorem OAI.DFVSGames.Reduction.CanonicalBodyMachine.fieldIndex_val line 444
  65. def OAI.DFVSGames.Reduction.CanonicalBodyMachine.savedFields line 447
  66. theorem OAI.DFVSGames.Reduction.CanonicalBodyMachine.savedFields_fieldIndex line 450
  67. def OAI.DFVSGames.Reduction.CanonicalBodyMachine.lowerToken line 455
  68. def OAI.DFVSGames.Reduction.CanonicalBodyMachine.lowerTemplate line 459
  69. theorem OAI.DFVSGames.Reduction.CanonicalBodyMachine.lowerTemplate_length line 462
  70. theorem OAI.DFVSGames.Reduction.CanonicalBodyMachine.tokenOutput_lowerToken line 465
  71. theorem OAI.DFVSGames.Reduction.CanonicalBodyMachine.templateOutput_lowerTemplate line 472
  72. def OAI.DFVSGames.Reduction.CanonicalBodyMachine.template line 480
  73. theorem OAI.DFVSGames.Reduction.CanonicalBodyMachine.template_length line 484
  74. theorem OAI.DFVSGames.Reduction.CanonicalBodyMachine.templateOutput_data line 489
  75. theorem OAI.DFVSGames.Reduction.CanonicalBodyMachine.templateOutput_actualQuery line 498
  76. theorem OAI.DFVSGames.Reduction.CanonicalBodyMachine.templateOutput_fromCoefficients line 507
  77. abbrev OAI.DFVSGames.Reduction.AddressMachineSpace.Extra line 526
  78. abbrev OAI.DFVSGames.Reduction.AddressMachineSpace.Tape line 530
  79. abbrev OAI.DFVSGames.Reduction.AddressMachineSpace.Control line 533
  80. abbrev OAI.DFVSGames.Reduction.AddressMachineSpace.State line 534
  81. def OAI.DFVSGames.Reduction.AddressMachineSpace.initialState line 536
  82. def OAI.DFVSGames.Reduction.AddressMachineSpace.headerArithmeticSlots line 540
  83. def OAI.DFVSGames.Reduction.AddressMachineSpace.headerTape line 545
  84. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.headerTape_eq_iff line 548
  85. def OAI.DFVSGames.Reduction.AddressMachineSpace.fullHeaderSlots line 552
  86. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.fullHeaderSlots_source line 564
  87. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.fullHeaderSlots_work line 565
  88. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.fullHeaderSlots_arithmetic line 566
  89. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.arithmeticSlots_fullHeaderSlots line 569
  90. def OAI.DFVSGames.Reduction.AddressMachineSpace.prefixSlots line 573
  91. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.prefixSlots_source line 576
  92. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.prefixSlots_work line 577
  93. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.prefixSlots_variables line 578
  94. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.prefixSlots_occurrences line 580
  95. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.prefixSlots_scratch line 582
  96. def OAI.DFVSGames.Reduction.AddressMachineSpace.canonicalField line 585
  97. def OAI.DFVSGames.Reduction.AddressMachineSpace.rhsField line 588
  98. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.canonicalField_occurrence line 590
  99. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.canonicalField_name line 593
  100. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.canonicalField_ne_rhsField line 604
  101. def OAI.DFVSGames.Reduction.AddressMachineSpace.privateAddress line 608
  102. def OAI.DFVSGames.Reduction.AddressMachineSpace.edgeSlot line 611
  103. def OAI.DFVSGames.Reduction.AddressMachineSpace.edgeDecode_inline_AddressMachineSpace line 620
  104. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.edgeDecode_canonicalField_inline_AddressMachineSpace line 631
  105. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.edgeDecode_edgeSlot_inline_AddressMachineSpace line 636
  106. def OAI.DFVSGames.Reduction.AddressMachineSpace.addressEdgeSlots line 646
  107. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.addressEdgeSlots_fieldIndex line 654
  108. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.addressSlots_name line 665
  109. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.addressSlots_occurrence line 672
  110. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.addressSlots_radix line 678
  111. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.addressSlots_capacity line 681
  112. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.addressSlots_output line 684
  113. def OAI.DFVSGames.Reduction.AddressMachineSpace.current line 688
  114. def OAI.DFVSGames.Reduction.AddressMachineSpace.remaining line 689
  115. def OAI.DFVSGames.Reduction.AddressMachineSpace.finalOutput line 690
  116. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.current_rev line 692
  117. def OAI.DFVSGames.Reduction.AddressMachineSpace.odometerSlots line 695
  118. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.odometerSlots_radix line 706
  119. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.odometerSlots_scratch line 708
  120. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.odometerSlots_current line 709
  121. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.odometerSlots_remaining line 711
  122. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.current_ne_remaining line 714
  123. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.current_ne_finalOutput line 716
  124. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.remaining_ne_finalOutput line 718
  125. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.edgeSlot_ne_of_decode_none_inline_AddressMachineSpace line 721
  126. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.addressEdgeSlots_ne_rhsField line 729
  127. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.addressEdgeSlots_ne_source line 734
  128. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.addressEdgeSlots_ne_copyScratch line 739
  129. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.addressEdgeSlots_ne_headerTape line 744
  130. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.addressEdgeSlots_ne_remaining line 752
  131. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.addressEdgeSlots_ne_finalOutput line 757
  132. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.headerTape_ne_finalOutput line 762
  133. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.headerTape_ne_current line 766
  134. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.headerTape_ne_remaining line 770
  135. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.tupleOutput_headerTape line 774
  136. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.tupleOutput_source line 784
  137. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.tupleOutput_rhs line 789
  138. theorem OAI.DFVSGames.Reduction.AddressMachineSpace.tupleOutput_occurrence line 797