Input = A P inv[A] A == A P inv[A] A P inv[A] == P inv[A] A^{T} (P inv[A])^{T} == P inv[A] A (P inv[A])^{T} A^{T} == A P inv[A] (P inv[A])^{T} == P inv[A^{T}] A^{T} A P inv[A] == A^{T} A P inv[A] P inv[A^{T}] == P inv[A^{T}] B P inv[B] B == B P inv[B] B P inv[B] == P inv[B] B^{T} (P inv[B])^{T} == P inv[B] B (P inv[B])^{T} B^{T} == B P inv[B] (P inv[B])^{T} == P inv[B^{T}] B^{T} B P inv[B] == B^{T} B P inv[B] P inv[B^{T}] == P inv[B^{T}] (A P inv[A] + P inv[B] B) P inv[A P inv[A] + P inv[B] B] (A P inv[A] + P inv[B] B) == A P inv[A] + P inv[B] B P inv[A P inv[A]+P inv[B] B] (A P inv[A]+P inv[B] B) P inv[A P inv[A]+P inv[B] B] == P inv[A P inv[A]+ P inv[B] B] (B^{T} (P inv[B])^{T} +(P inv[A])^{T} A^{T}) (P inv[A P inv[A] + P inv[B] B])^{T} == P inv[A P inv[A]+P inv[B] B] (A P inv[A]+ P inv[B] B) (P inv[A P inv[A] + P inv[B] B])^{T} (B^{T} (P inv[B])^{T} +(P inv[A])^{T} A^{T}) == (A P inv[A]+P inv[B] B) P inv[A P inv[A]+ P inv[B] B] (P inv[A P inv[A] + P inv[B] B])^{T} == P inv[B^{T} (P inv[B])^{T} + (P inv[A])^{T} A^{T}] (B^{T} (P inv[B])^{T} +(P inv[A])^{T} A^{T}) (A P inv[A]+P inv[B] B) P inv[A P inv[A]+P inv[B] B] == B^{T} (P inv[B])^{T} + (P inv[A])^{T} A^{T} (A P inv[A]+P inv[B] B) P inv[A P inv[A]+P inv[B] B] P inv[B^{T} (P inv[B])^{T} +(P inv[A])^{T} A^{T}] == P inv[B^{T} (P inv[B])^{T} + (P inv[A])^{T} A^{T}] (A P inv[A]−P inv[B] B A P inv[A]) P inv[A P inv[A]−P inv[B] B A P inv[A]] (A P inv[A]−P inv[B] B A P inv[A]) == A P inv[A] − P inv[B] B A P inv[A] P inv[A P inv[A]−P inv[B] B A P inv[A]] (A P inv[A]−P inv[B] B A P inv[A]) P inv[A P inv[A]−P inv[B] B A P inv[A]] == P inv[A P inv[A] − P inv[B] B A P inv[A]] ((P inv[A])^{T} A^{T} −(P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}) (P inv[A P inv[A] − P inv[B] B A P inv[A]])^{T} == P inv[A P inv[A] − P inv[B] B A P inv[A]] (A P inv[A] − P inv[B] B A P inv[A]) (P inv[A P inv[A] − P inv[B] B A P inv[A]])^{T} ((P inv[A])^{T} A^{T} −(P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}) == (A P inv[A] − P inv[B] B A P inv[A]) P inv[A P inv[A] − P inv[B] B A P inv[A]] (P inv[A P inv[A] − P inv[B] B A P inv[A]])^{T} == P inv[(P inv[A])^{T} A^{T} −(P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}] ((P inv[A])^{T} A^{T} −(P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}) (A P inv[A]−P inv[B] B A P inv[A]) P inv[A P inv[A]− P inv[B] B A P inv[A]] == (P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T} (A P inv[A]−P inv[B] B A P inv[A]) P inv[A P inv[A]−P inv[B] B A P inv[A]] P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}] == P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}] File Name = BothTogether NCMakeGB Iterations = 5 NCMakeGB on Digested Iterations = 0 SmallBasis Iterations = 0 SmallBasis on Knowns Iterations = 0 Deselect→ {} UserSelect→ {} UserUnknowns→ {} NCShortFormulas→-1 RR→False RRByCat→False SB→False SBByCat→False DegreeCap→-1 DegreeSumCap→-1 DegreeCapSB→-1 DegreeSumCapSB→-1 NCCV→False THE ORDER IS NOW THE FOLLOWING: A < B < A^{T} < B^{T} < P inv[A] < P inv[B] < P inv[A^{T}] < P inv[B^{T}] < (P inv[A])^{T} < (P inv[B])^{T} < P inv[A P inv[A]+P inv[B] B] < P inv[B^{T} (P inv[B])^{T} +(P inv[A])^{T} A^{T}] < (P inv[A P inv[A] + P inv[B] B])^{T} < P inv[A P inv[A]−P inv[B] B A P inv[A]] < P inv[(P inv[A])^{T} A^{T} −(P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}] <

