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, x1, x2, x3, x4 being Int_position
for i, c, md being Integer st s . x4 = ((s . x3) - c) + (s . x1) & md <= (s . x3) - c & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . x4 = ((t . x3) - c) + (t . x1) & md <= (t . x3) - c & t . x2 = s . x2 & 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)) . x4 = (((IExec (I,Q,t)) . x3) - c) + ((IExec (I,Q,t)) . x1) & md <= ((IExec (I,Q,t)) . x3) - c & (IExec (I,Q,t)) . x2 = t . x2 ) ) 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 SCMPDS
for a, x1, x2, x3, x4 being Int_position
for i, c, md being Integer st s . x4 = ((s . x3) - c) + (s . x1) & md <= (s . x3) - c & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . x4 = ((t . x3) - c) + (t . x1) & md <= (t . x3) - c & t . x2 = s . x2 & 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)) . x4 = (((IExec (I,Q,t)) . x3) - c) + ((IExec (I,Q,t)) . x1) & md <= ((IExec (I,Q,t)) . x3) - c & (IExec (I,Q,t)) . x2 = t . x2 ) ) 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 SCMPDS; :: thesis: for a, x1, x2, x3, x4 being Int_position
for i, c, md being Integer st s . x4 = ((s . x3) - c) + (s . x1) & md <= (s . x3) - c & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . x4 = ((t . x3) - c) + (t . x1) & md <= (t . x3) - c & t . x2 = s . x2 & 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)) . x4 = (((IExec (I,Q,t)) . x3) - c) + ((IExec (I,Q,t)) . x1) & md <= ((IExec (I,Q,t)) . x3) - c & (IExec (I,Q,t)) . x2 = t . x2 ) ) 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, x1, x2, x3, x4 be Int_position ; :: thesis: for i, c, md being Integer st s . x4 = ((s . x3) - c) + (s . x1) & md <= (s . x3) - c & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . x4 = ((t . x3) - c) + (t . x1) & md <= (t . x3) - c & t . x2 = s . x2 & 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)) . x4 = (((IExec (I,Q,t)) . x3) - c) + ((IExec (I,Q,t)) . x1) & md <= ((IExec (I,Q,t)) . x3) - c & (IExec (I,Q,t)) . x2 = t . x2 ) ) 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, md be Integer; :: thesis: ( s . x4 = ((s . x3) - c) + (s . x1) & md <= (s . x3) - c & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . x4 = ((t . x3) - c) + (t . x1) & md <= (t . x3) - c & t . x2 = s . x2 & 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)) . x4 = (((IExec (I,Q,t)) . x3) - c) + ((IExec (I,Q,t)) . x1) & md <= ((IExec (I,Q,t)) . x3) - c & (IExec (I,Q,t)) . x2 = t . x2 ) ) 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 S₁[ set ] means ex t being State of SCMPDS st
( t = $1 & t . x4 = ((t . x3) - c) + (t . x1) & md <= (t . x3) - c & t . x2 = s . x2 );
assume that
A2: s . x4 = ((s . x3) - c) + (s . x1) and
A3: md <= (s . x3) - c ; :: thesis: ( ex t being 0 -started State of SCMPDS ex Q being Instruction-Sequence of SCMPDS st
( t . x4 = ((t . x3) - c) + (t . x1) & md <= (t . x3) - c & t . x2 = s . x2 & 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)) . x4 = (((IExec (I,Q,t)) . x3) - c) + ((IExec (I,Q,t)) . x1) & md <= ((IExec (I,Q,t)) . x3) - c & (IExec (I,Q,t)) . x2 = t . x2 ) ) 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)))) ) ) )
consider f being Function of (product the Object-Kind of SCMPDS),NAT such that
A4: 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 H₁( State of SCMPDS) -> Element of NAT = f . $1;
A7: for t being 0 -started State of SCMPDS st S₁[t] & H₁(t) = 0 holds
t . (DataLoc ((s . a),i)) <= 0 by A4;
assume A8: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . x4 = ((t . x3) - c) + (t . x1) & md <= (t . x3) - c & t . x2 = s . x2 & 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)) . x4 = (((IExec (I,Q,t)) . x3) - c) + ((IExec (I,Q,t)) . x1) & md <= ((IExec (I,Q,t)) . x3) - c & (IExec (I,Q,t)) . x2 = t . x2 ) ; :: 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)))) ) )

