CONST 
  Id2 = ((1, 0), (0, 1)), A = ((1, 2), (1, 2));

FUNC z = Mat2Mul(x, y) IS 
  (E xr1, xr2, yc1, yc2, z11, z12, z21, z22 :: 
    x = (xr1, xr2) AND 
    z = ((z11, z12), (z21, z22)) AND 
    yc1 = (CAR(CAR(y)), CAR(CDR(y))) AND 
    yc2 = (CDR(CAR(y)), CDR(CDR(y))) AND 
    z11 = R2.Dot(xr1, yc1) AND 
    z12 = R2.Dot(xr1, yc2) AND 
    z21 = R2.Dot(xr2, yc1) AND 
    z22 = R2.Dot(xr2, yc2)) 
END;

PROC Cmd0() IS 
  IF VAR aInv ~ ((-3, 2), (2, -1)) IN Id2 = Mat2Mul(A, aInv) -> SKIP END FI 
END;