diff options
Diffstat (limited to 'src/Compilers/Z/CNotations.v')
| -rw-r--r-- | src/Compilers/Z/CNotations.v | 773 |
1 files changed, 773 insertions, 0 deletions
diff --git a/src/Compilers/Z/CNotations.v b/src/Compilers/Z/CNotations.v new file mode 100644 index 000000000..8ec885db3 --- /dev/null +++ b/src/Compilers/Z/CNotations.v @@ -0,0 +1,773 @@ +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). + +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('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 C_like := (Expr base_type op _).') +>> *) +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 ℤ := (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 "'(bool)' x * '(bool)' y" := (Op (Mul (TWord _) (TWord _) (TWord 0)) (Pair x y)) (at level 40). +Notation "'(bool)' x * '(bool)' y" := (Op (Mul (TWord _) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 40). +Notation "'(bool)' x * '(bool)' y" := (Op (Mul (TWord _) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 40). +Notation "'(bool)' x * '(bool)' y" := (Op (Mul (TWord _) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(bool)' y" := (Op (Mul (TWord 0) (TWord _) (TWord 0)) (Pair x y)) (at level 40). +Notation "'(bool)' x * y" := (Op (Mul (TWord _) (TWord 0) (TWord 0)) (Pair x y)) (at level 40). +Notation "x * '(bool)' y" := (Op (Mul (TWord 0) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 40). +Notation "'(bool)' x * y" := (Op (Mul (TWord _) (TWord 0) (TWord 0)) (Pair x (Var y))) (at level 40). +Notation "x * '(bool)' y" := (Op (Mul (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 40). +Notation "'(bool)' x * y" := (Op (Mul (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) y)) (at level 40). +Notation "x * '(bool)' y" := (Op (Mul (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(bool)' x * y" := (Op (Mul (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 0) (TWord 0) (TWord 0)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 0) (TWord 0) (TWord 0)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x * '(uint8_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 1)) (Pair x y)) (at level 40). +Notation "'(uint8_t)' x * '(uint8_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 40). +Notation "'(uint8_t)' x * '(uint8_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 40). +Notation "'(uint8_t)' x * '(uint8_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(uint8_t)' y" := (Op (Mul (TWord 1) (TWord _) (TWord 1)) (Pair x y)) (at level 40). +Notation "'(uint8_t)' x * y" := (Op (Mul (TWord _) (TWord 1) (TWord 1)) (Pair x y)) (at level 40). +Notation "x * '(uint8_t)' y" := (Op (Mul (TWord 1) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 40). +Notation "'(uint8_t)' x * y" := (Op (Mul (TWord _) (TWord 1) (TWord 1)) (Pair x (Var y))) (at level 40). +Notation "x * '(uint8_t)' y" := (Op (Mul (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 40). +Notation "'(uint8_t)' x * y" := (Op (Mul (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) y)) (at level 40). +Notation "x * '(uint8_t)' y" := (Op (Mul (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint8_t)' x * y" := (Op (Mul (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 1) (TWord 1) (TWord 1)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 1) (TWord 1) (TWord 1)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x * '(uint8_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 2)) (Pair x y)) (at level 40). +Notation "'(uint8_t)' x * '(uint8_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 40). +Notation "'(uint8_t)' x * '(uint8_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 40). +Notation "'(uint8_t)' x * '(uint8_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(uint8_t)' y" := (Op (Mul (TWord 2) (TWord _) (TWord 2)) (Pair x y)) (at level 40). +Notation "'(uint8_t)' x * y" := (Op (Mul (TWord _) (TWord 2) (TWord 2)) (Pair x y)) (at level 40). +Notation "x * '(uint8_t)' y" := (Op (Mul (TWord 2) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 40). +Notation "'(uint8_t)' x * y" := (Op (Mul (TWord _) (TWord 2) (TWord 2)) (Pair x (Var y))) (at level 40). +Notation "x * '(uint8_t)' y" := (Op (Mul (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 40). +Notation "'(uint8_t)' x * y" := (Op (Mul (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) y)) (at level 40). +Notation "x * '(uint8_t)' y" := (Op (Mul (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint8_t)' x * y" := (Op (Mul (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 2) (TWord 2) (TWord 2)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 2) (TWord 2) (TWord 2)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x * '(uint8_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 3)) (Pair x y)) (at level 40). +Notation "'(uint8_t)' x * '(uint8_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 40). +Notation "'(uint8_t)' x * '(uint8_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 40). +Notation "'(uint8_t)' x * '(uint8_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(uint8_t)' y" := (Op (Mul (TWord 3) (TWord _) (TWord 3)) (Pair x y)) (at level 40). +Notation "'(uint8_t)' x * y" := (Op (Mul (TWord _) (TWord 3) (TWord 3)) (Pair x y)) (at level 40). +Notation "x * '(uint8_t)' y" := (Op (Mul (TWord 3) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 40). +Notation "'(uint8_t)' x * y" := (Op (Mul (TWord _) (TWord 3) (TWord 3)) (Pair x (Var y))) (at level 40). +Notation "x * '(uint8_t)' y" := (Op (Mul (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 40). +Notation "'(uint8_t)' x * y" := (Op (Mul (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) y)) (at level 40). +Notation "x * '(uint8_t)' y" := (Op (Mul (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint8_t)' x * y" := (Op (Mul (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 3) (TWord 3) (TWord 3)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 3) (TWord 3) (TWord 3)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))). +Notation "'(uint16_t)' x * '(uint16_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 4)) (Pair x y)) (at level 40). +Notation "'(uint16_t)' x * '(uint16_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 40). +Notation "'(uint16_t)' x * '(uint16_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 40). +Notation "'(uint16_t)' x * '(uint16_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(uint16_t)' y" := (Op (Mul (TWord 4) (TWord _) (TWord 4)) (Pair x y)) (at level 40). +Notation "'(uint16_t)' x * y" := (Op (Mul (TWord _) (TWord 4) (TWord 4)) (Pair x y)) (at level 40). +Notation "x * '(uint16_t)' y" := (Op (Mul (TWord 4) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 40). +Notation "'(uint16_t)' x * y" := (Op (Mul (TWord _) (TWord 4) (TWord 4)) (Pair x (Var y))) (at level 40). +Notation "x * '(uint16_t)' y" := (Op (Mul (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 40). +Notation "'(uint16_t)' x * y" := (Op (Mul (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) y)) (at level 40). +Notation "x * '(uint16_t)' y" := (Op (Mul (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint16_t)' x * y" := (Op (Mul (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 4) (TWord 4) (TWord 4)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 4) (TWord 4) (TWord 4)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))). +Notation "'(uint32_t)' x * '(uint32_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 5)) (Pair x y)) (at level 40). +Notation "'(uint32_t)' x * '(uint32_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 40). +Notation "'(uint32_t)' x * '(uint32_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 40). +Notation "'(uint32_t)' x * '(uint32_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(uint32_t)' y" := (Op (Mul (TWord 5) (TWord _) (TWord 5)) (Pair x y)) (at level 40). +Notation "'(uint32_t)' x * y" := (Op (Mul (TWord _) (TWord 5) (TWord 5)) (Pair x y)) (at level 40). +Notation "x * '(uint32_t)' y" := (Op (Mul (TWord 5) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 40). +Notation "'(uint32_t)' x * y" := (Op (Mul (TWord _) (TWord 5) (TWord 5)) (Pair x (Var y))) (at level 40). +Notation "x * '(uint32_t)' y" := (Op (Mul (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 40). +Notation "'(uint32_t)' x * y" := (Op (Mul (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) y)) (at level 40). +Notation "x * '(uint32_t)' y" := (Op (Mul (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint32_t)' x * y" := (Op (Mul (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 5) (TWord 5) (TWord 5)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 5) (TWord 5) (TWord 5)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))). +Notation "'(uint64_t)' x * '(uint64_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 6)) (Pair x y)) (at level 40). +Notation "'(uint64_t)' x * '(uint64_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 40). +Notation "'(uint64_t)' x * '(uint64_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 40). +Notation "'(uint64_t)' x * '(uint64_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(uint64_t)' y" := (Op (Mul (TWord 6) (TWord _) (TWord 6)) (Pair x y)) (at level 40). +Notation "'(uint64_t)' x * y" := (Op (Mul (TWord _) (TWord 6) (TWord 6)) (Pair x y)) (at level 40). +Notation "x * '(uint64_t)' y" := (Op (Mul (TWord 6) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 40). +Notation "'(uint64_t)' x * y" := (Op (Mul (TWord _) (TWord 6) (TWord 6)) (Pair x (Var y))) (at level 40). +Notation "x * '(uint64_t)' y" := (Op (Mul (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 40). +Notation "'(uint64_t)' x * y" := (Op (Mul (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) y)) (at level 40). +Notation "x * '(uint64_t)' y" := (Op (Mul (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint64_t)' x * y" := (Op (Mul (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 6) (TWord 6) (TWord 6)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 6) (TWord 6) (TWord 6)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))). +Notation "'(uint128_t)' x * '(uint128_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 7)) (Pair x y)) (at level 40). +Notation "'(uint128_t)' x * '(uint128_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 40). +Notation "'(uint128_t)' x * '(uint128_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 40). +Notation "'(uint128_t)' x * '(uint128_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(uint128_t)' y" := (Op (Mul (TWord 7) (TWord _) (TWord 7)) (Pair x y)) (at level 40). +Notation "'(uint128_t)' x * y" := (Op (Mul (TWord _) (TWord 7) (TWord 7)) (Pair x y)) (at level 40). +Notation "x * '(uint128_t)' y" := (Op (Mul (TWord 7) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 40). +Notation "'(uint128_t)' x * y" := (Op (Mul (TWord _) (TWord 7) (TWord 7)) (Pair x (Var y))) (at level 40). +Notation "x * '(uint128_t)' y" := (Op (Mul (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 40). +Notation "'(uint128_t)' x * y" := (Op (Mul (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) y)) (at level 40). +Notation "x * '(uint128_t)' y" := (Op (Mul (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint128_t)' x * y" := (Op (Mul (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "x + y" := (Op (Add _ _ _) (Pair x y)). +Notation "x + y" := (Op (Add _ _ _) (Pair x (Var y))). +Notation "x + y" := (Op (Add _ _ _) (Pair (Var x) y)). +Notation "x + y" := (Op (Add _ _ _) (Pair (Var x) (Var y))). +Notation "'(bool)' x + '(bool)' y" := (Op (Add (TWord _) (TWord _) (TWord 0)) (Pair x y)) (at level 50). +Notation "'(bool)' x + '(bool)' y" := (Op (Add (TWord _) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 50). +Notation "'(bool)' x + '(bool)' y" := (Op (Add (TWord _) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 50). +Notation "'(bool)' x + '(bool)' y" := (Op (Add (TWord _) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(bool)' y" := (Op (Add (TWord 0) (TWord _) (TWord 0)) (Pair x y)) (at level 50). +Notation "'(bool)' x + y" := (Op (Add (TWord _) (TWord 0) (TWord 0)) (Pair x y)) (at level 50). +Notation "x + '(bool)' y" := (Op (Add (TWord 0) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 50). +Notation "'(bool)' x + y" := (Op (Add (TWord _) (TWord 0) (TWord 0)) (Pair x (Var y))) (at level 50). +Notation "x + '(bool)' y" := (Op (Add (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 50). +Notation "'(bool)' x + y" := (Op (Add (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) y)) (at level 50). +Notation "x + '(bool)' y" := (Op (Add (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(bool)' x + y" := (Op (Add (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 0) (TWord 0) (TWord 0)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 0) (TWord 0) (TWord 0)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x + '(uint8_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 1)) (Pair x y)) (at level 50). +Notation "'(uint8_t)' x + '(uint8_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 50). +Notation "'(uint8_t)' x + '(uint8_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 50). +Notation "'(uint8_t)' x + '(uint8_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(uint8_t)' y" := (Op (Add (TWord 1) (TWord _) (TWord 1)) (Pair x y)) (at level 50). +Notation "'(uint8_t)' x + y" := (Op (Add (TWord _) (TWord 1) (TWord 1)) (Pair x y)) (at level 50). +Notation "x + '(uint8_t)' y" := (Op (Add (TWord 1) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 50). +Notation "'(uint8_t)' x + y" := (Op (Add (TWord _) (TWord 1) (TWord 1)) (Pair x (Var y))) (at level 50). +Notation "x + '(uint8_t)' y" := (Op (Add (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 50). +Notation "'(uint8_t)' x + y" := (Op (Add (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) y)) (at level 50). +Notation "x + '(uint8_t)' y" := (Op (Add (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint8_t)' x + y" := (Op (Add (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 1) (TWord 1) (TWord 1)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 1) (TWord 1) (TWord 1)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x + '(uint8_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 2)) (Pair x y)) (at level 50). +Notation "'(uint8_t)' x + '(uint8_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 50). +Notation "'(uint8_t)' x + '(uint8_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 50). +Notation "'(uint8_t)' x + '(uint8_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(uint8_t)' y" := (Op (Add (TWord 2) (TWord _) (TWord 2)) (Pair x y)) (at level 50). +Notation "'(uint8_t)' x + y" := (Op (Add (TWord _) (TWord 2) (TWord 2)) (Pair x y)) (at level 50). +Notation "x + '(uint8_t)' y" := (Op (Add (TWord 2) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 50). +Notation "'(uint8_t)' x + y" := (Op (Add (TWord _) (TWord 2) (TWord 2)) (Pair x (Var y))) (at level 50). +Notation "x + '(uint8_t)' y" := (Op (Add (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 50). +Notation "'(uint8_t)' x + y" := (Op (Add (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) y)) (at level 50). +Notation "x + '(uint8_t)' y" := (Op (Add (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint8_t)' x + y" := (Op (Add (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 2) (TWord 2) (TWord 2)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 2) (TWord 2) (TWord 2)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x + '(uint8_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 3)) (Pair x y)) (at level 50). +Notation "'(uint8_t)' x + '(uint8_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 50). +Notation "'(uint8_t)' x + '(uint8_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 50). +Notation "'(uint8_t)' x + '(uint8_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(uint8_t)' y" := (Op (Add (TWord 3) (TWord _) (TWord 3)) (Pair x y)) (at level 50). +Notation "'(uint8_t)' x + y" := (Op (Add (TWord _) (TWord 3) (TWord 3)) (Pair x y)) (at level 50). +Notation "x + '(uint8_t)' y" := (Op (Add (TWord 3) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 50). +Notation "'(uint8_t)' x + y" := (Op (Add (TWord _) (TWord 3) (TWord 3)) (Pair x (Var y))) (at level 50). +Notation "x + '(uint8_t)' y" := (Op (Add (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 50). +Notation "'(uint8_t)' x + y" := (Op (Add (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) y)) (at level 50). +Notation "x + '(uint8_t)' y" := (Op (Add (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint8_t)' x + y" := (Op (Add (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 3) (TWord 3) (TWord 3)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 3) (TWord 3) (TWord 3)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))). +Notation "'(uint16_t)' x + '(uint16_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 4)) (Pair x y)) (at level 50). +Notation "'(uint16_t)' x + '(uint16_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 50). +Notation "'(uint16_t)' x + '(uint16_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 50). +Notation "'(uint16_t)' x + '(uint16_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(uint16_t)' y" := (Op (Add (TWord 4) (TWord _) (TWord 4)) (Pair x y)) (at level 50). +Notation "'(uint16_t)' x + y" := (Op (Add (TWord _) (TWord 4) (TWord 4)) (Pair x y)) (at level 50). +Notation "x + '(uint16_t)' y" := (Op (Add (TWord 4) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 50). +Notation "'(uint16_t)' x + y" := (Op (Add (TWord _) (TWord 4) (TWord 4)) (Pair x (Var y))) (at level 50). +Notation "x + '(uint16_t)' y" := (Op (Add (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 50). +Notation "'(uint16_t)' x + y" := (Op (Add (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) y)) (at level 50). +Notation "x + '(uint16_t)' y" := (Op (Add (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint16_t)' x + y" := (Op (Add (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 4) (TWord 4) (TWord 4)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 4) (TWord 4) (TWord 4)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))). +Notation "'(uint32_t)' x + '(uint32_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 5)) (Pair x y)) (at level 50). +Notation "'(uint32_t)' x + '(uint32_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 50). +Notation "'(uint32_t)' x + '(uint32_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 50). +Notation "'(uint32_t)' x + '(uint32_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(uint32_t)' y" := (Op (Add (TWord 5) (TWord _) (TWord 5)) (Pair x y)) (at level 50). +Notation "'(uint32_t)' x + y" := (Op (Add (TWord _) (TWord 5) (TWord 5)) (Pair x y)) (at level 50). +Notation "x + '(uint32_t)' y" := (Op (Add (TWord 5) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 50). +Notation "'(uint32_t)' x + y" := (Op (Add (TWord _) (TWord 5) (TWord 5)) (Pair x (Var y))) (at level 50). +Notation "x + '(uint32_t)' y" := (Op (Add (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 50). +Notation "'(uint32_t)' x + y" := (Op (Add (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) y)) (at level 50). +Notation "x + '(uint32_t)' y" := (Op (Add (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint32_t)' x + y" := (Op (Add (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 5) (TWord 5) (TWord 5)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 5) (TWord 5) (TWord 5)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))). +Notation "'(uint64_t)' x + '(uint64_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 6)) (Pair x y)) (at level 50). +Notation "'(uint64_t)' x + '(uint64_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 50). +Notation "'(uint64_t)' x + '(uint64_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 50). +Notation "'(uint64_t)' x + '(uint64_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(uint64_t)' y" := (Op (Add (TWord 6) (TWord _) (TWord 6)) (Pair x y)) (at level 50). +Notation "'(uint64_t)' x + y" := (Op (Add (TWord _) (TWord 6) (TWord 6)) (Pair x y)) (at level 50). +Notation "x + '(uint64_t)' y" := (Op (Add (TWord 6) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 50). +Notation "'(uint64_t)' x + y" := (Op (Add (TWord _) (TWord 6) (TWord 6)) (Pair x (Var y))) (at level 50). +Notation "x + '(uint64_t)' y" := (Op (Add (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 50). +Notation "'(uint64_t)' x + y" := (Op (Add (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) y)) (at level 50). +Notation "x + '(uint64_t)' y" := (Op (Add (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint64_t)' x + y" := (Op (Add (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 6) (TWord 6) (TWord 6)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 6) (TWord 6) (TWord 6)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))). +Notation "'(uint128_t)' x + '(uint128_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 7)) (Pair x y)) (at level 50). +Notation "'(uint128_t)' x + '(uint128_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 50). +Notation "'(uint128_t)' x + '(uint128_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 50). +Notation "'(uint128_t)' x + '(uint128_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(uint128_t)' y" := (Op (Add (TWord 7) (TWord _) (TWord 7)) (Pair x y)) (at level 50). +Notation "'(uint128_t)' x + y" := (Op (Add (TWord _) (TWord 7) (TWord 7)) (Pair x y)) (at level 50). +Notation "x + '(uint128_t)' y" := (Op (Add (TWord 7) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 50). +Notation "'(uint128_t)' x + y" := (Op (Add (TWord _) (TWord 7) (TWord 7)) (Pair x (Var y))) (at level 50). +Notation "x + '(uint128_t)' y" := (Op (Add (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 50). +Notation "'(uint128_t)' x + y" := (Op (Add (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) y)) (at level 50). +Notation "x + '(uint128_t)' y" := (Op (Add (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint128_t)' x + y" := (Op (Add (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "x - y" := (Op (Sub _ _ _) (Pair x y)). +Notation "x - y" := (Op (Sub _ _ _) (Pair x (Var y))). +Notation "x - y" := (Op (Sub _ _ _) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub _ _ _) (Pair (Var x) (Var y))). +Notation "'(bool)' x - '(bool)' y" := (Op (Sub (TWord _) (TWord _) (TWord 0)) (Pair x y)) (at level 50). +Notation "'(bool)' x - '(bool)' y" := (Op (Sub (TWord _) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 50). +Notation "'(bool)' x - '(bool)' y" := (Op (Sub (TWord _) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 50). +Notation "'(bool)' x - '(bool)' y" := (Op (Sub (TWord _) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(bool)' y" := (Op (Sub (TWord 0) (TWord _) (TWord 0)) (Pair x y)) (at level 50). +Notation "'(bool)' x - y" := (Op (Sub (TWord _) (TWord 0) (TWord 0)) (Pair x y)) (at level 50). +Notation "x - '(bool)' y" := (Op (Sub (TWord 0) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 50). +Notation "'(bool)' x - y" := (Op (Sub (TWord _) (TWord 0) (TWord 0)) (Pair x (Var y))) (at level 50). +Notation "x - '(bool)' y" := (Op (Sub (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 50). +Notation "'(bool)' x - y" := (Op (Sub (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) y)) (at level 50). +Notation "x - '(bool)' y" := (Op (Sub (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(bool)' x - y" := (Op (Sub (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 0) (TWord 0) (TWord 0)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 0) (TWord 0) (TWord 0)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x - '(uint8_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 1)) (Pair x y)) (at level 50). +Notation "'(uint8_t)' x - '(uint8_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 50). +Notation "'(uint8_t)' x - '(uint8_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 50). +Notation "'(uint8_t)' x - '(uint8_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(uint8_t)' y" := (Op (Sub (TWord 1) (TWord _) (TWord 1)) (Pair x y)) (at level 50). +Notation "'(uint8_t)' x - y" := (Op (Sub (TWord _) (TWord 1) (TWord 1)) (Pair x y)) (at level 50). +Notation "x - '(uint8_t)' y" := (Op (Sub (TWord 1) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 50). +Notation "'(uint8_t)' x - y" := (Op (Sub (TWord _) (TWord 1) (TWord 1)) (Pair x (Var y))) (at level 50). +Notation "x - '(uint8_t)' y" := (Op (Sub (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 50). +Notation "'(uint8_t)' x - y" := (Op (Sub (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) y)) (at level 50). +Notation "x - '(uint8_t)' y" := (Op (Sub (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint8_t)' x - y" := (Op (Sub (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 1) (TWord 1) (TWord 1)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 1) (TWord 1) (TWord 1)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x - '(uint8_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 2)) (Pair x y)) (at level 50). +Notation "'(uint8_t)' x - '(uint8_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 50). +Notation "'(uint8_t)' x - '(uint8_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 50). +Notation "'(uint8_t)' x - '(uint8_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(uint8_t)' y" := (Op (Sub (TWord 2) (TWord _) (TWord 2)) (Pair x y)) (at level 50). +Notation "'(uint8_t)' x - y" := (Op (Sub (TWord _) (TWord 2) (TWord 2)) (Pair x y)) (at level 50). +Notation "x - '(uint8_t)' y" := (Op (Sub (TWord 2) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 50). +Notation "'(uint8_t)' x - y" := (Op (Sub (TWord _) (TWord 2) (TWord 2)) (Pair x (Var y))) (at level 50). +Notation "x - '(uint8_t)' y" := (Op (Sub (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 50). +Notation "'(uint8_t)' x - y" := (Op (Sub (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) y)) (at level 50). +Notation "x - '(uint8_t)' y" := (Op (Sub (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint8_t)' x - y" := (Op (Sub (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 2) (TWord 2) (TWord 2)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 2) (TWord 2) (TWord 2)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x - '(uint8_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 3)) (Pair x y)) (at level 50). +Notation "'(uint8_t)' x - '(uint8_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 50). +Notation "'(uint8_t)' x - '(uint8_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 50). +Notation "'(uint8_t)' x - '(uint8_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(uint8_t)' y" := (Op (Sub (TWord 3) (TWord _) (TWord 3)) (Pair x y)) (at level 50). +Notation "'(uint8_t)' x - y" := (Op (Sub (TWord _) (TWord 3) (TWord 3)) (Pair x y)) (at level 50). +Notation "x - '(uint8_t)' y" := (Op (Sub (TWord 3) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 50). +Notation "'(uint8_t)' x - y" := (Op (Sub (TWord _) (TWord 3) (TWord 3)) (Pair x (Var y))) (at level 50). +Notation "x - '(uint8_t)' y" := (Op (Sub (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 50). +Notation "'(uint8_t)' x - y" := (Op (Sub (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) y)) (at level 50). +Notation "x - '(uint8_t)' y" := (Op (Sub (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint8_t)' x - y" := (Op (Sub (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 3) (TWord 3) (TWord 3)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 3) (TWord 3) (TWord 3)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))). +Notation "'(uint16_t)' x - '(uint16_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 4)) (Pair x y)) (at level 50). +Notation "'(uint16_t)' x - '(uint16_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 50). +Notation "'(uint16_t)' x - '(uint16_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 50). +Notation "'(uint16_t)' x - '(uint16_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(uint16_t)' y" := (Op (Sub (TWord 4) (TWord _) (TWord 4)) (Pair x y)) (at level 50). +Notation "'(uint16_t)' x - y" := (Op (Sub (TWord _) (TWord 4) (TWord 4)) (Pair x y)) (at level 50). +Notation "x - '(uint16_t)' y" := (Op (Sub (TWord 4) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 50). +Notation "'(uint16_t)' x - y" := (Op (Sub (TWord _) (TWord 4) (TWord 4)) (Pair x (Var y))) (at level 50). +Notation "x - '(uint16_t)' y" := (Op (Sub (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 50). +Notation "'(uint16_t)' x - y" := (Op (Sub (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) y)) (at level 50). +Notation "x - '(uint16_t)' y" := (Op (Sub (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint16_t)' x - y" := (Op (Sub (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 4) (TWord 4) (TWord 4)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 4) (TWord 4) (TWord 4)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))). +Notation "'(uint32_t)' x - '(uint32_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 5)) (Pair x y)) (at level 50). +Notation "'(uint32_t)' x - '(uint32_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 50). +Notation "'(uint32_t)' x - '(uint32_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 50). +Notation "'(uint32_t)' x - '(uint32_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(uint32_t)' y" := (Op (Sub (TWord 5) (TWord _) (TWord 5)) (Pair x y)) (at level 50). +Notation "'(uint32_t)' x - y" := (Op (Sub (TWord _) (TWord 5) (TWord 5)) (Pair x y)) (at level 50). +Notation "x - '(uint32_t)' y" := (Op (Sub (TWord 5) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 50). +Notation "'(uint32_t)' x - y" := (Op (Sub (TWord _) (TWord 5) (TWord 5)) (Pair x (Var y))) (at level 50). +Notation "x - '(uint32_t)' y" := (Op (Sub (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 50). +Notation "'(uint32_t)' x - y" := (Op (Sub (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) y)) (at level 50). +Notation "x - '(uint32_t)' y" := (Op (Sub (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint32_t)' x - y" := (Op (Sub (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 5) (TWord 5) (TWord 5)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 5) (TWord 5) (TWord 5)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))). +Notation "'(uint64_t)' x - '(uint64_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 6)) (Pair x y)) (at level 50). +Notation "'(uint64_t)' x - '(uint64_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 50). +Notation "'(uint64_t)' x - '(uint64_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 50). +Notation "'(uint64_t)' x - '(uint64_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(uint64_t)' y" := (Op (Sub (TWord 6) (TWord _) (TWord 6)) (Pair x y)) (at level 50). +Notation "'(uint64_t)' x - y" := (Op (Sub (TWord _) (TWord 6) (TWord 6)) (Pair x y)) (at level 50). +Notation "x - '(uint64_t)' y" := (Op (Sub (TWord 6) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 50). +Notation "'(uint64_t)' x - y" := (Op (Sub (TWord _) (TWord 6) (TWord 6)) (Pair x (Var y))) (at level 50). +Notation "x - '(uint64_t)' y" := (Op (Sub (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 50). +Notation "'(uint64_t)' x - y" := (Op (Sub (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) y)) (at level 50). +Notation "x - '(uint64_t)' y" := (Op (Sub (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint64_t)' x - y" := (Op (Sub (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 6) (TWord 6) (TWord 6)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 6) (TWord 6) (TWord 6)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))). +Notation "'(uint128_t)' x - '(uint128_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 7)) (Pair x y)) (at level 50). +Notation "'(uint128_t)' x - '(uint128_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 50). +Notation "'(uint128_t)' x - '(uint128_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 50). +Notation "'(uint128_t)' x - '(uint128_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(uint128_t)' y" := (Op (Sub (TWord 7) (TWord _) (TWord 7)) (Pair x y)) (at level 50). +Notation "'(uint128_t)' x - y" := (Op (Sub (TWord _) (TWord 7) (TWord 7)) (Pair x y)) (at level 50). +Notation "x - '(uint128_t)' y" := (Op (Sub (TWord 7) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 50). +Notation "'(uint128_t)' x - y" := (Op (Sub (TWord _) (TWord 7) (TWord 7)) (Pair x (Var y))) (at level 50). +Notation "x - '(uint128_t)' y" := (Op (Sub (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 50). +Notation "'(uint128_t)' x - y" := (Op (Sub (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) y)) (at level 50). +Notation "x - '(uint128_t)' y" := (Op (Sub (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint128_t)' x - y" := (Op (Sub (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "x & y" := (Op (Land _ _ _) (Pair x y)). +Notation "x & y" := (Op (Land _ _ _) (Pair x (Var y))). +Notation "x & y" := (Op (Land _ _ _) (Pair (Var x) y)). +Notation "x & y" := (Op (Land _ _ _) (Pair (Var x) (Var y))). +Notation "'(bool)' x & '(bool)' y" := (Op (Land (TWord _) (TWord _) (TWord 0)) (Pair x y)) (at level 40). +Notation "'(bool)' x & '(bool)' y" := (Op (Land (TWord _) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 40). +Notation "'(bool)' x & '(bool)' y" := (Op (Land (TWord _) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 40). +Notation "'(bool)' x & '(bool)' y" := (Op (Land (TWord _) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(bool)' y" := (Op (Land (TWord 0) (TWord _) (TWord 0)) (Pair x y)) (at level 40). +Notation "'(bool)' x & y" := (Op (Land (TWord _) (TWord 0) (TWord 0)) (Pair x y)) (at level 40). +Notation "x & '(bool)' y" := (Op (Land (TWord 0) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 40). +Notation "'(bool)' x & y" := (Op (Land (TWord _) (TWord 0) (TWord 0)) (Pair x (Var y))) (at level 40). +Notation "x & '(bool)' y" := (Op (Land (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 40). +Notation "'(bool)' x & y" := (Op (Land (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) y)) (at level 40). +Notation "x & '(bool)' y" := (Op (Land (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(bool)' x & y" := (Op (Land (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 0) (TWord 0) (TWord 0)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 0) (TWord 0) (TWord 0)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x & '(uint8_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 1)) (Pair x y)) (at level 40). +Notation "'(uint8_t)' x & '(uint8_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 40). +Notation "'(uint8_t)' x & '(uint8_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 40). +Notation "'(uint8_t)' x & '(uint8_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(uint8_t)' y" := (Op (Land (TWord 1) (TWord _) (TWord 1)) (Pair x y)) (at level 40). +Notation "'(uint8_t)' x & y" := (Op (Land (TWord _) (TWord 1) (TWord 1)) (Pair x y)) (at level 40). +Notation "x & '(uint8_t)' y" := (Op (Land (TWord 1) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 40). +Notation "'(uint8_t)' x & y" := (Op (Land (TWord _) (TWord 1) (TWord 1)) (Pair x (Var y))) (at level 40). +Notation "x & '(uint8_t)' y" := (Op (Land (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 40). +Notation "'(uint8_t)' x & y" := (Op (Land (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) y)) (at level 40). +Notation "x & '(uint8_t)' y" := (Op (Land (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint8_t)' x & y" := (Op (Land (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 1) (TWord 1) (TWord 1)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 1) (TWord 1) (TWord 1)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x & '(uint8_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 2)) (Pair x y)) (at level 40). +Notation "'(uint8_t)' x & '(uint8_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 40). +Notation "'(uint8_t)' x & '(uint8_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 40). +Notation "'(uint8_t)' x & '(uint8_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(uint8_t)' y" := (Op (Land (TWord 2) (TWord _) (TWord 2)) (Pair x y)) (at level 40). +Notation "'(uint8_t)' x & y" := (Op (Land (TWord _) (TWord 2) (TWord 2)) (Pair x y)) (at level 40). +Notation "x & '(uint8_t)' y" := (Op (Land (TWord 2) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 40). +Notation "'(uint8_t)' x & y" := (Op (Land (TWord _) (TWord 2) (TWord 2)) (Pair x (Var y))) (at level 40). +Notation "x & '(uint8_t)' y" := (Op (Land (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 40). +Notation "'(uint8_t)' x & y" := (Op (Land (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) y)) (at level 40). +Notation "x & '(uint8_t)' y" := (Op (Land (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint8_t)' x & y" := (Op (Land (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 2) (TWord 2) (TWord 2)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 2) (TWord 2) (TWord 2)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x & '(uint8_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 3)) (Pair x y)) (at level 40). +Notation "'(uint8_t)' x & '(uint8_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 40). +Notation "'(uint8_t)' x & '(uint8_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 40). +Notation "'(uint8_t)' x & '(uint8_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(uint8_t)' y" := (Op (Land (TWord 3) (TWord _) (TWord 3)) (Pair x y)) (at level 40). +Notation "'(uint8_t)' x & y" := (Op (Land (TWord _) (TWord 3) (TWord 3)) (Pair x y)) (at level 40). +Notation "x & '(uint8_t)' y" := (Op (Land (TWord 3) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 40). +Notation "'(uint8_t)' x & y" := (Op (Land (TWord _) (TWord 3) (TWord 3)) (Pair x (Var y))) (at level 40). +Notation "x & '(uint8_t)' y" := (Op (Land (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 40). +Notation "'(uint8_t)' x & y" := (Op (Land (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) y)) (at level 40). +Notation "x & '(uint8_t)' y" := (Op (Land (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint8_t)' x & y" := (Op (Land (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 3) (TWord 3) (TWord 3)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 3) (TWord 3) (TWord 3)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))). +Notation "'(uint16_t)' x & '(uint16_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 4)) (Pair x y)) (at level 40). +Notation "'(uint16_t)' x & '(uint16_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 40). +Notation "'(uint16_t)' x & '(uint16_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 40). +Notation "'(uint16_t)' x & '(uint16_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(uint16_t)' y" := (Op (Land (TWord 4) (TWord _) (TWord 4)) (Pair x y)) (at level 40). +Notation "'(uint16_t)' x & y" := (Op (Land (TWord _) (TWord 4) (TWord 4)) (Pair x y)) (at level 40). +Notation "x & '(uint16_t)' y" := (Op (Land (TWord 4) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 40). +Notation "'(uint16_t)' x & y" := (Op (Land (TWord _) (TWord 4) (TWord 4)) (Pair x (Var y))) (at level 40). +Notation "x & '(uint16_t)' y" := (Op (Land (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 40). +Notation "'(uint16_t)' x & y" := (Op (Land (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) y)) (at level 40). +Notation "x & '(uint16_t)' y" := (Op (Land (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint16_t)' x & y" := (Op (Land (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 4) (TWord 4) (TWord 4)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 4) (TWord 4) (TWord 4)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))). +Notation "'(uint32_t)' x & '(uint32_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 5)) (Pair x y)) (at level 40). +Notation "'(uint32_t)' x & '(uint32_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 40). +Notation "'(uint32_t)' x & '(uint32_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 40). +Notation "'(uint32_t)' x & '(uint32_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(uint32_t)' y" := (Op (Land (TWord 5) (TWord _) (TWord 5)) (Pair x y)) (at level 40). +Notation "'(uint32_t)' x & y" := (Op (Land (TWord _) (TWord 5) (TWord 5)) (Pair x y)) (at level 40). +Notation "x & '(uint32_t)' y" := (Op (Land (TWord 5) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 40). +Notation "'(uint32_t)' x & y" := (Op (Land (TWord _) (TWord 5) (TWord 5)) (Pair x (Var y))) (at level 40). +Notation "x & '(uint32_t)' y" := (Op (Land (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 40). +Notation "'(uint32_t)' x & y" := (Op (Land (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) y)) (at level 40). +Notation "x & '(uint32_t)' y" := (Op (Land (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint32_t)' x & y" := (Op (Land (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 5) (TWord 5) (TWord 5)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 5) (TWord 5) (TWord 5)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))). +Notation "'(uint64_t)' x & '(uint64_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 6)) (Pair x y)) (at level 40). +Notation "'(uint64_t)' x & '(uint64_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 40). +Notation "'(uint64_t)' x & '(uint64_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 40). +Notation "'(uint64_t)' x & '(uint64_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(uint64_t)' y" := (Op (Land (TWord 6) (TWord _) (TWord 6)) (Pair x y)) (at level 40). +Notation "'(uint64_t)' x & y" := (Op (Land (TWord _) (TWord 6) (TWord 6)) (Pair x y)) (at level 40). +Notation "x & '(uint64_t)' y" := (Op (Land (TWord 6) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 40). +Notation "'(uint64_t)' x & y" := (Op (Land (TWord _) (TWord 6) (TWord 6)) (Pair x (Var y))) (at level 40). +Notation "x & '(uint64_t)' y" := (Op (Land (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 40). +Notation "'(uint64_t)' x & y" := (Op (Land (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) y)) (at level 40). +Notation "x & '(uint64_t)' y" := (Op (Land (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint64_t)' x & y" := (Op (Land (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 6) (TWord 6) (TWord 6)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 6) (TWord 6) (TWord 6)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))). +Notation "'(uint128_t)' x & '(uint128_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 7)) (Pair x y)) (at level 40). +Notation "'(uint128_t)' x & '(uint128_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 40). +Notation "'(uint128_t)' x & '(uint128_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 40). +Notation "'(uint128_t)' x & '(uint128_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(uint128_t)' y" := (Op (Land (TWord 7) (TWord _) (TWord 7)) (Pair x y)) (at level 40). +Notation "'(uint128_t)' x & y" := (Op (Land (TWord _) (TWord 7) (TWord 7)) (Pair x y)) (at level 40). +Notation "x & '(uint128_t)' y" := (Op (Land (TWord 7) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 40). +Notation "'(uint128_t)' x & y" := (Op (Land (TWord _) (TWord 7) (TWord 7)) (Pair x (Var y))) (at level 40). +Notation "x & '(uint128_t)' y" := (Op (Land (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 40). +Notation "'(uint128_t)' x & y" := (Op (Land (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) y)) (at level 40). +Notation "x & '(uint128_t)' y" := (Op (Land (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint128_t)' x & y" := (Op (Land (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "x << y" := (Op (Shl _ _ _) (Pair x y)). +Notation "x << y" := (Op (Shl _ _ _) (Pair x (Var y))). +Notation "x << y" := (Op (Shl _ _ _) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl _ _ _) (Pair (Var x) (Var y))). +Notation "'(bool)' x << '(bool)' y" := (Op (Shl (TWord _) (TWord _) (TWord 0)) (Pair x y)) (at level 30). +Notation "'(bool)' x << '(bool)' y" := (Op (Shl (TWord _) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 30). +Notation "'(bool)' x << '(bool)' y" := (Op (Shl (TWord _) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 30). +Notation "'(bool)' x << '(bool)' y" := (Op (Shl (TWord _) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(bool)' y" := (Op (Shl (TWord 0) (TWord _) (TWord 0)) (Pair x y)) (at level 30). +Notation "'(bool)' x << y" := (Op (Shl (TWord _) (TWord 0) (TWord 0)) (Pair x y)) (at level 30). +Notation "x << '(bool)' y" := (Op (Shl (TWord 0) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 30). +Notation "'(bool)' x << y" := (Op (Shl (TWord _) (TWord 0) (TWord 0)) (Pair x (Var y))) (at level 30). +Notation "x << '(bool)' y" := (Op (Shl (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 30). +Notation "'(bool)' x << y" := (Op (Shl (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) y)) (at level 30). +Notation "x << '(bool)' y" := (Op (Shl (TWord 0) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(bool)' x << y" := (Op (Shl (TWord _) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 0) (TWord 0) (TWord 0)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 0) (TWord 0) (TWord 0)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 0) (TWord 0) (TWord 0)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x << '(uint8_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 1)) (Pair x y)) (at level 30). +Notation "'(uint8_t)' x << '(uint8_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 30). +Notation "'(uint8_t)' x << '(uint8_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 30). +Notation "'(uint8_t)' x << '(uint8_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(uint8_t)' y" := (Op (Shl (TWord 1) (TWord _) (TWord 1)) (Pair x y)) (at level 30). +Notation "'(uint8_t)' x << y" := (Op (Shl (TWord _) (TWord 1) (TWord 1)) (Pair x y)) (at level 30). +Notation "x << '(uint8_t)' y" := (Op (Shl (TWord 1) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 30). +Notation "'(uint8_t)' x << y" := (Op (Shl (TWord _) (TWord 1) (TWord 1)) (Pair x (Var y))) (at level 30). +Notation "x << '(uint8_t)' y" := (Op (Shl (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 30). +Notation "'(uint8_t)' x << y" := (Op (Shl (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) y)) (at level 30). +Notation "x << '(uint8_t)' y" := (Op (Shl (TWord 1) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint8_t)' x << y" := (Op (Shl (TWord _) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 1) (TWord 1) (TWord 1)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 1) (TWord 1) (TWord 1)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 1) (TWord 1) (TWord 1)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x << '(uint8_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 2)) (Pair x y)) (at level 30). +Notation "'(uint8_t)' x << '(uint8_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 30). +Notation "'(uint8_t)' x << '(uint8_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 30). +Notation "'(uint8_t)' x << '(uint8_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(uint8_t)' y" := (Op (Shl (TWord 2) (TWord _) (TWord 2)) (Pair x y)) (at level 30). +Notation "'(uint8_t)' x << y" := (Op (Shl (TWord _) (TWord 2) (TWord 2)) (Pair x y)) (at level 30). +Notation "x << '(uint8_t)' y" := (Op (Shl (TWord 2) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 30). +Notation "'(uint8_t)' x << y" := (Op (Shl (TWord _) (TWord 2) (TWord 2)) (Pair x (Var y))) (at level 30). +Notation "x << '(uint8_t)' y" := (Op (Shl (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 30). +Notation "'(uint8_t)' x << y" := (Op (Shl (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) y)) (at level 30). +Notation "x << '(uint8_t)' y" := (Op (Shl (TWord 2) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint8_t)' x << y" := (Op (Shl (TWord _) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 2) (TWord 2) (TWord 2)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 2) (TWord 2) (TWord 2)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 2) (TWord 2) (TWord 2)) (Pair (Var x) (Var y))). +Notation "'(uint8_t)' x << '(uint8_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 3)) (Pair x y)) (at level 30). +Notation "'(uint8_t)' x << '(uint8_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 30). +Notation "'(uint8_t)' x << '(uint8_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 30). +Notation "'(uint8_t)' x << '(uint8_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(uint8_t)' y" := (Op (Shl (TWord 3) (TWord _) (TWord 3)) (Pair x y)) (at level 30). +Notation "'(uint8_t)' x << y" := (Op (Shl (TWord _) (TWord 3) (TWord 3)) (Pair x y)) (at level 30). +Notation "x << '(uint8_t)' y" := (Op (Shl (TWord 3) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 30). +Notation "'(uint8_t)' x << y" := (Op (Shl (TWord _) (TWord 3) (TWord 3)) (Pair x (Var y))) (at level 30). +Notation "x << '(uint8_t)' y" := (Op (Shl (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 30). +Notation "'(uint8_t)' x << y" := (Op (Shl (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) y)) (at level 30). +Notation "x << '(uint8_t)' y" := (Op (Shl (TWord 3) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint8_t)' x << y" := (Op (Shl (TWord _) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 3) (TWord 3) (TWord 3)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 3) (TWord 3) (TWord 3)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 3) (TWord 3) (TWord 3)) (Pair (Var x) (Var y))). +Notation "'(uint16_t)' x << '(uint16_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 4)) (Pair x y)) (at level 30). +Notation "'(uint16_t)' x << '(uint16_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 30). +Notation "'(uint16_t)' x << '(uint16_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 30). +Notation "'(uint16_t)' x << '(uint16_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(uint16_t)' y" := (Op (Shl (TWord 4) (TWord _) (TWord 4)) (Pair x y)) (at level 30). +Notation "'(uint16_t)' x << y" := (Op (Shl (TWord _) (TWord 4) (TWord 4)) (Pair x y)) (at level 30). +Notation "x << '(uint16_t)' y" := (Op (Shl (TWord 4) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 30). +Notation "'(uint16_t)' x << y" := (Op (Shl (TWord _) (TWord 4) (TWord 4)) (Pair x (Var y))) (at level 30). +Notation "x << '(uint16_t)' y" := (Op (Shl (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 30). +Notation "'(uint16_t)' x << y" := (Op (Shl (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) y)) (at level 30). +Notation "x << '(uint16_t)' y" := (Op (Shl (TWord 4) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint16_t)' x << y" := (Op (Shl (TWord _) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 4) (TWord 4) (TWord 4)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 4) (TWord 4) (TWord 4)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 4) (TWord 4) (TWord 4)) (Pair (Var x) (Var y))). +Notation "'(uint32_t)' x << '(uint32_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 5)) (Pair x y)) (at level 30). +Notation "'(uint32_t)' x << '(uint32_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 30). +Notation "'(uint32_t)' x << '(uint32_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 30). +Notation "'(uint32_t)' x << '(uint32_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(uint32_t)' y" := (Op (Shl (TWord 5) (TWord _) (TWord 5)) (Pair x y)) (at level 30). +Notation "'(uint32_t)' x << y" := (Op (Shl (TWord _) (TWord 5) (TWord 5)) (Pair x y)) (at level 30). +Notation "x << '(uint32_t)' y" := (Op (Shl (TWord 5) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 30). +Notation "'(uint32_t)' x << y" := (Op (Shl (TWord _) (TWord 5) (TWord 5)) (Pair x (Var y))) (at level 30). +Notation "x << '(uint32_t)' y" := (Op (Shl (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 30). +Notation "'(uint32_t)' x << y" := (Op (Shl (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) y)) (at level 30). +Notation "x << '(uint32_t)' y" := (Op (Shl (TWord 5) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint32_t)' x << y" := (Op (Shl (TWord _) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 5) (TWord 5) (TWord 5)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 5) (TWord 5) (TWord 5)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 5) (TWord 5) (TWord 5)) (Pair (Var x) (Var y))). +Notation "'(uint64_t)' x << '(uint64_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 6)) (Pair x y)) (at level 30). +Notation "'(uint64_t)' x << '(uint64_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 30). +Notation "'(uint64_t)' x << '(uint64_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 30). +Notation "'(uint64_t)' x << '(uint64_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(uint64_t)' y" := (Op (Shl (TWord 6) (TWord _) (TWord 6)) (Pair x y)) (at level 30). +Notation "'(uint64_t)' x << y" := (Op (Shl (TWord _) (TWord 6) (TWord 6)) (Pair x y)) (at level 30). +Notation "x << '(uint64_t)' y" := (Op (Shl (TWord 6) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 30). +Notation "'(uint64_t)' x << y" := (Op (Shl (TWord _) (TWord 6) (TWord 6)) (Pair x (Var y))) (at level 30). +Notation "x << '(uint64_t)' y" := (Op (Shl (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 30). +Notation "'(uint64_t)' x << y" := (Op (Shl (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) y)) (at level 30). +Notation "x << '(uint64_t)' y" := (Op (Shl (TWord 6) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint64_t)' x << y" := (Op (Shl (TWord _) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 6) (TWord 6) (TWord 6)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 6) (TWord 6) (TWord 6)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 6) (TWord 6) (TWord 6)) (Pair (Var x) (Var y))). +Notation "'(uint128_t)' x << '(uint128_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 7)) (Pair x y)) (at level 30). +Notation "'(uint128_t)' x << '(uint128_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 30). +Notation "'(uint128_t)' x << '(uint128_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 30). +Notation "'(uint128_t)' x << '(uint128_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(uint128_t)' y" := (Op (Shl (TWord 7) (TWord _) (TWord 7)) (Pair x y)) (at level 30). +Notation "'(uint128_t)' x << y" := (Op (Shl (TWord _) (TWord 7) (TWord 7)) (Pair x y)) (at level 30). +Notation "x << '(uint128_t)' y" := (Op (Shl (TWord 7) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 30). +Notation "'(uint128_t)' x << y" := (Op (Shl (TWord _) (TWord 7) (TWord 7)) (Pair x (Var y))) (at level 30). +Notation "x << '(uint128_t)' y" := (Op (Shl (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 30). +Notation "'(uint128_t)' x << y" := (Op (Shl (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) y)) (at level 30). +Notation "x << '(uint128_t)' y" := (Op (Shl (TWord 7) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint128_t)' x << y" := (Op (Shl (TWord _) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "x >> y" := (Op (Shr _ _ _) (Pair x y)). +Notation "x >> y" := (Op (Shr _ _ _) (Pair x (Var y))). +Notation "x >> y" := (Op (Shr _ _ _) (Pair (Var x) y)). +Notation "x >> y" := (Op (Shr _ _ _) (Pair (Var x) (Var y))). +Notation "'(bool)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 0)) (Pair x y)) (at level 30). +Notation "'(bool)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 30). +Notation "'(bool)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 30). +Notation "'(bool)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint8_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 1)) (Pair x y)) (at level 30). +Notation "'(uint8_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 1)) (Pair x (Var y))) (at level 30). +Notation "'(uint8_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 1)) (Pair (Var x) y)) (at level 30). +Notation "'(uint8_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 1)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint8_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 2)) (Pair x y)) (at level 30). +Notation "'(uint8_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 2)) (Pair x (Var y))) (at level 30). +Notation "'(uint8_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 2)) (Pair (Var x) y)) (at level 30). +Notation "'(uint8_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 2)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint8_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 3)) (Pair x y)) (at level 30). +Notation "'(uint8_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 3)) (Pair x (Var y))) (at level 30). +Notation "'(uint8_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 3)) (Pair (Var x) y)) (at level 30). +Notation "'(uint8_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 3)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint16_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 4)) (Pair x y)) (at level 30). +Notation "'(uint16_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 4)) (Pair x (Var y))) (at level 30). +Notation "'(uint16_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 4)) (Pair (Var x) y)) (at level 30). +Notation "'(uint16_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 4)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint32_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 5)) (Pair x y)) (at level 30). +Notation "'(uint32_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 5)) (Pair x (Var y))) (at level 30). +Notation "'(uint32_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 5)) (Pair (Var x) y)) (at level 30). +Notation "'(uint32_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 5)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint64_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 6)) (Pair x y)) (at level 30). +Notation "'(uint64_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 6)) (Pair x (Var y))) (at level 30). +Notation "'(uint64_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 6)) (Pair (Var x) y)) (at level 30). +Notation "'(uint64_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 6)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint128_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 7)) (Pair x y)) (at level 30). +Notation "'(uint128_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 30). +Notation "'(uint128_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 30). +Notation "'(uint128_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 30). +Notation Return x := (Var x). +Notation C_like := (Expr base_type op _). |