let p be Program of SCMPDS; :: thesis: ( p = I ';' J implies p is parahalting )
assume Z: p = I ';' J ; :: thesis: p is parahalting
let s be 0 -started State of SCMPDS; :: according to SCMPDS_4:def 10 :: thesis: ( not stop p c= s or ProgramPart s halts_on s )
set sIJ = stop p;
set spJ = stop J;
set s1 = (Initialize s) +* (stop I);
set m1 = LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)));
set s3 = (Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J);
set m3 = LifeSpan ((ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))),((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J)));
set D = SCM-Data-Loc ;
A1: DataPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J)) = (DataPart (Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))))) +* (DataPart (stop J)) by FUNCT_4:75;

A2: now

let x be set ; :: thesis: ( x in dom (DataPart (stop J)) implies (DataPart (stop J)) . b₁ = (DataPart (Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))))) . b₁ )
assume x in dom (DataPart (stop J)) ; :: thesis: (DataPart (stop J)) . b₁ = (DataPart (Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))))) . b₁
then A3: x in (dom (stop J)) /\ SCM-Data-Loc by RELAT_1:90, SCMPDS_2:100;
A5: x in SCM-Data-Loc by A3, XBOOLE_0:def 4;

per cases ( x in dom (stop J) or x = IC SCMPDS ) by A3, XBOOLE_0:def 4;

suppose A6: x in dom (stop J) ; :: thesis: (DataPart (stop J)) . b₁ = (DataPart (Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))))) . b₁

dom (stop J) c= NAT by RELAT_1:def 18;
then reconsider l = x as Element of NAT by A6;
(DataPart (stop J)) . l = (DataPart (Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))))) . l by A5, SCMPDS_4:22;
hence (DataPart (stop J)) . x = (DataPart (Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))))) . x ; :: thesis: verum

end;

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

hence (DataPart (stop J)) . x = (DataPart (Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))))) . x by A3, SCMPDS_3:6, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

A7: dom (DataPart (stop J)) = (dom (stop J)) /\ SCM-Data-Loc by RELAT_1:90, SCMPDS_2:100;
A8: stop J c= (Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J) by FUNCT_4:26;
A9: ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J)) halts_on (Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J) by FUNCT_4:26, SCMPDS_4:def 10;
dom (stop J) c= dom ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J)) by A8, GRFUNC_1:8;
then dom (stop J) c= the carrier of SCMPDS by PARTFUN1:def 4;
then dom (DataPart (stop J)) c= the carrier of SCMPDS /\ SCM-Data-Loc by A7, XBOOLE_1:26;
then dom (DataPart (stop J)) c= (dom (Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))))) /\ SCM-Data-Loc by PARTFUN1:def 4;
then dom (DataPart (stop J)) c= dom (DataPart (Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))))) by RELAT_1:90, SCMPDS_2:100;
then WW: DataPart (stop J) c= DataPart (Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) by A2, GRFUNC_1:8;
A10: DataPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = DataPart (Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) by COMPOS_1:80
.= DataPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J)) by A1, WW, LATTICE2:8 ;
A11: I c= stop p by Z, Th15;
set s4 = Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))));
UU: ProgramPart (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = ProgramPart s by AMI_1:123;
I1: (Initialize s) +* (stop p) = s +* (Initialize (stop p)) by COMPOS_1:125;
assume A12: stop p c= s ; :: thesis: ProgramPart s halts_on s
AA: s = Initialize s by COMPOS_1:78;
s = (Initialize s) +* (stop p) by A12, AA, FUNCT_4:79
.= s +* ((I ';' (J ';' (Stop SCMPDS))) +* (Start-At (0,SCMPDS))) by Z, I1, AFINSQ_1:30 ;
then Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))), Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) equal_outside NAT by Th33, FUNCT_7:28;
then A14: DataPart (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = DataPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J)) by A10, COMPOS_1:138;

per cases ( CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) = halt SCMPDS or IC (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = card I ) by A12, A11, Th31, AA, XBOOLE_1:1;

suppose A15: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) = halt SCMPDS ; :: thesis: ProgramPart s halts_on s

take LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) ; :: according to EXTPRO_1:def 7 :: thesis: ( IC (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) in proj1 (ProgramPart s) & CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) = halt SCMPDS )
IC (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) in NAT ;
hence IC (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) in dom (ProgramPart s) by COMPOS_1:34; :: thesis: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) = halt SCMPDS
thus CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) = halt SCMPDS by A15; :: thesis: verum

end;

suppose A16: IC (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = card I ; :: thesis: ProgramPart s halts_on s

reconsider m = (LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + (LifeSpan ((ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))),((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J)))) as Element of NAT ;
take m ; :: according to EXTPRO_1:def 7 :: thesis: ( IC (Comput ((ProgramPart s),s,m)) in proj1 (ProgramPart s) & CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,m))) = halt SCMPDS )
IC (Comput ((ProgramPart s),s,m)) in NAT ;
hence IC (Comput ((ProgramPart s),s,m)) in dom (ProgramPart s) by COMPOS_1:34; :: thesis: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,m))) = halt SCMPDS
x: Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + (LifeSpan ((ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))),((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J)))))) = Comput ((ProgramPart s),(Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))),(LifeSpan ((ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))),((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))))) by EXTPRO_1:5;
stop p = I ';' (J ';' (Stop SCMPDS)) by Z, AFINSQ_1:30
.= I +* (Shift ((stop J),(card I))) ;
then Shift ((stop J),(card I)) c= stop p by FUNCT_4:26;
then Shift ((stop J),(card I)) c= s by A12, XBOOLE_1:1;
then AA: Shift ((stop J),(card I)) c= Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) by AMI_1:81;
CurInstr ((ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))),(Comput ((ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))),((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J)),(LifeSpan ((ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))),((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))))))) = CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + (LifeSpan ((ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))),((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J)))))))) by x, A8, A14, A16, UU, AA, SCMPDS_4:84;
hence CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,m))) = halt SCMPDS by A9, EXTPRO_1:def 14; :: thesis: verum

end;

end;