OAI/Combinatorics/VariableWL/PortListing.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VariableWL.Computation.Stack.PolyRecipe.underTwo line 11
  2. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.underTwo_value line 14
  3. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.underTwo_bit line 20
  4. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.apply₂_bit line 25
  5. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.count_value line 30
  6. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.select_value line 36
  7. structure OAI.VariableWL.Computation.Stack.PolyRecipe.GraphListing line 43
  8. def OAI.VariableWL.Computation.Stack.PolyRecipe.GraphListing.eval line 48
  9. def OAI.VariableWL.Computation.Stack.PolyRecipe.GraphListing.order line 53
  10. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.GraphListing.order_number line 55
  11. def OAI.VariableWL.Computation.Stack.PolyRecipe.GraphListing.matrix line 58
  12. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.GraphListing.matrix_value line 63
  13. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.GraphListing.matrix_correct line 71
  14. def OAI.VariableWL.Computation.Stack.PolyRecipe.GraphListing.code line 84
  15. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.GraphListing.code_correct line 86
  16. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.outputs line 90
  17. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.reduces line 103
  18. structure OAI.VariableWL.Descriptor.Presentation line 114
  19. def OAI.VariableWL.Descriptor.Presentation.encode line 121
  20. theorem OAI.VariableWL.Descriptor.Presentation.encode_lt line 123
  21. theorem OAI.VariableWL.Descriptor.Presentation.encode_valid line 124
  22. theorem OAI.VariableWL.Descriptor.Presentation.encode_injective line 126
  23. def OAI.VariableWL.Descriptor.Presentation.numbering line 132
  24. structure OAI.VariableWL.Descriptor.PortData line 139
  25. abbrev OAI.VariableWL.Descriptor.PortData.Owners line 147
  26. def OAI.VariableWL.Descriptor.PortData.Sound line 149
  27. def OAI.VariableWL.Descriptor.PortData.ports line 160
  28. abbrev OAI.VariableWL.Descriptor.PortData.Vertices line 166
  29. def OAI.VariableWL.Descriptor.PortData.stride line 168
  30. def OAI.VariableWL.Descriptor.PortData.owner line 169
  31. def OAI.VariableWL.Descriptor.PortData.port line 170
  32. def OAI.VariableWL.Descriptor.PortData.level line 171
  33. def OAI.VariableWL.Descriptor.PortData.code line 172
  34. def OAI.VariableWL.Descriptor.PortData.expanded line 174
  35. theorem OAI.VariableWL.Descriptor.PortData.stride_pos line 185
  36. theorem OAI.VariableWL.Descriptor.PortData.owner_lt line 187
  37. theorem OAI.VariableWL.Descriptor.PortData.code_parts line 193
  38. theorem OAI.VariableWL.Descriptor.PortData.code_lt line 208
  39. def OAI.VariableWL.Descriptor.PortData.presentation line 219
  40. theorem OAI.VariableWL.Descriptor.data_ext line 244
  41. theorem OAI.VariableWL.Descriptor.PortData.edge_correct line 252
  42. theorem OAI.VariableWL.Descriptor.PortData.sound_expanded line 269
  43. def OAI.VariableWL.Descriptor.PortData.graphIso line 283
  44. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.length_value line 298
  45. def OAI.VariableWL.Computation.Stack.PolyRecipe.applyNat line 301
  46. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.applyNat_value line 303
  47. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.applyNat_bit line 307
  48. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.applyNat_number line 312
  49. def OAI.VariableWL.Computation.Stack.PolyRecipe.applyNat₂ line 318
  50. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.applyNat₂_bit line 320
  51. structure OAI.VariableWL.Computation.Stack.PolyRecipe.PortListing line 325
  52. def OAI.VariableWL.Computation.Stack.PolyRecipe.PortListing.eval line 334
  53. def OAI.VariableWL.Computation.Stack.PolyRecipe.PortListing.up line 341
  54. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.PortListing.eval_up line 348
  55. def OAI.VariableWL.Computation.Stack.PolyRecipe.PortListing.stride line 356
  56. def OAI.VariableWL.Computation.Stack.PolyRecipe.PortListing.owner line 357
  57. def OAI.VariableWL.Computation.Stack.PolyRecipe.PortListing.port line 358
  58. def OAI.VariableWL.Computation.Stack.PolyRecipe.PortListing.level line 359
  59. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.PortListing.stride_number line 361
  60. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.PortListing.owner_number line 364
  61. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.PortListing.port_number line 368
  62. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.PortListing.level_number line 372
  63. def OAI.VariableWL.Computation.Stack.PolyRecipe.PortListing.expandedValid line 376
  64. def OAI.VariableWL.Computation.Stack.PolyRecipe.PortListing.expandedEdge line 380
  65. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.PortListing.expandedValid_bit line 391
  66. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.PortListing.expandedEdge_bit line 397
  67. def OAI.VariableWL.Computation.Stack.PolyRecipe.PortListing.expanded line 406
  68. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.PortListing.expanded_eval line 411
  69. def OAI.VariableWL.Computation.Stack.PolyRecipe.fixedNat line 428
  70. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.fixedNat_number line 433
  71. def OAI.VariableWL.Computation.Stack.PolyRecipe.fixedBool line 448
  72. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.fixedBool_bit line 451
  73. theorem OAI.VariableWL.Computation.Stack.Recipe.cons_two line 459