OAI/Computability/BinPacking/PCP/CompareLoop.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.Tape line 11
  2. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.Tape.enumList line 17
  3. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.Tape.enumList_getElem?_ctorIdx_eq line 21
  4. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.Tape.enumList_nodup line 25
  5. instance OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.(instance at line 27) line 27
  6. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.Alphabet line 31
  7. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.Flags line 33
  8. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.Ambient line 34
  9. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.State line 35
  10. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.normal line 37
  11. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.initial line 40
  12. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.context line 42
  13. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.compareEquiv line 45
  14. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.compareEquiv_normal line 52
  15. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.emitterEquiv line 57
  16. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.setupPorts line 63
  17. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.setupPorts_injective line 66
  18. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.headPorts line 70
  19. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.headPorts_injective line 73
  20. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.rowSources line 77
  21. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.headerSources line 78
  22. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.fieldPorts line 79
  23. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.cleanupPorts line 81
  24. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.cleanupPorts_ne_output line 85
  25. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.cleanupPorts_cover line 88
  26. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.compareStatement line 110
  27. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.emitterStatement line 115
  28. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.storeLoop line 119
  29. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.stepAux_storeLoop line 122
  30. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.nextRow line 127
  31. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.stepAux_nextRow line 131
  32. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.RuntimeModel.transportInTime line 139
  33. inductive OAI.BinPackingGames.Foundations.PCP.AlphabetTable.CompareLoop.Label line 160
  34. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetTable.CompareLoop.Label.enumList line 165
  35. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.CompareLoop.Label.enumList_getElem?_ctorIdx_eq line 168
  36. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.CompareLoop.Label.enumList_nodup line 172
  37. instance OAI.BinPackingGames.Foundations.PCP.AlphabetTable.CompareLoop.(instance at line 174) line 174
  38. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.CompareLoop.statement line 180
  39. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.CompareLoop.compareProgram_at line 199
  40. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.CompareLoop.compareWordsInTime line 209
  41. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.CompareLoop.comparisonTime line 265
  42. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.CompareLoop.encodeWord_eq_iff line 268
  43. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.CompareLoop.compareInTime line 277
  44. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.CompareLoop.comparisonTime_le line 294
  45. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.CompareLoop.comparisonTime_le_of_lt line 301
  46. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.CompareLoop.compareWordsInTime_bounded line 308
  47. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.CompareLoop.rowLoop line 327
  48. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.CompareLoop.rowState line 330
  49. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.CompareLoop.rowLoop_eq_graph line 333
  50. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.CompareLoop.rowContext_eq line 340
  51. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.CompareLoop.compareRowInTime line 347
  52. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.CompareLoop.relationFromRowState line 365