let P be Instruction-Sequence of SCMPDS; :: thesis: for s being State of SCMPDS

for I being halt-free shiftable Program of

for a being Int_position

for i being Integer

for n being Nat

for X being set st s . (DataLoc ((s . a),i)) < 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a holds

( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds

(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds

( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )

let s be State of SCMPDS; :: thesis: for I being halt-free shiftable Program of

for a being Int_position

for i being Integer

for n being Nat

for X being set st s . (DataLoc ((s . a),i)) < 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a holds

( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds

(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds

( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )

let I be halt-free shiftable Program of ; :: thesis: for a being Int_position

for i being Integer

for n being Nat

for X being set st s . (DataLoc ((s . a),i)) < 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a holds

( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds

(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds

( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )

let a be Int_position; :: thesis: for i being Integer

for n being Nat

for X being set st s . (DataLoc ((s . a),i)) < 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a holds

( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds

(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds

( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )

let i be Integer; :: thesis: for n being Nat

for X being set st s . (DataLoc ((s . a),i)) < 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a holds

( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds

(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds

( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )

let n be Nat; :: thesis: for X being set st s . (DataLoc ((s . a),i)) < 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a holds

( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds

(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds

( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )

let X be set ; :: thesis: ( s . (DataLoc ((s . a),i)) < 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a holds

( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds

(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) implies ( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P ) )

set b = DataLoc ((s . a),i);

set FOR = for-up (a,i,n,I);

set pFOR = stop (for-up (a,i,n,I));

set pI = stop I;

set i1 = (a,i) >=0_goto ((card I) + 3);

set i2 = AddTo (a,i,n);

set i3 = goto (- ((card I) + 2));

assume A1: s . (DataLoc ((s . a),i)) < 0 ; :: thesis: ( DataLoc ((s . a),i) in X or not n > 0 or not a <> DataLoc ((s . a),i) or ex t being State of SCMPDS ex Q being Instruction-Sequence of SCMPDS st

( ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a & not ( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds

(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) or ( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P ) )

defpred S_{1}[ Nat] means for t being State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st - (t . (DataLoc ((s . a),i))) <= $1 & ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a holds

( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q );

assume A2: not DataLoc ((s . a),i) in X ; :: thesis: ( not n > 0 or not a <> DataLoc ((s . a),i) or ex t being State of SCMPDS ex Q being Instruction-Sequence of SCMPDS st

( ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a & not ( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds

(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) or ( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P ) )

assume A3: n > 0 ; :: thesis: ( not a <> DataLoc ((s . a),i) or ex t being State of SCMPDS ex Q being Instruction-Sequence of SCMPDS st

( ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a & not ( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds

(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) or ( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P ) )

assume A4: a <> DataLoc ((s . a),i) ; :: thesis: ( ex t being State of SCMPDS ex Q being Instruction-Sequence of SCMPDS st

( ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a & not ( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds

(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) or ( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P ) )

assume A5: for t being State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a holds

( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds

(IExec (I,Q,(Initialize t))) . y = t . y ) ) ; :: thesis: ( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )

A6: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

A58: S_{1}[ 0 ]
_{1}[k]
from NAT_1:sch 2(A58, A6);

then A60: S_{1}[nn]
;

for x being Int_position st x in X holds

s . x = s . x ;

hence ( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P ) by A60; :: thesis: verum

for I being halt-free shiftable Program of

for a being Int_position

for i being Integer

for n being Nat

for X being set st s . (DataLoc ((s . a),i)) < 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a holds

( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds

(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds

( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )

let s be State of SCMPDS; :: thesis: for I being halt-free shiftable Program of

for a being Int_position

for i being Integer

for n being Nat

for X being set st s . (DataLoc ((s . a),i)) < 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a holds

( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds

(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds

( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )

let I be halt-free shiftable Program of ; :: thesis: for a being Int_position

for i being Integer

for n being Nat

for X being set st s . (DataLoc ((s . a),i)) < 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a holds

( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds

(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds

( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )

let a be Int_position; :: thesis: for i being Integer

for n being Nat

for X being set st s . (DataLoc ((s . a),i)) < 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a holds

( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds

(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds

( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )

let i be Integer; :: thesis: for n being Nat

for X being set st s . (DataLoc ((s . a),i)) < 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a holds

( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds

(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds

( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )

let n be Nat; :: thesis: for X being set st s . (DataLoc ((s . a),i)) < 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a holds

( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds

(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds

( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )

let X be set ; :: thesis: ( s . (DataLoc ((s . a),i)) < 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a holds

( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds

(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) implies ( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P ) )

set b = DataLoc ((s . a),i);

set FOR = for-up (a,i,n,I);

set pFOR = stop (for-up (a,i,n,I));

set pI = stop I;

set i1 = (a,i) >=0_goto ((card I) + 3);

set i2 = AddTo (a,i,n);

set i3 = goto (- ((card I) + 2));

assume A1: s . (DataLoc ((s . a),i)) < 0 ; :: thesis: ( DataLoc ((s . a),i) in X or not n > 0 or not a <> DataLoc ((s . a),i) or ex t being State of SCMPDS ex Q being Instruction-Sequence of SCMPDS st

( ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a & not ( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds

(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) or ( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P ) )

defpred S

for Q being Instruction-Sequence of SCMPDS st - (t . (DataLoc ((s . a),i))) <= $1 & ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a holds

( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q );

assume A2: not DataLoc ((s . a),i) in X ; :: thesis: ( not n > 0 or not a <> DataLoc ((s . a),i) or ex t being State of SCMPDS ex Q being Instruction-Sequence of SCMPDS st

( ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a & not ( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds

(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) or ( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P ) )

assume A3: n > 0 ; :: thesis: ( not a <> DataLoc ((s . a),i) or ex t being State of SCMPDS ex Q being Instruction-Sequence of SCMPDS st

( ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a & not ( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds

(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) or ( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P ) )

assume A4: a <> DataLoc ((s . a),i) ; :: thesis: ( ex t being State of SCMPDS ex Q being Instruction-Sequence of SCMPDS st

( ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a & not ( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds

(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) or ( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P ) )

assume A5: for t being State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a holds

( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds

(IExec (I,Q,(Initialize t))) . y = t . y ) ) ; :: thesis: ( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )

A6: for k being Nat st S

S

proof

reconsider nn = - (s . (DataLoc ((s . a),i))) as Element of NAT by A1, INT_1:3;
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A7: S_{1}[k]
; :: thesis: S_{1}[k + 1]

let t be State of SCMPDS; :: thesis: for Q being Instruction-Sequence of SCMPDS st - (t . (DataLoc ((s . a),i))) <= k + 1 & ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a holds

( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q )

let Q be Instruction-Sequence of SCMPDS; :: thesis: ( - (t . (DataLoc ((s . a),i))) <= k + 1 & ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a implies ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q ) )

assume A8: - (t . (DataLoc ((s . a),i))) <= k + 1 ; :: thesis: ( ex x being Int_position st

( x in X & not t . x = s . x ) or not t . a = s . a or ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q ) )

assume A9: for x being Int_position st x in X holds

t . x = s . x ; :: thesis: ( not t . a = s . a or ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q ) )

assume A10: t . a = s . a ; :: thesis: ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q )

end;assume A7: S

let t be State of SCMPDS; :: thesis: for Q being Instruction-Sequence of SCMPDS st - (t . (DataLoc ((s . a),i))) <= k + 1 & ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a holds

( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q )

let Q be Instruction-Sequence of SCMPDS; :: thesis: ( - (t . (DataLoc ((s . a),i))) <= k + 1 & ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a implies ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q ) )

assume A8: - (t . (DataLoc ((s . a),i))) <= k + 1 ; :: thesis: ( ex x being Int_position st

( x in X & not t . x = s . x ) or not t . a = s . a or ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q ) )

assume A9: for x being Int_position st x in X holds

t . x = s . x ; :: thesis: ( not t . a = s . a or ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q ) )

assume A10: t . a = s . a ; :: thesis: ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q )

per cases
( t . (DataLoc ((s . a),i)) >= 0 or t . (DataLoc ((s . a),i)) < 0 )
;

end;

suppose
t . (DataLoc ((s . a),i)) >= 0
; :: thesis: ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q )

hence
( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q )
by A10, Th33; :: thesis: verum

end;suppose A11:
t . (DataLoc ((s . a),i)) < 0
; :: thesis: ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q )

set t2 = Initialize t;

set t3 = Initialize t;

set Q2 = Q +* (stop I);

set Q3 = Q +* (stop (for-up (a,i,n,I)));

set t4 = Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1);

set Q4 = Q +* (stop (for-up (a,i,n,I)));

A12: stop I c= Q +* (stop I) by FUNCT_4:25;

A13: for-up (a,i,n,I) = ((a,i) >=0_goto ((card I) + 3)) ';' ((I ';' (AddTo (a,i,n))) ';' (goto (- ((card I) + 2)))) by Th2;

A14: Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(0 + 1)) = Following ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),0))) by EXTPRO_1:3

.= Exec (((a,i) >=0_goto ((card I) + 3)),(Initialize t)) by A13, SCMPDS_6:11 ;

for a being Int_position holds (Initialize t) . a = (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)) . a by A14, SCMPDS_2:57;

then A15: DataPart (Initialize t) = DataPart (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)) by SCMPDS_4:8;

A16: (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) by A5, A9, A10;

- (- n) > 0 by A3;

then - n < 0 ;

then - n <= - 1 by INT_1:8;

then A17: (- n) - (t . (DataLoc ((s . a),i))) <= (- 1) - (t . (DataLoc ((s . a),i))) by XREAL_1:9;

(- (t . (DataLoc ((s . a),i)))) - 1 <= k by A8, XREAL_1:20;

then A18: (- n) - (t . (DataLoc ((s . a),i))) <= k by A17, XXREAL_0:2;

A19: I is_closed_on t,Q by A5, A9, A10;

then A20: I is_closed_on Initialize t,Q +* (stop I) by SCMPDS_6:24;

A21: not DataLoc ((s . a),i) in dom (Start-At (0,SCMPDS)) by SCMPDS_4:18;

set m2 = LifeSpan ((Q +* (stop I)),(Initialize t));

set t5 = Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t))));

set Q5 = Q +* (stop (for-up (a,i,n,I)));

set l1 = (card I) + 1;

A22: IC (Initialize t) = 0 by MEMSTR_0:def 11;

set m3 = (LifeSpan ((Q +* (stop I)),(Initialize t))) + 1;

set t6 = Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1));

set Q6 = Q +* (stop (for-up (a,i,n,I)));

(card I) + 1 < (card I) + 3 by XREAL_1:6;

then A23: (card I) + 1 in dom (for-up (a,i,n,I)) by Th31;

set m5 = (((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1;

set t8 = Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1));

set Q8 = Q +* (stop (for-up (a,i,n,I)));

set t7 = Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1));

set Q7 = Q +* (stop (for-up (a,i,n,I)));

A24: (IExec (I,Q,(Initialize t))) . a = t . a by A5, A9, A10;

set l2 = (card I) + 2;

A25: 0 in dom (stop (for-up (a,i,n,I))) by COMPOS_1:36;

(card I) + 2 < (card I) + 3 by XREAL_1:6;

then A26: (card I) + 2 in dom (for-up (a,i,n,I)) by Th31;

A27: stop (for-up (a,i,n,I)) c= Q +* (stop (for-up (a,i,n,I))) by FUNCT_4:25;

for-up (a,i,n,I) c= stop (for-up (a,i,n,I)) by AFINSQ_1:74;

then A28: for-up (a,i,n,I) c= Q +* (stop (for-up (a,i,n,I))) by A27, XBOOLE_1:1;

Shift (I,1) c= for-up (a,i,n,I) by Lm3;

then A29: Shift (I,1) c= Q +* (stop (for-up (a,i,n,I))) by A28, XBOOLE_1:1;

I is_halting_on t,Q by A5, A9, A10;

then A30: Q +* (stop I) halts_on Initialize t by SCMPDS_6:def 3;

(Q +* (stop I)) +* (stop I) halts_on Initialize (Initialize t) by A30;

then A31: I is_halting_on Initialize t,Q +* (stop I) by SCMPDS_6:def 3;

not a in dom (Start-At (0,SCMPDS)) by SCMPDS_4:18;

then (Initialize t) . (DataLoc (((Initialize t) . a),i)) = (Initialize t) . (DataLoc ((s . a),i)) by A10, FUNCT_4:11

.= t . (DataLoc ((s . a),i)) by A21, FUNCT_4:11 ;

then A32: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)) = 0 + 1 by A22, A11, A14, SCMPDS_2:57;

then A33: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t))))) = (card I) + 1 by A12, A31, A20, A15, A29, Th16;

A34: (Q +* (stop (for-up (a,i,n,I)))) /. (IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1)))) = (Q +* (stop (for-up (a,i,n,I)))) . (IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1)))) by PBOOLE:143;

A35: Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1)) = Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t)))) by EXTPRO_1:4;

then A36: CurInstr ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1)))) = (Q +* (stop (for-up (a,i,n,I)))) . ((card I) + 1) by A12, A31, A20, A32, A15, A29, Th16, A34

.= (for-up (a,i,n,I)) . ((card I) + 1) by A23, A28, GRFUNC_1:2

.= AddTo (a,i,n) by Th32 ;

A37: Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1)) = Following ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1)))) by EXTPRO_1:3

.= Exec ((AddTo (a,i,n)),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1)))) by A36 ;

then A38: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) = (IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1)))) + 1 by SCMPDS_2:48

.= (card I) + (1 + 1) by A33, A35 ;

then A39: CurInstr ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1)))) = (Q +* (stop (for-up (a,i,n,I)))) . ((card I) + 2) by PBOOLE:143

.= (for-up (a,i,n,I)) . ((card I) + 2) by A28, A26, GRFUNC_1:2

.= goto (- ((card I) + 2)) by Th32 ;

A40: Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1)) = Following ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1)))) by EXTPRO_1:3

.= Exec ((goto (- ((card I) + 2))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1)))) by A39 ;

then IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) = ICplusConst ((Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))),(0 - ((card I) + 2))) by SCMPDS_2:54

.= 0 by A38, Th1 ;

then A41: Initialize (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) = Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1)) by MEMSTR_0:46;

