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