X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Femulator%2Fmemory%2Fmemory_struct.ma;h=26d5913ea1154ac6ee839b66718b8d174437c507;hb=2c38e6a237e6a0e263abccf8d8ef3e7a31272443;hp=0e023b5a18d1871b0d75efbd697eff75c4b96e19;hpb=0f13d14b63b012e0ea8ce0d0e71bf808fdd444eb;p=helm.git diff --git a/helm/software/matita/contribs/ng_assembly/emulator/memory/memory_struct.ma b/helm/software/matita/contribs/ng_assembly/emulator/memory/memory_struct.ma index 0e023b5a1..26d5913ea 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/memory/memory_struct.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/memory/memory_struct.ma @@ -44,6 +44,18 @@ nrecord Array16T (T:Type) : Type ≝ ; a16_9 : T ; a16_10 : T ; a16_11 : T ; a16_12 : T ; a16_13 : T ; a16_14 : T ; a16_15 : T ; a16_16 : T }. +(* operatore uguaglianza *) +ndefinition eq_ar16 ≝ +λT.λf:T → T → bool.λa1,a2:Array16T T. + (f (a16_1 ? a1) (a16_1 ? a2)) ⊗ (f (a16_2 ? a1) (a16_2 ? a2)) ⊗ + (f (a16_3 ? a1) (a16_3 ? a2)) ⊗ (f (a16_4 ? a1) (a16_4 ? a2)) ⊗ + (f (a16_5 ? a1) (a16_5 ? a2)) ⊗ (f (a16_6 ? a1) (a16_6 ? a2)) ⊗ + (f (a16_7 ? a1) (a16_7 ? a2)) ⊗ (f (a16_8 ? a1) (a16_8 ? a2)) ⊗ + (f (a16_9 ? a1) (a16_9 ? a2)) ⊗ (f (a16_10 ? a1) (a16_10 ? a2)) ⊗ + (f (a16_11 ? a1) (a16_11 ? a2)) ⊗ (f (a16_12 ? a1) (a16_12 ? a2)) ⊗ + (f (a16_13 ? a1) (a16_13 ? a2)) ⊗ (f (a16_14 ? a1) (a16_14 ? a2)) ⊗ + (f (a16_15 ? a1) (a16_15 ? a2)) ⊗ (f (a16_16 ? a1) (a16_16 ? a2)). + (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *) (* posso definire un getter a matrice sull'array *) @@ -335,6 +347,14 @@ nrecord Array8T (T:Type) : Type ≝ { a8_1 : T ; a8_2 : T ; a8_3 : T ; a8_4 : T ; a8_5 : T ; a8_6 : T ; a8_7 : T ; a8_8 : T }. +(* operatore uguaglianza *) +ndefinition eq_ar8 ≝ +λT.λf:T → T → bool.λa1,a2:Array8T T. + (f (a8_1 ? a1) (a8_1 ? a2)) ⊗ (f (a8_2 ? a1) (a8_2 ? a2)) ⊗ + (f (a8_3 ? a1) (a8_3 ? a2)) ⊗ (f (a8_4 ? a1) (a8_4 ? a2)) ⊗ + (f (a8_5 ? a1) (a8_5 ? a2)) ⊗ (f (a8_6 ? a1) (a8_6 ? a2)) ⊗ + (f (a8_7 ? a1) (a8_7 ? a2)) ⊗ (f (a8_8 ? a1) (a8_8 ? a2)). + (* abbiamo gia' gli ottali come tipo induttivo quindi: *) (* posso definire un getter a matrice sull'array *) ndefinition getn_array8T ≝ @@ -357,303 +377,57 @@ let e05 ≝ (a8_6 T p) in let e06 ≝ (a8_7 T p) in let e07 ≝ (a8_8 T p) in match n with - [ o0 ⇒ mk_Array8T T e07 e06 e05 e04 e03 e02 e01 v - | o1 ⇒ mk_Array8T T e07 e06 e05 e04 e03 e02 v e00 - | o2 ⇒ mk_Array8T T e07 e06 e05 e04 e03 v e01 e00 - | o3 ⇒ mk_Array8T T e07 e06 e05 e04 v e02 e01 e00 - | o4 ⇒ mk_Array8T T e07 e06 e05 v e03 e02 e01 e00 - | o5 ⇒ mk_Array8T T e07 e06 v e04 e03 e02 e01 e00 - | o6 ⇒ mk_Array8T T e07 v e05 e04 e03 e02 e01 e00 - | o7 ⇒ mk_Array8T T v e06 e05 e04 e03 e02 e01 e00 + [ o0 ⇒ mk_Array8T T v e01 e02 e03 e04 e05 e06 e07 + | o1 ⇒ mk_Array8T T e00 v e02 e03 e04 e05 e06 e07 + | o2 ⇒ mk_Array8T T e00 e01 v e03 e04 e05 e06 e07 + | o3 ⇒ mk_Array8T T e00 e01 e02 v e04 e05 e06 e07 + | o4 ⇒ mk_Array8T T e00 e01 e02 e03 v e05 e06 e07 + | o5 ⇒ mk_Array8T T e00 e01 e02 e03 e04 v e06 e07 + | o6 ⇒ mk_Array8T T e00 e01 e02 e03 e04 e05 v e07 + | o7 ⇒ mk_Array8T T e00 e01 e02 e03 e04 e05 e06 v ]. (* lettura byte *) ndefinition byte8_of_bits ≝ λp:Array8T bool. mk_byte8 - (or_ex (match a8_8 ? p with [ true ⇒ x8 | false ⇒ x0 ]) - (or_ex (match a8_7 ? p with [ true ⇒ x4 | false ⇒ x0 ]) - (or_ex (match a8_6 ? p with [ true ⇒ x2 | false ⇒ x0 ]) - (match a8_5 ? p with [ true ⇒ x1 | false ⇒ x0 ])))) - (or_ex (match a8_4 ? p with [ true ⇒ x8 | false ⇒ x0 ]) - (or_ex (match a8_3 ? p with [ true ⇒ x4 | false ⇒ x0 ]) - (or_ex (match a8_2 ? p with [ true ⇒ x2 | false ⇒ x0 ]) - (match a8_1 ? p with [ true ⇒ x1 | false ⇒ x0 ])))). + (or_ex (match a8_1 ? p with [ true ⇒ x8 | false ⇒ x0 ]) + (or_ex (match a8_2 ? p with [ true ⇒ x4 | false ⇒ x0 ]) + (or_ex (match a8_3 ? p with [ true ⇒ x2 | false ⇒ x0 ]) + (match a8_4 ? p with [ true ⇒ x1 | false ⇒ x0 ])))) + (or_ex (match a8_5 ? p with [ true ⇒ x8 | false ⇒ x0 ]) + (or_ex (match a8_6 ? p with [ true ⇒ x4 | false ⇒ x0 ]) + (or_ex (match a8_7 ? p with [ true ⇒ x2 | false ⇒ x0 ]) + (match a8_8 ? p with [ true ⇒ x1 | false ⇒ x0 ])))). (* scrittura byte *) +ndefinition bits_of_exadecim ≝ +λe:exadecim.match e with + [ x0 ⇒ quadruple … false false false false + | x1 ⇒ quadruple … false false false true + | x2 ⇒ quadruple … false false true false + | x3 ⇒ quadruple … false false true true + | x4 ⇒ quadruple … false true false false + | x5 ⇒ quadruple … false true false true + | x6 ⇒ quadruple … false true true false + | x7 ⇒ quadruple … false true true true + | x8 ⇒ quadruple … true false false false + | x9 ⇒ quadruple … true false false true + | xA ⇒ quadruple … true false true false + | xB ⇒ quadruple … true false true true + | xC ⇒ quadruple … true true false false + | xD ⇒ quadruple … true true false true + | xE ⇒ quadruple … true true true false + | xF ⇒ quadruple … true true true true + ]. + ndefinition bits_of_byte8 ≝ -λp:byte8. - match b8h p with - [ x0 ⇒ match b8l p with - [ x0 ⇒ mk_Array8T bool false false false false false false false false - | x1 ⇒ mk_Array8T bool false false false false false false false true - | x2 ⇒ mk_Array8T bool false false false false false false true false - | x3 ⇒ mk_Array8T bool false false false false false false true true - | x4 ⇒ mk_Array8T bool false false false false false true false false - | x5 ⇒ mk_Array8T bool false false false false false true false true - | x6 ⇒ mk_Array8T bool false false false false false true true false - | x7 ⇒ mk_Array8T bool false false false false false true true true - | x8 ⇒ mk_Array8T bool false false false false true false false false - | x9 ⇒ mk_Array8T bool false false false false true false false true - | xA ⇒ mk_Array8T bool false false false false true false true false - | xB ⇒ mk_Array8T bool false false false false true false true true - | xC ⇒ mk_Array8T bool false false false false true true false false - | xD ⇒ mk_Array8T bool false false false false true true false true - | xE ⇒ mk_Array8T bool false false false false true true true false - | xF ⇒ mk_Array8T bool false false false false true true true true ] - | x1 ⇒ match b8l p with - [ x0 ⇒ mk_Array8T bool false false false true false false false false - | x1 ⇒ mk_Array8T bool false false false true false false false true - | x2 ⇒ mk_Array8T bool false false false true false false true false - | x3 ⇒ mk_Array8T bool false false false true false false true true - | x4 ⇒ mk_Array8T bool false false false true false true false false - | x5 ⇒ mk_Array8T bool false false false true false true false true - | x6 ⇒ mk_Array8T bool false false false true false true true false - | x7 ⇒ mk_Array8T bool false false false true false true true true - | x8 ⇒ mk_Array8T bool false false false true true false false false - | x9 ⇒ mk_Array8T bool false false false true true false false true - | xA ⇒ mk_Array8T bool false false false true true false true false - | xB ⇒ mk_Array8T bool false false false true true false true true - | xC ⇒ mk_Array8T bool false false false true true true false false - | xD ⇒ mk_Array8T bool false false false true true true false true - | xE ⇒ mk_Array8T bool false false false true true true true false - | xF ⇒ mk_Array8T bool false false false true true true true true ] - | x2 ⇒ match b8l p with - [ x0 ⇒ mk_Array8T bool false false true false false false false false - | x1 ⇒ mk_Array8T bool false false true false false false false true - | x2 ⇒ mk_Array8T bool false false true false false false true false - | x3 ⇒ mk_Array8T bool false false true false false false true true - | x4 ⇒ mk_Array8T bool false false true false false true false false - | x5 ⇒ mk_Array8T bool false false true false false true false true - | x6 ⇒ mk_Array8T bool false false true false false true true false - | x7 ⇒ mk_Array8T bool false false true false false true true true - | x8 ⇒ mk_Array8T bool false false true false true false false false - | x9 ⇒ mk_Array8T bool false false true false true false false true - | xA ⇒ mk_Array8T bool false false true false true false true false - | xB ⇒ mk_Array8T bool false false true false true false true true - | xC ⇒ mk_Array8T bool false false true false true true false false - | xD ⇒ mk_Array8T bool false false true false true true false true - | xE ⇒ mk_Array8T bool false false true false true true true false - | xF ⇒ mk_Array8T bool false false true false true true true true ] - | x3 ⇒ match b8l p with - [ x0 ⇒ mk_Array8T bool false false true true false false false false - | x1 ⇒ mk_Array8T bool false false true true false false false true - | x2 ⇒ mk_Array8T bool false false true true false false true false - | x3 ⇒ mk_Array8T bool false false true true false false true true - | x4 ⇒ mk_Array8T bool false false true true false true false false - | x5 ⇒ mk_Array8T bool false false true true false true false true - | x6 ⇒ mk_Array8T bool false false true true false true true false - | x7 ⇒ mk_Array8T bool false false true true false true true true - | x8 ⇒ mk_Array8T bool false false true true true false false false - | x9 ⇒ mk_Array8T bool false false true true true false false true - | xA ⇒ mk_Array8T bool false false true true true false true false - | xB ⇒ mk_Array8T bool false false true true true false true true - | xC ⇒ mk_Array8T bool false false true true true true false false - | xD ⇒ mk_Array8T bool false false true true true true false true - | xE ⇒ mk_Array8T bool false false true true true true true false - | xF ⇒ mk_Array8T bool false false true true true true true true ] - | x4 ⇒ match b8l p with - [ x0 ⇒ mk_Array8T bool false true false false false false false false - | x1 ⇒ mk_Array8T bool false true false false false false false true - | x2 ⇒ mk_Array8T bool false true false false false false true false - | x3 ⇒ mk_Array8T bool false true false false false false true true - | x4 ⇒ mk_Array8T bool false true false false false true false false - | x5 ⇒ mk_Array8T bool false true false false false true false true - | x6 ⇒ mk_Array8T bool false true false false false true true false - | x7 ⇒ mk_Array8T bool false true false false false true true true - | x8 ⇒ mk_Array8T bool false true false false true false false false - | x9 ⇒ mk_Array8T bool false true false false true false false true - | xA ⇒ mk_Array8T bool false true false false true false true false - | xB ⇒ mk_Array8T bool false true false false true false true true - | xC ⇒ mk_Array8T bool false true false false true true false false - | xD ⇒ mk_Array8T bool false true false false true true false true - | xE ⇒ mk_Array8T bool false true false false true true true false - | xF ⇒ mk_Array8T bool false true false false true true true true ] - | x5 ⇒ match b8l p with - [ x0 ⇒ mk_Array8T bool false true false true false false false false - | x1 ⇒ mk_Array8T bool false true false true false false false true - | x2 ⇒ mk_Array8T bool false true false true false false true false - | x3 ⇒ mk_Array8T bool false true false true false false true true - | x4 ⇒ mk_Array8T bool false true false true false true false false - | x5 ⇒ mk_Array8T bool false true false true false true false true - | x6 ⇒ mk_Array8T bool false true false true false true true false - | x7 ⇒ mk_Array8T bool false true false true false true true true - | x8 ⇒ mk_Array8T bool false true false true true false false false - | x9 ⇒ mk_Array8T bool false true false true true false false true - | xA ⇒ mk_Array8T bool false true false true true false true false - | xB ⇒ mk_Array8T bool false true false true true false true true - | xC ⇒ mk_Array8T bool false true false true true true false false - | xD ⇒ mk_Array8T bool false true false true true true false true - | xE ⇒ mk_Array8T bool false true false true true true true false - | xF ⇒ mk_Array8T bool false true false true true true true true ] - | x6 ⇒ match b8l p with - [ x0 ⇒ mk_Array8T bool false true true false false false false false - | x1 ⇒ mk_Array8T bool false true true false false false false true - | x2 ⇒ mk_Array8T bool false true true false false false true false - | x3 ⇒ mk_Array8T bool false true true false false false true true - | x4 ⇒ mk_Array8T bool false true true false false true false false - | x5 ⇒ mk_Array8T bool false true true false false true false true - | x6 ⇒ mk_Array8T bool false true true false false true true false - | x7 ⇒ mk_Array8T bool false true true false false true true true - | x8 ⇒ mk_Array8T bool false true true false true false false false - | x9 ⇒ mk_Array8T bool false true true false true false false true - | xA ⇒ mk_Array8T bool false true true false true false true false - | xB ⇒ mk_Array8T bool false true true false true false true true - | xC ⇒ mk_Array8T bool false true true false true true false false - | xD ⇒ mk_Array8T bool false true true false true true false true - | xE ⇒ mk_Array8T bool false true true false true true true false - | xF ⇒ mk_Array8T bool false true true false true true true true ] - | x7 ⇒ match b8l p with - [ x0 ⇒ mk_Array8T bool false true true true false false false false - | x1 ⇒ mk_Array8T bool false true true true false false false true - | x2 ⇒ mk_Array8T bool false true true true false false true false - | x3 ⇒ mk_Array8T bool false true true true false false true true - | x4 ⇒ mk_Array8T bool false true true true false true false false - | x5 ⇒ mk_Array8T bool false true true true false true false true - | x6 ⇒ mk_Array8T bool false true true true false true true false - | x7 ⇒ mk_Array8T bool false true true true false true true true - | x8 ⇒ mk_Array8T bool false true true true true false false false - | x9 ⇒ mk_Array8T bool false true true true true false false true - | xA ⇒ mk_Array8T bool false true true true true false true false - | xB ⇒ mk_Array8T bool false true true true true false true true - | xC ⇒ mk_Array8T bool false true true true true true false false - | xD ⇒ mk_Array8T bool false true true true true true false true - | xE ⇒ mk_Array8T bool false true true true true true true false - | xF ⇒ mk_Array8T bool false true true true true true true true ] - | x8 ⇒ match b8l p with - [ x0 ⇒ mk_Array8T bool true false false false false false false false - | x1 ⇒ mk_Array8T bool true false false false false false false true - | x2 ⇒ mk_Array8T bool true false false false false false true false - | x3 ⇒ mk_Array8T bool true false false false false false true true - | x4 ⇒ mk_Array8T bool true false false false false true false false - | x5 ⇒ mk_Array8T bool true false false false false true false true - | x6 ⇒ mk_Array8T bool true false false false false true true false - | x7 ⇒ mk_Array8T bool true false false false false true true true - | x8 ⇒ mk_Array8T bool true false false false true false false false - | x9 ⇒ mk_Array8T bool true false false false true false false true - | xA ⇒ mk_Array8T bool true false false false true false true false - | xB ⇒ mk_Array8T bool true false false false true false true true - | xC ⇒ mk_Array8T bool true false false false true true false false - | xD ⇒ mk_Array8T bool true false false false true true false true - | xE ⇒ mk_Array8T bool true false false false true true true false - | xF ⇒ mk_Array8T bool true false false false true true true true ] - | x9 ⇒ match b8l p with - [ x0 ⇒ mk_Array8T bool true false false true false false false false - | x1 ⇒ mk_Array8T bool true false false true false false false true - | x2 ⇒ mk_Array8T bool true false false true false false true false - | x3 ⇒ mk_Array8T bool true false false true false false true true - | x4 ⇒ mk_Array8T bool true false false true false true false false - | x5 ⇒ mk_Array8T bool true false false true false true false true - | x6 ⇒ mk_Array8T bool true false false true false true true false - | x7 ⇒ mk_Array8T bool true false false true false true true true - | x8 ⇒ mk_Array8T bool true false false true true false false false - | x9 ⇒ mk_Array8T bool true false false true true false false true - | xA ⇒ mk_Array8T bool true false false true true false true false - | xB ⇒ mk_Array8T bool true false false true true false true true - | xC ⇒ mk_Array8T bool true false false true true true false false - | xD ⇒ mk_Array8T bool true false false true true true false true - | xE ⇒ mk_Array8T bool true false false true true true true false - | xF ⇒ mk_Array8T bool true false false true true true true true ] - | xA ⇒ match b8l p with - [ x0 ⇒ mk_Array8T bool true false true false false false false false - | x1 ⇒ mk_Array8T bool true false true false false false false true - | x2 ⇒ mk_Array8T bool true false true false false false true false - | x3 ⇒ mk_Array8T bool true false true false false false true true - | x4 ⇒ mk_Array8T bool true false true false false true false false - | x5 ⇒ mk_Array8T bool true false true false false true false true - | x6 ⇒ mk_Array8T bool true false true false false true true false - | x7 ⇒ mk_Array8T bool true false true false false true true true - | x8 ⇒ mk_Array8T bool true false true false true false false false - | x9 ⇒ mk_Array8T bool true false true false true false false true - | xA ⇒ mk_Array8T bool true false true false true false true false - | xB ⇒ mk_Array8T bool true false true false true false true true - | xC ⇒ mk_Array8T bool true false true false true true false false - | xD ⇒ mk_Array8T bool true false true false true true false true - | xE ⇒ mk_Array8T bool true false true false true true true false - | xF ⇒ mk_Array8T bool true false true false true true true true ] - | xB ⇒ match b8l p with - [ x0 ⇒ mk_Array8T bool true false true true false false false false - | x1 ⇒ mk_Array8T bool true false true true false false false true - | x2 ⇒ mk_Array8T bool true false true true false false true false - | x3 ⇒ mk_Array8T bool true false true true false false true true - | x4 ⇒ mk_Array8T bool true false true true false true false false - | x5 ⇒ mk_Array8T bool true false true true false true false true - | x6 ⇒ mk_Array8T bool true false true true false true true false - | x7 ⇒ mk_Array8T bool true false true true false true true true - | x8 ⇒ mk_Array8T bool true false true true true false false false - | x9 ⇒ mk_Array8T bool true false true true true false false true - | xA ⇒ mk_Array8T bool true false true true true false true false - | xB ⇒ mk_Array8T bool true false true true true false true true - | xC ⇒ mk_Array8T bool true false true true true true false false - | xD ⇒ mk_Array8T bool true false true true true true false true - | xE ⇒ mk_Array8T bool true false true true true true true false - | xF ⇒ mk_Array8T bool true false true true true true true true ] - | xC ⇒ match b8l p with - [ x0 ⇒ mk_Array8T bool true true false false false false false false - | x1 ⇒ mk_Array8T bool true true false false false false false true - | x2 ⇒ mk_Array8T bool true true false false false false true false - | x3 ⇒ mk_Array8T bool true true false false false false true true - | x4 ⇒ mk_Array8T bool true true false false false true false false - | x5 ⇒ mk_Array8T bool true true false false false true false true - | x6 ⇒ mk_Array8T bool true true false false false true true false - | x7 ⇒ mk_Array8T bool true true false false false true true true - | x8 ⇒ mk_Array8T bool true true false false true false false false - | x9 ⇒ mk_Array8T bool true true false false true false false true - | xA ⇒ mk_Array8T bool true true false false true false true false - | xB ⇒ mk_Array8T bool true true false false true false true true - | xC ⇒ mk_Array8T bool true true false false true true false false - | xD ⇒ mk_Array8T bool true true false false true true false true - | xE ⇒ mk_Array8T bool true true false false true true true false - | xF ⇒ mk_Array8T bool true true false false true true true true ] - | xD ⇒ match b8l p with - [ x0 ⇒ mk_Array8T bool true true false true false false false false - | x1 ⇒ mk_Array8T bool true true false true false false false true - | x2 ⇒ mk_Array8T bool true true false true false false true false - | x3 ⇒ mk_Array8T bool true true false true false false true true - | x4 ⇒ mk_Array8T bool true true false true false true false false - | x5 ⇒ mk_Array8T bool true true false true false true false true - | x6 ⇒ mk_Array8T bool true true false true false true true false - | x7 ⇒ mk_Array8T bool true true false true false true true true - | x8 ⇒ mk_Array8T bool true true false true true false false false - | x9 ⇒ mk_Array8T bool true true false true true false false true - | xA ⇒ mk_Array8T bool true true false true true false true false - | xB ⇒ mk_Array8T bool true true false true true false true true - | xC ⇒ mk_Array8T bool true true false true true true false false - | xD ⇒ mk_Array8T bool true true false true true true false true - | xE ⇒ mk_Array8T bool true true false true true true true false - | xF ⇒ mk_Array8T bool true true false true true true true true ] - | xE ⇒ match b8l p with - [ x0 ⇒ mk_Array8T bool true true true false false false false false - | x1 ⇒ mk_Array8T bool true true true false false false false true - | x2 ⇒ mk_Array8T bool true true true false false false true false - | x3 ⇒ mk_Array8T bool true true true false false false true true - | x4 ⇒ mk_Array8T bool true true true false false true false false - | x5 ⇒ mk_Array8T bool true true true false false true false true - | x6 ⇒ mk_Array8T bool true true true false false true true false - | x7 ⇒ mk_Array8T bool true true true false false true true true - | x8 ⇒ mk_Array8T bool true true true false true false false false - | x9 ⇒ mk_Array8T bool true true true false true false false true - | xA ⇒ mk_Array8T bool true true true false true false true false - | xB ⇒ mk_Array8T bool true true true false true false true true - | xC ⇒ mk_Array8T bool true true true false true true false false - | xD ⇒ mk_Array8T bool true true true false true true false true - | xE ⇒ mk_Array8T bool true true true false true true true false - | xF ⇒ mk_Array8T bool true true true false true true true true ] - | xF ⇒ match b8l p with - [ x0 ⇒ mk_Array8T bool true true true true false false false false - | x1 ⇒ mk_Array8T bool true true true true false false false true - | x2 ⇒ mk_Array8T bool true true true true false false true false - | x3 ⇒ mk_Array8T bool true true true true false false true true - | x4 ⇒ mk_Array8T bool true true true true false true false false - | x5 ⇒ mk_Array8T bool true true true true false true false true - | x6 ⇒ mk_Array8T bool true true true true false true true false - | x7 ⇒ mk_Array8T bool true true true true false true true true - | x8 ⇒ mk_Array8T bool true true true true true false false false - | x9 ⇒ mk_Array8T bool true true true true true false false true - | xA ⇒ mk_Array8T bool true true true true true false true false - | xB ⇒ mk_Array8T bool true true true true true false true true - | xC ⇒ mk_Array8T bool true true true true true true false false - | xD ⇒ mk_Array8T bool true true true true true true false true - | xE ⇒ mk_Array8T bool true true true true true true true false - | xF ⇒ mk_Array8T bool true true true true true true true true ] - ]. +λb:byte8. + mk_Array8T ? (fst4T … (bits_of_exadecim (cnH ? b))) + (snd4T … (bits_of_exadecim (cnH ? b))) + (thd4T … (bits_of_exadecim (cnH ? b))) + (fth4T … (bits_of_exadecim (cnH ? b))) + (fst4T … (bits_of_exadecim (cnL ? b))) + (snd4T … (bits_of_exadecim (cnL ? b))) + (thd4T … (bits_of_exadecim (cnL ? b))) + (fth4T … (bits_of_exadecim (cnL ? b))).