:: Mizar Analysis of Algorithms: Algorithms over Integers
:: by Grzegorz Bancerek
::
:: Received March 18, 2008
:: Copyright (c) 2008-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FUNCT_1, FUNCOP_1, RELAT_1, AOFA_000, FUNCT_4, XBOOLE_0,
SUBSET_1, TARSKI, ZFMISC_1, FUNCT_2, ZF_LANG, VALUED_0, VALUED_1, INT_1,
XXREAL_0, CARD_1, ARYTM_3, ARYTM_1, FINSET_1, ORDINAL2, MEMBER_1, CARD_3,
NAT_1, POWER, ORDINAL4, EUCLMETR, FREEALG, TREES_4, LANG1, MCART_1,
STRUCT_0, GRAPHSP, ABIAN, FUNCT_7, REALSET1, NEWTON, PRE_FF, INT_2,
COMPLEX1, AOFA_I00, REAL_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XTUPLE_0, MCART_1, ORDINAL1,
RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSET_1, LANG1, BINOP_1,
CARD_1, CARD_2, CARD_3, VALUED_0, PRE_FF, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, POWER, INT_1, INT_2, NAT_1, NAT_D, NEWTON, ABIAN, FUNCOP_1,
FUNCT_4, FUNCT_7, STRUCT_0, FREEALG, TREES_4, AOFA_000, VALUED_1;
constructors REAL_1, BORSUK_1, PREPOWER, POWER, NAT_D, NEWTON, ABIAN,
SQUARE_1, PRE_FF, WSIERP_1, WELLORD2, CARD_2, CAT_2, AOFA_000, XTUPLE_0,
FUNCT_4;
registrations RELSET_1, FUNCT_1, FUNCOP_1, FUNCT_2, NUMBERS, NAT_1, STRUCT_0,
FREEALG, INT_1, CARD_1, CARD_3, VALUED_0, VALUED_1, MEMBERED, XREAL_0,
XCMPLX_0, XXREAL_0, XBOOLE_0, FINSET_1, POWER, AOFA_000, ABIAN, XTUPLE_0,
ORDINAL1;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
begin :: Preliminaries
theorem :: AOFA_I00:1
for x,y,z,a,b,c being set st a <> b & b <> c & c <> a ex f being
Function st f.a = x & f.b = y & f.c = z;
definition
let F be non empty functional set;
let x be set;
let 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};
end;
theorem :: AOFA_I00:2
for F being non empty functional set, x,y be set, g being Element
of F holds g in F\(x,y) iff g.x <> y;
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
:: AOFA_I00:def 2
not contradiction;
end;
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
:: 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);
func t1 mod t2 -> INT-valued Function means
:: 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);
func leq(t1,t2) -> INT-valued Function means
:: 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);
func gt(t1,t2) -> INT-valued Function means
:: 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);
func eq(t1,t2) -> INT-valued Function means
:: 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);
end;
definition
let X be non empty set;
let f be Function of X, INT;
let x be Integer;
redefine func f+x -> Function of X, INT means
:: AOFA_I00:def 8
for s being Element of X holds it.s = f.s+x;
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;
redefine func f*x -> Function of X, INT means
:: AOFA_I00:def 10
for s being Element of X holds it.s = f.s*x;
end;
definition
let X be set;
let f,g be Function of X, INT;
redefine func f div g -> Function of X, INT;
redefine func f mod g -> Function of X, INT;
redefine func leq(f,g) -> Function of X, INT;
redefine func gt(f,g) -> Function of X, INT;
redefine func eq(f,g) -> Function of X, INT;
end;
definition
let X be non empty set;
let t1,t2 be Function of X, INT;
redefine func t1-t2 -> Function of X, INT means
:: AOFA_I00:def 11
for s being Element of X holds it.s = (t1.s)-(t2.s);
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);
end;
registration
let A be non empty set;
let B be infinite set;
cluster Funcs(A, B) -> infinite;
end;
definition
let N be set;
let v be Function;
let f be Function;
func v**(f,N) -> Function means
:: 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);
end;
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;
redefine func v**(f,N) -> Element of Funcs(Funcs(N,Y),Z);
end;
theorem :: AOFA_I00:3
for f1,f2,g being Function st rng g c= dom f2 holds (f1+*f2)*g = f2*g;
theorem :: 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 for n being Element of I holds (N-->n)
+*(s*c") is Function of N,I;
theorem :: 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) for f being Function of X, N st f is one-to-one
& v1**(f,N) = v2**(f,N) holds v1 = v2;
registration
let X be set;
cluster one-to-one onto for Function of X, card X;
cluster one-to-one onto for Function of card X, X;
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 :: AOFA_I00:6
for X being set, f being Function holds f is Enumeration of X iff
dom f = X & rng f = card X & f is one-to-one;
theorem :: AOFA_I00:7
for X being set, f being Function holds f is Denumeration of X
iff dom f = card X & rng f = X & f is one-to-one;
theorem :: AOFA_I00:8
for X being non empty set, x,y being Element of X for f being
Enumeration of X holds f+*(x,f.y)+*(y,f.x) is Enumeration of X;
theorem :: AOFA_I00:9
for X being non empty set, x being Element of X ex f being Enumeration
of X st f.x = 0;
theorem :: AOFA_I00:10
for X being non empty set, f being Denumeration of X holds f.0 in X;
theorem :: AOFA_I00:11
for X being countable set, f being Enumeration of X holds rng f c= NAT;
definition
let X be set;
let f be Enumeration of X;
redefine func f" -> Denumeration of X;
end;
definition
let X be set;
let f be Denumeration of X;
redefine func f" -> Enumeration of X;
end;
theorem :: AOFA_I00:12
for n,m being Nat holds 0 to_power (n+m) = (0 to_power n)*(0 to_power m);
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);
begin :: If-while algebra over integers
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;
reserve A for preIfWhileAlgebra;
definition
let A;
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, 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;
definition
let 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;
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;
definition
let 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 such that
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;
end;
definition
let 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 such that
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;
end;
definition
let X,Y be non empty set;
let f be Element of Funcs(X,Y);
let x be Element of X;
redefine func f.x -> Element of Y;
end;
definition
let X be non empty set;
let x be Element of X;
func .x -> INT-Expression of X means
:: AOFA_I00:def 18
for s being Element of Funcs(X, INT) holds it.s = s.x;
end;
definition
let X be non empty set;
let v be INT-Variable of X;
func .v -> INT-Expression of X means
:: AOFA_I00:def 19
for s being Element of Funcs(X, INT) holds it.s = s.(v.s);
end;
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;
end;
theorem :: AOFA_I00:14
for X being non empty set for x being Element of X holds .x = .(^x);
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;
end;
theorem :: AOFA_I00:15
for X being non empty set, t being INT-Expression of X holds t+ .(0,X)
= t & t(#).(1,X) = t;
:: 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;
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
:: AOFA_I00:def 22
(for v being INT-Variable of A,f, 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;
:: 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;
attr A is Euclidean means
:: AOFA_I00:def 23
for X being non empty countable set, T
being Subset of Funcs(X, INT) ex f being ExecutionFunction of A, Funcs(X, INT),
T st f is Euclidean;
end;
definition
func INT-ElemIns -> infinite disjoint_with_NAT set equals
:: AOFA_I00:def 24
[:Funcs(Funcs(NAT, INT), NAT), Funcs(Funcs(NAT, INT), INT):];
end;
definition
mode INT-Exec -> ExecutionFunction of FreeUnivAlgNSG(ECIW-signature,
INT-ElemIns), Funcs(NAT, INT), Funcs(NAT,INT)\(0,0) means
:: 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);
end;
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):];
end;
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);
end;
definition
let X be non empty set;
let T be Subset of Funcs(X, INT);
let c be Enumeration of X such that
rng c c= NAT;
mode INT-Exec of c,T -> ExecutionFunction of FreeUnivAlgNSG(ECIW-signature,
INT-ElemIns), Funcs(X, INT), T means
:: 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);
end;
theorem :: 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;
theorem :: 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;
theorem :: 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;
registration
cluster -> Euclidean for INT-Exec;
end;
theorem :: 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;
theorem :: 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;
theorem :: 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;
registration
let X be countable non empty set;
let T be Subset of Funcs(X, INT);
let c be Enumeration of X;
cluster -> Euclidean for INT-Exec of c,T;
end;
registration
cluster FreeUnivAlgNSG(ECIW-signature, INT-ElemIns) -> Euclidean;
end;
registration
cluster Euclidean non degenerated for preIfWhileAlgebra;
end;
registration
let A be Euclidean preIfWhileAlgebra;
let X be non empty countable set;
let T be Subset of Funcs(X, INT);
cluster Euclidean for ExecutionFunction of A, Funcs(X, INT), T;
end;
:: Arithmetic of Expressions
reserve A for Euclidean preIfWhileAlgebra;
reserve X for non empty countable set;
reserve T for Subset of Funcs(X, INT);
reserve f for Euclidean ExecutionFunction of A, Funcs(X, INT), T;
definition
let A,X,T,f;
let t be INT-Expression of A,f;
redefine func -t -> INT-Expression of A,f;
end;
definition
let A,X,T,f;
let t be INT-Expression of A,f;
let i be Integer;
redefine func t+i -> INT-Expression of A,f;
redefine func t-i -> INT-Expression of A,f;
redefine func t*i -> INT-Expression of A,f;
end;
definition
let A,X,T,f;
let t1,t2 be INT-Expression of A,f;
redefine func t1-t2 -> INT-Expression of A,f;
redefine func t1+t2 -> INT-Expression of A,f;
redefine func t1(#)t2 -> INT-Expression of A,f;
end;
definition
let A,X,T,f;
let t1,t2 be INT-Expression of A,f;
redefine func t1 div t2 -> INT-Expression of A,f means
:: AOFA_I00:def 29
for s being Element of Funcs(X, INT) holds it.s = t1.s div t2.s;
redefine func t1 mod t2 -> INT-Expression of A,f means
:: AOFA_I00:def 30
for s being Element of Funcs(X, INT) holds it.s = t1.s mod t2.s;
redefine func leq(t1,t2) -> INT-Expression of A,f means
:: AOFA_I00:def 31
for s being Element of Funcs(X, INT) holds it.s = IFGT(t1.s,t2.s,0,1);
redefine func gt(t1,t2) -> INT-Expression of A,f means
:: AOFA_I00:def 32
for s being Element of Funcs(X, INT) holds it.s = IFGT(t1.s,t2.s,1,0);
end;
definition
let A,X,T,f;
let t1,t2 be INT-Expression of A,f;
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);
end;
definition
let A,X,T,f;
let v be INT-Variable of A,f;
func .v -> INT-Expression of A,f equals
:: AOFA_I00:def 34
.v;
end;
definition
let A,X,T,f;
let x be Element of X;
func x^(A,f) -> INT-Variable of A,f equals
:: AOFA_I00:def 35
^x;
end;
notation
let A,X,T,f;
let x be Variable of f;
synonym ^x for x^(A,f);
end;
definition
let A,X,T,f;
let x be Variable of f;
func .x -> INT-Expression of A,f equals
:: AOFA_I00:def 36
.(^x);
end;
theorem :: AOFA_I00:22
for x being Variable of f for s being Element of Funcs(X, INT)
holds (.x).s = s.x;
definition
let A,X,T,f;
let i be Integer;
func .(i,A,f) -> INT-Expression of A,f equals
:: AOFA_I00:def 37
.(i,X);
end;
definition :: "choose" function may cause some problems in further development.
let A,X,T,f;
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)};
end;
theorem :: AOFA_I00:23
for v being INT-Variable of A,f for t being INT-Expression of A,
f holds v:=t in ElementaryInstructions A;
registration
let A,X,T,f;
let v be INT-Variable of A,f;
let t be INT-Expression of A,f;
cluster v:=t -> absolutely-terminating;
end;
definition
let A,X,T,f;
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);
func v*=t -> absolutely-terminating Element of A equals
:: AOFA_I00:def 40
v:=(.v(#)t);
end;
definition
let A,X,T,f;
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;
end;
definition
let A,X,T,f;
let x be Element of X;
let y be Variable of f;
func x:=y -> absolutely-terminating Element of A equals
:: AOFA_I00:def 42
x:=.y;
end;
definition
let A,X,T,f;
let x be Element of X;
let v be INT-Variable of A,f;
func x:=v -> absolutely-terminating Element of A equals
:: AOFA_I00:def 43
x:=.v;
end;
definition
let A,X,T,f;
let v,w be INT-Variable of A,f;
func v:=w -> absolutely-terminating Element of A equals
:: AOFA_I00:def 44
v:=.w;
end;
definition
let A,X,T,f;
let x be Variable of f;
let i be Integer;
func x:=i -> absolutely-terminating Element of A equals
:: AOFA_I00:def 45
x:=.(i,A,f);
end;
definition
let A,X,T,f;
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;
end;
definition
let A,X,T,f;
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);
func x*=t -> absolutely-terminating Element of A equals
:: AOFA_I00:def 48
x:=(.x(#)t);
func x%=t -> absolutely-terminating Element of A equals
:: AOFA_I00:def 49
x:=(.x mod t);
func x/=t -> absolutely-terminating Element of A equals
:: AOFA_I00:def 50
x:=(.x div t);
end;
definition
let A,X,T,f;
let x be Variable of f;
let i be Integer;
func x+=i -> absolutely-terminating Element of A equals
:: AOFA_I00:def 51
x:=(.x+i);
func x*=i -> absolutely-terminating Element of A equals
:: AOFA_I00:def 52
x:=(.x*i);
func x%=i -> absolutely-terminating Element of A equals
:: AOFA_I00:def 53
x:=(.x mod .(i,A,f));
func x/=i -> absolutely-terminating Element of A equals
:: AOFA_I00:def 54
x:=(.x div .(i,A,f));
func x div i -> INT-Expression of A,f equals
:: AOFA_I00:def 55
.x div .(i,A,f);
end;
definition
let A,X,T,f;
let v be INT-Variable of A,f;
let i be Integer;
func v:=i -> absolutely-terminating Element of A equals
:: AOFA_I00:def 56
v:=.(i,A,f);
end;
definition
let A,X,T,f;
let v be INT-Variable of A,f;
let i be Integer;
func v+=i -> absolutely-terminating Element of A equals
:: AOFA_I00:def 57
v:=(.v+i);
func v*=i -> absolutely-terminating Element of A equals
:: AOFA_I00:def 58
v:=(.v*i);
end;
definition
let A,X;
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));
func t1 is_even -> absolutely-terminating Element of A equals
:: AOFA_I00:def 60
b:=((t1+1) mod
.(2,A,g));
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);
func t1 gt t2 -> absolutely-terminating Element of A equals
:: AOFA_I00:def 62
b:=gt(t1,t2);
func t1 eq t2 -> absolutely-terminating Element of A equals
:: AOFA_I00:def 63
b:=eq(t1,t2);
end;
notation
let A,X;
let b be Element of X;
let g be Euclidean ExecutionFunction of A, Funcs(X,INT), Funcs(X, INT)\(b,0);
let t1,t2 be INT-Expression of A,g;
synonym t2 geq t1 for t1 leq t2;
synonym t2 lt t1 for t1 gt t2;
end;
definition
let A,X;
let b be Element of X;
let g be Euclidean ExecutionFunction of A, Funcs(X,INT), Funcs(X, INT)\(b,0);
let v1,v2 be INT-Variable of A,g;
func v1 leq v2 -> absolutely-terminating Element of A equals
:: AOFA_I00:def 64
.v1 leq .v2;
func v1 gt v2 -> absolutely-terminating Element of A equals
:: AOFA_I00:def 65
.v1 gt .v2;
end;
notation
let A,X;
let b be Element of X;
let g be Euclidean ExecutionFunction of A, Funcs(X,INT), Funcs(X, INT)\(b,0);
let v1,v2 be INT-Variable of A,g;
synonym v2 geq v1 for v1 leq v2;
synonym v2 lt v1 for v1 gt v2;
end;
definition
let A,X;
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;
func x1 is_even -> absolutely-terminating Element of A equals
:: AOFA_I00:def 67
.x1 is_even;
let x2 be Variable of g;
func x1 leq x2 -> absolutely-terminating Element of A equals
:: AOFA_I00:def 68
.x1 leq .x2;
func x1 gt x2 -> absolutely-terminating Element of A equals
:: AOFA_I00:def 69
.x1 gt .x2;
end;
notation
let A,X;
let b be Element of X;
let g be Euclidean ExecutionFunction of A, Funcs(X,INT), Funcs(X, INT)\(b,0);
let x1,x2 be Variable of g;
synonym x2 geq x1 for x1 leq x2;
synonym x2 lt x1 for x1 gt x2;
end;
definition
let A,X;
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;
func x leq i -> absolutely-terminating Element of A equals
:: AOFA_I00:def 70
.x leq .(i,A,g);
func x geq i -> absolutely-terminating Element of A equals
:: AOFA_I00:def 71
.x geq .(i,A,g);
func x gt i -> absolutely-terminating Element of A equals
:: AOFA_I00:def 72
.x gt .(i,A,g);
func x lt i -> absolutely-terminating Element of A equals
:: AOFA_I00:def 73
.x lt .(i,A,g);
func x / i -> INT-Expression of A,g equals
:: AOFA_I00:def 74
(.x) div .(i,A,g);
end;
definition
let A,X,T,f;
let x1,x2 be Variable of f;
func x1+=x2 -> absolutely-terminating Element of A equals
:: AOFA_I00:def 75
x1+=.x2;
func x1*=x2 -> absolutely-terminating Element of A equals
:: AOFA_I00:def 76
x1*=.x2;
func x1%=x2 -> absolutely-terminating Element of A equals
:: AOFA_I00:def 77
x1:=(.x1 mod .x2);
func x1/=x2 -> absolutely-terminating Element of A equals
:: AOFA_I00:def 78
x1:=(.x1 div .x2);
func x1+x2 -> INT-Expression of A,f equals
:: AOFA_I00:def 79
(.x1)+(.x2);
func x1*x2 -> INT-Expression of A,f equals
:: AOFA_I00:def 80
(.x1)(#)(.x2);
func x1 mod x2 -> INT-Expression of A,f equals
:: AOFA_I00:def 81
(.x1)mod(.x2);
func x1 div x2 -> INT-Expression of A,f equals
:: AOFA_I00:def 82
(.x1)div(.x2);
end;
reserve A for Euclidean preIfWhileAlgebra,
X for non empty countable set,
z for (Element of X),
s,s9 for (Element of Funcs(X, INT)),
T for Subset of Funcs(X, INT),
f for Euclidean ExecutionFunction of A, Funcs(X, INT), T,
v for INT-Variable of A,f,
t for INT-Expression of A,f;
reserve i for Integer;
theorem :: AOFA_I00:24
f.(s, v:=t).(v.s) = t.s & for z st z <> v.s holds f.(s, v:=t).z = s.z;
theorem :: AOFA_I00:25
for x being Variable of f for i being Integer holds f.(s,
x:=i).x = i & for z st z <> x holds f.(s, x:=i).z = s.z;
theorem :: AOFA_I00:26
for x being Variable of f for t being INT-Expression of A,f
holds f.(s, x:=t).x = t.s & for z st z <> x holds f.(s, x:=t).z = s.z;
theorem :: AOFA_I00:27
for x,y being Variable of f holds f.(s, x:=y).x = s.y & for z st
z <> x holds f.(s, x:=y).z = s.z;
theorem :: AOFA_I00:28
for x being Variable of f holds f.(s, x+=i).x = s.x+i & for z st
z <> x holds f.(s, x+=i).z = s.z;
theorem :: AOFA_I00:29
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 st z <> x holds f.(s, x+=t).z = s.z;
theorem :: AOFA_I00:30
for x,y being Variable of f holds f.(s, x+=y).x = s.x+s.y & for
z st z <> x holds f.(s, x+=y).z = s.z;
theorem :: AOFA_I00:31
for x being Variable of f holds f.(s, x*=i).x = s.x*i & for z st
z <> x holds f.(s, x*=i).z = s.z;
theorem :: AOFA_I00:32
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 st z <> x holds f.(s, x*=t).z = s.z;
theorem :: AOFA_I00:33
for x,y being Variable of f holds f.(s, x*=y).x = s.x*s.y & for
z st z <> x holds f.(s, x*=y).z = s.z;
theorem :: AOFA_I00:34
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 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 st z <> b holds g.(s, x leq i).z = s.
z & g.(s, x geq i).z = s.z;
theorem :: AOFA_I00:35
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 st z <> b holds g.(s, x leq y).z = s.z;
theorem :: AOFA_I00:36
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 iff g.(s, x leq i) in Funcs(X,INT)\(b,0)) & (s.x >= i
iff g.(s, x geq i) in Funcs(X,INT)\(b,0));
theorem :: AOFA_I00:37
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
iff g.(s, x leq y) in Funcs(X,INT)\(b,0)) & (s.x >= s.y iff g.(s, x geq y) in
Funcs(X,INT)\(b,0));
theorem :: AOFA_I00:38
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 st z <> b holds g.(s, x gt i).z = s.z & g.
(s, x lt i).z = s.z;
theorem :: AOFA_I00:39
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 st z <> b holds g.(s, x gt y).z = s.z & g.(s, x lt y).z = s.z;
theorem :: AOFA_I00:40
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 iff g.(s, x gt i) in Funcs(X,INT)\(b,0)) & (s.x <
i iff g.(s, x lt i) in Funcs(X,INT)\(b,0));
theorem :: AOFA_I00:41
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
iff g.(s, x gt y) in Funcs(X,INT)\(b,0)) & (s.x < s.y iff g.(s, x lt y) in
Funcs(X,INT)\(b,0));
theorem :: AOFA_I00:42
for x being Variable of f holds f.(s, x%=i).x = s.x mod i & for z st z
<> x holds f.(s, x%=i).z = s.z;
theorem :: AOFA_I00:43
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 st z <> x holds f.(s, x%=t).z = s.z
;
theorem :: AOFA_I00:44
for x,y being Variable of f holds f.(s, x%=y).x = s.x mod s.y &
for z st z <> x holds f.(s, x%=y).z = s.z;
theorem :: AOFA_I00:45
for x being Variable of f holds f.(s, x/=i).x = s.x div i & for
z st z <> x holds f.(s, x/=i).z = s.z;
theorem :: AOFA_I00:46
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 st z <> x holds f.(s, x/=t).z = s.z
;
theorem :: AOFA_I00:47
for x,y being Variable of f holds f.(s, x/=y).x = s.x div s.y & for z
st z <> x holds f.(s, x/=y).z = s.z;
theorem :: AOFA_I00:48
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 st
z <> b holds g.(s, t is_odd).z = s.z & g.(s, t is_even).z = s.z;
theorem :: AOFA_I00:49
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 st z <> b
holds g.(s, x is_odd).z = s.z;
theorem :: AOFA_I00:50
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 iff g.(s, t is_odd) in Funcs(X,INT)\(b,0)) & (t.s is even iff g.(s,
t is_even) in Funcs(X,INT)\(b,0));
theorem :: AOFA_I00:51
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
iff g.(s, x is_odd) in Funcs(X,INT)\(b,0)) & (s.x is even iff g.(s, x is_even)
in Funcs(X,INT)\(b,0));
scheme :: AOFA_I00:sch 1
ForToIteration {A() -> Euclidean preIfWhileAlgebra, X() -> countable non
empty set, b() -> (Element of X()), I,F() -> (Element of A()), g() -> Euclidean
ExecutionFunction of A(), Funcs(X(),INT), Funcs(X(),INT)\(b(),0), i,n() -> (
Variable of g()), s() -> (Element of Funcs(X(),INT)), a() -> INT-Expression of
A(),g(), P[set] }: P[g().(s(),F())] & (a().s() <= s().n() implies g().(s(),F())
.i() = s().n()+1) & (a().s() > s().n() implies g().(s(),F()).i() = a().s()) & g
().(s(),F()).n() = s().n()
provided
F() = for-do(i():=a(), i() leq n(), i()+=1, I()) and
P[g().(s(),i():=a())] and
for s being Element of Funcs(X(),INT) st P[s] holds P[g().(s,I()\;i(
)+=1)] & P[g().(s, i() leq n())] and
for s being Element of Funcs(X(),INT) st P[s] holds g().(s,I()).i()
= s.i() & g().(s,I()).n() = s.n() and
n() <> i() & n() <> b() & i() <> b();
scheme :: AOFA_I00:sch 2
ForDowntoIteration {A() -> Euclidean preIfWhileAlgebra, X() -> countable non
empty set, b() -> (Element of X()), I,F() -> (Element of A()), f() -> Euclidean
ExecutionFunction of A(), Funcs(X(),INT), Funcs(X(),INT)\(b(),0), i,n() -> (
Variable of f()), s() -> (Element of Funcs(X(),INT)), a() -> INT-Expression of
A(),f(), P[set] }: P[f().(s(),F())] & (a().s() >= s().n() implies f().(s(),F())
.i() = s().n()-1) & (a().s() < s().n() implies f().(s(),F()).i() = a().s()) & f
().(s(),F()).n() = s().n()
provided
F() = for-do(i():=a(),.n() leq .i(),i()+=-1,I()) and
P[f().(s(),i():=a())] and
for s being Element of Funcs(X(),INT) st P[s] holds P[f().(s,I()\;i(
)+=-1)] & P[f().(s, n() leq i())] and
for s being Element of Funcs(X(),INT) st P[s] holds f().(s,I()).i()
= s.i() & f().(s,I()).n() = s.n() and
n() <> i() & n() <> b() & i() <> b();
begin :: Termination in if-while algebras over integers
reserve b for (Element of X),
g for Euclidean ExecutionFunction of A, Funcs(X, INT), Funcs(X, INT)\(b,0);
theorem :: AOFA_I00:52
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 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);
theorem :: AOFA_I00:53
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 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 holds s in P implies g iteration_terminates_for I\; i+=1\; i
leq n, g.(s, i leq n);
theorem :: AOFA_I00:54
for I being Element of A st I is_terminating_wrt g for i,n being
Variable of g st (ex d being Function st d.b = 0 & d.n = 1 & d.i = 2) & for s
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;
theorem :: AOFA_I00:55
for P being set for I being Element of A st I is_terminating_wrt g, P
for i,n being Variable of g st (ex d being Function st d.b = 0 & d.n = 1 & d.i
= 2) & (for s 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;
begin :: Examples
definition
let X,A,T,f,s;
let I be Element of A;
redefine func f.(s,I) -> Element of Funcs(X, INT);
end;
theorem :: AOFA_I00:56
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;
theorem :: AOFA_I00:57
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 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!;
theorem :: AOFA_I00:58
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;
theorem :: AOFA_I00:59
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 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;
theorem :: AOFA_I00:60
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;
theorem :: AOFA_I00:61
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 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;
theorem :: AOFA_I00:62
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: s.x > s.y & s.y >= 0};
theorem :: AOFA_I00:63 :: Correctness of Euclid algorithm
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 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;
theorem :: AOFA_I00:64 :: Termination of Euclid algorithm 2
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: s.x >= 0 & s.y >= 0};
theorem :: AOFA_I00:65 :: Euclid algorithm 2
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 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;
theorem :: AOFA_I00:66
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: s.m >= 0};
::$N Correctness of the algorithm of exponentiation by squaring
theorem :: AOFA_I00:67
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 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;