let I be No-StopCode Program of ; :: thesis: for J being shiftable Program of
for s, s1, s2 being State of st I is_closed_on s & I is_halting_on s & J is_closed_on IExec I,s & J is_halting_on IExec I,s & s2 = s +* (Initialized (stop (I ';' J))) & s1 = s +* (Initialized (stop I)) holds
( IC (Computation s2,(LifeSpan s1)) = inspos (card I) & DataPart (Computation s2,(LifeSpan s1)) = DataPart ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))) & Shift (stop J),(card I) c= Computation s2,(LifeSpan s1) & LifeSpan s2 = (LifeSpan s1) + (LifeSpan ((Result s1) +* (Initialized (stop J)))) )
let J be shiftable Program of ; :: thesis: for s, s1, s2 being State of st I is_closed_on s & I is_halting_on s & J is_closed_on IExec I,s & J is_halting_on IExec I,s & s2 = s +* (Initialized (stop (I ';' J))) & s1 = s +* (Initialized (stop I)) holds
( IC (Computation s2,(LifeSpan s1)) = inspos (card I) & DataPart (Computation s2,(LifeSpan s1)) = DataPart ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))) & Shift (stop J),(card I) c= Computation s2,(LifeSpan s1) & LifeSpan s2 = (LifeSpan s1) + (LifeSpan ((Result s1) +* (Initialized (stop J)))) )
let s, s1, s2 be State of ; :: thesis: ( I is_closed_on s & I is_halting_on s & J is_closed_on IExec I,s & J is_halting_on IExec I,s & s2 = s +* (Initialized (stop (I ';' J))) & s1 = s +* (Initialized (stop I)) implies ( IC (Computation s2,(LifeSpan s1)) = inspos (card I) & DataPart (Computation s2,(LifeSpan s1)) = DataPart ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))) & Shift (stop J),(card I) c= Computation s2,(LifeSpan s1) & LifeSpan s2 = (LifeSpan s1) + (LifeSpan ((Result s1) +* (Initialized (stop J)))) ) )
set IsI = Initialized (stop I);
set spJ = stop J;
set IsJ = Initialized (stop J);
set IJ = I ';' J;
set sIJ = stop (I ';' J);
set IsIJ = Initialized (stop (I ';' J));
set m1 = LifeSpan s1;
set sm = Computation s1,(LifeSpan s1);
set s3 = (Computation s1,(LifeSpan s1)) +* (Initialized (stop J));
set m3 = LifeSpan ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J)));
set sE = IExec I,s;
assume that
A1: I is_closed_on s and
A2: I is_halting_on s and
A3: J is_closed_on IExec I,s and
A4: J is_halting_on IExec I,s and
A5: s2 = s +* (Initialized (stop (I ';' J))) and
A6: s1 = s +* (Initialized (stop I)) ; :: thesis: ( IC (Computation s2,(LifeSpan s1)) = inspos (card I) & DataPart (Computation s2,(LifeSpan s1)) = DataPart ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))) & Shift (stop J),(card I) c= Computation s2,(LifeSpan s1) & LifeSpan s2 = (LifeSpan s1) + (LifeSpan ((Result s1) +* (Initialized (stop J)))) )
A7: DataPart ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))) = (DataPart (Computation s1,(LifeSpan s1))) +* (DataPart (Initialized (stop J))) by FUNCT_4:75;
set s4 = Computation s2,(LifeSpan s1);
thus A8: IC (Computation s2,(LifeSpan s1)) = inspos (card I) by A1, A2, A5, A6, Th17, Th44; :: thesis: ( DataPart (Computation s2,(LifeSpan s1)) = DataPart ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))) & Shift (stop J),(card I) c= Computation s2,(LifeSpan s1) & LifeSpan s2 = (LifeSpan s1) + (LifeSpan ((Result s1) +* (Initialized (stop J)))) )

A9: now

