let p be Program of ; :: 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 7 :: thesis: for b1 being set holds
( not stop p c= b1 or b1 halts_on s )

let P be Instruction-Sequence of SCMPDS; :: 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)),());
set s3 = Initialize (Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),()))));
set P3 = (P +* (stop I)) +* (stop J);
set m3 = LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),()))))));
set D = SCM-Data-Loc ;
A2: stop J c= (P +* (stop I)) +* (stop J) by FUNCT_4:25;
then A3: (P +* (stop I)) +* (stop J) halts_on Initialize (Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),())))) by SCMPDS_4:def 7;
A4: DataPart (Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),())))) = DataPart (Initialize (Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),()))))) by MEMSTR_0:45;
A5: I c= stop p by ;
set s4 = Comput (P,s,(LifeSpan ((P +* (stop I)),())));
set P4 = P;
assume A6: stop p c= P ; :: thesis: P halts_on s
A7: p c= stop p by AFINSQ_1:74;
A8: s = Initialize s by MEMSTR_0:44;
P +* (I ';' J) = P by ;
then A9: DataPart (Comput (P,s,(LifeSpan ((P +* (stop I)),())))) = DataPart (Initialize (Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),()))))) by A4, A8, Th17;
per cases ( CurInstr (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),()))))) = halt SCMPDS or IC (Comput (P,s,(LifeSpan ((P +* (stop I)),())))) = card I ) by ;
suppose A10: CurInstr (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),()))))) = halt SCMPDS ; :: thesis: P halts_on s
take LifeSpan ((P +* (stop I)),()) ; :: according to EXTPRO_1:def 8 :: thesis: ( IC (Comput (P,s,(LifeSpan ((P +* (stop I)),())))) in proj1 P & CurInstr (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),()))))) = halt SCMPDS )
IC (Comput (P,s,(LifeSpan ((P +* (stop I)),())))) in NAT ;
hence IC (Comput (P,s,(LifeSpan ((P +* (stop I)),())))) in dom P by PARTFUN1:def 2; :: thesis: CurInstr (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),()))))) = halt SCMPDS
thus CurInstr (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),()))))) = halt SCMPDS by A10; :: thesis: verum
end;
suppose A11: IC (Comput (P,s,(LifeSpan ((P +* (stop I)),())))) = card I ; :: thesis: P halts_on s
reconsider m = (LifeSpan ((P +* (stop I)),())) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),()))))))) as Nat ;
take m ; :: according to EXTPRO_1:def 8 :: 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 2; :: thesis: CurInstr (P,(Comput (P,s,m))) = halt SCMPDS
A12: Comput (P,s,((LifeSpan ((P +* (stop I)),())) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),()))))))))) = Comput (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),())))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),())))))))) by EXTPRO_1:4;
stop p = I ';' (J ';' ()) by
.= I +* (Shift ((stop J),(card I))) ;
then Shift ((stop J),(card I)) c= stop p by FUNCT_4:25;
then A13: Shift ((stop J),(card I)) c= P by A6;
CurInstr (((P +* (stop I)) +* (stop J)),(Comput (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),()))))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),())))))))))) = CurInstr (P,(Comput (P,s,((LifeSpan ((P +* (stop I)),())) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),()))))))))))) by ;
hence CurInstr (P,(Comput (P,s,m))) = halt SCMPDS by ; :: thesis: verum
end;
end;