real.cseq.add_assoc
|
∀a b c : ℤ → C, a + b + c = a + (b + c)
|
real.cseq.add_comm
|
∀a b : ℤ → C, a + b = b + a
|
real.cseq.mul_assoc
|
∀a b c : ℤ → C, a * b * c = a * (b * c)
|
real.cseq.mul_comm
|
∀a b : ℤ → C, a * b = b * a
|
real.cseq.rezip_unzip
|
∀a : ℤ → C, C.rezip(C.unzip(a)) = a
|
real.cseq.unzip_rezip
|
∀ab : Tuple_Array_Array, C.unzip(C.rezip(ab)) = ab
|