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 ;
I: Initialize s = s by MEMSTR_0:44;
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:

now

let t be 0 -started State of SCMPDS; :: thesis:
let Q be Instruction-Sequence of SCMPDS; :: thesis:
T: Initialize t = t by MEMSTR_0:44;
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 A13: 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 A6, A7, Lm1, T; :: 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 A6, A7, Lm1, T; :: 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
A14: len h = (len g) + 1 and
A15: h is_FinSequence_on s,p0 by SCPISORT:2;
take h ; :: thesis:
thus h is_FinSequence_on s,p0 by A15; :: thesis:
thus len h = ((t . (intpos 2)) + n) + 1 by A4, A14; :: 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 A6, A7, Lm1, T
.= (p0 + 1) + (len h) by A14 ; :: thesis:
A16: p0 + 1 > p0 by XREAL_1:29;
set m = len h;
A17: len h >= 1 by A14, NAT_1:11;
then p0 + (len h) >= p0 + 1 by XREAL_1:6;
then A18: p0 + (len h) > p0 by A16, XXREAL_0:2;
reconsider q = h . (len h) as Element of INT by INT_1:def 2;

A19: now

let i be Nat; :: thesis:
A20: i in NAT by ORDINAL1:def 12;
assume that
A21: 1 <= i and
A22: i <= len h ; :: thesis:

per cases ;

suppose i = len h ; :: thesis:

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

end;

suppose i <> len h ; :: thesis:

then i < len h by A22, XXREAL_0:1;
then A23: i <= len g by A14, INT_1:7;
then i in Seg (len g) by A21, FINSEQ_1:1;
then A24: i in dom g by FINSEQ_1:def 3;
thus h . i = s . (intpos (p0 + i)) by A15, A20, A21, A22, SCPISORT:def 1
.= g . i by A3, A20, A21, A23, SCPISORT:def 1
.= (g ^ <*q*>) . i by A24, FINSEQ_1:def 7 ; :: thesis:

end;

end;

end;

len (g ^ <*q*>) = len h by A14, FINSEQ_2:16;
then A25: g ^ <*q*> = h by A19, FINSEQ_1:14;
h . (len h) = s . (intpos (p0 + (len h))) by A15, A17, SCPISORT:def 1
.= t . (intpos ((p0 + 1) + (len g))) by A13, A14, A18 ;
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 A6, A7, Lm1, T
.= Sum h by A5, A25, RVSUM_1:74 ;
:: thesis:

end;

hereby :: thesis:

let i be Element of NAT ; :: thesis:
assume A28: 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))),Q,t)) . (intpos i) = t . (intpos i) by A6, A7, Lm1, T
.= s . (intpos i) by A13, A28 ;
:: 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 A2, Th8, I; :: thesis: