calculation at match and substituion time

[malloc-realloc]

fn cx(a, b R) C
fn cmul(a, b C) C
know forall a, b, c, d R => cmul(cx(a, b), cx(c, d)) = cx(a*c-b*d, a*d+b*c)

cx(0, 1) \cmul cx(0, 1) = cx(0 * 0 - 1 * 1, 0 * 1 + 1 * 0)
cx(0, 1) \cmul cx(0, 1) = cx(-1, 0)

This is too complex, the following is much better

fn cx(a, b R) C
fn cmul(a, b C) C
know forall a, b, c, d R => cmul(cx(a, b), cx(c, d)) = cx(a*c-b*d, a*d+b*c)

cx(0, 1) \cmul cx(0, 1) = cx(-1, 0)

This requires calculation of 0 * 0 - 1 * 1 = -1 , 0 * 1 + 1 * 0 = 0 at calculation time