Theorem: HMem.Trace.CostedProgram.splitTimeCost
Proof state before:
α : 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
⊢ Stack.halts
    (Stack.execution
      {
        state :=
          Complexity.encode
            (Option.get (Complexity.decode γ✝ (Memory.getms m src✝))
              (_ : Option.isSome (Complexity.decode γ✝ (Memory.getms m src✝)) = true)),
        current := Encoding.getProgram fs✝, function := Encoding.getProgram fs✝ }
      [])

case 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
⊢ Stack.hasTimeCost
    (Stack.execution
      {
        state :=
          Memory.setms m dst✝
            (Complexity.encode
              (fs✝
                (Option.get (Complexity.decode γ✝ (Memory.getms m src✝))
                  (_ : Option.isSome (Complexity.decode γ✝ (Memory.getms m src✝)) = true)))),
        current := TracedProgram.toProgram (toTracedProgram next), function := toProgram fcp }
      [])
    ?m.173010

α : 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
⊢ ?m.173010 +
        Complexity.ALE.bound Complexity.cost_ale
          (Option.get (Complexity.decode γ✝ (Memory.getms m src✝))
            (_ : Option.isSome (Complexity.decode γ✝ (Memory.getms m src✝)) = true)) +
      1 ≤
    (subroutineTimeCost h + recurseTimeCost hf h + localTimeCost h) a
Tactic:
exact (hcost.toComputable.has_result _).elim λ _ h ↦ ⟨(_, _), h⟩
Proof state after:
case 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
⊢ Stack.hasTimeCost
    (Stack.execution
      {
        state :=
          Memory.setms m dst✝
            (Complexity.encode
              (fs✝
                (Option.get (Complexity.decode γ✝ (Memory.getms m src✝))
                  (_ : Option.isSome (Complexity.decode γ✝ (Memory.getms m src✝)) = true)))),
        current := TracedProgram.toProgram (toTracedProgram next), function := toProgram fcp }
      [])
    ?m.173010

α : 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
⊢ ?m.173010 +
        Complexity.ALE.bound Complexity.cost_ale
          (Option.get (Complexity.decode γ✝ (Memory.getms m src✝))
            (_ : Option.isSome (Complexity.decode γ✝ (Memory.getms m src✝)) = true)) +
      1 ≤
    (subroutineTimeCost h + recurseTimeCost hf h + localTimeCost h) a