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 that
A1: s1 is Accept-Halt and
A2: s1 = [ the InitS of tm1,h,t] and
A3: s2 is Accept-Halt and
A4: s2 = [ the InitS of tm2,((Result s1) `2),((Result s1) `3)] and
A5: 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
A6: ((Computation s1) . k) `1 = the AcceptS of tm1 and
A7: Result s1 = (Computation s1) . k and
A8: for i being Element of NAT st i < k holds
((Computation s1) . i) `1 <> the AcceptS of tm1 by A1, Th16;
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 ) );
A9: 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 A10: S1[i] ; :: thesis: S1[i + 1]
now
set s1i1 = (Computation s1) . (i + 1);
set s1i = (Computation s1) . i;
set s3i1 = (Computation s3) . (i + 1);
set s3i = (Computation s3) . i;
A11: i < i + 1 by XREAL_1:29;
set f = TRAN ((Computation s3) . i);
reconsider h = Head ((Computation s1) . i) as Element of INT ;
reconsider ss1 = ((Computation s1) . i) `3 as Tape of tm1 ;
reconsider y = ss1 . h as Symbol of tm1 ;
reconsider ss3 = ((Computation s3) . i) `3 as Tape of (tm1 ';' tm2) ;
set p = ((Computation s1) . i) `1 ;
set g = TRAN ((Computation s1) . i);
assume A12: 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 )
then A13: i < k by A11, XXREAL_0:2;
then A14: ((Computation s1) . i) `1 <> the AcceptS of tm1 by A8;
A15: ((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 A10, A12, A11, Def32, XXREAL_0:2;
hence contradiction by A14, ZFMISC_1:27; :: thesis: verum
end;
A16: TRAN ((Computation s3) . i) = the Tran of (tm1 ';' tm2) . [[(((Computation s1) . i) `1), the InitS of tm2],y] by A10, A12, A11, XXREAL_0:2
.= [[((TRAN ((Computation s1) . i)) `1), the InitS of tm2],((TRAN ((Computation s1) . i)) `2),((TRAN ((Computation s1) . i)) `3)] by A8, A13, Th48 ;
then A17: (TRAN ((Computation s1) . i)) `2 = (TRAN ((Computation s3) . i)) `2 by MCART_1:def 6;
A18: (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 A15, Def7 ;
A19: (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 A14, Def7 ;
hence [(((Computation s1) . (i + 1)) `1), the InitS of tm2] = [((TRAN ((Computation s1) . i)) `1), the InitS of tm2] by MCART_1:def 5
.= (TRAN ((Computation s3) . i)) `1 by A16, MCART_1:def 5
.= ((Computation s3) . (i + 1)) `1 by A18, 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 A16, MCART_1:def 7;
hence ((Computation s1) . (i + 1)) `2 = (Head ((Computation s3) . i)) + (offset (TRAN ((Computation s3) . i))) by A10, A12, A11, A19, MCART_1:def 6, XXREAL_0:2
.= ((Computation s3) . (i + 1)) `2 by A18, 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 A10, A12, A11, A19, MCART_1:def 7, XXREAL_0:2
.= ((Computation s3) . (i + 1)) `3 by A10, A12, A11, A17, A18, 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;
A20: s3 = [[ the InitS of tm1, the InitS of tm2],h,t] by A5, Def32;
A21: 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 )
A22: ((Computation s3) . 0) `1 = s3 `1 by Def8
.= [ the InitS of tm1, the InitS of tm2] by A20, MCART_1:64 ;
((Computation s1) . 0) `1 = s1 `1 by Def8
.= the InitS of tm1 by A2, MCART_1:64 ;
hence [(((Computation s1) . 0) `1), the InitS of tm2] = ((Computation s3) . 0) `1 by A22; :: 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 A2, MCART_1:64
.= s3 `2 by A5, MCART_1:64
.= ((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 A2, MCART_1:64
.= s3 `3 by A5, MCART_1:64
.= ((Computation s3) . 0) `3 by Def8 ; :: thesis: verum
end;
A23: for i being Element of NAT holds S1[i] from NAT_1:sch 1(A21, A9);
 then A24: ((Computation s1) . k) `2 = ((Computation s3) . k) `2 ;
consider m being Element of NAT such that
A25: ((Computation s2) . m) `1 = the AcceptS of tm2 and
A26: Result s2 = (Computation s2) . m and
A27: for i being Element of NAT st i < m holds
((Computation s2) . i) `1 <> the AcceptS of tm2 by A3, 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 ) );
A28: 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 A29: S2[i] ; :: thesis: S2[i + 1]
now
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;
A30: i < i + 1 by XREAL_1:29;
reconsider ssk = ((Computation ((Computation s3) . k)) . i) `3 as Tape of (tm1 ';' tm2) ;
set f = TRAN ((Computation ((Computation s3) . k)) . i);
set q = ((Computation s2) . i) `1 ;
set g = TRAN ((Computation s2) . i);
reconsider h = Head ((Computation s2) . i) as Element of INT ;
reconsider ss2 = ((Computation s2) . i) `3 as Tape of tm2 ;
reconsider y = ss2 . h as Symbol of tm2 ;
assume A31: 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 )
then A32: TRAN ((Computation ((Computation s3) . k)) . i) = the Tran of (tm1 ';' tm2) . [[ the AcceptS of tm1,(((Computation s2) . i) `1)],y] by A29, A30, 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 A33: (TRAN ((Computation s2) . i)) `2 = (TRAN ((Computation ((Computation s3) . k)) . i)) `2 by MCART_1:def 6;
i < m by A31, A30, XXREAL_0:2;
then A34: ((Computation s2) . i) `1 <> the AcceptS of tm2 by A27;
A35: ((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 A29, A31, A30, Def32, XXREAL_0:2;
hence contradiction by A34, ZFMISC_1:27; :: thesis: verum
end;
A36: (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 A35, Def7 ;
A37: (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 A34, Def7 ;
hence [ the AcceptS of tm1,(((Computation s2) . (i + 1)) `1)] = [ the AcceptS of tm1,((TRAN ((Computation s2) . i)) `1)] by MCART_1:def 5
.= (TRAN ((Computation ((Computation s3) . k)) . i)) `1 by A32, MCART_1:def 5
.= ((Computation ((Computation s3) . k)) . (i + 1)) `1 by A36, 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 A32, MCART_1:def 7;
hence ((Computation s2) . (i + 1)) `2 = (Head ((Computation ((Computation s3) . k)) . i)) + (offset (TRAN ((Computation ((Computation s3) . k)) . i))) by A29, A31, A30, A37, MCART_1:def 6, XXREAL_0:2
.= ((Computation ((Computation s3) . k)) . (i + 1)) `2 by A36, 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 A29, A31, A30, A37, MCART_1:def 7, XXREAL_0:2
.= ((Computation ((Computation s3) . k)) . (i + 1)) `3 by A29, A31, A30, A33, A36, MCART_1:def 7, XXREAL_0:2 ; :: thesis: verum
end;
hence S2[i + 1] ; :: thesis: verum
end;
A38: ((Computation s1) . k) `3 = ((Computation s3) . k) `3 by A23;
set s2m = (Computation s2) . m;
set skm = (Computation ((Computation s3) . k)) . m;
A39: (Computation s3) . (k + m) = (Computation ((Computation s3) . k)) . m by Th13;
A40: [(((Computation s1) . k) `1), the InitS of tm2] = ((Computation s3) . k) `1 by A23;
A41: 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 A4, MCART_1:64
.= ((Computation ((Computation s3) . k)) . 0) `1 by A6, A40, 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 A4, A7, A24, MCART_1:64
.= ((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 A4, A7, A38, MCART_1:64
.= ((Computation ((Computation s3) . k)) . 0) `3 by Def8 ; :: thesis: verum
end;
A42: for i being Element of NAT holds S2[i] from NAT_1:sch 1(A41, A28);
 then [ the AcceptS of tm1,(((Computation s2) . m) `1)] = ((Computation ((Computation s3) . k)) . m) `1 ;
then A43: ((Computation s3) . (k + m)) `1 = the AcceptS of (tm1 ';' tm2) by A25, A39, Def32;
hence A44: s3 is Accept-Halt by Def9; :: thesis: ( (Result s3) `2 = (Result s2) `2 & (Result s3) `3 = (Result s2) `3 )
( ((Computation s2) . m) `2 = ((Computation ((Computation s3) . k)) . m) `2 & ((Computation s2) . m) `3 = ((Computation ((Computation s3) . k)) . m) `3 ) by A42;
hence ( (Result s3) `2 = (Result s2) `2 & (Result s3) `3 = (Result s2) `3 ) by A26, A39, A43, A44, Def10; :: thesis: verum