let tm1, tm2 be TuringStr ; :: thesis: for s1 being All-State of tm1
for h being Element of NAT
for t being Tape of tm1
for s2 being All-State of tm2
for s3 being All-State of (tm1 ';' tm2) st s1 is Accept-Halt & s1 = [the InitS of tm1,h,t] & s2 is Accept-Halt & s2 = [the InitS of tm2,((Result s1) `2 ),((Result s1) `3 )] & s3 = [the InitS of (tm1 ';' tm2),h,t] holds
( s3 is Accept-Halt & (Result s3) `2 = (Result s2) `2 & (Result s3) `3 = (Result s2) `3 )
let s1 be All-State of tm1; :: thesis: for h being Element of NAT
for t being Tape of tm1
for s2 being All-State of tm2
for s3 being All-State of (tm1 ';' tm2) st s1 is Accept-Halt & s1 = [the InitS of tm1,h,t] & s2 is Accept-Halt & s2 = [the InitS of tm2,((Result s1) `2 ),((Result s1) `3 )] & s3 = [the InitS of (tm1 ';' tm2),h,t] holds
( s3 is Accept-Halt & (Result s3) `2 = (Result s2) `2 & (Result s3) `3 = (Result s2) `3 )
let h be Element of NAT ; :: thesis: for t being Tape of tm1
for s2 being All-State of tm2
for s3 being All-State of (tm1 ';' tm2) st s1 is Accept-Halt & s1 = [the InitS of tm1,h,t] & s2 is Accept-Halt & s2 = [the InitS of tm2,((Result s1) `2 ),((Result s1) `3 )] & s3 = [the InitS of (tm1 ';' tm2),h,t] holds
( s3 is Accept-Halt & (Result s3) `2 = (Result s2) `2 & (Result s3) `3 = (Result s2) `3 )
let t be Tape of tm1; :: thesis: for s2 being All-State of tm2
for s3 being All-State of (tm1 ';' tm2) st s1 is Accept-Halt & s1 = [the InitS of tm1,h,t] & s2 is Accept-Halt & s2 = [the InitS of tm2,((Result s1) `2 ),((Result s1) `3 )] & s3 = [the InitS of (tm1 ';' tm2),h,t] holds
( s3 is Accept-Halt & (Result s3) `2 = (Result s2) `2 & (Result s3) `3 = (Result s2) `3 )
let s2 be All-State of tm2; :: thesis: for s3 being All-State of (tm1 ';' tm2) st s1 is Accept-Halt & s1 = [the InitS of tm1,h,t] & s2 is Accept-Halt & s2 = [the InitS of tm2,((Result s1) `2 ),((Result s1) `3 )] & s3 = [the InitS of (tm1 ';' tm2),h,t] holds
( s3 is Accept-Halt & (Result s3) `2 = (Result s2) `2 & (Result s3) `3 = (Result s2) `3 )
let s3 be All-State of (tm1 ';' tm2); :: thesis: ( s1 is Accept-Halt & s1 = [the InitS of tm1,h,t] & s2 is Accept-Halt & s2 = [the InitS of tm2,((Result s1) `2 ),((Result s1) `3 )] & s3 = [the InitS of (tm1 ';' tm2),h,t] implies ( s3 is Accept-Halt & (Result s3) `2 = (Result s2) `2 & (Result s3) `3 = (Result s2) `3 ) )
set p0 = the InitS of tm1;
set q0 = the InitS of tm2;
assume A1: ( s1 is Accept-Halt & s1 = [the InitS of tm1,h,t] & s2 is Accept-Halt & s2 = [the InitS of tm2,((Result s1) `2 ),((Result s1) `3 )] & s3 = [the InitS of (tm1 ';' tm2),h,t] ) ; :: thesis: ( s3 is Accept-Halt & (Result s3) `2 = (Result s2) `2 & (Result s3) `3 = (Result s2) `3 )
set pF = the AcceptS of tm1;
set qF = the AcceptS of tm2;
consider k being Element of NAT such that
A2: ( ((Computation s1) . k) `1 = the AcceptS of tm1 & Result s1 = (Computation s1) . k & ( for i being Element of NAT st i < k holds
((Computation s1) . i) `1 <> the AcceptS of tm1 ) ) by A1, Th16;
A3: s3 = [[the InitS of tm1,the InitS of tm2],h,t] by A1, Def32;
defpred S1[ Element of NAT ] means ( $1 <= k implies ( [(((Computation s1) . $1) `1 ),the InitS of tm2] = ((Computation s3) . $1) `1 & ((Computation s1) . $1) `2 = ((Computation s3) . $1) `2 & ((Computation s1) . $1) `3 = ((Computation s3) . $1) `3 ) );
A4: S1[ 0 ]
proof
assume 0 <= k ; :: thesis: ( [(((Computation s1) . 0 ) `1 ),the InitS of tm2] = ((Computation s3) . 0 ) `1 & ((Computation s1) . 0 ) `2 = ((Computation s3) . 0 ) `2 & ((Computation s1) . 0 ) `3 = ((Computation s3) . 0 ) `3 )
A5: ((Computation s1) . 0 ) `1 = s1 `1 by Def8
.= the InitS of tm1 by A1, MCART_1:68 ;
((Computation s3) . 0 ) `1 = s3 `1 by Def8
.= [the InitS of tm1,the InitS of tm2] by A3, MCART_1:68 ;
hence [(((Computation s1) . 0 ) `1 ),the InitS of tm2] = ((Computation s3) . 0 ) `1 by A5; :: thesis: ( ((Computation s1) . 0 ) `2 = ((Computation s3) . 0 ) `2 & ((Computation s1) . 0 ) `3 = ((Computation s3) . 0 ) `3 )
thus ((Computation s1) . 0 ) `2 = s1 `2 by Def8
.= h by A1, MCART_1:68
.= s3 `2 by A1, MCART_1:68
.= ((Computation s3) . 0 ) `2 by Def8 ; :: thesis: ((Computation s1) . 0 ) `3 = ((Computation s3) . 0 ) `3
thus ((Computation s1) . 0 ) `3 = s1 `3 by Def8
.= t by A1, MCART_1:68
.= s3 `3 by A1, MCART_1:68
.= ((Computation s3) . 0 ) `3 by Def8 ; :: thesis: verum
end;
A6: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; :: thesis: ( S1[i] implies S1[i + 1] )
assume A7: S1[i] ; :: thesis: S1[i + 1]
now
assume A8: i + 1 <= k ; :: thesis: ( [(((Computation s1) . (i + 1)) `1 ),the InitS of tm2] = ((Computation s3) . (i + 1)) `1 & ((Computation s1) . (i + 1)) `2 = ((Computation s3) . (i + 1)) `2 & ((Computation s1) . (i + 1)) `3 = ((Computation s3) . (i + 1)) `3 )
set s1i1 = (Computation s1) . (i + 1);
set s1i = (Computation s1) . i;
set s3i1 = (Computation s3) . (i + 1);
set s3i = (Computation s3) . i;
A9: i < i + 1 by XREAL_1:31;
then A10: i < k by A8, XXREAL_0:2;
reconsider ss1 = ((Computation s1) . i) `3 as Tape of tm1 ;
reconsider ss3 = ((Computation s3) . i) `3 as Tape of (tm1 ';' tm2) ;
reconsider h = Head ((Computation s1) . i) as Element of INT ;
reconsider y = ss1 . h as Symbol of tm1 ;
set p = ((Computation s1) . i) `1 ;
set g = TRAN ((Computation s1) . i);
A11: ((Computation s1) . i) `1 <> the AcceptS of tm1 by A2, A10;
A12: ((Computation s3) . i) `1 <> the AcceptS of (tm1 ';' tm2)
proof
assume ((Computation s3) . i) `1 = the AcceptS of (tm1 ';' tm2) ; :: thesis: contradiction
then [(((Computation s1) . i) `1 ),the InitS of tm2] = [the AcceptS of tm1,the AcceptS of tm2] by A7, A8, A9, Def32, XXREAL_0:2;
hence contradiction by A11, ZFMISC_1:33; :: thesis: verum
end;
set f = TRAN ((Computation s3) . i);
A13: TRAN ((Computation s3) . i) = the Tran of (tm1 ';' tm2) . [[(((Computation s1) . i) `1 ),the InitS of tm2],y] by A7, A8, A9, XXREAL_0:2
.= [[((TRAN ((Computation s1) . i)) `1 ),the InitS of tm2],((TRAN ((Computation s1) . i)) `2 ),((TRAN ((Computation s1) . i)) `3 )] by A2, A10, Th48 ;
then A14: (TRAN ((Computation s1) . i)) `2 = (TRAN ((Computation s3) . i)) `2 by MCART_1:def 6;
A15: (Computation s1) . (i + 1) = Following ((Computation s1) . i) by Def8
.= [((TRAN ((Computation s1) . i)) `1 ),(h + (offset (TRAN ((Computation s1) . i)))),(Tape-Chg ss1,h,((TRAN ((Computation s1) . i)) `2 ))] by A11, Def7 ;
A16: (Computation s3) . (i + 1) = Following ((Computation s3) . i) by Def8
.= [((TRAN ((Computation s3) . i)) `1 ),((Head ((Computation s3) . i)) + (offset (TRAN ((Computation s3) . i)))),(Tape-Chg ss3,(Head ((Computation s3) . i)),((TRAN ((Computation s3) . i)) `2 ))] by A12, Def7 ;
thus [(((Computation s1) . (i + 1)) `1 ),the InitS of tm2] = [((TRAN ((Computation s1) . i)) `1 ),the InitS of tm2] by A15, MCART_1:def 5
.= (TRAN ((Computation s3) . i)) `1 by A13, MCART_1:def 5
.= ((Computation s3) . (i + 1)) `1 by A16, MCART_1:def 5 ; :: thesis: ( ((Computation s1) . (i + 1)) `2 = ((Computation s3) . (i + 1)) `2 & ((Computation s1) . (i + 1)) `3 = ((Computation s3) . (i + 1)) `3 )
offset (TRAN ((Computation s1) . i)) = offset (TRAN ((Computation s3) . i)) by A13, MCART_1:def 7;
hence ((Computation s1) . (i + 1)) `2 = (Head ((Computation s3) . i)) + (offset (TRAN ((Computation s3) . i))) by A7, A8, A9, A15, MCART_1:def 6, XXREAL_0:2
.= ((Computation s3) . (i + 1)) `2 by A16, MCART_1:def 6 ;
:: thesis: ((Computation s1) . (i + 1)) `3 = ((Computation s3) . (i + 1)) `3
thus ((Computation s1) . (i + 1)) `3 = ss3 +* (h .--> ((TRAN ((Computation s1) . i)) `2 )) by A7, A8, A9, A15, MCART_1:def 7, XXREAL_0:2
.= ((Computation s3) . (i + 1)) `3 by A7, A8, A9, A14, A16, MCART_1:def 7, XXREAL_0:2 ; :: thesis: verum
end;
hence S1[i + 1] ; :: thesis: verum
end;
set s1k = (Computation s1) . k;
set s3k = (Computation s3) . k;
for i being Element of NAT holds S1[i] from NAT_1:sch 1(A4, A6);
 then A17: ( [(((Computation s1) . k) `1 ),the InitS of tm2] = ((Computation s3) . k) `1 & ((Computation s1) . k) `2 = ((Computation s3) . k) `2 & ((Computation s1) . k) `3 = ((Computation s3) . k) `3 ) ;
consider m being Element of NAT such that
A18: ( ((Computation s2) . m) `1 = the AcceptS of tm2 & Result s2 = (Computation s2) . m & ( for i being Element of NAT st i < m holds
((Computation s2) . i) `1 <> the AcceptS of tm2 ) ) by A1, Th16;
defpred S2[ Element of NAT ] means ( $1 <= m implies ( [the AcceptS of tm1,(((Computation s2) . $1) `1 )] = ((Computation ((Computation s3) . k)) . $1) `1 & ((Computation s2) . $1) `2 = ((Computation ((Computation s3) . k)) . $1) `2 & ((Computation s2) . $1) `3 = ((Computation ((Computation s3) . k)) . $1) `3 ) );
A19: S2[ 0 ]
proof
assume 0 <= m ; :: thesis: ( [the AcceptS of tm1,(((Computation s2) . 0 ) `1 )] = ((Computation ((Computation s3) . k)) . 0 ) `1 & ((Computation s2) . 0 ) `2 = ((Computation ((Computation s3) . k)) . 0 ) `2 & ((Computation s2) . 0 ) `3 = ((Computation ((Computation s3) . k)) . 0 ) `3 )
thus [the AcceptS of tm1,(((Computation s2) . 0 ) `1 )] = [the AcceptS of tm1,(s2 `1 )] by Def8
.= [the AcceptS of tm1,the InitS of tm2] by A1, MCART_1:68
.= ((Computation ((Computation s3) . k)) . 0 ) `1 by A2, A17, Def8 ; :: thesis: ( ((Computation s2) . 0 ) `2 = ((Computation ((Computation s3) . k)) . 0 ) `2 & ((Computation s2) . 0 ) `3 = ((Computation ((Computation s3) . k)) . 0 ) `3 )
thus ((Computation s2) . 0 ) `2 = s2 `2 by Def8
.= ((Computation s3) . k) `2 by A1, A2, A17, MCART_1:68
.= ((Computation ((Computation s3) . k)) . 0 ) `2 by Def8 ; :: thesis: ((Computation s2) . 0 ) `3 = ((Computation ((Computation s3) . k)) . 0 ) `3
thus ((Computation s2) . 0 ) `3 = s2 `3 by Def8
.= ((Computation s3) . k) `3 by A1, A2, A17, MCART_1:68
.= ((Computation ((Computation s3) . k)) . 0 ) `3 by Def8 ; :: thesis: verum
end;
A20: for i being Element of NAT st S2[i] holds
S2[i + 1]
proof
let i be Element of NAT ; :: thesis: ( S2[i] implies S2[i + 1] )
assume A21: S2[i] ; :: thesis: S2[i + 1]
now
assume A22: i + 1 <= m ; :: thesis: ( [the AcceptS of tm1,(((Computation s2) . (i + 1)) `1 )] = ((Computation ((Computation s3) . k)) . (i + 1)) `1 & ((Computation s2) . (i + 1)) `2 = ((Computation ((Computation s3) . k)) . (i + 1)) `2 & ((Computation s2) . (i + 1)) `3 = ((Computation ((Computation s3) . k)) . (i + 1)) `3 )
set s2i1 = (Computation s2) . (i + 1);
set s2i = (Computation s2) . i;
set ski1 = (Computation ((Computation s3) . k)) . (i + 1);
set ski = (Computation ((Computation s3) . k)) . i;
A23: i < i + 1 by XREAL_1:31;
then A24: i < m by A22, XXREAL_0:2;
reconsider ss2 = ((Computation s2) . i) `3 as Tape of tm2 ;
reconsider ssk = ((Computation ((Computation s3) . k)) . i) `3 as Tape of (tm1 ';' tm2) ;
reconsider h = Head ((Computation s2) . i) as Element of INT ;
reconsider y = ss2 . h as Symbol of tm2 ;
set q = ((Computation s2) . i) `1 ;
set g = TRAN ((Computation s2) . i);
A25: ((Computation s2) . i) `1 <> the AcceptS of tm2 by A18, A24;
A26: ((Computation ((Computation s3) . k)) . i) `1 <> the AcceptS of (tm1 ';' tm2)
proof
assume ((Computation ((Computation s3) . k)) . i) `1 = the AcceptS of (tm1 ';' tm2) ; :: thesis: contradiction
then [the AcceptS of tm1,(((Computation s2) . i) `1 )] = [the AcceptS of tm1,the AcceptS of tm2] by A21, A22, A23, Def32, XXREAL_0:2;
hence contradiction by A25, ZFMISC_1:33; :: thesis: verum
end;
set f = TRAN ((Computation ((Computation s3) . k)) . i);
A27: TRAN ((Computation ((Computation s3) . k)) . i) = the Tran of (tm1 ';' tm2) . [[the AcceptS of tm1,(((Computation s2) . i) `1 )],y] by A21, A22, A23, XXREAL_0:2
.= [[the AcceptS of tm1,((TRAN ((Computation s2) . i)) `1 )],((TRAN ((Computation s2) . i)) `2 ),((TRAN ((Computation s2) . i)) `3 )] by Th49 ;
then A28: (TRAN ((Computation s2) . i)) `2 = (TRAN ((Computation ((Computation s3) . k)) . i)) `2 by MCART_1:def 6;
A29: (Computation s2) . (i + 1) = Following ((Computation s2) . i) by Def8
.= [((TRAN ((Computation s2) . i)) `1 ),(h + (offset (TRAN ((Computation s2) . i)))),(Tape-Chg ss2,h,((TRAN ((Computation s2) . i)) `2 ))] by A25, Def7 ;
A30: (Computation ((Computation s3) . k)) . (i + 1) = Following ((Computation ((Computation s3) . k)) . i) by Def8
.= [((TRAN ((Computation ((Computation s3) . k)) . i)) `1 ),((Head ((Computation ((Computation s3) . k)) . i)) + (offset (TRAN ((Computation ((Computation s3) . k)) . i)))),(Tape-Chg ssk,(Head ((Computation ((Computation s3) . k)) . i)),((TRAN ((Computation ((Computation s3) . k)) . i)) `2 ))] by A26, Def7 ;
thus [the AcceptS of tm1,(((Computation s2) . (i + 1)) `1 )] = [the AcceptS of tm1,((TRAN ((Computation s2) . i)) `1 )] by A29, MCART_1:def 5
.= (TRAN ((Computation ((Computation s3) . k)) . i)) `1 by A27, MCART_1:def 5
.= ((Computation ((Computation s3) . k)) . (i + 1)) `1 by A30, MCART_1:def 5 ; :: thesis: ( ((Computation s2) . (i + 1)) `2 = ((Computation ((Computation s3) . k)) . (i + 1)) `2 & ((Computation s2) . (i + 1)) `3 = ((Computation ((Computation s3) . k)) . (i + 1)) `3 )
offset (TRAN ((Computation s2) . i)) = offset (TRAN ((Computation ((Computation s3) . k)) . i)) by A27, MCART_1:def 7;
hence ((Computation s2) . (i + 1)) `2 = (Head ((Computation ((Computation s3) . k)) . i)) + (offset (TRAN ((Computation ((Computation s3) . k)) . i))) by A21, A22, A23, A29, MCART_1:def 6, XXREAL_0:2
.= ((Computation ((Computation s3) . k)) . (i + 1)) `2 by A30, MCART_1:def 6 ;
:: thesis: ((Computation s2) . (i + 1)) `3 = ((Computation ((Computation s3) . k)) . (i + 1)) `3
thus ((Computation s2) . (i + 1)) `3 = ssk +* (h .--> ((TRAN ((Computation s2) . i)) `2 )) by A21, A22, A23, A29, MCART_1:def 7, XXREAL_0:2
.= ((Computation ((Computation s3) . k)) . (i + 1)) `3 by A21, A22, A23, A28, A30, MCART_1:def 7, XXREAL_0:2 ; :: thesis: verum
end;
hence S2[i + 1] ; :: thesis: verum
end;
set s2m = (Computation s2) . m;
set skm = (Computation ((Computation s3) . k)) . m;
for i being Element of NAT holds S2[i] from NAT_1:sch 1(A19, A20);
 then A31: ( [the AcceptS of tm1,(((Computation s2) . m) `1 )] = ((Computation ((Computation s3) . k)) . m) `1 & ((Computation s2) . m) `2 = ((Computation ((Computation s3) . k)) . m) `2 & ((Computation s2) . m) `3 = ((Computation ((Computation s3) . k)) . m) `3 ) ;
A32: (Computation s3) . (k + m) = (Computation ((Computation s3) . k)) . m by Th13;
then A33: ((Computation s3) . (k + m)) `1 = the AcceptS of (tm1 ';' tm2) by A18, A31, Def32;
hence s3 is Accept-Halt by Def9; :: thesis: ( (Result s3) `2 = (Result s2) `2 & (Result s3) `3 = (Result s2) `3 )
hence ( (Result s3) `2 = (Result s2) `2 & (Result s3) `3 = (Result s2) `3 ) by A18, A31, A32, A33, Def10; :: thesis: verum