(P inv[A P inv[A] − P inv[B] B A P inv[A]])^{T}

YOUR SESSION HAS DIGESTED THE FOLLOWING RELATIONS

THE FOLLOWING VARIABLES HAVE BEEN SOLVED FOR: {P inv[B^{T} (P inv[B])^{T} +(P inv[A])^{T} A^{T}], (P inv[A])^{T} , (P inv[B])^{T} , (P inv[A P inv[A] + P inv[B] B])^{T} , (P inv[A P inv[A] − P inv[B] B A P inv[A]])^{T} } The corresponding rules are the following: P inv[B^{T} (P inv[B])^{T} + (P inv[A])^{T} A^{T}] → P inv[A P inv[A] + P inv[B] B]

(P inv[A])^{T} → P inv[A^{T}]

(P inv[B])^{T} → P inv[B^{T}]

(P inv[A P inv[A] + P inv[B] B])^{T} → P inv[A P inv[A] + P inv[B] B]

{(P inv[A P inv[A] − P inv[B] B A P inv[A]])^{T}  →  P inv[(P inv[A])^{T} A^{T}  − \atop (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}]}

The expressions with unknown variables {} and knowns {A, B, P inv[A], P inv[B], P inv[A P inv[A]+P inv[B] B], P inv[A P inv[A]−P inv[B] B A P inv[A]], P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}], P inv[A^{T}], P inv[B^{T}], A^{T} , B^{T} } B P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}] → 0

P inv[A] A → A^{T} P inv[A^{T}]

{P inv[A] P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}] → −2 P inv[A] P inv[A P inv[A] + \atop P inv[B] B] + 2 P inv[A] P inv[A P inv[A] − P inv[B] B A P inv[A]] + P inv[A]}

P inv[B] B → B^{T} P inv[B^{T}]

P inv[A P inv[A] − P inv[B] B A P inv[A]] P inv[B] → 0

{P inv[A P inv[A] − P inv[B] B A P inv[A]] P inv[A P inv[A] − P inv[B] B A P inv[A]] → \atop P inv[A P inv[A] − P inv[B] B A P inv[A]]}

P inv[A P inv[A] − P inv[B] B A P inv[A]] B^{T} → 0

{P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}] A → −\frac{1}{2} A + P inv[A P inv[A] + \atop P inv[B] B] A + \frac{1}{2} P inv[A P inv[A] − P inv[B] B A P inv[A]] A}

{P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}] P inv[A P inv[A] + P inv[B] B] → \atop P inv[A P inv[A] + P inv[B] B] P inv[A P inv[A] − P inv[B] B A P inv[A]]}

{P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}] P inv[A P inv[A] − P inv[B] B A P inv[A]] → \atop P inv[A P inv[A] + P inv[B] B] P inv[A P inv[A] − P inv[B] B A P inv[A]]}

{P inv[(P inv[A])^{T} A^{T}  −  (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}] P inv[(P inv[A])^{T} A^{T}  − \atop (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}] → P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}]}

