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 States of t1,{the InitS of t2}:] by ZFMISC_1:def 2;
then A3: [p,the InitS of t2] in [:the States of t1,{the InitS of t2}:] \/ [:{the AcceptS of t1},the States 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