AOFA_I00: Mizar Analysis of Algorithms: Algorithms over Integers

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

theorem Lem3: :: 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

proof end;

end;

:: deftheorem defines \ AOFA_I00:def 1 :

theorem LemTS: :: 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 :ELEM: :: AOFA_I00:def 2
verum;
existence ;

end;

:: deftheorem ELEM defines Variable AOFA_I00:def 2 :

notation

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

end;

definition

let t1, t2 be integer-yielding Function;
func t1 div t2 -> integer-yielding Function means :DEFdiv: :: 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

proof end;

func t1 mod t2 -> integer-yielding Function means :DEFmod: :: 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

proof end;

func leq t1,t2 -> integer-yielding Function means :DEFleq: :: 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

proof end;

func gt t1,t2 -> integer-yielding Function means :DEFgt: :: 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

proof end;

func eq t1,t2 -> integer-yielding Function means :DEFeq: :: 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

proof end;

end;

:: deftheorem DEFdiv defines div AOFA_I00:def 3 :

:: deftheorem DEFmod defines mod AOFA_I00:def 4 :

:: deftheorem DEFleq defines leq AOFA_I00:def 5 :

:: deftheorem DEFgt defines gt AOFA_I00:def 6 :

:: deftheorem DEFeq defines eq AOFA_I00:def 7 :

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 :DEFplus2: :: AOFA_I00:def 8
for s being Element of X holds it . s = (f . s) + x;
compatibility

proof end;

coherence

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

proof end;

coherence

proof end;

:: original: *
redefine func f * x -> Function of X, INT means :DEFmult2: :: AOFA_I00:def 10
for s being Element of X holds it . s = (f . s) * x;
compatibility

proof end;

coherence

proof end;

end;

:: deftheorem DEFplus2 defines + AOFA_I00:def 8 :

:: deftheorem defines - AOFA_I00:def 9 :

:: deftheorem DEFmult2 defines * AOFA_I00:def 10 :

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

proof end;

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

proof end;

:: original: leq
redefine func leq f,g -> Function of X, INT ;
coherence

proof end;

:: original: gt
redefine func gt f,g -> Function of X, INT ;
coherence

proof end;

:: original: eq
redefine func eq f,g -> Function of X, INT ;
coherence

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 :DEFminus3: :: AOFA_I00:def 11
for s being Element of X holds it . s = (t1 . s) - (t2 . s);
compatibility

proof end;

coherence

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

proof end;

coherence

proof end;

end;

:: deftheorem DEFminus3 defines - AOFA_I00:def 11 :

:: deftheorem defines + AOFA_I00:def 12 :

registration

let A be non empty set ;
let B be infinite set ;
cluster Funcs A,B -> infinite ;
coherence

proof end;

end;

definition

let N be set ;
let v, f be Function;
func v ** f,N -> Function means :DSTAR: :: 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

proof end;

existence

proof end;

end;

:: deftheorem DSTAR defines ** AOFA_I00:def 13 :

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

proof end;

end;

theorem LemR: :: AOFA_I00:3

for f1, f2, g being Function st rng g c= dom f2 holds
(f1 +* f2) * g = f2 * g

proof end;

theorem LemQ: :: 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 ThDS1: :: 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 one-to-one onto Relation of X, card X;
existence

proof end;

cluster one-to-one onto Relation of card X,X;
existence

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 ThNum1: :: 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 ThNum2: :: 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 ThNum6: :: 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 ThNum4: :: AOFA_I00:10

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

theorem ThNum5: :: 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

proof end;

end;

definition

let X be set ;
let f be Denumeration of X;
:: original: "
redefine func f " -> Enumeration of X;
coherence

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

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 :IA: :: 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 IA defines is_assignment_wrt AOFA_I00:def 14 :

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 :FA: :: 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 FA defines form_assignment_wrt AOFA_I00:def 15 :

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

proof end;

end;

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

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

proof end;

end;

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

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

proof end;

end;

definition

let X be non empty set ;
let x be Element of X;
func . x -> INT-Expression of X means :DEFvarexp1: :: AOFA_I00:def 18
for s being Element of Funcs X,INT holds it . s = s . x;
correctness

proof end;

end;

:: deftheorem DEFvarexp1 defines . AOFA_I00:def 18 :

definition

let X be non empty set ;
let v be INT-Variable of X;
func . v -> INT-Expression of X means :DEFvarexp: :: AOFA_I00:def 19
for s being Element of Funcs X,INT holds it . s = s . (v . s);
correctness

