:: deftheorem defines -compatible POLNOT_2:def 9 :
for B being Polish-arity-function
for S being Polish-language holds
( S is B -compatible iff for s being FinSequence st s in S & s is dom B -headed holds
ex n being Nat st
( n = B . ((dom B) -head s) & (dom B) -tail s in S ^^ n ) );