OAI/Combinatorics/KMedian/PCP/PathTable.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MetricKMedian.PCP.Compiler.PowerProgram.Testline 11 - def
OAI.MetricKMedian.PCP.Compiler.PowerProgram.relationline 17 - lemma
OAI.MetricKMedian.PCP.Compiler.PowerProgram.cut_prefixline 23 - lemma
OAI.MetricKMedian.PCP.Compiler.PowerProgram.path_literalline 32 - lemma
OAI.MetricKMedian.PCP.Compiler.PowerProgram.relation_correctline 52