:: Mizar Analysis of Algorithms: Algorithms over Integers
:: by Grzegorz Bancerek
::
:: Received March 18, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users


begin

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 )
proof end;

definition
let F be non empty functional set ;
let x, f be set ;
func F \ (x,f) -> Subset of F equals :: AOFA_I00:def 1
{ g where g is Element of F : g . x <> f } ;
coherence
{ g where g is Element of F : g . x <> f } is Subset of F
proof end;
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 } ;

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 )
proof end;

definition
let X be set ;
let Y, Z be set ;
let f be Function of [:(Funcs (X,INT)),Y:],Z;
mode Variable of f -> Element of X means :Def2: :: AOFA_I00:def 2
verum;
existence
ex b1 being Element of X st verum
;
end;

:: 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 b5 being Element of X holds
( b5 is Variable of f iff verum );

notation
let f be real-valued Function;
let x be real number ;
synonym f * x for x (#) f;
end;

definition
let t1, t2 be INT -valued Function;
func t1 div t2 -> INT -valued Function means :Def3: :: AOFA_I00:def 3
( dom it = (dom t1) /\ (dom t2) & ( for s being set st s in dom it holds
it . s = (t1 . s) div (t2 . s) ) );
correctness
existence
ex b1 being INT -valued Function st
( dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = (t1 . s) div (t2 . s) ) )
;
uniqueness
for b1, b2 being INT -valued Function st dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = (t1 . s) div (t2 . s) ) & dom b2 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b2 holds
b2 . s = (t1 . s) div (t2 . s) ) holds
b1 = b2
;
proof end;
func t1 mod t2 -> INT -valued Function means :Def4: :: AOFA_I00:def 4
( dom it = (dom t1) /\ (dom t2) & ( for s being set st s in dom it holds
it . s = (t1 . s) mod (t2 . s) ) );
correctness
existence
ex b1 being INT -valued Function st
( dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = (t1 . s) mod (t2 . s) ) )
;
uniqueness
for b1, b2 being INT -valued Function st dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = (t1 . s) mod (t2 . s) ) & dom b2 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b2 holds
b2 . s = (t1 . s) mod (t2 . s) ) holds
b1 = b2
;
proof end;
func leq (t1,t2) -> INT -valued Function means :Def5: :: AOFA_I00:def 5
( dom it = (dom t1) /\ (dom t2) & ( for s being set st s in dom it holds
it . s = IFGT ((t1 . s),(t2 . s),0,1) ) );
correctness
existence
ex b1 being INT -valued Function st
( dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = IFGT ((t1 . s),(t2 . s),0,1) ) )
;
uniqueness
for b1, b2 being INT -valued Function st dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = IFGT ((t1 . s),(t2 . s),0,1) ) & dom b2 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b2 holds
b2 . s = IFGT ((t1 . s),(t2 . s),0,1) ) holds
b1 = b2
;
proof end;
func gt (t1,t2) -> INT -valued Function means :Def6: :: AOFA_I00:def 6
( dom it = (dom t1) /\ (dom t2) & ( for s being set st s in dom it holds
it . s = IFGT ((t1 . s),(t2 . s),1,0) ) );
correctness
existence
ex b1 being INT -valued Function st
( dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = IFGT ((t1 . s),(t2 . s),1,0) ) )
;
uniqueness
for b1, b2 being INT -valued Function st dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = IFGT ((t1 . s),(t2 . s),1,0) ) & dom b2 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b2 holds
b2 . s = IFGT ((t1 . s),(t2 . s),1,0) ) holds
b1 = b2
;
proof end;
func eq (t1,t2) -> INT -valued Function means :Def7: :: AOFA_I00:def 7
( dom it = (dom t1) /\ (dom t2) & ( for s being set st s in dom it holds
it . s = IFEQ ((t1 . s),(t2 . s),1,0) ) );
correctness
existence
ex b1 being INT -valued Function st
( dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = IFEQ ((t1 . s),(t2 . s),1,0) ) )
;
uniqueness
for b1, b2 being INT -valued Function st dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = IFEQ ((t1 . s),(t2 . s),1,0) ) & dom b2 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b2 holds
b2 . s = IFEQ ((t1 . s),(t2 . s),1,0) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def3 defines div AOFA_I00:def 3 :
for t1, t2, b3 being INT -valued Function holds
( b3 = t1 div t2 iff ( dom b3 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b3 holds
b3 . s = (t1 . s) div (t2 . s) ) ) );

