OAI/Combinatorics/VariableWL/NumericProgram.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.VariableWL.NumericProgram.cons_one line 9
  2. structure OAI.VariableWL.NumericProgram.Data line 11
  3. def OAI.VariableWL.NumericProgram.Data.reindex line 19
  4. def OAI.VariableWL.NumericProgram.Data.up line 22
  5. def OAI.VariableWL.NumericProgram.Data.up₂ line 23
  6. def OAI.VariableWL.NumericProgram.Data.eval line 24
  7. def OAI.VariableWL.NumericProgram.Data.Good line 26
  8. theorem OAI.VariableWL.NumericProgram.eval_reindex line 29
  9. theorem OAI.VariableWL.NumericProgram.eval_up line 31
  10. theorem OAI.VariableWL.NumericProgram.eval_up₂ line 32
  11. theorem OAI.VariableWL.NumericProgram.good_up line 33
  12. theorem OAI.VariableWL.NumericProgram.good_up₂ line 34
  13. theorem OAI.VariableWL.NumericProgram.choose_number line 36
  14. theorem OAI.VariableWL.NumericProgram.up_bit line 41
  15. theorem OAI.VariableWL.NumericProgram.up₂_bit line 42
  16. theorem OAI.VariableWL.NumericProgram.power_bound line 44
  17. def OAI.VariableWL.NumericProgram.Data.leftCount line 52
  18. def OAI.VariableWL.NumericProgram.Data.rightCount line 53
  19. def OAI.VariableWL.NumericProgram.Data.count line 54
  20. def OAI.VariableWL.NumericProgram.Data.isLeft line 55
  21. def OAI.VariableWL.NumericProgram.Data.order line 56
  22. def OAI.VariableWL.NumericProgram.Data.offset line 57
  23. def OAI.VariableWL.NumericProgram.Data.power line 58
  24. def OAI.VariableWL.NumericProgram.Data.coordinate line 59
  25. def OAI.VariableWL.NumericProgram.Data.replacement line 60
  26. def OAI.VariableWL.NumericProgram.Data.edge line 62
  27. theorem OAI.VariableWL.NumericProgram.leftCount_number line 66
  28. theorem OAI.VariableWL.NumericProgram.rightCount_number line 70
  29. theorem OAI.VariableWL.NumericProgram.count_number line 74
  30. theorem OAI.VariableWL.NumericProgram.isLeft_bit line 78
  31. theorem OAI.VariableWL.NumericProgram.order_number line 82
  32. theorem OAI.VariableWL.NumericProgram.offset_number line 86
  33. theorem OAI.VariableWL.NumericProgram.power_number line 90
  34. theorem OAI.VariableWL.NumericProgram.coordinate_number line 100
  35. theorem OAI.VariableWL.NumericProgram.replacement_number line 107
  36. theorem OAI.VariableWL.NumericProgram.edge_bit line 114
  37. def OAI.VariableWL.NumericProgram.Data.initial line 121
  38. theorem OAI.VariableWL.NumericProgram.list_all_congr line 128
  39. theorem OAI.VariableWL.NumericProgram.initial_bit line 134
  40. def OAI.VariableWL.NumericProgram.sameRanges line 167
  41. theorem OAI.VariableWL.NumericProgram.sameRanges_bit line 172
  42. theorem OAI.VariableWL.NumericProgram.sameCounts_ranges line 182
  43. def OAI.VariableWL.NumericProgram.Data.get line 191
  44. def OAI.VariableWL.NumericProgram.Data.profile line 192
  45. def OAI.VariableWL.NumericProgram.Data.comparison line 195
  46. def OAI.VariableWL.NumericProgram.Data.update line 201
  47. theorem OAI.VariableWL.NumericProgram.get_bit line 203
  48. theorem OAI.VariableWL.NumericProgram.profile_bit line 208
  49. theorem OAI.VariableWL.NumericProgram.comparison_bit line 221
  50. theorem OAI.VariableWL.NumericProgram.update_bit line 230
  51. def OAI.VariableWL.NumericProgram.Data.initialArray line 235
  52. def OAI.VariableWL.NumericProgram.Data.nextArray line 238
  53. theorem OAI.VariableWL.NumericProgram.initialArray_value line 242
  54. theorem OAI.VariableWL.NumericProgram.nextArray_value line 249
  55. theorem OAI.VariableWL.NumericProgram.count_up₂ line 262
  56. theorem OAI.VariableWL.NumericProgram.initialArray_length line 267
  57. theorem OAI.VariableWL.NumericProgram.nextArray_length line 271
  58. def OAI.VariableWL.NumericProgram.Data.arrayBody line 275
  59. def OAI.VariableWL.NumericProgram.Data.arrayProgram line 276
  60. theorem OAI.VariableWL.NumericProgram.arrayPrefix_length line 279
  61. theorem OAI.VariableWL.NumericProgram.arrayProgram_poly line 287
  62. def OAI.VariableWL.NumericProgram.Data.array line 297
  63. theorem OAI.VariableWL.NumericProgram.arrayPrefix_value line 299
  64. theorem OAI.VariableWL.NumericProgram.array_value line 309
  65. def OAI.VariableWL.NumericProgram.Data.histogram line 317
  66. theorem OAI.VariableWL.NumericProgram.histogram_bit line 324
  67. theorem OAI.VariableWL.NumericProgram.sameRanges_singleton line 334
  68. def OAI.VariableWL.NumericProgram.Data.accepts line 338
  69. theorem OAI.VariableWL.NumericProgram.accepts_value line 340
  70. theorem OAI.VariableWL.NumericProgram.accepts_correct line 348
  71. def OAI.VariableWL.Computation.Stack.PolyRecipe.Expr.bind line 361
  72. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.bind_value line 363
  73. def OAI.VariableWL.Computation.Stack.PolyRecipe.length line 366
  74. def OAI.VariableWL.Computation.Stack.PolyRecipe.reverse line 367
  75. def OAI.VariableWL.Computation.Stack.PolyRecipe.drop line 368
  76. def OAI.VariableWL.Computation.Stack.PolyRecipe.minimum line 369
  77. def OAI.VariableWL.Computation.Stack.PolyRecipe.append line 370
  78. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.length_number line 371
  79. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.reverse_value line 373
  80. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.drop_value line 374
  81. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.minimum_value line 375
  82. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.minimum_number line 377
  83. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.append_value line 381
  84. def OAI.VariableWL.Computation.Stack.PolyRecipe.foldWordIndices line 383
  85. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.foldWord_env line 386
  86. def OAI.VariableWL.Computation.Stack.PolyRecipe.foldWordBody line 391
  87. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.foldWordBody_value line 394
  88. def OAI.VariableWL.Computation.Stack.PolyRecipe.foldWordStep line 402
  89. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.foldWord_prefix line 404
  90. def OAI.VariableWL.Computation.Stack.PolyRecipe.foldWordProgram line 417
  91. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.foldWordProgram_value line 420
  92. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.foldWordProgram_poly line 426