λm:mcu_type.λt:memory_impl.λs1,s2:any_status m t.λaddrl:list word16.
match s1 with [ mk_any_status alu1 mem1 chk1 clk1 ⇒
match s2 with [ mk_any_status alu2 mem2 chk2 clk2 ⇒
λm:mcu_type.λt:memory_impl.λs1,s2:any_status m t.λaddrl:list word16.
match s1 with [ mk_any_status alu1 mem1 chk1 clk1 ⇒
match s2 with [ mk_any_status alu2 mem2 chk2 clk2 ⇒