1) \ldots here and there

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / medium_tests.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/medium_tests.ma b/helm/software/matita/contribs/ng_assembly/freescale/medium_tests.ma
index 54004c4447184b0eba20227bead788fc5a97b5ba..04ceeaa5e1d90344207a85f3af38b5f592a2096d 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/medium_tests.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/medium_tests.ma
@@ -160,7 +160,7 @@ nlemma dTest_HCS08_sReverse_dump_aux ≝
    [ TickERR s _ ⇒ None ?
    (* azzeramento tutta RAM tranne dati *)
    | TickSUSP s _ ⇒ None ? 
-   | TickOK s ⇒ Some ? (byte8_hexdump t (get_mem_desc HCS08 t s) dTest_HCS08_RAM (nat_of_word16 (byte8_strlen string)))
+   | TickOK s ⇒ Some ? (byte8_hexdump t (mem_desc HCS08 t s) dTest_HCS08_RAM (nat_of_word16 (byte8_strlen string)))
    ] =
   Some ? (reverse_list ? string)).
 
@@ -192,10 +192,10 @@ nlemma dTest_HCS08_sReverse_aux ≝
    [ TickERR s _ ⇒ None ?
    (* azzeramento tutta RAM tranne dati *)
    | TickSUSP s _ ⇒ None ? 
-   | TickOK s ⇒ Some ? (set_mem_desc HCS08 t s (load_from_source_at t (get_mem_desc HCS08 t s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
+   | TickOK s ⇒ Some ? (set_mem_desc HCS08 t s (load_from_source_at t (mem_desc HCS08 t s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
    ] =
   Some ? (set_pc_reg HCS08 t
-   (dTest_HCS08_sReverse_status t (fst ?? (shr_b8 (w16h (byte8_strlen string)))) (fst ?? (shr_w16 (byte8_strlen string))) (byte8_strlen string) (reverse_list ? string)) 
+   (dTest_HCS08_sReverse_status t (fst … (shr_b8 (w16h (byte8_strlen string)))) (fst … (shr_w16 (byte8_strlen string))) (byte8_strlen string) (reverse_list ? string)) 
    (mk_word16 (mk_byte8 x1 x9) (mk_byte8 x2 xB)))).
 
 (*
@@ -233,14 +233,14 @@ ndefinition sReverseCalc ≝
   (42+79*(nat_of_word16 (byte8_strlen string))+5*((nat_of_word16 (byte8_strlen string))/512)) with
    [ TickERR s _ ⇒ None ?
    | TickSUSP s _ ⇒ None ? 
-   | TickOK s ⇒ Some ? (set_mem_desc HCS08 MEM_TREE s (load_from_source_at MEM_TREE (get_mem_desc HCS08 MEM_TREE s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
+   | TickOK s ⇒ Some ? (set_mem_desc HCS08 MEM_TREE s (load_from_source_at MEM_TREE (mem_desc HCS08 MEM_TREE s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
    ]. 
 
 ndefinition sReverseNoCalc ≝
 λstring:list byte8.
  Some ? (set_pc_reg HCS08 MEM_TREE
-   (dTest_HCS08_sReverse_status MEM_TREE (fst ?? (shr_b8 (w16h (byte8_strlen string))))
-                                         (fst ?? (shr_w16 (byte8_strlen string)))
+   (dTest_HCS08_sReverse_status MEM_TREE (fst … (shr_b8 (w16h (byte8_strlen string))))
+                                         (fst … (shr_w16 (byte8_strlen string)))
                                          (byte8_strlen string) (reverse_list ? string)) 
    (mk_word16 (mk_byte8 x1 x9) (mk_byte8 x2 xB))).
 
@@ -411,7 +411,7 @@ nlemma dTest_HCS08_cSort_aux ≝
   ((nat_of_word16 〈〈x6,x4〉:〈x6,x4〉〉)+(nat_of_byte8 〈x9,x6〉)*(nat_of_word16 (byte8_strlen string))) with
    [ TickERR s _ ⇒ None ?
    (* azzeramento tutta RAM tranne dati *)
-   | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 t s (load_from_source_at t (get_mem_desc HCS08 t s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
+   | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 t s (load_from_source_at t (mem_desc HCS08 t s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
    | TickOK s ⇒ None ?
    ] =
   Some ? (set_pc_reg HCS08 t
@@ -435,7 +435,7 @@ ndefinition cSortCalc ≝
   (TickOK ? (dTest_HCS08_cSort_status MEM_TREE true 〈x0,x0〉 〈〈x0,xF〉:〈x4,xC〉〉 (byte8_strlen string) string))
   ((nat_of_word16 〈〈x6,x4〉:〈x6,x4〉〉)+(nat_of_byte8 〈x9,x6〉)*(nat_of_word16 (byte8_strlen string))) with
    [ TickERR s _ ⇒ None ?
-   | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 MEM_TREE s (load_from_source_at MEM_TREE (get_mem_desc HCS08 MEM_TREE s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
+   | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 MEM_TREE s (load_from_source_at MEM_TREE (mem_desc HCS08 MEM_TREE s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
    | TickOK s ⇒ None ?
    ].
 
@@ -844,7 +844,7 @@ nlemma dTest_HCS08_gNum_aux ≝
   (nat_of_word16 num) with
    [ TickERR s _ ⇒ None ?
    (* azzeramento tutta RAM tranne dati *)
-   | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 t s (load_from_source_at t (get_mem_desc HCS08 t s) dTest_zeros3K 〈〈x0,x1〉:〈x2,x0〉〉))
+   | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 t s (load_from_source_at t (mem_desc HCS08 t s) dTest_zeros3K 〈〈x0,x1〉:〈x2,x0〉〉))
    | TickOK s ⇒ None ?
    ] =
   Some ? (dTest_HCS08_gNum_status t false 〈x0,x0〉 num 〈〈x1,x9〉:〈x5,x1〉〉 〈〈x1,x8〉:〈xB,xE〉〉 num (dTest_HCS08_gNum_aurei num)).
@@ -855,7 +855,7 @@ ndefinition gNumCalc ≝
   (TickOK ? (dTest_HCS08_gNum_status MEM_TREE true 〈x0,x0〉 〈〈x1,xA〉:〈x0,x0〉〉 〈〈x1,x8〉:〈xB,xE〉〉 〈〈x1,x8〉:〈xB,xE〉〉 num dTest_zeros))
   (nat_of_word16 num) with
    [ TickERR s _ ⇒ None ?
-   | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 MEM_TREE s (load_from_source_at MEM_TREE (get_mem_desc HCS08 MEM_TREE s) dTest_zeros3K 〈〈x0,x1〉:〈x2,x0〉〉))
+   | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 MEM_TREE s (load_from_source_at MEM_TREE (mem_desc HCS08 MEM_TREE s) dTest_zeros3K 〈〈x0,x1〉:〈x2,x0〉〉))
    | TickOK s ⇒ None ?
    ].