OAI/Combinatorics/MatchingCount/Arithmetic/ArithmeticSize.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.StackWords.encoded_length line 11
  2. lemma OAI.MatchingFPRAS.PostAddition.input_length line 22
  3. lemma OAI.MatchingFPRAS.PostAddition.input_length_bounds line 25
  4. lemma OAI.MatchingFPRAS.PostAddition.bit_time_bound line 31
  5. lemma OAI.MatchingFPRAS.PostComparison.input_length line 46
  6. lemma OAI.MatchingFPRAS.PostComparison.input_length_bounds line 49
  7. lemma OAI.MatchingFPRAS.PostComparison.bit_time_bound line 55
  8. def OAI.MatchingFPRAS.StackComposition.relabel line 74
  9. def OAI.MatchingFPRAS.StackComposition.mapCfg line 82
  10. lemma OAI.MatchingFPRAS.StackComposition.mapCfg_some line 85
  11. lemma OAI.MatchingFPRAS.StackComposition.mapCfg_none line 88
  12. lemma OAI.MatchingFPRAS.StackComposition.relabel_eval line 90
  13. lemma OAI.MatchingFPRAS.StackComposition.relabel_accesses line 104
  14. lemma OAI.MatchingFPRAS.StackComposition.run_halted line 112
  15. lemma OAI.MatchingFPRAS.StackComposition.run_relabel_to_halt line 118
  16. def OAI.MatchingFPRAS.StackComposition.sequence line 145
  17. lemma OAI.MatchingFPRAS.StackComposition.sequence_run line 150
  18. lemma OAI.MatchingFPRAS.StackComposition.sequence_accesses line 164
  19. lemma OAI.MatchingFPRAS.StackComposition.supports_univ line 171
  20. def OAI.MatchingFPRAS.StackComposition.loop line 184
  21. lemma OAI.MatchingFPRAS.StackComposition.loop_stop line 188
  22. lemma OAI.MatchingFPRAS.StackComposition.loop_once line 192
  23. lemma OAI.MatchingFPRAS.StackComposition.loop_accesses line 202
  24. lemma OAI.MatchingFPRAS.StackComposition.loop_bounded line 209
  25. abbrev OAI.MatchingFPRAS.StackReverse.S line 234
  26. abbrev OAI.MatchingFPRAS.StackReverse.Γ line 235
  27. def OAI.MatchingFPRAS.StackReverse.program line 236
  28. def OAI.MatchingFPRAS.StackReverse.cfg line 240
  29. lemma OAI.MatchingFPRAS.StackReverse.next_empty line 242
  30. lemma OAI.MatchingFPRAS.StackReverse.next_cons line 245
  31. theorem OAI.MatchingFPRAS.StackReverse.run_reverse line 249
  32. lemma OAI.MatchingFPRAS.StackReverse.accesses_bound line 257
  33. lemma OAI.MatchingFPRAS.StackReverse.finite_support line 259
  34. lemma OAI.MatchingFPRAS.StackReverse.reverse_addition_numerals line 264
  35. abbrev OAI.MatchingFPRAS.PostReverse.Alphabet line 272
  36. def OAI.MatchingFPRAS.PostReverse.machine line 273
  37. def OAI.MatchingFPRAS.PostReverse.overhead line 276
  38. def OAI.MatchingFPRAS.PostReverse.input line 279
  39. def OAI.MatchingFPRAS.PostReverse.output line 281
  40. def OAI.MatchingFPRAS.PostReverse.steps line 283
  41. theorem OAI.MatchingFPRAS.PostReverse.computes line 285
  42. lemma OAI.MatchingFPRAS.PostReverse.time_quadratic line 320
  43. abbrev OAI.MatchingFPRAS.ForwardAddition.Γ line 331
  44. def OAI.MatchingFPRAS.ForwardAddition.reverseProgram line 332
  45. def OAI.MatchingFPRAS.ForwardAddition.rcfg line 336
  46. lemma OAI.MatchingFPRAS.ForwardAddition.next_empty line 338
  47. lemma OAI.MatchingFPRAS.ForwardAddition.next_cons line 341
  48. lemma OAI.MatchingFPRAS.ForwardAddition.run_reverse line 345
  49. def OAI.MatchingFPRAS.ForwardAddition.program line 353
  50. lemma OAI.MatchingFPRAS.ForwardAddition.run_add line 355
  51. lemma OAI.MatchingFPRAS.ForwardAddition.accesses_bound line 376
  52. lemma OAI.MatchingFPRAS.ForwardAddition.support line 380
  53. lemma OAI.MatchingFPRAS.ForwardAddition.result_value line 381
  54. abbrev OAI.MatchingFPRAS.PostForwardAddition.Alphabet line 388
  55. lemma OAI.MatchingFPRAS.PostForwardAddition.support line 389
  56. def OAI.MatchingFPRAS.PostForwardAddition.machine line 391
  57. def OAI.MatchingFPRAS.PostForwardAddition.overhead line 394
  58. def OAI.MatchingFPRAS.PostForwardAddition.input line 397
  59. def OAI.MatchingFPRAS.PostForwardAddition.output line 399
  60. def OAI.MatchingFPRAS.PostForwardAddition.steps line 402
  61. theorem OAI.MatchingFPRAS.PostForwardAddition.computes line 404
  62. lemma OAI.MatchingFPRAS.PostForwardAddition.time_quadratic line 440
  63. lemma OAI.MatchingFPRAS.PostReverse.input_length line 448
  64. lemma OAI.MatchingFPRAS.PostReverse.input_length_bounds line 451
  65. lemma OAI.MatchingFPRAS.PostReverse.bit_time_bound line 457
  66. lemma OAI.MatchingFPRAS.PostForwardAddition.input_length line 471
  67. lemma OAI.MatchingFPRAS.PostForwardAddition.input_length_bounds line 474
  68. lemma OAI.MatchingFPRAS.PostForwardAddition.bit_time_bound line 480