interpretation "mk_alu_HC08" 'mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl =
(mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl).
+(* ****** *)
+(* SETTER *)
+(* ****** *)
+
+(* setter specifico HC08/HCS08 di A *)
+ndefinition set_acc_8_low_reg_HC08 ≝
+λalu.λacclow':byte8.
+ mk_alu_HC08
+ acclow'
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
+
+(* setter specifico HC08/HCS08 di X *)
+ndefinition set_indX_8_low_reg_HC08 ≝
+λalu.λindxlow':byte8.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ indxlow'
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
+
+(* setter specifico HC08/HCS08 di H *)
+ndefinition set_indX_8_high_reg_HC08 ≝
+λalu.λindxhigh':byte8.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ indxhigh'
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
+
+(* setter specifico HC08/HCS08 di H:X *)
+ndefinition set_indX_16_reg_HC08 ≝
+λalu.λindx16:word16.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (cnL ? indx16)
+ (cnH ? indx16)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
+
+(* setter specifico HC08/HCS08 di SP *)
+ndefinition set_sp_reg_HC08 ≝
+λalu.λsp':word16.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ sp'
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
+
+(* setter specifico HC08/HCS08 di PC *)
+ndefinition set_pc_reg_HC08 ≝
+λalu.λpc':word16.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ pc'
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
+
+(* setter specifico HC08/HCS08 di V *)
+ndefinition set_v_flag_HC08 ≝
+λalu.λvfl':bool.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ vfl'
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
+
+(* setter specifico HC08/HCS08 di H *)
+ndefinition set_h_flag_HC08 ≝
+λalu.λhfl':bool.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ hfl'
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
+
+(* setter specifico HC08/HCS08 di I *)
+ndefinition set_i_flag_HC08 ≝
+λalu.λifl':bool.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ ifl'
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
+
+(* setter specifico HC08/HCS08 di N *)
+ndefinition set_n_flag_HC08 ≝
+λalu.λnfl':bool.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ nfl'
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
+
+(* setter specifico HC08/HCS08 di Z *)
+ndefinition set_z_flag_HC08 ≝
+λalu.λzfl':bool.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ zfl'
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
+
+(* setter specifico HC08/HCS08 di C *)
+ndefinition set_c_flag_HC08 ≝
+λalu.λcfl':bool.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ cfl'
+ (irq_flag_HC08 alu).
+
+(* setter specifico HC08/HCS08 di IRQ *)
+ndefinition set_irq_flag_HC08 ≝
+λalu.λirqfl':bool.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ irqfl'.
+
(* ***************** *)
(* CONFRONTO FRA ALU *)
(* ***************** *)