OAI/Computability/MaxCut/Machines/MachineFiniteTable.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaxCutGames.Foundations.Complexity.MachineFiniteTable.dispatch line 14
2. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFiniteTable.stepAux_dispatch line 21
3. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFiniteTable.dispatch_push_bound line 39

   Source documentation

   A finite upper bound on all literal push chains in the decision tree.

   theorem dispatch_push_bound (dst : K) (table : σ → List (Γ dst))
       (next : TM2.Stmt Γ Λ σ) (keys : List σ) :
       Runtime.statementPushBound (dispatch dst table next keys) ≤
         (keys.map (fun state => (table state).length)).sum +
           Runtime.statementPushBound next := by
   …

   Mentions: OAI.MaxCutGames.Foundations.Complexity.Runtime.statementPushBound, OAI.MaxCutGames.Foundations.Complexity.MachineFiniteTable.dispatch

4. def OAI.MaxCutGames.Foundations.Complexity.MachineFiniteTable.emit line 51
5. def OAI.MaxCutGames.Foundations.Complexity.MachineFiniteTable.tableBound line 55
6. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFiniteTable.stepAux_emit line 58
7. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFiniteTable.emit_push_bound line 65
8. def OAI.MaxCutGames.Foundations.Complexity.MachineFiniteTable.emitInTime line 73

   Source documentation

   One actual transition emits the table entry and enters the continuation. The caller supplies its program equation, not an execution assumption.

   def emitInTime (dst : K) (table : σ → List (Γ dst))
       (keys : List σ) (hkeys : ∀ state, state ∈ keys)
       (program : Λ → TM2.Stmt Γ Λ σ) (label exitLabel : Λ)
       (atLabel : program label = emit dst table keys (.goto (fun _ => exitLabel)))
       (state : σ) (tapes : ∀ k, List (Γ k)) :
       StateTransition.EvalsToInTime (TM2.step program)
         ⟨some label, state, tapes⟩
         (some ⟨some exitLabel, state,
           Function.update tapes dst (table state ++ tapes dst)⟩) 1 where
   …

   Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineFiniteTable.emit

9. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFiniteTable.output_frame line 90