OAI/Combinatorics/VariableWL/NumericRefinement.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.VariableWL.NumericRefinement.Data line 7
  2. def OAI.VariableWL.NumericRefinement.Data.leftCount line 14
  3. def OAI.VariableWL.NumericRefinement.Data.rightCount line 15
  4. def OAI.VariableWL.NumericRefinement.Data.count line 16
  5. def OAI.VariableWL.NumericRefinement.Data.isLeft line 18
  6. def OAI.VariableWL.NumericRefinement.Data.order line 19
  7. def OAI.VariableWL.NumericRefinement.Data.offset line 20
  8. def OAI.VariableWL.NumericRefinement.Data.coordinate line 21
  9. def OAI.VariableWL.NumericRefinement.Data.replacement line 23
  10. def OAI.VariableWL.NumericRefinement.Data.edge line 26
  11. def OAI.VariableWL.NumericRefinement.Data.initial line 30
  12. def OAI.VariableWL.NumericRefinement.Data.get line 35
  13. def OAI.VariableWL.NumericRefinement.Data.profile line 37
  14. def OAI.VariableWL.NumericRefinement.Data.neighbors line 40
  15. def OAI.VariableWL.NumericRefinement.Data.update line 42
  16. def OAI.VariableWL.NumericRefinement.Data.pack line 45
  17. def OAI.VariableWL.NumericRefinement.Data.array line 48
  18. def OAI.VariableWL.NumericRefinement.Data.histogram line 52
  19. def OAI.VariableWL.NumericRefinement.Data.accepts line 56
  20. theorem OAI.VariableWL.NumericRefinement.all_range line 58
  21. theorem OAI.VariableWL.NumericRefinement.ofFn_nat line 63
  22. theorem OAI.VariableWL.NumericRefinement.sameCounts_map line 68
  23. def OAI.VariableWL.NumericRefinement.data line 77
  24. def OAI.VariableWL.NumericRefinement.address line 79
  25. theorem OAI.VariableWL.NumericRefinement.address_inl line 81
  26. theorem OAI.VariableWL.NumericRefinement.address_inr line 82
  27. theorem OAI.VariableWL.NumericRefinement.left_inl line 84
  28. theorem OAI.VariableWL.NumericRefinement.left_inr line 88
  29. theorem OAI.VariableWL.NumericRefinement.order_inl line 92
  30. theorem OAI.VariableWL.NumericRefinement.order_inr line 95
  31. theorem OAI.VariableWL.NumericRefinement.coordinate_inl line 99
  32. theorem OAI.VariableWL.NumericRefinement.coordinate_inr line 105
  33. theorem OAI.VariableWL.NumericRefinement.replacement_inl line 111
  34. theorem OAI.VariableWL.NumericRefinement.replacement_inr line 118
  35. theorem OAI.VariableWL.NumericRefinement.edge_inl line 125
  36. theorem OAI.VariableWL.NumericRefinement.edge_inr line 132
  37. theorem OAI.VariableWL.NumericRefinement.get_address line 139
  38. def OAI.VariableWL.Computation.Stack.Procedure.aux line 148
  39. theorem OAI.VariableWL.Computation.Stack.Procedure.front_ne_aux line 150
  40. theorem OAI.VariableWL.Computation.Stack.Procedure.aux_ne_front line 156
  41. theorem OAI.VariableWL.Computation.Stack.Procedure.extend_aux line 158
  42. theorem OAI.VariableWL.Computation.Stack.Procedure.clear_aux line 160
  43. theorem OAI.VariableWL.Computation.Stack.Procedure.pushHead line 163
  44. theorem OAI.VariableWL.Computation.Stack.Procedure.lookup line 168
  45. theorem OAI.VariableWL.Computation.Stack.Procedure.iterate_lengthAdd line 197
  46. theorem OAI.VariableWL.Computation.Stack.Procedure.multiplyAdd line 208
  47. theorem OAI.VariableWL.Computation.Stack.Procedure.length line 216
  48. theorem OAI.VariableWL.Computation.Stack.Procedure.add line 234
  49. theorem OAI.VariableWL.Computation.Stack.Procedure.subtract line 256
  50. theorem OAI.VariableWL.Computation.Stack.Procedure.multiply line 278
  51. abbrev OAI.VariableWL.NumericRefinement.Key line 304
  52. def OAI.VariableWL.NumericRefinement.keyPair line 306
  53. def OAI.VariableWL.NumericRefinement.keyVector line 310
  54. def OAI.VariableWL.NumericRefinement.keys line 314
  55. theorem OAI.VariableWL.NumericRefinement.keys_pair line 318
  56. theorem OAI.VariableWL.NumericRefinement.keys_vector line 324
  57. theorem OAI.VariableWL.NumericRefinement.replacement_key line 328
  58. theorem OAI.VariableWL.NumericRefinement.profile_key line 335
  59. theorem OAI.VariableWL.NumericRefinement.update_address line 344
  60. theorem OAI.VariableWL.NumericRefinement.atomic_address line 353
  61. theorem OAI.VariableWL.NumericRefinement.initial_address line 369
  62. theorem OAI.VariableWL.NumericRefinement.pack_correct line 378
  63. theorem OAI.VariableWL.NumericRefinement.array_correct line 391
  64. theorem OAI.VariableWL.NumericRefinement.sameCounts_perm line 404
  65. theorem OAI.VariableWL.NumericRefinement.ofFn_perm_univ line 415
  66. def OAI.VariableWL.NumericRefinement.leftEntries line 425
  67. def OAI.VariableWL.NumericRefinement.rightEntries line 427
  68. theorem OAI.VariableWL.NumericRefinement.leftEntries_address line 430
  69. theorem OAI.VariableWL.NumericRefinement.rightEntries_address line 437
  70. theorem OAI.VariableWL.NumericRefinement.leftEntries_perm line 445
  71. theorem OAI.VariableWL.NumericRefinement.rightEntries_perm line 451
  72. theorem OAI.VariableWL.NumericRefinement.histogram_correct line 457
  73. theorem OAI.VariableWL.NumericRefinement.accepts_correct line 465