OAI/Computability/PerfectCompleteness/Foundations/ClauseSupportLemmas.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.ClauseSupport.Answer line 14
  2. def OAI.PerfectCompleteness.ClauseSupport.coordinate line 16
  3. theorem OAI.PerfectCompleteness.ClauseSupport.coordinate_surjective line 19
  4. theorem OAI.PerfectCompleteness.ClauseSupport.pair_surjective line 25
  5. instance OAI.PerfectCompleteness.ClauseSupport.(instance at line 30) line 30
  6. def OAI.PerfectCompleteness.ClauseSupport.Unused line 34
  7. def OAI.PerfectCompleteness.ClauseSupport.Factors line 36
  8. abbrev OAI.PerfectCompleteness.ClauseSupport.Reducible line 39
  9. theorem OAI.PerfectCompleteness.ClauseSupport.unused_of_two_reductions line 42
  10. theorem OAI.PerfectCompleteness.ClauseSupport.used_reduction_unique line 49
  11. def OAI.PerfectCompleteness.ClauseSupport.pull line 55
  12. theorem OAI.PerfectCompleteness.ClauseSupport.unused_pull_iff line 58
  13. theorem OAI.PerfectCompleteness.ClauseSupport.factors_pull_iff line 70
  14. theorem OAI.PerfectCompleteness.ClauseSupport.unused_kernel_invariant line 83
  15. theorem OAI.PerfectCompleteness.ClauseSupport.factors_kernel_invariant line 89
  16. inductive OAI.PerfectCompleteness.ClauseSupport.Mode line 95
  17. def OAI.PerfectCompleteness.ClauseSupport.clauseMode line 101
  18. theorem OAI.PerfectCompleteness.ClauseSupport.clauseMode_unused line 106
  19. theorem OAI.PerfectCompleteness.ClauseSupport.clauseMode_bit line 110
  20. theorem OAI.PerfectCompleteness.ClauseSupport.clauseMode_full line 117
  21. theorem OAI.PerfectCompleteness.ClauseSupport.clauseMode_eq_of_predicates line 121
  22. theorem OAI.PerfectCompleteness.ClauseSupport.clauseMode_kernel_invariant line 137
  23. theorem OAI.PerfectCompleteness.ClauseSupport.unprojected_mode_eq line 144
  24. inductive OAI.PerfectCompleteness.ClauseSupport.ReducedValue line 152
  25. def OAI.PerfectCompleteness.ClauseSupport.reduceByMode line 158
  26. def OAI.PerfectCompleteness.ClauseSupport.clauseReduction line 164
  27. def OAI.PerfectCompleteness.ClauseSupport.bitReduction line 167
  28. theorem OAI.PerfectCompleteness.ClauseSupport.clauseReduction_sound line 171
  29. theorem OAI.PerfectCompleteness.ClauseSupport.bitReduction_sound line 188
  30. inductive OAI.PerfectCompleteness.ClauseSupport.SlotKey line 196
  31. def OAI.PerfectCompleteness.ClauseSupport.clauseKey line 202
  32. def OAI.PerfectCompleteness.ClauseSupport.bitKey line 209
  33. theorem OAI.PerfectCompleteness.ClauseSupport.unprojected_clause_key_eq line 213
  34. theorem OAI.PerfectCompleteness.ClauseSupport.unprojected_clause_reduction_eq line 219
  35. theorem OAI.PerfectCompleteness.ClauseSupport.unprojected_bit_key_eq line 224
  36. theorem OAI.PerfectCompleteness.ClauseSupport.unprojected_bit_reduction_eq line 230
  37. theorem OAI.PerfectCompleteness.ClauseSupport.projected_reducible line 236
  38. theorem OAI.PerfectCompleteness.ClauseSupport.projected_unused_iff line 242
  39. theorem OAI.PerfectCompleteness.ClauseSupport.projected_key_eq line 247
  40. theorem OAI.PerfectCompleteness.ClauseSupport.projected_reduction_eq line 261
  41. inductive OAI.PerfectCompleteness.MixedSupport.Slot line 286
  42. def OAI.PerfectCompleteness.MixedSupport.Slot.Domain line 290
  43. instance OAI.PerfectCompleteness.MixedSupport.(instance at line 294) line 294
  44. abbrev OAI.PerfectCompleteness.MixedSupport.Assignment line 297
  45. inductive OAI.PerfectCompleteness.MixedSupport.Projection line 299
  46. def OAI.PerfectCompleteness.MixedSupport.Projection.map line 305
  47. theorem OAI.PerfectCompleteness.MixedSupport.Projection.surjective line 309
  48. def OAI.PerfectCompleteness.MixedSupport.projectionMap line 315
  49. theorem OAI.PerfectCompleteness.MixedSupport.projectionMap_surjective line 320
  50. theorem OAI.PerfectCompleteness.MixedSupport.projectionMap_update line 327
  51. def OAI.PerfectCompleteness.MixedSupport.sectionFunction line 338
  52. theorem OAI.PerfectCompleteness.MixedSupport.sectionFunction_pullback line 342
  53. def OAI.PerfectCompleteness.MixedSupport.localKey line 350
  54. def OAI.PerfectCompleteness.MixedSupport.localReduction line 355
  55. theorem OAI.PerfectCompleteness.MixedSupport.localReduction_sound line 360
  56. theorem OAI.PerfectCompleteness.MixedSupport.localKey_projection line 367
  57. theorem OAI.PerfectCompleteness.MixedSupport.localReduction_projection line 380
  58. def OAI.PerfectCompleteness.MixedSupport.keyFields line 393
  59. def OAI.PerfectCompleteness.MixedSupport.coordinateReduction line 396
  60. def OAI.PerfectCompleteness.MixedSupport.reduction line 400
  61. theorem OAI.PerfectCompleteness.MixedSupport.keyFields_projection line 404
  62. theorem OAI.PerfectCompleteness.MixedSupport.reduction_projection line 413
  63. theorem OAI.PerfectCompleteness.MixedSupport.coordinateInvariant line 423
  64. theorem OAI.PerfectCompleteness.MixedSupport.constant_on_reduction_fibers line 430
  65. def OAI.PerfectCompleteness.MixedSupport.retainedKeys line 435
  66. theorem OAI.PerfectCompleteness.MixedSupport.retainedKeys_projection line 440