OAI/Computability/MaxCut/Machines/AddressMachineInitial.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MaxCutGames.Reduction.AddressMachineInitial.afterHeaders line 15
  2. def OAI.MaxCutGames.Reduction.AddressMachineInitial.initialized line 20
  3. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.input_header_inline_AddressMachineInitial line 24
  4. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.input_headerClean line 31
  5. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.afterHeaders_frame line 52
  6. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.afterHeaders_empty line 62
  7. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.afterHeaders_source line 73
  8. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.afterHeaders_variables line 78
  9. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.afterHeaders_occurrences line 90
  10. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.afterHeaders_base line 102
  11. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.afterHeaders_capacity line 107
  12. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.afterHeaders_reversed line 112
  13. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.afterHeaders_work line 126
  14. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.afterHeaders_current line 129
  15. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.afterHeaders_remaining line 133
  16. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.afterHeaders_copyScratch line 137
  17. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.initialized_frame line 141
  18. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.initialized_header line 147
  19. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.initialized_source line 155
  20. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.initialized_variables line 162
  21. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.initialized_occurrences line 165
  22. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.initialized_base line 168
  23. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.initialized_capacity line 172
  24. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.initialized_reversed line 176
  25. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.initialized_current line 182
  26. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.initialized_remaining line 187
  27. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.initialized_savedIndex line 193
  28. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.initialized_empty line 197
  29. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.initialized_work line 203
  30. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.initialized_index line 207
  31. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.initialized_scratch line 214
  32. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.initialized_copyScratch line 221
  33. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.initialized_field line 226
  34. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.initialized_finalOutput line 234
  35. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.initialized_privateAddress line 243
  36. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.initialized_edgeClean line 253
  37. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.initialized_eq_setDigits_zero line 269

    Source documentation

    An exact equality with the checked schedule's initial digit configuration.

    theorem initialized_eq_setDigits_zero (F : SourceEncoding.Input) :
    initialized k T F = AddressOdometerSchedule.setDigits F.equations.length
      (fun _ : Fin k => 0) (afterHeaders k T F) := by
…

    Mentions: OAI.MaxCutGames.Reduction.SourceEncoding.Input, OAI.MaxCutGames.Reduction.AddressMachineInitial.initialized, OAI.MaxCutGames.Reduction.AddressOdometerSchedule.setDigits, OAI.MaxCutGames.Reduction.AddressMachineInitial.afterHeaders

  38. def OAI.MaxCutGames.Reduction.AddressMachineInitial.inTime line 295

    Source documentation

    Actual two-phase initialization from the concrete machine input.

    def inTime (F : SourceEncoding.Input) :
    StateTransition.EvalsToInTime (AddressMachineProgram.machine k T).step
      (initList (AddressMachineProgram.machine k T) (SourceEncoding.inputBits F))
      (some ⟨some (AddressMachineProgram.bodyStart k T), AddressMachineSpace.initialState k,
        initialized k T F⟩)
      ((MachineAddressHeaders.timePolynomial k s d T.vectors.length).eval
        (SourceEncoding.inputBits F).length + k * (2 * (SourceEncoding.inputBits F).length + 6) + 1) := by
…

    Mentions: OAI.MaxCutGames.Reduction.SourceEncoding.Input, OAI.MaxCutGames.Reduction.AddressMachineProgram.machine, OAI.MaxCutGames.Reduction.SourceEncoding.inputBits, OAI.MaxCutGames.Reduction.AddressMachineProgram.bodyStart, OAI.MaxCutGames.Reduction.AddressMachineSpace.initialState, OAI.MaxCutGames.Reduction.AddressMachineInitial.initialized, OAI.MaxCutGames.Reduction.MachineAddressHeaders.timePolynomial

  39. def OAI.MaxCutGames.Reduction.AddressMachineInitial.timePolynomial line 329
  40. theorem OAI.MaxCutGames.Reduction.AddressMachineInitial.timePolynomial_eval line 333
  41. def OAI.MaxCutGames.Reduction.AddressMachineInitial.inPolynomialTime line 340