let s be 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:
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; :: 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; :: 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
.= (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;
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
.= Sum h by A5, A20, RVSUM_1:104 ;
:: thesis:

end;

hereby :: thesis:

let i be Element of NAT ; :: thesis:
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
.= 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: