theorem Th26: :: OSAFREE:26

for S being locally_directed OrderSortedSign
for X being non-empty ManySortedSet of S
for R being ManySortedRelation of (ParsedTermsOSA X) holds
( R = PTCongruence X iff ( ( for s1, s2 being Element of S
for x being object st x in X . s1 holds
( ( s1 <= s2 implies [(root-tree [x,s1]),(root-tree [x,s1])] in R . s2 ) & ( for y being object st ( [(root-tree [x,s1]),y] in R . s2 or [y,(root-tree [x,s1])] in R . s2 ) holds
( s1 <= s2 & y = root-tree [x,s1] ) ) ) ) & ( for o1, o2 being OperSymbol of S
for x1 being Element of Args (o1,(ParsedTermsOSA X))
for x2 being Element of Args (o2,(ParsedTermsOSA X))
for s3 being Element of S holds
( [((Den (o1,(ParsedTermsOSA X))) . x1),((Den (o2,(ParsedTermsOSA X))) . x2)] in R . s3 iff ( o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 & ex w3 being Element of the carrier of S * st
( dom w3 = dom x1 & ( for y being Nat st y in dom w3 holds
[(x1 . y),(x2 . y)] in R . (w3 /. y) ) ) ) ) ) ) )