let s be 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
ex g being FinSequence of INT st
( len g = n & g is_FinSequence_on t,p0 ) by SCPISORT:3;
hence sum n,p0 is_halting_on t by A1, Lm4; :: thesis: verum

end;

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