:: Program Algebra over an Algebra :: by Grzegorz Bancerek :: :: Received August 27, 2012 :: Copyright (c) 2012-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies AOFA_A00, AOFA_000, PROB_2, UNIALG_1, FUNCT_1, RELAT_1, NAT_1, FUNCT_2, XBOOLE_0, MSUALG_1, FUNCOP_1, TREES_4, FINSET_1, MCART_1, SUBSET_1, ZF_MODEL, PBOOLE, INCPROJ, MSUALG_3, AOFA_I00, CARD_3, ZFMISC_1, MSAFREE, MEMBERED, MSATERM, STRUCT_0, PZFMISC1, GRAPHSP, TARSKI, MARGREL1, REALSET1, PRELAMB, COMPUT_1, CARD_1, PARTFUN1, FUNCT_7, FINSEQ_1, UNIALG_2, WELLORD1, XXREAL_0, XBOOLEAN, INT_1, NUMBERS, ARYTM_1, ARYTM_3, ORDINAL4, FUNCT_4, FINSEQ_2, ORDINAL1, MSUALG_2, FUNCT_6, FUNCT_5, FINSEQ_4, MSAFREE4, EXCHSORT, AFINSQ_1, RFINSEQ, MATRIX_7, ALGSTR_4; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, ORDINAL1, TREES_1, ENUMSET1, FUNCT_2, FUNCOP_1, FINSET_1, FINSEQ_2, FINSEQ_1, FINSEQ_4, RFINSEQ, FUNCT_4, BINOP_1, CARD_1, CARD_3, PROB_2, NUMBERS, MEMBERED, FUNCT_7, COMPUT_1, PBOOLE, PZFMISC1, MARGREL1, AFINSQ_1, XXREAL_0, XCMPLX_0, INT_1, FUNCT_5, FUNCT_6, TREES_2, TREES_4, STRUCT_0, MATRIX_7, BORSUK_7, UNIALG_1, UNIALG_2, FREEALG, MSUALG_1, MSUALG_2, MSUALG_3, MSUALG_6, CIRCCOMB, AUTALG_1, MSAFREE, MSAFREE1, MSATERM, MSAFREE3, AOFA_000, MSAFREE4, EXCHSORT; constructors PZFMISC1, AOFA_000, CATALG_1, PUA2MSS1, MSAFREE1, MSUALG_3, COMPUT_1, FINSEQ_4, MSAFREE4, AUTALG_1, EXCHSORT, AFINSQ_1, CIRCCOMB, RFINSEQ, MATRIX_7, BORSUK_7, BINOP_1; registrations RELAT_1, RELSET_1, FUNCT_1, FUNCOP_1, FINSEQ_1, UNIALG_1, STRUCT_0, PUA2MSS1, PBOOLE, MSUALG_1, INSTALG1, MSAFREE1, CARD_3, XBOOLE_0, AOFA_000, MSAFREE, ORDINAL1, INT_1, XREAL_0, FUNCT_4, FINSEQ_4, MARGREL1, SUBSET_1, FINSEQ_2, NUMBERS, CATALG_1, TREES_2, MSUALG_2, TREES_3, MSAFREE4, EXCHSORT, NAT_1, XTUPLE_0, FUNCT_7, AFINSQ_1, XBOOLEAN, MEMBERED, FOMODEL0, PRE_CIRC, PRE_POLY; requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL; begin :: Preliminary reserve i for Nat, x,y for set; reserve S for non empty non void ManySortedSign; reserve X for non-empty ManySortedSet of S; theorem :: AOFA_A00:1 for A,B being set for R being A-valued Relation holds R.:B c= A; definition let I be set; let f be ManySortedSet of I; let i be object; let x; redefine func f+*(i,x) -> ManySortedSet of I; end; registration let I be set; let f be non-empty ManySortedSet of I; let i be object; let x be non empty set; cluster f+*(i,x) -> non-empty; end; theorem :: AOFA_A00:2 for I being set for f,g being ManySortedSet of I st f c= g holds f# c= g#; theorem :: AOFA_A00:3 for I being non empty set for J being set for A,B being ManySortedSet of I st A c= B for f being Function of J,I holds A*f c= B*f; registration let f be Function-yielding Function; cluster Frege f -> Function-yielding; end; theorem :: AOFA_A00:4 for f,g being Function-yielding Function holds doms (f*g) = (doms f)*g; theorem :: AOFA_A00:5 for f,g being Function st g = f.x holds g.y = f..(x,y); definition let I be set; let i be Element of I; let x; func i-singleton(x) -> ManySortedSet of I equals :: AOFA_A00:def 1 (EmptyMS I)+*(i,{x}); end; theorem :: AOFA_A00:6 for I being non empty set for i,j being Element of I for x holds (i-singleton x).i = {x} & (i <> j implies (i-singleton x).j = {}) ; theorem :: AOFA_A00:7 for I being non empty set for i being Element of I for A being ManySortedSet of I for x st x in A.i holds i-singleton x is ManySortedSubset of A; definition let I be set; let A,B be ManySortedSet of I; let F be ManySortedFunction of A,B; let i be set such that i in I; let j be set such that j in A.i; let v be set such that v in B.i; func F+*(i,j,v) -> ManySortedFunction of A,B means :: AOFA_A00:def 2 it.i = F.i+*(j,v) & for s being set st s in I & s <> i holds it.s = F.s; end; ::$CD ::$CT 5 theorem :: AOFA_A00:13 for X being set, a1,a2,a3,a4,a5,a6 being object st a1 in X & a2 in X & a3 in X & a4 in X & a5 in X & a6 in X holds {a1,a2,a3,a4,a5,a6} c= X; theorem :: AOFA_A00:14 for X being set, a1,a2,a3,a4,a5,a6,a7,a8,a9 being object st a1 in X & a2 in X & a3 in X & a4 in X & a5 in X & a6 in X & a7 in X & a8 in X & a9 in X holds {a1,a2,a3,a4,a5,a6,a7,a8,a9} c= X; theorem :: AOFA_A00:15 for X being set, a1,a2,a3,a4,a5,a6,a7,a8,a9,a10 being object st a1 in X & a2 in X & a3 in X & a4 in X & a5 in X & a6 in X & a7 in X & a8 in X & a9 in X & a10 in X holds {a1,a2,a3,a4,a5,a6,a7,a8,a9,a10} c= X; theorem :: AOFA_A00:16 for a1,a2,a3,a4,a5,a6,a7,a8,a9 being object holds {a1}\/{a2,a3,a4,a5,a6,a7,a8,a9} = {a1,a2,a3,a4,a5,a6,a7,a8,a9}; theorem :: AOFA_A00:17 for a1,a2,a3,a4,a5,a6,a7,a8,a9,a10 being object holds {a1}\/{a2,a3,a4,a5,a6,a7,a8,a9,a10} = {a1,a2,a3,a4,a5,a6,a7,a8,a9,a10}; theorem :: AOFA_A00:18 for a1,a2,a3,a4,a5,a6,a7,a8,a9 being object holds {a1,a2,a3}\/{a4,a5,a6,a7,a8,a9} = {a1,a2,a3,a4,a5,a6,a7,a8,a9}; theorem :: AOFA_A00:19 for a1,a2,a3,a4 being object st a1 <> a2 & a1 <> a3 & a1 <> a4 & a2 <> a3 & a2 <> a4 & a3 <> a4 holds <*a1,a2,a3,a4*> is one-to-one; definition let a1,a2,a3,a4,a5,a6 be object; func <*a1,a2,a3,a4,a5,a6*> -> FinSequence equals :: AOFA_A00:def 4 <*a1,a2,a3,a4,a5*>^<*a6*>; end; definition let X be non empty set; let a1,a2,a3,a4,a5,a6 be Element of X; redefine func <*a1,a2,a3,a4,a5,a6*> -> FinSequence of X; end; registration let a1,a2,a3,a4,a5,a6 be object; cluster <*a1,a2,a3,a4,a5,a6*> -> 6-element; end; theorem :: AOFA_A00:20 for a1,a2,a3,a4,a5,a6 being object for f being FinSequence holds f = <*a1,a2,a3,a4,a5,a6*> iff len f = 6 & f.1 = a1 & f.2 = a2 & f.3 = a3 & f.4 = a4 & f.5 = a5 & f.6 = a6; theorem :: AOFA_A00:21 for a1,a2,a3,a4,a5,a6 being object holds rng <*a1,a2,a3,a4,a5,a6*> = {a1,a2,a3,a4,a5,a6}; definition let a1,a2,a3,a4,a5,a6,a7 be object; func <*a1,a2,a3,a4,a5,a6,a7*> -> FinSequence equals :: AOFA_A00:def 5 <*a1,a2,a3,a4,a5*>^<*a6,a7*>; end; definition let X be non empty set; let a1,a2,a3,a4,a5,a6,a7 be Element of X; redefine func <*a1,a2,a3,a4,a5,a6,a7*> -> FinSequence of X; end; registration let a1,a2,a3,a4,a5,a6,a7 be object; cluster <*a1,a2,a3,a4,a5,a6,a7*> -> 7-element; end; theorem :: AOFA_A00:22 for a1,a2,a3,a4,a5,a6,a7 being object for f being FinSequence holds f = <*a1,a2,a3,a4,a5,a6,a7*> iff len f = 7 & f.1 = a1 & f.2 = a2 & f.3 = a3 & f.4 = a4 & f.5 = a5 & f.6 = a6 & f.7 = a7; theorem :: AOFA_A00:23 for a1,a2,a3,a4,a5,a6,a7 being object holds rng <*a1,a2,a3,a4,a5,a6,a7*> = {a1,a2,a3,a4,a5,a6,a7}; definition let a1,a2,a3,a4,a5,a6,a7,a8 be object; func <*a1,a2,a3,a4,a5,a6,a7,a8*> -> FinSequence equals :: AOFA_A00:def 6 <*a1,a2,a3,a4,a5*>^<*a6,a7,a8*>; end; definition let X be non empty set; let a1,a2,a3,a4,a5,a6,a7,a8 be Element of X; redefine func <*a1,a2,a3,a4,a5,a6,a7,a8*> -> FinSequence of X; end; registration let a1,a2,a3,a4,a5,a6,a7,a8 be object; cluster <*a1,a2,a3,a4,a5,a6,a7,a8*> -> 8-element; end; theorem :: AOFA_A00:24 for a1,a2,a3,a4,a5,a6,a7,a8 being object for f being FinSequence holds f = <*a1,a2,a3,a4,a5,a6,a7,a8*> iff len f = 8 & f.1 = a1 & f.2 = a2 & f.3 = a3 & f.4 = a4 & f.5 = a5 & f.6 = a6 & f.7 = a7 & f.8 = a8; theorem :: AOFA_A00:25 for a1,a2,a3,a4,a5,a6,a7,a8 being object holds rng <*a1,a2,a3,a4,a5,a6,a7,a8*> = {a1,a2,a3,a4,a5,a6,a7,a8}; theorem :: AOFA_A00:26 for a1,a2,a3,a4,a5,a6,a7,a8,a9 being object holds rng(<*a1,a2,a3,a4,a5,a6,a7,a8*>^<*a9*>) = {a1,a2,a3,a4,a5,a6,a7,a8,a9}; theorem :: AOFA_A00:27 Seg 9 = {1,2,3,4,5,6,7,8,9}; theorem :: AOFA_A00:28 Seg 10 = {1,2,3,4,5,6,7,8,9,10}; theorem :: AOFA_A00:29 for a1,a2,a3,a4,a5,a6,a7,a8,a9 being object holds dom (<*a1,a2,a3,a4,a5,a6,a7,a8*>^<*a9*>) = Seg 9 & (<*a1,a2,a3,a4,a5,a6,a7,a8*>^<*a9*>).1 = a1 & (<*a1,a2,a3,a4,a5,a6,a7,a8*>^<*a9*>).2 = a2 & (<*a1,a2,a3,a4,a5,a6,a7,a8*>^<*a9*>).3 = a3 & (<*a1,a2,a3,a4,a5,a6,a7,a8*>^<*a9*>).4 = a4 & (<*a1,a2,a3,a4,a5,a6,a7,a8*>^<*a9*>).5 = a5 & (<*a1,a2,a3,a4,a5,a6,a7,a8*>^<*a9*>).6 = a6 & (<*a1,a2,a3,a4,a5,a6,a7,a8*>^<*a9*>).7 = a7 & (<*a1,a2,a3,a4,a5,a6,a7,a8*>^<*a9*>).8 = a8 & (<*a1,a2,a3,a4,a5,a6,a7,a8*>^<*a9*>).9 = a9; theorem :: AOFA_A00:30 for a1,a2,a3,a4,a5,a6,a7,a8,a9,a10 being object holds dom (<*a1,a2,a3,a4,a5,a6,a7,a8*>^<*a9,a10*>) = Seg 10 & (<*a1,a2,a3,a4,a5,a6,a7,a8*>^<*a9,a10*>).1 = a1 & (<*a1,a2,a3,a4,a5,a6,a7,a8*>^<*a9,a10*>).2 = a2 & (<*a1,a2,a3,a4,a5,a6,a7,a8*>^<*a9,a10*>).3 = a3 & (<*a1,a2,a3,a4,a5,a6,a7,a8*>^<*a9,a10*>).4 = a4 & (<*a1,a2,a3,a4,a5,a6,a7,a8*>^<*a9,a10*>).5 = a5 & (<*a1,a2,a3,a4,a5,a6,a7,a8*>^<*a9,a10*>).6 = a6 & (<*a1,a2,a3,a4,a5,a6,a7,a8*>^<*a9,a10*>).7 = a7 & (<*a1,a2,a3,a4,a5,a6,a7,a8*>^<*a9,a10*>).8 = a8 & (<*a1,a2,a3,a4,a5,a6,a7,a8*>^<*a9,a10*>).9 = a9 & (<*a1,a2,a3,a4,a5,a6,a7,a8*>^<*a9,a10*>).10 = a10; definition let I,J be set; let S be ManySortedSet of I; mode ManySortedMSSet of S,J -> ManySortedFunction of I means :: AOFA_A00:def 7 for i,j being set st i in I holds dom(it.i) = S.i & (j in S.i implies it.i.j is ManySortedSet of J); end; definition let I,J be set; let S1 be ManySortedSet of I; let S2 be ManySortedSet of J; mode ManySortedMSSet of S1,S2 -> ManySortedMSSet of S1,J means :: AOFA_A00:def 8 for i,a being set st i in I & a in S1.i holds it.i.a is ManySortedSubset of S2; end; registration let I be set; let X,Y be ManySortedSet of I; let f be ManySortedMSSet of X,Y; let x,y; cluster f.x.y -> Function-like Relation-like; end; definition let S be ManySortedSign; let o,a be set; let r be Element of S; pred o is_of_type a,r means :: AOFA_A00:def 9 (the Arity of S).o = a & (the ResultSort of S).o = r; end; theorem :: AOFA_A00:31 for S being non void non empty ManySortedSign for o being OperSymbol of S for r being SortSymbol of S st o is_of_type {}, r for A being MSAlgebra over S st (the Sorts of A).r <> {} holds Den(In(o, the carrier' of S), A).{} is Element of (the Sorts of A).r; theorem :: AOFA_A00:32 for S being non void non empty ManySortedSign for o,a being set for r being SortSymbol of S st o is_of_type <*a*>, r for A being MSAlgebra over S st (the Sorts of A).a <> {} & (the Sorts of A).r <> {} for x being Element of (the Sorts of A).a holds Den(In(o, the carrier' of S), A).<*x*> is Element of (the Sorts of A).r; theorem :: AOFA_A00:33 for S being non void non empty ManySortedSign for o,a,b being set for r being SortSymbol of S st o is_of_type <*a,b*>, r for A being MSAlgebra over S st (the Sorts of A).a <> {} & (the Sorts of A).b <> {} & (the Sorts of A).r <> {} for x being Element of (the Sorts of A).a for y being Element of (the Sorts of A).b holds Den(In(o, the carrier' of S), A).<*x,y*> is Element of (the Sorts of A).r; theorem :: AOFA_A00:34 for S being non void non empty ManySortedSign for o,a,b,c being set for r being SortSymbol of S st o is_of_type <*a,b,c*>, r for A being MSAlgebra over S st (the Sorts of A).a <> {} & (the Sorts of A).b <> {} & (the Sorts of A).c <> {} & (the Sorts of A).r <> {} for x being Element of (the Sorts of A).a for y being Element of (the Sorts of A).b for z being Element of (the Sorts of A).c holds Den(In(o, the carrier' of S), A).<*x,y,z*> is Element of (the Sorts of A).r; theorem :: AOFA_A00:35 for S1,S2 being ManySortedSign st the ManySortedSign of S1 = the ManySortedSign of S2 for o,a be set, r1 be Element of S1 for r2 being Element of S2 st r1 = r2 holds o is_of_type a,r1 implies o is_of_type a,r2; begin :: Free Variables definition let S be non empty non void ManySortedSign; struct (MSAlgebra over S) VarMSAlgebra over S (# Sorts -> ManySortedSet of the carrier of S, Charact -> ManySortedFunction of (the Sorts)# * the Arity of S, the Sorts * the ResultSort of S, free-vars -> ManySortedMSSet of the Sorts, the Sorts #); end; registration let S be non empty non void ManySortedSign; let U be non-empty ManySortedSet of the carrier of S; let C be ManySortedFunction of U# * the Arity of S, U * the ResultSort of S; let v be ManySortedMSSet of U,U; cluster VarMSAlgebra(#U, C, v#) -> non-empty; end; registration let S be non empty non void ManySortedSign; let X be non-empty ManySortedSet of the carrier of S; cluster (X,S)-terms for strict VarMSAlgebra over S; end; registration let S be non empty non void ManySortedSign; cluster non-empty disjoint_valued for VarMSAlgebra over S; let X be non-empty ManySortedSet of the carrier of S; cluster all_vars_including -> non-empty for (X,S)-terms VarMSAlgebra over S; end; definition let S be non empty non void ManySortedSign; let A be non-empty VarMSAlgebra over S; let a be SortSymbol of S; let t be Element of A,a; func vf t -> ManySortedSubset of the Sorts of A equals :: AOFA_A00:def 10 (the free-vars of A).a.t; end; definition let S be non empty non void ManySortedSign; let A be non-empty VarMSAlgebra over S; attr A is vf-correct means :: AOFA_A00:def 11 for o being OperSymbol of S for p being FinSequence st p in Args(o,A) for b being Element of A, the_result_sort_of o st b = Den(o,A).p for s being SortSymbol of S holds (vf b).s c= union {(vf a).s where s0 is SortSymbol of S, a is Element of A,s0: ex i being Nat st i in dom the_arity_of o & s0 = (the_arity_of o).i & a = p.i}; end; theorem :: AOFA_A00:36 for S being non empty non void ManySortedSign for A,B being MSAlgebra over S st the MSAlgebra of A = the MSAlgebra of B for G being MSSubset of A for H being MSSubset of B st G = H holds GenMSAlg G = GenMSAlg H; theorem :: AOFA_A00:37 for S being non empty non void ManySortedSign for A,B being MSAlgebra over S st the MSAlgebra of A = the MSAlgebra of B for G being GeneratorSet of A holds G is GeneratorSet of B; theorem :: AOFA_A00:38 for S being non empty non void ManySortedSign for A,B being non-empty MSAlgebra over S st the MSAlgebra of A = the MSAlgebra of B for G being GeneratorSet of A for H being GeneratorSet of B st G = H holds G is free implies H is free; registration let S be non empty non void ManySortedSign; let X be non-empty ManySortedSet of the carrier of S; cluster all_vars_including inheriting_operations free_in_itself for (X,S)-terms strict 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 A be non-empty (X,S)-terms VarMSAlgebra over S; attr A is vf-free means :: AOFA_A00:def 12 for s,r being SortSymbol of S for t being Element of A,s holds (vf t).r = {t|p where p is Element of dom t: ((t|p).{})`2 = r}; end; scheme :: AOFA_A00:sch 1 Scheme{I() -> non empty set, X,Y() -> non-empty ManySortedSet of I(), F(object,object,object) -> set}: ex f being ManySortedMSSet of X(),Y() st for s,r being Element of I() for t being Element of X().s holds f.s.t.r = F(s,r,t) provided for s,r being Element of I() for t being Element of X().s holds F(s,r,t) is Subset of Y().r; theorem :: AOFA_A00:39 for S being non empty non void ManySortedSign for X being non-empty ManySortedSet of the carrier of S for A being all_vars_including inheriting_operations free_in_itself (X,S)-terms MSAlgebra over S ex VF being ManySortedMSSet of the Sorts of A,the Sorts of A, B being all_vars_including inheriting_operations free_in_itself (X,S)-terms VarMSAlgebra over S st B = VarMSAlgebra(#the Sorts of A, the Charact of A, VF#) & B is vf-free; registration let S be non empty non void ManySortedSign; let X be non-empty ManySortedSet of the carrier of S; cluster strict vf-free for all_vars_including inheriting_operations free_in_itself (X,S)-terms VarMSAlgebra over S; end; theorem :: AOFA_A00:40 for S being non empty non void ManySortedSign for X being non-empty ManySortedSet of the carrier of S for A being vf-free all_vars_including inheriting_operations free_in_itself (X,S)-terms VarMSAlgebra over S for s being SortSymbol of S for t being Element of A,s holds vf t is ManySortedSubset of FreeGen X; theorem :: AOFA_A00:41 for S being non empty non void ManySortedSign for X being non-empty ManySortedSet of the carrier of S for A being vf-free all_vars_including (X,S)-terms VarMSAlgebra over S for s being SortSymbol of S for x being Element of A,s st x in (FreeGen X).s holds vf x = s-singleton(x); begin :: Algebra with undefined values definition let I be set; let S be ManySortedSet of I; mode ManySortedElement of S -> ManySortedSet of I means :: AOFA_A00:def 13 for i being set st i in I holds it.i is Element of S.i; end; definition let S be non empty non void ManySortedSign; struct (MSAlgebra over S) UndefMSAlgebra over S (# Sorts -> ManySortedSet of the carrier of S, Charact -> ManySortedFunction of (the Sorts)# * the Arity of S, the Sorts * the ResultSort of S, undefined-map -> ManySortedElement of the Sorts #); end; definition let S be non empty non void ManySortedSign; let A be UndefMSAlgebra over S; let s be SortSymbol of S; let a be Element of A,s; attr a is undefined means :: AOFA_A00:def 14 a = (the undefined-map of A).s; end; definition let S be non empty non void ManySortedSign; let A be UndefMSAlgebra over S; attr A is undef-consequent means :: AOFA_A00:def 15 for o being OperSymbol of S for p being FinSequence st p in Args(o, A) & ex i being Nat, s being SortSymbol of S,a being Element of A,s st i in dom the_arity_of o & s = (the_arity_of o).i & a = p.i & a is undefined for b being Element of A, the_result_sort_of o st b = Den(o,A).p holds b is undefined; end; definition let S be non empty non void ManySortedSign; let A be MSAlgebra over S; let B be UndefMSAlgebra over S; attr B is A-undef means :: AOFA_A00:def 16 B is undef-consequent & the undefined-map of B = the Sorts of A & (for s being SortSymbol of S holds (the Sorts of B).s = succ ((the Sorts of A).s)) & for o being OperSymbol of S, a being Element of Args(o,A) st Args(o,A) <> {} holds Den(o,B).a <> Den(o,A).a implies Den(o,B).a = (the undefined-map of B).the_result_sort_of o; end; registration let S be non empty ManySortedSign; let A be MSAlgebra over S; cluster the Charact of A -> Function-yielding; end; registration let S be non empty non void ManySortedSign; let A be non-empty MSAlgebra over S; cluster A-undef -> undef-consequent for UndefMSAlgebra over S; cluster A-undef non-empty for strict UndefMSAlgebra over S; end; begin :: Program algebra definition let J be non empty non void ManySortedSign; let T be MSAlgebra over J; let X be GeneratorSet of T; struct (UAStr) ProgramAlgStr over J,T,X(# carrier -> set, charact -> PFuncFinSequence of the carrier, assignments -> Function of Union [|X, the Sorts of T|], the carrier #); end; definition let J be non empty non void ManySortedSign; let T be MSAlgebra over J; let X be GeneratorSet of T; let A be ProgramAlgStr over J,T,X; attr A is disjoint_valued means :: AOFA_A00:def 17 the Sorts of T is disjoint_valued & the assignments of A is one-to-one; end; registration let J be non empty non void ManySortedSign; let T be MSAlgebra over J; let X be GeneratorSet of T; cluster partial quasi_total non-empty for strict ProgramAlgStr over J,T,X; end; registration let J be non empty non void ManySortedSign; let T be MSAlgebra over J; let X be GeneratorSet of T; cluster with_empty-instruction with_catenation with_if-instruction with_while-instruction for partial quasi_total non-empty non empty strict ProgramAlgStr over J,T,X; end; theorem :: AOFA_A00:42 for U1,U2 be preIfWhileAlgebra st the UAStr of U1 = the UAStr of U2 holds EmptyIns U1 = EmptyIns U2 & for I1,J1 being Element of U1 for I2,J2 being Element of U2 st I1 = I2 & J1 = J2 holds I1\;J1 = I2\;J2 & while(I1,J1) = while(I2,J2) & for C1 being Element of U1 for C2 being Element of U2 st C1 = C2 holds if-then-else(C1,I1,J1) = if-then-else(C2,I2,J2); theorem :: AOFA_A00:43 for U1,U2 be preIfWhileAlgebra st the UAStr of U1 = the UAStr of U2 holds ElementaryInstructions U1 = ElementaryInstructions U2; theorem :: AOFA_A00:44 for U1,U2 being Universal_Algebra for S1 being Subset of U1, S2 being Subset of U2 st S1 = S2 for o1 being operation of U1, o2 being operation of U2 st o1 = o2 holds S1 is_closed_on o1 implies S2 is_closed_on o2; theorem :: AOFA_A00:45 for U1,U2 being Universal_Algebra st the UAStr of U1 = the UAStr of U2 for S1 being Subset of U1, S2 being Subset of U2 st S1 = S2 holds S1 is opers_closed implies S2 is opers_closed; theorem :: AOFA_A00:46 for U1,U2 being Universal_Algebra st the UAStr of U1 = the UAStr of U2 for G being GeneratorSet of U1 holds G is GeneratorSet of U2; theorem :: AOFA_A00:47 for U1,U2 be Universal_Algebra st the UAStr of U1 = the UAStr of U2 holds signature U1 = signature U2; registration let J be non empty non void ManySortedSign; let T be MSAlgebra over J; let X be GeneratorSet of T; cluster non degenerated well_founded ECIW-strict infinite for with_empty-instruction with_catenation with_if-instruction with_while-instruction partial quasi_total non-empty non empty strict ProgramAlgStr over J,T,X; end; definition let J be non empty non void ManySortedSign; let T be MSAlgebra over J; let X be GeneratorSet of T; mode preIfWhileAlgebra of X is with_empty-instruction with_catenation with_if-instruction with_while-instruction partial quasi_total non-empty non empty ProgramAlgStr over J,T,X; end; definition let J be non empty non void ManySortedSign; let T be MSAlgebra over J; let X be GeneratorSet of T; mode IfWhileAlgebra of X is non degenerated well_founded ECIW-strict preIfWhileAlgebra of X; end; definition let J be non empty non void ManySortedSign; let T be non-empty MSAlgebra over J; let X be non-empty GeneratorSet of T; let A be non empty ProgramAlgStr over J,T,X; let a be SortSymbol of J; let x be Element of X.a; let t be Element of T,a; func x:=(t,A) -> Algorithm of A equals :: AOFA_A00:def 18 (the assignments of A).[x,t]; end; registration let S be set; let T be disjoint_valued non-empty ManySortedSet of S; cluster non-empty for ManySortedSubset of T; end; definition let J be non void non empty ManySortedSign; let T,C be non-empty MSAlgebra over J; let X be non-empty GeneratorSet of T; func C-States(X) -> Subset of MSFuncs(X, the Sorts of C) means :: AOFA_A00:def 19 for s being ManySortedFunction of X, the Sorts of C holds s in it iff ex f being ManySortedFunction of T,C st f is_homomorphism T,C & s = f||X; end; registration let J be non void non empty ManySortedSign; let T be non-empty MSAlgebra over J; let C be non-empty image of T; let X be non-empty GeneratorSet of T; cluster C-States(X) -> non empty; end; theorem :: AOFA_A00:48 for B being non void non empty ManySortedSign for T,C being non-empty MSAlgebra over B for X being non-empty GeneratorSet of T for g being set st g in C-States(X) holds g is ManySortedFunction of X, the Sorts of C; registration let B be non void non empty ManySortedSign; let T,C be non-empty MSAlgebra over B; let X be non-empty GeneratorSet of T; cluster -> Relation-like Function-like for Element of C-States(X); end; registration let B be non void non empty ManySortedSign; let T,C be non-empty MSAlgebra over B; let X be non-empty GeneratorSet of T; cluster -> Function-yielding the carrier of B-defined for Element of (C)-States(X); end; registration let B be non void non empty ManySortedSign; let T be non-empty MSAlgebra over B; let C be non-empty image of T; let X be non-empty GeneratorSet of T; cluster -> total for Element of (C)-States(X); end; definition let B be non void non empty ManySortedSign; let T be non-empty MSAlgebra over B; let C be non-empty MSAlgebra over B; let X be non-empty GeneratorSet of T; let a be SortSymbol of B; let x be Element of X.a; let f be Element of C,a; func f-States(X,x) -> Subset of (C)-States(X) means :: AOFA_A00:def 20 for s being ManySortedFunction of X, the Sorts of C holds s in it iff s in (C)-States(X) & s.a.x <> f; end; registration let B be non void non empty ManySortedSign; let T be free non-empty MSAlgebra over B; let C be non-empty MSAlgebra over B; let X be non-empty GeneratorSet of T; cluster C-States(X) -> non empty; end; registration let S be non empty non void ManySortedSign; let A be non-empty MSAlgebra over S; let o be OperSymbol of S; cluster -> Function-like Relation-like for Element of Args(o,A); end; registration let B be non void non empty ManySortedSign; let X be non-empty ManySortedSet of the carrier of B; let T be (X,B)-terms non-empty MSAlgebra over B; let C be non-empty image of T; let G be non-empty GeneratorSet of T; cluster C-States(G) -> non empty; end; definition let B be non void non empty ManySortedSign; let X be non-empty ManySortedSet of the carrier of B; let T be (X,B)-terms non-empty MSAlgebra over B; let C be non-empty image of T; let a be SortSymbol of B; let t be Element of T, a; let s be Function-yielding Function; given h being ManySortedFunction of T,C, Q being GeneratorSet of T such that h is_homomorphism T,C & Q = doms s & s = h||Q; func t value_at(C, s) -> Element of C, a means :: AOFA_A00:def 21 ex f being ManySortedFunction of T,C, Q being GeneratorSet of T st f is_homomorphism T,C & Q = doms s & s = f||Q & it = f.a.t; end; begin :: Generator system definition let S,X; let T be all_vars_including inheriting_operations free_in_itself (X,S)-terms MSAlgebra over S; struct GeneratorSystem over S,X,T(# generators -> non-empty GeneratorSet of T, supported-var -> (ManySortedFunction of the generators, FreeGen X), supported-term -> ManySortedMSSet of the generators, the carrier of S #); end; definition let S,X; 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 s be SortSymbol of S; mode Element of G,s -> Element of T,s means :: AOFA_A00:def 22 it in (the generators of G).s; end; definition let S,X; 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 s be SortSymbol of S; func G.s -> Component of the generators of G equals :: AOFA_A00:def 23 (the generators of G).s; let g be Element of G,s; func supp-var g -> Element of (FreeGen X).s equals :: AOFA_A00:def 24 (the supported-var of G).s.g; end; definition let S,X; let T be all_vars_including inheriting_operations free_in_itself (X,S)-terms VarMSAlgebra over S; let G be GeneratorSystem over S,X,T; let s be SortSymbol of S; let g be Element of G,s; assume (the supported-term of G).s.g is ManySortedFunction of vf g, the Sorts of T; func supp-term g -> ManySortedFunction of vf g, the Sorts of T equals :: AOFA_A00:def 25 (the supported-term of G).s.g; end; definition let S be non void non empty 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 VarMSAlgebra over S; let C be non-empty image of T; let G be GeneratorSystem over S,X,T; attr G is C-supported means :: AOFA_A00:def 26 FreeGen X is ManySortedSubset of the generators of G & for s being SortSymbol of S holds dom ((the supported-term of G).s) = G.s & for t being Element of G,s holds (the supported-term of G).s.t is ManySortedFunction of vf t, the Sorts of T & (t in (FreeGen X).s implies supp-term t = id (s-singleton(t)) & supp-var t = t) & (for v being Element of C-States the generators of G st v.s.(supp-var t) = v.s.t for r being SortSymbol of S for x being Element of (FreeGen X).r for q being Element of (the Sorts of T).r st x in (vf t).r & q = (supp-term t).r.x holds v.r.x = q value_at(C, v)) & (t nin (FreeGen X).s implies for H being ManySortedSubset of the generators of G st H = FreeGen X for v being Element of C, s for f being ManySortedFunction of the generators of G, the Sorts of C st f in C-States the generators of G for u being ManySortedFunction of FreeGen X, the Sorts of C st for a being SortSymbol of S for z being Element of (FreeGen X).a st z in (vf t).a holds for q being Element of T,a st q = (supp-term t).a.z holds u.a.z = q value_at(C, (f||H)+*(s,supp-var t,v)) for H being ManySortedSubset of the Sorts of T st H = FreeGen X for h being ManySortedFunction of T,C st h is_homomorphism T,C & h||H = u holds v = h.s.t); end; definition let S; let X; let A be vf-free all_vars_including inheriting_operations free_in_itself (X,S)-terms VarMSAlgebra over S; let C be non-empty image of A; let G be GeneratorSystem over S,X,A such that G is C-supported; let s be Element of C-States the generators of G; let r be SortSymbol of S; let v be Element of C,r; let t be Element of G,r; func succ(s,t,v) -> Element of C-States the generators of G means :: AOFA_A00:def 27 it.r.t = v & for p being SortSymbol of S for x being Element of (FreeGen X).p st p = r implies x <> t holds (x nin (vf t).p implies it.p.x = s.p.x) & for u being ManySortedFunction of FreeGen X, the Sorts of C for H being ManySortedSubset of the generators of G st H = FreeGen X for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f||H)+*(r,supp-var t,v) holds (x in (vf t).p implies for q being Element of A,p st q = (supp-term t).p.x holds it.p.x = q value_at(C, u)); end; definition let B be non void non empty ManySortedSign; let Y be non-empty ManySortedSet of the carrier of B; let T be vf-free all_vars_including inheriting_operations free_in_itself (Y,B)-terms VarMSAlgebra over B; let C be non-empty image of T; let X be GeneratorSystem over B,Y,T; let A be preIfWhileAlgebra of the generators of X; let a be SortSymbol of B; let x be Element of (the generators of X).a; let z be Element of C,a; func C -Execution (A,x,z) -> Subset of Funcs([:C-States(the generators of X), the carrier of A:], C-States(the generators of X)) means :: AOFA_A00:def 28 for f being Function of [:C-States(the generators of X), the carrier of A:], C-States(the generators of X) holds f in it iff f is ExecutionFunction of A, C-States(the generators of X), z-States(the generators of X, x) & for s being Element of C-States(the generators of X) for b being SortSymbol of B for v being Element of (the generators of X).b for v0 being Element of X,b st v0 = v for t being Element of T, b holds f.(s, v:=(t,A)) = succ(s,v0,t value_at(C,s)); end; begin :: Boolean signature definition struct (ManySortedSign) ConnectivesSignature (# carrier,carrier' -> set, Arity -> Function of the carrier',(the carrier)*, ResultSort -> Function of the carrier', the carrier, connectives -> FinSequence of the carrier' #); end; definition let S be ConnectivesSignature; attr S is 1-1-connectives means :: AOFA_A00:def 29 the connectives of S is one-to-one; end; definition let n be Nat; let S be ConnectivesSignature; attr S is n-connectives means :: AOFA_A00:def 30 len the connectives of S = n; end; registration let n be Nat; cluster n-connectives non empty non void for strict ConnectivesSignature; end; definition struct (ConnectivesSignature) BoolSignature (# carrier,carrier' -> set, Arity -> Function of the carrier',(the carrier)*, ResultSort -> Function of the carrier', the carrier, bool-sort -> (Element of the carrier), connectives -> FinSequence of the carrier' #); end; registration let n be Nat; cluster n-connectives non empty non void for strict BoolSignature; end; definition let B be BoolSignature; attr B is bool-correct means :: AOFA_A00:def 31 len the connectives of B >= 3 & (the connectives of B).1 is_of_type {}, the bool-sort of B & (the connectives of B).2 is_of_type <*the bool-sort of B*>, the bool-sort of B & (the connectives of B).3 is_of_type <*the bool-sort of B, the bool-sort of B*>, the bool-sort of B; end; registration cluster 3-connectives 1-1-connectives bool-correct non empty non void for strict BoolSignature; end; registration cluster 1-1-connectives non empty non void for ConnectivesSignature; end; registration let S be 1-1-connectives non empty non void ConnectivesSignature; cluster the connectives of S -> one-to-one; end; definition let S be non empty non void BoolSignature; let B be MSAlgebra over S; attr B is bool-correct means :: AOFA_A00:def 32 (the Sorts of B).the bool-sort of S = BOOLEAN & Den(In((the connectives of S).1, the carrier' of S), B).{} = TRUE & for x,y be boolean object holds Den(In((the connectives of S).2, the carrier' of S), B).<*x*> = 'not' x & Den(In((the connectives of S).3, the carrier' of S), B).<*x,y*> = x '&' y; end; theorem :: AOFA_A00:49 for A being non empty set, n being Nat for f being Function of n-tuples_on A,A holds f is homogeneous quasi_total non empty PartFunc of A*,A & for g being homogeneous Function st f = g holds g is n-ary; registration let A be non empty set; let n be Nat; cluster n-ary for homogeneous quasi_total non empty PartFunc of A*,A; end; scheme :: AOFA_A00:sch 2 Sch1 {A() -> non empty set, F(set) -> Element of A()}: ex f being 1-ary homogeneous quasi_total non empty PartFunc of A()*,A() st for a being Element of A() holds f.<*a*> = F(a); scheme :: AOFA_A00:sch 3 Sch2 {A() -> non empty set, F(set,set) -> Element of A()}: ex f being 2-ary homogeneous quasi_total non empty PartFunc of A()*,A() st for a,b being Element of A() holds f.<*a,b*> = F(a,b); theorem :: AOFA_A00:50 for S being non empty non void ManySortedSign for A being non-empty ManySortedSet of the carrier of S for f being ManySortedFunction of A#*the Arity of S, A*the ResultSort of S for o being OperSymbol of S for d being Function of (A#*the Arity of S).o, (A*the ResultSort of S).o holds f+*(o,d) is ManySortedFunction of A#*the Arity of S, A*the ResultSort of S; theorem :: AOFA_A00:51 for S being bool-correct non empty non void BoolSignature for A being non-empty ManySortedSet of the carrier of S ex B being non-empty strict MSAlgebra over S st the Sorts of B = A+*(the bool-sort of S, BOOLEAN) & B is bool-correct; registration let S be bool-correct non empty non void BoolSignature; cluster bool-correct non-empty for strict MSAlgebra over S; end; definition let S be bool-correct non empty non void BoolSignature; let B be non-empty MSAlgebra over S; func \trueB -> Element of B, the bool-sort of S equals :: AOFA_A00:def 33 Den(In((the connectives of S).1, the carrier' of S), B).{}; let p be Element of B, the bool-sort of S; func \notp -> Element of B, the bool-sort of S equals :: AOFA_A00:def 34 Den(In((the connectives of S).2, the carrier' of S), B).<*p*>; let q be Element of B, the bool-sort of S; func p\andq -> Element of B, the bool-sort of S equals :: AOFA_A00:def 35 Den(In((the connectives of S).3, the carrier' of S), B).<*p,q*>; end; definition let S be bool-correct non empty non void BoolSignature; let B be non-empty MSAlgebra over S; let p be Element of B, the bool-sort of S; let q be Element of B, the bool-sort of S; func p\orq -> Element of B, the bool-sort of S equals :: AOFA_A00:def 36 \not(\notp\and\notq); func p\impq -> Element of B, the bool-sort of S equals :: AOFA_A00:def 37 \not(p\and\notq); end; definition let S be bool-correct non empty non void BoolSignature; let B be non-empty MSAlgebra over S; let p be Element of B, the bool-sort of S; let q be Element of B, the bool-sort of S; func p\iffq -> Element of B, the bool-sort of S equals :: AOFA_A00:def 38 p\andq\or(\notp\and\notq); end; begin :: Algebra with integers definition let i be Nat; let s be set; let S be BoolSignature; attr S is (i,s) integer means :: AOFA_A00:def 39 len the connectives of S >= i+6 & ex I being Element of S st I = s & I <> the bool-sort of S & (the connectives of S).i is_of_type {},I & :: 0 (the connectives of S).(i+1) is_of_type {},I & :: 1 (the connectives of S).i <> (the connectives of S).(i+1) & (the connectives of S).(i+2) is_of_type <*I*>,I & :: - (the connectives of S).(i+3) is_of_type <*I,I*>,I & :: + (the connectives of S).(i+4) is_of_type <*I,I*>,I & :: * (the connectives of S).(i+5) is_of_type <*I,I*>,I & :: div (the connectives of S).(i+3) <> (the connectives of S).(i+4) & (the connectives of S).(i+3) <> (the connectives of S).(i+5) & (the connectives of S).(i+4) <> (the connectives of S).(i+5) & (the connectives of S).(i+6) is_of_type <*I,I*>,the bool-sort of S; :: <= end; theorem :: AOFA_A00:52 ex S being 10-connectives non empty non void strict BoolSignature st S is 1-1-connectives (4,1) integer bool-correct & the carrier of S = {0,1} & ex I being SortSymbol of S st I = 1 & (the connectives of S).4 is_of_type {},I; registration cluster 10-connectives 1-1-connectives (4,1) integer bool-correct non empty non void for strict BoolSignature; end; definition let S be non empty non void BoolSignature; let I be SortSymbol of S; attr I is integer means :: AOFA_A00:def 40 I = 1; end; registration let S be (4,1) integer non empty non void BoolSignature; cluster integer for SortSymbol of S; end; theorem :: AOFA_A00:53 for S being (4,1) integer non empty non void BoolSignature for I being integer SortSymbol of S holds I <> the bool-sort of S & (the connectives of S).4 is_of_type {},I & (the connectives of S).(4+1) is_of_type {},I & (the connectives of S).4 <> (the connectives of S).(4+1) & (the connectives of S).(4+2) is_of_type <*I*>,I & (the connectives of S).(4+3) is_of_type <*I,I*>,I & (the connectives of S).(4+4) is_of_type <*I,I*>,I & (the connectives of S).(4+5) is_of_type <*I,I*>,I & (the connectives of S).(4+3) <> (the connectives of S).(4+4) & (the connectives of S).(4+3) <> (the connectives of S).(4+5) & (the connectives of S).(4+4) <> (the connectives of S).(4+5) & (the connectives of S).(4+6) is_of_type <*I,I*>,the bool-sort of S; definition let S be (4,1) integer non empty non void BoolSignature; let A be non-empty MSAlgebra over S; let I be integer SortSymbol of S; func \0(A,I) -> Element of (the Sorts of A).I equals :: AOFA_A00:def 41 Den(In((the connectives of S).4, the carrier' of S), A).{}; func \1(A,I) -> Element of (the Sorts of A).I equals :: AOFA_A00:def 42 Den(In((the connectives of S).5, the carrier' of S), A).{}; let a be Element of (the Sorts of A).I; func -a -> Element of (the Sorts of A).I equals :: AOFA_A00:def 43 Den(In((the connectives of S).6, the carrier' of S), A).<*a*>; let b be Element of (the Sorts of A).I; func a+b -> Element of (the Sorts of A).I equals :: AOFA_A00:def 44 Den(In((the connectives of S).7, the carrier' of S), A).<*a,b*>; func a*b -> Element of (the Sorts of A).I equals :: AOFA_A00:def 45 Den(In((the connectives of S).8, the carrier' of S), A).<*a,b*>; func a div b -> Element of (the Sorts of A).I equals :: AOFA_A00:def 46 Den(In((the connectives of S).9, the carrier' of S), A).<*a,b*>; func leq(a,b) -> Element of (the Sorts of A).the bool-sort of S equals :: AOFA_A00:def 47 Den(In((the connectives of S).10, the carrier' of S), A).<*a,b*>; end; definition let S be (4,1) integer non empty non void BoolSignature; let A be non-empty MSAlgebra over S; let I be integer SortSymbol of S; let a,b be Element of A,I; func a-b -> Element of A,I equals :: AOFA_A00:def 48 a+-b; func a mod b -> Element of A,I equals :: AOFA_A00:def 49 a+-(a div b)*b; end; registration let S be (4,1) integer non empty non void BoolSignature; let X be non-empty ManySortedSet of the carrier of S; cluster X.1 -> non empty; end; definition let n be Nat; let s be set; let S be bool-correct non empty non void BoolSignature; let A be bool-correct MSAlgebra over S; attr A is (n,s) integer means :: AOFA_A00:def 50 ex I being SortSymbol of S st I = s & (the connectives of S).n is_of_type {},I & (the Sorts of A).I = INT & Den(In((the connectives of S).n, the carrier' of S), A).{} = 0 & Den(In((the connectives of S).(n+1), the carrier' of S), A).{} = 1 & for i,j being Integer holds Den(In((the connectives of S).(n+2), the carrier' of S), A).<*i*> = -i & Den(In((the connectives of S).(n+3), the carrier' of S), A).<*i,j*> = i+j & Den(In((the connectives of S).(n+4), the carrier' of S), A).<*i,j*> = i*j & (j <> 0 implies Den(In((the connectives of S).(n+5), the carrier' of S), A).<*i,j*> = i div j) & Den(In((the connectives of S).(n+6), the carrier' of S), A).<*i,j*> = IFGT(i,j,FALSE,TRUE); end; theorem :: AOFA_A00:54 for n being Nat, I being set st n >= 1 for S being bool-correct non empty non void BoolSignature st S is (n,I) integer ex A being bool-correct non-empty strict MSAlgebra over S st A is (n,I) integer; registration let S be (4,1) integer bool-correct non empty non void BoolSignature; cluster (4,1) integer for bool-correct non-empty strict MSAlgebra over S; end; theorem :: AOFA_A00:55 for S being (4,1) integer bool-correct non empty non void BoolSignature for A being (4,1) integer bool-correct non-empty MSAlgebra over S for I being integer SortSymbol of S holds (the Sorts of A).I = INT & \0(A,I) = 0 & \1(A,I) = 1 & for i,j being Integer,a,b being Element of (the Sorts of A).I st a = i & b = j holds -a = -i & a+b = i+j & a*b = i*j & (j <> 0 implies a div b = i div j) & leq(a,b) = IFGT(i,j,FALSE,TRUE) & (leq(a,b) = TRUE iff i <= j) & (leq(a,b) = FALSE iff i > j); 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 -> integer for Element of (the Sorts of A).1; end; begin :: Algebras with arrays definition let I,N be set; let n be Nat; let S be ConnectivesSignature; attr S is (n,I,N)-array means :: AOFA_A00:def 51 len the connectives of S >= n+3 & :: I=L - type of elements of an array :: N=K - intgers :: J - array of I ex J,K,L being Element of S st L = I & K = N & J <> L & J <> K & (the connectives of S).n is_of_type <*J,K*>, L & ::(a,i) -> a[i] (the connectives of S).(n+1) is_of_type <*J,K,L*>, J & :: a[i]:=x (the connectives of S).(n+2) is_of_type <*J*>, K & :: length (the connectives of S).(n+3) is_of_type <*K,L*>, J; :: init end; definition let S be non empty non void ConnectivesSignature; let I,N be set; let n be Nat; let A be MSAlgebra over S; attr A is (n,I,N)-array means :: AOFA_A00:def 52 ex J,K being Element of S st K = I & (the connectives of S).n is_of_type <*J,N*>, K & (the Sorts of A).J = ((the Sorts of A).K)^omega & (the Sorts of A).N = INT & (for a being 0-based finite array of (the Sorts of A).K holds (for i being Integer st i in dom a holds Den((the connectives of S)/.n,A).<*a,i*> = a.i & for x being Element of A,K holds Den((the connectives of S)/.(n+1),A).<*a,i,x*> = a+*(i,x)) & Den((the connectives of S)/.(n+2),A).<*a*> = card a) & for i being Integer, x being Element of A,K st i >= 0 holds Den((the connectives of S)/.(n+3),A).<*i,x*> = Segm(i)-->x; end; definition let B be non empty BoolSignature; let C be non empty ConnectivesSignature; func B+*C -> strict BoolSignature means :: AOFA_A00:def 53 the ManySortedSign of it = B+*C & the bool-sort of it = the bool-sort of B & the connectives of it = (the connectives of B)^the connectives of C; end; theorem :: AOFA_A00:56 for B being non empty BoolSignature for C being non empty ConnectivesSignature holds the carrier of B+*C = (the carrier of B)\/the carrier of C & the carrier' of B+*C = (the carrier' of B)\/the carrier' of C & the Arity of B+*C = (the Arity of B)+*the Arity of C & the ResultSort of B+*C = (the ResultSort of B)+*the ResultSort of C; registration let B be non empty BoolSignature; let C be non empty ConnectivesSignature; cluster B+*C -> non empty; end; registration let B be non void non empty BoolSignature; let C be non empty ConnectivesSignature; cluster B+*C -> non void; end; registration let n1,n2 be Nat; let B be n1-connectives non empty non void BoolSignature; let C be n2-connectives non empty non void ConnectivesSignature; cluster B+*C -> n1+n2-connectives; end; theorem :: AOFA_A00:57 for M,O,N,I being set st I in M & N in M ex C being 4-connectives non empty non void strict ConnectivesSignature st C is (1,I,N)-array 1-1-connectives & M c= the carrier of C & O misses the carrier' of C & (the ResultSort of C).((the connectives of C).2) nin M; registration let I,N be set; cluster (1,I,N)-array 4-connectives for non empty non void strict ConnectivesSignature; end; theorem :: AOFA_A00:58 for n,m being Nat st m > 0 for B being n-connectives non empty non void BoolSignature for I,N being set for C being non empty non void ConnectivesSignature st C is (m,I,N)-array holds B+*C is (n+m,I,N)-array; theorem :: AOFA_A00:59 for m being Nat st m > 0 for s being set for B being non empty non void BoolSignature for C being non empty non void ConnectivesSignature st B is (m,s) integer & the carrier' of B misses the carrier' of C holds B+*C is (m,s) integer; theorem :: AOFA_A00:60 for B being bool-correct non empty non void BoolSignature for C being non empty non void ConnectivesSignature st the carrier' of B misses the carrier' of C holds B+*C is bool-correct; definition let n be Nat; let B be BoolSignature; attr B is n array-correct means :: AOFA_A00:def 54 (the ResultSort of B).((the connectives of B).(n+1)) <> the bool-sort of B; end; registration cluster 1-1-connectives 14-connectives (11,1,1)-array 11 array-correct (4,1) integer bool-correct non empty non void for strict BoolSignature; end; registration let S be (11,1,1)-array non empty non void BoolSignature; cluster integer for SortSymbol of S; end; definition let S be (11,1,1)-array non empty non void BoolSignature; func the_array_sort_of S -> SortSymbol of S equals :: AOFA_A00:def 55 (the ResultSort of S).((the connectives of S).12); end; definition let S be (4,1) integer (11,1,1)-array non empty non void BoolSignature; let A be non-empty MSAlgebra over S; let a be Element of (the Sorts of A).the_array_sort_of S; let I be integer SortSymbol of S; func length(a,I) -> Element of (the Sorts of A).I equals :: AOFA_A00:def 56 Den(In((the connectives of S).13, the carrier' of S), A).<*a*>; let i be Element of (the Sorts of A).I; func a.(i) -> Element of (the Sorts of A).I equals :: AOFA_A00:def 57 Den(In((the connectives of S).11, the carrier' of S), A).<*a,i*>; let x be Element of (the Sorts of A).I; func (a,i)<-x -> Element of (the Sorts of A).the_array_sort_of S equals :: AOFA_A00:def 58 Den(In((the connectives of S).12, the carrier' of S), A).<*a,i,x*>; end; definition let S be (4,1) integer (11,1,1)-array non empty non void BoolSignature; let A be non-empty MSAlgebra over S; let I be integer SortSymbol of S; let i be Element of (the Sorts of A).I; let x be Element of (the Sorts of A).I; func init.array(i,x) -> Element of (the Sorts of A).the_array_sort_of S equals :: AOFA_A00:def 59 Den(In((the connectives of S).14, the carrier' of S), A).<*i,x*>; end; registration let X be non empty set; cluster <*X*> -> non-empty; let Y,Z be non empty set; cluster <*X,Y,Z*> -> non-empty; end; registration let X be functional non empty set; let Y,Z be non empty set; let f be Element of product <*X,Y,Z*>; cluster f.1 -> Relation-like Function-like; end; registration let X be integer-membered non empty set; let Y be non empty set; let f be Element of product <*X,Y*>; cluster f.1 -> integer; end; theorem :: AOFA_A00:61 for I,N being set for S being (1,I,N)-array non empty non void ConnectivesSignature for Y being non empty set for X being non-empty ManySortedSet of Y st ((the ResultSort of S).((the connectives of S).2) nin Y or X.((the ResultSort of S).((the connectives of S).2)) = (X.I)^omega) & X.N = INT & I in Y ex A being non-empty strict MSAlgebra over S st A is (1,I,N)-array & the Sorts of A tolerates X; registration let I,N be set; let S be (1,I,N)-array non empty non void ConnectivesSignature; cluster (1,I,N)-array for non-empty strict MSAlgebra over S; end; definition let S1 be non empty BoolSignature; let S2 be non empty ConnectivesSignature; let A1 be non-empty MSAlgebra over S1; let A2 be non-empty MSAlgebra over S2; func (S1,A1) +* A2 -> strict non-empty MSAlgebra over S1+*S2 equals :: AOFA_A00:def 60 A1 +* A2; end; theorem :: AOFA_A00:62 for B being bool-correct non empty non void BoolSignature for A1 being bool-correct non-empty MSAlgebra over B for C being non empty non void ConnectivesSignature st the carrier' of B misses the carrier' of C for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 holds (B,A1)+*A2 is bool-correct; theorem :: AOFA_A00:63 for n being Nat, I being set st n >= 4 for B being bool-correct non empty non void BoolSignature st B is (n,I) integer for A1 being bool-correct non-empty MSAlgebra over B st A1 is (n,I) integer for C being non empty non void ConnectivesSignature st the carrier' of B misses the carrier' of C for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 for S being bool-correct non empty non void BoolSignature st the BoolSignature of S = B+*C for A being bool-correct non-empty MSAlgebra over S st A = (B,A1)+*A2 holds A is (n,I) integer; theorem :: AOFA_A00:64 for n,m being Nat, s,r being set st n >= 1 & m >= 1 for B being m-connectives non empty non void BoolSignature for A1 being non-empty MSAlgebra over B for C being non empty non void ConnectivesSignature st C is (n,s,r)-array for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 & A2 is (n,s,r)-array for S being non empty non void BoolSignature st the BoolSignature of S = B+*C for A being non-empty MSAlgebra over S st A = (B,A1)+*A2 holds A is (m+n,s,r)-array; theorem :: AOFA_A00:65 for n being Nat, s being set for S1,S2 being BoolSignature st the bool-sort of S1 = the bool-sort of S2 & len the connectives of S2 >= 3 & for i st i >= 1 & i <= 3 holds (the Arity of S1).((the connectives of S1).i) = (the Arity of S2).((the connectives of S2).i) & (the ResultSort of S1).((the connectives of S1).i) = (the ResultSort of S2).((the connectives of S2).i) holds S1 is bool-correct implies S2 is bool-correct; theorem :: AOFA_A00:66 for n being Nat, s being set for S1,S2 being non empty BoolSignature st n >= 1 & the bool-sort of S1 = the bool-sort of S2 & len the connectives of S2 >= n+6 & (the connectives of S2).n <> (the connectives of S2).(n+1) & (the connectives of S2).(n+3) <> (the connectives of S2).(n+4) & (the connectives of S2).(n+3) <> (the connectives of S2).(n+5) & (the connectives of S2).(n+4) <> (the connectives of S2).(n+5) & for i st i >= n & i <= n+6 holds (the Arity of S1).((the connectives of S1).i) = (the Arity of S2).((the connectives of S2).i) & (the ResultSort of S1).((the connectives of S1).i) = (the ResultSort of S2).((the connectives of S2).i) holds S1 is (n,s) integer implies S2 is (n,s) integer; theorem :: AOFA_A00:67 for n,m being Nat, s,r being set for S1,S2 being non empty ConnectivesSignature st 1 <= n & len the connectives of S1 >= n+3 & for i st i >= n & i <= n+3 holds (the Arity of S1).((the connectives of S1).i) = (the Arity of S2).((the connectives of S2).(i+m)) & (the ResultSort of S1).((the connectives of S1).i) = (the ResultSort of S2).((the connectives of S2).(i+m)) holds S2 is (n+m,s,r)-array implies S1 is (n,s,r)-array; theorem :: AOFA_A00:68 for j,k be set, i,m,n being Nat st m >= 4 & m+6 <= n & i >= 1 for S being 1-1-connectives bool-correct non empty non void BoolSignature st S is (n+i,j,k)-array (m,k) integer ex B being bool-correct non empty non void BoolSignature, C being non empty non void ConnectivesSignature st the BoolSignature of S = B+*C & B is n-connectives (m,k) integer & C is (i,j,k)-array & the carrier of B = the carrier of C & the carrier' of B = (the carrier' of S)\rng the connectives of C & the carrier' of C = rng the connectives of C & the connectives of B = (the connectives of S)|n & the connectives of C = (the connectives of S)/^n; theorem :: AOFA_A00:69 for s,I being set for S being bool-correct non empty non void BoolSignature st S is (4,I) integer for X being non empty set st s in the carrier of S & s <> I & s <> the bool-sort of S ex A being bool-correct non-empty MSAlgebra over S st A is (4,I) integer & (the Sorts of A).s = X; registration let S be 1-1-connectives (11,1,1)-array 11 array-correct (4,1) integer bool-correct non empty non void BoolSignature; cluster (11,1,1)-array (4,1) integer for bool-correct non-empty strict MSAlgebra over S; end;