let s be State of SCMPDS ; :: thesis: for I being Program of SCMPDS
for J being shiftable Program of SCMPDS 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 holds
( I ';' J is_closed_on s & I ';' J is_halting_on s )
let I be Program of SCMPDS ; :: thesis: for J being shiftable Program of SCMPDS 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 holds
( I ';' J is_closed_on s & I ';' J is_halting_on s )
let J be shiftable Program of SCMPDS ; :: 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 implies ( I ';' J is_closed_on s & I ';' J is_halting_on s ) )
set sE = IExec I,s;
assume A1: ( I is_closed_on s & I is_halting_on s & J is_closed_on IExec I,s & J is_halting_on IExec I,s ) ; :: thesis: ( I ';' J is_closed_on s & I ';' J is_halting_on s )
set IJ = I ';' J;
set sIJ = stop (I ';' J);
set IsIJ = Initialized (stop (I ';' J));
set spI = stop I;
set IsI = Initialized (stop I);
set ss = s +* (Initialized (stop (I ';' J)));
A2: s +* (Initialized (stop (I ';' J))) = s +* ((I ';' (J ';' (Stop SCMPDS ))) +* (Start-At (inspos 0 ))) by SCMPDS_4:46;
A3: stop (I ';' J) c= s +* (Initialized (stop (I ';' J))) by FUNCT_4:26, SCMPDS_4:57;
set spJ = stop J;
set IsJ = Initialized (stop J);
set s1 = s +* (Initialized (stop I));
set m1 = LifeSpan (s +* (Initialized (stop I)));
set sm = Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))));
set s3 = (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J));
set m3 = LifeSpan ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)));
A4: DataPart ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))) = (DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) +* (DataPart (Initialized (stop J))) by FUNCT_4:75;

A5: now

let x be set ; :: thesis: ( x in dom (DataPart (Initialized (stop J))) implies (DataPart (Initialized (stop J))) . b₁ = (DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) . b₁ )
assume x in dom (DataPart (Initialized (stop J))) ; :: thesis: (DataPart (Initialized (stop J))) . b₁ = (DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) . b₁
then A6: x in (dom (Initialized (stop J))) /\ SCM-Data-Loc by FUNCT_1:68, SCMPDS_2:100;
then A7: ( x in dom (Initialized (stop J)) & x in SCM-Data-Loc ) by XBOOLE_0:def 4;

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

suppose A8: x in dom (stop J) ; :: thesis: (DataPart (Initialized (stop J))) . b₁ = (DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) . b₁

dom (stop J) c= NAT by AMI_1:def 40;
then reconsider l = x as Instruction-Location of SCMPDS by A8, AMI_1:def 4;
l = x ;
hence (DataPart (Initialized (stop J))) . x = (DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) . x by A7, SCMPDS_4:22; :: thesis: verum

end;

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

hence (DataPart (Initialized (stop J))) . x = (DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) . x by A6, SCMPDS_3:6, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

A9: Initialized (stop J) c= (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)) by FUNCT_4:26;
then dom (Initialized (stop J)) c= dom ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))) by GRFUNC_1:8;
then A10: dom (Initialized (stop J)) c= the carrier of SCMPDS by AMI_1:79;
dom (DataPart (Initialized (stop J))) = (dom (Initialized (stop J))) /\ SCM-Data-Loc by RELAT_1:90, SCMPDS_2:100;
then dom (DataPart (Initialized (stop J))) c= the carrier of SCMPDS /\ SCM-Data-Loc by A10, XBOOLE_1:26;
then dom (DataPart (Initialized (stop J))) c= (dom (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) /\ SCM-Data-Loc by AMI_1:79;
then dom (DataPart (Initialized (stop J))) c= dom (DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) by RELAT_1:90, SCMPDS_2:100;
then DataPart (Initialized (stop J)) c= DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) by A5, GRFUNC_1:8;
then A11: DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = DataPart ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))) by A4, LATTICE2:8;
set s4 = Computation (s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I))));
A12: DataPart (Computation (s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = DataPart ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))) by A1, A2, A11, Th38, SCMPDS_4:24;
A13: ( J is_closed_on Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))) & J is_halting_on Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))) ) by A1, Th42;
then A14: J is_closed_on (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)) by SCMPDS_6:38;
A15: (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)) is halting by A13, SCMPDS_6:def 3;
A16: dom (stop I) c= dom (stop (I ';' J)) by SCMPDS_5:16;
stop (I ';' J) = I ';' (J ';' (Stop SCMPDS )) by SCMPDS_4:46
.= I +* (Shift (stop J),(card I)) ;
then Shift (stop J),(card I) c= stop (I ';' J) by FUNCT_4:26;
then Shift (stop J),(card I) c= s +* (Initialized (stop (I ';' J))) by A3, XBOOLE_1:1;
then A17: Shift (stop J),(card I) c= Computation (s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I)))) by AMI_1:81;

