OAI/Combinatorics/IndependentSets/PCP/Ambient.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.skipRowTrace line 24
  2. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.skipRowTrace_fromTapes line 53
  3. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.selectTrace line 67
  4. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.lookupTailTrace line 85
  5. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.lookupCost_le line 153
  6. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.lookupTailInTime line 172
  7. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.tableTailTrace line 195
  8. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.fullTableTailTrace line 227
  9. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.lookup_frame line 267
  10. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.tableTailCost line 273
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.tableTailCost_le line 277
  12. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.headIndex line 300
  13. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.headValue line 303
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.headValue_eq_semantics line 306
  15. abbrev OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.HeadTapes line 309
  16. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.headLookupTapes line 311
  17. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.headLookupCost line 320
  18. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.headLookupCost_le line 324
  19. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.headTimePolynomial line 333
  20. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.headLookupInTime line 336
  21. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.headLookupTapes_head line 428
  22. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.headLookupTapes_frame line 433
  23. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.readRowTapes line 439
  24. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.readRowTapes_source line 444
  25. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.readRowTapes_tail line 450
  26. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.readRowTapes_reverse line 456
  27. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.readRowTapes_frame line 462
  28. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.readRowCost line 468
  29. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.readRowCost_le line 471
  30. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.readRowCost_table_le line 478
  31. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.readRowInTime line 487
  32. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Lookup.machine line 571