A42: DataPart (Comput ((Q +* (stop I)),(Initialize t),(LifeSpan ((Q +* (stop I)),(Initialize t))))) = DataPart (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t))))) by A12, A31, A20, A32, A15, A29, Th16;

then A43: (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t))))) . a = (Comput ((Q +* (stop I)),(Initialize t),(LifeSpan ((Q +* (stop I)),(Initialize t))))) . a by SCMPDS_4:8

.= s . a by A10, A24, A30, EXTPRO_1:23 ;

then DataLoc (((Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1))) . a),i) = DataLoc ((s . a),i) by EXTPRO_1:4;

then (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) . a = (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1))) . a by A4, A37, SCMPDS_2:48

.= s . a by A43, EXTPRO_1:4 ;

then A44: (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) . a = s . a by A40, SCMPDS_2:54;

.= t . (DataLoc ((s . a),i)) by A16, A30, EXTPRO_1:23 ;

(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) . (DataLoc ((s . a),i)) = (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) . (DataLoc ((s . a),i)) by A40, SCMPDS_2:54

.= (t . (DataLoc ((s . a),i))) + n by A43, A47, A35, A37, SCMPDS_2:48 ;

then A48: - ((Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) . (DataLoc ((s . a),i))) = (- n) - (t . (DataLoc ((s . a),i))) ;

