(l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
match l with
[ nil ⇒ c
| cons hd tl ⇒ match thd4T … hd with
[ Byte _ ⇒ get_word_count m b c tl
| Word w ⇒ match eq_w16 〈〈x9,xE〉:b〉 w with
(l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
match l with
[ nil ⇒ c
| cons hd tl ⇒ match thd4T … hd with
[ Byte _ ⇒ get_word_count m b c tl
| Word w ⇒ match eq_w16 〈〈x9,xE〉:b〉 w with