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
A2: s . a = 0 and
A3: s . f0 = 0 and
A4: s . f1 = 1 and
A5: s . (intpos i) = n ; :: thesis:
consider ff being Function of (product the Object-Kind of SCMPDS),NAT such that
B6: 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 B6;
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 A9: 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:

A10: now

let t be 0 -started State of SCMPDS; :: thesis:
let Q be Instruction-Sequence of SCMPDS; :: thesis:
assume that
A11: S₁[t] and
A12: t . a = s . a and
A13: 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
A14: n = (t . (intpos i)) + k and
A15: t . f0 = Fib k and
A16: t . f1 = Fib (k + 1) by A11;
A17: t . f1 = Fib (k + 1) by A16;
A18: intpos (0 + i) = DataLoc ((s . a),i) by A2, SCMP_GCD:1;
A19: ( n = (t . (intpos i)) + k & t . f0 = Fib k ) by A14, A15;
hence (IExec (I,Q,t)) . a = t . a by A2, A9, A12, A13, A17, A18; :: thesis:
thus ( I is_closed_on t,Q & I is_halting_on t,Q ) by A2, A9, A12, A13, A19, A17, A18; :: thesis:
A20: (IExec (I,Q,t)) . (intpos i) = (t . (intpos i)) - 1 by A2, A9, A12, A13, A19, A17, A18;

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 A18, SCMPDS_5:15;
then A21: H₁( Initialize (IExec (I,Q,t))) = 0 by A6;
H₁(t) <> 0 by A7, A11, A13;
hence H₁( Initialize (IExec (I,Q,t))) < H₁(t) by A21, NAT_1:3; :: thesis:

end;

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

t . (DataLoc ((s . a),i)) > 0 by A13;
then A23: H₁(t) = t . (DataLoc ((s . a),i)) by A6
.= t . (intpos i) by A18 ;
(Initialize (IExec (I,Q,t))) . (DataLoc ((s . a),i)) > 0 by A18, A22, 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 A18, A20, SCMPDS_5:15 ;
hence H₁( Initialize (IExec (I,Q,t))) < H₁(t) by A23, XREAL_1:146; :: thesis:

end;

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

proof

t . (intpos i) >= 1 + 0 by A13, A18, INT_1:7;
then (t . (intpos i)) - 1 >= 0 by XREAL_1:48;
hence (Initialize (IExec (I,Q,t))) . (intpos i) >= 0 by A20, SCMPDS_5:15; :: thesis:
take m = k + 1; :: thesis:
thus n = (((t . (intpos i)) - 1) + 1) + k by A14
.= (((Initialize (IExec (I,Q,t))) . (intpos i)) + 1) + k by A20, 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 A2, A9, A12, A13, A19, A17, A18;
hence ( (Initialize (IExec (I,Q,t))) . f0 = Fib m & (Initialize (IExec (I,Q,t))) . f1 = Fib (m + 1) ) by SCMPDS_5:15; :: thesis:

end;

A24: S₁[s]

proof

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

end;

A25: ( 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, A24, A10);
X1: (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 A2, SCMP_GCD:1 ;
then (Initialize (IExec ((while>0 (a,i,I)),P,s))) . (intpos i) <= 0 by A7, A25, X1;
then (Initialize (IExec ((while>0 (a,i,I)),P,s))) . (intpos i) = 0 by A25, XXREAL_0:1;
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 A25, 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, A24, A10);
hence ( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P ) ; :: thesis: