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, Lm3; :: thesis: sum (n,p0) is parahalting
now :: thesis: for t being State of SCMPDS
for Q being Instruction-Sequence of SCMPDS holds sum (n,p0) is_halting_on t,Q
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 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;
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, Lm3, 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