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
A2: f is_FinSequence_on s,p0 and
A3: len f = n and
A4: s . b = 0 and
A5: s . a = 0 and
A6: s . (intpos i) = - n and
A7: s . c = p0 + 1 ; :: thesis:
consider ff being Function of (product the Object-Kind of SCMPDS),NAT such that
A8: 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 Th7;
deffunc H₁( State of SCMPDS) -> Element of NAT = ff . $1;
assume A9: 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:
A10: 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 A11: H₁(t) = 0 ; :: thesis:
assume A12: t . (DataLoc ((s . a),i)) < 0 ; :: thesis:
then t . (DataLoc ((s . a),i)) < 0 ;
then H₁(t) = - (t . (DataLoc ((s . a),i))) by A8;
hence contradiction by A11, A12; :: thesis:

end;

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

end;

A13: now

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

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 A23, SCMPDS_5:15;
then A30: H₁( Initialize (IExec (I,Q,t))) = 0 by A8;
H₁(t) <> 0 by A10, A14, A16;
hence H₁( Initialize (IExec (I,Q,t))) < H₁(t) by A30, NAT_1:3; :: thesis:

end;

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

t . (DataLoc ((s . a),i)) < 0 by A16;
then A32: H₁(t) = - (t . (DataLoc ((s . a),i))) by A8
.= - (t . (intpos i)) by A23 ;
(Initialize (IExec (I,Q,t))) . (DataLoc ((s . a),i)) < 0 by A23, A31, SCMPDS_5:15;
then H₁( Initialize (IExec (I,Q,t))) = - ((Initialize (IExec (I,Q,t))) . (DataLoc ((s . a),i))) by A8
.= - ((t . (intpos i)) + 1) by A23, A29, SCMPDS_5:15
.= (- (t . (intpos i))) - 1 ;
hence H₁( Initialize (IExec (I,Q,t))) < H₁(t) by A32, XREAL_1:146; :: thesis:

end;

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

proof

hereby :: thesis:

let i be Element of NAT ; :: thesis:
assume A33: 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 A5, A9, A15, A16, A21, A17, A24, A20, A23, A33 ; :: thesis:

end;

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

end;

A34: 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
A35: len h = 0 and
A36: h is_FinSequence_on s,p0 by SCPISORT:2;
take h ; :: thesis:
thus h is_FinSequence_on s,p0 by A36; :: thesis:
thus len h = (s . (intpos i)) + n by A6, A35
.= (s . (intpos i)) + n ; :: thesis:
h = <*> REAL by A35;
hence s . b = Sum h by A4, RVSUM_1:72; :: thesis:
thus s . (intpos i) <= 0 by A6; :: thesis:
thus s . c = (p0 + 1) + (len h) by A7, A35; :: thesis:

end;

A37: ( 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(A10, A34, A13);
then consider g being FinSequence of INT such that
A38: g is_FinSequence_on s,p0 and
A39: len g = ((Initialize (IExec ((while<0 (a,i,I)),P,s))) . (intpos i)) + n and
A40: (Initialize (IExec ((while<0 (a,i,I)),P,s))) . b = Sum g and
A41: (Initialize (IExec ((while<0 (a,i,I)),P,s))) . (intpos i) <= 0 ;
XX: (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 A5, 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 A10, A37, XX;
then A42: (Initialize (IExec ((while<0 (a,i,I)),P,s))) . (intpos i) = 0 by A41, XXREAL_0:1;

now

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

end;

then f = g by A3, A39, A42, FINSEQ_2:9;
hence (IExec ((while<0 (a,i,I)),P,s)) . b = Sum f by A40, SCMPDS_5:15; :: thesis:
A44: for t being 0 -started State of SCMPDS st S₁[t] & H₁(t) = 0 holds
t . (DataLoc ((s . a),i)) >= 0 by A10;
( 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(A44, A34, A13);
hence ( while<0 (a,i,I) is_closed_on s,P & while<0 (a,i,I) is_halting_on s,P ) ; :: thesis: