:: deftheorem defines Head TURING_1:def 4 :
for T being TuringStr
for s being All-State of T holds Head s = s `2_3 ;