let t1, t2 be TuringStr ; :: thesis: for g being Tran-Goal of t1
for p being State of t1
for y being Symbol of t1 st p <> the AcceptS of t1 & g = the Tran of t1 . [p,y] holds
the Tran of (t1 ';' t2) . [[p, the InitS of t2],y] = [[(g `1_3), the InitS of t2],(g `2_3),(g `3_3)]
let g be Tran-Goal of t1; :: thesis: for p being State of t1
for y being Symbol of t1 st p <> the AcceptS of t1 & g = the Tran of t1 . [p,y] holds
the Tran of (t1 ';' t2) . [[p, the InitS of t2],y] = [[(g `1_3), the InitS of t2],(g `2_3),(g `3_3)]
let p be State of t1; :: thesis: for y being Symbol of t1 st p <> the AcceptS of t1 & g = the Tran of t1 . [p,y] holds
the Tran of (t1 ';' t2) . [[p, the InitS of t2],y] = [[(g `1_3), the InitS of t2],(g `2_3),(g `3_3)]
let y be Symbol of t1; :: thesis: ( p <> the AcceptS of t1 & g = the Tran of t1 . [p,y] implies the Tran of (t1 ';' t2) . [[p, the InitS of t2],y] = [[(g `1_3), the InitS of t2],(g `2_3),(g `3_3)] )
assume that
A1: p <> the AcceptS of t1 and
A2: g = the Tran of t1 . [p,y] ; :: thesis: the Tran of (t1 ';' t2) . [[p, the InitS of t2],y] = [[(g `1_3), the InitS of t2],(g `2_3),(g `3_3)]
set q0 = the InitS of t2;
set x = [[p, the InitS of t2],y];
the InitS of t2 in { the InitS of t2} by TARSKI:def 1;
then [p, the InitS of t2] in [: the FStates of t1,{ the InitS of t2}:] by ZFMISC_1:def 2;
then A3: [p, the InitS of t2] in [: the FStates of t1,{ the InitS of t2}:] \/ [:{ the AcceptS of t1}, the FStates of t2:] by XBOOLE_0:def 3;
y in the Symbols of t1 \/ the Symbols of t2 by XBOOLE_0:def 3;
then reconsider xx = [[p, the InitS of t2],y] as Element of [:(UnionSt (t1,t2)),( the Symbols of t1 \/ the Symbols of t2):] by A3, ZFMISC_1:def 2;
A4: FirstTuringState xx = ([[p, the InitS of t2],y] `1) `1
.= [p, the InitS of t2] `1
.= p ;
A5: FirstTuringSymbol xx = [[p, the InitS of t2],y] `2 by Def27
.= y ;
thus the Tran of (t1 ';' t2) . [[p, the InitS of t2],y] = (UnionTran (t1,t2)) . xx by Def31
.= Uniontran (t1,t2,xx) by Def30
.= FirstTuringTran (t1,t2,( the Tran of t1 . [p,y])) by A1, A4, A5, Def29
.= [[(g `1_3), the InitS of t2],(g `2_3),(g `3_3)] by A2 ; :: thesis: verum