Theorem: HMem.Trace.TracedProgram.sound_subroutine_next (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✝
h : sound f size a next (Memory.setms m dst (Complexity.encode (fs x✝)))
⊢ sound f size a next
    (Memory.setms m dst
      (Complexity.encode
        (fs
          (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