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