proof end;

end;

:: deftheorem DEFvarexp defines . AOFA_I00:def 19 :

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 ;

end;

:: deftheorem defines ^ AOFA_I00:def 20 :

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

proof end;

end;

:: deftheorem defines . AOFA_I00:def 21 :

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;

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 :INT'iwa: :: 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 INT'iwa defines Euclidean AOFA_I00:def 22 :

definition

let A be preIfWhileAlgebra;
attr A is Euclidean means :INT'iwa2: :: 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 INT'iwa2 defines Euclidean AOFA_I00:def 23 :

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 ;

end;

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

definition

mode INT-Exec -> ExecutionFunction of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns , Funcs NAT ,INT ,(Funcs NAT ,INT ) \ 0 ,0 means :INTiwaEXEC: :: 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

proof end;

end;

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

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 ;

end;

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

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

proof end;

end;

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

definition

let X be non empty set ;
let T be Subset of (Funcs X,INT );
let c be Enumeration of X;
assume A: rng c c= NAT ;
mode INT-Exec of c,T -> ExecutionFunction of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns , Funcs X,INT ,T means :INTiwaEXECc: :: 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

proof end;

end;

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

theorem II1: :: 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 II2: :: 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 II3: :: 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 INT-Exec ;
coherence

proof end;

end;

theorem cII1: :: 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 cII2: :: 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 cII3: :: 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 INT-Exec of c,T;
coherence

proof end;

end;

registration

cluster FreeUnivAlgNSG ECIW-signature ,INT-ElemIns -> Euclidean ;
coherence

proof end;

end;

registration

cluster non degenerated Euclidean L6();
existence

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 Euclidean ExecutionFunction of A, Funcs X,INT ,T;
existence by INT'iwa2;

end;

definition

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

proof end;

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

proof end;

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

proof end;

end;

definition

proof end;

