Theorem: HMem.Trace.TracedProgram.sound_recurse_size (HMem/Trace/Sound.lean)

State before:
α : Type u_2
inst✝¹ : Complexity.Coding α Memory
β : Type u_3
inst✝ : Complexity.Encoding β Memory
f : α → β
γ : Type ?u.39174
δ : Type
enγ : Complexity.Coding γ Memory
enδ : Complexity.Encoding δ Memory
fs : γ → δ
hc : Complexity.Computable Encoding.Model fs
size : α → ℕ
a : α
dst src : Source
next : TracedProgram
m : Memory
h : sound f size a (recurse dst src next) m
x✝ : α
hm : Memory.getms m src = Complexity.encode x✝
hs : size x✝ < size a
right✝ : sound f size a next (Memory.setms m dst (Complexity.encode (f x✝)))
⊢ size
      (Option.get (Complexity.decode α (Memory.getms m src))
        (_ : Option.isSome (Complexity.decode α (Memory.getms m src)) = true)) <
    size a
Tactic:
simpa only [hm, Complexity.decode_inv, Option.get_some] using hs
State after:
no goals