X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fmultivm.ma;h=44dacea60f6f3cfb90d03faa3098019d71f2114e;hb=dc7e826399162e2fde3ddf1f02d5530d6cd11205;hp=fc374d9ab6e6d8530045268548d169b89a3b6dbf;hpb=0f99c7691f8a418003acea3f7856102c21dcab8d;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma b/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma
index fc374d9ab..44dacea60 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma
@@ -15,13 +15,12 @@
 (* ********************************************************************** *)
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
-(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
 include "freescale/load_write.ma".
-include "freescale/nat_lemmas.ma".
 
 (* ************************************************ *)
 (* LOGICHE AUSILIARE CHE ACCOMUNANO PIU' OPERAZIONI *)
@@ -42,7 +41,7 @@ include "freescale/nat_lemmas.ma".
 ndefinition execute_ADC_ADD_aux ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
 λfAMC:byte8 → byte8 → bool → ProdT byte8 bool.
- opt_map ?? (multi_mode_load true m t s cur_pc i)
+ opt_map … (multi_mode_load true m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ triple s_tmp1 M_op new_pc ⇒
     let A_op ≝ get_acc_8_low_reg m t s_tmp1 in
@@ -63,7 +62,7 @@ ndefinition execute_ADC_ADD_aux ≝
       (* V = A7&M7&nR7 | nA7&nM7&R7 *)
       let s_tmp7 ≝ setweak_v_flag m t s_tmp6 ((A7⊗M7⊗(⊖R7)) ⊕ ((⊖A7)⊗(⊖M7)⊗R7)) in
       (* newpc = nextpc *)
-      Some ? (pair ?? s_tmp7 new_pc) ]]).
+      Some ? (pair … s_tmp7 new_pc) ]]).
 
 (* A = [true] fAM(A,M), [false] A *)
 (* cioe' in caso di false l'operazione viene eseguita ma modifica solo i flag *)
@@ -71,7 +70,7 @@ ndefinition execute_ADC_ADD_aux ≝
 ndefinition execute_AND_BIT_EOR_ORA_aux ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
 λfAM:byte8 → byte8 → byte8.
- opt_map ?? (multi_mode_load true m t s cur_pc i)
+ opt_map … (multi_mode_load true m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ triple s_tmp1 M_op new_pc ⇒
     let R_op ≝ fAM (get_acc_8_low_reg m t s_tmp1) M_op in
@@ -84,19 +83,19 @@ ndefinition execute_AND_BIT_EOR_ORA_aux ≝
     (* V = 0 *) 
     let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
     (* newpc = nextpc *)
-    Some ? (pair ?? s_tmp5 new_pc) ]).
+    Some ? (pair … s_tmp5 new_pc) ]).
 
 (* M = fMC(M,C) *)
 (* fMC e' la logica da applicare: rc_/ro_/sh_ *)
 ndefinition execute_ASL_ASR_LSR_ROL_ROR_aux ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
 λfMC:byte8 → bool → ProdT byte8 bool.
- opt_map ?? (multi_mode_load true m t s cur_pc i)
+ opt_map … (multi_mode_load true m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ triple s_tmp1 M_op _ ⇒
     match fMC M_op (get_c_flag m t s_tmp1) with [ pair R_op carry ⇒
     (* M = fMC(M,C) *)
-    opt_map ?? (multi_mode_write true m t s_tmp1 cur_pc i R_op)
+    opt_map … (multi_mode_write true m t s_tmp1 cur_pc i R_op)
      (λS_PC.match S_PC with
       [ pair s_tmp2 new_pc ⇒
       (* C = carry *)
@@ -108,7 +107,7 @@ ndefinition execute_ASL_ASR_LSR_ROL_ROR_aux ≝
       (* V = R7 ⊙ carry *)
       let s_tmp6 ≝ setweak_v_flag m t s_tmp5 ((MSB_b8 R_op) ⊙ carry) in
       (* newpc = nextpc *)
-      Some ? (pair ?? s_tmp6 new_pc) ])]]).
+      Some ? (pair … s_tmp6 new_pc) ])]]).
 
 (* estensione del segno byte → word *)
 ndefinition byte_extension ≝
@@ -123,52 +122,52 @@ ndefinition branched_pc ≝
 (* tutti i branch calcoleranno la condizione e la passeranno qui *)
 ndefinition execute_any_BRANCH ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λfCOND:bool.
- opt_map ?? (multi_mode_load true m t s cur_pc i)
+ opt_map … (multi_mode_load true m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ triple s_tmp1 M_op new_pc ⇒
     (* if true, branch *) 
     match fCOND with
      (* newpc = nextpc + rel *)
-     [ true ⇒ Some ? (pair ?? s_tmp1 (branched_pc m t s_tmp1 new_pc M_op))
+     [ true ⇒ Some ? (pair … s_tmp1 (branched_pc m t s_tmp1 new_pc M_op))
      (* newpc = nextpc *)
-     | false ⇒ Some ? (pair ?? s_tmp1 new_pc) ]]).
+     | false ⇒ Some ? (pair … s_tmp1 new_pc) ]]).
 
 (* Mn = filtered optval *) 
 (* il chiamante passa 0x00 per azzerare, 0xFF per impostare il bit di M *)
 ndefinition execute_BCLRn_BSETn_aux ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λoptval:byte8.
  (* Mn = filtered optval *)
- opt_map ?? (multi_mode_write true m t s cur_pc i optval)
+ opt_map … (multi_mode_write true m t s cur_pc i optval)
   (λS_PC.match S_PC with
    (* newpc = nextpc *)
-   [ pair s_tmp1 new_pc ⇒ Some ? (pair ?? s_tmp1 new_pc) ]).
+   [ pair s_tmp1 new_pc ⇒ Some ? (pair … s_tmp1 new_pc) ]).
 
 (* if COND(Mn) branch *)
 (* il chiamante passa la logica da testare (0x00,¬0x00) e poi si salta *)
 ndefinition execute_BRCLRn_BRSETn_aux ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λfCOND:byte8 → bool.
- opt_map ?? (multi_mode_load false m t s cur_pc i)
+ opt_map … (multi_mode_load false m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ triple s_tmp1 M_op new_pc ⇒ match M_op with
     [ mk_word16 MH_op ML_op ⇒
      (* if COND(Mn) branch *)
      match fCOND MH_op with
       (* newpc = nextpc + rel *)
-      [ true ⇒ Some ? (pair ?? s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
+      [ true ⇒ Some ? (pair … s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
       (* newpc = nextpc *)
-      | false ⇒ Some ? (pair ?? s_tmp1 new_pc) ]]]).
+      | false ⇒ Some ? (pair … s_tmp1 new_pc) ]]]).
 
 (* M = fM(M) *)
 (* fM e' la logica da applicare: not/neg/++/-- *)
 ndefinition execute_COM_DEC_INC_NEG_aux ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
 λfM:byte8 → byte8.λfV:bool → bool → bool.λfC:bool → byte8 → bool.
- opt_map ?? (multi_mode_load true m t s cur_pc i)
+ opt_map … (multi_mode_load true m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ triple s_tmp1 M_op _ ⇒
     let R_op ≝ fM M_op in
     (* M = fM(M) *)
-    opt_map ?? (multi_mode_write true m t s_tmp1 cur_pc i R_op)
+    opt_map … (multi_mode_write true m t s_tmp1 cur_pc i R_op)
      (λS_PC.match S_PC with
       [ pair s_tmp2 new_pc ⇒
       (* C = fCR (C,R) *)
@@ -180,7 +179,7 @@ ndefinition execute_COM_DEC_INC_NEG_aux ≝
       (* V = fV (M7,R7) *)
       let s_tmp6 ≝ setweak_v_flag m t s_tmp5 (fV (MSB_b8 M_op) (MSB_b8 R_op)) in
       (* newpc = nextpc *)
-      Some ? (pair ?? s_tmp6 new_pc) ])]).
+      Some ? (pair … s_tmp6 new_pc) ])]).
 
 (* A = [true] fAMC(A,M,C), [false] A *)
 (* cioe' in caso di false l'operazione viene eseguita ma modifica solo i flag *)