let x be set ; :: thesis: ( x in dom (DataPart (Initialized (stop J))) implies (DataPart (Initialized (stop J))) . b₁ = (DataPart (Computation s1,(LifeSpan s1))) . b₁ )
assume x in dom (DataPart (Initialized (stop J))) ; :: thesis: (DataPart (Initialized (stop J))) . b₁ = (DataPart (Computation s1,(LifeSpan s1))) . b₁
then A10: x in (dom (Initialized (stop J))) /\ SCM-Data-Loc by RELAT_1:90, SCMPDS_2:100;
then A11: x in dom (Initialized (stop J)) by XBOOLE_0:def 4;
A12: x in SCM-Data-Loc by A10, XBOOLE_0:def 4;

per cases ( x in dom (stop J) or x = IC SCMPDS ) by A11, SCMPDS_4:28;

suppose A13: x in dom (stop J) ; :: thesis: (DataPart (Initialized (stop J))) . b₁ = (DataPart (Computation s1,(LifeSpan s1))) . b₁

dom (stop J) c= NAT by RELAT_1:def 18;
then reconsider l = x as Instruction-Location of SCMPDS by A13, AMI_1:def 4;
l = x ;
hence (DataPart (Initialized (stop J))) . x = (DataPart (Computation s1,(LifeSpan s1))) . x by A12, SCMPDS_4:22; :: thesis: verum

end;

suppose x = IC SCMPDS ; :: thesis: (DataPart (Initialized (stop J))) . b₁ = (DataPart (Computation s1,(LifeSpan s1))) . b₁

hence (DataPart (Initialized (stop J))) . x = (DataPart (Computation s1,(LifeSpan s1))) . x by A10, SCMPDS_3:6, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

A14: dom (DataPart (Initialized (stop J))) = (dom (Initialized (stop J))) /\ SCM-Data-Loc by RELAT_1:90, SCMPDS_2:100;
A15: Initialized (stop J) c= (Computation s1,(LifeSpan s1)) +* (Initialized (stop J)) by FUNCT_4:26;
then dom (Initialized (stop J)) c= dom ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))) by GRFUNC_1:8;
then dom (Initialized (stop J)) c= the carrier of SCMPDS by AMI_1:79;
then dom (DataPart (Initialized (stop J))) c= the carrier of SCMPDS /\ SCM-Data-Loc by A14, XBOOLE_1:26;
then dom (DataPart (Initialized (stop J))) c= (dom (Computation s1,(LifeSpan s1))) /\ SCM-Data-Loc by AMI_1:79;
then dom (DataPart (Initialized (stop J))) c= dom (DataPart (Computation s1,(LifeSpan s1))) by RELAT_1:90, SCMPDS_2:100;
then DataPart (Initialized (stop J)) c= DataPart (Computation s1,(LifeSpan s1)) by A9, GRFUNC_1:8;
then A16: DataPart (Computation s1,(LifeSpan s1)) = DataPart ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))) by A7, LATTICE2:8;
s2 = s +* ((I ';' (J ';' (Stop SCMPDS ))) +* (Start-At (inspos 0 ))) by A5, SCMPDS_4:46;
hence A17: DataPart (Computation s2,(LifeSpan s1)) = DataPart ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))) by A1, A2, A6, A16, Th38, SCMPDS_4:24; :: thesis: ( Shift (stop J),(card I) c= Computation s2,(LifeSpan s1) & LifeSpan s2 = (LifeSpan s1) + (LifeSpan ((Result s1) +* (Initialized (stop J)))) )
reconsider m = (LifeSpan s1) + (LifeSpan ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J)))) as Element of NAT ;
A18: stop (I ';' J) c= Initialized (stop (I ';' J)) by SCMPDS_4:9;
stop (I ';' J) = I ';' (J ';' (Stop SCMPDS )) by SCMPDS_4:46
.= I +* (Shift (stop J),(card I)) ;
then A19: Shift (stop J),(card I) c= stop (I ';' J) by FUNCT_4:26;
Initialized (stop (I ';' J)) c= s2 by A5, FUNCT_4:26;
then stop (I ';' J) c= s2 by A18, XBOOLE_1:1;
then Shift (stop J),(card I) c= s2 by A19, XBOOLE_1:1;
hence A20: Shift (stop J),(card I) c= Computation s2,(LifeSpan s1) by AMI_1:81; :: thesis: LifeSpan s2 = (LifeSpan s1) + (LifeSpan ((Result s1) +* (Initialized (stop J))))
J is_halting_on Computation s1,(LifeSpan s1) by A2, A3, A4, A6, Th42;
then A21: ProgramPart ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))) halts_on (Computation s1,(LifeSpan s1)) +* (Initialized (stop J)) by SCMPDS_6:def 3;
J is_closed_on Computation s1,(LifeSpan s1) by A2, A3, A4, A6, Th42;
then A22: J is_closed_on (Computation s1,(LifeSpan s1)) +* (Initialized (stop J)) by SCMPDS_6:38;
then CurInstr (Computation ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))),(LifeSpan ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))))) = CurInstr (Computation (Computation s2,(LifeSpan s1)),(LifeSpan ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))))) by A15, A8, A17, A20, SCMPDS_6:45;
then CurInstr (Computation ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))),(LifeSpan ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))))) = CurInstr (Computation s2,((LifeSpan s1) + (LifeSpan ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J)))))) by AMI_1:51;
then A23: CurInstr (Computation s2,m) = halt SCMPDS by A21, AMI_1:def 46;