now

let k be Element of NAT ; :: thesis: IC (Computation (s +* (Initialized (stop (I ';' J)))),b₁) in dom (stop (I ';' J))

per cases ( k <= LifeSpan (s +* (Initialized (stop I))) or k > LifeSpan (s +* (Initialized (stop I))) ) ;

suppose k <= LifeSpan (s +* (Initialized (stop I))) ; :: thesis: IC (Computation (s +* (Initialized (stop (I ';' J)))),b₁) in dom (stop (I ';' J))

then IC (Computation (s +* (Initialized (stop (I ';' J)))),k) in dom (stop I) by A1, Th17, Th40;
hence IC (Computation (s +* (Initialized (stop (I ';' J)))),k) in dom (stop (I ';' J)) by A16; :: thesis: verum

end;

suppose A18: k > LifeSpan (s +* (Initialized (stop I))) ; :: thesis: IC (Computation (s +* (Initialized (stop (I ';' J)))),b₁) in dom (stop (I ';' J))

A19: IC (Computation (s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) in dom (stop I) by A1, Th17, Th40;

hereby :: thesis: verum

per cases ( IC (Computation (s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = inspos (card I) or CurInstr (Computation (s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = halt SCMPDS ) by A1, Th17, Th41;

suppose A20: IC (Computation (s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = inspos (card I) ; :: thesis: IC (Computation (s +* (Initialized (stop (I ';' J)))),k) in dom (stop (I ';' J))

consider ii being Nat such that
A21: k = (LifeSpan (s +* (Initialized (stop I)))) + ii by A18, NAT_1:10;
reconsider ii = ii as Element of NAT by ORDINAL1:def 13;
A22: (IC (Computation ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))),ii)) + (card I) = IC (Computation (Computation (s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I))))),ii) by A9, A12, A14, A17, A20, SCMPDS_6:45;
reconsider nn = IC (Computation ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))),ii) as Element of NAT by ORDINAL1:def 13;
inspos nn in dom (stop J) by A13, SCMPDS_6:def 2;
then nn < card (stop J) by SCMPDS_4:1;
then nn < (card J) + 1 by SCMPDS_5:7;
then A24: (card I) + nn < (card I) + ((card J) + 1) by XREAL_1:8;
A25: card (stop (I ';' J)) = (card (I ';' J)) + 1 by SCMPDS_5:7
.= ((card I) + (card J)) + 1 by SCMPDS_4:45 ;
IC (Computation (s +* (Initialized (stop (I ';' J)))),k) = (inspos nn) + (card I) by A21, A22, AMI_1:51
.= inspos (nn + (card I)) ;
hence IC (Computation (s +* (Initialized (stop (I ';' J)))),k) in dom (stop (I ';' J)) by A24, A25, SCMPDS_4:1; :: thesis: verum

end;

suppose CurInstr (Computation (s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = halt SCMPDS ; :: thesis: IC (Computation (s +* (Initialized (stop (I ';' J)))),k) in dom (stop (I ';' J))

then IC (Computation (s +* (Initialized (stop (I ';' J)))),k) = IC (Computation (s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) by A18, AMI_1:52;
hence IC (Computation (s +* (Initialized (stop (I ';' J)))),k) in dom (stop (I ';' J)) by A16, A19; :: thesis: verum

end;

end;

end;

end;

end;

end;

hence I ';' J is_closed_on s by SCMPDS_6:def 2; :: thesis: I ';' J is_halting_on s

per cases ( CurInstr (Computation (s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = halt SCMPDS or IC (Computation (s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = inspos (card I) ) by A1, Th17, Th41;

suppose CurInstr (Computation (s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = halt SCMPDS ; :: thesis: I ';' J is_halting_on s

then s +* (Initialized (stop (I ';' J))) is halting by AMI_1:def 20;
hence I ';' J is_halting_on s by SCMPDS_6:def 3; :: thesis: verum

end;

suppose IC (Computation (s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = inspos (card I) ; :: thesis: I ';' J is_halting_on s

then CurInstr (Computation ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))),(LifeSpan ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))) = CurInstr (Computation (Computation (s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I))))),(LifeSpan ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))) by A9, A12, A14, A17, SCMPDS_6:45;
then CurInstr (Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + (LifeSpan ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))))) = CurInstr (Computation ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))),(LifeSpan ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))) by AMI_1:51
.= halt SCMPDS by A15, AMI_1:def 46 ;
then s +* (Initialized (stop (I ';' J))) is halting by AMI_1:def 20;
hence I ';' J is_halting_on s by SCMPDS_6:def 3; :: thesis: verum

end;

end;