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

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