diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-04-06 22:53:07 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-04-06 22:53:07 -0400 |
| commit | c9fc5a3cdf1f5ea2d104c150c30d1b1a6ac64239 (patch) | |
| tree | db7187f6984acff324ca468e7b33d9285806a1eb /src/Compilers/Z/JavaNotations.v | |
| parent | 21198245dab432d3c0ba2bb8a02254e7d0594382 (diff) | |
rename-everything
Diffstat (limited to 'src/Compilers/Z/JavaNotations.v')
| -rw-r--r-- | src/Compilers/Z/JavaNotations.v | 792 |
1 files changed, 792 insertions, 0 deletions
diff --git a/src/Compilers/Z/JavaNotations.v b/src/Compilers/Z/JavaNotations.v new file mode 100644 index 000000000..bab120b0a --- /dev/null +++ b/src/Compilers/Z/JavaNotations.v @@ -0,0 +1,792 @@ +Require Export Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.Z.Syntax. +Require Export Crypto.Compilers.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 "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). + +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)' x" := (Op (Cast _ (TWord 1)) x). +Notation "'(int)' x" := (Op (Cast _ (TWord 2)) x). +Notation "'(int)' x" := (Op (Cast _ (TWord 3)) x). +Notation "'(int)' x" := (Op (Cast _ (TWord 4)) x). +Notation "'(int)' x" := (Op (Cast _ (TWord 5)) x). +Notation "'M32' & x" := (Op (Cast _ (TWord 6)) x). +Notation "'(uint128_t)' x" := (Op (Cast _ (TWord 7)) x). +Notation "'(int)' x" := (Op (Cast _ (TWord 0)) (Var x)). +Notation "'(int)' x" := (Op (Cast _ (TWord 1)) (Var x)). +Notation "'(int)' x" := (Op (Cast _ (TWord 2)) (Var x)). +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)).*) +(* 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('Notation ℤ := (Tbase TZ).') +print('') +cast_pat = "'(%s)' %s" +for opn, op, lvl in (('*', 'Mul', 40), ('+', 'Add', 50), ('-', 'Sub', 50), ('&', 'Land', 40), ('<<', 'Shl', 30)): + for v1 in (False, True): + for v2 in (False, True): + lhs = ('x' if not v1 else '(Var x)') + rhs = ('y' if not v2 else '(Var y)') + print('Notation "x %s y" := (Op (%s _ _ _) (Pair %s %s)).' % (opn, op, lhs, rhs)) + for lgwordsz in range(0, len(types)): + for v1 in (False, True): + for v2 in (False, True): + lhs = ('x' if not v1 else '(Var x)') + rhs = ('y' if not v2 else '(Var y)') + print('Notation "%s %s %s" := (Op (%s (TWord _) (TWord _) (TWord %d)) (Pair %s %s)) (at level %d).' + % (cast_pat % (types[lgwordsz], 'x'), opn, cast_pat % (types[lgwordsz], 'y'), + op, lgwordsz, lhs, rhs, lvl)) + for v1 in (False, True): + for v2 in (False, True): + lhs = ('x' if not v1 else '(Var x)') + rhs = ('y' if not v2 else '(Var y)') + print('Notation "%s %s %s" := (Op (%s (TWord %d) (TWord _) (TWord %d)) (Pair %s %s)) (at level %d).' + % ('x', opn, cast_pat % (types[lgwordsz], 'y'), + op, lgwordsz, lgwordsz, lhs, rhs, lvl)) + print('Notation "%s %s %s" := (Op (%s (TWord _) (TWord %d) (TWord %d)) (Pair %s %s)) (at level %d).' + % (cast_pat % (types[lgwordsz], 'x'), opn, 'y', + op, lgwordsz, lgwordsz, lhs, rhs, lvl)) + for v1 in (False, True): + for v2 in (False, True): + lhs = ('x' if not v1 else '(Var x)') + rhs = ('y' if not v2 else '(Var y)') + print('Notation "x %s y" := (Op (%s (TWord %d) (TWord %d) (TWord %d)) (Pair %s %s)).' + % (opn, op, lgwordsz, lgwordsz, lgwordsz, lhs, rhs)) +for opn, op, lvl in (('>>', 'Shr', 30),): + for v1 in (False, True): + for v2 in (False, True): + lhs = ('x' if not v1 else '(Var x)') + rhs = ('y' if not v2 else '(Var y)') + print('Notation "x %s y" := (Op (%s _ _ _) (Pair %s %s)).' % (opn, op, lhs, rhs)) + for lgwordsz in range(0, len(types)): + for v1 in (False, True): + for v2 in (False, True): + lhs = ('x' if not v1 else '(Var x)') + rhs = ('y' if not v2 else '(Var y)') + print('Notation "\'(%s)\' ( x %s y )" := (Op (%s (TWord _) (TWord _) (TWord %d)) (Pair %s %s)) (at level %d).' + % (types[lgwordsz], opn, op, lgwordsz, lhs, rhs, lvl)) +print('Notation Return x := (Var x).') +print('Notation Java_like := (Expr base_type op _).') +>> *) +Notation "'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 ℤ := (Tbase TZ). + +Notation "x * y" := (Op (Mul _ _ _) (Pair x y)). +Notation "x * y" := (Op (Mul _ _ _) (Pair x (Var y))). +Notation "x * y" := (Op (Mul _ _ _) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul _ _ _) (Pair (Var x) (Var y))). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 0)) (Pair x y)) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 0) (TWord _) (TWord 0)) (Pair x y)) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 0) (TWord 0)) (Pair x y)) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 0) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 0) (TWord 0)) (Pair x (Var y))) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) y)) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 0) (TWord 0) (TWord 0)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 0) (TWord 0) (TWord 0)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 1)) (Pair x y)) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 1) (TWord _) (TWord 1)) (Pair x y)) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 1) (TWord 1)) (Pair x y)) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 1) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 1) (TWord 1)) (Pair x (Var y))) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) y)) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 1) (TWord 1) (TWord 1)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 1) (TWord 1) (TWord 1)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 2)) (Pair x y)) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 2) (TWord _) (TWord 2)) (Pair x y)) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 2) (TWord 2)) (Pair x y)) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 2) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 2) (TWord 2)) (Pair x (Var y))) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) y)) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 2) (TWord 2) (TWord 2)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 2) (TWord 2) (TWord 2)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 3)) (Pair x y)) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 3) (TWord _) (TWord 3)) (Pair x y)) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 3) (TWord 3)) (Pair x y)) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 3) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 3) (TWord 3)) (Pair x (Var y))) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) y)) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 3) (TWord 3) (TWord 3)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 3) (TWord 3) (TWord 3)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 4)) (Pair x y)) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 4) (TWord _) (TWord 4)) (Pair x y)) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 4) (TWord 4)) (Pair x y)) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 4) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 4) (TWord 4)) (Pair x (Var y))) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) y)) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 4) (TWord 4) (TWord 4)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 4) (TWord 4) (TWord 4)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 5)) (Pair x y)) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x * '(int)' y" := (Op (Mul (TWord _) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 5) (TWord _) (TWord 5)) (Pair x y)) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 5) (TWord 5)) (Pair x y)) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 5) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 5) (TWord 5)) (Pair x (Var y))) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) y)) (at level 40). +Notation "x * '(int)' y" := (Op (Mul (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(int)' x * y" := (Op (Mul (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 5) (TWord 5) (TWord 5)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 5) (TWord 5) (TWord 5)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))). +Notation "'(long)' x * '(long)' y" := (Op (Mul (TWord _) (TWord _) (TWord 6)) (Pair x y)) (at level 40). +Notation "'(long)' x * '(long)' y" := (Op (Mul (TWord _) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 40). +Notation "'(long)' x * '(long)' y" := (Op (Mul (TWord _) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 40). +Notation "'(long)' x * '(long)' y" := (Op (Mul (TWord _) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(long)' y" := (Op (Mul (TWord 6) (TWord _) (TWord 6)) (Pair x y)) (at level 40). +Notation "'(long)' x * y" := (Op (Mul (TWord _) (TWord 6) (TWord 6)) (Pair x y)) (at level 40). +Notation "x * '(long)' y" := (Op (Mul (TWord 6) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 40). +Notation "'(long)' x * y" := (Op (Mul (TWord _) (TWord 6) (TWord 6)) (Pair x (Var y))) (at level 40). +Notation "x * '(long)' y" := (Op (Mul (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 40). +Notation "'(long)' x * y" := (Op (Mul (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) y)) (at level 40). +Notation "x * '(long)' y" := (Op (Mul (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(long)' x * y" := (Op (Mul (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 6) (TWord 6) (TWord 6)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 6) (TWord 6) (TWord 6)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))). +Notation "'(uint128_t)' x * '(uint128_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 7)) (Pair x y)) (at level 40). +Notation "'(uint128_t)' x * '(uint128_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 40). +Notation "'(uint128_t)' x * '(uint128_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 40). +Notation "'(uint128_t)' x * '(uint128_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(uint128_t)' y" := (Op (Mul (TWord 7) (TWord _) (TWord 7)) (Pair x y)) (at level 40). +Notation "'(uint128_t)' x * y" := (Op (Mul (TWord _) (TWord 7) (TWord 7)) (Pair x y)) (at level 40). +Notation "x * '(uint128_t)' y" := (Op (Mul (TWord 7) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 40). +Notation "'(uint128_t)' x * y" := (Op (Mul (TWord _) (TWord 7) (TWord 7)) (Pair x (Var y))) (at level 40). +Notation "x * '(uint128_t)' y" := (Op (Mul (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 40). +Notation "'(uint128_t)' x * y" := (Op (Mul (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) y)) (at level 40). +Notation "x * '(uint128_t)' y" := (Op (Mul (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint128_t)' x * y" := (Op (Mul (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "x + y" := (Op (Add _ _ _) (Pair x y)). +Notation "x + y" := (Op (Add _ _ _) (Pair x (Var y))). +Notation "x + y" := (Op (Add _ _ _) (Pair (Var x) y)). +Notation "x + y" := (Op (Add _ _ _) (Pair (Var x) (Var y))). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 0)) (Pair x y)) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 0) (TWord _) (TWord 0)) (Pair x y)) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 0) (TWord 0)) (Pair x y)) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 0) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 0) (TWord 0)) (Pair x (Var y))) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) y)) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 0) (TWord 0) (TWord 0)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 0) (TWord 0) (TWord 0)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 1)) (Pair x y)) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 1) (TWord _) (TWord 1)) (Pair x y)) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 1) (TWord 1)) (Pair x y)) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 1) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 1) (TWord 1)) (Pair x (Var y))) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) y)) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 1) (TWord 1) (TWord 1)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 1) (TWord 1) (TWord 1)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 2)) (Pair x y)) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 2) (TWord _) (TWord 2)) (Pair x y)) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 2) (TWord 2)) (Pair x y)) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 2) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 2) (TWord 2)) (Pair x (Var y))) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) y)) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 2) (TWord 2) (TWord 2)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 2) (TWord 2) (TWord 2)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 3)) (Pair x y)) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 3) (TWord _) (TWord 3)) (Pair x y)) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 3) (TWord 3)) (Pair x y)) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 3) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 3) (TWord 3)) (Pair x (Var y))) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) y)) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 3) (TWord 3) (TWord 3)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 3) (TWord 3) (TWord 3)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 4)) (Pair x y)) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 4) (TWord _) (TWord 4)) (Pair x y)) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 4) (TWord 4)) (Pair x y)) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 4) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 4) (TWord 4)) (Pair x (Var y))) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) y)) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 4) (TWord 4) (TWord 4)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 4) (TWord 4) (TWord 4)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 5)) (Pair x y)) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x + '(int)' y" := (Op (Add (TWord _) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 5) (TWord _) (TWord 5)) (Pair x y)) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 5) (TWord 5)) (Pair x y)) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 5) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 5) (TWord 5)) (Pair x (Var y))) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) y)) (at level 50). +Notation "x + '(int)' y" := (Op (Add (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(int)' x + y" := (Op (Add (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 5) (TWord 5) (TWord 5)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 5) (TWord 5) (TWord 5)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))). +Notation "'(long)' x + '(long)' y" := (Op (Add (TWord _) (TWord _) (TWord 6)) (Pair x y)) (at level 50). +Notation "'(long)' x + '(long)' y" := (Op (Add (TWord _) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 50). +Notation "'(long)' x + '(long)' y" := (Op (Add (TWord _) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 50). +Notation "'(long)' x + '(long)' y" := (Op (Add (TWord _) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(long)' y" := (Op (Add (TWord 6) (TWord _) (TWord 6)) (Pair x y)) (at level 50). +Notation "'(long)' x + y" := (Op (Add (TWord _) (TWord 6) (TWord 6)) (Pair x y)) (at level 50). +Notation "x + '(long)' y" := (Op (Add (TWord 6) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 50). +Notation "'(long)' x + y" := (Op (Add (TWord _) (TWord 6) (TWord 6)) (Pair x (Var y))) (at level 50). +Notation "x + '(long)' y" := (Op (Add (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 50). +Notation "'(long)' x + y" := (Op (Add (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) y)) (at level 50). +Notation "x + '(long)' y" := (Op (Add (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(long)' x + y" := (Op (Add (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 6) (TWord 6) (TWord 6)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 6) (TWord 6) (TWord 6)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))). +Notation "'(uint128_t)' x + '(uint128_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 7)) (Pair x y)) (at level 50). +Notation "'(uint128_t)' x + '(uint128_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 50). +Notation "'(uint128_t)' x + '(uint128_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 50). +Notation "'(uint128_t)' x + '(uint128_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(uint128_t)' y" := (Op (Add (TWord 7) (TWord _) (TWord 7)) (Pair x y)) (at level 50). +Notation "'(uint128_t)' x + y" := (Op (Add (TWord _) (TWord 7) (TWord 7)) (Pair x y)) (at level 50). +Notation "x + '(uint128_t)' y" := (Op (Add (TWord 7) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 50). +Notation "'(uint128_t)' x + y" := (Op (Add (TWord _) (TWord 7) (TWord 7)) (Pair x (Var y))) (at level 50). +Notation "x + '(uint128_t)' y" := (Op (Add (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 50). +Notation "'(uint128_t)' x + y" := (Op (Add (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) y)) (at level 50). +Notation "x + '(uint128_t)' y" := (Op (Add (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint128_t)' x + y" := (Op (Add (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "x - y" := (Op (Sub _ _ _) (Pair x y)). +Notation "x - y" := (Op (Sub _ _ _) (Pair x (Var y))). +Notation "x - y" := (Op (Sub _ _ _) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub _ _ _) (Pair (Var x) (Var y))). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 0)) (Pair x y)) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 0) (TWord _) (TWord 0)) (Pair x y)) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 0) (TWord 0)) (Pair x y)) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 0) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 0) (TWord 0)) (Pair x (Var y))) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) y)) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 0) (TWord 0) (TWord 0)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 0) (TWord 0) (TWord 0)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 1)) (Pair x y)) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 1) (TWord _) (TWord 1)) (Pair x y)) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 1) (TWord 1)) (Pair x y)) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 1) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 1) (TWord 1)) (Pair x (Var y))) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) y)) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 1) (TWord 1) (TWord 1)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 1) (TWord 1) (TWord 1)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 2)) (Pair x y)) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 2) (TWord _) (TWord 2)) (Pair x y)) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 2) (TWord 2)) (Pair x y)) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 2) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 2) (TWord 2)) (Pair x (Var y))) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) y)) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 2) (TWord 2) (TWord 2)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 2) (TWord 2) (TWord 2)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 3)) (Pair x y)) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 3) (TWord _) (TWord 3)) (Pair x y)) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 3) (TWord 3)) (Pair x y)) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 3) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 3) (TWord 3)) (Pair x (Var y))) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) y)) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 3) (TWord 3) (TWord 3)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 3) (TWord 3) (TWord 3)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 4)) (Pair x y)) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 4) (TWord _) (TWord 4)) (Pair x y)) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 4) (TWord 4)) (Pair x y)) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 4) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 4) (TWord 4)) (Pair x (Var y))) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) y)) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 4) (TWord 4) (TWord 4)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 4) (TWord 4) (TWord 4)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 5)) (Pair x y)) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x - '(int)' y" := (Op (Sub (TWord _) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 5) (TWord _) (TWord 5)) (Pair x y)) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 5) (TWord 5)) (Pair x y)) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 5) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 5) (TWord 5)) (Pair x (Var y))) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) y)) (at level 50). +Notation "x - '(int)' y" := (Op (Sub (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(int)' x - y" := (Op (Sub (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 5) (TWord 5) (TWord 5)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 5) (TWord 5) (TWord 5)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))). +Notation "'(long)' x - '(long)' y" := (Op (Sub (TWord _) (TWord _) (TWord 6)) (Pair x y)) (at level 50). +Notation "'(long)' x - '(long)' y" := (Op (Sub (TWord _) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 50). +Notation "'(long)' x - '(long)' y" := (Op (Sub (TWord _) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 50). +Notation "'(long)' x - '(long)' y" := (Op (Sub (TWord _) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(long)' y" := (Op (Sub (TWord 6) (TWord _) (TWord 6)) (Pair x y)) (at level 50). +Notation "'(long)' x - y" := (Op (Sub (TWord _) (TWord 6) (TWord 6)) (Pair x y)) (at level 50). +Notation "x - '(long)' y" := (Op (Sub (TWord 6) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 50). +Notation "'(long)' x - y" := (Op (Sub (TWord _) (TWord 6) (TWord 6)) (Pair x (Var y))) (at level 50). +Notation "x - '(long)' y" := (Op (Sub (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 50). +Notation "'(long)' x - y" := (Op (Sub (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) y)) (at level 50). +Notation "x - '(long)' y" := (Op (Sub (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(long)' x - y" := (Op (Sub (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 6) (TWord 6) (TWord 6)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 6) (TWord 6) (TWord 6)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))). +Notation "'(uint128_t)' x - '(uint128_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 7)) (Pair x y)) (at level 50). +Notation "'(uint128_t)' x - '(uint128_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 50). +Notation "'(uint128_t)' x - '(uint128_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 50). +Notation "'(uint128_t)' x - '(uint128_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(uint128_t)' y" := (Op (Sub (TWord 7) (TWord _) (TWord 7)) (Pair x y)) (at level 50). +Notation "'(uint128_t)' x - y" := (Op (Sub (TWord _) (TWord 7) (TWord 7)) (Pair x y)) (at level 50). +Notation "x - '(uint128_t)' y" := (Op (Sub (TWord 7) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 50). +Notation "'(uint128_t)' x - y" := (Op (Sub (TWord _) (TWord 7) (TWord 7)) (Pair x (Var y))) (at level 50). +Notation "x - '(uint128_t)' y" := (Op (Sub (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 50). +Notation "'(uint128_t)' x - y" := (Op (Sub (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) y)) (at level 50). +Notation "x - '(uint128_t)' y" := (Op (Sub (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint128_t)' x - y" := (Op (Sub (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "x & y" := (Op (Land _ _ _) (Pair x y)). +Notation "x & y" := (Op (Land _ _ _) (Pair x (Var y))). +Notation "x & y" := (Op (Land _ _ _) (Pair (Var x) y)). +Notation "x & y" := (Op (Land _ _ _) (Pair (Var x) (Var y))). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 0)) (Pair x y)) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 0) (TWord _) (TWord 0)) (Pair x y)) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 0) (TWord 0)) (Pair x y)) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 0) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 0) (TWord 0)) (Pair x (Var y))) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) y)) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 0) (TWord 0) (TWord 0)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 0) (TWord 0) (TWord 0)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 1)) (Pair x y)) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 1) (TWord _) (TWord 1)) (Pair x y)) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 1) (TWord 1)) (Pair x y)) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 1) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 1) (TWord 1)) (Pair x (Var y))) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) y)) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 1) (TWord 1) (TWord 1)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 1) (TWord 1) (TWord 1)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 2)) (Pair x y)) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 2) (TWord _) (TWord 2)) (Pair x y)) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 2) (TWord 2)) (Pair x y)) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 2) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 2) (TWord 2)) (Pair x (Var y))) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) y)) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 2) (TWord 2) (TWord 2)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 2) (TWord 2) (TWord 2)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 3)) (Pair x y)) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 3) (TWord _) (TWord 3)) (Pair x y)) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 3) (TWord 3)) (Pair x y)) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 3) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 3) (TWord 3)) (Pair x (Var y))) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) y)) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 3) (TWord 3) (TWord 3)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 3) (TWord 3) (TWord 3)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 4)) (Pair x y)) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 4) (TWord _) (TWord 4)) (Pair x y)) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 4) (TWord 4)) (Pair x y)) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 4) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 4) (TWord 4)) (Pair x (Var y))) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) y)) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 4) (TWord 4) (TWord 4)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 4) (TWord 4) (TWord 4)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 5)) (Pair x y)) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x & '(int)' y" := (Op (Land (TWord _) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 5) (TWord _) (TWord 5)) (Pair x y)) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 5) (TWord 5)) (Pair x y)) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 5) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 5) (TWord 5)) (Pair x (Var y))) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) y)) (at level 40). +Notation "x & '(int)' y" := (Op (Land (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(int)' x & y" := (Op (Land (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 5) (TWord 5) (TWord 5)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 5) (TWord 5) (TWord 5)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))). +Notation "'(long)' x & '(long)' y" := (Op (Land (TWord _) (TWord _) (TWord 6)) (Pair x y)) (at level 40). +Notation "'(long)' x & '(long)' y" := (Op (Land (TWord _) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 40). +Notation "'(long)' x & '(long)' y" := (Op (Land (TWord _) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 40). +Notation "'(long)' x & '(long)' y" := (Op (Land (TWord _) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(long)' y" := (Op (Land (TWord 6) (TWord _) (TWord 6)) (Pair x y)) (at level 40). +Notation "'(long)' x & y" := (Op (Land (TWord _) (TWord 6) (TWord 6)) (Pair x y)) (at level 40). +Notation "x & '(long)' y" := (Op (Land (TWord 6) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 40). +Notation "'(long)' x & y" := (Op (Land (TWord _) (TWord 6) (TWord 6)) (Pair x (Var y))) (at level 40). +Notation "x & '(long)' y" := (Op (Land (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 40). +Notation "'(long)' x & y" := (Op (Land (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) y)) (at level 40). +Notation "x & '(long)' y" := (Op (Land (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(long)' x & y" := (Op (Land (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 6) (TWord 6) (TWord 6)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 6) (TWord 6) (TWord 6)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))). +Notation "'(uint128_t)' x & '(uint128_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 7)) (Pair x y)) (at level 40). +Notation "'(uint128_t)' x & '(uint128_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 40). +Notation "'(uint128_t)' x & '(uint128_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 40). +Notation "'(uint128_t)' x & '(uint128_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(uint128_t)' y" := (Op (Land (TWord 7) (TWord _) (TWord 7)) (Pair x y)) (at level 40). +Notation "'(uint128_t)' x & y" := (Op (Land (TWord _) (TWord 7) (TWord 7)) (Pair x y)) (at level 40). +Notation "x & '(uint128_t)' y" := (Op (Land (TWord 7) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 40). +Notation "'(uint128_t)' x & y" := (Op (Land (TWord _) (TWord 7) (TWord 7)) (Pair x (Var y))) (at level 40). +Notation "x & '(uint128_t)' y" := (Op (Land (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 40). +Notation "'(uint128_t)' x & y" := (Op (Land (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) y)) (at level 40). +Notation "x & '(uint128_t)' y" := (Op (Land (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint128_t)' x & y" := (Op (Land (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "x << y" := (Op (Shl _ _ _) (Pair x y)). +Notation "x << y" := (Op (Shl _ _ _) (Pair x (Var y))). +Notation "x << y" := (Op (Shl _ _ _) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl _ _ _) (Pair (Var x) (Var y))). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 0)) (Pair x y)) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 0) (TWord _) (TWord 0)) (Pair x y)) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 0) (TWord 0)) (Pair x y)) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 0) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 0) (TWord 0)) (Pair x (Var y))) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) y)) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 0) (TWord 0) (TWord 0)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 0) (TWord 0) (TWord 0)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 1)) (Pair x y)) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 1) (TWord _) (TWord 1)) (Pair x y)) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 1) (TWord 1)) (Pair x y)) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 1) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 1) (TWord 1)) (Pair x (Var y))) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) y)) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 1) (TWord 1) (TWord 1)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 1) (TWord 1) (TWord 1)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 2)) (Pair x y)) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 2) (TWord _) (TWord 2)) (Pair x y)) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 2) (TWord 2)) (Pair x y)) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 2) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 2) (TWord 2)) (Pair x (Var y))) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) y)) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 2) (TWord 2) (TWord 2)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 2) (TWord 2) (TWord 2)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 3)) (Pair x y)) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 3) (TWord _) (TWord 3)) (Pair x y)) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 3) (TWord 3)) (Pair x y)) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 3) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 3) (TWord 3)) (Pair x (Var y))) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) y)) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 3) (TWord 3) (TWord 3)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 3) (TWord 3) (TWord 3)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 4)) (Pair x y)) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 4) (TWord _) (TWord 4)) (Pair x y)) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 4) (TWord 4)) (Pair x y)) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 4) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 4) (TWord 4)) (Pair x (Var y))) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) y)) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 4) (TWord 4) (TWord 4)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 4) (TWord 4) (TWord 4)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 5)) (Pair x y)) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' x << '(int)' y" := (Op (Shl (TWord _) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 5) (TWord _) (TWord 5)) (Pair x y)) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 5) (TWord 5)) (Pair x y)) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 5) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 5) (TWord 5)) (Pair x (Var y))) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) y)) (at level 30). +Notation "x << '(int)' y" := (Op (Shl (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(int)' x << y" := (Op (Shl (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 5) (TWord 5) (TWord 5)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 5) (TWord 5) (TWord 5)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))). +Notation "'(long)' x << '(long)' y" := (Op (Shl (TWord _) (TWord _) (TWord 6)) (Pair x y)) (at level 30). +Notation "'(long)' x << '(long)' y" := (Op (Shl (TWord _) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 30). +Notation "'(long)' x << '(long)' y" := (Op (Shl (TWord _) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 30). +Notation "'(long)' x << '(long)' y" := (Op (Shl (TWord _) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(long)' y" := (Op (Shl (TWord 6) (TWord _) (TWord 6)) (Pair x y)) (at level 30). +Notation "'(long)' x << y" := (Op (Shl (TWord _) (TWord 6) (TWord 6)) (Pair x y)) (at level 30). +Notation "x << '(long)' y" := (Op (Shl (TWord 6) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 30). +Notation "'(long)' x << y" := (Op (Shl (TWord _) (TWord 6) (TWord 6)) (Pair x (Var y))) (at level 30). +Notation "x << '(long)' y" := (Op (Shl (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 30). +Notation "'(long)' x << y" := (Op (Shl (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) y)) (at level 30). +Notation "x << '(long)' y" := (Op (Shl (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(long)' x << y" := (Op (Shl (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 6) (TWord 6) (TWord 6)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 6) (TWord 6) (TWord 6)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))). +Notation "'(uint128_t)' x << '(uint128_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 7)) (Pair x y)) (at level 30). +Notation "'(uint128_t)' x << '(uint128_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 30). +Notation "'(uint128_t)' x << '(uint128_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 30). +Notation "'(uint128_t)' x << '(uint128_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(uint128_t)' y" := (Op (Shl (TWord 7) (TWord _) (TWord 7)) (Pair x y)) (at level 30). +Notation "'(uint128_t)' x << y" := (Op (Shl (TWord _) (TWord 7) (TWord 7)) (Pair x y)) (at level 30). +Notation "x << '(uint128_t)' y" := (Op (Shl (TWord 7) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 30). +Notation "'(uint128_t)' x << y" := (Op (Shl (TWord _) (TWord 7) (TWord 7)) (Pair x (Var y))) (at level 30). +Notation "x << '(uint128_t)' y" := (Op (Shl (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 30). +Notation "'(uint128_t)' x << y" := (Op (Shl (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) y)) (at level 30). +Notation "x << '(uint128_t)' y" := (Op (Shl (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint128_t)' x << y" := (Op (Shl (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "x >> y" := (Op (Shr _ _ _) (Pair x y)). +Notation "x >> y" := (Op (Shr _ _ _) (Pair x (Var y))). +Notation "x >> y" := (Op (Shr _ _ _) (Pair (Var x) y)). +Notation "x >> y" := (Op (Shr _ _ _) (Pair (Var x) (Var y))). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 0)) (Pair x y)) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 1)) (Pair x y)) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 2)) (Pair x y)) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 3)) (Pair x y)) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 4)) (Pair x y)) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 5)) (Pair x y)) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 30). +Notation "'(int)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(long)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 6)) (Pair x y)) (at level 30). +Notation "'(long)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 30). +Notation "'(long)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 30). +Notation "'(long)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint128_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 7)) (Pair x y)) (at level 30). +Notation "'(uint128_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 30). +Notation "'(uint128_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 30). +Notation "'(uint128_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 30). +Notation Return x := (Var x). +Notation Java_like := (Expr base_type op _). |