then A49: for-up (a,i,n,I) is_closed_on Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1)),Q +* (stop (for-up (a,i,n,I))) by A7, A44, A45, A18;

A57: (Q +* (stop (for-up (a,i,n,I)))) +* (stop (for-up (a,i,n,I))) = Q +* (stop (for-up (a,i,n,I))) ;

for-up (a,i,n,I) is_halting_on Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1)),Q +* (stop (for-up (a,i,n,I))) by A7, A44, A45, A18, A48;

then Q +* (stop (for-up (a,i,n,I))) halts_on Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1)) by A41, A57, SCMPDS_6:def 3;

then Q +* (stop (for-up (a,i,n,I))) halts_on Initialize t by EXTPRO_1:22;

hence for-up (a,i,n,I) is_halting_on t,Q by SCMPDS_6:def 3; :: thesis: verum

end;set t3 = Initialize t;

set Q2 = Q +* (stop I);

set Q3 = Q +* (stop (for-up (a,i,n,I)));

set t4 = Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1);

set Q4 = Q +* (stop (for-up (a,i,n,I)));

A12: stop I c= Q +* (stop I) by FUNCT_4:25;

A13: for-up (a,i,n,I) = ((a,i) >=0_goto ((card I) + 3)) ';' ((I ';' (AddTo (a,i,n))) ';' (goto (- ((card I) + 2)))) by Th2;

A14: Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(0 + 1)) = Following ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),0))) by EXTPRO_1:3

.= Exec (((a,i) >=0_goto ((card I) + 3)),(Initialize t)) by A13, SCMPDS_6:11 ;

