OAI/Combinatorics/VariableWL/PrefixListing.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.VariableWL.PrefixDescriptor.Data.treeValid_true line 10
  2. theorem OAI.VariableWL.PrefixDescriptor.Data.validRaw_true line 15
  3. theorem OAI.VariableWL.PrefixDescriptor.Data.sortValid_true line 20
  4. theorem OAI.VariableWL.PrefixDescriptor.Data.forward_true line 26
  5. theorem OAI.VariableWL.PrefixDescriptor.Data.internal_true line 34
  6. theorem OAI.VariableWL.PrefixDescriptor.Data.roots_true line 38
  7. theorem OAI.VariableWL.PrefixDescriptor.Data.anchors_true line 44
  8. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.underOne_number line 54
  9. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.underTwo_number line 59
  10. def OAI.VariableWL.PrefixAlphabet.TotalProgram.paddedEqual line 69
  11. theorem OAI.VariableWL.PrefixAlphabet.TotalProgram.paddedEqual_bit line 72
  12. structure OAI.VariableWL.PrefixDescriptor.Program.RawExpr line 91
  13. def OAI.VariableWL.PrefixDescriptor.Program.RawExpr.eval line 98
  14. def OAI.VariableWL.PrefixDescriptor.Program.RawExpr.up line 100
  15. theorem OAI.VariableWL.PrefixDescriptor.Program.RawExpr.eval_up line 102
  16. structure OAI.VariableWL.PrefixDescriptor.Program.Listing line 104
  17. def OAI.VariableWL.PrefixDescriptor.Program.Listing.eval line 117
  18. def OAI.VariableWL.PrefixDescriptor.Program.Listing.up line 127
  19. theorem OAI.VariableWL.PrefixDescriptor.Program.Listing.eval_up line 138
  20. def OAI.VariableWL.PrefixDescriptor.Program.Listing.sortBound line 149
  21. def OAI.VariableWL.PrefixDescriptor.Program.Listing.bound line 150
  22. def OAI.VariableWL.PrefixDescriptor.Program.Listing.tag line 151
  23. def OAI.VariableWL.PrefixDescriptor.Program.Listing.unpack line 153
  24. theorem OAI.VariableWL.PrefixDescriptor.Program.Listing.sortBound_number line 159
  25. theorem OAI.VariableWL.PrefixDescriptor.Program.Listing.bound_number line 161
  26. theorem OAI.VariableWL.PrefixDescriptor.Program.Listing.tag_number line 163
  27. theorem OAI.VariableWL.PrefixDescriptor.Program.Listing.unpack_eval line 165
  28. def OAI.VariableWL.PrefixDescriptor.Program.Listing.treePossible line 168
  29. def OAI.VariableWL.PrefixDescriptor.Program.Listing.treeValid line 171
  30. def OAI.VariableWL.PrefixDescriptor.Program.Listing.validRaw line 174
  31. def OAI.VariableWL.PrefixDescriptor.Program.Listing.valid line 181
  32. theorem OAI.VariableWL.PrefixDescriptor.Program.Listing.treePossible_bit line 183
  33. theorem OAI.VariableWL.PrefixDescriptor.Program.Listing.treeValid_bit line 189
  34. theorem OAI.VariableWL.PrefixDescriptor.Program.Listing.validRaw_bit line 197
  35. theorem OAI.VariableWL.PrefixDescriptor.Program.Listing.valid_bit line 205
  36. def OAI.VariableWL.PrefixDescriptor.Program.Listing.sortValid line 210
  37. def OAI.VariableWL.PrefixDescriptor.Program.Listing.sortPredicate line 216
  38. def OAI.VariableWL.PrefixDescriptor.Program.Listing.color line 217
  39. def OAI.VariableWL.PrefixDescriptor.Program.Listing.colorBound line 219
  40. theorem OAI.VariableWL.PrefixDescriptor.Program.Listing.sortValid_bit line 220
  41. theorem OAI.VariableWL.PrefixDescriptor.Program.Listing.sortPredicate_bit line 227
  42. theorem OAI.VariableWL.PrefixDescriptor.Program.Listing.color_number line 231
  43. theorem OAI.VariableWL.PrefixDescriptor.Program.Listing.colorBound_number line 236
  44. def OAI.VariableWL.PrefixDescriptor.Program.Listing.forward line 241
  45. def OAI.VariableWL.PrefixDescriptor.Program.Listing.slot line 254
  46. def OAI.VariableWL.PrefixDescriptor.Program.Listing.internal line 263
  47. theorem OAI.VariableWL.PrefixDescriptor.Program.Listing.forward_bit line 266
  48. theorem OAI.VariableWL.PrefixDescriptor.Program.Listing.slot_number line 275
  49. theorem OAI.VariableWL.PrefixDescriptor.Program.Listing.internal_bit line 280
  50. def OAI.VariableWL.PrefixDescriptor.Program.Listing.roots line 287
  51. def OAI.VariableWL.PrefixDescriptor.Program.Listing.anchors line 294
  52. def OAI.VariableWL.PrefixDescriptor.Program.Listing.incidence line 300
  53. theorem OAI.VariableWL.PrefixDescriptor.Program.Listing.roots_bit line 306
  54. theorem OAI.VariableWL.PrefixDescriptor.Program.Listing.anchors_bit line 315
  55. theorem OAI.VariableWL.PrefixDescriptor.Program.Listing.incidence_bit line 323
  56. def OAI.VariableWL.PrefixDescriptor.Program.Listing.portListing line 328
  57. theorem OAI.VariableWL.PrefixDescriptor.Program.Listing.portListing_eval line 334
  58. theorem OAI.VariableWL.Descriptor.Presentation.enumeration_val line 349