let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for n, p0 being Element of NAT
for f being FinSequence of INT st p0 >= 3 & f is_FinSequence_on s,p0 & len f = n holds
( (IExec ((sum (n,p0)),P,s)) . (intpos 1) = Sum f & sum (n,p0) is parahalting )
let s be 0 -started State of SCMPDS; :: thesis: for n, p0 being Element of NAT
for f being FinSequence of INT st p0 >= 3 & f is_FinSequence_on s,p0 & len f = n holds
( (IExec ((sum (n,p0)),P,s)) . (intpos 1) = Sum f & sum (n,p0) is parahalting )
let n, p0 be Element of NAT ; :: thesis: for f being FinSequence of INT st p0 >= 3 & f is_FinSequence_on s,p0 & len f = n holds
( (IExec ((sum (n,p0)),P,s)) . (intpos 1) = Sum f & sum (n,p0) is parahalting )
let f be FinSequence of INT ; :: thesis: ( p0 >= 3 & f is_FinSequence_on s,p0 & len f = n implies ( (IExec ((sum (n,p0)),P,s)) . (intpos 1) = Sum f & sum (n,p0) is parahalting ) )
assume that
A1: p0 >= 3 and
A2: ( f is_FinSequence_on s,p0 & len f = n ) ; :: thesis: ( (IExec ((sum (n,p0)),P,s)) . (intpos 1) = Sum f & sum (n,p0) is parahalting )
thus (IExec ((sum (n,p0)),P,s)) . (intpos 1) = Sum f by A1, A2, Lm4; :: thesis: sum (n,p0) is parahalting

now

let t be State of SCMPDS; :: thesis: for Q being Instruction-Sequence of SCMPDS holds sum (n,p0) is_halting_on t,Q
let Q be Instruction-Sequence of SCMPDS; :: thesis: sum (n,p0) is_halting_on t,Q
consider g being FinSequence of INT such that
A3: ( len g = n & g is_FinSequence_on t,p0 ) by SCPISORT:2;
g is_FinSequence_on Initialize t,p0

proof

let i be Element of NAT ; :: according to SCPISORT:def 1 :: thesis: ( not 1 <= i or not i <= len g or g . i = (Initialize t) . (intpos (p0 + i)) )
assume ( 1 <= i & i <= len g ) ; :: thesis: g . i = (Initialize t) . (intpos (p0 + i))
then g . i = t . (intpos (p0 + i)) by A3, SCPISORT:def 1;
hence g . i = (Initialize t) . (intpos (p0 + i)) by SCMPDS_5:15; :: thesis: verum

end;

then sum (n,p0) is_halting_on Initialize t,Q by A1, Lm4, A3;
hence sum (n,p0) is_halting_on t,Q by SCMPDS_6:126; :: thesis: verum

end;

hence sum (n,p0) is parahalting by SCMPDS_6:21; :: thesis: verum