for a being Int_position holds (Initialize t) . a = (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)) . a by A14, SCMPDS_2:57;

then A15: DataPart (Initialize t) = DataPart (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)) by SCMPDS_4:8;

A16: (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) by A5, A9, A10;

- (- n) > 0 by A3;

then - n < 0 ;

then - n <= - 1 by INT_1:8;

then A17: (- n) - (t . (DataLoc ((s . a),i))) <= (- 1) - (t . (DataLoc ((s . a),i))) by XREAL_1:9;

(- (t . (DataLoc ((s . a),i)))) - 1 <= k by A8, XREAL_1:20;

then A18: (- n) - (t . (DataLoc ((s . a),i))) <= k by A17, XXREAL_0:2;

A19: I is_closed_on t,Q by A5, A9, A10;

then A20: I is_closed_on Initialize t,Q +* (stop I) by SCMPDS_6:24;

A21: not DataLoc ((s . a),i) in dom (Start-At (0,SCMPDS)) by SCMPDS_4:18;

set m2 = LifeSpan ((Q +* (stop I)),(Initialize t));

set t5 = Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t))));

set Q5 = Q +* (stop (for-up (a,i,n,I)));

set l1 = (card I) + 1;

A22: IC (Initialize t) = 0 by MEMSTR_0:def 11;

set m3 = (LifeSpan ((Q +* (stop I)),(Initialize t))) + 1;

set t6 = Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1));

set Q6 = Q +* (stop (for-up (a,i,n,I)));

(card I) + 1 < (card I) + 3 by XREAL_1:6;

then A23: (card I) + 1 in dom (for-up (a,i,n,I)) by Th31;

set m5 = (((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1;

set t8 = Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1));

set Q8 = Q +* (stop (for-up (a,i,n,I)));

set t7 = Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1));

set Q7 = Q +* (stop (for-up (a,i,n,I)));

A24: (IExec (I,Q,(Initialize t))) . a = t . a by A5, A9, A10;

set l2 = (card I) + 2;

A25: 0 in dom (stop (for-up (a,i,n,I))) by COMPOS_1:36;

(card I) + 2 < (card I) + 3 by XREAL_1:6;

then A26: (card I) + 2 in dom (for-up (a,i,n,I)) by Th31;

A27: stop (for-up (a,i,n,I)) c= Q +* (stop (for-up (a,i,n,I))) by FUNCT_4:25;

for-up (a,i,n,I) c= stop (for-up (a,i,n,I)) by AFINSQ_1:74;

then A28: for-up (a,i,n,I) c= Q +* (stop (for-up (a,i,n,I))) by A27, XBOOLE_1:1;

Shift (I,1) c= for-up (a,i,n,I) by Lm3;

then A29: Shift (I,1) c= Q +* (stop (for-up (a,i,n,I))) by A28, XBOOLE_1:1;

I is_halting_on t,Q by A5, A9, A10;

then A30: Q +* (stop I) halts_on Initialize t by SCMPDS_6:def 3;

(Q +* (stop I)) +* (stop I) halts_on Initialize (Initialize t) by A30;

then A31: I is_halting_on Initialize t,Q +* (stop I) by SCMPDS_6:def 3;

not a in dom (Start-At (0,SCMPDS)) by SCMPDS_4:18;

then (Initialize t) . (DataLoc (((Initialize t) . a),i)) = (Initialize t) . (DataLoc ((s . a),i)) by A10, FUNCT_4:11

.= t . (DataLoc ((s . a),i)) by A21, FUNCT_4:11 ;

then A32: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)) = 0 + 1 by A22, A11, A14, SCMPDS_2:57;

then A33: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t))))) = (card I) + 1 by A12, A31, A20, A15, A29, Th16;

A34: (Q +* (stop (for-up (a,i,n,I)))) /. (IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1)))) = (Q +* (stop (for-up (a,i,n,I)))) . (IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1)))) by PBOOLE:143;

A35: Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1)) = Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t)))) by EXTPRO_1:4;

then A36: CurInstr ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1)))) = (Q +* (stop (for-up (a,i,n,I)))) . ((card I) + 1) by A12, A31, A20, A32, A15, A29, Th16, A34

.= (for-up (a,i,n,I)) . ((card I) + 1) by A23, A28, GRFUNC_1:2

.= AddTo (a,i,n) by Th32 ;

A37: Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1)) = Following ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1)))) by EXTPRO_1:3

