set a = GBP ;
let s be State of SCMPDS ; :: thesis:
let n, p0 be Element of NAT ; :: thesis:
let f be FinSequence of INT ; :: thesis:
assume A1: ( p0 >= 3 & 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:

now

let t be State of SCMPDS ; :: thesis:
given g being FinSequence of INT such that A2: ( g is_FinSequence_on s,p0 & len g = (t . (intpos 2)) + n & t . (intpos 1) = Sum g & t . (intpos 3) = (p0 + 1) + (len g) ) ; :: thesis:
assume A3: ( t . GBP = 0 & t . (intpos 2) < 0 ) ; :: thesis:
assume A4: 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 A2, A3, 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 A2, A3, 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:

proof

consider h being FinSequence of INT such that
A5: ( len h = (len g) + 1 & h is_FinSequence_on s,p0 ) by SCPISORT:3;
take h ; :: thesis:
thus h is_FinSequence_on s,p0 by A5; :: thesis:
thus len h = ((t . (intpos 2)) + n) + 1 by A2, A5; :: 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 A2, A3, Lm1
.= (p0 + 1) + (len h) by A5 ; :: thesis:
set m = len h;
reconsider q = h . (len h) as Element of INT by INT_1:def 2;

A6: now

let i be Nat; :: thesis:
A7: i in NAT by ORDINAL1:def 13;
assume A8: ( 1 <= i & i <= len h ) ; :: thesis:

per cases ;

suppose i = len h ; :: thesis:

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

end;

suppose i <> len h ; :: thesis:

then i < len h by A8, XXREAL_0:1;
then A9: i <= len g by A5, INT_1:20;
then i in Seg (len g) by A8, FINSEQ_1:3;
then A10: i in dom g by FINSEQ_1:def 3;
thus h . i = s . (intpos (p0 + i)) by A5, A7, A8, SCPISORT:def 1
.= g . i by A2, A7, A8, A9, SCPISORT:def 1
.= (g ^ <*q*>) . i by A10, FINSEQ_1:def 7 ; :: thesis:

end;

len (g ^ <*q*>) = len h by A5, FINSEQ_2:19;
then A11: g ^ <*q*> = h by A6, FINSEQ_1:18;
A12: len h >= 1 by A5, NAT_1:11;
then A13: p0 + (len h) >= p0 + 1 by XREAL_1:8;
p0 + 1 > p0 by XREAL_1:31;
then A14: p0 + (len h) > p0 by A13, XXREAL_0:2;
h . (len h) = s . (intpos (p0 + (len h))) by A5, A12, SCPISORT:def 1
.= t . (intpos ((p0 + 1) + (len g))) by A4, A5, A14 ;
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 A2, A3, Lm1
.= Sum h by A2, A11, RVSUM_1:104 ;
:: thesis:

end;

hereby :: thesis:

let i be Element of NAT ; :: thesis:
assume A15: 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 A2, A3, Lm1
.= s . (intpos i) by A4, A15 ;
:: thesis:

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 A1, Lm2, Th8; :: thesis: