A simple example of NCProcess1

A simple example of the use of NCProcess1 is to classify m × n matrices x such that

is an isometry where U is given, U is known to be a unitary and W is a given. Thus, we are trying to solve the following collection of equations for x.

Now, of course, since is invertible, x = 0. Let us see how NCProcess1 behaves on the equations of (§). NCProcess1 creates the following output which we call a ``spreadsheet''. The appearing in the spreadsheet below may be read as equal sign.

	YOUR SESSION HAS DIGESTED
	THE FOLLOWING RELATIONS

THE FOLLOWING VARIABLES HAVE BEEN SOLVED FOR:
{x, x*}
The corresponding rules are the following:
x 0

x* 0

The expressions with unknown variables {}
and knowns {U, W, U*, W*}
U U* 1

U* U 1

W* W 1

	USER CREATIONS APPEAR BELOW

	SOME RELATIONS WHICH APPEAR BELOW
		MAY BE UNDIGESTED

THE FOLLOWING VARIABLES HAVE NOT BEEN SOLVED FOR:
{}

The polynomials listed in the spreadsheet above generated the same ideal as (§). Therefore, any solution to (§) is a solution of the equations in the spreadsheet and vice-versa. Therefore, if U is unitary, then the matrix in (§) is an isometry if and only if x is the zero matrix and W is an isometry.