OAI/Computability/SpaceSimulation/Epoch/Meter.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Fifths.Tour.coins_array line 9
2. theorem OAI.Fifths.Tour.coins_history line 13
3. theorem OAI.Fifths.Tour.supplied line 19

   Source comment

   Both kinds at once. Charge a retained Y only on a call into an array column of this epoch.

   theorem supplied (v : D.Vertex) (p : D.baseOf v = false) :
       D.coins (D.header v) + D.coinsEasy ≤ D.coins v ∧
       (∀ i < D.N, D.coins (D.childrenOf v i) + D.circuit.price (D.guesses v) ≤ D.coins v) := by
   …

4. theorem OAI.Fifths.Tour.covers line 58
5. theorem OAI.Fifths.Tour.coins_total line 62