:: Mizar Analysis of Algorithms: Algorithms over Integers :: by Grzegorz Bancerek :: :: Received March 18, 2008 :: Copyright (c) 2008-2012 Association of Mizar Users begin theorem Th1: :: AOFA_I00:1 for x, y, z, a, b, c being set st a <> b & b <> c & c <> a holds ex f being Function st ( f . a = x & f . b = y & f . c = z ) proofend; definition let F be non empty functional set ; let x, f be set ; funcF \ (x,f) -> Subset of F equals :: AOFA_I00:def 1 { g where g is Element of F : g . x <> f } ; coherence { g where g is Element of F : g . x <> f } is Subset of F proofend; end; :: deftheorem defines \ AOFA_I00:def_1_:_ for F being non empty functional set for x, f being set holds F \ (x,f) = { g where g is Element of F : g . x <> f } ; theorem Th2: :: AOFA_I00:2 for F being non empty functional set for x, y being set for g being Element of F holds ( g in F \ (x,y) iff g . x <> y ) proofend; definition let X be set ; let Y, Z be set ; let f be Function of [:(Funcs (X,INT)),Y:],Z; mode Variable of f -> Element of X means :Def2: :: AOFA_I00:def 2 verum; existence ex b1 being Element of X st verum ; end; :: deftheorem Def2 defines Variable AOFA_I00:def_2_:_ for X, Y, Z being set for f being Function of [:(Funcs (X,INT)),Y:],Z for b5 being Element of X holds ( b5 is Variable of f iff verum ); notation let f be real-valued Function; let x be real number ; synonym f * x for x (#) f; end; definition let t1, t2 be INT -valued Function; funct1 div t2 -> INT -valued Function means :Def3: :: AOFA_I00:def 3 ( dom it = (dom t1) /\ (dom t2) & ( for s being set st s in dom it holds it . s = (t1 . s) div (t2 . s) ) ); correctness existence ex b1 being INT -valued Function st ( dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds b1 . s = (t1 . s) div (t2 . s) ) ); uniqueness for b1, b2 being INT -valued Function st dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds b1 . s = (t1 . s) div (t2 . s) ) & dom b2 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b2 holds b2 . s = (t1 . s) div (t2 . s) ) holds b1 = b2; proofend; funct1 mod t2 -> INT -valued Function means :Def4: :: AOFA_I00:def 4 ( dom it = (dom t1) /\ (dom t2) & ( for s being set st s in dom it holds it . s = (t1 . s) mod (t2 . s) ) ); correctness existence ex b1 being INT -valued Function st ( dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds b1 . s = (t1 . s) mod (t2 . s) ) ); uniqueness for b1, b2 being INT -valued Function st dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds b1 . s = (t1 . s) mod (t2 . s) ) & dom b2 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b2 holds b2 . s = (t1 . s) mod (t2 . s) ) holds b1 = b2; proofend; func leq (t1,t2) -> INT -valued Function means :Def5: :: AOFA_I00:def 5 ( dom it = (dom t1) /\ (dom t2) & ( for s being set st s in dom it holds it . s = IFGT ((t1 . s),(t2 . s),0,1) ) ); correctness existence ex b1 being INT -valued Function st ( dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds b1 . s = IFGT ((t1 . s),(t2 . s),0,1) ) ); uniqueness for b1, b2 being INT -valued Function st dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds b1 . s = IFGT ((t1 . s),(t2 . s),0,1) ) & dom b2 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b2 holds b2 . s = IFGT ((t1 . s),(t2 . s),0,1) ) holds b1 = b2; proofend; func gt (t1,t2) -> INT -valued Function means :Def6: :: AOFA_I00:def 6 ( dom it = (dom t1) /\ (dom t2) & ( for s being set st s in dom it holds it . s = IFGT ((t1 . s),(t2 . s),1,0) ) ); correctness existence ex b1 being INT -valued Function st ( dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds b1 . s = IFGT ((t1 . s),(t2 . s),1,0) ) ); uniqueness for b1, b2 being INT -valued Function st dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds b1 . s = IFGT ((t1 . s),(t2 . s),1,0) ) & dom b2 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b2 holds b2 . s = IFGT ((t1 . s),(t2 . s),1,0) ) holds b1 = b2; proofend; func eq (t1,t2) -> INT -valued Function means :Def7: :: AOFA_I00:def 7 ( dom it = (dom t1) /\ (dom t2) & ( for s being set st s in dom it holds it . s = IFEQ ((t1 . s),(t2 . s),1,0) ) ); correctness existence ex b1 being INT -valued Function st ( dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds b1 . s = IFEQ ((t1 . s),(t2 . s),1,0) ) ); uniqueness for b1, b2 being INT -valued Function st dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds b1 . s = IFEQ ((t1 . s),(t2 . s),1,0) ) & dom b2 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b2 holds b2 . s = IFEQ ((t1 . s),(t2 . s),1,0) ) holds b1 = b2; proofend; end; :: deftheorem Def3 defines div AOFA_I00:def_3_:_ for t1, t2, b3 being INT -valued Function holds ( b3 = t1 div t2 iff ( dom b3 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b3 holds b3 . s = (t1 . s) div (t2 . s) ) ) ); :: deftheorem Def4 defines mod AOFA_I00:def_4_:_ for t1, t2, b3 being INT -valued Function holds ( b3 = t1 mod t2 iff ( dom b3 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b3 holds b3 . s = (t1 . s) mod (t2 . s) ) ) ); :: deftheorem Def5 defines leq AOFA_I00:def_5_:_ for t1, t2, b3 being INT -valued Function holds ( b3 = leq (t1,t2) iff ( dom b3 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b3 holds b3 . s = IFGT ((t1 . s),(t2 . s),0,1) ) ) ); :: deftheorem Def6 defines gt AOFA_I00:def_6_:_ for t1, t2, b3 being INT -valued Function holds ( b3 = gt (t1,t2) iff ( dom b3 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b3 holds b3 . s = IFGT ((t1 . s),(t2 . s),1,0) ) ) ); :: deftheorem Def7 defines eq AOFA_I00:def_7_:_ for t1, t2, b3 being INT -valued Function holds ( b3 = eq (t1,t2) iff ( dom b3 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b3 holds b3 . s = IFEQ ((t1 . s),(t2 . s),1,0) ) ) ); definition let X be non empty set ; let f be Function of X,INT; let x be integer number ; :: original:+ redefine funcf + x -> Function of X,INT means :Def8: :: AOFA_I00:def 8 for s being Element of X holds it . s = (f . s) + x; compatibility for b1 being Function of X,INT holds ( b1 = x + f iff for s being Element of X holds b1 . s = (f . s) + x ) proofend; coherence x + f is Function of X,INT proofend; :: original:- redefine funcf - x -> Function of X,INT means :: AOFA_I00:def 9 for s being Element of X holds it . s = (f . s) - x; compatibility for b1 being Function of X,INT holds ( b1 = f - x iff for s being Element of X holds b1 . s = (f . s) - x ) proofend; coherence f - x is Function of X,INT proofend; :: original:* redefine funcf * x -> Function of X,INT means :Def10: :: AOFA_I00:def 10 for s being Element of X holds it . s = (f . s) * x; compatibility for b1 being Function of X,INT holds ( b1 = f * x iff for s being Element of X holds b1 . s = (f . s) * x ) proofend; coherence f * x is Function of X,INT proofend; end; :: deftheorem Def8 defines + AOFA_I00:def_8_:_ for X being non empty set for f being Function of X,INT for x being integer number for b4 being Function of X,INT holds ( b4 = f + x iff for s being Element of X holds b4 . s = (f . s) + x ); :: deftheorem defines - AOFA_I00:def_9_:_ for X being non empty set for f being Function of X,INT for x being integer number for b4 being Function of X,INT holds ( b4 = f - x iff for s being Element of X holds b4 . s = (f . s) - x ); :: deftheorem Def10 defines * AOFA_I00:def_10_:_ for X being non empty set for f being Function of X,INT for x being integer number for b4 being Function of X,INT holds ( b4 = f * x iff for s being Element of X holds b4 . s = (f . s) * x ); definition let X be set ; let f, g be Function of X,INT; :: original:div redefine funcf div g -> Function of X,INT; coherence f div g is Function of X,INT proofend; :: original:mod redefine funcf mod g -> Function of X,INT; coherence f mod g is Function of X,INT proofend; :: original:leq redefine func leq (f,g) -> Function of X,INT; coherence leq (f,g) is Function of X,INT proofend; :: original:gt redefine func gt (f,g) -> Function of X,INT; coherence gt (f,g) is Function of X,INT proofend; :: original:eq redefine func eq (f,g) -> Function of X,INT; coherence eq (f,g) is Function of X,INT proofend; end; definition let X be non empty set ; let t1, t2 be Function of X,INT; :: original:- redefine funct1 - t2 -> Function of X,INT means :Def11: :: AOFA_I00:def 11 for s being Element of X holds it . s = (t1 . s) - (t2 . s); compatibility for b1 being Function of X,INT holds ( b1 = t1 - t2 iff for s being Element of X holds b1 . s = (t1 . s) - (t2 . s) ) proofend; coherence t1 - t2 is Function of X,INT proofend; :: original:+ redefine funct1 + t2 -> Function of X,INT means :: AOFA_I00:def 12 for s being Element of X holds it . s = (t1 . s) + (t2 . s); compatibility for b1 being Function of X,INT holds ( b1 = t1 + t2 iff for s being Element of X holds b1 . s = (t1 . s) + (t2 . s) ) proofend; coherence t1 + t2 is Function of X,INT proofend; end; :: deftheorem Def11 defines - AOFA_I00:def_11_:_ for X being non empty set for t1, t2, b4 being Function of X,INT holds ( b4 = t1 - t2 iff for s being Element of X holds b4 . s = (t1 . s) - (t2 . s) ); :: deftheorem defines + AOFA_I00:def_12_:_ for X being non empty set for t1, t2, b4 being Function of X,INT holds ( b4 = t1 + t2 iff for s being Element of X holds b4 . s = (t1 . s) + (t2 . s) ); registration let A be non empty set ; let B be infinite set ; cluster Funcs (A,B) -> infinite ; coherence not Funcs (A,B) is finite proofend; end; definition let N be set ; let v, f be Function; funcv ** (f,N) -> Function means :Def13: :: AOFA_I00:def 13 ( ex Y being set st ( ( for y being set holds ( y in Y iff ex h being Function st ( h in dom v & y in rng h ) ) ) & ( for a being set holds ( a in dom it iff ( a in Funcs (N,Y) & ex g being Function st ( a = g & g * f in dom v ) ) ) ) ) & ( for g being Function st g in dom it holds it . g = v . (g * f) ) ); uniqueness for b1, b2 being Function st ex Y being set st ( ( for y being set holds ( y in Y iff ex h being Function st ( h in dom v & y in rng h ) ) ) & ( for a being set holds ( a in dom b1 iff ( a in Funcs (N,Y) & ex g being Function st ( a = g & g * f in dom v ) ) ) ) ) & ( for g being Function st g in dom b1 holds b1 . g = v . (g * f) ) & ex Y being set st ( ( for y being set holds ( y in Y iff ex h being Function st ( h in dom v & y in rng h ) ) ) & ( for a being set holds ( a in dom b2 iff ( a in Funcs (N,Y) & ex g being Function st ( a = g & g * f in dom v ) ) ) ) ) & ( for g being Function st g in dom b2 holds b2 . g = v . (g * f) ) holds b1 = b2 proofend; existence ex b1 being Function st ( ex Y being set st ( ( for y being set holds ( y in Y iff ex h being Function st ( h in dom v & y in rng h ) ) ) & ( for a being set holds ( a in dom b1 iff ( a in Funcs (N,Y) & ex g being Function st ( a = g & g * f in dom v ) ) ) ) ) & ( for g being Function st g in dom b1 holds b1 . g = v . (g * f) ) ) proofend; end; :: deftheorem Def13 defines ** AOFA_I00:def_13_:_ for N being set for v, f, b4 being Function holds ( b4 = v ** (f,N) iff ( ex Y being set st ( ( for y being set holds ( y in Y iff ex h being Function st ( h in dom v & y in rng h ) ) ) & ( for a being set holds ( a in dom b4 iff ( a in Funcs (N,Y) & ex g being Function st ( a = g & g * f in dom v ) ) ) ) ) & ( for g being Function st g in dom b4 holds b4 . g = v . (g * f) ) ) ); definition let X, Y, Z, N be non empty set ; let v be Element of Funcs ((Funcs (X,Y)),Z); let f be Function of X,N; :: original:** redefine funcv ** (f,N) -> Element of Funcs ((Funcs (N,Y)),Z); coherence v ** (f,N) is Element of Funcs ((Funcs (N,Y)),Z) proofend; end; theorem Th3: :: AOFA_I00:3 for f1, f2, g being Function st rng g c= dom f2 holds (f1 +* f2) * g = f2 * g proofend; 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 proofend; 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 proofend; registration let X be set ; cluster Relation-like X -defined card X -valued Function-like one-to-one quasi_total onto for Element of bool [:X,(card X):]; existence ex b1 being Function of X,(card X) st ( b1 is one-to-one & b1 is onto ) proofend; cluster Relation-like card X -defined X -valued Function-like one-to-one quasi_total onto for Element of bool [:(card X),X:]; existence ex b1 being Function of (card X),X st ( b1 is one-to-one & b1 is onto ) proofend; 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 ) ) proofend; 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 ) ) proofend; 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 proofend; 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 proofend; 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 proofend; definition let X be set ; let f be Enumeration of X; :: original:" redefine funcf " -> Denumeration of X; coherence f " is Denumeration of X proofend; end; definition let X be set ; let f be Denumeration of X; :: original:" redefine funcf " -> Enumeration of X; coherence f " is Enumeration of X proofend; end; theorem :: AOFA_I00:12 for n, m being Nat holds 0 to_power (n + m) = (0 to_power n) * (0 to_power m) proofend; theorem :: AOFA_I00:13 for x being real number for n, m being Nat holds (x to_power n) to_power m = x to_power (n * m) by NEWTON:9; begin definition let X be non empty set ; mode INT-Variable of X is Function of (Funcs (X,INT)),X; mode INT-Expression of X is Function of (Funcs (X,INT)),INT; mode INT-Array of X is Function of INT,X; end; definition let A be preIfWhileAlgebra; let I be Element of A; let X be non empty set ; let T be Subset of (Funcs (X,INT)); let f be ExecutionFunction of A, Funcs (X,INT),T; predI is_assignment_wrt A,X,f means :Def14: :: AOFA_I00:def 14 ( I in ElementaryInstructions A & ex v being INT-Variable of X ex t being INT-Expression of X st for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) ); end; :: deftheorem Def14 defines is_assignment_wrt AOFA_I00:def_14_:_ for A being preIfWhileAlgebra for I being Element of A for X being non empty set for T being Subset of (Funcs (X,INT)) for f being ExecutionFunction of A, Funcs (X,INT),T holds ( I is_assignment_wrt A,X,f iff ( I in ElementaryInstructions A & ex v being INT-Variable of X ex t being INT-Expression of X st for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) ) ); definition let A be preIfWhileAlgebra; let X be non empty set ; let T be Subset of (Funcs (X,INT)); let f be ExecutionFunction of A, Funcs (X,INT),T; let v be INT-Variable of X; let t be INT-Expression of X; predv,t form_assignment_wrt f means :Def15: :: AOFA_I00:def 15 ex I being Element of A st ( I in ElementaryInstructions A & ( for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) ) ); end; :: deftheorem Def15 defines form_assignment_wrt AOFA_I00:def_15_:_ for A being preIfWhileAlgebra for X being non empty set for T being Subset of (Funcs (X,INT)) for f being ExecutionFunction of A, Funcs (X,INT),T for v being INT-Variable of X for t being INT-Expression of X holds ( v,t form_assignment_wrt f iff ex I being Element of A st ( I in ElementaryInstructions A & ( for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) ) ) ); definition let A be preIfWhileAlgebra; let X be non empty set ; let T be Subset of (Funcs (X,INT)); let f be ExecutionFunction of A, Funcs (X,INT),T; assume B1: ex I being Element of A st I is_assignment_wrt A,X,f ; mode INT-Variable of A,f -> INT-Variable of X means :: AOFA_I00:def 16 ex t being INT-Expression of X st it,t form_assignment_wrt f; existence ex b1 being INT-Variable of X ex t being INT-Expression of X st b1,t form_assignment_wrt f proofend; end; :: deftheorem defines INT-Variable AOFA_I00:def_16_:_ for A being preIfWhileAlgebra for X being non empty set for T being Subset of (Funcs (X,INT)) for f being ExecutionFunction of A, Funcs (X,INT),T st ex I being Element of A st I is_assignment_wrt A,X,f holds for b5 being INT-Variable of X holds ( b5 is INT-Variable of A,f iff ex t being INT-Expression of X st b5,t form_assignment_wrt f ); definition let A be preIfWhileAlgebra; let X be non empty set ; let T be Subset of (Funcs (X,INT)); let f be ExecutionFunction of A, Funcs (X,INT),T; assume B1: ex I being Element of A st I is_assignment_wrt A,X,f ; mode INT-Expression of A,f -> INT-Expression of X means :: AOFA_I00:def 17 ex v being INT-Variable of X st v,it form_assignment_wrt f; existence ex b1 being INT-Expression of X ex v being INT-Variable of X st v,b1 form_assignment_wrt f proofend; end; :: deftheorem defines INT-Expression AOFA_I00:def_17_:_ for A being preIfWhileAlgebra for X being non empty set for T being Subset of (Funcs (X,INT)) for f being ExecutionFunction of A, Funcs (X,INT),T st ex I being Element of A st I is_assignment_wrt A,X,f holds for b5 being INT-Expression of X holds ( b5 is INT-Expression of A,f iff ex v being INT-Variable of X st v,b5 form_assignment_wrt f ); definition let X, Y be non empty set ; let f be Element of Funcs (X,Y); let x be Element of X; :: original:. redefine funcf . x -> Element of Y; coherence f . x is Element of Y proofend; end; definition let X be non empty set ; let x be Element of X; func . x -> INT-Expression of X means :Def18: :: AOFA_I00:def 18 for s being Element of Funcs (X,INT) holds it . s = s . x; correctness existence ex b1 being INT-Expression of X st for s being Element of Funcs (X,INT) holds b1 . s = s . x; uniqueness for b1, b2 being INT-Expression of X st ( for s being Element of Funcs (X,INT) holds b1 . s = s . x ) & ( for s being Element of Funcs (X,INT) holds b2 . s = s . x ) holds b1 = b2; proofend; end; :: deftheorem Def18 defines . AOFA_I00:def_18_:_ for X being non empty set for x being Element of X for b3 being INT-Expression of X holds ( b3 = . x iff for s being Element of Funcs (X,INT) holds b3 . s = s . x ); definition let X be non empty set ; let v be INT-Variable of X; func . v -> INT-Expression of X means :Def19: :: AOFA_I00:def 19 for s being Element of Funcs (X,INT) holds it . s = s . (v . s); correctness existence ex b1 being INT-Expression of X st for s being Element of Funcs (X,INT) holds b1 . s = s . (v . s); uniqueness for b1, b2 being INT-Expression of X st ( for s being Element of Funcs (X,INT) holds b1 . s = s . (v . s) ) & ( for s being Element of Funcs (X,INT) holds b2 . s = s . (v . s) ) holds b1 = b2; proofend; end; :: deftheorem Def19 defines . AOFA_I00:def_19_:_ for X being non empty set for v being INT-Variable of X for b3 being INT-Expression of X holds ( b3 = . v iff for s being Element of Funcs (X,INT) holds b3 . s = s . (v . s) ); definition let X be non empty set ; let x be Element of X; func ^ x -> INT-Variable of X equals :: AOFA_I00:def 20 (Funcs (X,INT)) --> x; correctness coherence (Funcs (X,INT)) --> x is INT-Variable of X; ; end; :: deftheorem defines ^ AOFA_I00:def_20_:_ for X being non empty set for x being Element of X holds ^ x = (Funcs (X,INT)) --> x; theorem :: AOFA_I00:14 for X being non empty set for x being Element of X holds . x = . (^ x) proofend; definition let X be non empty set ; let i be integer number ; func . (i,X) -> INT-Expression of X equals :: AOFA_I00:def 21 (Funcs (X,INT)) --> i; correctness coherence (Funcs (X,INT)) --> i is INT-Expression of X; proofend; end; :: deftheorem defines . AOFA_I00:def_21_:_ for X being non empty set for i being integer number holds . (i,X) = (Funcs (X,INT)) --> i; theorem :: AOFA_I00:15 for X being non empty set for t being INT-Expression of X holds ( t + (. (0,X)) = t & t (#) (. (1,X)) = t ) proofend; :: 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; attrf is Euclidean means :Def22: :: AOFA_I00:def 22 ( ( for v being INT-Variable of A,f for t being INT-Expression of A,f holds v,t form_assignment_wrt f ) & ( for i being integer number holds . (i,X) is INT-Expression of A,f ) & ( for v being INT-Variable of A,f holds . v is INT-Expression of A,f ) & ( for x being Element of X holds ^ x is INT-Variable of A,f ) & ex a being INT-Array of X st ( a | (card X) is one-to-one & ( for t being INT-Expression of A,f holds a * t is INT-Variable of A,f ) ) & ( for t being INT-Expression of A,f holds - t is INT-Expression of A,f ) & ( for t1, t2 being INT-Expression of A,f holds ( t1 (#) t2 is INT-Expression of A,f & t1 + t2 is INT-Expression of A,f & t1 div t2 is INT-Expression of A,f & t1 mod t2 is INT-Expression of A,f & leq (t1,t2) is INT-Expression of A,f & gt (t1,t2) is INT-Expression of A,f ) ) ); end; :: deftheorem Def22 defines Euclidean AOFA_I00:def_22_:_ for A being preIfWhileAlgebra for X being non empty set for T being Subset of (Funcs (X,INT)) for f being ExecutionFunction of A, Funcs (X,INT),T holds ( f is Euclidean iff ( ( for v being INT-Variable of A,f for t being INT-Expression of A,f holds v,t form_assignment_wrt f ) & ( for i being integer number holds . (i,X) is INT-Expression of A,f ) & ( for v being INT-Variable of A,f holds . v is INT-Expression of A,f ) & ( for x being Element of X holds ^ x is INT-Variable of A,f ) & ex a being INT-Array of X st ( a | (card X) is one-to-one & ( for t being INT-Expression of A,f holds a * t is INT-Variable of A,f ) ) & ( for t being INT-Expression of A,f holds - t is INT-Expression of A,f ) & ( for t1, t2 being INT-Expression of A,f holds ( t1 (#) t2 is INT-Expression of A,f & t1 + t2 is INT-Expression of A,f & t1 div t2 is INT-Expression of A,f & t1 mod t2 is INT-Expression of A,f & leq (t1,t2) is INT-Expression of A,f & gt (t1,t2) is INT-Expression of A,f ) ) ) ); :: Remark: :: Incorrect definition of "mod" in INT_1: 5 mod 0 = 0 i 5 div 0 = 0 :: and 5 <> 0*(5 div 0)+(5 mod 0) :: In our case "mod" is still expressible with "basic" operations :: but in complicated way: :: f1 mod f2 :: = (gt(f2,(dom f2)-->0)+gt((dom f2)-->0,f2))(#)(f1-f2(#)(f1 div f2)) :: To avoid complications "mod" is mentioned in the definition above. definition let A be preIfWhileAlgebra; attrA is Euclidean means :Def23: :: AOFA_I00:def 23 for X being non empty countable set for T being Subset of (Funcs (X,INT)) ex f being ExecutionFunction of A, Funcs (X,INT),T st f is Euclidean ; end; :: deftheorem Def23 defines Euclidean AOFA_I00:def_23_:_ for A being preIfWhileAlgebra holds ( A is Euclidean iff for X being non empty countable set for T being Subset of (Funcs (X,INT)) ex f being ExecutionFunction of A, Funcs (X,INT),T st f is Euclidean ); definition func INT-ElemIns -> infinite disjoint_with_NAT set equals :: AOFA_I00:def 24 [:(Funcs ((Funcs (NAT,INT)),NAT)),(Funcs ((Funcs (NAT,INT)),INT)):]; coherence [:(Funcs ((Funcs (NAT,INT)),NAT)),(Funcs ((Funcs (NAT,INT)),INT)):] is infinite disjoint_with_NAT set ; end; :: deftheorem defines INT-ElemIns AOFA_I00:def_24_:_ INT-ElemIns = [:(Funcs ((Funcs (NAT,INT)),NAT)),(Funcs ((Funcs (NAT,INT)),INT)):]; definition mode INT-Exec -> ExecutionFunction of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns), Funcs (NAT,INT),(Funcs (NAT,INT)) \ (0,0) means :Def25: :: AOFA_I00:def 25 for s being Element of Funcs (NAT,INT) for v being Element of Funcs ((Funcs (NAT,INT)),NAT) for e being Element of Funcs ((Funcs (NAT,INT)),INT) holds it . (s,(root-tree [v,e])) = s +* ((v . s),(e . s)); existence ex b1 being ExecutionFunction of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns), Funcs (NAT,INT),(Funcs (NAT,INT)) \ (0,0) st for s being Element of Funcs (NAT,INT) for v being Element of Funcs ((Funcs (NAT,INT)),NAT) for e being Element of Funcs ((Funcs (NAT,INT)),INT) holds b1 . (s,(root-tree [v,e])) = s +* ((v . s),(e . s)) proofend; end; :: deftheorem Def25 defines INT-Exec AOFA_I00:def_25_:_ for b1 being ExecutionFunction of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns), Funcs (NAT,INT),(Funcs (NAT,INT)) \ (0,0) holds ( b1 is INT-Exec iff for s being Element of Funcs (NAT,INT) for v being Element of Funcs ((Funcs (NAT,INT)),NAT) for e being Element of Funcs ((Funcs (NAT,INT)),INT) holds b1 . (s,(root-tree [v,e])) = s +* ((v . s),(e . s)) ); definition let X be non empty set ; func INT-ElemIns X -> infinite disjoint_with_NAT set equals :: AOFA_I00:def 26 [:(Funcs ((Funcs (X,INT)),X)),(Funcs ((Funcs (X,INT)),INT)):]; coherence [:(Funcs ((Funcs (X,INT)),X)),(Funcs ((Funcs (X,INT)),INT)):] is infinite disjoint_with_NAT set ; end; :: deftheorem defines INT-ElemIns AOFA_I00:def_26_:_ for X being non empty set holds INT-ElemIns X = [:(Funcs ((Funcs (X,INT)),X)),(Funcs ((Funcs (X,INT)),INT)):]; definition let X be non empty set ; let x be Element of X; mode INT-Exec of x -> ExecutionFunction of FreeUnivAlgNSG (ECIW-signature,(INT-ElemIns X)), Funcs (X,INT),(Funcs (X,INT)) \ (x,0) means :: AOFA_I00:def 27 for s being Element of Funcs (X,INT) for v being Element of Funcs ((Funcs (X,INT)),X) for e being Element of Funcs ((Funcs (X,INT)),INT) holds it . (s,(root-tree [v,e])) = s +* ((v . s),(e . s)); existence ex b1 being ExecutionFunction of FreeUnivAlgNSG (ECIW-signature,(INT-ElemIns X)), Funcs (X,INT),(Funcs (X,INT)) \ (x,0) st for s being Element of Funcs (X,INT) for v being Element of Funcs ((Funcs (X,INT)),X) for e being Element of Funcs ((Funcs (X,INT)),INT) holds b1 . (s,(root-tree [v,e])) = s +* ((v . s),(e . s)) proofend; end; :: deftheorem defines INT-Exec AOFA_I00:def_27_:_ for X being non empty set for x being Element of X for b3 being ExecutionFunction of FreeUnivAlgNSG (ECIW-signature,(INT-ElemIns X)), Funcs (X,INT),(Funcs (X,INT)) \ (x,0) holds ( b3 is INT-Exec of x iff for s being Element of Funcs (X,INT) for v being Element of Funcs ((Funcs (X,INT)),X) for e being Element of Funcs ((Funcs (X,INT)),INT) holds b3 . (s,(root-tree [v,e])) = s +* ((v . s),(e . s)) ); definition let X be non empty set ; let T be Subset of (Funcs (X,INT)); let c be Enumeration of X; assume A1: rng c c= NAT ; mode INT-Exec of c,T -> ExecutionFunction of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns), Funcs (X,INT),T means :Def28: :: AOFA_I00:def 28 for s being Element of Funcs (X,INT) for v being Element of Funcs ((Funcs (X,INT)),X) for e being Element of Funcs ((Funcs (X,INT)),INT) holds it . (s,(root-tree [((c * v) ** (c,NAT)),(e ** (c,NAT))])) = s +* ((v . s),(e . s)); existence ex b1 being ExecutionFunction of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns), Funcs (X,INT),T st for s being Element of Funcs (X,INT) for v being Element of Funcs ((Funcs (X,INT)),X) for e being Element of Funcs ((Funcs (X,INT)),INT) holds b1 . (s,(root-tree [((c * v) ** (c,NAT)),(e ** (c,NAT))])) = s +* ((v . s),(e . s)) proofend; end; :: deftheorem Def28 defines INT-Exec AOFA_I00:def_28_:_ for X being non empty set for T being Subset of (Funcs (X,INT)) for c being Enumeration of X st rng c c= NAT holds for b4 being ExecutionFunction of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns), Funcs (X,INT),T holds ( b4 is INT-Exec of c,T iff for s being Element of Funcs (X,INT) for v being Element of Funcs ((Funcs (X,INT)),X) for e being Element of Funcs ((Funcs (X,INT)),INT) holds b4 . (s,(root-tree [((c * v) ** (c,NAT)),(e ** (c,NAT))])) = s +* ((v . s),(e . s)) ); theorem Th16: :: AOFA_I00:16 for f being INT-Exec for v being INT-Variable of NAT for t being INT-Expression of NAT holds v,t form_assignment_wrt f proofend; 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 proofend; 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 proofend; registration cluster -> Euclidean for INT-Exec ; coherence for b1 being INT-Exec holds b1 is Euclidean proofend; 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 proofend; 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 proofend; 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 proofend; registration let X be non empty countable set ; let T be Subset of (Funcs (X,INT)); let c be Enumeration of X; cluster -> Euclidean for INT-Exec of c,T; coherence for b1 being INT-Exec of c,T holds b1 is Euclidean proofend; end; registration cluster FreeUnivAlgNSG (ECIW-signature,INT-ElemIns) -> Euclidean ; coherence FreeUnivAlgNSG (ECIW-signature,INT-ElemIns) is Euclidean proofend; end; registration cluster non empty V157() V158() V159() with_empty-instruction with_catenation with_if-instruction with_while-instruction non degenerated Euclidean for L9(); existence ex b1 being preIfWhileAlgebra st ( b1 is Euclidean & not b1 is degenerated ) proofend; end; registration let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let T be Subset of (Funcs (X,INT)); cluster non empty Relation-like [:(Funcs (X,INT)), the carrier of A:] -defined Funcs (X,INT) -valued Function-like V29([:(Funcs (X,INT)), the carrier of A:]) quasi_total Function-yielding V89() complying_with_empty-instruction complying_with_catenation Euclidean for ExecutionFunction of A, Funcs (X,INT),T; existence ex b1 being ExecutionFunction of A, Funcs (X,INT),T st b1 is Euclidean by Def23; end; definition let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let T be Subset of (Funcs (X,INT)); let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; let t be INT-Expression of A,f; :: original:- redefine func - t -> INT-Expression of A,f; coherence - t is INT-Expression of A,f by Def22; end; definition let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let T be Subset of (Funcs (X,INT)); let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; let t be INT-Expression of A,f; let i be integer number ; :: original:+ redefine funct + i -> INT-Expression of A,f; coherence i + t is INT-Expression of A,f proofend; :: original:- redefine funct - i -> INT-Expression of A,f; coherence t - i is INT-Expression of A,f proofend; :: original:* redefine funct * i -> INT-Expression of A,f; coherence t * i is INT-Expression of A,f proofend; 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 funct1 - t2 -> INT-Expression of A,f; coherence t1 - t2 is INT-Expression of A,f proofend; :: original:+ redefine funct1 + t2 -> INT-Expression of A,f; coherence t1 + t2 is INT-Expression of A,f by Def22; :: original:(#) redefine funct1 (#) t2 -> INT-Expression of A,f; coherence t1 (#) t2 is INT-Expression of A,f by Def22; end; definition let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let T be Subset of (Funcs (X,INT)); let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; let t1, t2 be INT-Expression of A,f; :: original:div redefine funct1 div t2 -> INT-Expression of A,f means :Def29: :: AOFA_I00:def 29 for s being Element of Funcs (X,INT) holds it . s = (t1 . s) div (t2 . s); coherence t1 div t2 is INT-Expression of A,f by Def22; compatibility for b1 being INT-Expression of A,f holds ( b1 = t1 div t2 iff for s being Element of Funcs (X,INT) holds b1 . s = (t1 . s) div (t2 . s) ) proofend; :: original:mod redefine funct1 mod t2 -> INT-Expression of A,f means :Def30: :: AOFA_I00:def 30 for s being Element of Funcs (X,INT) holds it . s = (t1 . s) mod (t2 . s); coherence t1 mod t2 is INT-Expression of A,f by Def22; compatibility for b1 being INT-Expression of A,f holds ( b1 = t1 mod t2 iff for s being Element of Funcs (X,INT) holds b1 . s = (t1 . s) mod (t2 . s) ) proofend; :: original:leq redefine func leq (t1,t2) -> INT-Expression of A,f means :Def31: :: AOFA_I00:def 31 for s being Element of Funcs (X,INT) holds it . s = IFGT ((t1 . s),(t2 . s),0,1); compatibility for b1 being INT-Expression of A,f holds ( b1 = leq (t1,t2) iff for s being Element of Funcs (X,INT) holds b1 . s = IFGT ((t1 . s),(t2 . s),0,1) ) proofend; coherence leq (t1,t2) is INT-Expression of A,f by Def22; :: original:gt redefine func gt (t1,t2) -> INT-Expression of A,f means :Def32: :: AOFA_I00:def 32 for s being Element of Funcs (X,INT) holds it . s = IFGT ((t1 . s),(t2 . s),1,0); coherence gt (t1,t2) is INT-Expression of A,f by Def22; compatibility for b1 being INT-Expression of A,f holds ( b1 = gt (t1,t2) iff for s being Element of Funcs (X,INT) holds b1 . s = IFGT ((t1 . s),(t2 . s),1,0) ) proofend; end; :: deftheorem Def29 defines div AOFA_I00:def_29_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for t1, t2, b7 being INT-Expression of A,f holds ( b7 = t1 div t2 iff for s being Element of Funcs (X,INT) holds b7 . s = (t1 . s) div (t2 . s) ); :: deftheorem Def30 defines mod AOFA_I00:def_30_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for t1, t2, b7 being INT-Expression of A,f holds ( b7 = t1 mod t2 iff for s being Element of Funcs (X,INT) holds b7 . s = (t1 . s) mod (t2 . s) ); :: deftheorem Def31 defines leq AOFA_I00:def_31_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for t1, t2, b7 being INT-Expression of A,f holds ( b7 = leq (t1,t2) iff for s being Element of Funcs (X,INT) holds b7 . s = IFGT ((t1 . s),(t2 . s),0,1) ); :: deftheorem Def32 defines gt AOFA_I00:def_32_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for t1, t2, b7 being INT-Expression of A,f holds ( b7 = gt (t1,t2) iff for s being Element of Funcs (X,INT) holds b7 . s = IFGT ((t1 . s),(t2 . s),1,0) ); definition let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let T be Subset of (Funcs (X,INT)); let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; let t1, t2 be INT-Expression of A,f; :: original:eq redefine func eq (t1,t2) -> INT-Expression of A,f means :: AOFA_I00:def 33 for s being Element of Funcs (X,INT) holds it . s = IFEQ ((t1 . s),(t2 . s),1,0); compatibility for b1 being INT-Expression of A,f holds ( b1 = eq (t1,t2) iff for s being Element of Funcs (X,INT) holds b1 . s = IFEQ ((t1 . s),(t2 . s),1,0) ) proofend; coherence eq (t1,t2) is INT-Expression of A,f proofend; end; :: deftheorem defines eq AOFA_I00:def_33_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for t1, t2, b7 being INT-Expression of A,f holds ( b7 = eq (t1,t2) iff for s being Element of Funcs (X,INT) holds b7 . s = IFEQ ((t1 . s),(t2 . s),1,0) ); definition let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let T be Subset of (Funcs (X,INT)); let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; let v be INT-Variable of A,f; func . v -> INT-Expression of A,f equals :: AOFA_I00:def 34 . v; coherence . v is INT-Expression of A,f by Def22; end; :: deftheorem defines . AOFA_I00:def_34_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for v being INT-Variable of A,f holds . v = . v; definition let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let T be Subset of (Funcs (X,INT)); let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; let x be Element of X; funcx ^ (A,f) -> INT-Variable of A,f equals :: AOFA_I00:def 35 ^ x; coherence ^ x is INT-Variable of A,f by Def22; end; :: deftheorem defines ^ AOFA_I00:def_35_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for x being Element of X holds x ^ (A,f) = ^ x; notation let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let T be Subset of (Funcs (X,INT)); let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; let x be Variable of f; synonym ^ x for x ^ (A,f); end; definition let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let T be Subset of (Funcs (X,INT)); let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; let x be Variable of f; func . x -> INT-Expression of A,f equals :: AOFA_I00:def 36 . (^ x); coherence . (^ x) is INT-Expression of A,f ; end; :: deftheorem defines . AOFA_I00:def_36_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for x being Variable of f holds . x = . (^ x); theorem Th22: :: AOFA_I00:22 for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for x being Variable of f for s being Element of Funcs (X,INT) holds (. x) . s = s . x proofend; definition let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let T be Subset of (Funcs (X,INT)); let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; let i be integer number ; func . (i,A,f) -> INT-Expression of A,f equals :: AOFA_I00:def 37 . (i,X); coherence . (i,X) is INT-Expression of A,f by Def22; end; :: deftheorem defines . AOFA_I00:def_37_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for i being integer number holds . (i,A,f) = . (i,X); definition let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let T be Subset of (Funcs (X,INT)); let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; let v be INT-Variable of A,f; let t be INT-Expression of A,f; funcv := t -> Element of A equals :: AOFA_I00:def 38 choose { I where I is Element of A : ( I in ElementaryInstructions A & ( for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) ) ) } ; coherence choose { I where I is Element of A : ( I in ElementaryInstructions A & ( for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) ) ) } is Element of A proofend; end; :: deftheorem defines := AOFA_I00:def_38_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for v being INT-Variable of A,f for t being INT-Expression of A,f holds v := t = choose { I where I is Element of A : ( I in ElementaryInstructions A & ( for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) ) ) } ; theorem Th23: :: AOFA_I00:23 for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for v being INT-Variable of A,f for t being INT-Expression of A,f holds v := t in ElementaryInstructions A proofend; registration let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let T be Subset of (Funcs (X,INT)); let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; let v be INT-Variable of A,f; let t be INT-Expression of A,f; clusterv := t -> absolutely-terminating ; coherence v := t is absolutely-terminating by Th23, AOFA_000:95; end; definition let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let T be Subset of (Funcs (X,INT)); let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; let v be INT-Variable of A,f; let t be INT-Expression of A,f; funcv += t -> absolutely-terminating Element of A equals :: AOFA_I00:def 39 v := ((. v) + t); coherence v := ((. v) + t) is absolutely-terminating Element of A ; funcv *= t -> absolutely-terminating Element of A equals :: AOFA_I00:def 40 v := ((. v) (#) t); coherence v := ((. v) (#) t) is absolutely-terminating Element of A ; end; :: deftheorem defines += AOFA_I00:def_39_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for v being INT-Variable of A,f for t being INT-Expression of A,f holds v += t = v := ((. v) + t); :: deftheorem defines *= AOFA_I00:def_40_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for v being INT-Variable of A,f for t being INT-Expression of A,f holds v *= t = v := ((. v) (#) t); definition let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let T be Subset of (Funcs (X,INT)); let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; let x be Element of X; let t be INT-Expression of A,f; funcx := t -> absolutely-terminating Element of A equals :: AOFA_I00:def 41 (x ^ (A,f)) := t; correctness coherence (x ^ (A,f)) := t is absolutely-terminating Element of A; ; end; :: deftheorem defines := AOFA_I00:def_41_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for x being Element of X for t being INT-Expression of A,f holds x := t = (x ^ (A,f)) := t; definition let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let T be Subset of (Funcs (X,INT)); let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; let x be Element of X; let y be Variable of f; funcx := y -> absolutely-terminating Element of A equals :: AOFA_I00:def 42 x := (. y); correctness coherence x := (. y) is absolutely-terminating Element of A; ; end; :: deftheorem defines := AOFA_I00:def_42_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for x being Element of X for y being Variable of f holds x := y = x := (. y); definition let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let T be Subset of (Funcs (X,INT)); let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; let x be Element of X; let v be INT-Variable of A,f; funcx := v -> absolutely-terminating Element of A equals :: AOFA_I00:def 43 x := (. v); correctness coherence x := (. v) is absolutely-terminating Element of A; ; end; :: deftheorem defines := AOFA_I00:def_43_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for x being Element of X for v being INT-Variable of A,f holds x := v = x := (. v); definition let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let T be Subset of (Funcs (X,INT)); let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; let v, w be INT-Variable of A,f; funcv := w -> absolutely-terminating Element of A equals :: AOFA_I00:def 44 v := (. w); correctness coherence v := (. w) is absolutely-terminating Element of A; ; end; :: deftheorem defines := AOFA_I00:def_44_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for v, w being INT-Variable of A,f holds v := w = v := (. w); definition let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let T be Subset of (Funcs (X,INT)); let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; let x be Variable of f; let i be integer number ; funcx := i -> absolutely-terminating Element of A equals :: AOFA_I00:def 45 x := (. (i,A,f)); correctness coherence x := (. (i,A,f)) is absolutely-terminating Element of A; ; end; :: deftheorem defines := AOFA_I00:def_45_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for x being Variable of f for i being integer number holds x := i = x := (. (i,A,f)); definition let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let T be Subset of (Funcs (X,INT)); let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; let v1, v2 be INT-Variable of A,f; let x be Variable of f; func swap (v1,x,v2) -> absolutely-terminating Element of A equals :: AOFA_I00:def 46 ((x := v1) \; (v1 := v2)) \; (v2 := (. x)); coherence ((x := v1) \; (v1 := v2)) \; (v2 := (. x)) is absolutely-terminating Element of A ; end; :: deftheorem defines swap AOFA_I00:def_46_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for v1, v2 being INT-Variable of A,f for x being Variable of f holds swap (v1,x,v2) = ((x := v1) \; (v1 := v2)) \; (v2 := (. x)); definition let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let T be Subset of (Funcs (X,INT)); let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; let x be Variable of f; let t be INT-Expression of A,f; funcx += t -> absolutely-terminating Element of A equals :: AOFA_I00:def 47 x := ((. x) + t); correctness coherence x := ((. x) + t) is absolutely-terminating Element of A; ; funcx *= t -> absolutely-terminating Element of A equals :: AOFA_I00:def 48 x := ((. x) (#) t); correctness coherence x := ((. x) (#) t) is absolutely-terminating Element of A; ; funcx %= t -> absolutely-terminating Element of A equals :: AOFA_I00:def 49 x := ((. x) mod t); correctness coherence x := ((. x) mod t) is absolutely-terminating Element of A; ; funcx /= t -> absolutely-terminating Element of A equals :: AOFA_I00:def 50 x := ((. x) div t); correctness coherence x := ((. x) div t) is absolutely-terminating Element of A; ; end; :: deftheorem defines += AOFA_I00:def_47_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for x being Variable of f for t being INT-Expression of A,f holds x += t = x := ((. x) + t); :: deftheorem defines *= AOFA_I00:def_48_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for x being Variable of f for t being INT-Expression of A,f holds x *= t = x := ((. x) (#) t); :: deftheorem defines %= AOFA_I00:def_49_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for x being Variable of f for t being INT-Expression of A,f holds x %= t = x := ((. x) mod t); :: deftheorem defines /= AOFA_I00:def_50_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for x being Variable of f for t being INT-Expression of A,f holds x /= t = x := ((. x) div t); definition let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let T be Subset of (Funcs (X,INT)); let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; let x be Variable of f; let i be integer number ; funcx += i -> absolutely-terminating Element of A equals :: AOFA_I00:def 51 x := ((. x) + i); correctness coherence x := ((. x) + i) is absolutely-terminating Element of A; ; funcx *= i -> absolutely-terminating Element of A equals :: AOFA_I00:def 52 x := ((. x) * i); correctness coherence x := ((. x) * i) is absolutely-terminating Element of A; ; funcx %= i -> absolutely-terminating Element of A equals :: AOFA_I00:def 53 x := ((. x) mod (. (i,A,f))); correctness coherence x := ((. x) mod (. (i,A,f))) is absolutely-terminating Element of A; ; funcx /= i -> absolutely-terminating Element of A equals :: AOFA_I00:def 54 x := ((. x) div (. (i,A,f))); correctness coherence x := ((. x) div (. (i,A,f))) is absolutely-terminating Element of A; ; funcx div i -> INT-Expression of A,f equals :: AOFA_I00:def 55 (. x) div (. (i,A,f)); correctness coherence (. x) div (. (i,A,f)) is INT-Expression of A,f; ; end; :: deftheorem defines += AOFA_I00:def_51_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for x being Variable of f for i being integer number holds x += i = x := ((. x) + i); :: deftheorem defines *= AOFA_I00:def_52_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for x being Variable of f for i being integer number holds x *= i = x := ((. x) * i); :: deftheorem defines %= AOFA_I00:def_53_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for x being Variable of f for i being integer number holds x %= i = x := ((. x) mod (. (i,A,f))); :: deftheorem defines /= AOFA_I00:def_54_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for x being Variable of f for i being integer number holds x /= i = x := ((. x) div (. (i,A,f))); :: deftheorem defines div AOFA_I00:def_55_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for x being Variable of f for i being integer number holds x div i = (. x) div (. (i,A,f)); definition let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let T be Subset of (Funcs (X,INT)); let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; let v be INT-Variable of A,f; let i be integer number ; funcv := i -> absolutely-terminating Element of A equals :: AOFA_I00:def 56 v := (. (i,A,f)); correctness coherence v := (. (i,A,f)) is absolutely-terminating Element of A; ; end; :: deftheorem defines := AOFA_I00:def_56_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for v being INT-Variable of A,f for i being integer number holds v := i = v := (. (i,A,f)); definition let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let T be Subset of (Funcs (X,INT)); let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; let v be INT-Variable of A,f; let i be integer number ; funcv += i -> absolutely-terminating Element of A equals :: AOFA_I00:def 57 v := ((. v) + i); correctness coherence v := ((. v) + i) is absolutely-terminating Element of A; ; funcv *= i -> absolutely-terminating Element of A equals :: AOFA_I00:def 58 v := ((. v) * i); correctness coherence v := ((. v) * i) is absolutely-terminating Element of A; ; end; :: deftheorem defines += AOFA_I00:def_57_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for v being INT-Variable of A,f for i being integer number holds v += i = v := ((. v) + i); :: deftheorem defines *= AOFA_I00:def_58_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for v being INT-Variable of A,f for i being integer number holds v *= i = v := ((. v) * i); definition let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let b be Element of X; let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0); let t1 be INT-Expression of A,g; funct1 is_odd -> absolutely-terminating Element of A equals :: AOFA_I00:def 59 b := (t1 mod (. (2,A,g))); coherence b := (t1 mod (. (2,A,g))) is absolutely-terminating Element of A ; funct1 is_even -> absolutely-terminating Element of A equals :: AOFA_I00:def 60 b := ((t1 + 1) mod (. (2,A,g))); coherence b := ((t1 + 1) mod (. (2,A,g))) is absolutely-terminating Element of A ; let t2 be INT-Expression of A,g; funct1 leq t2 -> absolutely-terminating Element of A equals :: AOFA_I00:def 61 b := (leq (t1,t2)); coherence b := (leq (t1,t2)) is absolutely-terminating Element of A ; funct1 gt t2 -> absolutely-terminating Element of A equals :: AOFA_I00:def 62 b := (gt (t1,t2)); coherence b := (gt (t1,t2)) is absolutely-terminating Element of A ; funct1 eq t2 -> absolutely-terminating Element of A equals :: AOFA_I00:def 63 b := (eq (t1,t2)); coherence b := (eq (t1,t2)) is absolutely-terminating Element of A ; end; :: deftheorem defines is_odd AOFA_I00:def_59_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for b being Element of X for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0) for t1 being INT-Expression of A,g holds t1 is_odd = b := (t1 mod (. (2,A,g))); :: deftheorem defines is_even AOFA_I00:def_60_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for b being Element of X for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0) for t1 being INT-Expression of A,g holds t1 is_even = b := ((t1 + 1) mod (. (2,A,g))); :: deftheorem defines leq AOFA_I00:def_61_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for b being Element of X for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0) for t1, t2 being INT-Expression of A,g holds t1 leq t2 = b := (leq (t1,t2)); :: deftheorem defines gt AOFA_I00:def_62_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for b being Element of X for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0) for t1, t2 being INT-Expression of A,g holds t1 gt t2 = b := (gt (t1,t2)); :: deftheorem defines eq AOFA_I00:def_63_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for b being Element of X for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0) for t1, t2 being INT-Expression of A,g holds t1 eq t2 = b := (eq (t1,t2)); notation let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let b be Element of X; let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0); let t1, t2 be INT-Expression of A,g; synonym t2 geq t1 for t1 leq t2; synonym t2 lt t1 for t1 gt t2; end; definition let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let b be Element of X; let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0); let v1, v2 be INT-Variable of A,g; funcv1 leq v2 -> absolutely-terminating Element of A equals :: AOFA_I00:def 64 (. v1) leq (. v2); coherence (. v1) leq (. v2) is absolutely-terminating Element of A ; funcv1 gt v2 -> absolutely-terminating Element of A equals :: AOFA_I00:def 65 (. v1) gt (. v2); coherence (. v1) gt (. v2) is absolutely-terminating Element of A ; end; :: deftheorem defines leq AOFA_I00:def_64_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for b being Element of X for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0) for v1, v2 being INT-Variable of A,g holds v1 leq v2 = (. v1) leq (. v2); :: deftheorem defines gt AOFA_I00:def_65_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for b being Element of X for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0) for v1, v2 being INT-Variable of A,g holds v1 gt v2 = (. v1) gt (. v2); notation let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let b be Element of X; let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0); let v1, v2 be INT-Variable of A,g; synonym v2 geq v1 for v1 leq v2; synonym v2 lt v1 for v1 gt v2; end; definition let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let b be Element of X; let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0); let x1 be Variable of g; funcx1 is_odd -> absolutely-terminating Element of A equals :: AOFA_I00:def 66 (. x1) is_odd ; coherence (. x1) is_odd is absolutely-terminating Element of A ; funcx1 is_even -> absolutely-terminating Element of A equals :: AOFA_I00:def 67 (. x1) is_even ; coherence (. x1) is_even is absolutely-terminating Element of A ; let x2 be Variable of g; funcx1 leq x2 -> absolutely-terminating Element of A equals :: AOFA_I00:def 68 (. x1) leq (. x2); coherence (. x1) leq (. x2) is absolutely-terminating Element of A ; funcx1 gt x2 -> absolutely-terminating Element of A equals :: AOFA_I00:def 69 (. x1) gt (. x2); coherence (. x1) gt (. x2) is absolutely-terminating Element of A ; end; :: deftheorem defines is_odd AOFA_I00:def_66_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for b being Element of X for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0) for x1 being Variable of g holds x1 is_odd = (. x1) is_odd ; :: deftheorem defines is_even AOFA_I00:def_67_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for b being Element of X for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0) for x1 being Variable of g holds x1 is_even = (. x1) is_even ; :: deftheorem defines leq AOFA_I00:def_68_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for b being Element of X for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0) for x1, x2 being Variable of g holds x1 leq x2 = (. x1) leq (. x2); :: deftheorem defines gt AOFA_I00:def_69_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for b being Element of X for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0) for x1, x2 being Variable of g holds x1 gt x2 = (. x1) gt (. x2); notation let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let b be Element of X; let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0); let x1, x2 be Variable of g; synonym x2 geq x1 for x1 leq x2; synonym x2 lt x1 for x1 gt x2; end; definition let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let b be Element of X; let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0); let x be Variable of g; let i be integer number ; funcx leq i -> absolutely-terminating Element of A equals :: AOFA_I00:def 70 (. x) leq (. (i,A,g)); coherence (. x) leq (. (i,A,g)) is absolutely-terminating Element of A ; funcx geq i -> absolutely-terminating Element of A equals :: AOFA_I00:def 71 (. x) geq (. (i,A,g)); coherence (. x) geq (. (i,A,g)) is absolutely-terminating Element of A ; funcx gt i -> absolutely-terminating Element of A equals :: AOFA_I00:def 72 (. x) gt (. (i,A,g)); coherence (. x) gt (. (i,A,g)) is absolutely-terminating Element of A ; funcx lt i -> absolutely-terminating Element of A equals :: AOFA_I00:def 73 (. x) lt (. (i,A,g)); coherence (. x) lt (. (i,A,g)) is absolutely-terminating Element of A ; funcx / i -> INT-Expression of A,g equals :: AOFA_I00:def 74 (. x) div (. (i,A,g)); coherence (. x) div (. (i,A,g)) is INT-Expression of A,g ; end; :: deftheorem defines leq AOFA_I00:def_70_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for b being Element of X for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0) for x being Variable of g for i being integer number holds x leq i = (. x) leq (. (i,A,g)); :: deftheorem defines geq AOFA_I00:def_71_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for b being Element of X for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0) for x being Variable of g for i being integer number holds x geq i = (. x) geq (. (i,A,g)); :: deftheorem defines gt AOFA_I00:def_72_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for b being Element of X for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0) for x being Variable of g for i being integer number holds x gt i = (. x) gt (. (i,A,g)); :: deftheorem defines lt AOFA_I00:def_73_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for b being Element of X for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0) for x being Variable of g for i being integer number holds x lt i = (. x) lt (. (i,A,g)); :: deftheorem defines / AOFA_I00:def_74_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for b being Element of X for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0) for x being Variable of g for i being integer number holds x / i = (. x) div (. (i,A,g)); definition let A be Euclidean preIfWhileAlgebra; let X be non empty countable set ; let T be Subset of (Funcs (X,INT)); let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; let x1, x2 be Variable of f; funcx1 += x2 -> absolutely-terminating Element of A equals :: AOFA_I00:def 75 x1 += (. x2); coherence x1 += (. x2) is absolutely-terminating Element of A ; funcx1 *= x2 -> absolutely-terminating Element of A equals :: AOFA_I00:def 76 x1 *= (. x2); coherence x1 *= (. x2) is absolutely-terminating Element of A ; funcx1 %= x2 -> absolutely-terminating Element of A equals :: AOFA_I00:def 77 x1 := ((. x1) mod (. x2)); coherence x1 := ((. x1) mod (. x2)) is absolutely-terminating Element of A ; funcx1 /= x2 -> absolutely-terminating Element of A equals :: AOFA_I00:def 78 x1 := ((. x1) div (. x2)); coherence x1 := ((. x1) div (. x2)) is absolutely-terminating Element of A ; funcx1 + x2 -> INT-Expression of A,f equals :: AOFA_I00:def 79 (. x1) + (. x2); coherence (. x1) + (. x2) is INT-Expression of A,f ; funcx1 * x2 -> INT-Expression of A,f equals :: AOFA_I00:def 80 (. x1) (#) (. x2); coherence (. x1) (#) (. x2) is INT-Expression of A,f ; funcx1 mod x2 -> INT-Expression of A,f equals :: AOFA_I00:def 81 (. x1) mod (. x2); coherence (. x1) mod (. x2) is INT-Expression of A,f ; funcx1 div x2 -> INT-Expression of A,f equals :: AOFA_I00:def 82 (. x1) div (. x2); coherence (. x1) div (. x2) is INT-Expression of A,f ; end; :: deftheorem defines += AOFA_I00:def_75_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for x1, x2 being Variable of f holds x1 += x2 = x1 += (. x2); :: deftheorem defines *= AOFA_I00:def_76_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for x1, x2 being Variable of f holds x1 *= x2 = x1 *= (. x2); :: deftheorem defines %= AOFA_I00:def_77_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for x1, x2 being Variable of f holds x1 %= x2 = x1 := ((. x1) mod (. x2)); :: deftheorem defines /= AOFA_I00:def_78_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for x1, x2 being Variable of f holds x1 /= x2 = x1 := ((. x1) div (. x2)); :: deftheorem defines + AOFA_I00:def_79_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for x1, x2 being Variable of f holds x1 + x2 = (. x1) + (. x2); :: deftheorem defines * AOFA_I00:def_80_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for x1, x2 being Variable of f holds x1 * x2 = (. x1) (#) (. x2); :: deftheorem defines mod AOFA_I00:def_81_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for x1, x2 being Variable of f holds x1 mod x2 = (. x1) mod (. x2); :: deftheorem defines div AOFA_I00:def_82_:_ for A being Euclidean preIfWhileAlgebra for X being non empty countable set for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for x1, x2 being Variable of f holds x1 div x2 = (. x1) div (. x2); theorem Th24: :: AOFA_I00:24 for A being Euclidean preIfWhileAlgebra for X being non empty countable set for s being Element of Funcs (X,INT) for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for v being INT-Variable of A,f for t being INT-Expression of A,f holds ( (f . (s,(v := t))) . (v . s) = t . s & ( for z being Element of X st z <> v . s holds (f . (s,(v := t))) . z = s . z ) ) proofend; theorem Th25: :: AOFA_I00:25 for A being Euclidean preIfWhileAlgebra for X being non empty countable set for s being Element of Funcs (X,INT) for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for x being Variable of f for i being integer number holds ( (f . (s,(x := i))) . x = i & ( for z being Element of X st z <> x holds (f . (s,(x := i))) . z = s . z ) ) proofend; 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 ) ) proofend; 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 ) ) proofend; theorem Th28: :: AOFA_I00:28 for A being Euclidean preIfWhileAlgebra for X being non empty countable set for s being Element of Funcs (X,INT) for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for i being integer number for x being Variable of f holds ( (f . (s,(x += i))) . x = (s . x) + i & ( for z being Element of X st z <> x holds (f . (s,(x += i))) . z = s . z ) ) proofend; 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 ) ) proofend; 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 ) ) proofend; theorem Th31: :: AOFA_I00:31 for A being Euclidean preIfWhileAlgebra for X being non empty countable set for s being Element of Funcs (X,INT) for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for i being integer number for x being Variable of f holds ( (f . (s,(x *= i))) . x = (s . x) * i & ( for z being Element of X st z <> x holds (f . (s,(x *= i))) . z = s . z ) ) proofend; 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 ) ) proofend; 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 ) ) proofend; theorem Th34: :: AOFA_I00:34 for A being Euclidean preIfWhileAlgebra for X being non empty countable set for s being Element of Funcs (X,INT) for b being Element of X for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0) for x being Variable of g for i being integer number holds ( ( s . x <= i implies (g . (s,(x leq i))) . b = 1 ) & ( s . x > i implies (g . (s,(x leq i))) . b = 0 ) & ( s . x >= i implies (g . (s,(x geq i))) . b = 1 ) & ( s . x < i implies (g . (s,(x geq i))) . b = 0 ) & ( for z being Element of X st z <> b holds ( (g . (s,(x leq i))) . z = s . z & (g . (s,(x geq i))) . z = s . z ) ) ) proofend; 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 ) ) proofend; theorem :: AOFA_I00:36 for A being Euclidean preIfWhileAlgebra for X being non empty countable set for s being Element of Funcs (X,INT) for b being Element of X for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0) for x being Variable of g for i being integer number holds ( ( s . x <= i implies g . (s,(x leq i)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x leq i)) in (Funcs (X,INT)) \ (b,0) implies s . x <= i ) & ( s . x >= i implies g . (s,(x geq i)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x geq i)) in (Funcs (X,INT)) \ (b,0) implies s . x >= i ) ) proofend; 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 ) ) proofend; theorem Th38: :: AOFA_I00:38 for A being Euclidean preIfWhileAlgebra for X being non empty countable set for s being Element of Funcs (X,INT) for b being Element of X for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0) for x being Variable of g for i being integer number holds ( ( s . x > i implies (g . (s,(x gt i))) . b = 1 ) & ( s . x <= i implies (g . (s,(x gt i))) . b = 0 ) & ( s . x < i implies (g . (s,(x lt i))) . b = 1 ) & ( s . x >= i implies (g . (s,(x lt i))) . b = 0 ) & ( for z being Element of X st z <> b holds ( (g . (s,(x gt i))) . z = s . z & (g . (s,(x lt i))) . z = s . z ) ) ) proofend; 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 ) ) ) proofend; theorem Th40: :: AOFA_I00:40 for A being Euclidean preIfWhileAlgebra for X being non empty countable set for s being Element of Funcs (X,INT) for b being Element of X for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0) for x being Variable of g for i being integer number holds ( ( s . x > i implies g . (s,(x gt i)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x gt i)) in (Funcs (X,INT)) \ (b,0) implies s . x > i ) & ( s . x < i implies g . (s,(x lt i)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x lt i)) in (Funcs (X,INT)) \ (b,0) implies s . x < i ) ) proofend; 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 ) ) proofend; theorem :: AOFA_I00:42 for A being Euclidean preIfWhileAlgebra for X being non empty countable set for s being Element of Funcs (X,INT) for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for i being integer number for x being Variable of f holds ( (f . (s,(x %= i))) . x = (s . x) mod i & ( for z being Element of X st z <> x holds (f . (s,(x %= i))) . z = s . z ) ) proofend; 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 ) ) proofend; 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 ) ) proofend; theorem Th45: :: AOFA_I00:45 for A being Euclidean preIfWhileAlgebra for X being non empty countable set for s being Element of Funcs (X,INT) for T being Subset of (Funcs (X,INT)) for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T for i being integer number for x being Variable of f holds ( (f . (s,(x /= i))) . x = (s . x) div i & ( for z being Element of X st z <> x holds (f . (s,(x /= i))) . z = s . z ) ) proofend; 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 ) ) proofend; 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 ) ) proofend; 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 ) ) ) proofend; 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 ) ) proofend; 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 ) ) proofend; 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 ) ) proofend; scheme :: AOFA_I00:sch 1 ForToIteration{ F1() -> Euclidean preIfWhileAlgebra, F2() -> non empty countable set , F3() -> Element of F2(), F4() -> Element of F1(), F5() -> Element of F1(), F6() -> Euclidean ExecutionFunction of F1(), Funcs (F2(),INT),(Funcs (F2(),INT)) \ (F3(),0), F7() -> Variable of F6(), F8() -> Variable of F6(), F9() -> Element of Funcs (F2(),INT), F10() -> INT-Expression of F1(),F6(), P1[ set ] } : ( P1[F6() . (F9(),F5())] & ( F10() . F9() <= F9() . F8() implies (F6() . (F9(),F5())) . F7() = (F9() . F8()) + 1 ) & ( F10() . F9() > F9() . F8() implies (F6() . (F9(),F5())) . F7() = F10() . F9() ) & (F6() . (F9(),F5())) . F8() = F9() . F8() ) provided A1: F5() = for-do ((F7() := F10()),(F7() leq F8()),(F7() += 1),F4()) and A2: P1[F6() . (F9(),(F7() := F10()))] and A3: for s being Element of Funcs (F2(),INT) st P1[s] holds ( P1[F6() . (s,(F4() \; (F7() += 1)))] & P1[F6() . (s,(F7() leq F8()))] ) and A4: for s being Element of Funcs (F2(),INT) st P1[s] holds ( (F6() . (s,F4())) . F7() = s . F7() & (F6() . (s,F4())) . F8() = s . F8() ) and A5: ( F8() <> F7() & F8() <> F3() & F7() <> F3() ) proofend; scheme :: AOFA_I00:sch 2 ForDowntoIteration{ F1() -> Euclidean preIfWhileAlgebra, F2() -> non empty countable set , F3() -> Element of F2(), F4() -> Element of F1(), F5() -> Element of F1(), F6() -> Euclidean ExecutionFunction of F1(), Funcs (F2(),INT),(Funcs (F2(),INT)) \ (F3(),0), F7() -> Variable of F6(), F8() -> Variable of F6(), F9() -> Element of Funcs (F2(),INT), F10() -> INT-Expression of F1(),F6(), P1[ set ] } : ( P1[F6() . (F9(),F5())] & ( F10() . F9() >= F9() . F8() implies (F6() . (F9(),F5())) . F7() = (F9() . F8()) - 1 ) & ( F10() . F9() < F9() . F8() implies (F6() . (F9(),F5())) . F7() = F10() . F9() ) & (F6() . (F9(),F5())) . F8() = F9() . F8() ) provided A1: F5() = for-do ((F7() := F10()),((. F8()) leq (. F7())),(F7() += (- 1)),F4()) and A2: P1[F6() . (F9(),(F7() := F10()))] and A3: for s being Element of Funcs (F2(),INT) st P1[s] holds ( P1[F6() . (s,(F4() \; (F7() += (- 1))))] & P1[F6() . (s,(F8() leq F7()))] ) and A4: for s being Element of Funcs (F2(),INT) st P1[s] holds ( (F6() . (s,F4())) . F7() = s . F7() & (F6() . (s,F4())) . F8() = s . F8() ) and A5: ( F8() <> F7() & F8() <> F3() & F7() <> F3() ) proofend; begin theorem Th52: :: AOFA_I00:52 for A being Euclidean preIfWhileAlgebra for X being non empty countable set for s being Element of Funcs (X,INT) for b being Element of X for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0) for I being Element of A for i, n being Variable of g st ex d being Function st ( d . b = 0 & d . n = 1 & d . i = 2 ) & ( for s being Element of Funcs (X,INT) holds ( (g . (s,I)) . n = s . n & (g . (s,I)) . i = s . i ) ) holds g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n)) proofend; 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)) proofend; 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 proofend; 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 proofend; begin definition let X be non empty countable set ; let A be Euclidean preIfWhileAlgebra; let T be Subset of (Funcs (X,INT)); let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; let s be Element of Funcs (X,INT); let I be Element of A; :: original:. redefine funcf . (s,I) -> Element of Funcs (X,INT); coherence f . (s,I) is Element of Funcs (X,INT) proofend; 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 proofend; 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 ! proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 ) ) ) proofend; 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 ) } proofend; 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 proofend; Lm2: for A being Euclidean preIfWhileAlgebra for X being non empty countable set for b being Element of X for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0) for x, y, z being Variable of g st ex d being Function st ( d . b = 0 & d . x = 1 & d . y = 2 & d . z = 3 ) holds for s being Element of Funcs (X,INT) holds ( (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . x = s . y & (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . y = abs ((s . x) - (s . y)) & ( for n, m being Element of NAT st n = s . x & m = s . y & ( s in (Funcs (X,INT)) \ (b,0) implies m > 0 ) & ( m > 0 implies s in (Funcs (X,INT)) \ (b,0) ) holds g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0),s ) ) proofend; 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 ) } proofend; 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 proofend; 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 } proofend; :: [WP: ] Correctness_of_the_algorithm_of_exponentiation_by_squaring theorem :: AOFA_I00:67 for A being Euclidean preIfWhileAlgebra for X being non empty countable set for b being Element of X for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0) for x, y, m being Variable of g st ex d being Function st ( d . b = 0 & d . x = 1 & d . y = 2 & d . m = 3 ) holds for s being Element of Funcs (X,INT) for n being Nat st n = s . m holds (g . (s,((y := 1) \; (while ((m gt 0),(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x))))))) . y = (s . x) |^ n proofend;