:: deftheorem defines FirstTuringState TURING_1:def 25 :
for s, t being TuringStr
for x being Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):] holds FirstTuringState x = (x `1) `1 ;