@@ -188,7 +187,7 @@ ndefinition execute_COM_DEC_INC_NEG_aux ≝
 ndefinition execute_SBC_SUB_aux ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
 λfAMC:byte8 → byte8 → bool → ProdT byte8 bool.
- opt_map ?? (multi_mode_load true m t s cur_pc i)
+ opt_map … (multi_mode_load true m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ triple s_tmp1 M_op new_pc ⇒
     let A_op ≝ get_acc_8_low_reg m t s_tmp1 in
@@ -206,29 +205,29 @@ ndefinition execute_SBC_SUB_aux ≝
       (* V = A7&nM7&nR7 | nA7&M7&R7 *)
       let s_tmp6 ≝ setweak_v_flag m t s_tmp5 ((A7⊗(⊖M7)⊗(⊖R7)) ⊕ ((⊖A7)⊗M7⊗R7)) in
       (* newpc = nextpc *)
-      Some ? (pair ?? s_tmp6 new_pc) ]]).
+      Some ? (pair … s_tmp6 new_pc) ]]).
 
 (* il classico push *)
 ndefinition aux_push ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval:byte8.
- opt_map ?? (get_sp_reg m t s)
+ opt_map … (get_sp_reg m t s)
   (* [SP] = val *)
-  (λSP_op.opt_map ?? (memory_filter_write m t s SP_op val)
+  (λSP_op.opt_map … (memory_filter_write m t s SP_op val)
    (* SP -- *)
-   (λs_tmp1.opt_map ?? (set_sp_reg m t s_tmp1 (pred_w16 SP_op))
+   (λs_tmp1.opt_map … (set_sp_reg m t s_tmp1 (pred_w16 SP_op))
     (λs_tmp2.Some ? s_tmp2))).
 
 (* il classico pop *)
 (* NB: l'incremento di SP deve essere filtrato dalla ALU, quindi get(set(SP)) *)
 ndefinition aux_pop ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.
- opt_map ?? (get_sp_reg m t s)
+ opt_map … (get_sp_reg m t s)
   (* SP ++ *)
-  (λSP_op.opt_map ?? (set_sp_reg m t s (succ_w16 SP_op))
-   (λs_tmp1.opt_map ?? (get_sp_reg m t s_tmp1)
+  (λSP_op.opt_map … (set_sp_reg m t s (succ_w16 SP_op))
+   (λs_tmp1.opt_map … (get_sp_reg m t s_tmp1)
     (* val = [SP] *)
-    (λSP_op'.opt_map ?? (memory_filter_read m t s_tmp1 SP_op')
-     (λval.Some ? (pair ?? s_tmp1 val))))).
+    (λSP_op'.opt_map … (memory_filter_read m t s_tmp1 SP_op')
+     (λval.Some ? (pair … s_tmp1 val))))).
 
 (* CCR corrisponde a V11HINZC e cmq 1 se un flag non esiste *)
 (* i flag mantengono posizione costante nelle varie ALU, e se non sono
@@ -279,24 +278,24 @@ ndefinition execute_ADD ≝
 (* SP += extended M *)
 ndefinition execute_AIS ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load true m t s cur_pc i)
+ opt_map … (multi_mode_load true m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ triple s_tmp1 M_op new_pc ⇒
-   opt_map ?? (get_sp_reg m t s_tmp1)
+   opt_map … (get_sp_reg m t s_tmp1)
     (* SP += extended M *)
-    (λSP_op.opt_map ?? (set_sp_reg m t s_tmp1 (plus_w16_d_d SP_op (byte_extension M_op)))
-     (λs_tmp2.Some ? (pair ?? s_tmp2 new_pc))) ]).
+    (λSP_op.opt_map … (set_sp_reg m t s_tmp1 (plus_w16_d_d SP_op (byte_extension M_op)))
+     (λs_tmp2.Some ? (pair … s_tmp2 new_pc))) ]).
 
 (* H:X += extended M *)
 ndefinition execute_AIX ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load true m t s cur_pc i)
+ opt_map … (multi_mode_load true m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ triple s_tmp1 M_op new_pc ⇒
-   opt_map ?? (get_indX_16_reg m t s_tmp1)
+   opt_map … (get_indX_16_reg m t s_tmp1)
     (* H:X += extended M *)
-    (λHX_op.opt_map ?? (set_indX_16_reg m t s_tmp1 (plus_w16_d_d HX_op (byte_extension M_op)))
-     (λs_tmp2.Some ? (pair ?? s_tmp2 new_pc))) ]).
+    (λHX_op.opt_map … (set_indX_16_reg m t s_tmp1 (plus_w16_d_d HX_op (byte_extension M_op)))
+     (λs_tmp2.Some ? (pair … s_tmp2 new_pc))) ]).
 
 (* A = A & M *)
 ndefinition execute_AND ≝
@@ -336,32 +335,32 @@ ndefinition execute_BEQ ≝
 (* if N⊙V=0, branch *)
 ndefinition execute_BGE ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_n_flag m t s)
-  (λN_op.opt_map ?? (get_v_flag m t s)
+ opt_map … (get_n_flag m t s)
+  (λN_op.opt_map … (get_v_flag m t s)
    (λV_op.execute_any_BRANCH m t s i cur_pc (⊖(N_op ⊙ V_op)))).
 
 (* BGND mode *)
 ndefinition execute_BGND ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pair ?? s cur_pc).
+ Some ? (pair … s cur_pc).
 
 (* if Z|N⊙V=0, branch *)
 ndefinition execute_BGT ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_n_flag m t s)
-  (λN_op.opt_map ?? (get_v_flag m t s)
+ opt_map … (get_n_flag m t s)
+  (λN_op.opt_map … (get_v_flag m t s)
    (λV_op.execute_any_BRANCH m t s i cur_pc (⊖((get_z_flag m t s) ⊕ (N_op ⊙ V_op))))).
 
 (* if H=0, branch *)
 ndefinition execute_BHCC ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_h_flag m t s)
+ opt_map … (get_h_flag m t s)
   (λH_op.execute_any_BRANCH m t s i cur_pc (⊖H_op)).
 
 (* if H=1, branch *)
 ndefinition execute_BHCS ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_h_flag m t s)
