OAI/Combinatorics/VariableWL/CertifiedRecipe.lean

GitHub source file

109 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.VariableWL.Computation.Stack.Recipe.Certified.reindex line 9
  2. abbrev OAI.VariableWL.Computation.Stack.Recipe.Certified.bind line 10
  3. theorem OAI.VariableWL.Computation.Stack.Recipe.cons_zero line 13
  4. theorem OAI.VariableWL.Computation.Stack.Recipe.cons_succ line 14
  5. theorem OAI.VariableWL.Computation.Stack.Recipe.reindex_value line 15
  6. theorem OAI.VariableWL.Computation.Stack.Recipe.bind_value line 17
  7. theorem OAI.VariableWL.Computation.Stack.Recipe.input_value line 19
  8. theorem OAI.VariableWL.Computation.Stack.Recipe.literal_value line 20
  9. theorem OAI.VariableWL.Computation.Stack.Recipe.cons_comp_succ line 21
  10. def OAI.VariableWL.Computation.Stack.Recipe.unary line 23
  11. def OAI.VariableWL.Computation.Stack.Recipe.binary line 24
  12. def OAI.VariableWL.Computation.Stack.Recipe.len line 27
  13. def OAI.VariableWL.Computation.Stack.Recipe.plus line 28
  14. def OAI.VariableWL.Computation.Stack.Recipe.minus line 29
  15. def OAI.VariableWL.Computation.Stack.Recipe.times line 30
  16. def OAI.VariableWL.Computation.Stack.Recipe.cat line 31
  17. def OAI.VariableWL.Computation.Stack.Recipe.rev line 32
  18. def OAI.VariableWL.Computation.Stack.Recipe.atIndex line 33
  19. def OAI.VariableWL.Computation.Stack.Recipe.tailAt line 34
  20. theorem OAI.VariableWL.Computation.Stack.Recipe.len_value line 36
  21. theorem OAI.VariableWL.Computation.Stack.Recipe.plus_value line 38
  22. theorem OAI.VariableWL.Computation.Stack.Recipe.minus_value line 40
  23. theorem OAI.VariableWL.Computation.Stack.Recipe.times_value line 42
  24. theorem OAI.VariableWL.Computation.Stack.Recipe.cat_value line 44
  25. theorem OAI.VariableWL.Computation.Stack.Recipe.rev_value line 46
  26. theorem OAI.VariableWL.Computation.Stack.Recipe.atIndex_value line 47
  27. theorem OAI.VariableWL.Computation.Stack.Recipe.tailAt_value line 49
  28. def OAI.VariableWL.Computation.Stack.Recipe.asBool line 52
  29. def OAI.VariableWL.Computation.Stack.Recipe.isZero line 53
  30. def OAI.VariableWL.Computation.Stack.Recipe.choose line 54
  31. def OAI.VariableWL.Computation.Stack.Recipe.lessEq line 56
  32. def OAI.VariableWL.Computation.Stack.Recipe.equal line 57
  33. def OAI.VariableWL.Computation.Stack.Recipe.conj line 58
  34. theorem OAI.VariableWL.Computation.Stack.Recipe.asBool_value line 61
  35. theorem OAI.VariableWL.Computation.Stack.Recipe.isZero_value line 67
  36. theorem OAI.VariableWL.Computation.Stack.Recipe.choose_value line 73
  37. theorem OAI.VariableWL.Computation.Stack.Recipe.lessEq_value line 77
  38. theorem OAI.VariableWL.Computation.Stack.Recipe.equal_value line 80
  39. theorem OAI.VariableWL.Computation.Stack.Recipe.conj_value line 88
  40. def OAI.VariableWL.Computation.Stack.Recipe.liftIndices line 93
  41. theorem OAI.VariableWL.Computation.Stack.Recipe.lift_env line 96
  42. theorem OAI.VariableWL.Computation.Stack.Recipe.foldValue_reindex line 101
  43. def OAI.VariableWL.Computation.Stack.Recipe.iterate line 107
  44. theorem OAI.VariableWL.Computation.Stack.Recipe.iterate_value line 110
  45. def OAI.VariableWL.Computation.Stack.Recipe.collect line 117
  46. theorem OAI.VariableWL.Computation.Stack.Recipe.collect_value line 120
  47. theorem OAI.VariableWL.Computation.Stack.Recipe.decide_bool line 132
  48. def OAI.VariableWL.Computation.Stack.Recipe.all line 134
  49. theorem OAI.VariableWL.Computation.Stack.Recipe.all_value line 137
  50. def OAI.VariableWL.Computation.Stack.Recipe.countTrue line 150
  51. theorem OAI.VariableWL.Computation.Stack.Recipe.countTrue_value line 153
  52. def OAI.VariableWL.Computation.Stack.Recipe.power line 166
  53. theorem OAI.VariableWL.Computation.Stack.Recipe.power_value line 169
  54. theorem OAI.VariableWL.Computation.Stack.Recipe.count_range_lt line 184
  55. theorem OAI.VariableWL.Computation.Stack.Recipe.count_range_multiples line 193
  56. def OAI.VariableWL.Computation.Stack.Recipe.divide line 203
  57. theorem OAI.VariableWL.Computation.Stack.Recipe.divide_value line 207
  58. def OAI.VariableWL.Computation.Stack.Recipe.quotient line 224
  59. def OAI.VariableWL.Computation.Stack.Recipe.remainder line 225
  60. theorem OAI.VariableWL.Computation.Stack.Recipe.quotient_value line 227
  61. theorem OAI.VariableWL.Computation.Stack.Recipe.remainder_value line 232
  62. def OAI.VariableWL.Computation.Stack.Recipe.minimum line 236
  63. theorem OAI.VariableWL.Computation.Stack.Recipe.minimum_value line 237
  64. theorem OAI.VariableWL.Computation.Stack.Recipe.min_mul_cap line 242
  65. def OAI.VariableWL.Computation.Stack.Recipe.boundedPower line 248
  66. theorem OAI.VariableWL.Computation.Stack.Recipe.boundedPower_value line 252
  67. def OAI.VariableWL.Computation.Stack.Recipe.Growth line 270
  68. theorem OAI.VariableWL.Computation.Stack.Recipe.Growth.constant line 273
  69. theorem OAI.VariableWL.Computation.Stack.Recipe.Growth.ident line 274
  70. theorem OAI.VariableWL.Computation.Stack.Recipe.Growth.mono line 275
  71. theorem OAI.VariableWL.Computation.Stack.Recipe.Growth.add line 278
  72. theorem OAI.VariableWL.Computation.Stack.Recipe.Growth.mul line 285
  73. theorem OAI.VariableWL.Computation.Stack.Recipe.Growth.comp line 290
  74. theorem OAI.VariableWL.Computation.Stack.Recipe.Growth.pow line 299
  75. def OAI.VariableWL.Computation.Stack.Recipe.EnvBound line 305
  76. def OAI.VariableWL.Computation.Stack.Recipe.Poly line 307
  77. theorem OAI.VariableWL.Computation.Stack.Recipe.envBound_cons line 310
  78. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_of_bound line 315
  79. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_reindex line 319
  80. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_input line 323
  81. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_literal line 331
  82. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_bind line 334
  83. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_headBranch line 348
  84. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_test line 360
  85. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_length line 363
  86. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_add line 371
  87. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_subtract line 380
  88. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_multiply line 389
  89. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_reverse line 400
  90. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_append line 408
  91. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_drop line 417
  92. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_lookup line 426
  93. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_unary line 435
  94. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_binary line 438
  95. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_len line 442
  96. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_plus line 443
  97. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_minus line 444
  98. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_times line 445
  99. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_cat line 446
  100. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_rev line 447
  101. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_atIndex line 448
  102. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_tailAt line 449
  103. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_asBool line 450
  104. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_isZero line 451
  105. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_choose line 452
  106. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_lessEq line 454
  107. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_equal line 455
  108. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_conj line 457
  109. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_minimum line 459