OAI/Combinatorics/VariableWL/AffineCatalog.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.VariableWL.AffineCatalog.Data line 10
  2. def OAI.VariableWL.AffineCatalog.Data.vertexDimension line 20
  3. def OAI.VariableWL.AffineCatalog.Data.horizontalDimension line 21
  4. def OAI.VariableWL.AffineCatalog.Data.squareLeftDimension line 22
  5. def OAI.VariableWL.AffineCatalog.Data.squareRightDimension line 23
  6. def OAI.VariableWL.AffineCatalog.Data.dimension line 24
  7. def OAI.VariableWL.AffineCatalog.Data.readDimension line 26
  8. def OAI.VariableWL.AffineCatalog.Data.linkLeft line 27
  9. def OAI.VariableWL.AffineCatalog.Data.linkRight line 29
  10. def OAI.VariableWL.AffineCatalog.Data.linkLeftConstant line 31
  11. def OAI.VariableWL.AffineCatalog.Data.linkRightConstant line 32
  12. def OAI.VariableWL.AffineCatalog.Data.constant line 33
  13. def OAI.VariableWL.AffineCatalog.Data.zeroOrder line 35
  14. def OAI.VariableWL.AffineCatalog.Data.readOrder line 36
  15. def OAI.VariableWL.AffineCatalog.Data.legal line 40
  16. def OAI.VariableWL.AffineCatalog.Data.core line 43
  17. structure OAI.VariableWL.AffineCatalog.Good line 57
  18. theorem OAI.VariableWL.AffineCatalog.vertex_dimension line 69
  19. theorem OAI.VariableWL.AffineCatalog.horizontal_dimension line 78
  20. theorem OAI.VariableWL.AffineCatalog.square_dimensions line 81
  21. theorem OAI.VariableWL.AffineCatalog.dimension_code line 89
  22. theorem OAI.VariableWL.AffineCatalog.read_dimension line 108
  23. theorem OAI.VariableWL.AffineCatalog.link_left line 120
  24. theorem OAI.VariableWL.AffineCatalog.link_right line 134
  25. theorem OAI.VariableWL.AffineCatalog.link_left_constant line 148
  26. theorem OAI.VariableWL.AffineCatalog.link_right_constant line 154
  27. theorem OAI.VariableWL.AffineCatalog.constant_code line 160
  28. theorem OAI.VariableWL.AffineCatalog.zero_order line 180
  29. theorem OAI.VariableWL.AffineCatalog.read_order line 184
  30. theorem OAI.VariableWL.AffineCatalog.legal_code line 247
  31. theorem OAI.VariableWL.AffineCatalog.core_good line 276
  32. theorem OAI.VariableWL.AffineAlphabet.horizontalLegal_false line 294
  33. theorem OAI.VariableWL.AffineAlphabet.squareLegal_false line 300
  34. theorem OAI.VariableWL.AffineAlphabet.squareLegal_mod line 310
  35. theorem OAI.VariableWL.AffineAlphabet.horizontalOrder_false line 313
  36. theorem OAI.VariableWL.AffineAlphabet.squareOrder_false line 314
  37. theorem OAI.VariableWL.AffineAlphabet.squareOrder_cap line 317
  38. theorem OAI.VariableWL.AffineAlphabet.zeroOrder_false line 325
  39. def OAI.VariableWL.AffineAlphabet.Program.horizontalLegal line 331
  40. def OAI.VariableWL.AffineAlphabet.Program.squareLegalBody line 333
  41. def OAI.VariableWL.AffineAlphabet.Program.horizontalOrder line 337
  42. def OAI.VariableWL.AffineAlphabet.Program.squareOrder line 338
  43. def OAI.VariableWL.AffineAlphabet.Program.zeroOrder line 339
  44. theorem OAI.VariableWL.AffineAlphabet.Program.horizontalOrder_number line 340
  45. theorem OAI.VariableWL.AffineAlphabet.Program.zeroOrder_number line 346
  46. theorem OAI.VariableWL.AffineAlphabet.Program.squareOrder_number line 352
  47. theorem OAI.VariableWL.AffineAlphabet.Program.horizontalLegal_bit line 358
  48. theorem OAI.VariableWL.AffineAlphabet.Program.squareLegal_bit_bounded line 366
  49. def OAI.VariableWL.AffineAlphabet.Program.squareLegal line 380
  50. theorem OAI.VariableWL.AffineAlphabet.Program.squareLegal_bit line 382
  51. theorem OAI.VariableWL.BlockDescriptor.Program.Listing.eval_blocks line 393
  52. theorem OAI.VariableWL.BlockDescriptor.Program.Listing.eval_reads line 394
  53. theorem OAI.VariableWL.BlockDescriptor.Program.Listing.eval_validBlock line 395
  54. theorem OAI.VariableWL.BlockDescriptor.Program.Listing.eval_validRead line 396
  55. theorem OAI.VariableWL.AffineCatalog.Data.core_blocks_eq line 399
  56. theorem OAI.VariableWL.AffineCatalog.Data.core_reads_eq line 400
  57. theorem OAI.VariableWL.AffineCatalog.Data.core_validBlock_eq line 401
  58. theorem OAI.VariableWL.AffineCatalog.Data.core_validRead_eq line 402
  59. theorem OAI.VariableWL.BlockDescriptor.Core.ext_fields line 405