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, b, c be Int_position; :: thesis:
let i, d be Integer; :: thesis:
set ci = DataLoc ((s . a),i);
consider f being Function of (product (the_Values_of SCMPDS)),NAT such that
A1: for s being State of SCMPDS holds
( ( s . b = s . c implies f . s = 0 ) & ( s . b <> s . c implies f . s = max (|.(s . b).|,|.(s . c).|) ) ) by Th2;
deffunc H₁( State of SCMPDS) -> Element of NAT = f . $1;
set s1 = IExec ((while<>0 (a,i,I)),P,s);
set ss = IExec ((while<>0 (a,i,I)),P,s);
defpred S₁[ set ] means ex t being 0 -started State of SCMPDS st
( t = $1 & t . b > 0 & t . c > 0 & (t . b) gcd (t . c) = (s . b) gcd (s . c) & t . (DataLoc (d,i)) = (t . b) - (t . c) );
assume that
A2: s . a = d and
A3: s . b > 0 and
A4: s . c > 0 and
A5: s . (DataLoc (d,i)) = (s . b) - (s . c) ; :: thesis:
assume A6: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . b > 0 & t . c > 0 & t . a = d & t . (DataLoc (d,i)) = (t . b) - (t . c) & t . b <> t . c holds
( (IExec (I,Q,t)) . a = d & I is_closed_on t,Q & I is_halting_on t,Q & ( t . b > t . c implies ( (IExec (I,Q,t)) . b = (t . b) - (t . c) & (IExec (I,Q,t)) . c = t . c ) ) & ( t . b <= t . c implies ( (IExec (I,Q,t)) . c = (t . c) - (t . b) & (IExec (I,Q,t)) . b = t . b ) ) & (IExec (I,Q,t)) . (DataLoc (d,i)) = ((IExec (I,Q,t)) . b) - ((IExec (I,Q,t)) . c) ) ; :: thesis:

A7: now :: thesis:

let t be 0 -started State of SCMPDS; :: thesis:
let Q be Instruction-Sequence of SCMPDS; :: thesis:
assume that
A8: S₁[t] and
A9: t . a = s . a and
A10: t . (DataLoc ((s . a),i)) <> 0 ; :: thesis:
set It = IExec (I,Q,t);
set t2 = Initialize (IExec (I,Q,t));
set t1 = t;
set x = (IExec (I,Q,t)) . b;
set y = (IExec (I,Q,t)) . c;
consider v being State of SCMPDS such that
A11: v = t and
A12: v . b > 0 and
A13: v . c > 0 and
A14: (v . b) gcd (v . c) = (s . b) gcd (s . c) and
A15: v . (DataLoc (d,i)) = (v . b) - (v . c) by A8;
A16: t . b > 0 by A11, A12;
A17: t . c > 0 by A11, A13;
A18: t . (DataLoc (d,i)) = (v . b) - (v . c) by A11, A15
.= (t . b) - (v . c) by A11
.= (t . b) - (t . c) by A11 ;
then A19: ( t . b > t . c implies ( (IExec (I,Q,t)) . b = (t . b) - (t . c) & (IExec (I,Q,t)) . c = t . c ) ) by A2, A6, A9, A17;
A20: t . b <> t . c by A2, A10, A18;
hence (IExec (I,Q,t)) . a = t . a by A2, A6, A9, A16, A17, A18; :: thesis:
thus ( I is_closed_on t,Q & I is_halting_on t,Q ) by A2, A6, A9, A16, A17, A18, A20; :: thesis:
A21: ( t . b <= t . c implies ( (IExec (I,Q,t)) . c = (t . c) - (t . b) & (IExec (I,Q,t)) . b = t . b ) ) by A2, A6, A9, A16, A18, A20;

A22: now :: thesis:

per cases ;

suppose A23: t . b > t . c ; :: thesis:

then (t . b) - (t . c) > 0 by XREAL_1:50;
hence (IExec (I,Q,t)) . b > 0 by A2, A6, A9, A17, A18, A23; :: thesis:
thus (IExec (I,Q,t)) . c > 0 by A2, A6, A9, A17, A18, A23; :: thesis:
thus ((IExec (I,Q,t)) . b) gcd ((IExec (I,Q,t)) . c) = (t . b) gcd (t . c) by A16, A17, A19, A21, PREPOWER:97; :: thesis:
A24: (IExec (I,Q,t)) . b = (t . b) - (t . c) by A2, A6, A9, A17, A18, A23;

