OAI/Computability/SpaceSimulation/Evaluation/Evaluate.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Fifths.Circuit.pic line 13
2. theorem OAI.Fifths.Circuit.Ready.flow_uniform line 17
3. theorem OAI.Fifths.Circuit.evaluate line 38

   Source documentation

   Compute the designated word using only the requested budget. All sizes in Ready, Scaled and Comp are uniform.

   theorem evaluate (c : Ready C x S cp) (g : ∀ i, (C i).Good)
       (B : ∀ i, (C i).Node → ℕ) (funding : ∀ i, (C i).Meter (B i))
       (v : ∀ i, (C i).Node)
       (w : Comp x S cp (fun i => (v i).val))
       (h : Scaled S (fun i => B i (v i))) :
       Comp x S cp (fun i => (C i).semantic (v i)) := by
   …

   Mentions: OAI.Fifths.Circuit.Ready, OAI.Fifths.Circuit.Good, OAI.Fifths.Circuit.Node, OAI.Fifths.Circuit.Meter, OAI.Fifths.Comp, OAI.Fifths.Scaled