diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-10 15:09:18 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-10 15:09:18 -0500 |
| commit | 78cd7077c6fbaba2d1af540ba622db2ea03a3fbb (patch) | |
| tree | a4b9762a2fe47731eda8dd9e8497e3c475b424dc /src | |
| parent | 6cd81910217d155564c7c2f0070b20229def2550 (diff) | |
Add more fine-grained cmovnz notations
Builds, but haven't tested the output
This closes #265
Diffstat (limited to 'src')
| -rw-r--r-- | src/Compilers/Z/CNotations.v | 951 |
1 files changed, 789 insertions, 162 deletions
diff --git a/src/Compilers/Z/CNotations.v b/src/Compilers/Z/CNotations.v index 0d9b10576..33535c01d 100644 --- a/src/Compilers/Z/CNotations.v +++ b/src/Compilers/Z/CNotations.v @@ -87,6 +87,9 @@ Reserved Notation "'mulx_u32ℤ' ( a , b )" (format "'mulx_u32ℤ' ( a , b )"). Reserved Notation "'mulx_u64ℤ' ( a , b )" (format "'mulx_u64ℤ' ( a , b )"). Reserved Notation "'mulx_u128ℤ' ( a , b )" (format "'mulx_u128ℤ' ( a , b )"). +Reserved Notation "'cmovznz32' ( v , a , b )" (format "'cmovznz32' ( v , a , b )"). +Reserved Notation "'cmovznz64' ( v , a , b )" (format "'cmovznz64' ( v , a , b )"). +Reserved Notation "'cmovznz128' ( v , a , b )" (format "'cmovznz128' ( v , a , b )"). Reserved Notation "'cmovznz' ( v , a , b )" (format "'cmovznz' ( v , a , b )"). Reserved Notation "'cmovznzℤ' ( v , a , b )" (format "'cmovznzℤ' ( v , a , b )"). (* python: @@ -186,6 +189,9 @@ Reserved Notation "'mulx_u32ℤ' ( a , b )" (format "'mulx_u32ℤ' ( a , b )"). Reserved Notation "'mulx_u64ℤ' ( a , b )" (format "'mulx_u64ℤ' ( a , b )"). Reserved Notation "'mulx_u128ℤ' ( a , b )" (format "'mulx_u128ℤ' ( a , b )"). +Reserved Notation "'cmovznz32' ( v , a , b )" (format "'cmovznz32' ( v , a , b )"). +Reserved Notation "'cmovznz64' ( v , a , b )" (format "'cmovznz64' ( v , a , b )"). +Reserved Notation "'cmovznz128' ( v , a , b )" (format "'cmovznz128' ( v , a , b )"). Reserved Notation "'cmovznz' ( v , a , b )" (format "'cmovznz' ( v , a , b )"). Reserved Notation "'cmovznzℤ' ( v , a , b )" (format "'cmovznzℤ' ( v , a , b )"). (""" + r"""* python: @@ -296,17 +302,38 @@ for v0 in (False, True): tes = ('v' if not v0 else '(Var v)') lhs = ('x' if not v1 else '(Var x)') rhs = ('y' if not v2 else '(Var y)') - print('Notation "\'cmovznz\' ( v , x , y )" := (Op (Zselect _ _ _ _) (Pair (Pair %s %s) %s)).' % (tes, lhs, rhs)) + print('Notation "\'cmovznz32\' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord _) (TWord _)) (Pair (Pair %s %s) %s)).' % (tes, lhs, rhs)) +for (wordsz, cmovsz) in ((16,'32'), (32,'64'), (64,'128'), (128,'ℤ')): + lgwordsz = log2_up(wordsz) + for lgwordsz_out in range(0, lgwordsz+2): # + 2 so that we get one instance of lgwordsz_out > lgwordsz + for v0 in (False, True): + for v1 in (False, True): + for v2 in (False, True): + tes = ('v' if not v0 else '(Var v)') + lhs = ('x' if not v1 else '(Var x)') + rhs = ('y' if not v2 else '(Var y)') + TWordSz = TWord(at_least_S_pattern(lgwordsz+1)) # + 1, because we need strictly not equal + TWordSz_out = TWord(at_least_S_pattern(lgwordsz_out)) + if lgwordsz_out > lgwordsz: + pat = 'Notation "\'cmovznz%s\' ( v , x , y )" := (Op (Zselect %s %s %s %s) (Pair (Pair %s %s) %s)).' + print(pat % (cmovsz, TWordSz, TWord(_), TWord(_), TWordSz_out, tes, lhs, rhs)) + print(pat % (cmovsz, TWord(_), TWordSz, TWord(_), TWordSz_out, tes, lhs, rhs)) + print(pat % (cmovsz, TWord(_), TWord(_), TWordSz, TWordSz_out, tes, lhs, rhs)) + else: + pat = 'Notation "\'(%s)\' \'cmovznz%s\' ( v , x , y )" := (Op (Zselect %s %s %s %s) (Pair (Pair %s %s) %s)) (format "\'(%s)\' \'cmovznz%s\' ( v , x , y )").' + print(pat % (types[lgwordsz_out], cmovsz, TWordSz, TWord(_), TWord(_), TWordSz_out, tes, lhs, rhs, types[lgwordsz_out], cmovsz)) + print(pat % (types[lgwordsz_out], cmovsz, TWord(_), TWordSz, TWord(_), TWordSz_out, tes, lhs, rhs, types[lgwordsz_out], cmovsz)) + print(pat % (types[lgwordsz_out], cmovsz, TWord(_), TWord(_), TWordSz, TWordSz_out, tes, lhs, rhs, types[lgwordsz_out], cmovsz)) +for v0 in (False, True): + for v1 in (False, True): + for v2 in (False, True): + tes = ('v' if not v0 else '(Var v)') + lhs = ('x' if not v1 else '(Var x)') + rhs = ('y' if not v2 else '(Var y)') + print('Notation "\'cmovznzℤ\' ( v , x , y )" := (Op (Zselect TZ _ _ _) (Pair (Pair %s %s) %s)).' % (tes, lhs, rhs)) + print('Notation "\'cmovznzℤ\' ( v , x , y )" := (Op (Zselect _ TZ _ _) (Pair (Pair %s %s) %s)).' % (tes, lhs, rhs)) + print('Notation "\'cmovznzℤ\' ( v , x , y )" := (Op (Zselect _ _ TZ _) (Pair (Pair %s %s) %s)).' % (tes, lhs, rhs)) print('Notation "\'cmovznzℤ\' ( v , x , y )" := (Op (Zselect _ _ _ TZ) (Pair (Pair %s %s) %s)).' % (tes, lhs, rhs)) -for lgwordsz in range(0, len(types)): - for v0 in (False, True): - for v1 in (False, True): - for v2 in (False, True): - tes = ('v' if not v0 else '(Var v)') - lhs = ('x' if not v1 else '(Var x)') - rhs = ('y' if not v2 else '(Var y)') - print('Notation "\'(%s)\' \'cmovznz\' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord %d)) (Pair (Pair %s %s) %s)) (format "\'(%s)\' \'cmovznz\' ( v , x , y )").' % (types[lgwordsz], lgwordsz, tes, lhs, rhs, types[lgwordsz])) - print('Notation "\'cmovznz\' ( v , x , y )" := (Op (Zselect _ (TWord %d) (TWord %d) (TWord %d)) (Pair (Pair %s %s) %s)).' % (lgwordsz, lgwordsz, lgwordsz, tes, lhs, rhs)) for opn, op in (('addcarryx', 'AddWithGetCarry'), ('subborrow', 'SubWithGetBorrow')): for wordsz in (32, 64, 128, 51): lgwordsz = log2_up(wordsz) @@ -1740,166 +1767,766 @@ Notation "'(uint256_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 8)) ( Notation "( x >> y )" := (Op (Shr (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) y)) (format "( x >> y )"). Notation "'(uint256_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 30). Notation "( x >> y )" := (Op (Shr (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (format "( x >> y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ _ _ _) (Pair (Pair v x) y)). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord _) (TWord _)) (Pair (Pair v x) y)). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord _) (TWord _)) (Pair (Pair v x) (Var y))). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord _) (TWord _)) (Pair (Pair v (Var x)) y)). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord _) (TWord _)) (Pair (Pair v (Var x)) (Var y))). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord _) (TWord _)) (Pair (Pair (Var v) x) y)). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord _) (TWord _)) (Pair (Pair (Var v) x) (Var y))). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord _) (TWord _)) (Pair (Pair (Var v) (Var x)) y)). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord _) (TWord _)) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'(bool)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair v x) y)) (format "'(bool)' 'cmovznz32' ( v , x , y )"). +Notation "'(bool)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _)) (Pair (Pair v x) y)) (format "'(bool)' 'cmovznz32' ( v , x , y )"). +Notation "'(bool)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _)) (Pair (Pair v x) y)) (format "'(bool)' 'cmovznz32' ( v , x , y )"). +Notation "'(bool)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair v x) (Var y))) (format "'(bool)' 'cmovznz32' ( v , x , y )"). +Notation "'(bool)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _)) (Pair (Pair v x) (Var y))) (format "'(bool)' 'cmovznz32' ( v , x , y )"). +Notation "'(bool)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _)) (Pair (Pair v x) (Var y))) (format "'(bool)' 'cmovznz32' ( v , x , y )"). +Notation "'(bool)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair v (Var x)) y)) (format "'(bool)' 'cmovznz32' ( v , x , y )"). +Notation "'(bool)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _)) (Pair (Pair v (Var x)) y)) (format "'(bool)' 'cmovznz32' ( v , x , y )"). +Notation "'(bool)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _)) (Pair (Pair v (Var x)) y)) (format "'(bool)' 'cmovznz32' ( v , x , y )"). +Notation "'(bool)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair v (Var x)) (Var y))) (format "'(bool)' 'cmovznz32' ( v , x , y )"). +Notation "'(bool)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _)) (Pair (Pair v (Var x)) (Var y))) (format "'(bool)' 'cmovznz32' ( v , x , y )"). +Notation "'(bool)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _)) (Pair (Pair v (Var x)) (Var y))) (format "'(bool)' 'cmovznz32' ( v , x , y )"). +Notation "'(bool)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair (Var v) x) y)) (format "'(bool)' 'cmovznz32' ( v , x , y )"). +Notation "'(bool)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _)) (Pair (Pair (Var v) x) y)) (format "'(bool)' 'cmovznz32' ( v , x , y )"). +Notation "'(bool)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _)) (Pair (Pair (Var v) x) y)) (format "'(bool)' 'cmovznz32' ( v , x , y )"). +Notation "'(bool)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair (Var v) x) (Var y))) (format "'(bool)' 'cmovznz32' ( v , x , y )"). +Notation "'(bool)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _)) (Pair (Pair (Var v) x) (Var y))) (format "'(bool)' 'cmovznz32' ( v , x , y )"). +Notation "'(bool)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _)) (Pair (Pair (Var v) x) (Var y))) (format "'(bool)' 'cmovznz32' ( v , x , y )"). +Notation "'(bool)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair (Var v) (Var x)) y)) (format "'(bool)' 'cmovznz32' ( v , x , y )"). +Notation "'(bool)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _)) (Pair (Pair (Var v) (Var x)) y)) (format "'(bool)' 'cmovznz32' ( v , x , y )"). +Notation "'(bool)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _)) (Pair (Pair (Var v) (Var x)) y)) (format "'(bool)' 'cmovznz32' ( v , x , y )"). +Notation "'(bool)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(bool)' 'cmovznz32' ( v , x , y )"). +Notation "'(bool)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(bool)' 'cmovznz32' ( v , x , y )"). +Notation "'(bool)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(bool)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S _))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S _))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S _))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S _))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S _))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S _))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S _))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S _))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S _))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S _))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S _))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S _))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S _))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S _))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S _))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S _))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S _)))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S _)))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S _)))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S _)))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S _)))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S _)))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S _)))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S _)))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S _)))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S _)))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S _)))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S _)))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S (S _))))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S (S _))))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S (S _))))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S (S _))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S (S _))))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S (S _))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S (S _))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S (S _))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v x) y)) (format "'(uint16_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v x) y)) (format "'(uint16_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S (S (S _)))))) (Pair (Pair v x) y)) (format "'(uint16_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v x) (Var y))) (format "'(uint16_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v x) (Var y))) (format "'(uint16_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S (S (S _)))))) (Pair (Pair v x) (Var y))) (format "'(uint16_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v (Var x)) y)) (format "'(uint16_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v (Var x)) y)) (format "'(uint16_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S (S (S _)))))) (Pair (Pair v (Var x)) y)) (format "'(uint16_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint16_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint16_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S (S (S _)))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint16_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) x) y)) (format "'(uint16_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) x) y)) (format "'(uint16_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) x) y)) (format "'(uint16_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint16_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint16_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint16_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint16_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint16_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint16_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint16_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint16_t)' 'cmovznz32' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint16_t)' 'cmovznz32' ( v , x , y )"). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v x) y)). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v x) y)). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair v x) y)). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v x) (Var y))). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v x) (Var y))). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair v x) (Var y))). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v (Var x)) y)). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v (Var x)) y)). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair v (Var x)) y)). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v (Var x)) (Var y))). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v (Var x)) (Var y))). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair v (Var x)) (Var y))). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) x) y)). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) x) y)). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) x) y)). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) x) (Var y))). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) x) (Var y))). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) x) (Var y))). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) (Var x)) y)). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) (Var x)) y)). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) (Var x)) y)). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S _)))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S _)))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'cmovznz32' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S _)))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'(bool)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair v x) y)) (format "'(bool)' 'cmovznz64' ( v , x , y )"). +Notation "'(bool)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _)) (Pair (Pair v x) y)) (format "'(bool)' 'cmovznz64' ( v , x , y )"). +Notation "'(bool)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _)) (Pair (Pair v x) y)) (format "'(bool)' 'cmovznz64' ( v , x , y )"). +Notation "'(bool)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair v x) (Var y))) (format "'(bool)' 'cmovznz64' ( v , x , y )"). +Notation "'(bool)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _)) (Pair (Pair v x) (Var y))) (format "'(bool)' 'cmovznz64' ( v , x , y )"). +Notation "'(bool)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _)) (Pair (Pair v x) (Var y))) (format "'(bool)' 'cmovznz64' ( v , x , y )"). +Notation "'(bool)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair v (Var x)) y)) (format "'(bool)' 'cmovznz64' ( v , x , y )"). +Notation "'(bool)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _)) (Pair (Pair v (Var x)) y)) (format "'(bool)' 'cmovznz64' ( v , x , y )"). +Notation "'(bool)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _)) (Pair (Pair v (Var x)) y)) (format "'(bool)' 'cmovznz64' ( v , x , y )"). +Notation "'(bool)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair v (Var x)) (Var y))) (format "'(bool)' 'cmovznz64' ( v , x , y )"). +Notation "'(bool)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _)) (Pair (Pair v (Var x)) (Var y))) (format "'(bool)' 'cmovznz64' ( v , x , y )"). +Notation "'(bool)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _)) (Pair (Pair v (Var x)) (Var y))) (format "'(bool)' 'cmovznz64' ( v , x , y )"). +Notation "'(bool)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair (Var v) x) y)) (format "'(bool)' 'cmovznz64' ( v , x , y )"). +Notation "'(bool)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _)) (Pair (Pair (Var v) x) y)) (format "'(bool)' 'cmovznz64' ( v , x , y )"). +Notation "'(bool)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _)) (Pair (Pair (Var v) x) y)) (format "'(bool)' 'cmovznz64' ( v , x , y )"). +Notation "'(bool)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair (Var v) x) (Var y))) (format "'(bool)' 'cmovznz64' ( v , x , y )"). +Notation "'(bool)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _)) (Pair (Pair (Var v) x) (Var y))) (format "'(bool)' 'cmovznz64' ( v , x , y )"). +Notation "'(bool)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _)) (Pair (Pair (Var v) x) (Var y))) (format "'(bool)' 'cmovznz64' ( v , x , y )"). +Notation "'(bool)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair (Var v) (Var x)) y)) (format "'(bool)' 'cmovznz64' ( v , x , y )"). +Notation "'(bool)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _)) (Pair (Pair (Var v) (Var x)) y)) (format "'(bool)' 'cmovznz64' ( v , x , y )"). +Notation "'(bool)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _)) (Pair (Pair (Var v) (Var x)) y)) (format "'(bool)' 'cmovznz64' ( v , x , y )"). +Notation "'(bool)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(bool)' 'cmovznz64' ( v , x , y )"). +Notation "'(bool)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(bool)' 'cmovznz64' ( v , x , y )"). +Notation "'(bool)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(bool)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S _))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S _))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S _))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S _))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S _))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S _))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S _))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S _))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S _))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S _))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S _))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S _))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S _))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S _))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S _))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S _))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S _)))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S _)))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S _)))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S _)))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S _)))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S _)))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S _)))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S _)))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S _)))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S _)))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S _)))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S _)))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S _))))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S _))))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S _))))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S _))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S _))))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S _))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S _))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S _))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v x) y)) (format "'(uint16_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v x) y)) (format "'(uint16_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S (S _)))))) (Pair (Pair v x) y)) (format "'(uint16_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v x) (Var y))) (format "'(uint16_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v x) (Var y))) (format "'(uint16_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S (S _)))))) (Pair (Pair v x) (Var y))) (format "'(uint16_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v (Var x)) y)) (format "'(uint16_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v (Var x)) y)) (format "'(uint16_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S (S _)))))) (Pair (Pair v (Var x)) y)) (format "'(uint16_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint16_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint16_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S (S _)))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint16_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) x) y)) (format "'(uint16_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) x) y)) (format "'(uint16_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) x) y)) (format "'(uint16_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint16_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint16_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint16_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint16_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint16_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint16_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint16_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint16_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint16_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v x) y)) (format "'(uint32_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v x) y)) (format "'(uint32_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair v x) y)) (format "'(uint32_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v x) (Var y))) (format "'(uint32_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v x) (Var y))) (format "'(uint32_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair v x) (Var y))) (format "'(uint32_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v (Var x)) y)) (format "'(uint32_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v (Var x)) y)) (format "'(uint32_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair v (Var x)) y)) (format "'(uint32_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint32_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint32_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint32_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) x) y)) (format "'(uint32_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) x) y)) (format "'(uint32_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) x) y)) (format "'(uint32_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint32_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint32_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint32_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint32_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint32_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint32_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint32_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint32_t)' 'cmovznz64' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint32_t)' 'cmovznz64' ( v , x , y )"). +Notation "'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v x) y)). +Notation "'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v x) y)). +Notation "'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v x) y)). +Notation "'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v x) (Var y))). +Notation "'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v x) (Var y))). +Notation "'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v x) (Var y))). +Notation "'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v (Var x)) y)). +Notation "'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v (Var x)) y)). +Notation "'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v (Var x)) y)). +Notation "'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v (Var x)) (Var y))). +Notation "'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v (Var x)) (Var y))). +Notation "'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v (Var x)) (Var y))). +Notation "'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) x) y)). +Notation "'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) x) y)). +Notation "'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) x) y)). +Notation "'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) x) (Var y))). +Notation "'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) x) (Var y))). +Notation "'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) x) (Var y))). +Notation "'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) (Var x)) y)). +Notation "'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) (Var x)) y)). +Notation "'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) (Var x)) y)). +Notation "'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'cmovznz64' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S _))))))) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'(bool)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair v x) y)) (format "'(bool)' 'cmovznz128' ( v , x , y )"). +Notation "'(bool)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _)) (Pair (Pair v x) y)) (format "'(bool)' 'cmovznz128' ( v , x , y )"). +Notation "'(bool)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _)) (Pair (Pair v x) y)) (format "'(bool)' 'cmovznz128' ( v , x , y )"). +Notation "'(bool)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair v x) (Var y))) (format "'(bool)' 'cmovznz128' ( v , x , y )"). +Notation "'(bool)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _)) (Pair (Pair v x) (Var y))) (format "'(bool)' 'cmovznz128' ( v , x , y )"). +Notation "'(bool)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _)) (Pair (Pair v x) (Var y))) (format "'(bool)' 'cmovznz128' ( v , x , y )"). +Notation "'(bool)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair v (Var x)) y)) (format "'(bool)' 'cmovznz128' ( v , x , y )"). +Notation "'(bool)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _)) (Pair (Pair v (Var x)) y)) (format "'(bool)' 'cmovznz128' ( v , x , y )"). +Notation "'(bool)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _)) (Pair (Pair v (Var x)) y)) (format "'(bool)' 'cmovznz128' ( v , x , y )"). +Notation "'(bool)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair v (Var x)) (Var y))) (format "'(bool)' 'cmovznz128' ( v , x , y )"). +Notation "'(bool)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _)) (Pair (Pair v (Var x)) (Var y))) (format "'(bool)' 'cmovznz128' ( v , x , y )"). +Notation "'(bool)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _)) (Pair (Pair v (Var x)) (Var y))) (format "'(bool)' 'cmovznz128' ( v , x , y )"). +Notation "'(bool)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair (Var v) x) y)) (format "'(bool)' 'cmovznz128' ( v , x , y )"). +Notation "'(bool)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _)) (Pair (Pair (Var v) x) y)) (format "'(bool)' 'cmovznz128' ( v , x , y )"). +Notation "'(bool)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _)) (Pair (Pair (Var v) x) y)) (format "'(bool)' 'cmovznz128' ( v , x , y )"). +Notation "'(bool)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair (Var v) x) (Var y))) (format "'(bool)' 'cmovznz128' ( v , x , y )"). +Notation "'(bool)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _)) (Pair (Pair (Var v) x) (Var y))) (format "'(bool)' 'cmovznz128' ( v , x , y )"). +Notation "'(bool)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _)) (Pair (Pair (Var v) x) (Var y))) (format "'(bool)' 'cmovznz128' ( v , x , y )"). +Notation "'(bool)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair (Var v) (Var x)) y)) (format "'(bool)' 'cmovznz128' ( v , x , y )"). +Notation "'(bool)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _)) (Pair (Pair (Var v) (Var x)) y)) (format "'(bool)' 'cmovznz128' ( v , x , y )"). +Notation "'(bool)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _)) (Pair (Pair (Var v) (Var x)) y)) (format "'(bool)' 'cmovznz128' ( v , x , y )"). +Notation "'(bool)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(bool)' 'cmovznz128' ( v , x , y )"). +Notation "'(bool)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(bool)' 'cmovznz128' ( v , x , y )"). +Notation "'(bool)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(bool)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S _))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S _))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S _))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S _))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S _))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S _))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S _))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S _))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S _))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S _))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S _))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S _))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S _))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S _))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S _))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S _))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S _)))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S _)))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S _)))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S _)))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S _)))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S _)))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S _)))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S _)))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S _)))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S _)))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S _)))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S _)))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S _))))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S _))))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S _))))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S _))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S _))))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S _))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S _))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S _))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v x) y)) (format "'(uint16_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v x) y)) (format "'(uint16_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S _)))))) (Pair (Pair v x) y)) (format "'(uint16_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v x) (Var y))) (format "'(uint16_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v x) (Var y))) (format "'(uint16_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S _)))))) (Pair (Pair v x) (Var y))) (format "'(uint16_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v (Var x)) y)) (format "'(uint16_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v (Var x)) y)) (format "'(uint16_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S _)))))) (Pair (Pair v (Var x)) y)) (format "'(uint16_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint16_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint16_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S _)))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint16_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) x) y)) (format "'(uint16_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) x) y)) (format "'(uint16_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) x) y)) (format "'(uint16_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint16_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint16_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint16_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint16_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint16_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint16_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint16_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint16_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint16_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v x) y)) (format "'(uint32_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v x) y)) (format "'(uint32_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair v x) y)) (format "'(uint32_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v x) (Var y))) (format "'(uint32_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v x) (Var y))) (format "'(uint32_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair v x) (Var y))) (format "'(uint32_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v (Var x)) y)) (format "'(uint32_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v (Var x)) y)) (format "'(uint32_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair v (Var x)) y)) (format "'(uint32_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint32_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint32_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint32_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) x) y)) (format "'(uint32_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) x) y)) (format "'(uint32_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) x) y)) (format "'(uint32_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint32_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint32_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint32_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint32_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint32_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint32_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint32_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint32_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint32_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v x) y)) (format "'(uint64_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v x) y)) (format "'(uint64_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v x) y)) (format "'(uint64_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v x) (Var y))) (format "'(uint64_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v x) (Var y))) (format "'(uint64_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v x) (Var y))) (format "'(uint64_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v (Var x)) y)) (format "'(uint64_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v (Var x)) y)) (format "'(uint64_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v (Var x)) y)) (format "'(uint64_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint64_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint64_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint64_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) x) y)) (format "'(uint64_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) x) y)) (format "'(uint64_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) x) y)) (format "'(uint64_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint64_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint64_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint64_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint64_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint64_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint64_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint64_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint64_t)' 'cmovznz128' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint64_t)' 'cmovznz128' ( v , x , y )"). +Notation "'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair v x) y)). +Notation "'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair v x) y)). +Notation "'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair v x) y)). +Notation "'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair v x) (Var y))). +Notation "'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair v x) (Var y))). +Notation "'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair v x) (Var y))). +Notation "'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair v (Var x)) y)). +Notation "'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair v (Var x)) y)). +Notation "'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair v (Var x)) y)). +Notation "'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair v (Var x)) (Var y))). +Notation "'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair v (Var x)) (Var y))). +Notation "'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair v (Var x)) (Var y))). +Notation "'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair (Var v) x) y)). +Notation "'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair (Var v) x) y)). +Notation "'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair (Var v) x) y)). +Notation "'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair (Var v) x) (Var y))). +Notation "'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair (Var v) x) (Var y))). +Notation "'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair (Var v) x) (Var y))). +Notation "'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair (Var v) (Var x)) y)). +Notation "'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair (Var v) (Var x)) y)). +Notation "'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair (Var v) (Var x)) y)). +Notation "'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'cmovznz128' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _)))))))) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'(bool)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair v x) y)) (format "'(bool)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(bool)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _)) (Pair (Pair v x) y)) (format "'(bool)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(bool)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _)) (Pair (Pair v x) y)) (format "'(bool)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(bool)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair v x) (Var y))) (format "'(bool)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(bool)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _)) (Pair (Pair v x) (Var y))) (format "'(bool)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(bool)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _)) (Pair (Pair v x) (Var y))) (format "'(bool)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(bool)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair v (Var x)) y)) (format "'(bool)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(bool)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _)) (Pair (Pair v (Var x)) y)) (format "'(bool)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(bool)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _)) (Pair (Pair v (Var x)) y)) (format "'(bool)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(bool)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair v (Var x)) (Var y))) (format "'(bool)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(bool)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _)) (Pair (Pair v (Var x)) (Var y))) (format "'(bool)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(bool)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _)) (Pair (Pair v (Var x)) (Var y))) (format "'(bool)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(bool)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair (Var v) x) y)) (format "'(bool)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(bool)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _)) (Pair (Pair (Var v) x) y)) (format "'(bool)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(bool)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _)) (Pair (Pair (Var v) x) y)) (format "'(bool)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(bool)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair (Var v) x) (Var y))) (format "'(bool)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(bool)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _)) (Pair (Pair (Var v) x) (Var y))) (format "'(bool)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(bool)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _)) (Pair (Pair (Var v) x) (Var y))) (format "'(bool)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(bool)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair (Var v) (Var x)) y)) (format "'(bool)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(bool)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _)) (Pair (Pair (Var v) (Var x)) y)) (format "'(bool)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(bool)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _)) (Pair (Pair (Var v) (Var x)) y)) (format "'(bool)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(bool)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord _)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(bool)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(bool)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(bool)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(bool)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(bool)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S _))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S _))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S _))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S _))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S _))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S _))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S _))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S _))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S _))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S _))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S _))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S _))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S _))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S _))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S _))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S _))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S _))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S _)))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S _)))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S _)))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S _)))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S _)))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S _)))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S _)))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S _)))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S _)))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S _)))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S _)))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S _)))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S _)))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S _))))) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S _))))) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S _))))) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S _))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S _))))) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S _))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S _))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S _))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint8_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S _))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v x) y)) (format "'(uint16_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v x) y)) (format "'(uint16_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S _)))))) (Pair (Pair v x) y)) (format "'(uint16_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v x) (Var y))) (format "'(uint16_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v x) (Var y))) (format "'(uint16_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S _)))))) (Pair (Pair v x) (Var y))) (format "'(uint16_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v (Var x)) y)) (format "'(uint16_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v (Var x)) y)) (format "'(uint16_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S _)))))) (Pair (Pair v (Var x)) y)) (format "'(uint16_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint16_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint16_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S _)))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint16_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) x) y)) (format "'(uint16_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) x) y)) (format "'(uint16_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) x) y)) (format "'(uint16_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint16_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint16_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint16_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint16_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint16_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint16_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint16_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint16_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint16_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S _)))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint16_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v x) y)) (format "'(uint32_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v x) y)) (format "'(uint32_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair v x) y)) (format "'(uint32_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v x) (Var y))) (format "'(uint32_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v x) (Var y))) (format "'(uint32_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair v x) (Var y))) (format "'(uint32_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v (Var x)) y)) (format "'(uint32_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v (Var x)) y)) (format "'(uint32_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair v (Var x)) y)) (format "'(uint32_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint32_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint32_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint32_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) x) y)) (format "'(uint32_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) x) y)) (format "'(uint32_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) x) y)) (format "'(uint32_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint32_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint32_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint32_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint32_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint32_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint32_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint32_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint32_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint32_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S _))))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint32_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v x) y)) (format "'(uint64_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v x) y)) (format "'(uint64_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v x) y)) (format "'(uint64_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v x) (Var y))) (format "'(uint64_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v x) (Var y))) (format "'(uint64_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v x) (Var y))) (format "'(uint64_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v (Var x)) y)) (format "'(uint64_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v (Var x)) y)) (format "'(uint64_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v (Var x)) y)) (format "'(uint64_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint64_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint64_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint64_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) x) y)) (format "'(uint64_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) x) y)) (format "'(uint64_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) x) y)) (format "'(uint64_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint64_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint64_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint64_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint64_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint64_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint64_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint64_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint64_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint64_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S (S _)))))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint64_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint128_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair v x) y)) (format "'(uint128_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint128_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair v x) y)) (format "'(uint128_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint128_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair v x) y)) (format "'(uint128_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint128_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair v x) (Var y))) (format "'(uint128_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint128_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair v x) (Var y))) (format "'(uint128_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint128_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair v x) (Var y))) (format "'(uint128_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint128_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair v (Var x)) y)) (format "'(uint128_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint128_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair v (Var x)) y)) (format "'(uint128_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint128_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair v (Var x)) y)) (format "'(uint128_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint128_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint128_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint128_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint128_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint128_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair v (Var x)) (Var y))) (format "'(uint128_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint128_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair (Var v) x) y)) (format "'(uint128_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint128_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair (Var v) x) y)) (format "'(uint128_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint128_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair (Var v) x) y)) (format "'(uint128_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint128_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint128_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint128_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint128_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint128_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair (Var v) x) (Var y))) (format "'(uint128_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint128_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint128_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint128_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint128_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint128_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint128_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint128_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint128_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint128_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint128_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'(uint128_t)' 'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S (S (S _))))))))) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint128_t)' 'cmovznzℤ' ( v , x , y )"). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _)))))))))) (Pair (Pair v x) y)). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S (S (S (S _)))))))))) (Pair (Pair v x) y)). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S (S (S (S _)))))))))) (Pair (Pair v x) y)). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _)))))))))) (Pair (Pair v x) (Var y))). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S (S (S (S _)))))))))) (Pair (Pair v x) (Var y))). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S (S (S (S _)))))))))) (Pair (Pair v x) (Var y))). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _)))))))))) (Pair (Pair v (Var x)) y)). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S (S (S (S _)))))))))) (Pair (Pair v (Var x)) y)). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S (S (S (S _)))))))))) (Pair (Pair v (Var x)) y)). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _)))))))))) (Pair (Pair v (Var x)) (Var y))). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S (S (S (S _)))))))))) (Pair (Pair v (Var x)) (Var y))). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S (S (S (S _)))))))))) (Pair (Pair v (Var x)) (Var y))). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _)))))))))) (Pair (Pair (Var v) x) y)). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S (S (S (S _)))))))))) (Pair (Pair (Var v) x) y)). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S (S (S (S _)))))))))) (Pair (Pair (Var v) x) y)). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _)))))))))) (Pair (Pair (Var v) x) (Var y))). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S (S (S (S _)))))))))) (Pair (Pair (Var v) x) (Var y))). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S (S (S (S _)))))))))) (Pair (Pair (Var v) x) (Var y))). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _)))))))))) (Pair (Pair (Var v) (Var x)) y)). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S (S (S (S _)))))))))) (Pair (Pair (Var v) (Var x)) y)). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S (S (S (S _)))))))))) (Pair (Pair (Var v) (Var x)) y)). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _)))))))))) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord _) (TWord (S (S (S (S (S (S (S (S _)))))))))) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect (TWord _) (TWord _) (TWord (S (S (S (S (S (S (S (S _))))))))) (TWord (S (S (S (S (S (S (S (S _)))))))))) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect TZ _ _ _) (Pair (Pair v x) y)). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ TZ _ _) (Pair (Pair v x) y)). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ _ TZ _) (Pair (Pair v x) y)). Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ _ _ TZ) (Pair (Pair v x) y)). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ _ _ _) (Pair (Pair v x) (Var y))). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect TZ _ _ _) (Pair (Pair v x) (Var y))). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ TZ _ _) (Pair (Pair v x) (Var y))). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ _ TZ _) (Pair (Pair v x) (Var y))). Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ _ _ TZ) (Pair (Pair v x) (Var y))). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ _ _ _) (Pair (Pair v (Var x)) y)). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect TZ _ _ _) (Pair (Pair v (Var x)) y)). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ TZ _ _) (Pair (Pair v (Var x)) y)). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ _ TZ _) (Pair (Pair v (Var x)) y)). Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ _ _ TZ) (Pair (Pair v (Var x)) y)). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ _ _ _) (Pair (Pair v (Var x)) (Var y))). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect TZ _ _ _) (Pair (Pair v (Var x)) (Var y))). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ TZ _ _) (Pair (Pair v (Var x)) (Var y))). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ _ TZ _) (Pair (Pair v (Var x)) (Var y))). Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ _ _ TZ) (Pair (Pair v (Var x)) (Var y))). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ _ _ _) (Pair (Pair (Var v) x) y)). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect TZ _ _ _) (Pair (Pair (Var v) x) y)). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ TZ _ _) (Pair (Pair (Var v) x) y)). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ _ TZ _) (Pair (Pair (Var v) x) y)). Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ _ _ TZ) (Pair (Pair (Var v) x) y)). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ _ _ _) (Pair (Pair (Var v) x) (Var y))). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect TZ _ _ _) (Pair (Pair (Var v) x) (Var y))). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ TZ _ _) (Pair (Pair (Var v) x) (Var y))). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ _ TZ _) (Pair (Pair (Var v) x) (Var y))). Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ _ _ TZ) (Pair (Pair (Var v) x) (Var y))). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ _ _ _) (Pair (Pair (Var v) (Var x)) y)). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect TZ _ _ _) (Pair (Pair (Var v) (Var x)) y)). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ TZ _ _) (Pair (Pair (Var v) (Var x)) y)). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ _ TZ _) (Pair (Pair (Var v) (Var x)) y)). Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ _ _ TZ) (Pair (Pair (Var v) (Var x)) y)). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ _ _ _) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect TZ _ _ _) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ TZ _ _) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ _ TZ _) (Pair (Pair (Var v) (Var x)) (Var y))). Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ _ _ TZ) (Pair (Pair (Var v) (Var x)) (Var y))). -Notation "'(bool)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair v x) y)) (format "'(bool)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair v x) y)). -Notation "'(bool)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair v x) (Var y))) (format "'(bool)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair v x) (Var y))). -Notation "'(bool)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair v (Var x)) y)) (format "'(bool)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair v (Var x)) y)). -Notation "'(bool)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair v (Var x)) (Var y))) (format "'(bool)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair v (Var x)) (Var y))). -Notation "'(bool)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair (Var v) x) y)) (format "'(bool)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair (Var v) x) y)). -Notation "'(bool)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair (Var v) x) (Var y))) (format "'(bool)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair (Var v) x) (Var y))). -Notation "'(bool)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair (Var v) (Var x)) y)) (format "'(bool)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair (Var v) (Var x)) y)). -Notation "'(bool)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(bool)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair (Var v) (Var x)) (Var y))). -Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair v x) y)). -Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair v x) (Var y))). -Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair v (Var x)) y)). -Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair v (Var x)) (Var y))). -Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair (Var v) x) y)). -Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair (Var v) x) (Var y))). -Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair (Var v) (Var x)) y)). -Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair (Var v) (Var x)) (Var y))). -Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair v x) y)). -Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair v x) (Var y))). -Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair v (Var x)) y)). -Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair v (Var x)) (Var y))). -Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair (Var v) x) y)). -Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair (Var v) x) (Var y))). -Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair (Var v) (Var x)) y)). -Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair (Var v) (Var x)) (Var y))). -Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair v x) y)). -Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair v x) (Var y))). -Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair v (Var x)) y)). -Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair v (Var x)) (Var y))). -Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair (Var v) x) y)). -Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair (Var v) x) (Var y))). -Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair (Var v) (Var x)) y)). -Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair (Var v) (Var x)) (Var y))). -Notation "'(uint16_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair v x) y)) (format "'(uint16_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair v x) y)). -Notation "'(uint16_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair v x) (Var y))) (format "'(uint16_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair v x) (Var y))). -Notation "'(uint16_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair v (Var x)) y)) (format "'(uint16_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair v (Var x)) y)). -Notation "'(uint16_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair v (Var x)) (Var y))) (format "'(uint16_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair v (Var x)) (Var y))). -Notation "'(uint16_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair (Var v) x) y)) (format "'(uint16_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair (Var v) x) y)). -Notation "'(uint16_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair (Var v) x) (Var y))) (format "'(uint16_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair (Var v) x) (Var y))). -Notation "'(uint16_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint16_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair (Var v) (Var x)) y)). -Notation "'(uint16_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint16_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair (Var v) (Var x)) (Var y))). -Notation "'(uint32_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair v x) y)) (format "'(uint32_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair v x) y)). -Notation "'(uint32_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair v x) (Var y))) (format "'(uint32_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair v x) (Var y))). -Notation "'(uint32_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair v (Var x)) y)) (format "'(uint32_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair v (Var x)) y)). -Notation "'(uint32_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair v (Var x)) (Var y))) (format "'(uint32_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair v (Var x)) (Var y))). -Notation "'(uint32_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair (Var v) x) y)) (format "'(uint32_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair (Var v) x) y)). -Notation "'(uint32_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair (Var v) x) (Var y))) (format "'(uint32_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair (Var v) x) (Var y))). -Notation "'(uint32_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint32_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair (Var v) (Var x)) y)). -Notation "'(uint32_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint32_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair (Var v) (Var x)) (Var y))). -Notation "'(uint64_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair v x) y)) (format "'(uint64_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair v x) y)). -Notation "'(uint64_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair v x) (Var y))) (format "'(uint64_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair v x) (Var y))). -Notation "'(uint64_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair v (Var x)) y)) (format "'(uint64_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair v (Var x)) y)). -Notation "'(uint64_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair v (Var x)) (Var y))) (format "'(uint64_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair v (Var x)) (Var y))). -Notation "'(uint64_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair (Var v) x) y)) (format "'(uint64_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair (Var v) x) y)). -Notation "'(uint64_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair (Var v) x) (Var y))) (format "'(uint64_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair (Var v) x) (Var y))). -Notation "'(uint64_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint64_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair (Var v) (Var x)) y)). -Notation "'(uint64_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint64_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair (Var v) (Var x)) (Var y))). -Notation "'(uint128_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair v x) y)) (format "'(uint128_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair v x) y)). -Notation "'(uint128_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair v x) (Var y))) (format "'(uint128_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair v x) (Var y))). -Notation "'(uint128_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair v (Var x)) y)) (format "'(uint128_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair v (Var x)) y)). -Notation "'(uint128_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair v (Var x)) (Var y))) (format "'(uint128_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair v (Var x)) (Var y))). -Notation "'(uint128_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair (Var v) x) y)) (format "'(uint128_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair (Var v) x) y)). -Notation "'(uint128_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair (Var v) x) (Var y))) (format "'(uint128_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair (Var v) x) (Var y))). -Notation "'(uint128_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint128_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair (Var v) (Var x)) y)). -Notation "'(uint128_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint128_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair (Var v) (Var x)) (Var y))). -Notation "'(uint256_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair v x) y)) (format "'(uint256_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair v x) y)). -Notation "'(uint256_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair v x) (Var y))) (format "'(uint256_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair v x) (Var y))). -Notation "'(uint256_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair v (Var x)) y)) (format "'(uint256_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair v (Var x)) y)). -Notation "'(uint256_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair v (Var x)) (Var y))) (format "'(uint256_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair v (Var x)) (Var y))). -Notation "'(uint256_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair (Var v) x) y)) (format "'(uint256_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair (Var v) x) y)). -Notation "'(uint256_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair (Var v) x) (Var y))) (format "'(uint256_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair (Var v) x) (Var y))). -Notation "'(uint256_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint256_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair (Var v) (Var x)) y)). -Notation "'(uint256_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint256_t)' 'cmovznz' ( v , x , y )"). -Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair (Var v) (Var x)) (Var y))). Notation "'addcarryx_u32' ( c , a , b )" := (Op (AddWithGetCarry 32 (TWord 0) (TWord 5) (TWord 5) (TWord 5) (TWord 0)) (Pair (Pair c a) b)). Notation "'addcarryx_u32' ( c , a , b )" := (Op (AddWithGetCarry 32 (TWord 0) (TWord 0) (TWord 5) (TWord 5) (TWord 0)) (Pair (Pair c a) b)). Notation "'addcarryx_u32' ( c , a , b )" := (Op (AddWithGetCarry 32 (TWord 0) (TWord 5) (TWord 0) (TWord 5) (TWord 0)) (Pair (Pair c a) b)). |