let A be Euclidean preIfWhileAlgebra; for X being non empty countable set
for b being Element of X
for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)
for x, y, z being Variable of g st ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . z = 3 ) holds
for s being Element of Funcs (X,INT) holds
( (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . x = s . y & (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . y = |.((s . x) - (s . y)).| & ( for n, m being Element of NAT st n = s . x & m = s . y & ( s in (Funcs (X,INT)) \ (b,0) implies m > 0 ) & ( m > 0 implies s in (Funcs (X,INT)) \ (b,0) ) holds
g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0),s ) )
let X be non empty countable set ; for b being Element of X
for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)
for x, y, z being Variable of g st ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . z = 3 ) holds
for s being Element of Funcs (X,INT) holds
( (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . x = s . y & (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . y = |.((s . x) - (s . y)).| & ( for n, m being Element of NAT st n = s . x & m = s . y & ( s in (Funcs (X,INT)) \ (b,0) implies m > 0 ) & ( m > 0 implies s in (Funcs (X,INT)) \ (b,0) ) holds
g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0),s ) )
let b be Element of X; for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)
for x, y, z being Variable of g st ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . z = 3 ) holds
for s being Element of Funcs (X,INT) holds
( (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . x = s . y & (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . y = |.((s . x) - (s . y)).| & ( for n, m being Element of NAT st n = s . x & m = s . y & ( s in (Funcs (X,INT)) \ (b,0) implies m > 0 ) & ( m > 0 implies s in (Funcs (X,INT)) \ (b,0) ) holds
g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0),s ) )
let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0); for x, y, z being Variable of g st ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . z = 3 ) holds
for s being Element of Funcs (X,INT) holds
( (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . x = s . y & (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . y = |.((s . x) - (s . y)).| & ( for n, m being Element of NAT st n = s . x & m = s . y & ( s in (Funcs (X,INT)) \ (b,0) implies m > 0 ) & ( m > 0 implies s in (Funcs (X,INT)) \ (b,0) ) holds
g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0),s ) )
set S = Funcs (X,INT);
set T = (Funcs (X,INT)) \ (b,0);
let x, y, z be Variable of g; ( ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . z = 3 ) implies for s being Element of Funcs (X,INT) holds
( (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . x = s . y & (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . y = |.((s . x) - (s . y)).| & ( for n, m being Element of NAT st n = s . x & m = s . y & ( s in (Funcs (X,INT)) \ (b,0) implies m > 0 ) & ( m > 0 implies s in (Funcs (X,INT)) \ (b,0) ) holds
g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0),s ) ) )
given d being Function such that A1:
d . b = 0
and
A2:
d . x = 1
and
A3:
d . y = 2
and
A4:
d . z = 3
; for s being Element of Funcs (X,INT) holds
( (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . x = s . y & (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . y = |.((s . x) - (s . y)).| & ( for n, m being Element of NAT st n = s . x & m = s . y & ( s in (Funcs (X,INT)) \ (b,0) implies m > 0 ) & ( m > 0 implies s in (Funcs (X,INT)) \ (b,0) ) holds
g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0),s ) )
A5:
y <> z
by A3, A4;
let s be Element of Funcs (X,INT); ( (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . x = s . y & (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . y = |.((s . x) - (s . y)).| & ( for n, m being Element of NAT st n = s . x & m = s . y & ( s in (Funcs (X,INT)) \ (b,0) implies m > 0 ) & ( m > 0 implies s in (Funcs (X,INT)) \ (b,0) ) holds
g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0),s ) )
set J = if-then ((z lt 0),(z *= (- 1)));
A6:
g complies_with_if_wrt (Funcs (X,INT)) \ (b,0)
by AOFA_000:def 32;
A7:
z <> x
by A2, A4;
set I = (((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z);
A8:
x <> y
by A2, A3;
A9:
now for s being Element of Funcs (X,INT) holds
( (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . x = s . y & (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . y = |.((s . x) - (s . y)).| )let s be
Element of
Funcs (
X,
INT);
( (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . x = s . y & (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . y = |.((s . x) - (s . y)).| )set s1 =
g . (
s,
(z := ((. x) - (. y))));
set s2 =
g . (
(g . (s,(z := ((. x) - (. y))))),
(z lt 0));
set q =
g . (
(g . (s,(z := ((. x) - (. y))))),
(if-then ((z lt 0),(z *= (- 1)))));
set qz =
g . (
(g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))),
(z *= (- 1)));
A10:
((g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))) . z) * (- 1) = - ((g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))) . z)
;
set s3 =
g . (
(g . ((g . (s,(z := ((. x) - (. y))))),(if-then ((z lt 0),(z *= (- 1)))))),
(x := y));
set s4 =
g . (
(g . ((g . ((g . (s,(z := ((. x) - (. y))))),(if-then ((z lt 0),(z *= (- 1)))))),(x := y))),
(y := z));
A11:
g . (
s,
((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z))) =
g . (
(g . (s,(((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)))),
(y := z))
by AOFA_000:def 29
.=
g . (
(g . ((g . (s,((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))))),(x := y))),
(y := z))
by AOFA_000:def 29
.=
g . (
(g . ((g . ((g . (s,(z := ((. x) - (. y))))),(if-then ((z lt 0),(z *= (- 1)))))),(x := y))),
(y := z))
by AOFA_000:def 29
;
(
(g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))) . b = 1 implies
g . (
(g . (s,(z := ((. x) - (. y))))),
(z lt 0))
in (Funcs (X,INT)) \ (
b,
0) )
;
then A12:
(
(g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))) . b = 1 implies
g . (
(g . (s,(z := ((. x) - (. y))))),
(if-then ((z lt 0),(z *= (- 1)))))
= g . (
(g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))),
(z *= (- 1))) )
by A6;
A13:
(. x) . s = s . x
by Th22;
A14:
(g . ((g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))),(z *= (- 1)))) . y = (g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))) . y
by A5, Th31;
A15:
(. y) . s = s . y
by Th22;
((. x) - (. y)) . s = ((. x) . s) - ((. y) . s)
by Def11;
then A16:
(g . (s,(z := ((. x) - (. y))))) . z = (s . x) - (s . y)
by A13, A15, Th26;
A17:
(
(g . (s,(z := ((. x) - (. y))))) . z < 0 implies
(g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))) . b = 1 )
by Th38;
A18:
(g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))) . z = (g . (s,(z := ((. x) - (. y))))) . z
by A1, A4, Th38;
A19:
(g . ((g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))),(z *= (- 1)))) . z = ((g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))) . z) * (- 1)
by Th31;
A20:
(g . ((g . ((g . (s,(z := ((. x) - (. y))))),(if-then ((z lt 0),(z *= (- 1)))))),(x := y))) . z = (g . ((g . (s,(z := ((. x) - (. y))))),(if-then ((z lt 0),(z *= (- 1)))))) . z
by A7, Th27;
A21:
(g . ((g . ((g . ((g . (s,(z := ((. x) - (. y))))),(if-then ((z lt 0),(z *= (- 1)))))),(x := y))),(y := z))) . y = (g . ((g . ((g . (s,(z := ((. x) - (. y))))),(if-then ((z lt 0),(z *= (- 1)))))),(x := y))) . z
by Th27;
(
(g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))) . b = 0 implies
g . (
(g . (s,(z := ((. x) - (. y))))),
(z lt 0))
nin (Funcs (X,INT)) \ (
b,
0) )
by Th2;
then A22:
(
(g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))) . b = 0 implies
g . (
(g . (s,(z := ((. x) - (. y))))),
(if-then ((z lt 0),(z *= (- 1)))))
= g . (
(g . (s,(z := ((. x) - (. y))))),
(z lt 0)) )
by A6, AOFA_000:80;
A23:
(
(g . (s,(z := ((. x) - (. y))))) . z >= 0 implies
(g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))) . b = 0 )
by Th38;
A24:
(g . (s,(z := ((. x) - (. y))))) . y = s . y
by A5, Th26;
A25:
(g . ((g . ((g . (s,(z := ((. x) - (. y))))),(if-then ((z lt 0),(z *= (- 1)))))),(x := y))) . x = (g . ((g . (s,(z := ((. x) - (. y))))),(if-then ((z lt 0),(z *= (- 1)))))) . y
by Th27;
(g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))) . y = (g . (s,(z := ((. x) - (. y))))) . y
by A1, A3, Th38;
hence
(
(g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . x = s . y &
(g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . y = |.((s . x) - (s . y)).| )
by A8, A22, A12, A18, A17, A23, A14, A19, A10, A11, A24, A16, A25, A20, A21, Th27, ABSVALUE:def 1;
verum end;
hence
( (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . x = s . y & (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . y = |.((s . x) - (s . y)).| )
; for n, m being Element of NAT st n = s . x & m = s . y & ( s in (Funcs (X,INT)) \ (b,0) implies m > 0 ) & ( m > 0 implies s in (Funcs (X,INT)) \ (b,0) ) holds
g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0),s
deffunc H1( Element of Funcs (X,INT)) -> Element of NAT = IFEQ (($1 . y),0,0,(IFEQ (($1 . x),0,2,(IFEQ (($1 . x),($1 . y),1,(In ((max ((2 * ($1 . x)),((2 * ($1 . y)) + 1))),NAT)))))));
defpred S1[ Element of Funcs (X,INT)] means ( $1 . x >= 0 & $1 . y > 0 );
set C = y gt 0;
A26:
for s being Element of Funcs (X,INT) st S1[s] holds
( ( S1[g . (s,(((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0)))] implies g . (s,(((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0))) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0))) in (Funcs (X,INT)) \ (b,0) implies S1[g . (s,(((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0)))] ) & H1(g . (s,(((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0)))) < H1(s) )
proof
let s be
Element of
Funcs (
X,
INT);
( S1[s] implies ( ( S1[g . (s,(((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0)))] implies g . (s,(((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0))) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0))) in (Funcs (X,INT)) \ (b,0) implies S1[g . (s,(((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0)))] ) & H1(g . (s,(((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0)))) < H1(s) ) )
assume that A27:
s . x >= 0
and A28:
s . y > 0
;
( ( S1[g . (s,(((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0)))] implies g . (s,(((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0))) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0))) in (Funcs (X,INT)) \ (b,0) implies S1[g . (s,(((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0)))] ) & H1(g . (s,(((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0)))) < H1(s) )
reconsider s9 =
g . (
s,
((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z))) as
Element of
Funcs (
X,
INT) ;
reconsider s99 =
g . (
s9,
(y gt 0)) as
Element of
Funcs (
X,
INT) ;
A29:
s9 . y = |.((s . x) - (s . y)).|
by A9;
then reconsider nx =
s . x,
ny =
s . y,
nn =
s99 . y as
Element of
NAT by A1, A3, A27, A28, Th38, INT_1:3;
A30:
g . (
s,
(((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0)))
= s99
by AOFA_000:def 29;
A31:
s99 . x = s9 . x
by A1, A2, Th38;
A32:
(
s9 . y <= 0 implies
s99 . b = 0 )
by Th38;
A33:
(
s9 . y > 0 implies
s99 . b = 1 )
by Th38;
hence
(
S1[
g . (
s,
(((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0)))] iff
g . (
s,
(((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0)))
in (Funcs (X,INT)) \ (
b,
0) )
by A9, A28, A30, A31, A32, Th2, Th38;
H1(g . (s,(((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0)))) < H1(s)
A34:
s9 . x = s . y
by A9;
A35:
H1(
s99)
= IFEQ (
nn,
0,
0,
(IFEQ (ny,0,2,(IFEQ (ny,nn,1,(max ((2 * ny),((2 * nn) + 1))))))))
by A31, A34;
(2 * ny) + 1
> 2
* ny
by NAT_1:13;
then A36:
max (
(2 * nx),
((2 * ny) + 1))
> 2
* ny
by XXREAL_0:30;
A37:
s99 . y = s9 . y
by A1, A3, Th38;
A38:
H1(
s) =
IFEQ (
ny,
0,
0,
(IFEQ (nx,0,2,(IFEQ (nx,ny,1,(max ((2 * nx),((2 * ny) + 1))))))))
.=
IFEQ (
nx,
0,2,
(IFEQ (nx,ny,1,(max ((2 * nx),((2 * ny) + 1))))))
by A28, FUNCOP_1:def 8
;
per cases
( nx = ny or nx > ny or ( nx < ny & nx > 0 ) or nx = 0 )
by XXREAL_0:1;
suppose A39:
nx = ny
;
H1(g . (s,(((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0)))) < H1(s)then A40:
IFEQ (
nx,
ny,1,
(max ((2 * nx),((2 * ny) + 1))))
= 1
by FUNCOP_1:def 8;
A41:
nn = 0
by A37, A29, A39, ABSVALUE:2;
H1(
s)
= IFEQ (
nx,
ny,1,
(max ((2 * nx),((2 * ny) + 1))))
by A28, A38, A39, FUNCOP_1:def 8;
hence
H1(
g . (
s,
(((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0))))
< H1(
s)
by A30, A40, A41, FUNCOP_1:def 8;
verum end; suppose A42:
nx > ny
;
H1(g . (s,(((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0)))) < H1(s)then
IFEQ (
nx,
ny,1,
(max ((2 * nx),((2 * ny) + 1))))
= max (
(2 * nx),
((2 * ny) + 1))
by FUNCOP_1:def 8;
then A43:
H1(
s)
= max (
(2 * nx),
((2 * ny) + 1))
by A38, A42, FUNCOP_1:def 8;
A44:
nx - ny > 0
by A42, XREAL_1:50;
then A45:
H1(
s99) =
IFEQ (
ny,
0,2,
(IFEQ (ny,nn,1,(max ((2 * ny),((2 * nn) + 1))))))
by A37, A33, A32, A29, A35, ABSVALUE:def 1, FUNCOP_1:def 8
.=
IFEQ (
ny,
nn,1,
(max ((2 * ny),((2 * nn) + 1))))
by A28, FUNCOP_1:def 8
;
then A46:
(
ny = nn implies
H1(
s99)
= 1 )
by FUNCOP_1:def 8;
nn = nx - ny
by A37, A29, A44, ABSVALUE:def 1;
then
nn < nx
by A28, XREAL_1:44;
then
nn + 1
<= nx
by NAT_1:13;
then A47:
2
* (nn + 1) <= 2
* nx
by XREAL_1:64;
A48:
1
<= (2 * nn) + 1
by NAT_1:11;
A49:
(
ny <> nn implies
H1(
s99)
= max (
(2 * ny),
((2 * nn) + 1)) )
by A45, FUNCOP_1:def 8;
(2 * nn) + 2
= ((2 * nn) + 1) + 1
;
then
(2 * nn) + 1
< 2
* nx
by A47, NAT_1:13;
then
(2 * nn) + 1
< H1(
s)
by A43, XXREAL_0:30;
hence
H1(
g . (
s,
(((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0))))
< H1(
s)
by A30, A36, A43, A46, A49, A48, XXREAL_0:2, XXREAL_0:29;
verum end; suppose A50:
(
nx < ny &
nx > 0 )
;
H1(g . (s,(((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0)))) < H1(s)A51:
- (nx - ny) = ny - nx
;
A52:
nx - ny < 0
by A50, XREAL_1:49;
then A53:
nn = - (nx - ny)
by A37, A29, ABSVALUE:def 1;
then A54:
nn < ny
by A50, A51, XREAL_1:44;
2
* nn < 2
* ny
by A50, A53, A51, XREAL_1:44, XREAL_1:68;
then
(2 * nn) + 1
< (2 * ny) + 1
by XREAL_1:6;
then A55:
(2 * nn) + 1
< max (
(2 * nx),
((2 * ny) + 1))
by XXREAL_0:30;
nn > 0
by A37, A29, A52, A51, ABSVALUE:def 1;
then A56:
H1(
s99) =
IFEQ (
ny,
0,2,
(IFEQ (ny,nn,1,(max ((2 * ny),((2 * nn) + 1))))))
by A35, FUNCOP_1:def 8
.=
IFEQ (
ny,
nn,1,
(max ((2 * ny),((2 * nn) + 1))))
by A28, FUNCOP_1:def 8
.=
max (
(2 * ny),
((2 * nn) + 1))
by A54, FUNCOP_1:def 8
;
H1(
s) =
IFEQ (
nx,
ny,1,
(max ((2 * nx),((2 * ny) + 1))))
by A38, A50, FUNCOP_1:def 8
.=
max (
(2 * nx),
((2 * ny) + 1))
by A50, FUNCOP_1:def 8
;
hence
H1(
g . (
s,
(((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0))))
< H1(
s)
by A30, A36, A55, A56, XXREAL_0:29;
verum end; suppose A57:
nx = 0
;
H1(g . (s,(((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0)))) < H1(s)then A58:
H1(
s)
= 2
by A38, FUNCOP_1:def 8;
A59:
nn =
- (nx - ny)
by A28, A37, A29, A57, ABSVALUE:def 1
.=
ny
by A57
;
then H1(
s99) =
IFEQ (
ny,
0,2,
(IFEQ (ny,nn,1,(max ((2 * ny),((2 * nn) + 1))))))
by A28, A35, FUNCOP_1:def 8
.=
IFEQ (
ny,
nn,1,
(max ((2 * ny),((2 * nn) + 1))))
by A28, FUNCOP_1:def 8
.=
1
by A59, FUNCOP_1:def 8
;
hence
H1(
g . (
s,
(((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0))))
< H1(
s)
by A30, A58;
verum end;
end;
let n, m be Element of NAT ; ( n = s . x & m = s . y & ( s in (Funcs (X,INT)) \ (b,0) implies m > 0 ) & ( m > 0 implies s in (Funcs (X,INT)) \ (b,0) ) implies g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0),s )
assume that
A60:
n = s . x
and
A61:
m = s . y
; ( ( s in (Funcs (X,INT)) \ (b,0) & not m > 0 ) or ( m > 0 & not s in (Funcs (X,INT)) \ (b,0) ) or g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0),s )
assume
( s in (Funcs (X,INT)) \ (b,0) iff m > 0 )
; g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0),s
then A62:
( s in (Funcs (X,INT)) \ (b,0) iff S1[s] )
by A60, A61;
g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0),s
from AOFA_000:sch 3(A62, A26);
hence
g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0),s
; verum