Theorem: HMem.Program.simpleLoopCost
Proof state before:
case hi.h₁.h₁
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₀
⊢ (subroutineTimeCost h + recurseTimeCost h + localTimeCost h) a = ?hi.h₁.b

case hi.h₁.h₂
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₀
⊢ ?hi.h₁.b = ?hi.b

case hi.h₁.b
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₀
⊢ ℕ

case hi.h₂
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₀
⊢ ?hi.b ≤ x * Nat.succ n₀ + x

case hi.b
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₀
⊢ ℕ
Tactic:
apply Nat.add_right_comm _ _ _
Proof state after:
case hi.h₁.h₂
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₀
⊢ subroutineTimeCost h a + localTimeCost h a + recurseTimeCost h a = ?hi.b

case hi.h₂
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₀
⊢ ?hi.b ≤ x * Nat.succ n₀ + x

case hi.b
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₀
⊢ ℕ