:: Analysis of Algorithms: An Example of a Sort Algorithm :: by Grzegorz Bancerek :: :: Received November 9, 2012 :: Copyright (c) 2012-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies INT_1, AOFA_A00, XBOOLE_0, STRUCT_0, RELAT_1, PBOOLE, MSAFREE4, NAT_1, SUBSET_1, ORDINAL1, MSUALG_1, AOFA_000, ZF_MODEL, FUNCT_1, INCPROJ, FUNCT_2, CARD_1, GRAPHSP, AOFA_I00, QC_LANG1, MSAFREE, AOFA_A01, ARYTM_3, NEWTON, ABCMIZ_1, ZFMISC_1, XREAL_0, MSUALG_3, GROUP_6, REAL_1, MSUALG_2, TARSKI, MARGREL1, XBOOLEAN, PARTFUN1, FINSEQ_1, XXREAL_0, CARD_3, NUMBERS, FUNCT_7, ARYTM_1, PRELAMB, REALSET1, TREES_4, POWER, PROB_2, FUNCT_6, PZFMISC1, ALGSTR_4, ORDINAL4, MEMBERED, FINSET_1, XXREAL_2, AFINSQ_1, EXCHSORT, FUNCT_4, FUNCOP_1, FINSEQ_4, MODELC_3, UNIALG_1, WELLORD1, ORDERS_2, LFUZZY_0, REARRAN1, SETLIM_2, MCART_1, EQUATION, FOMODEL2, TREES_2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, WELLORD2, MCART_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, MARGREL1, XTUPLE_0, FUNCT_4, FUNCT_6, FUNCT_7, FUNCOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, AFINSQ_1, CARD_1, CARD_3, POWER, MEMBERED, STRUCT_0, ORDINAL1, NAT_1, BINOP_1, PBOOLE, TREES_3, TREES_4, PZFMISC1, TREES_2, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, XXREAL_2, INT_1, NAT_D, NEWTON, TREES_1, PROB_2, ORDERS_2, WAYBEL_0, LFUZZY_0, UNIALG_1, FREEALG, COMPUT_1, PUA2MSS1, MSUALG_1, MSUALG_2, MSUALG_3, MSAFREE, MSAFREE1, MSUALG_6, MSAFREE3, MSATERM, AOFA_000, EXCHSORT, MSAFREE4, AOFA_A00; constructors XBOOLE_0, AOFA_000, AOFA_A00, SUBSET_1, BINOP_1, ORDINAL1, NAT_1, INSTALG1, MSAFREE3, ZFMISC_1, NEWTON, XCMPLX_0, MSAFREE4, CATALG_1, AUTALG_1, POWER, PUA2MSS1, MSUALG_3, FINSEQ_4, NUMBERS, RELSET_1, REAL_1, MSAFREE1, PZFMISC1, PRALG_2, SQUARE_1, NAT_D, XXREAL_0, XXREAL_2, EXCHSORT, AFINSQ_1, WELLORD2, FUNCT_4, PARTFUN1, COMPUT_1, LFUZZY_0, MEMBERED, WAYBEL_0, MCART_1, MSATERM, TREES_9, TREES_2; registrations AOFA_000, AOFA_A00, ORDINAL1, NUMBERS, PBOOLE, MSUALG_1, INSTALG1, MSAFREE4, FUNCOP_1, RELSET_1, STRUCT_0, INT_1, XREAL_0, MSUALG_2, FUNCT_1, FINSEQ_1, XBOOLEAN, MARGREL1, XBOOLE_0, NAT_1, RELAT_1, MSUALG_9, POWER, MEMBERED, XXREAL_2, EXCHSORT, FINSET_1, AFINSQ_1, CARD_1, UNIALG_1, LFUZZY_0, TREES_3, TREES_2, VALUED_0, XTUPLE_0; requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL; begin :: Exponentiation by squaring revisited theorem :: AOFA_A01:1 1 mod 2 = 1 & 2 mod 2 = 0; theorem :: AOFA_A01:2 for S being non empty non void ManySortedSign for A being MSAlgebra over S for B being MSSubAlgebra of A for s being SortSymbol of S for a being set st a in (the Sorts of B).s holds a in (the Sorts of A).s; theorem :: AOFA_A01:3 for I being non empty set, a,b,c being set, i being Element of I holds c in (i-singleton a).b iff b = i & c = a; theorem :: AOFA_A01:4 for I being non empty set, a,b,c,d being set, i,j being Element of I holds c in ((i-singleton a)(\/)(j-singleton d)).b iff b = i & c = a or b = j & c = d; definition let S be (4,1) integer bool-correct non empty non void BoolSignature; let A be non-empty MSAlgebra over S; attr A is integer means :: AOFA_A01:def 1 ex C being image of A st C is (4,1) integer bool-correct MSAlgebra over S; end; theorem :: AOFA_A01:5 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S holds Image id the Sorts of A = the MSAlgebra of A; theorem :: AOFA_A01:6 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S holds A is image of A; registration let S be (4,1) integer bool-correct non empty non void BoolSignature; cluster integer for non-empty MSAlgebra over S; end; registration let S be (4,1) integer bool-correct non empty non void BoolSignature; let A be integer non-empty MSAlgebra over S; cluster bool-correct for image of A; end; registration let S be (4,1) integer bool-correct non empty non void BoolSignature; let A be integer non-empty MSAlgebra over S; cluster (4,1) integer for bool-correct image of A; end; theorem :: AOFA_A01:7 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for o being OperSymbol of S, a being set, r being SortSymbol of S st o is_of_type a,r holds Den(o,A) is Function of (the Sorts of A)#.a, (the Sorts of A).r & Args(o,A) = (the Sorts of A)#.a & Result(o,A) = (the Sorts of A).r; registration let S be bool-correct non empty non void BoolSignature; let A be bool-correct non-empty MSAlgebra over S; cluster -> bool-correct for non-empty MSSubAlgebra of A; end; registration let S be (4,1) integer bool-correct non empty non void BoolSignature; let A be (4,1) integer bool-correct non-empty MSAlgebra over S; cluster -> (4,1) integer for non-empty MSSubAlgebra of A; end; registration let S be (4,1) integer bool-correct non empty non void BoolSignature; let X be non-empty ManySortedSet of the carrier of S; cluster Free(S,X) -> integer for non-empty MSAlgebra over S; end; theorem :: AOFA_A01:8 for S being non empty non void ManySortedSign for A1,A2,B1 being MSAlgebra over S, B2 being non-empty MSAlgebra over S st the MSAlgebra of A1 = the MSAlgebra of A2 & the MSAlgebra of B1 = the MSAlgebra of B2 for h1 being ManySortedFunction of A1,B1 for h2 being ManySortedFunction of A2,B2 st h1 = h2 & h1 is_epimorphism A1,B1 holds h2 is_epimorphism A2,B2; registration let S be (4,1) integer bool-correct non empty non void BoolSignature; let X be non-empty ManySortedSet of the carrier of S; cluster vf-free integer for all_vars_including inheriting_operations free_in_itself (X,S)-terms non-empty VarMSAlgebra over S; end; definition let S be non empty non void ManySortedSign; let X be non-empty ManySortedSet of the carrier of S; let T be all_vars_including inheriting_operations (X,S)-terms MSAlgebra over S; func FreeGen T -> non-empty GeneratorSet of T equals :: AOFA_A01:def 2 FreeGen X; end; registration let S be non empty non void ManySortedSign; let X0 be countable non-empty ManySortedSet of the carrier of S; let T be all_vars_including inheriting_operations free_in_itself (X0,S)-terms MSAlgebra over S; cluster FreeGen T -> (Equations(S, T))-free non-empty; end; definition let S be non empty non void ManySortedSign; let X be non-empty ManySortedSet of the carrier of S; let T be all_vars_including inheriting_operations (X,S)-terms MSAlgebra over S; let G be GeneratorSet of T; attr G is basic means :: AOFA_A01:def 3 FreeGen T c= G; let s be SortSymbol of S; let x be Element of G.s; attr x is pure means :: AOFA_A01:def 4 x in (FreeGen T).s; end; registration let S be non empty non void ManySortedSign; let X be non-empty ManySortedSet of the carrier of S; let T be all_vars_including inheriting_operations (X,S)-terms MSAlgebra over S; cluster FreeGen T -> basic; end; registration let S be non empty non void ManySortedSign; let X be non-empty ManySortedSet of the carrier of S; let T be all_vars_including inheriting_operations (X,S)-terms MSAlgebra over S; cluster basic for non-empty GeneratorSet of T; end; registration let S be non empty non void ManySortedSign; let X be non-empty ManySortedSet of the carrier of S; let T be all_vars_including inheriting_operations (X,S)-terms MSAlgebra over S; let G be basic GeneratorSet of T; let s be SortSymbol of S; cluster pure for Element of G.s; end; theorem :: AOFA_A01:9 for S being non empty non void ManySortedSign for X being non-empty ManySortedSet of the carrier of S for T being all_vars_including inheriting_operations (X,S)-terms MSAlgebra over S for G being basic GeneratorSet of T for s being SortSymbol of S for a being set holds a is pure Element of G.s iff a in (FreeGen T).s; definition let S be non empty non void ManySortedSign; let X be non-empty ManySortedSet of the carrier of S; let T be all_vars_including inheriting_operations free_in_itself (X,S)-terms MSAlgebra over S; let G be GeneratorSystem over S,X,T; attr G is basic means :: AOFA_A01:def 5 the generators of G is basic; end; registration let S be non empty non void ManySortedSign; let X be non-empty ManySortedSet of the carrier of S; let T be all_vars_including inheriting_operations free_in_itself (X,S)-terms MSAlgebra over S; cluster basic for GeneratorSystem over S,X,T; end; registration let S be non empty non void ManySortedSign; let X be non-empty ManySortedSet of the carrier of S; let T be all_vars_including inheriting_operations free_in_itself (X,S)-terms MSAlgebra over S; let G be basic GeneratorSystem over S,X,T; cluster the generators of G -> basic; end; reserve S for (4,1) integer bool-correct non empty non void BoolSignature, X for non-empty ManySortedSet of the carrier of S, T for vf-free integer all_vars_including inheriting_operations free_in_itself (X,S)-terms VarMSAlgebra over S, C for (4,1) integer bool-correct non-empty image of T, G for basic GeneratorSystem over S,X,T, A for IfWhileAlgebra of the generators of G, I for integer SortSymbol of S, x,y,z,m for pure (Element of (the generators of G).I), b for pure (Element of (the generators of G).the bool-sort of S), t,t1,t2 for Element of T,I, P for Algorithm of A, s,s1,s2 for Element of C-States(the generators of G); definition let S be bool-correct non empty non void BoolSignature; let A be non-empty MSAlgebra over S; func \falseA -> Element of A, the bool-sort of S equals :: AOFA_A01:def 6 \not\trueA; end; reserve f for ExecutionFunction of A, C-States(the generators of G), (\falseC)-States(the generators of G, b); theorem :: AOFA_A01:10 \falseC = FALSE; definition let S be bool-correct non empty non void BoolSignature; let X be non-empty ManySortedSet of the carrier of S; let T be all_vars_including inheriting_operations free_in_itself (X,S)-terms MSAlgebra over S; let G be GeneratorSystem over S,X,T; let b be Element of (the generators of G).the bool-sort of S; let C be image of T; let A be preIfWhileAlgebra; let f be ExecutionFunction of A, C-States(the generators of G), (\falseC)-States(the generators of G, b); let s be Element of C-States(the generators of G); let P be Algorithm of A; redefine func f.(s,P) -> Element of C-States(the generators of G); end; definition let S be non empty non void ManySortedSign; let T be non-empty MSAlgebra over S; let G be non-empty GeneratorSet of T; let s be SortSymbol of S; let x be Element of G.s; func @x -> Element of T,s equals :: AOFA_A01:def 7 x; end; definition let S,X,T,G,A,b,I,t1,t2; func b leq(t1, t2, A) -> Algorithm of A equals :: AOFA_A01:def 8 b:=(leq(t1,t2),A); func b gt(t1, t2, A) -> Algorithm of A equals :: AOFA_A01:def 9 b:=(\not(leq(t1,t2)),A); end; definition let S,X,T,I; func \2(T,I) -> Element of T,I equals :: AOFA_A01:def 10 \1(T,I)+\1(T,I); end; definition let S,X,T,G,A,b,I,t; func t is_odd(b,A) -> Algorithm of A equals :: AOFA_A01:def 11 b gt(t mod \2(T,I),\0(T,I),A); func t is_even(b,A) -> Algorithm of A equals :: AOFA_A01:def 12 b leq(t mod \2(T,I),\0(T,I),A); end; registration let S,X,T,G,C,I,s; let x be Element of (the generators of G).I; cluster s.I.x -> integer; end; registration let S,X,T,G,C,I,s,t; cluster t value_at(C,s) -> integer; end; reserve u for ManySortedFunction of FreeGen T, the Sorts of C; registration let S,X,T,C,I,u,t; cluster t value_at(C,u) -> integer; end; registration let S,X,T,G,C,s; let t be Element of T, the bool-sort of S; cluster t value_at(C,s) -> boolean; end; registration let S,X,T,C,u; let t be Element of T, the bool-sort of S; cluster t value_at(C,u) -> boolean; end; theorem :: AOFA_A01:11 for o being OperSymbol of S st o = In((the connectives of S).1, the carrier' of S) holds o = (the connectives of S).1 & the_arity_of o = {} & the_result_sort_of o = the bool-sort of S; theorem :: AOFA_A01:12 for o being OperSymbol of S st o = In((the connectives of S).2, the carrier' of S) holds o = (the connectives of S).2 & the_arity_of o = <*the bool-sort of S*> & the_result_sort_of o = the bool-sort of S; theorem :: AOFA_A01:13 for o being OperSymbol of S st o = In((the connectives of S).3, the carrier' of S) holds o = (the connectives of S).3 & the_arity_of o = <*the bool-sort of S, the bool-sort of S*> & the_result_sort_of o = the bool-sort of S; theorem :: AOFA_A01:14 for o being OperSymbol of S st o = In((the connectives of S).4, the carrier' of S) holds the_arity_of o = {} & the_result_sort_of o = I; theorem :: AOFA_A01:15 for o being OperSymbol of S st o = In((the connectives of S).5, the carrier' of S) holds the_arity_of o = {} & the_result_sort_of o = I; theorem :: AOFA_A01:16 for o being OperSymbol of S st o = In((the connectives of S).6, the carrier' of S) holds the_arity_of o = <*I*> & the_result_sort_of o = I; theorem :: AOFA_A01:17 for o being OperSymbol of S st o = In((the connectives of S).7, the carrier' of S) holds the_arity_of o = <*I,I*> & the_result_sort_of o = I; theorem :: AOFA_A01:18 for o being OperSymbol of S st o = In((the connectives of S).8, the carrier' of S) holds the_arity_of o = <*I,I*> & the_result_sort_of o = I; theorem :: AOFA_A01:19 for o being OperSymbol of S st o = In((the connectives of S).9, the carrier' of S) holds the_arity_of o = <*I,I*> & the_result_sort_of o = I; theorem :: AOFA_A01:20 for o being OperSymbol of S st o = In((the connectives of S).10, the carrier' of S) holds the_arity_of o = <*I,I*> & the_result_sort_of o = the bool-sort of S; theorem :: AOFA_A01:21 for S being non empty non void ManySortedSign for o being OperSymbol of S st the_arity_of o = {} for A being MSAlgebra over S holds Args(o,A) = {{}}; theorem :: AOFA_A01:22 for S being non empty non void ManySortedSign for a being SortSymbol of S for o being OperSymbol of S st the_arity_of o = <*a*> for A being MSAlgebra over S holds Args(o,A) = product <*(the Sorts of A).a*>; theorem :: AOFA_A01:23 for S being non empty non void ManySortedSign for a,b being SortSymbol of S for o being OperSymbol of S st the_arity_of o = <*a,b*> for A being MSAlgebra over S holds Args(o,A) = product <*(the Sorts of A).a, (the Sorts of A).b*>; theorem :: AOFA_A01:24 for S being non empty non void ManySortedSign for a,b,c being SortSymbol of S for o being OperSymbol of S st the_arity_of o = <*a,b,c*> for A being MSAlgebra over S holds Args(o,A) = product <*(the Sorts of A).a, (the Sorts of A).b, (the Sorts of A).c*>; theorem :: AOFA_A01:25 for S being non empty non void ManySortedSign for A,B being non-empty MSAlgebra over S for s being SortSymbol of S for a being Element of A,s for h being ManySortedFunction of A,B for o being OperSymbol of S st the_arity_of o = <*s*> for p being Element of Args(o,A) st p = <*a*> holds h#p = <*h.s.a*>; theorem :: AOFA_A01:26 for S being non empty non void ManySortedSign for A,B being non-empty MSAlgebra over S for s1,s2 being SortSymbol of S for a being Element of A,s1, b being Element of A,s2 for h being ManySortedFunction of A,B for o being OperSymbol of S st the_arity_of o = <*s1,s2*> for p being Element of Args(o,A) st p = <*a,b*> holds h#p = <*h.s1.a, h.s2.b*>; theorem :: AOFA_A01:27 for S being non empty non void ManySortedSign for A,B being non-empty MSAlgebra over S for s1,s2,s3 being SortSymbol of S for a being Element of A,s1, b being Element of A,s2, c being Element of A,s3 for h being ManySortedFunction of A,B for o being OperSymbol of S st the_arity_of o = <*s1,s2,s3*> for p being Element of Args(o,A) st p = <*a,b,c*> holds h#p = <*h.s1.a,h.s2.b,h.s3.c*>; theorem :: AOFA_A01:28 for h being ManySortedFunction of T,C st h is_homomorphism T,C for a being SortSymbol of S for t being Element of T,a holds t value_at(C,h||FreeGen T) = h.a.t; theorem :: AOFA_A01:29 for h being ManySortedFunction of T,C st h is_homomorphism T,C & s = h||the generators of G for a being SortSymbol of S for t being Element of T,a holds t value_at(C,s) = h.a.t; theorem :: AOFA_A01:30 \trueT value_at(C,s) = TRUE; theorem :: AOFA_A01:31 for t being Element of T, the bool-sort of S holds \nott value_at(C,s) = \not(t value_at(C,s)); theorem :: AOFA_A01:32 for a being boolean object for t being Element of T, the bool-sort of S holds \nott value_at(C,s) = 'not' a iff t value_at(C,s) = a; theorem :: AOFA_A01:33 for a being Element of C, the bool-sort of S for x being boolean object holds \nota = 'not' x iff a = x; theorem :: AOFA_A01:34 (\falseT) value_at(C,s) = FALSE; theorem :: AOFA_A01:35 for t1,t2 being Element of T, the bool-sort of S holds t1\andt2 value_at(C,s) = (t1 value_at(C,s))\and(t2 value_at(C,s)); theorem :: AOFA_A01:36 \0(T,I) value_at(C,s) = 0; theorem :: AOFA_A01:37 \1(T,I) value_at(C,s) = 1; theorem :: AOFA_A01:38 (-t) value_at(C,s) = -(t value_at(C,s)); theorem :: AOFA_A01:39 (t1+t2) value_at(C,s) = (t1 value_at(C,s))+(t2 value_at(C,s)); theorem :: AOFA_A01:40 \2(T,I) value_at (C,s) = 2; theorem :: AOFA_A01:41 (t1-t2) value_at(C,s) = (t1 value_at(C,s))-(t2 value_at(C,s)); theorem :: AOFA_A01:42 (t1*t2) value_at(C,s) = (t1 value_at(C,s))*(t2 value_at(C,s)); theorem :: AOFA_A01:43 (t1 div t2) value_at(C,s) = (t1 value_at(C,s))div(t2 value_at(C,s)); theorem :: AOFA_A01:44 (t1 mod t2) value_at(C,s) = (t1 value_at(C,s)) mod (t2 value_at(C,s)); theorem :: AOFA_A01:45 leq(t1,t2) value_at(C,s) = leq(t1 value_at(C,s), t2 value_at(C,s)); theorem :: AOFA_A01:46 \trueT value_at(C,u) = TRUE; theorem :: AOFA_A01:47 for t being Element of T, the bool-sort of S holds \nott value_at(C,u) = \not(t value_at(C,u)); theorem :: AOFA_A01:48 for a being boolean object for t being Element of T, the bool-sort of S holds \nott value_at(C,u) = 'not' a iff t value_at(C,u) = a; theorem :: AOFA_A01:49 (\falseT) value_at(C,u) = FALSE; theorem :: AOFA_A01:50 for t1,t2 being Element of T, the bool-sort of S holds t1\andt2 value_at(C,u) = (t1 value_at(C,u))\and(t2 value_at(C,u)); theorem :: AOFA_A01:51 \0(T,I) value_at(C,u) = 0; theorem :: AOFA_A01:52 \1(T,I) value_at(C,u) = 1; theorem :: AOFA_A01:53 (-t) value_at(C,u) = -(t value_at(C,u)); theorem :: AOFA_A01:54 (t1+t2) value_at(C,u) = (t1 value_at(C,u))+(t2 value_at(C,u)); theorem :: AOFA_A01:55 \2(T,I) value_at (C,u) = 2; theorem :: AOFA_A01:56 (t1-t2) value_at(C,u) = (t1 value_at(C,u))-(t2 value_at(C,u)); theorem :: AOFA_A01:57 (t1*t2) value_at(C,u) = (t1 value_at(C,u))*(t2 value_at(C,u)); theorem :: AOFA_A01:58 (t1 div t2) value_at(C,u) = (t1 value_at(C,u))div(t2 value_at(C,u)); theorem :: AOFA_A01:59 (t1 mod t2) value_at(C,u) = (t1 value_at(C,u)) mod (t2 value_at(C,u)); theorem :: AOFA_A01:60 leq(t1,t2) value_at(C,u) = leq(t1 value_at(C,u), t2 value_at(C,u)); theorem :: AOFA_A01:61 for a being SortSymbol of S for x being Element of (the generators of G).a holds @x value_at(C,s) = s.a.x; theorem :: AOFA_A01:62 for a being SortSymbol of S for x being pure Element of (the generators of G).a for u being ManySortedFunction of FreeGen T, the Sorts of C holds @x value_at(C,u) = u.a.x; theorem :: AOFA_A01:63 for i,j being Integer, a,b being Element of C,I st a = i & b = j holds a-b = i-j; theorem :: AOFA_A01:64 for i,j being Integer, a,b being Element of C,I st a = i & b = j & j <> 0 holds a mod b = i mod j; theorem :: AOFA_A01:65 G is C-supported & f in C-Execution(A,b,\falseC) implies for a being SortSymbol of S, x being pure Element of (the generators of G).a for t being Element of T,a holds f.(s,x:=(t,A)).a.x = t value_at(C,s) & (for z being pure Element of (the generators of G).a st z <> x holds f.(s, x:=(t,A)).a.z = s.a.z) & for b being SortSymbol of S st a <> b holds (for z being pure Element of (the generators of G).b holds f.(s, x:=(t,A)).b.z = s.b.z); theorem :: AOFA_A01:66 G is C-supported & f in C-Execution(A,b,\falseC) implies (t1 value_at(C,s) < t2 value_at(C,s) iff f.(s, b gt(t2,t1,A)) in (\falseC)-States(the generators of G,b)) & (t1 value_at(C,s) <= t2 value_at(C,s) iff f.(s, b leq(t1,t2,A)) in (\falseC)-States(the generators of G,b)) & (for x holds f.(s, b gt(t1,t2,A)).I.x = s.I.x & f.(s, b leq(t1,t2,A)).I.x = s.I.x) & for c being pure Element of (the generators of G).the bool-sort of S st c <> b holds f.(s, b gt(t1,t2,A)).(the bool-sort of S).c = s.(the bool-sort of S).c & f.(s, b leq(t1,t2,A)).(the bool-sort of S).c = s.(the bool-sort of S).c; registration let i,j be Real; let a,b be boolean object; cluster IFGT(i,j,a,b) -> boolean; end; theorem :: AOFA_A01:67 G is C-supported & f in C-Execution(A,b,\falseC) implies f.(s, t is_odd(b,A)).(the bool-sort of S).b = (t value_at(C,s)) mod 2 & f.(s, t is_even(b,A)).(the bool-sort of S).b = ((t value_at(C,s))+1) mod 2 & for z holds f.(s, t is_odd(b,A)).I.z = s.I.z & f.(s, t is_even(b,A)).I.z = s.I.z; definition let S,X,T,G,A; attr A is elementary means :: AOFA_A01:def 13 rng the assignments of A c= ElementaryInstructions A; end; theorem :: AOFA_A01:68 A is elementary implies for a being SortSymbol of S for x being Element of (the generators of G).a for t being Element of T,a holds x:=(t,A) in ElementaryInstructions A; registration let S,X,T,G; cluster elementary for strict IfWhileAlgebra of the generators of G; end; registration let S,X,T,G; let A be elementary IfWhileAlgebra of the generators of G; let a be SortSymbol of S; let x be Element of (the generators of G).a; let t be Element of T,a; cluster x:=(t,A) -> absolutely-terminating; end; theorem :: AOFA_A01:69 for A being elementary IfWhileAlgebra of the generators of G for f being ExecutionFunction of A, C-States(the generators of G), (\falseC)-States(the generators of G,b) holds G is C-supported & f in C-Execution(A,b,\falseC) & (ex d being Function st d.x = 1 & d.y = 2 & d.m = 3) implies y:=(\1(T,I),A)\; while(b gt(@m, \0(T,I), A), if-then(@m is_odd(b,A), y:=(@y*@x,A))\; m:=(@m div \2(T,I),A)\; x:=(@x*@x,A)) is_terminating_wrt f, {s: s.I.m >= 0}; theorem :: AOFA_A01:70 G is C-supported & (ex d being Function st d.b = 0 & d.x = 1 & d.y = 2 & d.m = 3) implies for s being Element of C-States(the generators of G) for n being Nat st n = s.I.m holds f in C-Execution(A,b,\falseC) implies f.(s, y:=(\1(T,I),A)\; while(b gt(@m, \0(T,I), A), if-then(@m is_odd(b,A), y:=(@y*@x,A))\; m:=(@m div \2(T,I),A)\; x:=(@x*@x,A)) ).I.y = (s.I.x)|^n; begin :: Calculation of maximum registration let X be non empty set; let f be FinSequence of X^omega; let x be Nat; cluster f.x -> Sequence-like finite Function-like Relation-like; end; registration let X be non empty set; cluster -> Function-yielding for FinSequence of X^omega; end; registration let i be Nat; let f be i-based finite array; let a,x be set; cluster f+*(a,x) -> i-based finite segmental; end; registration let X be non empty set; let f be X-valued Function; let a be set; let x be Element of X; cluster f+*(a,x) -> X-valued; end; scheme :: AOFA_A01:sch 1 Sch1{X()->non empty set, j()->Nat, B()->set, F(set,set,set)->set, A(set)->set}: ex f being FinSequence of X()^omega st len f = j() & (f.1 = B() or j() = 0) & for i being Nat st 1 <= i & i < j() holds f.(i+1) = F(f.i,i,A(i)) provided for a being 0-based finite array of X() for i being Nat st 1 <= i & i < j() for x being Element of X() holds F(a,i,x) is 0-based finite array of X() and B() is 0-based finite array of X() and for i being Nat st i < j() holds A(i) in X(); theorem :: AOFA_A01:71 for S being (11,1,1)-array non empty non void BoolSignature for J,L being set, K being SortSymbol of S st (the connectives of S).11 is_of_type <*J,L*>, K holds J = the_array_sort_of S & for I being integer SortSymbol of S holds the_array_sort_of S <> I; theorem :: AOFA_A01:72 for S being 1-1-connectives (4,1) integer (11,1,1)-array 11 array-correct bool-correct non empty non void BoolSignature for I being integer SortSymbol of S for A being (4,1) integer (11,1,1)-array bool-correct non-empty MSAlgebra over S for a,b being Element of A,I st a = 0 holds init.array(a,b) = {}; theorem :: AOFA_A01:73 for S being (11,1,1)-array 11 array-correct bool-correct non empty non void BoolSignature for I being integer SortSymbol of S holds the_array_sort_of S <> I & (the connectives of S).11 is_of_type <*the_array_sort_of S,I*>, I & (the connectives of S).(11+1) is_of_type <*the_array_sort_of S,I,I*>, the_array_sort_of S & (the connectives of S).(11+2) is_of_type <*the_array_sort_of S*>, I & (the connectives of S).(11+3) is_of_type <*I,I*>, the_array_sort_of S; theorem :: AOFA_A01:74 for S being 1-1-connectives (11,1,1)-array 11 array-correct (4,1) integer bool-correct non empty non void BoolSignature for I being integer SortSymbol of S for A being (11,1,1)-array (4,1) integer bool-correct non-empty MSAlgebra over S holds (the Sorts of A).the_array_sort_of S = INT^omega & (for i,j being Element of A,I st i is non negative Integer holds init.array(i,j) = Segm(i)-->j) & for a being Element of (the Sorts of A).the_array_sort_of S holds length(a,I) = card a & for i being Element of A,I for f being Function st f = a & i in dom f holds a.(i) = f.i & for x being Element of A,I holds (a,i)<-x = f+*(i,x); registration let a be 0-based finite array; cluster len-a -> finite; end; registration let S be 1-1-connectives (4,1) integer (11,1,1)-array 11 array-correct bool-correct non empty non void BoolSignature; let A be (11,1,1)-array (4,1) integer bool-correct non-empty MSAlgebra over S; cluster -> (11,1,1)-array for non-empty MSSubAlgebra of A; end; definition let S be 1-1-connectives (4,1) integer (11,1,1)-array 11 array-correct bool-correct non empty non void BoolSignature; let A be non-empty MSAlgebra over S; attr A is integer-array means :: AOFA_A01:def 14 ex C being image of A st C is (4,1) integer (11,1,1)-array bool-correct MSAlgebra over S; end; registration let S be 1-1-connectives (4,1) integer (11,1,1)-array 11 array-correct bool-correct non empty non void BoolSignature; let X be non-empty ManySortedSet of the carrier of S; cluster Free(S,X) -> integer-array for non-empty MSAlgebra over S; end; registration let S be 1-1-connectives (4,1) integer (11,1,1)-array 11 array-correct bool-correct non empty non void BoolSignature; cluster integer-array -> integer for non-empty MSAlgebra over S; let X be non-empty ManySortedSet of the carrier of S; cluster vf-free integer-array for all_vars_including inheriting_operations free_in_itself (X,S)-terms non-empty strict VarMSAlgebra over S; end; registration let S be 1-1-connectives (4,1) integer (11,1,1)-array 11 array-correct bool-correct non empty non void BoolSignature; cluster integer-array for non-empty MSAlgebra over S; end; registration let S be 1-1-connectives (4,1) integer (11,1,1)-array 11 array-correct bool-correct non empty non void BoolSignature; let A be integer-array non-empty MSAlgebra over S; cluster (4,1) integer (11,1,1)-array for bool-correct image of A; end; reserve S for 1-1-connectives (4,1) integer (11,1,1)-array 11 array-correct bool-correct non empty non void BoolSignature, X for non-empty ManySortedSet of the carrier of S, T for vf-free all_vars_including inheriting_operations free_in_itself (X,S)-terms integer-array non-empty VarMSAlgebra over S, C for (11,1,1)-array (4,1) integer bool-correct non-empty image of T, G for basic GeneratorSystem over S,X,T, A for IfWhileAlgebra of the generators of G, I for integer SortSymbol of S, x,y,m,i for pure (Element of (the generators of G).I), M,N for pure (Element of (the generators of G).the_array_sort_of S), b for pure (Element of (the generators of G).the bool-sort of S), s,s1 for (Element of C-States(the generators of G)); registration let S; let A be (11,1,1)-array bool-correct non-empty MSAlgebra over S; cluster -> Relation-like Function-like for Element of (the Sorts of A).the_array_sort_of S; end; registration let S; let A be (11,1,1)-array bool-correct non-empty MSAlgebra over S; cluster -> finite Sequence-like for Element of (the Sorts of A).the_array_sort_of S; end; theorem :: AOFA_A01:75 for o being OperSymbol of S st o = In((the connectives of S).11, the carrier' of S) holds the_arity_of o = <*the_array_sort_of S,I*> & the_result_sort_of o = I; theorem :: AOFA_A01:76 for o being OperSymbol of S st o = In((the connectives of S).12, the carrier' of S) holds the_arity_of o = <*the_array_sort_of S,I,I*> & the_result_sort_of o = the_array_sort_of S; theorem :: AOFA_A01:77 for o being OperSymbol of S st o = In((the connectives of S).13, the carrier' of S) holds the_arity_of o = <*the_array_sort_of S*> & the_result_sort_of o = I; theorem :: AOFA_A01:78 for o being OperSymbol of S st o = In((the connectives of S).14, the carrier' of S) holds the_arity_of o = <*I,I*> & the_result_sort_of o = the_array_sort_of S; theorem :: AOFA_A01:79 for t being Element of T, the_array_sort_of S holds for t1 being Element of T, I holds t.(t1) value_at(C,s) = (t value_at(C,s)).(t1 value_at(C,s)); theorem :: AOFA_A01:80 for t being Element of T, the_array_sort_of S holds for t1,t2 being Element of T, I holds (t,t1)<-t2 value_at(C,s) = (t value_at(C,s), t1 value_at(C,s))<-(t2 value_at(C,s)); theorem :: AOFA_A01:81 for t being Element of T, the_array_sort_of S holds length(t,I) value_at(C,s) = length(t value_at(C,s), I); theorem :: AOFA_A01:82 for t1,t2 being Element of T, I holds init.array(t1,t2) value_at(C,s) = init.array(t1 value_at(C,s), t2 value_at(C,s)); reserve u for ManySortedFunction of FreeGen T, the Sorts of C; theorem :: AOFA_A01:83 for t being Element of T, the_array_sort_of S holds for t1 being Element of T, I holds t.(t1) value_at(C,u) = (t value_at(C,u)).(t1 value_at(C,u)); theorem :: AOFA_A01:84 for t being Element of T, the_array_sort_of S holds for t1,t2 being Element of T, I holds (t,t1)<-t2 value_at(C,u) = (t value_at(C,u), t1 value_at(C,u))<-(t2 value_at(C,u)); theorem :: AOFA_A01:85 for t being Element of T, the_array_sort_of S holds length(t,I) value_at(C,u) = length(t value_at(C,u), I); theorem :: AOFA_A01:86 for t1,t2 being Element of T, I holds init.array(t1,t2) value_at(C,u) = init.array(t1 value_at(C,u), t2 value_at(C,u)); definition let S,X,T,I; let i be Integer; func ^(i,T,I) -> Element of T,I means :: AOFA_A01:def 15 ex f being Function of INT, (the Sorts of T).I st it = f.i & f.0 = \0(T,I) & for j being Nat, t being Element of T,I st f.j = t holds f.(j+1) = t+\1(T,I) & f.(-(j+1)) = -(t+\1(T,I)); end; theorem :: AOFA_A01:87 ^(0,T,I) = \0(T,I); theorem :: AOFA_A01:88 for n being Nat holds ^(n+1,T,I) = ^(n,T,I)+\1(T,I) & ^(-(n+1),T,I) = - ^(n+1,T,I); theorem :: AOFA_A01:89 ^(1,T,I) = \0(T,I)+\1(T,I); theorem :: AOFA_A01:90 for i being Integer holds ^(i,T,I) value_at(C,s) = i; definition let S,X,T,G,I,M; let i be Integer; func M.(i,I) -> Element of T,I equals :: AOFA_A01:def 16 @M.(^(i,T,I)); end; registration let S,X,T,G,C,s,M; cluster s.(the_array_sort_of S).M -> Function-like Relation-like; end; registration let S,X,T,G,C,s,M; cluster s.(the_array_sort_of S).M -> finite Sequence-like INT-valued; end; registration let S,X,T,G,C,s,M; cluster rng (s.(the_array_sort_of S).M) -> finite integer-membered; end; theorem :: AOFA_A01:91 for j being Integer st j in dom (s.(the_array_sort_of S).M) & M.(j,I) in (the generators of G).I holds s.(the_array_sort_of S).M.j = s.I.(M.(j,I)); theorem :: AOFA_A01:92 for j being Integer st j in dom (s.(the_array_sort_of S).M) & @M.(@i) in (the generators of G).I & j = @i value_at(C,s) holds s.(the_array_sort_of S).M.(@i value_at(C,s)) = s.I.(@M.(@i)); registration let X be non empty set; cluster X^omega -> infinite; end; theorem :: AOFA_A01:93 for f being ExecutionFunction of A, C-States(the generators of G), (\falseC)-States(the generators of G, b) st f in C-Execution(A,b,\falseC) & G is C-supported & i <> m & s.(the_array_sort_of S).M <> {} holds for n being Nat st f.(s, m:=(\0(T,I),A)\; for-do(i:=(\1(T,I),A), b gt(length(@M,I),@i,A), i:=(@i+\1(T,I),A), if-then(b gt(@M.(@i), @M.(@m), A), m:=(@i,A)))).I.m = n for X being non empty finite integer-membered set st X = rng (s.(the_array_sort_of S).M) holds (M.(n,I)) value_at(C,s) = max X; theorem :: AOFA_A01:94 for A being elementary IfWhileAlgebra of the generators of G for f being ExecutionFunction of A, C-States(the generators of G), (\falseC)-States(the generators of G,b) st f in C-Execution(A,b,\falseC) & G is C-supported for t0,t1 being Element of T,I for J being Algorithm of A for P being set st P is_invariant_wrt i:=(t0,A),f & P is_invariant_wrt b gt(t1,@i,A),f & P is_invariant_wrt i:=(@i+\1(T,I),A),f & P is_invariant_wrt J,f & J is_terminating_wrt f,P & for s holds f.(s,J).I.i = s.I.i & f.(s,b gt(t1,@i,A)).I.i = s.I.i & t1 value_at(C,f.(s, b gt(t1,@i,A))) = t1 value_at(C,s) & t1 value_at(C,f.(s, J\;i:=(@i+\1(T,I),A))) = t1 value_at(C,s) holds for-do(i:=(t0,A),b gt(t1,@i,A),i:=(@i+\1(T,I),A), J) is_terminating_wrt f, P; theorem :: AOFA_A01:95 for A being elementary IfWhileAlgebra of the generators of G for f being ExecutionFunction of A, C-States(the generators of G), (\falseC)-States(the generators of G,b) holds f in C-Execution(A,b,\falseC) & G is C-supported & i <> m implies m:=(\0(T,I),A)\; for-do(i:=(\1(T,I),A), b gt(length(@M,I),@i,A), i:=(@i+\1(T,I),A), if-then(b gt(@M.(@i), @M.(@m), A), m:=(@i,A))) is_terminating_wrt f, {s: s.(the_array_sort_of S).M <> {}}; begin :: Sorting by exchanging reserve i1,i2 for pure Element of (the generators of G).I; definition let S,X,T,G; attr G is integer-array means :: AOFA_A01:def 17 for I holds the set of all @M.t where t is Element of T,I c= (the generators of G).I & for M for t being Element of T,I for g being Element of G,I st g = @M.t ex x st x nin (vf t).I & supp-var g = x & (supp-term g).(the_array_sort_of S).M = (@M,t)<-@x & for s being SortSymbol of S for y st y in (vf g).s & (s = the_array_sort_of S implies y <> M) holds (supp-term g).s.y = y; end; theorem :: AOFA_A01:96 G is integer-array implies for t being Element of T,I holds @M.t in (the generators of G).I; definition func (#INT,<=#) -> strict real non empty Poset equals :: AOFA_A01:def 18 RealPoset INT; end; definition let S,X,T,G; let A be elementary IfWhileAlgebra of the generators of G; let a be SortSymbol of S; let t1,t2 be Element of T,a such that t1 in (the generators of G).a; func t1:=(t2,A) -> absolutely-terminating Algorithm of A equals :: AOFA_A01:def 19 (the assignments of A).[t1,t2]; end; theorem :: AOFA_A01:97 for X being countable non-empty ManySortedSet of the carrier of S for T being vf-free all_vars_including inheriting_operations free_in_itself (X,S)-terms integer-array non-empty VarMSAlgebra over S for G being basic GeneratorSystem over S,X,T for M being pure Element of (the generators of G).the_array_sort_of S for i,x being pure Element of (the generators of G).I holds @M.@i <> x; registration let S be non empty non void ManySortedSign; let A be disjoint_valued MSAlgebra over S; cluster the Sorts of A -> disjoint_valued; end; definition let S,X; let T be all_vars_including inheriting_operations free_in_itself (X,S)-terms MSAlgebra over S; attr T is array-degenerated means :: AOFA_A01:def 20 ex I st ex M being Element of (FreeGen T).the_array_sort_of S st ex t being Element of T,I st @M.t <> Sym(In((the connectives of S).11, the carrier' of S),X)-tree<*M,t*>; end; registration let S,X; cluster Free(S,X) -> non array-degenerated; end; registration let S,X; cluster non array-degenerated for all_vars_including inheriting_operations free_in_itself (X,S)-terms MSAlgebra over S; end; theorem :: AOFA_A01:98 T is non array-degenerated implies vf (@M.@i) = (I-singleton i) (\/) ((the_array_sort_of S)-singleton M); theorem :: AOFA_A01:99 for A being elementary IfWhileAlgebra of the generators of G for f being ExecutionFunction of A, C-States(the generators of G), (\falseC)-States(the generators of G, b) st G is integer-array C-supported & f in C-Execution(A,b,\falseC) & X is countable & T is non array-degenerated for t being Element of T,I holds f.(s,@M.@i:=(t,A)) = f.(s,M:=((@M,@i)<-t,A)); registration let S,X,T,G,C,s,b; cluster s.(the bool-sort of S).b -> boolean; end; theorem :: AOFA_A01:100 for A being elementary IfWhileAlgebra of the generators of G for f being ExecutionFunction of A, C-States(the generators of G), (\falseC)-States(the generators of G, b) st G is integer-array C-supported & f in C-Execution(A,b,\falseC) & T is non array-degenerated & X is countable for J being Algorithm of A st for s holds f.(s,J).(the_array_sort_of S).M = s.(the_array_sort_of S).M & for D being array of (#INT,<=#) st D = s.(the_array_sort_of S).M holds (D <> {} implies f.(s,J).I.i1 in dom D & f.(s,J).I.i2 in dom D) & (inversions D <> {} implies [f.(s,J).I.i1,f.(s,J).I.i2] in inversions D) & (f.(s,J).(the bool-sort of S).b = TRUE iff inversions D <> {}) for D being 0-based finite array of (#INT,<=#) st D = s.(the_array_sort_of S).M & y <> i1 & y <> i2 holds f.(s,while(J, y:=(@M.@i1,A)\;@M.@i1:=(@M.@i2,A)\;@M.@i2:=(@y,A))). (the_array_sort_of S).M is ascending permutation of D & (J is absolutely-terminating implies while(J, y:=(@M.@i1,A)\;@M.@i1:=(@M.@i2,A)\;@M.@i2:=(@y,A)) is_terminating_wrt f, {s1: s1.(the_array_sort_of S).M <> {}});