:: deftheorem defines FirstTuringTran TURING_1:def 23 :
for s, t being TuringStr
for x being Tran-Goal of s holds FirstTuringTran (s,t,x) = [[(x `1_3), the InitS of t],(x `2_3),(x `3_3)];