Add notations for mulx involving uint8_t

1 files changed, 528 insertions, 0 deletions

diff --git a/src/Compilers/Z/CNotations.v b/src/Compilers/Z/CNotations.v
index 699538012..26d944901 100644
--- a/src/Compilers/Z/CNotations.v
+++ b/src/Compilers/Z/CNotations.v
@@ -282,6 +282,22 @@ for opn, op in (('mulx', 'MulSplit'),):
             for v1 in (False, True):
                 a = ('a' if not v0 else '(Var a)')
                 b = ('b' if not v1 else '(Var b)')
+                for lgwordsz_small in (0, 3):
+                    for notation_string in ('Notation "%s\'%s_u%d\' ( a , b )" := (Op (%s %d (TWord %d) (TWord %d) (TWord %d) (TWord %d)) (Pair %s %s)).',
+                                            ('(' + '*Notation "T0 out ; T1 c_out = %s\'_%s_u%d\' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (%s %d (TWord %d) (TWord %d) (TWord %d) (TWord %d)) (Pair %s %s)) (fun \'((out, c_out)%%core) => REST)).*' + ')')):
+                        for arg1 in (lgwordsz_small, lgwordsz):
+                            for arg2 in (lgwordsz_small, lgwordsz):
+                                for arg3 in (lgwordsz, ): # N.B. the third argument, which is the high bits, must be of a compatible pointer type, and cannot be a pointer to a short word
+                                    for arg4 in (lgwordsz_small, lgwordsz):
+                                        cast_val = ('' if arg4 == lgwordsz and arg3 == lgwordsz else (cast_pat % (types[lgwordsz_small], '')))
+                                        print(notation_string % (cast_val, opn, wordsz, op, wordsz, arg1, arg2, arg3, arg4, a, b))
+for opn, op in (('mulx', 'MulSplit'),):
+    for wordsz in (32, 64, 128, 51):
+        lgwordsz = log2_up(wordsz)
+        for v0 in (False, True):
+            for v1 in (False, True):
+                a = ('a' if not v0 else '(Var a)')
+                b = ('b' if not v1 else '(Var b)')
                 print(('Notation "\'%s_u%d\' ( a , b )" := (Op (%s %d (TWord %d) (TWord %d) (TWord %d) (TWord %d)) (Pair %s %s)).') % (opn, wordsz, op, wordsz, lgwordsz, lgwordsz, lgwordsz, lgwordsz, a, b))
                 print(('(' + '*Notation "T0 out ; T1 c_out = \'_%s_u%d\' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (%s %d (TWord %d) (TWord %d) (TWord %d) (TWord %d)) (Pair %s %s)) (fun \'((out, c_out)%%core) => REST)).*' + ')') % (opn, wordsz, op, wordsz, lgwordsz, lgwordsz, lgwordsz, lgwordsz, a, b))
 for opn, op in (('addcarryx', 'AddWithGetCarry'), ('subborrow', 'SubWithGetBorrow')):
