let P be Instruction-Sequence of SCMPDS; :: thesis:
let s be 0 -started State of SCMPDS; :: thesis:
let I be halt-free shiftable Program of SCMPDS; :: thesis:
let a, b, c be Int_position; :: thesis:
let n, i, p0 be Element of NAT ; :: thesis:
let f be FinSequence of INT ; :: thesis:
set Iw = IExec ((while<0 (a,i,I)),P,s);
set Dw = Initialize (IExec ((while<0 (a,i,I)),P,s));
set da = DataLoc ((s . a),i);
defpred S₁[ State of SCMPDS] means ( ( for i being Element of NAT st i > p0 holds
$1 . (intpos i) = s . (intpos i) ) & ex g being FinSequence of INT st
( g is_FinSequence_on s,p0 & len g = ($1 . (intpos i)) + n & $1 . b = Sum g & $1 . (intpos i) <= 0 & $1 . c = (p0 + 1) + (len g) ) );
assume that
A1: f is_FinSequence_on s,p0 and
A2: len f = n and
A3: s . b = 0 and
A4: s . a = 0 and
A5: s . (intpos i) = - n and
A6: s . c = p0 + 1 ; :: thesis:
consider ff being Function of (product (the_Values_of SCMPDS)),NAT such that
A7: for t being State of SCMPDS holds
( ( t . (DataLoc ((s . a),i)) >= 0 implies ff . t = 0 ) & ( t . (DataLoc ((s . a),i)) < 0 implies ff . t = - (t . (DataLoc ((s . a),i))) ) ) by Th3;
deffunc H₁( State of SCMPDS) -> Element of NAT = ff . $1;
assume A8: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st ex g being FinSequence of INT st
( g is_FinSequence_on s,p0 & len g = (t . (intpos i)) + n & t . b = Sum g & t . c = (p0 + 1) + (len g) ) & t . a = 0 & t . (intpos i) < 0 & ( for i being Element of NAT st i > p0 holds
t . (intpos i) = s . (intpos i) ) holds
( (IExec (I,Q,t)) . a = 0 & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (intpos i) = (t . (intpos i)) + 1 & ex g being FinSequence of INT st
( g is_FinSequence_on s,p0 & len g = ((t . (intpos i)) + n) + 1 & (IExec (I,Q,t)) . c = (p0 + 1) + (len g) & (IExec (I,Q,t)) . b = Sum g ) & ( for i being Element of NAT st i > p0 holds
(IExec (I,Q,t)) . (intpos i) = s . (intpos i) ) ) ; :: thesis:
A9: for t being 0 -started State of SCMPDS st S₁[t] holds
( ( H₁(t) = 0 implies not t . (DataLoc ((s . a),i)) < 0 ) & ( t . (DataLoc ((s . a),i)) >= 0 implies H₁(t) = 0 ) )

proof

let t be 0 -started State of SCMPDS; :: thesis:
assume S₁[t] ; :: thesis:

hereby :: thesis:

assume A10: H₁(t) = 0 ; :: thesis:
assume A11: t . (DataLoc ((s . a),i)) < 0 ; :: thesis:
then t . (DataLoc ((s . a),i)) < 0 ;
then H₁(t) = - (t . (DataLoc ((s . a),i))) by A7;
hence contradiction by A10, A11; :: thesis:

end;

assume t . (DataLoc ((s . a),i)) >= 0 ; :: thesis:
then t . (DataLoc ((s . a),i)) >= 0 ;
hence H₁(t) = 0 by A7; :: thesis:

end;

A12: now :: thesis:

