List of theorems referencing the symbol PLUZ

(518) Theorem sigma_theory4: [Removal of single element from domain of a sum] ((C in F) & Finite(F) & (range(F) •incin s)) •imp (sigma_thryvar(F) = pluz(sigma_thryvar(F - {C}),cdr(C)))
(519) Theorem sigma_theory5: [The generalized sum of a union map is a sum of sums] (Finite(F) & Is_map(F) & (range(F) •incin s)) •imp (sigma_thryvar(F) = pluz(sigma_thryvar(F •ON (domain(F) * T)), sigma_thryvar(F •ON (domain(F) - T))))
(555) Theorem Ordered_add.0: [Echo of relator definitions] (GE_thryvar(X,Y) •eq nneg(pluz(X,rvz(Y)))) & (LE_thryvar(X,Y) •eq GE_thryvar(Y,X)) & (GT_thryvar(X,Y) •eq (GE_thryvar(X,Y) & (X /= Y))) & (LT_thryvar(X,Y) •eq GT_thryvar(Y,X))
(556) Theorem Ordered_add.1: [Interface to Otter-based THEORY of orderedGroups] (LE_thryvar(X,Y) •eq nneg(pluz(Y,rvz(X)))) & (((X in g) & (Y in g)) •imp (GT_thryvar(X,Y) •eq (nneg(pluz(X,rvz(Y))) & (X /= Y)))) & (((X in g) & (Y in g)) •imp (GT_thryvar(X,Y) •eq (nneg(minz(X,Y)) & (X /= Y))))