let s be State of SCMPDS ; :: thesis: for I being halt-free shiftable Program of SCMPDS
for a, b, c being Int_position
for i, d being Integer st card I > 0 & s . a = d & s . b > 0 & s . c > 0 & s . (DataLoc d,i) = (s . b) - (s . c) & ( for t being State of SCMPDS st t . b > 0 & t . c > 0 & t . a = d & t . (DataLoc d,i) = (t . b) - (t . c) & t . b <> t . c holds
( (IExec I,t) . a = d & I is_closed_on t & I is_halting_on t & ( t . b > t . c implies ( (IExec I,t) . b = (t . b) - (t . c) & (IExec I,t) . c = t . c ) ) & ( t . b <= t . c implies ( (IExec I,t) . c = (t . c) - (t . b) & (IExec I,t) . b = t . b ) ) & (IExec I,t) . (DataLoc d,i) = ((IExec I,t) . b) - ((IExec I,t) . c) ) ) holds
( while<>0 a,i,I is_closed_on s & while<>0 a,i,I is_halting_on s & ( s . (DataLoc (s . a),i) <> 0 implies IExec (while<>0 a,i,I),s = IExec (while<>0 a,i,I),(IExec I,s) ) )
let I be halt-free shiftable Program of SCMPDS ; :: thesis: for a, b, c being Int_position
for i, d being Integer st card I > 0 & s . a = d & s . b > 0 & s . c > 0 & s . (DataLoc d,i) = (s . b) - (s . c) & ( for t being State of SCMPDS st t . b > 0 & t . c > 0 & t . a = d & t . (DataLoc d,i) = (t . b) - (t . c) & t . b <> t . c holds
( (IExec I,t) . a = d & I is_closed_on t & I is_halting_on t & ( t . b > t . c implies ( (IExec I,t) . b = (t . b) - (t . c) & (IExec I,t) . c = t . c ) ) & ( t . b <= t . c implies ( (IExec I,t) . c = (t . c) - (t . b) & (IExec I,t) . b = t . b ) ) & (IExec I,t) . (DataLoc d,i) = ((IExec I,t) . b) - ((IExec I,t) . c) ) ) holds
( while<>0 a,i,I is_closed_on s & while<>0 a,i,I is_halting_on s & ( s . (DataLoc (s . a),i) <> 0 implies IExec (while<>0 a,i,I),s = IExec (while<>0 a,i,I),(IExec I,s) ) )
let a, b, c be Int_position ; :: thesis: for i, d being Integer st card I > 0 & s . a = d & s . b > 0 & s . c > 0 & s . (DataLoc d,i) = (s . b) - (s . c) & ( for t being State of SCMPDS st t . b > 0 & t . c > 0 & t . a = d & t . (DataLoc d,i) = (t . b) - (t . c) & t . b <> t . c holds
( (IExec I,t) . a = d & I is_closed_on t & I is_halting_on t & ( t . b > t . c implies ( (IExec I,t) . b = (t . b) - (t . c) & (IExec I,t) . c = t . c ) ) & ( t . b <= t . c implies ( (IExec I,t) . c = (t . c) - (t . b) & (IExec I,t) . b = t . b ) ) & (IExec I,t) . (DataLoc d,i) = ((IExec I,t) . b) - ((IExec I,t) . c) ) ) holds
( while<>0 a,i,I is_closed_on s & while<>0 a,i,I is_halting_on s & ( s . (DataLoc (s . a),i) <> 0 implies IExec (while<>0 a,i,I),s = IExec (while<>0 a,i,I),(IExec I,s) ) )
let i, d be Integer; :: thesis: ( card I > 0 & s . a = d & s . b > 0 & s . c > 0 & s . (DataLoc d,i) = (s . b) - (s . c) & ( for t being State of SCMPDS st t . b > 0 & t . c > 0 & t . a = d & t . (DataLoc d,i) = (t . b) - (t . c) & t . b <> t . c holds
( (IExec I,t) . a = d & I is_closed_on t & I is_halting_on t & ( t . b > t . c implies ( (IExec I,t) . b = (t . b) - (t . c) & (IExec I,t) . c = t . c ) ) & ( t . b <= t . c implies ( (IExec I,t) . c = (t . c) - (t . b) & (IExec I,t) . b = t . b ) ) & (IExec I,t) . (DataLoc d,i) = ((IExec I,t) . b) - ((IExec I,t) . c) ) ) implies ( while<>0 a,i,I is_closed_on s & while<>0 a,i,I is_halting_on s & ( s . (DataLoc (s . a),i) <> 0 implies IExec (while<>0 a,i,I),s = IExec (while<>0 a,i,I),(IExec I,s) ) ) )
set ci = DataLoc (s . a),i;
assume A1: card I > 0 ; :: thesis: ( not s . a = d or not s . b > 0 or not s . c > 0 or not s . (DataLoc d,i) = (s . b) - (s . c) or ex t being State of SCMPDS st
( t . b > 0 & t . c > 0 & t . a = d & t . (DataLoc d,i) = (t . b) - (t . c) & t . b <> t . c & not ( (IExec I,t) . a = d & I is_closed_on t & I is_halting_on t & ( t . b > t . c implies ( (IExec I,t) . b = (t . b) - (t . c) & (IExec I,t) . c = t . c ) ) & ( t . b <= t . c implies ( (IExec I,t) . c = (t . c) - (t . b) & (IExec I,t) . b = t . b ) ) & (IExec I,t) . (DataLoc d,i) = ((IExec I,t) . b) - ((IExec I,t) . c) ) ) or ( while<>0 a,i,I is_closed_on s & while<>0 a,i,I is_halting_on s & ( s . (DataLoc (s . a),i) <> 0 implies IExec (while<>0 a,i,I),s = IExec (while<>0 a,i,I),(IExec I,s) ) ) )
consider f being Function of (product the Object-Kind of SCMPDS ),NAT such that
A2: for s being State of SCMPDS holds
( ( s . b = s . c implies f . s = 0 ) & ( s . b <> s . c implies f . s = max (abs (s . b)),(abs (s . c)) ) ) by Th6;
deffunc H₁( State of SCMPDS ) -> Element of NAT = f . $1;
defpred S₁[ set ] means ex t being State of SCMPDS st
( t = $1 & t . b > 0 & t . c > 0 & t . (DataLoc d,i) = (t . b) - (t . c) );
assume that
A3: s . a = d and
A4: s . b > 0 and
A5: s . c > 0 and
A6: s . (DataLoc d,i) = (s . b) - (s . c) ; :: thesis: ( ex t being State of SCMPDS st
( t . b > 0 & t . c > 0 & t . a = d & t . (DataLoc d,i) = (t . b) - (t . c) & t . b <> t . c & not ( (IExec I,t) . a = d & I is_closed_on t & I is_halting_on t & ( t . b > t . c implies ( (IExec I,t) . b = (t . b) - (t . c) & (IExec I,t) . c = t . c ) ) & ( t . b <= t . c implies ( (IExec I,t) . c = (t . c) - (t . b) & (IExec I,t) . b = t . b ) ) & (IExec I,t) . (DataLoc d,i) = ((IExec I,t) . b) - ((IExec I,t) . c) ) ) or ( while<>0 a,i,I is_closed_on s & while<>0 a,i,I is_halting_on s & ( s . (DataLoc (s . a),i) <> 0 implies IExec (while<>0 a,i,I),s = IExec (while<>0 a,i,I),(IExec I,s) ) ) )
assume A7: for t being State of SCMPDS st t . b > 0 & t . c > 0 & t . a = d & t . (DataLoc d,i) = (t . b) - (t . c) & t . b <> t . c holds
( (IExec I,t) . a = d & I is_closed_on t & I is_halting_on t & ( t . b > t . c implies ( (IExec I,t) . b = (t . b) - (t . c) & (IExec I,t) . c = t . c ) ) & ( t . b <= t . c implies ( (IExec I,t) . c = (t . c) - (t . b) & (IExec I,t) . b = t . b ) ) & (IExec I,t) . (DataLoc d,i) = ((IExec I,t) . b) - ((IExec I,t) . c) ) ; :: thesis: ( while<>0 a,i,I is_closed_on s & while<>0 a,i,I is_halting_on s & ( s . (DataLoc (s . a),i) <> 0 implies IExec (while<>0 a,i,I),s = IExec (while<>0 a,i,I),(IExec I,s) ) )

A8: now

let t be State of SCMPDS ; :: thesis: ( S₁[ Dstate t] & t . a = s . a & t . (DataLoc (s . a),i) <> 0 implies ( (IExec I,t) . a = t . a & I is_closed_on t & I is_halting_on t & H₁( Dstate (IExec I,t)) < H₁( Dstate t) & S₁[ Dstate (IExec I,t)] ) )
assume that
A9: S₁[ Dstate t] and
A10: t . a = s . a and
A11: t . (DataLoc (s . a),i) <> 0 ; :: thesis: ( (IExec I,t) . a = t . a & I is_closed_on t & I is_halting_on t & H₁( Dstate (IExec I,t)) < H₁( Dstate t) & S₁[ Dstate (IExec I,t)] )
set It = IExec I,t;
set t2 = Dstate (IExec I,t);
set t1 = Dstate t;
set x = (IExec I,t) . b;
set y = (IExec I,t) . c;
consider v being State of SCMPDS such that
A12: v = Dstate t and
A13: v . b > 0 and
A14: v . c > 0 and
A15: v . (DataLoc d,i) = (v . b) - (v . c) by A9;
A16: t . b > 0 by A12, A13, SCMPDS_8:4;
A17: t . c > 0 by A12, A14, SCMPDS_8:4;
A18: t . (DataLoc d,i) = (v . b) - (v . c) by A12, A15, SCMPDS_8:4
.= (t . b) - (v . c) by A12, SCMPDS_8:4
.= (t . b) - (t . c) by A12, SCMPDS_8:4 ;
then A19: t . b <> t . c by A3, A11;
hence (IExec I,t) . a = t . a by A3, A7, A10, A16, A17, A18; :: thesis: ( I is_closed_on t & I is_halting_on t & H₁( Dstate (IExec I,t)) < H₁( Dstate t) & S₁[ Dstate (IExec I,t)] )
thus ( I is_closed_on t & I is_halting_on t ) by A3, A7, A10, A16, A17, A18, A19; :: thesis: ( H₁( Dstate (IExec I,t)) < H₁( Dstate t) & S₁[ Dstate (IExec I,t)] )

A20: now

per cases ( t . b > t . c or t . b <= t . c ) ;

suppose A21: t . b > t . c ; :: thesis: ( (IExec I,t) . b > 0 & (IExec I,t) . c > 0 & max ((IExec I,t) . b),((IExec I,t) . c) < max (t . b),(t . c) )

then (t . b) - (t . c) > 0 by XREAL_1:52;
hence (IExec I,t) . b > 0 by A3, A7, A10, A16, A17, A18, A21; :: thesis: ( (IExec I,t) . c > 0 & max ((IExec I,t) . b),((IExec I,t) . c) < max (t . b),(t . c) )
thus (IExec I,t) . c > 0 by A3, A7, A10, A16, A17, A18, A21; :: thesis: max ((IExec I,t) . b),((IExec I,t) . c) < max (t . b),(t . c)
A22: (IExec I,t) . b = (t . b) - (t . c) by A3, A7, A10, A16, A17, A18, A21;

hereby :: thesis: verum

A23: max (t . b),(t . c) = t . b by A21, XXREAL_0:def 10;

per cases ( max ((IExec I,t) . b),((IExec I,t) . c) = (IExec I,t) . b or max ((IExec I,t) . b),((IExec I,t) . c) = (IExec I,t) . c ) by XXREAL_0:16;

suppose max ((IExec I,t) . b),((IExec I,t) . c) = (IExec I,t) . b ; :: thesis: max ((IExec I,t) . b),((IExec I,t) . c) < max (t . b),(t . c)

hence max ((IExec I,t) . b),((IExec I,t) . c) < max (t . b),(t . c) by A17, A22, A23, XREAL_1:46; :: thesis: verum

end;

suppose max ((IExec I,t) . b),((IExec I,t) . c) = (IExec I,t) . c ; :: thesis: max ((IExec I,t) . b),((IExec I,t) . c) < max (t . b),(t . c)

hence max ((IExec I,t) . b),((IExec I,t) . c) < max (t . b),(t . c) by A3, A7, A10, A16, A17, A18, A21, A23; :: thesis: verum

end;

end;

end;

end;

suppose A24: t . b <= t . c ; :: thesis: ( (IExec I,t) . b > 0 & (IExec I,t) . c > 0 & max ((IExec I,t) . b),((IExec I,t) . c) < max (t . b),(t . c) )

hence (IExec I,t) . b > 0 by A3, A7, A10, A16, A17, A18, A19; :: thesis: ( (IExec I,t) . c > 0 & max ((IExec I,t) . b),((IExec I,t) . c) < max (t . b),(t . c) )
t . b < t . c by A19, A24, XXREAL_0:1;
then (t . c) - (t . b) > 0 by XREAL_1:52;
hence (IExec I,t) . c > 0 by A3, A7, A10, A16, A17, A18, A19, A24; :: thesis: max ((IExec I,t) . b),((IExec I,t) . c) < max (t . b),(t . c)
A25: (IExec I,t) . c = (t . c) - (t . b) by A3, A7, A10, A16, A17, A18, A19, A24;
A26: (IExec I,t) . b = t . b by A3, A7, A10, A16, A17, A18, A19, A24;

hereby :: thesis: verum

A27: max (t . b),(t . c) = t . c by A24, XXREAL_0:def 10;

per cases ( max ((IExec I,t) . b),((IExec I,t) . c) = (IExec I,t) . c or max ((IExec I,t) . b),((IExec I,t) . c) = (IExec I,t) . b ) by XXREAL_0:16;

suppose max ((IExec I,t) . b),((IExec I,t) . c) = (IExec I,t) . c ; :: thesis: max ((IExec I,t) . b),((IExec I,t) . c) < max (t . b),(t . c)

hence max ((IExec I,t) . b),((IExec I,t) . c) < max (t . b),(t . c) by A16, A25, A27, XREAL_1:46; :: thesis: verum

end;

suppose max ((IExec I,t) . b),((IExec I,t) . c) = (IExec I,t) . b ; :: thesis: max ((IExec I,t) . b),((IExec I,t) . c) < max (t . b),(t . c)

hence max ((IExec I,t) . b),((IExec I,t) . c) < max (t . b),(t . c) by A19, A24, A26, A27, XXREAL_0:1; :: thesis: verum

end;

end;

end;

end;

end;

end;

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

proof

(Dstate t) . b <> t . c by A19, SCMPDS_8:4;
then (Dstate t) . b <> (Dstate t) . c by SCMPDS_8:4;
then A28: H₁( Dstate t) = max (abs ((Dstate t) . b)),(abs ((Dstate t) . c)) by A2
.= max (abs (t . b)),(abs ((Dstate t) . c)) by SCMPDS_8:4
.= max (abs (t . b)),(abs (t . c)) by SCMPDS_8:4
.= max (t . b),(abs (t . c)) by A16, ABSVALUE:def 1
.= max (t . b),(t . c) by A17, ABSVALUE:def 1 ;
then H₁( Dstate t) >= t . b by XXREAL_0:25;
then A29: H₁( Dstate t) > 0 by A16, XXREAL_0:2;

per cases ( (Dstate (IExec I,t)) . b = (Dstate (IExec I,t)) . c or (Dstate (IExec I,t)) . b <> (Dstate (IExec I,t)) . c ) ;

suppose (Dstate (IExec I,t)) . b = (Dstate (IExec I,t)) . c ; :: thesis: H₁( Dstate (IExec I,t)) < H₁( Dstate t)

hence H₁( Dstate (IExec I,t)) < H₁( Dstate t) by A2, A29; :: thesis: verum

end;

suppose (Dstate (IExec I,t)) . b <> (Dstate (IExec I,t)) . c ; :: thesis: H₁( Dstate (IExec I,t)) < H₁( Dstate t)

then H₁( Dstate (IExec I,t)) = max (abs ((Dstate (IExec I,t)) . b)),(abs ((Dstate (IExec I,t)) . c)) by A2
.= max (abs ((IExec I,t) . b)),(abs ((Dstate (IExec I,t)) . c)) by SCMPDS_8:4
.= max (abs ((IExec I,t) . b)),(abs ((IExec I,t) . c)) by SCMPDS_8:4
.= max ((IExec I,t) . b),(abs ((IExec I,t) . c)) by A20, ABSVALUE:def 1
.= max ((IExec I,t) . b),((IExec I,t) . c) by A20, ABSVALUE:def 1 ;
hence H₁( Dstate (IExec I,t)) < H₁( Dstate t) by A20, A28; :: thesis: verum

end;

end;

end;

A30: (IExec I,t) . (DataLoc d,i) = ((IExec I,t) . b) - ((IExec I,t) . c) by A3, A7, A10, A16, A17, A18, A19;
thus S₁[ Dstate (IExec I,t)] :: thesis: verum

proof

take v = Dstate (IExec I,t); :: thesis: ( v = Dstate (IExec I,t) & v . b > 0 & v . c > 0 & v . (DataLoc d,i) = (v . b) - (v . c) )
thus v = Dstate (IExec I,t) ; :: thesis: ( v . b > 0 & v . c > 0 & v . (DataLoc d,i) = (v . b) - (v . c) )
thus ( v . b > 0 & v . c > 0 ) by A20, SCMPDS_8:4; :: thesis: v . (DataLoc d,i) = (v . b) - (v . c)
thus v . (DataLoc d,i) = ((IExec I,t) . b) - ((IExec I,t) . c) by A30, SCMPDS_8:4
.= (v . b) - ((IExec I,t) . c) by SCMPDS_8:4
.= (v . b) - (v . c) by SCMPDS_8:4 ; :: thesis: verum

end;

end;

A31: for t being State of SCMPDS st S₁[ Dstate t] & H₁( Dstate t) = 0 holds
t . (DataLoc (s . a),i) = 0

proof

let t be State of SCMPDS ; :: thesis: ( S₁[ Dstate t] & H₁( Dstate t) = 0 implies t . (DataLoc (s . a),i) = 0 )
assume that
A32: S₁[ Dstate t] and
A33: H₁( Dstate t) = 0 ; :: thesis: t . (DataLoc (s . a),i) = 0
consider v being State of SCMPDS such that
A34: v = Dstate t and
A35: v . b > 0 and
v . c > 0 and
A36: v . (DataLoc d,i) = (v . b) - (v . c) by A32;

A37: now

assume t . b <> t . c ; :: thesis: contradiction
then (Dstate t) . b <> t . c by SCMPDS_8:4;
then (Dstate t) . b <> (Dstate t) . c by SCMPDS_8:4;
then A38: H₁( Dstate t) = max (abs ((Dstate t) . b)),(abs ((Dstate t) . c)) by A2
.= max (abs (t . b)),(abs ((Dstate t) . c)) by SCMPDS_8:4
.= max (abs (t . b)),(abs (t . c)) by SCMPDS_8:4 ;
t . b > 0 by A34, A35, SCMPDS_8:4;
then abs (t . b) > 0 by COMPLEX1:133;
hence contradiction by A33, A38, XXREAL_0:25; :: thesis: verum

end;

thus t . (DataLoc (s . a),i) = (v . b) - (v . c) by A3, A34, A36, SCMPDS_8:4
.= (t . b) - (v . c) by A34, SCMPDS_8:4
.= (t . b) - (t . c) by A34, SCMPDS_8:4
.= 0 by A37 ; :: thesis: verum

end;

A39: S₁[ Dstate s]

proof

take t = Dstate s; :: thesis: ( t = Dstate s & t . b > 0 & t . c > 0 & t . (DataLoc d,i) = (t . b) - (t . c) )
thus t = Dstate s ; :: thesis: ( t . b > 0 & t . c > 0 & t . (DataLoc d,i) = (t . b) - (t . c) )
thus t . b > 0 by A4, SCMPDS_8:4; :: thesis: ( t . c > 0 & t . (DataLoc d,i) = (t . b) - (t . c) )
thus t . c > 0 by A5, SCMPDS_8:4; :: thesis: t . (DataLoc d,i) = (t . b) - (t . c)
thus t . (DataLoc d,i) = (s . b) - (s . c) by A6, SCMPDS_8:4
.= (t . b) - (s . c) by SCMPDS_8:4
.= (t . b) - (t . c) by SCMPDS_8:4 ; :: thesis: verum

end;

( while<>0 a,i,I is_closed_on s & while<>0 a,i,I is_halting_on s ) from SCPINVAR:sch 3(A1, A31, A39, A8);
hence ( while<>0 a,i,I is_closed_on s & while<>0 a,i,I is_halting_on s ) ; :: thesis: ( s . (DataLoc (s . a),i) <> 0 implies IExec (while<>0 a,i,I),s = IExec (while<>0 a,i,I),(IExec I,s) )
assume A40: s . (DataLoc (s . a),i) <> 0 ; :: thesis: IExec (while<>0 a,i,I),s = IExec (while<>0 a,i,I),(IExec I,s)
IExec (while<>0 a,i,I),s = IExec (while<>0 a,i,I),(IExec I,s) from SCPINVAR:sch 4(A1, A40, A31, A39, A8);
hence IExec (while<>0 a,i,I),s = IExec (while<>0 a,i,I),(IExec I,s) ; :: thesis: verum