let P be Instruction-Sequence of SCMPDS; for s being 0 -started State of SCMPDS
for I being halt-free shiftable Program of SCMPDS
for a, b, c being Int_position
for i, d being Integer st s . a = d & s . b > 0 & s . c > 0 & s . (DataLoc (d,i)) = (s . b) - (s . c) & ( 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) ) ) holds
( (IExec ((while<>0 (a,i,I)),P,s)) . b = (s . b) gcd (s . c) & (IExec ((while<>0 (a,i,I)),P,s)) . c = (s . b) gcd (s . c) )
let s be 0 -started State of SCMPDS; for I being halt-free shiftable Program of SCMPDS
for a, b, c being Int_position
for i, d being Integer st s . a = d & s . b > 0 & s . c > 0 & s . (DataLoc (d,i)) = (s . b) - (s . c) & ( 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) ) ) holds
( (IExec ((while<>0 (a,i,I)),P,s)) . b = (s . b) gcd (s . c) & (IExec ((while<>0 (a,i,I)),P,s)) . c = (s . b) gcd (s . c) )
let I be halt-free shiftable Program of SCMPDS; for a, b, c being Int_position
for i, d being Integer st s . a = d & s . b > 0 & s . c > 0 & s . (DataLoc (d,i)) = (s . b) - (s . c) & ( 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) ) ) holds
( (IExec ((while<>0 (a,i,I)),P,s)) . b = (s . b) gcd (s . c) & (IExec ((while<>0 (a,i,I)),P,s)) . c = (s . b) gcd (s . c) )
let a, b, c be Int_position; for i, d being Integer st s . a = d & s . b > 0 & s . c > 0 & s . (DataLoc (d,i)) = (s . b) - (s . c) & ( 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) ) ) holds
( (IExec ((while<>0 (a,i,I)),P,s)) . b = (s . b) gcd (s . c) & (IExec ((while<>0 (a,i,I)),P,s)) . c = (s . b) gcd (s . c) )
let i, d be Integer; ( s . a = d & s . b > 0 & s . c > 0 & s . (DataLoc (d,i)) = (s . b) - (s . c) & ( 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) ) ) implies ( (IExec ((while<>0 (a,i,I)),P,s)) . b = (s . b) gcd (s . c) & (IExec ((while<>0 (a,i,I)),P,s)) . c = (s . b) gcd (s . c) ) )
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 H1( 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 S1[ 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)
; ( ex t being 0 -started State of SCMPDS ex 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 & not ( (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) ) ) or ( (IExec ((while<>0 (a,i,I)),P,s)) . b = (s . b) gcd (s . c) & (IExec ((while<>0 (a,i,I)),P,s)) . c = (s . b) gcd (s . c) ) )
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) )
; ( (IExec ((while<>0 (a,i,I)),P,s)) . b = (s . b) gcd (s . c) & (IExec ((while<>0 (a,i,I)),P,s)) . c = (s . b) gcd (s . c) )
A7:
now for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st S1[t] & t . a = s . a & t . (DataLoc ((s . a),i)) <> 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & H1( Initialize (IExec (I,Q,t))) < H1(t) & S1[ Initialize (IExec (I,Q,t))] )let t be
0 -started State of
SCMPDS;
for Q being Instruction-Sequence of SCMPDS st S1[t] & t . a = s . a & t . (DataLoc ((s . a),i)) <> 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & H1( Initialize (IExec (I,Q,t))) < H1(t) & S1[ Initialize (IExec (I,Q,t))] )let Q be
Instruction-Sequence of
SCMPDS;
( S1[t] & t . a = s . a & t . (DataLoc ((s . a),i)) <> 0 implies ( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & H1( Initialize (IExec (I,Q,t))) < H1(t) & S1[ Initialize (IExec (I,Q,t))] ) )assume that A8:
S1[
t]
and A9:
t . a = s . a
and A10:
t . (DataLoc ((s . a),i)) <> 0
;
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & H1( Initialize (IExec (I,Q,t))) < H1(t) & S1[ Initialize (IExec (I,Q,t))] )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;
( I is_closed_on t,Q & I is_halting_on t,Q & H1( Initialize (IExec (I,Q,t))) < H1(t) & S1[ Initialize (IExec (I,Q,t))] )thus
(
I is_closed_on t,
Q &
I is_halting_on t,
Q )
by A2, A6, A9, A16, A17, A18, A20;
( H1( Initialize (IExec (I,Q,t))) < H1(t) & S1[ Initialize (IExec (I,Q,t))] )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 ( (IExec (I,Q,t)) . b > 0 & (IExec (I,Q,t)) . c > 0 & ((IExec (I,Q,t)) . b) gcd ((IExec (I,Q,t)) . c) = (t . b) gcd (t . c) & max (((IExec (I,Q,t)) . b),((IExec (I,Q,t)) . c)) < max ((t . b),(t . c)) )per cases
( t . b > t . c or t . b <= t . c )
;
suppose A23:
t . b > t . c
;
( (IExec (I,Q,t)) . b > 0 & (IExec (I,Q,t)) . c > 0 & ((IExec (I,Q,t)) . b) gcd ((IExec (I,Q,t)) . c) = (t . b) gcd (t . c) & max (((IExec (I,Q,t)) . b),((IExec (I,Q,t)) . c)) < max ((t . b),(t . c)) )then
(t . b) - (t . c) > 0
by XREAL_1:50;
hence
(IExec (I,Q,t)) . b > 0
by A2, A6, A9, A17, A18, A23;
( (IExec (I,Q,t)) . c > 0 & ((IExec (I,Q,t)) . b) gcd ((IExec (I,Q,t)) . c) = (t . b) gcd (t . c) & max (((IExec (I,Q,t)) . b),((IExec (I,Q,t)) . c)) < max ((t . b),(t . c)) )thus
(IExec (I,Q,t)) . c > 0
by A2, A6, A9, A17, A18, A23;
( ((IExec (I,Q,t)) . b) gcd ((IExec (I,Q,t)) . c) = (t . b) gcd (t . c) & max (((IExec (I,Q,t)) . b),((IExec (I,Q,t)) . c)) < max ((t . b),(t . c)) )thus
((IExec (I,Q,t)) . b) gcd ((IExec (I,Q,t)) . c) = (t . b) gcd (t . c)
by A16, A17, A19, A21, PREPOWER:97;
max (((IExec (I,Q,t)) . b),((IExec (I,Q,t)) . c)) < max ((t . b),(t . c))A24:
(IExec (I,Q,t)) . b = (t . b) - (t . c)
by A2, A6, A9, A17, A18, A23;
hereby verum
A25:
max (
(t . b),
(t . c))
= t . b
by A23, XXREAL_0:def 10;
per cases
( max (((IExec (I,Q,t)) . b),((IExec (I,Q,t)) . c)) = (IExec (I,Q,t)) . b or max (((IExec (I,Q,t)) . b),((IExec (I,Q,t)) . c)) = (IExec (I,Q,t)) . c )
by XXREAL_0:16;
suppose
max (
((IExec (I,Q,t)) . b),
((IExec (I,Q,t)) . c))
= (IExec (I,Q,t)) . b
;
max (((IExec (I,Q,t)) . b),((IExec (I,Q,t)) . c)) < max ((t . b),(t . c))end; suppose
max (
((IExec (I,Q,t)) . b),
((IExec (I,Q,t)) . c))
= (IExec (I,Q,t)) . c
;
max (((IExec (I,Q,t)) . b),((IExec (I,Q,t)) . c)) < max ((t . b),(t . c))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;
verum end; end;
end; end; suppose A26:
t . b <= t . c
;
( (IExec (I,Q,t)) . b > 0 & (IExec (I,Q,t)) . c > 0 & ((IExec (I,Q,t)) . b) gcd ((IExec (I,Q,t)) . c) = (t . b) gcd (t . c) & max (((IExec (I,Q,t)) . b),((IExec (I,Q,t)) . c)) < max ((t . b),(t . c)) )hence
(IExec (I,Q,t)) . b > 0
by A2, A6, A9, A16, A18, A20;
( (IExec (I,Q,t)) . c > 0 & ((IExec (I,Q,t)) . b) gcd ((IExec (I,Q,t)) . c) = (t . b) gcd (t . c) & max (((IExec (I,Q,t)) . b),((IExec (I,Q,t)) . c)) < max ((t . b),(t . c)) )
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;
( ((IExec (I,Q,t)) . b) gcd ((IExec (I,Q,t)) . c) = (t . b) gcd (t . c) & max (((IExec (I,Q,t)) . b),((IExec (I,Q,t)) . c)) < max ((t . b),(t . c)) )thus
((IExec (I,Q,t)) . b) gcd ((IExec (I,Q,t)) . c) = (t . b) gcd (t . c)
by A16, A17, A19, A21, PREPOWER:97;
max (((IExec (I,Q,t)) . b),((IExec (I,Q,t)) . c)) < max ((t . b),(t . c))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 verum
A29:
max (
(t . b),
(t . c))
= t . c
by A26, XXREAL_0:def 10;
per cases
( max (((IExec (I,Q,t)) . b),((IExec (I,Q,t)) . c)) = (IExec (I,Q,t)) . c or max (((IExec (I,Q,t)) . b),((IExec (I,Q,t)) . c)) = (IExec (I,Q,t)) . b )
by XXREAL_0:16;
suppose
max (
((IExec (I,Q,t)) . b),
((IExec (I,Q,t)) . c))
= (IExec (I,Q,t)) . c
;
max (((IExec (I,Q,t)) . b),((IExec (I,Q,t)) . c)) < max ((t . b),(t . c))end; suppose
max (
((IExec (I,Q,t)) . b),
((IExec (I,Q,t)) . c))
= (IExec (I,Q,t)) . b
;
max (((IExec (I,Q,t)) . b),((IExec (I,Q,t)) . c)) < max ((t . b),(t . c))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;
verum end; end;
end; end; end; end; thus
H1(
Initialize (IExec (I,Q,t)))
< H1(
t)
S1[ Initialize (IExec (I,Q,t))]proof
t . b <> t . c
by A20;
then
t . b <> t . c
;
then A30:
H1(
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
H1(
t)
>= t . b
by XXREAL_0:25;
then A31:
H1(
t)
> 0
by A16;
per cases
( (Initialize (IExec (I,Q,t))) . 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
;
H1( Initialize (IExec (I,Q,t))) < H1(t)then H1(
Initialize (IExec (I,Q,t))) =
max (
|.((Initialize (IExec (I,Q,t))) . b).|,
|.((Initialize (IExec (I,Q,t))) . c).|)
by A1
.=
max (
|.((IExec (I,Q,t)) . b).|,
|.((Initialize (IExec (I,Q,t))) . c).|)
by SCMPDS_5:15
.=
max (
|.((IExec (I,Q,t)) . b).|,
|.((IExec (I,Q,t)) . c).|)
by SCMPDS_5:15
.=
max (
((IExec (I,Q,t)) . b),
|.((IExec (I,Q,t)) . c).|)
by A22, ABSVALUE:def 1
.=
max (
((IExec (I,Q,t)) . b),
((IExec (I,Q,t)) . c))
by A22, ABSVALUE:def 1
;
hence
H1(
Initialize (IExec (I,Q,t)))
< H1(
t)
by A22, A30;
verum end; end;
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
S1[
Initialize (IExec (I,Q,t))]
verumproof
take u =
Initialize (IExec (I,Q,t));
( u = Initialize (IExec (I,Q,t)) & u . b > 0 & u . c > 0 & (u . b) gcd (u . c) = (s . b) gcd (s . c) & u . (DataLoc (d,i)) = (u . b) - (u . c) )
thus
u = Initialize (IExec (I,Q,t))
;
( u . b > 0 & u . c > 0 & (u . b) gcd (u . c) = (s . b) gcd (s . c) & u . (DataLoc (d,i)) = (u . b) - (u . c) )
thus
(
u . b > 0 &
u . c > 0 )
by A22, SCMPDS_5:15;
( (u . b) gcd (u . c) = (s . b) gcd (s . c) & u . (DataLoc (d,i)) = (u . b) - (u . c) )
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
;
u . (DataLoc (d,i)) = (u . b) - (u . c)
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
;
verum
end; end;
A33:
for t being 0 -started State of SCMPDS st S1[t] holds
( H1(t) = 0 iff t . (DataLoc ((s . a),i)) = 0 )
A40:
S1[s]
by A3, A4, A5;
A41:
( H1( Initialize (IExec ((while<>0 (a,i,I)),P,s))) = 0 & S1[ 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
; (IExec ((while<>0 (a,i,I)),P,s)) . c = (s . b) gcd (s . c)
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
; verum