+ opt_map … (get_h_flag m t s)
   (λH_op.execute_any_BRANCH m t s i cur_pc H_op).
 
 (* if C|Z=0, branch *)
@@ -372,13 +371,13 @@ ndefinition execute_BHI ≝
 (* if nIRQ=1, branch NB: irqflag e' un negato del pin *)
 ndefinition execute_BIH ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_irq_flag m t s)
+ opt_map … (get_irq_flag m t s)
   (λIRQ_op.execute_any_BRANCH m t s i cur_pc (⊖IRQ_op)).
 
 (* if nIRQ=0, branch NB: irqflag e' un negato del pin *)
 ndefinition execute_BIL ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_irq_flag m t s)
+ opt_map … (get_irq_flag m t s)
   (λIRQ_op.execute_any_BRANCH m t s i cur_pc IRQ_op).
 
 (* flags = A & M *)
@@ -389,8 +388,8 @@ ndefinition execute_BIT ≝
 (* if Z|N⊙V=1, branch *)
 ndefinition execute_BLE ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_n_flag m t s)
-  (λN_op.opt_map ?? (get_v_flag m t s)
+ opt_map … (get_n_flag m t s)
+  (λN_op.opt_map … (get_v_flag m t s)
    (λV_op.execute_any_BRANCH m t s i cur_pc ((get_z_flag m t s) ⊕ (N_op ⊙ V_op)))).
 
 (* if C|Z=1, branch *)
@@ -401,26 +400,26 @@ ndefinition execute_BLS ≝
 (* if N⊙V=1, branch *)
 ndefinition execute_BLT ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_n_flag m t s)
-  (λN_op.opt_map ?? (get_v_flag m t s)
+ opt_map … (get_n_flag m t s)
+  (λN_op.opt_map … (get_v_flag m t s)
    (λV_op.execute_any_BRANCH m t s i cur_pc (N_op ⊙ V_op))).
 
 (* if I=0, branch *)
 ndefinition execute_BMC ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_i_flag m t s)
+ opt_map … (get_i_flag m t s)
   (λI_op.execute_any_BRANCH m t s i cur_pc (⊖I_op)).
 
 (* if N=1, branch *)
 ndefinition execute_BMI ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_n_flag m t s)
+ opt_map … (get_n_flag m t s)
   (λN_op.execute_any_BRANCH m t s i cur_pc N_op).
 
 (* if I=1, branch *)
 ndefinition execute_BMS ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_i_flag m t s)
+ opt_map … (get_i_flag m t s)
   (λI_op.execute_any_BRANCH m t s i cur_pc I_op).
 
 (* if Z=0, branch *)
@@ -431,7 +430,7 @@ ndefinition execute_BNE ≝
 (* if N=0, branch *)
 ndefinition execute_BPL ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_n_flag m t s)
+ opt_map … (get_n_flag m t s)
   (λN_op.execute_any_BRANCH m t s i cur_pc (⊖N_op)).
 
 (* branch always *)
@@ -465,28 +464,28 @@ ndefinition execute_BSETn ≝
 (* HC05/HC08/HCS08 si appoggiano allo stack, RS08 a SPC *)
 ndefinition execute_BSR ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t .λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load true m t s cur_pc i)
+ opt_map … (multi_mode_load true m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ triple s_tmp1 M_op new_pc ⇒ let aux ≝
     (* push (new_pc low) *)
-    opt_map ?? (aux_push m t s_tmp1 (w16l new_pc))
+    opt_map … (aux_push m t s_tmp1 (w16l new_pc))
      (* push (new_pc high) *)
-     (λs_tmp2.opt_map ?? (aux_push m t s_tmp2 (w16h new_pc))
+     (λs_tmp2.opt_map … (aux_push m t s_tmp2 (w16h new_pc))
       (* new_pc = new_pc + rel *)
-      (λs_tmp3.Some ? (pair ?? s_tmp3 (branched_pc m t s_tmp3 new_pc M_op))))
+      (λs_tmp3.Some ? (pair … s_tmp3 (branched_pc m t s_tmp3 new_pc M_op))))
      in match m with
     [ HC05 ⇒ aux | HC08 ⇒ aux | HCS08 ⇒ aux
     | RS08 ⇒
      (* SPC = new_pc *) 
-     opt_map ?? (set_spc_reg m t s_tmp1 new_pc)
+     opt_map … (set_spc_reg m t s_tmp1 new_pc)
       (* new_pc = new_pc + rel *)
-      (λs_tmp2.Some ? (pair ?? s_tmp2 (branched_pc m t s_tmp2 new_pc M_op)))
+      (λs_tmp2.Some ? (pair … s_tmp2 (branched_pc m t s_tmp2 new_pc M_op)))
     ]]).
 
 (* if A=M, branch *)
 ndefinition execute_CBEQA ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load false m t s cur_pc i)
+ opt_map … (multi_mode_load false m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ triple s_tmp1 M_op new_pc ⇒
     match M_op with
@@ -494,44 +493,44 @@ ndefinition execute_CBEQA ≝
       (* if A=M, branch *)
       match eq_b8 (get_acc_8_low_reg m t s_tmp1) MH_op with
        (* new_pc = new_pc + rel *)
-       [ true ⇒ Some ? (pair ?? s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
+       [ true ⇒ Some ? (pair … s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
        (* new_pc = new_pc *)
-       | false ⇒ Some ? (pair ?? s_tmp1 new_pc)
+       | false ⇒ Some ? (pair … s_tmp1 new_pc)
        ]]]).
 
 (* if X=M, branch *)
 ndefinition execute_CBEQX ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load false m t s cur_pc i)
+ opt_map … (multi_mode_load false m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ triple s_tmp1 M_op new_pc ⇒
     match M_op with
      [ mk_word16 MH_op ML_op ⇒
-      opt_map ?? (get_indX_8_low_reg m t s_tmp1)
+      opt_map … (get_indX_8_low_reg m t s_tmp1)
        (* if X=M, branch *)
        (λX_op.match eq_b8 X_op MH_op with
         (* new_pc = new_pc + rel *)
-        [ true ⇒ Some ? (pair ?? s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
+        [ true ⇒ Some ? (pair … s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
         (* new_pc = new_pc *)
-        | false ⇒ Some ? (pair ?? s_tmp1 new_pc)
+        | false ⇒ Some ? (pair … s_tmp1 new_pc)
         ])]]).
 
 (* C = 0 *)
 ndefinition execute_CLC ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pair ?? (set_c_flag m t s false) cur_pc).
+ Some ? (pair … (set_c_flag m t s false) cur_pc).
 
 (* I = 0 *)
 ndefinition execute_CLI ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (set_i_flag m t s false)
-  (λs_tmp.Some ? (pair ?? s_tmp cur_pc)).
+ opt_map … (set_i_flag m t s false)
+  (λs_tmp.Some ? (pair … s_tmp cur_pc)).
 
 (* M = 0 *)
 ndefinition execute_CLR ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
  (* M = 0 *)
- opt_map ?? (multi_mode_write true m t s cur_pc i 〈x0,x0〉)
+ opt_map … (multi_mode_write true m t s cur_pc i 〈x0,x0〉)
   (λS_PC.match S_PC with
    [ pair s_tmp1 new_pc ⇒
    (* Z = 1 *)
@@ -541,7 +540,7 @@ ndefinition execute_CLR ≝
    (* V = 0 *)
    let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
    (* newpc = nextpc *)
-   Some ? (pair ?? s_tmp4 new_pc) ]).
+   Some ? (pair … s_tmp4 new_pc) ]).
 
 (* flags = A - M *)
 ndefinition execute_CMP ≝
