OAI/Computability/BinPacking/Information/SourceFieldArray.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingGames.Foundations.Hastad.SourceMachine.Alphabet line 12
  2. def OAI.BinPackingGames.Foundations.Hastad.SourceMachine.fieldLoop line 14
  3. def OAI.BinPackingGames.Foundations.Hastad.SourceMachine.fieldStart line 22
  4. def OAI.BinPackingGames.Foundations.Hastad.SourceMachine.fieldTapes line 26
  5. theorem OAI.BinPackingGames.Foundations.Hastad.SourceMachine.fieldTapes_source line 30
  6. theorem OAI.BinPackingGames.Foundations.Hastad.SourceMachine.fieldTapes_destination line 35
  7. theorem OAI.BinPackingGames.Foundations.Hastad.SourceMachine.fieldTapes_self line 40
  8. theorem OAI.BinPackingGames.Foundations.Hastad.SourceMachine.fieldTapes_other line 44
  9. theorem OAI.BinPackingGames.Foundations.Hastad.SourceMachine.update_field_source line 50
  10. theorem OAI.BinPackingGames.Foundations.Hastad.SourceMachine.update_field_destination line 61
  11. theorem OAI.BinPackingGames.Foundations.Hastad.SourceMachine.fieldStep_delimiter line 67
  12. theorem OAI.BinPackingGames.Foundations.Hastad.SourceMachine.fieldStep_true line 81
  13. theorem OAI.BinPackingGames.Foundations.Hastad.SourceMachine.fieldLoopTrace line 95
  14. theorem OAI.BinPackingGames.Foundations.Hastad.SourceMachine.fieldStartStep line 127
  15. def OAI.BinPackingGames.Foundations.Hastad.SourceMachine.fieldInTime line 141
  16. def OAI.BinPackingGames.Foundations.Hastad.SourceMachine.afterField line 171
  17. def OAI.BinPackingGames.Foundations.Hastad.SourceMachine.fieldNext line 175
  18. def OAI.BinPackingGames.Foundations.Hastad.SourceMachine.fourTapes line 182
  19. theorem OAI.BinPackingGames.Foundations.Hastad.SourceMachine.fourTapes_source line 189
  20. theorem OAI.BinPackingGames.Foundations.Hastad.SourceMachine.fourTapes_other line 195
  21. theorem OAI.BinPackingGames.Foundations.Hastad.SourceMachine.fourField_time_eq_length line 201
  22. def OAI.BinPackingGames.Foundations.Hastad.SourceMachine.fourFieldsInTime line 206
  23. def OAI.BinPackingGames.Foundations.Hastad.SourceMachine.fieldDestination line 250
  24. theorem OAI.BinPackingGames.Foundations.Hastad.SourceMachine.fourTapes_concrete line 252
  25. def OAI.BinPackingGames.Foundations.Hastad.SourceMachine.groupingProgram line 264
  26. def OAI.BinPackingGames.Foundations.Hastad.SourceMachine.groupingMachine line 271
  27. def OAI.BinPackingGames.Foundations.Hastad.SourceMachine.groupingMachineInTime line 282
  28. def OAI.BinPackingGames.Foundations.Hastad.SourceFieldArray.finish line 306
  29. theorem OAI.BinPackingGames.Foundations.Hastad.SourceFieldArray.finishStep line 310
  30. def OAI.BinPackingGames.Foundations.Hastad.SourceFieldArray.sequenceTapes line 320
  31. theorem OAI.BinPackingGames.Foundations.Hastad.SourceFieldArray.sequenceTrace line 328
  32. def OAI.BinPackingGames.Foundations.Hastad.SourceFieldArray.sequenceInTime line 387
  33. theorem OAI.BinPackingGames.Foundations.Hastad.SourceFieldArray.sequence_time_eq_length line 409
  34. theorem OAI.BinPackingGames.Foundations.Hastad.SourceFieldArray.sequenceTapes_other line 414
  35. theorem OAI.BinPackingGames.Foundations.Hastad.SourceFieldArray.sequenceTapes_source line 429
  36. theorem OAI.BinPackingGames.Foundations.Hastad.SourceFieldArray.sequenceTapes_selected line 444
  37. def OAI.BinPackingGames.Foundations.Hastad.SourceFieldArray.boundedIndex line 492
  38. theorem OAI.BinPackingGames.Foundations.Hastad.SourceFieldArray.boundedIndex_val line 494
  39. def OAI.BinPackingGames.Foundations.Hastad.SourceFieldArray.destination line 497
  40. def OAI.BinPackingGames.Foundations.Hastad.SourceFieldArray.startLabel line 498
  41. def OAI.BinPackingGames.Foundations.Hastad.SourceFieldArray.loopLabel line 499
  42. theorem OAI.BinPackingGames.Foundations.Hastad.SourceFieldArray.destination_ne_source line 501
  43. theorem OAI.BinPackingGames.Foundations.Hastad.SourceFieldArray.destination_injective_below line 509
  44. theorem OAI.BinPackingGames.Foundations.Hastad.SourceFieldArray.destination_eq_succ line 516
  45. theorem OAI.BinPackingGames.Foundations.Hastad.SourceFieldArray.output_source line 520
  46. theorem OAI.BinPackingGames.Foundations.Hastad.SourceFieldArray.output_field line 528
  47. def OAI.BinPackingGames.Foundations.Hastad.SourceFieldArray.program line 541
  48. def OAI.BinPackingGames.Foundations.Hastad.SourceFieldArray.machine line 550
  49. theorem OAI.BinPackingGames.Foundations.Hastad.SourceFieldArray.atStart line 561
  50. theorem OAI.BinPackingGames.Foundations.Hastad.SourceFieldArray.atLoop line 565
  51. theorem OAI.BinPackingGames.Foundations.Hastad.SourceFieldArray.atDone line 570
  52. def OAI.BinPackingGames.Foundations.Hastad.SourceFieldArray.machineInTime line 573
  53. def OAI.BinPackingGames.Foundations.Hastad.SourceFieldArray.machineInTime_inputBound line 601
  54. def OAI.BinPackingGames.Foundations.Hastad.SourceFieldArray.sixFieldsInTime line 615