.= Exec ((AddTo (a,i,n)),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1)))) by A36 ;

then A38: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) = (IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1)))) + 1 by SCMPDS_2:48

.= (card I) + (1 + 1) by A33, A35 ;

then A39: CurInstr ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1)))) = (Q +* (stop (for-up (a,i,n,I)))) . ((card I) + 2) by PBOOLE:143

.= (for-up (a,i,n,I)) . ((card I) + 2) by A28, A26, GRFUNC_1:2

.= goto (- ((card I) + 2)) by Th32 ;

A40: Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1)) = Following ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1)))) by EXTPRO_1:3

.= Exec ((goto (- ((card I) + 2))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1)))) by A39 ;

then IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) = ICplusConst ((Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))),(0 - ((card I) + 2))) by SCMPDS_2:54

.= 0 by A38, Th1 ;

then A41: Initialize (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) = Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1)) by MEMSTR_0:46;

A42: DataPart (Comput ((Q +* (stop I)),(Initialize t),(LifeSpan ((Q +* (stop I)),(Initialize t))))) = DataPart (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t))))) by A12, A31, A20, A32, A15, A29, Th16;

then A43: (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t))))) . a = (Comput ((Q +* (stop I)),(Initialize t),(LifeSpan ((Q +* (stop I)),(Initialize t))))) . a by SCMPDS_4:8

.= s . a by A10, A24, A30, EXTPRO_1:23 ;

then DataLoc (((Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1))) . a),i) = DataLoc ((s . a),i) by EXTPRO_1:4;

then (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) . a = (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1))) . a by A4, A37, SCMPDS_2:48

.= s . a by A43, EXTPRO_1:4 ;

then A44: (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) . a = s . a by A40, SCMPDS_2:54;

A45: now :: thesis: for x being Int_position st x in X holds

(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) . x = s . x

A47: (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t))))) . (DataLoc ((s . a),i)) =
(Comput ((Q +* (stop I)),(Initialize t),(LifeSpan ((Q +* (stop I)),(Initialize t))))) . (DataLoc ((s . a),i))
by A42, SCMPDS_4:8
(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) . x = s . x

let x be Int_position; :: thesis: ( x in X implies (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) . x = s . x )

assume A46: x in X ; :: thesis: (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) . x = s . x

(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t))))) . x = (Comput ((Q +* (stop I)),(Initialize t),(LifeSpan ((Q +* (stop I)),(Initialize t))))) . x by A42, SCMPDS_4:8

.= (IExec (I,Q,(Initialize t))) . x by A30, EXTPRO_1:23

.= t . x by A5, A9, A10, A46

.= s . x by A9, A46 ;

then (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) . x = s . x by A2, A43, A35, A37, A46, SCMPDS_2:48;

hence (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) . x = s . x by A40, SCMPDS_2:54; :: thesis: verum

end;assume A46: x in X ; :: thesis: (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) . x = s . x

(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t))))) . x = (Comput ((Q +* (stop I)),(Initialize t),(LifeSpan ((Q +* (stop I)),(Initialize t))))) . x by A42, SCMPDS_4:8

.= (IExec (I,Q,(Initialize t))) . x by A30, EXTPRO_1:23

.= t . x by A5, A9, A10, A46

.= s . x by A9, A46 ;

then (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) . x = s . x by A2, A43, A35, A37, A46, SCMPDS_2:48;

hence (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) . x = s . x by A40, SCMPDS_2:54; :: thesis: verum

.= t . (DataLoc ((s . a),i)) by A16, A30, EXTPRO_1:23 ;

(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) . (DataLoc ((s . a),i)) = (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) . (DataLoc ((s . a),i)) by A40, SCMPDS_2:54

.= (t . (DataLoc ((s . a),i))) + n by A43, A47, A35, A37, SCMPDS_2:48 ;

then A48: - ((Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) . (DataLoc ((s . a),i))) = (- n) - (t . (DataLoc ((s . a),i))) ;

then A49: for-up (a,i,n,I) is_closed_on Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1)),Q +* (stop (for-up (a,i,n,I))) by A7, A44, A45, A18;

now :: thesis: for k being Nat holds IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),k)) in dom (stop (for-up (a,i,n,I)))

hence
for-up (a,i,n,I) is_closed_on t,Q
by SCMPDS_6:def 2; :: thesis: for-up (a,i,n,I) is_halting_on t,Qlet k be Nat; :: thesis: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),b_{1})) in dom (stop (for-up (a,i,n,I)))