hereby :: thesis:

A25: max ((t . b),(t . c)) = t . b by A23, XXREAL_0:def 10;

per cases by XXREAL_0:16;

suppose max (((IExec (I,Q,t)) . b),((IExec (I,Q,t)) . c)) = (IExec (I,Q,t)) . b ; :: thesis:

hence max (((IExec (I,Q,t)) . b),((IExec (I,Q,t)) . c)) < max ((t . b),(t . c)) by A17, A24, A25, XREAL_1:44; :: thesis:

end;

suppose max (((IExec (I,Q,t)) . b),((IExec (I,Q,t)) . c)) = (IExec (I,Q,t)) . c ; :: thesis:

hence max (((IExec (I,Q,t)) . b),((IExec (I,Q,t)) . c)) < max ((t . b),(t . c)) by A2, A6, A9, A17, A18, A23, A25; :: thesis:

end;

suppose A26: t . b <= t . c ; :: thesis:

hence (IExec (I,Q,t)) . b > 0 by A2, A6, A9, A16, A18, A20; :: thesis:
t . b < t . c by A20, A26, XXREAL_0:1;
then (t . c) - (t . b) > 0 by XREAL_1:50;
hence (IExec (I,Q,t)) . c > 0 by A2, A6, A9, A16, A18, A20, A26; :: thesis:
thus ((IExec (I,Q,t)) . b) gcd ((IExec (I,Q,t)) . c) = (t . b) gcd (t . c) by A16, A17, A19, A21, PREPOWER:97; :: thesis:
A27: (IExec (I,Q,t)) . c = (t . c) - (t . b) by A2, A6, A9, A16, A18, A20, A26;
A28: (IExec (I,Q,t)) . b = t . b by A2, A6, A9, A16, A18, A20, A26;

hereby :: thesis:

A29: max ((t . b),(t . c)) = t . c by A26, XXREAL_0:def 10;

per cases by XXREAL_0:16;

suppose max (((IExec (I,Q,t)) . b),((IExec (I,Q,t)) . c)) = (IExec (I,Q,t)) . c ; :: thesis:

hence max (((IExec (I,Q,t)) . b),((IExec (I,Q,t)) . c)) < max ((t . b),(t . c)) by A16, A27, A29, XREAL_1:44; :: thesis:

end;

suppose max (((IExec (I,Q,t)) . b),((IExec (I,Q,t)) . c)) = (IExec (I,Q,t)) . b ; :: thesis:

hence max (((IExec (I,Q,t)) . b),((IExec (I,Q,t)) . c)) < max ((t . b),(t . c)) by A20, A26, A28, A29, XXREAL_0:1; :: thesis:

end;

thus H₁( Initialize (IExec (I,Q,t))) < H₁(t) :: thesis:

proof

t . b <> t . c by A20;
then t . b <> t . c ;
then A30: H₁(t) = max (|.(t . b).|,|.(t . c).|) by A1
.= max (|.(t . b).|,|.(t . c).|)
.= max (|.(t . b).|,|.(t . c).|)
.= max ((t . b),|.(t . c).|) by A16, ABSVALUE:def 1
.= max ((t . b),(t . c)) by A17, ABSVALUE:def 1 ;
then H₁(t) >= t . b by XXREAL_0:25;
then A31: H₁(t) > 0 by A16;

per cases ) . b = (Initialize (IExec (I,Q,t))) . c or (Initialize (IExec (I,Q,t))) . b <> (Initialize (IExec (I,Q,t))) . c ) ;

suppose (Initialize (IExec (I,Q,t))) . b = (Initialize (IExec (I,Q,t))) . c ; :: thesis:

hence H₁( Initialize (IExec (I,Q,t))) < H₁(t) by A1, A31; :: thesis:

end;

suppose (Initialize (IExec (I,Q,t))) . b <> (Initialize (IExec (I,Q,t))) . c ; :: thesis:

end;

A32: (IExec (I,Q,t)) . (DataLoc (d,i)) = ((IExec (I,Q,t)) . b) - ((IExec (I,Q,t)) . c) by A2, A6, A9, A16, A17, A18, A20;
thus S₁[ Initialize (IExec (I,Q,t))] :: thesis:

proof