:: original: +
redefine func t1 + t2 -> INT-Expression of A,f;
coherence by INT'iwa;
:: original: (#)
redefine func t1 (#) t2 -> INT-Expression of A,f;
coherence by INT'iwa;

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 :DEFdiv2: :: AOFA_I00:def 29
for s being Element of Funcs X,INT holds it . s = (t1 . s) div (t2 . s);
coherence by INT'iwa;
compatibility

proof end;

:: original: mod
redefine func t1 mod t2 -> INT-Expression of A,f means :DEFmod2: :: AOFA_I00:def 30
for s being Element of Funcs X,INT holds it . s = (t1 . s) mod (t2 . s);
coherence by INT'iwa;
compatibility

proof end;

:: original: leq
redefine func leq t1,t2 -> INT-Expression of A,f means :DEFleq2: :: AOFA_I00:def 31
for s being Element of Funcs X,INT holds it . s = IFGT (t1 . s),(t2 . s),0 ,1;
compatibility

proof end;

coherence by INT'iwa;
:: original: gt
redefine func gt t1,t2 -> INT-Expression of A,f means :DEFgt2: :: AOFA_I00:def 32
for s being Element of Funcs X,INT holds it . s = IFGT (t1 . s),(t2 . s),1,0 ;
coherence by INT'iwa;
compatibility

proof end;

end;

:: deftheorem DEFdiv2 defines div AOFA_I00:def 29 :

:: deftheorem DEFmod2 defines mod AOFA_I00:def 30 :

:: deftheorem DEFleq2 defines leq AOFA_I00:def 31 :

:: deftheorem DEFgt2 defines gt AOFA_I00:def 32 :

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

proof end;

coherence

proof end;

end;

:: deftheorem defines eq AOFA_I00:def 33 :

definition

end;

:: deftheorem defines . AOFA_I00:def 34 :

definition

end;

:: deftheorem defines ^ AOFA_I00:def 35 :

notation

end;

definition

end;

:: deftheorem defines . AOFA_I00:def 36 :

theorem ThE1: :: 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

end;

:: deftheorem defines . AOFA_I00:def 37 :

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

proof end;

end;

:: deftheorem defines := AOFA_I00:def 38 :

theorem Th99: :: 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 by Th99, 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 ;
func v *= t -> absolutely-terminating Element of A equals :: AOFA_I00:def 40
v := ((. v) (#) t);
coherence ;

end;

:: deftheorem defines += AOFA_I00:def 39 :

:: deftheorem defines *= AOFA_I00:def 40 :

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 ;

end;

:: deftheorem defines := AOFA_I00:def 41 :

definition

end;

:: deftheorem defines := AOFA_I00:def 42 :

definition

end;

:: deftheorem defines := AOFA_I00:def 43 :

definition

end;

:: deftheorem defines := AOFA_I00:def 44 :

definition

end;

:: deftheorem defines := AOFA_I00:def 45 :

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 ;

end;

:: deftheorem defines swap AOFA_I00:def 46 :

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

end;

:: deftheorem defines += AOFA_I00:def 47 :

:: deftheorem defines *= AOFA_I00:def 48 :

:: deftheorem defines %= AOFA_I00:def 49 :

:: deftheorem defines /= AOFA_I00:def 50 :

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 ;
func x *= i -> absolutely-terminating Element of A equals :: AOFA_I00:def 52
x := ((. x) * i);
correctness ;
func x %= i -> absolutely-terminating Element of A equals :: AOFA_I00:def 53
x := ((. x) mod (. i,A,f));
correctness ;
func x /= i -> absolutely-terminating Element of A equals :: AOFA_I00:def 54
x := ((. x) div (. i,A,f));
correctness ;
func x div i -> INT-Expression of A,f equals :: AOFA_I00:def 55
(. x) div (. i,A,f);
correctness ;

end;

:: deftheorem defines += AOFA_I00:def 51 :

:: deftheorem defines *= AOFA_I00:def 52 :

:: deftheorem defines %= AOFA_I00:def 53 :

:: deftheorem defines /= AOFA_I00:def 54 :

:: deftheorem defines div AOFA_I00:def 55 :

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 ;

end;

:: deftheorem defines := AOFA_I00:def 56 :

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

end;

:: deftheorem defines += AOFA_I00:def 57 :

:: deftheorem defines *= AOFA_I00:def 58 :

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 ;
func t1 is_even -> absolutely-terminating Element of A equals :: AOFA_I00:def 60
b := ((t1 + 1) mod (. 2,A,g));
coherence ;
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 ;
func t1 gt t2 -> absolutely-terminating Element of A equals :: AOFA_I00:def 62
b := (gt t1,t2);
coherence ;
func t1 eq t2 -> absolutely-terminating Element of A equals :: AOFA_I00:def 63
b := (eq t1,t2);
coherence ;

end;

:: deftheorem defines is_odd AOFA_I00:def 59 :

:: deftheorem defines is_even AOFA_I00:def 60 :

:: deftheorem defines leq AOFA_I00:def 61 :

:: deftheorem defines gt AOFA_I00:def 62 :

:: deftheorem defines eq AOFA_I00:def 63 :

notation

end;

definition

end;

:: deftheorem defines leq AOFA_I00:def 64 :

:: deftheorem defines gt AOFA_I00:def 65 :

notation

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

end;

:: deftheorem defines is_odd AOFA_I00:def 66 :

:: deftheorem defines is_even AOFA_I00:def 67 :

:: deftheorem defines leq AOFA_I00:def 68 :

:: deftheorem defines gt AOFA_I00:def 69 :

notation

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

end;

:: deftheorem defines leq AOFA_I00:def 70 :

:: deftheorem defines geq AOFA_I00:def 71 :

:: deftheorem defines gt AOFA_I00:def 72 :

:: deftheorem defines lt AOFA_I00:def 73 :

:: deftheorem defines / AOFA_I00:def 74 :

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

end;

:: deftheorem defines += AOFA_I00:def 75 :

:: deftheorem defines *= AOFA_I00:def 76 :

:: deftheorem defines %= AOFA_I00:def 77 :

:: deftheorem defines /= AOFA_I00:def 78 :

:: deftheorem defines + AOFA_I00:def 79 :

:: deftheorem defines * AOFA_I00:def 80 :

:: deftheorem defines mod AOFA_I00:def 81 :

:: deftheorem defines div AOFA_I00:def 82 :

theorem Th100: :: 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 Th011: :: 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 Th111: :: 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 Th211: :: 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 Th012: :: 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 Th112: :: 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 Th212: :: 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 Th013: :: 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 Th113: :: 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 Th213: :: 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 Th014: :: 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 Th114: :: 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 Th015: :: 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 Th115: :: 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 Th015': :: 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 Th116: :: 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 Th216: :: 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 Th017: :: 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 Th117: :: 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 Th118: :: 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 Th218: :: 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 Th318: :: 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
( ( not t . s is even implies g . s,(t is_odd ) in (Funcs X,INT ) \ b,0 ) & ( g . s,(t is_odd ) in (Funcs X,INT ) \ b,0 implies not t . s is even ) & ( 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
( ( not s . x is even implies g . s,(x is_odd ) in (Funcs X,INT ) \ b,0 ) & ( g . s,(x is_odd ) in (Funcs X,INT ) \ b,0 implies not s . x is even ) & ( s . x is even implies g . s,(x is_even ) in (Funcs X,INT ) \ b,0 ) & ( g . s,(x is_even ) in (Funcs X,INT ) \ b,0 implies s . x is even ) )

proof end;

scheme :: AOFA_I00:sch 1
ForToIteration{ F₁() -> Euclidean preIfWhileAlgebra, F₂() -> non empty countable set , F₃() -> Element of F₂(), F₄() -> Element of F₁(), F₅() -> Element of F₁(), F₆() -> Euclidean ExecutionFunction of F₁(), Funcs F₂(),INT ,(Funcs F₂(),INT ) \ F₃(),0 , F₇() -> Variable of F₆(), F₈() -> Variable of F₆(), F₉() -> Element of Funcs F₂(),INT , F₁₀() -> INT-Expression of F₁(),F₆(), P₁[ set ] } :

( P₁[F₆() . F₉(),F₅()] & ( F₁₀() . F₉() <= F₉() . F₈() implies (F₆() . F₉(),F₅()) . F₇() = (F₉() . F₈()) + 1 ) & ( F₁₀() . F₉() > F₉() . F₈() implies (F₆() . F₉(),F₅()) . F₇() = F₁₀() . F₉() ) & (F₆() . F₉(),F₅()) . F₈() = F₉() . F₈() )

provided

F: F₅() = for-do (F₇() := F₁₀()),(F₇() leq F₈()),(F₇() += 1),F₄() and
A: P₁[F₆() . F₉(),(F₇() := F₁₀())] and
B: for s being Element of Funcs F₂(),INT st P₁[s] holds
( P₁[F₆() . s,(F₄() \; (F₇() += 1))] & P₁[F₆() . s,(F₇() leq F₈())] ) and
C: for s being Element of Funcs F₂(),INT st P₁[s] holds
( (F₆() . s,F₄()) . F₇() = s . F₇() & (F₆() . s,F₄()) . F₈() = s . F₈() ) and
D: ( F₈() <> F₇() & F₈() <> F₃() & F₇() <> F₃() )

proof end;

scheme :: AOFA_I00:sch 2
ForDowntoIteration{ F₁() -> Euclidean preIfWhileAlgebra, F₂() -> non empty countable set , F₃() -> Element of F₂(), F₄() -> Element of F₁(), F₅() -> Element of F₁(), F₆() -> Euclidean ExecutionFunction of F₁(), Funcs F₂(),INT ,(Funcs F₂(),INT ) \ F₃(),0 , F₇() -> Variable of F₆(), F₈() -> Variable of F₆(), F₉() -> Element of Funcs F₂(),INT , F₁₀() -> INT-Expression of F₁(),F₆(), P₁[ set ] } :

( P₁[F₆() . F₉(),F₅()] & ( F₁₀() . F₉() >= F₉() . F₈() implies (F₆() . F₉(),F₅()) . F₇() = (F₉() . F₈()) - 1 ) & ( F₁₀() . F₉() < F₉() . F₈() implies (F₆() . F₉(),F₅()) . F₇() = F₁₀() . F₉() ) & (F₆() . F₉(),F₅()) . F₈() = F₉() . F₈() )

provided

F: F₅() = for-do (F₇() := F₁₀()),((. F₈()) leq (. F₇())),(F₇() += (- 1)),F₄() and
A: P₁[F₆() . F₉(),(F₇() := F₁₀())] and
B: for s being Element of Funcs F₂(),INT st P₁[s] holds
( P₁[F₆() . s,(F₄() \; (F₇() += (- 1)))] & P₁[F₆() . s,(F₈() leq F₇())] ) and
C: for s being Element of Funcs F₂(),INT st P₁[s] holds
( (F₆() . s,F₄()) . F₇() = s . F₇() & (F₆() . s,F₄()) . F₈() = s . F₈() ) and
D: ( F₈() <> F₇() & F₈() <> F₃() & F₇() <> F₃() )

proof end;

theorem ThT1: :: 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 ThT12: :: 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 ThT4: :: 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;

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

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 natural number 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 . x = 0 & 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 natural number 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;

LemEAterm: 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 st n = s . x & m = s . y & n > m & ( 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) \; (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;

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

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;