Theorem: HMem.Trace.CostedProgram.splitTimeCost
Proof state before:
case h₂.h.h.ha
α : 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
⊢ ?h₂.h.h.a ∈ fm a

case h₂.h.h.hf
α : 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
⊢ ?h₂.h.b ∈ (Complexity.decode γ✝ ∘ flip Memory.getms src✝) ?h₂.h.h.a

case h₂.h.h.a
α : 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
⊢ Memory

case h₂.h.b
α : 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
⊢ γ✝

α : 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 ?h₂.h.b
Tactic:
apply hm
Proof state after:
case h₂.h.h.hf
α : 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
⊢ ?h₂.h.b ∈ (Complexity.decode γ✝ ∘ flip Memory.getms src✝) m

case h₂.h.b
α : 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
⊢ γ✝

α : 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 ?h₂.h.b