OAI/Combinatorics/VariableWL/PrefixAlphabet.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.applyNat₂_number line 11
  2. def OAI.VariableWL.Computation.Stack.PolyRecipe.applyNat₃ line 16
  3. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.applyNat₃_bit line 19
  4. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.applyNat₃_number line 24
  5. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.fixedNat_zero line 29
  6. def OAI.VariableWL.Computation.Stack.PolyRecipe.tableLookup line 38
  7. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.fixedNat_total line 40
  8. def OAI.VariableWL.Descriptor.Presentation.ofEncoding line 52
  9. theorem OAI.VariableWL.Descriptor.Presentation.ofEncoding_encode line 63
  10. theorem OAI.VariableWL.Descriptor.PortData.sound_of_equiv line 74
  11. theorem OAI.VariableWL.Descriptor.PortData.sound_of_encoding line 94
  12. abbrev OAI.VariableWL.PrefixAlphabet.Vector line 121
  13. abbrev OAI.VariableWL.PrefixAlphabet.Order line 122
  14. instance OAI.VariableWL.PrefixAlphabet.vectorFintype line 123
  15. instance OAI.VariableWL.PrefixAlphabet.orderFintype line 124
  16. def OAI.VariableWL.PrefixAlphabet.vectorNumber line 125
  17. def OAI.VariableWL.PrefixAlphabet.orderNumber line 126
  18. def OAI.VariableWL.PrefixAlphabet.vectorCount line 127
  19. def OAI.VariableWL.PrefixAlphabet.orderCount line 128
  20. def OAI.VariableWL.PrefixAlphabet.encode line 130
  21. def OAI.VariableWL.PrefixAlphabet.encodeOrder line 132
  22. theorem OAI.VariableWL.PrefixAlphabet.encode_lt line 135
  23. theorem OAI.VariableWL.PrefixAlphabet.order_lt line 137
  24. theorem OAI.VariableWL.PrefixAlphabet.encode_injective line 139
  25. def OAI.VariableWL.PrefixAlphabet.dimension line 144
  26. def OAI.VariableWL.PrefixAlphabet.truncated line 147
  27. def OAI.VariableWL.PrefixAlphabet.permuted line 150
  28. def OAI.VariableWL.PrefixAlphabet.prefixCode line 153
  29. def OAI.VariableWL.PrefixAlphabet.bit line 158
  30. def OAI.VariableWL.PrefixAlphabet.paddedEqual line 164
  31. theorem OAI.VariableWL.PrefixAlphabet.dimension_encode line 170
  32. theorem OAI.VariableWL.PrefixAlphabet.prefix_encode line 175
  33. theorem OAI.VariableWL.PrefixAlphabet.bit_encode line 185
  34. theorem OAI.VariableWL.PrefixAlphabet.paddedEqual_encode line 193
  35. def OAI.VariableWL.Computation.Stack.PolyRecipe.fixedNat₂ line 206
  36. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.fixedNat₂_number line 209
  37. def OAI.VariableWL.Computation.Stack.PolyRecipe.fixedNat₃ line 221
  38. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.fixedNat₃_number line 224
  39. def OAI.VariableWL.Computation.Stack.PolyRecipe.fixedBool₂ line 236
  40. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.fixedBool₂_bit line 239
  41. def OAI.VariableWL.PrefixAlphabet.Program.dimension line 251
  42. def OAI.VariableWL.PrefixAlphabet.Program.prefixCode line 253
  43. def OAI.VariableWL.PrefixAlphabet.Program.bit line 255
  44. def OAI.VariableWL.PrefixAlphabet.Program.paddedEqual line 257
  45. theorem OAI.VariableWL.PrefixAlphabet.Program.dimension_number line 260
  46. theorem OAI.VariableWL.PrefixAlphabet.Program.prefixCode_number line 262
  47. theorem OAI.VariableWL.PrefixAlphabet.Program.bit_number line 266
  48. theorem OAI.VariableWL.PrefixAlphabet.Program.paddedEqual_bit line 268
  49. theorem OAI.VariableWL.PrefixAlphabet.vectorCount_pos line 274
  50. structure OAI.VariableWL.PrefixDescriptor.Raw line 283
  51. structure OAI.VariableWL.PrefixDescriptor.Data line 291
  52. def OAI.VariableWL.PrefixDescriptor.Data.sortBound line 305
  53. def OAI.VariableWL.PrefixDescriptor.Data.bound line 306
  54. def OAI.VariableWL.PrefixDescriptor.Data.tag line 308
  55. def OAI.VariableWL.PrefixDescriptor.Data.pack line 309
  56. def OAI.VariableWL.PrefixDescriptor.Data.unpack line 310
  57. theorem OAI.VariableWL.PrefixDescriptor.Data.join_div line 316
  58. theorem OAI.VariableWL.PrefixDescriptor.Data.join_mod line 318
  59. theorem OAI.VariableWL.PrefixDescriptor.Data.unpack_pack line 321
  60. theorem OAI.VariableWL.PrefixDescriptor.Data.pack_unpack line 328
  61. theorem OAI.VariableWL.PrefixDescriptor.Data.tag_lt line 335
  62. theorem OAI.VariableWL.PrefixDescriptor.Data.pack_lt line 342
  63. theorem OAI.VariableWL.PrefixDescriptor.Data.unpack_bounds line 350
  64. def OAI.VariableWL.PrefixDescriptor.Data.treeValid line 364
  65. def OAI.VariableWL.PrefixDescriptor.Data.validRaw line 369
  66. def OAI.VariableWL.PrefixDescriptor.Data.valid line 373
  67. def OAI.VariableWL.PrefixDescriptor.Data.sortValid line 375
  68. structure OAI.VariableWL.PrefixDescriptor.Good line 386
  69. def OAI.VariableWL.PrefixDescriptor.raw line 398
  70. theorem OAI.VariableWL.PrefixDescriptor.raw_block line 404
  71. theorem OAI.VariableWL.PrefixDescriptor.raw_bounds line 407
  72. theorem OAI.VariableWL.PrefixDescriptor.raw_valid line 421