λm:mcu_type.λt:memory_impl.λs:any_status m t.λw:word16.
get_pc_reg m t (set_pc_reg m t s (succ_w16 w)).
-let rec filtered_plus_w16 (m:mcu_type) (t:memory_impl) (s:any_status m t) (w:word16) (n:nat) on n ≝
+definition filtered_plus_w16 := \lambda m:mcu_type.
+let rec filtered_plus_w16 (t:memory_impl) (s:any_status m t) (w:word16) (n:nat) on n ≝
match n with
[ O ⇒ w
- | S n' ⇒ filtered_plus_w16 m t s (filtered_inc_w16 m t s w) n' ].
+ | S n' ⇒ filtered_plus_w16 t s (filtered_inc_w16 m t s w) n' ]
+in filtered_plus_w16.
(*
errore1: non esiste traduzione ILL_OP