let s be 0 -started State of SCMPDS; :: thesis:
let n, p0 be Element of NAT ; :: thesis:
let f be FinSequence of INT ; :: thesis:
set a = GBP ;
assume that
A1: p0 >= 3 and
A2: ( f is_FinSequence_on s,p0 & len f = n & s . (intpos 1) = 0 & s . GBP = 0 & s . (intpos 2) = - n & s . (intpos 3) = p0 + 1 ) ; :: thesis:

let t be State of SCMPDS; :: thesis:
given g being FinSequence of INT such that A3: g is_FinSequence_on s,p0 and
A4: len g = (t . (intpos 2)) + n and
A5: t . (intpos 1) = Sum g and
A6: t . (intpos 3) = (p0 + 1) + (len g) ; :: thesis:
assume that
A7: t . GBP = 0 and
t . (intpos 2) < 0 ; :: thesis:
X1: IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),t) = IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),(Initialize t)) by SCMPDS_5:48;
X2: (Initialize t) . (intpos 3) = t . (intpos 3) by SCMPDS_5:40;
X3: (Initialize t) . (intpos 1) = t . (intpos 1) by SCMPDS_5:40;
X4: (Initialize t) . GBP = t . GBP by SCMPDS_5:40;
X5: (Initialize t) . (intpos 2) = t . (intpos 2) by SCMPDS_5:40;
assume A8: for i being Element of NAT st i > p0 holds
t . (intpos i) = s . (intpos i) ; :: thesis:
thus (IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),t)) . GBP = 0 by A6, A7, Lm1, X1, X2, X4; :: thesis:
thus ( ((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1)) is_closed_on t & ((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1)) is_halting_on t ) by SCMPDS_6:34, SCMPDS_6:35; :: thesis:
thus (IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),t)) . (intpos 2) = (t . (intpos 2)) + 1 by A6, A7, Lm1, X1, X2, X4, X5; :: thesis:
thus ex g being FinSequence of INT st
( g is_FinSequence_on s,p0 & len g = ((t . (intpos 2)) + n) + 1 & (IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),t)) . (intpos 3) = (p0 + 1) + (len g) & (IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),t)) . (intpos 1) = Sum g ) :: thesis:

consider h being FinSequence of INT such that
A9: len h = (len g) + 1 and
A10: h is_FinSequence_on s,p0 by SCPISORT:3;
take h ; :: thesis:
thus h is_FinSequence_on s,p0 by A10; :: thesis:
thus len h = ((t . (intpos 2)) + n) + 1 by A4, A9; :: thesis:
thus (IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),t)) . (intpos 3) = ((p0 + 1) + (len g)) + 1 by A6, A7, Lm1, X1, X2, X4
.= (p0 + 1) + (len h) by A9 ; :: thesis:
A11: p0 + 1 > p0 by XREAL_1:31;
set m = len h;
A12: len h >= 1 by A9, NAT_1:11;
then p0 + (len h) >= p0 + 1 by XREAL_1:8;
then A13: p0 + (len h) > p0 by A11, XXREAL_0:2;
reconsider q = h . (len h) as Element of INT by INT_1:def 2;

A14: now

let i be Nat; :: thesis:
A15: i in NAT by ORDINAL1:def 13;
assume that
A16: 1 <= i and
A17: i <= len h ; :: thesis:

suppose i = len h ; :: thesis:

hence h . i = (g ^ <*q*>) . i by A9, FINSEQ_1:59; :: thesis:

end;

suppose i <> len h ; :: thesis:

then i < len h by A17, XXREAL_0:1;
then A18: i <= len g by A9, INT_1:20;
then i in Seg (len g) by A16, FINSEQ_1:3;
then A19: i in dom g by FINSEQ_1:def 3;
thus h . i = s . (intpos (p0 + i)) by A10, A15, A16, A17, SCPISORT:def 1
.= g . i by A3, A15, A16, A18, SCPISORT:def 1
.= (g ^ <*q*>) . i by A19, FINSEQ_1:def 7 ; :: thesis:

end;

end;

end;

len (g ^ <*q*>) = len h by A9, FINSEQ_2:19;
then A20: g ^ <*q*> = h by A14, FINSEQ_1:18;
Y0: (Initialize t) . (intpos ((p0 + 1) + (len g))) = t . (intpos ((p0 + 1) + (len g))) by SCMPDS_5:40;
h . (len h) = s . (intpos (p0 + (len h))) by A10, A12, SCPISORT:def 1
.= t . (intpos ((p0 + 1) + (len g))) by A8, A9, A13 ;
hence (IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),t)) . (intpos 1) = (t . (intpos 1)) + (h . (len h)) by A6, A7, Lm1, X1, X2, X3, X4, Y0
.= Sum h by A5, A20, RVSUM_1:104 ;
:: thesis:

end;

hereby :: thesis:

let i be Element of NAT ; :: thesis:
Y0: (Initialize t) . (intpos i) = t . (intpos i) by SCMPDS_5:40;
assume A21: i > p0 ; :: thesis:
then i > 3 by A1, XXREAL_0:2;
hence (IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),t)) . (intpos i) = t . (intpos i) by A6, A7, Lm1, X1, X2, X4, Y0
.= s . (intpos i) by A8, A21 ;
:: thesis:

end;

end;

hence ( (IExec ((while<0 (GBP,2,(((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))))),s)) . (intpos 1) = Sum f & while<0 (GBP,2,(((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1)))) is_closed_on s & while<0 (GBP,2,(((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1)))) is_halting_on s ) by A2, Lm2, Th8; :: thesis: