OAI/Computability/DeterministicSum/PrunedProgram.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Instruction-level prefix enumeration and bounded level traversal.

  1. def OAI.DeterministicThreeSum.Structured.Pruned.Stored line 12
  2. def OAI.DeterministicThreeSum.Structured.Pruned.storePair line 15
  3. lemma OAI.DeterministicThreeSum.Structured.Pruned.storePair_outside line 18
  4. lemma OAI.DeterministicThreeSum.Structured.Pruned.storePair_stored line 22
  5. lemma OAI.DeterministicThreeSum.Structured.Pruned.stored_nil line 34
  6. def OAI.DeterministicThreeSum.Structured.Pruned.pushDigit line 36
  7. def OAI.DeterministicThreeSum.Structured.Pruned.pushDigitState line 46
  8. lemma OAI.DeterministicThreeSum.Structured.Pruned.pushDigit_correct line 50
  9. def OAI.DeterministicThreeSum.Structured.Pruned.tryDigit line 68
  10. lemma OAI.DeterministicThreeSum.Structured.Pruned.tryDigit_writes line 72
  11. theorem OAI.DeterministicThreeSum.Structured.Pruned.tryDigit_correct line 76
  12. def OAI.DeterministicThreeSum.Structured.Pruned.accepted line 122
  13. lemma OAI.DeterministicThreeSum.Structured.Pruned.accepted_length line 125
  14. lemma OAI.DeterministicThreeSum.Structured.Pruned.accepted_cons line 129
  15. def OAI.DeterministicThreeSum.Structured.Pruned.childrenCode line 134
  16. theorem OAI.DeterministicThreeSum.Structured.Pruned.childrenCode_correct line 138
  17. def OAI.DeterministicThreeSum.Structured.Pruned.loadPrefix line 186
  18. def OAI.DeterministicThreeSum.Structured.Pruned.loadPrefixState line 193
  19. lemma OAI.DeterministicThreeSum.Structured.Pruned.loadPrefix_correct line 196
  20. lemma OAI.DeterministicThreeSum.Structured.Pruned.childrenCode_writes line 208
  21. def OAI.DeterministicThreeSum.Structured.Pruned.expandStep line 214
  22. lemma OAI.DeterministicThreeSum.Structured.Pruned.expandStep_writes line 216
  23. theorem OAI.DeterministicThreeSum.Structured.Pruned.expandStep_correct line 227
  24. lemma OAI.DeterministicThreeSum.Structured.Pruned.expand_take line 252
  25. def OAI.DeterministicThreeSum.Structured.Pruned.expandLoop line 257
  26. theorem OAI.DeterministicThreeSum.Structured.Pruned.expandLoop_correct line 260
  27. def OAI.DeterministicThreeSum.Structured.Pruned.levels line 339
  28. def OAI.DeterministicThreeSum.Structured.Pruned.banks line 343
  29. lemma OAI.DeterministicThreeSum.Structured.Pruned.banks_zero line 344
  30. lemma OAI.DeterministicThreeSum.Structured.Pruned.banks_succ line 345
  31. def OAI.DeterministicThreeSum.Structured.Pruned.levelUpdate line 349
  32. def OAI.DeterministicThreeSum.Structured.Pruned.levelUpdateState line 354
  33. lemma OAI.DeterministicThreeSum.Structured.Pruned.levelUpdate_correct line 357
  34. def OAI.DeterministicThreeSum.Structured.Pruned.levelsCommand line 370
  35. def OAI.DeterministicThreeSum.Structured.Pruned.LevelRegs line 373
  36. theorem OAI.DeterministicThreeSum.Structured.Pruned.levelsCommand_correct line 377
  37. def OAI.DeterministicThreeSum.Pruned.scalarAlphabet line 439
  38. lemma OAI.DeterministicThreeSum.Pruned.volume_append line 440
  39. lemma OAI.DeterministicThreeSum.Pruned.volume_replicate line 444
  40. lemma OAI.DeterministicThreeSum.Pruned.volume_pos line 448
  41. lemma OAI.DeterministicThreeSum.Structured.Pruned.levels_enumerate line 457
  42. lemma OAI.DeterministicThreeSum.Structured.Pruned.levelsCommand_writes line 467
  43. lemma OAI.DeterministicThreeSum.Structured.Pruned.volume_prefix_le line 482
  44. lemma OAI.DeterministicThreeSum.Structured.Pruned.repeat_remaining line 487
  45. theorem OAI.DeterministicThreeSum.Structured.Pruned.levelsEnumerate_correct line 491