:: deftheorem Def18 defines SynTypes_Calculus-like PRELAMB:def 18 :
for IT being non empty typestr holds
( IT is SynTypes_Calculus-like iff ( ( for x being type of IT holds <*x*> ==>. x ) & ( for T being FinSequence of IT
for x, y being type of IT st T ^ <*y*> ==>. x holds
T ==>. x /" y ) & ( for T being FinSequence of IT
for x, y being type of IT st <*y*> ^ T ==>. x holds
T ==>. y \ x ) & ( for T, X, Y being FinSequence of IT
for x, y, z being type of IT st T ==>. y & (X ^ <*x*>) ^ Y ==>. z holds
((X ^ <*(x /" y)*>) ^ T) ^ Y ==>. z ) & ( for T, X, Y being FinSequence of IT
for x, y, z being type of IT st T ==>. y & (X ^ <*x*>) ^ Y ==>. z holds
((X ^ T) ^ <*(y \ x)*>) ^ Y ==>. z ) & ( for X, Y being FinSequence of IT
for x, y, z being type of IT st ((X ^ <*x*>) ^ <*y*>) ^ Y ==>. z holds
(X ^ <*(x * y)*>) ^ Y ==>. z ) & ( for X, Y being FinSequence of IT
for x, y being type of IT st X ==>. x & Y ==>. y holds
X ^ Y ==>. x * y ) ) );