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

State before:
α : Type u_2
inst✝¹ : Complexity.Coding α Memory
β : Type u_3
inst✝ : Complexity.Encoding β Memory
f : α → β
γ : Type ?u.40501
δ : 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✝
left✝ : size x✝ < size a
h : sound f size a next (Memory.setms m dst (Complexity.encode (f x✝)))
⊢ sound f size a next
    (Memory.setms m dst
      (Complexity.encode
        (f
          (Option.get (Complexity.decode α (Memory.getms m src))
            (_ : Option.isSome (Complexity.decode α (Memory.getms m src)) = true)))))
Tactic:
simpa only [hm, Complexity.decode_inv, Option.get_some] using h
State after:
no goals