for T being TuringStr
for s being All-State of T st s `1_3 = the AcceptS of T holds
s = Following s by Def6;