@@ -560,10 +559,10 @@ ndefinition execute_COM ≝
 (* flags = H:X - M *)
 ndefinition execute_CPHX ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load false m t s cur_pc i)
+ opt_map … (multi_mode_load false m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ triple s_tmp1 M_op new_pc ⇒
-    opt_map ?? (get_indX_16_reg m t s_tmp1)
+    opt_map … (get_indX_16_reg m t s_tmp1)
      (λX_op. 
       match plus_w16_dc_dc X_op (compl_w16 M_op) false with
        [ pair R_op carry ⇒
@@ -577,15 +576,15 @@ ndefinition execute_CPHX ≝
         (* V = X15&nM15&nR15 | nX15&M15&R15 *)
         let s_tmp5 ≝ setweak_v_flag m t s_tmp4 ((X15⊗(⊖M15)⊗(⊖R15)) ⊕ ((⊖X15)⊗M15⊗R15)) in
         (* newpc = nextpc *)
-        Some ? (pair ?? s_tmp5 new_pc) ] ) ]).
+        Some ? (pair … s_tmp5 new_pc) ] ) ]).
 
 (* flags = X - M *)
 ndefinition execute_CPX ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load true m t s cur_pc i)
+ opt_map … (multi_mode_load true m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ triple s_tmp1 M_op new_pc ⇒
-    opt_map ?? (get_indX_8_low_reg m t s_tmp1)
+    opt_map … (get_indX_8_low_reg m t s_tmp1)
      (λX_op. 
       match plus_b8_dc_dc X_op (compl_b8 M_op) false with
        [ pair R_op carry ⇒
@@ -599,13 +598,13 @@ ndefinition execute_CPX ≝
         (* V = X7&nM7&nR7 | nX7&M7&R7 *)
         let s_tmp5 ≝ setweak_v_flag m t s_tmp4 ((X7⊗(⊖M7)⊗(⊖R7)) ⊕ ((⊖X7)⊗M7⊗R7)) in
         (* newpc = nextpc *)
-        Some ? (pair ?? s_tmp5 new_pc) ] ) ]).
+        Some ? (pair … s_tmp5 new_pc) ] ) ]).
 
 (* decimal adjiust A *)
 (* per i dettagli vedere daa_b8 (modulo byte8) *)
 ndefinition execute_DAA ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_h_flag m t s)
+ opt_map … (get_h_flag m t s)
   (λH.
    let M_op ≝ get_acc_8_low_reg m t s in
    match daa_b8 H (get_c_flag m t s) M_op with
@@ -621,27 +620,27 @@ ndefinition execute_DAA ≝
      (* V = M7 ⊙ R7 *)
      let s_tmp5 ≝ setweak_v_flag m t s_tmp4 ((MSB_b8 M_op) ⊙ (MSB_b8 R_op)) in
      (* newpc = curpc *)
-     Some ? (pair ?? s_tmp5 cur_pc) ]).
+     Some ? (pair … s_tmp5 cur_pc) ]).
 
 (* if (--M)≠0, branch *)
 ndefinition execute_DBNZ ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load false m t s cur_pc i)
+ opt_map … (multi_mode_load false m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ triple s_tmp1 M_op new_pc ⇒
     match M_op with
      [ mk_word16 MH_op ML_op ⇒
      (* --M *)
      let MH_op' ≝ pred_b8 MH_op in
-     opt_map ?? (multi_mode_write true m t s_tmp1 cur_pc i MH_op')
+     opt_map … (multi_mode_write true m t s_tmp1 cur_pc i MH_op')
       (λS_PC.match S_PC with
        [ pair s_tmp2 _ ⇒
         (* if (--M)≠0, branch *)
         match eq_b8 MH_op' 〈x0,x0〉 with
          (* new_pc = new_pc *)
-         [ true ⇒ Some ? (pair ?? s_tmp2 new_pc)
+         [ true ⇒ Some ? (pair … s_tmp2 new_pc)
          (* new_pc = new_pc + rel *)
-         | false ⇒ Some ? (pair ?? s_tmp2 (branched_pc m t s_tmp2 new_pc ML_op)) ]])]]).
+         | false ⇒ Some ? (pair … s_tmp2 (branched_pc m t s_tmp2 new_pc ML_op)) ]])]]).
 
 (* M = M - 1 *)
 ndefinition execute_DEC ≝
@@ -656,8 +655,8 @@ ndefinition execute_DEC ≝
 (* per i dettagli vedere div_b8 (modulo word16) *)
 ndefinition execute_DIV ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_indX_8_high_reg m t s)
-  (λH_op.opt_map ?? (get_indX_8_low_reg m t s)
+ opt_map … (get_indX_8_high_reg m t s)
+  (λH_op.opt_map … (get_indX_8_low_reg m t s)
    (λX_op.match div_b8 〈H_op:(get_acc_8_low_reg m t s)〉 X_op with
     [ triple quoz rest overflow ⇒
      (* C = overflow *)
@@ -670,10 +669,10 @@ ndefinition execute_DIV ≝
      (* NB: che A sia cambiato o no, lo testa *)
      let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 (get_acc_8_low_reg m t s_tmp2) 〈x0,x0〉) in
      (* H = H o H:AmodX *)
-     opt_map ?? (match overflow with
+     opt_map … (match overflow with
                  [ true ⇒ Some ? s_tmp3
                  | false ⇒ set_indX_8_high_reg m t s_tmp3 rest])
-      (λs_tmp4.Some ? (pair ?? s_tmp4 cur_pc)) ])).
+      (λs_tmp4.Some ? (pair … s_tmp4 cur_pc)) ])).
 
 (* A = A ⊙ M *)
 ndefinition execute_EOR ≝
@@ -692,37 +691,37 @@ ndefinition execute_INC ≝
 (* jmp, il nuovo indirizzo e' una WORD *)
 ndefinition execute_JMP ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load false m t s cur_pc i)
+ opt_map … (multi_mode_load false m t s cur_pc i)
   (λS_M_PC.
    (* newpc = M_op *)
-   Some ? (pair ?? (fst3T ??? S_M_PC) (snd3T ??? S_M_PC))).
+   Some ? (pair … (fst3T ??? S_M_PC) (snd3T ??? S_M_PC))).
 
 (* jump to subroutine *)
 (* HC05/HC08/HCS08 si appoggiano allo stack, RS08 a SPC *)
 ndefinition execute_JSR ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load false m t s cur_pc i)
+ opt_map … (multi_mode_load false m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ triple s_tmp1 M_op new_pc ⇒ let aux ≝
     (* push (new_pc low) *)
-    opt_map ?? (aux_push m t s_tmp1 (w16l new_pc))
+    opt_map … (aux_push m t s_tmp1 (w16l new_pc))
      (* push (new_pc high) *)
-     (λs_tmp2.opt_map ?? (aux_push m t s_tmp2 (w16h new_pc))
+     (λs_tmp2.opt_map … (aux_push m t s_tmp2 (w16h new_pc))
       (* newpc = M_op *)
-      (λs_tmp3.Some ? (pair ?? s_tmp3 M_op)))
+      (λs_tmp3.Some ? (pair … s_tmp3 M_op)))
      in match m with
     [ HC05 ⇒ aux | HC08 ⇒ aux | HCS08 ⇒ aux
     | RS08 ⇒
      (* SPC = new_pc *) 
-     opt_map ?? (set_spc_reg m t s_tmp1 new_pc)
+     opt_map … (set_spc_reg m t s_tmp1 new_pc)
       (* newpc = M_op *)
-      (λs_tmp2.Some ? (pair ?? s_tmp2 M_op))
+      (λs_tmp2.Some ? (pair … s_tmp2 M_op))
     ]]).
 
 (* A = M *)
 ndefinition execute_LDA ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load true m t s cur_pc i)
+ opt_map … (multi_mode_load true m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ triple s_tmp1 M_op new_pc ⇒
     (* A = M *) 
@@ -734,15 +733,15 @@ ndefinition execute_LDA ≝
     (* V = 0 *) 
     let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
     (* newpc = nextpc *)
-    Some ? (pair ?? s_tmp5 new_pc) ]).
+    Some ? (pair … s_tmp5 new_pc) ]).
 
 (* H:X = M *)
 ndefinition execute_LDHX ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load false m t s cur_pc i)
+ opt_map … (multi_mode_load false m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ triple s_tmp1 M_op new_pc ⇒
-    opt_map ?? (set_indX_16_reg m t s_tmp1 M_op)
+    opt_map … (set_indX_16_reg m t s_tmp1 M_op)
      (λs_tmp2.
       (* Z = nR15&nR14&nR13nR12&nR11&nR10&nR9&nR8nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
       let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_w16 M_op 〈〈x0,x0〉:〈x0,x0〉〉) in
@@ -751,15 +750,15 @@ ndefinition execute_LDHX ≝
       (* V = 0 *) 
       let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
       (* newpc = nextpc *)
-      Some ? (pair ?? s_tmp5 new_pc)) ]).
+      Some ? (pair … s_tmp5 new_pc)) ]).
 
 (* X = M *)
 ndefinition execute_LDX ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load true m t s cur_pc i)
+ opt_map … (multi_mode_load true m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ triple s_tmp1 M_op new_pc ⇒
-    opt_map ?? (set_indX_8_low_reg m t s_tmp1 M_op)
+    opt_map … (set_indX_8_low_reg m t s_tmp1 M_op)
      (λs_tmp2.
       (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
       let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 M_op 〈x0,x0〉) in
@@ -768,7 +767,7 @@ ndefinition execute_LDX ≝
       (* V = 0 *) 
       let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
       (* newpc = nextpc *)
-      Some ? (pair ?? s_tmp5 new_pc)) ]).
+      Some ? (pair … s_tmp5 new_pc)) ]).
 
 (* M = 0 -> rcr M -> C' *)
 ndefinition execute_LSR ≝
@@ -779,11 +778,11 @@ ndefinition execute_LSR ≝
 ndefinition execute_MOV ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
  (* R_op = M1 *)
- opt_map ?? (multi_mode_load true m t s cur_pc i)
+ opt_map … (multi_mode_load true m t s cur_pc i)
   (λS_R_PC.match S_R_PC with
    [ triple s_tmp1 R_op tmp_pc ⇒
     (* M2 = R_op *)
-    opt_map ?? (multi_mode_write true m t s_tmp1 tmp_pc i R_op)
+    opt_map … (multi_mode_write true m t s_tmp1 tmp_pc i R_op)
      (λS_PC.match S_PC with
       [ pair s_tmp2 new_pc ⇒
        (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
@@ -793,15 +792,15 @@ ndefinition execute_MOV ≝
        (* V = 0 *) 
        let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
        (* newpc = nextpc *)
-       Some ? (pair ?? s_tmp5 new_pc)])]).
+       Some ? (pair … s_tmp5 new_pc)])]).
 
 (* X:A = X * A *)
 ndefinition execute_MUL ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_indX_8_low_reg m t s)
+ opt_map … (get_indX_8_low_reg m t s)
   (λX_op.let R_op ≝ mul_b8 X_op (get_acc_8_low_reg m t s) in
-   opt_map ?? (set_indX_8_low_reg m t s (w16h R_op))
-    (λs_tmp.Some ? (pair ?? (set_acc_8_low_reg m t s_tmp (w16l R_op)) cur_pc))).
+   opt_map … (set_indX_8_low_reg m t s (w16h R_op))
+    (λs_tmp.Some ? (pair … (set_acc_8_low_reg m t s_tmp (w16l R_op)) cur_pc))).
 
 (* M = compl M *)
 ndefinition execute_NEG ≝
@@ -815,7 +814,7 @@ ndefinition execute_NEG ≝
 (* nulla *)
 ndefinition execute_NOP ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pair ?? s cur_pc).
+ Some ? (pair … s cur_pc).
 
 (* A = (mk_byte8 (b8l A) (b8h A)) *)
 (* cioe' swap del nibble alto/nibble basso di A *)
@@ -823,7 +822,7 @@ ndefinition execute_NSA ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
  match get_acc_8_low_reg m t s with [ mk_byte8 ah al ⇒
   (* A = (mk_byte8 (b8l A) (b8h A)) *)
-  Some ? (pair ?? (set_acc_8_low_reg m t s 〈al,ah〉) cur_pc) ].
+  Some ? (pair … (set_acc_8_low_reg m t s 〈al,ah〉) cur_pc) ].
 
 (* A = A | M *)
 ndefinition execute_ORA ≝
@@ -833,45 +832,45 @@ ndefinition execute_ORA ≝
 (* push A *)
 ndefinition execute_PSHA ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (aux_push m t s (get_acc_8_low_reg m t s))
-  (λs_tmp1.Some ? (pair ?? s_tmp1 cur_pc)).
+ opt_map … (aux_push m t s (get_acc_8_low_reg m t s))
+  (λs_tmp1.Some ? (pair … s_tmp1 cur_pc)).
 
 (* push H *)
 ndefinition execute_PSHH ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_indX_8_high_reg m t s)
-  (λH_op.opt_map ?? (aux_push m t s H_op)
-   (λs_tmp1.Some ? (pair ?? s_tmp1 cur_pc))).
+ opt_map … (get_indX_8_high_reg m t s)
+  (λH_op.opt_map … (aux_push m t s H_op)
+   (λs_tmp1.Some ? (pair … s_tmp1 cur_pc))).
 
 (* push X *)
 ndefinition execute_PSHX ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_indX_8_low_reg m t s)
-  (λH_op.opt_map ?? (aux_push m t s H_op)
-   (λs_tmp1.Some ? (pair ?? s_tmp1 cur_pc))).
+ opt_map … (get_indX_8_low_reg m t s)
+  (λH_op.opt_map … (aux_push m t s H_op)
+   (λs_tmp1.Some ? (pair … s_tmp1 cur_pc))).
 
 (* pop A *)
 ndefinition execute_PULA ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (aux_pop m t s)
+ opt_map … (aux_pop m t s)
   (λS_and_A.match S_and_A with [ pair s_tmp1 A_op ⇒
-   Some ? (pair ?? (set_acc_8_low_reg m t s_tmp1 A_op) cur_pc) ]).
+   Some ? (pair … (set_acc_8_low_reg m t s_tmp1 A_op) cur_pc) ]).
 
 (* pop H *)
 ndefinition execute_PULH ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (aux_pop m t s)
+ opt_map … (aux_pop m t s)
   (λS_and_H.match S_and_H with [ pair s_tmp1 H_op ⇒
-   opt_map ?? (set_indX_8_high_reg m t s_tmp1 H_op)
-    (λs_tmp2.Some ? (pair ?? s_tmp2 cur_pc))]).
+   opt_map … (set_indX_8_high_reg m t s_tmp1 H_op)
+    (λs_tmp2.Some ? (pair … s_tmp2 cur_pc))]).
 
 (* pop X *)
 ndefinition execute_PULX ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (aux_pop m t s)
+ opt_map … (aux_pop m t s)
   (λS_and_X.match S_and_X with [ pair s_tmp1 X_op ⇒
-   opt_map ?? (set_indX_8_low_reg m t s_tmp1 X_op)
-    (λs_tmp2.Some ? (pair ?? s_tmp2 cur_pc))]).
+   opt_map … (set_indX_8_low_reg m t s_tmp1 X_op)
+    (λs_tmp2.Some ? (pair … s_tmp2 cur_pc))]).
 
 (* M = C' <- rcl M <- C *)
 ndefinition execute_ROL ≝
@@ -887,33 +886,33 @@ ndefinition execute_ROR ≝
 (* lascia inalterato il byte superiore di SP *)
 ndefinition execute_RSP ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_sp_reg m t s)
+ opt_map … (get_sp_reg m t s)
   (λSP_op.match SP_op with [ mk_word16 sph spl ⇒
-   opt_map ?? (set_sp_reg m t s 〈sph:〈xF,xF〉〉)
-    (λs_tmp.Some ? (pair ?? s_tmp cur_pc))]).
+   opt_map … (set_sp_reg m t s 〈sph:〈xF,xF〉〉)
+    (λs_tmp.Some ? (pair … s_tmp cur_pc))]).
 
 (* return from interrupt *)
 ndefinition execute_RTI ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
  (* pop (CCR) *)
- opt_map ?? (aux_pop m t s)
+ opt_map … (aux_pop m t s)
   (λS_and_CCR.match S_and_CCR with [ pair s_tmp1 CCR_op ⇒
    let s_tmp2 ≝ aux_set_CCR m t s_tmp1 CCR_op in
    (* pop (A) *)
-   opt_map ?? (aux_pop m t s_tmp2)
+   opt_map … (aux_pop m t s_tmp2)
     (λS_and_A.match S_and_A with [ pair s_tmp3 A_op ⇒
      let s_tmp4 ≝ set_acc_8_low_reg m t s_tmp3 A_op in
      (* pop (X) *)
-     opt_map ?? (aux_pop m t s_tmp4)
+     opt_map … (aux_pop m t s_tmp4)
       (λS_and_X.match S_and_X with [ pair s_tmp5 X_op ⇒
-       opt_map ?? (set_indX_8_low_reg m t s_tmp5 X_op)
+       opt_map … (set_indX_8_low_reg m t s_tmp5 X_op)
         (* pop (PC high) *)
-        (λs_tmp6.opt_map ?? (aux_pop m t s_tmp6)
+        (λs_tmp6.opt_map … (aux_pop m t s_tmp6)
          (λS_and_PCH.match S_and_PCH with [ pair s_tmp7 PCH_op ⇒
           (* pop (PC low) *)
-          opt_map ?? (aux_pop m t s_tmp7)
+          opt_map … (aux_pop m t s_tmp7)
            (λS_and_PCL.match S_and_PCL with [ pair s_tmp8 PCL_op ⇒
-            Some ? (pair ?? s_tmp8 〈PCH_op:PCL_op〉)])]))])])]).
+            Some ? (pair … s_tmp8 〈PCH_op:PCL_op〉)])]))])])]).
 
 (* return from subroutine *)
 (* HC05/HC08/HCS08 si appoggia allo stack, RS08 si appoggia a SPC *)
@@ -921,18 +920,18 @@ ndefinition execute_RTS ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
  let aux ≝
   (* pop (PC high) *)
-  opt_map ?? (aux_pop m t s)
+  opt_map … (aux_pop m t s)
    (λS_and_PCH.match S_and_PCH with [ pair s_tmp1 PCH_op ⇒
     (* pop (PC low) *)
-    opt_map ?? (aux_pop m t s_tmp1)
+    opt_map … (aux_pop m t s_tmp1)
      (λS_and_PCL.match S_and_PCL with [ pair s_tmp2 PCL_op ⇒
-      Some ? (pair ?? s_tmp2 〈PCH_op:PCL_op〉)])])
+      Some ? (pair … s_tmp2 〈PCH_op:PCL_op〉)])])
  in match m with
   [ HC05 ⇒ aux | HC08 ⇒ aux | HCS08 ⇒ aux
   | RS08 ⇒
    (* new_pc = SPC *)
-   opt_map ?? (get_spc_reg m t s)
-    (λSPC_op.Some ? (pair ?? s SPC_op))
+   opt_map … (get_spc_reg m t s)
+    (λSPC_op.Some ? (pair … s SPC_op))
   ].
 
 (* A = A - M - C *)
@@ -942,18 +941,18 @@ ndefinition execute_SBC ≝
  (λA_op.λM_op.λC_op.match plus_b8_dc_dc A_op (compl_b8 M_op) false with
   [ pair resb resc ⇒ match C_op with
    [ true ⇒ plus_b8_dc_dc resb 〈xF,xF〉 false
-   | false ⇒ pair ?? resb resc ]]).
+   | false ⇒ pair … resb resc ]]).
 
 (* C = 1 *)
 ndefinition execute_SEC ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pair ?? (set_c_flag m t s true) cur_pc).
+ Some ? (pair … (set_c_flag m t s true) cur_pc).
 
 (* I = 1 *)
 ndefinition execute_SEI ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (set_i_flag m t s true)
-  (λs_tmp.Some ? (pair ?? s_tmp cur_pc)).
+ opt_map … (set_i_flag m t s true)
+  (λs_tmp.Some ? (pair … s_tmp cur_pc)).
 
 (* swap SPCh,A *)
 (* senso: nell'RS08 SPC non e' accessibile direttamente e come si possono
@@ -961,9 +960,9 @@ ndefinition execute_SEI ≝
           occore accedere a SPC e salvarne il contenuto *)
 ndefinition execute_SHA ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_spc_reg m t s)
