:: deftheorem defines represents PRELAMB:def 9 :
for s being non empty typealg
for Tr being finite DecoratedTree of the carrier of s
for x being type of s holds
( Tr represents x iff ( dom Tr is finite & ( for v being Element of dom Tr holds
( ( branchdeg v = 0 or branchdeg v = 2 ) & ( branchdeg v = 0 implies Tr . v is primitive ) & ( branchdeg v = 2 implies ex y, z being type of s st
( ( Tr . v = y /" z or Tr . v = y \ z or Tr . v = y * z ) & Tr . (v ^ <*0*>) = y & Tr . (v ^ <*1*>) = z ) ) ) ) ) );