@@ -2859,6 +2875,518 @@ Notation "'subborrow_u51' ( c , a , b )" := (Op (SubWithGetBorrow 51 (TWord 3) (
 (*Notation "T0 out ; T1 c_out = '_subborrow_u51' ( c , a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (SubWithGetBorrow 51 (TWord 3) (TWord 3) (TWord 6) (TWord 6) (TWord 3)) (Pair (Pair (Var c) (Var a)) (Var b))) (fun '((out, c_out)%core) => REST)).*)
 (*Notation "T0 out ; T1 c_out = '_subborrow_u51' ( c , a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (SubWithGetBorrow 51 (TWord 3) (TWord 6) (TWord 3) (TWord 6) (TWord 3)) (Pair (Pair (Var c) (Var a)) (Var b))) (fun '((out, c_out)%core) => REST)).*)
 (*Notation "T0 out ; T1 c_out = '_subborrow_u51' ( c , a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (SubWithGetBorrow 51 (TWord 3) (TWord 3) (TWord 3) (TWord 6) (TWord 3)) (Pair (Pair (Var c) (Var a)) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(bool)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 0) (TWord 0) (TWord 5) (TWord 0)) (Pair a b)).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 0) (TWord 0) (TWord 5) (TWord 5)) (Pair a b)).
+Notation "'(bool)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 0) (TWord 5) (TWord 5) (TWord 0)) (Pair a b)).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 0) (TWord 5) (TWord 5) (TWord 5)) (Pair a b)).
+Notation "'(bool)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 0) (TWord 5) (TWord 0)) (Pair a b)).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 0) (TWord 5) (TWord 5)) (Pair a b)).
+Notation "'(bool)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 0)) (Pair a b)).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 5)) (Pair a b)).
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 0) (TWord 0) (TWord 5) (TWord 0)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 0) (TWord 0) (TWord 5) (TWord 5)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 0) (TWord 5) (TWord 5) (TWord 0)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 0) (TWord 5) (TWord 5) (TWord 5)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 0) (TWord 5) (TWord 0)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 0) (TWord 5) (TWord 5)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 0)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 5)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(uint8_t)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 3) (TWord 3) (TWord 5) (TWord 3)) (Pair a b)).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 3) (TWord 3) (TWord 5) (TWord 5)) (Pair a b)).
+Notation "'(uint8_t)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 3) (TWord 5) (TWord 5) (TWord 3)) (Pair a b)).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 3) (TWord 5) (TWord 5) (TWord 5)) (Pair a b)).
+Notation "'(uint8_t)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 3) (TWord 5) (TWord 3)) (Pair a b)).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 3) (TWord 5) (TWord 5)) (Pair a b)).
+Notation "'(uint8_t)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 3)) (Pair a b)).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 5)) (Pair a b)).
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 3) (TWord 3) (TWord 5) (TWord 3)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 3) (TWord 3) (TWord 5) (TWord 5)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 3) (TWord 5) (TWord 5) (TWord 3)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 3) (TWord 5) (TWord 5) (TWord 5)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 3) (TWord 5) (TWord 3)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 3) (TWord 5) (TWord 5)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 3)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 5)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(bool)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 0) (TWord 0) (TWord 5) (TWord 0)) (Pair a (Var b))).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 0) (TWord 0) (TWord 5) (TWord 5)) (Pair a (Var b))).
+Notation "'(bool)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 0) (TWord 5) (TWord 5) (TWord 0)) (Pair a (Var b))).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 0) (TWord 5) (TWord 5) (TWord 5)) (Pair a (Var b))).
+Notation "'(bool)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 0) (TWord 5) (TWord 0)) (Pair a (Var b))).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 0) (TWord 5) (TWord 5)) (Pair a (Var b))).
+Notation "'(bool)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 0)) (Pair a (Var b))).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 5)) (Pair a (Var b))).
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 0) (TWord 0) (TWord 5) (TWord 0)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 0) (TWord 0) (TWord 5) (TWord 5)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 0) (TWord 5) (TWord 5) (TWord 0)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 0) (TWord 5) (TWord 5) (TWord 5)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 0) (TWord 5) (TWord 0)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 0) (TWord 5) (TWord 5)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 0)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 5)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(uint8_t)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 3) (TWord 3) (TWord 5) (TWord 3)) (Pair a (Var b))).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 3) (TWord 3) (TWord 5) (TWord 5)) (Pair a (Var b))).
+Notation "'(uint8_t)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 3) (TWord 5) (TWord 5) (TWord 3)) (Pair a (Var b))).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 3) (TWord 5) (TWord 5) (TWord 5)) (Pair a (Var b))).
+Notation "'(uint8_t)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 3) (TWord 5) (TWord 3)) (Pair a (Var b))).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 3) (TWord 5) (TWord 5)) (Pair a (Var b))).
+Notation "'(uint8_t)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 3)) (Pair a (Var b))).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 5)) (Pair a (Var b))).
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 3) (TWord 3) (TWord 5) (TWord 3)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 3) (TWord 3) (TWord 5) (TWord 5)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 3) (TWord 5) (TWord 5) (TWord 3)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 3) (TWord 5) (TWord 5) (TWord 5)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 3) (TWord 5) (TWord 3)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 3) (TWord 5) (TWord 5)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 3)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 5)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(bool)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 0) (TWord 0) (TWord 5) (TWord 0)) (Pair (Var a) b)).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 0) (TWord 0) (TWord 5) (TWord 5)) (Pair (Var a) b)).
+Notation "'(bool)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 0) (TWord 5) (TWord 5) (TWord 0)) (Pair (Var a) b)).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 0) (TWord 5) (TWord 5) (TWord 5)) (Pair (Var a) b)).
+Notation "'(bool)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 0) (TWord 5) (TWord 0)) (Pair (Var a) b)).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 0) (TWord 5) (TWord 5)) (Pair (Var a) b)).
+Notation "'(bool)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 0)) (Pair (Var a) b)).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 5)) (Pair (Var a) b)).
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 0) (TWord 0) (TWord 5) (TWord 0)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 0) (TWord 0) (TWord 5) (TWord 5)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 0) (TWord 5) (TWord 5) (TWord 0)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 0) (TWord 5) (TWord 5) (TWord 5)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 0) (TWord 5) (TWord 0)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 0) (TWord 5) (TWord 5)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 0)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 5)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(uint8_t)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 3) (TWord 3) (TWord 5) (TWord 3)) (Pair (Var a) b)).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 3) (TWord 3) (TWord 5) (TWord 5)) (Pair (Var a) b)).
+Notation "'(uint8_t)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 3) (TWord 5) (TWord 5) (TWord 3)) (Pair (Var a) b)).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 3) (TWord 5) (TWord 5) (TWord 5)) (Pair (Var a) b)).
+Notation "'(uint8_t)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 3) (TWord 5) (TWord 3)) (Pair (Var a) b)).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 3) (TWord 5) (TWord 5)) (Pair (Var a) b)).
+Notation "'(uint8_t)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 3)) (Pair (Var a) b)).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 5)) (Pair (Var a) b)).
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 3) (TWord 3) (TWord 5) (TWord 3)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 3) (TWord 3) (TWord 5) (TWord 5)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 3) (TWord 5) (TWord 5) (TWord 3)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 3) (TWord 5) (TWord 5) (TWord 5)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 3) (TWord 5) (TWord 3)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 3) (TWord 5) (TWord 5)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 3)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 5)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(bool)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 0) (TWord 0) (TWord 5) (TWord 0)) (Pair (Var a) (Var b))).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 0) (TWord 0) (TWord 5) (TWord 5)) (Pair (Var a) (Var b))).
+Notation "'(bool)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 0) (TWord 5) (TWord 5) (TWord 0)) (Pair (Var a) (Var b))).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 0) (TWord 5) (TWord 5) (TWord 5)) (Pair (Var a) (Var b))).
+Notation "'(bool)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 0) (TWord 5) (TWord 0)) (Pair (Var a) (Var b))).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 0) (TWord 5) (TWord 5)) (Pair (Var a) (Var b))).
+Notation "'(bool)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 0)) (Pair (Var a) (Var b))).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 5)) (Pair (Var a) (Var b))).
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 0) (TWord 0) (TWord 5) (TWord 0)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 0) (TWord 0) (TWord 5) (TWord 5)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 0) (TWord 5) (TWord 5) (TWord 0)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 0) (TWord 5) (TWord 5) (TWord 5)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 0) (TWord 5) (TWord 0)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 0) (TWord 5) (TWord 5)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 0)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 5)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(uint8_t)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 3) (TWord 3) (TWord 5) (TWord 3)) (Pair (Var a) (Var b))).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 3) (TWord 3) (TWord 5) (TWord 5)) (Pair (Var a) (Var b))).
+Notation "'(uint8_t)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 3) (TWord 5) (TWord 5) (TWord 3)) (Pair (Var a) (Var b))).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 3) (TWord 5) (TWord 5) (TWord 5)) (Pair (Var a) (Var b))).
+Notation "'(uint8_t)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 3) (TWord 5) (TWord 3)) (Pair (Var a) (Var b))).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 3) (TWord 5) (TWord 5)) (Pair (Var a) (Var b))).
+Notation "'(uint8_t)' 'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 3)) (Pair (Var a) (Var b))).
+Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 5)) (Pair (Var a) (Var b))).
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 3) (TWord 3) (TWord 5) (TWord 3)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 3) (TWord 3) (TWord 5) (TWord 5)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 3) (TWord 5) (TWord 5) (TWord 3)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 3) (TWord 5) (TWord 5) (TWord 5)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 3) (TWord 5) (TWord 3)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 3) (TWord 5) (TWord 5)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 3)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 5)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(bool)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 0) (TWord 0) (TWord 6) (TWord 0)) (Pair a b)).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 0) (TWord 0) (TWord 6) (TWord 6)) (Pair a b)).
+Notation "'(bool)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 0) (TWord 6) (TWord 6) (TWord 0)) (Pair a b)).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 0) (TWord 6) (TWord 6) (TWord 6)) (Pair a b)).
+Notation "'(bool)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 0) (TWord 6) (TWord 0)) (Pair a b)).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 0) (TWord 6) (TWord 6)) (Pair a b)).
+Notation "'(bool)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 0)) (Pair a b)).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair a b)).
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 0) (TWord 0) (TWord 6) (TWord 0)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 0) (TWord 0) (TWord 6) (TWord 6)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 0) (TWord 6) (TWord 6) (TWord 0)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 0) (TWord 6) (TWord 6) (TWord 6)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 0) (TWord 6) (TWord 0)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 0) (TWord 6) (TWord 6)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 0)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(uint8_t)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 3) (TWord 3) (TWord 6) (TWord 3)) (Pair a b)).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 3) (TWord 3) (TWord 6) (TWord 6)) (Pair a b)).
+Notation "'(uint8_t)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 3) (TWord 6) (TWord 6) (TWord 3)) (Pair a b)).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 3) (TWord 6) (TWord 6) (TWord 6)) (Pair a b)).
+Notation "'(uint8_t)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 3) (TWord 6) (TWord 3)) (Pair a b)).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 3) (TWord 6) (TWord 6)) (Pair a b)).
+Notation "'(uint8_t)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 3)) (Pair a b)).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair a b)).
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 3) (TWord 3) (TWord 6) (TWord 3)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 3) (TWord 3) (TWord 6) (TWord 6)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 3) (TWord 6) (TWord 6) (TWord 3)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 3) (TWord 6) (TWord 6) (TWord 6)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 3) (TWord 6) (TWord 3)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 3) (TWord 6) (TWord 6)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 3)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(bool)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 0) (TWord 0) (TWord 6) (TWord 0)) (Pair a (Var b))).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 0) (TWord 0) (TWord 6) (TWord 6)) (Pair a (Var b))).
+Notation "'(bool)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 0) (TWord 6) (TWord 6) (TWord 0)) (Pair a (Var b))).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 0) (TWord 6) (TWord 6) (TWord 6)) (Pair a (Var b))).
+Notation "'(bool)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 0) (TWord 6) (TWord 0)) (Pair a (Var b))).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 0) (TWord 6) (TWord 6)) (Pair a (Var b))).
+Notation "'(bool)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 0)) (Pair a (Var b))).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair a (Var b))).
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 0) (TWord 0) (TWord 6) (TWord 0)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 0) (TWord 0) (TWord 6) (TWord 6)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 0) (TWord 6) (TWord 6) (TWord 0)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 0) (TWord 6) (TWord 6) (TWord 6)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 0) (TWord 6) (TWord 0)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 0) (TWord 6) (TWord 6)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 0)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(uint8_t)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 3) (TWord 3) (TWord 6) (TWord 3)) (Pair a (Var b))).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 3) (TWord 3) (TWord 6) (TWord 6)) (Pair a (Var b))).
+Notation "'(uint8_t)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 3) (TWord 6) (TWord 6) (TWord 3)) (Pair a (Var b))).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 3) (TWord 6) (TWord 6) (TWord 6)) (Pair a (Var b))).
+Notation "'(uint8_t)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 3) (TWord 6) (TWord 3)) (Pair a (Var b))).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 3) (TWord 6) (TWord 6)) (Pair a (Var b))).
+Notation "'(uint8_t)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 3)) (Pair a (Var b))).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair a (Var b))).
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 3) (TWord 3) (TWord 6) (TWord 3)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 3) (TWord 3) (TWord 6) (TWord 6)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 3) (TWord 6) (TWord 6) (TWord 3)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 3) (TWord 6) (TWord 6) (TWord 6)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 3) (TWord 6) (TWord 3)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 3) (TWord 6) (TWord 6)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 3)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(bool)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 0) (TWord 0) (TWord 6) (TWord 0)) (Pair (Var a) b)).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 0) (TWord 0) (TWord 6) (TWord 6)) (Pair (Var a) b)).
+Notation "'(bool)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 0) (TWord 6) (TWord 6) (TWord 0)) (Pair (Var a) b)).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 0) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) b)).
+Notation "'(bool)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 0) (TWord 6) (TWord 0)) (Pair (Var a) b)).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 0) (TWord 6) (TWord 6)) (Pair (Var a) b)).
+Notation "'(bool)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 0)) (Pair (Var a) b)).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) b)).
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 0) (TWord 0) (TWord 6) (TWord 0)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 0) (TWord 0) (TWord 6) (TWord 6)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 0) (TWord 6) (TWord 6) (TWord 0)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 0) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 0) (TWord 6) (TWord 0)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 0) (TWord 6) (TWord 6)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 0)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(uint8_t)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 3) (TWord 3) (TWord 6) (TWord 3)) (Pair (Var a) b)).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 3) (TWord 3) (TWord 6) (TWord 6)) (Pair (Var a) b)).
+Notation "'(uint8_t)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 3) (TWord 6) (TWord 6) (TWord 3)) (Pair (Var a) b)).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 3) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) b)).
+Notation "'(uint8_t)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 3) (TWord 6) (TWord 3)) (Pair (Var a) b)).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 3) (TWord 6) (TWord 6)) (Pair (Var a) b)).
+Notation "'(uint8_t)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 3)) (Pair (Var a) b)).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) b)).
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 3) (TWord 3) (TWord 6) (TWord 3)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 3) (TWord 3) (TWord 6) (TWord 6)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 3) (TWord 6) (TWord 6) (TWord 3)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 3) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 3) (TWord 6) (TWord 3)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 3) (TWord 6) (TWord 6)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 3)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(bool)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 0) (TWord 0) (TWord 6) (TWord 0)) (Pair (Var a) (Var b))).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 0) (TWord 0) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))).
+Notation "'(bool)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 0) (TWord 6) (TWord 6) (TWord 0)) (Pair (Var a) (Var b))).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 0) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))).
+Notation "'(bool)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 0) (TWord 6) (TWord 0)) (Pair (Var a) (Var b))).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 0) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))).
+Notation "'(bool)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 0)) (Pair (Var a) (Var b))).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))).
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 0) (TWord 0) (TWord 6) (TWord 0)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 0) (TWord 0) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 0) (TWord 6) (TWord 6) (TWord 0)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 0) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 0) (TWord 6) (TWord 0)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 0) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 0)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(uint8_t)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 3) (TWord 3) (TWord 6) (TWord 3)) (Pair (Var a) (Var b))).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 3) (TWord 3) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))).
+Notation "'(uint8_t)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 3) (TWord 6) (TWord 6) (TWord 3)) (Pair (Var a) (Var b))).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 3) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))).
+Notation "'(uint8_t)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 3) (TWord 6) (TWord 3)) (Pair (Var a) (Var b))).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 3) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))).
+Notation "'(uint8_t)' 'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 3)) (Pair (Var a) (Var b))).
+Notation "'mulx_u64' ( a , b )" := (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))).
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 3) (TWord 3) (TWord 6) (TWord 3)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 3) (TWord 3) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 3) (TWord 6) (TWord 6) (TWord 3)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 3) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 3) (TWord 6) (TWord 3)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 3) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 3)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u64' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 64 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(bool)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 0) (TWord 0) (TWord 7) (TWord 0)) (Pair a b)).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 0) (TWord 0) (TWord 7) (TWord 7)) (Pair a b)).
+Notation "'(bool)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 0) (TWord 7) (TWord 7) (TWord 0)) (Pair a b)).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 0) (TWord 7) (TWord 7) (TWord 7)) (Pair a b)).
+Notation "'(bool)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 0) (TWord 7) (TWord 0)) (Pair a b)).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 0) (TWord 7) (TWord 7)) (Pair a b)).
+Notation "'(bool)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 0)) (Pair a b)).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 7)) (Pair a b)).
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 0) (TWord 0) (TWord 7) (TWord 0)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 0) (TWord 0) (TWord 7) (TWord 7)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 0) (TWord 7) (TWord 7) (TWord 0)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 0) (TWord 7) (TWord 7) (TWord 7)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 0) (TWord 7) (TWord 0)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 0) (TWord 7) (TWord 7)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 0)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 7)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(uint8_t)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 3) (TWord 3) (TWord 7) (TWord 3)) (Pair a b)).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 3) (TWord 3) (TWord 7) (TWord 7)) (Pair a b)).
+Notation "'(uint8_t)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 3) (TWord 7) (TWord 7) (TWord 3)) (Pair a b)).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 3) (TWord 7) (TWord 7) (TWord 7)) (Pair a b)).
+Notation "'(uint8_t)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 3) (TWord 7) (TWord 3)) (Pair a b)).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 3) (TWord 7) (TWord 7)) (Pair a b)).
+Notation "'(uint8_t)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 3)) (Pair a b)).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 7)) (Pair a b)).
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 3) (TWord 3) (TWord 7) (TWord 3)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 3) (TWord 3) (TWord 7) (TWord 7)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 3) (TWord 7) (TWord 7) (TWord 3)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 3) (TWord 7) (TWord 7) (TWord 7)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 3) (TWord 7) (TWord 3)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 3) (TWord 7) (TWord 7)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 3)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 7)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(bool)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 0) (TWord 0) (TWord 7) (TWord 0)) (Pair a (Var b))).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 0) (TWord 0) (TWord 7) (TWord 7)) (Pair a (Var b))).
+Notation "'(bool)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 0) (TWord 7) (TWord 7) (TWord 0)) (Pair a (Var b))).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 0) (TWord 7) (TWord 7) (TWord 7)) (Pair a (Var b))).
+Notation "'(bool)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 0) (TWord 7) (TWord 0)) (Pair a (Var b))).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 0) (TWord 7) (TWord 7)) (Pair a (Var b))).
+Notation "'(bool)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 0)) (Pair a (Var b))).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 7)) (Pair a (Var b))).
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 0) (TWord 0) (TWord 7) (TWord 0)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 0) (TWord 0) (TWord 7) (TWord 7)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 0) (TWord 7) (TWord 7) (TWord 0)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 0) (TWord 7) (TWord 7) (TWord 7)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 0) (TWord 7) (TWord 0)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 0) (TWord 7) (TWord 7)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 0)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 7)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(uint8_t)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 3) (TWord 3) (TWord 7) (TWord 3)) (Pair a (Var b))).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 3) (TWord 3) (TWord 7) (TWord 7)) (Pair a (Var b))).
+Notation "'(uint8_t)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 3) (TWord 7) (TWord 7) (TWord 3)) (Pair a (Var b))).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 3) (TWord 7) (TWord 7) (TWord 7)) (Pair a (Var b))).
+Notation "'(uint8_t)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 3) (TWord 7) (TWord 3)) (Pair a (Var b))).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 3) (TWord 7) (TWord 7)) (Pair a (Var b))).
+Notation "'(uint8_t)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 3)) (Pair a (Var b))).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 7)) (Pair a (Var b))).
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 3) (TWord 3) (TWord 7) (TWord 3)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 3) (TWord 3) (TWord 7) (TWord 7)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 3) (TWord 7) (TWord 7) (TWord 3)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 3) (TWord 7) (TWord 7) (TWord 7)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 3) (TWord 7) (TWord 3)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 3) (TWord 7) (TWord 7)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 3)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 7)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(bool)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 0) (TWord 0) (TWord 7) (TWord 0)) (Pair (Var a) b)).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 0) (TWord 0) (TWord 7) (TWord 7)) (Pair (Var a) b)).
+Notation "'(bool)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 0) (TWord 7) (TWord 7) (TWord 0)) (Pair (Var a) b)).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 0) (TWord 7) (TWord 7) (TWord 7)) (Pair (Var a) b)).
+Notation "'(bool)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 0) (TWord 7) (TWord 0)) (Pair (Var a) b)).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 0) (TWord 7) (TWord 7)) (Pair (Var a) b)).
+Notation "'(bool)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 0)) (Pair (Var a) b)).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 7)) (Pair (Var a) b)).
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 0) (TWord 0) (TWord 7) (TWord 0)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 0) (TWord 0) (TWord 7) (TWord 7)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 0) (TWord 7) (TWord 7) (TWord 0)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 0) (TWord 7) (TWord 7) (TWord 7)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 0) (TWord 7) (TWord 0)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 0) (TWord 7) (TWord 7)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 0)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 7)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(uint8_t)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 3) (TWord 3) (TWord 7) (TWord 3)) (Pair (Var a) b)).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 3) (TWord 3) (TWord 7) (TWord 7)) (Pair (Var a) b)).
+Notation "'(uint8_t)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 3) (TWord 7) (TWord 7) (TWord 3)) (Pair (Var a) b)).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 3) (TWord 7) (TWord 7) (TWord 7)) (Pair (Var a) b)).
+Notation "'(uint8_t)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 3) (TWord 7) (TWord 3)) (Pair (Var a) b)).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 3) (TWord 7) (TWord 7)) (Pair (Var a) b)).
+Notation "'(uint8_t)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 3)) (Pair (Var a) b)).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 7)) (Pair (Var a) b)).
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 3) (TWord 3) (TWord 7) (TWord 3)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 3) (TWord 3) (TWord 7) (TWord 7)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 3) (TWord 7) (TWord 7) (TWord 3)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 3) (TWord 7) (TWord 7) (TWord 7)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 3) (TWord 7) (TWord 3)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 3) (TWord 7) (TWord 7)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 3)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 7)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(bool)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 0) (TWord 0) (TWord 7) (TWord 0)) (Pair (Var a) (Var b))).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 0) (TWord 0) (TWord 7) (TWord 7)) (Pair (Var a) (Var b))).
+Notation "'(bool)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 0) (TWord 7) (TWord 7) (TWord 0)) (Pair (Var a) (Var b))).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 0) (TWord 7) (TWord 7) (TWord 7)) (Pair (Var a) (Var b))).
+Notation "'(bool)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 0) (TWord 7) (TWord 0)) (Pair (Var a) (Var b))).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 0) (TWord 7) (TWord 7)) (Pair (Var a) (Var b))).
+Notation "'(bool)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 0)) (Pair (Var a) (Var b))).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 7)) (Pair (Var a) (Var b))).
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 0) (TWord 0) (TWord 7) (TWord 0)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 0) (TWord 0) (TWord 7) (TWord 7)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 0) (TWord 7) (TWord 7) (TWord 0)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 0) (TWord 7) (TWord 7) (TWord 7)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 0) (TWord 7) (TWord 0)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 0) (TWord 7) (TWord 7)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 0)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 7)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(uint8_t)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 3) (TWord 3) (TWord 7) (TWord 3)) (Pair (Var a) (Var b))).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 3) (TWord 3) (TWord 7) (TWord 7)) (Pair (Var a) (Var b))).
+Notation "'(uint8_t)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 3) (TWord 7) (TWord 7) (TWord 3)) (Pair (Var a) (Var b))).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 3) (TWord 7) (TWord 7) (TWord 7)) (Pair (Var a) (Var b))).
+Notation "'(uint8_t)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 3) (TWord 7) (TWord 3)) (Pair (Var a) (Var b))).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 3) (TWord 7) (TWord 7)) (Pair (Var a) (Var b))).
+Notation "'(uint8_t)' 'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 3)) (Pair (Var a) (Var b))).
+Notation "'mulx_u128' ( a , b )" := (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 7)) (Pair (Var a) (Var b))).
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 3) (TWord 3) (TWord 7) (TWord 3)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 3) (TWord 3) (TWord 7) (TWord 7)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 3) (TWord 7) (TWord 7) (TWord 3)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 3) (TWord 7) (TWord 7) (TWord 7)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 3) (TWord 7) (TWord 3)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 3) (TWord 7) (TWord 7)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 3)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u128' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 128 (TWord 7) (TWord 7) (TWord 7) (TWord 7)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(bool)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 0) (TWord 0) (TWord 6) (TWord 0)) (Pair a b)).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 0) (TWord 0) (TWord 6) (TWord 6)) (Pair a b)).
+Notation "'(bool)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 0) (TWord 6) (TWord 6) (TWord 0)) (Pair a b)).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 0) (TWord 6) (TWord 6) (TWord 6)) (Pair a b)).
+Notation "'(bool)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 0) (TWord 6) (TWord 0)) (Pair a b)).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 0) (TWord 6) (TWord 6)) (Pair a b)).
+Notation "'(bool)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 0)) (Pair a b)).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair a b)).
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 0) (TWord 0) (TWord 6) (TWord 0)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 0) (TWord 0) (TWord 6) (TWord 6)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 0) (TWord 6) (TWord 6) (TWord 0)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 0) (TWord 6) (TWord 6) (TWord 6)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 0) (TWord 6) (TWord 0)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 0) (TWord 6) (TWord 6)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 0)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(uint8_t)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 3) (TWord 3) (TWord 6) (TWord 3)) (Pair a b)).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 3) (TWord 3) (TWord 6) (TWord 6)) (Pair a b)).
+Notation "'(uint8_t)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 3) (TWord 6) (TWord 6) (TWord 3)) (Pair a b)).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 3) (TWord 6) (TWord 6) (TWord 6)) (Pair a b)).
+Notation "'(uint8_t)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 3) (TWord 6) (TWord 3)) (Pair a b)).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 3) (TWord 6) (TWord 6)) (Pair a b)).
+Notation "'(uint8_t)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 3)) (Pair a b)).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair a b)).
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 3) (TWord 3) (TWord 6) (TWord 3)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 3) (TWord 3) (TWord 6) (TWord 6)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 3) (TWord 6) (TWord 6) (TWord 3)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 3) (TWord 6) (TWord 6) (TWord 6)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 3) (TWord 6) (TWord 3)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 3) (TWord 6) (TWord 6)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 3)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(bool)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 0) (TWord 0) (TWord 6) (TWord 0)) (Pair a (Var b))).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 0) (TWord 0) (TWord 6) (TWord 6)) (Pair a (Var b))).
+Notation "'(bool)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 0) (TWord 6) (TWord 6) (TWord 0)) (Pair a (Var b))).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 0) (TWord 6) (TWord 6) (TWord 6)) (Pair a (Var b))).
+Notation "'(bool)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 0) (TWord 6) (TWord 0)) (Pair a (Var b))).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 0) (TWord 6) (TWord 6)) (Pair a (Var b))).
+Notation "'(bool)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 0)) (Pair a (Var b))).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair a (Var b))).
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 0) (TWord 0) (TWord 6) (TWord 0)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 0) (TWord 0) (TWord 6) (TWord 6)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 0) (TWord 6) (TWord 6) (TWord 0)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 0) (TWord 6) (TWord 6) (TWord 6)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 0) (TWord 6) (TWord 0)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 0) (TWord 6) (TWord 6)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 0)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(uint8_t)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 3) (TWord 3) (TWord 6) (TWord 3)) (Pair a (Var b))).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 3) (TWord 3) (TWord 6) (TWord 6)) (Pair a (Var b))).
+Notation "'(uint8_t)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 3) (TWord 6) (TWord 6) (TWord 3)) (Pair a (Var b))).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 3) (TWord 6) (TWord 6) (TWord 6)) (Pair a (Var b))).
+Notation "'(uint8_t)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 3) (TWord 6) (TWord 3)) (Pair a (Var b))).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 3) (TWord 6) (TWord 6)) (Pair a (Var b))).
+Notation "'(uint8_t)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 3)) (Pair a (Var b))).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair a (Var b))).
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 3) (TWord 3) (TWord 6) (TWord 3)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 3) (TWord 3) (TWord 6) (TWord 6)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 3) (TWord 6) (TWord 6) (TWord 3)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 3) (TWord 6) (TWord 6) (TWord 6)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 3) (TWord 6) (TWord 3)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 3) (TWord 6) (TWord 6)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 3)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair a (Var b))) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(bool)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 0) (TWord 0) (TWord 6) (TWord 0)) (Pair (Var a) b)).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 0) (TWord 0) (TWord 6) (TWord 6)) (Pair (Var a) b)).
+Notation "'(bool)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 0) (TWord 6) (TWord 6) (TWord 0)) (Pair (Var a) b)).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 0) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) b)).
+Notation "'(bool)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 0) (TWord 6) (TWord 0)) (Pair (Var a) b)).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 0) (TWord 6) (TWord 6)) (Pair (Var a) b)).
+Notation "'(bool)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 0)) (Pair (Var a) b)).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) b)).
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 0) (TWord 0) (TWord 6) (TWord 0)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 0) (TWord 0) (TWord 6) (TWord 6)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 0) (TWord 6) (TWord 6) (TWord 0)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 0) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 0) (TWord 6) (TWord 0)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 0) (TWord 6) (TWord 6)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 0)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(uint8_t)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 3) (TWord 3) (TWord 6) (TWord 3)) (Pair (Var a) b)).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 3) (TWord 3) (TWord 6) (TWord 6)) (Pair (Var a) b)).
+Notation "'(uint8_t)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 3) (TWord 6) (TWord 6) (TWord 3)) (Pair (Var a) b)).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 3) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) b)).
+Notation "'(uint8_t)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 3) (TWord 6) (TWord 3)) (Pair (Var a) b)).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 3) (TWord 6) (TWord 6)) (Pair (Var a) b)).
+Notation "'(uint8_t)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 3)) (Pair (Var a) b)).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) b)).
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 3) (TWord 3) (TWord 6) (TWord 3)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 3) (TWord 3) (TWord 6) (TWord 6)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 3) (TWord 6) (TWord 6) (TWord 3)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 3) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 3) (TWord 6) (TWord 3)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 3) (TWord 6) (TWord 6)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 3)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) b)) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(bool)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 0) (TWord 0) (TWord 6) (TWord 0)) (Pair (Var a) (Var b))).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 0) (TWord 0) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))).
+Notation "'(bool)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 0) (TWord 6) (TWord 6) (TWord 0)) (Pair (Var a) (Var b))).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 0) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))).
+Notation "'(bool)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 0) (TWord 6) (TWord 0)) (Pair (Var a) (Var b))).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 0) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))).
+Notation "'(bool)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 0)) (Pair (Var a) (Var b))).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))).
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 0) (TWord 0) (TWord 6) (TWord 0)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 0) (TWord 0) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 0) (TWord 6) (TWord 6) (TWord 0)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 0) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 0) (TWord 6) (TWord 0)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 0) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(bool)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 0)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+Notation "'(uint8_t)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 3) (TWord 3) (TWord 6) (TWord 3)) (Pair (Var a) (Var b))).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 3) (TWord 3) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))).
+Notation "'(uint8_t)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 3) (TWord 6) (TWord 6) (TWord 3)) (Pair (Var a) (Var b))).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 3) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))).
+Notation "'(uint8_t)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 3) (TWord 6) (TWord 3)) (Pair (Var a) (Var b))).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 3) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))).
+Notation "'(uint8_t)' 'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 3)) (Pair (Var a) (Var b))).
+Notation "'mulx_u51' ( a , b )" := (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))).
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 3) (TWord 3) (TWord 6) (TWord 3)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 3) (TWord 3) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 3) (TWord 6) (TWord 6) (TWord 3)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 3) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 3) (TWord 6) (TWord 3)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 3) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '(uint8_t)' '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 3)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
+(*Notation "T0 out ; T1 c_out = '_mulx_u51' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 51 (TWord 6) (TWord 6) (TWord 6) (TWord 6)) (Pair (Var a) (Var b))) (fun '((out, c_out)%core) => REST)).*)
 Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 5)) (Pair a b)).
 (*Notation "T0 out ; T1 c_out = '_mulx_u32' ( a , b , & out ) ; REST" := (LetIn (tx:=Prod T0 T1) (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 5)) (Pair a b)) (fun '((out, c_out)%core) => REST)).*)
 Notation "'mulx_u32' ( a , b )" := (Op (MulSplit 32 (TWord 5) (TWord 5) (TWord 5) (TWord 5)) (Pair a (Var b))).