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₁( State of SCMPDS) -> Element of NAT = f . $1;
defpred S₁[ 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₁[t] & H₁(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))))

A4: now :: thesis: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st S₁[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₁( Initialize (IExec (I,Q,t))) < H₁(t) & S₁[ Initialize (IExec (I,Q,t))] )

let t be 0 -started State of SCMPDS; :: thesis: for Q being Instruction-Sequence of SCMPDS st S₁[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₁( Initialize (IExec (I,Q,t))) < H₁(t) & S₁[ Initialize (IExec (I,Q,t))] )
let Q be Instruction-Sequence of SCMPDS; :: thesis: ( S₁[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₁( Initialize (IExec (I,Q,t))) < H₁(t) & S₁[ Initialize (IExec (I,Q,t))] ) )
set v = t;
assume that
A5: S₁[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₁( Initialize (IExec (I,Q,t))) < H₁(t) & S₁[ 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₁( Initialize (IExec (I,Q,t))) < H₁(t) ) by A3, A6, A5; :: thesis: S₁[ Initialize (IExec (I,Q,t))]
thus S₁[ Initialize (IExec (I,Q,t))] :: thesis: verum

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;

end;

A8: S₁[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