let t1, t2 be TuringStr ; :: thesis: for g being Tran-Goal of t2
for q being State of t2
for y being Symbol of t2 st g = the Tran of t2 . [q,y] holds
the Tran of (t1 ';' t2) . [[ the AcceptS of t1,q],y] = [[ the AcceptS of t1,(g `1)],(g `2),(g `3)]
let g be Tran-Goal of t2; :: thesis: for q being State of t2
for y being Symbol of t2 st g = the Tran of t2 . [q,y] holds
the Tran of (t1 ';' t2) . [[ the AcceptS of t1,q],y] = [[ the AcceptS of t1,(g `1)],(g `2),(g `3)]
let q be State of t2; :: thesis: for y being Symbol of t2 st g = the Tran of t2 . [q,y] holds
the Tran of (t1 ';' t2) . [[ the AcceptS of t1,q],y] = [[ the AcceptS of t1,(g `1)],(g `2),(g `3)]
let y be Symbol of t2; :: thesis: ( g = the Tran of t2 . [q,y] implies the Tran of (t1 ';' t2) . [[ the AcceptS of t1,q],y] = [[ the AcceptS of t1,(g `1)],(g `2),(g `3)] )
assume A1: g = the Tran of t2 . [q,y] ; :: thesis: the Tran of (t1 ';' t2) . [[ the AcceptS of t1,q],y] = [[ the AcceptS of t1,(g `1)],(g `2),(g `3)]
set pF = the AcceptS of t1;
set x = [[ the AcceptS of t1,q],y];
the AcceptS of t1 in { the AcceptS of t1} by TARSKI:def 1;
then [ the AcceptS of t1,q] in [:{ the AcceptS of t1}, the FStates of t2:] by ZFMISC_1:def 2;
then A2: [ the AcceptS of t1,q] 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 = [[ the AcceptS of t1,q],y] as Element of [:(UnionSt (t1,t2)),( the Symbols of t1 \/ the Symbols of t2):] by A2, ZFMISC_1:def 2;
A3: SecondTuringState xx = [ the AcceptS of t1,q] `2 by MCART_1:def 1
.= q by MCART_1:def 2 ;
A4: SecondTuringSymbol xx = xx `2 by Def29
.= y by MCART_1:def 2 ;
thus the Tran of (t1 ';' t2) . [[ the AcceptS of t1,q],y] = (UnionTran (t1,t2)) . xx by Def32
.= Uniontran (t1,t2,xx) by Def31
.= SecondTuringTran (t1,t2,( the Tran of t2 . [q,y])) by A3, A4, Def30
.= [[ the AcceptS of t1,(g `1)],(g `2),(g `3)] by A1 ; :: thesis: verum