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_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;
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 ;
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 ;
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 ;
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 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 A1, A3, A19, A21, A16, A12, Lm3;
(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, A12, Lm3;
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