@[simp]

theorem Fin.and_val {n : Nat} (a b : Fin n) : ↑(a &&& b) = ↑a &&& ↑b

@[simp]

theorem Fin.or_val_of_two_pow {w : Nat} (a b : Fin (2 ^ w)) : ↑(a ||| b) = ↑a ||| ↑b

@[simp]

theorem Fin.or_val_of_uInt8Size (a b : Fin UInt8.size) : ↑(a ||| b) = ↑a ||| ↑b

@[simp]

theorem Fin.or_val_of_uInt16Size (a b : Fin UInt16.size) : ↑(a ||| b) = ↑a ||| ↑b

@[simp]

theorem Fin.or_val_of_uInt32Size (a b : Fin UInt32.size) : ↑(a ||| b) = ↑a ||| ↑b

@[simp]

theorem Fin.or_val_of_uInt64Size (a b : Fin UInt64.size) : ↑(a ||| b) = ↑a ||| ↑b

@[simp]

theorem Fin.or_val_of_uSizeSize (a b : Fin USize.size) : ↑(a ||| b) = ↑a ||| ↑b

theorem Fin.or_val {n : Nat} (a b : Fin n) : ↑(a ||| b) = (↑a ||| ↑b) % n

@[simp]

theorem Fin.xor_val_of_two_pow {w : Nat} (a b : Fin (2 ^ w)) : ↑(a ^^^ b) = ↑a ^^^ ↑b

@[simp]

theorem Fin.xor_val_of_uInt8Size (a b : Fin UInt8.size) : ↑(a ^^^ b) = ↑a ^^^ ↑b

@[simp]

theorem Fin.xor_val_of_uInt16Size (a b : Fin UInt16.size) : ↑(a ^^^ b) = ↑a ^^^ ↑b

@[simp]

theorem Fin.xor_val_of_uInt32Size (a b : Fin UInt32.size) : ↑(a ^^^ b) = ↑a ^^^ ↑b

@[simp]

theorem Fin.xor_val_of_uInt64Size (a b : Fin UInt64.size) : ↑(a ^^^ b) = ↑a ^^^ ↑b

@[simp]

theorem Fin.xor_val_of_uSizeSize (a b : Fin USize.size) : ↑(a ^^^ b) = ↑a ^^^ ↑b

theorem Fin.xor_val {n : Nat} (a b : Fin n) : ↑(a ^^^ b) = (↑a ^^^ ↑b) % n

@[simp]

theorem Fin.shiftLeft_val {n : Nat} (a b : Fin n) : ↑(a <<< b) = ↑a <<< ↑b % n

@[simp]

theorem Fin.shiftRight_val {n : Nat} (a b : Fin n) : ↑(a >>> b) = ↑a >>> ↑b