OAI/Combinatorics/VariableWL/PolyRecipe.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.VariableWL.Computation.Stack.Recipe.reindex_time line 8
  2. theorem OAI.VariableWL.Computation.Stack.Recipe.bind_time line 10
  3. theorem OAI.VariableWL.Computation.Stack.Recipe.fold_time line 12
  4. theorem OAI.VariableWL.Computation.Stack.Recipe.foldTime_reindex line 17
  5. theorem OAI.VariableWL.Computation.Stack.Recipe.iterate_time line 21
  6. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_iterate line 44
  7. theorem OAI.VariableWL.Computation.Stack.Recipe.collect_prefix line 86
  8. theorem OAI.VariableWL.Computation.Stack.Recipe.all_prefix line 93
  9. theorem OAI.VariableWL.Computation.Stack.Recipe.countTrue_prefix line 101
  10. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_collect line 109
  11. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_all line 117
  12. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_countTrue line 122
  13. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_divide line 131
  14. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_quotient line 135
  15. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_remainder line 137
  16. theorem OAI.VariableWL.Computation.Stack.Recipe.boundedPower_prefix line 140
  17. theorem OAI.VariableWL.Computation.Stack.Recipe.poly_boundedPower line 149
  18. structure OAI.VariableWL.Computation.Stack.PolyRecipe.Expr line 164
  19. def OAI.VariableWL.Computation.Stack.PolyRecipe.Expr.value line 169
  20. def OAI.VariableWL.Computation.Stack.PolyRecipe.Expr.number line 170
  21. def OAI.VariableWL.Computation.Stack.PolyRecipe.Expr.bit line 171
  22. def OAI.VariableWL.Computation.Stack.PolyRecipe.Expr.reindex line 172
  23. def OAI.VariableWL.Computation.Stack.PolyRecipe.Expr.up line 174
  24. def OAI.VariableWL.Computation.Stack.PolyRecipe.Expr.up₂ line 175
  25. def OAI.VariableWL.Computation.Stack.PolyRecipe.input line 176
  26. def OAI.VariableWL.Computation.Stack.PolyRecipe.literal line 177
  27. def OAI.VariableWL.Computation.Stack.PolyRecipe.numeral line 178
  28. def OAI.VariableWL.Computation.Stack.PolyRecipe.add line 179
  29. def OAI.VariableWL.Computation.Stack.PolyRecipe.sub line 180
  30. def OAI.VariableWL.Computation.Stack.PolyRecipe.mul line 181
  31. def OAI.VariableWL.Computation.Stack.PolyRecipe.div line 182
  32. def OAI.VariableWL.Computation.Stack.PolyRecipe.mod line 183
  33. def OAI.VariableWL.Computation.Stack.PolyRecipe.capPow line 184
  34. def OAI.VariableWL.Computation.Stack.PolyRecipe.eq line 186
  35. def OAI.VariableWL.Computation.Stack.PolyRecipe.le line 187
  36. def OAI.VariableWL.Computation.Stack.PolyRecipe.choose line 188
  37. def OAI.VariableWL.Computation.Stack.PolyRecipe.neg line 190
  38. def OAI.VariableWL.Computation.Stack.PolyRecipe.lt line 191
  39. def OAI.VariableWL.Computation.Stack.PolyRecipe.conj line 192
  40. def OAI.VariableWL.Computation.Stack.PolyRecipe.bitEq line 193
  41. def OAI.VariableWL.Computation.Stack.PolyRecipe.lookup line 194
  42. def OAI.VariableWL.Computation.Stack.PolyRecipe.all line 195
  43. def OAI.VariableWL.Computation.Stack.PolyRecipe.collect line 196
  44. def OAI.VariableWL.Computation.Stack.PolyRecipe.count line 198
  45. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.reindex_value line 201
  46. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.up_value line 203
  47. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.up₂_value line 204
  48. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.input_value line 205
  49. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.literal_value line 206
  50. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.numeral_number line 207
  51. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.reindex_number line 208
  52. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.up_number line 210
  53. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.up₂_number line 211
  54. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.input_number line 212
  55. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.add_number line 213
  56. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.sub_number line 215
  57. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.mul_number line 217
  58. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.div_number line 219
  59. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.mod_number line 221
  60. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.capPow_number line 223
  61. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.eq_value line 226
  62. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.le_value line 228
  63. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.choose_value line 230
  64. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.neg_value line 234
  65. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.lt_value line 237
  66. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.bit_singleton line 242
  67. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.eq_bit line 246
  68. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.le_bit line 247
  69. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.lt_bit line 248
  70. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.neg_bit line 249
  71. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.conj_value line 250
  72. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.conj_bit line 251
  73. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.choose_bit line 252
  74. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.bitEq_bit line 257
  75. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.lookup_value line 260
  76. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.lookup_bit line 262
  77. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.all_value line 263
  78. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.all_bit line 265
  79. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.collect_value line 267
  80. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.count_number line 269