let t be 0 -started State of SCMPDS; :: thesis:
let Q be Instruction-Sequence of SCMPDS; :: thesis:
assume that
A13: S₁[t] and
A14: t . a = s . a and
A15: t . (DataLoc ((s . a),i)) < 0 ; :: thesis:
consider h being FinSequence of INT such that
A16: h is_FinSequence_on s,p0 and
A17: ( len h = (t . (intpos i)) + n & t . b = Sum h ) and
A18: t . c = (p0 + 1) + (len h) by A13;
A19: t . c = (p0 + 1) + (len h) by A18;
set It = IExec (I,Q,t);
set Dit = Initialize (IExec (I,Q,t));
A20: for i being Element of NAT st i > p0 holds
t . (intpos i) = s . (intpos i) by A13;
A21: intpos (0 + i) = DataLoc ((s . a),i) by A4, SCMP_GCD:1;
A22: ( len h = (t . (intpos i)) + n & t . b = Sum h ) by A17;
hence (IExec (I,Q,t)) . a = t . a by A4, A8, A14, A15, A20, A16, A19, A21; :: thesis:
consider g being FinSequence of INT such that
A23: g is_FinSequence_on s,p0 and
A24: len g = ((t . (intpos i)) + n) + 1 and
A25: (IExec (I,Q,t)) . c = (p0 + 1) + (len g) and
A26: (IExec (I,Q,t)) . b = Sum g by A4, A8, A14, A15, A20, A16, A22, A19, A21;
thus ( I is_closed_on t,Q & I is_halting_on t,Q ) by A4, A8, A14, A15, A20, A16, A22, A19, A21; :: thesis:
A27: (IExec (I,Q,t)) . (intpos i) = (t . (intpos i)) + 1 by A4, A8, A14, A15, A20, A16, A22, A19, A21;

hereby :: thesis:

per cases ) . (intpos i) >= 0 or (IExec (I,Q,t)) . (intpos i) < 0 ) ;

suppose (IExec (I,Q,t)) . (intpos i) >= 0 ; :: thesis:

then (Initialize (IExec (I,Q,t))) . (DataLoc ((s . a),i)) >= 0 by A21, SCMPDS_5:15;
then A28: H₁( Initialize (IExec (I,Q,t))) = 0 by A7;
H₁(t) <> 0 by A9, A13, A15;
hence H₁( Initialize (IExec (I,Q,t))) < H₁(t) by A28; :: thesis:

end;

suppose A29: (IExec (I,Q,t)) . (intpos i) < 0 ; :: thesis:

t . (DataLoc ((s . a),i)) < 0 by A15;
then A30: H₁(t) = - (t . (DataLoc ((s . a),i))) by A7
.= - (t . (intpos i)) by A21 ;
(Initialize (IExec (I,Q,t))) . (DataLoc ((s . a),i)) < 0 by A21, A29, SCMPDS_5:15;
then H₁( Initialize (IExec (I,Q,t))) = - ((Initialize (IExec (I,Q,t))) . (DataLoc ((s . a),i))) by A7
.= - ((t . (intpos i)) + 1) by A21, A27, SCMPDS_5:15
.= (- (t . (intpos i))) - 1 ;
hence H₁( Initialize (IExec (I,Q,t))) < H₁(t) by A30, XREAL_1:146; :: thesis:

end;

thus S₁[ Initialize (IExec (I,Q,t))] :: thesis:

proof

hereby :: thesis:

let i be Element of NAT ; :: thesis:
assume A31: i > p0 ; :: thesis:
thus (Initialize (IExec (I,Q,t))) . (intpos i) = (IExec (I,Q,t)) . (intpos i) by SCMPDS_5:15
.= s . (intpos i) by A4, A8, A14, A15, A20, A16, A22, A19, A21, A31 ; :: thesis:

end;

