OAI/Computability/DirectedFeedback/Machines/MachineOutcomeRows.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.DFVSGames.Reduction.MachineOutcomeRows.Spec line 56
  2. structure OAI.DFVSGames.Reduction.MachineOutcomeRows.Values line 61
  3. abbrev OAI.DFVSGames.Reduction.MachineOutcomeRows.Rhs line 67
  4. abbrev OAI.DFVSGames.Reduction.MachineOutcomeRows.Row line 68
  5. abbrev OAI.DFVSGames.Reduction.MachineOutcomeRows.State line 69
  6. abbrev OAI.DFVSGames.Reduction.MachineOutcomeRows.Alphabet line 70
  7. abbrev OAI.DFVSGames.Reduction.MachineOutcomeRows.LocalLabel line 74
  8. def OAI.DFVSGames.Reduction.MachineOutcomeRows.localMain line 78
  9. def OAI.DFVSGames.Reduction.MachineOutcomeRows.localInstruction line 83
  10. def OAI.DFVSGames.Reduction.MachineOutcomeRows.payload line 88
  11. def OAI.DFVSGames.Reduction.MachineOutcomeRows.rowResult line 92
  12. def OAI.DFVSGames.Reduction.MachineOutcomeRows.rowCost line 97
  13. def OAI.DFVSGames.Reduction.MachineOutcomeRows.rowCosts line 103
  14. theorem OAI.DFVSGames.Reduction.MachineOutcomeRows.rowCosts_length line 110
  15. structure OAI.DFVSGames.Reduction.MachineOutcomeRows.Invariant line 118
  16. theorem OAI.DFVSGames.Reduction.MachineOutcomeRows.Invariant.appended line 132
  17. theorem OAI.DFVSGames.Reduction.MachineOutcomeRows.appended_nil line 143
  18. theorem OAI.DFVSGames.Reduction.MachineOutcomeRows.sequence_result line 147
  19. theorem OAI.DFVSGames.Reduction.MachineOutcomeRows.sequence_steps line 159
  20. def OAI.DFVSGames.Reduction.MachineOutcomeRows.sequenceInstruction line 168
  21. theorem OAI.DFVSGames.Reduction.MachineOutcomeRows.sequenceTrace line 174
  22. def OAI.DFVSGames.Reduction.MachineOutcomeRows.selected line 201
  23. theorem OAI.DFVSGames.Reduction.MachineOutcomeRows.selected_length line 204
  24. abbrev OAI.DFVSGames.Reduction.MachineOutcomeRows.Label line 207
  25. instance OAI.DFVSGames.Reduction.MachineOutcomeRows.localLabelFintype line 210
  26. instance OAI.DFVSGames.Reduction.MachineOutcomeRows.localLabelDecidableEq line 213
  27. instance OAI.DFVSGames.Reduction.MachineOutcomeRows.labelFintype line 224
  28. instance OAI.DFVSGames.Reduction.MachineOutcomeRows.labelDecidableEq line 227
  29. def OAI.DFVSGames.Reduction.MachineOutcomeRows.sequenceEntry line 230
  30. def OAI.DFVSGames.Reduction.MachineOutcomeRows.dispatcher line 236
  31. def OAI.DFVSGames.Reduction.MachineOutcomeRows.instruction line 244
  32. def OAI.DFVSGames.Reduction.MachineOutcomeRows.program line 251
  33. theorem OAI.DFVSGames.Reduction.MachineOutcomeRows.dispatcherStep line 255
  34. theorem OAI.DFVSGames.Reduction.MachineOutcomeRows.phaseTrace line 268
  35. def OAI.DFVSGames.Reduction.MachineOutcomeRows.phaseInTime line 290
  36. theorem OAI.DFVSGames.Reduction.MachineOutcomeRows.emitted_output line 307
  37. theorem OAI.DFVSGames.Reduction.MachineOutcomeRows.exact_row_count line 316
  38. def OAI.DFVSGames.Reduction.MachineOutcomeRows.timePolynomial line 322
  39. theorem OAI.DFVSGames.Reduction.MachineOutcomeRows.rowCosts_sum_le line 326
  40. theorem OAI.DFVSGames.Reduction.MachineOutcomeRows.phaseCost_le_timePolynomial line 355
  41. structure OAI.DFVSGames.Reduction.WeightedSource.RationalSource line 382
  42. def OAI.DFVSGames.Reduction.WeightedSource.RationalSource.denominator line 394
  43. theorem OAI.DFVSGames.Reduction.WeightedSource.RationalSource.denominator_positive line 396
  44. theorem OAI.DFVSGames.Reduction.WeightedSource.RationalSource.den_dvd_denominator line 399
  45. def OAI.DFVSGames.Reduction.WeightedSource.RationalSource.numerator line 403
  46. theorem OAI.DFVSGames.Reduction.WeightedSource.RationalSource.numerator_cast line 406
  47. theorem OAI.DFVSGames.Reduction.WeightedSource.RationalSource.weight_eq_ratio line 422
  48. def OAI.DFVSGames.Reduction.WeightedSource.RationalSource.numerators line 428
  49. theorem OAI.DFVSGames.Reduction.WeightedSource.RationalSource.length_numerators line 430
  50. theorem OAI.DFVSGames.Reduction.WeightedSource.RationalSource.sum_numerators line 433
  51. def OAI.DFVSGames.Reduction.WeightedSource.RationalSource.equationAt line 439
  52. theorem OAI.DFVSGames.Reduction.WeightedSource.RationalSource.equationAt_fin line 442
  53. def OAI.DFVSGames.Reduction.WeightedSource.RationalSource.roundedEquations line 445
  54. theorem OAI.DFVSGames.Reduction.WeightedSource.RationalSource.roundedEquations_length line 448
  55. theorem OAI.DFVSGames.Reduction.WeightedSource.RationalSource.roundedEquations_nonempty line 452
  56. theorem OAI.DFVSGames.Reduction.WeightedSource.RationalSource.roundedEquations_origin line 459
  57. def OAI.DFVSGames.Reduction.WeightedSource.RationalSource.weightedValue line 468
  58. def OAI.DFVSGames.Reduction.WeightedSource.RationalSource.roundedValue line 471
  59. theorem OAI.DFVSGames.Reduction.WeightedSource.selectedSum_ofFn line 476
  60. theorem OAI.DFVSGames.Reduction.WeightedSource.RationalSource.selectedMass_cast line 489
  61. theorem OAI.DFVSGames.Reduction.WeightedSource.RationalSource.roundedValue_bounds line 499
  62. def OAI.DFVSGames.Reduction.WeightedSource.RationalSource.roundingDenominator line 540
  63. theorem OAI.DFVSGames.Reduction.WeightedSource.RationalSource.roundingDenominator_positive line 543
  64. theorem OAI.DFVSGames.Reduction.WeightedSource.RationalSource.roundingDenominator_budget line 548
  65. theorem OAI.DFVSGames.Reduction.WeightedSource.RationalSource.roundingDenominator_size line 569
  66. theorem OAI.DFVSGames.Reduction.WeightedSource.RationalSource.completeness_transport line 573
  67. theorem OAI.DFVSGames.Reduction.WeightedSource.RationalSource.soundness_transport line 580
  68. theorem OAI.DFVSGames.Reduction.WeightedSource.RationalSource.roundedEquations_for_nonempty line 588
  69. theorem OAI.DFVSGames.Reduction.WeightedSource.e3lin_completeness line 598
  70. theorem OAI.DFVSGames.Reduction.WeightedSource.e3lin_soundness line 614
  71. def OAI.DFVSGames.Reduction.Preprocessing.rounded line 646
  72. theorem OAI.DFVSGames.Reduction.Preprocessing.rounded_failure_add_value line 651
  73. theorem OAI.DFVSGames.Reduction.Preprocessing.rounded_complete line 661
  74. theorem OAI.DFVSGames.Reduction.Preprocessing.rounded_sound line 673
  75. def OAI.DFVSGames.Reduction.Preprocessing.uniformSource line 686
  76. theorem OAI.DFVSGames.Reduction.Preprocessing.cloned_failure_eq line 689
  77. theorem OAI.DFVSGames.Reduction.Preprocessing.uniformSource_complete line 709
  78. theorem OAI.DFVSGames.Reduction.Preprocessing.uniformSource_distinct line 721
  79. theorem OAI.DFVSGames.Reduction.Preprocessing.uniformSource_sound line 725
  80. theorem OAI.DFVSGames.Reduction.OuterCompleteness.weighted_completeAt line 763
  81. def OAI.DFVSGames.Reduction.OuterCompleteness.sourceError line 777
  82. theorem OAI.DFVSGames.Reduction.OuterCompleteness.sourceError_pos line 780
  83. theorem OAI.DFVSGames.Reduction.OuterCompleteness.weighted_completeAt_of_parameters line 785
  84. theorem OAI.DFVSGames.Reduction.OuterCompleteness.weighted_explicit_completeAt_of_parameters line 806