let P be Instruction-Sequence of SCMPDS; 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; 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 ; 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; 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; ( 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)))
; ( 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 )
; ( 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 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;
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;
( ( 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
;
( (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;
( ( 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 for x being Int_position st x in {y1} holds
(IExec (I,Q,t)) . x = t . x
let x be
Int_position;
( x in {x1} implies (IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) )assume A9:
x in {x1}
;
(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;
verum
end; let x be
Int_position;
( x in {y1} implies (IExec (I,Q,t)) . x = t . x )assume A10:
x in {y1}
;
(IExec (I,Q,t)) . x = t . xhence (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
;
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; verum