Wiki ยป
Why we need combination of theories, multipication of non-constants
Short Code example:t1 = x*y;x' = x;y'= y;t2 = x'*y';assert(t1 != t2);
Solution: t1 = f(x, y)