let s be State of SCMPDS ; :: thesis: for I being halt-free shiftable Program of SCMPDS
for a being Int_position
for i being Integer
for n being Element of NAT st s . (DataLoc (s . a),i) > 0 & n > 0 & card I > 0 & a <> DataLoc (s . a),i & ( for t being State of SCMPDS st t . a = s . a holds
( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) = t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t ) ) holds
( for-down a,i,n,I is_closed_on s & for-down a,i,n,I is_halting_on s )
let I be halt-free shiftable Program of SCMPDS ; :: thesis: for a being Int_position
for i being Integer
for n being Element of NAT st s . (DataLoc (s . a),i) > 0 & n > 0 & card I > 0 & a <> DataLoc (s . a),i & ( for t being State of SCMPDS st t . a = s . a holds
( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) = t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t ) ) holds
( for-down a,i,n,I is_closed_on s & for-down a,i,n,I is_halting_on s )
let a be Int_position ; :: thesis: for i being Integer
for n being Element of NAT st s . (DataLoc (s . a),i) > 0 & n > 0 & card I > 0 & a <> DataLoc (s . a),i & ( for t being State of SCMPDS st t . a = s . a holds
( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) = t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t ) ) holds
( for-down a,i,n,I is_closed_on s & for-down a,i,n,I is_halting_on s )
let i be Integer; :: thesis: for n being Element of NAT st s . (DataLoc (s . a),i) > 0 & n > 0 & card I > 0 & a <> DataLoc (s . a),i & ( for t being State of SCMPDS st t . a = s . a holds
( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) = t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t ) ) holds
( for-down a,i,n,I is_closed_on s & for-down a,i,n,I is_halting_on s )
let n be Element of NAT ; :: thesis: ( s . (DataLoc (s . a),i) > 0 & n > 0 & card I > 0 & a <> DataLoc (s . a),i & ( for t being State of SCMPDS st t . a = s . a holds
( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) = t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t ) ) implies ( for-down a,i,n,I is_closed_on s & for-down a,i,n,I is_halting_on s ) )
assume that
A1: ( s . (DataLoc (s . a),i) > 0 & n > 0 & card I > 0 & a <> DataLoc (s . a),i ) and
A2: for t being State of SCMPDS st t . a = s . a holds
( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) = t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t ) ; :: thesis: ( for-down a,i,n,I is_closed_on s & for-down a,i,n,I is_halting_on s )
for t being State of SCMPDS st ( for x being Int_position st x in {} holds
t . x = s . x ) & t . a = s . a holds
( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) = t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t & ( for y being Int_position st y in {} holds
(IExec I,t) . y = t . y ) ) by A2;
hence ( for-down a,i,n,I is_closed_on s & for-down a,i,n,I is_halting_on s ) by A1, SCMPDS_7:67; :: thesis: verum