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_halting_on s,P )
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_halting_on s,P )
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_halting_on s,P )
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_halting_on s,P ) )
A1: Initialize s = s by MEMSTR_0:44;
assume that
A2: p0 >= 3 and
A3: f is_FinSequence_on s,p0 and
A4: len f = n ; :: thesis: ( (IExec ((sum (n,p0)),P,s)) . (intpos 1) = Sum f & sum (n,p0) is_halting_on s,P )
set a = GBP ;
set i1 = GBP := 0;
set i2 = (intpos 1) := 0;
set i3 = (intpos 2) := (- n);
set i4 = (intpos 3) := (p0 + 1);
set t0 = Initialize s;
set I4 = (((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1));
set t1 = IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s));
set Q1 = P;
set t2 = IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))),P,(Initialize s));
set t3 = IExec (((GBP := 0) ';' ((intpos 1) := 0)),P,(Initialize s));
set t4 = Exec ((GBP := 0),(Initialize s));

now :: thesis: for i being Nat st 1 <= i & i <= len f holds
(IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s))) . (intpos (p0 + i)) = f . i

let i be Nat; :: thesis: ( 1 <= i & i <= len f implies (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s))) . (intpos (p0 + i)) = f . i )
assume that
A5: 1 <= i and
A6: i <= len f ; :: thesis: (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s))) . (intpos (p0 + i)) = f . i
A7: p0 + 1 >= 3 + 1 by A2, XREAL_1:6;
A8: p0 + i >= p0 + 1 by A5, XREAL_1:6;
then p0 + i <> 3 by A7, XXREAL_0:2;
then A9: intpos (p0 + i) <> intpos 3 by XTUPLE_0:1;
p0 + i <> 0 by A8;
then A10: intpos (p0 + i) <> GBP by XTUPLE_0:1;
p0 + i <> 1 by A7, A8, XXREAL_0:2;
then A11: intpos (p0 + i) <> intpos 1 by XTUPLE_0:1;
p0 + i <> 2 by A7, A8, XXREAL_0:2;
then A12: intpos (p0 + i) <> intpos 2 by XTUPLE_0:1;
thus (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s))) . (intpos (p0 + i)) = (Exec (((intpos 3) := (p0 + 1)),(IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))),P,(Initialize s))))) . (intpos (p0 + i)) by SCMPDS_5:41
.= (IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))),P,(Initialize s))) . (intpos (p0 + i)) by A9, SCMPDS_2:45
.= (Exec (((intpos 2) := (- n)),(IExec (((GBP := 0) ';' ((intpos 1) := 0)),P,(Initialize s))))) . (intpos (p0 + i)) by SCMPDS_5:41
.= (IExec (((GBP := 0) ';' ((intpos 1) := 0)),P,(Initialize s))) . (intpos (p0 + i)) by A12, SCMPDS_2:45
.= (Exec (((intpos 1) := 0),(Exec ((GBP := 0),(Initialize s))))) . (intpos (p0 + i)) by SCMPDS_5:42
.= (Exec ((GBP := 0),(Initialize s))) . (intpos (p0 + i)) by A11, SCMPDS_2:45
.= (Initialize s) . (intpos (p0 + i)) by A10, SCMPDS_2:45
.= s . (intpos (p0 + i)) by SCMPDS_5:15
.= f . i by A3, A5, A6 ; :: thesis: verum

end;

then A13: f is_FinSequence_on IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s)),p0 ;
A14: f is_FinSequence_on Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s))),p0

proof

let i be Nat; :: according to SCPISORT:def 1 :: thesis: ( not 1 <= i or not i <= len f or f . i = (Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s)))) . (intpos (p0 + i)) )
assume ( 1 <= i & i <= len f ) ; :: thesis: f . i = (Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s)))) . (intpos (p0 + i))
then f . i = (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s))) . (intpos (p0 + i)) by A13;
hence f . i = (Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s)))) . (intpos (p0 + i)) by SCMPDS_5:15; :: thesis: verum

end;

