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_3),((Result s1) `3_3)] & s3 = [ the InitS of (tm1 ';' tm2),h,t] holds
( s3 is Accept-Halt & (Result s3) `2_3 = (Result s2) `2_3 & (Result s3) `3_3 = (Result s2) `3_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_3),((Result s1) `3_3)] & s3 = [ the InitS of (tm1 ';' tm2),h,t] holds
( s3 is Accept-Halt & (Result s3) `2_3 = (Result s2) `2_3 & (Result s3) `3_3 = (Result s2) `3_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_3),((Result s1) `3_3)] & s3 = [ the InitS of (tm1 ';' tm2),h,t] holds
( s3 is Accept-Halt & (Result s3) `2_3 = (Result s2) `2_3 & (Result s3) `3_3 = (Result s2) `3_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_3),((Result s1) `3_3)] & s3 = [ the InitS of (tm1 ';' tm2),h,t] holds
( s3 is Accept-Halt & (Result s3) `2_3 = (Result s2) `2_3 & (Result s3) `3_3 = (Result s2) `3_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_3),((Result s1) `3_3)] & s3 = [ the InitS of (tm1 ';' tm2),h,t] holds
( s3 is Accept-Halt & (Result s3) `2_3 = (Result s2) `2_3 & (Result s3) `3_3 = (Result s2) `3_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_3),((Result s1) `3_3)] & s3 = [ the InitS of (tm1 ';' tm2),h,t] implies ( s3 is Accept-Halt & (Result s3) `2_3 = (Result s2) `2_3 & (Result s3) `3_3 = (Result s2) `3_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_3),((Result s1) `3_3)] and
A5: s3 = [ the InitS of (tm1 ';' tm2),h,t] ; :: thesis: ( s3 is Accept-Halt & (Result s3) `2_3 = (Result s2) `2_3 & (Result s3) `3_3 = (Result s2) `3_3 )
set pF = the AcceptS of tm1;
set qF = the AcceptS of tm2;
consider k being Nat such that
A6: ((Computation s1) . k) `1_3 = the AcceptS of tm1 and
A7: Result s1 = () . k and
A8: for i being Nat st i < k holds
(() . i) `1_3 <> the AcceptS of tm1 by ;
defpred S1[ Nat] means ( \$1 <= k implies ( [((() . \$1) `1_3), the InitS of tm2] = (() . \$1) `1_3 & (() . \$1) `2_3 = (() . \$1) `2_3 & (() . \$1) `3_3 = (() . \$1) `3_3 ) );
A9: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A10: S1[i] ; :: thesis: S1[i + 1]
now :: thesis: ( i + 1 <= k implies ( [((() . (i + 1)) `1_3), the InitS of tm2] = (() . (i + 1)) `1_3 & (() . (i + 1)) `2_3 = (() . (i + 1)) `2_3 & (() . (i + 1)) `3_3 = (() . (i + 1)) `3_3 ) )
set s1i1 = () . (i + 1);
set s1i = () . i;
set s3i1 = () . (i + 1);
set s3i = () . i;
A11: i < i + 1 by XREAL_1:29;
set f = TRAN (() . i);
reconsider h = Head (() . i) as Element of INT ;
reconsider ss1 = (() . i) `3_3 as Tape of tm1 ;
reconsider y = ss1 . h as Symbol of tm1 ;
reconsider ss3 = (() . i) `3_3 as Tape of (tm1 ';' tm2) ;
set p = (() . i) `1_3 ;
set g = TRAN (() . i);
assume A12: i + 1 <= k ; :: thesis: ( [((() . (i + 1)) `1_3), the InitS of tm2] = (() . (i + 1)) `1_3 & (() . (i + 1)) `2_3 = (() . (i + 1)) `2_3 & (() . (i + 1)) `3_3 = (() . (i + 1)) `3_3 )
then A13: i < k by ;
then A14: ((Computation s1) . i) `1_3 <> the AcceptS of tm1 by A8;
A15: ((Computation s3) . i) `1_3 <> the AcceptS of (tm1 ';' tm2)
proof
assume ((Computation s3) . i) `1_3 = the AcceptS of (tm1 ';' tm2) ; :: thesis: contradiction
then [((() . i) `1_3), the InitS of tm2] = [ the AcceptS of tm1, the AcceptS of tm2] by ;
hence contradiction by A14, XTUPLE_0:1; :: thesis: verum
end;
A16: TRAN (() . i) = the Tran of (tm1 ';' tm2) . [[((() . i) `1_3), the InitS of tm2],y] by
.= [[((TRAN (() . i)) `1_3), the InitS of tm2],((TRAN (() . i)) `2_3),((TRAN (() . i)) `3_3)] by ;
then A17: (TRAN (() . i)) `2_3 = (TRAN (() . i)) `2_3 ;
A18: () . (i + 1) = Following (() . i) by Def7
.= [((TRAN (() . i)) `1_3),((Head (() . i)) + (offset (TRAN (() . i)))),(Tape-Chg (ss3,(Head (() . i)),((TRAN (() . i)) `2_3)))] by ;
A19: () . (i + 1) = Following (() . i) by Def7
.= [((TRAN (() . i)) `1_3),(h + (offset (TRAN (() . i)))),(Tape-Chg (ss1,h,((TRAN (() . i)) `2_3)))] by ;
hence [((() . (i + 1)) `1_3), the InitS of tm2] = [((TRAN (() . i)) `1_3), the InitS of tm2]
.= (TRAN (() . i)) `1_3 by A16
.= (() . (i + 1)) `1_3 by A18 ;
:: thesis: ( (() . (i + 1)) `2_3 = (() . (i + 1)) `2_3 & (() . (i + 1)) `3_3 = (() . (i + 1)) `3_3 )
offset (TRAN (() . i)) = offset (TRAN (() . i)) by A16;
hence (() . (i + 1)) `2_3 = (Head (() . i)) + (offset (TRAN (() . i))) by
.= (() . (i + 1)) `2_3 by A18 ;
:: thesis: (() . (i + 1)) `3_3 = (() . (i + 1)) `3_3
thus (() . (i + 1)) `3_3 = ss3 +* (h .--> ((TRAN (() . i)) `2_3)) by
.= (() . (i + 1)) `3_3 by ; :: thesis: verum
end;
hence S1[i + 1] ; :: thesis: verum
end;
set s1k = () . k;
set s3k = () . k;
A20: s3 = [[ the InitS of tm1, the InitS of tm2],h,t] by ;
A21: S1[ 0 ]
proof
assume 0 <= k ; :: thesis: ( [((() . 0) `1_3), the InitS of tm2] = (() . 0) `1_3 & (() . 0) `2_3 = (() . 0) `2_3 & (() . 0) `3_3 = (() . 0) `3_3 )
A22: (() . 0) `1_3 = s3 `1_3 by Def7
.= [ the InitS of tm1, the InitS of tm2] by A20 ;
(() . 0) `1_3 = s1 `1_3 by Def7
.= the InitS of tm1 by A2 ;
hence [((() . 0) `1_3), the InitS of tm2] = (() . 0) `1_3 by A22; :: thesis: ( (() . 0) `2_3 = (() . 0) `2_3 & (() . 0) `3_3 = (() . 0) `3_3 )
thus (() . 0) `2_3 = s1 `2_3 by Def7
.= h by A2
.= s3 `2_3 by A5
.= (() . 0) `2_3 by Def7 ; :: thesis: (() . 0) `3_3 = (() . 0) `3_3
thus (() . 0) `3_3 = s1 `3_3 by Def7
.= t by A2
.= s3 `3_3 by A5
.= (() . 0) `3_3 by Def7 ; :: thesis: verum
end;
A23: for i being Nat holds S1[i] from NAT_1:sch 2(A21, A9);
then A24: ((Computation s1) . k) `2_3 = (() . k) `2_3 ;
consider m being Nat such that
A25: ((Computation s2) . m) `1_3 = the AcceptS of tm2 and
A26: Result s2 = () . m and
A27: for i being Nat st i < m holds
(() . i) `1_3 <> the AcceptS of tm2 by ;
defpred S2[ Nat] means ( \$1 <= m implies ( [ the AcceptS of tm1,((() . \$1) `1_3)] = ((Computation (() . k)) . \$1) `1_3 & (() . \$1) `2_3 = ((Computation (() . k)) . \$1) `2_3 & (() . \$1) `3_3 = ((Computation (() . k)) . \$1) `3_3 ) );
A28: for i being Nat st S2[i] holds
S2[i + 1]
proof
let i be Nat; :: thesis: ( S2[i] implies S2[i + 1] )
assume A29: S2[i] ; :: thesis: S2[i + 1]
now :: thesis: ( i + 1 <= m implies ( [ the AcceptS of tm1,((() . (i + 1)) `1_3)] = ((Computation (() . k)) . (i + 1)) `1_3 & (() . (i + 1)) `2_3 = ((Computation (() . k)) . (i + 1)) `2_3 & (() . (i + 1)) `3_3 = ((Computation (() . k)) . (i + 1)) `3_3 ) )
set s2i1 = () . (i + 1);
set s2i = () . i;
set ski1 = (Computation (() . k)) . (i + 1);
set ski = (Computation (() . k)) . i;
A30: i < i + 1 by XREAL_1:29;
reconsider ssk = ((Computation (() . k)) . i) `3_3 as Tape of (tm1 ';' tm2) ;
set f = TRAN ((Computation (() . k)) . i);
set q = (() . i) `1_3 ;
set g = TRAN (() . i);
reconsider h = Head (() . i) as Element of INT ;
reconsider ss2 = (() . i) `3_3 as Tape of tm2 ;
reconsider y = ss2 . h as Symbol of tm2 ;
assume A31: i + 1 <= m ; :: thesis: ( [ the AcceptS of tm1,((() . (i + 1)) `1_3)] = ((Computation (() . k)) . (i + 1)) `1_3 & (() . (i + 1)) `2_3 = ((Computation (() . k)) . (i + 1)) `2_3 & (() . (i + 1)) `3_3 = ((Computation (() . k)) . (i + 1)) `3_3 )
then A32: TRAN ((Computation (() . k)) . i) = the Tran of (tm1 ';' tm2) . [[ the AcceptS of tm1,((() . i) `1_3)],y] by
.= [[ the AcceptS of tm1,((TRAN (() . i)) `1_3)],((TRAN (() . i)) `2_3),((TRAN (() . i)) `3_3)] by Th44 ;
then A33: (TRAN (() . i)) `2_3 = (TRAN ((Computation (() . k)) . i)) `2_3 ;
i < m by ;
then A34: ((Computation s2) . i) `1_3 <> the AcceptS of tm2 by A27;
A35: ((Computation (() . k)) . i) `1_3 <> the AcceptS of (tm1 ';' tm2)
proof
assume ((Computation (() . k)) . i) `1_3 = the AcceptS of (tm1 ';' tm2) ; :: thesis: contradiction
then [ the AcceptS of tm1,((() . i) `1_3)] = [ the AcceptS of tm1, the AcceptS of tm2] by ;
hence contradiction by A34, XTUPLE_0:1; :: thesis: verum
end;
A36: (Computation (() . k)) . (i + 1) = Following ((Computation (() . k)) . i) by Def7
.= [((TRAN ((Computation (() . k)) . i)) `1_3),((Head ((Computation (() . k)) . i)) + (offset (TRAN ((Computation (() . k)) . i)))),(Tape-Chg (ssk,(Head ((Computation (() . k)) . i)),((TRAN ((Computation (() . k)) . i)) `2_3)))] by ;
A37: () . (i + 1) = Following (() . i) by Def7
.= [((TRAN (() . i)) `1_3),(h + (offset (TRAN (() . i)))),(Tape-Chg (ss2,h,((TRAN (() . i)) `2_3)))] by ;
hence [ the AcceptS of tm1,((() . (i + 1)) `1_3)] = [ the AcceptS of tm1,((TRAN (() . i)) `1_3)]
.= (TRAN ((Computation (() . k)) . i)) `1_3 by A32
.= ((Computation (() . k)) . (i + 1)) `1_3 by A36 ;
:: thesis: ( (() . (i + 1)) `2_3 = ((Computation (() . k)) . (i + 1)) `2_3 & (() . (i + 1)) `3_3 = ((Computation (() . k)) . (i + 1)) `3_3 )
offset (TRAN (() . i)) = offset (TRAN ((Computation (() . k)) . i)) by A32;
hence (() . (i + 1)) `2_3 = (Head ((Computation (() . k)) . i)) + (offset (TRAN ((Computation (() . k)) . i))) by
.= ((Computation (() . k)) . (i + 1)) `2_3 by A36 ;
:: thesis: (() . (i + 1)) `3_3 = ((Computation (() . k)) . (i + 1)) `3_3
thus (() . (i + 1)) `3_3 = ssk +* (h .--> ((TRAN (() . i)) `2_3)) by
.= ((Computation (() . k)) . (i + 1)) `3_3 by ; :: thesis: verum
end;
hence S2[i + 1] ; :: thesis: verum
end;
A38: ((Computation s1) . k) `3_3 = (() . k) `3_3 by A23;
set s2m = () . m;
set skm = (Computation (() . k)) . m;
A39: (Computation s3) . (k + m) = (Computation (() . k)) . m by Th10;
A40: [((() . k) `1_3), the InitS of tm2] = (() . k) `1_3 by A23;
A41: S2[ 0 ]
proof
assume 0 <= m ; :: thesis: ( [ the AcceptS of tm1,((() . 0) `1_3)] = ((Computation (() . k)) . 0) `1_3 & (() . 0) `2_3 = ((Computation (() . k)) . 0) `2_3 & (() . 0) `3_3 = ((Computation (() . k)) . 0) `3_3 )
thus [ the AcceptS of tm1,((() . 0) `1_3)] = [ the AcceptS of tm1,(s2 `1_3)] by Def7
.= [ the AcceptS of tm1, the InitS of tm2] by A4
.= ((Computation (() . k)) . 0) `1_3 by ; :: thesis: ( (() . 0) `2_3 = ((Computation (() . k)) . 0) `2_3 & (() . 0) `3_3 = ((Computation (() . k)) . 0) `3_3 )
thus (() . 0) `2_3 = s2 `2_3 by Def7
.= (() . k) `2_3 by A4, A7, A24
.= ((Computation (() . k)) . 0) `2_3 by Def7 ; :: thesis: (() . 0) `3_3 = ((Computation (() . k)) . 0) `3_3
thus (() . 0) `3_3 = s2 `3_3 by Def7
.= (() . k) `3_3 by A4, A7, A38
.= ((Computation (() . k)) . 0) `3_3 by Def7 ; :: thesis: verum
end;
A42: for i being Nat holds S2[i] from then [ the AcceptS of tm1,((() . m) `1_3)] = ((Computation (() . k)) . m) `1_3 ;
then A43: ((Computation s3) . (k + m)) `1_3 = the AcceptS of (tm1 ';' tm2) by ;
hence A44: s3 is Accept-Halt ; :: thesis: ( (Result s3) `2_3 = (Result s2) `2_3 & (Result s3) `3_3 = (Result s2) `3_3 )
( ((Computation s2) . m) `2_3 = ((Computation (() . k)) . m) `2_3 & (() . m) `3_3 = ((Computation (() . k)) . m) `3_3 ) by A42;
hence ( (Result s3) `2_3 = (Result s2) `2_3 & (Result s3) `3_3 = (Result s2) `3_3 ) by A26, A39, A43, A44, Def9; :: thesis: verum