From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 25 Mar 2008 13:23:33 +0000 (+0000)
Subject: argument of type mcu_type always abstracted first
X-Git-Tag: make_still_working~5501
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=84ef7e61acf6d6bc785fced0ed5790897f86c746;p=helm.git

argument of type mcu_type always abstracted first
---

diff --git a/helm/software/matita/contribs/assembly/freescale/load_write.ma b/helm/software/matita/contribs/assembly/freescale/load_write.ma
index 28c78b6bb..b288f9863 100644
--- 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 ≝
-λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+λm:mcu_type.λt:memory_impl.λbyteflag:bool.λ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 ≝
-λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+λm:mcu_type.λt:memory_impl.λbyteflag:bool.λ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 ≝
-λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+λm:mcu_type.λt:memory_impl.λbyteflag:bool.λ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 ≝
-λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+λm:mcu_type.λt:memory_impl.λbyteflag:bool.λ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 ≝
-λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+λm:mcu_type.λt:memory_impl.λbyteflag:bool.λ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 ≝
-λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+λm:mcu_type.λt:memory_impl.λbyteflag:bool.λ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 ≝
-λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+λm:mcu_type.λt:memory_impl.λbyteflag:bool.λ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 ≝
-λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+λm:mcu_type.λt:memory_impl.λbyteflag:bool.λ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 ≝
-λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+λm:mcu_type.λt:memory_impl.λbyteflag:bool.λ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 ≝
-λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+λm:mcu_type.λt:memory_impl.λbyteflag:bool.λ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 ≝
-λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+λm:mcu_type.λt:memory_impl.λbyteflag:bool.λ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 ≝
-λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+λm:mcu_type.λt:memory_impl.λbyteflag:bool.λ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 ≝
-λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+λm:mcu_type.λt:memory_impl.λbyteflag:bool.λ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 ≝
-λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+λm:mcu_type.λt:memory_impl.λbyteflag:bool.λ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 ≝
-λbyteflag:bool.λm:mcu_type.λt:memory_impl.
+λm:mcu_type.λt:memory_impl.λbyteflag:bool.
  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 true m t s cur_pc
+   | MODE_DIR1 ⇒ mode_DIR1_load m t true s cur_pc
 (* preleva 1 byte da indirizzo diretto 1 word *)
-   | MODE_DIR2 ⇒ mode_DIR2_load true m t s cur_pc
+   | MODE_DIR2 ⇒ mode_DIR2_load m t true s cur_pc
 (* preleva 1 byte da H:X *)
-   | MODE_IX0  ⇒ mode_IX0_load true m t s cur_pc
+   | MODE_IX0  ⇒ mode_IX0_load m t true s cur_pc
 (* preleva 1 byte da H:X+1 byte offset *)
-   | MODE_IX1  ⇒ mode_IX1_load true m t s cur_pc
+   | MODE_IX1  ⇒ mode_IX1_load m t true s cur_pc
 (* preleva 1 byte da H:X+1 word offset *)
-   | MODE_IX2  ⇒ mode_IX2_load true m t s cur_pc
+   | MODE_IX2  ⇒ mode_IX2_load m t true s cur_pc
 (* preleva 1 byte da SP+1 byte offset *)
-   | MODE_SP1  ⇒ mode_SP1_load true m t s cur_pc
+   | MODE_SP1  ⇒ mode_SP1_load m t true s cur_pc
 (* preleva 1 byte da SP+1 word offset *)
-   | MODE_SP2  ⇒ mode_SP2_load true m t s cur_pc
+   | MODE_SP2  ⇒ mode_SP2_load m t true s cur_pc
 
 (* come DIR1, chiamare scrittura per passo2: scrittura su DIR1 *)
-   | MODE_DIR1_to_DIR1 ⇒ mode_DIR1_load true m t s cur_pc
+   | MODE_DIR1_to_DIR1 ⇒ mode_DIR1_load m t true 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 true m t s cur_pc
+   | MODE_IX0p_to_DIR1 ⇒ mode_IX0_load m t true s cur_pc
 (* come DIR1, chiamare scrittura per passo2: scrittura su IX0 e X++ *)
-   | MODE_DIR1_to_IX0p ⇒ mode_DIR1_load true m t s cur_pc
+   | MODE_DIR1_to_IX0p ⇒ mode_DIR1_load m t true 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 false m t s cur_pc
+   | MODE_DIR1 ⇒ mode_DIR1_load m t false s cur_pc
 (* preleva 1 word da indirizzo diretto 1 word *) 