A24: now

let k be Element of NAT ; :: thesis: ( (LifeSpan s1) + k < m implies not CurInstr (Computation s2,((LifeSpan s1) + k)) = halt SCMPDS )
assume (LifeSpan s1) + k < m ; :: thesis: not CurInstr (Computation s2,((LifeSpan s1) + k)) = halt SCMPDS
then A25: k < LifeSpan ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))) by XREAL_1:8;
assume A26: CurInstr (Computation s2,((LifeSpan s1) + k)) = halt SCMPDS ; :: thesis: contradiction
CurInstr (Computation ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))),k) = CurInstr (Computation (Computation s2,(LifeSpan s1)),k) by A15, A22, A8, A17, A20, SCMPDS_6:45
.= halt SCMPDS by A26, AMI_1:51 ;
hence contradiction by A21, A25, AMI_1:def 46; :: thesis: verum

end;

now

let k be Element of NAT ; :: thesis: ( k < m implies CurInstr (Computation s2,b₁) <> halt SCMPDS )
assume A27: k < m ; :: thesis: CurInstr (Computation s2,b₁) <> halt SCMPDS

per cases ( k < LifeSpan s1 or LifeSpan s1 <= k ) ;

suppose k < LifeSpan s1 ; :: thesis: CurInstr (Computation s2,b₁) <> halt SCMPDS

hence CurInstr (Computation s2,k) <> halt SCMPDS by A1, A2, A5, A6, Th46; :: thesis: verum

end;

suppose LifeSpan s1 <= k ; :: thesis: CurInstr (Computation s2,b₁) <> halt SCMPDS

then consider kk being Nat such that
A28: (LifeSpan s1) + kk = k by NAT_1:10;
reconsider kk = kk as Element of NAT by ORDINAL1:def 13;
(LifeSpan s1) + kk = k by A28;
hence CurInstr (Computation s2,k) <> halt SCMPDS by A24, A27; :: thesis: verum

end;

end;

end;

then A29: for k being Element of NAT st CurInstr (Computation s2,k) = halt SCMPDS holds
m <= k ;
A30: ProgramPart s1 halts_on s1 by A2, A6, SCMPDS_6:def 3;
I ';' J is_halting_on s by A1, A2, A3, A4, Th43;
then ProgramPart s2 halts_on s2 by A5, SCMPDS_6:def 3;
then LifeSpan s2 = m by A23, A29, AMI_1:def 46;
hence LifeSpan s2 = (LifeSpan s1) + (LifeSpan ((Result s1) +* (Initialized (stop J)))) by A30, AMI_1:122; :: thesis: verum