A9: now

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))] ) )
assume that
A10: S₁[t] and
A11: t . a = s . a and
A12: 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);
set t2 = Initialize (IExec (I,Q,t));
consider v being State of SCMPDS such that
A13: v = t and
A14: v . x4 = ((v . x3) - c) + (v . x1) and
A15: md <= (v . x3) - c and
A16: v . x2 = s . x2 by A10;
A17: t . x2 = s . x2 by A13, A16;
A18: t . x4 = ((t . x3) - c) + (t . x1) by A13, A14;
A19: md <= (t . x3) - c by A13, A15;
thus ( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q ) by A8, A11, A12, A18, A16, A13, A15; :: thesis: ( H₁( Initialize (IExec (I,Q,t))) < H₁(t) & S₁[ Initialize (IExec (I,Q,t))] )
thus H₁( Initialize (IExec (I,Q,t))) < H₁(t) :: thesis: S₁[ Initialize (IExec (I,Q,t))]

proof

A20: H₁(t) = t . (DataLoc ((s . a),i)) by A4, A12
.= t . (DataLoc ((s . a),i)) ;
assume A21: H₁( Initialize (IExec (I,Q,t))) >= H₁(t) ; :: thesis: contradiction
then (Initialize (IExec (I,Q,t))) . (DataLoc ((s . a),i)) > 0 by A4, A12, A20;
then H₁( Initialize (IExec (I,Q,t))) = (Initialize (IExec (I,Q,t))) . (DataLoc ((s . a),i)) by A4
.= (IExec (I,Q,t)) . (DataLoc ((s . a),i)) by SCMPDS_5:15 ;
hence contradiction by A8, A11, A12, A18, A19, A13, A16, A21, A20; :: thesis: verum

end;

thus S₁[ Initialize (IExec (I,Q,t))] :: thesis: verum

proof

take v = Initialize (IExec (I,Q,t)); :: thesis: ( v = Initialize (IExec (I,Q,t)) & v . x4 = ((v . x3) - c) + (v . x1) & md <= (v . x3) - c & v . x2 = s . x2 )
thus v = Initialize (IExec (I,Q,t)) ; :: thesis: ( v . x4 = ((v . x3) - c) + (v . x1) & md <= (v . x3) - c & v . x2 = s . x2 )
(IExec (I,Q,t)) . x4 = (((IExec (I,Q,t)) . x3) - c) + ((IExec (I,Q,t)) . x1) by A8, A11, A12, A18, A19, A17;
then v . x4 = (((IExec (I,Q,t)) . x3) - c) + ((IExec (I,Q,t)) . x1) by SCMPDS_5:15;
then v . x4 = ((v . x3) - c) + ((IExec (I,Q,t)) . x1) by SCMPDS_5:15;
hence v . x4 = ((v . x3) - c) + (v . x1) by SCMPDS_5:15; :: thesis: ( md <= (v . x3) - c & v . x2 = s . x2 )
md <= ((IExec (I,Q,t)) . x3) - c by A8, A11, A12, A18, A19, A17;
hence md <= (v . x3) - c by SCMPDS_5:15; :: thesis: v . x2 = s . x2
(IExec (I,Q,t)) . x2 = t . x2 by A8, A11, A12, A18, A19, A13, A16;
hence v . x2 = s . x2 by A13, A16, SCMPDS_5:15; :: thesis: verum

end;

end;

A22: S₁[s] by A2, A3;
( 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(A7, A22, A9);
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 A23: 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(A23, A7, A22, A9);
hence IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) ; :: thesis: verum