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

A5: 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)] ) )
set v = Dstate t;
assume that
A6: S₁[ Dstate t] and
A7: ( t . a = s . a & 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;

A8: now

let x be Int_position ; :: thesis: ( x in X implies t . x = s . x )
assume x in X ; :: thesis: t . x = s . x
then (Dstate t) . x = s . x by A6;
hence t . x = s . x by Th4; :: thesis: verum

end;

hence ( (IExec I,t) . a = t . a & I is_closed_on t & I is_halting_on t & H₁( Dstate (IExec I,t)) < H₁( Dstate t) ) by A4, A7; :: thesis: S₁[ Dstate (IExec I,t)]
thus S₁[ Dstate (IExec I,t)] :: thesis: verum

proof

set v = Dstate (IExec I,t);

hereby :: thesis: verum

let x be Int_position ; :: thesis: ( x in X implies (Dstate (IExec I,t)) . x = s . x )
assume A9: x in X ; :: thesis: (Dstate (IExec I,t)) . x = s . x
then (IExec I,t) . x = t . x by A4, A7, A8;
then (Dstate (IExec I,t)) . x = t . x by Th4;
hence (Dstate (IExec I,t)) . x = s . x by A8, A9; :: thesis: verum

end;

end;

end;

A10: S₁[ Dstate s] by Th4;
( ( 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 2(A1, A2, A3, A10, A5);
hence IExec (while<0 a,i,I),s = IExec (while<0 a,i,I),(IExec I,s) ; :: thesis: verum