Theorem: HMem.Trace.CostedProgram.splitTimeCost (HMem/Trace/Cost.lean)

State before:
case h₁.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✝¹
⊢ (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)))
        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)))) =
    ?b

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✝¹
⊢ ?b ≤ (subroutineTimeCost h + recurseTimeCost hf h) x✝¹

case 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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ fm x✝¹
⊢ ℕ
Tactic:
apply Nat.add_assoc _ _ _
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✝¹
⊢ 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))
        x✝¹ +
      (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))
          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))))) ≤
    (subroutineTimeCost h + recurseTimeCost hf h) x✝¹

State before:
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✝¹
⊢ 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))
        x✝¹ +
      (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))
          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))))) ≤
    (subroutineTimeCost h + recurseTimeCost hf h) x✝¹
Tactic:
apply add_le_add (le_refl _)
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✝¹
⊢ 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))
        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)))) ≤
    recurseTimeCost hf h x✝¹

State before:
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✝¹
⊢ 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))
        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)))) ≤
    recurseTimeCost hf h x✝¹
Tactic:
apply add_le_add (le_refl _)
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.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)))) ≤
    Complexity.CostFunction.flatMap (TracedProgram.sound'_recurse_arg h)
      (fun arg =>
        Program.timeCost (TracedProgram.toProgram (toTracedProgram fcp))
          (_ : Program.haltsOn (TracedProgram.toProgram (toTracedProgram fcp)) (Complexity.encode arg)))
      x✝¹

State before:
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.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)))) ≤
    Complexity.CostFunction.flatMap (TracedProgram.sound'_recurse_arg h)
      (fun arg =>
        Program.timeCost (TracedProgram.toProgram (toTracedProgram fcp))
          (_ : Program.haltsOn (TracedProgram.toProgram (toTracedProgram fcp)) (Complexity.encode arg)))
      x✝¹
Tactic:
apply le_of_le_of_eq _
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✝¹
⊢ ?m.183728 =
    Complexity.CostFunction.flatMap (TracedProgram.sound'_recurse_arg h)
      (fun arg =>
        Program.timeCost (TracedProgram.toProgram (toTracedProgram fcp))
          (_ : Program.haltsOn (TracedProgram.toProgram (toTracedProgram fcp)) (Complexity.encode arg)))
      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✝¹
⊢ 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)))) ≤
    ?m.183728

State before:
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✝¹
⊢ ?m.183728 =
    Complexity.CostFunction.flatMap (TracedProgram.sound'_recurse_arg h)
      (fun arg =>
        Program.timeCost (TracedProgram.toProgram (toTracedProgram fcp))
          (_ : Program.haltsOn (TracedProgram.toProgram (toTracedProgram fcp)) (Complexity.encode arg)))
      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✝¹
⊢ 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)))) ≤
    ?m.183728
Tactic:
apply Eq.symm
State after:
case h₂.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✝¹
⊢ Complexity.CostFunction.flatMap (TracedProgram.sound'_recurse_arg h)
      (fun arg =>
        Program.timeCost (TracedProgram.toProgram (toTracedProgram fcp))
          (_ : Program.haltsOn (TracedProgram.toProgram (toTracedProgram fcp)) (Complexity.encode arg)))
      x✝¹ =
    ?m.183728

α : 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✝¹
⊢ 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)))) ≤
    ?m.183728

State before:
case h₂.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✝¹
⊢ Complexity.CostFunction.flatMap (TracedProgram.sound'_recurse_arg h)
      (fun arg =>
        Program.timeCost (TracedProgram.toProgram (toTracedProgram fcp))
          (_ : Program.haltsOn (TracedProgram.toProgram (toTracedProgram fcp)) (Complexity.encode arg)))
      x✝¹ =
    ?m.183728

α : 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✝¹
⊢ 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)))) ≤
    ?m.183728
Tactic:
apply Complexity.CostFunction.flatMap_some
State after:
case h₂.h.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✝¹
⊢ TracedProgram.sound'_recurse_arg h x✝¹ = some ?h₂.h.b

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
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✝¹
⊢ 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)))) ≤
    Program.timeCost (TracedProgram.toProgram (toTracedProgram fcp))
      (_ : Program.haltsOn (TracedProgram.toProgram (toTracedProgram fcp)) (Complexity.encode ?h₂.h.b))

