include "emulator/status/status.ma".
include "common/option_lemmas.ma".
include "common/prod_lemmas.ma".
-include "emulator/opcodes/opcode_lemmas.ma".
+include "emulator/opcodes/pseudo_lemmas.ma".
(* *********************************** *)
(* STATUS INTERNO DEL PROCESSORE (ALU) *)
##[ ##1: napply symmetric_eqw16
##| ##2: napply symmetric_eqb8
##| ##3: napply (symmetric_eqim m)
- ##| ##4: napply (symmetric_eqop m)
+ ##| ##4: napply (symmetric_eqpseudo m)
##| ##5: napply symmetric_eqb8
##]
nqed.
##[ ##1: napply eqw16_to_eq
##| ##2: napply eqb8_to_eq
##| ##3: napply (eqim_to_eq m)
- ##| ##4: napply (eqop_to_eq m)
+ ##| ##4: napply (eqpseudo_to_eq m)
##| ##5: napply eqb8_to_eq
##]
nqed.
##[ ##1: napply eq_to_eqw16
##| ##2: napply eq_to_eqb8
##| ##3: napply (eq_to_eqim m)
- ##| ##4: napply (eq_to_eqop m)
+ ##| ##4: napply (eq_to_eqpseudo m)
##| ##5: napply eq_to_eqb8
##]
nqed.
##[ ##1: napply neqw16_to_neq
##| ##2: napply neqb8_to_neq
##| ##3: napply (neqim_to_neq m)
- ##| ##4: napply (neqop_to_neq m)
+ ##| ##4: napply (neqpseudo_to_neq m)
##| ##5: napply neqb8_to_neq
##]
nqed.
##[ ##1: napply neq_to_neqw16
##| ##2: napply neq_to_neqb8
##| ##3: napply (neq_to_neqim m)
- ##| ##4: napply (neq_to_neqop m)
+ ##| ##4: napply (neq_to_neqpseudo m)
##| ##5: napply neq_to_neqb8
##| ##6: napply decidable_w16
##| ##7: napply decidable_b8
##| ##8: napply (decidable_im m)
- ##| ##9: napply (decidable_op m)
+ ##| ##9: napply (decidable_pseudo m)
##| ##10: napply decidable_b8
##]
nqed.
##[ ##1: napply decidable_w16
##| ##2: napply decidable_b8
##| ##3: napply (decidable_im m)
- ##| ##4: napply (decidable_op m)
+ ##| ##4: napply (decidable_pseudo m)
##| ##5: napply decidable_b8
##]
nqed.