let s be State of SCMPDS; :: thesis: for I being halt-free shiftable Program of SCMPDS
for a being Int_position
for i, c being Integer
for X, Y being set st card I > 0 & ( for x being Int_position st x in X holds
s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being State of SCMPDS st ( for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,t)) . a = t . a & I is_closed_on t & I is_halting_on t & (IExec (I,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for x being Int_position st x in X holds
(IExec (I,t)) . x >= c + ((IExec (I,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds
(IExec (I,t)) . x = t . x ) ) ) 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 being Int_position
for i, c being Integer
for X, Y being set st card I > 0 & ( for x being Int_position st x in X holds
s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being State of SCMPDS st ( for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,t)) . a = t . a & I is_closed_on t & I is_halting_on t & (IExec (I,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for x being Int_position st x in X holds
(IExec (I,t)) . x >= c + ((IExec (I,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds
(IExec (I,t)) . x = t . x ) ) ) 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 be Int_position ; :: thesis: for i, c being Integer
for X, Y being set st card I > 0 & ( for x being Int_position st x in X holds
s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being State of SCMPDS st ( for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,t)) . a = t . a & I is_closed_on t & I is_halting_on t & (IExec (I,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for x being Int_position st x in X holds
(IExec (I,t)) . x >= c + ((IExec (I,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds
(IExec (I,t)) . x = t . x ) ) ) 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, c be Integer; :: thesis: for X, Y being set st card I > 0 & ( for x being Int_position st x in X holds
s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being State of SCMPDS st ( for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,t)) . a = t . a & I is_closed_on t & I is_halting_on t & (IExec (I,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for x being Int_position st x in X holds
(IExec (I,t)) . x >= c + ((IExec (I,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds
(IExec (I,t)) . x = t . x ) ) ) 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 X, Y be set ; :: thesis: ( card I > 0 & ( for x being Int_position st x in X holds
s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being State of SCMPDS st ( for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,t)) . a = t . a & I is_closed_on t & I is_halting_on t & (IExec (I,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for x being Int_position st x in X holds
(IExec (I,t)) . x >= c + ((IExec (I,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds
(IExec (I,t)) . x = t . x ) ) ) 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 b = DataLoc ((s . a),i);
assume A1: card I > 0 ; :: thesis: ( ex x being Int_position st
( x in X & not s . x >= c + (s . (DataLoc ((s . a),i))) ) or ex t being State of SCMPDS st
( ( for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 & not ( (IExec (I,t)) . a = t . a & I is_closed_on t & I is_halting_on t & (IExec (I,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for x being Int_position st x in X holds
(IExec (I,t)) . x >= c + ((IExec (I,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds
(IExec (I,t)) . x = t . x ) ) ) 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))) ) ) )
defpred S₁[ State of SCMPDS] means ( ( for x being Int_position st x in X holds
$1 . x >= c + ($1 . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds
$1 . x = s . x ) );
consider f being Function of (product the Object-Kind of SCMPDS),NAT such that
A2: for s being State of SCMPDS holds
( ( s . (DataLoc ((s . a),i)) <= 0 implies f . s = 0 ) & ( s . (DataLoc ((s . a),i)) > 0 implies f . s = s . (DataLoc ((s . a),i)) ) ) by Th5;
deffunc H₁( State of SCMPDS) -> Element of NAT = f . $1;
A3: for t being State of SCMPDS holds
( H₁( Dstate t) = 0 iff t . (DataLoc ((s . a),i)) <= 0 )

proof

let t be State of SCMPDS; :: thesis: ( H₁( Dstate t) = 0 iff t . (DataLoc ((s . a),i)) <= 0 )
thus ( H₁( Dstate t) = 0 implies t . (DataLoc ((s . a),i)) <= 0 ) :: thesis: ( t . (DataLoc ((s . a),i)) <= 0 implies H₁( Dstate t) = 0 )

proof

assume A4: H₁( Dstate t) = 0 ; :: thesis: t . (DataLoc ((s . a),i)) <= 0
assume t . (DataLoc ((s . a),i)) > 0 ; :: thesis: contradiction
then (Dstate t) . (DataLoc ((s . a),i)) > 0 by Th4;
hence contradiction by A2, A4; :: thesis: verum

end;

assume t . (DataLoc ((s . a),i)) <= 0 ; :: thesis: H₁( Dstate t) = 0
then (Dstate t) . (DataLoc ((s . a),i)) <= 0 by Th4;
hence H₁( Dstate t) = 0 by A2; :: thesis: verum

end;

then A5: for t being State of SCMPDS st S₁[ Dstate t] & H₁( Dstate t) = 0 holds
t . (DataLoc ((s . a),i)) <= 0 ;
assume A6: for x being Int_position st x in X holds
s . x >= c + (s . (DataLoc ((s . a),i))) ; :: thesis: ( ex t being State of SCMPDS st
( ( for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 & not ( (IExec (I,t)) . a = t . a & I is_closed_on t & I is_halting_on t & (IExec (I,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for x being Int_position st x in X holds
(IExec (I,t)) . x >= c + ((IExec (I,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds
(IExec (I,t)) . x = t . x ) ) ) 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))) ) ) )
A7: S₁[ Dstate s]

proof

set t = Dstate s;

hereby :: thesis: for x being Int_position st x in Y holds
(Dstate s) . x = s . x

let x be Int_position ; :: thesis: ( x in X implies (Dstate s) . x >= c + ((Dstate s) . (DataLoc ((s . a),i))) )
assume x in X ; :: thesis: (Dstate s) . x >= c + ((Dstate s) . (DataLoc ((s . a),i)))
then s . x >= c + (s . (DataLoc ((s . a),i))) by A6;
then (Dstate s) . x >= c + (s . (DataLoc ((s . a),i))) by Th4;
hence (Dstate s) . x >= c + ((Dstate s) . (DataLoc ((s . a),i))) by Th4; :: thesis: verum

end;

thus for x being Int_position st x in Y holds
(Dstate s) . x = s . x by Th4; :: thesis: verum

end;

assume A8: for t being State of SCMPDS st ( for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,t)) . a = t . a & I is_closed_on t & I is_halting_on t & (IExec (I,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for x being Int_position st x in X holds
(IExec (I,t)) . x >= c + ((IExec (I,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds
(IExec (I,t)) . x = t . x ) ) ; :: 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))) ) )

A9: 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
A10: S₁[ Dstate t] and
A11: t . a = s . a and
A12: 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;
consider v being State of SCMPDS such that
A13: v = Dstate t and
A14: for x being Int_position st x in X holds
v . x >= c + (v . (DataLoc ((s . a),i))) and
A15: for x being Int_position st x in Y holds
v . x = s . x by A10;

A16: now

let x be Int_position ; :: thesis: ( x in Y implies t . x = s . x )
assume x in Y ; :: thesis: t . x = s . x
then v . x = s . x by A15;
hence t . x = s . x by A13, Th4; :: thesis: verum

end;

A17: now

let x be Int_position ; :: thesis: ( x in X implies t . x >= c + (t . (DataLoc ((s . a),i))) )
assume x in X ; :: thesis: t . x >= c + (t . (DataLoc ((s . a),i)))
then v . x >= c + (v . (DataLoc ((s . a),i))) by A14;
then t . x >= c + (v . (DataLoc ((s . a),i))) by A13, Th4;
hence t . x >= c + (t . (DataLoc ((s . a),i))) by A13, Th4; :: thesis: verum

end;

hence ( (IExec (I,t)) . a = t . a & I is_closed_on t & I is_halting_on t ) by A8, A11, A12, A16; :: thesis: ( H₁( Dstate (IExec (I,t))) < H₁( Dstate t) & S₁[ Dstate (IExec (I,t))] )
thus H₁( Dstate (IExec (I,t))) < H₁( Dstate t) :: thesis: S₁[ Dstate (IExec (I,t))]

proof

(Dstate t) . (DataLoc ((s . a),i)) > 0 by A12, Th4;
then A18: H₁( Dstate t) = (Dstate t) . (DataLoc ((s . a),i)) by A2
.= t . (DataLoc ((s . a),i)) by Th4 ;
assume A19: H₁( Dstate (IExec (I,t))) >= H₁( Dstate t) ; :: thesis: contradiction
then (IExec (I,t)) . (DataLoc ((s . a),i)) > 0 by A3, A12, A18;
then (Dstate (IExec (I,t))) . (DataLoc ((s . a),i)) > 0 by Th4;
then H₁( Dstate (IExec (I,t))) = (Dstate (IExec (I,t))) . (DataLoc ((s . a),i)) by A2
.= (IExec (I,t)) . (DataLoc ((s . a),i)) by Th4 ;
hence contradiction by A8, A11, A12, A17, A16, A19, A18; :: thesis: verum

end;

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

proof

set v = Dstate (IExec (I,t));

hereby :: thesis: for x being Int_position st x in Y holds
(Dstate (IExec (I,t))) . x = s . x

let x be Int_position ; :: thesis: ( x in X implies (Dstate (IExec (I,t))) . x >= c + ((Dstate (IExec (I,t))) . (DataLoc ((s . a),i))) )
assume x in X ; :: thesis: (Dstate (IExec (I,t))) . x >= c + ((Dstate (IExec (I,t))) . (DataLoc ((s . a),i)))
then (IExec (I,t)) . x >= c + ((IExec (I,t)) . (DataLoc ((s . a),i))) by A8, A11, A12, A17, A16;
then (Dstate (IExec (I,t))) . x >= c + ((IExec (I,t)) . (DataLoc ((s . a),i))) by Th4;
hence (Dstate (IExec (I,t))) . x >= c + ((Dstate (IExec (I,t))) . (DataLoc ((s . a),i))) by Th4; :: thesis: verum

end;

hereby :: thesis: verum

let x be Int_position ; :: thesis: ( x in Y implies (Dstate (IExec (I,t))) . x = s . x )
assume A20: x in Y ; :: thesis: (Dstate (IExec (I,t))) . x = s . x
then (IExec (I,t)) . x = t . x by A8, A11, A12, A17, A16;
then (Dstate (IExec (I,t))) . x = t . x by Th4;
hence (Dstate (IExec (I,t))) . x = s . x by A16, A20; :: thesis: verum

end;

end;

end;

( ( 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 3(A1, A5, A7, A9);
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 A21: s . (DataLoc ((s . a),i)) > 0 ; :: thesis: IExec ((while>0 (a,i,I)),s) = IExec ((while>0 (a,i,I)),(IExec (I,s)))
( ( H₁(s) = H₁(s) or S₁[s] ) & IExec ((while>0 (a,i,I)),s) = IExec ((while>0 (a,i,I)),(IExec (I,s))) ) from SCMPDS_8:sch 4(A1, A21, A5, A7, A9);
hence IExec ((while>0 (a,i,I)),s) = IExec ((while>0 (a,i,I)),(IExec (I,s))) ; :: thesis: verum