OAI/Computability/MinUncut/Games/Target.lean
19 declarations, 0 contain sorry, 0 declared as axioms
- structure
OAI.MinUncutGames.Foundations.Target.Literalline 9 - def
OAI.MinUncutGames.Foundations.Target.Literal.evalline 14 - abbrev
OAI.MinUncutGames.Foundations.Target.Clauseline 17 - def
OAI.MinUncutGames.Foundations.Target.Clause.evalline 19 - structure
OAI.MinUncutGames.Foundations.Target.Formulaline 22 - def
OAI.MinUncutGames.Foundations.Target.Formula.Satisfiableline 26 - structure
OAI.MinUncutGames.Foundations.Target.PermutationTableline 30 - theorem
OAI.MinUncutGames.Foundations.Target.PermutationTable.images_injectiveline 36 - theorem
OAI.MinUncutGames.Foundations.Target.PermutationTable.images_surjectiveline 41 - structure
OAI.MinUncutGames.Foundations.Target.Constraintline 45 - def
OAI.MinUncutGames.Foundations.Target.Constraint.satisfiedline 50 - structure
OAI.MinUncutGames.Foundations.Target.Instanceline 54 - def
OAI.MinUncutGames.Foundations.Target.countSatisfiedline 59 - theorem
OAI.MinUncutGames.Foundations.Target.countSatisfied_le_lengthline 65 - theorem
OAI.MinUncutGames.Foundations.Target.Instance.constraintCount_positiveline 74 - structure
OAI.MinUncutGames.Foundations.Target.RationalErrorline 80 - def
OAI.MinUncutGames.Foundations.Target.CompleteAtline 87 - def
OAI.MinUncutGames.Foundations.Target.SoundAtline 93 - structure
OAI.MinUncutGames.Foundations.Target.SemanticGapReductionline 98