Theorem: HMem.Program.simpleLoopCost
Proof state before:
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
arg : α
harg : sz arg < sz a
⊢ Nat.succ (sz arg) ≤ sz a

TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
a : α
hsz : sz a = Nat.succ n₀
arg : α
harg : sz arg < sz a
ih : ∀ (a : α), sz a = sz arg → timeCost' p h a ≤ x * sz arg + x
⊢ timeCost (Trace.TracedProgram.toProgram (Trace.CostedProgram.toTracedProgram (costed p)))
      (_ :
        haltsOn (Trace.TracedProgram.toProgram (Trace.CostedProgram.toTracedProgram (costed p)))
          (Complexity.encode arg)) ≤
    x * sz arg + x

TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
arg : α
harg : sz arg < sz a
⊢ sz arg ≤ n₀

case a
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
⊢ maxRecurse (Trace.CostedProgram.toProgram (costed p)) * (x * n₀ + x) ≤ x * Nat.succ n₀
Tactic:
apply Nat.succ_le_of_lt harg
Proof state after:
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
a : α
hsz : sz a = Nat.succ n₀
arg : α
harg : sz arg < sz a
ih : ∀ (a : α), sz a = sz arg → timeCost' p h a ≤ x * sz arg + x
⊢ timeCost (Trace.TracedProgram.toProgram (Trace.CostedProgram.toTracedProgram (costed p)))
      (_ :
        haltsOn (Trace.TracedProgram.toProgram (Trace.CostedProgram.toTracedProgram (costed p)))
          (Complexity.encode arg)) ≤
    x * sz arg + x

TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
arg : α
harg : sz arg < sz a
⊢ sz arg ≤ n₀

case a
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
⊢ maxRecurse (Trace.CostedProgram.toProgram (costed p)) * (x * n₀ + x) ≤ x * Nat.succ n₀