A15: (Exec ((GBP := 0),(Initialize s))) . GBP = 0 by SCMPDS_2:45;
A16: (IExec (((GBP := 0) ';' ((intpos 1) := 0)),P,(Initialize s))) . GBP = (Exec (((intpos 1) := 0),(Exec ((GBP := 0),(Initialize s))))) . GBP by SCMPDS_5:42
.= 0 by A15, AMI_3:10, SCMPDS_2:45 ;
A17: (IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))),P,(Initialize s))) . GBP = (Exec (((intpos 2) := (- n)),(IExec (((GBP := 0) ';' ((intpos 1) := 0)),P,(Initialize s))))) . GBP by SCMPDS_5:41
.= 0 by A16, AMI_3:10, SCMPDS_2:45 ;
A18: (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s))) . (intpos 3) = (Exec (((intpos 3) := (p0 + 1)),(IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))),P,(Initialize s))))) . (intpos 3) by SCMPDS_5:41
.= p0 + 1 by SCMPDS_2:45 ;
A19: (Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s)))) . (intpos 3) = (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s))) . (intpos 3) by SCMPDS_5:15;
A20: (IExec (((GBP := 0) ';' ((intpos 1) := 0)),P,(Initialize s))) . (intpos 1) = (Exec (((intpos 1) := 0),(Exec ((GBP := 0),(Initialize s))))) . (intpos 1) by SCMPDS_5:42
.= 0 by SCMPDS_2:45 ;
A21: (IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))),P,(Initialize s))) . (intpos 1) = (Exec (((intpos 2) := (- n)),(IExec (((GBP := 0) ';' ((intpos 1) := 0)),P,(Initialize s))))) . (intpos 1) by SCMPDS_5:41
.= 0 by A20, AMI_3:10, SCMPDS_2:45 ;
A22: (Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s)))) . (intpos 1) = (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s))) . (intpos 1) by SCMPDS_5:15;
A23: (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s))) . (intpos 1) = (Exec (((intpos 3) := (p0 + 1)),(IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))),P,(Initialize s))))) . (intpos 1) by SCMPDS_5:41
.= 0 by A21, AMI_3:10, SCMPDS_2:45 ;
A24: (IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))),P,(Initialize s))) . (intpos 2) = (Exec (((intpos 2) := (- n)),(IExec (((GBP := 0) ';' ((intpos 1) := 0)),P,(Initialize s))))) . (intpos 2) by SCMPDS_5:41
.= - n by SCMPDS_2:45 ;
A25: (Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s)))) . (intpos 2) = (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s))) . (intpos 2) by SCMPDS_5:15;
A26: (Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s)))) . GBP = (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s))) . GBP by SCMPDS_5:15;
A27: (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s))) . (intpos 2) = (Exec (((intpos 3) := (p0 + 1)),(IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))),P,(Initialize s))))) . (intpos 2) by SCMPDS_5:41
.= - n by A24, AMI_3:10, SCMPDS_2:45 ;
A28: (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s))) . GBP = (Exec (((intpos 3) := (p0 + 1)),(IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))),P,(Initialize s))))) . GBP by SCMPDS_5:41
.= 0 by A17, AMI_3:10, SCMPDS_2:45 ;
then ( while<0 (GBP,2,(((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1)))) is_closed_on Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s))),P & while<0 (GBP,2,(((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1)))) is_halting_on Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s))),P ) by A2, A4, A23, A27, A18, Lm2, A14, A19, A22, A25, A26;
then A29: ( while<0 (GBP,2,(((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1)))) is_closed_on IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s)),P & while<0 (GBP,2,(((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1)))) is_halting_on IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s)),P ) by SCMPDS_6:125, SCMPDS_6:126;
IExec ((while<0 (GBP,2,(((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))))),P,(Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s))))) = IExec ((while<0 (GBP,2,(((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))))),P,(Initialize (Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s)))))) ;
then (IExec ((while<0 (GBP,2,(((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))))),P,(Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,(Initialize s)))))) . (intpos 1) = Sum f by A2, A4, A28, A23, A27, A18, Lm2, A14, A19, A22, A25, A26;
hence (IExec ((sum (n,p0)),P,s)) . (intpos 1) = Sum f by A29, A1, SCPISORT:7; :: thesis: sum (n,p0) is_halting_on s,P
thus sum (n,p0) is_halting_on s,P by A29, SCPISORT:9; :: thesis: verum