:: by Grzegorz Bancerek

::

:: Received March 18, 2008

:: Copyright (c) 2008-2017 Association of Mizar Users

theorem Th1: :: AOFA_I00:1

for x, y, z, a, b, c being set st a <> b & b <> c & c <> a holds

ex f being Function st

( f . a = x & f . b = y & f . c = z )

ex f being Function st

( f . a = x & f . b = y & f . c = z )

proof end;

definition

let F be non empty functional set ;

let x, f be set ;

coherence

{ g where g is Element of F : g . x <> f } is Subset of F

end;
let x, f be set ;

coherence

{ g where g is Element of F : g . x <> f } is Subset of F

proof end;

:: deftheorem defines \ AOFA_I00:def 1 :

for F being non empty functional set

for x, f being set holds F \ (x,f) = { g where g is Element of F : g . x <> f } ;

for F being non empty functional set

for x, f being set holds F \ (x,f) = { g where g is Element of F : g . x <> f } ;

theorem Th2: :: AOFA_I00:2

for F being non empty functional set

for x, y being set

for g being Element of F holds

( g in F \ (x,y) iff g . x <> y )

for x, y being set

for g being Element of F holds

( g in F \ (x,y) iff g . x <> y )

proof end;

definition

let X be set ;

let Y, Z be set ;

let f be Function of [:(Funcs (X,INT)),Y:],Z;

existence

ex b_{1} being Element of X st verum
;

end;
let Y, Z be set ;

let f be Function of [:(Funcs (X,INT)),Y:],Z;

existence

ex b

:: deftheorem Def2 defines Variable AOFA_I00:def 2 :

for X, Y, Z being set

for f being Function of [:(Funcs (X,INT)),Y:],Z

for b_{5} being Element of X holds

( b_{5} is Variable of f iff verum );

for X, Y, Z being set

for f being Function of [:(Funcs (X,INT)),Y:],Z

for b

( b

definition

let t1, t2 be INT -valued Function;

existence

ex b_{1} being INT -valued Function st

( dom b_{1} = (dom t1) /\ (dom t2) & ( for s being object st s in dom b_{1} holds

b_{1} . s = (t1 . s) div (t2 . s) ) );

uniqueness

for b_{1}, b_{2} being INT -valued Function st dom b_{1} = (dom t1) /\ (dom t2) & ( for s being object st s in dom b_{1} holds

b_{1} . s = (t1 . s) div (t2 . s) ) & dom b_{2} = (dom t1) /\ (dom t2) & ( for s being object st s in dom b_{2} holds

b_{2} . s = (t1 . s) div (t2 . s) ) holds

b_{1} = b_{2};

existence

ex b_{1} being INT -valued Function st

( dom b_{1} = (dom t1) /\ (dom t2) & ( for s being object st s in dom b_{1} holds

b_{1} . s = (t1 . s) mod (t2 . s) ) );

uniqueness

for b_{1}, b_{2} being INT -valued Function st dom b_{1} = (dom t1) /\ (dom t2) & ( for s being object st s in dom b_{1} holds

b_{1} . s = (t1 . s) mod (t2 . s) ) & dom b_{2} = (dom t1) /\ (dom t2) & ( for s being object st s in dom b_{2} holds

b_{2} . s = (t1 . s) mod (t2 . s) ) holds

b_{1} = b_{2};

existence

ex b_{1} being INT -valued Function st

( dom b_{1} = (dom t1) /\ (dom t2) & ( for s being object st s in dom b_{1} holds

b_{1} . s = IFGT ((t1 . s),(t2 . s),0,1) ) );

uniqueness

for b_{1}, b_{2} being INT -valued Function st dom b_{1} = (dom t1) /\ (dom t2) & ( for s being object st s in dom b_{1} holds

b_{1} . s = IFGT ((t1 . s),(t2 . s),0,1) ) & dom b_{2} = (dom t1) /\ (dom t2) & ( for s being object st s in dom b_{2} holds

b_{2} . s = IFGT ((t1 . s),(t2 . s),0,1) ) holds

b_{1} = b_{2};

existence

ex b_{1} being INT -valued Function st

( dom b_{1} = (dom t1) /\ (dom t2) & ( for s being object st s in dom b_{1} holds

b_{1} . s = IFGT ((t1 . s),(t2 . s),1,0) ) );

uniqueness

for b_{1}, b_{2} being INT -valued Function st dom b_{1} = (dom t1) /\ (dom t2) & ( for s being object st s in dom b_{1} holds

b_{1} . s = IFGT ((t1 . s),(t2 . s),1,0) ) & dom b_{2} = (dom t1) /\ (dom t2) & ( for s being object st s in dom b_{2} holds

b_{2} . s = IFGT ((t1 . s),(t2 . s),1,0) ) holds

b_{1} = b_{2};

existence

ex b_{1} being INT -valued Function st

( dom b_{1} = (dom t1) /\ (dom t2) & ( for s being object st s in dom b_{1} holds

b_{1} . s = IFEQ ((t1 . s),(t2 . s),1,0) ) );

uniqueness

for b_{1}, b_{2} being INT -valued Function st dom b_{1} = (dom t1) /\ (dom t2) & ( for s being object st s in dom b_{1} holds

b_{1} . s = IFEQ ((t1 . s),(t2 . s),1,0) ) & dom b_{2} = (dom t1) /\ (dom t2) & ( for s being object st s in dom b_{2} holds

b_{2} . s = IFEQ ((t1 . s),(t2 . s),1,0) ) holds

b_{1} = b_{2};

end;
func t1 div t2 -> INT -valued Function means :Def3: :: AOFA_I00:def 3

( dom it = (dom t1) /\ (dom t2) & ( for s being object st s in dom it holds

it . s = (t1 . s) div (t2 . s) ) );

correctness ( dom it = (dom t1) /\ (dom t2) & ( for s being object st s in dom it holds

it . s = (t1 . s) div (t2 . s) ) );

existence

ex b

( dom b

b

uniqueness

for b

b

b

b

proof end;

func t1 mod t2 -> INT -valued Function means :Def4: :: AOFA_I00:def 4

( dom it = (dom t1) /\ (dom t2) & ( for s being object st s in dom it holds

it . s = (t1 . s) mod (t2 . s) ) );

correctness ( dom it = (dom t1) /\ (dom t2) & ( for s being object st s in dom it holds

it . s = (t1 . s) mod (t2 . s) ) );

existence

ex b

( dom b

b

uniqueness

for b

b

b

b

proof end;

func leq (t1,t2) -> INT -valued Function means :Def5: :: AOFA_I00:def 5

( dom it = (dom t1) /\ (dom t2) & ( for s being object st s in dom it holds

it . s = IFGT ((t1 . s),(t2 . s),0,1) ) );

correctness ( dom it = (dom t1) /\ (dom t2) & ( for s being object st s in dom it holds

it . s = IFGT ((t1 . s),(t2 . s),0,1) ) );

existence

ex b

( dom b

b

uniqueness

for b

b

b

b

proof end;

func gt (t1,t2) -> INT -valued Function means :Def6: :: AOFA_I00:def 6

( dom it = (dom t1) /\ (dom t2) & ( for s being object st s in dom it holds

it . s = IFGT ((t1 . s),(t2 . s),1,0) ) );

correctness ( dom it = (dom t1) /\ (dom t2) & ( for s being object st s in dom it holds

it . s = IFGT ((t1 . s),(t2 . s),1,0) ) );

existence

ex b

( dom b

b

uniqueness

for b

b

b

b

proof end;

func eq (t1,t2) -> INT -valued Function means :Def7: :: AOFA_I00:def 7

( dom it = (dom t1) /\ (dom t2) & ( for s being object st s in dom it holds

it . s = IFEQ ((t1 . s),(t2 . s),1,0) ) );

correctness ( dom it = (dom t1) /\ (dom t2) & ( for s being object st s in dom it holds

it . s = IFEQ ((t1 . s),(t2 . s),1,0) ) );

existence

ex b

( dom b

b

uniqueness

for b

b

b

b

proof end;

:: deftheorem Def3 defines div AOFA_I00:def 3 :

for t1, t2, b_{3} being INT -valued Function holds

( b_{3} = t1 div t2 iff ( dom b_{3} = (dom t1) /\ (dom t2) & ( for s being object st s in dom b_{3} holds

b_{3} . s = (t1 . s) div (t2 . s) ) ) );

for t1, t2, b

( b

b

:: deftheorem Def4 defines mod AOFA_I00:def 4 :

for t1, t2, b_{3} being INT -valued Function holds

( b_{3} = t1 mod t2 iff ( dom b_{3} = (dom t1) /\ (dom t2) & ( for s being object st s in dom b_{3} holds

b_{3} . s = (t1 . s) mod (t2 . s) ) ) );

for t1, t2, b

( b

b

:: deftheorem Def5 defines leq AOFA_I00:def 5 :

for t1, t2, b_{3} being INT -valued Function holds

( b_{3} = leq (t1,t2) iff ( dom b_{3} = (dom t1) /\ (dom t2) & ( for s being object st s in dom b_{3} holds

b_{3} . s = IFGT ((t1 . s),(t2 . s),0,1) ) ) );

for t1, t2, b

( b

b

:: deftheorem Def6 defines gt AOFA_I00:def 6 :

for t1, t2, b_{3} being INT -valued Function holds

( b_{3} = gt (t1,t2) iff ( dom b_{3} = (dom t1) /\ (dom t2) & ( for s being object st s in dom b_{3} holds

b_{3} . s = IFGT ((t1 . s),(t2 . s),1,0) ) ) );

for t1, t2, b

( b

b

:: deftheorem Def7 defines eq AOFA_I00:def 7 :

for t1, t2, b_{3} being INT -valued Function holds

( b_{3} = eq (t1,t2) iff ( dom b_{3} = (dom t1) /\ (dom t2) & ( for s being object st s in dom b_{3} holds

b_{3} . s = IFEQ ((t1 . s),(t2 . s),1,0) ) ) );

for t1, t2, b

( b

b

definition

let X be non empty set ;

let f be Function of X,INT;

let x be Integer;

for b_{1} being Function of X,INT holds

( b_{1} = x + f iff for s being Element of X holds b_{1} . s = (f . s) + x )

x + f is Function of X,INT

for b_{1} being Function of X,INT holds

( b_{1} = f - x iff for s being Element of X holds b_{1} . s = (f . s) - x )

f - x is Function of X,INT

for b_{1} being Function of X,INT holds

( b_{1} = f * x iff for s being Element of X holds b_{1} . s = (f . s) * x )

f * x is Function of X,INT

end;
let f be Function of X,INT;

let x be Integer;

:: original: +

redefine func f + x -> Function of X,INT means :Def8: :: AOFA_I00:def 8

for s being Element of X holds it . s = (f . s) + x;

compatibility redefine func f + x -> Function of X,INT means :Def8: :: AOFA_I00:def 8

for s being Element of X holds it . s = (f . s) + x;

for b

( b

proof end;

coherence x + f is Function of X,INT

proof end;

:: original: -

redefine func f - x -> Function of X,INT means :: AOFA_I00:def 9

for s being Element of X holds it . s = (f . s) - x;

compatibility redefine func f - x -> Function of X,INT means :: AOFA_I00:def 9

for s being Element of X holds it . s = (f . s) - x;

for b

( b

proof end;

coherence f - x is Function of X,INT

proof end;

:: original: *

redefine func f * x -> Function of X,INT means :Def10: :: AOFA_I00:def 10

for s being Element of X holds it . s = (f . s) * x;

compatibility redefine func f * x -> Function of X,INT means :Def10: :: AOFA_I00:def 10

for s being Element of X holds it . s = (f . s) * x;

for b

( b

proof end;

coherence f * x is Function of X,INT

proof end;

:: deftheorem Def8 defines + AOFA_I00:def 8 :

for X being non empty set

for f being Function of X,INT

for x being Integer

for b_{4} being Function of X,INT holds

( b_{4} = f + x iff for s being Element of X holds b_{4} . s = (f . s) + x );

for X being non empty set

for f being Function of X,INT

for x being Integer

for b

( b

:: deftheorem defines - AOFA_I00:def 9 :

for X being non empty set

for f being Function of X,INT

for x being Integer

for b_{4} being Function of X,INT holds

( b_{4} = f - x iff for s being Element of X holds b_{4} . s = (f . s) - x );

for X being non empty set

for f being Function of X,INT

for x being Integer

for b

( b

:: deftheorem Def10 defines * AOFA_I00:def 10 :

for X being non empty set

for f being Function of X,INT

for x being Integer

for b_{4} being Function of X,INT holds

( b_{4} = f * x iff for s being Element of X holds b_{4} . s = (f . s) * x );

for X being non empty set

for f being Function of X,INT

for x being Integer

for b

( b

definition

let X be set ;

let f, g be Function of X,INT;

:: original: div

redefine func f div g -> Function of X,INT;

coherence

f div g is Function of X,INT

redefine func f mod g -> Function of X,INT;

coherence

f mod g is Function of X,INT

redefine func leq (f,g) -> Function of X,INT;

coherence

leq (f,g) is Function of X,INT

redefine func gt (f,g) -> Function of X,INT;

coherence

gt (f,g) is Function of X,INT

redefine func eq (f,g) -> Function of X,INT;

coherence

eq (f,g) is Function of X,INT

end;
let f, g be Function of X,INT;

:: original: div

redefine func f div g -> Function of X,INT;

coherence

f div g is Function of X,INT

proof end;

:: original: modredefine func f mod g -> Function of X,INT;

coherence

f mod g is Function of X,INT

proof end;

:: original: leqredefine func leq (f,g) -> Function of X,INT;

coherence

leq (f,g) is Function of X,INT

proof end;

:: original: gtredefine func gt (f,g) -> Function of X,INT;

coherence

gt (f,g) is Function of X,INT

proof end;

:: original: eqredefine func eq (f,g) -> Function of X,INT;

coherence

eq (f,g) is Function of X,INT

proof end;

definition

let X be non empty set ;

let t1, t2 be Function of X,INT;

for b_{1} being Function of X,INT holds

( b_{1} = t1 - t2 iff for s being Element of X holds b_{1} . s = (t1 . s) - (t2 . s) )

t1 - t2 is Function of X,INT

for b_{1} being Function of X,INT holds

( b_{1} = t1 + t2 iff for s being Element of X holds b_{1} . s = (t1 . s) + (t2 . s) )

t1 + t2 is Function of X,INT

end;
let t1, t2 be Function of X,INT;

:: original: -

redefine func t1 - t2 -> Function of X,INT means :Def11: :: AOFA_I00:def 11

for s being Element of X holds it . s = (t1 . s) - (t2 . s);

compatibility redefine func t1 - t2 -> Function of X,INT means :Def11: :: AOFA_I00:def 11

for s being Element of X holds it . s = (t1 . s) - (t2 . s);

for b

( b

proof end;

coherence t1 - t2 is Function of X,INT

proof end;

:: original: +

redefine func t1 + t2 -> Function of X,INT means :: AOFA_I00:def 12

for s being Element of X holds it . s = (t1 . s) + (t2 . s);

compatibility redefine func t1 + t2 -> Function of X,INT means :: AOFA_I00:def 12

for s being Element of X holds it . s = (t1 . s) + (t2 . s);

for b

( b

proof end;

coherence t1 + t2 is Function of X,INT

proof end;

:: deftheorem Def11 defines - AOFA_I00:def 11 :

for X being non empty set

for t1, t2, b_{4} being Function of X,INT holds

( b_{4} = t1 - t2 iff for s being Element of X holds b_{4} . s = (t1 . s) - (t2 . s) );

for X being non empty set

for t1, t2, b

( b

:: deftheorem defines + AOFA_I00:def 12 :

for X being non empty set

for t1, t2, b_{4} being Function of X,INT holds

( b_{4} = t1 + t2 iff for s being Element of X holds b_{4} . s = (t1 . s) + (t2 . s) );

for X being non empty set

for t1, t2, b

( b

registration
end;

definition

let N be set ;

let v, f be Function;

for b_{1}, b_{2} being Function st ex Y being set st

( ( for y being set holds

( y in Y iff ex h being Function st

( h in dom v & y in rng h ) ) ) & ( for a being set holds

( a in dom b_{1} iff ( a in Funcs (N,Y) & ex g being Function st

( a = g & g * f in dom v ) ) ) ) ) & ( for g being Function st g in dom b_{1} holds

b_{1} . g = v . (g * f) ) & ex Y being set st

( ( for y being set holds

( y in Y iff ex h being Function st

( h in dom v & y in rng h ) ) ) & ( for a being set holds

( a in dom b_{2} iff ( a in Funcs (N,Y) & ex g being Function st

( a = g & g * f in dom v ) ) ) ) ) & ( for g being Function st g in dom b_{2} holds

b_{2} . g = v . (g * f) ) holds

b_{1} = b_{2}

ex b_{1} being Function st

( ex Y being set st

( ( for y being set holds

( y in Y iff ex h being Function st

( h in dom v & y in rng h ) ) ) & ( for a being set holds

( a in dom b_{1} iff ( a in Funcs (N,Y) & ex g being Function st

( a = g & g * f in dom v ) ) ) ) ) & ( for g being Function st g in dom b_{1} holds

b_{1} . g = v . (g * f) ) )

end;
let v, f be Function;

func v ** (f,N) -> Function means :Def13: :: AOFA_I00:def 13

( ex Y being set st

( ( for y being set holds

( y in Y iff ex h being Function st

( h in dom v & y in rng h ) ) ) & ( for a being set holds

( a in dom it iff ( a in Funcs (N,Y) & ex g being Function st

( a = g & g * f in dom v ) ) ) ) ) & ( for g being Function st g in dom it holds

it . g = v . (g * f) ) );

uniqueness ( ex Y being set st

( ( for y being set holds

( y in Y iff ex h being Function st

( h in dom v & y in rng h ) ) ) & ( for a being set holds

( a in dom it iff ( a in Funcs (N,Y) & ex g being Function st

( a = g & g * f in dom v ) ) ) ) ) & ( for g being Function st g in dom it holds

it . g = v . (g * f) ) );

for b

( ( for y being set holds

( y in Y iff ex h being Function st

( h in dom v & y in rng h ) ) ) & ( for a being set holds

( a in dom b

( a = g & g * f in dom v ) ) ) ) ) & ( for g being Function st g in dom b

b

( ( for y being set holds

( y in Y iff ex h being Function st

( h in dom v & y in rng h ) ) ) & ( for a being set holds

( a in dom b

( a = g & g * f in dom v ) ) ) ) ) & ( for g being Function st g in dom b

b

b

proof end;

existence ex b

( ex Y being set st

( ( for y being set holds

( y in Y iff ex h being Function st

( h in dom v & y in rng h ) ) ) & ( for a being set holds

( a in dom b

( a = g & g * f in dom v ) ) ) ) ) & ( for g being Function st g in dom b

b

proof end;

:: deftheorem Def13 defines ** AOFA_I00:def 13 :

for N being set

for v, f, b_{4} being Function holds

( b_{4} = v ** (f,N) iff ( ex Y being set st

( ( for y being set holds

( y in Y iff ex h being Function st

( h in dom v & y in rng h ) ) ) & ( for a being set holds

( a in dom b_{4} iff ( a in Funcs (N,Y) & ex g being Function st

( a = g & g * f in dom v ) ) ) ) ) & ( for g being Function st g in dom b_{4} holds

b_{4} . g = v . (g * f) ) ) );

for N being set

for v, f, b

( b

( ( for y being set holds

( y in Y iff ex h being Function st

( h in dom v & y in rng h ) ) ) & ( for a being set holds

( a in dom b

( a = g & g * f in dom v ) ) ) ) ) & ( for g being Function st g in dom b

b

definition

let X, Y, Z, N be non empty set ;

let v be Element of Funcs ((Funcs (X,Y)),Z);

let f be Function of X,N;

:: original: **

redefine func v ** (f,N) -> Element of Funcs ((Funcs (N,Y)),Z);

coherence

v ** (f,N) is Element of Funcs ((Funcs (N,Y)),Z)

end;
let v be Element of Funcs ((Funcs (X,Y)),Z);

let f be Function of X,N;

:: original: **

redefine func v ** (f,N) -> Element of Funcs ((Funcs (N,Y)),Z);

coherence

v ** (f,N) is Element of Funcs ((Funcs (N,Y)),Z)

proof end;

theorem Th4: :: AOFA_I00:4

for X, N, I being non empty set

for s being Function of X,I

for c being Function of X,N st c is one-to-one holds

for n being Element of I holds (N --> n) +* (s * (c ")) is Function of N,I

for s being Function of X,I

for c being Function of X,N st c is one-to-one holds

for n being Element of I holds (N --> n) +* (s * (c ")) is Function of N,I

proof end;

theorem Th5: :: AOFA_I00:5

for N, X, I being non empty set

for v1, v2 being Function st dom v1 = dom v2 & dom v1 = Funcs (X,I) holds

for f being Function of X,N st f is one-to-one & v1 ** (f,N) = v2 ** (f,N) holds

v1 = v2

for v1, v2 being Function st dom v1 = dom v2 & dom v1 = Funcs (X,I) holds

for f being Function of X,N st f is one-to-one & v1 ** (f,N) = v2 ** (f,N) holds

v1 = v2

proof end;

registration

let X be set ;

ex b_{1} being Function of X,(card X) st

( b_{1} is one-to-one & b_{1} is onto )

ex b_{1} being Function of (card X),X st

( b_{1} is one-to-one & b_{1} is onto )

end;
cluster Relation-like X -defined card X -valued Function-like one-to-one quasi_total onto for Element of bool [:X,(card X):];

existence ex b

( b

proof end;

cluster Relation-like card X -defined X -valued Function-like one-to-one quasi_total onto for Element of bool [:(card X),X:];

existence ex b

( b

proof end;

definition

let X be set ;

mode Enumeration of X is one-to-one onto Function of X,(card X);

mode Denumeration of X is one-to-one onto Function of (card X),X;

end;
mode Enumeration of X is one-to-one onto Function of X,(card X);

mode Denumeration of X is one-to-one onto Function of (card X),X;

theorem Th6: :: AOFA_I00:6

for X being set

for f being Function holds

( f is Enumeration of X iff ( dom f = X & rng f = card X & f is one-to-one ) )

for f being Function holds

( f is Enumeration of X iff ( dom f = X & rng f = card X & f is one-to-one ) )

proof end;

theorem Th7: :: AOFA_I00:7

for X being set

for f being Function holds

( f is Denumeration of X iff ( dom f = card X & rng f = X & f is one-to-one ) )

for f being Function holds

( f is Denumeration of X iff ( dom f = card X & rng f = X & f is one-to-one ) )

proof end;

theorem Th8: :: AOFA_I00:8

for X being non empty set

for x, y being Element of X

for f being Enumeration of X holds (f +* (x,(f . y))) +* (y,(f . x)) is Enumeration of X

for x, y being Element of X

for f being Enumeration of X holds (f +* (x,(f . y))) +* (y,(f . x)) is Enumeration of X

proof end;

theorem :: AOFA_I00:10

definition

let X be set ;

let f be Enumeration of X;

:: original: "

redefine func f " -> Denumeration of X;

coherence

f " is Denumeration of X

end;
let f be Enumeration of X;

:: original: "

redefine func f " -> Denumeration of X;

coherence

f " is Denumeration of X

proof end;

definition

let X be set ;

let f be Denumeration of X;

:: original: "

redefine func f " -> Enumeration of X;

coherence

f " is Enumeration of X

end;
let f be Denumeration of X;

:: original: "

redefine func f " -> Enumeration of X;

coherence

f " is Enumeration of X

proof end;

theorem :: AOFA_I00:13

definition

let X be non empty set ;

mode INT-Variable of X is Function of (Funcs (X,INT)),X;

mode INT-Expression of X is Function of (Funcs (X,INT)),INT;

mode INT-Array of X is Function of INT,X;

end;
mode INT-Variable of X is Function of (Funcs (X,INT)),X;

mode INT-Expression of X is Function of (Funcs (X,INT)),INT;

mode INT-Array of X is Function of INT,X;

definition

let A be preIfWhileAlgebra;

let I be Element of A;

let X be non empty set ;

let T be Subset of (Funcs (X,INT));

let f be ExecutionFunction of A, Funcs (X,INT),T;

end;
let I be Element of A;

let X be non empty set ;

let T be Subset of (Funcs (X,INT));

let f be ExecutionFunction of A, Funcs (X,INT),T;

pred I is_assignment_wrt A,X,f means :: AOFA_I00:def 14

( I in ElementaryInstructions A & ex v being INT-Variable of X ex t being INT-Expression of X st

for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) );

( I in ElementaryInstructions A & ex v being INT-Variable of X ex t being INT-Expression of X st

for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) );

:: deftheorem defines is_assignment_wrt AOFA_I00:def 14 :

for A being preIfWhileAlgebra

for I being Element of A

for X being non empty set

for T being Subset of (Funcs (X,INT))

for f being ExecutionFunction of A, Funcs (X,INT),T holds

( I is_assignment_wrt A,X,f iff ( I in ElementaryInstructions A & ex v being INT-Variable of X ex t being INT-Expression of X st

for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) ) );

for A being preIfWhileAlgebra

for I being Element of A

for X being non empty set

for T being Subset of (Funcs (X,INT))

for f being ExecutionFunction of A, Funcs (X,INT),T holds

( I is_assignment_wrt A,X,f iff ( I in ElementaryInstructions A & ex v being INT-Variable of X ex t being INT-Expression of X st

for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) ) );

definition

let A be preIfWhileAlgebra;

let X be non empty set ;

let T be Subset of (Funcs (X,INT));

let f be ExecutionFunction of A, Funcs (X,INT),T;

let v be INT-Variable of X;

let t be INT-Expression of X;

end;
let X be non empty set ;

let T be Subset of (Funcs (X,INT));

let f be ExecutionFunction of A, Funcs (X,INT),T;

let v be INT-Variable of X;

let t be INT-Expression of X;

pred v,t form_assignment_wrt f means :: AOFA_I00:def 15

ex I being Element of A st

( I in ElementaryInstructions A & ( for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) ) );

ex I being Element of A st

( I in ElementaryInstructions A & ( for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) ) );

:: deftheorem defines form_assignment_wrt AOFA_I00:def 15 :

for A being preIfWhileAlgebra

for X being non empty set

for T being Subset of (Funcs (X,INT))

for f being ExecutionFunction of A, Funcs (X,INT),T

for v being INT-Variable of X

for t being INT-Expression of X holds

( v,t form_assignment_wrt f iff ex I being Element of A st

( I in ElementaryInstructions A & ( for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) ) ) );

for A being preIfWhileAlgebra

for X being non empty set

for T being Subset of (Funcs (X,INT))

for f being ExecutionFunction of A, Funcs (X,INT),T

for v being INT-Variable of X

for t being INT-Expression of X holds

( v,t form_assignment_wrt f iff ex I being Element of A st

( I in ElementaryInstructions A & ( for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) ) ) );

definition

let A be preIfWhileAlgebra;

let X be non empty set ;

let T be Subset of (Funcs (X,INT));

let f be ExecutionFunction of A, Funcs (X,INT),T;

assume A1: ex I being Element of A st I is_assignment_wrt A,X,f ;

ex b_{1} being INT-Variable of X ex t being INT-Expression of X st b_{1},t form_assignment_wrt f

end;
let X be non empty set ;

let T be Subset of (Funcs (X,INT));

let f be ExecutionFunction of A, Funcs (X,INT),T;

assume A1: ex I being Element of A st I is_assignment_wrt A,X,f ;

mode INT-Variable of A,f -> INT-Variable of X means :: AOFA_I00:def 16

ex t being INT-Expression of X st it,t form_assignment_wrt f;

existence ex t being INT-Expression of X st it,t form_assignment_wrt f;

ex b

proof end;

:: deftheorem defines INT-Variable AOFA_I00:def 16 :

for A being preIfWhileAlgebra

for X being non empty set

for T being Subset of (Funcs (X,INT))

for f being ExecutionFunction of A, Funcs (X,INT),T st ex I being Element of A st I is_assignment_wrt A,X,f holds

for b_{5} being INT-Variable of X holds

( b_{5} is INT-Variable of A,f iff ex t being INT-Expression of X st b_{5},t form_assignment_wrt f );

for A being preIfWhileAlgebra

for X being non empty set

for T being Subset of (Funcs (X,INT))

for f being ExecutionFunction of A, Funcs (X,INT),T st ex I being Element of A st I is_assignment_wrt A,X,f holds

for b

( b

definition

let A be preIfWhileAlgebra;

let X be non empty set ;

let T be Subset of (Funcs (X,INT));

let f be ExecutionFunction of A, Funcs (X,INT),T;

assume A1: ex I being Element of A st I is_assignment_wrt A,X,f ;

ex b_{1} being INT-Expression of X ex v being INT-Variable of X st v,b_{1} form_assignment_wrt f

end;
let X be non empty set ;

let T be Subset of (Funcs (X,INT));

let f be ExecutionFunction of A, Funcs (X,INT),T;

assume A1: ex I being Element of A st I is_assignment_wrt A,X,f ;

mode INT-Expression of A,f -> INT-Expression of X means :: AOFA_I00:def 17

ex v being INT-Variable of X st v,it form_assignment_wrt f;

existence ex v being INT-Variable of X st v,it form_assignment_wrt f;

ex b

proof end;

:: deftheorem defines INT-Expression AOFA_I00:def 17 :

for A being preIfWhileAlgebra

for X being non empty set

for T being Subset of (Funcs (X,INT))

for f being ExecutionFunction of A, Funcs (X,INT),T st ex I being Element of A st I is_assignment_wrt A,X,f holds

for b_{5} being INT-Expression of X holds

( b_{5} is INT-Expression of A,f iff ex v being INT-Variable of X st v,b_{5} form_assignment_wrt f );

for A being preIfWhileAlgebra

for X being non empty set

for T being Subset of (Funcs (X,INT))

for f being ExecutionFunction of A, Funcs (X,INT),T st ex I being Element of A st I is_assignment_wrt A,X,f holds

for b

( b

definition

let X, Y be non empty set ;

let f be Element of Funcs (X,Y);

let x be Element of X;

:: original: .

redefine func f . x -> Element of Y;

coherence

f . x is Element of Y

end;
let f be Element of Funcs (X,Y);

let x be Element of X;

:: original: .

redefine func f . x -> Element of Y;

coherence

f . x is Element of Y

proof end;

definition

let X be non empty set ;

let x be Element of X;

existence

ex b_{1} being INT-Expression of X st

for s being Element of Funcs (X,INT) holds b_{1} . s = s . x;

uniqueness

for b_{1}, b_{2} being INT-Expression of X st ( for s being Element of Funcs (X,INT) holds b_{1} . s = s . x ) & ( for s being Element of Funcs (X,INT) holds b_{2} . s = s . x ) holds

b_{1} = b_{2};

end;
let x be Element of X;

func . x -> INT-Expression of X means :Def18: :: AOFA_I00:def 18

for s being Element of Funcs (X,INT) holds it . s = s . x;

correctness for s being Element of Funcs (X,INT) holds it . s = s . x;

existence

ex b

for s being Element of Funcs (X,INT) holds b

uniqueness

for b

b

proof end;

:: deftheorem Def18 defines . AOFA_I00:def 18 :

for X being non empty set

for x being Element of X

for b_{3} being INT-Expression of X holds

( b_{3} = . x iff for s being Element of Funcs (X,INT) holds b_{3} . s = s . x );

for X being non empty set

for x being Element of X

for b

( b

definition

let X be non empty set ;

let v be INT-Variable of X;

existence

ex b_{1} being INT-Expression of X st

for s being Element of Funcs (X,INT) holds b_{1} . s = s . (v . s);

uniqueness

for b_{1}, b_{2} being INT-Expression of X st ( for s being Element of Funcs (X,INT) holds b_{1} . s = s . (v . s) ) & ( for s being Element of Funcs (X,INT) holds b_{2} . s = s . (v . s) ) holds

b_{1} = b_{2};

end;
let v be INT-Variable of X;

func . v -> INT-Expression of X means :Def19: :: AOFA_I00:def 19

for s being Element of Funcs (X,INT) holds it . s = s . (v . s);

correctness for s being Element of Funcs (X,INT) holds it . s = s . (v . s);

existence

ex b

for s being Element of Funcs (X,INT) holds b

uniqueness

for b

b

proof end;

:: deftheorem Def19 defines . AOFA_I00:def 19 :

for X being non empty set

for v being INT-Variable of X

for b_{3} being INT-Expression of X holds

( b_{3} = . v iff for s being Element of Funcs (X,INT) holds b_{3} . s = s . (v . s) );

for X being non empty set

for v being INT-Variable of X

for b

( b

definition

let X be non empty set ;

let x be Element of X;

correctness

coherence

(Funcs (X,INT)) --> x is INT-Variable of X;

;

end;
let x be Element of X;

correctness

coherence

(Funcs (X,INT)) --> x is INT-Variable of X;

;

:: deftheorem defines ^ AOFA_I00:def 20 :

for X being non empty set

for x being Element of X holds ^ x = (Funcs (X,INT)) --> x;

for X being non empty set

for x being Element of X holds ^ x = (Funcs (X,INT)) --> x;

definition

let X be non empty set ;

let i be Integer;

correctness

coherence

(Funcs (X,INT)) --> i is INT-Expression of X;

end;
let i be Integer;

correctness

coherence

(Funcs (X,INT)) --> i is INT-Expression of X;

proof end;

:: deftheorem defines . AOFA_I00:def 21 :

for X being non empty set

for i being Integer holds . (i,X) = (Funcs (X,INT)) --> i;

for X being non empty set

for i being Integer holds . (i,X) = (Funcs (X,INT)) --> i;

theorem :: AOFA_I00:15

for X being non empty set

for t being INT-Expression of X holds

( t + (. (0,X)) = t & t (#) (. (1,X)) = t )

for t being INT-Expression of X holds

( t + (. (0,X)) = t & t (#) (. (1,X)) = t )

proof end;

definition

let A be preIfWhileAlgebra;

let X be non empty set ;

let T be Subset of (Funcs (X,INT));

let f be ExecutionFunction of A, Funcs (X,INT),T;

end;
let X be non empty set ;

let T be Subset of (Funcs (X,INT));

let f be ExecutionFunction of A, Funcs (X,INT),T;

attr f is Euclidean means :Def22: :: AOFA_I00:def 22

( ( for v being INT-Variable of A,f

for t being INT-Expression of A,f holds v,t form_assignment_wrt f ) & ( for i being Integer holds . (i,X) is INT-Expression of A,f ) & ( for v being INT-Variable of A,f holds . v is INT-Expression of A,f ) & ( for x being Element of X holds ^ x is INT-Variable of A,f ) & ex a being INT-Array of X st

( a | (card X) is one-to-one & ( for t being INT-Expression of A,f holds a * t is INT-Variable of A,f ) ) & ( for t being INT-Expression of A,f holds - t is INT-Expression of A,f ) & ( for t1, t2 being INT-Expression of A,f holds

( t1 (#) t2 is INT-Expression of A,f & t1 + t2 is INT-Expression of A,f & t1 div t2 is INT-Expression of A,f & t1 mod t2 is INT-Expression of A,f & leq (t1,t2) is INT-Expression of A,f & gt (t1,t2) is INT-Expression of A,f ) ) );

( ( for v being INT-Variable of A,f

for t being INT-Expression of A,f holds v,t form_assignment_wrt f ) & ( for i being Integer holds . (i,X) is INT-Expression of A,f ) & ( for v being INT-Variable of A,f holds . v is INT-Expression of A,f ) & ( for x being Element of X holds ^ x is INT-Variable of A,f ) & ex a being INT-Array of X st

( a | (card X) is one-to-one & ( for t being INT-Expression of A,f holds a * t is INT-Variable of A,f ) ) & ( for t being INT-Expression of A,f holds - t is INT-Expression of A,f ) & ( for t1, t2 being INT-Expression of A,f holds

( t1 (#) t2 is INT-Expression of A,f & t1 + t2 is INT-Expression of A,f & t1 div t2 is INT-Expression of A,f & t1 mod t2 is INT-Expression of A,f & leq (t1,t2) is INT-Expression of A,f & gt (t1,t2) is INT-Expression of A,f ) ) );

:: deftheorem Def22 defines Euclidean AOFA_I00:def 22 :

for A being preIfWhileAlgebra

for X being non empty set

for T being Subset of (Funcs (X,INT))

for f being ExecutionFunction of A, Funcs (X,INT),T holds

( f is Euclidean iff ( ( for v being INT-Variable of A,f

for t being INT-Expression of A,f holds v,t form_assignment_wrt f ) & ( for i being Integer holds . (i,X) is INT-Expression of A,f ) & ( for v being INT-Variable of A,f holds . v is INT-Expression of A,f ) & ( for x being Element of X holds ^ x is INT-Variable of A,f ) & ex a being INT-Array of X st

( a | (card X) is one-to-one & ( for t being INT-Expression of A,f holds a * t is INT-Variable of A,f ) ) & ( for t being INT-Expression of A,f holds - t is INT-Expression of A,f ) & ( for t1, t2 being INT-Expression of A,f holds

( t1 (#) t2 is INT-Expression of A,f & t1 + t2 is INT-Expression of A,f & t1 div t2 is INT-Expression of A,f & t1 mod t2 is INT-Expression of A,f & leq (t1,t2) is INT-Expression of A,f & gt (t1,t2) is INT-Expression of A,f ) ) ) );

for A being preIfWhileAlgebra

for X being non empty set

for T being Subset of (Funcs (X,INT))

for f being ExecutionFunction of A, Funcs (X,INT),T holds

( f is Euclidean iff ( ( for v being INT-Variable of A,f

for t being INT-Expression of A,f holds v,t form_assignment_wrt f ) & ( for i being Integer holds . (i,X) is INT-Expression of A,f ) & ( for v being INT-Variable of A,f holds . v is INT-Expression of A,f ) & ( for x being Element of X holds ^ x is INT-Variable of A,f ) & ex a being INT-Array of X st

( a | (card X) is one-to-one & ( for t being INT-Expression of A,f holds a * t is INT-Variable of A,f ) ) & ( for t being INT-Expression of A,f holds - t is INT-Expression of A,f ) & ( for t1, t2 being INT-Expression of A,f holds

( t1 (#) t2 is INT-Expression of A,f & t1 + t2 is INT-Expression of A,f & t1 div t2 is INT-Expression of A,f & t1 mod t2 is INT-Expression of A,f & leq (t1,t2) is INT-Expression of A,f & gt (t1,t2) is INT-Expression of A,f ) ) ) );

:: Remark:

:: Incorrect definition of "mod" in INT_1: 5 mod 0 = 0 i 5 div 0 = 0

:: and 5 <> 0*(5 div 0)+(5 mod 0)

:: In our case "mod" is still expressible with "basic" operations

:: but in complicated way:

:: f1 mod f2

:: = (gt(f2,(dom f2)-->0)+gt((dom f2)-->0,f2))(#)(f1-f2(#)(f1 div f2))

:: To avoid complications "mod" is mentioned in the definition above.

:: Incorrect definition of "mod" in INT_1: 5 mod 0 = 0 i 5 div 0 = 0

:: and 5 <> 0*(5 div 0)+(5 mod 0)

:: In our case "mod" is still expressible with "basic" operations

:: but in complicated way:

:: f1 mod f2

:: = (gt(f2,(dom f2)-->0)+gt((dom f2)-->0,f2))(#)(f1-f2(#)(f1 div f2))

:: To avoid complications "mod" is mentioned in the definition above.

:: deftheorem Def23 defines Euclidean AOFA_I00:def 23 :

for A being preIfWhileAlgebra holds

( A is Euclidean iff for X being non empty countable set

for T being Subset of (Funcs (X,INT)) ex f being ExecutionFunction of A, Funcs (X,INT),T st f is Euclidean );

for A being preIfWhileAlgebra holds

( A is Euclidean iff for X being non empty countable set

for T being Subset of (Funcs (X,INT)) ex f being ExecutionFunction of A, Funcs (X,INT),T st f is Euclidean );

definition

[:(Funcs ((Funcs (NAT,INT)),NAT)),(Funcs ((Funcs (NAT,INT)),INT)):] is infinite disjoint_with_NAT set ;

end;

func INT-ElemIns -> infinite disjoint_with_NAT set equals :: AOFA_I00:def 24

[:(Funcs ((Funcs (NAT,INT)),NAT)),(Funcs ((Funcs (NAT,INT)),INT)):];

coherence [:(Funcs ((Funcs (NAT,INT)),NAT)),(Funcs ((Funcs (NAT,INT)),INT)):];

[:(Funcs ((Funcs (NAT,INT)),NAT)),(Funcs ((Funcs (NAT,INT)),INT)):] is infinite disjoint_with_NAT set ;

:: deftheorem defines INT-ElemIns AOFA_I00:def 24 :

INT-ElemIns = [:(Funcs ((Funcs (NAT,INT)),NAT)),(Funcs ((Funcs (NAT,INT)),INT)):];

INT-ElemIns = [:(Funcs ((Funcs (NAT,INT)),NAT)),(Funcs ((Funcs (NAT,INT)),INT)):];

definition

ex b_{1} being ExecutionFunction of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns), Funcs (NAT,INT),(Funcs (NAT,INT)) \ (0,0) st

for s being Element of Funcs (NAT,INT)

for v being Element of Funcs ((Funcs (NAT,INT)),NAT)

for e being Element of Funcs ((Funcs (NAT,INT)),INT) holds b_{1} . (s,(root-tree [v,e])) = s +* ((v . s),(e . s))
end;

mode INT-Exec -> ExecutionFunction of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns), Funcs (NAT,INT),(Funcs (NAT,INT)) \ (0,0) means :Def25: :: AOFA_I00:def 25

for s being Element of Funcs (NAT,INT)

for v being Element of Funcs ((Funcs (NAT,INT)),NAT)

for e being Element of Funcs ((Funcs (NAT,INT)),INT) holds it . (s,(root-tree [v,e])) = s +* ((v . s),(e . s));

existence for s being Element of Funcs (NAT,INT)

for v being Element of Funcs ((Funcs (NAT,INT)),NAT)

for e being Element of Funcs ((Funcs (NAT,INT)),INT) holds it . (s,(root-tree [v,e])) = s +* ((v . s),(e . s));

ex b

for s being Element of Funcs (NAT,INT)

for v being Element of Funcs ((Funcs (NAT,INT)),NAT)

for e being Element of Funcs ((Funcs (NAT,INT)),INT) holds b

proof end;

:: deftheorem Def25 defines INT-Exec AOFA_I00:def 25 :

for b_{1} being ExecutionFunction of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns), Funcs (NAT,INT),(Funcs (NAT,INT)) \ (0,0) holds

( b_{1} is INT-Exec iff for s being Element of Funcs (NAT,INT)

for v being Element of Funcs ((Funcs (NAT,INT)),NAT)

for e being Element of Funcs ((Funcs (NAT,INT)),INT) holds b_{1} . (s,(root-tree [v,e])) = s +* ((v . s),(e . s)) );

for b

( b

for v being Element of Funcs ((Funcs (NAT,INT)),NAT)

for e being Element of Funcs ((Funcs (NAT,INT)),INT) holds b

definition

let X be non empty set ;

[:(Funcs ((Funcs (X,INT)),X)),(Funcs ((Funcs (X,INT)),INT)):] is infinite disjoint_with_NAT set ;

end;
func INT-ElemIns X -> infinite disjoint_with_NAT set equals :: AOFA_I00:def 26

[:(Funcs ((Funcs (X,INT)),X)),(Funcs ((Funcs (X,INT)),INT)):];

coherence [:(Funcs ((Funcs (X,INT)),X)),(Funcs ((Funcs (X,INT)),INT)):];

[:(Funcs ((Funcs (X,INT)),X)),(Funcs ((Funcs (X,INT)),INT)):] is infinite disjoint_with_NAT set ;

:: deftheorem defines INT-ElemIns AOFA_I00:def 26 :

for X being non empty set holds INT-ElemIns X = [:(Funcs ((Funcs (X,INT)),X)),(Funcs ((Funcs (X,INT)),INT)):];

for X being non empty set holds INT-ElemIns X = [:(Funcs ((Funcs (X,INT)),X)),(Funcs ((Funcs (X,INT)),INT)):];

definition

let X be non empty set ;

let x be Element of X;

ex b_{1} being ExecutionFunction of FreeUnivAlgNSG (ECIW-signature,(INT-ElemIns X)), Funcs (X,INT),(Funcs (X,INT)) \ (x,0) st

for s being Element of Funcs (X,INT)

for v being Element of Funcs ((Funcs (X,INT)),X)

for e being Element of Funcs ((Funcs (X,INT)),INT) holds b_{1} . (s,(root-tree [v,e])) = s +* ((v . s),(e . s))

end;
let x be Element of X;

mode INT-Exec of x -> ExecutionFunction of FreeUnivAlgNSG (ECIW-signature,(INT-ElemIns X)), Funcs (X,INT),(Funcs (X,INT)) \ (x,0) means :: AOFA_I00:def 27

for s being Element of Funcs (X,INT)

for v being Element of Funcs ((Funcs (X,INT)),X)

for e being Element of Funcs ((Funcs (X,INT)),INT) holds it . (s,(root-tree [v,e])) = s +* ((v . s),(e . s));

existence for s being Element of Funcs (X,INT)

for v being Element of Funcs ((Funcs (X,INT)),X)

for e being Element of Funcs ((Funcs (X,INT)),INT) holds it . (s,(root-tree [v,e])) = s +* ((v . s),(e . s));

ex b

for s being Element of Funcs (X,INT)

for v being Element of Funcs ((Funcs (X,INT)),X)

for e being Element of Funcs ((Funcs (X,INT)),INT) holds b

proof end;

:: deftheorem defines INT-Exec AOFA_I00:def 27 :

for X being non empty set

for x being Element of X

for b_{3} being ExecutionFunction of FreeUnivAlgNSG (ECIW-signature,(INT-ElemIns X)), Funcs (X,INT),(Funcs (X,INT)) \ (x,0) holds

( b_{3} is INT-Exec of x iff for s being Element of Funcs (X,INT)

for v being Element of Funcs ((Funcs (X,INT)),X)

for e being Element of Funcs ((Funcs (X,INT)),INT) holds b_{3} . (s,(root-tree [v,e])) = s +* ((v . s),(e . s)) );

for X being non empty set

for x being Element of X

for b

( b

for v being Element of Funcs ((Funcs (X,INT)),X)

for e being Element of Funcs ((Funcs (X,INT)),INT) holds b

definition

let X be non empty set ;

let T be Subset of (Funcs (X,INT));

let c be Enumeration of X;

assume A1: rng c c= NAT ;

ex b_{1} being ExecutionFunction of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns), Funcs (X,INT),T st

for s being Element of Funcs (X,INT)

for v being Element of Funcs ((Funcs (X,INT)),X)

for e being Element of Funcs ((Funcs (X,INT)),INT) holds b_{1} . (s,(root-tree [((c * v) ** (c,NAT)),(e ** (c,NAT))])) = s +* ((v . s),(e . s))

end;
let T be Subset of (Funcs (X,INT));

let c be Enumeration of X;

assume A1: rng c c= NAT ;

mode INT-Exec of c,T -> ExecutionFunction of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns), Funcs (X,INT),T means :Def28: :: AOFA_I00:def 28

for s being Element of Funcs (X,INT)

for v being Element of Funcs ((Funcs (X,INT)),X)

for e being Element of Funcs ((Funcs (X,INT)),INT) holds it . (s,(root-tree [((c * v) ** (c,NAT)),(e ** (c,NAT))])) = s +* ((v . s),(e . s));

existence for s being Element of Funcs (X,INT)

for v being Element of Funcs ((Funcs (X,INT)),X)

for e being Element of Funcs ((Funcs (X,INT)),INT) holds it . (s,(root-tree [((c * v) ** (c,NAT)),(e ** (c,NAT))])) = s +* ((v . s),(e . s));

ex b

for s being Element of Funcs (X,INT)

for v being Element of Funcs ((Funcs (X,INT)),X)

for e being Element of Funcs ((Funcs (X,INT)),INT) holds b

proof end;

:: deftheorem Def28 defines INT-Exec AOFA_I00:def 28 :

for X being non empty set

for T being Subset of (Funcs (X,INT))

for c being Enumeration of X st rng c c= NAT holds

for b_{4} being ExecutionFunction of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns), Funcs (X,INT),T holds

( b_{4} is INT-Exec of c,T iff for s being Element of Funcs (X,INT)

for v being Element of Funcs ((Funcs (X,INT)),X)

for e being Element of Funcs ((Funcs (X,INT)),INT) holds b_{4} . (s,(root-tree [((c * v) ** (c,NAT)),(e ** (c,NAT))])) = s +* ((v . s),(e . s)) );

for X being non empty set

for T being Subset of (Funcs (X,INT))

for c being Enumeration of X st rng c c= NAT holds

for b

( b

for v being Element of Funcs ((Funcs (X,INT)),X)

for e being Element of Funcs ((Funcs (X,INT)),INT) holds b

theorem Th16: :: AOFA_I00:16

for f being INT-Exec

for v being INT-Variable of NAT

for t being INT-Expression of NAT holds v,t form_assignment_wrt f

for v being INT-Variable of NAT

for t being INT-Expression of NAT holds v,t form_assignment_wrt f

proof end;

theorem Th17: :: AOFA_I00:17

for f being INT-Exec

for v being INT-Variable of NAT holds v is INT-Variable of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f

for v being INT-Variable of NAT holds v is INT-Variable of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f

proof end;

theorem Th18: :: AOFA_I00:18

for f being INT-Exec

for t being INT-Expression of NAT holds t is INT-Expression of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f

for t being INT-Expression of NAT holds t is INT-Expression of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f

proof end;

theorem Th19: :: AOFA_I00:19

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for c being Enumeration of X

for f being INT-Exec of c,T

for v being INT-Variable of X

for t being INT-Expression of X holds v,t form_assignment_wrt f

for T being Subset of (Funcs (X,INT))

for c being Enumeration of X

for f being INT-Exec of c,T

for v being INT-Variable of X

for t being INT-Expression of X holds v,t form_assignment_wrt f

proof end;

theorem Th20: :: AOFA_I00:20

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for c being Enumeration of X

for f being INT-Exec of c,T

for v being INT-Variable of X holds v is INT-Variable of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f

for T being Subset of (Funcs (X,INT))

for c being Enumeration of X

for f being INT-Exec of c,T

for v being INT-Variable of X holds v is INT-Variable of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f

proof end;

theorem Th21: :: AOFA_I00:21

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for c being Enumeration of X

for f being INT-Exec of c,T

for t being INT-Expression of X holds t is INT-Expression of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f

for T being Subset of (Funcs (X,INT))

for c being Enumeration of X

for f being INT-Exec of c,T

for t being INT-Expression of X holds t is INT-Expression of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f

proof end;

registration

let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let c be Enumeration of X;

coherence

for b_{1} being INT-Exec of c,T holds b_{1} is Euclidean

end;
let T be Subset of (Funcs (X,INT));

let c be Enumeration of X;

coherence

for b

proof end;

registration

ex b_{1} being preIfWhileAlgebra st

( b_{1} is Euclidean & not b_{1} is degenerated )
end;

cluster non empty V161() V162() V163() with_empty-instruction with_catenation with_if-instruction with_while-instruction non degenerated Euclidean for L9();

existence ex b

( b

proof end;

registration

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

ex b_{1} being ExecutionFunction of A, Funcs (X,INT),T st b_{1} is Euclidean
by Def23;

end;
let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

cluster Relation-like [:(Funcs (X,INT)), the carrier of A:] -defined Funcs (X,INT) -valued non empty Function-like V31([:(Funcs (X,INT)), the carrier of A:]) quasi_total Function-yielding V93() complying_with_empty-instruction complying_with_catenation Euclidean for ExecutionFunction of A, Funcs (X,INT),T;

existence ex b

definition

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let t be INT-Expression of A,f;

:: original: -

redefine func - t -> INT-Expression of A,f;

coherence

- t is INT-Expression of A,f by Def22;

end;
let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let t be INT-Expression of A,f;

:: original: -

redefine func - t -> INT-Expression of A,f;

coherence

- t is INT-Expression of A,f by Def22;

definition

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let t be INT-Expression of A,f;

let i be Integer;

:: original: +

redefine func t + i -> INT-Expression of A,f;

coherence

i + t is INT-Expression of A,f

redefine func t - i -> INT-Expression of A,f;

coherence

t - i is INT-Expression of A,f

redefine func t * i -> INT-Expression of A,f;

coherence

t * i is INT-Expression of A,f

end;
let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let t be INT-Expression of A,f;

let i be Integer;

:: original: +

redefine func t + i -> INT-Expression of A,f;

coherence

i + t is INT-Expression of A,f

proof end;

:: original: -redefine func t - i -> INT-Expression of A,f;

coherence

t - i is INT-Expression of A,f

proof end;

:: original: *redefine func t * i -> INT-Expression of A,f;

coherence

t * i is INT-Expression of A,f

proof end;

definition

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let t1, t2 be INT-Expression of A,f;

:: original: -

redefine func t1 - t2 -> INT-Expression of A,f;

coherence

t1 - t2 is INT-Expression of A,f

redefine func t1 + t2 -> INT-Expression of A,f;

coherence

t1 + t2 is INT-Expression of A,f by Def22;

:: original: (#)

redefine func t1 (#) t2 -> INT-Expression of A,f;

coherence

t1 (#) t2 is INT-Expression of A,f by Def22;

end;
let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let t1, t2 be INT-Expression of A,f;

:: original: -

redefine func t1 - t2 -> INT-Expression of A,f;

coherence

t1 - t2 is INT-Expression of A,f

proof end;

:: original: +redefine func t1 + t2 -> INT-Expression of A,f;

coherence

t1 + t2 is INT-Expression of A,f by Def22;

:: original: (#)

redefine func t1 (#) t2 -> INT-Expression of A,f;

coherence

t1 (#) t2 is INT-Expression of A,f by Def22;

definition

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let t1, t2 be INT-Expression of A,f;

t1 div t2 is INT-Expression of A,f by Def22;

compatibility

for b_{1} being INT-Expression of A,f holds

( b_{1} = t1 div t2 iff for s being Element of Funcs (X,INT) holds b_{1} . s = (t1 . s) div (t2 . s) )

t1 mod t2 is INT-Expression of A,f by Def22;

compatibility

for b_{1} being INT-Expression of A,f holds

( b_{1} = t1 mod t2 iff for s being Element of Funcs (X,INT) holds b_{1} . s = (t1 . s) mod (t2 . s) )

for b_{1} being INT-Expression of A,f holds

( b_{1} = leq (t1,t2) iff for s being Element of Funcs (X,INT) holds b_{1} . s = IFGT ((t1 . s),(t2 . s),0,1) )

leq (t1,t2) is INT-Expression of A,f by Def22;

gt (t1,t2) is INT-Expression of A,f by Def22;

compatibility

for b_{1} being INT-Expression of A,f holds

( b_{1} = gt (t1,t2) iff for s being Element of Funcs (X,INT) holds b_{1} . s = IFGT ((t1 . s),(t2 . s),1,0) )

end;
let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let t1, t2 be INT-Expression of A,f;

:: original: div

redefine func t1 div t2 -> INT-Expression of A,f means :Def29: :: AOFA_I00:def 29

for s being Element of Funcs (X,INT) holds it . s = (t1 . s) div (t2 . s);

coherence redefine func t1 div t2 -> INT-Expression of A,f means :Def29: :: AOFA_I00:def 29

for s being Element of Funcs (X,INT) holds it . s = (t1 . s) div (t2 . s);

t1 div t2 is INT-Expression of A,f by Def22;

compatibility

for b

( b

proof end;

:: original: mod

redefine func t1 mod t2 -> INT-Expression of A,f means :Def30: :: AOFA_I00:def 30

for s being Element of Funcs (X,INT) holds it . s = (t1 . s) mod (t2 . s);

coherence redefine func t1 mod t2 -> INT-Expression of A,f means :Def30: :: AOFA_I00:def 30

for s being Element of Funcs (X,INT) holds it . s = (t1 . s) mod (t2 . s);

t1 mod t2 is INT-Expression of A,f by Def22;

compatibility

for b

( b

proof end;

:: original: leq

redefine func leq (t1,t2) -> INT-Expression of A,f means :Def31: :: AOFA_I00:def 31

for s being Element of Funcs (X,INT) holds it . s = IFGT ((t1 . s),(t2 . s),0,1);

compatibility redefine func leq (t1,t2) -> INT-Expression of A,f means :Def31: :: AOFA_I00:def 31

for s being Element of Funcs (X,INT) holds it . s = IFGT ((t1 . s),(t2 . s),0,1);

for b

( b

proof end;

coherence leq (t1,t2) is INT-Expression of A,f by Def22;

:: original: gt

redefine func gt (t1,t2) -> INT-Expression of A,f means :Def32: :: AOFA_I00:def 32

for s being Element of Funcs (X,INT) holds it . s = IFGT ((t1 . s),(t2 . s),1,0);

coherence redefine func gt (t1,t2) -> INT-Expression of A,f means :Def32: :: AOFA_I00:def 32

for s being Element of Funcs (X,INT) holds it . s = IFGT ((t1 . s),(t2 . s),1,0);

gt (t1,t2) is INT-Expression of A,f by Def22;

compatibility

for b

( b

proof end;

:: deftheorem Def29 defines div AOFA_I00:def 29 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for t1, t2, b_{7} being INT-Expression of A,f holds

( b_{7} = t1 div t2 iff for s being Element of Funcs (X,INT) holds b_{7} . s = (t1 . s) div (t2 . s) );

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for t1, t2, b

( b

:: deftheorem Def30 defines mod AOFA_I00:def 30 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for t1, t2, b_{7} being INT-Expression of A,f holds

( b_{7} = t1 mod t2 iff for s being Element of Funcs (X,INT) holds b_{7} . s = (t1 . s) mod (t2 . s) );

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for t1, t2, b

( b

:: deftheorem Def31 defines leq AOFA_I00:def 31 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for t1, t2, b_{7} being INT-Expression of A,f holds

( b_{7} = leq (t1,t2) iff for s being Element of Funcs (X,INT) holds b_{7} . s = IFGT ((t1 . s),(t2 . s),0,1) );

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for t1, t2, b

( b

:: deftheorem Def32 defines gt AOFA_I00:def 32 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for t1, t2, b_{7} being INT-Expression of A,f holds

( b_{7} = gt (t1,t2) iff for s being Element of Funcs (X,INT) holds b_{7} . s = IFGT ((t1 . s),(t2 . s),1,0) );

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for t1, t2, b

( b

definition

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let t1, t2 be INT-Expression of A,f;

for b_{1} being INT-Expression of A,f holds

( b_{1} = eq (t1,t2) iff for s being Element of Funcs (X,INT) holds b_{1} . s = IFEQ ((t1 . s),(t2 . s),1,0) )

eq (t1,t2) is INT-Expression of A,f

end;
let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let t1, t2 be INT-Expression of A,f;

:: original: eq

redefine func eq (t1,t2) -> INT-Expression of A,f means :: AOFA_I00:def 33

for s being Element of Funcs (X,INT) holds it . s = IFEQ ((t1 . s),(t2 . s),1,0);

compatibility redefine func eq (t1,t2) -> INT-Expression of A,f means :: AOFA_I00:def 33

for s being Element of Funcs (X,INT) holds it . s = IFEQ ((t1 . s),(t2 . s),1,0);

for b

( b

proof end;

coherence eq (t1,t2) is INT-Expression of A,f

proof end;

:: deftheorem defines eq AOFA_I00:def 33 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for t1, t2, b_{7} being INT-Expression of A,f holds

( b_{7} = eq (t1,t2) iff for s being Element of Funcs (X,INT) holds b_{7} . s = IFEQ ((t1 . s),(t2 . s),1,0) );

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for t1, t2, b

( b

definition

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let v be INT-Variable of A,f;

coherence

. v is INT-Expression of A,f by Def22;

end;
let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let v be INT-Variable of A,f;

coherence

. v is INT-Expression of A,f by Def22;

:: deftheorem defines . AOFA_I00:def 34 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for v being INT-Variable of A,f holds . v = . v;

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for v being INT-Variable of A,f holds . v = . v;

definition

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let x be Element of X;

coherence

^ x is INT-Variable of A,f by Def22;

end;
let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let x be Element of X;

coherence

^ x is INT-Variable of A,f by Def22;

:: deftheorem defines ^ AOFA_I00:def 35 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Element of X holds x ^ (A,f) = ^ x;

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Element of X holds x ^ (A,f) = ^ x;

notation

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let x be Variable of f;

synonym ^ x for x ^ (A,f);

end;
let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let x be Variable of f;

synonym ^ x for x ^ (A,f);

definition

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let x be Variable of f;

coherence

. (^ x) is INT-Expression of A,f ;

end;
let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let x be Variable of f;

coherence

. (^ x) is INT-Expression of A,f ;

:: deftheorem defines . AOFA_I00:def 36 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f holds . x = . (^ x);

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f holds . x = . (^ x);

theorem Th22: :: AOFA_I00:22

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for s being Element of Funcs (X,INT) holds (. x) . s = s . x

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for s being Element of Funcs (X,INT) holds (. x) . s = s . x

proof end;

definition

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let i be Integer;

coherence

. (i,X) is INT-Expression of A,f by Def22;

end;
let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let i be Integer;

coherence

. (i,X) is INT-Expression of A,f by Def22;

:: deftheorem defines . AOFA_I00:def 37 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for i being Integer holds . (i,A,f) = . (i,X);

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for i being Integer holds . (i,A,f) = . (i,X);

definition

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let v be INT-Variable of A,f;

let t be INT-Expression of A,f;

the Element of { I where I is Element of A : ( I in ElementaryInstructions A & ( for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) ) ) } is Element of A

end;
let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let v be INT-Variable of A,f;

let t be INT-Expression of A,f;

func v := t -> Element of A equals :: AOFA_I00:def 38

the Element of { I where I is Element of A : ( I in ElementaryInstructions A & ( for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) ) ) } ;

coherence the Element of { I where I is Element of A : ( I in ElementaryInstructions A & ( for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) ) ) } ;

the Element of { I where I is Element of A : ( I in ElementaryInstructions A & ( for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) ) ) } is Element of A

proof end;

:: deftheorem defines := AOFA_I00:def 38 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for v being INT-Variable of A,f

for t being INT-Expression of A,f holds v := t = the Element of { I where I is Element of A : ( I in ElementaryInstructions A & ( for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) ) ) } ;

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for v being INT-Variable of A,f

for t being INT-Expression of A,f holds v := t = the Element of { I where I is Element of A : ( I in ElementaryInstructions A & ( for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) ) ) } ;

theorem Th23: :: AOFA_I00:23

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for v being INT-Variable of A,f

for t being INT-Expression of A,f holds v := t in ElementaryInstructions A

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for v being INT-Variable of A,f

for t being INT-Expression of A,f holds v := t in ElementaryInstructions A

proof end;

registration

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let v be INT-Variable of A,f;

let t be INT-Expression of A,f;

coherence

v := t is absolutely-terminating by Th23, AOFA_000:95;

end;
let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let v be INT-Variable of A,f;

let t be INT-Expression of A,f;

coherence

v := t is absolutely-terminating by Th23, AOFA_000:95;

definition

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let v be INT-Variable of A,f;

let t be INT-Expression of A,f;

coherence

v := ((. v) + t) is absolutely-terminating Element of A ;

coherence

v := ((. v) (#) t) is absolutely-terminating Element of A ;

end;
let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let v be INT-Variable of A,f;

let t be INT-Expression of A,f;

coherence

v := ((. v) + t) is absolutely-terminating Element of A ;

coherence

v := ((. v) (#) t) is absolutely-terminating Element of A ;

:: deftheorem defines += AOFA_I00:def 39 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for v being INT-Variable of A,f

for t being INT-Expression of A,f holds v += t = v := ((. v) + t);

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for v being INT-Variable of A,f

for t being INT-Expression of A,f holds v += t = v := ((. v) + t);

:: deftheorem defines *= AOFA_I00:def 40 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for v being INT-Variable of A,f

for t being INT-Expression of A,f holds v *= t = v := ((. v) (#) t);

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for v being INT-Variable of A,f

for t being INT-Expression of A,f holds v *= t = v := ((. v) (#) t);

definition

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let x be Element of X;

let t be INT-Expression of A,f;

correctness

coherence

(x ^ (A,f)) := t is absolutely-terminating Element of A;

;

end;
let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let x be Element of X;

let t be INT-Expression of A,f;

correctness

coherence

(x ^ (A,f)) := t is absolutely-terminating Element of A;

;

:: deftheorem defines := AOFA_I00:def 41 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Element of X

for t being INT-Expression of A,f holds x := t = (x ^ (A,f)) := t;

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Element of X

for t being INT-Expression of A,f holds x := t = (x ^ (A,f)) := t;

definition

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let x be Element of X;

let y be Variable of f;

correctness

coherence

x := (. y) is absolutely-terminating Element of A;

;

end;
let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let x be Element of X;

let y be Variable of f;

correctness

coherence

x := (. y) is absolutely-terminating Element of A;

;

:: deftheorem defines := AOFA_I00:def 42 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Element of X

for y being Variable of f holds x := y = x := (. y);

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Element of X

for y being Variable of f holds x := y = x := (. y);

definition

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let x be Element of X;

let v be INT-Variable of A,f;

correctness

coherence

x := (. v) is absolutely-terminating Element of A;

;

end;
let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let x be Element of X;

let v be INT-Variable of A,f;

correctness

coherence

x := (. v) is absolutely-terminating Element of A;

;

:: deftheorem defines := AOFA_I00:def 43 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Element of X

for v being INT-Variable of A,f holds x := v = x := (. v);

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Element of X

for v being INT-Variable of A,f holds x := v = x := (. v);

definition

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let v, w be INT-Variable of A,f;

correctness

coherence

v := (. w) is absolutely-terminating Element of A;

;

end;
let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let v, w be INT-Variable of A,f;

correctness

coherence

v := (. w) is absolutely-terminating Element of A;

;

:: deftheorem defines := AOFA_I00:def 44 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for v, w being INT-Variable of A,f holds v := w = v := (. w);

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for v, w being INT-Variable of A,f holds v := w = v := (. w);

definition

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let x be Variable of f;

let i be Integer;

correctness

coherence

x := (. (i,A,f)) is absolutely-terminating Element of A;

;

end;
let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let x be Variable of f;

let i be Integer;

correctness

coherence

x := (. (i,A,f)) is absolutely-terminating Element of A;

;

:: deftheorem defines := AOFA_I00:def 45 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for i being Integer holds x := i = x := (. (i,A,f));

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for i being Integer holds x := i = x := (. (i,A,f));

definition

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let v1, v2 be INT-Variable of A,f;

let x be Variable of f;

((x := v1) \; (v1 := v2)) \; (v2 := (. x)) is absolutely-terminating Element of A ;

end;
let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let v1, v2 be INT-Variable of A,f;

let x be Variable of f;

func swap (v1,x,v2) -> absolutely-terminating Element of A equals :: AOFA_I00:def 46

((x := v1) \; (v1 := v2)) \; (v2 := (. x));

coherence ((x := v1) \; (v1 := v2)) \; (v2 := (. x));

((x := v1) \; (v1 := v2)) \; (v2 := (. x)) is absolutely-terminating Element of A ;

:: deftheorem defines swap AOFA_I00:def 46 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for v1, v2 being INT-Variable of A,f

for x being Variable of f holds swap (v1,x,v2) = ((x := v1) \; (v1 := v2)) \; (v2 := (. x));

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for v1, v2 being INT-Variable of A,f

for x being Variable of f holds swap (v1,x,v2) = ((x := v1) \; (v1 := v2)) \; (v2 := (. x));

definition

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let x be Variable of f;

let t be INT-Expression of A,f;

correctness

coherence

x := ((. x) + t) is absolutely-terminating Element of A;

;

correctness

coherence

x := ((. x) (#) t) is absolutely-terminating Element of A;

;

correctness

coherence

x := ((. x) mod t) is absolutely-terminating Element of A;

;

correctness

coherence

x := ((. x) div t) is absolutely-terminating Element of A;

;

end;
let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let x be Variable of f;

let t be INT-Expression of A,f;

correctness

coherence

x := ((. x) + t) is absolutely-terminating Element of A;

;

correctness

coherence

x := ((. x) (#) t) is absolutely-terminating Element of A;

;

correctness

coherence

x := ((. x) mod t) is absolutely-terminating Element of A;

;

correctness

coherence

x := ((. x) div t) is absolutely-terminating Element of A;

;

:: deftheorem defines += AOFA_I00:def 47 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for t being INT-Expression of A,f holds x += t = x := ((. x) + t);

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for t being INT-Expression of A,f holds x += t = x := ((. x) + t);

:: deftheorem defines *= AOFA_I00:def 48 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for t being INT-Expression of A,f holds x *= t = x := ((. x) (#) t);

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for t being INT-Expression of A,f holds x *= t = x := ((. x) (#) t);

:: deftheorem defines %= AOFA_I00:def 49 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for t being INT-Expression of A,f holds x %= t = x := ((. x) mod t);

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for t being INT-Expression of A,f holds x %= t = x := ((. x) mod t);

:: deftheorem defines /= AOFA_I00:def 50 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for t being INT-Expression of A,f holds x /= t = x := ((. x) div t);

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for t being INT-Expression of A,f holds x /= t = x := ((. x) div t);

definition

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let x be Variable of f;

let i be Integer;

correctness

coherence

x := ((. x) + i) is absolutely-terminating Element of A;

;

correctness

coherence

x := ((. x) * i) is absolutely-terminating Element of A;

;

coherence

x := ((. x) mod (. (i,A,f))) is absolutely-terminating Element of A;

;

coherence

x := ((. x) div (. (i,A,f))) is absolutely-terminating Element of A;

;

correctness

coherence

(. x) div (. (i,A,f)) is INT-Expression of A,f;

;

end;
let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let x be Variable of f;

let i be Integer;

correctness

coherence

x := ((. x) + i) is absolutely-terminating Element of A;

;

correctness

coherence

x := ((. x) * i) is absolutely-terminating Element of A;

;

func x %= i -> absolutely-terminating Element of A equals :: AOFA_I00:def 53

x := ((. x) mod (. (i,A,f)));

correctness x := ((. x) mod (. (i,A,f)));

coherence

x := ((. x) mod (. (i,A,f))) is absolutely-terminating Element of A;

;

func x /= i -> absolutely-terminating Element of A equals :: AOFA_I00:def 54

x := ((. x) div (. (i,A,f)));

correctness x := ((. x) div (. (i,A,f)));

coherence

x := ((. x) div (. (i,A,f))) is absolutely-terminating Element of A;

;

correctness

coherence

(. x) div (. (i,A,f)) is INT-Expression of A,f;

;

:: deftheorem defines += AOFA_I00:def 51 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for i being Integer holds x += i = x := ((. x) + i);

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for i being Integer holds x += i = x := ((. x) + i);

:: deftheorem defines *= AOFA_I00:def 52 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for i being Integer holds x *= i = x := ((. x) * i);

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for i being Integer holds x *= i = x := ((. x) * i);

:: deftheorem defines %= AOFA_I00:def 53 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for i being Integer holds x %= i = x := ((. x) mod (. (i,A,f)));

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for i being Integer holds x %= i = x := ((. x) mod (. (i,A,f)));

:: deftheorem defines /= AOFA_I00:def 54 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for i being Integer holds x /= i = x := ((. x) div (. (i,A,f)));

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for i being Integer holds x /= i = x := ((. x) div (. (i,A,f)));

:: deftheorem defines div AOFA_I00:def 55 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for i being Integer holds x div i = (. x) div (. (i,A,f));

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for i being Integer holds x div i = (. x) div (. (i,A,f));

definition

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let v be INT-Variable of A,f;

let i be Integer;

correctness

coherence

v := (. (i,A,f)) is absolutely-terminating Element of A;

;

end;
let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let v be INT-Variable of A,f;

let i be Integer;

correctness

coherence

v := (. (i,A,f)) is absolutely-terminating Element of A;

;

:: deftheorem defines := AOFA_I00:def 56 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for v being INT-Variable of A,f

for i being Integer holds v := i = v := (. (i,A,f));

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for v being INT-Variable of A,f

for i being Integer holds v := i = v := (. (i,A,f));

definition

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let v be INT-Variable of A,f;

let i be Integer;

correctness

coherence

v := ((. v) + i) is absolutely-terminating Element of A;

;

correctness

coherence

v := ((. v) * i) is absolutely-terminating Element of A;

;

end;
let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let v be INT-Variable of A,f;

let i be Integer;

correctness

coherence

v := ((. v) + i) is absolutely-terminating Element of A;

;

correctness

coherence

v := ((. v) * i) is absolutely-terminating Element of A;

;

:: deftheorem defines += AOFA_I00:def 57 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for v being INT-Variable of A,f

for i being Integer holds v += i = v := ((. v) + i);

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for v being INT-Variable of A,f

for i being Integer holds v += i = v := ((. v) + i);

:: deftheorem defines *= AOFA_I00:def 58 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for v being INT-Variable of A,f

for i being Integer holds v *= i = v := ((. v) * i);

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for v being INT-Variable of A,f

for i being Integer holds v *= i = v := ((. v) * i);

definition

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let b be Element of X;

let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0);

let t1 be INT-Expression of A,g;

b := (t1 mod (. (2,A,g))) is absolutely-terminating Element of A ;

b := ((t1 + 1) mod (. (2,A,g))) is absolutely-terminating Element of A ;

let t2 be INT-Expression of A,g;

coherence

b := (leq (t1,t2)) is absolutely-terminating Element of A ;

coherence

b := (gt (t1,t2)) is absolutely-terminating Element of A ;

coherence

b := (eq (t1,t2)) is absolutely-terminating Element of A ;

end;
let X be non empty countable set ;

let b be Element of X;

let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0);

let t1 be INT-Expression of A,g;

func t1 is_odd -> absolutely-terminating Element of A equals :: AOFA_I00:def 59

b := (t1 mod (. (2,A,g)));

coherence b := (t1 mod (. (2,A,g)));

b := (t1 mod (. (2,A,g))) is absolutely-terminating Element of A ;

func t1 is_even -> absolutely-terminating Element of A equals :: AOFA_I00:def 60

b := ((t1 + 1) mod (. (2,A,g)));

coherence b := ((t1 + 1) mod (. (2,A,g)));

b := ((t1 + 1) mod (. (2,A,g))) is absolutely-terminating Element of A ;

let t2 be INT-Expression of A,g;

coherence

b := (leq (t1,t2)) is absolutely-terminating Element of A ;

coherence

b := (gt (t1,t2)) is absolutely-terminating Element of A ;

coherence

b := (eq (t1,t2)) is absolutely-terminating Element of A ;

:: deftheorem defines is_odd AOFA_I00:def 59 :

for A being 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 t1 being INT-Expression of A,g holds t1 is_odd = b := (t1 mod (. (2,A,g)));

for A being 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 t1 being INT-Expression of A,g holds t1 is_odd = b := (t1 mod (. (2,A,g)));

:: deftheorem defines is_even AOFA_I00:def 60 :

for A being 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 t1 being INT-Expression of A,g holds t1 is_even = b := ((t1 + 1) mod (. (2,A,g)));

for A being 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 t1 being INT-Expression of A,g holds t1 is_even = b := ((t1 + 1) mod (. (2,A,g)));

:: deftheorem defines leq AOFA_I00:def 61 :

for A being 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 t1, t2 being INT-Expression of A,g holds t1 leq t2 = b := (leq (t1,t2));

for A being 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 t1, t2 being INT-Expression of A,g holds t1 leq t2 = b := (leq (t1,t2));

:: deftheorem defines gt AOFA_I00:def 62 :

for A being 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 t1, t2 being INT-Expression of A,g holds t1 gt t2 = b := (gt (t1,t2));

for A being 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 t1, t2 being INT-Expression of A,g holds t1 gt t2 = b := (gt (t1,t2));

:: deftheorem defines eq AOFA_I00:def 63 :

for A being 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 t1, t2 being INT-Expression of A,g holds t1 eq t2 = b := (eq (t1,t2));

for A being 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 t1, t2 being INT-Expression of A,g holds t1 eq t2 = b := (eq (t1,t2));

notation

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let b be Element of X;

let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0);

let t1, t2 be INT-Expression of A,g;

synonym t2 geq t1 for t1 leq t2;

synonym t2 lt t1 for t1 gt t2;

end;
let X be non empty countable set ;

let b be Element of X;

let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0);

let t1, t2 be INT-Expression of A,g;

synonym t2 geq t1 for t1 leq t2;

synonym t2 lt t1 for t1 gt t2;

definition

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let b be Element of X;

let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0);

let v1, v2 be INT-Variable of A,g;

coherence

(. v1) leq (. v2) is absolutely-terminating Element of A ;

coherence

(. v1) gt (. v2) is absolutely-terminating Element of A ;

end;
let X be non empty countable set ;

let b be Element of X;

let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0);

let v1, v2 be INT-Variable of A,g;

coherence

(. v1) leq (. v2) is absolutely-terminating Element of A ;

coherence

(. v1) gt (. v2) is absolutely-terminating Element of A ;

:: deftheorem defines leq AOFA_I00:def 64 :

for A being 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 v1, v2 being INT-Variable of A,g holds v1 leq v2 = (. v1) leq (. v2);

for A being 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 v1, v2 being INT-Variable of A,g holds v1 leq v2 = (. v1) leq (. v2);

:: deftheorem defines gt AOFA_I00:def 65 :

for A being 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 v1, v2 being INT-Variable of A,g holds v1 gt v2 = (. v1) gt (. v2);

for A being 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 v1, v2 being INT-Variable of A,g holds v1 gt v2 = (. v1) gt (. v2);

notation

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let b be Element of X;

let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0);

let v1, v2 be INT-Variable of A,g;

synonym v2 geq v1 for v1 leq v2;

synonym v2 lt v1 for v1 gt v2;

end;
let X be non empty countable set ;

let b be Element of X;

let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0);

let v1, v2 be INT-Variable of A,g;

synonym v2 geq v1 for v1 leq v2;

synonym v2 lt v1 for v1 gt v2;

definition

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let b be Element of X;

let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0);

let x1 be Variable of g;

coherence

(. x1) is_odd is absolutely-terminating Element of A ;

coherence

(. x1) is_even is absolutely-terminating Element of A ;

let x2 be Variable of g;

coherence

(. x1) leq (. x2) is absolutely-terminating Element of A ;

coherence

(. x1) gt (. x2) is absolutely-terminating Element of A ;

end;
let X be non empty countable set ;

let b be Element of X;

let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0);

let x1 be Variable of g;

coherence

(. x1) is_odd is absolutely-terminating Element of A ;

coherence

(. x1) is_even is absolutely-terminating Element of A ;

let x2 be Variable of g;

coherence

(. x1) leq (. x2) is absolutely-terminating Element of A ;

coherence

(. x1) gt (. x2) is absolutely-terminating Element of A ;

:: deftheorem defines is_odd AOFA_I00:def 66 :

for A being 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 x1 being Variable of g holds x1 is_odd = (. x1) is_odd ;

for A being 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 x1 being Variable of g holds x1 is_odd = (. x1) is_odd ;

:: deftheorem defines is_even AOFA_I00:def 67 :

for A being 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 x1 being Variable of g holds x1 is_even = (. x1) is_even ;

for A being 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 x1 being Variable of g holds x1 is_even = (. x1) is_even ;

:: deftheorem defines leq AOFA_I00:def 68 :

for A being 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 x1, x2 being Variable of g holds x1 leq x2 = (. x1) leq (. x2);

for A being 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 x1, x2 being Variable of g holds x1 leq x2 = (. x1) leq (. x2);

:: deftheorem defines gt AOFA_I00:def 69 :

for A being 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 x1, x2 being Variable of g holds x1 gt x2 = (. x1) gt (. x2);

for A being 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 x1, x2 being Variable of g holds x1 gt x2 = (. x1) gt (. x2);

notation

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let b be Element of X;

let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0);

let x1, x2 be Variable of g;

synonym x2 geq x1 for x1 leq x2;

synonym x2 lt x1 for x1 gt x2;

end;
let X be non empty countable set ;

let b be Element of X;

let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0);

let x1, x2 be Variable of g;

synonym x2 geq x1 for x1 leq x2;

synonym x2 lt x1 for x1 gt x2;

definition

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let b be Element of X;

let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0);

let x be Variable of g;

let i be Integer;

coherence

(. x) leq (. (i,A,g)) is absolutely-terminating Element of A ;

coherence

(. x) geq (. (i,A,g)) is absolutely-terminating Element of A ;

coherence

(. x) gt (. (i,A,g)) is absolutely-terminating Element of A ;

coherence

(. x) lt (. (i,A,g)) is absolutely-terminating Element of A ;

coherence

(. x) div (. (i,A,g)) is INT-Expression of A,g ;

end;
let X be non empty countable set ;

let b be Element of X;

let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0);

let x be Variable of g;

let i be Integer;

coherence

(. x) leq (. (i,A,g)) is absolutely-terminating Element of A ;

coherence

(. x) geq (. (i,A,g)) is absolutely-terminating Element of A ;

coherence

(. x) gt (. (i,A,g)) is absolutely-terminating Element of A ;

coherence

(. x) lt (. (i,A,g)) is absolutely-terminating Element of A ;

coherence

(. x) div (. (i,A,g)) is INT-Expression of A,g ;

:: deftheorem defines leq AOFA_I00:def 70 :

for A being 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 being Variable of g

for i being Integer holds x leq i = (. x) leq (. (i,A,g));

for A being 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 being Variable of g

for i being Integer holds x leq i = (. x) leq (. (i,A,g));

:: deftheorem defines geq AOFA_I00:def 71 :

for A being 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 being Variable of g

for i being Integer holds x geq i = (. x) geq (. (i,A,g));

for A being 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 being Variable of g

for i being Integer holds x geq i = (. x) geq (. (i,A,g));

:: deftheorem defines gt AOFA_I00:def 72 :

for A being 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 being Variable of g

for i being Integer holds x gt i = (. x) gt (. (i,A,g));

for A being 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 being Variable of g

for i being Integer holds x gt i = (. x) gt (. (i,A,g));

:: deftheorem defines lt AOFA_I00:def 73 :

for A being 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 being Variable of g

for i being Integer holds x lt i = (. x) lt (. (i,A,g));

for A being 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 being Variable of g

for i being Integer holds x lt i = (. x) lt (. (i,A,g));

:: deftheorem defines / AOFA_I00:def 74 :

for A being 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 being Variable of g

for i being Integer holds x / i = (. x) div (. (i,A,g));

for A being 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 being Variable of g

for i being Integer holds x / i = (. x) div (. (i,A,g));

definition

let A be Euclidean preIfWhileAlgebra;

let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let x1, x2 be Variable of f;

coherence

x1 += (. x2) is absolutely-terminating Element of A ;

coherence

x1 *= (. x2) is absolutely-terminating Element of A ;

x1 := ((. x1) mod (. x2)) is absolutely-terminating Element of A ;

x1 := ((. x1) div (. x2)) is absolutely-terminating Element of A ;

coherence

(. x1) + (. x2) is INT-Expression of A,f ;

coherence

(. x1) (#) (. x2) is INT-Expression of A,f ;

coherence

(. x1) mod (. x2) is INT-Expression of A,f ;

coherence

(. x1) div (. x2) is INT-Expression of A,f ;

end;
let X be non empty countable set ;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let x1, x2 be Variable of f;

coherence

x1 += (. x2) is absolutely-terminating Element of A ;

coherence

x1 *= (. x2) is absolutely-terminating Element of A ;

func x1 %= x2 -> absolutely-terminating Element of A equals :: AOFA_I00:def 77

x1 := ((. x1) mod (. x2));

coherence x1 := ((. x1) mod (. x2));

x1 := ((. x1) mod (. x2)) is absolutely-terminating Element of A ;

func x1 /= x2 -> absolutely-terminating Element of A equals :: AOFA_I00:def 78

x1 := ((. x1) div (. x2));

coherence x1 := ((. x1) div (. x2));

x1 := ((. x1) div (. x2)) is absolutely-terminating Element of A ;

coherence

(. x1) + (. x2) is INT-Expression of A,f ;

coherence

(. x1) (#) (. x2) is INT-Expression of A,f ;

coherence

(. x1) mod (. x2) is INT-Expression of A,f ;

coherence

(. x1) div (. x2) is INT-Expression of A,f ;

:: deftheorem defines += AOFA_I00:def 75 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x1, x2 being Variable of f holds x1 += x2 = x1 += (. x2);

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x1, x2 being Variable of f holds x1 += x2 = x1 += (. x2);

:: deftheorem defines *= AOFA_I00:def 76 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x1, x2 being Variable of f holds x1 *= x2 = x1 *= (. x2);

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x1, x2 being Variable of f holds x1 *= x2 = x1 *= (. x2);

:: deftheorem defines %= AOFA_I00:def 77 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x1, x2 being Variable of f holds x1 %= x2 = x1 := ((. x1) mod (. x2));

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x1, x2 being Variable of f holds x1 %= x2 = x1 := ((. x1) mod (. x2));

:: deftheorem defines /= AOFA_I00:def 78 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x1, x2 being Variable of f holds x1 /= x2 = x1 := ((. x1) div (. x2));

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x1, x2 being Variable of f holds x1 /= x2 = x1 := ((. x1) div (. x2));

:: deftheorem defines + AOFA_I00:def 79 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x1, x2 being Variable of f holds x1 + x2 = (. x1) + (. x2);

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x1, x2 being Variable of f holds x1 + x2 = (. x1) + (. x2);

:: deftheorem defines * AOFA_I00:def 80 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x1, x2 being Variable of f holds x1 * x2 = (. x1) (#) (. x2);

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x1, x2 being Variable of f holds x1 * x2 = (. x1) (#) (. x2);

:: deftheorem defines mod AOFA_I00:def 81 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x1, x2 being Variable of f holds x1 mod x2 = (. x1) mod (. x2);

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x1, x2 being Variable of f holds x1 mod x2 = (. x1) mod (. x2);

:: deftheorem defines div AOFA_I00:def 82 :

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x1, x2 being Variable of f holds x1 div x2 = (. x1) div (. x2);

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x1, x2 being Variable of f holds x1 div x2 = (. x1) div (. x2);

theorem Th24: :: AOFA_I00:24

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for v being INT-Variable of A,f

for t being INT-Expression of A,f holds

( (f . (s,(v := t))) . (v . s) = t . s & ( for z being Element of X st z <> v . s holds

(f . (s,(v := t))) . z = s . z ) )

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for v being INT-Variable of A,f

for t being INT-Expression of A,f holds

( (f . (s,(v := t))) . (v . s) = t . s & ( for z being Element of X st z <> v . s holds

(f . (s,(v := t))) . z = s . z ) )

proof end;

theorem Th25: :: AOFA_I00:25

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for i being Integer holds

( (f . (s,(x := i))) . x = i & ( for z being Element of X st z <> x holds

(f . (s,(x := i))) . z = s . z ) )

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for i being Integer holds

( (f . (s,(x := i))) . x = i & ( for z being Element of X st z <> x holds

(f . (s,(x := i))) . z = s . z ) )

proof end;

theorem Th26: :: AOFA_I00:26

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for t being INT-Expression of A,f holds

( (f . (s,(x := t))) . x = t . s & ( for z being Element of X st z <> x holds

(f . (s,(x := t))) . z = s . z ) )

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for t being INT-Expression of A,f holds

( (f . (s,(x := t))) . x = t . s & ( for z being Element of X st z <> x holds

(f . (s,(x := t))) . z = s . z ) )

proof end;

theorem Th27: :: AOFA_I00:27

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x, y being Variable of f holds

( (f . (s,(x := y))) . x = s . y & ( for z being Element of X st z <> x holds

(f . (s,(x := y))) . z = s . z ) )

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x, y being Variable of f holds

( (f . (s,(x := y))) . x = s . y & ( for z being Element of X st z <> x holds

(f . (s,(x := y))) . z = s . z ) )

proof end;

theorem Th28: :: AOFA_I00:28

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for i being Integer

for x being Variable of f holds

( (f . (s,(x += i))) . x = (s . x) + i & ( for z being Element of X st z <> x holds

(f . (s,(x += i))) . z = s . z ) )

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for i being Integer

for x being Variable of f holds

( (f . (s,(x += i))) . x = (s . x) + i & ( for z being Element of X st z <> x holds

(f . (s,(x += i))) . z = s . z ) )

proof end;

theorem Th29: :: AOFA_I00:29

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for t being INT-Expression of A,f holds

( (f . (s,(x += t))) . x = (s . x) + (t . s) & ( for z being Element of X st z <> x holds

(f . (s,(x += t))) . z = s . z ) )

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for t being INT-Expression of A,f holds

( (f . (s,(x += t))) . x = (s . x) + (t . s) & ( for z being Element of X st z <> x holds

(f . (s,(x += t))) . z = s . z ) )

proof end;

theorem Th30: :: AOFA_I00:30

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x, y being Variable of f holds

( (f . (s,(x += y))) . x = (s . x) + (s . y) & ( for z being Element of X st z <> x holds

(f . (s,(x += y))) . z = s . z ) )

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x, y being Variable of f holds

( (f . (s,(x += y))) . x = (s . x) + (s . y) & ( for z being Element of X st z <> x holds

(f . (s,(x += y))) . z = s . z ) )

proof end;

theorem Th31: :: AOFA_I00:31

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for i being Integer

for x being Variable of f holds

( (f . (s,(x *= i))) . x = (s . x) * i & ( for z being Element of X st z <> x holds

(f . (s,(x *= i))) . z = s . z ) )

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for i being Integer

for x being Variable of f holds

( (f . (s,(x *= i))) . x = (s . x) * i & ( for z being Element of X st z <> x holds

(f . (s,(x *= i))) . z = s . z ) )

proof end;

theorem Th32: :: AOFA_I00:32

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for t being INT-Expression of A,f holds

( (f . (s,(x *= t))) . x = (s . x) * (t . s) & ( for z being Element of X st z <> x holds

(f . (s,(x *= t))) . z = s . z ) )

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for t being INT-Expression of A,f holds

( (f . (s,(x *= t))) . x = (s . x) * (t . s) & ( for z being Element of X st z <> x holds

(f . (s,(x *= t))) . z = s . z ) )

proof end;

theorem Th33: :: AOFA_I00:33

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x, y being Variable of f holds

( (f . (s,(x *= y))) . x = (s . x) * (s . y) & ( for z being Element of X st z <> x holds

(f . (s,(x *= y))) . z = s . z ) )

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x, y being Variable of f holds

( (f . (s,(x *= y))) . x = (s . x) * (s . y) & ( for z being Element of X st z <> x holds

(f . (s,(x *= y))) . z = s . z ) )

proof end;

theorem Th34: :: AOFA_I00:34

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for x being Variable of g

for i being Integer holds

( ( s . x <= i implies (g . (s,(x leq i))) . b = 1 ) & ( s . x > i implies (g . (s,(x leq i))) . b = 0 ) & ( s . x >= i implies (g . (s,(x geq i))) . b = 1 ) & ( s . x < i implies (g . (s,(x geq i))) . b = 0 ) & ( for z being Element of X st z <> b holds

( (g . (s,(x leq i))) . z = s . z & (g . (s,(x geq i))) . z = s . z ) ) )

for X being non empty countable set

for s being Element of Funcs (X,INT)

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for x being Variable of g

for i being Integer holds

( ( s . x <= i implies (g . (s,(x leq i))) . b = 1 ) & ( s . x > i implies (g . (s,(x leq i))) . b = 0 ) & ( s . x >= i implies (g . (s,(x geq i))) . b = 1 ) & ( s . x < i implies (g . (s,(x geq i))) . b = 0 ) & ( for z being Element of X st z <> b holds

( (g . (s,(x leq i))) . z = s . z & (g . (s,(x geq i))) . z = s . z ) ) )

proof end;

theorem Th35: :: AOFA_I00:35

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for x, y being Variable of g holds

( ( s . x <= s . y implies (g . (s,(x leq y))) . b = 1 ) & ( s . x > s . y implies (g . (s,(x leq y))) . b = 0 ) & ( for z being Element of X st z <> b holds

(g . (s,(x leq y))) . z = s . z ) )

for X being non empty countable set

for s being Element of Funcs (X,INT)

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for x, y being Variable of g holds

( ( s . x <= s . y implies (g . (s,(x leq y))) . b = 1 ) & ( s . x > s . y implies (g . (s,(x leq y))) . b = 0 ) & ( for z being Element of X st z <> b holds

(g . (s,(x leq y))) . z = s . z ) )

proof end;

theorem :: AOFA_I00:36

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for x being Variable of g

for i being Integer holds

( ( s . x <= i implies g . (s,(x leq i)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x leq i)) in (Funcs (X,INT)) \ (b,0) implies s . x <= i ) & ( s . x >= i implies g . (s,(x geq i)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x geq i)) in (Funcs (X,INT)) \ (b,0) implies s . x >= i ) )

for X being non empty countable set

for s being Element of Funcs (X,INT)

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for x being Variable of g

for i being Integer holds

( ( s . x <= i implies g . (s,(x leq i)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x leq i)) in (Funcs (X,INT)) \ (b,0) implies s . x <= i ) & ( s . x >= i implies g . (s,(x geq i)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x geq i)) in (Funcs (X,INT)) \ (b,0) implies s . x >= i ) )

proof end;

theorem :: AOFA_I00:37

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for x, y being Variable of g holds

( ( s . x <= s . y implies g . (s,(x leq y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x leq y)) in (Funcs (X,INT)) \ (b,0) implies s . x <= s . y ) & ( s . x >= s . y implies g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) implies s . x >= s . y ) )

for X being non empty countable set

for s being Element of Funcs (X,INT)

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for x, y being Variable of g holds

( ( s . x <= s . y implies g . (s,(x leq y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x leq y)) in (Funcs (X,INT)) \ (b,0) implies s . x <= s . y ) & ( s . x >= s . y implies g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) implies s . x >= s . y ) )

proof end;

theorem Th38: :: AOFA_I00:38

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for x being Variable of g

for i being Integer holds

( ( s . x > i implies (g . (s,(x gt i))) . b = 1 ) & ( s . x <= i implies (g . (s,(x gt i))) . b = 0 ) & ( s . x < i implies (g . (s,(x lt i))) . b = 1 ) & ( s . x >= i implies (g . (s,(x lt i))) . b = 0 ) & ( for z being Element of X st z <> b holds

( (g . (s,(x gt i))) . z = s . z & (g . (s,(x lt i))) . z = s . z ) ) )

for X being non empty countable set

for s being Element of Funcs (X,INT)

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for x being Variable of g

for i being Integer holds

( ( s . x > i implies (g . (s,(x gt i))) . b = 1 ) & ( s . x <= i implies (g . (s,(x gt i))) . b = 0 ) & ( s . x < i implies (g . (s,(x lt i))) . b = 1 ) & ( s . x >= i implies (g . (s,(x lt i))) . b = 0 ) & ( for z being Element of X st z <> b holds

( (g . (s,(x gt i))) . z = s . z & (g . (s,(x lt i))) . z = s . z ) ) )

proof end;

theorem Th39: :: AOFA_I00:39

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for x, y being Variable of g holds

( ( s . x > s . y implies (g . (s,(x gt y))) . b = 1 ) & ( s . x <= s . y implies (g . (s,(x gt y))) . b = 0 ) & ( s . x < s . y implies (g . (s,(x lt y))) . b = 1 ) & ( s . x >= s . y implies (g . (s,(x lt y))) . b = 0 ) & ( for z being Element of X st z <> b holds

( (g . (s,(x gt y))) . z = s . z & (g . (s,(x lt y))) . z = s . z ) ) )

for X being non empty countable set

for s being Element of Funcs (X,INT)

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for x, y being Variable of g holds

( ( s . x > s . y implies (g . (s,(x gt y))) . b = 1 ) & ( s . x <= s . y implies (g . (s,(x gt y))) . b = 0 ) & ( s . x < s . y implies (g . (s,(x lt y))) . b = 1 ) & ( s . x >= s . y implies (g . (s,(x lt y))) . b = 0 ) & ( for z being Element of X st z <> b holds

( (g . (s,(x gt y))) . z = s . z & (g . (s,(x lt y))) . z = s . z ) ) )

proof end;

theorem Th40: :: AOFA_I00:40

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for x being Variable of g

for i being Integer holds

( ( s . x > i implies g . (s,(x gt i)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x gt i)) in (Funcs (X,INT)) \ (b,0) implies s . x > i ) & ( s . x < i implies g . (s,(x lt i)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x lt i)) in (Funcs (X,INT)) \ (b,0) implies s . x < i ) )

for X being non empty countable set

for s being Element of Funcs (X,INT)

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for x being Variable of g

for i being Integer holds

( ( s . x > i implies g . (s,(x gt i)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x gt i)) in (Funcs (X,INT)) \ (b,0) implies s . x > i ) & ( s . x < i implies g . (s,(x lt i)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x lt i)) in (Funcs (X,INT)) \ (b,0) implies s . x < i ) )

proof end;

theorem :: AOFA_I00:41

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for x, y being Variable of g holds

( ( s . x > s . y implies g . (s,(x gt y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x gt y)) in (Funcs (X,INT)) \ (b,0) implies s . x > s . y ) & ( s . x < s . y implies g . (s,(x lt y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x lt y)) in (Funcs (X,INT)) \ (b,0) implies s . x < s . y ) )

for X being non empty countable set

for s being Element of Funcs (X,INT)

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for x, y being Variable of g holds

( ( s . x > s . y implies g . (s,(x gt y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x gt y)) in (Funcs (X,INT)) \ (b,0) implies s . x > s . y ) & ( s . x < s . y implies g . (s,(x lt y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x lt y)) in (Funcs (X,INT)) \ (b,0) implies s . x < s . y ) )

proof end;

theorem :: AOFA_I00:42

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for i being Integer

for x being Variable of f holds

( (f . (s,(x %= i))) . x = (s . x) mod i & ( for z being Element of X st z <> x holds

(f . (s,(x %= i))) . z = s . z ) )

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for i being Integer

for x being Variable of f holds

( (f . (s,(x %= i))) . x = (s . x) mod i & ( for z being Element of X st z <> x holds

(f . (s,(x %= i))) . z = s . z ) )

proof end;

theorem Th43: :: AOFA_I00:43

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for t being INT-Expression of A,f holds

( (f . (s,(x %= t))) . x = (s . x) mod (t . s) & ( for z being Element of X st z <> x holds

(f . (s,(x %= t))) . z = s . z ) )

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for t being INT-Expression of A,f holds

( (f . (s,(x %= t))) . x = (s . x) mod (t . s) & ( for z being Element of X st z <> x holds

(f . (s,(x %= t))) . z = s . z ) )

proof end;

theorem Th44: :: AOFA_I00:44

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x, y being Variable of f holds

( (f . (s,(x %= y))) . x = (s . x) mod (s . y) & ( for z being Element of X st z <> x holds

(f . (s,(x %= y))) . z = s . z ) )

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x, y being Variable of f holds

( (f . (s,(x %= y))) . x = (s . x) mod (s . y) & ( for z being Element of X st z <> x holds

(f . (s,(x %= y))) . z = s . z ) )

proof end;

theorem Th45: :: AOFA_I00:45

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for i being Integer

for x being Variable of f holds

( (f . (s,(x /= i))) . x = (s . x) div i & ( for z being Element of X st z <> x holds

(f . (s,(x /= i))) . z = s . z ) )

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for i being Integer

for x being Variable of f holds

( (f . (s,(x /= i))) . x = (s . x) div i & ( for z being Element of X st z <> x holds

(f . (s,(x /= i))) . z = s . z ) )

proof end;

theorem Th46: :: AOFA_I00:46

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for t being INT-Expression of A,f holds

( (f . (s,(x /= t))) . x = (s . x) div (t . s) & ( for z being Element of X st z <> x holds

(f . (s,(x /= t))) . z = s . z ) )

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x being Variable of f

for t being INT-Expression of A,f holds

( (f . (s,(x /= t))) . x = (s . x) div (t . s) & ( for z being Element of X st z <> x holds

(f . (s,(x /= t))) . z = s . z ) )

proof end;

theorem :: AOFA_I00:47

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x, y being Variable of f holds

( (f . (s,(x /= y))) . x = (s . x) div (s . y) & ( for z being Element of X st z <> x holds

(f . (s,(x /= y))) . z = s . z ) )

for X being non empty countable set

for s being Element of Funcs (X,INT)

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for x, y being Variable of f holds

( (f . (s,(x /= y))) . x = (s . x) div (s . y) & ( for z being Element of X st z <> x holds

(f . (s,(x /= y))) . z = s . z ) )

proof end;

theorem Th48: :: AOFA_I00:48

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for t being INT-Expression of A,g holds

( (g . (s,(t is_odd))) . b = (t . s) mod 2 & (g . (s,(t is_even))) . b = ((t . s) + 1) mod 2 & ( for z being Element of X st z <> b holds

( (g . (s,(t is_odd))) . z = s . z & (g . (s,(t is_even))) . z = s . z ) ) )

for X being non empty countable set

for s being Element of Funcs (X,INT)

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for t being INT-Expression of A,g holds

( (g . (s,(t is_odd))) . b = (t . s) mod 2 & (g . (s,(t is_even))) . b = ((t . s) + 1) mod 2 & ( for z being Element of X st z <> b holds

( (g . (s,(t is_odd))) . z = s . z & (g . (s,(t is_even))) . z = s . z ) ) )

proof end;

theorem Th49: :: AOFA_I00:49

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for x being Variable of g holds

( (g . (s,(x is_odd))) . b = (s . x) mod 2 & (g . (s,(x is_even))) . b = ((s . x) + 1) mod 2 & ( for z being Element of X st z <> b holds

(g . (s,(x is_odd))) . z = s . z ) )

for X being non empty countable set

for s being Element of Funcs (X,INT)

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for x being Variable of g holds

( (g . (s,(x is_odd))) . b = (s . x) mod 2 & (g . (s,(x is_even))) . b = ((s . x) + 1) mod 2 & ( for z being Element of X st z <> b holds

(g . (s,(x is_odd))) . z = s . z ) )

proof end;

theorem Th50: :: AOFA_I00:50

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for t being INT-Expression of A,g holds

( ( t . s is odd implies g . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) implies t . s is odd ) & ( t . s is even implies g . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) implies t . s is even ) )

for X being non empty countable set

for s being Element of Funcs (X,INT)

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for t being INT-Expression of A,g holds

( ( t . s is odd implies g . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) implies t . s is odd ) & ( t . s is even implies g . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) implies t . s is even ) )

proof end;

theorem :: AOFA_I00:51

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for x being Variable of g holds

( ( s . x is odd implies g . (s,(x is_odd)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x is_odd)) in (Funcs (X,INT)) \ (b,0) implies s . x is odd ) & ( s . x is even implies g . (s,(x is_even)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x is_even)) in (Funcs (X,INT)) \ (b,0) implies s . x is even ) )

for X being non empty countable set

for s being Element of Funcs (X,INT)

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for x being Variable of g holds

( ( s . x is odd implies g . (s,(x is_odd)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x is_odd)) in (Funcs (X,INT)) \ (b,0) implies s . x is odd ) & ( s . x is even implies g . (s,(x is_even)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x is_even)) in (Funcs (X,INT)) \ (b,0) implies s . x is even ) )

proof end;

scheme :: AOFA_I00:sch 1

ForToIteration{ F_{1}() -> Euclidean preIfWhileAlgebra, F_{2}() -> non empty countable set , F_{3}() -> Element of F_{2}(), F_{4}() -> Element of F_{1}(), F_{5}() -> Element of F_{1}(), F_{6}() -> Euclidean ExecutionFunction of F_{1}(), Funcs (F_{2}(),INT),(Funcs (F_{2}(),INT)) \ (F_{3}(),0), F_{7}() -> Variable of F_{6}(), F_{8}() -> Variable of F_{6}(), F_{9}() -> Element of Funcs (F_{2}(),INT), F_{10}() -> INT-Expression of F_{1}(),F_{6}(), P_{1}[ set ] } :

ForToIteration{ F

( P_{1}[F_{6}() . (F_{9}(),F_{5}())] & ( F_{10}() . F_{9}() <= F_{9}() . F_{8}() implies (F_{6}() . (F_{9}(),F_{5}())) . F_{7}() = (F_{9}() . F_{8}()) + 1 ) & ( F_{10}() . F_{9}() > F_{9}() . F_{8}() implies (F_{6}() . (F_{9}(),F_{5}())) . F_{7}() = F_{10}() . F_{9}() ) & (F_{6}() . (F_{9}(),F_{5}())) . F_{8}() = F_{9}() . F_{8}() )

provided
A1:
F_{5}() = for-do ((F_{7}() := F_{10}()),(F_{7}() leq F_{8}()),(F_{7}() += 1),F_{4}())
and

A2: P_{1}[F_{6}() . (F_{9}(),(F_{7}() := F_{10}()))]
and

A3: for s being Element of Funcs (F_{2}(),INT) st P_{1}[s] holds

( P_{1}[F_{6}() . (s,(F_{4}() \; (F_{7}() += 1)))] & P_{1}[F_{6}() . (s,(F_{7}() leq F_{8}()))] )
and

A4: for s being Element of Funcs (F_{2}(),INT) st P_{1}[s] holds

( (F_{6}() . (s,F_{4}())) . F_{7}() = s . F_{7}() & (F_{6}() . (s,F_{4}())) . F_{8}() = s . F_{8}() )
and

A5: ( F_{8}() <> F_{7}() & F_{8}() <> F_{3}() & F_{7}() <> F_{3}() )

A2: P

A3: for s being Element of Funcs (F

( P

A4: for s being Element of Funcs (F

( (F

A5: ( F

proof end;

scheme :: AOFA_I00:sch 2

ForDowntoIteration{ F_{1}() -> Euclidean preIfWhileAlgebra, F_{2}() -> non empty countable set , F_{3}() -> Element of F_{2}(), F_{4}() -> Element of F_{1}(), F_{5}() -> Element of F_{1}(), F_{6}() -> Euclidean ExecutionFunction of F_{1}(), Funcs (F_{2}(),INT),(Funcs (F_{2}(),INT)) \ (F_{3}(),0), F_{7}() -> Variable of F_{6}(), F_{8}() -> Variable of F_{6}(), F_{9}() -> Element of Funcs (F_{2}(),INT), F_{10}() -> INT-Expression of F_{1}(),F_{6}(), P_{1}[ set ] } :

ForDowntoIteration{ F

( P_{1}[F_{6}() . (F_{9}(),F_{5}())] & ( F_{10}() . F_{9}() >= F_{9}() . F_{8}() implies (F_{6}() . (F_{9}(),F_{5}())) . F_{7}() = (F_{9}() . F_{8}()) - 1 ) & ( F_{10}() . F_{9}() < F_{9}() . F_{8}() implies (F_{6}() . (F_{9}(),F_{5}())) . F_{7}() = F_{10}() . F_{9}() ) & (F_{6}() . (F_{9}(),F_{5}())) . F_{8}() = F_{9}() . F_{8}() )

provided
A1:
F_{5}() = for-do ((F_{7}() := F_{10}()),((. F_{8}()) leq (. F_{7}())),(F_{7}() += (- 1)),F_{4}())
and

A2: P_{1}[F_{6}() . (F_{9}(),(F_{7}() := F_{10}()))]
and

A3: for s being Element of Funcs (F_{2}(),INT) st P_{1}[s] holds

( P_{1}[F_{6}() . (s,(F_{4}() \; (F_{7}() += (- 1))))] & P_{1}[F_{6}() . (s,(F_{8}() leq F_{7}()))] )
and

A4: for s being Element of Funcs (F_{2}(),INT) st P_{1}[s] holds

( (F_{6}() . (s,F_{4}())) . F_{7}() = s . F_{7}() & (F_{6}() . (s,F_{4}())) . F_{8}() = s . F_{8}() )
and

A5: ( F_{8}() <> F_{7}() & F_{8}() <> F_{3}() & F_{7}() <> F_{3}() )

A2: P

A3: for s being Element of Funcs (F

( P

A4: for s being Element of Funcs (F

( (F

A5: ( F

proof end;

theorem Th52: :: AOFA_I00:52

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for I being Element of A

for i, n being Variable of g st ex d being Function st

( d . b = 0 & d . n = 1 & d . i = 2 ) & ( for s being Element of Funcs (X,INT) holds

( (g . (s,I)) . n = s . n & (g . (s,I)) . i = s . i ) ) holds

g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n))

for X being non empty countable set

for s being Element of Funcs (X,INT)

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for I being Element of A

for i, n being Variable of g st ex d being Function st

( d . b = 0 & d . n = 1 & d . i = 2 ) & ( for s being Element of Funcs (X,INT) holds

( (g . (s,I)) . n = s . n & (g . (s,I)) . i = s . i ) ) holds

g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n))

proof end;

theorem Th53: :: AOFA_I00:53

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for s being Element of Funcs (X,INT)

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for P being set

for I being Element of A

for i, n being Variable of g st ex d being Function st

( d . b = 0 & d . n = 1 & d . i = 2 ) & ( for s being Element of Funcs (X,INT) st s in P holds

( (g . (s,I)) . n = s . n & (g . (s,I)) . i = s . i & g . (s,I) in P & g . (s,(i leq n)) in P & g . (s,(i += 1)) in P ) ) & s in P holds

g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n))

for X being non empty countable set

for s being Element of Funcs (X,INT)

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for P being set

for I being Element of A

for i, n being Variable of g st ex d being Function st

( d . b = 0 & d . n = 1 & d . i = 2 ) & ( for s being Element of Funcs (X,INT) st s in P holds

( (g . (s,I)) . n = s . n & (g . (s,I)) . i = s . i & g . (s,I) in P & g . (s,(i leq n)) in P & g . (s,(i += 1)) in P ) ) & s in P holds

g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n))

proof end;

theorem Th54: :: AOFA_I00:54

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for t being INT-Expression of A,f

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for I being Element of A st I is_terminating_wrt g holds

for i, n being Variable of g st ex d being Function st

( d . b = 0 & d . n = 1 & d . i = 2 ) & ( for s being Element of Funcs (X,INT) holds

( (g . (s,I)) . n = s . n & (g . (s,I)) . i = s . i ) ) holds

for-do ((i := t),(i leq n),(i += 1),I) is_terminating_wrt g

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for t being INT-Expression of A,f

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for I being Element of A st I is_terminating_wrt g holds

for i, n being Variable of g st ex d being Function st

( d . b = 0 & d . n = 1 & d . i = 2 ) & ( for s being Element of Funcs (X,INT) holds

( (g . (s,I)) . n = s . n & (g . (s,I)) . i = s . i ) ) holds

for-do ((i := t),(i leq n),(i += 1),I) is_terminating_wrt g

proof end;

theorem :: AOFA_I00:55

for A being Euclidean preIfWhileAlgebra

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for t being INT-Expression of A,f

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for P being set

for I being Element of A st I is_terminating_wrt g,P holds

for i, n being Variable of g st ex d being Function st

( d . b = 0 & d . n = 1 & d . i = 2 ) & ( for s being Element of Funcs (X,INT) st s in P holds

( (g . (s,I)) . n = s . n & (g . (s,I)) . i = s . i ) ) & P is_invariant_wrt i := t,g & P is_invariant_wrt I,g & P is_invariant_wrt i leq n,g & P is_invariant_wrt i += 1,g holds

for-do ((i := t),(i leq n),(i += 1),I) is_terminating_wrt g,P

for X being non empty countable set

for T being Subset of (Funcs (X,INT))

for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T

for t being INT-Expression of A,f

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for P being set

for I being Element of A st I is_terminating_wrt g,P holds

for i, n being Variable of g st ex d being Function st

( d . b = 0 & d . n = 1 & d . i = 2 ) & ( for s being Element of Funcs (X,INT) st s in P holds

( (g . (s,I)) . n = s . n & (g . (s,I)) . i = s . i ) ) & P is_invariant_wrt i := t,g & P is_invariant_wrt I,g & P is_invariant_wrt i leq n,g & P is_invariant_wrt i += 1,g holds

for-do ((i := t),(i leq n),(i += 1),I) is_terminating_wrt g,P

proof end;

definition

let X be non empty countable set ;

let A be Euclidean preIfWhileAlgebra;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let s be Element of Funcs (X,INT);

let I be Element of A;

:: original: .

redefine func f . (s,I) -> Element of Funcs (X,INT);

coherence

f . (s,I) is Element of Funcs (X,INT)

end;
let A be Euclidean preIfWhileAlgebra;

let T be Subset of (Funcs (X,INT));

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T;

let s be Element of Funcs (X,INT);

let I be Element of A;

:: original: .

redefine func f . (s,I) -> Element of Funcs (X,INT);

coherence

f . (s,I) is Element of Funcs (X,INT)

proof end;

theorem :: AOFA_I00:56

for A being 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 n, s, i being Variable of g st ex d being Function st

( d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds

(s := 1) \; (for-do ((i := 2),(i leq n),(i += 1),(s *= i))) is_terminating_wrt g

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 n, s, i being Variable of g st ex d being Function st

( d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds

(s := 1) \; (for-do ((i := 2),(i leq n),(i += 1),(s *= i))) is_terminating_wrt g

proof end;

theorem :: AOFA_I00:57

for A being 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 n, s, i being Variable of g st ex d being Function st

( d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds

for q being Element of Funcs (X,INT)

for N being Nat st N = q . n holds

(g . (q,((s := 1) \; (for-do ((i := 2),(i leq n),(i += 1),(s *= i)))))) . s = N !

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 n, s, i being Variable of g st ex d being Function st

( d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds

for q being Element of Funcs (X,INT)

for N being Nat st N = q . n holds

(g . (q,((s := 1) \; (for-do ((i := 2),(i leq n),(i += 1),(s *= i)))))) . s = N !

proof end;

theorem :: AOFA_I00:58

for A being 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, n, s, i being Variable of g st ex d being Function st

( d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds

(s := 1) \; (for-do ((i := 1),(i leq n),(i += 1),(s *= x))) is_terminating_wrt g

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, n, s, i being Variable of g st ex d being Function st

( d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds

(s := 1) \; (for-do ((i := 1),(i leq n),(i += 1),(s *= x))) is_terminating_wrt g

proof end;

theorem :: AOFA_I00:59

for A being 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, n, s, i being Variable of g st ex d being Function st

( d . x = 0 & d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds

for q being Element of Funcs (X,INT)

for N being Nat st N = q . n holds

(g . (q,((s := 1) \; (for-do ((i := 1),(i leq n),(i += 1),(s *= x)))))) . s = (q . x) |^ N

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, n, s, i being Variable of g st ex d being Function st

( d . x = 0 & d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds

for q being Element of Funcs (X,INT)

for N being Nat st N = q . n holds

(g . (q,((s := 1) \; (for-do ((i := 1),(i leq n),(i += 1),(s *= x)))))) . s = (q . x) |^ N

proof end;

theorem :: AOFA_I00:60

for A being 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 n, x, y, z, i being Variable of g st ex d being Function st

( d . b = 0 & d . n = 1 & d . x = 2 & d . y = 3 & d . z = 4 & d . i = 5 ) holds

((x := 0) \; (y := 1)) \; (for-do ((i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z)))) is_terminating_wrt g

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 n, x, y, z, i being Variable of g st ex d being Function st

( d . b = 0 & d . n = 1 & d . x = 2 & d . y = 3 & d . z = 4 & d . i = 5 ) holds

((x := 0) \; (y := 1)) \; (for-do ((i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z)))) is_terminating_wrt g

proof end;

theorem :: AOFA_I00:61

for A being 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 n, x, y, z, i being Variable of g st ex d being Function st

( d . b = 0 & d . n = 1 & d . x = 2 & d . y = 3 & d . z = 4 & d . i = 5 ) holds

for s being Element of Funcs (X,INT)

for N being Element of NAT st N = s . n holds

(g . (s,(((x := 0) \; (y := 1)) \; (for-do ((i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))))))) . x = Fib N

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 n, x, y, z, i being Variable of g st ex d being Function st

( d . b = 0 & d . n = 1 & d . x = 2 & d . y = 3 & d . z = 4 & d . i = 5 ) holds

for s being Element of Funcs (X,INT)

for N being Element of NAT st N = s . n holds

(g . (s,(((x := 0) \; (y := 1)) \; (for-do ((i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))))))) . x = Fib N

proof end;

Lm1: for A being 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) \; (z %= y)) \; (x := y)) \; (y := z)))) . x = s . y & (g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . y = (s . x) mod (s . y) & ( for n, m being Element of NAT holds

not ( m = s . y & ( s in (Funcs (X,INT)) \ (b,0) implies m > 0 ) & ( m > 0 implies s in (Funcs (X,INT)) \ (b,0) ) & not g iteration_terminates_for ((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0),s ) ) )

proof end;

theorem :: AOFA_I00:62

for A being 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) \; (z %= y)) \; (x := y)) \; (y := z))) is_terminating_wrt g, { s where s is Element of Funcs (X,INT) : ( s . x > s . y & s . y >= 0 ) }

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) \; (z %= y)) \; (x := y)) \; (y := z))) is_terminating_wrt g, { s where s is Element of Funcs (X,INT) : ( s . x > s . y & s . y >= 0 ) }

proof end;

theorem :: AOFA_I00:63

for A being 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)

for n, m being Element of NAT st n = s . x & m = s . y & n > m holds

(g . (s,(while ((y gt 0),((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))))) . x = n gcd m

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)

for n, m being Element of NAT st n = s . x & m = s . y & n > m holds

(g . (s,(while ((y gt 0),((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))))) . x = n gcd m

proof end;

Lm2: for A being 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 ) )

proof end;

theorem :: AOFA_I00:64

for A being 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 ) }

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 ) }

proof end;

theorem :: AOFA_I00:65

for A being 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)

for n, m being Element of NAT st n = s . x & m = s . y & n > 0 holds

(g . (s,(while ((y gt 0),((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))))) . x = n gcd m

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)

for n, m being Element of NAT st n = s . x & m = s . y & n > 0 holds

(g . (s,(while ((y gt 0),((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))))) . x = n gcd m

proof end;

theorem :: AOFA_I00:66

for A being 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, m being Variable of g st ex d being Function st

( d . b = 0 & d . x = 1 & d . y = 2 & d . m = 3 ) holds

(y := 1) \; (while ((m gt 0),(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x)))) is_terminating_wrt g, { s where s is Element of Funcs (X,INT) : s . m >= 0 }

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, m being Variable of g st ex d being Function st

( d . b = 0 & d . x = 1 & d . y = 2 & d . m = 3 ) holds

(y := 1) \; (while ((m gt 0),(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x)))) is_terminating_wrt g, { s where s is Element of Funcs (X,INT) : s . m >= 0 }

proof end;

theorem :: AOFA_I00:67

for A being 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, m being Variable of g st ex d being Function st

( d . b = 0 & d . x = 1 & d . y = 2 & d . m = 3 ) holds

for s being Element of Funcs (X,INT)

for n being Nat st n = s . m holds

(g . (s,((y := 1) \; (while ((m gt 0),(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x))))))) . y = (s . x) |^ n

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, m being Variable of g st ex d being Function st

( d . b = 0 & d . x = 1 & d . y = 2 & d . m = 3 ) holds

for s being Element of Funcs (X,INT)

for n being Nat st n = s . m holds

(g . (s,((y := 1) \; (while ((m gt 0),(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x))))))) . y = (s . x) |^ n

proof end;

:: to suggest that Euclid algoritm could be annotated

:: in quite natural way (all needed expressions are allowed).