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] + B P inv[B]) P inv[A P inv[A] + B P inv[B]] (A P inv[A] + B P inv[B]) == A P inv[A] + B P inv[B] P inv[A P inv[A]+B P inv[B]] (A P inv[A]+B P inv[B]) P inv[A P inv[A]+B P inv[B]] == P inv[A P inv[A]+ B P inv[B]] ((P inv[A])^{T} A^{T} +(P inv[B])^{T} B^{T}) (P inv[A P inv[A] + B P inv[B]])^{T} == P inv[A P inv[A]+B P inv[B]] (A P inv[A]+ B P inv[B]) (P inv[A P inv[A] + B P inv[B]])^{T} ((P inv[A])^{T} A^{T} +(P inv[B])^{T} B^{T}) == (A P inv[A]+B P inv[B]) P inv[A P inv[A]+ B P inv[B]] (P inv[A P inv[A] + B P inv[B]])^{T} == P inv[(P inv[A])^{T} A^{T} + (P inv[B])^{T} B^{T}] ((P inv[A])^{T} A^{T} +(P inv[B])^{T} B^{T}) (A P inv[A]+B P inv[B]) P inv[A P inv[A]+B P inv[B]] == (P inv[A])^{T} A^{T} + (P inv[B])^{T} B^{T} (A P inv[A] + B P inv[B]) P inv[A P inv[A] + B P inv[B]] P inv[(P inv[A])^{T} A^{T} + (P inv[B])^{T} B^{T}] == P inv[(P inv[A])^{T} A^{T} + (P inv[B])^{T} B^{T}] File Name = APinvAPlusBPinvB NCMakeGB Iterations = 6 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]+B P inv[B]] < P inv[(P inv[A])^{T} A^{T} +(P inv[B])^{T} B^{T}] < (P inv[A P inv[A] + B P inv[B]])^{T}

YOUR SESSION HAS DIGESTED THE FOLLOWING RELATIONS

THE FOLLOWING VARIABLES HAVE BEEN SOLVED FOR:

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

The corresponding rules are the following: P inv[(P inv[A])^{T} A^{T} + (P inv[B])^{T} B^{T}] → P inv[A P inv[A] + B P inv[B]] (P inv[A])^{T} → P inv[A^{T}] (P inv[B])^{T} → P inv[B^{T}] (P inv[A P inv[A] + B P inv[B]])^{T} → P inv[A P inv[A] + B P inv[B]]

The expressions with unknown variables {} and knowns {A, B, P inv[A], P inv[B], P inv[A P inv[A]+B P inv[B]], P inv[A^{T}], P inv[B^{T}], A^{T} , B^{T} } P inv[A] A → A^{T} P inv[A^{T}] P inv[B] B → B^{T} P inv[B^{T}] P inv[A^{T}] A^{T} → A P inv[A] P inv[B^{T}] B^{T} → B P inv[B] 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 B^{T} P inv[B^{T}] → B

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

A^{T} A P inv[A] → 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 P inv[B] P inv[A P inv[A] + B P inv[B]] P inv[A P inv[A] + B P inv[B]] → −1 A P inv[A] P inv[A P inv[A] + B P inv[B]] P inv[A P inv[A] + B P inv[B]] + P inv[A P inv[A] + B P inv[B]]

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

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

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

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

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

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

2 A P inv[A] P inv[A P inv[A] + B P inv[B]] B + B P inv[B] P inv[A P inv[A] + B P inv[B]] B + 4 P inv[A P inv[A] + B P inv[B]] A P inv[A] P inv[A P inv[A] + B P inv[B]] B

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

{B^{T} P inv[A P inv[A] + B P inv[B]] A P inv[A] P inv[A P inv[A] + B P inv[B]] P inv[B^{T}] → \atop \frac{1}{2} B^{T} P inv[B^{T}] − \frac{1}{2} B^{T} P inv[A P inv[A] + B P inv[B]] 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] + B P inv[B]], 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:08 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:01 The time for SmallBasis was 0:00:00 The time for CreateCategories was 0:00:07 The time for NCCV was 0:00:00 The time for RegularOutput was 0:00:01 The time for everything so far was 0:00:17