:: deftheorem Def4 defines mod AOFA_I00:def 4 :
for t1, t2, b3 being INT -valued Function holds
( b3 = t1 mod t2 iff ( dom b3 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b3 holds
b3 . s = (t1 . s) mod (t2 . s) ) ) );

:: deftheorem Def5 defines leq AOFA_I00:def 5 :
for t1, t2, b3 being INT -valued Function holds
( b3 = leq (t1,t2) iff ( dom b3 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b3 holds
b3 . s = IFGT ((t1 . s),(t2 . s),0,1) ) ) );

:: deftheorem Def6 defines gt AOFA_I00:def 6 :
for t1, t2, b3 being INT -valued Function holds
( b3 = gt (t1,t2) iff ( dom b3 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b3 holds
b3 . s = IFGT ((t1 . s),(t2 . s),1,0) ) ) );

:: deftheorem Def7 defines eq AOFA_I00:def 7 :
for t1, t2, b3 being INT -valued Function holds
( b3 = eq (t1,t2) iff ( dom b3 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b3 holds
b3 . s = IFEQ ((t1 . s),(t2 . s),1,0) ) ) );

definition
let X be non empty set ;
let f be Function of X,INT;
let x be integer number ;
:: 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
for b1 being Function of X,INT holds
( b1 = x + f iff for s being Element of X holds b1 . s = (f . s) + x )
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
for b1 being Function of X,INT holds
( b1 = f - x iff for s being Element of X holds b1 . s = (f . s) - x )
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
for b1 being Function of X,INT holds
( b1 = f * x iff for s being Element of X holds b1 . s = (f . s) * x )
proof end;
coherence
f * x is Function of X,INT
proof end;
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 number
for b4 being Function of X,INT holds
( b4 = f + x iff for s being Element of X holds b4 . s = (f . s) + x );

:: deftheorem defines - AOFA_I00:def 9 :
for X being non empty set
for f being Function of X,INT
for x being integer number
for b4 being Function of X,INT holds
( b4 = f - x iff for s being Element of X holds b4 . s = (f . s) - x );

:: deftheorem Def10 defines * AOFA_I00:def 10 :
for X being non empty set
for f being Function of X,INT
for x being integer number
for b4 being Function of X,INT holds
( b4 = f * x iff for s being Element of X holds b4 . s = (f . s) * x );

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
proof end;
:: original: mod
redefine func f mod g -> Function of X,INT;
coherence
f mod g is Function of X,INT
proof end;
:: original: leq
redefine func leq (f,g) -> Function of X,INT;
coherence
leq (f,g) is Function of X,INT
proof end;
:: original: gt
redefine func gt (f,g) -> Function of X,INT;
coherence
gt (f,g) is Function of X,INT
proof end;
:: original: eq
redefine func eq (f,g) -> Function of X,INT;
coherence
eq (f,g) is Function of X,INT
proof end;
end;

definition
let X be non empty set ;
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
for b1 being Function of X,INT holds
( b1 = t1 - t2 iff for s being Element of X holds b1 . s = (t1 . s) - (t2 . s) )
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
for b1 being Function of X,INT holds
( b1 = t1 + t2 iff for s being Element of X holds b1 . s = (t1 . s) + (t2 . s) )
proof end;
coherence
t1 + t2 is Function of X,INT
proof end;
end;

:: deftheorem Def11 defines - AOFA_I00:def 11 :
for X being non empty set
for t1, t2, b4 being Function of X,INT holds
( b4 = t1 - t2 iff for s being Element of X holds b4 . s = (t1 . s) - (t2 . s) );

:: deftheorem defines + AOFA_I00:def 12 :
for X being non empty set
for t1, t2, b4 being Function of X,INT holds
( b4 = t1 + t2 iff for s being Element of X holds b4 . s = (t1 . s) + (t2 . s) );

registration
let A be non empty set ;
let B be infinite set ;
cluster Funcs (A,B) -> infinite ;
coherence
not Funcs (A,B) is finite
proof end;
end;

