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 "T0 x , T1 y = A ; b" (at level 200, b at level 200, format "T0  x ,  T1  y  =  A ; '//' b").
Reserved Notation "v == 0 ? a : b" (at level 40, a at level 10, b at level 10).
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.
Notation "T0 x , T1 y = A ; b" := (LetIn (tx:=Prod T0 T1) A (fun '((x, y)%core) => 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:
<<
#!/usr/bin/env python
# -*- coding: utf-8 -*-
types = ('int', 'int', 'int', 'int', 'int', 'int', 'long', 'uint128_t', 'uint256_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 "'uint256_t'" := (Tbase (TWord 8)).
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 "'(uint256_t)' x * '(uint256_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 8)) (Pair x y)) (at level 40).
Notation "'(uint256_t)' x * '(uint256_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 40).
Notation "'(uint256_t)' x * '(uint256_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 40).
Notation "'(uint256_t)' x * '(uint256_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 40).
Notation "x * '(uint256_t)' y" := (Op (Mul (TWord 8) (TWord _) (TWord 8)) (Pair x y)) (at level 40).
Notation "'(uint256_t)' x * y" := (Op (Mul (TWord _) (TWord 8) (TWord 8)) (Pair x y)) (at level 40).
Notation "x * '(uint256_t)' y" := (Op (Mul (TWord 8) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 40).
Notation "'(uint256_t)' x * y" := (Op (Mul (TWord _) (TWord 8) (TWord 8)) (Pair x (Var y))) (at level 40).
Notation "x * '(uint256_t)' y" := (Op (Mul (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 40).
Notation "'(uint256_t)' x * y" := (Op (Mul (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) y)) (at level 40).
Notation "x * '(uint256_t)' y" := (Op (Mul (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 40).
Notation "'(uint256_t)' x * y" := (Op (Mul (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) (Var y))) (at level 40).
Notation "x * y" := (Op (Mul (TWord 8) (TWord 8) (TWord 8)) (Pair x y)).
Notation "x * y" := (Op (Mul (TWord 8) (TWord 8) (TWord 8)) (Pair x (Var y))).
Notation "x * y" := (Op (Mul (TWord 8) (TWord 8) (TWord 8)) (Pair (Var x) y)).
Notation "x * y" := (Op (Mul (TWord 8) (TWord 8) (TWord 8)) (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 "'(uint256_t)' x + '(uint256_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 8)) (Pair x y)) (at level 50).
Notation "'(uint256_t)' x + '(uint256_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 50).
Notation "'(uint256_t)' x + '(uint256_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 50).
Notation "'(uint256_t)' x + '(uint256_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 50).
Notation "x + '(uint256_t)' y" := (Op (Add (TWord 8) (TWord _) (TWord 8)) (Pair x y)) (at level 50).
Notation "'(uint256_t)' x + y" := (Op (Add (TWord _) (TWord 8) (TWord 8)) (Pair x y)) (at level 50).
Notation "x + '(uint256_t)' y" := (Op (Add (TWord 8) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 50).
Notation "'(uint256_t)' x + y" := (Op (Add (TWord _) (TWord 8) (TWord 8)) (Pair x (Var y))) (at level 50).
Notation "x + '(uint256_t)' y" := (Op (Add (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 50).
Notation "'(uint256_t)' x + y" := (Op (Add (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) y)) (at level 50).
Notation "x + '(uint256_t)' y" := (Op (Add (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 50).
Notation "'(uint256_t)' x + y" := (Op (Add (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) (Var y))) (at level 50).
Notation "x + y" := (Op (Add (TWord 8) (TWord 8) (TWord 8)) (Pair x y)).
Notation "x + y" := (Op (Add (TWord 8) (TWord 8) (TWord 8)) (Pair x (Var y))).
Notation "x + y" := (Op (Add (TWord 8) (TWord 8) (TWord 8)) (Pair (Var x) y)).
Notation "x + y" := (Op (Add (TWord 8) (TWord 8) (TWord 8)) (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 "'(uint256_t)' x - '(uint256_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 8)) (Pair x y)) (at level 50).
Notation "'(uint256_t)' x - '(uint256_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 50).
Notation "'(uint256_t)' x - '(uint256_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 50).
Notation "'(uint256_t)' x - '(uint256_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 50).
Notation "x - '(uint256_t)' y" := (Op (Sub (TWord 8) (TWord _) (TWord 8)) (Pair x y)) (at level 50).
Notation "'(uint256_t)' x - y" := (Op (Sub (TWord _) (TWord 8) (TWord 8)) (Pair x y)) (at level 50).
Notation "x - '(uint256_t)' y" := (Op (Sub (TWord 8) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 50).
Notation "'(uint256_t)' x - y" := (Op (Sub (TWord _) (TWord 8) (TWord 8)) (Pair x (Var y))) (at level 50).
Notation "x - '(uint256_t)' y" := (Op (Sub (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 50).
Notation "'(uint256_t)' x - y" := (Op (Sub (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) y)) (at level 50).
Notation "x - '(uint256_t)' y" := (Op (Sub (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 50).
Notation "'(uint256_t)' x - y" := (Op (Sub (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) (Var y))) (at level 50).
Notation "x - y" := (Op (Sub (TWord 8) (TWord 8) (TWord 8)) (Pair x y)).
Notation "x - y" := (Op (Sub (TWord 8) (TWord 8) (TWord 8)) (Pair x (Var y))).
Notation "x - y" := (Op (Sub (TWord 8) (TWord 8) (TWord 8)) (Pair (Var x) y)).
Notation "x - y" := (Op (Sub (TWord 8) (TWord 8) (TWord 8)) (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 "'(uint256_t)' x & '(uint256_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 8)) (Pair x y)) (at level 40).
Notation "'(uint256_t)' x & '(uint256_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 40).
Notation "'(uint256_t)' x & '(uint256_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 40).
Notation "'(uint256_t)' x & '(uint256_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 40).
Notation "x & '(uint256_t)' y" := (Op (Land (TWord 8) (TWord _) (TWord 8)) (Pair x y)) (at level 40).
Notation "'(uint256_t)' x & y" := (Op (Land (TWord _) (TWord 8) (TWord 8)) (Pair x y)) (at level 40).
Notation "x & '(uint256_t)' y" := (Op (Land (TWord 8) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 40).
Notation "'(uint256_t)' x & y" := (Op (Land (TWord _) (TWord 8) (TWord 8)) (Pair x (Var y))) (at level 40).
Notation "x & '(uint256_t)' y" := (Op (Land (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 40).
Notation "'(uint256_t)' x & y" := (Op (Land (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) y)) (at level 40).
Notation "x & '(uint256_t)' y" := (Op (Land (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 40).
Notation "'(uint256_t)' x & y" := (Op (Land (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) (Var y))) (at level 40).
Notation "x & y" := (Op (Land (TWord 8) (TWord 8) (TWord 8)) (Pair x y)).
Notation "x & y" := (Op (Land (TWord 8) (TWord 8) (TWord 8)) (Pair x (Var y))).
Notation "x & y" := (Op (Land (TWord 8) (TWord 8) (TWord 8)) (Pair (Var x) y)).
Notation "x & y" := (Op (Land (TWord 8) (TWord 8) (TWord 8)) (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 "'(uint256_t)' x << '(uint256_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 8)) (Pair x y)) (at level 30).
Notation "'(uint256_t)' x << '(uint256_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 30).
Notation "'(uint256_t)' x << '(uint256_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 30).
Notation "'(uint256_t)' x << '(uint256_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 30).
Notation "x << '(uint256_t)' y" := (Op (Shl (TWord 8) (TWord _) (TWord 8)) (Pair x y)) (at level 30).
Notation "'(uint256_t)' x << y" := (Op (Shl (TWord _) (TWord 8) (TWord 8)) (Pair x y)) (at level 30).
Notation "x << '(uint256_t)' y" := (Op (Shl (TWord 8) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 30).
Notation "'(uint256_t)' x << y" := (Op (Shl (TWord _) (TWord 8) (TWord 8)) (Pair x (Var y))) (at level 30).
Notation "x << '(uint256_t)' y" := (Op (Shl (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 30).
Notation "'(uint256_t)' x << y" := (Op (Shl (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) y)) (at level 30).
Notation "x << '(uint256_t)' y" := (Op (Shl (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 30).
Notation "'(uint256_t)' x << y" := (Op (Shl (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) (Var y))) (at level 30).
Notation "x << y" := (Op (Shl (TWord 8) (TWord 8) (TWord 8)) (Pair x y)).
Notation "x << y" := (Op (Shl (TWord 8) (TWord 8) (TWord 8)) (Pair x (Var y))).
Notation "x << y" := (Op (Shl (TWord 8) (TWord 8) (TWord 8)) (Pair (Var x) y)).
Notation "x << y" := (Op (Shl (TWord 8) (TWord 8) (TWord 8)) (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 "'(uint256_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 8)) (Pair x y)) (at level 30).
Notation "'(uint256_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 30).
Notation "'(uint256_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 30).
Notation "'(uint256_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 30).
Notation Return x := (Var x).
Notation Java_like := (Expr base_type op _).