:: deftheorem defines TRAN TURING_1:def 5 :
for T being TuringStr
for s being All-State of T holds TRAN s = the Tran of T . [(s `1_3),((s `3_3) . (Head s))];