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