let s be 0 -started 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 0 -started 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