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)),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)),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)),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)),s)) . (intpos 1) = Sum f & sum (n,p0) is parahalting )
thus (IExec ((sum (n,p0)),s)) . (intpos 1) = Sum f by A1, A2, Lm4; :: thesis: sum (n,p0) is parahalting

now

let t be State of SCMPDS; :: thesis: sum (n,p0) is_halting_on t
consider g being FinSequence of INT such that
W: ( len g = n & g is_FinSequence_on t,p0 ) by SCPISORT:3;
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 W, SCPISORT:def 1;
hence g . i = (Initialize t) . (intpos (p0 + i)) by SCMPDS_5:40; :: thesis: verum

end;

then sum (n,p0) is_halting_on Initialize t by A1, Lm4, W;
hence sum (n,p0) is_halting_on t by SCMPDS_6:140; :: thesis: verum

end;

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