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), the InitS of t2],(g `2),(g `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), the InitS of t2],(g `2),(g `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), the InitS of t2],(g `2),(g `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), the InitS of t2],(g `2),(g `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), the InitS of t2],(g `2),(g `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] `1 by MCART_1:def 1
.= p by MCART_1:def 1 ;
A5: FirstTuringSymbol xx = xx `2 by Def28
.= y by MCART_1:def 2 ;
thus the Tran of (t1 ';' t2) . [[p, the InitS of t2],y] = (UnionTran (t1,t2)) . xx by Def32
.= Uniontran (t1,t2,xx) by Def31
.= FirstTuringTran (t1,t2,( the Tran of t1 . [p,y])) by A1, A4, A5, Def30
.= [[(g `1), the InitS of t2],(g `2),(g `3)] by A2 ; :: thesis: verum