let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: 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 ) )
assume that
A1: p0 >= 3 and
A2: f is_FinSequence_on s,p0 and
A3: 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,s);
set Q1 = P;
set t2 = IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))),P,s);
set t3 = IExec (((GBP := 0) ';' ((intpos 1) := 0)),P,s);
set t4 = Exec ((GBP := 0),(Initialize s));

now

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len f implies (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,s)) . (intpos (p0 + i)) = f . i )
assume that
A4: 1 <= i and
A5: i <= len f ; :: thesis: (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,s)) . (intpos (p0 + i)) = f . i
A6: p0 + 1 >= 3 + 1 by A1, XREAL_1:8;
A7: p0 + i >= p0 + 1 by A4, XREAL_1:8;
then p0 + i <> 3 by A6, XXREAL_0:2;
then A8: intpos (p0 + i) <> intpos 3 by ZFMISC_1:33;
p0 + i <> 0 by A6, A7, XXREAL_0:2;
then A9: intpos (p0 + i) <> GBP by ZFMISC_1:33;
p0 + i <> 1 by A6, A7, XXREAL_0:2;
then A10: intpos (p0 + i) <> intpos 1 by ZFMISC_1:33;
p0 + i <> 2 by A6, A7, XXREAL_0:2;
then A11: intpos (p0 + i) <> intpos 2 by ZFMISC_1:33;
thus (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,s)) . (intpos (p0 + i)) = (Exec (((intpos 3) := (p0 + 1)),(IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))),P,s)))) . (intpos (p0 + i)) by SCMPDS_5:46
.= (IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))),P,s)) . (intpos (p0 + i)) by A8, SCMPDS_2:57
.= (Exec (((intpos 2) := (- n)),(IExec (((GBP := 0) ';' ((intpos 1) := 0)),P,s)))) . (intpos (p0 + i)) by SCMPDS_5:46
.= (IExec (((GBP := 0) ';' ((intpos 1) := 0)),P,s)) . (intpos (p0 + i)) by A11, SCMPDS_2:57
.= (Exec (((intpos 1) := 0),(Exec ((GBP := 0),(Initialize s))))) . (intpos (p0 + i)) by SCMPDS_5:47
.= (Exec ((GBP := 0),(Initialize s))) . (intpos (p0 + i)) by A10, SCMPDS_2:57
.= (Initialize s) . (intpos (p0 + i)) by A9, SCMPDS_2:57
.= s . (intpos (p0 + i)) by SCMPDS_5:40
.= f . i by A2, A4, A5, SCPISORT:def 1 ; :: thesis: verum

end;

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

proof

let i be Element of 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,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,s))) . (intpos (p0 + i))
then f . i = (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,s)) . (intpos (p0 + i)) by A12, SCPISORT:def 1;
hence f . i = (Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,s))) . (intpos (p0 + i)) by SCMPDS_5:40; :: thesis: verum

end;

A14: (Exec ((GBP := 0),(Initialize s))) . GBP = 0 by SCMPDS_2:57;
A15: (IExec (((GBP := 0) ';' ((intpos 1) := 0)),P,s)) . GBP = (Exec (((intpos 1) := 0),(Exec ((GBP := 0),(Initialize s))))) . GBP by SCMPDS_5:47
.= 0 by A14, AMI_3:52, SCMPDS_2:57 ;
A16: (IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))),P,s)) . GBP = (Exec (((intpos 2) := (- n)),(IExec (((GBP := 0) ';' ((intpos 1) := 0)),P,s)))) . GBP by SCMPDS_5:46
.= 0 by A15, AMI_3:52, SCMPDS_2:57 ;
A17: (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,s)) . (intpos 3) = (Exec (((intpos 3) := (p0 + 1)),(IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))),P,s)))) . (intpos 3) by SCMPDS_5:46
.= p0 + 1 by SCMPDS_2:57 ;
A18: (Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,s))) . (intpos 3) = (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,s)) . (intpos 3) by SCMPDS_5:40;
A19: (IExec (((GBP := 0) ';' ((intpos 1) := 0)),P,s)) . (intpos 1) = (Exec (((intpos 1) := 0),(Exec ((GBP := 0),(Initialize s))))) . (intpos 1) by SCMPDS_5:47
.= 0 by SCMPDS_2:57 ;
A20: (IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))),P,s)) . (intpos 1) = (Exec (((intpos 2) := (- n)),(IExec (((GBP := 0) ';' ((intpos 1) := 0)),P,s)))) . (intpos 1) by SCMPDS_5:46
.= 0 by A19, AMI_3:52, SCMPDS_2:57 ;
A21: (Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,s))) . (intpos 1) = (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,s)) . (intpos 1) by SCMPDS_5:40;
A22: (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,s)) . (intpos 1) = (Exec (((intpos 3) := (p0 + 1)),(IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))),P,s)))) . (intpos 1) by SCMPDS_5:46
.= 0 by A20, AMI_3:52, SCMPDS_2:57 ;
A23: (IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))),P,s)) . (intpos 2) = (Exec (((intpos 2) := (- n)),(IExec (((GBP := 0) ';' ((intpos 1) := 0)),P,s)))) . (intpos 2) by SCMPDS_5:46
.= - n by SCMPDS_2:57 ;
A24: (Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,s))) . (intpos 2) = (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,s)) . (intpos 2) by SCMPDS_5:40;
A25: (Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,s))) . GBP = (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,s)) . GBP by SCMPDS_5:40;
A26: (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,s)) . (intpos 2) = (Exec (((intpos 3) := (p0 + 1)),(IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))),P,s)))) . (intpos 2) by SCMPDS_5:46
.= - n by A23, AMI_3:52, SCMPDS_2:57 ;
A27: (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,s)) . GBP = (Exec (((intpos 3) := (p0 + 1)),(IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))),P,s)))) . GBP by SCMPDS_5:46
.= 0 by A16, AMI_3:52, SCMPDS_2:57 ;
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,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,s)),P ) by A1, A3, A22, A26, A17, Lm3, A13, A18, A21, A24, A25;
then A28: ( 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,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,s),P ) by SCMPDS_6:139, SCMPDS_6:140;
IExec ((while<0 (GBP,2,(((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))))),P,(IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,s))) = 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,s)))) by SCMPDS_5:48;
then (IExec ((while<0 (GBP,2,(((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))))),P,(IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),P,s)))) . (intpos 1) = Sum f by A1, A3, A27, A22, A26, A17, Lm3, A13, A18, A21, A24, A25;
hence (IExec ((sum (n,p0)),P,s)) . (intpos 1) = Sum f by A28, SCPISORT:8; :: thesis: sum (n,p0) is_halting_on s,P
thus sum (n,p0) is_halting_on s,P by A28, SCPISORT:10; :: thesis: verum