OAI/Computability/MaxCut/Encoding/InputData.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.inputData line 13
2. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.headerData line 26
3. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.headerStacks line 29
4. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.headerTrace line 33
5. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.oldData line 52
6. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.originalData_eq line 55
7. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.oldBodyTrace line 60

   Source documentation

   The actual old-vertex body is transported with all outer counters and header words untouched. No body-execution hypothesis occurs in this lemma.

   theorem oldBodyTrace (H : BaseTable) (t : GraphTables.Table) (e : Fin t.darts)
       (output : List Bool) (header : Header.Tape → List Bool) (counters : Fin 4 → List Bool) :
       (advance (TM2.step (program H)))^[MachineRegularOriginalBody.totalSteps H t e output]
         (some (cfg H (some (Label.oldBody MachineRegularOriginalBody.entry))
           (oldData t e.val output) header counters)) =
         some (cfg H (some .oldIncrement)
           (oldData t e.val (output ++ MachineRegularOriginalBody.emittedBits H t e)) header counters) := by
   …

   Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.BaseTable, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.program, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.totalSteps, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.cfg, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.entry, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.oldData, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.emittedBits

8. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.counterStacks line 75
9. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.frame_oldFuel line 78
10. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.frame_ownerFuel line 82
11. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_oldFuel line 86
12. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_ownerFuel line 97
13. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_global line 108
14. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_owner line 121
15. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.oldGuardStep line 134
16. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.oldGuardExit line 148
17. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.oldIncrementStep line 159
18. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.oldPrefix line 173
19. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.oldElapsed line 176
20. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.joinTrace_inline_MachineRegularTable line 183
21. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.oldPrefixTrace line 189

    Source documentation

    Each actual fuel/body/increment segment appends exactly the next original vertex block. This induction is over a specification index, not a register.

    theorem oldPrefixTrace (H : BaseTable) (t : GraphTables.Table) (output : List Bool)
        (header : Header.Tape → List Bool) (k : Nat) : k ≤ t.darts →
        (advance (TM2.step (program H)))^[oldElapsed H t output k]
          (some (cfg H (some .oldGuard) (oldData t 0 output) header
            (counterStacks (encodeWord t.darts) [] [] []))) =
          some (cfg H (some .oldGuard) (oldData t k (output ++ oldPrefix H t k)) header
            (counterStacks (encodeWord (t.darts-k)) [] [] [])) := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.BaseTable, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.program, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.oldElapsed, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.cfg, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.oldData, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.counterStacks, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.oldPrefix

22. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.oldLoopTrace line 220
23. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.frame_scratch line 232
24. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.frame_darts line 236
25. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.frame_header_n line 239
26. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.oldSeedStep line 243
27. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.copyOldTrace line 256
28. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.oldStageTrace line 271
29. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_offset line 281
30. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.ownerData line 294
31. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.ownerSeedStep line 302
32. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.copyOwnerTrace line 320
33. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.ownerPlacement line 334
34. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.ownerInitialData_eq line 346
35. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.ownerBodyTrace line 349
36. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.ownerGuardStep line 365
37. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.ownerGuardExit line 379
38. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.ownerIncrementStep line 390
39. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.ownerPrefix line 410
40. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.ownerElapsed line 413
41. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.ownerPrefixTrace line 420
42. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.ownerLoopTrace line 450
43. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.ownerStageTrace line 462
44. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.owner_output_eq_ownerPrefix line 472
45. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.cleaned line 488
46. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.cleanupTime line 493
47. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.drainTrace line 498
48. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.cleanupPrefixTrace line 506
49. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.cleanupTrace line 520
50. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.finalStacks line 526
51. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.cleaned_finalStacks line 529
52. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.cleaned_length_le line 549
53. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.cleanupTime_le line 563
54. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.cleanupTime_final_le line 579
55. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.headerOutput line 643
56. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.oldOutput line 646
57. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.finalOutput line 649
58. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.totalTime line 652
59. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.old_output_eq_originalPrefix line 658
60. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.finalOutput_eq line 663