take g ; :: thesis:
thus g is_FinSequence_on s,p0 by A23; :: thesis:
thus len g = ((IExec (I,Q,t)) . (intpos i)) + n by A27, A24
.= ((Initialize (IExec (I,Q,t))) . (intpos i)) + n by SCMPDS_5:15 ; :: thesis:
thus (Initialize (IExec (I,Q,t))) . b = Sum g by A26, SCMPDS_5:15; :: thesis:
(Initialize (IExec (I,Q,t))) . (intpos i) = (t . (intpos i)) + 1 by A27, SCMPDS_5:15;
hence (Initialize (IExec (I,Q,t))) . (intpos i) <= 0 by A15, A21, INT_1:7; :: thesis:
thus (Initialize (IExec (I,Q,t))) . c = (p0 + 1) + (len g) by A25, SCMPDS_5:15; :: thesis:

end;

A32: S₁[s]

proof

thus for i being Element of NAT st i > p0 holds
s . (intpos i) = s . (intpos i) ; :: thesis:
consider h being FinSequence of INT such that
A33: len h = 0 and
A34: h is_FinSequence_on s,p0 by SCPISORT:2;
take h ; :: thesis:
thus h is_FinSequence_on s,p0 by A34; :: thesis:
thus len h = (s . (intpos i)) + n by A5, A33
.= (s . (intpos i)) + n ; :: thesis:
h = <*> REAL by A33;
hence s . b = Sum h by A3, RVSUM_1:72; :: thesis:
thus s . (intpos i) <= 0 by A5; :: thesis:
thus s . c = (p0 + 1) + (len h) by A6, A33; :: thesis:

end;

A35: ( H₁( Initialize (IExec ((while<0 (a,i,I)),P,s))) = 0 & S₁[ Initialize (IExec ((while<0 (a,i,I)),P,s))] ) from SCPINVAR:sch 1(A9, A32, A12);
then consider g being FinSequence of INT such that
A36: g is_FinSequence_on s,p0 and
A37: len g = ((Initialize (IExec ((while<0 (a,i,I)),P,s))) . (intpos i)) + n and
A38: (Initialize (IExec ((while<0 (a,i,I)),P,s))) . b = Sum g and
A39: (Initialize (IExec ((while<0 (a,i,I)),P,s))) . (intpos i) <= 0 ;
A40: (Initialize (IExec ((while<0 (a,i,I)),P,s))) . (intpos i) = (IExec ((while<0 (a,i,I)),P,s)) . (intpos (0 + i)) by SCMPDS_5:15
.= (IExec ((while<0 (a,i,I)),P,s)) . (DataLoc ((s . a),i)) by A4, SCMP_GCD:1 ;
(IExec ((while<0 (a,i,I)),P,s)) . (DataLoc ((s . a),i)) = (Initialize (IExec ((while<0 (a,i,I)),P,s))) . (DataLoc ((s . a),i)) by SCMPDS_5:15;
then (Initialize (IExec ((while<0 (a,i,I)),P,s))) . (intpos i) >= 0 by A9, A35, A40;
then A41: (Initialize (IExec ((while<0 (a,i,I)),P,s))) . (intpos i) = 0 by A39;

now :: thesis:

let i be Nat; :: thesis:
reconsider a = i as Element of NAT by ORDINAL1:def 12;
assume i in dom f ; :: thesis:
then A42: ( 1 <= i & i <= n ) by A2, FINSEQ_3:25;
hence f . i = s . (intpos (p0 + a)) by A1, A2
.= g . i by A36, A37, A41, A42 ;
:: thesis:

end;

then f = g by A2, A37, A41, FINSEQ_2:9;
hence (IExec ((while<0 (a,i,I)),P,s)) . b = Sum f by A38, SCMPDS_5:15; :: thesis:
A43: for t being 0 -started State of SCMPDS st S₁[t] & H₁(t) = 0 holds
t . (DataLoc ((s . a),i)) >= 0 by A9;
( while<0 (a,i,I) is_closed_on s,P & while<0 (a,i,I) is_halting_on s,P ) from SCMPDS_8:sch 1(A43, A32, A12);
hence ( while<0 (a,i,I) is_closed_on s,P & while<0 (a,i,I) is_halting_on s,P ) ; :: thesis: