let s be State of SCMPDS ; :: thesis: for I being halt-free shiftable Program of SCMPDS
for a, x, y being Int_position
for i, c being Integer st card I > 0 & s . x >= c & ( for t being State of SCMPDS st t . x >= c & t . y = s . y & 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) & (IExec I,t) . x >= c & (IExec I,t) . y = t . y ) ) 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, x, y being Int_position
for i, c being Integer st card I > 0 & s . x >= c & ( for t being State of SCMPDS st t . x >= c & t . y = s . y & 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) & (IExec I,t) . x >= c & (IExec I,t) . y = t . y ) ) 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, x, y be Int_position ; :: thesis: for i, c being Integer st card I > 0 & s . x >= c & ( for t being State of SCMPDS st t . x >= c & t . y = s . y & 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) & (IExec I,t) . x >= c & (IExec I,t) . y = t . y ) ) 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: ( card I > 0 & s . x >= c & ( for t being State of SCMPDS st t . x >= c & t . y = s . y & 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) & (IExec I,t) . x >= c & (IExec I,t) . y = t . y ) ) 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: ( not s . x >= c or ex t being State of SCMPDS st
( t . x >= c & t . y = s . y & 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) & (IExec I,t) . x >= c & (IExec I,t) . y = t . y ) ) 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₁[ set ] means ex t being State of SCMPDS st
( t = $1 & t . x >= c & t . y = s . y );
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 SCMPDS_8:5;
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 SCMPDS_8:4;
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 SCMPDS_8:4;
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: s . x >= c ; :: thesis: ( ex t being State of SCMPDS st
( t . x >= c & t . y = s . y & 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) & (IExec I,t) . x >= c & (IExec I,t) . y = t . y ) ) 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

take t = Dstate s; :: thesis: ( t = Dstate s & t . x >= c & t . y = s . y )
thus t = Dstate s ; :: thesis: ( t . x >= c & t . y = s . y )
thus t . x >= c by A6, SCMPDS_8:4; :: thesis: t . y = s . y
thus t . y = s . y by SCMPDS_8:4; :: thesis: verum

end;

assume A8: for t being State of SCMPDS st t . x >= c & t . y = s . y & 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) & (IExec I,t) . x >= c & (IExec I,t) . y = t . y ) ; :: 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;
A13: t . y = s . y by A10, SCMPDS_8:4;
A14: t . x >= c by A10, SCMPDS_8:4;
hence ( (IExec I,t) . a = t . a & I is_closed_on t & I is_halting_on t ) by A8, A11, A12, A13; :: 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, SCMPDS_8:4;
then A15: H₁( Dstate t) = (Dstate t) . (DataLoc (s . a),i) by A2
.= t . (DataLoc (s . a),i) by SCMPDS_8:4 ;
assume A16: H₁( Dstate (IExec I,t)) >= H₁( Dstate t) ; :: thesis: contradiction
then (IExec I,t) . (DataLoc (s . a),i) > 0 by A3, A12, A15;
then (Dstate (IExec I,t)) . (DataLoc (s . a),i) > 0 by SCMPDS_8:4;
then H₁( Dstate (IExec I,t)) = (Dstate (IExec I,t)) . (DataLoc (s . a),i) by A2
.= (IExec I,t) . (DataLoc (s . a),i) by SCMPDS_8:4 ;
hence contradiction by A8, A11, A12, A14, A13, A16, A15; :: thesis: verum

end;

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

proof

take v = Dstate (IExec I,t); :: thesis: ( v = Dstate (IExec I,t) & v . x >= c & v . y = s . y )
thus v = Dstate (IExec I,t) ; :: thesis: ( v . x >= c & v . y = s . y )
(IExec I,t) . x >= c by A8, A11, A12, A14, A13;
hence v . x >= c by SCMPDS_8:4; :: thesis: v . y = s . y
(IExec I,t) . y = t . y by A8, A11, A12, A14, A13;
hence v . y = s . y by A13, SCMPDS_8:4; :: thesis: verum

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 A17: 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, A17, A5, A7, A9);
hence IExec (while>0 a,i,I),s = IExec (while>0 a,i,I),(IExec I,s) ; :: thesis: verum