end;per cases
( k < (((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1 or k >= (((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1 )
;

end;

suppose
k < (((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1
; :: thesis: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),b_{1})) in dom (stop (for-up (a,i,n,I)))

then
k <= ((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1
by INT_1:7;

then A50: ( k <= (LifeSpan ((Q +* (stop I)),(Initialize t))) + 1 or k = ((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1 ) by NAT_1:8;

end;then A50: ( k <= (LifeSpan ((Q +* (stop I)),(Initialize t))) + 1 or k = ((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1 ) by NAT_1:8;

hereby :: thesis: verum
end;

per cases
( k <= LifeSpan ((Q +* (stop I)),(Initialize t)) or k = (LifeSpan ((Q +* (stop I)),(Initialize t))) + 1 or k = ((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1 )
by A50, NAT_1:8;

end;

suppose A51:
k <= LifeSpan ((Q +* (stop I)),(Initialize t))
; :: thesis: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),k)) in dom (stop (for-up (a,i,n,I)))

end;

hereby :: thesis: verum
end;

per cases
( k = 0 or k <> 0 )
;

end;

suppose
k = 0
; :: thesis: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),k)) in dom (stop (for-up (a,i,n,I)))

hence
IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),k)) in dom (stop (for-up (a,i,n,I)))
by A25, A22; :: thesis: verum

end;suppose
k <> 0
; :: thesis: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),k)) in dom (stop (for-up (a,i,n,I)))

then consider kn being Nat such that

A52: k = kn + 1 by NAT_1:6;

reconsider kn = kn as Nat ;

reconsider lm = IC (Comput ((Q +* (stop I)),(Initialize t),kn)) as Nat ;

kn < k by A52, XREAL_1:29;

then kn < LifeSpan ((Q +* (stop I)),(Initialize t)) by A51, XXREAL_0:2;

then (IC (Comput ((Q +* (stop I)),(Initialize t),kn))) + 1 = IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)),kn)) by A12, A31, A20, A32, A15, A29, Th14;

then A53: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),k)) = lm + 1 by A52, EXTPRO_1:4;

IC (Comput ((Q +* (stop I)),(Initialize t),kn)) in dom (stop I) by A19, SCMPDS_6:def 2;

then lm < card (stop I) by AFINSQ_1:66;

then lm < (card I) + 1 by COMPOS_1:55;

then A54: lm + 1 <= (card I) + 1 by INT_1:7;

(card I) + 1 < (card I) + 4 by XREAL_1:6;

then lm + 1 < (card I) + 4 by A54, XXREAL_0:2;

then lm + 1 < card (stop (for-up (a,i,n,I))) by Lm2;

hence IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),k)) in dom (stop (for-up (a,i,n,I))) by A53, AFINSQ_1:66; :: thesis: verum

end;A52: k = kn + 1 by NAT_1:6;

reconsider kn = kn as Nat ;

reconsider lm = IC (Comput ((Q +* (stop I)),(Initialize t),kn)) as Nat ;

kn < k by A52, XREAL_1:29;

then kn < LifeSpan ((Q +* (stop I)),(Initialize t)) by A51, XXREAL_0:2;

then (IC (Comput ((Q +* (stop I)),(Initialize t),kn))) + 1 = IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)),kn)) by A12, A31, A20, A32, A15, A29, Th14;

then A53: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),k)) = lm + 1 by A52, EXTPRO_1:4;

IC (Comput ((Q +* (stop I)),(Initialize t),kn)) in dom (stop I) by A19, SCMPDS_6:def 2;

then lm < card (stop I) by AFINSQ_1:66;

then lm < (card I) + 1 by COMPOS_1:55;

then A54: lm + 1 <= (card I) + 1 by INT_1:7;

(card I) + 1 < (card I) + 4 by XREAL_1:6;

then lm + 1 < (card I) + 4 by A54, XXREAL_0:2;

then lm + 1 < card (stop (for-up (a,i,n,I))) by Lm2;

hence IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),k)) in dom (stop (for-up (a,i,n,I))) by A53, AFINSQ_1:66; :: thesis: verum

suppose A55:
k = (LifeSpan ((Q +* (stop I)),(Initialize t))) + 1
; :: thesis: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),k)) in dom (stop (for-up (a,i,n,I)))

