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);
assume card I > 0 ; :: thesis:
consider f being Function of (product the Object-Kind of SCMPDS),NAT such that
A2: for s being State of SCMPDS holds
( ( s . b = s . c implies f . s = 0 ) & ( s . b <> s . c implies f . s = max ((abs (s . b)),(abs (s . c))) ) ) by Th6;
deffunc H₁( State of SCMPDS) -> Element of NAT = f . $1;
defpred S₁[ set ] means ex t being State of SCMPDS st
( t = $1 & t . b > 0 & t . c > 0 & t . (DataLoc (d,i)) = (t . b) - (t . c) );
assume that
A3: s . a = d and
A4: s . b > 0 and
A5: s . c > 0 and
A6: s . (DataLoc (d,i)) = (s . b) - (s . c) ; :: thesis:
assume A7: 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:

A8: now

let t be 0 -started State of SCMPDS; :: thesis:
let Q be Instruction-Sequence of SCMPDS; :: thesis:
assume that
A9: S₁[t] and
A10: t . a = s . a and
A11: 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
A12: v = t and
A13: v . b > 0 and
A14: v . c > 0 and
A15: v . (DataLoc (d,i)) = (v . b) - (v . c) by A9;
A16: t . b > 0 by A12, A13;
A17: t . c > 0 by A12, A14;
A18: t . (DataLoc (d,i)) = (v . b) - (v . c) by A12, A15
.= (t . b) - (v . c) by A12
.= (t . b) - (t . c) by A12 ;
then A19: t . b <> t . c by A3, A11;
hence (IExec (I,Q,t)) . a = t . a by A3, A7, A10, A16, A17, A18; :: thesis:
thus ( I is_closed_on t,Q & I is_halting_on t,Q ) by A3, A7, A10, A16, A17, A18, A19; :: thesis:

A20: now

per cases ;

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

then (t . b) - (t . c) > 0 by XREAL_1:50;
hence (IExec (I,Q,t)) . b > 0 by A3, A7, A10, A16, A17, A18, A21; :: thesis:
thus (IExec (I,Q,t)) . c > 0 by A3, A7, A10, A16, A17, A18, A21; :: thesis:
A22: (IExec (I,Q,t)) . b = (t . b) - (t . c) by A3, A7, A10, A16, A17, A18, A21;

hereby :: thesis:

A23: max ((t . b),(t . c)) = t . b by A21, 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, A22, A23, 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 A3, A7, A10, A16, A17, A18, A21, A23; :: thesis:

end;

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

hence (IExec (I,Q,t)) . b > 0 by A3, A7, A10, A16, A17, A18, A19; :: thesis:
t . b < t . c by A19, A24, XXREAL_0:1;
then (t . c) - (t . b) > 0 by XREAL_1:50;
hence (IExec (I,Q,t)) . c > 0 by A3, A7, A10, A16, A17, A18, A19, A24; :: thesis:
A25: (IExec (I,Q,t)) . c = (t . c) - (t . b) by A3, A7, A10, A16, A17, A18, A19, A24;
A26: (IExec (I,Q,t)) . b = t . b by A3, A7, A10, A16, A17, A18, A19, A24;

hereby :: thesis:

A27: max ((t . b),(t . c)) = t . c by A24, 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, A25, A27, 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 A19, A24, A26, A27, XXREAL_0:1; :: thesis:

end;

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

proof

t . b <> t . c by A19;
then t . b <> t . c ;
then A28: H₁(t) = max ((abs (t . b)),(abs (t . c))) by A2
.= max ((abs (t . b)),(abs (t . c)))
.= max ((abs (t . b)),(abs (t . c)))
.= max ((t . b),(abs (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 A29: H₁(t) > 0 by A16, XXREAL_0:2;

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 A2, A29; :: thesis:

end;

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

then H₁( Initialize (IExec (I,Q,t))) = max ((abs ((Initialize (IExec (I,Q,t))) . b)),(abs ((Initialize (IExec (I,Q,t))) . c))) by A2
.= max ((abs ((IExec (I,Q,t)) . b)),(abs ((Initialize (IExec (I,Q,t))) . c))) by SCMPDS_5:15
.= max ((abs ((IExec (I,Q,t)) . b)),(abs ((IExec (I,Q,t)) . c))) by SCMPDS_5:15
.= max (((IExec (I,Q,t)) . b),(abs ((IExec (I,Q,t)) . c))) by A20, ABSVALUE:def 1
.= max (((IExec (I,Q,t)) . b),((IExec (I,Q,t)) . c)) by A20, ABSVALUE:def 1 ;
hence H₁( Initialize (IExec (I,Q,t))) < H₁(t) by A20, A28; :: thesis:

end;

A30: (IExec (I,Q,t)) . (DataLoc (d,i)) = ((IExec (I,Q,t)) . b) - ((IExec (I,Q,t)) . c) by A3, A7, A10, A16, A17, A18, A19;
thus S₁[ Initialize (IExec (I,Q,t))] :: thesis:

proof

take v = Initialize (IExec (I,Q,t)); :: thesis:
thus v = Initialize (IExec (I,Q,t)) ; :: thesis:
thus ( v . b > 0 & v . c > 0 ) by A20, SCMPDS_5:15; :: thesis:
thus v . (DataLoc (d,i)) = ((IExec (I,Q,t)) . b) - ((IExec (I,Q,t)) . c) by A30, SCMPDS_5:15
.= (v . b) - ((IExec (I,Q,t)) . c) by SCMPDS_5:15
.= (v . b) - (v . c) by SCMPDS_5:15 ; :: thesis:

end;

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

proof

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

A37: now

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

end;

thus t . (DataLoc ((s . a),i)) = (v . b) - (v . c) by A3, A34, A36
.= (t . b) - (v . c) by A34
.= (t . b) - (t . c) by A34
.= 0 by A37 ; :: thesis:

end;

A39: S₁[s] by A4, A5, A6;
( while<>0 (a,i,I) is_closed_on s,P & while<>0 (a,i,I) is_halting_on s,P ) from SCPINVAR:sch 3(A31, A39, A8);
hence ( while<>0 (a,i,I) is_closed_on s,P & while<>0 (a,i,I) is_halting_on s,P ) ; :: thesis:
assume A40: s . (DataLoc ((s . a),i)) <> 0 ; :: thesis:
IExec ((while<>0 (a,i,I)),P,s) = IExec ((while<>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) from SCPINVAR:sch 4(A40, A31, A39, A8);
hence IExec ((while<>0 (a,i,I)),P,s) = IExec ((while<>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) ; :: thesis: