let s be State of SCMPDS ; :: thesis: for I being halt-free shiftable Program of SCMPDS
for a, f0, f1 being Int_position
for n, i being Element of NAT st card I > 0 & s . a = 0 & s . f0 = 0 & s . f1 = 1 & s . (intpos i) = n & ( for t being State of SCMPDS
for k being Element of NAT st n = (t . (intpos i)) + k & t . f0 = Fib k & t . f1 = Fib (k + 1) & t . a = 0 & t . (intpos i) > 0 holds
( (IExec I,t) . a = 0 & I is_closed_on t & I is_halting_on t & (IExec I,t) . (intpos i) = (t . (intpos i)) - 1 & (IExec I,t) . f0 = Fib (k + 1) & (IExec I,t) . f1 = Fib ((k + 1) + 1) ) ) holds
( (IExec (while>0 a,i,I),s) . f0 = Fib n & (IExec (while>0 a,i,I),s) . f1 = Fib (n + 1) & while>0 a,i,I is_closed_on s & while>0 a,i,I is_halting_on s )
let I be halt-free shiftable Program of SCMPDS ; :: thesis: for a, f0, f1 being Int_position
for n, i being Element of NAT st card I > 0 & s . a = 0 & s . f0 = 0 & s . f1 = 1 & s . (intpos i) = n & ( for t being State of SCMPDS
for k being Element of NAT st n = (t . (intpos i)) + k & t . f0 = Fib k & t . f1 = Fib (k + 1) & t . a = 0 & t . (intpos i) > 0 holds
( (IExec I,t) . a = 0 & I is_closed_on t & I is_halting_on t & (IExec I,t) . (intpos i) = (t . (intpos i)) - 1 & (IExec I,t) . f0 = Fib (k + 1) & (IExec I,t) . f1 = Fib ((k + 1) + 1) ) ) holds
( (IExec (while>0 a,i,I),s) . f0 = Fib n & (IExec (while>0 a,i,I),s) . f1 = Fib (n + 1) & while>0 a,i,I is_closed_on s & while>0 a,i,I is_halting_on s )
let a, f0, f1 be Int_position ; :: thesis: for n, i being Element of NAT st card I > 0 & s . a = 0 & s . f0 = 0 & s . f1 = 1 & s . (intpos i) = n & ( for t being State of SCMPDS
for k being Element of NAT st n = (t . (intpos i)) + k & t . f0 = Fib k & t . f1 = Fib (k + 1) & t . a = 0 & t . (intpos i) > 0 holds
( (IExec I,t) . a = 0 & I is_closed_on t & I is_halting_on t & (IExec I,t) . (intpos i) = (t . (intpos i)) - 1 & (IExec I,t) . f0 = Fib (k + 1) & (IExec I,t) . f1 = Fib ((k + 1) + 1) ) ) holds
( (IExec (while>0 a,i,I),s) . f0 = Fib n & (IExec (while>0 a,i,I),s) . f1 = Fib (n + 1) & while>0 a,i,I is_closed_on s & while>0 a,i,I is_halting_on s )
let n, i be Element of NAT ; :: thesis: ( card I > 0 & s . a = 0 & s . f0 = 0 & s . f1 = 1 & s . (intpos i) = n & ( for t being State of SCMPDS
for k being Element of NAT st n = (t . (intpos i)) + k & t . f0 = Fib k & t . f1 = Fib (k + 1) & t . a = 0 & t . (intpos i) > 0 holds
( (IExec I,t) . a = 0 & I is_closed_on t & I is_halting_on t & (IExec I,t) . (intpos i) = (t . (intpos i)) - 1 & (IExec I,t) . f0 = Fib (k + 1) & (IExec I,t) . f1 = Fib ((k + 1) + 1) ) ) implies ( (IExec (while>0 a,i,I),s) . f0 = Fib n & (IExec (while>0 a,i,I),s) . f1 = Fib (n + 1) & while>0 a,i,I is_closed_on s & while>0 a,i,I is_halting_on s ) )
assume A1: card I > 0 ; :: thesis: ( not s . a = 0 or not s . f0 = 0 or not s . f1 = 1 or not s . (intpos i) = n or ex t being State of SCMPDS ex k being Element of NAT st
( n = (t . (intpos i)) + k & t . f0 = Fib k & t . f1 = Fib (k + 1) & t . a = 0 & t . (intpos i) > 0 & not ( (IExec I,t) . a = 0 & I is_closed_on t & I is_halting_on t & (IExec I,t) . (intpos i) = (t . (intpos i)) - 1 & (IExec I,t) . f0 = Fib (k + 1) & (IExec I,t) . f1 = Fib ((k + 1) + 1) ) ) or ( (IExec (while>0 a,i,I),s) . f0 = Fib n & (IExec (while>0 a,i,I),s) . f1 = Fib (n + 1) & while>0 a,i,I is_closed_on s & while>0 a,i,I is_halting_on s ) )
set Iw = IExec (while>0 a,i,I),s;
set Dw = Dstate (IExec (while>0 a,i,I),s);
set da = DataLoc (s . a),i;
defpred S₁[ State of SCMPDS ] means ( $1 . (intpos i) >= 0 & ex k being Element of NAT st
( n = ($1 . (intpos i)) + k & $1 . f0 = Fib k & $1 . f1 = Fib (k + 1) ) );
assume that
A2: s . a = 0 and
A3: s . f0 = 0 and
A4: s . f1 = 1 and
A5: s . (intpos i) = n ; :: thesis: ( ex t being State of SCMPDS ex k being Element of NAT st
( n = (t . (intpos i)) + k & t . f0 = Fib k & t . f1 = Fib (k + 1) & t . a = 0 & t . (intpos i) > 0 & not ( (IExec I,t) . a = 0 & I is_closed_on t & I is_halting_on t & (IExec I,t) . (intpos i) = (t . (intpos i)) - 1 & (IExec I,t) . f0 = Fib (k + 1) & (IExec I,t) . f1 = Fib ((k + 1) + 1) ) ) or ( (IExec (while>0 a,i,I),s) . f0 = Fib n & (IExec (while>0 a,i,I),s) . f1 = Fib (n + 1) & while>0 a,i,I is_closed_on s & while>0 a,i,I is_halting_on s ) )
consider ff being Function of (product the Object-Kind of SCMPDS ),NAT such that
A6: for t being State of SCMPDS holds
( ( t . (DataLoc (s . a),i) <= 0 implies ff . t = 0 ) & ( t . (DataLoc (s . a),i) > 0 implies ff . t = t . (DataLoc (s . a),i) ) ) by SCMPDS_8:5;
deffunc H₁( State of SCMPDS ) -> Element of NAT = ff . $1;

A7: now

let t be State of SCMPDS ; :: thesis: ( S₁[ Dstate t] implies ( ( H₁( Dstate t) = 0 implies not t . (DataLoc (s . a),i) > 0 ) & ( t . (DataLoc (s . a),i) <= 0 implies H₁( Dstate t) = 0 ) ) )
set dt = Dstate t;
assume S₁[ Dstate t] ; :: thesis: ( ( H₁( Dstate t) = 0 implies not t . (DataLoc (s . a),i) > 0 ) & ( t . (DataLoc (s . a),i) <= 0 implies H₁( Dstate t) = 0 ) )

hereby :: thesis: ( t . (DataLoc (s . a),i) <= 0 implies H₁( Dstate t) = 0 )

assume A8: H₁( Dstate t) = 0 ; :: thesis: not 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 A6, A8; :: thesis: verum

end;

assume t . (DataLoc (s . a),i) <= 0 ; :: thesis: H₁( Dstate t) = 0
then (Dstate t) . (DataLoc (s . a),i) <= 0 by SCMPDS_8:4;
hence H₁( Dstate t) = 0 by A6; :: thesis: verum

end;

assume A9: for t being State of SCMPDS
for k being Element of NAT st n = (t . (intpos i)) + k & t . f0 = Fib k & t . f1 = Fib (k + 1) & t . a = 0 & t . (intpos i) > 0 holds
( (IExec I,t) . a = 0 & I is_closed_on t & I is_halting_on t & (IExec I,t) . (intpos i) = (t . (intpos i)) - 1 & (IExec I,t) . f0 = Fib (k + 1) & (IExec I,t) . f1 = Fib ((k + 1) + 1) ) ; :: thesis: ( (IExec (while>0 a,i,I),s) . f0 = Fib n & (IExec (while>0 a,i,I),s) . f1 = Fib (n + 1) & while>0 a,i,I is_closed_on s & while>0 a,i,I is_halting_on s )

