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
while ((y gt 0),((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z))) is_terminating_wrt g, { s where s is Element of Funcs (X,INT) : ( s . x >= 0 & s . y >= 0 ) }
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
while ((y gt 0),((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z))) is_terminating_wrt g, { s where s is Element of Funcs (X,INT) : ( s . x >= 0 & s . y >= 0 ) }
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
while ((y gt 0),((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z))) is_terminating_wrt g, { s where s is Element of Funcs (X,INT) : ( s . x >= 0 & s . y >= 0 ) }
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
while ((y gt 0),((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z))) is_terminating_wrt g, { s where s is Element of Funcs (X,INT) : ( s . x >= 0 & s . y >= 0 ) }
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 while ((y gt 0),((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z))) is_terminating_wrt g, { s where s is Element of Funcs (X,INT) : ( s . x >= 0 & s . y >= 0 ) } )
set P = { s where s is Element of Funcs (X,INT) : ( s . x >= 0 & s . y >= 0 ) } ;
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
; while ((y gt 0),((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z))) is_terminating_wrt g, { s where s is Element of Funcs (X,INT) : ( s . x >= 0 & s . y >= 0 ) }
set C = y gt 0;
set I = (((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z);
A5:
now for s being Element of Funcs (X,INT) st s in { s where s is Element of Funcs (X,INT) : ( s . x >= 0 & s . y >= 0 ) } & g . ((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) holds
g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z))) in { s where s is Element of Funcs (X,INT) : ( s . x >= 0 & s . y >= 0 ) } let s be
Element of
Funcs (
X,
INT);
( s in { s where s is Element of Funcs (X,INT) : ( s . x >= 0 & s . y >= 0 ) } & g . ((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 g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z))) in { s where s is Element of Funcs (X,INT) : ( s . x >= 0 & s . y >= 0 ) } )assume
s in { s where s is Element of Funcs (X,INT) : ( s . x >= 0 & s . y >= 0 ) }
;
( g . ((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 g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z))) in { s where s is Element of Funcs (X,INT) : ( s . x >= 0 & s . y >= 0 ) } )then
ex
s9 being
Element of
Funcs (
X,
INT) st
(
s9 = s &
s9 . x >= 0 &
s9 . y >= 0 )
;
then reconsider m =
s . y as
Element of
NAT by INT_1:3;
assume
g . (
(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))) in { s where s is Element of Funcs (X,INT) : ( s . x >= 0 & s . y >= 0 ) } A6:
(g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . x = m
by A1, A2, A3, A4, Lm2;
(g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . y = |.((s . x) - (s . y)).|
by A1, A2, A3, A4, Lm2;
hence
g . (
s,
((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))
in { s where s is Element of Funcs (X,INT) : ( s . x >= 0 & s . y >= 0 ) }
by A6;
verum end;
A7:
now for s being Element of Funcs (X,INT) st g . (s,(y gt 0)) in { s where s is Element of Funcs (X,INT) : ( s . x >= 0 & s . y >= 0 ) } holds
g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0),g . (s,(y gt 0))let s be
Element of
Funcs (
X,
INT);
( g . (s,(y gt 0)) in { s where s is Element of Funcs (X,INT) : ( s . x >= 0 & s . y >= 0 ) } implies g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0),g . (s,(y gt 0)) )set s1 =
g . (
s,
(y gt 0));
A8:
(
s . y <= 0 implies
(g . (s,(y gt 0))) . b = 0 )
by Th38;
assume
g . (
s,
(y gt 0))
in { s where s is Element of Funcs (X,INT) : ( s . x >= 0 & s . y >= 0 ) }
;
g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0),g . (s,(y gt 0))then
ex
s9 being
Element of
Funcs (
X,
INT) st
(
s9 = g . (
s,
(y gt 0)) &
s9 . x >= 0 &
s9 . y >= 0 )
;
then reconsider n =
(g . (s,(y gt 0))) . x,
m =
(g . (s,(y gt 0))) . y as
Element of
NAT by INT_1:3;
A9:
n = n
;
(
s . y > 0 implies
(g . (s,(y gt 0))) . b = 1 )
by Th38;
then
(
g . (
s,
(y gt 0))
in (Funcs (X,INT)) \ (
b,
0) iff
m > 0 )
by A8, Th2, Th38;
hence
g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0),
g . (
s,
(y gt 0))
by A1, A2, A3, A4, A9, Lm2;
verum end;
A10:
{ s where s is Element of Funcs (X,INT) : ( s . x >= 0 & s . y >= 0 ) } is_invariant_wrt y gt 0,g
proof
let s be
Element of
Funcs (
X,
INT);
AOFA_000:def 39 ( not s in { s where s is Element of Funcs (X,INT) : ( s . x >= 0 & s . y >= 0 ) } or g . (s,(y gt 0)) in { s where s is Element of Funcs (X,INT) : ( s . x >= 0 & s . y >= 0 ) } )
set s1 =
g . (
s,
(y gt 0));
assume
s in { s where s is Element of Funcs (X,INT) : ( s . x >= 0 & s . y >= 0 ) }
;
g . (s,(y gt 0)) in { s where s is Element of Funcs (X,INT) : ( s . x >= 0 & s . y >= 0 ) }
then A11:
ex
s9 being
Element of
Funcs (
X,
INT) st
(
s9 = s &
s9 . x >= 0 &
s9 . y >= 0 )
;
A12:
(g . (s,(y gt 0))) . y = s . y
by A1, A3, Th38;
(g . (s,(y gt 0))) . x = s . x
by A1, A2, Th38;
hence
g . (
s,
(y gt 0))
in { s where s is Element of Funcs (X,INT) : ( s . x >= 0 & s . y >= 0 ) }
by A11, A12;
verum
end;
y gt 0 is_terminating_wrt g
by AOFA_000:104;
hence
while ((y gt 0),((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z))) is_terminating_wrt g, { s where s is Element of Funcs (X,INT) : ( s . x >= 0 & s . y >= 0 ) }
by A10, A5, A7, AOFA_000:107, AOFA_000:118; verum