let P be Instruction-Sequence of SCMPDS; :: thesis: 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 & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . x >= c & 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)) . 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; :: thesis: for I being halt-free shiftable Program of
for a, x, y being Int_position
for i, c being Integer st s . x >= c & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . x >= c & 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)) . 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 ; :: thesis: for a, x, y being Int_position
for i, c being Integer st s . x >= c & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . x >= c & 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)) . 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, x, y be Int_position; :: thesis: for i, c being Integer st s . x >= c & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . x >= c & 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)) . 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, c be Integer; :: thesis: ( s . x >= c & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . x >= c & 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)) . y = t . y ) ) 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);
defpred S1[ set ] means ex t being State of SCMPDS st
( t = $1 & t . x >= c & t . y = s . y );
consider f being Function of (product (the_Values_of SCMPDS)),NAT such that
A1: for s being State of SCMPDS holds
( ( s . (DataLoc ((s . a),i)) <= 0 implies f . s = 0 ) & ( s . (DataLoc ((s . a),i)) > 0 implies f . s = s . (DataLoc ((s . a),i)) ) ) by SCMPDS_8:5;
deffunc H1( State of SCMPDS) -> Element of NAT = f . $1;
A2: for t being 0 -started State of SCMPDS st S1[t] & H1(t) = 0 holds
t . (DataLoc ((s . a),i)) <= 0 by A1;
assume A3: s . x >= c ; :: thesis: ( ex t being 0 -started State of SCMPDS ex Q being Instruction-Sequence of SCMPDS st
( t . x >= c & t . y = s . y & 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)) . x >= c & (IExec (I,Q,t)) . y = t . y ) ) 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)))) ) ) )
A4: S1[s] by A3;
assume A5: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . x >= c & 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)) . y = t . y ) ; :: thesis: ( 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)))) ) )
A6: now :: thesis: 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; :: thesis: 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; :: thesis: ( 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))] ) )
assume that
A7: S1[t] and
A8: t . a = s . a and
A9: 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 & H1( Initialize (IExec (I,Q,t))) < H1(t) & S1[ Initialize (IExec (I,Q,t))] )
set It = IExec (I,Q,t);
set t2 = Initialize (IExec (I,Q,t));
thus ( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q ) by A5, A8, A9, A7; :: thesis: ( H1( Initialize (IExec (I,Q,t))) < H1(t) & S1[ Initialize (IExec (I,Q,t))] )
thus H1( Initialize (IExec (I,Q,t))) < H1(t) :: thesis: S1[ Initialize (IExec (I,Q,t))]
proof
A10: H1(t) = t . (DataLoc ((s . a),i)) by A1, A9;
assume A11: H1( Initialize (IExec (I,Q,t))) >= H1(t) ; :: thesis: contradiction
then (Initialize (IExec (I,Q,t))) . (DataLoc ((s . a),i)) > 0 by A1, A9, A10;
then H1( Initialize (IExec (I,Q,t))) = (Initialize (IExec (I,Q,t))) . (DataLoc ((s . a),i)) by A1
.= (IExec (I,Q,t)) . (DataLoc ((s . a),i)) by SCMPDS_5:15 ;
hence contradiction by A5, A8, A9, A7, A11, A10; :: thesis: verum
end;
thus S1[ Initialize (IExec (I,Q,t))] :: thesis: verum
proof
take v = Initialize (IExec (I,Q,t)); :: thesis: ( v = Initialize (IExec (I,Q,t)) & v . x >= c & v . y = s . y )
thus v = Initialize (IExec (I,Q,t)) ; :: thesis: ( v . x >= c & v . y = s . y )
(IExec (I,Q,t)) . x >= c by A5, A8, A9, A7;
hence v . x >= c by SCMPDS_5:15; :: thesis: v . y = s . y
(IExec (I,Q,t)) . y = t . y by A5, A8, A9, A7;
hence v . y = s . y by A7, SCMPDS_5:15; :: thesis: verum
end;
end;
( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P ) from SCMPDS_8:sch 3(A2, A4, A6);
 hence ( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P ) ; :: thesis: ( 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)))) )
assume A12: s . (DataLoc ((s . a),i)) > 0 ; :: thesis: IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,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 4(A12, A2, A4, A6);
 hence IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) ; :: thesis: verum