(forall_memory_ranged t chk1 chk2 mem1 mem2 tl)
].
-ndefinition eq_clk ≝
-λm:mcu_type.λc1,c2:option (aux_clk_type m).
- match c1 with
- [ None ⇒ match c2 with
- [ None ⇒ true | Some _ ⇒ false ]
- | Some c1' ⇒ match c2 with
- [ None ⇒ false | Some c2' ⇒ (eq_b8 (fst5T … c1') (fst5T … c2')) ⊗
- (eq_op m (snd5T … c1') (snd5T … c2')) ⊗
- (eq_im m (thd5T … c1') (thd5T … c2')) ⊗
- (eq_b8 (fth5T … c1') (fth5T … c2')) ⊗
- (eq_w16 (fft5T … c1') (fft5T … c2')) ]
- ].
+ndefinition eq_clk ≝ λm.eq_option … (eq_quintuple … eq_b8 (eq_op m) (eq_im m) eq_b8 eq_w16).
(* generalizzazione del confronto fra stati *)
ndefinition eq_anystatus ≝