OAI/Combinatorics/ParityLifts/Simulator.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ParityWL.Complexity.TapePair line 7
  2. def OAI.ParityWL.Complexity.listCell line 9
  3. lemma OAI.ParityWL.Complexity.listCell_nil line 12
  4. lemma OAI.ParityWL.Complexity.listCell_cons_zero line 14
  5. lemma OAI.ParityWL.Complexity.listCell_cons_succ line 16
  6. lemma OAI.ParityWL.Complexity.listCell_tail line 18
  7. lemma OAI.ParityWL.Complexity.listCell_zero line 20
  8. def OAI.ParityWL.Complexity.TapePair.cell line 23
  9. def OAI.ParityWL.Complexity.TapePair.advance line 27
  10. lemma OAI.ParityWL.Complexity.TapePair.advance_cell line 32
  11. lemma OAI.ParityWL.Complexity.TapePair.advance_length line 82
  12. abbrev OAI.ParityWL.Complexity.SmallConfiguration line 90
  13. def OAI.ParityWL.Complexity.smallStep line 93
  14. def OAI.ParityWL.Complexity.smallInitial line 100
  15. def OAI.ParityWL.Complexity.SmallRepresents line 103
  16. lemma OAI.ParityWL.Complexity.smallStep_represents line 106
  17. lemma OAI.ParityWL.Complexity.smallInitial_represents line 126
  18. lemma OAI.ParityWL.Complexity.smallRun_represents line 146
  19. lemma OAI.ParityWL.Complexity.smallRun_output line 153
  20. lemma OAI.ParityWL.Complexity.smallRun_tape_length line 158
  21. lemma OAI.ParityWL.Complexity.treeEncode_symbol_list_size line 176
  22. lemma OAI.ParityWL.Complexity.smallRun_size line 185
  23. def OAI.ParityWL.Complexity.TExpr.caseTuple line 214
  24. lemma OAI.ParityWL.Complexity.TExpr.caseTuple_eval line 220
  25. def OAI.ParityWL.Complexity.TExpr.tapeHead line 235
  26. def OAI.ParityWL.Complexity.TExpr.tapeAdvance line 238
  27. lemma OAI.ParityWL.Complexity.TExpr.tapeHead_eval line 244
  28. lemma OAI.ParityWL.Complexity.TExpr.tapeAdvance_eval line 250
  29. def OAI.ParityWL.Complexity.TExpr.smallStep line 257
  30. lemma OAI.ParityWL.Complexity.TExpr.smallStep_eval line 268
  31. def OAI.ParityWL.Complexity.TExpr.smallContinue line 287
  32. def OAI.ParityWL.Complexity.TExpr.smallAnswer line 291
  33. lemma OAI.ParityWL.Complexity.TExpr.smallContinue_eval line 295
  34. lemma OAI.ParityWL.Complexity.TExpr.smallAnswer_eval line 301