Theorem: HMem.Trace.CostedProgram.splitTimeCost
Proof state before:
case h₂.h.h.hf.h
α : 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
size : α → ℕ
fm : α → Option Memory
fcp : CostedProgram
hf : Program.sound (TracedProgram.toProgram (toTracedProgram fcp)) f size
dst✝ src✝ : Source
γ✝ δ✝ : Type
inst✝¹ : Complexity.Coding γ✝ Memory
inst✝ : Complexity.Encoding δ✝ Memory
fs✝ : γ✝ → δ✝
cs✝ : Complexity.CostFunction γ✝ ℕ
hcost : Complexity Encoding.Model fs✝ cs✝
next : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (subroutine' dst✝ src✝ inst✝¹ inst✝ fs✝ cs✝ hcost next)) fm
a : α
m : Memory
hm : m ∈ fm a
⊢ Option.isSome ((Complexity.decode γ✝ ∘ flip Memory.getms src✝) m) = true

α : 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
size : α → ℕ
fm : α → Option Memory
fcp : CostedProgram
hf : Program.sound (TracedProgram.toProgram (toTracedProgram fcp)) f size
dst✝ src✝ : Source
γ✝ δ✝ : Type
inst✝¹ : Complexity.Coding γ✝ Memory
inst✝ : Complexity.Encoding δ✝ Memory
fs✝ : γ✝ → δ✝
cs✝ : Complexity.CostFunction γ✝ ℕ
hcost : Complexity Encoding.Model fs✝ cs✝
next : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (subroutine' dst✝ src✝ inst✝¹ inst✝ fs✝ cs✝ hcost next)) fm
a : α
m : Memory
hm : m ∈ fm a
⊢ Complexity.ALE.bound Complexity.cost_ale
      (Option.get (Complexity.decode γ✝ (Memory.getms m src✝))
        (_ : Option.isSome (Complexity.decode γ✝ (Memory.getms m src✝)) = true)) ≤
    Encoding.getBound hcost (Option.get ((Complexity.decode γ✝ ∘ flip Memory.getms src✝) m) ?h₂.h.h.hf.h)
Tactic:
apply (h.left _ _ hm).elim λ hsome _ ↦ hsome
Proof state after:
α : 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
size : α → ℕ
fm : α → Option Memory
fcp : CostedProgram
hf : Program.sound (TracedProgram.toProgram (toTracedProgram fcp)) f size
dst✝ src✝ : Source
γ✝ δ✝ : Type
inst✝¹ : Complexity.Coding γ✝ Memory
inst✝ : Complexity.Encoding δ✝ Memory
fs✝ : γ✝ → δ✝
cs✝ : Complexity.CostFunction γ✝ ℕ
hcost : Complexity Encoding.Model fs✝ cs✝
next : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (subroutine' dst✝ src✝ inst✝¹ inst✝ fs✝ cs✝ hcost next)) fm
a : α
m : Memory
hm : m ∈ fm a
⊢ Complexity.ALE.bound Complexity.cost_ale
      (Option.get (Complexity.decode γ✝ (Memory.getms m src✝))
        (_ : Option.isSome (Complexity.decode γ✝ (Memory.getms m src✝)) = true)) ≤
    Encoding.getBound hcost
      (Option.get ((Complexity.decode γ✝ ∘ flip Memory.getms src✝) m)
        (_ : Option.isSome (Complexity.decode γ✝ (Memory.getms m src✝)) = true))