let P be Instruction-Sequence of SCMPDS; :: thesis:
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 ;
A1: Initialize s = s by MEMSTR_0:44;
assume that
A2: p0 >= 3 and
A3: ( 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 :: thesis:

let t be 0 -started State of SCMPDS; :: thesis:
let Q be Instruction-Sequence of SCMPDS; :: thesis:
A4: Initialize t = t by MEMSTR_0:44;
given g being FinSequence of INT such that A5: g is_FinSequence_on s,p0 and
A6: len g = (t . (intpos 2)) + n and
A7: t . (intpos 1) = Sum g and
A8: t . (intpos 3) = (p0 + 1) + (len g) ; :: thesis:
assume that
A9: t . GBP = 0 and
t . (intpos 2) < 0 ; :: thesis:
assume A10: 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))),Q,t)) . GBP = 0 by A8, A9, Lm1, A4; :: thesis:
thus ( ((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1)) is_closed_on t,Q & ((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1)) is_halting_on t,Q ) by SCMPDS_6:20, SCMPDS_6:21; :: thesis:
thus (IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),Q,t)) . (intpos 2) = (t . (intpos 2)) + 1 by A8, A9, Lm1, A4; :: 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))),Q,t)) . (intpos 3) = (p0 + 1) + (len g) & (IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),Q,t)) . (intpos 1) = Sum g ) :: thesis:

proof

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

A16: now :: thesis:

let i be Nat; :: thesis:
assume that
A17: 1 <= i and
A18: i <= len h ; :: thesis:

per cases ;

suppose i = len h ; :: thesis:

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

end;

suppose i <> len h ; :: thesis:

then i < len h by A18, XXREAL_0:1;
then A19: i <= len g by A11, INT_1:7;
then i in Seg (len g) by A17, FINSEQ_1:1;
then A20: i in dom g by FINSEQ_1:def 3;
thus h . i = s . (intpos (p0 + i)) by A12, A17, A18
.= g . i by A5, A17, A19
.= (g ^ <*q*>) . i by A20, FINSEQ_1:def 7 ; :: thesis:

end;

end;

end;

len (g ^ <*q*>) = len h by A11, FINSEQ_2:16;
then A21: g ^ <*q*> = h by A16, FINSEQ_1:14;
h . (len h) = s . (intpos (p0 + (len h))) by A12, A14
.= t . (intpos ((p0 + 1) + (len g))) by A10, A11, A15 ;
hence (IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),Q,t)) . (intpos 1) = (t . (intpos 1)) + (h . (len h)) by A8, A9, Lm1, A4
.= Sum h by A7, A21, RVSUM_1:74 ;
:: thesis:

end;

hereby :: thesis:

let i be Element of NAT ; :: thesis:
assume A22: i > p0 ; :: thesis:
then i > 3 by A2, XXREAL_0:2;
hence (IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),Q,t)) . (intpos i) = t . (intpos i) by A8, A9, Lm1, A4
.= s . (intpos i) by A10, A22 ;
:: thesis:

end;

end;

hence ( (IExec ((while<0 (GBP,2,(((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))))),P,(Initialize 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,P & while<0 (GBP,2,(((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1)))) is_halting_on s,P ) by A3, Th4, A1; :: thesis: