:: deftheorem Def31 defines ';' TURING_1:def 31 :
for T1, T2 being TuringStr
for b₃ being strict TuringStr holds
( b₃ = T1 ';' T2 iff ( the Symbols of b₃ = the Symbols of T1 \/ the Symbols of T2 & the FStates of b₃ = UnionSt (T1,T2) & the Tran of b₃ = UnionTran (T1,T2) & the InitS of b₃ = [ the InitS of T1, the InitS of T2] & the AcceptS of b₃ = [ the AcceptS of T1, the AcceptS of T2] ) );