let s be 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:
assume A1: card I > 0 ; :: thesis:
set Iw = IExec (while<0 a,i,I),s;
set Dw = Dstate (IExec (while<0 a,i,I),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 State 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,t) . a = 0 & I is_closed_on t & I is_halting_on t & (IExec I,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,t) . c = (p0 + 1) + (len g) & (IExec I,t) . b = Sum g ) & ( for i being Element of NAT st i > p0 holds
(IExec I,t) . (intpos i) = s . (intpos i) ) ) ; :: thesis:

A10: now

let t be State of SCMPDS ; :: thesis:
set dt = Dstate t;
assume S₁[ Dstate t] ; :: thesis:

hereby :: thesis:

assume A11: H₁( Dstate t) = 0 ; :: thesis:
assume A12: t . (DataLoc (s . a),i) < 0 ; :: thesis:
then (Dstate t) . (DataLoc (s . a),i) < 0 by SCMPDS_8:4;
then H₁( Dstate t) = - ((Dstate t) . (DataLoc (s . a),i)) by A8;
hence contradiction by A11, A12, SCMPDS_8:4; :: thesis:

end;

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

end;

A13: now

let t be State of SCMPDS ; :: thesis:
set Dt = Dstate t;
assume that
A14: S₁[ Dstate 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 = ((Dstate t) . (intpos i)) + n & (Dstate t) . b = Sum h ) and
A19: (Dstate t) . c = (p0 + 1) + (len h) by A14;
A20: t . c = (p0 + 1) + (len h) by A19, SCMPDS_8:4;
set It = IExec I,t;
set Dit = Dstate (IExec I,t);

A21: now

let i be Element of NAT ; :: thesis:
assume A22: i > p0 ; :: thesis:
thus t . (intpos i) = (Dstate t) . (intpos i) by SCMPDS_8:4
.= s . (intpos i) by A14, A22 ; :: thesis:

end;

A23: intpos (0 + i) = DataLoc (s . a),i by A5, SCMP_GCD:5;
A24: ( len h = (t . (intpos i)) + n & t . b = Sum h ) by A18, SCMPDS_8:4;
hence (IExec I,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,t) . c = (p0 + 1) + (len g) and
A28: (IExec I,t) . b = Sum g by A5, A9, A15, A16, A21, A17, A24, A20, A23;
thus ( I is_closed_on t & I is_halting_on t ) by A5, A9, A15, A16, A21, A17, A24, A20, A23; :: thesis:
A29: (IExec I,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,t) . (intpos i) < 0 ) ;

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

then (Dstate (IExec I,t)) . (DataLoc (s . a),i) >= 0 by A23, SCMPDS_8:4;
then A30: H₁( Dstate (IExec I,t)) = 0 by A8;
H₁( Dstate t) <> 0 by A10, A14, A16;
hence H₁( Dstate (IExec I,t)) < H₁( Dstate t) by A30, NAT_1:3; :: thesis:

end;

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

(Dstate t) . (DataLoc (s . a),i) < 0 by A16, SCMPDS_8:4;
then A32: H₁( Dstate t) = - ((Dstate t) . (DataLoc (s . a),i)) by A8
.= - (t . (intpos i)) by A23, SCMPDS_8:4 ;
(Dstate (IExec I,t)) . (DataLoc (s . a),i) < 0 by A23, A31, SCMPDS_8:4;
then H₁( Dstate (IExec I,t)) = - ((Dstate (IExec I,t)) . (DataLoc (s . a),i)) by A8
.= - ((t . (intpos i)) + 1) by A23, A29, SCMPDS_8:4
.= (- (t . (intpos i))) - 1 ;
hence H₁( Dstate (IExec I,t)) < H₁( Dstate t) by A32, XREAL_1:148; :: thesis:

end;

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

proof

hereby :: thesis:

let i be Element of NAT ; :: thesis:
assume A33: i > p0 ; :: thesis:
thus (Dstate (IExec I,t)) . (intpos i) = (IExec I,t) . (intpos i) by SCMPDS_8:4
.= 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,t) . (intpos i)) + n by A29, A26
.= ((Dstate (IExec I,t)) . (intpos i)) + n by SCMPDS_8:4 ; :: thesis:
thus (Dstate (IExec I,t)) . b = Sum g by A28, SCMPDS_8:4; :: thesis:
(Dstate (IExec I,t)) . (intpos i) = (t . (intpos i)) + 1 by A29, SCMPDS_8:4;
hence (Dstate (IExec I,t)) . (intpos i) <= 0 by A16, A23, INT_1:20; :: thesis:
thus (Dstate (IExec I,t)) . c = (p0 + 1) + (len g) by A27, SCMPDS_8:4; :: thesis:

end;

A34: S₁[ Dstate s]

proof

set Ds = Dstate s;
thus for i being Element of NAT st i > p0 holds
(Dstate s) . (intpos i) = s . (intpos i) by SCMPDS_8:4; :: thesis:
consider h being FinSequence of INT such that
A35: len h = 0 and
A36: h is_FinSequence_on s,p0 by SCPISORT:3;
take h ; :: thesis:
thus h is_FinSequence_on s,p0 by A36; :: thesis:
thus len h = (s . (intpos i)) + n by A6, A35
.= ((Dstate s) . (intpos i)) + n by SCMPDS_8:4 ; :: thesis:
h = <*> REAL by A35;
hence (Dstate s) . b = Sum h by A4, RVSUM_1:102, SCMPDS_8:4; :: thesis:
thus (Dstate s) . (intpos i) <= 0 by A6, SCMPDS_8:4; :: thesis:
thus (Dstate s) . c = (p0 + 1) + (len h) by A7, A35, SCMPDS_8:4; :: thesis:

end;

now

let i be Nat; :: thesis:
reconsider a = i as Element of NAT by ORDINAL1:def 13;
assume i in dom f ; :: thesis:
then A43: ( 1 <= i & i <= n ) by A3, FINSEQ_3:27;
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:10;
hence (IExec (while<0 a,i,I),s) . b = Sum f by A40, SCMPDS_8:4; :: thesis:
A44: for t being State of SCMPDS st S₁[ Dstate t] & H₁( Dstate t) = 0 holds
t . (DataLoc (s . a),i) >= 0 by A10;
( ( H₁(s) = H₁(s) or S₁[s] ) & while<0 a,i,I is_closed_on s & while<0 a,i,I is_halting_on s ) from SCMPDS_8:sch 1(A1, A44, A34, A13);
hence ( while<0 a,i,I is_closed_on s & while<0 a,i,I is_halting_on s ) ; :: thesis: