a) update with upstream version

[helm.git] / helm / software / matita / contribs / assembly / freescale / load_write.ma

diff --git a/helm/software/matita/contribs/assembly/freescale/load_write.ma b/helm/software/matita/contribs/assembly/freescale/load_write.ma
index b288f9863d3726e636265177e0a299f7e5f43422..28c78b6bb74164d64c5efd582fef2dc09451c5c6 100644 (file)
--- a/helm/software/matita/contribs/assembly/freescale/load_write.ma
+++ b/helm/software/matita/contribs/assembly/freescale/load_write.ma
@@ -398,7 +398,7 @@ definition mode_IMM2_load ≝
 
 (* lettura da [byte [curpc]]: true=DIR1 loadb, false=DIR1 loadw *)
 definition mode_DIR1_load ≝
-λm:mcu_type.λt:memory_impl.λbyteflag:bool.λs:any_status m t.λcur_pc:word16.
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
  opt_map ?? (memory_filter_read m t s cur_pc)
   (λaddr.(aux_load m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc 1).
 
@@ -410,7 +410,7 @@ definition mode_DIR1n_load ≝
 
 (* scrittura su [byte [curpc]]: true=DIR1 writeb, false=DIR1 writew *)
 definition mode_DIR1_write ≝
-λm:mcu_type.λt:memory_impl.λbyteflag:bool.λs:any_status m t.λcur_pc:word16.
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
  opt_map ?? (memory_filter_read m t s cur_pc)
   (λaddr.(aux_write m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc 1 writebw).
@@ -423,14 +423,14 @@ definition mode_DIR1n_write ≝
 
 (* lettura da [word [curpc]]: true=DIR2 loadb, false=DIR2 loadw *)
 definition mode_DIR2_load ≝
-λm:mcu_type.λt:memory_impl.λbyteflag:bool.λs:any_status m t.λcur_pc:word16.
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
  opt_map ?? (memory_filter_read m t s cur_pc)
   (λaddrh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
    (λaddrl.(aux_load m t byteflag) s 〈addrh:addrl〉 cur_pc 2)).
 
 (* scrittura su [word [curpc]]: true=DIR2 writeb, false=DIR2 writew *)
 definition mode_DIR2_write ≝
-λm:mcu_type.λt:memory_impl.λbyteflag:bool.λs:any_status m t.λcur_pc:word16.
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
  opt_map ?? (memory_filter_read m t s cur_pc)
   (λaddrh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
@@ -446,20 +446,20 @@ definition get_IX ≝
 
 (* lettura da [IX]: true=IX0 loadb, false=IX0 loadw *)
 definition mode_IX0_load ≝
-λm:mcu_type.λt:memory_impl.λbyteflag:bool.λs:any_status m t.λcur_pc:word16.
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
  opt_map ?? (get_IX m t s)
   (λaddr.(aux_load m t byteflag) s addr cur_pc 0).
 
 (* scrittura su [IX]: true=IX0 writeb, false=IX0 writew *)
 definition mode_IX0_write ≝
-λm:mcu_type.λt:memory_impl.λbyteflag:bool.λs:any_status m t.λcur_pc:word16.
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
  opt_map ?? (get_IX m t s)
   (λaddr.(aux_write m t byteflag) s addr cur_pc 0 writebw).
 
 (* lettura da [IX+byte [pc]]: true=IX1 loadb, false=IX1 loadw *)
 definition mode_IX1_load ≝
-λm:mcu_type.λt:memory_impl.λbyteflag:bool.λs:any_status m t.λcur_pc:word16.
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
  opt_map ?? (get_IX m t s)
   (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
    (λoffs.(aux_load m t byteflag) s (plus_w16nc addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
@@ -473,7 +473,7 @@ definition mode_IX1ADD_load ≝
 
 (* scrittura su [IX+byte [pc]]: true=IX1 writeb, false=IX1 writew *)
 definition mode_IX1_write ≝
-λm:mcu_type.λt:memory_impl.λbyteflag:bool.λs:any_status m t.λcur_pc:word16.
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
  opt_map ?? (get_IX m t s)
   (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
@@ -481,7 +481,7 @@ definition mode_IX1_write ≝
 
 (* lettura da [IX+word [pc]]: true=IX2 loadb, false=IX2 loadw *)
 definition mode_IX2_load ≝
-λm:mcu_type.λt:memory_impl.λbyteflag:bool.λs:any_status m t.λcur_pc:word16.
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
  opt_map ?? (get_IX m t s)
   (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
    (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
@@ -497,7 +497,7 @@ definition mode_IX2ADD_load ≝
 
 (* scrittura su [IX+word [pc]]: true=IX2 writeb, false=IX2 writew *)
 definition mode_IX2_write ≝
-λm:mcu_type.λt:memory_impl.λbyteflag:bool.λs:any_status m t.λcur_pc:word16.
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
  opt_map ?? (get_IX m t s)
   (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
@@ -506,14 +506,14 @@ definition mode_IX2_write ≝
 
 (* lettura da [SP+byte [pc]]: true=SP1 loadb, false=SP1 loadw *)
 definition mode_SP1_load ≝
-λm:mcu_type.λt:memory_impl.λbyteflag:bool.λs:any_status m t.λcur_pc:word16.
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
  opt_map ?? (get_sp_reg m t s)
   (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
    (λoffs.(aux_load m t byteflag) s (plus_w16nc addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
 
 (* scrittura su [SP+byte [pc]]: true=SP1 writeb, false=SP1 writew *)
 definition mode_SP1_write ≝
-λm:mcu_type.λt:memory_impl.λbyteflag:bool.λs:any_status m t.λcur_pc:word16.
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
  opt_map ?? (get_sp_reg m t s)
   (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
@@ -521,7 +521,7 @@ definition mode_SP1_write ≝
 
 (* lettura da [SP+word [pc]]: true=SP2 loadb, false=SP2 loadw *)
 definition mode_SP2_load ≝
-λm:mcu_type.λt:memory_impl.λbyteflag:bool.λs:any_status m t.λcur_pc:word16.
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
  opt_map ?? (get_sp_reg m t s)
   (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
    (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
@@ -529,7 +529,7 @@ definition mode_SP2_load ≝
 
 (* scrittura su [SP+word [pc]]: true=SP2 writeb, false=SP2 writew *)
 definition mode_SP2_write ≝
-λm:mcu_type.λt:memory_impl.λbyteflag:bool.λs:any_status m t.λcur_pc:word16.
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
  opt_map ?? (get_sp_reg m t s)
   (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
@@ -549,7 +549,7 @@ definition aux_inc_indX_16 ≝
 
 (* tutte le modalita' di lettura: false=loadb true=loadw *)
 definition multi_mode_load ≝
-λm:mcu_type.λt:memory_impl.λbyteflag:bool.
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.
  match byteflag
  return λbyteflag:bool.any_status m t → word16 → instr_mode → 
   option (Prod3T (any_status m t) match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] word16)
@@ -581,28 +581,28 @@ definition multi_mode_load ≝
 (* NO: solo lettura word *)
    | MODE_IMM2 ⇒ None ?
 (* preleva 1 byte da indirizzo diretto 1 byte *) 
-   | MODE_DIR1 ⇒ mode_DIR1_load m t true s cur_pc
+   | MODE_DIR1 ⇒ mode_DIR1_load true m t s cur_pc
 (* preleva 1 byte da indirizzo diretto 1 word *)
-   | MODE_DIR2 ⇒ mode_DIR2_load m t true s cur_pc
+   | MODE_DIR2 ⇒ mode_DIR2_load true m t s cur_pc
 (* preleva 1 byte da H:X *)
-   | MODE_IX0  ⇒ mode_IX0_load m t true s cur_pc
+   | MODE_IX0  ⇒ mode_IX0_load true m t s cur_pc
 (* preleva 1 byte da H:X+1 byte offset *)
-   | MODE_IX1  ⇒ mode_IX1_load m t true s cur_pc
+   | MODE_IX1  ⇒ mode_IX1_load true m t s cur_pc
 (* preleva 1 byte da H:X+1 word offset *)
-   | MODE_IX2  ⇒ mode_IX2_load m t true s cur_pc
+   | MODE_IX2  ⇒ mode_IX2_load true m t s cur_pc
 (* preleva 1 byte da SP+1 byte offset *)
-   | MODE_SP1  ⇒ mode_SP1_load m t true s cur_pc
+   | MODE_SP1  ⇒ mode_SP1_load true m t s cur_pc
 (* preleva 1 byte da SP+1 word offset *)
-   | MODE_SP2  ⇒ mode_SP2_load m t true s cur_pc
+   | MODE_SP2  ⇒ mode_SP2_load true m t s cur_pc
 
 (* come DIR1, chiamare scrittura per passo2: scrittura su DIR1 *)
-   | MODE_DIR1_to_DIR1 ⇒ mode_DIR1_load m t true s cur_pc
+   | MODE_DIR1_to_DIR1 ⇒ mode_DIR1_load true m t s cur_pc
 (* come IMM1, chiamare scrittura per passo2: scrittura su DIR1 *)
    | MODE_IMM1_to_DIR1 ⇒ mode_IMM1_load m t s cur_pc
 (* come IX0, chiamare scrittura per passo2: scrittura su DIR1 e X++ *)
-   | MODE_IX0p_to_DIR1 ⇒ mode_IX0_load m t true s cur_pc
+   | MODE_IX0p_to_DIR1 ⇒ mode_IX0_load true m t s cur_pc
 (* come DIR1, chiamare scrittura per passo2: scrittura su IX0 e X++ *)
-   | MODE_DIR1_to_IX0p ⇒ mode_DIR1_load m t true s cur_pc
+   | MODE_DIR1_to_IX0p ⇒ mode_DIR1_load true m t s cur_pc
 
 (* NO: solo lettura word/scrittura byte *)
    | MODE_INHA_and_IMM1 ⇒ None ?
@@ -660,19 +660,19 @@ definition multi_mode_load ≝
 (* preleva 1 word immediato *) 
    | MODE_IMM2 ⇒ mode_IMM2_load m t s cur_pc
 (* preleva 1 word da indirizzo diretto 1 byte *) 
-   | MODE_DIR1 ⇒ mode_DIR1_load m t false s cur_pc
+   | MODE_DIR1 ⇒ mode_DIR1_load false m t s cur_pc
 (* preleva 1 word da indirizzo diretto 1 word *) 
-   | MODE_DIR2 ⇒ mode_DIR2_load m t false s cur_pc
+   | MODE_DIR2 ⇒ mode_DIR2_load false m t s cur_pc
 (* preleva 1 word da H:X *)
-   | MODE_IX0  ⇒ mode_IX0_load m t false s cur_pc
+   | MODE_IX0  ⇒ mode_IX0_load false m t s cur_pc
 (* preleva 1 word da H:X+1 byte offset *)
-   | MODE_IX1  ⇒ mode_IX1_load m t false s cur_pc
+   | MODE_IX1  ⇒ mode_IX1_load false m t s cur_pc
 (* preleva 1 word da H:X+1 word offset *)
-   | MODE_IX2  ⇒ mode_IX2_load m t false s cur_pc
+   | MODE_IX2  ⇒ mode_IX2_load false m t s cur_pc
 (* preleva 1 word da SP+1 byte offset *)
-   | MODE_SP1  ⇒ mode_SP1_load m t false s cur_pc
+   | MODE_SP1  ⇒ mode_SP1_load false m t s cur_pc
 (* preleva 1 word da SP+1 word offset *)
-   | MODE_SP2  ⇒ mode_SP2_load m t false s cur_pc
+   | MODE_SP2  ⇒ mode_SP2_load false m t s cur_pc
 
 (* NO: solo lettura/scrittura byte *)
    | MODE_DIR1_to_DIR1 ⇒ None ?
@@ -703,7 +703,7 @@ definition multi_mode_load ≝
                                [ tripleT _ immb2 cur_pc'' ⇒
                                 Some ? (tripleT ??? s 〈immb1:immb2〉 cur_pc'')])])
 (* preleva 2 byte, possibilita' modificare Io argomento *)
-   | MODE_DIR1_and_IMM1 ⇒ opt_map ?? (mode_DIR1_load m t true s cur_pc)
+   | MODE_DIR1_and_IMM1 ⇒ opt_map ?? (mode_DIR1_load true m t s cur_pc)
                            (λS_dirb_and_PC.match S_dirb_and_PC with
                             [ tripleT _ dirb cur_pc' ⇒
                              opt_map ?? (mode_IMM1_load m t s cur_pc')
@@ -711,7 +711,7 @@ definition multi_mode_load ≝
                                [ tripleT _ immb cur_pc'' ⇒
                                 Some ? (tripleT ??? s 〈dirb:immb〉 cur_pc'')])])
 (* preleva 2 byte, possibilita' modificare Io argomento *)
-   | MODE_IX0_and_IMM1  ⇒ opt_map ?? (mode_IX0_load m t true s cur_pc)
+   | MODE_IX0_and_IMM1  ⇒ opt_map ?? (mode_IX0_load true m t s cur_pc)
                            (λS_ixb_and_PC.match S_ixb_and_PC with
                             [ tripleT _ ixb cur_pc' ⇒
                              opt_map ?? (mode_IMM1_load m t s cur_pc')
@@ -719,7 +719,7 @@ definition multi_mode_load ≝
                                [ tripleT _ immb cur_pc'' ⇒
                                 Some ? (tripleT ??? s 〈ixb:immb〉 cur_pc'')])])
 (* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
-   | MODE_IX0p_and_IMM1 ⇒ opt_map ?? (mode_IX0_load m t true s cur_pc)
+   | MODE_IX0p_and_IMM1 ⇒ opt_map ?? (mode_IX0_load true m t s cur_pc)
                            (λS_ixb_and_PC.match S_ixb_and_PC with
                             [ tripleT _ ixb cur_pc' ⇒
                              opt_map ?? (mode_IMM1_load m t s cur_pc')
@@ -729,7 +729,7 @@ definition multi_mode_load ≝
                                 opt_map ?? (aux_inc_indX_16 m t s)
                                  (λs'.Some ? (tripleT ??? s' 〈ixb:immb〉 cur_pc''))])])
 (* preleva 2 byte, possibilita' modificare Io argomento *)
-   | MODE_IX1_and_IMM1  ⇒ opt_map ?? (mode_IX1_load m t true s cur_pc)
+   | MODE_IX1_and_IMM1  ⇒ opt_map ?? (mode_IX1_load true m t s cur_pc)
                            (λS_ixb_and_PC.match S_ixb_and_PC with
                             [ tripleT _ ixb cur_pc' ⇒
                              opt_map ?? (mode_IMM1_load m t s cur_pc')
@@ -737,7 +737,7 @@ definition multi_mode_load ≝
                                [ tripleT _ immb cur_pc'' ⇒
                                 Some ? (tripleT ??? s 〈ixb:immb〉 cur_pc'')])])
 (* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
-   | MODE_IX1p_and_IMM1 ⇒ opt_map ?? (mode_IX1_load m t true s cur_pc)
+   | MODE_IX1p_and_IMM1 ⇒ opt_map ?? (mode_IX1_load true m t s cur_pc)
                            (λS_ixb_and_PC.match S_ixb_and_PC with
                             [ tripleT _ ixb cur_pc' ⇒
                              opt_map ?? (mode_IMM1_load m t s cur_pc')
@@ -747,7 +747,7 @@ definition multi_mode_load ≝
                                 opt_map ?? (aux_inc_indX_16 m t s)
                                  (λs'.Some ? (tripleT ??? s' 〈ixb:immb〉 cur_pc''))])])
 (* preleva 2 byte, possibilita' modificare Io argomento *)
-   | MODE_SP1_and_IMM1  ⇒ opt_map ?? (mode_SP1_load m t true s cur_pc)
+   | MODE_SP1_and_IMM1  ⇒ opt_map ?? (mode_SP1_load true m t s cur_pc)
                            (λS_spb_and_PC.match S_spb_and_PC with
                             [ tripleT _ spb cur_pc' ⇒
                              opt_map ?? (mode_IMM1_load m t s cur_pc')
@@ -778,7 +778,7 @@ definition multi_mode_load ≝
 
 (* tutte le modalita' di scrittura: true=writeb, false=writew *)
 definition multi_mode_write ≝
-λm:mcu_type.λt:memory_impl.λbyteflag:bool.match byteflag
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.match byteflag
  return λbyteflag:bool.any_status m t → word16 → instr_mode →
   match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] →
   option (Prod (any_status m t) word16) with
@@ -809,32 +809,32 @@ definition multi_mode_write ≝
 (* NO: solo lettura word *)
   | MODE_IMM2       ⇒ None ?
 (* scrive 1 byte su indirizzo diretto 1 byte *)
-  | MODE_DIR1       ⇒ mode_DIR1_write m t true s cur_pc writeb
+  | MODE_DIR1       ⇒ mode_DIR1_write true m t s cur_pc writeb
 (* scrive 1 byte su indirizzo diretto 1 word *)
-  | MODE_DIR2       ⇒ mode_DIR2_write m t true s cur_pc writeb
+  | MODE_DIR2       ⇒ mode_DIR2_write true m t s cur_pc writeb
 (* scrive 1 byte su H:X *)
-  | MODE_IX0        ⇒ mode_IX0_write m t true s cur_pc writeb
+  | MODE_IX0        ⇒ mode_IX0_write true m t s cur_pc writeb
 (* scrive 1 byte su H:X+1 byte offset *)
-  | MODE_IX1        ⇒ mode_IX1_write m t true s cur_pc writeb
+  | MODE_IX1        ⇒ mode_IX1_write true m t s cur_pc writeb
 (* scrive 1 byte su H:X+1 word offset *)
-  | MODE_IX2        ⇒ mode_IX2_write m t true s cur_pc writeb
+  | MODE_IX2        ⇒ mode_IX2_write true m t s cur_pc writeb
 (* scrive 1 byte su SP+1 byte offset *)
-  | MODE_SP1        ⇒ mode_SP1_write m t true s cur_pc writeb
+  | MODE_SP1        ⇒ mode_SP1_write true m t s cur_pc writeb
 (* scrive 1 byte su SP+1 word offset *)
-  | MODE_SP2        ⇒ mode_SP2_write m t true s cur_pc writeb
+  | MODE_SP2        ⇒ mode_SP2_write true m t s cur_pc writeb
 
 (* passo2: scrittura su DIR1, passo1: lettura da DIR1 *)
-  | MODE_DIR1_to_DIR1   ⇒ mode_DIR1_write m t true s cur_pc writeb
+  | MODE_DIR1_to_DIR1   ⇒ mode_DIR1_write true m t s cur_pc writeb
 (* passo2: scrittura su DIR1, passo1: lettura da IMM1 *)
-  | MODE_IMM1_to_DIR1   ⇒ mode_DIR1_write m t true s cur_pc writeb
+  | MODE_IMM1_to_DIR1   ⇒ mode_DIR1_write true m t s cur_pc writeb
 (* passo2: scrittura su DIR1 e X++, passo1: lettura da IX0 *)
-  | MODE_IX0p_to_DIR1   ⇒ opt_map ?? (mode_DIR1_write m t true s cur_pc writeb)
+  | MODE_IX0p_to_DIR1   ⇒ opt_map ?? (mode_DIR1_write true m t s cur_pc writeb)
                            (λS_and_PC.match S_and_PC with [ pair S_op PC_op ⇒
                             (* H:X++ *)
                             opt_map ?? (aux_inc_indX_16 m t S_op)
                              (λS_op'.Some ? (pair ?? S_op' PC_op))])
 (* passo2: scrittura su IX0 e X++, passo1: lettura da DIR1 *)
-  | MODE_DIR1_to_IX0p   ⇒ opt_map ?? (mode_IX0_write m t true s cur_pc writeb)
+  | MODE_DIR1_to_IX0p   ⇒ opt_map ?? (mode_IX0_write true m t s cur_pc writeb)
                            (λS_and_PC.match S_and_PC with [ pair S_op PC_op ⇒
                             (* H:X++ *)
                             opt_map ?? (aux_inc_indX_16 m t S_op)
@@ -848,17 +848,17 @@ definition multi_mode_write ≝
 (* NO: solo lettura word *) 
   | MODE_IMM1_and_IMM1 ⇒ None ?
 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = DIR1 *) 
-  | MODE_DIR1_and_IMM1 ⇒ mode_DIR1_write m t true s cur_pc writeb
+  | MODE_DIR1_and_IMM1 ⇒ mode_DIR1_write true m t s cur_pc writeb
 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = IX0 *)
-  | MODE_IX0_and_IMM1  ⇒ mode_IX0_write m t true s cur_pc writeb
+  | MODE_IX0_and_IMM1  ⇒ mode_IX0_write true m t s cur_pc writeb
 (* NO: solo lettura word *) 
   | MODE_IX0p_and_IMM1 ⇒ None ?
 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = IX1 *)
-  | MODE_IX1_and_IMM1  ⇒ mode_IX1_write m t true s cur_pc writeb
+  | MODE_IX1_and_IMM1  ⇒ mode_IX1_write true m t s cur_pc writeb
 (* NO: solo lettura word *) 
   | MODE_IX1p_and_IMM1 ⇒ None ?
 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = SP1 *)
-  | MODE_SP1_and_IMM1  ⇒ mode_SP1_write m t true s cur_pc writeb
+  | MODE_SP1_and_IMM1  ⇒ mode_SP1_write true m t s cur_pc writeb
 
 (* scrive 1 byte, ma la scrittura avviene solo per n-simo bit = leggi/modifica bit/scrivi *)
   | MODE_DIRn msk ⇒ mode_DIR1n_write m t s cur_pc msk (getn_array8T msk bool (bits_of_byte8 writeb))   
@@ -895,19 +895,19 @@ definition multi_mode_write ≝
 (* NO: solo lettura word *)
   | MODE_IMM2       ⇒ None ?
 (* scrive 1 word su indirizzo diretto 1 byte *) 
-  | MODE_DIR1       ⇒ mode_DIR1_write m t false s cur_pc writew
+  | MODE_DIR1       ⇒ mode_DIR1_write false m t s cur_pc writew
 (* scrive 1 word su indirizzo diretto 1 word *)
-  | MODE_DIR2       ⇒ mode_DIR2_write m t false s cur_pc writew
+  | MODE_DIR2       ⇒ mode_DIR2_write false m t s cur_pc writew
 (* scrive 1 word su H:X *)
-  | MODE_IX0        ⇒ mode_IX0_write m t false s cur_pc writew
+  | MODE_IX0        ⇒ mode_IX0_write false m t s cur_pc writew
 (* scrive 1 word su H:X+1 byte offset *)
-  | MODE_IX1        ⇒ mode_IX1_write m t false s cur_pc writew
+  | MODE_IX1        ⇒ mode_IX1_write false m t s cur_pc writew
 (* scrive 1 word su H:X+1 word offset *)
-  | MODE_IX2        ⇒ mode_IX2_write m t false s cur_pc writew
+  | MODE_IX2        ⇒ mode_IX2_write false m t s cur_pc writew
 (* scrive 1 word su SP+1 byte offset *)
-  | MODE_SP1        ⇒ mode_SP1_write m t false s cur_pc writew
+  | MODE_SP1        ⇒ mode_SP1_write false m t s cur_pc writew
 (* scrive 1 word su SP+1 word offset *)
-  | MODE_SP2        ⇒ mode_SP2_write m t false s cur_pc writew
+  | MODE_SP2        ⇒ mode_SP2_write false m t s cur_pc writew
 
 (* NO: solo lettura/scrittura byte *)
   | MODE_DIR1_to_DIR1 ⇒ None ?