Theorem: HMem.Trace.CostedProgram.splitTimeCost
Proof state before:
case hr
α : 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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ fm x✝¹
⊢ Stack.hasResult
    (Stack.execution
      {
        state :=
          Complexity.encode
            (Option.get (Complexity.decode α (Memory.getms x✝ src✝))
              (_ : Option.isSome (Complexity.decode α (Memory.getms x✝ src✝)) = true)),
        current := toProgram fcp, function := toProgram fcp }
      [])
    ?m.179017

α : 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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ fm x✝¹
⊢ Memory

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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ fm x✝¹
⊢ Stack.hasTimeCost
    (Stack.execution { state := Memory.getms x✝ src✝, current := toProgram fcp, function := toProgram fcp } [])
    ?m.179014

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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ fm x✝¹
⊢ Stack.hasTimeCost
    (Stack.execution
      { state := Memory.setms x✝ dst✝ ?m.179017, current := TracedProgram.toProgram (toTracedProgram next✝),
        function := toProgram fcp }
      [])
    ?m.179013

α : 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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ fm x✝¹
⊢ ℕ

α : 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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ fm x✝¹
⊢ ℕ

α : 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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ fm x✝¹
⊢ Memory

α : 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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ fm x✝¹
⊢ ?m.179013 + ?m.179014 + 1 ≤ (subroutineTimeCost h + recurseTimeCost hf h + localTimeCost h) x✝¹
Tactic:
apply Program.hasResult_of_sound hf
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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ fm x✝¹
⊢ Stack.hasTimeCost
    (Stack.execution { state := Memory.getms x✝ src✝, current := toProgram fcp, function := toProgram fcp } [])
    ?m.179014

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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ fm x✝¹
⊢ Stack.hasTimeCost
    (Stack.execution
      {
        state :=
          Memory.setms x✝ dst✝
            (Complexity.encode
              (f
                (Option.get (Complexity.decode α (Memory.getms x✝ src✝))
                  (_ : Option.isSome (Complexity.decode α (Memory.getms x✝ src✝)) = true)))),
        current := TracedProgram.toProgram (toTracedProgram next✝), function := toProgram fcp }
      [])
    ?m.179013

α : 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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ fm x✝¹
⊢ ℕ

α : 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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ fm x✝¹
⊢ ℕ

α : 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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ fm x✝¹
⊢ ?m.179013 + ?m.179014 + 1 ≤ (subroutineTimeCost h + recurseTimeCost hf h + localTimeCost h) x✝¹