OAI/Computability/DirectedFeedback/Machines/MachineBinaryNameMachine.lean

GitHub source file

98 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.BinaryNameMachine.frame line 14
  2. def OAI.DFVSGames.BinaryNameMachine.finalDigit line 18
  3. def OAI.DFVSGames.BinaryNameMachine.canonical line 22
  4. structure OAI.DFVSGames.BinaryNameMachine.Result line 24
  5. def OAI.DFVSGames.BinaryNameMachine.scanSpec line 30
  6. def OAI.DFVSGames.BinaryNameMachine.steps line 36
  7. theorem OAI.DFVSGames.BinaryNameMachine.steps_le line 40
  8. theorem OAI.DFVSGames.BinaryNameMachine.frame_length line 49
  9. theorem OAI.DFVSGames.BinaryNameMachine.scanSpec_frame line 55
  10. theorem OAI.DFVSGames.BinaryNameMachine.steps_frame line 64
  11. abbrev OAI.DFVSGames.BinaryNameMachine.Alphabet line 74
  12. abbrev OAI.DFVSGames.BinaryNameMachine.State line 75
  13. def OAI.DFVSGames.BinaryNameMachine.clean line 77
  14. def OAI.DFVSGames.BinaryNameMachine.exitAt line 79
  15. def OAI.DFVSGames.BinaryNameMachine.finish line 84
  16. def OAI.DFVSGames.BinaryNameMachine.scan line 87
  17. theorem OAI.DFVSGames.BinaryNameMachine.stepAux_finish line 102
  18. theorem OAI.DFVSGames.BinaryNameMachine.update_source_inline_MachineBinaryNameMachine line 107
  19. theorem OAI.DFVSGames.BinaryNameMachine.update_destination_inline_MachineBinaryNameMachine line 118
  20. theorem OAI.DFVSGames.BinaryNameMachine.step_empty line 132
  21. theorem OAI.DFVSGames.BinaryNameMachine.step_end line 140
  22. theorem OAI.DFVSGames.BinaryNameMachine.step_truncated line 151
  23. theorem OAI.DFVSGames.BinaryNameMachine.step_digit line 159
  24. theorem OAI.DFVSGames.BinaryNameMachine.scanTrace line 169
  25. def OAI.DFVSGames.BinaryNameMachine.scanInTime line 203
  26. theorem OAI.DFVSGames.BinaryNameMachine.framedTrace line 215
  27. def OAI.DFVSGames.BinaryNameMachine.machine line 228
  28. theorem OAI.DFVSGames.BinaryNameMachine.machine_finiteAlphabet line 239
  29. def OAI.DFVSGames.BinaryNameMachine.machineInTime line 243
  30. theorem OAI.DFVSGames.BinaryParsing.frame_eq line 260
  31. theorem OAI.DFVSGames.BinaryParsing.canonical_cons_cons line 265
  32. theorem OAI.DFVSGames.BinaryParsing.canonical_iff line 268
  33. theorem OAI.DFVSGames.BinaryParsing.canonical_nat_bits line 293
  34. theorem OAI.DFVSGames.BinaryParsing.parseFrame_sound line 298
  35. theorem OAI.DFVSGames.BinaryParsing.parseName_sound line 322
  36. theorem OAI.DFVSGames.BinaryParsing.parseLiteral_sound line 338
  37. theorem OAI.DFVSGames.BinaryParsing.parseClause_sound line 353
  38. theorem OAI.DFVSGames.BinaryParsing.parseClauses_sound line 377
  39. theorem OAI.DFVSGames.BinaryParsing.decodeFormula_sound line 405
  40. theorem OAI.DFVSGames.BinaryParsing.decodeFormula_eq_some_iff line 419
  41. theorem OAI.DFVSGames.BinaryParsing.scanSpec_nameBits line 423
  42. theorem OAI.DFVSGames.BinaryOccurrenceRename.literal_mem_names line 440
  43. def OAI.DFVSGames.BinaryOccurrenceRename.nameIndex line 447
  44. def OAI.DFVSGames.BinaryOccurrenceRename.literal line 451
  45. def OAI.DFVSGames.BinaryOccurrenceRename.clause line 455
  46. def OAI.DFVSGames.BinaryOccurrenceRename.renamed line 461
  47. def OAI.DFVSGames.BinaryOccurrenceRename.restrictAssignment line 465
  48. def OAI.DFVSGames.BinaryOccurrenceRename.extendAssignment line 469
  49. theorem OAI.DFVSGames.BinaryOccurrenceRename.nameIndex_reads_name line 472
  50. theorem OAI.DFVSGames.BinaryOccurrenceRename.clause_eval_restrict line 476
  51. theorem OAI.DFVSGames.BinaryOccurrenceRename.clause_eval_extend line 481
  52. theorem OAI.DFVSGames.BinaryOccurrenceRename.renamed_clause_count line 491
  53. theorem OAI.DFVSGames.BinaryOccurrenceRename.renamed_variable_count line 494
  54. theorem OAI.DFVSGames.BinaryOccurrenceRename.renamed_satisfiable_iff line 498
  55. theorem OAI.DFVSGames.BinaryOccurrenceRename.nat_bits_injective line 513
  56. theorem OAI.DFVSGames.BinaryOccurrenceRename.idxOf_binary_payloads line 518
  57. theorem OAI.DFVSGames.BinaryOccurrenceRename.renamed_encoding_bound line 530
  58. theorem OAI.DFVSGames.BinaryOccurrenceRename.renamed_encoding_bound_bits line 537
  59. def OAI.DFVSGames.BinaryLanguage.rejectBinary line 554
  60. theorem OAI.DFVSGames.BinaryLanguage.rejectBinary_unsatisfiable line 558
  61. def OAI.DFVSGames.BinaryLanguage.rejectFormula line 567
  62. theorem OAI.DFVSGames.BinaryLanguage.reject_unsatisfiable line 569
  63. def OAI.DFVSGames.BinaryLanguage.language line 573
  64. def OAI.DFVSGames.BinaryLanguage.totalParsed line 576
  65. def OAI.DFVSGames.BinaryLanguage.totalRename line 579
  66. theorem OAI.DFVSGames.BinaryLanguage.totalParsed_satisfiable_iff line 582
  67. theorem OAI.DFVSGames.BinaryLanguage.totalRename_satisfiable_iff line 588
  68. theorem OAI.DFVSGames.BinaryLanguage.totalRename_encoded line 593
  69. theorem OAI.DFVSGames.BinaryLanguage.language_encoded line 597
  70. theorem OAI.DFVSGames.BinaryLanguage.reject_bits_length line 601
  71. theorem OAI.DFVSGames.BinaryLanguage.totalRename_output_length line 603
  72. structure OAI.DFVSGames.Explicit.MachineOutputContract.SimpleBipartite line 627
  73. def OAI.DFVSGames.Explicit.MachineOutputContract.permutationEquiv line 636
  74. theorem OAI.DFVSGames.Explicit.MachineOutputContract.SimpleBipartite.no_loops line 647
  75. theorem OAI.DFVSGames.Explicit.MachineOutputContract.SimpleBipartite.no_reverse line 655
  76. theorem OAI.DFVSGames.Explicit.MachineOutputContract.SimpleBipartite.undirected_unique line 664
  77. def OAI.DFVSGames.Explicit.MachineOutputContract.SimpleBipartite.toBipartiteGame line 674
  78. theorem OAI.DFVSGames.Explicit.MachineOutputContract.SimpleBipartite.toBipartiteGame_satisfied_iff line 688
  79. def OAI.DFVSGames.Explicit.MachineOutputContract.SimpleBipartite.mergeLabelings line 696
  80. theorem OAI.DFVSGames.Explicit.MachineOutputContract.SimpleBipartite.mergeLabelings_left line 703
  81. theorem OAI.DFVSGames.Explicit.MachineOutputContract.SimpleBipartite.mergeLabelings_right line 710
  82. theorem OAI.DFVSGames.Explicit.MachineOutputContract.SimpleBipartite.toBipartiteGame_count line 717
  83. theorem OAI.DFVSGames.Explicit.MachineOutputContract.SimpleBipartite.toBipartiteGame_count_merge line 731
  84. theorem OAI.DFVSGames.Explicit.MachineOutputContract.SimpleBipartite.toBipartiteGame_maxSatisfied line 739
  85. theorem OAI.DFVSGames.Explicit.MachineOutputContract.SimpleBipartite.toBipartiteGame_value line 755
  86. structure OAI.DFVSGames.Explicit.MachineOutputContract.BinaryGapReduction line 763
  87. theorem OAI.DFVSGames.Explicit.MachineOutputContract.BinaryGapReduction.nonempty line 788
  88. theorem OAI.DFVSGames.Explicit.MachineOutputContract.BinaryGapReduction.occurrence_count_positive line 791
  89. theorem OAI.DFVSGames.Explicit.MachineOutputContract.BinaryGapReduction.completeness_value line 795
  90. theorem OAI.DFVSGames.Explicit.MachineOutputContract.BinaryGapReduction.soundness_value line 802
  91. theorem OAI.DFVSGames.Explicit.MachineOutputContract.BinaryGapReduction.alphabet_eq_two_pow line 809
  92. theorem OAI.DFVSGames.Explicit.MachineOutputContract.BinaryGapReduction.no_loops line 813
  93. theorem OAI.DFVSGames.Explicit.MachineOutputContract.BinaryGapReduction.undirected_unique line 819
  94. theorem OAI.DFVSGames.Explicit.MachineOutputContract.BinaryGapReduction.full_table_length line 832
  95. theorem OAI.DFVSGames.Explicit.MachineOutputContract.BinaryGapReduction.translation_equation line 838
  96. theorem OAI.DFVSGames.Explicit.MachineOutputContract.BinaryGapReduction.decode_output line 847
  97. theorem OAI.DFVSGames.Explicit.MachineOutputContract.BinaryGapReduction.output_word_count line 853
  98. theorem OAI.DFVSGames.Explicit.MachineOutputContract.BinaryGapReduction.malformed_soundness line 858