OAI/Combinatorics/IndependentSets/Machines/PCPGapMachine.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargeIndependentSets.PCPGapMachine.round line 13
  2. lemma OAI.LargeIndependentSets.PCPGapMachine.round_finiteAlphabet line 16
  3. def OAI.LargeIndependentSets.PCPGapMachine.certificate line 21
  4. lemma OAI.LargeIndependentSets.PCPGapMachine.finiteAlphabet line 26
  5. lemma OAI.LargeIndependentSets.BinaryNormalize.annotated_input line 36
  6. def OAI.LargeIndependentSets.BinaryNormalize.eventCode line 39
  7. def OAI.LargeIndependentSets.BinaryNormalize.sourcePosition line 44
  8. def OAI.LargeIndependentSets.BinaryNormalize.blockValue line 48
  9. lemma OAI.LargeIndependentSets.BinaryNormalize.blockValue_spec line 58
  10. lemma OAI.LargeIndependentSets.BinaryNormalize.clauses_length line 72
  11. def OAI.LargeIndependentSets.BinaryNormalize.tableCount line 75
  12. def OAI.LargeIndependentSets.BinaryNormalize.tableValue line 77
  13. lemma OAI.LargeIndependentSets.BinaryNormalize.tableValue_spec line 81
  14. lemma OAI.LargeIndependentSets.BinaryNormalize.encodeWords_flatMap line 105
  15. lemma OAI.LargeIndependentSets.BinaryNormalize.tableWords_spec line 111
  16. def OAI.LargeIndependentSets.BinaryNormalize.finiteTableExpr line 115
  17. lemma OAI.LargeIndependentSets.BinaryNormalize.finiteTableExpr_eval line 119
  18. def OAI.LargeIndependentSets.BinaryNormalize.tagExpr line 130
  19. lemma OAI.LargeIndependentSets.BinaryNormalize.tagExpr_eval line 134
  20. def OAI.LargeIndependentSets.BinaryNormalize.sourcePositionExpr line 148
  21. lemma OAI.LargeIndependentSets.BinaryNormalize.sourcePositionExpr_eval line 153
  22. def OAI.LargeIndependentSets.BinaryNormalize.blockExpr line 162
  23. lemma OAI.LargeIndependentSets.BinaryNormalize.blockExpr_eval line 171
  24. def OAI.LargeIndependentSets.BinaryNormalize.countExpr line 187
  25. def OAI.LargeIndependentSets.BinaryNormalize.valueExpr line 188
  26. lemma OAI.LargeIndependentSets.BinaryNormalize.countExpr_eval line 195
  27. lemma OAI.LargeIndependentSets.BinaryNormalize.valueExpr_eval line 199
  28. lemma OAI.LargeIndependentSets.BinaryNormalize.serializer_spec line 207
  29. def OAI.LargeIndependentSets.BinaryNormalize.serializer line 213
  30. lemma OAI.LargeIndependentSets.BinaryNormalize.serializer_finiteAlphabet line 217
  31. def OAI.LargeIndependentSets.BinaryNormalize.annotator line 220
  32. def OAI.LargeIndependentSets.BinaryNormalize.certificate line 228
  33. lemma OAI.LargeIndependentSets.BinaryNormalize.finiteAlphabet line 232
  34. def OAI.LargeIndependentSets.BinaryNormalize.gapCertificate line 236
  35. lemma OAI.LargeIndependentSets.BinaryNormalize.gap_finiteAlphabet line 241