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 B P inv[A B] A B == A B P inv[A B] A B P inv[A B] == P inv[A B] B^{T} A^{T} (P inv[A B])^{T} == P inv[A B] A B (P inv[A B])^{T} B^{T} A^{T} == A B P inv[A B] (P inv[A B])^{T} == P inv[B^{T} A^{T}] B^{T} A^{T} A B P inv[A B] == B^{T} A^{T} A B P inv[A B] P inv[B^{T} A^{T}] == P inv[B^{T} A^{T}] File Name = PinvAB-5iters 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 B] < P inv[B^{T} A^{T}] < (P inv[A B])^{T}

YOUR SESSION HAS DIGESTED THE FOLLOWING RELATIONS

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

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

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

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 B], P inv[B^{T} A^{T}], P inv[A^{T}], P inv[B^{T}], A^{T} , B^{T} }

0.7 The expressions with unknown variables {P inv[A B]} and knowns {A, B, P inv[A], P inv[B], P inv[A^{T}], P inv[B^{T}], A^{T} , B^{T} } P inv[A B] A P inv[A] → P inv[A B] B^{T} P inv[B^{T}] P inv[A B] → P inv[A B] A B P inv[A B] A P inv[B^{T}] → A P inv[B^{T}] P inv[B] A^{T} A B P inv[A B] → P inv[B] A^{T} P inv[A^{T}] B P inv[A B] A P inv[B^{T}] → P inv[A^{T}] P inv[B^{T}] B^{T} A^{T} A B P inv[A B] → B^{T} A^{T}

0.9 The expressions with unknown variables {P inv[B^{T} A^{T}]} and knowns {A, B, P inv[A], P inv[B], P inv[A^{T}], P inv[B^{T}], A^{T} , B^{T} } A P inv[A] P inv[B^{T} A^{T}] → P inv[B^{T} A^{T}] P inv[B^{T} A^{T}] B^{T} P inv[B^{T}] → P inv[B^{T} A^{T}] A B B^{T} A^{T} P inv[B^{T} A^{T}] → A B P inv[B] A^{T} P inv[B^{T} A^{T}] B^{T} P inv[A] → P inv[B] P inv[A] P inv[A^{T}] B B^{T} A^{T} P inv[B^{T} A^{T}] → P inv[A^{T}] B B^{T} A^{T} P inv[B^{T} A^{T}] B^{T} P inv[A] → B^{T} P inv[A] 1.6 The expressions with unknown variables {P inv[B^{T} A^{T}], P inv[A B]} and knowns {A, B, P inv[A], P inv[B], P inv[A^{T}], P inv[B^{T}], A^{T} , B^{T} } P inv[A B] A B → B^{T} A^{T} P inv[B^{T} A^{T}] P inv[B^{T} A^{T}] B^{T} A^{T} → A B P inv[A B] A B P inv[A B] P inv[B^{T} A^{T}] → P inv[B^{T} A^{T}] P inv[B] A^{T} P inv[B^{T} A^{T}] P inv[A B] → P inv[B] P inv[B^{T}] P inv[A B] P inv[A B] P inv[B^{T} A^{T}] B^{T} P inv[A] → P inv[A B] P inv[A^{T}] P inv[A] P inv[B^{T} A^{T}] P inv[A B] A P inv[B^{T}] → P inv[B^{T} A^{T}] P inv[B] P inv[B^{T}] P inv[A^{T}] B P inv[A B] P inv[B^{T} A^{T}] → P inv[A^{T}] P inv[A] P inv[B^{T} A^{T}] B^{T} A^{T} P inv[B^{T} A^{T}] P inv[A B] → P inv[A B] A B P inv[A B] P inv[A^{T}] P inv[A] → P inv[B^{T} A^{T}] B^{T} P inv[A] P inv[B] P inv[B^{T}] P inv[A B] A P inv[B^{T}] → P inv[B] A^{T} P inv[B^{T} A^{T}] P inv[B] P inv[B^{T}] P inv[A^{T}] P inv[A] P inv[B^{T} A^{T}] B^{T} P inv[A] → P inv[A^{T}] B P inv[A B] P inv[A^{T}] P inv[A] B^{T} A^{T} P inv[B^{T} A^{T}] P inv[B] P inv[B^{T}] → P inv[A B] A P inv[B^{T}] B P inv[B] A^{T} P inv[B^{T} A^{T}] P inv[B] P inv[B^{T}] → P inv[B^{T}] P inv[A B] A P inv[B^{T}] A^{T} P inv[A^{T}] B P inv[A B] P inv[A^{T}] P inv[A] → P inv[A] P inv[B^{T} A^{T}] B^{T} P inv[A] A B P inv[A B] P inv[A^{T}] B P inv[A B] P inv[A^{T}] P inv[A] → P inv[B^{T} A^{T}] B^{T} P inv[A] P inv[B^{T} A^{T}] B^{T} P inv[A]

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

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

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

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

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

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

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

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

{B^{T} A^{T} P inv[B^{T} A^{T}] P inv[B] A^{T} P inv[B^{T} A^{T}] P inv[B] A^{T} P inv[B^{T} A^{T}] P inv[B] A^{T} P inv[B^{T} A^{T}] P inv[B] P inv[B^{T}] → \atop P inv[A B] A P inv[B^{T}] P inv[A B] A P inv[B^{T}] P inv[A B] A P inv[B^{T}] P inv[A B] A P inv[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:01 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:02 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:03