-   | MODE_DIR2 ⇒ mode_DIR2_load false m t s cur_pc
+   | MODE_DIR2 ⇒ mode_DIR2_load m t false s cur_pc
 (* preleva 1 word da H:X *)
-   | MODE_IX0  ⇒ mode_IX0_load false m t s cur_pc
+   | MODE_IX0  ⇒ mode_IX0_load m t false s cur_pc
 (* preleva 1 word da H:X+1 byte offset *)
-   | MODE_IX1  ⇒ mode_IX1_load false m t s cur_pc
+   | MODE_IX1  ⇒ mode_IX1_load m t false s cur_pc
 (* preleva 1 word da H:X+1 word offset *)
-   | MODE_IX2  ⇒ mode_IX2_load false m t s cur_pc
+   | MODE_IX2  ⇒ mode_IX2_load m t false s cur_pc
 (* preleva 1 word da SP+1 byte offset *)
-   | MODE_SP1  ⇒ mode_SP1_load false m t s cur_pc
+   | MODE_SP1  ⇒ mode_SP1_load m t false s cur_pc
 (* preleva 1 word da SP+1 word offset *)
-   | MODE_SP2  ⇒ mode_SP2_load false m t s cur_pc
+   | MODE_SP2  ⇒ mode_SP2_load m t false 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 true m t s cur_pc)
+   | MODE_DIR1_and_IMM1 ⇒ opt_map ?? (mode_DIR1_load m t true 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 true m t s cur_pc)
+   | MODE_IX0_and_IMM1  ⇒ opt_map ?? (mode_IX0_load m t true 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 true m t s cur_pc)
+   | MODE_IX0p_and_IMM1 ⇒ opt_map ?? (mode_IX0_load m t true 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 true m t s cur_pc)
+   | MODE_IX1_and_IMM1  ⇒ opt_map ?? (mode_IX1_load m t true 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 true m t s cur_pc)
+   | MODE_IX1p_and_IMM1 ⇒ opt_map ?? (mode_IX1_load m t true 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 true m t s cur_pc)
+   | MODE_SP1_and_IMM1  ⇒ opt_map ?? (mode_SP1_load m t true 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 ≝
-λbyteflag:bool.λm:mcu_type.λt:memory_impl.match byteflag
+λm:mcu_type.λt:memory_impl.λbyteflag:bool.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 true m t s cur_pc writeb
+  | MODE_DIR1       ⇒ mode_DIR1_write m t true s cur_pc writeb
 (* scrive 1 byte su indirizzo diretto 1 word *)
-  | MODE_DIR2       ⇒ mode_DIR2_write true m t s cur_pc writeb
+  | MODE_DIR2       ⇒ mode_DIR2_write m t true s cur_pc writeb
 (* scrive 1 byte su H:X *)
-  | MODE_IX0        ⇒ mode_IX0_write true m t s cur_pc writeb
+  | MODE_IX0        ⇒ mode_IX0_write m t true s cur_pc writeb
 (* scrive 1 byte su H:X+1 byte offset *)
-  | MODE_IX1        ⇒ mode_IX1_write true m t s cur_pc writeb
+  | MODE_IX1        ⇒ mode_IX1_write m t true s cur_pc writeb
 (* scrive 1 byte su H:X+1 word offset *)
-  | MODE_IX2        ⇒ mode_IX2_write true m t s cur_pc writeb
+  | MODE_IX2        ⇒ mode_IX2_write m t true s cur_pc writeb
 (* scrive 1 byte su SP+1 byte offset *)
-  | MODE_SP1        ⇒ mode_SP1_write true m t s cur_pc writeb
+  | MODE_SP1        ⇒ mode_SP1_write m t true s cur_pc writeb
 (* scrive 1 byte su SP+1 word offset *)
-  | MODE_SP2        ⇒ mode_SP2_write true m t s cur_pc writeb
+  | MODE_SP2        ⇒ mode_SP2_write m t true s cur_pc writeb
 
 (* passo2: scrittura su DIR1, passo1: lettura da DIR1 *)
-  | MODE_DIR1_to_DIR1   ⇒ mode_DIR1_write true m t s cur_pc writeb
+  | MODE_DIR1_to_DIR1   ⇒ mode_DIR1_write m t true s cur_pc writeb
 (* passo2: scrittura su DIR1, passo1: lettura da IMM1 *)
-  | MODE_IMM1_to_DIR1   ⇒ mode_DIR1_write true m t s cur_pc writeb
+  | MODE_IMM1_to_DIR1   ⇒ mode_DIR1_write m t true s cur_pc writeb
 (* passo2: scrittura su DIR1 e X++, passo1: lettura da IX0 *)
-  | MODE_IX0p_to_DIR1   ⇒ opt_map ?? (mode_DIR1_write true m t s cur_pc writeb)
+  | MODE_IX0p_to_DIR1   ⇒ opt_map ?? (mode_DIR1_write m t true 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 true m t s cur_pc writeb)
+  | MODE_DIR1_to_IX0p   ⇒ opt_map ?? (mode_IX0_write m t true 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 true m t s cur_pc writeb
+  | MODE_DIR1_and_IMM1 ⇒ mode_DIR1_write m t true s cur_pc writeb
 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = IX0 *)
-  | MODE_IX0_and_IMM1  ⇒ mode_IX0_write true m t s cur_pc writeb
+  | MODE_IX0_and_IMM1  ⇒ mode_IX0_write m t true 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 true m t s cur_pc writeb
+  | MODE_IX1_and_IMM1  ⇒ mode_IX1_write m t true 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 true m t s cur_pc writeb
+  | MODE_SP1_and_IMM1  ⇒ mode_SP1_write m t true 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 false m t s cur_pc writew
+  | MODE_DIR1       ⇒ mode_DIR1_write m t false s cur_pc writew
 (* scrive 1 word su indirizzo diretto 1 word *)
-  | MODE_DIR2       ⇒ mode_DIR2_write false m t s cur_pc writew
+  | MODE_DIR2       ⇒ mode_DIR2_write m t false s cur_pc writew
 (* scrive 1 word su H:X *)
-  | MODE_IX0        ⇒ mode_IX0_write false m t s cur_pc writew
+  | MODE_IX0        ⇒ mode_IX0_write m t false s cur_pc writew
 (* scrive 1 word su H:X+1 byte offset *)
-  | MODE_IX1        ⇒ mode_IX1_write false m t s cur_pc writew
+  | MODE_IX1        ⇒ mode_IX1_write m t false s cur_pc writew
 (* scrive 1 word su H:X+1 word offset *)
-  | MODE_IX2        ⇒ mode_IX2_write false m t s cur_pc writew
+  | MODE_IX2        ⇒ mode_IX2_write m t false s cur_pc writew
 (* scrive 1 word su SP+1 byte offset *)
-  | MODE_SP1        ⇒ mode_SP1_write false m t s cur_pc writew
+  | MODE_SP1        ⇒ mode_SP1_write m t false s cur_pc writew
 (* scrive 1 word su SP+1 word offset *)
-  | MODE_SP2        ⇒ mode_SP2_write false m t s cur_pc writew
+  | MODE_SP2        ⇒ mode_SP2_write m t false s cur_pc writew
 
 (* NO: solo lettura/scrittura byte *)
   | MODE_DIR1_to_DIR1 ⇒ None ?
diff --git a/helm/software/matita/contribs/assembly/freescale/multivm.ma b/helm/software/matita/contribs/assembly/freescale/multivm.ma
index b78efba70..00de15cfa 100644
--- a/helm/software/matita/contribs/assembly/freescale/multivm.ma
+++ b/helm/software/matita/contribs/assembly/freescale/multivm.ma
@@ -45,7 +45,7 @@ include "freescale/load_write.ma".
 definition 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 → Prod byte8 bool.
- opt_map ?? (multi_mode_load true m t s cur_pc i)
+ opt_map ?? (multi_mode_load m t true s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
     let A_op ≝ get_acc_8_low_reg m t s_tmp1 in
@@ -74,7 +74,7 @@ definition execute_ADC_ADD_aux ≝
 definition 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 m t true s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
     let R_op ≝ fAM (get_acc_8_low_reg m t s_tmp1) M_op in
@@ -94,12 +94,12 @@ definition execute_AND_BIT_EOR_ORA_aux ≝
 definition 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 → Prod byte8 bool.
- opt_map ?? (multi_mode_load true m t s cur_pc i)
+ opt_map ?? (multi_mode_load m t true s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT 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 m t true s_tmp1 cur_pc i R_op)
      (λS_PC.match S_PC with
       [ pair s_tmp2 new_pc ⇒
       (* C = carry *)
@@ -126,7 +126,7 @@ definition branched_pc ≝
 (* tutti i branch calcoleranno la condizione e la passeranno qui *)
 definition 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 m t true s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
     (* if true, branch *) 
@@ -141,7 +141,7 @@ definition execute_any_BRANCH ≝
 definition 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 m t true s cur_pc i optval)
   (λS_PC.match S_PC with
    (* newpc = nextpc *)
    [ pair s_tmp1 new_pc ⇒ Some ? (pair ?? s_tmp1 new_pc) ]).
@@ -150,7 +150,7 @@ definition execute_BCLRn_BSETn_aux ≝
 (* il chiamante passa la logica da testare (0x00,¬0x00) e poi si salta *)
 definition 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 m t false s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒ match M_op with
     [ mk_word16 MH_op ML_op ⇒
@@ -166,12 +166,12 @@ definition execute_BRCLRn_BRSETn_aux ≝
 definition 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 m t true s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT 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 m t true s_tmp1 cur_pc i R_op)
      (λS_PC.match S_PC with
       [ pair s_tmp2 new_pc ⇒
       (* C = fCR (C,R) *)
@@ -191,7 +191,7 @@ definition execute_COM_DEC_INC_NEG_aux ≝
 definition 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 → Prod byte8 bool.
- opt_map ?? (multi_mode_load true m t s cur_pc i)
+ opt_map ?? (multi_mode_load m t true s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
     let A_op ≝ get_acc_8_low_reg m t s_tmp1 in
@@ -282,7 +282,7 @@ definition execute_ADD ≝
 (* SP += extended M *)
 definition 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 m t true s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
    opt_map ?? (get_sp_reg m t s_tmp1)
@@ -293,7 +293,7 @@ definition execute_AIS ≝
 (* H:X += extended M *)
 definition 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 m t true s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
    opt_map ?? (get_indX_16_reg m t s_tmp1)
@@ -468,7 +468,7 @@ definition execute_BSETn ≝
 (* HC05/HC08/HCS08 si appoggiano allo stack, RS08 a SPC *)
 definition 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 m t true s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒ let aux ≝
     (* push (new_pc low) *)
@@ -489,7 +489,7 @@ definition execute_BSR ≝
 (* if A=M, branch *)
 definition 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 m t false s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
     match M_op with
@@ -505,7 +505,7 @@ definition execute_CBEQA ≝
 (* if X=M, branch *)
 definition 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 m t false s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
     match M_op with
@@ -534,7 +534,7 @@ definition execute_CLI ≝
 definition 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 m t true s cur_pc i 〈x0,x0〉)
   (λS_PC.match S_PC with
    [ pair s_tmp1 new_pc ⇒
    (* Z = 1 *)
@@ -563,7 +563,7 @@ definition execute_COM ≝
 (* flags = H:X - M *)
 definition 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 m t false s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
     opt_map ?? (get_indX_16_reg m t s_tmp1)
@@ -585,7 +585,7 @@ definition execute_CPHX ≝
 (* flags = X - M *)
 definition 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 m t true s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
     opt_map ?? (get_indX_8_low_reg m t s_tmp1)
@@ -629,14 +629,14 @@ definition execute_DAA ≝
 (* if (--M)≠0, branch *)
 definition 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 m t false s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT 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 m t true s_tmp1 cur_pc i MH_op')
       (λS_PC.match S_PC with
        [ pair s_tmp2 _ ⇒
         (* if (--M)≠0, branch *)
@@ -695,7 +695,7 @@ definition execute_INC ≝
 (* jmp, il nuovo indirizzo e' una WORD *)
 definition 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 m t false s cur_pc i)
   (λS_M_PC.
    (* newpc = M_op *)
    Some ? (pair ?? (fst3T ??? S_M_PC) (snd3T ??? S_M_PC))).
@@ -704,7 +704,7 @@ definition execute_JMP ≝
 (* HC05/HC08/HCS08 si appoggiano allo stack, RS08 a SPC *)
 definition 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 m t false s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒ let aux ≝
     (* push (new_pc low) *)
@@ -725,7 +725,7 @@ definition execute_JSR ≝
 (* A = M *)
 definition 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 m t true s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
     (* A = M *) 
@@ -742,7 +742,7 @@ definition execute_LDA ≝
 (* H:X = M *)
 definition 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 m t false s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
     opt_map ?? (set_indX_16_reg m t s_tmp1 M_op)
@@ -759,7 +759,7 @@ definition execute_LDHX ≝
 (* X = M *)
 definition 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 m t true s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
     opt_map ?? (set_indX_8_low_reg m t s_tmp1 M_op)
@@ -782,11 +782,11 @@ definition execute_LSR ≝
 definition 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 m t true s cur_pc i)
   (λS_R_PC.match S_R_PC with
    [ tripleT 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 m t true 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 *)
@@ -983,7 +983,7 @@ definition 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 m t true 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 *)
@@ -1000,7 +1000,7 @@ definition 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)
+  (λX_op.opt_map ?? (multi_mode_write m t false 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 *)
@@ -1022,7 +1022,7 @@ definition 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)
+  (λX_op.opt_map ?? (multi_mode_write m t true 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 *)
@@ -1085,7 +1085,7 @@ definition execute_TPA ≝
    e' immediata *)
 definition 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 m t true s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
     (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)