:: Mizar Analysis of Algorithms: Algorithms over Integers :: by Grzegorz Bancerek :: :: Received March 18, 2008 :: Copyright (c) 2008-2021 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;