-  (λSPC_op.opt_map ?? (set_spc_reg m t s 〈(get_acc_8_low_reg m t s):(w16l SPC_op)〉)
-   (λs_tmp1.Some ? (pair ?? (set_acc_8_low_reg m t s_tmp1 (w16h SPC_op)) cur_pc))).
+ opt_map … (get_spc_reg m t s)
+  (λSPC_op.opt_map … (set_spc_reg m t s 〈(get_acc_8_low_reg m t s):(w16l SPC_op)〉)
+   (λs_tmp1.Some ? (pair … (set_acc_8_low_reg m t s_tmp1 (w16h SPC_op)) cur_pc))).
 
 (* swap SPCl,A *)
 (* senso: nell'RS08 SPC non e' accessibile direttamente e come si possono
@@ -971,16 +970,16 @@ ndefinition execute_SHA ≝
           occore accedere a SPC e salvarne il contenuto *)
 ndefinition execute_SLA ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_spc_reg m t s)
-  (λSPC_op.opt_map ?? (set_spc_reg m t s 〈(w16h SPC_op):(get_acc_8_low_reg m t s)〉)
-   (λs_tmp1.Some ? (pair ?? (set_acc_8_low_reg m t s_tmp1 (w16l SPC_op)) cur_pc))).
+ opt_map … (get_spc_reg m t s)
+  (λSPC_op.opt_map … (set_spc_reg m t s 〈(w16h SPC_op):(get_acc_8_low_reg m t s)〉)
+   (λs_tmp1.Some ? (pair … (set_acc_8_low_reg m t s_tmp1 (w16l SPC_op)) cur_pc))).
 
 (* M = A *)
 ndefinition execute_STA ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
  (* M = A *)
  let A_op ≝ (get_acc_8_low_reg m t s) in
- opt_map ?? (multi_mode_write true m t s cur_pc i A_op)
+ opt_map … (multi_mode_write true m t s cur_pc i A_op)
   (λS_op_and_PC.match S_op_and_PC with
    [ pair s_tmp1 new_pc ⇒
    (* Z = nA7&nA6&nA5&nA4&nA3&nA2&nA1&nA0 *)
@@ -990,14 +989,14 @@ ndefinition execute_STA ≝
    (* V = 0 *)
    let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
    (* newpc = nextpc *)
-   Some ? (pair ?? s_tmp4 new_pc) ]).
+   Some ? (pair … s_tmp4 new_pc) ]).
 
 (* M = H:X *)
 ndefinition execute_STHX ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
  (* M = H:X *)
- opt_map ?? (get_indX_16_reg m t s)
-  (λX_op.opt_map ?? (multi_mode_write false m t s cur_pc i X_op)
+ opt_map … (get_indX_16_reg m t s)
+  (λX_op.opt_map … (multi_mode_write false m t s cur_pc i X_op)
    (λS_op_and_PC.match S_op_and_PC with
     [ pair s_tmp1 new_pc ⇒
      (* Z = nR15&nR14&nR13nR12&nR11&nR10&nR9&nR8nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
@@ -1007,19 +1006,19 @@ ndefinition execute_STHX ≝
      (* V = 0 *)
      let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
      (* newpc = nextpc *)
-      Some ? (pair ?? s_tmp4 new_pc) ])).
+      Some ? (pair … s_tmp4 new_pc) ])).
 
 (* I = 0 *)
 ndefinition execute_STOP ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pair ?? (setweak_i_flag m t s false) cur_pc).
+ Some ? (pair … (setweak_i_flag m t s false) cur_pc).
 
 (* M = X *)
 ndefinition execute_STX ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
  (* M = X *)
- opt_map ?? (get_indX_8_low_reg m t s)
-  (λX_op.opt_map ?? (multi_mode_write true m t s cur_pc i X_op)
+ opt_map … (get_indX_8_low_reg m t s)
+  (λX_op.opt_map … (multi_mode_write true m t s cur_pc i X_op)
    (λS_op_and_PC.match S_op_and_PC with
     [ pair s_tmp1 new_pc ⇒
      (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
@@ -1029,7 +1028,7 @@ ndefinition execute_STX ≝
      (* V = 0 *)
      let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
      (* newpc = nextpc *)
-     Some ? (pair ?? s_tmp4 new_pc) ])).
+     Some ? (pair … s_tmp4 new_pc) ])).
 
 (* A = A - M *)
 ndefinition execute_SUB ≝
@@ -1042,47 +1041,47 @@ ndefinition execute_SWI ≝
  (* indirizzo da cui caricare il nuovo pc *)
  let vector ≝ get_pc_reg m t (set_pc_reg m t s 〈〈xF,xF〉:〈xF,xC〉〉) in
  (* push (cur_pc low) *)
- opt_map ?? (aux_push m t s (w16l cur_pc))
+ opt_map … (aux_push m t s (w16l cur_pc))
   (* push (cur_pc high *)
-  (λs_tmp1.opt_map ?? (aux_push m t s_tmp1 (w16h cur_pc))
-   (λs_tmp2.opt_map ?? (get_indX_8_low_reg m t s_tmp2)
+  (λs_tmp1.opt_map … (aux_push m t s_tmp1 (w16h cur_pc))
+   (λs_tmp2.opt_map … (get_indX_8_low_reg m t s_tmp2)
     (* push (X) *)
-    (λX_op.opt_map ?? (aux_push m t s_tmp2 X_op)
+    (λX_op.opt_map … (aux_push m t s_tmp2 X_op)
      (* push (A) *)
-     (λs_tmp3.opt_map ?? (aux_push m t s_tmp3 (get_acc_8_low_reg m t s_tmp3))
+     (λs_tmp3.opt_map … (aux_push m t s_tmp3 (get_acc_8_low_reg m t s_tmp3))
       (* push (CCR) *)
-      (λs_tmp4.opt_map ?? (aux_push m t s_tmp4 (aux_get_CCR m t s_tmp4))
+      (λs_tmp4.opt_map … (aux_push m t s_tmp4 (aux_get_CCR m t s_tmp4))
        (* I = 1 *)
-       (λs_tmp5.opt_map ?? (set_i_flag m t s_tmp5 true)
+       (λs_tmp5.opt_map … (set_i_flag m t s_tmp5 true)
         (* load from vector high *)
-        (λs_tmp6.opt_map ?? (memory_filter_read m t s_tmp6 vector)
+        (λs_tmp6.opt_map … (memory_filter_read m t s_tmp6 vector)
          (* load from vector low *)
-         (λaddrh.opt_map ?? (memory_filter_read m t s_tmp6 (succ_w16 vector))
+         (λaddrh.opt_map … (memory_filter_read m t s_tmp6 (succ_w16 vector))
           (* newpc = [vector] *)
-          (λaddrl.Some ? (pair ?? s_tmp6 〈addrh:addrl〉)))))))))).
+          (λaddrl.Some ? (pair … s_tmp6 〈addrh:addrl〉)))))))))).
 
 (* flags = A *)
 ndefinition execute_TAP ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pair ?? (aux_set_CCR m t s (get_acc_8_low_reg m t s)) cur_pc). 
