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_{1} being set holds

( not stop p c= b_{1} or b_{1} 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;

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

( not stop p c= b

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;

end;

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;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

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;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