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 + (s . (DataLoc (s . a),i)) & ( for t being State of SCMPDS st t . x >= c + (t . (DataLoc (s . a),i)) & 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) . (DataLoc (s . a),i)) & (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 + (s . (DataLoc (s . a),i)) & ( for t being State of SCMPDS st t . x >= c + (t . (DataLoc (s . a),i)) & 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) . (DataLoc (s . a),i)) & (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, x1, y1 be Int_position ; :: thesis: for i, c being Integer st card I > 0 & s . x1 >= c + (s . (DataLoc (s . a),i)) & ( for t being State of SCMPDS st t . x1 >= c + (t . (DataLoc (s . a),i)) & t . y1 = s . y1 & 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) . x1 >= c + ((IExec I,t) . (DataLoc (s . a),i)) & (IExec I,t) . y1 = t . y1 ) ) 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 . x1 >= c + (s . (DataLoc (s . a),i)) & ( for t being State of SCMPDS st t . x1 >= c + (t . (DataLoc (s . a),i)) & t . y1 = s . y1 & 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) . x1 >= c + ((IExec I,t) . (DataLoc (s . a),i)) & (IExec I,t) . y1 = t . y1 ) ) 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 . x1 >= c + (s . (DataLoc (s . a),i)) or ex t being State of SCMPDS st
( t . x1 >= c + (t . (DataLoc (s . a),i)) & t . y1 = s . y1 & 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) . x1 >= c + ((IExec I,t) . (DataLoc (s . a),i)) & (IExec I,t) . y1 = t . y1 ) ) 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 s . x1 >= c + (s . (DataLoc (s . a),i)) ; :: thesis: ( ex t being State of SCMPDS st
( t . x1 >= c + (t . (DataLoc (s . a),i)) & t . y1 = s . y1 & 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) . x1 >= c + ((IExec I,t) . (DataLoc (s . a),i)) & (IExec I,t) . y1 = t . y1 ) ) 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) ) ) )
then A2: for x being Int_position st x in {x1} holds
s . x >= c + (s . (DataLoc (s . a),i)) by TARSKI:def 1;
assume A3: for t being State of SCMPDS st t . x1 >= c + (t . (DataLoc (s . a),i)) & t . y1 = s . y1 & 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) . x1 >= c + ((IExec I,t) . (DataLoc (s . a),i)) & (IExec I,t) . y1 = t . y1 ) ; :: 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) ) )

now

let t be State of SCMPDS ; :: thesis: ( ( for x being Int_position st x in {x1} holds
t . x >= c + (t . (DataLoc (s . a),i)) ) & ( for x being Int_position st x in {y1} holds
t . x = s . x ) & 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 & (IExec I,t) . (DataLoc (s . a),i) < t . (DataLoc (s . a),i) & ( for x being Int_position st x in {x1} holds
(IExec I,t) . x >= c + ((IExec I,t) . (DataLoc (s . a),i)) ) & ( for x being Int_position st x in {y1} holds
(IExec I,t) . x = t . x ) ) )
assume that
A4: for x being Int_position st x in {x1} holds
t . x >= c + (t . (DataLoc (s . a),i)) and
A5: for x being Int_position st x in {y1} holds
t . x = s . x and
A6: t . a = s . a and
A7: t . (DataLoc (s . a),i) > 0 ; :: thesis: ( (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 {x1} holds
(IExec I,t) . x >= c + ((IExec I,t) . (DataLoc (s . a),i)) ) & ( for x being Int_position st x in {y1} holds
(IExec I,t) . x = t . x ) )
y1 in {y1} by TARSKI:def 1;
then A8: t . y1 = s . y1 by A5;
x1 in {x1} by TARSKI:def 1;
then A9: t . x1 >= c + (t . (DataLoc (s . a),i)) by A4;
hence ( (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) ) by A3, A6, A7, A8; :: thesis: ( ( for x being Int_position st x in {x1} holds
(IExec I,t) . x >= c + ((IExec I,t) . (DataLoc (s . a),i)) ) & ( for x being Int_position st x in {y1} holds
(IExec I,t) . x = t . x ) )

hereby :: thesis: for x being Int_position st x in {y1} holds
(IExec I,t) . x = t . x

let x be Int_position ; :: thesis: ( x in {x1} implies (IExec I,t) . x >= c + ((IExec I,t) . (DataLoc (s . a),i)) )
assume A10: x in {x1} ; :: thesis: (IExec I,t) . x >= c + ((IExec I,t) . (DataLoc (s . a),i))
(IExec I,t) . x1 >= c + ((IExec I,t) . (DataLoc (s . a),i)) by A3, A6, A7, A9, A8;
hence (IExec I,t) . x >= c + ((IExec I,t) . (DataLoc (s . a),i)) by A10, TARSKI:def 1; :: thesis: verum

end;

hereby :: thesis: verum

let x be Int_position ; :: thesis: ( x in {y1} implies (IExec I,t) . x = t . x )
assume A11: x in {y1} ; :: thesis: (IExec I,t) . x = t . x
hence (IExec I,t) . x = (IExec I,t) . y1 by TARSKI:def 1
.= t . y1 by A3, A6, A7, A9, A8
.= t . x by A11, TARSKI:def 1 ;
:: thesis: verum

end;

end;

hence ( 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) ) ) by A1, A2, SCMPDS_8:27; :: thesis: verum