OAI/Computability/PerfectCompleteness/Machines/SourceOccurrenceProducerLemmas.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.SourceOccurrenceProducer.normalizedComputation line 13
  2. theorem OAI.PerfectCompleteness.SourceOccurrenceProducer.normalized_finiteAlphabet line 22
  3. def OAI.PerfectCompleteness.SourceOccurrenceProducer.rawComputation line 28
  4. theorem OAI.PerfectCompleteness.SourceOccurrenceProducer.raw_finiteAlphabet line 37
  5. def OAI.PerfectCompleteness.SourceOccurrenceProducer.computation line 42
  6. theorem OAI.PerfectCompleteness.SourceOccurrenceProducer.computation_finiteAlphabet line 52
  7. structure OAI.PerfectCompleteness.NormalizedSourceInput.Input line 70
  8. def OAI.PerfectCompleteness.NormalizedSourceInput.bits line 76
  9. def OAI.PerfectCompleteness.NormalizedSourceInput.variableCount line 78
  10. def OAI.PerfectCompleteness.NormalizedSourceInput.clauseCount line 79
  11. theorem OAI.PerfectCompleteness.NormalizedSourceInput.clauseCount_positive line 81
  12. instance OAI.PerfectCompleteness.NormalizedSourceInput.clauseCount_neZero line 84
  13. def OAI.PerfectCompleteness.NormalizedSourceInput.clauses line 87
  14. theorem OAI.PerfectCompleteness.NormalizedSourceInput.clause_eq line 92
  15. theorem OAI.PerfectCompleteness.NormalizedSourceInput.variable_eq line 95
  16. theorem OAI.PerfectCompleteness.NormalizedSourceInput.signs_eq line 98
  17. theorem OAI.PerfectCompleteness.NormalizedSourceInput.bits_eq line 104
  18. theorem OAI.PerfectCompleteness.NormalizedSourceInput.decode_bits line 109
  19. theorem OAI.PerfectCompleteness.NormalizedSourceInput.ext line 113
  20. theorem OAI.PerfectCompleteness.NormalizedSourceInput.bits_injective line 119
  21. def OAI.PerfectCompleteness.NormalizedSourceInput.normalized line 125
  22. theorem OAI.PerfectCompleteness.NormalizedSourceInput.normalized_formula line 130
  23. theorem OAI.PerfectCompleteness.NormalizedSourceInput.normalized_bits line 133
  24. theorem OAI.PerfectCompleteness.NormalizedSourceInput.violatedCount_eq_failedCount line 136
  25. theorem OAI.PerfectCompleteness.NormalizedSourceInput.clauseGap_of_count line 143
  26. theorem OAI.PerfectCompleteness.NormalizedSourceInput.clauseGap_mk line 160
  27. theorem OAI.PerfectCompleteness.NormalizedSourceInput.normalized_clauseGap line 170
  28. def OAI.PerfectCompleteness.NormalizedSourceInput.normalizedComputation line 177
  29. theorem OAI.PerfectCompleteness.NormalizedSourceInput.normalized_finiteAlphabet line 182
  30. def OAI.PerfectCompleteness.NormalizedSourceInput.raw line 186
  31. theorem OAI.PerfectCompleteness.NormalizedSourceInput.raw_formula line 188
  32. def OAI.PerfectCompleteness.NormalizedSourceInput.rawComputation line 191
  33. theorem OAI.PerfectCompleteness.NormalizedSourceInput.raw_finiteAlphabet line 196
  34. theorem OAI.PerfectCompleteness.NormalizedSourceInput.raw_satisfiable_iff line 199
  35. theorem OAI.PerfectCompleteness.NormalizedSourceInput.raw_clauseGap line 203
  36. def OAI.PerfectCompleteness.NormalizedSourceInput.fromReduction line 208
  37. theorem OAI.PerfectCompleteness.NormalizedSourceInput.fromReduction_formula line 212
  38. def OAI.PerfectCompleteness.NormalizedSourceInput.computation line 216
  39. theorem OAI.PerfectCompleteness.NormalizedSourceInput.computation_finiteAlphabet line 223
  40. theorem OAI.PerfectCompleteness.NormalizedSourceInput.producer line 229