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_halting_on s )
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_halting_on s )
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_halting_on s ) )
assume that
A1: p0 >= 3 and
A2: f is_FinSequence_on s,p0 and
A3: len f = n ; :: thesis: ( (IExec ((sum (n,p0)),s)) . (intpos 1) = Sum f & sum (n,p0) is_halting_on s )
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))),s);
set t2 = IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))),s);
set t3 = IExec (((GBP := 0) ';' ((intpos 1) := 0)),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))),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))),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))),s)) . (intpos (p0 + i)) = (Exec (((intpos 3) := (p0 + 1)),(IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))),s)))) . (intpos (p0 + i)) by SCMPDS_5:46
.= (IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))),s)) . (intpos (p0 + i)) by A8, SCMPDS_2:57
.= (Exec (((intpos 2) := (- n)),(IExec (((GBP := 0) ';' ((intpos 1) := 0)),s)))) . (intpos (p0 + i)) by SCMPDS_5:46
.= (IExec (((GBP := 0) ';' ((intpos 1) := 0)),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))),s),p0 by SCPISORT:def 1;
B12: f is_FinSequence_on Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),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))),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))),s))) . (intpos (p0 + i))
then f . i = (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))),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))),s))) . (intpos (p0 + i)) by SCMPDS_5:40; :: thesis: verum

end;

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