diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-03-30 16:36:50 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-03-30 16:36:50 -0400 |
| commit | 16d3eb50638fc280b790aff9cdaa6d28cbb42c8a (patch) | |
| tree | db36b1af22b6f72287f0a1beae5cad9c665681b9 /src/Reflection/Z | |
| parent | 0ddbe1be29582a0c6495100f6b6d9ec3d74820ef (diff) | |
Update CNotations, JavaNotations
Diffstat (limited to 'src/Reflection/Z')
| -rw-r--r-- | src/Reflection/Z/CNotations.v | 894 | ||||
| -rw-r--r-- | src/Reflection/Z/JavaNotations.v | 869 |
2 files changed, 1513 insertions, 250 deletions
diff --git a/src/Reflection/Z/CNotations.v b/src/Reflection/Z/CNotations.v index 0b3bfa161..74b945222 100644 --- a/src/Reflection/Z/CNotations.v +++ b/src/Reflection/Z/CNotations.v @@ -4,152 +4,768 @@ Require Export Crypto.Reflection.Z.HexNotationConstants. Require Export Crypto.Util.Notations. Reserved Notation "T x = A ; b" (at level 200, b at level 200, format "T x = A ; '//' b"). -Reserved Notation "'(bool)' x" (at level 200, x at level 9). -Reserved Notation "'(uint8_t)' x" (at level 200, x at level 9). -Reserved Notation "'(uint16_t)' x" (at level 200, x at level 9). -Reserved Notation "'(uint32_t)' x" (at level 200, x at level 9). -Reserved Notation "'(uint64_t)' x" (at level 200, x at level 9). -Reserved Notation "'(uint128_t)' x" (at level 200, x at level 9). Reserved Notation "x & y" (at level 40). Global Open Scope expr_scope. Notation "T x = A ; b" := (LetIn (tx:=T) A (fun x => b)) : expr_scope. -(*Notation uint32_t := (_ (TWord 5)). -Notation uint64_t := (_ (TWord 6)). -Notation uint128_t := (_ (TWord 7)).*) -Notation bool := (Tbase (TWord 0)). -Notation "'uint8_t'" := (Tbase (TWord 1)). -Notation "'uint8_t'" := (Tbase (TWord 2)). -Notation "'uint8_t'" := (Tbase (TWord 3)). -Notation uint16_t := (Tbase (TWord 4)). -Notation uint32_t := (Tbase (TWord 5)). -Notation uint64_t := (Tbase (TWord 6)). -Notation uint128_t := (Tbase (TWord 7)). -Notation "'(bool)' x" := (Op (Cast _ (TWord 0)) x). -Notation "'(uint8_t)' x" := (Op (Cast _ (TWord 1)) x). -Notation "'(uint8_t)' x" := (Op (Cast _ (TWord 2)) x). -Notation "'(uint8_t)' x" := (Op (Cast _ (TWord 3)) x). -Notation "'(uint16_t)' x" := (Op (Cast _ (TWord 4)) x). -Notation "'(uint32_t)' x" := (Op (Cast _ (TWord 5)) x). -Notation "'(uint64_t)' x" := (Op (Cast _ (TWord 6)) x). -Notation "'(uint128_t)' x" := (Op (Cast _ (TWord 7)) x). -Notation "'(bool)' x" := (Op (Cast _ (TWord 0)) (Var x)). -Notation "'(uint8_t)' x" := (Op (Cast _ (TWord 1)) (Var x)). -Notation "'(uint8_t)' x" := (Op (Cast _ (TWord 2)) (Var x)). -Notation "'(uint8_t)' x" := (Op (Cast _ (TWord 3)) (Var x)). -Notation "'(uint16_t)' x" := (Op (Cast _ (TWord 4)) (Var x)). -Notation "'(uint32_t)' x" := (Op (Cast _ (TWord 5)) (Var x)). -Notation "'(uint64_t)' x" := (Op (Cast _ (TWord 6)) (Var x)). -Notation "'(uint128_t)' x" := (Op (Cast _ (TWord 7)) (Var x)). -Notation "x + y" := (Op (Add _) (Pair x y)). -Notation "x + y" := (Op (Add _) (Pair (Var x) y)). -Notation "x + y" := (Op (Add _) (Pair x (Var y))). -Notation "x + y" := (Op (Add _) (Pair (Var x) (Var y))). -Notation "x - y" := (Op (Sub _) (Pair x y)). -Notation "x - y" := (Op (Sub _) (Pair (Var x) y)). -Notation "x - y" := (Op (Sub _) (Pair x (Var y))). -Notation "x - y" := (Op (Sub _) (Pair (Var x) (Var y))). -Notation "x * y" := (Op (Mul _) (Pair x y)). -Notation "x * y" := (Op (Mul _) (Pair (Var x) y)). -Notation "x * y" := (Op (Mul _) (Pair x (Var y))). -Notation "x * y" := (Op (Mul _) (Pair (Var x) (Var y))). (* python: << -for opn, op in (('*', 'Mul'), ('+', 'Add'), ('&', 'Land')): - for lgwordsz in (5, 6, 7): - for side in ('l', 'r'): - for v1 in (False, True): - for v2 in (False, True): - lhs = ('x' if not v1 else '(Var x)') - lhs = (lhs if side != 'l' else '(Op (Cast _ (TWord %d)) %s)' % (lgwordsz, lhs)) - rhs = ('y' if not v2 else '(Var y)') - rhs = (rhs if side != 'r' else '(Op (Cast _ (TWord %d)) %s)' % (lgwordsz, rhs)) - print('Notation "x %s y" := (Op (%s (TWord %d)) (Pair %s %s)).' % (opn, op, lgwordsz, lhs, rhs)) +types = ('bool', 'uint8_t', 'uint8_t', 'uint8_t', 'uint16_t', 'uint32_t', 'uint64_t', 'uint128_t') +for lgwordsz in range(0, len(types)): + print('Notation "\'%s\'" := (Tbase (TWord %d)).' % (types[lgwordsz], lgwordsz)) +print('') +cast_pat = "'(%s)' %s" +for opn, op, lvl in (('*', 'Mul', 40), ('+', 'Add', 50), ('-', 'Sub', 50), ('&', 'Land', 40), ('<<', 'Shl', 30)): + for v1 in (False, True): + for v2 in (False, True): + lhs = ('x' if not v1 else '(Var x)') + rhs = ('y' if not v2 else '(Var y)') + print('Notation "x %s y" := (Op (%s _ _ _) (Pair %s %s)).' % (opn, op, lhs, rhs)) + for lgwordsz in range(0, len(types)): + for v1 in (False, True): + for v2 in (False, True): + lhs = ('x' if not v1 else '(Var x)') + rhs = ('y' if not v2 else '(Var y)') + print('Notation "%s %s %s" := (Op (%s (TWord _) (TWord _) (TWord %d)) (Pair %s %s)) (at level %d).' + % (cast_pat % (types[lgwordsz], 'x'), opn, cast_pat % (types[lgwordsz], 'y'), + op, lgwordsz, lhs, rhs, lvl)) + for v1 in (False, True): + for v2 in (False, True): + lhs = ('x' if not v1 else '(Var x)') + rhs = ('y' if not v2 else '(Var y)') + print('Notation "%s %s %s" := (Op (%s (TWord %d) (TWord _) (TWord %d)) (Pair %s %s)) (at level %d).' + % ('x', opn, cast_pat % (types[lgwordsz], 'y'), + op, lgwordsz, lgwordsz, lhs, rhs, lvl)) + print('Notation "%s %s %s" := (Op (%s (TWord _) (TWord %d) (TWord %d)) (Pair %s %s)) (at level %d).' + % (cast_pat % (types[lgwordsz], 'x'), opn, 'y', + op, lgwordsz, lgwordsz, lhs, rhs, lvl)) + for v1 in (False, True): + for v2 in (False, True): + lhs = ('x' if not v1 else '(Var x)') + rhs = ('y' if not v2 else '(Var y)') + print('Notation "x %s y" := (Op (%s (TWord %d) (TWord %d) (TWord %d)) (Pair %s %s)).' + % (opn, op, lgwordsz, lgwordsz, lgwordsz, lhs, rhs)) +for opn, op, lvl in (('>>', 'Shr', 30),): + for v1 in (False, True): + for v2 in (False, True): + lhs = ('x' if not v1 else '(Var x)') + rhs = ('y' if not v2 else '(Var y)') + print('Notation "x %s y" := (Op (%s _ _ _) (Pair %s %s)).' % (opn, op, lhs, rhs)) + for lgwordsz in range(0, len(types)): + for v1 in (False, True): + for v2 in (False, True): + lhs = ('x' if not v1 else '(Var x)') + rhs = ('y' if not v2 else '(Var y)') + print('Notation "\'(%s)\' ( x %s y )" := (Op (%s (TWord _) (TWord _) (TWord %d)) (Pair %s %s)) (at level %d).' + % (types[lgwordsz], opn, op, lgwordsz, lhs, rhs, lvl)) +print('Notation Return x := (Var x).') +print('Notation C_like := (Expr base_type op _).') >> *) -Notation "x * y" := (Op (Mul (TWord 5)) (Pair (Op (Cast _ (TWord 5)) x) y)). -Notation "x * y" := (Op (Mul (TWord 5)) (Pair (Op (Cast _ (TWord 5)) x) (Var y))). -Notation "x * y" := (Op (Mul (TWord 5)) (Pair (Op (Cast _ (TWord 5)) (Var x)) y)). -Notation "x * y" := (Op (Mul (TWord 5)) (Pair (Op (Cast _ (TWord 5)) (Var x)) (Var y))). -Notation "x * y" := (Op (Mul (TWord 5)) (Pair x (Op (Cast _ (TWord 5)) y))). -Notation "x * y" := (Op (Mul (TWord 5)) (Pair x (Op (Cast _ (TWord 5)) (Var y)))). -Notation "x * y" := (Op (Mul (TWord 5)) (Pair (Var x) (Op (Cast _ (TWord 5)) y))). -Notation "x * y" := (Op (Mul (TWord 5)) (Pair (Var x) (Op (Cast _ (TWord 5)) (Var y)))). -Notation "x * y" := (Op (Mul (TWord 6)) (Pair (Op (Cast _ (TWord 6)) x) y)). -Notation "x * y" := (Op (Mul (TWord 6)) (Pair (Op (Cast _ (TWord 6)) x) (Var y))). -Notation "x * y" := (Op (Mul (TWord 6)) (Pair (Op (Cast _ (TWord 6)) (Var x)) y)). -Notation "x * y" := (Op (Mul (TWord 6)) (Pair (Op (Cast _ (TWord 6)) (Var x)) (Var y))). -Notation "x * y" := (Op (Mul (TWord 6)) (Pair x (Op (Cast _ (TWord 6)) y))). -Notation "x * y" := (Op (Mul (TWord 6)) (Pair x (Op (Cast _ (TWord 6)) (Var y)))). -Notation "x * y" := (Op (Mul (TWord 6)) (Pair (Var x) (Op (Cast _ (TWord 6)) y))). -Notation "x * y" := (Op (Mul (TWord 6)) (Pair (Var x) (Op (Cast _ (TWord 6)) (Var y)))). -Notation "x * y" := (Op (Mul (TWord 7)) (Pair (Op (Cast _ (TWord 7)) x) y)). -Notation "x * y" := (Op (Mul (TWord 7)) (Pair (Op (Cast _ (TWord 7)) x) (Var y))). -Notation "x * y" := (Op (Mul (TWord 7)) (Pair (Op (Cast _ (TWord 7)) (Var x)) y)). -Notation "x * y" := (Op (Mul (TWord 7)) (Pair (Op (Cast _ (TWord 7)) (Var x)) (Var y))). -Notation "x * y" := (Op (Mul (TWord 7)) (Pair x (Op (Cast _ (TWord 7)) y))). -Notation "x * y" := (Op (Mul (TWord 7)) (Pair x (Op (Cast _ (TWord 7)) (Var y)))). -Notation "x * y" := (Op (Mul (TWord 7)) (Pair (Var x) (Op (Cast _ (TWord 7)) y))). -Notation "x * y" := (Op (Mul (TWord 7)) (Pair (Var x) (Op (Cast _ (TWord 7)) (Var y)))). -Notation "x + y" := (Op (Add (TWord 5)) (Pair (Op (Cast _ (TWord 5)) x) y)). -Notation "x + y" := (Op (Add (TWord 5)) (Pair (Op (Cast _ (TWord 5)) x) (Var y))). -Notation "x + y" := (Op (Add (TWord 5)) (Pair (Op (Cast _ (TWord 5)) (Var x)) y)). -Notation "x + y" := (Op (Add (TWord 5)) (Pair (Op (Cast _ (TWord 5)) (Var x)) (Var y))). -Notation "x + y" := (Op (Add (TWord 5)) (Pair x (Op (Cast _ (TWord 5)) y))). -Notation "x + y" := (Op (Add (TWord 5)) (Pair x (Op (Cast _ (TWord 5)) (Var y)))). -Notation "x + y" := (Op (Add (TWord 5)) (Pair (Var x) (Op (Cast _ (TWord 5)) y))). -Notation "x + y" := (Op (Add (TWord 5)) (Pair (Var x) (Op (Cast _ (TWord 5)) (Var y)))). -Notation "x + y" := (Op (Add (TWord 6)) (Pair (Op (Cast _ (TWord 6)) x) y)). -Notation "x + y" := (Op (Add (TWord 6)) (Pair (Op (Cast _ (TWord 6)) x) (Var y))). -Notation "x + y" := (Op (Add (TWord 6)) (Pair (Op (Cast _ (TWord 6)) (Var x)) y)). -Notation "x + y" := (Op (Add (TWord 6)) (Pair (Op (Cast _ (TWord 6)) (Var x)) (Var y))). -Notation "x + y" := (Op (Add (TWord 6)) (Pair x (Op (Cast _ (TWord 6)) y))). -Notation "x + y" := (Op (Add (TWord 6)) (Pair x (Op (Cast _ (TWord 6)) (Var y)))). -Notation "x + y" := (Op (Add (TWord 6)) (Pair (Var x) (Op (Cast _ (TWord 6)) y))). -Notation "x + y" := (Op (Add (TWord 6)) (Pair (Var x) (Op (Cast _ (TWord 6)) (Var y)))). -Notation "x + y" := (Op (Add (TWord 7)) (Pair (Op (Cast _ (TWord 7)) x) y)). -Notation "x + y" := (Op (Add (TWord 7)) (Pair (Op (Cast _ (TWord 7)) x) (Var y))). -Notation "x + y" := (Op (Add (TWord 7)) (Pair (Op (Cast _ (TWord 7)) (Var x)) y)). -Notation "x + y" := (Op (Add (TWord 7)) (Pair (Op (Cast _ (TWord 7)) (Var x)) (Var y))). -Notation "x + y" := (Op (Add (TWord 7)) (Pair x (Op (Cast _ (TWord 7)) y))). -Notation "x + y" := (Op (Add (TWord 7)) (Pair x (Op (Cast _ (TWord 7)) (Var y)))). -Notation "x + y" := (Op (Add (TWord 7)) (Pair (Var x) (Op (Cast _ (TWord 7)) y))). -Notation "x + y" := (Op (Add (TWord 7)) (Pair (Var x) (Op (Cast _ (TWord 7)) (Var y)))). -Notation "x >> y" := (Op (Shr _) (Pair x y)). -Notation "x >> y" := (Op (Shr _) (Pair (Var x) y)). -Notation "x >> y" := (Op (Shr _) (Pair x (Var y))). -Notation "x >> y" := (Op (Shr _) (Pair (Var x) (Var y))). -Notation "x >> y" := (Op (Shr _) (Pair x (Op (Cast _ _) y))). -Notation "x >> y" := (Op (Shr _) (Pair (Var x) (Op (Cast _ _) y))). -Notation "x >> y" := (Op (Shr _) (Pair x (Op (Cast _ _) (Var y)))). -Notation "x >> y" := (Op (Shr _) (Pair (Var x) (Op (Cast _ _) (Var y)))). -Notation "x & y" := (Op (Land _) (Pair x y)). -Notation "x & y" := (Op (Land _) (Pair (Var x) y)). -Notation "x & y" := (Op (Land _) (Pair x (Var y))). -Notation "x & y" := (Op (Land _) (Pair (Var x) (Var y))). -Notation "x & y" := (Op (Land (TWord 5)) (Pair (Op (Cast _ (TWord 5)) x) y)). -Notation "x & y" := (Op (Land (TWord 5)) (Pair (Op (Cast _ (TWord 5)) x) (Var y))). -Notation "x & y" := (Op (Land (TWord 5)) (Pair (Op (Cast _ (TWord 5)) (Var x)) y)). -Notation "x & y" := (Op (Land (TWord 5)) (Pair (Op (Cast _ (TWord 5)) (Var x)) (Var y))). -Notation "x & y" := (Op (Land (TWord 5)) (Pair x (Op (Cast _ (TWord 5)) y))). -Notation "x & y" := (Op (Land (TWord 5)) (Pair x (Op (Cast _ (TWord 5)) (Var y)))). -Notation "x & y" := (Op (Land (TWord 5)) (Pair (Var x) (Op (Cast _ (TWord 5)) y))). -Notation "x & y" := (Op (Land (TWord 5)) (Pair (Var x) (Op (Cast _ (TWord 5)) (Var y)))). -Notation "x & y" := (Op (Land (TWord 6)) (Pair (Op (Cast _ (TWord 6)) x) y)). -Notation "x & y" := (Op (Land (TWord 6)) (Pair (Op (Cast _ (TWord 6)) x) (Var y))). -Notation "x & y" := (Op (Land (TWord 6)) (Pair (Op (Cast _ (TWord 6)) (Var x)) y)). -Notation "x & y" := (Op (Land (TWord 6)) (Pair (Op (Cast _ (TWord 6)) (Var x)) (Var y))). -Notation "x & y" := (Op (Land (TWord 6)) (Pair x (Op (Cast _ (TWord 6)) y))). -Notation "x & y" := (Op (Land (TWord 6)) (Pair x (Op (Cast _ (TWord 6)) (Var y)))). -Notation "x & y" := (Op (Land (TWord 6)) (Pair (Var x) (Op (Cast _ (TWord 6)) y))). -Notation "x & y" := (Op (Land (TWord 6)) (Pair (Var x) (Op (Cast _ (TWord 6)) (Var y)))). -Notation "x & y" := (Op (Land (TWord 7)) (Pair (Op (Cast _ (TWord 7)) x) y)). -Notation "x & y" := (Op (Land (TWord 7)) (Pair (Op (Cast _ (TWord 7)) x) (Var y))). -Notation "x & y" := (Op (Land (TWord 7)) (Pair (Op (Cast _ (TWord 7)) (Var x)) y)). -Notation "x & y" := (Op (Land (TWord 7)) (Pair (Op (Cast _ (TWord 7)) (Var x)) (Var y))). -Notation "x & y" := (Op (Land (TWord 7)) (Pair x (Op (Cast _ (TWord 7)) y))). -Notation "x & y" := (Op (Land (TWord 7)) (Pair x (Op (Cast _ (TWord 7)) (Var y)))). -Notation "x & y" := (Op (Land (TWord 7)) (Pair (Var x) (Op (Cast _ (TWord 7)) y))). -Notation "x & y" := (Op (Land (TWord 7)) (Pair (Var x) (Op (Cast _ (TWord 7)) (Var y)))). +Notation "'bool'" := (Tbase (TWord 0)). +Notation "'uint8_t'" := (Tbase (TWord 1)). +Notation "'uint8_t'" := (Tbase (TWord 2)). +Notation "'uint8_t'" := (Tbase (TWord 3)). +Notation "'uint16_t'" := (Tbase (TWord 4)). +Notation "'uint32_t'" := (Tbase (TWord 5)). +Notation "'uint64_t'" := (Tbase (TWord 6)). +Notation "'uint128_t'" := (Tbase (TWord 7)). + +Notation "x * y" := (Op (Mul _ _ _) (Pair x y)). +Notation "x * y" := (Op (Mul _ _ _) (Pair x (Var y))). +Notation "x * y" := (Op (Mul _ _ _) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul _ _ _) (Pair (Var x) (Var y))). +Notation "'(bool)' x * '(bool)' y" := (Op (Mul (TWord _) (TWord _) (TWord 0)) (Pair x y)) (at level 40). +Notation "'(bool)' x * '(bool)' y" := (Op (Mul (TWord _) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 40). +Notation "'(bool)' x * '(bool)' y" := (Op (Mul (TWord _) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 40). +Notation "'(bool)' x * '(bool)' y" := (Op (Mul (TWord _) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(bool)' y" := (Op (Mul (TWord 0) (TWord _) (TWord 0)) (Pair x y)) (at level 40). +Notation "'(bool)' x * y" := (Op (Mul (TWord _) (TWord 0) (TWord 0)) (Pair x y)) (at level 40). +Notation "x * '(bool)' y" := (Op (Mul (TWord 0) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 40). +Notation "'(bool)' x * y" := (Op (Mul (TWord _) (TWord 0) (TWord 0)) (Pair x (Var y))) (at level 40). +Notation "x * '(bool)' y" := (Op (Mul (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 40). +Notation "'(bool)' x * y" := (Op (Mul (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) y)) (at level 40). +Notation "x * '(bool)' y" := (Op (Mul (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(bool)' x * y" := (Op (Mul (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 0) (TWord 0) (TWord 0)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 0) (TWord 0) (TWord 0)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x * '(uint8_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 1)) (Pair x y)) (at level 40). +Notation "'(uint8_t)' x * '(uint8_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 40). +Notation "'(uint8_t)' x * '(uint8_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 40). +Notation "'(uint8_t)' x * '(uint8_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(uint8_t)' y" := (Op (Mul (TWord 1) (TWord _) (TWord 1)) (Pair x y)) (at level 40). +Notation "'(uint8_t)' x * y" := (Op (Mul (TWord _) (TWord 1) (TWord 1)) (Pair x y)) (at level 40). +Notation "x * '(uint8_t)' y" := (Op (Mul (TWord 1) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 40). +Notation "'(uint8_t)' x * y" := (Op (Mul (TWord _) (TWord 1) (TWord 1)) (Pair x (Var y))) (at level 40). +Notation "x * '(uint8_t)' y" := (Op (Mul (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 40). +Notation "'(uint8_t)' x * y" := (Op (Mul (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) y)) (at level 40). +Notation "x * '(uint8_t)' y" := (Op (Mul (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint8_t)' x * y" := (Op (Mul (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 1) (TWord 1) (TWord 1)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 1) (TWord 1) (TWord 1)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x * '(uint8_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 2)) (Pair x y)) (at level 40). +Notation "'(uint8_t)' x * '(uint8_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 40). +Notation "'(uint8_t)' x * '(uint8_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 40). +Notation "'(uint8_t)' x * '(uint8_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(uint8_t)' y" := (Op (Mul (TWord 2) (TWord _) (TWord 2)) (Pair x y)) (at level 40). +Notation "'(uint8_t)' x * y" := (Op (Mul (TWord _) (TWord 2) (TWord 2)) (Pair x y)) (at level 40). +Notation "x * '(uint8_t)' y" := (Op (Mul (TWord 2) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 40). +Notation "'(uint8_t)' x * y" := (Op (Mul (TWord _) (TWord 2) (TWord 2)) (Pair x (Var y))) (at level 40). +Notation "x * '(uint8_t)' y" := (Op (Mul (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 40). +Notation "'(uint8_t)' x * y" := (Op (Mul (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) y)) (at level 40). +Notation "x * '(uint8_t)' y" := (Op (Mul (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint8_t)' x * y" := (Op (Mul (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 2) (TWord 2) (TWord 2)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 2) (TWord 2) (TWord 2)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x * '(uint8_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 3)) (Pair x y)) (at level 40). +Notation "'(uint8_t)' x * '(uint8_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 40). +Notation "'(uint8_t)' x * '(uint8_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 40). +Notation "'(uint8_t)' x * '(uint8_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(uint8_t)' y" := (Op (Mul (TWord 3) (TWord _) (TWord 3)) (Pair x y)) (at level 40). +Notation "'(uint8_t)' x * y" := (Op (Mul (TWord _) (TWord 3) (TWord 3)) (Pair x y)) (at level 40). +Notation "x * '(uint8_t)' y" := (Op (Mul (TWord 3) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 40). +Notation "'(uint8_t)' x * y" := (Op (Mul (TWord _) (TWord 3) (TWord 3)) (Pair x (Var y))) (at level 40). +Notation "x * '(uint8_t)' y" := (Op (Mul (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 40). +Notation "'(uint8_t)' x * y" := (Op (Mul (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) y)) (at level 40). +Notation "x * '(uint8_t)' y" := (Op (Mul (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint8_t)' x * y" := (Op (Mul (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 3) (TWord 3) (TWord 3)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 3) (TWord 3) (TWord 3)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))). +Notation "'(uint16_t)' x * '(uint16_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 4)) (Pair x y)) (at level 40). +Notation "'(uint16_t)' x * '(uint16_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 40). +Notation "'(uint16_t)' x * '(uint16_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 40). +Notation "'(uint16_t)' x * '(uint16_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(uint16_t)' y" := (Op (Mul (TWord 4) (TWord _) (TWord 4)) (Pair x y)) (at level 40). +Notation "'(uint16_t)' x * y" := (Op (Mul (TWord _) (TWord 4) (TWord 4)) (Pair x y)) (at level 40). +Notation "x * '(uint16_t)' y" := (Op (Mul (TWord 4) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 40). +Notation "'(uint16_t)' x * y" := (Op (Mul (TWord _) (TWord 4) (TWord 4)) (Pair x (Var y))) (at level 40). +Notation "x * '(uint16_t)' y" := (Op (Mul (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 40). +Notation "'(uint16_t)' x * y" := (Op (Mul (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) y)) (at level 40). +Notation "x * '(uint16_t)' y" := (Op (Mul (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint16_t)' x * y" := (Op (Mul (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 4) (TWord 4) (TWord 4)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 4) (TWord 4) (TWord 4)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))). +Notation "'(uint32_t)' x * '(uint32_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 5)) (Pair x y)) (at level 40). +Notation "'(uint32_t)' x * '(uint32_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 40). +Notation "'(uint32_t)' x * '(uint32_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 40). +Notation "'(uint32_t)' x * '(uint32_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(uint32_t)' y" := (Op (Mul (TWord 5) (TWord _) (TWord 5)) (Pair x y)) (at level 40). +Notation "'(uint32_t)' x * y" := (Op (Mul (TWord _) (TWord 5) (TWord 5)) (Pair x y)) (at level 40). +Notation "x * '(uint32_t)' y" := (Op (Mul (TWord 5) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 40). +Notation "'(uint32_t)' x * y" := (Op (Mul (TWord _) (TWord 5) (TWord 5)) (Pair x (Var y))) (at level 40). +Notation "x * '(uint32_t)' y" := (Op (Mul (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 40). +Notation "'(uint32_t)' x * y" := (Op (Mul (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) y)) (at level 40). +Notation "x * '(uint32_t)' y" := (Op (Mul (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint32_t)' x * y" := (Op (Mul (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 5) (TWord 5) (TWord 5)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 5) (TWord 5) (TWord 5)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))). +Notation "'(uint64_t)' x * '(uint64_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 6)) (Pair x y)) (at level 40). +Notation "'(uint64_t)' x * '(uint64_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 40). +Notation "'(uint64_t)' x * '(uint64_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 40). +Notation "'(uint64_t)' x * '(uint64_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(uint64_t)' y" := (Op (Mul (TWord 6) (TWord _) (TWord 6)) (Pair x y)) (at level 40). +Notation "'(uint64_t)' x * y" := (Op (Mul (TWord _) (TWord 6) (TWord 6)) (Pair x y)) (at level 40). +Notation "x * '(uint64_t)' y" := (Op (Mul (TWord 6) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 40). +Notation "'(uint64_t)' x * y" := (Op (Mul (TWord _) (TWord 6) (TWord 6)) (Pair x (Var y))) (at level 40). +Notation "x * '(uint64_t)' y" := (Op (Mul (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 40). +Notation "'(uint64_t)' x * y" := (Op (Mul (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) y)) (at level 40). +Notation "x * '(uint64_t)' y" := (Op (Mul (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint64_t)' x * y" := (Op (Mul (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 6) (TWord 6) (TWord 6)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 6) (TWord 6) (TWord 6)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))). +Notation "'(uint128_t)' x * '(uint128_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 7)) (Pair x y)) (at level 40). +Notation "'(uint128_t)' x * '(uint128_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 40). +Notation "'(uint128_t)' x * '(uint128_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 40). +Notation "'(uint128_t)' x * '(uint128_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(uint128_t)' y" := (Op (Mul (TWord 7) (TWord _) (TWord 7)) (Pair x y)) (at level 40). +Notation "'(uint128_t)' x * y" := (Op (Mul (TWord _) (TWord 7) (TWord 7)) (Pair x y)) (at level 40). +Notation "x * '(uint128_t)' y" := (Op (Mul (TWord 7) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 40). +Notation "'(uint128_t)' x * y" := (Op (Mul (TWord _) (TWord 7) (TWord 7)) (Pair x (Var y))) (at level 40). +Notation "x * '(uint128_t)' y" := (Op (Mul (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 40). +Notation "'(uint128_t)' x * y" := (Op (Mul (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) y)) (at level 40). +Notation "x * '(uint128_t)' y" := (Op (Mul (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint128_t)' x * y" := (Op (Mul (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "x + y" := (Op (Add _ _ _) (Pair x y)). +Notation "x + y" := (Op (Add _ _ _) (Pair x (Var y))). +Notation "x + y" := (Op (Add _ _ _) (Pair (Var x) y)). +Notation "x + y" := (Op (Add _ _ _) (Pair (Var x) (Var y))). +Notation "'(bool)' x + '(bool)' y" := (Op (Add (TWord _) (TWord _) (TWord 0)) (Pair x y)) (at level 50). +Notation "'(bool)' x + '(bool)' y" := (Op (Add (TWord _) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 50). +Notation "'(bool)' x + '(bool)' y" := (Op (Add (TWord _) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 50). +Notation "'(bool)' x + '(bool)' y" := (Op (Add (TWord _) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(bool)' y" := (Op (Add (TWord 0) (TWord _) (TWord 0)) (Pair x y)) (at level 50). +Notation "'(bool)' x + y" := (Op (Add (TWord _) (TWord 0) (TWord 0)) (Pair x y)) (at level 50). +Notation "x + '(bool)' y" := (Op (Add (TWord 0) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 50). +Notation "'(bool)' x + y" := (Op (Add (TWord _) (TWord 0) (TWord 0)) (Pair x (Var y))) (at level 50). +Notation "x + '(bool)' y" := (Op (Add (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 50). +Notation "'(bool)' x + y" := (Op (Add (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) y)) (at level 50). +Notation "x + '(bool)' y" := (Op (Add (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(bool)' x + y" := (Op (Add (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 0) (TWord 0) (TWord 0)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 0) (TWord 0) (TWord 0)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x + '(uint8_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 1)) (Pair x y)) (at level 50). +Notation "'(uint8_t)' x + '(uint8_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 50). +Notation "'(uint8_t)' x + '(uint8_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 50). +Notation "'(uint8_t)' x + '(uint8_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(uint8_t)' y" := (Op (Add (TWord 1) (TWord _) (TWord 1)) (Pair x y)) (at level 50). +Notation "'(uint8_t)' x + y" := (Op (Add (TWord _) (TWord 1) (TWord 1)) (Pair x y)) (at level 50). +Notation "x + '(uint8_t)' y" := (Op (Add (TWord 1) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 50). +Notation "'(uint8_t)' x + y" := (Op (Add (TWord _) (TWord 1) (TWord 1)) (Pair x (Var y))) (at level 50). +Notation "x + '(uint8_t)' y" := (Op (Add (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 50). +Notation "'(uint8_t)' x + y" := (Op (Add (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) y)) (at level 50). +Notation "x + '(uint8_t)' y" := (Op (Add (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint8_t)' x + y" := (Op (Add (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 1) (TWord 1) (TWord 1)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 1) (TWord 1) (TWord 1)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x + '(uint8_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 2)) (Pair x y)) (at level 50). +Notation "'(uint8_t)' x + '(uint8_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 50). +Notation "'(uint8_t)' x + '(uint8_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 50). +Notation "'(uint8_t)' x + '(uint8_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(uint8_t)' y" := (Op (Add (TWord 2) (TWord _) (TWord 2)) (Pair x y)) (at level 50). +Notation "'(uint8_t)' x + y" := (Op (Add (TWord _) (TWord 2) (TWord 2)) (Pair x y)) (at level 50). +Notation "x + '(uint8_t)' y" := (Op (Add (TWord 2) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 50). +Notation "'(uint8_t)' x + y" := (Op (Add (TWord _) (TWord 2) (TWord 2)) (Pair x (Var y))) (at level 50). +Notation "x + '(uint8_t)' y" := (Op (Add (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 50). +Notation "'(uint8_t)' x + y" := (Op (Add (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) y)) (at level 50). +Notation "x + '(uint8_t)' y" := (Op (Add (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint8_t)' x + y" := (Op (Add (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 2) (TWord 2) (TWord 2)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 2) (TWord 2) (TWord 2)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x + '(uint8_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 3)) (Pair x y)) (at level 50). +Notation "'(uint8_t)' x + '(uint8_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 50). +Notation "'(uint8_t)' x + '(uint8_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 50). +Notation "'(uint8_t)' x + '(uint8_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(uint8_t)' y" := (Op (Add (TWord 3) (TWord _) (TWord 3)) (Pair x y)) (at level 50). +Notation "'(uint8_t)' x + y" := (Op (Add (TWord _) (TWord 3) (TWord 3)) (Pair x y)) (at level 50). +Notation "x + '(uint8_t)' y" := (Op (Add (TWord 3) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 50). +Notation "'(uint8_t)' x + y" := (Op (Add (TWord _) (TWord 3) (TWord 3)) (Pair x (Var y))) (at level 50). +Notation "x + '(uint8_t)' y" := (Op (Add (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 50). +Notation "'(uint8_t)' x + y" := (Op (Add (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) y)) (at level 50). +Notation "x + '(uint8_t)' y" := (Op (Add (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint8_t)' x + y" := (Op (Add (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 3) (TWord 3) (TWord 3)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 3) (TWord 3) (TWord 3)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))). +Notation "'(uint16_t)' x + '(uint16_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 4)) (Pair x y)) (at level 50). +Notation "'(uint16_t)' x + '(uint16_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 50). +Notation "'(uint16_t)' x + '(uint16_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 50). +Notation "'(uint16_t)' x + '(uint16_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(uint16_t)' y" := (Op (Add (TWord 4) (TWord _) (TWord 4)) (Pair x y)) (at level 50). +Notation "'(uint16_t)' x + y" := (Op (Add (TWord _) (TWord 4) (TWord 4)) (Pair x y)) (at level 50). +Notation "x + '(uint16_t)' y" := (Op (Add (TWord 4) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 50). +Notation "'(uint16_t)' x + y" := (Op (Add (TWord _) (TWord 4) (TWord 4)) (Pair x (Var y))) (at level 50). +Notation "x + '(uint16_t)' y" := (Op (Add (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 50). +Notation "'(uint16_t)' x + y" := (Op (Add (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) y)) (at level 50). +Notation "x + '(uint16_t)' y" := (Op (Add (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint16_t)' x + y" := (Op (Add (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 4) (TWord 4) (TWord 4)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 4) (TWord 4) (TWord 4)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))). +Notation "'(uint32_t)' x + '(uint32_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 5)) (Pair x y)) (at level 50). +Notation "'(uint32_t)' x + '(uint32_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 50). +Notation "'(uint32_t)' x + '(uint32_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 50). +Notation "'(uint32_t)' x + '(uint32_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(uint32_t)' y" := (Op (Add (TWord 5) (TWord _) (TWord 5)) (Pair x y)) (at level 50). +Notation "'(uint32_t)' x + y" := (Op (Add (TWord _) (TWord 5) (TWord 5)) (Pair x y)) (at level 50). +Notation "x + '(uint32_t)' y" := (Op (Add (TWord 5) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 50). +Notation "'(uint32_t)' x + y" := (Op (Add (TWord _) (TWord 5) (TWord 5)) (Pair x (Var y))) (at level 50). +Notation "x + '(uint32_t)' y" := (Op (Add (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 50). +Notation "'(uint32_t)' x + y" := (Op (Add (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) y)) (at level 50). +Notation "x + '(uint32_t)' y" := (Op (Add (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint32_t)' x + y" := (Op (Add (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 5) (TWord 5) (TWord 5)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 5) (TWord 5) (TWord 5)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))). +Notation "'(uint64_t)' x + '(uint64_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 6)) (Pair x y)) (at level 50). +Notation "'(uint64_t)' x + '(uint64_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 50). +Notation "'(uint64_t)' x + '(uint64_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 50). +Notation "'(uint64_t)' x + '(uint64_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(uint64_t)' y" := (Op (Add (TWord 6) (TWord _) (TWord 6)) (Pair x y)) (at level 50). +Notation "'(uint64_t)' x + y" := (Op (Add (TWord _) (TWord 6) (TWord 6)) (Pair x y)) (at level 50). +Notation "x + '(uint64_t)' y" := (Op (Add (TWord 6) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 50). +Notation "'(uint64_t)' x + y" := (Op (Add (TWord _) (TWord 6) (TWord 6)) (Pair x (Var y))) (at level 50). +Notation "x + '(uint64_t)' y" := (Op (Add (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 50). +Notation "'(uint64_t)' x + y" := (Op (Add (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) y)) (at level 50). +Notation "x + '(uint64_t)' y" := (Op (Add (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint64_t)' x + y" := (Op (Add (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 6) (TWord 6) (TWord 6)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 6) (TWord 6) (TWord 6)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))). +Notation "'(uint128_t)' x + '(uint128_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 7)) (Pair x y)) (at level 50). +Notation "'(uint128_t)' x + '(uint128_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 50). +Notation "'(uint128_t)' x + '(uint128_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 50). +Notation "'(uint128_t)' x + '(uint128_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(uint128_t)' y" := (Op (Add (TWord 7) (TWord _) (TWord 7)) (Pair x y)) (at level 50). +Notation "'(uint128_t)' x + y" := (Op (Add (TWord _) (TWord 7) (TWord 7)) (Pair x y)) (at level 50). +Notation "x + '(uint128_t)' y" := (Op (Add (TWord 7) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 50). +Notation "'(uint128_t)' x + y" := (Op (Add (TWord _) (TWord 7) (TWord 7)) (Pair x (Var y))) (at level 50). +Notation "x + '(uint128_t)' y" := (Op (Add (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 50). +Notation "'(uint128_t)' x + y" := (Op (Add (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) y)) (at level 50). +Notation "x + '(uint128_t)' y" := (Op (Add (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint128_t)' x + y" := (Op (Add (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "x - y" := (Op (Sub _ _ _) (Pair x y)). +Notation "x - y" := (Op (Sub _ _ _) (Pair x (Var y))). +Notation "x - y" := (Op (Sub _ _ _) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub _ _ _) (Pair (Var x) (Var y))). +Notation "'(bool)' x - '(bool)' y" := (Op (Sub (TWord _) (TWord _) (TWord 0)) (Pair x y)) (at level 50). +Notation "'(bool)' x - '(bool)' y" := (Op (Sub (TWord _) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 50). +Notation "'(bool)' x - '(bool)' y" := (Op (Sub (TWord _) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 50). +Notation "'(bool)' x - '(bool)' y" := (Op (Sub (TWord _) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(bool)' y" := (Op (Sub (TWord 0) (TWord _) (TWord 0)) (Pair x y)) (at level 50). +Notation "'(bool)' x - y" := (Op (Sub (TWord _) (TWord 0) (TWord 0)) (Pair x y)) (at level 50). +Notation "x - '(bool)' y" := (Op (Sub (TWord 0) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 50). +Notation "'(bool)' x - y" := (Op (Sub (TWord _) (TWord 0) (TWord 0)) (Pair x (Var y))) (at level 50). +Notation "x - '(bool)' y" := (Op (Sub (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 50). +Notation "'(bool)' x - y" := (Op (Sub (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) y)) (at level 50). +Notation "x - '(bool)' y" := (Op (Sub (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(bool)' x - y" := (Op (Sub (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 0) (TWord 0) (TWord 0)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 0) (TWord 0) (TWord 0)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x - '(uint8_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 1)) (Pair x y)) (at level 50). +Notation "'(uint8_t)' x - '(uint8_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 50). +Notation "'(uint8_t)' x - '(uint8_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 50). +Notation "'(uint8_t)' x - '(uint8_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(uint8_t)' y" := (Op (Sub (TWord 1) (TWord _) (TWord 1)) (Pair x y)) (at level 50). +Notation "'(uint8_t)' x - y" := (Op (Sub (TWord _) (TWord 1) (TWord 1)) (Pair x y)) (at level 50). +Notation "x - '(uint8_t)' y" := (Op (Sub (TWord 1) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 50). +Notation "'(uint8_t)' x - y" := (Op (Sub (TWord _) (TWord 1) (TWord 1)) (Pair x (Var y))) (at level 50). +Notation "x - '(uint8_t)' y" := (Op (Sub (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 50). +Notation "'(uint8_t)' x - y" := (Op (Sub (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) y)) (at level 50). +Notation "x - '(uint8_t)' y" := (Op (Sub (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint8_t)' x - y" := (Op (Sub (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 1) (TWord 1) (TWord 1)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 1) (TWord 1) (TWord 1)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x - '(uint8_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 2)) (Pair x y)) (at level 50). +Notation "'(uint8_t)' x - '(uint8_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 50). +Notation "'(uint8_t)' x - '(uint8_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 50). +Notation "'(uint8_t)' x - '(uint8_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(uint8_t)' y" := (Op (Sub (TWord 2) (TWord _) (TWord 2)) (Pair x y)) (at level 50). +Notation "'(uint8_t)' x - y" := (Op (Sub (TWord _) (TWord 2) (TWord 2)) (Pair x y)) (at level 50). +Notation "x - '(uint8_t)' y" := (Op (Sub (TWord 2) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 50). +Notation "'(uint8_t)' x - y" := (Op (Sub (TWord _) (TWord 2) (TWord 2)) (Pair x (Var y))) (at level 50). +Notation "x - '(uint8_t)' y" := (Op (Sub (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 50). +Notation "'(uint8_t)' x - y" := (Op (Sub (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) y)) (at level 50). +Notation "x - '(uint8_t)' y" := (Op (Sub (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint8_t)' x - y" := (Op (Sub (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 2) (TWord 2) (TWord 2)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 2) (TWord 2) (TWord 2)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x - '(uint8_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 3)) (Pair x y)) (at level 50). +Notation "'(uint8_t)' x - '(uint8_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 50). +Notation "'(uint8_t)' x - '(uint8_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 50). +Notation "'(uint8_t)' x - '(uint8_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(uint8_t)' y" := (Op (Sub (TWord 3) (TWord _) (TWord 3)) (Pair x y)) (at level 50). +Notation "'(uint8_t)' x - y" := (Op (Sub (TWord _) (TWord 3) (TWord 3)) (Pair x y)) (at level 50). +Notation "x - '(uint8_t)' y" := (Op (Sub (TWord 3) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 50). +Notation "'(uint8_t)' x - y" := (Op (Sub (TWord _) (TWord 3) (TWord 3)) (Pair x (Var y))) (at level 50). +Notation "x - '(uint8_t)' y" := (Op (Sub (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 50). +Notation "'(uint8_t)' x - y" := (Op (Sub (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) y)) (at level 50). +Notation "x - '(uint8_t)' y" := (Op (Sub (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint8_t)' x - y" := (Op (Sub (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 3) (TWord 3) (TWord 3)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 3) (TWord 3) (TWord 3)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))). +Notation "'(uint16_t)' x - '(uint16_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 4)) (Pair x y)) (at level 50). +Notation "'(uint16_t)' x - '(uint16_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 50). +Notation "'(uint16_t)' x - '(uint16_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 50). +Notation "'(uint16_t)' x - '(uint16_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(uint16_t)' y" := (Op (Sub (TWord 4) (TWord _) (TWord 4)) (Pair x y)) (at level 50). +Notation "'(uint16_t)' x - y" := (Op (Sub (TWord _) (TWord 4) (TWord 4)) (Pair x y)) (at level 50). +Notation "x - '(uint16_t)' y" := (Op (Sub (TWord 4) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 50). +Notation "'(uint16_t)' x - y" := (Op (Sub (TWord _) (TWord 4) (TWord 4)) (Pair x (Var y))) (at level 50). +Notation "x - '(uint16_t)' y" := (Op (Sub (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 50). +Notation "'(uint16_t)' x - y" := (Op (Sub (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) y)) (at level 50). +Notation "x - '(uint16_t)' y" := (Op (Sub (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint16_t)' x - y" := (Op (Sub (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 4) (TWord 4) (TWord 4)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 4) (TWord 4) (TWord 4)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))). +Notation "'(uint32_t)' x - '(uint32_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 5)) (Pair x y)) (at level 50). +Notation "'(uint32_t)' x - '(uint32_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 50). +Notation "'(uint32_t)' x - '(uint32_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 50). +Notation "'(uint32_t)' x - '(uint32_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(uint32_t)' y" := (Op (Sub (TWord 5) (TWord _) (TWord 5)) (Pair x y)) (at level 50). +Notation "'(uint32_t)' x - y" := (Op (Sub (TWord _) (TWord 5) (TWord 5)) (Pair x y)) (at level 50). +Notation "x - '(uint32_t)' y" := (Op (Sub (TWord 5) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 50). +Notation "'(uint32_t)' x - y" := (Op (Sub (TWord _) (TWord 5) (TWord 5)) (Pair x (Var y))) (at level 50). +Notation "x - '(uint32_t)' y" := (Op (Sub (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 50). +Notation "'(uint32_t)' x - y" := (Op (Sub (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) y)) (at level 50). +Notation "x - '(uint32_t)' y" := (Op (Sub (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint32_t)' x - y" := (Op (Sub (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 5) (TWord 5) (TWord 5)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 5) (TWord 5) (TWord 5)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))). +Notation "'(uint64_t)' x - '(uint64_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 6)) (Pair x y)) (at level 50). +Notation "'(uint64_t)' x - '(uint64_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 50). +Notation "'(uint64_t)' x - '(uint64_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 50). +Notation "'(uint64_t)' x - '(uint64_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(uint64_t)' y" := (Op (Sub (TWord 6) (TWord _) (TWord 6)) (Pair x y)) (at level 50). +Notation "'(uint64_t)' x - y" := (Op (Sub (TWord _) (TWord 6) (TWord 6)) (Pair x y)) (at level 50). +Notation "x - '(uint64_t)' y" := (Op (Sub (TWord 6) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 50). +Notation "'(uint64_t)' x - y" := (Op (Sub (TWord _) (TWord 6) (TWord 6)) (Pair x (Var y))) (at level 50). +Notation "x - '(uint64_t)' y" := (Op (Sub (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 50). +Notation "'(uint64_t)' x - y" := (Op (Sub (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) y)) (at level 50). +Notation "x - '(uint64_t)' y" := (Op (Sub (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint64_t)' x - y" := (Op (Sub (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 6) (TWord 6) (TWord 6)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 6) (TWord 6) (TWord 6)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))). +Notation "'(uint128_t)' x - '(uint128_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 7)) (Pair x y)) (at level 50). +Notation "'(uint128_t)' x - '(uint128_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 50). +Notation "'(uint128_t)' x - '(uint128_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 50). +Notation "'(uint128_t)' x - '(uint128_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(uint128_t)' y" := (Op (Sub (TWord 7) (TWord _) (TWord 7)) (Pair x y)) (at level 50). +Notation "'(uint128_t)' x - y" := (Op (Sub (TWord _) (TWord 7) (TWord 7)) (Pair x y)) (at level 50). +Notation "x - '(uint128_t)' y" := (Op (Sub (TWord 7) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 50). +Notation "'(uint128_t)' x - y" := (Op (Sub (TWord _) (TWord 7) (TWord 7)) (Pair x (Var y))) (at level 50). +Notation "x - '(uint128_t)' y" := (Op (Sub (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 50). +Notation "'(uint128_t)' x - y" := (Op (Sub (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) y)) (at level 50). +Notation "x - '(uint128_t)' y" := (Op (Sub (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint128_t)' x - y" := (Op (Sub (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "x & y" := (Op (Land _ _ _) (Pair x y)). +Notation "x & y" := (Op (Land _ _ _) (Pair x (Var y))). +Notation "x & y" := (Op (Land _ _ _) (Pair (Var x) y)). +Notation "x & y" := (Op (Land _ _ _) (Pair (Var x) (Var y))). +Notation "'(bool)' x & '(bool)' y" := (Op (Land (TWord _) (TWord _) (TWord 0)) (Pair x y)) (at level 40). +Notation "'(bool)' x & '(bool)' y" := (Op (Land (TWord _) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 40). +Notation "'(bool)' x & '(bool)' y" := (Op (Land (TWord _) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 40). +Notation "'(bool)' x & '(bool)' y" := (Op (Land (TWord _) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(bool)' y" := (Op (Land (TWord 0) (TWord _) (TWord 0)) (Pair x y)) (at level 40). +Notation "'(bool)' x & y" := (Op (Land (TWord _) (TWord 0) (TWord 0)) (Pair x y)) (at level 40). +Notation "x & '(bool)' y" := (Op (Land (TWord 0) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 40). +Notation "'(bool)' x & y" := (Op (Land (TWord _) (TWord 0) (TWord 0)) (Pair x (Var y))) (at level 40). +Notation "x & '(bool)' y" := (Op (Land (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 40). +Notation "'(bool)' x & y" := (Op (Land (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) y)) (at level 40). +Notation "x & '(bool)' y" := (Op (Land (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(bool)' x & y" := (Op (Land (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 0) (TWord 0) (TWord 0)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 0) (TWord 0) (TWord 0)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x & '(uint8_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 1)) (Pair x y)) (at level 40). +Notation "'(uint8_t)' x & '(uint8_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 40). +Notation "'(uint8_t)' x & '(uint8_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 40). +Notation "'(uint8_t)' x & '(uint8_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(uint8_t)' y" := (Op (Land (TWord 1) (TWord _) (TWord 1)) (Pair x y)) (at level 40). +Notation "'(uint8_t)' x & y" := (Op (Land (TWord _) (TWord 1) (TWord 1)) (Pair x y)) (at level 40). +Notation "x & '(uint8_t)' y" := (Op (Land (TWord 1) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 40). +Notation "'(uint8_t)' x & y" := (Op (Land (TWord _) (TWord 1) (TWord 1)) (Pair x (Var y))) (at level 40). +Notation "x & '(uint8_t)' y" := (Op (Land (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 40). +Notation "'(uint8_t)' x & y" := (Op (Land (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) y)) (at level 40). +Notation "x & '(uint8_t)' y" := (Op (Land (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint8_t)' x & y" := (Op (Land (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 1) (TWord 1) (TWord 1)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 1) (TWord 1) (TWord 1)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x & '(uint8_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 2)) (Pair x y)) (at level 40). +Notation "'(uint8_t)' x & '(uint8_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 40). +Notation "'(uint8_t)' x & '(uint8_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 40). +Notation "'(uint8_t)' x & '(uint8_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(uint8_t)' y" := (Op (Land (TWord 2) (TWord _) (TWord 2)) (Pair x y)) (at level 40). +Notation "'(uint8_t)' x & y" := (Op (Land (TWord _) (TWord 2) (TWord 2)) (Pair x y)) (at level 40). +Notation "x & '(uint8_t)' y" := (Op (Land (TWord 2) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 40). +Notation "'(uint8_t)' x & y" := (Op (Land (TWord _) (TWord 2) (TWord 2)) (Pair x (Var y))) (at level 40). +Notation "x & '(uint8_t)' y" := (Op (Land (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 40). +Notation "'(uint8_t)' x & y" := (Op (Land (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) y)) (at level 40). +Notation "x & '(uint8_t)' y" := (Op (Land (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint8_t)' x & y" := (Op (Land (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 2) (TWord 2) (TWord 2)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 2) (TWord 2) (TWord 2)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x & '(uint8_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 3)) (Pair x y)) (at level 40). +Notation "'(uint8_t)' x & '(uint8_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 40). +Notation "'(uint8_t)' x & '(uint8_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 40). +Notation "'(uint8_t)' x & '(uint8_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(uint8_t)' y" := (Op (Land (TWord 3) (TWord _) (TWord 3)) (Pair x y)) (at level 40). +Notation "'(uint8_t)' x & y" := (Op (Land (TWord _) (TWord 3) (TWord 3)) (Pair x y)) (at level 40). +Notation "x & '(uint8_t)' y" := (Op (Land (TWord 3) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 40). +Notation "'(uint8_t)' x & y" := (Op (Land (TWord _) (TWord 3) (TWord 3)) (Pair x (Var y))) (at level 40). +Notation "x & '(uint8_t)' y" := (Op (Land (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 40). +Notation "'(uint8_t)' x & y" := (Op (Land (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) y)) (at level 40). +Notation "x & '(uint8_t)' y" := (Op (Land (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint8_t)' x & y" := (Op (Land (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 3) (TWord 3) (TWord 3)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 3) (TWord 3) (TWord 3)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))). +Notation "'(uint16_t)' x & '(uint16_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 4)) (Pair x y)) (at level 40). +Notation "'(uint16_t)' x & '(uint16_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 40). +Notation "'(uint16_t)' x & '(uint16_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 40). +Notation "'(uint16_t)' x & '(uint16_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(uint16_t)' y" := (Op (Land (TWord 4) (TWord _) (TWord 4)) (Pair x y)) (at level 40). +Notation "'(uint16_t)' x & y" := (Op (Land (TWord _) (TWord 4) (TWord 4)) (Pair x y)) (at level 40). +Notation "x & '(uint16_t)' y" := (Op (Land (TWord 4) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 40). +Notation "'(uint16_t)' x & y" := (Op (Land (TWord _) (TWord 4) (TWord 4)) (Pair x (Var y))) (at level 40). +Notation "x & '(uint16_t)' y" := (Op (Land (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 40). +Notation "'(uint16_t)' x & y" := (Op (Land (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) y)) (at level 40). +Notation "x & '(uint16_t)' y" := (Op (Land (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint16_t)' x & y" := (Op (Land (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 4) (TWord 4) (TWord 4)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 4) (TWord 4) (TWord 4)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))). +Notation "'(uint32_t)' x & '(uint32_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 5)) (Pair x y)) (at level 40). +Notation "'(uint32_t)' x & '(uint32_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 40). +Notation "'(uint32_t)' x & '(uint32_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 40). +Notation "'(uint32_t)' x & '(uint32_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(uint32_t)' y" := (Op (Land (TWord 5) (TWord _) (TWord 5)) (Pair x y)) (at level 40). +Notation "'(uint32_t)' x & y" := (Op (Land (TWord _) (TWord 5) (TWord 5)) (Pair x y)) (at level 40). +Notation "x & '(uint32_t)' y" := (Op (Land (TWord 5) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 40). +Notation "'(uint32_t)' x & y" := (Op (Land (TWord _) (TWord 5) (TWord 5)) (Pair x (Var y))) (at level 40). +Notation "x & '(uint32_t)' y" := (Op (Land (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 40). +Notation "'(uint32_t)' x & y" := (Op (Land (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) y)) (at level 40). +Notation "x & '(uint32_t)' y" := (Op (Land (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint32_t)' x & y" := (Op (Land (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 5) (TWord 5) (TWord 5)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 5) (TWord 5) (TWord 5)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))). +Notation "'(uint64_t)' x & '(uint64_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 6)) (Pair x y)) (at level 40). +Notation "'(uint64_t)' x & '(uint64_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 40). +Notation "'(uint64_t)' x & '(uint64_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 40). +Notation "'(uint64_t)' x & '(uint64_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(uint64_t)' y" := (Op (Land (TWord 6) (TWord _) (TWord 6)) (Pair x y)) (at level 40). +Notation "'(uint64_t)' x & y" := (Op (Land (TWord _) (TWord 6) (TWord 6)) (Pair x y)) (at level 40). +Notation "x & '(uint64_t)' y" := (Op (Land (TWord 6) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 40). +Notation "'(uint64_t)' x & y" := (Op (Land (TWord _) (TWord 6) (TWord 6)) (Pair x (Var y))) (at level 40). +Notation "x & '(uint64_t)' y" := (Op (Land (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 40). +Notation "'(uint64_t)' x & y" := (Op (Land (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) y)) (at level 40). +Notation "x & '(uint64_t)' y" := (Op (Land (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint64_t)' x & y" := (Op (Land (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 6) (TWord 6) (TWord 6)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 6) (TWord 6) (TWord 6)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))). +Notation "'(uint128_t)' x & '(uint128_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 7)) (Pair x y)) (at level 40). +Notation "'(uint128_t)' x & '(uint128_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 40). +Notation "'(uint128_t)' x & '(uint128_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 40). +Notation "'(uint128_t)' x & '(uint128_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(uint128_t)' y" := (Op (Land (TWord 7) (TWord _) (TWord 7)) (Pair x y)) (at level 40). +Notation "'(uint128_t)' x & y" := (Op (Land (TWord _) (TWord 7) (TWord 7)) (Pair x y)) (at level 40). +Notation "x & '(uint128_t)' y" := (Op (Land (TWord 7) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 40). +Notation "'(uint128_t)' x & y" := (Op (Land (TWord _) (TWord 7) (TWord 7)) (Pair x (Var y))) (at level 40). +Notation "x & '(uint128_t)' y" := (Op (Land (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 40). +Notation "'(uint128_t)' x & y" := (Op (Land (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) y)) (at level 40). +Notation "x & '(uint128_t)' y" := (Op (Land (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint128_t)' x & y" := (Op (Land (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "x << y" := (Op (Shl _ _ _) (Pair x y)). +Notation "x << y" := (Op (Shl _ _ _) (Pair x (Var y))). +Notation "x << y" := (Op (Shl _ _ _) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl _ _ _) (Pair (Var x) (Var y))). +Notation "'(bool)' x << '(bool)' y" := (Op (Shl (TWord _) (TWord _) (TWord 0)) (Pair x y)) (at level 30). +Notation "'(bool)' x << '(bool)' y" := (Op (Shl (TWord _) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 30). +Notation "'(bool)' x << '(bool)' y" := (Op (Shl (TWord _) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 30). +Notation "'(bool)' x << '(bool)' y" := (Op (Shl (TWord _) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(bool)' y" := (Op (Shl (TWord 0) (TWord _) (TWord 0)) (Pair x y)) (at level 30). +Notation "'(bool)' x << y" := (Op (Shl (TWord _) (TWord 0) (TWord 0)) (Pair x y)) (at level 30). +Notation "x << '(bool)' y" := (Op (Shl (TWord 0) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 30). +Notation "'(bool)' x << y" := (Op (Shl (TWord _) (TWord 0) (TWord 0)) (Pair x (Var y))) (at level 30). +Notation "x << '(bool)' y" := (Op (Shl (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 30). +Notation "'(bool)' x << y" := (Op (Shl (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) y)) (at level 30). +Notation "x << '(bool)' y" := (Op (Shl (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(bool)' x << y" := (Op (Shl (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 0) (TWord 0) (TWord 0)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 0) (TWord 0) (TWord 0)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x << '(uint8_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 1)) (Pair x y)) (at level 30). +Notation "'(uint8_t)' x << '(uint8_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 30). +Notation "'(uint8_t)' x << '(uint8_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 30). +Notation "'(uint8_t)' x << '(uint8_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(uint8_t)' y" := (Op (Shl (TWord 1) (TWord _) (TWord 1)) (Pair x y)) (at level 30). +Notation "'(uint8_t)' x << y" := (Op (Shl (TWord _) (TWord 1) (TWord 1)) (Pair x y)) (at level 30). +Notation "x << '(uint8_t)' y" := (Op (Shl (TWord 1) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 30). +Notation "'(uint8_t)' x << y" := (Op (Shl (TWord _) (TWord 1) (TWord 1)) (Pair x (Var y))) (at level 30). +Notation "x << '(uint8_t)' y" := (Op (Shl (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 30). +Notation "'(uint8_t)' x << y" := (Op (Shl (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) y)) (at level 30). +Notation "x << '(uint8_t)' y" := (Op (Shl (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint8_t)' x << y" := (Op (Shl (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 1) (TWord 1) (TWord 1)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 1) (TWord 1) (TWord 1)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x << '(uint8_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 2)) (Pair x y)) (at level 30). +Notation "'(uint8_t)' x << '(uint8_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 30). +Notation "'(uint8_t)' x << '(uint8_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 30). +Notation "'(uint8_t)' x << '(uint8_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(uint8_t)' y" := (Op (Shl (TWord 2) (TWord _) (TWord 2)) (Pair x y)) (at level 30). +Notation "'(uint8_t)' x << y" := (Op (Shl (TWord _) (TWord 2) (TWord 2)) (Pair x y)) (at level 30). +Notation "x << '(uint8_t)' y" := (Op (Shl (TWord 2) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 30). +Notation "'(uint8_t)' x << y" := (Op (Shl (TWord _) (TWord 2) (TWord 2)) (Pair x (Var y))) (at level 30). +Notation "x << '(uint8_t)' y" := (Op (Shl (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 30). +Notation "'(uint8_t)' x << y" := (Op (Shl (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) y)) (at level 30). +Notation "x << '(uint8_t)' y" := (Op (Shl (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint8_t)' x << y" := (Op (Shl (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 2) (TWord 2) (TWord 2)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 2) (TWord 2) (TWord 2)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x << '(uint8_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 3)) (Pair x y)) (at level 30). +Notation "'(uint8_t)' x << '(uint8_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 30). +Notation "'(uint8_t)' x << '(uint8_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 30). +Notation "'(uint8_t)' x << '(uint8_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(uint8_t)' y" := (Op (Shl (TWord 3) (TWord _) (TWord 3)) (Pair x y)) (at level 30). +Notation "'(uint8_t)' x << y" := (Op (Shl (TWord _) (TWord 3) (TWord 3)) (Pair x y)) (at level 30). +Notation "x << '(uint8_t)' y" := (Op (Shl (TWord 3) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 30). +Notation "'(uint8_t)' x << y" := (Op (Shl (TWord _) (TWord 3) (TWord 3)) (Pair x (Var y))) (at level 30). +Notation "x << '(uint8_t)' y" := (Op (Shl (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 30). +Notation "'(uint8_t)' x << y" := (Op (Shl (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) y)) (at level 30). +Notation "x << '(uint8_t)' y" := (Op (Shl (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint8_t)' x << y" := (Op (Shl (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 3) (TWord 3) (TWord 3)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 3) (TWord 3) (TWord 3)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))). +Notation "'(uint16_t)' x << '(uint16_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 4)) (Pair x y)) (at level 30). +Notation "'(uint16_t)' x << '(uint16_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 30). +Notation "'(uint16_t)' x << '(uint16_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 30). +Notation "'(uint16_t)' x << '(uint16_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(uint16_t)' y" := (Op (Shl (TWord 4) (TWord _) (TWord 4)) (Pair x y)) (at level 30). +Notation "'(uint16_t)' x << y" := (Op (Shl (TWord _) (TWord 4) (TWord 4)) (Pair x y)) (at level 30). +Notation "x << '(uint16_t)' y" := (Op (Shl (TWord 4) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 30). +Notation "'(uint16_t)' x << y" := (Op (Shl (TWord _) (TWord 4) (TWord 4)) (Pair x (Var y))) (at level 30). +Notation "x << '(uint16_t)' y" := (Op (Shl (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 30). +Notation "'(uint16_t)' x << y" := (Op (Shl (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) y)) (at level 30). +Notation "x << '(uint16_t)' y" := (Op (Shl (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint16_t)' x << y" := (Op (Shl (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 4) (TWord 4) (TWord 4)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 4) (TWord 4) (TWord 4)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))). +Notation "'(uint32_t)' x << '(uint32_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 5)) (Pair x y)) (at level 30). +Notation "'(uint32_t)' x << '(uint32_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 30). +Notation "'(uint32_t)' x << '(uint32_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 30). +Notation "'(uint32_t)' x << '(uint32_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(uint32_t)' y" := (Op (Shl (TWord 5) (TWord _) (TWord 5)) (Pair x y)) (at level 30). +Notation "'(uint32_t)' x << y" := (Op (Shl (TWord _) (TWord 5) (TWord 5)) (Pair x y)) (at level 30). +Notation "x << '(uint32_t)' y" := (Op (Shl (TWord 5) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 30). +Notation "'(uint32_t)' x << y" := (Op (Shl (TWord _) (TWord 5) (TWord 5)) (Pair x (Var y))) (at level 30). +Notation "x << '(uint32_t)' y" := (Op (Shl (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 30). +Notation "'(uint32_t)' x << y" := (Op (Shl (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) y)) (at level 30). +Notation "x << '(uint32_t)' y" := (Op (Shl (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint32_t)' x << y" := (Op (Shl (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 5) (TWord 5) (TWord 5)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 5) (TWord 5) (TWord 5)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))). +Notation "'(uint64_t)' x << '(uint64_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 6)) (Pair x y)) (at level 30). +Notation "'(uint64_t)' x << '(uint64_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 30). +Notation "'(uint64_t)' x << '(uint64_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 30). +Notation "'(uint64_t)' x << '(uint64_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(uint64_t)' y" := (Op (Shl (TWord 6) (TWord _) (TWord 6)) (Pair x y)) (at level 30). +Notation "'(uint64_t)' x << y" := (Op (Shl (TWord _) (TWord 6) (TWord 6)) (Pair x y)) (at level 30). +Notation "x << '(uint64_t)' y" := (Op (Shl (TWord 6) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 30). +Notation "'(uint64_t)' x << y" := (Op (Shl (TWord _) (TWord 6) (TWord 6)) (Pair x (Var y))) (at level 30). +Notation "x << '(uint64_t)' y" := (Op (Shl (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 30). +Notation "'(uint64_t)' x << y" := (Op (Shl (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) y)) (at level 30). +Notation "x << '(uint64_t)' y" := (Op (Shl (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint64_t)' x << y" := (Op (Shl (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 6) (TWord 6) (TWord 6)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 6) (TWord 6) (TWord 6)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))). +Notation "'(uint128_t)' x << '(uint128_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 7)) (Pair x y)) (at level 30). +Notation "'(uint128_t)' x << '(uint128_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 30). +Notation "'(uint128_t)' x << '(uint128_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 30). +Notation "'(uint128_t)' x << '(uint128_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(uint128_t)' y" := (Op (Shl (TWord 7) (TWord _) (TWord 7)) (Pair x y)) (at level 30). +Notation "'(uint128_t)' x << y" := (Op (Shl (TWord _) (TWord 7) (TWord 7)) (Pair x y)) (at level 30). +Notation "x << '(uint128_t)' y" := (Op (Shl (TWord 7) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 30). +Notation "'(uint128_t)' x << y" := (Op (Shl (TWord _) (TWord 7) (TWord 7)) (Pair x (Var y))) (at level 30). +Notation "x << '(uint128_t)' y" := (Op (Shl (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 30). +Notation "'(uint128_t)' x << y" := (Op (Shl (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) y)) (at level 30). +Notation "x << '(uint128_t)' y" := (Op (Shl (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint128_t)' x << y" := (Op (Shl (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "x >> y" := (Op (Shr _ _ _) (Pair x y)). +Notation "x >> y" := (Op (Shr _ _ _) (Pair x (Var y))). +Notation "x >> y" := (Op (Shr _ _ _) (Pair (Var x) y)). +Notation "x >> y" := (Op (Shr _ _ _) (Pair (Var x) (Var y))). +Notation "'(bool)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 0)) (Pair x y)) (at level 30). +Notation "'(bool)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 30). +Notation "'(bool)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 30). +Notation "'(bool)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint8_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 1)) (Pair x y)) (at level 30). +Notation "'(uint8_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 30). +Notation "'(uint8_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 30). +Notation "'(uint8_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint8_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 2)) (Pair x y)) (at level 30). +Notation "'(uint8_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 30). +Notation "'(uint8_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 30). +Notation "'(uint8_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint8_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 3)) (Pair x y)) (at level 30). +Notation "'(uint8_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 30). +Notation "'(uint8_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 30). +Notation "'(uint8_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint16_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 4)) (Pair x y)) (at level 30). +Notation "'(uint16_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 30). +Notation "'(uint16_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 30). +Notation "'(uint16_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint32_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 5)) (Pair x y)) (at level 30). +Notation "'(uint32_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 30). +Notation "'(uint32_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 30). +Notation "'(uint32_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint64_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 6)) (Pair x y)) (at level 30). +Notation "'(uint64_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 30). +Notation "'(uint64_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 30). +Notation "'(uint64_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint128_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 7)) (Pair x y)) (at level 30). +Notation "'(uint128_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 30). +Notation "'(uint128_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 30). +Notation "'(uint128_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 30). Notation Return x := (Var x). Notation C_like := (Expr base_type op _). diff --git a/src/Reflection/Z/JavaNotations.v b/src/Reflection/Z/JavaNotations.v index 96a04f5fc..d0e32610b 100644 --- a/src/Reflection/Z/JavaNotations.v +++ b/src/Reflection/Z/JavaNotations.v @@ -4,9 +4,6 @@ Require Export Crypto.Reflection.Z.HexNotationConstants. Require Export Crypto.Util.Notations. Reserved Notation "T x = A ; b" (at level 200, b at level 200, format "T x = A ; '//' b"). -Reserved Notation "'(int)' x" (at level 200, x at level 9). -Reserved Notation "'(long)' x" (at level 200, x at level 9). -Reserved Notation "'(uint128_t)' x" (at level 200, x at level 9). Reserved Notation "x & y" (at level 40). (* N.B. M32 is 0xFFFFFFFFL, and is how to cast a 64-bit thing to a 32-bit thing in Java *) Reserved Notation "'M32' & x" (at level 200, x at level 9). @@ -14,15 +11,8 @@ Reserved Notation "'M32' & x" (at level 200, x at level 9). Global Open Scope expr_scope. Notation "T x = A ; b" := (LetIn (tx:=T) A (fun x => b)) : expr_scope. -Notation "'int'" := (Tbase (TWord 0)). -Notation "'int'" := (Tbase (TWord 1)). -Notation "'int'" := (Tbase (TWord 2)). -Notation "'int'" := (Tbase (TWord 3)). -Notation "'int'" := (Tbase (TWord 4)). -Notation "'int'" := (Tbase (TWord 5)). -Notation long := (Tbase (TWord 6)). -Notation uint128_t := (Tbase (TWord 7)). -Notation "'(int)' x" := (Op (Cast _ (TWord 0)) x). +(* ??? Did I get M32 wrong? *) +(*Notation "'(int)' x" := (Op (Cast _ (TWord 0)) x). Notation "'(int)' x" := (Op (Cast _ (TWord 1)) x). Notation "'(int)' x" := (Op (Cast _ (TWord 2)) x). Notation "'(int)' x" := (Op (Cast _ (TWord 3)) x). @@ -37,107 +27,764 @@ Notation "'(int)' x" := (Op (Cast _ (TWord 3)) (Var x)). Notation "'(int)' x" := (Op (Cast _ (TWord 4)) (Var x)). Notation "'(int)' x" := (Op (Cast _ (TWord 5)) (Var x)). Notation "'M32' & x" := (Op (Cast _ (TWord 6)) (Var x)). -Notation "'(uint128_t)' x" := (Op (Cast _ (TWord 7)) (Var x)). -Notation "x + y" := (Op (Add _) (Pair x y)). -Notation "x + y" := (Op (Add _) (Pair (Var x) y)). -Notation "x + y" := (Op (Add _) (Pair x (Var y))). -Notation "x + y" := (Op (Add _) (Pair (Var x) (Var y))). -Notation "x - y" := (Op (Sub _) (Pair x y)). -Notation "x - y" := (Op (Sub _) (Pair (Var x) y)). -Notation "x - y" := (Op (Sub _) (Pair x (Var y))). -Notation "x - y" := (Op (Sub _) (Pair (Var x) (Var y))). -Notation "x * y" := (Op (Mul _) (Pair x y)). -Notation "x * y" := (Op (Mul _) (Pair (Var x) y)). -Notation "x * y" := (Op (Mul _) (Pair x (Var y))). -Notation "x * y" := (Op (Mul _) (Pair (Var x) (Var y))). +Notation "'(uint128_t)' x" := (Op (Cast _ (TWord 7)) (Var x)).*) (* python: << -for opn, op in (('*', 'Mul'), ('+', 'Add'), ('&', 'Land')): - for lgwordsz in (5, 6, 7): - for side in ('l', 'r'): - for v1 in (False, True): - for v2 in (False, True): - lhs = ('x' if not v1 else '(Var x)') - lhs = (lhs if side != 'l' else '(Op (Cast _ (TWord %d)) %s)' % (lgwordsz, lhs)) - rhs = ('y' if not v2 else '(Var y)') - rhs = (rhs if side != 'r' else '(Op (Cast _ (TWord %d)) %s)' % (lgwordsz, rhs)) - print('Notation "x %s y" := (Op (%s (TWord %d)) (Pair %s %s)).' % (opn, op, lgwordsz, lhs, rhs)) +types = ('int', 'int', 'int', 'int', 'int', 'int', 'long', 'uint128_t') +for lgwordsz in range(0, len(types)): + print('Notation "\'%s\'" := (Tbase (TWord %d)).' % (types[lgwordsz], lgwordsz)) +print('') +cast_pat = "'(%s)' %s" +for opn, op, lvl in (('*', 'Mul', 40), ('+', 'Add', 50), ('-', 'Sub', 50), ('&', 'Land', 40), ('<<', 'Shl', 30)): + for v1 in (False, True): + for v2 in (False, True): + lhs = ('x' if not v1 else '(Var x)') + rhs = ('y' if not v2 else '(Var y)') + print('Notation "x %s y" := (Op (%s _ _ _) (Pair %s %s)).' % (opn, op, lhs, rhs)) + for lgwordsz in range(0, len(types)): + for v1 in (False, True): + for v2 in (False, True): + lhs = ('x' if not v1 else '(Var x)') + rhs = ('y' if not v2 else '(Var y)') + print('Notation "%s %s %s" := (Op (%s (TWord _) (TWord _) (TWord %d)) (Pair %s %s)) (at level %d).' + % (cast_pat % (types[lgwordsz], 'x'), opn, cast_pat % (types[lgwordsz], 'y'), + op, lgwordsz, lhs, rhs, lvl)) + for v1 in (False, True): + for v2 in (False, True): + lhs = ('x' if not v1 else '(Var x)') + rhs = ('y' if not v2 else '(Var y)') + print('Notation "%s %s %s" := (Op (%s (TWord %d) (TWord _) (TWord %d)) (Pair %s %s)) (at level %d).' + % ('x', opn, cast_pat % (types[lgwordsz], 'y'), + op, lgwordsz, lgwordsz, lhs, rhs, lvl)) + print('Notation "%s %s %s" := (Op (%s (TWord _) (TWord %d) (TWord %d)) (Pair %s %s)) (at level %d).' + % (cast_pat % (types[lgwordsz], 'x'), opn, 'y', + op, lgwordsz, lgwordsz, lhs, rhs, lvl)) + for v1 in (False, True): + for v2 in (False, True): + lhs = ('x' if not v1 else '(Var x)') + rhs = ('y' if not v2 else '(Var y)') + print('Notation "x %s y" := (Op (%s (TWord %d) (TWord %d) (TWord %d)) (Pair %s %s)).' + % (opn, op, lgwordsz, lgwordsz, lgwordsz, lhs, rhs)) +for opn, op, lvl in (('>>', 'Shr', 30),): + for v1 in (False, True): + for v2 in (False, True): + lhs = ('x' if not v1 else '(Var x)') + rhs = ('y' if not v2 else '(Var y)') + print('Notation "x %s y" := (Op (%s _ _ _) (Pair %s %s)).' % (opn, op, lhs, rhs)) + for lgwordsz in range(0, len(types)): + for v1 in (False, True): + for v2 in (False, True): + lhs = ('x' if not v1 else '(Var x)') + rhs = ('y' if not v2 else '(Var y)') + print('Notation "\'(%s)\' ( x %s y )" := (Op (%s (TWord _) (TWord _) (TWord %d)) (Pair %s %s)) (at level %d).' + % (types[lgwordsz], opn, op, lgwordsz, lhs, rhs, lvl)) +print('Notation Return x := (Var x).') +print('Notation Java_like := (Expr base_type op _).') >> *) -Notation "x * y" := (Op (Mul (TWord 5)) (Pair (Op (Cast _ (TWord 5)) x) y)). -Notation "x * y" := (Op (Mul (TWord 5)) (Pair (Op (Cast _ (TWord 5)) x) (Var y))). -Notation "x * y" := (Op (Mul (TWord 5)) (Pair (Op (Cast _ (TWord 5)) (Var x)) y)). -Notation "x * y" := (Op (Mul (TWord 5)) (Pair (Op (Cast _ (TWord 5)) (Var x)) (Var y))). -Notation "x * y" := (Op (Mul (TWord 5)) (Pair x (Op (Cast _ (TWord 5)) y))). -Notation "x * y" := (Op (Mul (TWord 5)) (Pair x (Op (Cast _ (TWord 5)) (Var y)))). -Notation "x * y" := (Op (Mul (TWord 5)) (Pair (Var x) (Op (Cast _ (TWord 5)) y))). -Notation "x * y" := (Op (Mul (TWord 5)) (Pair (Var x) (Op (Cast _ (TWord 5)) (Var y)))). -Notation "x * y" := (Op (Mul (TWord 6)) (Pair (Op (Cast _ (TWord 6)) x) y)). -Notation "x * y" := (Op (Mul (TWord 6)) (Pair (Op (Cast _ (TWord 6)) x) (Var y))). -Notation "x * y" := (Op (Mul (TWord 6)) (Pair (Op (Cast _ (TWord 6)) (Var x)) y)). -Notation "x * y" := (Op (Mul (TWord 6)) (Pair (Op (Cast _ (TWord 6)) (Var x)) (Var y))). -Notation "x * y" := (Op (Mul (TWord 6)) (Pair x (Op (Cast _ (TWord 6)) y))). -Notation "x * y" := (Op (Mul (TWord 6)) (Pair x (Op (Cast _ (TWord 6)) (Var y)))). -Notation "x * y" := (Op (Mul (TWord 6)) (Pair (Var x) (Op (Cast _ (TWord 6)) y))). -Notation "x * y" := (Op (Mul (TWord 6)) (Pair (Var x) (Op (Cast _ (TWord 6)) (Var y)))). -Notation "x * y" := (Op (Mul (TWord 7)) (Pair (Op (Cast _ (TWord 7)) x) y)). -Notation "x * y" := (Op (Mul (TWord 7)) (Pair (Op (Cast _ (TWord 7)) x) (Var y))). -Notation "x * y" := (Op (Mul (TWord 7)) (Pair (Op (Cast _ (TWord 7)) (Var x)) y)). -Notation "x * y" := (Op (Mul (TWord 7)) (Pair (Op (Cast _ (TWord 7)) (Var x)) (Var y))). -Notation "x * y" := (Op (Mul (TWord 7)) (Pair x (Op (Cast _ (TWord 7)) y))). -Notation "x * y" := (Op (Mul (TWord 7)) (Pair x (Op (Cast _ (TWord 7)) (Var y)))). -Notation "x * y" := (Op (Mul (TWord 7)) (Pair (Var x) (Op (Cast _ (TWord 7)) y))). -Notation "x * y" := (Op (Mul (TWord 7)) (Pair (Var x) (Op (Cast _ (TWord 7)) (Var y)))). -Notation "x + y" := (Op (Add (TWord 5)) (Pair (Op (Cast _ (TWord 5)) x) y)). -Notation "x + y" := (Op (Add (TWord 5)) (Pair (Op (Cast _ (TWord 5)) x) (Var y))). -Notation "x + y" := (Op (Add (TWord 5)) (Pair (Op (Cast _ (TWord 5)) (Var x)) y)). -Notation "x + y" := (Op (Add (TWord 5)) (Pair (Op (Cast _ (TWord 5)) (Var x)) (Var y))). -Notation "x + y" := (Op (Add (TWord 5)) (Pair x (Op (Cast _ (TWord 5)) y))). -Notation "x + y" := (Op (Add (TWord 5)) (Pair x (Op (Cast _ (TWord 5)) (Var y)))). -Notation "x + y" := (Op (Add (TWord 5)) (Pair (Var x) (Op (Cast _ (TWord 5)) y))). -Notation "x + y" := (Op (Add (TWord 5)) (Pair (Var x) (Op (Cast _ (TWord 5)) (Var y)))). -Notation "x + y" := (Op (Add (TWord 6)) (Pair (Op (Cast _ (TWord 6)) x) y)). -Notation "x + y" := (Op (Add (TWord 6)) (Pair (Op (Cast _ (TWord 6)) x) (Var y))). -Notation "x + y" := (Op (Add (TWord 6)) (Pair (Op (Cast _ (TWord 6)) (Var x)) y)). -Notation "x + y" := (Op (Add (TWord 6)) (Pair (Op (Cast _ (TWord 6)) (Var x)) (Var y))). -Notation "x + y" := (Op (Add (TWord 6)) (Pair x (Op (Cast _ (TWord 6)) y))). -Notation "x + y" := (Op (Add (TWord 6)) (Pair x (Op (Cast _ (TWord 6)) (Var y)))). -Notation "x + y" := (Op (Add (TWord 6)) (Pair (Var x) (Op (Cast _ (TWord 6)) y))). -Notation "x + y" := (Op (Add (TWord 6)) (Pair (Var x) (Op (Cast _ (TWord 6)) (Var y)))). -Notation "x + y" := (Op (Add (TWord 7)) (Pair (Op (Cast _ (TWord 7)) x) y)). -Notation "x + y" := (Op (Add (TWord 7)) (Pair (Op (Cast _ (TWord 7)) x) (Var y))). -Notation "x + y" := (Op (Add (TWord 7)) (Pair (Op (Cast _ (TWord 7)) (Var x)) y)). -Notation "x + y" := (Op (Add (TWord 7)) (Pair (Op (Cast _ (TWord 7)) (Var x)) (Var y))). -Notation "x + y" := (Op (Add (TWord 7)) (Pair x (Op (Cast _ (TWord 7)) y))). -Notation "x + y" := (Op (Add (TWord 7)) (Pair x (Op (Cast _ (TWord 7)) (Var y)))). -Notation "x + y" := (Op (Add (TWord 7)) (Pair (Var x) (Op (Cast _ (TWord 7)) y))). -Notation "x + y" := (Op (Add (TWord 7)) (Pair (Var x) (Op (Cast _ (TWord 7)) (Var y)))). -Notation "x >>> y" := (Op (Shr _) (Pair x y)). -Notation "x >>> y" := (Op (Shr _) (Pair (Var x) y)). -Notation "x >>> y" := (Op (Shr _) (Pair x (Var y))). -Notation "x >>> y" := (Op (Shr _) (Pair (Var x) (Var y))). -Notation "x >>> y" := (Op (Shr _) (Pair x (Op (Cast _ _) y))). -Notation "x >>> y" := (Op (Shr _) (Pair (Var x) (Op (Cast _ _) y))). -Notation "x >>> y" := (Op (Shr _) (Pair x (Op (Cast _ _) (Var y)))). -Notation "x >>> y" := (Op (Shr _) (Pair (Var x) (Op (Cast _ _) (Var y)))). -Notation "x & y" := (Op (Land _) (Pair x y)). -Notation "x & y" := (Op (Land _) (Pair (Var x) y)). -Notation "x & y" := (Op (Land _) (Pair x (Var y))). -Notation "x & y" := (Op (Land _) (Pair (Var x) (Var y))). -Notation "x & y" := (Op (Land (TWord 6)) (Pair (Op (Cast _ (TWord 6)) x) y)). -Notation "x & y" := (Op (Land (TWord 6)) (Pair (Op (Cast _ (TWord 6)) x) (Var y))). -Notation "x & y" := (Op (Land (TWord 6)) (Pair (Op (Cast _ (TWord 6)) (Var x)) y)). -Notation "x & y" := (Op (Land (TWord 6)) (Pair (Op (Cast _ (TWord 6)) (Var x)) (Var y))). -Notation "x & y" := (Op (Land (TWord 6)) (Pair x (Op (Cast _ (TWord 6)) y))). -Notation "x & y" := (Op (Land (TWord 6)) (Pair x (Op (Cast _ (TWord 6)) (Var y)))). -Notation "x & y" := (Op (Land (TWord 6)) (Pair (Var x) (Op (Cast _ (TWord 6)) y))). -Notation "x & y" := (Op (Land (TWord 6)) (Pair (Var x) (Op (Cast _ (TWord 6)) (Var y)))). -Notation "x & y" := (Op (Land (TWord 7)) (Pair (Op (Cast _ (TWord 7)) x) y)). -Notation "x & y" := (Op (Land (TWord 7)) (Pair (Op (Cast _ (TWord 7)) x) (Var y))). -Notation "x & y" := (Op (Land (TWord 7)) (Pair (Op (Cast _ (TWord 7)) (Var x)) y)). -Notation "x & y" := (Op (Land (TWord 7)) (Pair (Op (Cast _ (TWord 7)) (Var x)) (Var y))). -Notation "x & y" := (Op (Land (TWord 7)) (Pair x (Op (Cast _ (TWord 7)) y))). -Notation "x & y" := (Op (Land (TWord 7)) (Pair x (Op (Cast _ (TWord 7)) (Var y)))). -Notation "x & y" := (Op (Land (TWord 7)) (Pair (Var x) (Op (Cast _ (TWord 7)) y))). -Notation "x & y" := (Op (Land (TWord 7)) (Pair (Var x) (Op (Cast _ (TWord 7)) (Var y)))). +Notation "'int'" := (Tbase (TWord 0)). +Notation "'int'" := (Tbase (TWord 1)). +Notation "'int'" := (Tbase (TWord 2)). +Notation "'int'" := (Tbase (TWord 3)). +Notation "'int'" := (Tbase (TWord 4)). +Notation "'int'" := (Tbase (TWord 5)). +Notation "'long'" := (Tbase (TWord 6)). +Notation "'uint128_t'" := (Tbase (TWord 7)). + +Notation "x * y" := (Op (Mul _ _ _) (Pair x y)). +Notation "x * y" := (Op (Mul _ _ _) (Pair x (Var y))). +Notation "x * y" := (Op (Mul _ _ _) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul _ _ _) (Pair (Var x) (Var y))). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 0)) (Pair x y)) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 0) (TWord _) (TWord 0)) (Pair x y)) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 0) (TWord 0)) (Pair x y)) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 0) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 0) (TWord 0)) (Pair x (Var y))) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) y)) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 0) (TWord 0) (TWord 0)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 0) (TWord 0) (TWord 0)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 1)) (Pair x y)) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 1) (TWord _) (TWord 1)) (Pair x y)) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 1) (TWord 1)) (Pair x y)) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 1) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 1) (TWord 1)) (Pair x (Var y))) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) y)) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 1) (TWord 1) (TWord 1)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 1) (TWord 1) (TWord 1)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 2)) (Pair x y)) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 2) (TWord _) (TWord 2)) (Pair x y)) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 2) (TWord 2)) (Pair x y)) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 2) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 2) (TWord 2)) (Pair x (Var y))) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) y)) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 2) (TWord 2) (TWord 2)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 2) (TWord 2) (TWord 2)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 3)) (Pair x y)) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 3) (TWord _) (TWord 3)) (Pair x y)) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 3) (TWord 3)) (Pair x y)) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 3) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 3) (TWord 3)) (Pair x (Var y))) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) y)) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 3) (TWord 3) (TWord 3)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 3) (TWord 3) (TWord 3)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 4)) (Pair x y)) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 4) (TWord _) (TWord 4)) (Pair x y)) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 4) (TWord 4)) (Pair x y)) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 4) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 4) (TWord 4)) (Pair x (Var y))) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) y)) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 4) (TWord 4) (TWord 4)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 4) (TWord 4) (TWord 4)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 5)) (Pair x y)) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 5) (TWord _) (TWord 5)) (Pair x y)) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 5) (TWord 5)) (Pair x y)) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 5) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 5) (TWord 5)) (Pair x (Var y))) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) y)) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 5) (TWord 5) (TWord 5)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 5) (TWord 5) (TWord 5)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))). +Notation "'(long)' x * '(long)' y" := (Op (Mul (TWord _) (TWord _) (TWord 6)) (Pair x y)) (at level 40). +Notation "'(long)' x * '(long)' y" := (Op (Mul (TWord _) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 40). +Notation "'(long)' x * '(long)' y" := (Op (Mul (TWord _) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 40). +Notation "'(long)' x * '(long)' y" := (Op (Mul (TWord _) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(long)' y" := (Op (Mul (TWord 6) (TWord _) (TWord 6)) (Pair x y)) (at level 40). +Notation "'(long)' x * y" := (Op (Mul (TWord _) (TWord 6) (TWord 6)) (Pair x y)) (at level 40). +Notation "x * '(long)' y" := (Op (Mul (TWord 6) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 40). +Notation "'(long)' x * y" := (Op (Mul (TWord _) (TWord 6) (TWord 6)) (Pair x (Var y))) (at level 40). +Notation "x * '(long)' y" := (Op (Mul (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 40). +Notation "'(long)' x * y" := (Op (Mul (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) y)) (at level 40). +Notation "x * '(long)' y" := (Op (Mul (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(long)' x * y" := (Op (Mul (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 6) (TWord 6) (TWord 6)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 6) (TWord 6) (TWord 6)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))). +Notation "'(uint128_t)' x * '(uint128_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 7)) (Pair x y)) (at level 40). +Notation "'(uint128_t)' x * '(uint128_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 40). +Notation "'(uint128_t)' x * '(uint128_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 40). +Notation "'(uint128_t)' x * '(uint128_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(uint128_t)' y" := (Op (Mul (TWord 7) (TWord _) (TWord 7)) (Pair x y)) (at level 40). +Notation "'(uint128_t)' x * y" := (Op (Mul (TWord _) (TWord 7) (TWord 7)) (Pair x y)) (at level 40). +Notation "x * '(uint128_t)' y" := (Op (Mul (TWord 7) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 40). +Notation "'(uint128_t)' x * y" := (Op (Mul (TWord _) (TWord 7) (TWord 7)) (Pair x (Var y))) (at level 40). +Notation "x * '(uint128_t)' y" := (Op (Mul (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 40). +Notation "'(uint128_t)' x * y" := (Op (Mul (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) y)) (at level 40). +Notation "x * '(uint128_t)' y" := (Op (Mul (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint128_t)' x * y" := (Op (Mul (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "x + y" := (Op (Add _ _ _) (Pair x y)). +Notation "x + y" := (Op (Add _ _ _) (Pair x (Var y))). +Notation "x + y" := (Op (Add _ _ _) (Pair (Var x) y)). +Notation "x + y" := (Op (Add _ _ _) (Pair (Var x) (Var y))). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 0)) (Pair x y)) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 0) (TWord _) (TWord 0)) (Pair x y)) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 0) (TWord 0)) (Pair x y)) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 0) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 0) (TWord 0)) (Pair x (Var y))) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) y)) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 0) (TWord 0) (TWord 0)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 0) (TWord 0) (TWord 0)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 1)) (Pair x y)) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 1) (TWord _) (TWord 1)) (Pair x y)) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 1) (TWord 1)) (Pair x y)) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 1) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 1) (TWord 1)) (Pair x (Var y))) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) y)) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 1) (TWord 1) (TWord 1)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 1) (TWord 1) (TWord 1)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 2)) (Pair x y)) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 2) (TWord _) (TWord 2)) (Pair x y)) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 2) (TWord 2)) (Pair x y)) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 2) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 2) (TWord 2)) (Pair x (Var y))) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) y)) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 2) (TWord 2) (TWord 2)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 2) (TWord 2) (TWord 2)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 3)) (Pair x y)) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 3) (TWord _) (TWord 3)) (Pair x y)) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 3) (TWord 3)) (Pair x y)) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 3) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 3) (TWord 3)) (Pair x (Var y))) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) y)) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 3) (TWord 3) (TWord 3)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 3) (TWord 3) (TWord 3)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 4)) (Pair x y)) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 4) (TWord _) (TWord 4)) (Pair x y)) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 4) (TWord 4)) (Pair x y)) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 4) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 4) (TWord 4)) (Pair x (Var y))) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) y)) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 4) (TWord 4) (TWord 4)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 4) (TWord 4) (TWord 4)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 5)) (Pair x y)) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 5) (TWord _) (TWord 5)) (Pair x y)) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 5) (TWord 5)) (Pair x y)) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 5) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 5) (TWord 5)) (Pair x (Var y))) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) y)) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 5) (TWord 5) (TWord 5)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 5) (TWord 5) (TWord 5)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))). +Notation "'(long)' x + '(long)' y" := (Op (Add (TWord _) (TWord _) (TWord 6)) (Pair x y)) (at level 50). +Notation "'(long)' x + '(long)' y" := (Op (Add (TWord _) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 50). +Notation "'(long)' x + '(long)' y" := (Op (Add (TWord _) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 50). +Notation "'(long)' x + '(long)' y" := (Op (Add (TWord _) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(long)' y" := (Op (Add (TWord 6) (TWord _) (TWord 6)) (Pair x y)) (at level 50). +Notation "'(long)' x + y" := (Op (Add (TWord _) (TWord 6) (TWord 6)) (Pair x y)) (at level 50). +Notation "x + '(long)' y" := (Op (Add (TWord 6) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 50). +Notation "'(long)' x + y" := (Op (Add (TWord _) (TWord 6) (TWord 6)) (Pair x (Var y))) (at level 50). +Notation "x + '(long)' y" := (Op (Add (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 50). +Notation "'(long)' x + y" := (Op (Add (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) y)) (at level 50). +Notation "x + '(long)' y" := (Op (Add (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(long)' x + y" := (Op (Add (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 6) (TWord 6) (TWord 6)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 6) (TWord 6) (TWord 6)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))). +Notation "'(uint128_t)' x + '(uint128_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 7)) (Pair x y)) (at level 50). +Notation "'(uint128_t)' x + '(uint128_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 50). +Notation "'(uint128_t)' x + '(uint128_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 50). +Notation "'(uint128_t)' x + '(uint128_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(uint128_t)' y" := (Op (Add (TWord 7) (TWord _) (TWord 7)) (Pair x y)) (at level 50). +Notation "'(uint128_t)' x + y" := (Op (Add (TWord _) (TWord 7) (TWord 7)) (Pair x y)) (at level 50). +Notation "x + '(uint128_t)' y" := (Op (Add (TWord 7) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 50). +Notation "'(uint128_t)' x + y" := (Op (Add (TWord _) (TWord 7) (TWord 7)) (Pair x (Var y))) (at level 50). +Notation "x + '(uint128_t)' y" := (Op (Add (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 50). +Notation "'(uint128_t)' x + y" := (Op (Add (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) y)) (at level 50). +Notation "x + '(uint128_t)' y" := (Op (Add (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint128_t)' x + y" := (Op (Add (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "x - y" := (Op (Sub _ _ _) (Pair x y)). +Notation "x - y" := (Op (Sub _ _ _) (Pair x (Var y))). +Notation "x - y" := (Op (Sub _ _ _) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub _ _ _) (Pair (Var x) (Var y))). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 0)) (Pair x y)) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 0) (TWord _) (TWord 0)) (Pair x y)) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 0) (TWord 0)) (Pair x y)) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 0) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 0) (TWord 0)) (Pair x (Var y))) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) y)) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 0) (TWord 0) (TWord 0)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 0) (TWord 0) (TWord 0)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 1)) (Pair x y)) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 1) (TWord _) (TWord 1)) (Pair x y)) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 1) (TWord 1)) (Pair x y)) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 1) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 1) (TWord 1)) (Pair x (Var y))) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) y)) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 1) (TWord 1) (TWord 1)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 1) (TWord 1) (TWord 1)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 2)) (Pair x y)) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 2) (TWord _) (TWord 2)) (Pair x y)) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 2) (TWord 2)) (Pair x y)) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 2) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 2) (TWord 2)) (Pair x (Var y))) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) y)) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 2) (TWord 2) (TWord 2)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 2) (TWord 2) (TWord 2)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 3)) (Pair x y)) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 3) (TWord _) (TWord 3)) (Pair x y)) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 3) (TWord 3)) (Pair x y)) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 3) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 3) (TWord 3)) (Pair x (Var y))) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) y)) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 3) (TWord 3) (TWord 3)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 3) (TWord 3) (TWord 3)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 4)) (Pair x y)) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 4) (TWord _) (TWord 4)) (Pair x y)) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 4) (TWord 4)) (Pair x y)) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 4) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 4) (TWord 4)) (Pair x (Var y))) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) y)) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 4) (TWord 4) (TWord 4)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 4) (TWord 4) (TWord 4)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 5)) (Pair x y)) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 5) (TWord _) (TWord 5)) (Pair x y)) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 5) (TWord 5)) (Pair x y)) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 5) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 5) (TWord 5)) (Pair x (Var y))) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) y)) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 5) (TWord 5) (TWord 5)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 5) (TWord 5) (TWord 5)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))). +Notation "'(long)' x - '(long)' y" := (Op (Sub (TWord _) (TWord _) (TWord 6)) (Pair x y)) (at level 50). +Notation "'(long)' x - '(long)' y" := (Op (Sub (TWord _) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 50). +Notation "'(long)' x - '(long)' y" := (Op (Sub (TWord _) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 50). +Notation "'(long)' x - '(long)' y" := (Op (Sub (TWord _) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(long)' y" := (Op (Sub (TWord 6) (TWord _) (TWord 6)) (Pair x y)) (at level 50). +Notation "'(long)' x - y" := (Op (Sub (TWord _) (TWord 6) (TWord 6)) (Pair x y)) (at level 50). +Notation "x - '(long)' y" := (Op (Sub (TWord 6) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 50). +Notation "'(long)' x - y" := (Op (Sub (TWord _) (TWord 6) (TWord 6)) (Pair x (Var y))) (at level 50). +Notation "x - '(long)' y" := (Op (Sub (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 50). +Notation "'(long)' x - y" := (Op (Sub (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) y)) (at level 50). +Notation "x - '(long)' y" := (Op (Sub (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(long)' x - y" := (Op (Sub (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 6) (TWord 6) (TWord 6)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 6) (TWord 6) (TWord 6)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))). +Notation "'(uint128_t)' x - '(uint128_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 7)) (Pair x y)) (at level 50). +Notation "'(uint128_t)' x - '(uint128_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 50). +Notation "'(uint128_t)' x - '(uint128_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 50). +Notation "'(uint128_t)' x - '(uint128_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(uint128_t)' y" := (Op (Sub (TWord 7) (TWord _) (TWord 7)) (Pair x y)) (at level 50). +Notation "'(uint128_t)' x - y" := (Op (Sub (TWord _) (TWord 7) (TWord 7)) (Pair x y)) (at level 50). +Notation "x - '(uint128_t)' y" := (Op (Sub (TWord 7) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 50). +Notation "'(uint128_t)' x - y" := (Op (Sub (TWord _) (TWord 7) (TWord 7)) (Pair x (Var y))) (at level 50). +Notation "x - '(uint128_t)' y" := (Op (Sub (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 50). +Notation "'(uint128_t)' x - y" := (Op (Sub (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) y)) (at level 50). +Notation "x - '(uint128_t)' y" := (Op (Sub (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint128_t)' x - y" := (Op (Sub (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "x & y" := (Op (Land _ _ _) (Pair x y)). +Notation "x & y" := (Op (Land _ _ _) (Pair x (Var y))). +Notation "x & y" := (Op (Land _ _ _) (Pair (Var x) y)). +Notation "x & y" := (Op (Land _ _ _) (Pair (Var x) (Var y))). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 0)) (Pair x y)) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 0) (TWord _) (TWord 0)) (Pair x y)) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 0) (TWord 0)) (Pair x y)) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 0) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 0) (TWord 0)) (Pair x (Var y))) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) y)) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 0) (TWord 0) (TWord 0)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 0) (TWord 0) (TWord 0)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 1)) (Pair x y)) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 1) (TWord _) (TWord 1)) (Pair x y)) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 1) (TWord 1)) (Pair x y)) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 1) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 1) (TWord 1)) (Pair x (Var y))) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) y)) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 1) (TWord 1) (TWord 1)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 1) (TWord 1) (TWord 1)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 2)) (Pair x y)) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 2) (TWord _) (TWord 2)) (Pair x y)) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 2) (TWord 2)) (Pair x y)) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 2) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 2) (TWord 2)) (Pair x (Var y))) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) y)) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 2) (TWord 2) (TWord 2)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 2) (TWord 2) (TWord 2)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 3)) (Pair x y)) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 3) (TWord _) (TWord 3)) (Pair x y)) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 3) (TWord 3)) (Pair x y)) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 3) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 3) (TWord 3)) (Pair x (Var y))) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) y)) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 3) (TWord 3) (TWord 3)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 3) (TWord 3) (TWord 3)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 4)) (Pair x y)) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 4) (TWord _) (TWord 4)) (Pair x y)) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 4) (TWord 4)) (Pair x y)) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 4) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 4) (TWord 4)) (Pair x (Var y))) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) y)) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 4) (TWord 4) (TWord 4)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 4) (TWord 4) (TWord 4)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 5)) (Pair x y)) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 5) (TWord _) (TWord 5)) (Pair x y)) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 5) (TWord 5)) (Pair x y)) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 5) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 5) (TWord 5)) (Pair x (Var y))) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) y)) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 5) (TWord 5) (TWord 5)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 5) (TWord 5) (TWord 5)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))). +Notation "'(long)' x & '(long)' y" := (Op (Land (TWord _) (TWord _) (TWord 6)) (Pair x y)) (at level 40). +Notation "'(long)' x & '(long)' y" := (Op (Land (TWord _) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 40). +Notation "'(long)' x & '(long)' y" := (Op (Land (TWord _) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 40). +Notation "'(long)' x & '(long)' y" := (Op (Land (TWord _) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(long)' y" := (Op (Land (TWord 6) (TWord _) (TWord 6)) (Pair x y)) (at level 40). +Notation "'(long)' x & y" := (Op (Land (TWord _) (TWord 6) (TWord 6)) (Pair x y)) (at level 40). +Notation "x & '(long)' y" := (Op (Land (TWord 6) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 40). +Notation "'(long)' x & y" := (Op (Land (TWord _) (TWord 6) (TWord 6)) (Pair x (Var y))) (at level 40). +Notation "x & '(long)' y" := (Op (Land (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 40). +Notation "'(long)' x & y" := (Op (Land (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) y)) (at level 40). +Notation "x & '(long)' y" := (Op (Land (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(long)' x & y" := (Op (Land (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 6) (TWord 6) (TWord 6)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 6) (TWord 6) (TWord 6)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))). +Notation "'(uint128_t)' x & '(uint128_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 7)) (Pair x y)) (at level 40). +Notation "'(uint128_t)' x & '(uint128_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 40). +Notation "'(uint128_t)' x & '(uint128_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 40). +Notation "'(uint128_t)' x & '(uint128_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(uint128_t)' y" := (Op (Land (TWord 7) (TWord _) (TWord 7)) (Pair x y)) (at level 40). +Notation "'(uint128_t)' x & y" := (Op (Land (TWord _) (TWord 7) (TWord 7)) (Pair x y)) (at level 40). +Notation "x & '(uint128_t)' y" := (Op (Land (TWord 7) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 40). +Notation "'(uint128_t)' x & y" := (Op (Land (TWord _) (TWord 7) (TWord 7)) (Pair x (Var y))) (at level 40). +Notation "x & '(uint128_t)' y" := (Op (Land (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 40). +Notation "'(uint128_t)' x & y" := (Op (Land (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) y)) (at level 40). +Notation "x & '(uint128_t)' y" := (Op (Land (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint128_t)' x & y" := (Op (Land (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "x << y" := (Op (Shl _ _ _) (Pair x y)). +Notation "x << y" := (Op (Shl _ _ _) (Pair x (Var y))). +Notation "x << y" := (Op (Shl _ _ _) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl _ _ _) (Pair (Var x) (Var y))). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 0)) (Pair x y)) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 0) (TWord _) (TWord 0)) (Pair x y)) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 0) (TWord 0)) (Pair x y)) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 0) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 0) (TWord 0)) (Pair x (Var y))) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) y)) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 0) (TWord 0) (TWord 0)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 0) (TWord 0) (TWord 0)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 1)) (Pair x y)) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 1) (TWord _) (TWord 1)) (Pair x y)) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 1) (TWord 1)) (Pair x y)) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 1) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 1) (TWord 1)) (Pair x (Var y))) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) y)) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 1) (TWord 1) (TWord 1)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 1) (TWord 1) (TWord 1)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 2)) (Pair x y)) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 2) (TWord _) (TWord 2)) (Pair x y)) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 2) (TWord 2)) (Pair x y)) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 2) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 2) (TWord 2)) (Pair x (Var y))) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) y)) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 2) (TWord 2) (TWord 2)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 2) (TWord 2) (TWord 2)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 3)) (Pair x y)) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 3) (TWord _) (TWord 3)) (Pair x y)) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 3) (TWord 3)) (Pair x y)) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 3) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 3) (TWord 3)) (Pair x (Var y))) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) y)) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 3) (TWord 3) (TWord 3)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 3) (TWord 3) (TWord 3)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 4)) (Pair x y)) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 4) (TWord _) (TWord 4)) (Pair x y)) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 4) (TWord 4)) (Pair x y)) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 4) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 4) (TWord 4)) (Pair x (Var y))) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) y)) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 4) (TWord 4) (TWord 4)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 4) (TWord 4) (TWord 4)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 5)) (Pair x y)) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 5) (TWord _) (TWord 5)) (Pair x y)) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 5) (TWord 5)) (Pair x y)) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 5) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 5) (TWord 5)) (Pair x (Var y))) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) y)) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 5) (TWord 5) (TWord 5)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 5) (TWord 5) (TWord 5)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))). +Notation "'(long)' x << '(long)' y" := (Op (Shl (TWord _) (TWord _) (TWord 6)) (Pair x y)) (at level 30). +Notation "'(long)' x << '(long)' y" := (Op (Shl (TWord _) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 30). +Notation "'(long)' x << '(long)' y" := (Op (Shl (TWord _) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 30). +Notation "'(long)' x << '(long)' y" := (Op (Shl (TWord _) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(long)' y" := (Op (Shl (TWord 6) (TWord _) (TWord 6)) (Pair x y)) (at level 30). +Notation "'(long)' x << y" := (Op (Shl (TWord _) (TWord 6) (TWord 6)) (Pair x y)) (at level 30). +Notation "x << '(long)' y" := (Op (Shl (TWord 6) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 30). +Notation "'(long)' x << y" := (Op (Shl (TWord _) (TWord 6) (TWord 6)) (Pair x (Var y))) (at level 30). +Notation "x << '(long)' y" := (Op (Shl (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 30). +Notation "'(long)' x << y" := (Op (Shl (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) y)) (at level 30). +Notation "x << '(long)' y" := (Op (Shl (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(long)' x << y" := (Op (Shl (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 6) (TWord 6) (TWord 6)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 6) (TWord 6) (TWord 6)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))). +Notation "'(uint128_t)' x << '(uint128_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 7)) (Pair x y)) (at level 30). +Notation "'(uint128_t)' x << '(uint128_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 30). +Notation "'(uint128_t)' x << '(uint128_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 30). +Notation "'(uint128_t)' x << '(uint128_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(uint128_t)' y" := (Op (Shl (TWord 7) (TWord _) (TWord 7)) (Pair x y)) (at level 30). +Notation "'(uint128_t)' x << y" := (Op (Shl (TWord _) (TWord 7) (TWord 7)) (Pair x y)) (at level 30). +Notation "x << '(uint128_t)' y" := (Op (Shl (TWord 7) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 30). +Notation "'(uint128_t)' x << y" := (Op (Shl (TWord _) (TWord 7) (TWord 7)) (Pair x (Var y))) (at level 30). +Notation "x << '(uint128_t)' y" := (Op (Shl (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 30). +Notation "'(uint128_t)' x << y" := (Op (Shl (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) y)) (at level 30). +Notation "x << '(uint128_t)' y" := (Op (Shl (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint128_t)' x << y" := (Op (Shl (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "x >> y" := (Op (Shr _ _ _) (Pair x y)). +Notation "x >> y" := (Op (Shr _ _ _) (Pair x (Var y))). +Notation "x >> y" := (Op (Shr _ _ _) (Pair (Var x) y)). +Notation "x >> y" := (Op (Shr _ _ _) (Pair (Var x) (Var y))). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 0)) (Pair x y)) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 1)) (Pair x y)) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 2)) (Pair x y)) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 3)) (Pair x y)) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 4)) (Pair x y)) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 5)) (Pair x y)) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(long)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 6)) (Pair x y)) (at level 30). +Notation "'(long)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 30). +Notation "'(long)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 30). +Notation "'(long)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint128_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 7)) (Pair x y)) (at level 30). +Notation "'(uint128_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 30). +Notation "'(uint128_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 30). +Notation "'(uint128_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 30). Notation Return x := (Var x). Notation Java_like := (Expr base_type op _). |