OAI/Combinatorics/VariableWL/BlockDescriptor.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.VariableWL.PrefixDescriptor.raw_anchors line 13
  2. theorem OAI.VariableWL.PrefixDescriptor.raw_incidence line 49
  3. theorem OAI.VariableWL.PrefixDescriptor.tag_sort line 67
  4. theorem OAI.VariableWL.PrefixDescriptor.raw_color line 71
  5. theorem OAI.VariableWL.PrefixDescriptor.color_le line 82
  6. def OAI.VariableWL.Descriptor.Presentation.product line 95
  7. theorem OAI.VariableWL.Descriptor.Presentation.product_encode line 125
  8. def OAI.VariableWL.Descriptor.Presentation.sum line 128
  9. theorem OAI.VariableWL.Descriptor.Presentation.sum_inl line 153
  10. theorem OAI.VariableWL.Descriptor.Presentation.sum_inr line 155
  11. def OAI.VariableWL.Descriptor.Presentation.filter line 158
  12. theorem OAI.VariableWL.Descriptor.Presentation.filter_encode line 171
  13. theorem OAI.VariableWL.PrefixDescriptor.presentation_inverse_val line 183
  14. theorem OAI.VariableWL.PrefixDescriptor.port_sound line 186
  15. def OAI.VariableWL.PrefixDescriptor.uncoloredIso line 196
  16. def OAI.VariableWL.Descriptor.Presentation.transport line 226
  17. theorem OAI.VariableWL.Descriptor.Presentation.transport_encode line 227
  18. def OAI.VariableWL.Descriptor.Presentation.fin line 233
  19. theorem OAI.VariableWL.Descriptor.Presentation.fin_encode line 237
  20. theorem OAI.VariableWL.Descriptor.Presentation.count_eq_card line 239
  21. theorem OAI.VariableWL.Descriptor.Presentation.pick_enumeration line 243
  22. def OAI.VariableWL.BlockDescriptor.properEquiv line 257
  23. def OAI.VariableWL.BlockDescriptor.ProperPredicate line 264
  24. theorem OAI.VariableWL.BlockDescriptor.properPredicate_code line 269
  25. def OAI.VariableWL.BlockDescriptor.properPresentation line 278
  26. theorem OAI.VariableWL.BlockDescriptor.properPresentation_encode line 284
  27. theorem OAI.VariableWL.BlockDescriptor.properPresentation_valid line 288
  28. theorem OAI.VariableWL.BlockDescriptor.properNumber_val line 292
  29. theorem OAI.VariableWL.BlockDescriptor.properNumber_pick line 297
  30. structure OAI.VariableWL.BlockDescriptor.Core line 310
  31. def OAI.VariableWL.BlockDescriptor.Core.properBound line 323
  32. def OAI.VariableWL.BlockDescriptor.Core.channelBound line 324
  33. def OAI.VariableWL.BlockDescriptor.Core.proper line 325
  34. def OAI.VariableWL.BlockDescriptor.Core.channels line 328
  35. def OAI.VariableWL.BlockDescriptor.Core.select line 329
  36. def OAI.VariableWL.BlockDescriptor.Core.other line 330
  37. def OAI.VariableWL.BlockDescriptor.Core.readout line 331
  38. def OAI.VariableWL.BlockDescriptor.Core.root line 332
  39. def OAI.VariableWL.BlockDescriptor.Core.order line 333
  40. def OAI.VariableWL.BlockDescriptor.Core.matching line 334
  41. def OAI.VariableWL.BlockDescriptor.Core.toPrefix line 338
  42. theorem OAI.VariableWL.BlockDescriptor.Core.channelBound_pos line 348
  43. theorem OAI.VariableWL.BlockDescriptor.Core.channels_le line 349
  44. structure OAI.VariableWL.BlockDescriptor.Program.Listing line 358
  45. def OAI.VariableWL.BlockDescriptor.Program.Listing.eval line 371
  46. def OAI.VariableWL.BlockDescriptor.Program.Listing.up line 382
  47. theorem OAI.VariableWL.BlockDescriptor.Program.Listing.eval_up line 393
  48. def OAI.VariableWL.BlockDescriptor.Program.Listing.properBound line 405
  49. def OAI.VariableWL.BlockDescriptor.Program.Listing.channelBound line 406
  50. def OAI.VariableWL.BlockDescriptor.Program.Listing.proper line 407
  51. def OAI.VariableWL.BlockDescriptor.Program.Listing.channels line 411
  52. def OAI.VariableWL.BlockDescriptor.Program.Listing.select line 412
  53. def OAI.VariableWL.BlockDescriptor.Program.Listing.other line 413
  54. def OAI.VariableWL.BlockDescriptor.Program.Listing.readout line 414
  55. def OAI.VariableWL.BlockDescriptor.Program.Listing.root line 415
  56. def OAI.VariableWL.BlockDescriptor.Program.Listing.order line 416
  57. def OAI.VariableWL.BlockDescriptor.Program.Listing.matching line 417
  58. theorem OAI.VariableWL.BlockDescriptor.Program.Listing.properBound_number line 421
  59. theorem OAI.VariableWL.BlockDescriptor.Program.Listing.channelBound_number line 423
  60. theorem OAI.VariableWL.BlockDescriptor.Program.Listing.proper_bit line 425
  61. theorem OAI.VariableWL.BlockDescriptor.Program.Listing.channels_number line 429
  62. theorem OAI.VariableWL.BlockDescriptor.Program.Listing.select_number line 432
  63. theorem OAI.VariableWL.BlockDescriptor.Program.Listing.other_number line 435
  64. theorem OAI.VariableWL.BlockDescriptor.Program.Listing.readout_number line 437
  65. theorem OAI.VariableWL.BlockDescriptor.Program.Listing.root_number line 439
  66. theorem OAI.VariableWL.BlockDescriptor.Program.Listing.order_number line 442
  67. theorem OAI.VariableWL.BlockDescriptor.Program.Listing.matching_bit line 445
  68. def OAI.VariableWL.BlockDescriptor.Program.Listing.toPrefix line 450
  69. theorem OAI.VariableWL.BlockDescriptor.Program.Listing.prefix_eval line 460