- (λtmps.opt_map ?? (memory_filter_write m t s (succ_w16 addr) (w16l writew))
- (λtmps'.Some ? (pair ?? tmps' (filtered_plus_w16 m t s cur_pc fetched)))).
+ (λtmps1.opt_map ?? (memory_filter_write m t tmps1 (succ_w16 addr) (w16l writew))
+ (λtmps2.Some ? (pair ?? tmps2 (filtered_plus_w16 m t tmps2 cur_pc fetched)))).