OAI/Combinatorics/VariableWL/PrefixParts.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.VariableWL.PrefixParts.Data line 10
  2. theorem OAI.VariableWL.PrefixParts.Data.vec_add_self line 24
  3. abbrev OAI.VariableWL.PrefixParts.Data.Valuation line 28
  4. def OAI.VariableWL.PrefixParts.Data.translate line 30
  5. def OAI.VariableWL.PrefixParts.Data.truncate line 36
  6. theorem OAI.VariableWL.PrefixParts.Data.truncate_add line 38
  7. theorem OAI.VariableWL.PrefixParts.Data.truncate_truncate line 41
  8. theorem OAI.VariableWL.PrefixParts.Data.truncate_zero line 45
  9. theorem OAI.VariableWL.PrefixParts.Data.truncate_full line 48
  10. abbrev OAI.VariableWL.PrefixParts.Data.RawTree line 51
  11. def OAI.VariableWL.PrefixParts.Data.TreeLegal line 53
  12. abbrev OAI.VariableWL.PrefixParts.Data.Tree line 57
  13. abbrev OAI.VariableWL.PrefixParts.Data.Vertex line 58
  14. abbrev OAI.VariableWL.PrefixParts.Data.Tree.channel line 62
  15. abbrev OAI.VariableWL.PrefixParts.Data.Tree.height line 63
  16. abbrev OAI.VariableWL.PrefixParts.Data.Tree.bits line 64
  17. def OAI.VariableWL.PrefixParts.Data.Tree.ofValuation line 66
  18. theorem OAI.VariableWL.PrefixParts.Data.Tree.ext line 70
  19. theorem OAI.VariableWL.PrefixParts.Data.Tree.truncated line 75
  20. theorem OAI.VariableWL.PrefixParts.Data.Tree.above_zero line 80
  21. theorem OAI.VariableWL.PrefixParts.Data.Tree.height_zero line 84
  22. def OAI.VariableWL.PrefixParts.Data.TreeStep line 90
  23. def OAI.VariableWL.PrefixParts.Data.Forward line 93
  24. def OAI.VariableWL.PrefixParts.Data.graph line 102
  25. def OAI.VariableWL.PrefixParts.Data.treeTranslation line 114
  26. def OAI.VariableWL.PrefixParts.Data.vertexTranslation line 142
  27. theorem OAI.VariableWL.PrefixParts.Data.treeTranslation_step line 146
  28. theorem OAI.VariableWL.PrefixParts.Data.vertexTranslation_forward line 160
  29. def OAI.VariableWL.PrefixParts.Data.translationIso line 194
  30. theorem OAI.VariableWL.PrefixParts.Data.tree_to_leaf line 198
  31. theorem OAI.VariableWL.PrefixParts.Data.spine_to_zero line 216
  32. theorem OAI.VariableWL.PrefixParts.Data.leaf_spine line 226
  33. theorem OAI.VariableWL.PrefixParts.Data.connected line 230
  34. theorem OAI.VariableWL.PrefixParts.Data.Tree.height_le line 260
  35. theorem OAI.VariableWL.PrefixParts.Data.TreeStep.lower_lt line 262
  36. theorem OAI.VariableWL.PrefixParts.Data.TreeStep.parent_unique line 267
  37. theorem OAI.VariableWL.PrefixParts.Data.TreeStep.child_unique line 275
  38. theorem OAI.VariableWL.PrefixParts.Data.Tree.root_unique line 290
  39. def OAI.VariableWL.PrefixParts.Data.bitPort line 294
  40. theorem OAI.VariableWL.PrefixParts.Data.bitPort_ne_zero line 296
  41. theorem OAI.VariableWL.PrefixParts.Data.bitPort_injective line 302
  42. def OAI.VariableWL.PrefixParts.Data.slot line 309
  43. theorem OAI.VariableWL.PrefixParts.Data.slot_parent line 319
  44. theorem OAI.VariableWL.PrefixParts.Data.slot_child line 324
  45. theorem OAI.VariableWL.PrefixParts.Data.leaf_unique line 329
  46. theorem OAI.VariableWL.PrefixParts.Data.leaf_node_unique line 341
  47. theorem OAI.VariableWL.PrefixParts.Data.slot_injective line 346
  48. theorem OAI.VariableWL.PrefixParts.Data.degree_le_three line 411
  49. def OAI.VariableWL.PrefixParts.Data.portAlphabet line 422
  50. theorem OAI.VariableWL.PrefixParts.Data.portAlphabet_zero line 424
  51. theorem OAI.VariableWL.PrefixParts.Data.portAlphabet_bitPort line 426
  52. def OAI.VariableWL.PrefixParts.Data.shiftPorts line 429
  53. theorem OAI.VariableWL.PrefixParts.Data.shiftPorts_zero line 432
  54. theorem OAI.VariableWL.PrefixParts.Data.shiftPorts_bitPort line 436
  55. def OAI.VariableWL.PrefixParts.Data.localPorts line 440
  56. theorem OAI.VariableWL.PrefixParts.Data.localPorts_zero line 445
  57. theorem OAI.VariableWL.PrefixParts.Data.slot_translation line 449
  58. theorem OAI.VariableWL.PrefixParts.Data.proper_root_reserved line 477