let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for s being State of SCMPDS
for I being halt-free shiftable Program of SCMPDS
for a being Int_position
for i, c being Integer
for X 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
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st ( for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc ((s . a),i))) ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) ) ) holds
( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(IExec (I,P,s))) ) )
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 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
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st ( for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc ((s . a),i))) ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) ) ) holds
( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(IExec (I,P,s))) ) )
let I be halt-free shiftable Program of SCMPDS; :: thesis: for a being Int_position
for i, c being Integer
for X 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
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st ( for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc ((s . a),i))) ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) ) ) holds
( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(IExec (I,P,s))) ) )
let a be Int_position ; :: thesis: for i, c being Integer
for X 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
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st ( for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc ((s . a),i))) ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) ) ) holds
( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(IExec (I,P,s))) ) )
let i, c be Integer; :: thesis: for X 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
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st ( for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc ((s . a),i))) ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) ) ) holds
( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(IExec (I,P,s))) ) )
let X 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
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st ( for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc ((s . a),i))) ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) ) ) implies ( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(IExec (I,P,s))) ) ) )
set b = DataLoc ((s . a),i);
assume 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 ex Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st
( ( for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc ((s . a),i))) ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 & not ( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) ) ) or ( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(IExec (I,P,s))) ) ) )
assume A2: 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 ex Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st
( ( for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc ((s . a),i))) ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 & not ( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) ) ) or ( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(IExec (I,P,s))) ) ) )
assume A3: for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st ( for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc ((s . a),i))) ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) ) ; :: thesis: ( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(IExec (I,P,s))) ) )
then for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT 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 {} holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in {} holds
(IExec (I,Q,t)) . x = t . x ) ) ;
hence ( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P ) by A2, Th27; :: thesis: ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(IExec (I,P,s))) )
assume A4: s . (DataLoc ((s . a),i)) > 0 ; :: thesis: IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(IExec (I,P,s)))
for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT 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 {} holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in {} holds
(IExec (I,Q,t)) . x = t . x ) ) by A3;
hence IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(IExec (I,P,s))) by A2, A4, Th27; :: thesis: verum