A10: now

let t be State of SCMPDS ; :: thesis: ( S₁[ 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 & H₁( Dstate (IExec I,t)) < H₁( Dstate t) & S₁[ Dstate (IExec I,t)] ) )
set Dt = Dstate t;
assume that
A11: S₁[ Dstate t] and
A12: t . a = s . a and
A13: t . (DataLoc (s . a),i) > 0 ; :: thesis: ( (IExec I,t) . a = t . a & I is_closed_on t & I is_halting_on t & H₁( Dstate (IExec I,t)) < H₁( Dstate t) & S₁[ Dstate (IExec I,t)] )
set It = IExec I,t;
set Dit = Dstate (IExec I,t);
consider k being Element of NAT such that
A14: n = ((Dstate t) . (intpos i)) + k and
A15: (Dstate t) . f0 = Fib k and
A16: (Dstate t) . f1 = Fib (k + 1) by A11;
A17: t . f1 = Fib (k + 1) by A16, SCMPDS_8:4;
A18: intpos (0 + i) = DataLoc (s . a),i by A2, SCMP_GCD:5;
A19: ( n = (t . (intpos i)) + k & t . f0 = Fib k ) by A14, A15, SCMPDS_8:4;
hence (IExec I,t) . a = t . a by A2, A9, A12, A13, A17, A18; :: thesis: ( I is_closed_on t & I is_halting_on t & H₁( Dstate (IExec I,t)) < H₁( Dstate t) & S₁[ Dstate (IExec I,t)] )
thus ( I is_closed_on t & I is_halting_on t ) by A2, A9, A12, A13, A19, A17, A18; :: thesis: ( H₁( Dstate (IExec I,t)) < H₁( Dstate t) & S₁[ Dstate (IExec I,t)] )
A20: (IExec I,t) . (intpos i) = (t . (intpos i)) - 1 by A2, A9, A12, A13, A19, A17, A18;

hereby :: thesis: S₁[ Dstate (IExec I,t)]

per cases ( (IExec I,t) . (intpos i) <= 0 or (IExec I,t) . (intpos i) > 0 ) ;

suppose (IExec I,t) . (intpos i) <= 0 ; :: thesis: H₁( Dstate (IExec I,t)) < H₁( Dstate t)

then (Dstate (IExec I,t)) . (DataLoc (s . a),i) <= 0 by A18, SCMPDS_8:4;
then A21: H₁( Dstate (IExec I,t)) = 0 by A6;
H₁( Dstate t) <> 0 by A7, A11, A13;
hence H₁( Dstate (IExec I,t)) < H₁( Dstate t) by A21, NAT_1:3; :: thesis: verum

end;

suppose A22: (IExec I,t) . (intpos i) > 0 ; :: thesis: H₁( Dstate (IExec I,t)) < H₁( Dstate t)

(Dstate t) . (DataLoc (s . a),i) > 0 by A13, SCMPDS_8:4;
then A23: H₁( Dstate t) = (Dstate t) . (DataLoc (s . a),i) by A6
.= t . (intpos i) by A18, SCMPDS_8:4 ;
(Dstate (IExec I,t)) . (DataLoc (s . a),i) > 0 by A18, A22, SCMPDS_8:4;
then H₁( Dstate (IExec I,t)) = (Dstate (IExec I,t)) . (DataLoc (s . a),i) by A6
.= (t . (intpos i)) - 1 by A18, A20, SCMPDS_8:4 ;
hence H₁( Dstate (IExec I,t)) < H₁( Dstate t) by A23, XREAL_1:148; :: thesis: verum

end;

end;

end;

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

proof