definition
let N be set ;
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
for b1, b2 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 b1 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 b1 holds
b1 . 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 b2 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 b2 holds
b2 . g = v . (g * f) ) holds
b1 = b2
proof end;
existence
ex b1 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 b1 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 b1 holds
b1 . g = v . (g * f) ) )
proof end;
end;

:: deftheorem Def13 defines ** AOFA_I00:def 13 :
for N being set
for v, f, b4 being Function holds
( b4 = 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 b4 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 b4 holds
b4 . g = v . (g * f) ) ) );

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)
proof end;
end;

theorem Th3: :: AOFA_I00:3
for f1, f2, g being Function st rng g c= dom f2 holds
(f1 +* f2) * g = f2 * g
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
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
proof end;

registration
let X be set ;
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 b1 being Function of X,(card X) st
( b1 is one-to-one & b1 is onto )
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 b1 being Function of (card X),X st
( b1 is one-to-one & b1 is onto )
proof end;
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;

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 ) )
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 ) )
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
proof end;

theorem :: AOFA_I00:9
for X being non empty set
for x being Element of X ex f being Enumeration of X st f . x = 0
proof end;

theorem :: AOFA_I00:10
for X being non empty set
for f being Denumeration of X holds f . 0 in X by FUNCT_2:5, ORDINAL3:8;

theorem Th11: :: AOFA_I00:11
for X being countable set
for f being Enumeration of X holds rng f c= NAT
proof end;

definition
let X be set ;
let f be Enumeration of X;
:: original: "
redefine func f " -> Denumeration of X;
coherence
f " is Denumeration of X
proof end;
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
proof end;
end;

theorem :: AOFA_I00:12
for n, m being Nat holds 0 to_power (n + m) = (0 to_power n) * (0 to_power m)
proof end;

theorem :: AOFA_I00:13
for x being real number
for n, m being Nat holds (x to_power n) to_power m = x to_power (n * m) by NEWTON:9;

begin

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;

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;
pred I is_assignment_wrt A,X,f means :Def14: :: 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)) );
end;

:: deftheorem Def14 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)) ) );

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;
pred v,t form_assignment_wrt f means :Def15: :: 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)) ) );
end;

:: deftheorem Def15 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)) ) ) );

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 B1: 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 b1 being INT-Variable of X ex t being INT-Expression of X st b1,t form_assignment_wrt f
proof end;
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 b5 being INT-Variable of X holds
( b5 is INT-Variable of A,f iff ex t being INT-Expression of X st b5,t form_assignment_wrt f );

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 B1: 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 b1 being INT-Expression of X ex v being INT-Variable of X st v,b1 form_assignment_wrt f
proof end;
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 b5 being INT-Expression of X holds
( b5 is INT-Expression of A,f iff ex v being INT-Variable of X st v,b5 form_assignment_wrt f );

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
proof end;
end;

definition
let X be non empty set ;
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
existence
ex b1 being INT-Expression of X st
for s being Element of Funcs (X,INT) holds b1 . s = s . x
;
uniqueness
for b1, b2 being INT-Expression of X st ( for s being Element of Funcs (X,INT) holds b1 . s = s . x ) & ( for s being Element of Funcs (X,INT) holds b2 . s = s . x ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def18 defines . AOFA_I00:def 18 :
for X being non empty set
for x being Element of X
for b3 being INT-Expression of X holds
( b3 = . x iff for s being Element of Funcs (X,INT) holds b3 . s = s . x );

definition
let X be non empty set ;
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
existence
ex b1 being INT-Expression of X st
for s being Element of Funcs (X,INT) holds b1 . s = s . (v . s)
;
uniqueness
for b1, b2 being INT-Expression of X st ( for s being Element of Funcs (X,INT) holds b1 . s = s . (v . s) ) & ( for s being Element of Funcs (X,INT) holds b2 . s = s . (v . s) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def19 defines . AOFA_I00:def 19 :
for X being non empty set
for v being INT-Variable of X
for b3 being INT-Expression of X holds
( b3 = . v iff for s being Element of Funcs (X,INT) holds b3 . s = s . (v . s) );

definition
let X be non empty set ;
let x be Element of X;
func ^ x -> INT-Variable of X equals :: AOFA_I00:def 20
(Funcs (X,INT)) --> x;
correctness
coherence
(Funcs (X,INT)) --> x is INT-Variable of X
;
;
end;

:: deftheorem defines ^ AOFA_I00:def 20 :
for X being non empty set
for x being Element of X holds ^ x = (Funcs (X,INT)) --> x;

theorem :: AOFA_I00:14
for X being non empty set
for x being Element of X holds . x = . (^ x)
proof end;

definition
let X be non empty set ;
let i be integer number ;
func . (i,X) -> INT-Expression of X equals :: AOFA_I00:def 21
(Funcs (X,INT)) --> i;
correctness
coherence
(Funcs (X,INT)) --> i is INT-Expression of X
;
proof end;
end;

:: deftheorem defines . AOFA_I00:def 21 :
for X being non empty set
for i being integer number 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 )
proof end;

:: The word "Euclidean" is chosen in following definition
:: to suggest that Euclid algoritm could be annotated
:: in quite natural way (all needed expressions are allowed).
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;
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 number 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 ) ) );
end;

