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

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for i being Integer

for X being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st s . (DataLoc ((s . a),i)) < 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) >= 0 ) & ( for t being 0 -started 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 & 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 & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

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 SCMPDS

for a being Int_position

for i being Integer

for X being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st s . (DataLoc ((s . a),i)) < 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) >= 0 ) & ( for t being 0 -started 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 & 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 & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

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 SCMPDS; :: thesis: for a being Int_position

for i being Integer

for X being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st s . (DataLoc ((s . a),i)) < 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) >= 0 ) & ( for t being 0 -started 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 & 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 & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

IExec ((while<0 (a,i,I)),P,s) = IExec ((while<0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

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

for X being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st s . (DataLoc ((s . a),i)) < 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) >= 0 ) & ( for t being 0 -started 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 & 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 & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

IExec ((while<0 (a,i,I)),P,s) = IExec ((while<0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

let i be Integer; :: thesis: for X being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st s . (DataLoc ((s . a),i)) < 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) >= 0 ) & ( for t being 0 -started 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 & 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 & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

IExec ((while<0 (a,i,I)),P,s) = IExec ((while<0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

let X be set ; :: thesis: for f being Function of (product (the_Values_of SCMPDS)),NAT st s . (DataLoc ((s . a),i)) < 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) >= 0 ) & ( for t being 0 -started 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 & 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 & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

IExec ((while<0 (a,i,I)),P,s) = IExec ((while<0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

let f be Function of (product (the_Values_of SCMPDS)),NAT; :: thesis: ( s . (DataLoc ((s . a),i)) < 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) >= 0 ) & ( for t being 0 -started 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 & 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 & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) 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);

deffunc H_{1}( State of SCMPDS) -> Element of NAT = f . $1;

defpred S_{1}[ State of SCMPDS] means for x being Int_position st x in X holds

$1 . x = s . x;

assume A1: s . (DataLoc ((s . a),i)) < 0 ; :: thesis: ( ex t being 0 -started State of SCMPDS st

( f . t = 0 & not t . (DataLoc ((s . a),i)) >= 0 ) or ex t being 0 -started 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 & 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 & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) or IExec ((while<0 (a,i,I)),P,s) = IExec ((while<0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) )

assume for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) >= 0 ; :: thesis: ( ex t being 0 -started 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 & 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 & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) or IExec ((while<0 (a,i,I)),P,s) = IExec ((while<0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) )

then A2: for t being 0 -started State of SCMPDS st S_{1}[t] & H_{1}(t) = 0 holds

t . (DataLoc ((s . a),i)) >= 0 ;

assume A3: for t being 0 -started 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 & 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 & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ; :: thesis: IExec ((while<0 (a,i,I)),P,s) = IExec ((while<0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

_{1}[s]
;

IExec ((while<0 (a,i,I)),P,s) = IExec ((while<0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) from SCMPDS_8:sch 2(A1, A2, A8, A4);

hence IExec ((while<0 (a,i,I)),P,s) = IExec ((while<0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) ; :: thesis: verum

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for i being Integer

for X being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st s . (DataLoc ((s . a),i)) < 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) >= 0 ) & ( for t being 0 -started 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 & 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 & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

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 SCMPDS

for a being Int_position

for i being Integer

for X being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st s . (DataLoc ((s . a),i)) < 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) >= 0 ) & ( for t being 0 -started 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 & 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 & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

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 SCMPDS; :: thesis: for a being Int_position

for i being Integer

for X being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st s . (DataLoc ((s . a),i)) < 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) >= 0 ) & ( for t being 0 -started 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 & 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 & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

IExec ((while<0 (a,i,I)),P,s) = IExec ((while<0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

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

for X being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st s . (DataLoc ((s . a),i)) < 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) >= 0 ) & ( for t being 0 -started 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 & 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 & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

IExec ((while<0 (a,i,I)),P,s) = IExec ((while<0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

let i be Integer; :: thesis: for X being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st s . (DataLoc ((s . a),i)) < 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) >= 0 ) & ( for t being 0 -started 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 & 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 & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

IExec ((while<0 (a,i,I)),P,s) = IExec ((while<0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

let X be set ; :: thesis: for f being Function of (product (the_Values_of SCMPDS)),NAT st s . (DataLoc ((s . a),i)) < 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) >= 0 ) & ( for t being 0 -started 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 & 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 & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

IExec ((while<0 (a,i,I)),P,s) = IExec ((while<0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

let f be Function of (product (the_Values_of SCMPDS)),NAT; :: thesis: ( s . (DataLoc ((s . a),i)) < 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) >= 0 ) & ( for t being 0 -started 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 & 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 & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) 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);

deffunc H

defpred S

$1 . x = s . x;

assume A1: s . (DataLoc ((s . a),i)) < 0 ; :: thesis: ( ex t being 0 -started State of SCMPDS st

( f . t = 0 & not t . (DataLoc ((s . a),i)) >= 0 ) or ex t being 0 -started 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 & 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 & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) or IExec ((while<0 (a,i,I)),P,s) = IExec ((while<0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) )

assume for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) >= 0 ; :: thesis: ( ex t being 0 -started 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 & 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 & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) or IExec ((while<0 (a,i,I)),P,s) = IExec ((while<0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) )

then A2: for t being 0 -started State of SCMPDS st S

t . (DataLoc ((s . a),i)) >= 0 ;

assume A3: for t being 0 -started 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 & 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 & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ; :: thesis: IExec ((while<0 (a,i,I)),P,s) = IExec ((while<0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

A4: now :: thesis: for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st S_{1}[t] & 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 & H_{1}( Initialize (IExec (I,Q,t))) < H_{1}(t) & S_{1}[ Initialize (IExec (I,Q,t))] )

A8:
Sfor Q being Instruction-Sequence of SCMPDS st S

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & H

let t be 0 -started State of SCMPDS; :: thesis: for Q being Instruction-Sequence of SCMPDS st S_{1}[t] & 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 & H_{1}( Initialize (IExec (I,Q,t))) < H_{1}(t) & S_{1}[ Initialize (IExec (I,Q,t))] )

let Q be Instruction-Sequence of SCMPDS; :: thesis: ( S_{1}[t] & 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 & H_{1}( Initialize (IExec (I,Q,t))) < H_{1}(t) & S_{1}[ Initialize (IExec (I,Q,t))] ) )

set v = t;

assume that

A5: S_{1}[t]
and

A6: ( t . a = s . a & 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 & H_{1}( Initialize (IExec (I,Q,t))) < H_{1}(t) & S_{1}[ Initialize (IExec (I,Q,t))] )

set It = IExec (I,Q,t);

thus ( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & H_{1}( Initialize (IExec (I,Q,t))) < H_{1}(t) )
by A3, A6, A5; :: thesis: S_{1}[ Initialize (IExec (I,Q,t))]

thus S_{1}[ Initialize (IExec (I,Q,t))]
:: thesis: verum

end;( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & H

let Q be Instruction-Sequence of SCMPDS; :: thesis: ( S

set v = t;

assume that

A5: S

A6: ( t . a = s . a & 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 & H

set It = IExec (I,Q,t);

thus ( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & H

thus S

proof

set v = Initialize (IExec (I,Q,t));

let x be Int_position; :: thesis: ( x in X implies (Initialize (IExec (I,Q,t))) . x = s . x )

assume A7: x in X ; :: thesis: (Initialize (IExec (I,Q,t))) . x = s . x

then (IExec (I,Q,t)) . x = t . x by A3, A6, A5;

then (Initialize (IExec (I,Q,t))) . x = t . x by SCMPDS_5:15;

hence (Initialize (IExec (I,Q,t))) . x = s . x by A5, A7; :: thesis: verum

end;let x be Int_position; :: thesis: ( x in X implies (Initialize (IExec (I,Q,t))) . x = s . x )

assume A7: x in X ; :: thesis: (Initialize (IExec (I,Q,t))) . x = s . x

then (IExec (I,Q,t)) . x = t . x by A3, A6, A5;

then (Initialize (IExec (I,Q,t))) . x = t . x by SCMPDS_5:15;

hence (Initialize (IExec (I,Q,t))) . x = s . x by A5, A7; :: thesis: verum

IExec ((while<0 (a,i,I)),P,s) = IExec ((while<0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) from SCMPDS_8:sch 2(A1, A2, A8, A4);

hence IExec ((while<0 (a,i,I)),P,s) = IExec ((while<0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) ; :: thesis: verum