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-2021 Association of Mizar Users

theorem Th1: :: AOFA_I00:1

for x, y, z, a, b, c being set st a <> b & b <> c & c <> a holds
ex f being Function st
( f . a = x & f . b = y & f . c = z )

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

end;

:: deftheorem Def2 defines Variable AOFA_I00:def 2 :

notation

let f be real-valued Function;
let x be Real;
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 object st s in dom it holds
it . s = (t1 . s) div (t2 . s) ) );

correctness

proof end;

func t1 mod t2 -> INT -valued Function means :Def4: :: AOFA_I00:def 4
( dom it = (dom t1) /\ (dom t2) & ( for s being object st s in dom it holds
it . s = (t1 . s) mod (t2 . s) ) );

correctness

proof end;

func leq (t1,t2) -> INT -valued Function means :Def5: :: AOFA_I00:def 5
( dom it = (dom t1) /\ (dom t2) & ( for s being object st s in dom it holds
it . s = IFGT ((t1 . s),(t2 . s),0,1) ) );

correctness

proof end;

func gt (t1,t2) -> INT -valued Function means :Def6: :: AOFA_I00:def 6
( dom it = (dom t1) /\ (dom t2) & ( for s being object st s in dom it holds
it . s = IFGT ((t1 . s),(t2 . s),1,0) ) );

correctness

proof end;

func eq (t1,t2) -> INT -valued Function means :Def7: :: AOFA_I00:def 7
( dom it = (dom t1) /\ (dom t2) & ( for s being object st s in dom it holds
it . s = IFEQ ((t1 . s),(t2 . s),1,0) ) );

correctness

proof end;

end;

:: deftheorem Def3 defines div AOFA_I00:def 3 :

:: deftheorem Def4 defines mod AOFA_I00:def 4 :

:: deftheorem Def5 defines leq AOFA_I00:def 5 :

:: deftheorem Def6 defines gt AOFA_I00:def 6 :

:: deftheorem Def7 defines eq AOFA_I00:def 7 :

definition

let X be non empty set ;
let f be Function of X,INT;
let x be Integer;

:: original: +
redefine func f + x -> Function of X,INT means :Def8: :: AOFA_I00:def 8
for s being Element of X holds it . s = (f . s) + x;

compatibility

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 :Def10: :: AOFA_I00:def 10
for s being Element of X holds it . s = (f . s) * x;

compatibility

proof end;

coherence

proof end;

end;

:: deftheorem Def8 defines + AOFA_I00:def 8 :

:: deftheorem defines - AOFA_I00:def 9 :

:: deftheorem Def10 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 :Def11: :: 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 Def11 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 :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

proof end;

existence

proof end;

end;

:: deftheorem Def13 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 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

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

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

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
for n, m being Nat holds (x to_power n) to_power m = x to_power (n * m) by NEWTON:9;

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 :: 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 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 :: 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 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 A1: ex I being Element of A st I is_assignment_wrt A,X,f ;

mode INT-Variable of A,f -> INT-Variable of X means :: AOFA_I00:def 16
ex t being INT-Expression of X st it,t form_assignment_wrt f;

existence

proof end;

end;

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

definition

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 :Def18: :: AOFA_I00:def 18
for s being Element of Funcs (X,INT) holds it . s = s . x;

correctness

proof end;

end;

:: deftheorem Def18 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 :Def19: :: AOFA_I00:def 19
for s being Element of Funcs (X,INT) holds it . s = s . (v . s);

correctness

proof end;

end;

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

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;

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

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

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

proof end;

end;

:: deftheorem Def25 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 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

proof end;

end;

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

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

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

proof end;

end;

registration

cluster FreeUnivAlgNSG (ECIW-signature,INT-ElemIns) -> Euclidean ;

coherence

proof end;

end;

registration

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

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

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

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

proof end;

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

end;

definition

:: 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 by Def22;
compatibility

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 by Def22;
compatibility

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

proof end;

coherence 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 by Def22;
compatibility

proof end;

end;

:: deftheorem Def29 defines div AOFA_I00:def 29 :

:: deftheorem Def30 defines mod AOFA_I00:def 30 :

:: deftheorem Def31 defines leq AOFA_I00:def 31 :

:: deftheorem Def32 defines gt AOFA_I00:def 32 :

definition

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

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 by Def22;

end;

:: deftheorem defines . AOFA_I00:def 34 :

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 by Def22;

end;

:: deftheorem defines ^ AOFA_I00:def 35 :

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 ;

end;

:: deftheorem defines . AOFA_I00:def 36 :

theorem Th22: :: AOFA_I00:22

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;

func . (i,A,f) -> INT-Expression of A,f equals :: AOFA_I00:def 37
. (i,X);

coherence by Def22;

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

coherence

proof end;

end;

:: deftheorem defines := AOFA_I00:def 38 :

theorem Th23: :: AOFA_I00:23

proof end;

registration

cluster v := t -> absolutely-terminating ;

coherence by Th23, AOFA_000:95;

end;

definition

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

func x := y -> absolutely-terminating Element of A equals :: AOFA_I00:def 42
x := (. y);

correctness ;

end;

:: deftheorem defines := AOFA_I00:def 42 :

definition

func x := v -> absolutely-terminating Element of A equals :: AOFA_I00:def 43
x := (. v);

correctness ;

end;

:: deftheorem defines := AOFA_I00:def 43 :

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 ;

end;

:: deftheorem defines := AOFA_I00:def 44 :

definition

func x := i -> absolutely-terminating Element of A equals :: AOFA_I00:def 45
x := (. (i,A,f));

correctness ;

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

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

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

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

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

func v1 leq v2 -> absolutely-terminating Element of A equals :: AOFA_I00:def 64
(. v1) leq (. v2);

coherence ;

func v1 gt v2 -> absolutely-terminating Element of A equals :: AOFA_I00:def 65
(. v1) gt (. v2);

coherence ;

end;

:: deftheorem defines leq AOFA_I00:def 64 :

:: deftheorem defines gt AOFA_I00:def 65 :

notation

end;

definition

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

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 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 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
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
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 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 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 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 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
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
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{ 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

A1: F₅() = for-do ((F₇() := F₁₀()),(F₇() leq F₈()),(F₇() += 1),F₄()) and
A2: P₁[F₆() . (F₉(),(F₇() := F₁₀()))] and
A3: 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
A4: 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
A5: ( 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

A1: F₅() = for-do ((F₇() := F₁₀()),((. F₈()) leq (. F₇())),(F₇() += (- 1)),F₄()) and
A2: P₁[F₆() . (F₉(),(F₇() := F₁₀()))] and
A3: 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
A4: 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
A5: ( F₈() <> F₇() & F₈() <> F₃() & F₇() <> F₃() )

proof end;

theorem Th52: :: AOFA_I00:52

for A being Euclidean preIfWhileAlgebra
for X being non empty countable set
for s being Element of Funcs (X,INT)
for b being Element of X
for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)
for I being Element of A
for i, n being Variable of g st ex d being Function st
( d . b = 0 & d . n = 1 & d . i = 2 ) & ( for s being Element of Funcs (X,INT) holds
( (g . (s,I)) . n = s . n & (g . (s,I)) . i = s . i ) ) holds
g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n))

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;

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 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 = |.((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;

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;