1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* Questo materiale fa parte della tesi: *)
22 (* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
24 (* data ultima modifica 15/11/2007 *)
25 (* ********************************************************************** *)
27 set "baseuri" "cic:/matita/freescale/medium_tests_tools/".
29 (*include "/media/VIRTUOSO/freescale/multivm.ma".*)
30 include "freescale/multivm.ma".
36 (* specifico per MC9S08GB60 in modo da caricare codice compilato da CodeWarrior *)
37 (* l'obbiettivo e' dimostrare una routine scritta in C *)
38 (* passo 1 e' formalizzare l'uso di 3Kb dei 4Kb di RAM [0x0100-0x0CFF] *)
39 definition dTest_HCS08_RAM ≝ 〈〈x0,x1〉:〈x0,x0〉〉.
40 definition dTest_HCS08_prog ≝ 〈〈x1,x8〉:〈xC,x8〉〉.
46 (* visita di un albero da 256B di elementi: ln16(256)=2 passaggi *)
47 definition dTest_visit ≝
48 λdata:Prod16T (Prod16T (list byte8)).λaddr:byte8.
49 getn_array16T (b8l addr) ?
50 (getn_array16T (b8h addr) ? data).
52 (* scrittura di un elemento in un albero da 256B *)
53 definition dTest_update ≝
54 λdata:Prod16T (Prod16T (list byte8)).λaddr:byte8.λv:list byte8.
55 let lev2 ≝ getn_array16T (b8h addr) ? data in
56 setn_array16T (b8h addr) ? data
57 (setn_array16T (b8l addr) ? lev2 v) .
60 definition dTest_zero_array ≝
61 let elem ≝ nil byte8 in
62 let lev2 ≝ array_16T ?
63 elem elem elem elem elem elem elem elem
64 elem elem elem elem elem elem elem elem
66 let lev1 ≝ array_16T ?
67 lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
68 lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
72 (* incrementa n-simo elemento *)
73 definition dTest_inc ≝
74 λdata:Prod16T (Prod16T (list byte8)).λaddr:byte8.
75 dTest_update data addr ((dTest_visit data addr)@[ addr ]).
77 (* costruisce una lista a partire dai conteggi per elemento *)
78 definition dTest_build_list_from_count ≝
79 λdata:Prod16T (Prod16T (list byte8)).
80 let aux1 ≝ λparam1:Prod16T (list byte8).
82 [ array_16T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 ⇒
83 e00@e01@e02@e03@e04@e05@e06@e07@e08@e09@e10@e11@e12@e13@e14@e15 ] in
84 let aux2 ≝ λparam2:Prod16T (Prod16T (list byte8)).
86 [ array_16T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 ⇒
87 (aux1 e00)@(aux1 e01)@(aux1 e02)@(aux1 e03)@(aux1 e04)@(aux1 e05)@(aux1 e06)@(aux1 e07)@
88 (aux1 e08)@(aux1 e09)@(aux1 e10)@(aux1 e11)@(aux1 e12)@(aux1 e13)@(aux1 e14)@(aux1 e15) ] in
91 (* ci sono ora tutti gli elementi per definire l'ordinamento *)
92 (* di una lista di byte8 secondo il counting sort *)
93 let rec byte8_list_ordering_aux (source:list byte8) (count:Prod16T (Prod16T (list byte8))) on source ≝
95 [ nil ⇒ dTest_build_list_from_count count
96 | cons hd tl ⇒ byte8_list_ordering_aux tl (dTest_inc count hd)
99 definition byte8_list_ordering ≝
100 λsource:list byte8.byte8_list_ordering_aux source dTest_zero_array.
102 (* strlen esadecimale limitato, considerando overflow! *)
103 let rec byte8_bounded_strlen_aux (source:list byte8) (count,limit:word16) on source ≝
106 | cons _ tl ⇒ match eq_w16 count 〈〈xF,xF〉:〈xF,xF〉〉 with
108 | false ⇒ match le_w16 (succ_w16 count) limit with
109 [ true ⇒ byte8_bounded_strlen_aux tl (succ_w16 count) limit
115 definition byte8_bounded_strlen ≝
116 λsource:list byte8.λlimit:word16.
117 byte8_bounded_strlen_aux source 〈〈x0,x0〉:〈x0,x0〉〉 limit.
119 (* strlen esadecimale normale *)
120 let rec byte8_strlen_aux (source:list byte8) (count:word16) on source ≝
123 | cons _ tl ⇒ byte8_strlen_aux tl (succ_w16 count)
126 definition byte8_strlen ≝
128 byte8_strlen_aux source 〈〈x0,x0〉:〈x0,x0〉〉.
131 let rec byte8_reverse (source:list byte8) on source ≝
132 match source return λ_.list byte8 with
134 | cons hd tl ⇒ (byte8_reverse tl)@[ hd ]
137 (* hex dump: memory -> list byte8 *)
138 let rec byte8_hexdump_aux (t:memory_impl) (mem:aux_mem_type t) (inf:word16) (count:nat) (out:list byte8) on count ≝
141 | S n ⇒ byte8_hexdump_aux t mem (succ_w16 inf) n (out@[ mem_read_abs t mem inf ])
144 definition byte8_hexdump ≝
145 λt:memory_impl.λmem:aux_mem_type t.λinf:word16.λcount:nat.
146 byte8_hexdump_aux t mem inf count [].
152 (* lista di 3072 numeri random generati da Mathematica, in blocchi da 256, per velocita' di parsing *)
153 definition dTest_random_ex01a ≝
155 〈x8,x1〉;〈x5,xE〉;〈x7,x6〉;〈xD,x1〉;〈x7,x5〉;〈x1,x0〉;〈x8,x5〉;〈x9,x0〉;〈x1,xF〉;〈x1,x2〉;〈xE,x2〉;〈x3,xC〉;〈x1,xD〉;〈x0,x6〉;〈x3,xC〉;〈xD,x1〉;
156 〈x8,x3〉;〈xE,xB〉;〈x7,x2〉;〈x1,xF〉;〈x9,x0〉;〈xF,x0〉;〈x4,x7〉;〈xA,x3〉;〈xD,x0〉;〈x4,x6〉;〈xC,x5〉;〈x3,x2〉;〈xC,x9〉;〈x0,xB〉;〈x1,xB〉;〈x7,x3〉
159 definition dTest_random_ex01b ≝
161 〈x1,x1〉;〈xA,xF〉;〈xD,x2〉;〈xB,xF〉;〈x0,xB〉;〈xB,xC〉;〈x0,x8〉;〈xE,x5〉;〈xF,xE〉;〈xA,xC〉;〈xF,xC〉;〈x9,x4〉;〈x3,x4〉;〈x8,x8〉;〈x2,x8〉;〈xD,xB〉;
162 〈xD,x3〉;〈x3,xD〉;〈x3,x8〉;〈x6,xA〉;〈x4,xD〉;〈x7,x4〉;〈x4,x9〉;〈x7,xE〉;〈x6,xF〉;〈x4,xD〉;〈x3,xD〉;〈x3,xA〉;〈xC,x2〉;〈xD,x3〉;〈x3,x6〉;〈x7,x0〉
165 definition dTest_random_ex01c ≝
167 〈x8,x0〉;〈xC,x9〉;〈x3,xB〉;〈x5,x2〉;〈x8,xF〉;〈x1,xE〉;〈x8,x4〉;〈x5,x2〉;〈x2,xD〉;〈xA,xF〉;〈x1,xB〉;〈x0,x1〉;〈x3,x5〉;〈x7,x2〉;〈x1,x0〉;〈x0,x7〉;
168 〈x5,xD〉;〈xA,xB〉;〈xE,x0〉;〈x7,x6〉;〈xB,xD〉;〈x3,xC〉;〈x0,xD〉;〈xC,xE〉;〈xB,x7〉;〈x9,xD〉;〈xA,x9〉;〈xF,x3〉;〈xC,x1〉;〈x9,x3〉;〈x8,xC〉;〈x4,xE〉;
169 〈xF,x8〉;〈xC,x3〉;〈x1,x3〉;〈x3,xA〉;〈xA,x2〉;〈xB,xD〉;〈x1,x0〉;〈x9,xB〉;〈x5,xC〉;〈xC,x8〉;〈xE,x5〉;〈xC,x8〉;〈xA,x6〉;〈xF,xB〉;〈x1,x3〉;〈xC,x8〉;
170 〈x6,x4〉;〈x0,x9〉;〈xD,x6〉;〈xD,x7〉;〈x3,x9〉;〈xF,x9〉;〈xE,x4〉;〈x0,x3〉;〈x4,x9〉;〈xC,xE〉;〈x7,x1〉;〈x5,x7〉;〈x3,x4〉;〈x2,xE〉;〈xA,x3〉;〈x5,x3〉
173 definition dTest_random_ex01d ≝
175 〈xF,x9〉;〈x2,xA〉;〈xF,x0〉;〈xE,x1〉;〈x6,x6〉;〈x8,x9〉;〈x2,xE〉;〈x8,x6〉;〈xC,x7〉;〈x2,xD〉;〈x1,x2〉;〈xD,x5〉;〈x4,xA〉;〈x7,x9〉;〈x6,xD〉;〈x1,xB〉;
176 〈x4,x1〉;〈x9,x4〉;〈x6,xC〉;〈x6,xD〉;〈xF,x4〉;〈x5,xD〉;〈x8,xB〉;〈xB,xE〉;〈xC,x8〉;〈xE,x5〉;〈xA,x4〉;〈xB,xA〉;〈xB,x1〉;〈x2,x1〉;〈x5,x0〉;〈x6,xB〉;
177 〈x9,x5〉;〈x0,x6〉;〈x4,x5〉;〈xE,x0〉;〈x0,xF〉;〈x5,xA〉;〈xC,xE〉;〈xC,x8〉;〈x8,x2〉;〈x4,xF〉;〈xC,x2〉;〈xF,x5〉;〈xF,x8〉;〈x1,x3〉;〈xD,xA〉;〈x2,xB〉;
178 〈x7,x9〉;〈xB,xF〉;〈xA,x4〉;〈x5,xA〉;〈xD,x2〉;〈x7,x6〉;〈x8,xD〉;〈x1,xF〉;〈x1,x5〉;〈x5,xA〉;〈xD,xE〉;〈x2,x3〉;〈x9,xD〉;〈x7,xE〉;〈x6,x7〉;〈x6,x3〉;
179 〈x1,x1〉;〈xF,x5〉;〈x2,x4〉;〈xD,x6〉;〈x6,xA〉;〈x0,xC〉;〈x7,xF〉;〈x1,x2〉;〈xD,x6〉;〈xE,xE〉;〈xB,xA〉;〈x4,x4〉;〈x3,x9〉;〈x9,x2〉;〈x6,x6〉;〈xE,xA〉;
180 〈x2,x3〉;〈x4,x4〉;〈xC,xF〉;〈x7,x4〉;〈x6,xB〉;〈x8,x3〉;〈x7,x7〉;〈x0,x4〉;〈x6,x4〉;〈xB,x3〉;〈x3,xC〉;〈x2,x6〉;〈xF,xC〉;〈xD,x5〉;〈x4,x1〉;〈xB,x7〉;
181 〈x2,x4〉;〈xE,x0〉;〈xB,x4〉;〈x1,x3〉;〈x3,x2〉;〈x4,x5〉;〈x1,x8〉;〈xD,xB〉;〈x0,x0〉;〈xB,x6〉;〈x5,xF〉;〈x3,xA〉;〈xB,x7〉;〈x4,xF〉;〈xB,x4〉;〈xD,xF〉;
182 〈xF,x4〉;〈x1,xA〉;〈x1,x0〉;〈xE,x9〉;〈xC,x5〉;〈x2,xC〉;〈xB,xC〉;〈x5,xB〉;〈x0,x5〉;〈x4,xA〉;〈x5,x2〉;〈xC,x0〉;〈x1,xF〉;〈x5,x9〉;〈xF,x2〉;〈xE,x5〉
185 definition dTest_random_ex02 ≝
187 〈x9,x7〉;〈x5,x1〉;〈xF,x7〉;〈x3,xC〉;〈x7,x7〉;〈x8,x1〉;〈x7,xC〉;〈xB,x0〉;〈x1,xD〉;〈x1,xA〉;〈x7,xB〉;〈x4,x7〉;〈x7,x9〉;〈xC,x2〉;〈x3,xF〉;〈xD,x3〉;
188 〈xB,x6〉;〈xD,x7〉;〈xC,x9〉;〈x9,x2〉;〈x0,xD〉;〈x7,xF〉;〈x0,xB〉;〈x7,x5〉;〈x0,xE〉;〈x5,x1〉;〈x9,xF〉;〈x4,xC〉;〈xE,x5〉;〈xD,x0〉;〈xC,x1〉;〈x3,x9〉;
189 〈x7,xF〉;〈xE,xA〉;〈x4,x1〉;〈x0,x5〉;〈x0,x8〉;〈x7,xE〉;〈x7,x6〉;〈x2,xF〉;〈x6,x2〉;〈x7,x1〉;〈xF,x8〉;〈x3,x8〉;〈xB,x6〉;〈x7,x0〉;〈xD,xD〉;〈xD,x0〉;
190 〈xA,xD〉;〈x7,x8〉;〈x3,xD〉;〈x7,xB〉;〈xC,xC〉;〈x6,xD〉;〈x3,xF〉;〈xA,xC〉;〈xC,x7〉;〈x6,xE〉;〈xF,xF〉;〈x4,x5〉;〈xC,x1〉;〈x7,x4〉;〈xB,xF〉;〈x2,x9〉;
191 〈x4,x9〉;〈xC,x5〉;〈x7,xC〉;〈x2,xD〉;〈xF,x2〉;〈xC,xC〉;〈xF,xA〉;〈x5,x8〉;〈xA,xC〉;〈x5,x8〉;〈x5,x1〉;〈x0,xE〉;〈x4,x8〉;〈x7,x0〉;〈x4,x1〉;〈xE,xD〉;
192 〈x9,x5〉;〈xB,x4〉;〈x4,x7〉;〈xF,x1〉;〈x8,x1〉;〈xE,x4〉;〈x4,x0〉;〈x5,x4〉;〈x7,xB〉;〈xA,x1〉;〈xD,x2〉;〈x0,x2〉;〈xC,x5〉;〈x7,xD〉;〈x7,xA〉;〈xF,x1〉;
193 〈x0,x0〉;〈x8,xD〉;〈x6,x6〉;〈xB,x0〉;〈xA,x9〉;〈x7,xA〉;〈x2,xB〉;〈x2,xC〉;〈x6,xF〉;〈x5,xF〉;〈x6,xF〉;〈x4,xE〉;〈x2,xB〉;〈x1,x1〉;〈xF,xF〉;〈x4,x7〉;
194 〈x7,xF〉;〈xC,xF〉;〈xD,x3〉;〈x8,x5〉;〈xB,x8〉;〈x4,xD〉;〈x9,x9〉;〈x8,x3〉;〈x7,x6〉;〈xE,x8〉;〈x3,x0〉;〈xF,x8〉;〈xD,x0〉;〈x5,x9〉;〈xB,x8〉;〈x7,x1〉;
195 〈x5,x7〉;〈xA,xF〉;〈xB,x5〉;〈xD,x5〉;〈xF,xC〉;〈x8,x2〉;〈x1,x6〉;〈x1,x0〉;〈xB,x3〉;〈xC,x1〉;〈x1,xA〉;〈x0,x1〉;〈x1,x1〉;〈xF,xF〉;〈x5,x9〉;〈x2,x4〉;
196 〈xC,x5〉;〈x7,x2〉;〈xD,x8〉;〈xD,x0〉;〈xA,xD〉;〈xF,xE〉;〈xD,x7〉;〈x1,x1〉;〈xC,xE〉;〈xF,x9〉;〈xB,x8〉;〈x7,x7〉;〈x3,xA〉;〈x1,xF〉;〈x6,x1〉;〈x1,xB〉;
197 〈xB,xB〉;〈x5,x5〉;〈x8,x0〉;〈x7,xC〉;〈x2,x5〉;〈x3,x4〉;〈x8,x9〉;〈xF,x2〉;〈xC,x9〉;〈xD,xF〉;〈x3,x5〉;〈xC,x5〉;〈x1,x2〉;〈xF,x0〉;〈x0,x5〉;〈xD,xE〉;
198 〈x2,x6〉;〈x4,x9〉;〈xB,x7〉;〈x3,x9〉;〈x0,x5〉;〈xC,x2〉;〈xD,xB〉;〈xF,xC〉;〈x9,xF〉;〈xA,x9〉;〈x6,x6〉;〈xA,xD〉;〈x4,xA〉;〈x3,xF〉;〈xB,xF〉;〈x6,xD〉;
199 〈x8,x7〉;〈x6,xA〉;〈xB,x1〉;〈x3,xE〉;〈xB,x6〉;〈x0,xE〉;〈x7,xA〉;〈x3,xB〉;〈x4,x5〉;〈xE,x9〉;〈xC,xE〉;〈x6,xA〉;〈x6,xA〉;〈x7,x0〉;〈x6,x0〉;〈x6,xA〉;
200 〈x2,xC〉;〈xD,x2〉;〈xB,x8〉;〈x3,x6〉;〈x2,x1〉;〈x0,x0〉;〈x5,x4〉;〈x3,x1〉;〈x6,x0〉;〈x1,xB〉;〈x4,xC〉;〈xC,xA〉;〈xB,xE〉;〈x5,xF〉;〈x8,x1〉;〈xB,x7〉;
201 〈x9,xB〉;〈x2,x6〉;〈x9,x4〉;〈x2,xB〉;〈x4,x1〉;〈x2,xB〉;〈x9,x8〉;〈x6,x3〉;〈x6,x6〉;〈x6,x5〉;〈x4,x6〉;〈x2,x3〉;〈xE,x5〉;〈x0,x7〉;〈x9,xE〉;〈x1,xC〉;
202 〈x3,x8〉;〈x5,xC〉;〈x9,x7〉;〈x6,x3〉;〈x5,x3〉;〈x6,x6〉;〈x0,x8〉;〈x5,xD〉;〈x0,x8〉;〈xD,xB〉;〈x6,xE〉;〈x5,x6〉;〈x7,x0〉;〈x3,x2〉;〈x4,x5〉;〈x0,x2〉
205 definition dTest_random_ex03 ≝
207 〈x6,x3〉;〈x7,x2〉;〈x9,xC〉;〈xD,x9〉;〈x5,x0〉;〈x0,x6〉;〈x5,x9〉;〈x1,x7〉;〈x6,x8〉;〈xD,x2〉;〈xD,x7〉;〈x8,xE〉;〈x6,x9〉;〈x5,xF〉;〈x8,x1〉;〈x8,x4〉;
208 〈x8,x7〉;〈xD,xC〉;〈x9,x8〉;〈xE,x5〉;〈xB,x5〉;〈xC,x3〉;〈x2,x5〉;〈x6,xC〉;〈x9,x2〉;〈xD,xD〉;〈x2,xA〉;〈xD,x1〉;〈x1,x4〉;〈x7,xE〉;〈x1,x7〉;〈xB,x2〉;
209 〈x9,x8〉;〈x5,x5〉;〈xF,xC〉;〈x3,xD〉;〈x8,xD〉;〈xE,xF〉;〈x8,x1〉;〈xB,x8〉;〈xB,xB〉;〈x5,x1〉;〈x0,x0〉;〈xB,x4〉;〈x2,xE〉;〈x3,x0〉;〈x6,x0〉;〈x7,xE〉;
210 〈x9,x0〉;〈xE,x3〉;〈xF,x4〉;〈x7,x2〉;〈x1,xC〉;〈xB,x3〉;〈x7,x8〉;〈x1,xB〉;〈x9,xF〉;〈x1,xB〉;〈x0,x3〉;〈xA,x3〉;〈x0,x5〉;〈xD,xE〉;〈x3,x8〉;〈xB,xA〉;
211 〈x0,xE〉;〈xE,xD〉;〈xE,xC〉;〈x1,xF〉;〈x3,x8〉;〈xE,x3〉;〈xF,x7〉;〈xA,xA〉;〈xE,x9〉;〈x3,xD〉;〈xF,xF〉;〈xF,x3〉;〈x1,x4〉;〈x2,xC〉;〈x8,x8〉;〈x6,x1〉;
212 〈x3,x0〉;〈xA,xB〉;〈x1,x8〉;〈xD,xC〉;〈xF,xE〉;〈x6,xA〉;〈x2,x9〉;〈xF,x1〉;〈xC,xB〉;〈x9,x0〉;〈x7,x8〉;〈x9,x9〉;〈x1,xF〉;〈x2,x8〉;〈xF,x9〉;〈xC,xB〉;
213 〈x1,x4〉;〈x8,x4〉;〈xF,x3〉;〈xD,x6〉;〈x7,xE〉;〈xE,xC〉;〈x5,x6〉;〈xC,xE〉;〈xD,xA〉;〈x5,xE〉;〈x6,x1〉;〈xF,x1〉;〈x6,x6〉;〈x6,x9〉;〈x9,x3〉;〈x5,x9〉;
214 〈x3,xC〉;〈x1,xD〉;〈x6,xB〉;〈xF,x4〉;〈x5,x9〉;〈x4,xD〉;〈x3,x8〉;〈xA,x9〉;〈x3,xB〉;〈x7,xF〉;〈xB,x2〉;〈xE,xC〉;〈xA,xE〉;〈xF,x6〉;〈xB,x2〉;〈x2,x2〉;
215 〈x6,x4〉;〈x2,x7〉;〈x6,xC〉;〈x2,x0〉;〈xE,xE〉;〈x5,x1〉;〈x3,xE〉;〈x8,x8〉;〈xD,xD〉;〈xC,x1〉;〈xD,xC〉;〈xC,x1〉;〈x6,x6〉;〈x6,x1〉;〈x4,x2〉;〈x7,x7〉;
216 〈x3,x6〉;〈x0,x8〉;〈x2,x9〉;〈x6,x0〉;〈xA,x9〉;〈xF,xC〉;〈x7,xC〉;〈xA,x7〉;〈xB,x4〉;〈xF,xC〉;〈x8,x7〉;〈x1,xD〉;〈x6,xC〉;〈xA,x2〉;〈x3,xF〉;〈x1,xD〉;
217 〈x1,x7〉;〈x0,xF〉;〈x0,x2〉;〈x2,x6〉;〈xA,x2〉;〈x6,xA〉;〈x5,xC〉;〈xE,xD〉;〈x2,x7〉;〈xC,x5〉;〈x7,xB〉;〈xF,x5〉;〈x9,xC〉;〈x8,x5〉;〈x6,x3〉;〈x5,x6〉;
218 〈xC,x3〉;〈x4,xB〉;〈x1,xB〉;〈xA,x0〉;〈x1,xB〉;〈x8,x9〉;〈x3,x5〉;〈xD,x6〉;〈xD,x9〉;〈xD,xD〉;〈x2,xE〉;〈x6,x2〉;〈x7,x5〉;〈xE,x7〉;〈x1,x8〉;〈x4,xD〉;
219 〈xD,x7〉;〈x5,x8〉;〈xA,x7〉;〈x5,xF〉;〈x9,x4〉;〈x8,x7〉;〈xA,x8〉;〈xE,x7〉;〈x2,xB〉;〈xF,x2〉;〈xE,x7〉;〈xB,x9〉;〈x0,x6〉;〈xA,xF〉;〈xD,xA〉;〈xD,xC〉;
220 〈xC,x6〉;〈x3,xF〉;〈x8,xD〉;〈x7,x9〉;〈x9,x5〉;〈xD,xA〉;〈x5,xB〉;〈x9,x2〉;〈xE,xE〉;〈x3,xC〉;〈xF,xE〉;〈x4,x9〉;〈x5,xA〉;〈x1,x0〉;〈x4,xD〉;〈x8,x9〉;
221 〈x8,x3〉;〈x2,x6〉;〈xE,xC〉;〈x8,xD〉;〈xC,x9〉;〈x7,x7〉;〈xE,xE〉;〈xF,x1〉;〈x4,x0〉;〈x6,xD〉;〈x4,x9〉;〈x5,x7〉;〈x9,xB〉;〈xC,x4〉;〈x1,xF〉;〈x8,x0〉;
222 〈x9,x5〉;〈xB,xC〉;〈xE,x8〉;〈xF,x9〉;〈xD,x7〉;〈x1,x4〉;〈x3,xE〉;〈xC,x3〉;〈x6,xF〉;〈x8,xF〉;〈x7,x2〉;〈xD,x5〉;〈xB,xE〉;〈x8,xA〉;〈xA,x3〉;〈xF,x7〉
225 definition dTest_random_ex04 ≝
227 〈x6,x0〉;〈x3,xA〉;〈x7,x4〉;〈xF,xB〉;〈xB,xD〉;〈x7,x4〉;〈x8,x3〉;〈xE,x3〉;〈x9,xD〉;〈xD,x9〉;〈xB,x8〉;〈x1,x3〉;〈x5,x0〉;〈x4,x0〉;〈x8,xA〉;〈x9,x6〉;
228 〈x3,xA〉;〈xA,x6〉;〈xE,xC〉;〈x7,xC〉;〈x1,x5〉;〈x8,x7〉;〈x4,xD〉;〈x6,xA〉;〈xA,xA〉;〈xE,x0〉;〈xB,xA〉;〈xF,xF〉;〈x3,xB〉;〈xE,x2〉;〈x5,x1〉;〈x2,x2〉;
229 〈x2,x2〉;〈x1,xF〉;〈xA,x1〉;〈x2,x1〉;〈xA,xF〉;〈x3,x7〉;〈x8,xA〉;〈xD,xF〉;〈xE,x3〉;〈x6,x9〉;〈xE,xE〉;〈xC,x4〉;〈xE,x7〉;〈x7,x1〉;〈x9,x6〉;〈x1,x1〉;
230 〈xE,x4〉;〈x3,x9〉;〈xE,x5〉;〈xA,xF〉;〈xF,x5〉;〈x5,x7〉;〈xE,xB〉;〈x5,x5〉;〈x6,x5〉;〈x8,xB〉;〈x3,xE〉;〈x8,xD〉;〈x4,x6〉;〈x5,x3〉;〈xB,x2〉;〈x1,x9〉;
231 〈x3,x4〉;〈xE,x9〉;〈x4,xA〉;〈x4,xB〉;〈x5,x2〉;〈x3,x0〉;〈x3,xF〉;〈xA,x7〉;〈x4,xF〉;〈x1,xA〉;〈xB,x8〉;〈x6,x4〉;〈x5,xB〉;〈xD,x9〉;〈x6,xD〉;〈x6,x1〉;
232 〈xA,x5〉;〈xC,xF〉;〈x8,xC〉;〈xD,xD〉;〈xE,x6〉;〈xD,x5〉;〈x3,x6〉;〈x0,xC〉;〈x8,xD〉;〈xF,x7〉;〈x4,xE〉;〈x9,xC〉;〈xB,xF〉;〈x2,xB〉;〈x4,x4〉;〈xD,x1〉;
233 〈xC,x0〉;〈x8,x0〉;〈x0,x8〉;〈xA,xD〉;〈xC,xE〉;〈xB,xD〉;〈x4,xC〉;〈x5,x3〉;〈x6,x5〉;〈xB,x6〉;〈x4,x8〉;〈xF,x6〉;〈x6,x4〉;〈x7,xC〉;〈x9,x8〉;〈x1,x0〉;
234 〈x9,xD〉;〈xF,xD〉;〈x4,x9〉;〈xC,x4〉;〈xD,xD〉;〈x1,x4〉;〈xB,x6〉;〈x6,xF〉;〈x3,xB〉;〈x4,x6〉;〈xD,x7〉;〈x1,xA〉;〈x4,x4〉;〈xA,x4〉;〈x8,x1〉;〈x3,x1〉;
235 〈xA,x2〉;〈x4,x0〉;〈x7,x0〉;〈x3,x9〉;〈x9,xA〉;〈x4,xC〉;〈x4,xF〉;〈x9,x3〉;〈x9,xD〉;〈xD,x4〉;〈x9,x7〉;〈x3,x9〉;〈xA,x8〉;〈xA,x8〉;〈xF,x9〉;〈xB,x3〉;
236 〈xE,x7〉;〈xD,x8〉;〈x4,xD〉;〈x6,xD〉;〈x8,x8〉;〈x6,xB〉;〈x5,x4〉;〈x5,x5〉;〈x9,x2〉;〈x1,x9〉;〈xE,x4〉;〈xB,x1〉;〈xE,x3〉;〈x4,x6〉;〈xD,x5〉;〈x6,xC〉;
237 〈xF,x9〉;〈x3,x3〉;〈xE,x5〉;〈xD,x2〉;〈x7,x7〉;〈x1,x8〉;〈x8,x6〉;〈x1,x4〉;〈x7,xE〉;〈x1,xE〉;〈xC,x8〉;〈xB,x4〉;〈xC,xE〉;〈xC,x7〉;〈x5,x7〉;〈x2,xD〉;
238 〈x5,x2〉;〈xE,x7〉;〈x5,x7〉;〈x9,xB〉;〈x1,xA〉;〈x4,x9〉;〈x0,x9〉;〈x4,xB〉;〈xF,x6〉;〈xB,x5〉;〈x0,xA〉;〈x2,xC〉;〈xB,xA〉;〈x1,xF〉;〈x2,x6〉;〈x3,x8〉;
239 〈x6,x0〉;〈x3,x4〉;〈xC,x4〉;〈x8,x9〉;〈xB,xF〉;〈x0,x4〉;〈x5,xF〉;〈xF,x4〉;〈x1,x1〉;〈xF,x3〉;〈x4,xA〉;〈xE,x2〉;〈xD,x8〉;〈x3,x6〉;〈xF,xA〉;〈x4,x3〉;
240 〈x0,xC〉;〈x6,x0〉;〈x5,x1〉;〈x2,xD〉;〈x0,x3〉;〈xF,xC〉;〈x9,x2〉;〈x2,x1〉;〈xC,xA〉;〈x7,x5〉;〈x6,x6〉;〈xD,xC〉;〈x8,x4〉;〈xC,x4〉;〈x6,xF〉;〈xF,x0〉;
241 〈x0,x4〉;〈x5,x2〉;〈xA,xB〉;〈x9,xA〉;〈xC,xE〉;〈xA,xA〉;〈x2,xF〉;〈x3,x6〉;〈xF,x3〉;〈xA,x7〉;〈x4,x2〉;〈x0,x7〉;〈x5,xE〉;〈xB,x6〉;〈x5,xB〉;〈x9,x8〉;
242 〈x7,x9〉;〈x4,x3〉;〈x8,x8〉;〈x9,xA〉;〈x0,xA〉;〈x5,x5〉;〈xE,x3〉;〈x9,x8〉;〈x7,x5〉;〈xA,x2〉;〈xE,xA〉;〈xB,x9〉;〈x3,x2〉;〈x4,x1〉;〈x0,x7〉;〈x3,x8〉
245 definition dTest_random_ex05 ≝
247 〈xB,x1〉;〈x0,x3〉;〈x4,xE〉;〈x6,xF〉;〈x9,x7〉;〈x3,xC〉;〈x5,x4〉;〈xB,xB〉;〈xB,xC〉;〈x0,xB〉;〈x0,xC〉;〈xA,xB〉;〈x3,xB〉;〈x2,x8〉;〈xA,xA〉;〈x0,x4〉;
248 〈x5,x0〉;〈xA,x3〉;〈x6,xB〉;〈xF,xA〉;〈xF,x0〉;〈xE,x6〉;〈x1,x8〉;〈xD,x8〉;〈x7,xA〉;〈x5,xF〉;〈x0,x3〉;〈x8,x2〉;〈x9,x6〉;〈x9,xA〉;〈xB,xF〉;〈x1,x5〉;
249 〈x8,x5〉;〈xE,xF〉;〈xB,x3〉;〈x7,xB〉;〈xE,xE〉;〈xE,xF〉;〈x1,x0〉;〈x6,x9〉;〈xC,x2〉;〈xF,x9〉;〈x2,xD〉;〈x8,x1〉;〈xF,x3〉;〈x0,xE〉;〈xC,x3〉;〈x7,xF〉;
250 〈xD,xD〉;〈x2,xE〉;〈x2,xA〉;〈xB,xD〉;〈xE,xA〉;〈x9,x2〉;〈xF,xF〉;〈xF,xA〉;〈x7,xB〉;〈xD,x3〉;〈x3,x0〉;〈x7,x5〉;〈x6,x7〉;〈xA,x8〉;〈x0,xF〉;〈x2,x1〉;
251 〈xD,xC〉;〈xE,x5〉;〈xE,x2〉;〈x8,x9〉;〈x2,x9〉;〈xC,x5〉;〈xA,x3〉;〈xA,x2〉;〈x4,x2〉;〈x3,xF〉;〈xA,x3〉;〈x5,x8〉;〈xE,x0〉;〈x7,xC〉;〈x0,x3〉;〈xF,xF〉;
252 〈x2,x8〉;〈x8,xB〉;〈x8,xB〉;〈x1,x2〉;〈xD,x8〉;〈xA,x8〉;〈x7,x6〉;〈xB,x9〉;〈xE,x2〉;〈xF,xE〉;〈x2,x1〉;〈x3,xF〉;〈xA,xC〉;〈x4,x6〉;〈xB,xC〉;〈xF,x8〉;
253 〈xD,x3〉;〈xE,xB〉;〈xF,xC〉;〈x9,xF〉;〈xE,x7〉;〈x6,x1〉;〈xC,xB〉;〈xB,xF〉;〈x4,xE〉;〈xC,x4〉;〈x9,x7〉;〈x1,xE〉;〈x0,xD〉;〈x7,x9〉;〈x8,x3〉;〈xA,xB〉;
254 〈x4,xC〉;〈x2,x6〉;〈x6,x3〉;〈x6,xF〉;〈xE,xE〉;〈x5,x9〉;〈x8,x1〉;〈x0,x2〉;〈x2,xC〉;〈xE,xD〉;〈x6,xF〉;〈x0,x4〉;〈x1,x0〉;〈xE,x0〉;〈xD,xA〉;〈xB,xE〉;
255 〈xE,xE〉;〈x5,x7〉;〈xB,x0〉;〈x3,x1〉;〈x4,x1〉;〈xD,xC〉;〈x3,xC〉;〈xC,xC〉;〈x5,x8〉;〈x2,x8〉;〈x2,xC〉;〈x1,xB〉;〈x8,x6〉;〈xD,x6〉;〈xF,x9〉;〈xD,x5〉;
256 〈x4,xA〉;〈xE,xA〉;〈x0,xB〉;〈x2,x0〉;〈x2,xC〉;〈x4,x2〉;〈xC,xE〉;〈x4,x5〉;〈x2,xB〉;〈x0,x1〉;〈xA,xA〉;〈xB,x1〉;〈x6,xE〉;〈xB,x7〉;〈xB,x7〉;〈x2,x8〉;
257 〈x9,x5〉;〈x1,x9〉;〈xA,x7〉;〈x5,xC〉;〈x4,xE〉;〈x7,xB〉;〈x3,xE〉;〈xD,x3〉;〈x9,x0〉;〈x8,x6〉;〈x7,x1〉;〈x1,x4〉;〈xD,x2〉;〈xD,x4〉;〈xB,x4〉;〈xF,x2〉;
258 〈x3,x1〉;〈x2,x8〉;〈x4,x5〉;〈xF,xD〉;〈x7,x8〉;〈x5,xD〉;〈xF,xA〉;〈xF,x3〉;〈x9,x5〉;〈x4,xD〉;〈x3,x1〉;〈xB,x8〉;〈xC,xC〉;〈x2,x1〉;〈x1,x9〉;〈x4,x2〉;
259 〈x2,xA〉;〈xF,x2〉;〈xB,xA〉;〈x0,x4〉;〈x9,xF〉;〈x4,x3〉;〈x4,x5〉;〈x1,xC〉;〈x7,x4〉;〈xB,xB〉;〈x7,x0〉;〈x5,xE〉;〈x0,x1〉;〈xA,xC〉;〈x6,xD〉;〈xD,x7〉;
260 〈x9,xC〉;〈x9,xD〉;〈x1,xA〉;〈x9,x8〉;〈xB,x1〉;〈xF,xC〉;〈x6,x1〉;〈xA,x3〉;〈x4,x1〉;〈x4,x1〉;〈xA,xF〉;〈x1,xD〉;〈xE,x1〉;〈x3,x2〉;〈x1,x9〉;〈x6,x0〉;
261 〈x2,x9〉;〈x9,x7〉;〈x8,x5〉;〈x5,x3〉;〈x5,x3〉;〈x9,x1〉;〈xB,x3〉;〈x9,x4〉;〈xD,x5〉;〈x9,xD〉;〈x4,xC〉;〈x3,x6〉;〈x0,xE〉;〈x8,x4〉;〈xA,x1〉;〈x4,x6〉;
262 〈x6,xA〉;〈x1,xF〉;〈xF,x3〉;〈x6,xB〉;〈xB,xE〉;〈x4,xA〉;〈x1,x9〉;〈x7,x5〉;〈xF,xC〉;〈xC,x6〉;〈xE,xA〉;〈x7,xE〉;〈xD,x1〉;〈x3,x3〉;〈x6,x7〉;〈xB,x7〉
265 definition dTest_random_ex06 ≝
267 〈xE,xE〉;〈x5,x9〉;〈xE,x2〉;〈xD,xD〉;〈x2,x2〉;〈x8,xC〉;〈x9,xB〉;〈x3,xE〉;〈x9,x8〉;〈xF,xC〉;〈x1,x3〉;〈xE,x2〉;〈x0,xC〉;〈x4,xE〉;〈x3,x1〉;〈x8,x7〉;
268 〈x6,x7〉;〈x6,xA〉;〈x4,xC〉;〈x4,xC〉;〈x7,x2〉;〈x0,x0〉;〈x0,x5〉;〈x1,xF〉;〈xF,x6〉;〈x3,x0〉;〈xE,xE〉;〈xD,xE〉;〈xB,x1〉;〈x4,xC〉;〈xF,x7〉;〈xE,xC〉;
269 〈x2,xC〉;〈x4,x0〉;〈x6,xB〉;〈x6,x8〉;〈x9,x0〉;〈x8,x8〉;〈x6,xF〉;〈xB,x3〉;〈x4,x7〉;〈x6,x2〉;〈x9,x2〉;〈x9,xB〉;〈x2,xB〉;〈x3,x2〉;〈x4,x0〉;〈xA,x7〉;
270 〈x8,x9〉;〈x4,x0〉;〈x2,x3〉;〈x5,xC〉;〈xF,x9〉;〈x2,x9〉;〈x6,x2〉;〈xA,xE〉;〈x5,xB〉;〈xC,x9〉;〈x2,xC〉;〈x9,x2〉;〈x6,xF〉;〈xF,x5〉;〈xA,x0〉;〈x0,xE〉;
271 〈xD,xE〉;〈xF,x9〉;〈x0,x9〉;〈x1,x0〉;〈x3,x9〉;〈x4,x6〉;〈xC,x5〉;〈xE,x2〉;〈x8,x3〉;〈xD,x5〉;〈x8,xE〉;〈x4,x6〉;〈x4,xC〉;〈xA,xC〉;〈x7,xF〉;〈x4,xF〉;
272 〈xC,x1〉;〈x4,xF〉;〈x1,xA〉;〈x6,x1〉;〈x9,x6〉;〈x0,xB〉;〈x0,x0〉;〈x6,xF〉;〈x2,x6〉;〈x8,xC〉;〈xE,xE〉;〈x9,x3〉;〈x1,xB〉;〈x9,xE〉;〈xA,x5〉;〈x9,x6〉;
273 〈x2,xA〉;〈xE,xB〉;〈x4,x6〉;〈x5,xF〉;〈x3,xC〉;〈xD,x6〉;〈x2,xD〉;〈x9,x4〉;〈x6,xB〉;〈xF,x4〉;〈xD,xA〉;〈x6,x9〉;〈x5,x9〉;〈xA,xC〉;〈xB,xD〉;〈x9,xE〉;
274 〈x4,x8〉;〈x0,x2〉;〈xD,xC〉;〈x5,xC〉;〈x6,x0〉;〈x2,xA〉;〈x6,xE〉;〈xC,xA〉;〈x6,xE〉;〈x1,xF〉;〈xD,x4〉;〈x3,xA〉;〈xB,x0〉;〈x9,xE〉;〈x8,xF〉;〈xA,xB〉;
275 〈xB,x2〉;〈x0,x2〉;〈x4,x7〉;〈x7,xD〉;〈xA,xB〉;〈xD,xB〉;〈xB,x5〉;〈x6,xD〉;〈xE,x2〉;〈x8,x9〉;〈x4,xD〉;〈x0,x4〉;〈xB,xE〉;〈xF,xA〉;〈x2,x2〉;〈x1,x4〉;
276 〈x7,x1〉;〈x1,x2〉;〈x1,xB〉;〈x0,xD〉;〈xB,xA〉;〈x5,xA〉;〈x6,xC〉;〈x1,xE〉;〈x3,xA〉;〈x0,xF〉;〈x6,xE〉;〈x4,x4〉;〈xC,x8〉;〈xB,x5〉;〈x8,xC〉;〈x0,x3〉;
277 〈x0,x6〉;〈x6,x4〉;〈x8,x5〉;〈x2,x8〉;〈x6,x4〉;〈x2,x2〉;〈x8,x1〉;〈x7,x6〉;〈xF,xE〉;〈xF,xA〉;〈x6,x2〉;〈x9,x1〉;〈xB,xE〉;〈xB,xC〉;〈x6,x1〉;〈x4,xB〉;
278 〈x7,xE〉;〈x5,x0〉;〈xB,xC〉;〈xE,xE〉;〈x6,x3〉;〈xC,xF〉;〈x1,xD〉;〈xF,xD〉;〈x6,x2〉;〈x5,xC〉;〈x8,x5〉;〈x9,xE〉;〈xA,x5〉;〈x2,x6〉;〈xE,x7〉;〈x4,x6〉;
279 〈x3,xB〉;〈xE,xA〉;〈xB,xE〉;〈x0,x4〉;〈x8,x8〉;〈xF,x2〉;〈x9,x2〉;〈x0,xB〉;〈xD,x9〉;〈xE,x9〉;〈x2,x9〉;〈x3,x8〉;〈x8,x8〉;〈x8,xA〉;〈x6,x9〉;〈x1,x7〉;
280 〈x4,xB〉;〈xB,xF〉;〈x0,xC〉;〈xF,x2〉;〈xF,xD〉;〈x7,x3〉;〈x5,x9〉;〈xB,xE〉;〈x5,x4〉;〈x1,xC〉;〈xD,x3〉;〈x3,x1〉;〈x6,x2〉;〈x1,xB〉;〈xB,x7〉;〈x3,x2〉;
281 〈xA,x4〉;〈xF,x1〉;〈x7,x0〉;〈x9,xA〉;〈x4,x6〉;〈xA,x1〉;〈x1,xC〉;〈x0,x4〉;〈x6,xC〉;〈xF,x2〉;〈xE,x6〉;〈xC,x1〉;〈xA,x4〉;〈xF,x2〉;〈x2,xA〉;〈x4,xB〉;
282 〈x3,x5〉;〈x9,xB〉;〈x9,x9〉;〈xF,xF〉;〈x0,x1〉;〈x1,x3〉;〈xF,x9〉;〈x5,xC〉;〈x3,xC〉;〈x5,x1〉;〈x8,xA〉;〈xA,x5〉;〈x5,xF〉;〈x9,xE〉;〈x5,xE〉;〈xC,x6〉
285 definition dTest_random_ex07 ≝
287 〈x2,x1〉;〈x3,x7〉;〈xD,x2〉;〈xB,x9〉;〈x9,x8〉;〈xA,x1〉;〈x6,x0〉;〈xE,x9〉;〈x4,x5〉;〈xC,xA〉;〈xD,x7〉;〈xB,xD〉;〈xC,xF〉;〈x0,xF〉;〈x2,x4〉;〈xE,x5〉;
288 〈x7,x9〉;〈x4,xB〉;〈x1,xC〉;〈x5,x7〉;〈x3,xA〉;〈x2,x4〉;〈x2,x2〉;〈x0,x8〉;〈x3,x3〉;〈xE,x2〉;〈xA,x2〉;〈x5,x8〉;〈x2,x5〉;〈x5,x4〉;〈x7,x1〉;〈x2,xB〉;
289 〈xF,xF〉;〈xE,xD〉;〈x4,x8〉;〈xF,x6〉;〈x2,x3〉;〈x3,x1〉;〈xB,xA〉;〈x5,x1〉;〈x9,xF〉;〈xA,xA〉;〈xC,xC〉;〈x0,x3〉;〈x1,x5〉;〈xC,x7〉;〈x2,xD〉;〈xD,x3〉;
290 〈xE,xB〉;〈x8,xF〉;〈x8,x4〉;〈x4,x0〉;〈x5,x3〉;〈xA,xD〉;〈x6,x7〉;〈xE,xC〉;〈xA,xF〉;〈xD,xC〉;〈x1,xC〉;〈x7,x4〉;〈x6,xB〉;〈xA,xD〉;〈xC,xD〉;〈xA,x7〉;
291 〈x1,x1〉;〈x1,x0〉;〈xC,xF〉;〈xB,xE〉;〈xA,x1〉;〈x0,x1〉;〈x3,xF〉;〈xC,x0〉;〈x8,x5〉;〈x2,x8〉;〈x6,xB〉;〈xC,x3〉;〈x6,xD〉;〈xD,x8〉;〈x7,x5〉;〈x5,xA〉;
292 〈xF,x0〉;〈x2,x2〉;〈x4,xB〉;〈x9,xC〉;〈x3,x1〉;〈xE,x4〉;〈xE,x7〉;〈xC,x6〉;〈xF,xC〉;〈x3,x0〉;〈xD,x5〉;〈xF,x9〉;〈x1,xA〉;〈x4,x0〉;〈x1,xF〉;〈x6,xD〉;
293 〈xD,x5〉;〈x7,x8〉;〈xB,x5〉;〈x7,x6〉;〈xC,x9〉;〈xE,x1〉;〈xD,xF〉;〈x1,x2〉;〈x6,x1〉;〈xD,xF〉;〈x9,xF〉;〈x5,x7〉;〈x7,xD〉;〈x0,xB〉;〈xA,xD〉;〈x5,xA〉;
294 〈xA,x1〉;〈x8,x4〉;〈xE,x5〉;〈xF,x7〉;〈xB,xC〉;〈xD,x3〉;〈xA,x5〉;〈xB,x4〉;〈x8,x5〉;〈x6,x7〉;〈x3,x6〉;〈xF,xC〉;〈xB,x1〉;〈xB,x3〉;〈xC,xB〉;〈x1,xE〉;
295 〈xE,xC〉;〈x6,xE〉;〈xE,x1〉;〈x1,xC〉;〈xA,x5〉;〈x5,x3〉;〈x9,x8〉;〈xF,x6〉;〈xD,xF〉;〈x4,x1〉;〈x1,x3〉;〈x2,xE〉;〈x7,xF〉;〈x0,xE〉;〈x3,x8〉;〈x3,xC〉;
296 〈xD,x4〉;〈x8,xC〉;〈x2,xA〉;〈x2,x8〉;〈x4,xE〉;〈x7,xE〉;〈x0,xE〉;〈xF,x7〉;〈xC,xA〉;〈x3,xE〉;〈xE,x4〉;〈xB,x4〉;〈x0,x5〉;〈x5,x8〉;〈xD,xC〉;〈x7,x8〉;
297 〈xD,x9〉;〈xF,x9〉;〈x7,x9〉;〈x8,x4〉;〈x0,x2〉;〈x3,xF〉;〈xC,xF〉;〈x3,x8〉;〈xD,x7〉;〈x2,x6〉;〈x1,xD〉;〈x1,x8〉;〈x4,xD〉;〈xE,xA〉;〈x7,xA〉;〈xD,x4〉;
298 〈x2,x4〉;〈x0,xD〉;〈x4,xD〉;〈x9,x0〉;〈x1,x7〉;〈x1,xE〉;〈x6,xE〉;〈xB,x6〉;〈xC,xC〉;〈xC,x0〉;〈xB,x0〉;〈x5,xE〉;〈x9,x9〉;〈x6,xD〉;〈xC,xF〉;〈xE,xE〉;
299 〈x2,x9〉;〈xC,xF〉;〈xA,x2〉;〈x0,xC〉;〈xA,xB〉;〈x7,x4〉;〈x2,x9〉;〈x4,xE〉;〈x8,x2〉;〈x9,x3〉;〈x6,x9〉;〈x7,xB〉;〈xE,xC〉;〈xC,x7〉;〈x8,x9〉;〈xC,xA〉;
300 〈xD,xD〉;〈xA,xC〉;〈x6,x5〉;〈x8,x0〉;〈x1,x4〉;〈x0,x9〉;〈x5,x5〉;〈x0,xE〉;〈x8,x4〉;〈x5,xE〉;〈x6,xF〉;〈x3,x4〉;〈x1,x8〉;〈xC,x9〉;〈x8,xB〉;〈xE,x4〉;
301 〈x3,xE〉;〈xC,x4〉;〈x1,x6〉;〈xA,x4〉;〈x1,x9〉;〈x3,x4〉;〈x0,xE〉;〈x5,xE〉;〈xF,x9〉;〈x0,x3〉;〈x1,x3〉;〈x7,x2〉;〈x2,x7〉;〈x2,x8〉;〈xA,x7〉;〈x6,xD〉;
302 〈xC,x1〉;〈x1,xD〉;〈xF,x0〉;〈x2,x8〉;〈xF,xB〉;〈xF,x6〉;〈x3,x8〉;〈x0,x1〉;〈xF,x9〉;〈xB,xC〉;〈x6,x6〉;〈xF,x8〉;〈x6,xE〉;〈xD,x1〉;〈xB,x5〉;〈x3,x8〉
305 definition dTest_random_ex08 ≝
307 〈x4,x3〉;〈xB,x6〉;〈x6,x8〉;〈xA,xC〉;〈x0,x9〉;〈xF,xD〉;〈x0,x9〉;〈x6,x8〉;〈xE,x0〉;〈x2,x2〉;〈xA,xF〉;〈x4,x0〉;〈x2,x6〉;〈x0,xC〉;〈x5,x2〉;〈xA,x7〉;
308 〈xA,xD〉;〈xC,x3〉;〈x8,x2〉;〈xD,xC〉;〈x3,xC〉;〈x6,x5〉;〈xF,x2〉;〈xE,x8〉;〈xC,x0〉;〈x0,x6〉;〈x6,x4〉;〈xB,x1〉;〈x2,x0〉;〈x9,x5〉;〈x2,x2〉;〈xD,xD〉;
309 〈xA,xD〉;〈xF,xF〉;〈x1,xB〉;〈x8,xB〉;〈xB,x6〉;〈x4,xA〉;〈xB,xB〉;〈x9,x8〉;〈x1,xA〉;〈xE,xC〉;〈x7,xB〉;〈xA,x6〉;〈x2,xC〉;〈xE,x1〉;〈xC,x7〉;〈xD,xC〉;
310 〈x1,x9〉;〈x0,x6〉;〈x0,xA〉;〈x9,xF〉;〈x5,x2〉;〈x2,xB〉;〈xC,xA〉;〈x2,xF〉;〈x4,x0〉;〈xF,x8〉;〈xE,xA〉;〈x8,x7〉;〈x8,x9〉;〈xF,xD〉;〈x5,xD〉;〈x0,x0〉;
311 〈x6,xE〉;〈x0,x0〉;〈x0,xD〉;〈x3,x0〉;〈x4,x3〉;〈x5,xA〉;〈x8,xF〉;〈x8,xA〉;〈xA,x4〉;〈x5,x0〉;〈x8,xF〉;〈x0,xC〉;〈x7,x7〉;〈xF,x2〉;〈x6,x5〉;〈xE,x4〉;
312 〈x2,xD〉;〈xE,x5〉;〈xA,x8〉;〈x7,xF〉;〈x7,x8〉;〈xE,x3〉;〈x9,x5〉;〈xD,xA〉;〈x0,x7〉;〈x2,x9〉;〈x5,x1〉;〈x9,x4〉;〈xE,x4〉;〈x0,x1〉;〈xB,xF〉;〈x6,xE〉;
313 〈x9,x8〉;〈x9,xC〉;〈x9,x0〉;〈xA,x8〉;〈x0,xA〉;〈x3,xD〉;〈x3,xC〉;〈x5,x0〉;〈xE,xB〉;〈x1,x2〉;〈xC,x4〉;〈x5,xF〉;〈x4,x7〉;〈x7,xB〉;〈x2,xC〉;〈xD,xF〉;
314 〈x7,x8〉;〈x1,x3〉;〈x7,x4〉;〈xE,x0〉;〈x7,xB〉;〈x7,x1〉;〈x4,x7〉;〈x4,x8〉;〈x1,xB〉;〈xE,x3〉;〈x6,xB〉;〈x0,xB〉;〈x4,xB〉;〈x5,x9〉;〈x9,x3〉;〈xD,xF〉;
315 〈xE,x1〉;〈x1,xB〉;〈xD,x0〉;〈xE,xD〉;〈x4,x7〉;〈x4,xD〉;〈xC,x2〉;〈xD,xE〉;〈x5,xC〉;〈xD,xA〉;〈x9,x5〉;〈xC,x8〉;〈x1,x0〉;〈x7,x7〉;〈x7,xF〉;〈xC,x0〉;
316 〈xA,x7〉;〈xD,x3〉;〈xD,x3〉;〈xD,x8〉;〈x3,x4〉;〈xA,x1〉;〈x1,x5〉;〈xE,x0〉;〈x0,x4〉;〈x1,xE〉;〈x8,x2〉;〈xC,xA〉;〈xD,x9〉;〈x1,x1〉;〈xB,x1〉;〈xC,x9〉;
317 〈x4,xC〉;〈x4,xB〉;〈x0,x9〉;〈x4,x8〉;〈xF,xC〉;〈xD,xD〉;〈x6,xE〉;〈xC,xA〉;〈x7,x6〉;〈xA,xE〉;〈x8,xE〉;〈x3,xB〉;〈xF,xB〉;〈x6,x5〉;〈x8,x3〉;〈x1,xD〉;
318 〈xD,xB〉;〈xA,xE〉;〈x4,xF〉;〈xC,x6〉;〈x1,xE〉;〈xC,x5〉;〈xC,xC〉;〈x7,xC〉;〈x2,x8〉;〈xF,x9〉;〈xD,x2〉;〈x8,x6〉;〈x1,x5〉;〈xF,xA〉;〈x4,x1〉;〈x4,x5〉;
319 〈x2,xE〉;〈x9,x5〉;〈xB,xF〉;〈x0,xD〉;〈x8,xB〉;〈x8,xD〉;〈x1,x1〉;〈x9,xC〉;〈xB,x8〉;〈xF,xB〉;〈x2,x6〉;〈xD,x6〉;〈x9,x1〉;〈x0,xD〉;〈xC,xD〉;〈x0,x7〉;
320 〈x5,x0〉;〈xF,xA〉;〈x2,x9〉;〈x3,xF〉;〈x0,xC〉;〈x2,xB〉;〈xF,xE〉;〈x9,x7〉;〈x5,x5〉;〈x5,xA〉;〈x6,xD〉;〈x9,x6〉;〈x0,x5〉;〈x0,x9〉;〈x4,x5〉;〈xE,xF〉;
321 〈x0,xF〉;〈x7,x4〉;〈x9,x3〉;〈x6,xC〉;〈x8,x2〉;〈x3,x7〉;〈xE,xB〉;〈x5,x0〉;〈xF,x5〉;〈xC,x4〉;〈x0,xB〉;〈x3,x8〉;〈x2,xD〉;〈x8,xA〉;〈x9,x3〉;〈x6,xD〉;
322 〈x1,xD〉;〈xE,x5〉;〈xF,x7〉;〈xE,x7〉;〈xD,x7〉;〈x5,xC〉;〈xB,x4〉;〈x5,x0〉;〈x7,x5〉;〈x0,xD〉;〈xF,x3〉;〈xC,xE〉;〈x3,x1〉;〈xF,x1〉;〈x8,xE〉;〈x8,xF〉
325 definition dTest_random_ex09 ≝
327 〈xD,xB〉;〈x1,x4〉;〈xF,x6〉;〈x0,x3〉;〈xA,xB〉;〈xA,xE〉;〈xB,xC〉;〈xE,xB〉;〈xC,x8〉;〈x6,x7〉;〈xC,xC〉;〈xF,xF〉;〈x4,xF〉;〈xC,x6〉;〈x2,x9〉;〈x9,x5〉;
328 〈xB,xC〉;〈x6,x5〉;〈x5,x2〉;〈xF,x2〉;〈x3,x5〉;〈xC,x4〉;〈xF,x4〉;〈x9,xB〉;〈x4,x5〉;〈x1,xC〉;〈xD,xB〉;〈x6,x1〉;〈xF,xE〉;〈x3,xF〉;〈xB,x9〉;〈xD,x8〉;
329 〈xF,x1〉;〈xA,xC〉;〈x0,x7〉;〈xA,x4〉;〈xB,x8〉;〈x8,x8〉;〈x9,x5〉;〈xB,x8〉;〈x5,x6〉;〈x3,x2〉;〈x5,xA〉;〈x3,xE〉;〈x2,x2〉;〈x0,xB〉;〈x9,x6〉;〈xE,xE〉;
330 〈x6,xF〉;〈x1,xE〉;〈x3,x2〉;〈x4,x9〉;〈x4,xF〉;〈xC,xC〉;〈xD,xB〉;〈x5,x1〉;〈x4,xD〉;〈xD,x1〉;〈x4,xF〉;〈x0,x9〉;〈x5,xA〉;〈xA,xC〉;〈xE,x7〉;〈x8,x6〉;
331 〈x5,x8〉;〈xA,x5〉;〈xA,x7〉;〈x5,xE〉;〈x3,x6〉;〈x1,x1〉;〈x3,xA〉;〈x8,x9〉;〈x8,x2〉;〈xD,xC〉;〈x6,x2〉;〈x0,xE〉;〈xA,xB〉;〈x2,xB〉;〈x2,x5〉;〈xF,x9〉;
332 〈x7,x7〉;〈x8,x6〉;〈x1,xD〉;〈x7,x9〉;〈x5,x1〉;〈xB,xD〉;〈x9,x8〉;〈xB,x7〉;〈xB,xB〉;〈xF,x6〉;〈xD,x9〉;〈x6,x6〉;〈x0,x1〉;〈x1,x2〉;〈xE,xB〉;〈x0,xA〉;
333 〈xC,xD〉;〈x1,xA〉;〈xA,xA〉;〈xC,xC〉;〈x6,x5〉;〈x4,x2〉;〈x8,xF〉;〈x2,xA〉;〈x4,x8〉;〈xC,x6〉;〈xB,xA〉;〈xD,x8〉;〈x2,xD〉;〈x2,x9〉;〈xE,x8〉;〈x5,x7〉;
334 〈x7,x7〉;〈x7,xA〉;〈xB,x4〉;〈x4,x9〉;〈x6,x5〉;〈x4,x3〉;〈x5,x7〉;〈xF,xE〉;〈xC,x6〉;〈xC,x7〉;〈x6,x2〉;〈x6,x7〉;〈x5,x8〉;〈xD,x6〉;〈x9,xA〉;〈xC,x8〉;
335 〈xE,x8〉;〈x3,x0〉;〈x6,x0〉;〈x7,x3〉;〈x8,x9〉;〈x2,x3〉;〈x0,x8〉;〈x7,xA〉;〈xA,xC〉;〈x5,xD〉;〈x6,xD〉;〈xC,xE〉;〈x0,xC〉;〈x1,xB〉;〈x1,x7〉;〈xC,x1〉;
336 〈x4,x2〉;〈x5,x3〉;〈x1,x5〉;〈x7,xC〉;〈x7,x4〉;〈x2,xB〉;〈x2,x5〉;〈x5,x6〉;〈x6,x1〉;〈xE,xC〉;〈x0,xB〉;〈x4,x2〉;〈x0,x4〉;〈xC,xA〉;〈x0,x9〉;〈xA,xB〉;
337 〈x1,xB〉;〈xD,x0〉;〈x9,xF〉;〈x6,xA〉;〈x7,xF〉;〈x4,x1〉;〈xF,x8〉;〈xE,xA〉;〈x8,x2〉;〈x8,x1〉;〈x4,x1〉;〈xC,xE〉;〈xC,xE〉;〈x0,xD〉;〈x2,xB〉;〈x3,x3〉;
338 〈xA,x3〉;〈x6,x4〉;〈xF,xA〉;〈xA,x6〉;〈x3,x9〉;〈x7,xF〉;〈xF,x6〉;〈xB,x2〉;〈x5,x5〉;〈x6,xB〉;〈xA,xC〉;〈x3,x3〉;〈x9,x3〉;〈xE,x7〉;〈xB,xE〉;〈x3,x4〉;
339 〈xC,xF〉;〈xE,xF〉;〈xA,x2〉;〈xE,xE〉;〈xE,xD〉;〈xC,xB〉;〈xB,x0〉;〈x8,x9〉;〈xD,xA〉;〈x3,xB〉;〈xB,xE〉;〈x3,xE〉;〈x3,x3〉;〈x5,x1〉;〈xA,x5〉;〈x3,xC〉;
340 〈xC,xC〉;〈xA,x0〉;〈xF,xD〉;〈x3,x9〉;〈xC,xB〉;〈xF,xC〉;〈x1,xF〉;〈x8,xD〉;〈x6,x8〉;〈xD,x4〉;〈x8,xC〉;〈xA,xA〉;〈x8,xE〉;〈x3,xA〉;〈x9,x7〉;〈x2,x6〉;
341 〈x6,xB〉;〈xA,xC〉;〈x8,xA〉;〈x4,xB〉;〈x7,x4〉;〈x3,xF〉;〈xB,x7〉;〈xB,xF〉;〈x0,xC〉;〈xE,x6〉;〈xC,xD〉;〈x4,x2〉;〈xF,xA〉;〈xE,xE〉;〈xF,x9〉;〈x0,xC〉;
342 〈x2,xC〉;〈x7,x9〉;〈x7,xE〉;〈xD,x8〉;〈x4,x0〉;〈x7,xC〉;〈x3,x8〉;〈x4,x9〉;〈x7,x1〉;〈x7,x5〉;〈xB,x7〉;〈x3,x6〉;〈x0,x7〉;〈x1,xA〉;〈x2,xC〉;〈x1,xE〉
345 definition dTest_random_ex10 ≝
347 〈x3,xC〉;〈x7,xA〉;〈x3,x8〉;〈x4,xA〉;〈x3,x4〉;〈x2,x0〉;〈x9,x5〉;〈x6,x0〉;〈xF,x7〉;〈xC,x3〉;〈xB,x1〉;〈x6,xE〉;〈xB,x1〉;〈x7,x0〉;〈x7,x4〉;〈x3,xB〉;
348 〈x0,xD〉;〈x6,xD〉;〈xF,xB〉;〈xE,x5〉;〈xE,x2〉;〈x6,x6〉;〈x6,x8〉;〈x0,x8〉;〈xF,xB〉;〈x3,xC〉;〈x8,xC〉;〈xD,xD〉;〈x0,x2〉;〈x2,xE〉;〈x6,xE〉;〈xF,x1〉;
349 〈xA,xF〉;〈x7,x9〉;〈x6,x7〉;〈xE,x2〉;〈x4,xC〉;〈xA,x5〉;〈x7,x9〉;〈xC,x6〉;〈xB,x5〉;〈xA,xF〉;〈x1,x5〉;〈xF,xE〉;〈xE,x2〉;〈x2,xB〉;〈xC,xA〉;〈xE,x6〉;
350 〈x3,xE〉;〈x2,xC〉;〈x5,x8〉;〈x7,x2〉;〈xC,xE〉;〈x7,x1〉;〈x8,xC〉;〈xB,xE〉;〈x2,x0〉;〈x6,x6〉;〈x0,x7〉;〈x6,xF〉;〈xD,x1〉;〈x8,x2〉;〈x3,x1〉;〈xF,x3〉;
351 〈x9,x5〉;〈x9,x1〉;〈x1,x2〉;〈xF,x3〉;〈x4,xF〉;〈x6,xC〉;〈xA,x6〉;〈x8,xE〉;〈xB,x2〉;〈x7,x8〉;〈xD,xE〉;〈x7,x9〉;〈xC,x5〉;〈x2,x2〉;〈xF,x3〉;〈x0,x7〉;
352 〈xE,x7〉;〈x9,xE〉;〈x9,x2〉;〈x7,x3〉;〈x3,xC〉;〈xA,x1〉;〈xD,xA〉;〈x2,x1〉;〈x2,x3〉;〈x4,x5〉;〈xE,x5〉;〈x7,x4〉;〈x8,x4〉;〈xC,x2〉;〈x6,x8〉;〈x3,x5〉;
353 〈x9,xA〉;〈xC,x8〉;〈x2,xE〉;〈x1,xD〉;〈xD,x1〉;〈xA,x6〉;〈xD,xF〉;〈x0,x6〉;〈x7,xF〉;〈x8,xC〉;〈x2,x8〉;〈xF,x6〉;〈xC,x3〉;〈xF,x8〉;〈x6,x2〉;〈xF,x9〉;
354 〈x5,x7〉;〈x2,x7〉;〈xD,x1〉;〈xD,x3〉;〈x0,xB〉;〈xA,x3〉;〈x8,x7〉;〈x8,x3〉;〈xC,x9〉;〈x1,x4〉;〈xB,x4〉;〈xC,x5〉;〈xE,xD〉;〈x5,x4〉;〈xE,x1〉;〈xB,x9〉;
355 〈x2,x9〉;〈x6,xF〉;〈xE,x3〉;〈x0,xD〉;〈xC,xC〉;〈xF,x6〉;〈x0,xD〉;〈x2,x4〉;〈x4,x5〉;〈x6,xE〉;〈xE,x4〉;〈xD,xB〉;〈xF,x9〉;〈xC,x1〉;〈xD,x4〉;〈xB,x4〉;
356 〈xB,x5〉;〈x6,x6〉;〈x1,xC〉;〈x6,xE〉;〈xA,xF〉;〈x4,x0〉;〈xE,x6〉;〈x4,x9〉;〈x7,xE〉;〈x4,x1〉;〈x1,x8〉;〈x8,x7〉;〈xD,xF〉;〈xB,xB〉;〈x6,x0〉;〈x0,x5〉;
357 〈xF,x4〉;〈x5,xD〉;〈xA,x1〉;〈xD,x6〉;〈x6,x7〉;〈x2,xA〉;〈xC,x8〉;〈x7,x7〉;〈xF,x9〉;〈x8,xA〉;〈xF,x9〉;〈x2,x6〉;〈xE,xF〉;〈x7,x4〉;〈x5,x8〉;〈x6,xA〉;
358 〈xC,x8〉;〈x3,x5〉;〈x1,x0〉;〈xC,x5〉;〈x1,xE〉;〈x0,xB〉;〈x8,x3〉;〈x6,xA〉;〈x4,x4〉;〈x8,xD〉;〈x5,xC〉;〈xF,xB〉;〈xF,xE〉;〈x9,x2〉;〈x0,x3〉;〈x4,x3〉;
359 〈x0,x5〉;〈xA,xF〉;〈xC,x0〉;〈xF,x3〉;〈x0,x4〉;〈x2,x8〉;〈x9,xD〉;〈x0,x9〉;〈x3,x5〉;〈xE,x3〉;〈x5,xF〉;〈x4,x5〉;〈xA,xB〉;〈xC,xD〉;〈x8,xC〉;〈xF,xD〉;
360 〈x2,xC〉;〈x9,xD〉;〈xA,xF〉;〈x6,x4〉;〈x4,x3〉;〈x8,x0〉;〈x8,x2〉;〈xE,x5〉;〈x8,xE〉;〈x3,xD〉;〈x2,xD〉;〈xD,xB〉;〈xD,xF〉;〈xA,xB〉;〈x0,x8〉;〈x1,x6〉;
361 〈xE,xC〉;〈x7,xE〉;〈xA,x7〉;〈xC,xB〉;〈xD,x8〉;〈x5,xC〉;〈x2,xC〉;〈x8,x8〉;〈x9,x8〉;〈xC,x2〉;〈xA,xD〉;〈x1,xD〉;〈xB,x0〉;〈xB,x1〉;〈xC,xE〉;〈x9,x3〉;
362 〈xE,x2〉;〈xF,x4〉;〈xD,xB〉;〈xA,x5〉;〈xB,x6〉;〈x4,x9〉;〈x8,x7〉;〈x1,xD〉;〈xA,x2〉;〈x7,x9〉;〈x3,x5〉;〈xB,xE〉;〈x5,x5〉;〈xC,xD〉;〈x6,x3〉;〈x2,xC〉
365 definition dTest_random_ex11 ≝
367 〈x1,x0〉;〈x1,xF〉;〈xE,xC〉;〈x3,xB〉;〈x8,xA〉;〈x3,xF〉;〈x3,x8〉;〈x8,x0〉;〈x1,xC〉;〈x2,xD〉;〈x9,x2〉;〈x5,xF〉;〈xE,x1〉;〈xB,x5〉;〈xB,xC〉;〈x8,x3〉;
368 〈xB,x6〉;〈x1,xB〉;〈xE,xD〉;〈x4,xF〉;〈x3,xA〉;〈xC,x4〉;〈xF,xE〉;〈xF,xF〉;〈xC,xB〉;〈x8,x1〉;〈x6,x7〉;〈xC,x2〉;〈x5,x9〉;〈xD,xA〉;〈x0,xA〉;〈x9,xC〉;
369 〈x2,x2〉;〈xE,xB〉;〈x9,x3〉;〈xE,x2〉;〈x7,xF〉;〈xA,xC〉;〈x4,xA〉;〈x8,x2〉;〈x8,x1〉;〈x3,xF〉;〈xE,xB〉;〈x8,xB〉;〈x0,xF〉;〈x9,xC〉;〈x4,x1〉;〈x8,x2〉;
370 〈x9,xB〉;〈x7,xC〉;〈x5,x1〉;〈xA,x7〉;〈xA,xB〉;〈xA,xD〉;〈x9,x2〉;〈x1,x9〉;〈xF,x0〉;〈xF,xD〉;〈x9,x3〉;〈xF,x6〉;〈xA,xD〉;〈x2,x4〉;〈xC,xB〉;〈xD,xE〉;
371 〈xB,x5〉;〈xA,xB〉;〈x8,x1〉;〈x5,x4〉;〈xA,xE〉;〈x2,x4〉;〈x6,x4〉;〈xD,x2〉;〈xD,x0〉;〈xF,xE〉;〈x3,x3〉;〈x2,xA〉;〈x7,x5〉;〈x0,x7〉;〈x8,xF〉;〈x3,xA〉;
372 〈x1,x2〉;〈x9,xF〉;〈xB,xE〉;〈x1,xB〉;〈x1,xB〉;〈x1,xF〉;〈xC,x7〉;〈xF,x1〉;〈x7,xC〉;〈x9,x1〉;〈x5,xD〉;〈x3,x2〉;〈xD,x9〉;〈xD,x6〉;〈xE,xA〉;〈x0,x6〉;
373 〈x5,xB〉;〈x6,x9〉;〈x6,xB〉;〈xA,xC〉;〈x0,x9〉;〈x1,x6〉;〈xA,x3〉;〈xC,xA〉;〈x8,xE〉;〈x8,x3〉;〈x3,x4〉;〈xB,x7〉;〈x4,x1〉;〈x2,x7〉;〈xB,x3〉;〈x0,x1〉;
374 〈xE,x6〉;〈x0,x6〉;〈x8,xC〉;〈x0,x4〉;〈x3,xD〉;〈xB,xE〉;〈x2,xC〉;〈x6,x6〉;〈xB,x5〉;〈x8,x6〉;〈x1,x1〉;〈x1,x3〉;〈x6,xD〉;〈xD,x0〉;〈xB,xE〉;〈x8,xD〉;
375 〈xC,x7〉;〈x5,x5〉;〈x0,x2〉;〈xC,x1〉;〈x7,x6〉;〈x5,xF〉;〈x2,x0〉;〈x5,xE〉;〈xE,x4〉;〈x3,xE〉;〈x7,x7〉;〈xE,x1〉;〈x3,xF〉;〈xE,x8〉;〈x6,xC〉;〈x4,xA〉;
376 〈xA,x0〉;〈xF,xE〉;〈xC,xE〉;〈x3,xF〉;〈x6,x7〉;〈x9,x4〉;〈x3,xF〉;〈xE,xF〉;〈xE,xF〉;〈x8,x6〉;〈xD,x9〉;〈x4,xA〉;〈x0,x8〉;〈x8,xB〉;〈xC,x8〉;〈x1,xC〉;
377 〈xA,xD〉;〈x2,x0〉;〈xA,x7〉;〈x8,xC〉;〈x0,x6〉;〈x6,x7〉;〈xA,xF〉;〈x7,x3〉;〈xC,xD〉;〈x1,x6〉;〈x8,x4〉;〈x3,x2〉;〈xD,x0〉;〈xF,x3〉;〈xD,xC〉;〈xD,xB〉;
378 〈xB,x7〉;〈x2,x4〉;〈x6,xA〉;〈x6,x3〉;〈x1,xC〉;〈xA,x1〉;〈xD,xE〉;〈xB,xC〉;〈x9,x2〉;〈xF,x1〉;〈x5,xC〉;〈xE,x7〉;〈xE,x0〉;〈xD,x5〉;〈xA,x4〉;〈x4,xA〉;
379 〈x0,x0〉;〈xD,x6〉;〈x2,x2〉;〈x9,xC〉;〈x5,x2〉;〈x8,xF〉;〈xE,x8〉;〈x2,x2〉;〈xA,x2〉;〈xF,x0〉;〈x9,x8〉;〈x3,x8〉;〈x0,xD〉;〈xF,x6〉;〈x4,x3〉;〈x7,x9〉;
380 〈x8,x2〉;〈xA,xF〉;〈xD,x5〉;〈xC,x1〉;〈x8,x2〉;〈x5,x2〉;〈xD,xB〉;〈x8,xF〉;〈x7,xE〉;〈xD,x1〉;〈x9,xD〉;〈xA,x6〉;〈x8,xE〉;〈x9,xE〉;〈xA,x9〉;〈x8,xE〉;
381 〈xD,x1〉;〈xF,x6〉;〈xB,x0〉;〈xE,xA〉;〈x8,x3〉;〈xE,x9〉;〈xF,x7〉;〈x3,xB〉;〈x4,xA〉;〈x0,x9〉;〈x1,xE〉;〈x3,x2〉;〈xD,x2〉;〈x5,xD〉;〈xD,x7〉;〈xA,xB〉;
382 〈x4,xD〉;〈x6,xF〉;〈x5,x9〉;〈xF,xC〉;〈x4,x3〉;〈x4,x1〉;〈x0,x0〉;〈x3,xC〉;〈x9,x4〉;〈x5,x2〉;〈x5,x9〉;〈x6,xC〉;〈x6,xE〉;〈xE,x8〉;〈x6,x6〉;〈xF,x5〉
385 definition dTest_random_ex12 ≝
387 〈x9,xC〉;〈x5,x7〉;〈x6,xC〉;〈xE,x2〉;〈x3,xB〉;〈xA,x2〉;〈x2,x1〉;〈xE,xE〉;〈xF,x6〉;〈x4,xF〉;〈xF,x3〉;〈x6,x2〉;〈xD,xB〉;〈x8,xF〉;〈x6,x4〉;〈xD,x3〉;
388 〈x8,x0〉;〈x6,x9〉;〈x9,x7〉;〈x4,x7〉;〈x8,xB〉;〈xB,x6〉;〈x3,x8〉;〈x4,x5〉;〈xB,xE〉;〈x0,xD〉;〈x6,x1〉;〈xC,xF〉;〈x7,x8〉;〈xC,xF〉;〈x4,x1〉;〈x7,xF〉;
389 〈xF,x4〉;〈x5,xA〉;〈x8,xB〉;〈x7,x2〉;〈xE,x6〉;〈x7,xD〉;〈x4,xC〉;〈x1,x8〉;〈xE,xE〉;〈x3,xA〉;〈x1,x2〉;〈x9,x4〉;〈x3,x4〉;〈x3,x0〉;〈x3,x9〉;〈x0,x0〉;
390 〈x9,x5〉;〈x6,x0〉;〈xF,xA〉;〈x7,xF〉;〈xA,x6〉;〈xC,x7〉;〈xB,x1〉;〈x7,xE〉;〈x0,xD〉;〈x2,x4〉;〈xF,xF〉;〈x4,x3〉;〈x7,x8〉;〈x8,x8〉;〈x6,xC〉;〈x0,x7〉;
391 〈x7,x3〉;〈x9,x2〉;〈xC,x8〉;〈x0,xB〉;〈x5,x0〉;〈x9,x7〉;〈xF,x4〉;〈x1,xB〉;〈xD,xB〉;〈x4,x5〉;〈x6,x2〉;〈x9,x1〉;〈x8,x7〉;〈x5,xD〉;〈xF,x5〉;〈x6,x1〉;
392 〈x3,x8〉;〈xF,x3〉;〈x8,xA〉;〈x4,xF〉;〈xD,xB〉;〈x3,xD〉;〈x4,x3〉;〈x2,xF〉;〈xB,xA〉;〈xA,x9〉;〈xB,x4〉;〈xA,x9〉;〈x2,x6〉;〈x7,xE〉;〈x8,xC〉;〈x1,x6〉;
393 〈xF,xC〉;〈x1,xC〉;〈xA,x7〉;〈x9,xD〉;〈x7,xC〉;〈x8,x5〉;〈xA,x7〉;〈x3,x5〉;〈x8,x6〉;〈x4,xF〉;〈xC,x8〉;〈x9,xA〉;〈x0,xD〉;〈x2,x4〉;〈x0,x4〉;〈x5,x8〉;
394 〈x4,x2〉;〈x3,x0〉;〈x7,x5〉;〈x8,xD〉;〈xB,xC〉;〈x7,x2〉;〈x3,x4〉;〈xF,x9〉;〈x4,x6〉;〈x5,xE〉;〈xF,x4〉;〈x5,xC〉;〈x6,x7〉;〈x0,x4〉;〈x8,x8〉;〈x2,x8〉;
395 〈xA,x9〉;〈xE,xC〉;〈xE,xC〉;〈x7,xC〉;〈x4,x6〉;〈x6,xE〉;〈x1,xC〉;〈xD,x9〉;〈xC,x0〉;〈x6,x1〉;〈x5,x8〉;〈x5,xE〉;〈x3,x7〉;〈xB,x0〉;〈x9,x9〉;〈x9,x7〉;
396 〈xA,x0〉;〈x9,xB〉;〈x7,x7〉;〈x4,xA〉;〈xD,x0〉;〈xB,x5〉;〈x1,xD〉;〈xA,x6〉;〈x4,xA〉;〈xC,x5〉;〈x3,xA〉;〈x9,x4〉;〈xB,x4〉;〈x5,x0〉;〈x0,x6〉;〈xC,x0〉;
397 〈xA,x8〉;〈x0,x2〉;〈x5,xF〉;〈x0,xE〉;〈x2,x1〉;〈x0,x3〉;〈xB,x1〉;〈x9,x6〉;〈x0,x2〉;〈x9,x7〉;〈x8,x0〉;〈x1,xA〉;〈x0,xB〉;〈x3,xD〉;〈x2,x1〉;〈x7,xF〉;
398 〈x0,x3〉;〈x2,x9〉;〈x3,x2〉;〈x6,x6〉;〈xB,xF〉;〈x3,xB〉;〈x5,x7〉;〈x5,x3〉;〈xE,x7〉;〈xD,x5〉;〈xE,x5〉;〈x4,x5〉;〈xA,x3〉;〈x1,xA〉;〈x1,xB〉;〈xF,x8〉;
399 〈xC,xF〉;〈xB,x3〉;〈x9,x5〉;〈x5,x9〉;〈x4,xE〉;〈x6,x4〉;〈x4,x3〉;〈xF,x4〉;〈x2,x5〉;〈xC,xC〉;〈x6,x1〉;〈x3,x5〉;〈xD,xF〉;〈x3,x6〉;〈x5,x5〉;〈xC,xF〉;
400 〈x9,xA〉;〈x1,x1〉;〈xF,x6〉;〈xD,x4〉;〈x4,xF〉;〈x9,xB〉;〈xA,xF〉;〈xF,x2〉;〈x0,x3〉;〈x1,x9〉;〈x9,xB〉;〈xA,xB〉;〈xC,x4〉;〈x1,x9〉;〈xA,x1〉;〈xE,xA〉;
401 〈x1,xB〉;〈x2,x5〉;〈xA,xD〉;〈xA,xA〉;〈x0,x0〉;〈x5,xB〉;〈x9,xD〉;〈x6,xF〉;〈x8,x8〉;〈x6,xF〉;〈x3,x0〉;〈x8,x5〉;〈xC,x6〉;〈x1,x7〉;〈x5,x7〉;〈x1,x1〉;
402 〈xA,xB〉;〈x0,x2〉;〈xD,xD〉;〈x9,x2〉;〈x4,xD〉;〈x8,x2〉;〈x0,x2〉;〈x3,x5〉;〈xC,xB〉;〈x4,x4〉;〈xA,x4〉;〈x4,x1〉;〈xD,x5〉;〈x1,x2〉;〈xE,x7〉;〈x4,xD〉
405 definition dTest_random_32 ≝
408 definition dTest_random_64 ≝
409 dTest_random_32@dTest_random_ex01b.
411 definition dTest_random_128 ≝
412 dTest_random_64@dTest_random_ex01c.
414 definition dTest_random_256 ≝
415 dTest_random_128@dTest_random_ex01d.
417 definition dTest_random_512 ≝
418 dTest_random_256@dTest_random_ex02.
420 definition dTest_random_1024 ≝
421 dTest_random_512@dTest_random_ex03@dTest_random_ex04.
423 definition dTest_random_2048 ≝
424 dTest_random_1024@dTest_random_ex05@dTest_random_ex06@dTest_random_ex07@dTest_random_ex08.
426 definition dTest_random_3072 ≝
427 dTest_random_2048@dTest_random_ex09@dTest_random_ex10@dTest_random_ex11@dTest_random_ex12.
429 (* campitura di 0x00 *)
430 definition dTest_bytes_aux : list byte8 ≝
432 〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;
433 〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;
434 〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;
435 〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;
436 〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;
437 〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;
438 〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;
439 〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉;〈x0,x0〉
442 (* blocco di 0x00 lungo 0x0380 da caricare dopo dati per azzerare
443 counters, index, position, e stack di esecuzione *)
444 definition dTest_bytes : list byte8 ≝
445 dTest_bytes_aux@dTest_bytes_aux@dTest_bytes_aux@dTest_bytes_aux@
446 dTest_bytes_aux@dTest_bytes_aux@dTest_bytes_aux.
projects / helm.git / blob