Stream: Beginner Questions

Topic: ✔ trace decomposition

view this post on Zulip sadra (Jun 12 2026 at 04:35):

Okay nevermind. Just need to strengthen the inductive hypothesis to allow for further frames on the stack
lemma split_trace_call:
assumes ‹prg ⊢ x →* y›
assumes ‹fst x = cstk›
assumes ‹fst y = g @ f # cstk›
shows ‹∃ x' y'.
prg ⊢ x →* x' ∧
prg ⊢ x' → y' ∧
prg ⊢ y' →* y ∧
fst x' = cstk ∧
fst y' = f # cstk›

view this post on Zulip Notification Bot (Jun 12 2026 at 04:35):

sadra has marked this topic as resolved.

Last updated: Jun 26 2026 at 21:20 UTC