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