t . (intpos i) >= 1 + 0 by A13, A18, INT_1:20;
then (t . (intpos i)) - 1 >= 0 by XREAL_1:50;
hence (Dstate (IExec I,t)) . (intpos i) >= 0 by A20, SCMPDS_8:4; :: thesis: ex k being Element of NAT st
( n = ((Dstate (IExec I,t)) . (intpos i)) + k & (Dstate (IExec I,t)) . f0 = Fib k & (Dstate (IExec I,t)) . f1 = Fib (k + 1) )
take m = k + 1; :: thesis: ( n = ((Dstate (IExec I,t)) . (intpos i)) + m & (Dstate (IExec I,t)) . f0 = Fib m & (Dstate (IExec I,t)) . f1 = Fib (m + 1) )
thus n = (((t . (intpos i)) - 1) + 1) + k by A14, SCMPDS_8:4
.= (((Dstate (IExec I,t)) . (intpos i)) + 1) + k by A20, SCMPDS_8:4
.= ((Dstate (IExec I,t)) . (intpos i)) + m ; :: thesis: ( (Dstate (IExec I,t)) . f0 = Fib m & (Dstate (IExec I,t)) . f1 = Fib (m + 1) )
( (IExec I,t) . f0 = Fib m & (IExec I,t) . f1 = Fib ((k + 1) + 1) ) by A2, A9, A12, A13, A19, A17, A18;
hence ( (Dstate (IExec I,t)) . f0 = Fib m & (Dstate (IExec I,t)) . f1 = Fib (m + 1) ) by SCMPDS_8:4; :: thesis: verum

end;

end;

A24: S₁[ Dstate s]

proof

set Ds = Dstate s;
(Dstate s) . (intpos i) = n by A5, SCMPDS_8:4;
hence (Dstate s) . (intpos i) >= 0 by NAT_1:2; :: thesis: ex k being Element of NAT st
( n = ((Dstate s) . (intpos i)) + k & (Dstate s) . f0 = Fib k & (Dstate s) . f1 = Fib (k + 1) )
take k = 0 ; :: thesis: ( n = ((Dstate s) . (intpos i)) + k & (Dstate s) . f0 = Fib k & (Dstate s) . f1 = Fib (k + 1) )
thus n = ((Dstate s) . (intpos i)) + k by A5, SCMPDS_8:4; :: thesis: ( (Dstate s) . f0 = Fib k & (Dstate s) . f1 = Fib (k + 1) )
thus (Dstate s) . f0 = Fib k by A3, PRE_FF:1, SCMPDS_8:4; :: thesis: (Dstate s) . f1 = Fib (k + 1)
thus (Dstate s) . f1 = Fib (k + 1) by A4, PRE_FF:1, SCMPDS_8:4; :: thesis: verum

end;

A25: ( H₁( Dstate (IExec (while>0 a,i,I),s)) = 0 & S₁[ Dstate (IExec (while>0 a,i,I),s)] ) from SCPINVAR:sch 2(A1, A7, A24, A10);
(Dstate (IExec (while>0 a,i,I),s)) . (intpos i) = (IExec (while>0 a,i,I),s) . (intpos (0 + i)) by SCMPDS_8:4
.= (IExec (while>0 a,i,I),s) . (DataLoc (s . a),i) by A2, SCMP_GCD:5 ;
then (Dstate (IExec (while>0 a,i,I),s)) . (intpos i) <= 0 by A7, A25;
then (Dstate (IExec (while>0 a,i,I),s)) . (intpos i) = 0 by A25, XXREAL_0:1;
hence ( (IExec (while>0 a,i,I),s) . f0 = Fib n & (IExec (while>0 a,i,I),s) . f1 = Fib (n + 1) ) by A25, SCMPDS_8:4; :: thesis: ( while>0 a,i,I is_closed_on s & while>0 a,i,I is_halting_on s )
A26: for t being State of SCMPDS st S₁[ Dstate t] & H₁( Dstate t) = 0 holds
t . (DataLoc (s . a),i) <= 0 by A7;
( ( H₁(s) = H₁(s) or S₁[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, A26, A24, A10);
hence ( while>0 a,i,I is_closed_on s & while>0 a,i,I is_halting_on s ) ; :: thesis: verum