Theorem: HMem.Trace.CostedProgram.splitTimeCost
Proof state before:
case 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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ fm x✝¹
⊢ Memory.setms x✝ dst✝
      (Complexity.encode
        (f
          (Option.get (Complexity.decode α (Memory.getms x✝ src✝))
            (_ : Option.isSome (Complexity.decode α (Memory.getms x✝ src✝)) = true)))) ∈
    ((flip Option.bind fun m =>
          Option.map (Memory.setms m dst✝ ∘ Complexity.encode ∘ f) (Complexity.decode α (Memory.getms m src✝))) ∘
        fm)
      ?h₁.a

case 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
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✝¹
⊢ (subroutineTimeCost
                (_ :
                  TracedProgram.sound' f size (toTracedProgram next✝)
                    ((flip Option.bind fun m =>
                        Option.map (Memory.setms m dst✝ ∘ Complexity.encode ∘ f)
                          (Complexity.decode α (Memory.getms m src✝))) ∘
                      fm)) +
              recurseTimeCost hf
                (_ :
                  TracedProgram.sound' f size (toTracedProgram next✝)
                    ((flip Option.bind fun m =>
                        Option.map (Memory.setms m dst✝ ∘ Complexity.encode ∘ f)
                          (Complexity.decode α (Memory.getms m src✝))) ∘
                      fm)) +
            localTimeCost
              (_ :
                TracedProgram.sound' f size (toTracedProgram next✝)
                  ((flip Option.bind fun m =>
                      Option.map (Memory.setms m dst✝ ∘ Complexity.encode ∘ f)
                        (Complexity.decode α (Memory.getms m src✝))) ∘
                    fm)))
          ?h₁.a +
        Stack.timeCost
          (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 }
            [])
          (_ :
            Program.haltsOn (TracedProgram.toProgram (toTracedProgram fcp))
              (Complexity.encode
                (Option.get (Complexity.decode α (Memory.getms x✝ src✝))
                  (_ : Option.isSome (Complexity.decode α (Memory.getms x✝ src✝)) = true)))) +
      1 ≤
    (subroutineTimeCost h + recurseTimeCost hf h + localTimeCost h) x✝¹
Tactic:
apply Option.mem_bind_of_mem hm
Proof state after:
case 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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ fm x✝¹
⊢ Memory.setms x✝ dst✝
      (Complexity.encode
        (f
          (Option.get (Complexity.decode α (Memory.getms x✝ src✝))
            (_ : Option.isSome (Complexity.decode α (Memory.getms x✝ src✝)) = true)))) ∈
    Option.map (Memory.setms x✝ dst✝ ∘ Complexity.encode ∘ f) (Complexity.decode α (Memory.getms x✝ src✝))

α : 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✝¹
⊢ (subroutineTimeCost
                (_ :
                  TracedProgram.sound' f size (toTracedProgram next✝)
                    ((flip Option.bind fun m =>
                        Option.map (Memory.setms m dst✝ ∘ Complexity.encode ∘ f)
                          (Complexity.decode α (Memory.getms m src✝))) ∘
                      fm)) +
              recurseTimeCost hf
                (_ :
                  TracedProgram.sound' f size (toTracedProgram next✝)
                    ((flip Option.bind fun m =>
                        Option.map (Memory.setms m dst✝ ∘ Complexity.encode ∘ f)
                          (Complexity.decode α (Memory.getms m src✝))) ∘
                      fm)) +
            localTimeCost
              (_ :
                TracedProgram.sound' f size (toTracedProgram next✝)
                  ((flip Option.bind fun m =>
                      Option.map (Memory.setms m dst✝ ∘ Complexity.encode ∘ f)
                        (Complexity.decode α (Memory.getms m src✝))) ∘
                    fm)))
          x✝¹ +
        Stack.timeCost
          (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 }
            [])
          (_ :
            Program.haltsOn (TracedProgram.toProgram (toTracedProgram fcp))
              (Complexity.encode
                (Option.get (Complexity.decode α (Memory.getms x✝ src✝))
                  (_ : Option.isSome (Complexity.decode α (Memory.getms x✝ src✝)) = true)))) +
      1 ≤
    (subroutineTimeCost h + recurseTimeCost hf h + localTimeCost h) x✝¹