OAI/Combinatorics/IndependentSets/PCP/Lookup.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.Alphabet line 14
  2. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.skipBits line 16
  3. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.stepAux_skipBits line 27
  4. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.stepAux_skipBits_fromTapes line 44
  5. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.skipBits_pushBound line 58
  6. inductive OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.Label line 66
  7. instance OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.(instance at line 70) line 70
  8. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.statement line 74
  9. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.program line 83
  10. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.rowBits line 87
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.rowBits_eq line 89
  12. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.rowsBits line 94
  13. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.rowsBits_nil line 97
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.rowsBits_cons line 99
  15. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.skipCost line 103
  16. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.prefixCost line 106
  17. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.lookupCost line 109