let P be Instruction-Sequence of SCMPDS; :: thesis:
let s be 0 -started State of SCMPDS; :: thesis:
let I be halt-free shiftable Program of SCMPDS; :: thesis:
let a, f0, f1 be Int_position; :: thesis:
let n, i be Element of NAT ; :: thesis:
set Iw = IExec ((while>0 (a,i,I)),P,s);
set Dw = Initialize (IExec ((while>0 (a,i,I)),P,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
A1: s . a = 0 and
A2: s . f0 = 0 and
A3: s . f1 = 1 and
A4: s . (intpos i) = n ; :: thesis:
consider ff being Function of (product (the_Values_of SCMPDS)),NAT such that
A5: 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;
A6: for t being 0 -started 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 A5;
deffunc H₁( State of SCMPDS) -> Element of NAT = ff . $1;
A7: for t being 0 -started State of SCMPDS st S₁[t] holds
( ( not H₁(t) = 0 or not t . (DataLoc ((s . a),i)) > 0 ) & ( t . (DataLoc ((s . a),i)) <= 0 implies H₁(t) = 0 ) ) by A6;
assume A8: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence 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,Q,t)) . a = 0 & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (intpos i) = (t . (intpos i)) - 1 & (IExec (I,Q,t)) . f0 = Fib (k + 1) & (IExec (I,Q,t)) . f1 = Fib ((k + 1) + 1) ) ; :: thesis:

A9: now :: thesis:

let t be 0 -started State of SCMPDS; :: thesis:
let Q be Instruction-Sequence of SCMPDS; :: thesis:
assume that
A10: S₁[t] and
A11: t . a = s . a and
A12: t . (DataLoc ((s . a),i)) > 0 ; :: thesis:
set It = IExec (I,Q,t);
set Dit = Initialize (IExec (I,Q,t));
consider k being Element of NAT such that
A13: n = (t . (intpos i)) + k and
A14: t . f0 = Fib k and
A15: t . f1 = Fib (k + 1) by A10;
A16: t . f1 = Fib (k + 1) by A15;
A17: intpos (0 + i) = DataLoc ((s . a),i) by A1, SCMP_GCD:1;
A18: ( n = (t . (intpos i)) + k & t . f0 = Fib k ) by A13, A14;
hence (IExec (I,Q,t)) . a = t . a by A1, A8, A11, A12, A16, A17; :: thesis:
thus ( I is_closed_on t,Q & I is_halting_on t,Q ) by A1, A8, A11, A12, A18, A16, A17; :: thesis:
A19: (IExec (I,Q,t)) . (intpos i) = (t . (intpos i)) - 1 by A1, A8, A11, A12, A18, A16, A17;

hereby :: thesis:

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

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

then (Initialize (IExec (I,Q,t))) . (DataLoc ((s . a),i)) <= 0 by A17, SCMPDS_5:15;
then A20: H₁( Initialize (IExec (I,Q,t))) = 0 by A6;
H₁(t) <> 0 by A7, A10, A12;
hence H₁( Initialize (IExec (I,Q,t))) < H₁(t) by A20; :: thesis:

end;

suppose A21: (IExec (I,Q,t)) . (intpos i) > 0 ; :: thesis:

t . (DataLoc ((s . a),i)) > 0 by A12;
then A22: H₁(t) = t . (DataLoc ((s . a),i)) by A6
.= t . (intpos i) by A17 ;
(Initialize (IExec (I,Q,t))) . (DataLoc ((s . a),i)) > 0 by A17, A21, SCMPDS_5:15;
then H₁( Initialize (IExec (I,Q,t))) = (Initialize (IExec (I,Q,t))) . (DataLoc ((s . a),i)) by A6
.= (t . (intpos i)) - 1 by A17, A19, SCMPDS_5:15 ;
hence H₁( Initialize (IExec (I,Q,t))) < H₁(t) by A22, XREAL_1:146; :: thesis:

end;

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

proof

t . (intpos i) >= 1 + 0 by A12, A17, INT_1:7;
then (t . (intpos i)) - 1 >= 0 by XREAL_1:48;
hence (Initialize (IExec (I,Q,t))) . (intpos i) >= 0 by A19, SCMPDS_5:15; :: thesis:
take m = k + 1; :: thesis:
thus n = (((t . (intpos i)) - 1) + 1) + k by A13
.= (((Initialize (IExec (I,Q,t))) . (intpos i)) + 1) + k by A19, SCMPDS_5:15
.= ((Initialize (IExec (I,Q,t))) . (intpos i)) + m ; :: thesis:
( (IExec (I,Q,t)) . f0 = Fib m & (IExec (I,Q,t)) . f1 = Fib ((k + 1) + 1) ) by A1, A8, A11, A12, A18, A16, A17;
hence ( (Initialize (IExec (I,Q,t))) . f0 = Fib m & (Initialize (IExec (I,Q,t))) . f1 = Fib (m + 1) ) by SCMPDS_5:15; :: thesis:

end;

A23: S₁[s]

proof

s . (intpos i) = n by A4;
hence s . (intpos i) >= 0 ; :: thesis:
take k = 0 ; :: thesis:
thus n = (s . (intpos i)) + k by A4; :: thesis:
thus s . f0 = Fib k by A2, PRE_FF:1; :: thesis:
thus s . f1 = Fib (k + 1) by A3, PRE_FF:1; :: thesis:

end;

A24: ( H₁( Initialize (IExec ((while>0 (a,i,I)),P,s))) = 0 & S₁[ Initialize (IExec ((while>0 (a,i,I)),P,s))] ) from SCPINVAR:sch 2(A7, A23, A9);
A25: (Initialize (IExec ((while>0 (a,i,I)),P,s))) . (DataLoc ((s . a),i)) = (IExec ((while>0 (a,i,I)),P,s)) . (DataLoc ((s . a),i)) by SCMPDS_5:15;
(Initialize (IExec ((while>0 (a,i,I)),P,s))) . (intpos i) = (IExec ((while>0 (a,i,I)),P,s)) . (intpos (0 + i)) by SCMPDS_5:15
.= (IExec ((while>0 (a,i,I)),P,s)) . (DataLoc ((s . a),i)) by A1, SCMP_GCD:1 ;
then (Initialize (IExec ((while>0 (a,i,I)),P,s))) . (intpos i) <= 0 by A7, A24, A25;
then (Initialize (IExec ((while>0 (a,i,I)),P,s))) . (intpos i) = 0 by A24;
hence ( (IExec ((while>0 (a,i,I)),P,s)) . f0 = Fib n & (IExec ((while>0 (a,i,I)),P,s)) . f1 = Fib (n + 1) ) by A24, SCMPDS_5:15; :: thesis:
A26: for t being 0 -started State of SCMPDS st S₁[t] & H₁(t) = 0 holds
t . (DataLoc ((s . a),i)) <= 0 by A7;
( 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(A26, A23, A9);
hence ( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P ) ; :: thesis: