:: deftheorem defines -compatible POLNOT_2:def 10 :
for T being Polish-language
for A being Polish-arity-function of T
for S being Polish-language holds
( S is A -compatible iff for s being FinSequence st s in S & s is T -headed holds
T -tail s in S ^^ (A . (T -head s)) );