+ Some ? (pair … (aux_set_CCR m t s (get_acc_8_low_reg m t s)) cur_pc). 
 
 (* X = A *)
 ndefinition execute_TAX ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (set_indX_8_low_reg m t s (get_acc_8_low_reg m t s))
-  (λs_tmp.Some ? (pair ?? s_tmp cur_pc)).
+ opt_map … (set_indX_8_low_reg m t s (get_acc_8_low_reg m t s))
+  (λs_tmp.Some ? (pair … s_tmp cur_pc)).
 
 (* A = flags *)
 ndefinition execute_TPA ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pair ?? (set_acc_8_low_reg m t s (aux_get_CCR m t s)) cur_pc).
+ Some ? (pair … (set_acc_8_low_reg m t s (aux_get_CCR m t s)) cur_pc).
 
 (* flags = M - 0 *)
 (* implementata senza richiamare la sottrazione, la modifica dei flag
    e' immediata *)
 ndefinition execute_TST ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load true m t s cur_pc i)
+ opt_map … (multi_mode_load true m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ triple s_tmp1 M_op new_pc ⇒
     (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
@@ -1092,34 +1091,34 @@ ndefinition execute_TST ≝
     (* V = 0 *) 
     let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
     (* newpc = nextpc *)
-    Some ? (pair ?? s_tmp4 new_pc) ]).
+    Some ? (pair … s_tmp4 new_pc) ]).
 
 (* H:X = SP + 1 *)
 ndefinition execute_TSX ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_sp_reg m t s )
-  (λSP_op.opt_map ?? (set_indX_16_reg m t s (succ_w16 SP_op))
+ opt_map … (get_sp_reg m t s )
+  (λSP_op.opt_map … (set_indX_16_reg m t s (succ_w16 SP_op))
    (* H:X = SP + 1 *)
-   (λs_tmp.Some ? (pair ?? s_tmp cur_pc))).
+   (λs_tmp.Some ? (pair … s_tmp cur_pc))).
 
 (* A = X *)
 ndefinition execute_TXA ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_indX_8_low_reg m t s)
-  (λX_op.Some ? (pair ?? (set_acc_8_low_reg m t s X_op) cur_pc)).
+ opt_map … (get_indX_8_low_reg m t s)
+  (λX_op.Some ? (pair … (set_acc_8_low_reg m t s X_op) cur_pc)).
 
 (* SP = H:X - 1 *)
 ndefinition execute_TXS ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_indX_16_reg m t s )
-  (λX_op.opt_map ?? (set_sp_reg m t s (pred_w16 X_op))
+ opt_map … (get_indX_16_reg m t s )
+  (λX_op.opt_map … (set_sp_reg m t s (pred_w16 X_op))
    (* SP = H:X - 1 *)
-   (λs_tmp.Some ? (pair ?? s_tmp cur_pc))).
+   (λs_tmp.Some ? (pair … s_tmp cur_pc))).
 
 (* I = 0 *)
 ndefinition execute_WAIT ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pair ?? (setweak_i_flag m t s false) cur_pc).
+ Some ? (pair … (setweak_i_flag m t s false) cur_pc).
 
 (* **** *)
 (* TICK *)
@@ -1132,8 +1131,8 @@ ninductive susp_type : Type ≝
 | WAIT_MODE: susp_type.
 
 (* un tipo opzione ad hoc
-   - errore: errore+stato (seguira' reset o ??, cmq lo stato non va buttato)
-   - sospensione: sospensione+stato (seguira' resume o ??)
+   - errore: errore+stato (seguira' reset o …, cmq lo stato non va buttato)
+   - sospensione: sospensione+stato (seguira' resume o …)
    - ok: stato
 *)
 ninductive tick_result (A:Type) : Type ≝
@@ -1268,7 +1267,7 @@ ndefinition tick_execute ≝
 
 ndefinition tick ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.
- let opt_info ≝ get_clk_desc m t s in
+ let opt_info ≝ clk_desc m t s in
  match opt_info with
   (* e' il momento del fetch *)
   [ None ⇒ match fetch m t s with
@@ -1281,7 +1280,7 @@ ndefinition tick ≝
        (* un solo clk, execute subito *)
        [ true ⇒ tick_execute m t s pseudo mode cur_pc
        (* piu' clk, execute rimandata *)
-       | false ⇒ TickOK ? (set_clk_desc m t s (Some ? (quintuple ????? 〈x0,x1〉 pseudo mode tot_clk cur_pc)))
+       | false ⇒ TickOK ? (set_clk_desc m t s (Some ? (quintuple … 〈x0,x1〉 pseudo mode tot_clk cur_pc)))
        ]
       ]
     ]
@@ -1291,7 +1290,7 @@ ndefinition tick ≝
     (* si *)
     [ true ⇒ tick_execute m t s pseudo mode cur_pc
     (* no, avanzamento cur_clk *)
-    | false ⇒ TickOK ? (set_clk_desc m t s (Some ? (quintuple ????? (succ_b8 cur_clk) pseudo mode tot_clk cur_pc)))
+    | false ⇒ TickOK ? (set_clk_desc m t s (Some ? (quintuple … (succ_b8 cur_clk) pseudo mode tot_clk cur_pc)))
     ]
    ]
   ].
@@ -1306,36 +1305,3 @@ nlet rec execute (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (
   | TickSUSP s' susp ⇒ TickSUSP ? s' susp
   | TickOK s'        ⇒ match n with [ O ⇒ TickOK ? s' | S n' ⇒ execute m t (tick m t s') n' ]
   ].
-
-nlemma breakpoint_err : ∀m,t,s,err,n.execute m t (TickERR ? s err) n = TickERR ? s err.
- #m; #t; #s; #err; #n;
- ncases n;
- ##[ ##2: #n1 ##]
- nnormalize;
- napply (refl_eq ??).
-nqed.
-
-nlemma breakpoint_susp : ∀m,t,s,susp,n.execute m t (TickSUSP ? s susp) n = TickSUSP ? s susp.
- #m; #t; #s; #susp; #n;
- ncases n;
- ##[ ##2: #n1 ##]
- nnormalize;
- napply (refl_eq ??).
-nqed.
-
-nlemma breakpoint :
- ∀m,t,n1,n2,s. execute m t s (n1 + n2) = execute m t (execute m t s n1) n2.
- #m; #t; #n1;
- nelim n1;
- ##[ ##1: nnormalize; #n2; #s; ncases s; nnormalize; ##[ ##1,2: #x ##] #y; napply (refl_eq ??)
- ##| ##2: #n3; #H; #n2; #s; ncases s;
-          ##[ ##1: #x; #y; nnormalize; nrewrite > (breakpoint_err m t x y n2); napply (refl_eq ??)
-          ##| ##2: #x; #y; nnormalize; nrewrite > (breakpoint_susp m t x y n2); napply (refl_eq ??)
-          ##| ##3: #x; nrewrite > (Sn_p_n_to_S_npn n3 n2);
-                   nchange with ((execute m t (tick m t x) (n3+n2)) =
-                                 (execute m t (execute m t (tick m t x) n3) n2));
-                   nrewrite > (H n2 (tick m t x));
-                   napply (refl_eq ??)
-          ##]
- ##]
-nqed.