{P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}] P inv[A^{T}] → P inv[A P inv[A] + \atop P inv[B] B] P inv[A^{T}] + \frac{1}{2} P inv[A P inv[A] − P inv[B] B A P inv[A]] P inv[A^{T}] − \frac{1}{2} P inv[A^{T}]}

P inv[A^{T}] A^{T} → A P inv[A]

P inv[B^{T}] P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}] → 0

P inv[B^{T}] B^{T} → B P inv[B]

{A^{T} P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}] → −2 A^{T} P inv[A P inv[A] + \atop P inv[B] B] + 2 A^{T} P inv[A P inv[A] − P inv[B] B A P inv[A]] + A^{T}}

A P inv[A] P inv[A P inv[A] − P inv[B] B A P inv[A]] → P inv[A P inv[A] − P inv[B] B A P inv[A]]

A P inv[A] P inv[A^{T}] → P inv[A^{T}]

A A^{T} P inv[A^{T}] → A

B P inv[B] P inv[B^{T}] → P inv[B^{T}]

B P inv[A P inv[A] + P inv[B] B] P inv[A P inv[A] − P inv[B] B A P inv[A]] → 0

B P inv[A P inv[A] − P inv[B] B A P inv[A]] A → B A − 2 B P inv[A P inv[A] + P inv[B] B] A

B P inv[A P inv[A] − P inv[B] B A P inv[A]] P inv[A P inv[A] + P inv[B] B] → −\frac{1}{2} B + \frac{3}{2} B P inv[A P inv[A] + P inv[B] B] + \frac{1}{2} B P inv[A P inv[A] − P inv[B] B A P inv[A]] − B P inv[A P inv[A] + P inv[B] B] P inv[A P inv[A] + P inv[B] B]

B P inv[A P inv[A]  −  P inv[B] B A P inv[A]] P inv[(P inv[A])^{T} A^{T}  −

(P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}] → −1 B P inv[A P inv[A] + P inv[B] B] P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}]

{B P inv[A P inv[A] − P inv[B] B A P inv[A]] P inv[A^{T}] → B P inv[A^{T}] − 2 B P inv[A P inv[A] + \atop P inv[B] B] P inv[A^{T}]}

B B^{T} P inv[B^{T}] → B

{P inv[A] P inv[A P inv[A] + P inv[B] B] P inv[A P inv[A] − P inv[B] B A P inv[A]] → \atop P inv[A] P inv[A P inv[A] − P inv[B] B A P inv[A]]}

{P inv[A] P inv[A P inv[A] − P inv[B] B A P inv[A]] A  →  −1 A^{T} P inv[A^{T}] + \atop 2 P inv[A] P inv[A P inv[A] + P inv[B] B] A}

P inv[A] P inv[A P inv[A] − P inv[B] B A P inv[A]] P inv[A P inv[A] + P inv[B] B] → −\frac{1}{2} P inv[A] P inv[A P inv[A] + P inv[B] B] + \frac{1}{2} P inv[A] P inv[A P inv[A] − P inv[B] B A P inv[A]] + P inv[A] P inv[A P inv[A] + P inv[B] B] P inv[A P inv[A] + P inv[B] B]

P inv[A] P inv[A P inv[A]  −  P inv[B] B A P inv[A]] P inv[(P inv[A])^{T} A^{T}  −

(P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}] → P inv[A] P inv[A P inv[A] + P inv[B] B] P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}]

{P inv[A] P inv[A P inv[A] − P inv[B] B A P inv[A]] P inv[A^{T}]  →  −1 P inv[A] P inv[A^{T}] + \atop 2 P inv[A] P inv[A P inv[A] + P inv[B] B] P inv[A^{T}]}

{P inv[A P inv[A] + P inv[B] B] A P inv[A] → A P inv[A] P inv[A P inv[A] + P inv[B] B] − \atop P inv[A P inv[A] − P inv[B] B A P inv[A]] + P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}]}

