intro a
TracedProgram : Sort ?u.211566
α : Type u_1
inst✝⁶ : Complexity.Coding α Memory
β : Type u_2
inst✝⁵ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
γ δ : Type
inst✝⁴ : Complexity.Coding γ Memory
inst✝³ : Complexity.Encoding δ Memory
fs : γ → δ
cs : Complexity.CostFunction γ ℕ
inst✝² : Complexity.Computable Encoding.Model fs
inst✝¹ : Complexity Encoding.Model fs cs
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
⊢ timeCost' p h ≤ subroutineTimeCost h + recurseTimeCost h + localTimeCost h
TracedProgram : Sort ?u.211566
α : Type u_1
inst✝⁶ : Complexity.Coding α Memory
β : Type u_2
inst✝⁵ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
γ δ : Type
inst✝⁴ : Complexity.Coding γ Memory
inst✝³ : Complexity.Encoding δ Memory
fs : γ → δ
cs : Complexity.CostFunction γ ℕ
inst✝² : Complexity.Computable Encoding.Model fs
inst✝¹ : Complexity Encoding.Model fs cs
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
a : α
⊢ timeCost' p h a ≤ (subroutineTimeCost h + recurseTimeCost h + localTimeCost h) a