take u = Initialize (IExec (I,Q,t)); :: thesis:
thus u = Initialize (IExec (I,Q,t)) ; :: thesis:
thus ( u . b > 0 & u . c > 0 ) by A22, SCMPDS_5:15; :: thesis:
thus (u . b) gcd (u . c) = ((IExec (I,Q,t)) . b) gcd (u . c) by SCMPDS_5:15
.= (t . b) gcd (t . c) by A22, SCMPDS_5:15
.= (v . b) gcd (t . c) by A11
.= (s . b) gcd (s . c) by A11, A14 ; :: thesis:
thus u . (DataLoc (d,i)) = ((IExec (I,Q,t)) . b) - ((IExec (I,Q,t)) . c) by A32, SCMPDS_5:15
.= (u . b) - ((IExec (I,Q,t)) . c) by SCMPDS_5:15
.= (u . b) - (u . c) by SCMPDS_5:15 ; :: thesis:

end;

A33: for t being 0 -started State of SCMPDS st S₁[t] holds
( H₁(t) = 0 iff t . (DataLoc ((s . a),i)) = 0 )

proof

let t be 0 -started State of SCMPDS; :: thesis:
assume S₁[t] ; :: thesis:
then consider v being State of SCMPDS such that
A34: v = t and
A35: v . b > 0 and
v . c > 0 and
(v . b) gcd (v . c) = (s . b) gcd (s . c) and
A36: v . (DataLoc (d,i)) = (v . b) - (v . c) ;
A37: t . (DataLoc ((s . a),i)) = (v . b) - (v . c) by A2, A34, A36
.= (t . b) - (v . c) by A34
.= (t . b) - (t . c) by A34 ;

hereby :: thesis:

assume A38: H₁(t) = 0 ; :: thesis:

now :: thesis:

assume t . b <> t . c ; :: thesis:
then t . b <> t . c ;
then t . b <> t . c ;
then A39: H₁(t) = max (|.(t . b).|,|.(t . c).|) by A1
.= max (|.(t . b).|,|.(t . c).|)
.= max (|.(t . b).|,|.(t . c).|) ;
t . b > 0 by A34, A35;
then |.(t . b).| > 0 by COMPLEX1:47;
hence contradiction by A38, A39, XXREAL_0:25; :: thesis:

end;

hence t . (DataLoc ((s . a),i)) = 0 by A37; :: thesis:

end;

thus ( t . (DataLoc ((s . a),i)) = 0 implies H₁(t) = 0 ) by A1, A37; :: thesis:

end;

A40: S₁[s] by A3, A4, A5;
A41: ( H₁( Initialize (IExec ((while<>0 (a,i,I)),P,s))) = 0 & S₁[ Initialize (IExec ((while<>0 (a,i,I)),P,s))] ) from SCPINVAR:sch 5(A33, A40, A7);
then consider w being 0 -started State of SCMPDS such that
A42: w = Initialize (IExec ((while<>0 (a,i,I)),P,s)) and
A43: w . b > 0 and
w . c > 0 and
A44: (w . b) gcd (w . c) = (s . b) gcd (s . c) and
A45: w . (DataLoc (d,i)) = (w . b) - (w . c) ;
A46: (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;
A47: (Initialize (IExec ((while<>0 (a,i,I)),P,s))) . b = (IExec ((while<>0 (a,i,I)),P,s)) . b by SCMPDS_5:15;
A48: (Initialize (IExec ((while<>0 (a,i,I)),P,s))) . c = (IExec ((while<>0 (a,i,I)),P,s)) . c by SCMPDS_5:15;
A49: (w . b) - (w . c) = (IExec ((while<>0 (a,i,I)),P,s)) . (DataLoc ((s . a),i)) by A2, A42, A45, SCMPDS_5:15
.= 0 by A33, A41, A46 ;
then A50: |.(w . b).| = |.(w . b).| gcd |.(w . c).| by NAT_D:32
.= (s . b) gcd (s . c) by A44, INT_2:34 ;
thus (IExec ((while<>0 (a,i,I)),P,s)) . b = (IExec ((while<>0 (a,i,I)),P,s)) . b
.= (s . b) gcd (s . c) by A42, A43, A50, A47, ABSVALUE:def 1 ; :: thesis:
thus (IExec ((while<>0 (a,i,I)),P,s)) . c = (IExec ((while<>0 (a,i,I)),P,s)) . c
.= (s . b) gcd (s . c) by A42, A43, A49, A50, A48, ABSVALUE:def 1 ; :: thesis: