:: deftheorem Def29 defines Uniontran TURING_1:def 29 :
for s, t being TuringStr
for x being Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):] holds
( ( ex p being State of s ex y being Symbol of s st
( x = [[p, the InitS of t],y] & p <> the AcceptS of s ) implies Uniontran (s,t,x) = FirstTuringTran (s,t,( the Tran of s . [(FirstTuringState x),(FirstTuringSymbol x)])) ) & ( ex q being State of t ex y being Symbol of t st x = [[ the AcceptS of s,q],y] implies Uniontran (s,t,x) = SecondTuringTran (s,t,( the Tran of t . [(SecondTuringState x),(SecondTuringSymbol x)])) ) & ( ( for p being State of s
for y being Symbol of s holds
( not x = [[p, the InitS of t],y] or not p <> the AcceptS of s ) ) & ( for q being State of t
for y being Symbol of t holds not x = [[ the AcceptS of s,q],y] ) implies Uniontran (s,t,x) = [(x `1),(x `2),(- 1)] ) );