P inv[A P inv[A] + P inv[B] B] P inv[A P inv[A] + P inv[B] B] P inv[A P inv[A] − P inv[B] B A P inv[A]] → \frac{1}{2} P inv[A P inv[A] + P inv[B] B] P inv[A P inv[A] + P inv[B] B] + \frac{1}{2} P inv[A P inv[A] + P inv[B] B] P inv[A P inv[A] − P inv[B] B A P inv[A]] + \frac{1}{2} P inv[A P inv[A] + P inv[B] B] P inv[(P inv[A])^{T} A^{T} −(P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}]+ \frac{1}{4} A P inv[A] P inv[A P inv[A]+ P inv[B] B] − \frac{1}{2} P inv[A P inv[A] + P inv[B] B] − \frac{1}{4} P inv[A P inv[A] − P inv[B] B A P inv[A]]

{P inv[A P inv[A] + P inv[B] B] P inv[A P inv[A] − P inv[B] B A P inv[A]] A → −\frac{1}{2} A + \atop P inv[A P inv[A] + P inv[B] B] A + \frac{1}{2} P inv[A P inv[A] − P inv[B] B A P inv[A]] A}

P inv[A P inv[A] + P inv[B] B] P inv[A P inv[A] − P inv[B] B A P inv[A]] P inv[A P inv[A] + P inv[B] B] → \frac{1}{2} P inv[A P inv[A] + P inv[B] B] P inv[A P inv[A] + P inv[B] B] + \frac{1}{2} P inv[A P inv[A] + P inv[B] B] P inv[A P inv[A] − P inv[B] B A P inv[A]] + \frac{1}{2} P inv[A P inv[A] − P inv[B] B A P inv[A]] P inv[A P inv[A] + P inv[B] B] + \frac{1}{4} A P inv[A] P inv[A P inv[A] + P inv[B] B] − \frac{1}{2} P inv[A P inv[A] + P inv[B] B] − \frac{1}{4} P inv[A P inv[A] − P inv[B] B A P inv[A]] P inv[A P inv[A] + P inv[B] B] P inv[A P inv[A] − P inv[B] B A P inv[A]] P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}] → \frac{1}{2} P inv[A P inv[A] + P inv[B] B] P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}]+ \frac{1}{2} P inv[A P inv[A]−P inv[B] B A P inv[A]] P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}]

P inv[A P inv[A] + P inv[B] B] P inv[A P inv[A] − P inv[B] B A P inv[A]] P inv[A^{T}] → P inv[A P inv[A] + P inv[B] B] P inv[A^{T}] + \frac{1}{2} P inv[A P inv[A] − P inv[B] B A P inv[A]] P inv[A^{T}] − \frac{1}{2} P inv[A^{T}]

P inv[A P inv[A] + P inv[B] B] P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}] P inv[B] → \frac{3}{2} P inv[A P inv[A] + P inv[B] B] P inv[B] + \frac{1}{2} P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}] P inv[B] − P inv[A P inv[A] + P inv[B] B] P inv[A P inv[A] + P inv[B] B] P inv[B] − \frac{1}{2} P inv[B]

P inv[A P inv[A] + P inv[B] B] P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}] B^{T} → \frac{3}{2} P inv[A P inv[A]+P inv[B] B] B^{T} + \frac{1}{2} P inv[(P inv[A])^{T} A^{T} −(P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}] B^{T} − P inv[A P inv[A] + P inv[B] B] P inv[A P inv[A] + P inv[B] B] B^{T} − \frac{1}{2} B^{T}

{P inv[A P inv[A] + P inv[B] B] B^{T} P inv[B^{T}] → −2 P inv[A P inv[A] + P inv[B] B] P inv[A P inv[A] − \atop P inv[B] B A P inv[A]] + P inv[A P inv[A] + P inv[B] B] + P inv[A P inv[A] − P inv[B] B A P inv[A]]}

{P inv[A P inv[A] − P inv[B] B A P inv[A]] A P inv[A] → A P inv[A] − 2 A P inv[A] P inv[A P inv[A] + \atop P inv[B] B] + 2 P inv[A P inv[A] − P inv[B] B A P inv[A]]}

