let s be State of SCMPDS ; :: thesis: for I being shiftable No-StopCode 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 & ( 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
( 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 shiftable No-StopCode 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 & ( 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
( 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 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 & ( 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
( 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 Integer; :: thesis: for X being set
for f being Function of (product the Object-Kind of SCMPDS ),NAT st card 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
( 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 X be set ; :: thesis: for f being Function of (product the Object-Kind of SCMPDS ),NAT st card 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
( 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 f be Function of (product the Object-Kind of SCMPDS ),NAT ; :: thesis: ( card 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 ( 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: ( 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 ( 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 A2: 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 ( 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 A3: 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: ( 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) ) )
A4: for x being Int_position st x in {} holds
s . x >= 0 + (s . (DataLoc (s . a),i)) ;
for t being State of SCMPDS st ( for x being Int_position st x in {} holds
t . x >= 0 + (t . (DataLoc (s . a),i)) ) & ( 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 {} holds
(IExec I,t) . x >= 0 + ((IExec I,t) . (DataLoc (s . a),i)) ) & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) ) by A3;
hence ( while>0 a,i,I is_closed_on s & while>0 a,i,I is_halting_on s ) by A1, A2, A4, Th24; :: 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 A5: s . (DataLoc (s . a),i) > 0 ; :: thesis: IExec (while>0 a,i,I),s = IExec (while>0 a,i,I),(IExec I,s)
for t being State of SCMPDS st ( for x being Int_position st x in {} holds
t . x >= 0 + (t . (DataLoc (s . a),i)) ) & ( 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 {} holds
(IExec I,t) . x >= 0 + ((IExec I,t) . (DataLoc (s . a),i)) ) & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) ) by A3;
hence IExec (while>0 a,i,I),s = IExec (while>0 a,i,I),(IExec I,s) by A1, A2, A4, A5, Th25; :: thesis: verum