let p be Program of SCMPDS; :: thesis: ( p = I ';' J implies p is parahalting )
assume A1: p = I ';' J ; :: thesis: p is parahalting
let s be 0 -started State of SCMPDS; :: according to SCMPDS_4:def 10 :: thesis: for b₁ being set holds
( not stop p c= b₁ or b₁ halts_on s )
let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: ( not stop p c= P or P halts_on s )
set sIJ = stop p;
set spJ = stop J;
set s1 = Initialize s;
set P1 = P +* (stop I);
set m1 = LifeSpan ((P +* (stop I)),(Initialize s));
set s3 = Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))));
set P3 = (P +* (stop I)) +* (stop J);
set m3 = LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))));
set D = SCM-Data-Loc ;
A8: stop J c= (P +* (stop I)) +* (stop J) by FUNCT_4:26;
A9: (P +* (stop I)) +* (stop J) halts_on Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) by FUNCT_4:26, SCMPDS_4:def 10;
A11: DataPart (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = DataPart (Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by COMPOS_1:80
.= DataPart (Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) ;
A12: I c= stop p by A1, Th15;
set s4 = Comput (P,s,(LifeSpan ((P +* (stop I)),(Initialize s))));
set P4 = P;
assume A15: stop p c= P ; :: thesis: P halts_on s
p c= stop p by AFINSQ_1:78;
then B15: p c= P by A15, XBOOLE_1:1;
A16: s = Initialize s by COMPOS_1:78;
I ';' J c= P by B15, A1;
then P +* (I ';' J) = P by FUNCT_4:104;
then NPP (Comput (P,s,(LifeSpan ((P +* (stop I)),(Initialize s))))) = NPP (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) by A16, Th33;
then A17: DataPart (Comput (P,s,(LifeSpan ((P +* (stop I)),(Initialize s))))) = DataPart (Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by A11, COMPOS_1:138;

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

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

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

end;

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

reconsider m = (LifeSpan ((P +* (stop I)),(Initialize s))) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))))) as Element of NAT ;
take m ; :: according to EXTPRO_1:def 7 :: thesis: ( IC (Comput (P,s,m)) in proj1 P & CurInstr (P,(Comput (P,s,m))) = halt SCMPDS )
IC (Comput (P,s,m)) in NAT ;
hence IC (Comput (P,s,m)) in dom P by PARTFUN1:def 4; :: thesis: CurInstr (P,(Comput (P,s,m))) = halt SCMPDS
A20: Comput (P,s,((LifeSpan ((P +* (stop I)),(Initialize s))) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))))))) = Comput (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),(Initialize s))))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))))))) by EXTPRO_1:5;
stop p = I ';' (J ';' (Stop SCMPDS)) by A1, 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= P by A15, XBOOLE_1:1;
then A21: Shift ((stop J),(card I)) c= P ;
CurInstr (((P +* (stop I)) +* (stop J)),(Comput (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))))))))) = CurInstr (P,(Comput (P,s,((LifeSpan ((P +* (stop I)),(Initialize s))) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))))))))) by A20, A8, A17, A19, A21, SCMPDS_4:84;
hence CurInstr (P,(Comput (P,s,m))) = halt SCMPDS by A9, EXTPRO_1:def 14; :: thesis: verum

end;

end;