let P be Instruction-Sequence of SCMPDS; 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; 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; 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; 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; 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 ; 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; ( 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 H1( State of SCMPDS) -> Element of NAT = f . $1;
defpred S1[ 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
; ( 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
; ( 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 S1[t] & H1(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 ) )
; IExec ((while<0 (a,i,I)),P,s) = IExec ((while<0 (a,i,I)),P,(Initialize (IExec (I,P,s))))
A4:
now for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st S1[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 & H1( Initialize (IExec (I,Q,t))) < H1(t) & S1[ Initialize (IExec (I,Q,t))] )let t be
0 -started State of
SCMPDS;
for Q being Instruction-Sequence of SCMPDS st S1[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 & H1( Initialize (IExec (I,Q,t))) < H1(t) & S1[ Initialize (IExec (I,Q,t))] )let Q be
Instruction-Sequence of
SCMPDS;
( S1[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 & H1( Initialize (IExec (I,Q,t))) < H1(t) & S1[ Initialize (IExec (I,Q,t))] ) )set v =
t;
assume that A5:
S1[
t]
and A6:
(
t . a = s . a &
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 & H1( Initialize (IExec (I,Q,t))) < H1(t) & S1[ 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 &
H1(
Initialize (IExec (I,Q,t)))
< H1(
t) )
by A3, A6, A5;
S1[ Initialize (IExec (I,Q,t))]thus
S1[
Initialize (IExec (I,Q,t))]
verumproof
set v =
Initialize (IExec (I,Q,t));
let x be
Int_position;
( x in X implies (Initialize (IExec (I,Q,t))) . x = s . x )
assume A7:
x in X
;
(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;
verum
end; end;
A8:
S1[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))))
; verum