OAI/Computability/PerfectCompleteness/Foundations/SourceClause.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.SourceClause.Triple line 11
  2. def OAI.PerfectCompleteness.SourceClause.Triple.at line 13
  3. def OAI.PerfectCompleteness.SourceClause.literalTruth line 19
  4. def OAI.PerfectCompleteness.SourceClause.localEval line 22
  5. def OAI.PerfectCompleteness.SourceClause.allTriples line 26
  6. def OAI.PerfectCompleteness.SourceClause.satisfyingTriples line 32
  7. theorem OAI.PerfectCompleteness.SourceClause.mem_allTriples line 35
  8. theorem OAI.PerfectCompleteness.SourceClause.mem_satisfyingTriples line 39
  9. theorem OAI.PerfectCompleteness.SourceClause.satisfyingTriples_nodup line 43
  10. theorem OAI.PerfectCompleteness.SourceClause.satisfyingTriples_length line 48
  11. theorem OAI.PerfectCompleteness.SourceClause.coordinate_truth_table line 53
  12. theorem OAI.PerfectCompleteness.SourceClause.coordinate_surjective line 60
  13. theorem OAI.PerfectCompleteness.SourceClause.pair_truth_table line 66
  14. theorem OAI.PerfectCompleteness.SourceClause.pair_surjective line 73
  15. structure OAI.PerfectCompleteness.SourceClause.NormalizedClause line 80
  16. def OAI.PerfectCompleteness.SourceClause.NormalizedClause.variable line 85
  17. def OAI.PerfectCompleteness.SourceClause.NormalizedClause.signs line 88
  18. def OAI.PerfectCompleteness.SourceClause.NormalizedClause.restrict line 91
  19. theorem OAI.PerfectCompleteness.SourceClause.localEval_restrict line 95
  20. theorem OAI.PerfectCompleteness.SourceClause.variable_ne line 100
  21. def OAI.PerfectCompleteness.SourceClause.NormalizedClause.extend line 104
  22. theorem OAI.PerfectCompleteness.SourceClause.restrict_extend line 108
  23. theorem OAI.PerfectCompleteness.SourceClause.satisfying_label_realized line 115
  24. abbrev OAI.PerfectCompleteness.SourceClause.Occurrence line 123
  25. def OAI.PerfectCompleteness.SourceClause.occurrenceVariable line 125
  26. theorem OAI.PerfectCompleteness.SourceClause.occurrence_determined_by_endpoints line 129
  27. theorem OAI.PerfectCompleteness.SourceClause.projection_determined_by_endpoints line 142
  28. def OAI.PerfectCompleteness.SourceClause.agreementCount line 149
  29. theorem OAI.PerfectCompleteness.SourceClause.agreementCount_le_three line 155
  30. theorem OAI.PerfectCompleteness.SourceClause.agreementCount_le_two_of_unsatisfied line 160
  31. theorem OAI.PerfectCompleteness.SourceClause.agreementCount_le_two_add_satisfied line 180
  32. theorem OAI.PerfectCompleteness.SourceClause.totalAgreement_le line 189