let s be State of SCMPDS ; :: thesis: for I being shiftable No-StopCode Program of SCMPDS
for a, x1, x2, x3, x4 being Int_position
for i, c, md being Integer st card I > 0 & s . x4 = ((s . x3) - c) + (s . x1) & md <= (s . x3) - c & ( for t being State 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,t) . a = t . a & I is_closed_on t & I is_halting_on t & (IExec I,t) . (DataLoc (s . a),i) < t . (DataLoc (s . a),i) & (IExec I,t) . x4 = (((IExec I,t) . x3) - c) + ((IExec I,t) . x1) & md <= ((IExec I,t) . x3) - c & (IExec I,t) . x2 = t . x2 ) ) holds
( while>0 a,i,I is_closed_on s & while>0 a,i,I is_halting_on s & ( s . (DataLoc (s . a),i) > 0 implies IExec (while>0 a,i,I),s = IExec (while>0 a,i,I),(IExec I,s) ) )
let I be shiftable No-StopCode Program of SCMPDS ; :: thesis: for a, x1, x2, x3, x4 being Int_position
for i, c, md being Integer st card I > 0 & s . x4 = ((s . x3) - c) + (s . x1) & md <= (s . x3) - c & ( for t being State 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,t) . a = t . a & I is_closed_on t & I is_halting_on t & (IExec I,t) . (DataLoc (s . a),i) < t . (DataLoc (s . a),i) & (IExec I,t) . x4 = (((IExec I,t) . x3) - c) + ((IExec I,t) . x1) & md <= ((IExec I,t) . x3) - c & (IExec I,t) . x2 = t . x2 ) ) holds
( while>0 a,i,I is_closed_on s & while>0 a,i,I is_halting_on s & ( s . (DataLoc (s . a),i) > 0 implies IExec (while>0 a,i,I),s = IExec (while>0 a,i,I),(IExec I,s) ) )
let a, x1, x2, x3, x4 be Int_position ; :: thesis: for i, c, md being Integer st card I > 0 & s . x4 = ((s . x3) - c) + (s . x1) & md <= (s . x3) - c & ( for t being State 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,t) . a = t . a & I is_closed_on t & I is_halting_on t & (IExec I,t) . (DataLoc (s . a),i) < t . (DataLoc (s . a),i) & (IExec I,t) . x4 = (((IExec I,t) . x3) - c) + ((IExec I,t) . x1) & md <= ((IExec I,t) . x3) - c & (IExec I,t) . x2 = t . x2 ) ) holds
( while>0 a,i,I is_closed_on s & while>0 a,i,I is_halting_on s & ( s . (DataLoc (s . a),i) > 0 implies IExec (while>0 a,i,I),s = IExec (while>0 a,i,I),(IExec I,s) ) )
let i, c, md be Integer; :: thesis: ( card I > 0 & s . x4 = ((s . x3) - c) + (s . x1) & md <= (s . x3) - c & ( for t being State 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,t) . a = t . a & I is_closed_on t & I is_halting_on t & (IExec I,t) . (DataLoc (s . a),i) < t . (DataLoc (s . a),i) & (IExec I,t) . x4 = (((IExec I,t) . x3) - c) + ((IExec I,t) . x1) & md <= ((IExec I,t) . x3) - c & (IExec I,t) . x2 = t . x2 ) ) implies ( while>0 a,i,I is_closed_on s & while>0 a,i,I is_halting_on s & ( s . (DataLoc (s . a),i) > 0 implies IExec (while>0 a,i,I),s = IExec (while>0 a,i,I),(IExec I,s) ) ) )
set b = DataLoc (s . a),i;
assume A1: card I > 0 ; :: thesis: ( not s . x4 = ((s . x3) - c) + (s . x1) or not md <= (s . x3) - c or ex t being State 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,t) . a = t . a & I is_closed_on t & I is_halting_on t & (IExec I,t) . (DataLoc (s . a),i) < t . (DataLoc (s . a),i) & (IExec I,t) . x4 = (((IExec I,t) . x3) - c) + ((IExec I,t) . x1) & md <= ((IExec I,t) . x3) - c & (IExec I,t) . x2 = t . x2 ) ) or ( while>0 a,i,I is_closed_on s & while>0 a,i,I is_halting_on s & ( s . (DataLoc (s . a),i) > 0 implies IExec (while>0 a,i,I),s = IExec (while>0 a,i,I),(IExec I,s) ) ) )
assume A2: ( s . x4 = ((s . x3) - c) + (s . x1) & md <= (s . x3) - c ) ; :: thesis: ( ex t being State 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,t) . a = t . a & I is_closed_on t & I is_halting_on t & (IExec I,t) . (DataLoc (s . a),i) < t . (DataLoc (s . a),i) & (IExec I,t) . x4 = (((IExec I,t) . x3) - c) + ((IExec I,t) . x1) & md <= ((IExec I,t) . x3) - c & (IExec I,t) . x2 = t . x2 ) ) or ( while>0 a,i,I is_closed_on s & while>0 a,i,I is_halting_on s & ( s . (DataLoc (s . a),i) > 0 implies IExec (while>0 a,i,I),s = IExec (while>0 a,i,I),(IExec I,s) ) ) )
assume A3: for t being State 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,t) . a = t . a & I is_closed_on t & I is_halting_on t & (IExec I,t) . (DataLoc (s . a),i) < t . (DataLoc (s . a),i) & (IExec I,t) . x4 = (((IExec I,t) . x3) - c) + ((IExec I,t) . x1) & md <= ((IExec I,t) . x3) - c & (IExec I,t) . x2 = t . x2 ) ; :: thesis: ( while>0 a,i,I is_closed_on s & while>0 a,i,I is_halting_on s & ( s . (DataLoc (s . a),i) > 0 implies IExec (while>0 a,i,I),s = IExec (while>0 a,i,I),(IExec I,s) ) )
defpred S1[ 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 );
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 H1( State of SCMPDS ) -> Element of NAT = f . $1;
A5: for t being State of SCMPDS holds
( H1( Dstate t) = 0 iff t . (DataLoc (s . a),i) <= 0 )
proof
let t be State of SCMPDS ; :: thesis: ( H1( Dstate t) = 0 iff t . (DataLoc (s . a),i) <= 0 )
thus ( H1( Dstate t) = 0 implies t . (DataLoc (s . a),i) <= 0 ) :: thesis: ( t . (DataLoc (s . a),i) <= 0 implies H1( Dstate t) = 0 )
proof
assume A6: H1( Dstate t) = 0 ; :: thesis: t . (DataLoc (s . a),i) <= 0
assume t . (DataLoc (s . a),i) > 0 ; :: thesis: contradiction
then (Dstate t) . (DataLoc (s . a),i) > 0 by SCMPDS_8:4;
hence contradiction by A4, A6; :: thesis: verum
end;
assume t . (DataLoc (s . a),i) <= 0 ; :: thesis: H1( Dstate t) = 0
then (Dstate t) . (DataLoc (s . a),i) <= 0 by SCMPDS_8:4;
hence H1( Dstate t) = 0 by A4; :: thesis: verum
end;
then A7: for t being State of SCMPDS st S1[ Dstate t] & H1( Dstate t) = 0 holds
t . (DataLoc (s . a),i) <= 0 ;
A8: S1[ Dstate s]
proof
take t = Dstate s; :: thesis: ( t = Dstate s & t . x4 = ((t . x3) - c) + (t . x1) & md <= (t . x3) - c & t . x2 = s . x2 )
thus t = Dstate s ; :: thesis: ( t . x4 = ((t . x3) - c) + (t . x1) & md <= (t . x3) - c & t . x2 = s . x2 )
t . x4 = ((s . x3) - c) + (s . x1) by A2, SCMPDS_8:4;
then t . x4 = ((t . x3) - c) + (s . x1) by SCMPDS_8:4;
hence t . x4 = ((t . x3) - c) + (t . x1) by SCMPDS_8:4; :: thesis: ( md <= (t . x3) - c & t . x2 = s . x2 )
thus md <= (t . x3) - c by A2, SCMPDS_8:4; :: thesis: t . x2 = s . x2
thus t . x2 = s . x2 by SCMPDS_8:4; :: thesis: verum
end;
A9: now
let t be State of SCMPDS ; :: thesis: ( S1[ Dstate t] & t . a = s . a & t . (DataLoc (s . a),i) > 0 implies ( (IExec I,t) . a = t . a & I is_closed_on t & I is_halting_on t & H1( Dstate (IExec I,t)) < H1( Dstate t) & S1[ Dstate (IExec I,t)] ) )
assume A10: ( S1[ Dstate t] & t . a = s . a & t . (DataLoc (s . a),i) > 0 ) ; :: thesis: ( (IExec I,t) . a = t . a & I is_closed_on t & I is_halting_on t & H1( Dstate (IExec I,t)) < H1( Dstate t) & S1[ Dstate (IExec I,t)] )
then consider v being State of SCMPDS such that
A11: ( v = Dstate t & v . x4 = ((v . x3) - c) + (v . x1) & md <= (v . x3) - c & v . x2 = s . x2 ) ;
t . x4 = ((v . x3) - c) + (v . x1) by A11, SCMPDS_8:4;
then t . x4 = ((t . x3) - c) + (v . x1) by A11, SCMPDS_8:4;
then A12: t . x4 = ((t . x3) - c) + (t . x1) by A11, SCMPDS_8:4;
A13: md <= (t . x3) - c by A11, SCMPDS_8:4;
A14: t . x2 = s . x2 by A11, SCMPDS_8:4;
hence ( (IExec I,t) . a = t . a & I is_closed_on t & I is_halting_on t ) by A3, A10, A12, A13; :: thesis: ( H1( Dstate (IExec I,t)) < H1( Dstate t) & S1[ Dstate (IExec I,t)] )
set It = IExec I,t;
set t2 = Dstate (IExec I,t);
set t1 = Dstate t;
thus H1( Dstate (IExec I,t)) < H1( Dstate t) :: thesis: S1[ Dstate (IExec I,t)]
proof
assume A15: H1( Dstate (IExec I,t)) >= H1( Dstate t) ; :: thesis: contradiction
(Dstate t) . (DataLoc (s . a),i) > 0 by A10, SCMPDS_8:4;
then A16: H1( Dstate t) = (Dstate t) . (DataLoc (s . a),i) by A4
.= t . (DataLoc (s . a),i) by SCMPDS_8:4 ;
then (IExec I,t) . (DataLoc (s . a),i) > 0 by A5, A10, A15;
then (Dstate (IExec I,t)) . (DataLoc (s . a),i) > 0 by SCMPDS_8:4;
then H1( Dstate (IExec I,t)) = (Dstate (IExec I,t)) . (DataLoc (s . a),i) by A4
.= (IExec I,t) . (DataLoc (s . a),i) by SCMPDS_8:4 ;
hence contradiction by A3, A10, A12, A13, A14, A15, A16; :: thesis: verum
end;
thus S1[ Dstate (IExec I,t)] :: thesis: verum
proof
take v = Dstate (IExec I,t); :: thesis: ( v = Dstate (IExec I,t) & v . x4 = ((v . x3) - c) + (v . x1) & md <= (v . x3) - c & v . x2 = s . x2 )
thus v = Dstate (IExec I,t) ; :: thesis: ( v . x4 = ((v . x3) - c) + (v . x1) & md <= (v . x3) - c & v . x2 = s . x2 )
(IExec I,t) . x4 = (((IExec I,t) . x3) - c) + ((IExec I,t) . x1) by A3, A10, A12, A13, A14;
then v . x4 = (((IExec I,t) . x3) - c) + ((IExec I,t) . x1) by SCMPDS_8:4;
then v . x4 = ((v . x3) - c) + ((IExec I,t) . x1) by SCMPDS_8:4;
hence v . x4 = ((v . x3) - c) + (v . x1) by SCMPDS_8:4; :: thesis: ( md <= (v . x3) - c & v . x2 = s . x2 )
md <= ((IExec I,t) . x3) - c by A3, A10, A12, A13, A14;
hence md <= (v . x3) - c by SCMPDS_8:4; :: thesis: v . x2 = s . x2
(IExec I,t) . x2 = t . x2 by A3, A10, A12, A13, A14;
hence v . x2 = s . x2 by A14, SCMPDS_8:4; :: thesis: verum
end;
end;
( ( H1(s) = H1(s) or S1[s] ) & while>0 a,i,I is_closed_on s & while>0 a,i,I is_halting_on s ) from SCMPDS_8:sch 3(A1, A7, A8, A9);
 hence ( while>0 a,i,I is_closed_on s & while>0 a,i,I is_halting_on s ) ; :: thesis: ( s . (DataLoc (s . a),i) > 0 implies IExec (while>0 a,i,I),s = IExec (while>0 a,i,I),(IExec I,s) )
assume A17: s . (DataLoc (s . a),i) > 0 ; :: thesis: IExec (while>0 a,i,I),s = IExec (while>0 a,i,I),(IExec I,s)
( ( H1(s) = H1(s) or S1[s] ) & IExec (while>0 a,i,I),s = IExec (while>0 a,i,I),(IExec I,s) ) from SCMPDS_8:sch 4(A1, A17, A7, A8, A9);
 hence IExec (while>0 a,i,I),s = IExec (while>0 a,i,I),(IExec I,s) ; :: thesis: verum