let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for I being halt-free shiftable Program of
for a, x, y being Int_position
for i, c being Integer st s . x >= c + (s . (DataLoc ((s . a),i))) & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence 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,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)) & (IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) & (IExec (I,Q,t)) . y = t . y ) ) 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,(Initialize (IExec (I,P,s)))) ) )
let s be 0 -started State of SCMPDS; :: thesis: for I being halt-free shiftable Program of
for a, x, y being Int_position
for i, c being Integer st s . x >= c + (s . (DataLoc ((s . a),i))) & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence 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,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)) & (IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) & (IExec (I,Q,t)) . y = t . y ) ) 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,(Initialize (IExec (I,P,s)))) ) )
let I be halt-free shiftable Program of ; :: thesis: for a, x, y being Int_position
for i, c being Integer st s . x >= c + (s . (DataLoc ((s . a),i))) & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence 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,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)) & (IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) & (IExec (I,Q,t)) . y = t . y ) ) 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,(Initialize (IExec (I,P,s)))) ) )
let a, x1, y1 be Int_position; :: thesis: for i, c being Integer st s . x1 >= c + (s . (DataLoc ((s . a),i))) & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence 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,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)) & (IExec (I,Q,t)) . x1 >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) & (IExec (I,Q,t)) . y1 = t . y1 ) ) 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,(Initialize (IExec (I,P,s)))) ) )
let i, c be Integer; :: thesis: ( s . x1 >= c + (s . (DataLoc ((s . a),i))) & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence 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,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)) & (IExec (I,Q,t)) . x1 >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) & (IExec (I,Q,t)) . y1 = t . y1 ) ) 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,(Initialize (IExec (I,P,s)))) ) ) )
set b = DataLoc ((s . a),i);
assume s . x1 >= c + (s . (DataLoc ((s . a),i))) ; :: thesis: ( ex t being 0 -started State of SCMPDS ex Q being Instruction-Sequence 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,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)) & (IExec (I,Q,t)) . x1 >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) & (IExec (I,Q,t)) . y1 = t . y1 ) ) 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,(Initialize (IExec (I,P,s)))) ) ) )
then A1: for x being Int_position st x in {x1} holds
s . x >= c + (s . (DataLoc ((s . a),i))) by TARSKI:def 1;
assume A2: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence 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,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)) & (IExec (I,Q,t)) . x1 >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) & (IExec (I,Q,t)) . y1 = t . y1 ) ; :: 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,(Initialize (IExec (I,P,s)))) ) )

now :: thesis: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st ( 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 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 {x1} holds
(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in {y1} holds
(IExec (I,Q,t)) . x = t . x ) )

let t be 0 -started State of SCMPDS; :: thesis: for Q being Instruction-Sequence of SCMPDS st ( 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 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 {x1} holds
(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in {y1} holds
(IExec (I,Q,t)) . x = t . x ) )
let Q be Instruction-Sequence 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,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 {x1} holds
(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in {y1} holds
(IExec (I,Q,t)) . x = t . x ) ) )
assume that
A3: for x being Int_position st x in {x1} holds
t . x >= c + (t . (DataLoc ((s . a),i))) and
A4: for x being Int_position st x in {y1} holds
t . x = s . x and
A5: t . a = s . a and
A6: t . (DataLoc ((s . a),i)) > 0 ; :: thesis: ( (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 {x1} holds
(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in {y1} holds
(IExec (I,Q,t)) . x = t . x ) )
y1 in {y1} by TARSKI:def 1;
then A7: t . y1 = s . y1 by A4;
x1 in {x1} by TARSKI:def 1;
then A8: t . x1 >= c + (t . (DataLoc ((s . a),i))) by A3;
hence ( (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)) ) by A2, A5, A6, A7; :: thesis: ( ( for x being Int_position st x in {x1} holds
(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in {y1} holds
(IExec (I,Q,t)) . x = t . x ) )

hereby :: thesis: for x being Int_position st x in {y1} holds
(IExec (I,Q,t)) . x = t . x

let x be Int_position; :: thesis: ( x in {x1} implies (IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) )
assume A9: x in {x1} ; :: thesis: (IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i)))
(IExec (I,Q,t)) . x1 >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) by A2, A5, A6, A8, A7;
hence (IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) by A9, TARSKI:def 1; :: thesis: verum

end;

let x be Int_position; :: thesis: ( x in {y1} implies (IExec (I,Q,t)) . x = t . x )
assume A10: x in {y1} ; :: thesis: (IExec (I,Q,t)) . x = t . x
hence (IExec (I,Q,t)) . x = (IExec (I,Q,t)) . y1 by TARSKI:def 1
.= t . y1 by A2, A5, A6, A8, A7
.= t . x by A10, TARSKI:def 1 ;
:: thesis: verum

end;

hence ( 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,(Initialize (IExec (I,P,s)))) ) ) by A1, SCMPDS_8:27; :: thesis: verum