State before:
case h₂.h.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✝¹
⊢ TracedProgram.sound'_recurse_arg h x✝¹ = some ?h₂.h.b

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
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✝¹
⊢ 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)))) ≤
    Program.timeCost (TracedProgram.toProgram (toTracedProgram fcp))
      (_ : Program.haltsOn (TracedProgram.toProgram (toTracedProgram fcp)) (Complexity.encode ?h₂.h.b))
Tactic:
apply Option.mem_bind_of_mem
State after:
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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ fm x✝¹
⊢ ?h₂.h.h.a ∈ fm x✝¹

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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ fm x✝¹
⊢ ?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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ fm x✝¹
⊢ 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
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✝¹
⊢ 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)))) ≤
    Program.timeCost (TracedProgram.toProgram (toTracedProgram fcp))
      (_ : Program.haltsOn (TracedProgram.toProgram (toTracedProgram fcp)) (Complexity.encode ?h₂.h.b))

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

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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ fm x✝¹
⊢ ?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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ fm x✝¹
⊢ 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
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✝¹
⊢ 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)))) ≤
    Program.timeCost (TracedProgram.toProgram (toTracedProgram fcp))
      (_ : Program.haltsOn (TracedProgram.toProgram (toTracedProgram fcp)) (Complexity.encode ?h₂.h.b))
Tactic:
apply hm
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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ fm x✝¹
⊢ ?h₂.h.b ∈ (Complexity.decode α ∘ flip Memory.getms src✝) x✝

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
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✝¹
⊢ 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)))) ≤
    Program.timeCost (TracedProgram.toProgram (toTracedProgram fcp))
      (_ : Program.haltsOn (TracedProgram.toProgram (toTracedProgram fcp)) (Complexity.encode ?h₂.h.b))

State before:
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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ fm x✝¹
⊢ ?h₂.h.b ∈ (Complexity.decode α ∘ flip Memory.getms src✝) x✝

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
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✝¹
⊢ 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)))) ≤
    Program.timeCost (TracedProgram.toProgram (toTracedProgram fcp))
      (_ : Program.haltsOn (TracedProgram.toProgram (toTracedProgram fcp)) (Complexity.encode ?h₂.h.b))
Tactic:
apply Option.get_mem
State after:
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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ fm x✝¹
⊢ Option.isSome ((Complexity.decode α ∘ flip Memory.getms src✝) x✝) = 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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ 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)))) ≤
    Program.timeCost (TracedProgram.toProgram (toTracedProgram fcp))
      (_ :
        Program.haltsOn (TracedProgram.toProgram (toTracedProgram fcp))
          (Complexity.encode (Option.get ((Complexity.decode α ∘ flip Memory.getms src✝) x✝) ?h₂.h.h.hf.h)))

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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ fm x✝¹
⊢ Option.isSome ((Complexity.decode α ∘ flip Memory.getms src✝) x✝) = 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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ 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)))) ≤
    Program.timeCost (TracedProgram.toProgram (toTracedProgram fcp))
      (_ :
        Program.haltsOn (TracedProgram.toProgram (toTracedProgram fcp))
          (Complexity.encode (Option.get ((Complexity.decode α ∘ flip Memory.getms src✝) x✝) ?h₂.h.h.hf.h)))
Tactic:
apply (h.left _ _ hm).elim λ hsome _ ↦ hsome
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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ 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)))) ≤
    Program.timeCost (TracedProgram.toProgram (toTracedProgram fcp))
      (_ :
        Program.haltsOn (TracedProgram.toProgram (toTracedProgram fcp))
          (Complexity.encode
            (Option.get ((Complexity.decode α ∘ flip Memory.getms src✝) x✝)
              (_ : Option.isSome (Complexity.decode α (Memory.getms x✝ src✝)) = true))))

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
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ 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)))) ≤
    Program.timeCost (TracedProgram.toProgram (toTracedProgram fcp))
      (_ :
        Program.haltsOn (TracedProgram.toProgram (toTracedProgram fcp))
          (Complexity.encode
            (Option.get ((Complexity.decode α ∘ flip Memory.getms src✝) x✝)
              (_ : Option.isSome (Complexity.decode α (Memory.getms x✝ src✝)) = true))))
Tactic:
apply le_refl
State after:
no goals