xor.agda

xor-linear : ∀ {n} (x y : BitVector n) → bitwise-xor x y ≡ zipWith _xor_ x y
xor-linear x y = refl

xor-comm : ∀ {n} (x y : BitVector n) → bitwise-xor x y ≡ bitwise-xor y x
xor-comm [] [] = refl
xor-comm (0# ∷ xs) (0# ∷ ys) rewrite xor-comm xs ys = refl
xor-comm (0# ∷ xs) (1# ∷ ys) rewrite xor-comm xs ys = refl
xor-comm (1# ∷ xs) (0# ∷ ys) rewrite xor-comm xs ys = refl
xor-comm (1# ∷ xs) (1# ∷ ys) rewrite xor-comm xs ys  = refl

xor-involution : ∀ {n} (x y : BitVector n) → bitwise-xor (bitwise-xor x y) y ≡ x
xor-involution [] [] = refl
xor-involution (0# ∷ xs) (0# ∷ ys) rewrite xor-involution xs ys = refl
xor-involution (0# ∷ xs) (1# ∷ ys) rewrite xor-involution xs ys = refl
xor-involution (1# ∷ xs) (0# ∷ ys) rewrite xor-involution xs ys = refl
xor-involution (1# ∷ xs) (1# ∷ ys) rewrite xor-involution xs ys = refl