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 b₁ being set holds
( not stop p c= b₁ or b₁ 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)),(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 ;
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)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) by SCMPDS_4:def 7;
A4: 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 MEMSTR_0:45;
A5: I c= stop p by A1, Th1;
set s4 = Comput (P,s,(LifeSpan ((P +* (stop I)),(Initialize s))));
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 A7, A1, A6, FUNCT_4:98, XBOOLE_1:1;
then A9: 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 A4, A8, Th17;

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 A6, A5, Th15, A8, XBOOLE_1:1;

suppose A10: 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 8 :: 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 2; :: 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 A10; :: thesis: verum

end;

suppose A11: 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 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)),(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:4;
stop p = I ';' (J ';' (Stop SCMPDS)) by A1, AFINSQ_1:27
.= 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)),(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 A12, A2, A9, A11, A13, SCMPDS_4:29;
hence CurInstr (P,(Comput (P,s,m))) = halt SCMPDS by A3, EXTPRO_1:def 15; :: thesis: verum

end;

end;