(card I) + 1 in dom (stop (for-up (a,i,n,I)))
by A23, COMPOS_1:62;

hence IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),k)) in dom (stop (for-up (a,i,n,I))) by A12, A31, A20, A32, A15, A29, A35, A55, Th16; :: thesis: verum

end;hence IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),k)) in dom (stop (for-up (a,i,n,I))) by A12, A31, A20, A32, A15, A29, A35, A55, Th16; :: thesis: verum

suppose
k = ((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1
; :: thesis: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),k)) in dom (stop (for-up (a,i,n,I)))

hence
IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),k)) in dom (stop (for-up (a,i,n,I)))
by A38, A26, COMPOS_1:62; :: thesis: verum

end;suppose
k >= (((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1
; :: thesis: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),b_{1})) in dom (stop (for-up (a,i,n,I)))

then consider nn being Nat such that

A56: k = ((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1) + nn by NAT_1:10;

reconsider nn = nn as Nat ;

Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),k) = Comput (((Q +* (stop (for-up (a,i,n,I)))) +* (stop (for-up (a,i,n,I)))),(Initialize (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1)))),nn) by A41, A56, EXTPRO_1:4;

hence IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),k)) in dom (stop (for-up (a,i,n,I))) by A49, SCMPDS_6:def 2; :: thesis: verum

end;A56: k = ((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1) + nn by NAT_1:10;

reconsider nn = nn as Nat ;

Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),k) = Comput (((Q +* (stop (for-up (a,i,n,I)))) +* (stop (for-up (a,i,n,I)))),(Initialize (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1)))),nn) by A41, A56, EXTPRO_1:4;

hence IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),k)) in dom (stop (for-up (a,i,n,I))) by A49, SCMPDS_6:def 2; :: thesis: verum

A57: (Q +* (stop (for-up (a,i,n,I)))) +* (stop (for-up (a,i,n,I))) = Q +* (stop (for-up (a,i,n,I))) ;

for-up (a,i,n,I) is_halting_on Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1)),Q +* (stop (for-up (a,i,n,I))) by A7, A44, A45, A18, A48;

then Q +* (stop (for-up (a,i,n,I))) halts_on Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1)) by A41, A57, SCMPDS_6:def 3;

then Q +* (stop (for-up (a,i,n,I))) halts_on Initialize t by EXTPRO_1:22;

hence for-up (a,i,n,I) is_halting_on t,Q by SCMPDS_6:def 3; :: thesis: verum

A58: S

proof

for k being Nat holds S
let t be State of SCMPDS; :: thesis: for Q being Instruction-Sequence of SCMPDS st - (t . (DataLoc ((s . a),i))) <= 0 & ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a holds

( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q )

let Q be Instruction-Sequence of SCMPDS; :: thesis: ( - (t . (DataLoc ((s . a),i))) <= 0 & ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a implies ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q ) )

assume - (t . (DataLoc ((s . a),i))) <= 0 ; :: thesis: ( ex x being Int_position st

( x in X & not t . x = s . x ) or not t . a = s . a or ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q ) )

then - (t . (DataLoc ((s . a),i))) <= - 0 ;

then A59: t . (DataLoc ((s . a),i)) >= 0 by XREAL_1:24;

assume for x being Int_position st x in X holds

t . x = s . x ; :: thesis: ( not t . a = s . a or ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q ) )

assume t . a = s . a ; :: thesis: ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q )

hence ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q ) by A59, Th33; :: thesis: verum

end;t . x = s . x ) & t . a = s . a holds

( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q )

let Q be Instruction-Sequence of SCMPDS; :: thesis: ( - (t . (DataLoc ((s . a),i))) <= 0 & ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a implies ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q ) )

assume - (t . (DataLoc ((s . a),i))) <= 0 ; :: thesis: ( ex x being Int_position st

( x in X & not t . x = s . x ) or not t . a = s . a or ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q ) )

then - (t . (DataLoc ((s . a),i))) <= - 0 ;

then A59: t . (DataLoc ((s . a),i)) >= 0 by XREAL_1:24;

assume for x being Int_position st x in X holds

t . x = s . x ; :: thesis: ( not t . a = s . a or ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q ) )

assume t . a = s . a ; :: thesis: ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q )

hence ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q ) by A59, Th33; :: thesis: verum

then A60: S

for x being Int_position st x in X holds

s . x = s . x ;

hence ( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P ) by A60; :: thesis: verum