:: 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 number 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.
definition
let A be preIfWhileAlgebra;
attr A is Euclidean means :Def23: :: AOFA_I00:def 23
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 ;
end;

:: 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 );

definition
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)):] is infinite disjoint_with_NAT set
;
end;

:: deftheorem defines INT-ElemIns AOFA_I00:def 24 :
INT-ElemIns = [:(Funcs ((Funcs (NAT,INT)),NAT)),(Funcs ((Funcs (NAT,INT)),INT)):];

definition
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
ex b1 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 b1 . (s,(root-tree [v,e])) = s +* ((v . s),(e . s))
proof end;
end;

:: deftheorem Def25 defines INT-Exec AOFA_I00:def 25 :
for b1 being ExecutionFunction of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns), Funcs (NAT,INT),(Funcs (NAT,INT)) \ (0,0) holds
( b1 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 b1 . (s,(root-tree [v,e])) = s +* ((v . s),(e . s)) );

definition
let X be non empty set ;
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)):] is infinite disjoint_with_NAT set
;
end;

:: 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)):];

definition
let X be non empty set ;
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
ex b1 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 b1 . (s,(root-tree [v,e])) = s +* ((v . s),(e . s))
proof end;
end;

:: deftheorem defines INT-Exec AOFA_I00:def 27 :
for X being non empty set
for x being Element of X
for b3 being ExecutionFunction of FreeUnivAlgNSG (ECIW-signature,(INT-ElemIns X)), Funcs (X,INT),(Funcs (X,INT)) \ (x,0) holds
( b3 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 b3 . (s,(root-tree [v,e])) = s +* ((v . s),(e . s)) );

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 ;
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
ex b1 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 b1 . (s,(root-tree [((c * v) ** (c,NAT)),(e ** (c,NAT))])) = s +* ((v . s),(e . s))
proof end;
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 b4 being ExecutionFunction of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns), Funcs (X,INT),T holds
( b4 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 b4 . (s,(root-tree [((c * v) ** (c,NAT)),(e ** (c,NAT))])) = s +* ((v . s),(e . s)) );

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
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
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
proof end;

registration
cluster -> Euclidean for INT-Exec ;
coherence
for b1 being INT-Exec holds b1 is Euclidean
proof end;
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
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
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
proof end;

registration
let X be non empty countable set ;
let T be Subset of (Funcs (X,INT));
let c be Enumeration of X;
cluster -> Euclidean for INT-Exec of c,T;
coherence
for b1 being INT-Exec of c,T holds b1 is Euclidean
proof end;
end;

registration
cluster FreeUnivAlgNSG (ECIW-signature,INT-ElemIns) -> Euclidean ;
coherence
FreeUnivAlgNSG (ECIW-signature,INT-ElemIns) is Euclidean
proof end;
end;

registration
cluster non empty V157() V158() V159() with_empty-instruction with_catenation with_if-instruction with_while-instruction non degenerated Euclidean for L9();
existence
ex b1 being preIfWhileAlgebra st
( b1 is Euclidean & not b1 is degenerated )
proof end;
end;

registration
let A be Euclidean preIfWhileAlgebra;
let X be non empty countable set ;
let T be Subset of (Funcs (X,INT));
cluster non empty Relation-like [:(Funcs (X,INT)), the carrier of A:] -defined Funcs (X,INT) -valued Function-like V29([:(Funcs (X,INT)), the carrier of A:]) quasi_total Function-yielding V89() complying_with_empty-instruction complying_with_catenation Euclidean for ExecutionFunction of A, Funcs (X,INT),T;
existence
ex b1 being ExecutionFunction of A, Funcs (X,INT),T st b1 is Euclidean
by Def23;
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 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;

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 number ;
:: 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;
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
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;
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: 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
t1 div t2 is INT-Expression of A,f
by Def22;
compatibility
for b1 being INT-Expression of A,f holds
( b1 = t1 div t2 iff for s being Element of Funcs (X,INT) holds b1 . s = (t1 . s) div (t2 . s) )
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
t1 mod t2 is INT-Expression of A,f
by Def22;
compatibility
for b1 being INT-Expression of A,f holds
( b1 = t1 mod t2 iff for s being Element of Funcs (X,INT) holds b1 . s = (t1 . s) mod (t2 . s) )
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
for b1 being INT-Expression of A,f holds
( b1 = leq (t1,t2) iff for s being Element of Funcs (X,INT) holds b1 . s = IFGT ((t1 . s),(t2 . s),0,1) )
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
gt (t1,t2) is INT-Expression of A,f
by Def22;
compatibility
for b1 being INT-Expression of A,f holds
( b1 = gt (t1,t2) iff for s being Element of Funcs (X,INT) holds b1 . s = IFGT ((t1 . s),(t2 . s),1,0) )
proof end;
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, b7 being INT-Expression of A,f holds
( b7 = t1 div t2 iff for s being Element of Funcs (X,INT) holds b7 . s = (t1 . s) div (t2 . s) );

:: 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, b7 being INT-Expression of A,f holds
( b7 = t1 mod t2 iff for s being Element of Funcs (X,INT) holds b7 . s = (t1 . s) mod (t2 . s) );

:: 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, b7 being INT-Expression of A,f holds
( b7 = leq (t1,t2) iff for s being Element of Funcs (X,INT) holds b7 . s = IFGT ((t1 . s),(t2 . s),0,1) );

:: 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, b7 being INT-Expression of A,f holds
( b7 = gt (t1,t2) iff for s being Element of Funcs (X,INT) holds b7 . s = IFGT ((t1 . s),(t2 . s),1,0) );

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: 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
for b1 being INT-Expression of A,f holds
( b1 = eq (t1,t2) iff for s being Element of Funcs (X,INT) holds b1 . s = IFEQ ((t1 . s),(t2 . s),1,0) )
proof end;
coherence
eq (t1,t2) is INT-Expression of A,f
proof end;
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, b7 being INT-Expression of A,f holds
( b7 = eq (t1,t2) iff for s being Element of Funcs (X,INT) holds b7 . s = IFEQ ((t1 . s),(t2 . s),1,0) );

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;
func . v -> INT-Expression of A,f equals :: AOFA_I00:def 34
. v;
coherence
. v is INT-Expression of A,f
by Def22;
end;

:: 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;

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;
func x ^ (A,f) -> INT-Variable of A,f equals :: AOFA_I00:def 35
^ x;
coherence
^ x is INT-Variable of A,f
by Def22;
end;

:: 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;

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;

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;
func . x -> INT-Expression of A,f equals :: AOFA_I00:def 36
. (^ x);
coherence
. (^ x) is INT-Expression of A,f
;
end;

:: 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);

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
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 number ;
func . (i,A,f) -> INT-Expression of A,f equals :: AOFA_I00:def 37
. (i,X);
coherence
. (i,X) is INT-Expression of A,f
by Def22;
end;

:: 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 number 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;
func v := t -> Element of A equals :: AOFA_I00:def 38
choose { 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
choose { 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;
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 = choose { 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
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;
cluster v := t -> absolutely-terminating ;
coherence
v := t is absolutely-terminating
by Th23, AOFA_000:95;
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 v be INT-Variable of A,f;
let t be INT-Expression of A,f;
func v += t -> absolutely-terminating Element of A equals :: AOFA_I00:def 39
v := ((. v) + t);
coherence
v := ((. v) + t) is absolutely-terminating Element of A
;
func v *= t -> absolutely-terminating Element of A equals :: AOFA_I00:def 40
v := ((. v) (#) t);
coherence
v := ((. v) (#) t) is absolutely-terminating Element of A
;
end;

:: 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);

:: 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);

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;
func x := t -> absolutely-terminating Element of A equals :: AOFA_I00:def 41
(x ^ (A,f)) := t;
correctness
coherence
(x ^ (A,f)) := t is absolutely-terminating Element of A
;
;
end;

:: 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;

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;
func x := y -> absolutely-terminating Element of A equals :: AOFA_I00:def 42
x := (. y);
correctness
coherence
x := (. y) is absolutely-terminating Element of A
;
;
end;

:: 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);

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;
func x := v -> absolutely-terminating Element of A equals :: AOFA_I00:def 43
x := (. v);
correctness
coherence
x := (. v) is absolutely-terminating Element of A
;
;
end;

:: 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);

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;
func v := w -> absolutely-terminating Element of A equals :: AOFA_I00:def 44
v := (. w);
correctness
coherence
v := (. w) is absolutely-terminating Element of A
;
;
end;

:: 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);

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 number ;
func x := i -> absolutely-terminating Element of A equals :: AOFA_I00:def 45
x := (. (i,A,f));
correctness
coherence
x := (. (i,A,f)) is absolutely-terminating Element of A
;
;
end;

:: 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 number 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;
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)) is absolutely-terminating Element of A
;
end;

:: 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));

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;
func x += t -> absolutely-terminating Element of A equals :: AOFA_I00:def 47
x := ((. x) + t);
correctness
coherence
x := ((. x) + t) is absolutely-terminating Element of A
;
;
func x *= t -> absolutely-terminating Element of A equals :: AOFA_I00:def 48
x := ((. x) (#) t);
correctness
coherence
x := ((. x) (#) t) is absolutely-terminating Element of A
;
;
func x %= t -> absolutely-terminating Element of A equals :: AOFA_I00:def 49
x := ((. x) mod t);
correctness
coherence
x := ((. x) mod t) is absolutely-terminating Element of A
;
;
func x /= t -> absolutely-terminating Element of A equals :: AOFA_I00:def 50
x := ((. x) div t);
correctness
coherence
x := ((. x) div t) is absolutely-terminating Element of A
;
;
end;

:: 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);

:: 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);

:: 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);

:: 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);

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 number ;
func x += i -> absolutely-terminating Element of A equals :: AOFA_I00:def 51
x := ((. x) + i);
correctness
coherence
x := ((. x) + i) is absolutely-terminating Element of A
;
;
func x *= i -> absolutely-terminating Element of A equals :: AOFA_I00:def 52
x := ((. x) * i);
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
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
coherence
x := ((. x) div (. (i,A,f))) is absolutely-terminating Element of A
;
;
func x div i -> INT-Expression of A,f equals :: AOFA_I00:def 55
(. x) div (. (i,A,f));
correctness
coherence
(. x) div (. (i,A,f)) is INT-Expression of A,f
;
;
end;

:: 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 number 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 number 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 number 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 number 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 number 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 number ;
func v := i -> absolutely-terminating Element of A equals :: AOFA_I00:def 56
v := (. (i,A,f));
correctness
coherence
v := (. (i,A,f)) is absolutely-terminating Element of A
;
;
end;

:: 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 number 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 number ;
func v += i -> absolutely-terminating Element of A equals :: AOFA_I00:def 57
v := ((. v) + i);
correctness
coherence
v := ((. v) + i) is absolutely-terminating Element of A
;
;
func v *= i -> absolutely-terminating Element of A equals :: AOFA_I00:def 58
v := ((. v) * i);
correctness
coherence
v := ((. v) * i) is absolutely-terminating Element of A
;
;
end;

:: 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 number 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 number 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;
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))) 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))) is absolutely-terminating Element of A
;
let t2 be INT-Expression of A,g;
func t1 leq t2 -> absolutely-terminating Element of A equals :: AOFA_I00:def 61
b := (leq (t1,t2));
coherence
b := (leq (t1,t2)) is absolutely-terminating Element of A
;
func t1 gt t2 -> absolutely-terminating Element of A equals :: AOFA_I00:def 62
b := (gt (t1,t2));
coherence
b := (gt (t1,t2)) is absolutely-terminating Element of A
;
func t1 eq t2 -> absolutely-terminating Element of A equals :: AOFA_I00:def 63
b := (eq (t1,t2));
coherence
b := (eq (t1,t2)) is absolutely-terminating Element of A
;
end;

:: 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)));

:: 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)));

:: 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));

:: 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));

:: 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));

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;

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;
func v1 leq v2 -> absolutely-terminating Element of A equals :: AOFA_I00:def 64
(. v1) leq (. v2);
coherence
(. v1) leq (. v2) is absolutely-terminating Element of A
;
func v1 gt v2 -> absolutely-terminating Element of A equals :: AOFA_I00:def 65
(. v1) gt (. v2);
coherence
(. v1) gt (. v2) is absolutely-terminating Element of A
;
end;

:: 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);

:: 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);

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;

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;
func x1 is_odd -> absolutely-terminating Element of A equals :: AOFA_I00:def 66
(. x1) is_odd ;
coherence
(. x1) is_odd is absolutely-terminating Element of A
;
func x1 is_even -> absolutely-terminating Element of A equals :: AOFA_I00:def 67
(. x1) is_even ;
coherence
(. x1) is_even is absolutely-terminating Element of A
;
let x2 be Variable of g;
func x1 leq x2 -> absolutely-terminating Element of A equals :: AOFA_I00:def 68
(. x1) leq (. x2);
coherence
(. x1) leq (. x2) is absolutely-terminating Element of A
;
func x1 gt x2 -> absolutely-terminating Element of A equals :: AOFA_I00:def 69
(. x1) gt (. x2);
coherence
(. x1) gt (. x2) is absolutely-terminating Element of A
;
end;

:: 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 ;

:: 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 ;

:: 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);

:: 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);

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;

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 number ;
func x leq i -> absolutely-terminating Element of A equals :: AOFA_I00:def 70
(. x) leq (. (i,A,g));
coherence
(. x) leq (. (i,A,g)) is absolutely-terminating Element of A
;
func x geq i -> absolutely-terminating Element of A equals :: AOFA_I00:def 71
(. x) geq (. (i,A,g));
coherence
(. x) geq (. (i,A,g)) is absolutely-terminating Element of A
;
func x gt i -> absolutely-terminating Element of A equals :: AOFA_I00:def 72
(. x) gt (. (i,A,g));
coherence
(. x) gt (. (i,A,g)) is absolutely-terminating Element of A
;
func x lt i -> absolutely-terminating Element of A equals :: AOFA_I00:def 73
(. x) lt (. (i,A,g));
coherence
(. x) lt (. (i,A,g)) is absolutely-terminating Element of A
;
func x / i -> INT-Expression of A,g equals :: AOFA_I00:def 74
(. x) div (. (i,A,g));
coherence
(. x) div (. (i,A,g)) is INT-Expression of A,g
;
end;

:: 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 number 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 number 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 number 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 number 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 number 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;
func x1 += x2 -> absolutely-terminating Element of A equals :: AOFA_I00:def 75
x1 += (. x2);
coherence
x1 += (. x2) is absolutely-terminating Element of A
;
func x1 *= x2 -> absolutely-terminating Element of A equals :: AOFA_I00:def 76
x1 *= (. x2);
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)) 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)) is absolutely-terminating Element of A
;
func x1 + x2 -> INT-Expression of A,f equals :: AOFA_I00:def 79
(. x1) + (. x2);
coherence
(. x1) + (. x2) is INT-Expression of A,f
;
func x1 * x2 -> INT-Expression of A,f equals :: AOFA_I00:def 80
(. x1) (#) (. x2);
coherence
(. x1) (#) (. x2) is INT-Expression of A,f
;
func x1 mod x2 -> INT-Expression of A,f equals :: AOFA_I00:def 81
(. x1) mod (. x2);
coherence
(. x1) mod (. x2) is INT-Expression of A,f
;
func x1 div x2 -> INT-Expression of A,f equals :: AOFA_I00:def 82
(. x1) div (. x2);
coherence
(. x1) div (. x2) is INT-Expression of A,f
;
end;

:: 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);

:: 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);

:: 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));

:: 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));

:: 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);

:: 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);

:: 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);

:: 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);

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 ) )
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 number 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 ) )
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 ) )
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 number
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 ) )
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 ) )
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 number
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 ) )
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 ) )
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 number 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 ) )
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 number 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 ) )
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 number 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 ) ) )
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 number 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 ) )
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 number
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 ) )
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 ) )
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 number
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 ) )
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 ) )
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 ) ) )
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 ) )
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 ) )
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 ) )
proof end;

scheme :: AOFA_I00:sch 1
ForToIteration{ F1() -> Euclidean preIfWhileAlgebra, F2() -> non empty countable set , F3() -> Element of F2(), F4() -> Element of F1(), F5() -> Element of F1(), F6() -> Euclidean ExecutionFunction of F1(), Funcs (F2(),INT),(Funcs (F2(),INT)) \ (F3(),0), F7() -> Variable of F6(), F8() -> Variable of F6(), F9() -> Element of Funcs (F2(),INT), F10() -> INT-Expression of F1(),F6(), P1[ set ] } :
( P1[F6() . (F9(),F5())] & ( F10() . F9() <= F9() . F8() implies (F6() . (F9(),F5())) . F7() = (F9() . F8()) + 1 ) & ( F10() . F9() > F9() . F8() implies (F6() . (F9(),F5())) . F7() = F10() . F9() ) & (F6() . (F9(),F5())) . F8() = F9() . F8() )
provided
A1: F5() = for-do ((F7() := F10()),(F7() leq F8()),(F7() += 1),F4()) and
A2: P1[F6() . (F9(),(F7() := F10()))] and
A3: for s being Element of Funcs (F2(),INT) st P1[s] holds
( P1[F6() . (s,(F4() \; (F7() += 1)))] & P1[F6() . (s,(F7() leq F8()))] ) and
A4: for s being Element of Funcs (F2(),INT) st P1[s] holds
( (F6() . (s,F4())) . F7() = s . F7() & (F6() . (s,F4())) . F8() = s . F8() ) and
A5: ( F8() <> F7() & F8() <> F3() & F7() <> F3() )
proof end;

scheme :: AOFA_I00:sch 2
ForDowntoIteration{ F1() -> Euclidean preIfWhileAlgebra, F2() -> non empty countable set , F3() -> Element of F2(), F4() -> Element of F1(), F5() -> Element of F1(), F6() -> Euclidean ExecutionFunction of F1(), Funcs (F2(),INT),(Funcs (F2(),INT)) \ (F3(),0), F7() -> Variable of F6(), F8() -> Variable of F6(), F9() -> Element of Funcs (F2(),INT), F10() -> INT-Expression of F1(),F6(), P1[ set ] } :
( P1[F6() . (F9(),F5())] & ( F10() . F9() >= F9() . F8() implies (F6() . (F9(),F5())) . F7() = (F9() . F8()) - 1 ) & ( F10() . F9() < F9() . F8() implies (F6() . (F9(),F5())) . F7() = F10() . F9() ) & (F6() . (F9(),F5())) . F8() = F9() . F8() )
provided
A1: F5() = for-do ((F7() := F10()),((. F8()) leq (. F7())),(F7() += (- 1)),F4()) and
A2: P1[F6() . (F9(),(F7() := F10()))] and
A3: for s being Element of Funcs (F2(),INT) st P1[s] holds
( P1[F6() . (s,(F4() \; (F7() += (- 1))))] & P1[F6() . (s,(F8() leq F7()))] ) and
A4: for s being Element of Funcs (F2(),INT) st P1[s] holds
( (F6() . (s,F4())) . F7() = s . F7() & (F6() . (s,F4())) . F8() = s . F8() ) and
A5: ( F8() <> F7() & F8() <> F3() & F7() <> F3() )
proof end;

begin

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))
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))
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
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
proof end;

begin

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)
proof end;
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
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 !
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
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
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
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
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 ) }
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
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 = abs ((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 ) }
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
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 }
proof end;

:: WP: Correctness of the algorithm of exponentiation by squaring
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
proof end;