OAI/Computability/MinUncut/PCP/FieldArray.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Foundations.Hastad.SourceFieldArray.finish line 14
  2. theorem OAI.MinUncutGames.Foundations.Hastad.SourceFieldArray.finishStep line 18
  3. def OAI.MinUncutGames.Foundations.Hastad.SourceFieldArray.sequenceTapes line 28
  4. theorem OAI.MinUncutGames.Foundations.Hastad.SourceFieldArray.sequenceTrace line 36
  5. def OAI.MinUncutGames.Foundations.Hastad.SourceFieldArray.sequenceInTime line 95
  6. theorem OAI.MinUncutGames.Foundations.Hastad.SourceFieldArray.sequence_time_eq_length line 117
  7. theorem OAI.MinUncutGames.Foundations.Hastad.SourceFieldArray.sequenceTapes_other line 122
  8. theorem OAI.MinUncutGames.Foundations.Hastad.SourceFieldArray.sequenceTapes_source line 137
  9. theorem OAI.MinUncutGames.Foundations.Hastad.SourceFieldArray.sequenceTapes_selected line 152
  10. def OAI.MinUncutGames.Foundations.Hastad.SourceFieldArray.boundedIndex line 200
  11. theorem OAI.MinUncutGames.Foundations.Hastad.SourceFieldArray.boundedIndex_val line 202
  12. def OAI.MinUncutGames.Foundations.Hastad.SourceFieldArray.destination line 205
  13. def OAI.MinUncutGames.Foundations.Hastad.SourceFieldArray.startLabel line 206
  14. def OAI.MinUncutGames.Foundations.Hastad.SourceFieldArray.loopLabel line 207
  15. theorem OAI.MinUncutGames.Foundations.Hastad.SourceFieldArray.destination_ne_source line 209
  16. theorem OAI.MinUncutGames.Foundations.Hastad.SourceFieldArray.destination_injective_below line 217
  17. theorem OAI.MinUncutGames.Foundations.Hastad.SourceFieldArray.destination_eq_succ line 224
  18. theorem OAI.MinUncutGames.Foundations.Hastad.SourceFieldArray.output_source line 228
  19. theorem OAI.MinUncutGames.Foundations.Hastad.SourceFieldArray.output_field line 236
  20. def OAI.MinUncutGames.Foundations.Hastad.SourceFieldArray.program line 249
  21. def OAI.MinUncutGames.Foundations.Hastad.SourceFieldArray.machine line 258
  22. theorem OAI.MinUncutGames.Foundations.Hastad.SourceFieldArray.atStart line 269
  23. theorem OAI.MinUncutGames.Foundations.Hastad.SourceFieldArray.atLoop line 273
  24. theorem OAI.MinUncutGames.Foundations.Hastad.SourceFieldArray.atDone line 278
  25. def OAI.MinUncutGames.Foundations.Hastad.SourceFieldArray.machineInTime line 281
  26. def OAI.MinUncutGames.Foundations.Hastad.SourceFieldArray.machineInTime_inputBound line 309
  27. def OAI.MinUncutGames.Foundations.Hastad.SourceFieldArray.sixFieldsInTime line 323