:: deftheorem DEF3 defines TotalTRS ABSRED_0:def 32 :
for X being non empty set
for x being Element of X
for b₃ being non empty non-empty strict TRSStr holds
( b₃ = TotalTRS (X,x) iff ( the carrier of b₃ = X & the charact of b₃ = <*((0 -tuples_on X) --> x),((1 -tuples_on X) --> x),((2 -tuples_on X) --> x)*> & the reduction of b₃ = nabla X ) );