diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-03-30 16:38:15 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-03-30 16:38:41 -0400 |
| commit | 7d70da13d3d44c6eed92dfd490138d7a05120208 (patch) | |
| tree | a5e7dd19b4cbee7be87fc7fbae3190b81b18bb2f /src/Reflection | |
| parent | 01874b3bfe5d9788d7c3dfd2432993e99c4595da (diff) | |
Revert "Update CNotations, JavaNotations"
This reverts commit 16d3eb50638fc280b790aff9cdaa6d28cbb42c8a.
I forgot that I hadn't merged the changes to Z.Syntax.op yet.
Diffstat (limited to 'src/Reflection')
| -rw-r--r-- | src/Reflection/Z/CNotations.v | 894 | ||||
| -rw-r--r-- | src/Reflection/Z/JavaNotations.v | 869 |
2 files changed, 250 insertions, 1513 deletions
diff --git a/src/Reflection/Z/CNotations.v b/src/Reflection/Z/CNotations.v index 74b945222..0b3bfa161 100644 --- a/src/Reflection/Z/CNotations.v +++ b/src/Reflection/Z/CNotations.v @@ -4,768 +4,152 @@ 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. -(* python: -<< -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 "'bool'" := (Tbase (TWord 0)). +(*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 "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 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)) +>> *) +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 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 d0e32610b..96a04f5fc 100644 --- a/src/Reflection/Z/JavaNotations.v +++ b/src/Reflection/Z/JavaNotations.v @@ -4,6 +4,9 @@ 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). @@ -11,8 +14,15 @@ 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. -(* ??? Did I get M32 wrong? *) -(*Notation "'(int)' x" := (Op (Cast _ (TWord 0)) x). +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). Notation "'(int)' x" := (Op (Cast _ (TWord 1)) x). Notation "'(int)' x" := (Op (Cast _ (TWord 2)) x). Notation "'(int)' x" := (Op (Cast _ (TWord 3)) x). @@ -27,764 +37,107 @@ 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 "'(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: << -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 _).') +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)) >> *) -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 "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 Return x := (Var x). Notation Java_like := (Expr base_type op _). |