OAI/Combinatorics/VariableWL/Completeness.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VariableWL.AffineCatalog.Data.resign line 11
  2. def OAI.VariableWL.AffineCatalog.Data.descriptor line 12
  3. theorem OAI.VariableWL.AffineCatalog.sortPredicate_congr line 15
  4. theorem OAI.VariableWL.AffineCatalog.resign_good line 34
  5. def OAI.VariableWL.AffineCatalog.blockPresentation line 36
  6. def OAI.VariableWL.AffineCatalog.readPresentation line 37
  7. theorem OAI.VariableWL.AffineCatalog.coordinateBound line 39
  8. theorem OAI.VariableWL.AffineCatalog.core_resign_good line 44
  9. def OAI.VariableWL.AffineCatalog.properNumbering line 48
  10. theorem OAI.VariableWL.AffineCatalog.properNumbering_eq line 53
  11. theorem OAI.VariableWL.AffineCatalog.prefix_resign_good line 58
  12. theorem OAI.VariableWL.AffineCatalog.matching_resign_good line 68
  13. theorem OAI.VariableWL.AffineCatalog.descriptor_sound line 78
  14. def OAI.VariableWL.AffineCatalog.sortPresentation line 84
  15. theorem OAI.VariableWL.AffineCatalog.core_proper_resign line 90
  16. theorem OAI.VariableWL.AffineCatalog.core_channels_resign line 94
  17. theorem OAI.VariableWL.AffineCatalog.core_dimension_resign line 99
  18. theorem OAI.VariableWL.AffineCatalog.core_readDimension_resign line 103
  19. theorem OAI.VariableWL.AffineCatalog.core_root_resign line 107
  20. theorem OAI.VariableWL.AffineCatalog.prefix_channelBound_resign line 113
  21. theorem OAI.VariableWL.AffineCatalog.prefix_sortPredicate_resign line 117
  22. theorem OAI.VariableWL.AffineCatalog.prefix_tag_resign line 123
  23. theorem OAI.VariableWL.AffineCatalog.sort_spec line 129
  24. theorem OAI.VariableWL.AffineCatalog.sort_valid line 139
  25. theorem OAI.VariableWL.AffineCatalog.sort_encode line 144
  26. def OAI.VariableWL.AffineCatalog.descriptor_iso line 151
  27. theorem OAI.VariableWL.AffineCatalog.compiler_correct line 166
  28. def OAI.VariableWL.AffineCatalog.Program.Listing.graph line 193
  29. theorem OAI.VariableWL.AffineCatalog.Program.Listing.graph_eval line 194
  30. def OAI.VariableWL.CellularCatalog.Program.Listing.graph line 202
  31. theorem OAI.VariableWL.CellularCatalog.Program.Listing.graph_eval line 203
  32. def OAI.VariableWL.CellularCatalog.Data.resign line 208
  33. theorem OAI.VariableWL.CellularCatalog.Data.ext_fields line 209
  34. theorem OAI.VariableWL.CellularCatalog.Data.resign_affine line 215
  35. theorem OAI.VariableWL.MachineCellular.listing_eval_resign line 221
  36. def OAI.VariableWL.MachineCellular.graphListing line 225
  37. def OAI.VariableWL.MachineCellular.base line 226
  38. theorem OAI.VariableWL.MachineCellular.graphListing_eval line 227
  39. def OAI.VariableWL.MachineCellular.realPresentation line 238
  40. def OAI.VariableWL.MachineCellular.comparisonPresentation line 241
  41. theorem OAI.VariableWL.MachineCellular.base_good line 244
  42. theorem OAI.VariableWL.MachineCellular.compiled_correct line 255
  43. def OAI.VariableWL.MachineCellular.dimensionProgram line 269
  44. theorem OAI.VariableWL.MachineCellular.dimensionProgram_number line 270
  45. def OAI.VariableWL.MachineCellular.pairProgram line 274
  46. theorem OAI.VariableWL.MachineCellular.pairProgram_value line 276
  47. theorem OAI.VariableWL.MachineCellular.reduction_correct line 285
  48. theorem OAI.VariableWL.general_hard line 303
  49. theorem OAI.VariableWL.subcubic_hard line 309
  50. theorem OAI.VariableWL.main line 315

    Distinct definitions of this name: ComparatorChallenges/VariableWL.lean:125 (same statement text; different proof or body). Qualify references as OAI.VariableWL.main@path.