P inv[A P inv[A] − P inv[B] B A P inv[A]] P inv[A P inv[A] + P inv[B] B] P inv[A P inv[A] − P inv[B] B A P inv[A]] → \frac{1}{2} P inv[A P inv[A] − P inv[B] B A P inv[A]] P inv[A P inv[A] + P inv[B] B] + \frac{1}{2} P inv[A P inv[A] − P inv[B] B A P inv[A]] P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}]

{P inv[A P inv[A]−P inv[B] B A P inv[A]] P inv[(P inv[A])^{T} A^{T} −(P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}] P inv[B] → \atop −1 P inv[A P inv[A] − P inv[B] B A P inv[A]] P inv[A P inv[A] + P inv[B] B] P inv[B]}

{P inv[A P inv[A]−P inv[B] B A P inv[A]] P inv[(P inv[A])^{T} A^{T} −(P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}] B^{T} → \atop −1 P inv[A P inv[A] − P inv[B] B A P inv[A]] P inv[A P inv[A] + P inv[B] B] B^{T}}

P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}] B^{T} P inv[B^{T}] → 2 P inv[A P inv[A] + P inv[B] B] P inv[A P inv[A] − P inv[B] B A P inv[A]] + B^{T} P inv[B^{T}] − A P inv[A] P inv[A P inv[A] + P inv[B] B] − P inv[A P inv[A] + P inv[B] B]

P inv[B^{T}] P inv[A P inv[A] + P inv[B] B] P inv[A P inv[A] − P inv[B] B A P inv[A]] → 0

{P inv[B^{T}] P inv[A P inv[A]−P inv[B] B A P inv[A]] A → P inv[B^{T}] A−2 P inv[B^{T}] P inv[A P inv[A]+ \atop P inv[B] B] A}

P inv[B^{T}] P inv[A P inv[A] − P inv[B] B A P inv[A]] P inv[A P inv[A] + P inv[B] B] → \frac{3}{2} P inv[B^{T}] P inv[A P inv[A] + P inv[B] B] + \frac{1}{2} P inv[B^{T}] P inv[A P inv[A] − P inv[B] B A P inv[A]] − P inv[B^{T}] P inv[A P inv[A] + P inv[B] B] P inv[A P inv[A] + P inv[B] B] − \frac{1}{2} P inv[B^{T}]

P inv[B^{T}] P inv[A P inv[A]  −  P inv[B] B A P inv[A]] P inv[(P inv[A])^{T} A^{T}  −
(P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}]  →  −1 P inv[B^{T}] P inv[A P inv[A]  +

P inv[B] B] P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}]

{P inv[B^{T}] P inv[A P inv[A] − P inv[B] B A P inv[A]] P inv[A^{T}]  →  P inv[B^{T}] P inv[A^{T}] − \atop 2 P inv[B^{T}] P inv[A P inv[A] + P inv[B] B] P inv[A^{T}]}

A^{T} A P inv[A] → A^{T}

{A^{T} P inv[A P inv[A] + P inv[B] B] P inv[A P inv[A] − P inv[B] B A P inv[A]] → A^{T} P inv[A P inv[A] − \atop P inv[B] B A P inv[A]]}

A^{T} P inv[A P inv[A] − P inv[B] B A P inv[A]] A → −1 A^{T} A + 2 A^{T} P inv[A P inv[A] + P inv[B] B] A

A^{T} P inv[A P inv[A] − P inv[B] B A P inv[A]] P inv[A P inv[A] + P inv[B] B] → −\frac{1}{2} A^{T} P inv[A P inv[A] + P inv[B] B] + \frac{1}{2} A^{T} P inv[A P inv[A] − P inv[B] B A P inv[A]] + A^{T} P inv[A P inv[A] + P inv[B] B] P inv[A P inv[A] + P inv[B] B]

A^{T} P inv[A P inv[A]  −  P inv[B] B A P inv[A]] P inv[(P inv[A])^{T} A^{T}  −

(P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}] → A^{T} P inv[A P inv[A] + P inv[B] B] P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}]

{A^{T} P inv[A P inv[A] − P inv[B] B A P inv[A]] P inv[A^{T}] → −1 A^{T} P inv[A^{T}] + 2 A^{T} P inv[A P inv[A] + \atop P inv[B] B] P inv[A^{T}]}

A^{T} P inv[A^{T}] P inv[A] → P inv[A]

B^{T} B P inv[B] → B^{T}

B^{T} P inv[B^{T}] P inv[B] → P inv[B]

B^{T} P inv[B^{T}] P inv[A P inv[A] + P inv[B] B] → −2 P inv[A P inv[A] + P inv[B] B] P inv[A P inv[A] − P inv[B] B A P inv[A]] + P inv[A P inv[A] + P inv[B] B] + P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}]

B^{T} P inv[B^{T}] P inv[A P inv[A] − P inv[B] B A P inv[A]]  →  2 P inv[A P inv[A] +

P inv[B] B] P inv[A P inv[A] − P inv[B] B A P inv[A]] + B^{T} P inv[B^{T}] − A P inv[A] P inv[A P inv[A] + P inv[B] B] − P inv[A P inv[A] + P inv[B] B] + P inv[A P inv[A] − P inv[B] B A P inv[A]] − P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}]

A P inv[A] P inv[A P inv[A] + P inv[B] B] A → \frac{1}{2} A + \frac{1}{2} P inv[A P inv[A] − P inv[B] B A P inv[A]] A

{A P inv[A] P inv[A P inv[A] + P inv[B] B] P inv[B] → −1 P inv[A P inv[A] + P inv[B] B] P inv[B] − \atop P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}] P inv[B] + P inv[B]}

A P inv[A] P inv[A P inv[A] + P inv[B] B] P inv[A P inv[A] + P inv[B] B] → P inv[A P inv[A] − P inv[B] B A P inv[A]] P inv[A P inv[A] + P inv[B] B] + \frac{1}{2} A P inv[A] P inv[A P inv[A] + P inv[B] B] − \frac{1}{2} P inv[A P inv[A] − P inv[B] B A P inv[A]]

{A P inv[A] P inv[A P inv[A] + P inv[B] B] P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}] → \atop P inv[A P inv[A] − P inv[B] B A P inv[A]] P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}]}

{A P inv[A] P inv[A P inv[A] + P inv[B] B] P inv[A^{T}]  →  \frac{1}{2} P inv[A P inv[A] − \atop P inv[B] B A P inv[A]] P inv[A^{T}] + \frac{1}{2} P inv[A^{T}]}

{A P inv[A] P inv[A P inv[A] + P inv[B] B] B^{T} → −1 P inv[A P inv[A] + P inv[B] B] B^{T} − \atop P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}] B^{T} + B^{T}}

B A P inv[A] P inv[A P inv[A] + P inv[B] B] → B − B P inv[A P inv[A] + P inv[B] B]

{P inv[B^{T}] A P inv[A] P inv[A P inv[A] + P inv[B] B] → −1 P inv[B^{T}] P inv[A P inv[A] + P inv[B] B] + \atop P inv[B^{T}]}

USER CREATIONS APPEAR BELOW

SOME RELATIONS WHICH APPEAR BELOW MAY BE UNDIGESTED

THE FOLLOWING VARIABLES HAVE NOT BEEN SOLVED FOR: {A, B, P inv[A], P inv[B], P inv[A P inv[A] + P inv[B] B], P inv[A P inv[A] − P inv[B] B A P inv[A]], P inv[(P inv[A])^{T} A^{T} − (P inv[A])^{T} A^{T} B^{T} (P inv[B])^{T}], P inv[A^{T}], P inv[B^{T}], A^{T} , B^{T} }

The time for preliminaries was 0:00:00 The time for NCMakeGB 1 was 0:00:00 The time for Remove Redundant 1 was 0:00:00 The time for the main NCMakeGB was 0:00:43 The time for Remove Redundant 2 was 0:00:00 The time for reducing unknowns was 0:00:00 The time for clean up basis was 0:00:00 The time for SmallBasis was 0:00:00 The time for CreateCategories was 0:00:16 The time for NCCV was 0:00:00 The time for RegularOutput was 0:00:00 The time for everything so far was 0:00:59