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_3)],(g `2_3),(g `3_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_3)],(g `2_3),(g `3_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_3)],(g `2_3),(g `3_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_3)],(g `2_3),(g `3_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_3)],(g `2_3),(g `3_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],y] `1) `2
.= q ;
A4: SecondTuringSymbol xx = [[ the AcceptS of t1,q],y] `2 by Def28
.= y ;
thus the Tran of (t1 ';' t2) . [[ the AcceptS of t1,q],y] = (UnionTran (t1,t2)) . xx by Def31
.= Uniontran (t1,t2,xx) by Def30
.= SecondTuringTran (t1,t2,( the Tran of t2 . [q,y])) by A3, A4, Def29
.= [[ the AcceptS of t1,(g `1_3)],(g `2_3),(g `3_3)] by A1 ; :: thesis: verum