:: Free Term Algebras :: by Grzegorz Bancerek :: :: Received May 15, 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 TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, FUNCOP_1, ZF_LANG, ZF_MODEL, REALSET1, PBOOLE, TREES_1, ORDINAL4, FUNCT_4, FINSET_1, PROB_2, GROUP_6, CARD_3, TREES_2, CARD_1, ARYTM_3, XXREAL_0, MCART_1, MEMBER_1, PRELAMB, TREES_4, DTCONSTR, TDGROUP, TREES_3, FUNCT_6, TREES_A, TREES_9, MSUALG_6, MATROID0, ZF_LANG1, MARGREL1, PZFMISC1, NUMBERS, NAT_1, STRUCT_0, UNIALG_2, MSUALG_1, MSUALG_2, MSUALG_3, MSAFREE, ALGSPEC1, MSATERM, EQUATION, AOFA_000, AOFA_I00, MSAFREE4, FOMODEL2, SETLIM_2, PENCIL_1, MSUALG_4, REWRITE1, CIRCUIT2, MOD_4, RLTOPSP1, RFINSEQ, ARYTM_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XTUPLE_0, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, ORDINAL1, FINSET_1, CARD_1, XXREAL_0, XCMPLX_0, AOFA_I00, FINSEQ_1, FINSEQ_2, LANG1, FUNCT_6, NUMBERS, FUNCOP_1, TREES_1, CARD_3, PBOOLE, PROB_2, FUNCT_4, TREES_2, TREES_3, TREES_4, TREES_9, RFINSEQ, REWRITE1, PENCIL_1, FUNCT_7, DTCONSTR, PZFMISC1, COMPUT_1, STRUCT_0, MSUALG_1, MSUALG_2, MSUALG_3, MSUALG_4, MSAFREE, MSAFREE1, MSATERM, MSUALG_6, ALGSPEC1, CATALG_1, MSAFREE3, EQUATION, AOFA_000; constructors RELSET_1, DOMAIN_1, PZFMISC1, FUNCT_4, TREES_9, COMPUT_1, MSUALG_3, MSAFREE1, MSUALG_6, EQUATION, CATALG_1, ALGSPEC1, MSAFREE3, REAL_1, PRALG_2, PENCIL_1, REWRITE1, RFINSEQ; registrations XBOOLE_0, RELSET_1, PBOOLE, MSUALG_1, INSTALG1, MSAFREE1, FUNCT_1, FUNCOP_1, FINSET_1, FINSEQ_1, STRUCT_0, MSAFREE3, EQUATION, COMPUT_1, CARD_3, MSAFREE, NAT_1, ORDINAL1, CARD_1, RELAT_1, SUBSET_1, CATALG_1, TREES_2, MSUALG_2, MSATERM, TREES_1, TREES_3, MSUALG_3, ALTCAT_2, MSSUBFAM, TREES_9, MSUALG_4, MSUALG_6, REWRITE1, MSUALG_9, XREAL_0, XTUPLE_0; requirements BOOLE, SUBSET, ARITHM, NUMERALS; begin :: Preliminaries reserve S for non empty non void ManySortedSign; reserve X for non-empty ManySortedSet of S; theorem :: MSAFREE4:1 for I being set, f1,f2 being ManySortedSet of I st f1 c= f2 holds Union f1 c= Union f2; reserve x,y,z for set, i,j for Nat; definition let I be set; let X be non-empty ManySortedSet of I; let A be Component of X; redefine mode Element of A -> Element of Union X; end; definition let I be set; let X be ManySortedSet of I; let i be Element of I; redefine func X.i -> Component of X; end; definition let I be set; let X,Y be ManySortedSet of I; let f be ManySortedFunction of X,Y; let x be object; redefine func f.x -> Function of X.x,Y.x; end; scheme :: MSAFREE4:sch 1 Sch1{I()-> set, A()->non-empty ManySortedSet of I(), F(object,object)->set}: ex f being ManySortedFunction of I() st for x st x in I() holds dom(f.x) = A().x & for y being Element of A().x holds f.x .y = F(x,y); scheme :: MSAFREE4:sch 2 Sch2{I()->non empty set, A,B()->non-empty ManySortedSet of I(), F(object,object) -> set}: ex f being ManySortedFunction of A(),B() st for i being Element of I() for a being Element of A().i holds f.i.a = F(i,a) provided for i being Element of I() for a being Element of A().i holds F(i,a) in B().i; definition let X be non empty set; let O be set; let f be Function of O,X; let g be ManySortedSet of X; redefine func g*f -> ManySortedSet of O; end; registration let S, X; let F be ManySortedSet of S -Terms X; let o be OperSymbol of S; let p be ArgumentSeq of Sym(o,X); cluster F*p -> FinSequence-like; end; theorem :: MSAFREE4:2 Subtrees root-tree x = {root-tree x}; registration let f be DTree-yielding Function; cluster rng f -> constituted-DTrees; end; theorem :: MSAFREE4:3 for p being non empty DTree-yielding FinSequence holds Subtrees(x-tree p) = {x-tree p} \/ Subtrees rng p; theorem :: MSAFREE4:4 Subtrees(x-tree{}) = {x-tree {}}; theorem :: MSAFREE4:5 x-tree {} = root-tree x; registration cluster finite-yielding DTree-yielding non empty for FinSequence; cluster finite-yielding Tree-yielding non empty for FinSequence; end; registration let f be finite-yielding Function-yielding Function; cluster doms f -> finite-yielding; end; registration let p be finite-yielding Tree-yielding FinSequence; cluster tree p -> finite; end; registration let t be finite DecoratedTree; cluster Subtrees t -> finite-membered; end; registration let p be finite-yielding DTree-yielding FinSequence; let x; cluster x-tree p -> finite; end; theorem :: MSAFREE4:6 for t1,t2 being finite DecoratedTree st t1 in Subtrees t2 holds height dom t1 <= height dom t2; theorem :: MSAFREE4:7 for p being DTree-yielding FinSequence st p is finite-yielding for t being DecoratedTree st x in Subtrees t & t in rng p holds x <> y-tree p; registration let S; let X be ManySortedSet of S; cluster -> finite-yielding for S-Terms X-valued Function; end; theorem :: MSAFREE4:8 for X being non empty constituted-DTrees set for t being DecoratedTree st t in X holds Subtrees t c= Subtrees X; theorem :: MSAFREE4:9 for X being non empty constituted-DTrees set holds X c= Subtrees X; theorem :: MSAFREE4:10 for t being Term of S,X for x st x in Subtrees t holds x is Term of S,X; theorem :: MSAFREE4:11 for p being DTree-yielding FinSequence holds rng p c= Subtrees (x-tree p); theorem :: MSAFREE4:12 for t1,t2 being DecoratedTree st t1 in Subtrees t2 holds Subtrees t1 c= Subtrees t2; theorem :: MSAFREE4:13 for X being ManySortedSet of S for o being OperSymbol of S for p being FinSequence st p in Args(o,Free(S,X)) holds Den(o,Free(S,X)).p = [o,the carrier of S]-tree p; registration let I be set; let A,B be non-empty ManySortedSet of I; let f be ManySortedFunction of A,B; cluster rngs f -> non-empty; end; registration let S; cluster -> Relation-like Function-like for Element of TermAlg S; end; registration let I be set; let A be ManySortedSet of I; let f be FinSequence of I; cluster A*f -> dom f-defined; end; registration let I be set; let A be ManySortedSet of I; let f be FinSequence of I; cluster A*f -> total for dom f-defined Relation; end; theorem :: MSAFREE4:14 for I being non empty set, 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 qua ManySortedSet of J; theorem :: MSAFREE4:15 for I being set for A,B being ManySortedSet of I st A c= B for f being FinSequence of I holds A*f c= B*f qua ManySortedSet of dom f; theorem :: MSAFREE4:16 for I being set for A,B being ManySortedSet of I st A c= B holds product A c= product B; theorem :: MSAFREE4:17 for R being weakly-normalizing with_UN_property Relation st x is_a_normal_form_wrt R holds nf(x,R) = x; theorem :: MSAFREE4:18 for R being weakly-normalizing with_UN_property Relation holds nf(nf(x,R),R) = nf(x,R); registration let S, X; let A be MSSubset of FreeMSA X; let x be object; cluster -> Relation-like Function-like for Element of A.x; end; definition let I be set; let A be ManySortedSet of I; attr A is countable means :: MSAFREE4:def 1 for x st x in I holds A.x is countable; end; registration let I be set; let X be countable set; cluster I --> X -> countable for ManySortedSet of I; end; registration let I be set; cluster non-empty countable for ManySortedSet of I; end; registration let I be set; let X be countable ManySortedSet of I; let x be object; cluster X.x -> countable; end; registration let A be countable set; cluster one-to-one for Function of A,NAT; end; registration let I be set; let X0 be countable ManySortedSet of I; cluster "1-1" for ManySortedFunction of X0, I-->NAT; end; theorem :: MSAFREE4:19 for S being set for X being ManySortedSet of S for Y being non-empty ManySortedSet of S for w being ManySortedFunction of X, Y holds rngs w is ManySortedSubset of Y; theorem :: MSAFREE4:20 for S being set for X being countable ManySortedSet of S ex Y being ManySortedSubset of S-->NAT, w being ManySortedFunction of X, S-->NAT st w is "1-1" & Y = rngs w & for x st x in S holds w.x is Enumeration of X.x & Y.x = card(X.x); theorem :: MSAFREE4:21 for I being set for A being ManySortedSet of I for B being non-empty ManySortedSet of I holds A is_transformable_to B; theorem :: MSAFREE4:22 for I being set for A,B,C being non-empty ManySortedSet of I for f being ManySortedFunction of A,B st B is ManySortedSubset of C holds f is ManySortedFunction of A,C; theorem :: MSAFREE4:23 for I being set, A,B being ManySortedSet of I st A is_transformable_to B for f being ManySortedFunction of A,B st f is "onto" ex g being ManySortedFunction of B,A st f**g = id B; theorem :: MSAFREE4:24 for A1,A2 being MSAlgebra over S st the MSAlgebra of A1 = the MSAlgebra of A2 for B1 being MSSubset of A1, B2 being MSSubset of A2 st B1 = B2 for o being OperSymbol of S st B1 is_closed_on o holds B2 is_closed_on o; theorem :: MSAFREE4:25 for A1,A2 being MSAlgebra over S st the MSAlgebra of A1 = the MSAlgebra of A2 for B1 being MSSubset of A1, B2 being MSSubset of A2 st B1 = B2 for o being OperSymbol of S st B1 is_closed_on o holds o/.B2 = o/.B1; theorem :: MSAFREE4:26 for A1,A2 being MSAlgebra over S st the MSAlgebra of A1 = the MSAlgebra of A2 for B1 being MSSubset of A1, B2 being MSSubset of A2 st B1 = B2 & B1 is opers_closed holds Opers(A2,B2) = Opers(A1,B1); theorem :: MSAFREE4:27 for A1,A2 being MSAlgebra over S st the MSAlgebra of A1 = the MSAlgebra of A2 for B1 being MSSubset of A1, B2 being MSSubset of A2 st B1 = B2 & B1 is opers_closed holds B2 is opers_closed; theorem :: MSAFREE4:28 for A1,A2,B being MSAlgebra over S st the MSAlgebra of A1 = the MSAlgebra of A2 for B1 being MSSubAlgebra of A1 st the MSAlgebra of B = the MSAlgebra of B1 holds B is MSSubAlgebra of A2; theorem :: MSAFREE4:29 for A1,A2 being MSAlgebra over S st A2 is empty for h being ManySortedFunction of A1,A2 holds h is_homomorphism A1,A2; theorem :: MSAFREE4:30 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_homomorphism A1,B1 holds h2 is_homomorphism A2,B2; begin :: Trivial algebras definition let I be set; let X be ManySortedSet of I; redefine attr X is trivial-yielding means :: MSAFREE4:def 2 for x st x in I holds X.x is trivial; end; registration let I be set; cluster non-empty trivial-yielding for ManySortedSet of I; end; registration let I be set; let S be trivial-yielding ManySortedSet of I; let x be object; cluster S.x -> trivial; end; definition let S; let A be MSAlgebra over S; attr A is trivial means :: MSAFREE4:def 3 the Sorts of A is trivial-yielding; end; registration let S; cluster trivial disjoint_valued non-empty for strict MSAlgebra over S; end; registration let S; let A be trivial MSAlgebra over S; cluster the Sorts of A -> trivial-yielding; end; theorem :: MSAFREE4:31 for A being trivial non-empty MSAlgebra over S for s being SortSymbol of S for e being Element of (Equations S).s holds A |= e; theorem :: MSAFREE4:32 for A being trivial non-empty MSAlgebra over S for T being EqualSet of S holds A |= T; theorem :: MSAFREE4:33 for A being non-empty MSAlgebra over S for T being non-empty trivial MSAlgebra over S for f being ManySortedFunction of A,T holds f is_homomorphism A,T; theorem :: MSAFREE4:34 for T being non-empty trivial MSAlgebra over S for A being non-empty MSSubAlgebra of T holds the MSAlgebra of A = the MSAlgebra of T; begin :: Image definition let S; let A be non-empty MSAlgebra over S; let C be MSAlgebra over S; attr C is A-Image means :: MSAFREE4:def 4 ex B being non-empty MSAlgebra over S, h being ManySortedFunction of A,B st h is_homomorphism A,B & the MSAlgebra of C = Image h; end; registration let S; let A be non-empty MSAlgebra over S; cluster A-Image -> non-empty for MSAlgebra over S; cluster A-Image for non-empty strict MSAlgebra over S; end; definition let S; let A be non-empty MSAlgebra over S; let C be non-empty MSAlgebra over S; redefine attr C is A-Image means :: MSAFREE4:def 5 ex h being ManySortedFunction of A,C st h is_epimorphism A,C; end; definition let S; let A be non-empty MSAlgebra over S; mode image of A is A-Image non-empty MSAlgebra over S; end; registration let S; let A be non-empty MSAlgebra over S; cluster disjoint_valued trivial for image of A; end; theorem :: MSAFREE4:35 for A being non-empty MSAlgebra over S for B being A-Image MSAlgebra over S for s being SortSymbol of S for e being Element of (Equations S).s st A |= e holds B |= e; theorem :: MSAFREE4:36 for A being non-empty MSAlgebra over S for B being A-Image MSAlgebra over S for T being EqualSet of S st A |= T holds B |= T; begin :: Term Algebras definition let S, X; let A be MSAlgebra over S; attr A is (X,S)-terms means :: MSAFREE4:def 6 the Sorts of A is ManySortedSubset of the Sorts of Free(S,X); end; registration let S,X; cluster Free(S,X) -> X,S-terms; end; registration let S, X; cluster Free(S,X) -> non-empty disjoint_valued; end; registration let S,X; cluster X,S-terms non-empty for strict MSAlgebra over S; end; definition let S,X; let A be X,S-terms MSAlgebra over S; attr A is all_vars_including means :: MSAFREE4:def 7 FreeGen X is ManySortedSubset of the Sorts of A; attr A is inheriting_operations means :: MSAFREE4:def 8 for o being OperSymbol of S, p being FinSequence holds (p in Args(o, Free(S,X)) & Den(o,Free(S,X)).p in (the Sorts of A).the_result_sort_of o implies p in Args(o,A) & Den(o,A).p = Den(o,Free(S,X)).p); attr A is free_in_itself means :: MSAFREE4:def 9 for f being ManySortedFunction of FreeGen X, the Sorts of A for G being ManySortedSubset of the Sorts of A st G = FreeGen X ex h being ManySortedFunction of A,A st h is_homomorphism A,A & f = h || G; end; theorem :: MSAFREE4:37 for A,B being non-empty MSAlgebra over S st the MSAlgebra of A = the MSAlgebra of B holds A is (X,S)-terms implies B is (X,S)-terms; theorem :: MSAFREE4:38 for A,B being X,S-terms non-empty MSAlgebra over S st the MSAlgebra of A = the MSAlgebra of B holds (A is all_vars_including implies B is all_vars_including) & (A is inheriting_operations implies B is inheriting_operations) & (A is free_in_itself implies B is free_in_itself); registration let J be non empty non void ManySortedSign; let T be non-empty MSAlgebra over J; cluster non-empty for GeneratorSet of T; end; registration let S, X; cluster Free(S,X) -> all_vars_including inheriting_operations free_in_itself; end; registration let S, X; cluster all_vars_including -> non-empty for (X,S)-terms MSAlgebra over S; cluster all_vars_including inheriting_operations free_in_itself for (X,S)-terms strict MSAlgebra over S; end; reserve A0 for (X,S)-terms non-empty MSAlgebra over S, A1 for all_vars_including (X,S)-terms MSAlgebra over S, A2 for all_vars_including inheriting_operations (X,S)-terms MSAlgebra over S, A for all_vars_including inheriting_operations free_in_itself (X,S)-terms MSAlgebra over S; theorem :: MSAFREE4:39 (for t being Element of A0 holds t is Element of Free(S,X)) & for s being SortSymbol of S for t being Element of A0,s holds t is Element of Free(S,X),s; theorem :: MSAFREE4:40 for s being SortSymbol of S for x being Element of X.s holds root-tree [x,s] is Element of A1,s; theorem :: MSAFREE4:41 for o being OperSymbol of S holds Args(o,A1) c= Args(o, Free(S,X)); registration let S be set; cluster disjoint_valued non-empty for ManySortedSet of S; end; registration let S be set; let T be disjoint_valued non-empty ManySortedSet of S; cluster -> disjoint_valued for ManySortedSubset of T; end; registration let S, X; cluster (X,S)-terms strict for MSAlgebra over S; end; definition let S, X, A1; func canonical_homomorphism A1 -> ManySortedFunction of Free(S,X),A1 means :: MSAFREE4:def 10 it is_homomorphism Free(S,X),A1 & for G being GeneratorSet of Free(S,X) st G = FreeGen X holds id G = it || G; end; registration let S, X, A0; cluster -> Function-like Relation-like for Element of A0; let s be SortSymbol of S; cluster -> Function-like Relation-like for Element of A0,s; end; registration let S, X, A0; cluster -> DecoratedTree-like for Element of A0; let s be SortSymbol of S; cluster -> DecoratedTree-like for Element of A0,s; end; registration let S, X; cluster (X,S)-terms -> disjoint_valued for MSAlgebra over S; end; theorem :: MSAFREE4:42 for t being Element of A0 holds t is Term of S,X; theorem :: MSAFREE4:43 for t being Element of A0 for s being SortSymbol of S st t in (the Sorts of Free(S,X)).s holds t in (the Sorts of A0).s; theorem :: MSAFREE4:44 for t being Element of A2 for p being Element of dom t holds t|p is Element of A2; theorem :: MSAFREE4:45 FreeGen X is GeneratorSet of A2; theorem :: MSAFREE4:46 for T being free_in_itself non-empty (X,S)-terms MSAlgebra over S for A being image of T for G being GeneratorSet of T st G = FreeGen X for f being ManySortedFunction of G, the Sorts of A ex h being ManySortedFunction of T,A st h is_homomorphism T,A & f = h||G; theorem :: MSAFREE4:47 canonical_homomorphism A2 is_epimorphism Free(S,X),A2 & for s being SortSymbol of S, t being Element of A2,s holds (canonical_homomorphism A2).s.t = t; theorem :: MSAFREE4:48 (canonical_homomorphism A2)**(canonical_homomorphism A2) = canonical_homomorphism A2; theorem :: MSAFREE4:49 A is Free(S,X)-Image; begin :: Satisfiability theorem :: MSAFREE4:50 for A being non-empty MSAlgebra over S for s being SortSymbol of S for t being Element of TermAlg S,s holds A |= t '=' t; theorem :: MSAFREE4:51 for A being non-empty MSAlgebra over S for s being SortSymbol of S for t1,t2 being Element of TermAlg S,s holds A |= t1 '=' t2 implies A |= t2 '=' t1; theorem :: MSAFREE4:52 for A being non-empty MSAlgebra over S for s being SortSymbol of S for t1,t2,t3 being Element of TermAlg S,s holds A |= t1 '=' t2 & A |= t2 '=' t3 implies A |= t1 '=' t3; theorem :: MSAFREE4:53 for A being non-empty MSAlgebra over S for o being OperSymbol of S for a1,a2 being FinSequence st a1 in Args(o,TermAlg S) & a2 in Args(o,TermAlg S) & for i being Nat st i in dom the_arity_of o for s being SortSymbol of S st s = (the_arity_of o).i for t1,t2 being Element of TermAlg S, s st t1 = a1.i & t2 = a2.i holds A |= t1 '=' t2 for t1,t2 being Element of TermAlg S, the_result_sort_of o st t1 = [o,the carrier of S]-tree a1 & t2 = [o,the carrier of S]-tree a2 holds A |= t1 '=' t2; definition let S; let T be EqualSet of S; let A be MSAlgebra over S; attr A is T-satisfying means :: MSAFREE4:def 11 A |= T; end; registration let S; let T be EqualSet of S; cluster T-satisfying non-empty trivial for MSAlgebra over S; end; registration let S; let T be EqualSet of S; let A be T-satisfying non-empty MSAlgebra over S; cluster A-Image -> T-satisfying for non-empty MSAlgebra over S; end; definition let S; let A be MSAlgebra over S; let T be EqualSet of S; let G be GeneratorSet of A; attr G is T-free means :: MSAFREE4:def 12 for B be T-satisfying non-empty MSAlgebra over S for f be ManySortedFunction of G, the Sorts of B ex h be ManySortedFunction of A, B st h is_homomorphism A,B & h || G = f; end; definition let S; let T be EqualSet of S; let A be MSAlgebra over S; attr A is T-free means :: MSAFREE4:def 13 ex G being GeneratorSet of A st G is T-free; end; definition let S; let A be MSAlgebra over S; func Equations(S,A) -> EqualSet of S means :: MSAFREE4:def 14 for s being SortSymbol of S holds it.s = {e where e is Element of (Equations S).s: A |= e}; end; theorem :: MSAFREE4:54 for A being MSAlgebra over S holds A |= Equations(S,A); registration let S; let A be non-empty MSAlgebra over S; cluster -> Equations(S,A)-satisfying for A-Image MSAlgebra over S; end; begin :: Term correspondence scheme :: MSAFREE4:sch 3 TermDefEx{ S()-> non empty non void ManySortedSign, X()-> non-empty ManySortedSet of S(), R(set,set)->set, F(set,set)->set}: ex F being ManySortedSet of S()-Terms X() st (for s being SortSymbol of S(), x being Element of X().s holds F.root-tree [x,s] = R(x,s)) & for o being OperSymbol of S(), p being ArgumentSeq of Sym(o,X()) holds F.(Sym(o,X())-tree p) = F(o,F*p); scheme :: MSAFREE4:sch 4 TermDefUniq{ S()-> non empty non void ManySortedSign, X()-> non-empty ManySortedSet of S(), R(set,set)->set, F(set,FinSequence)->set, F1,F2()->ManySortedSet of S()-Terms X()}: F1() = F2() provided (for s being SortSymbol of S(), x being Element of X().s holds F1().root-tree [x,s] = R(x,s)) and for o being OperSymbol of S(), p being ArgumentSeq of Sym(o,X()) holds F1().(Sym(o,X())-tree p) = F(o,F1()*p) and (for s being SortSymbol of S(), x being Element of X().s holds F2().root-tree [x,s] = R(x,s)) and for o being OperSymbol of S(), p being ArgumentSeq of Sym(o,X()) holds F2().(Sym(o,X())-tree p) = F(o,F2()*p); definition let S, X; let w be ManySortedFunction of X, (the carrier of S) --> NAT; let t be Function such that t is Element of Free(S,X); func #(t,w) -> Element of TermAlg S means :: MSAFREE4:def 15 ex F being ManySortedSet of S-Terms X st it = F.t & (for s being SortSymbol of S, x being Element of X.s holds F.root-tree [x,s] = root-tree [w.s.x,s]) & for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) holds F.(Sym(o,X)-tree p) = Sym(o,(the carrier of S)-->NAT)-tree(F*p); end; theorem :: MSAFREE4:55 for w being ManySortedFunction of X, (the carrier of S) --> NAT for F being ManySortedSet of S-Terms X st (for s being SortSymbol of S, x being Element of X.s holds F.root-tree [x,s] = root-tree [w.s.x,s]) & for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) holds F.(Sym(o,X)-tree p) = Sym(o,(the carrier of S)-->NAT)-tree(F*p) holds for t being Element of Free(S,X) holds F.t = #(t,w); registration let S, X; let G be non-empty MSSubset of Free(S,X); let s be SortSymbol of S; cluster -> Relation-like Function-like for Element of G.s; end; theorem :: MSAFREE4:56 for w being ManySortedFunction of X, (the carrier of S) --> NAT ex h being ManySortedFunction of Free(S,X), TermAlg S st h is_homomorphism Free(S,X), TermAlg S & for s being SortSymbol of S, t being Element of Free(S,X),s holds #(t,w) = h.s.t; theorem :: MSAFREE4:57 for w being ManySortedFunction of X, (the carrier of S) --> NAT for s being SortSymbol of S, x being Element of X.s holds #(root-tree [x,s], w) = root-tree [w.s.x, s]; theorem :: MSAFREE4:58 for w being ManySortedFunction of X, (the carrier of S) --> NAT for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) for q being FinSequence st dom q = dom p & for i being Nat, t being Element of Free(S,X) st i in dom p & t = p.i holds q.i = #(t,w) holds #(Sym(o,X)-tree p, w) = Sym(o,(the carrier of S)-->NAT)-tree q; theorem :: MSAFREE4:59 for Y being ManySortedSubset of X holds Free(S,Y) is MSSubAlgebra of Free(S,X); theorem :: MSAFREE4:60 for w being ManySortedFunction of X, (the carrier of S)-->NAT for t being Term of S,X holds #(t,w) is Element of Free(S, rngs w), the_sort_of t & #(t,w) is Element of TermAlg S, the_sort_of t; theorem :: MSAFREE4:61 for w being ManySortedFunction of X, (the carrier of S) --> NAT for F being ManySortedSet of S-Terms X st (for s being SortSymbol of S, x being Element of X.s holds F.root-tree [x,s] = root-tree [w.s.x,s]) & for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) holds F.(Sym(o,X)-tree p) = Sym(o,(the carrier of S)-->NAT)-tree(F*p) for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) holds F*p in Args(o, Free(S, rngs w)) & F*p in Args(o, Free(S, (the carrier of S)-->NAT)); theorem :: MSAFREE4:62 for w being ManySortedFunction of (the carrier of S)-->NAT, X ex h being ManySortedFunction of TermAlg S, A st h is_homomorphism TermAlg S, A & for s being SortSymbol of S, i being Nat holds h.s.root-tree [i,s] = root-tree [w.s.i, s]; theorem :: MSAFREE4:63 for w being ManySortedFunction of X, (the carrier of S)-->NAT ex h being ManySortedFunction of FreeGen X, the Sorts of TermAlg S st for s being SortSymbol of S, i being Element of X.s holds h.s.root-tree [i,s] = root-tree [w.s.i, s]; begin :: Free algebras reserve X0 for non-empty countable ManySortedSet of S; reserve A0 for all_vars_including inheriting_operations free_in_itself (X0,S)-terms MSAlgebra over S; theorem :: MSAFREE4:64 for h being ManySortedFunction of TermAlg S, A0 st h is_homomorphism TermAlg S, A0 for w being ManySortedFunction of X0, (the carrier of S)-->NAT st w is "1-1" ex Y being non-empty ManySortedSubset of (the carrier of S)-->NAT, B being MSSubset of TermAlg S, ww being ManySortedFunction of Free(S,Y), A0, g being ManySortedFunction of A0,A0 st Y = rngs w & B = the Sorts of Free(S,Y) & FreeGen rngs w c= B & ww is_homomorphism Free(S,Y), A0 & g is_homomorphism A0,A0 & h||B = g**ww & for s being SortSymbol of S, i being Nat st i in Y.s ex x being Element of X0.s st w.s.x = i & ww.s.root-tree [i,s] = root-tree [x, s]; theorem :: MSAFREE4:65 for h being ManySortedFunction of Free(S,X), A st h is_homomorphism Free(S,X), A ex g being ManySortedFunction of A,A st g is_homomorphism A,A & h = g**canonical_homomorphism A; theorem :: MSAFREE4:66 for o being OperSymbol of S for x being Element of Args(o,A) holds for x0 being Element of Args(o,Free(S,X)) st x0 = x holds (canonical_homomorphism A)#x0 = x; theorem :: MSAFREE4:67 for o being OperSymbol of S for x being Element of Args(o,A) holds Den(o,A).x = (canonical_homomorphism A).(the_result_sort_of o).(Den(o,Free(S,X)).x); theorem :: MSAFREE4:68 for h being ManySortedFunction of Free(S,X), A st h is_homomorphism Free(S,X), A for o being OperSymbol of S for x being Element of Args(o,A) holds h.(the_result_sort_of o).(Den(o,A).x) = h.(the_result_sort_of o).(Den(o,Free(S,X)).x); theorem :: MSAFREE4:69 for h being ManySortedFunction of Free(S,X), A st h is_homomorphism Free(S,X), A for o being OperSymbol of S for x being Element of Args(o,Free(S,X)) holds h.(the_result_sort_of o).(Den(o,Free(S,X)).x) = h.(the_result_sort_of o).(Den(o,Free(S,X)). ((canonical_homomorphism A)#x)); theorem :: MSAFREE4:70 for X0,Y0 being non-empty countable ManySortedSet of S for A being all_vars_including inheriting_operations (X0,S)-terms MSAlgebra over S for h being ManySortedFunction of Free(S,Y0), A st h is_homomorphism Free(S,Y0), A ex g being ManySortedFunction of Free(S,Y0),Free(S,X0) st g is_homomorphism Free(S,Y0),Free(S,X0) & h = (canonical_homomorphism A)**g & for G being GeneratorSet of Free(S,Y0) st G = FreeGen Y0 holds g||G = h||G; theorem :: MSAFREE4:71 for w being ManySortedFunction of X0, (the carrier of S)-->NAT for s being SortSymbol of S for t being Element of Free(S,X0),s for t1,t2 being Element of TermAlg S, s st t1 = #(t,w) & t2 = #((canonical_homomorphism A0).s.t,w) holds A0 |= t1 '=' t2; theorem :: MSAFREE4:72 for w being ManySortedFunction of X0, (the carrier of S)-->NAT for o being OperSymbol of S for p being Element of Args(o,Free(S,X0)) for q being Element of Args(o,A0) st (canonical_homomorphism A0)#p = q for t1,t2 being Term of S,X0 st t1 = Den(o,Free(S,X0)).p & t2 = Den(o,A0).q for t3,t4 being Element of TermAlg S, the_result_sort_of o st t3 = #(t1,w) & t4 = #(t2,w) holds A0 |= t3 '=' t4; theorem :: MSAFREE4:73 for w being ManySortedFunction of X0, (the carrier of S)-->NAT st w is "1-1" ex g being ManySortedFunction of TermAlg S, Free(S,X0) st g is_homomorphism TermAlg S, Free(S,X0) & for s being SortSymbol of S for t being Element of Free(S,X0),s holds g.s. #(t,w) = t; theorem :: MSAFREE4:74 for B being non-empty MSAlgebra over S for h being ManySortedFunction of Free(S,X0),B st h is_homomorphism Free(S,X0),B for w being ManySortedFunction of X0, (the carrier of S)-->NAT st w is "1-1" for s being SortSymbol of S for t1,t2 being Element of Free(S,X0),s for t3,t4 being Element of TermAlg S, s st t3 = #(t1,w) & t4 = #(t2,w) holds B |= t3 '=' t4 implies h.s.t1 = h.s.t2; theorem :: MSAFREE4:75 for G being GeneratorSet of A0 st G = FreeGen X0 holds G is Equations(S,A0)-free; theorem :: MSAFREE4:76 A0 is Equations(S,A0)-free; begin :: Algebra of normal forms definition let I be set; let X,Y be ManySortedSet of I; let R be ManySortedRelation of X,Y; let x be object; redefine func R.x -> Relation of X.x,Y.x; end; definition let I be set; let X be ManySortedSet of I; let R be ManySortedRelation of X; attr R is terminating means :: MSAFREE4:def 16 for x being set st x in I holds R.x is strongly-normalizing; attr R is with_UN_property means :: MSAFREE4:def 17 for x being set st x in I holds R.x is with_UN_property; end; registration cluster -> strongly-normalizing with_UN_property for empty set; end; theorem :: MSAFREE4:77 for I being set for A being ManySortedSet of I ex R being ManySortedRelation of A st R = I-->{} & R is terminating; registration let I be set; let X be ManySortedSet of I; cluster empty-yielding -> with_UN_property terminating for ManySortedRelation of X; cluster empty-yielding for ManySortedRelation of X; end; registration let I be set; let X be ManySortedSet of I; let R be terminating ManySortedRelation of X; let i be object; cluster R.i -> strongly-normalizing for Relation; end; registration let I be set; let X be ManySortedSet of I; let R be with_UN_property ManySortedRelation of X; let i be object; cluster R.i -> with_UN_property for Relation; end; definition let S,X; let R be ManySortedRelation of Free(S,X); attr R is NF-var means :: MSAFREE4:def 18 for s being SortSymbol of S for x being Element of (FreeGen X).s holds x is_a_normal_form_wrt R.s; end; theorem :: MSAFREE4:78 x is_a_normal_form_wrt {}; registration let S,X; cluster empty-yielding -> NF-var invariant stable for ManySortedRelation of Free(S,X); end; registration let S,X; cluster NF-var terminating with_UN_property for invariant stable ManySortedRelation of Free(S,X); end; scheme :: MSAFREE4:sch 5 A {x1,x2()->set, R()->Relation, P[set] }: P[x2()] provided P[x1()] and R() reduces x1(),x2() and for y,z being set st R() reduces x1(),y & [y,z] in R() & P[y] holds P[z]; scheme :: MSAFREE4:sch 6 B {x1,x2()->set, R()->Relation, P[set] }: P[x1()] provided P[x2()] and R() reduces x1(),x2() and for y,z being set st [y,z] in R() & P[z] holds P[y]; definition let X be non empty set; let R be with_UN_property strongly-normalizing Relation of X; let x be Element of X; redefine func nf(x,R) -> Element of X; end; definition let I be non empty set; let X be non-empty ManySortedSet of I; let R be with_UN_property terminating ManySortedRelation of X; func NForms R -> non-empty ManySortedSubset of X means :: MSAFREE4:def 19 for i being Element of I holds it.i = the set of all nf(x,R.i) where x is Element of X.i; end; scheme :: MSAFREE4:sch 7 MSFLambda {B()->non empty set,D(object)->non empty set, F(object,object)->set}: ex f being ManySortedFunction of B() st for o being Element of B() holds dom (f.o) = D(o) & for x being Element of D(o) holds f.o.x = F(o,x); definition let S,X; let R be terminating with_UN_property invariant stable ManySortedRelation of Free(S,X); func NFAlgebra R -> non-empty strict MSAlgebra over S means :: MSAFREE4:def 20 the Sorts of it = NForms R & for o being OperSymbol of S, a being Element of Args(o,it) holds Den(o,it).a = nf (Den(o,Free(S,X)).a, R.the_result_sort_of o); end; theorem :: MSAFREE4:79 for R being terminating with_UN_property invariant stable ManySortedRelation of Free(S,X) for a being SortSymbol of S st x in (NForms R).a holds nf(x,R.a) = x; theorem :: MSAFREE4:80 for R being terminating with_UN_property invariant stable ManySortedRelation of Free(S,X) for g being ManySortedFunction of Free(S,X),Free(S,X) st g is_homomorphism Free(S,X),Free(S,X) for s being SortSymbol of S for a being Element of Free(S,X),s holds nf(g.s.nf(a,R.s), R.s) = nf(g.s.a, R.s); theorem :: MSAFREE4:81 for p being FinSequence holds p/^0 = p & for i being Nat st i >= len p holds p/^i = {}; theorem :: MSAFREE4:82 for p,q being FinSequence holds (p^<*x*>^q)+*(len p+1,y) = p^<*y*>^q; theorem :: MSAFREE4:83 for p being FinSequence, i being Nat st i+1 <= len p holds p|(i+1) = (p|i)^<*p.(i+1)*>; theorem :: MSAFREE4:84 for p being FinSequence, i being Nat st i+1 <= len p holds p/^i = <*p.(i+1)*>^(p/^(i+1)); theorem :: MSAFREE4:85 for R being terminating with_UN_property invariant stable ManySortedRelation of Free(S,X) for g being ManySortedFunction of Free(S,X),Free(S,X) st g is_homomorphism Free(S,X),Free(S,X) for h being ManySortedFunction of NFAlgebra R, NFAlgebra R st for s being SortSymbol of S, x being Element of NFAlgebra R,s holds h.s.x = nf(g.s.x,R.s) for s being SortSymbol of S for o being OperSymbol of S st s = the_result_sort_of o for x being Element of Args(o,NFAlgebra R) for y being Element of Args(o,Free(S,X)) st x = y holds nf(Den(o,NFAlgebra R).(h#x),R.s) = nf(Den(o,Free(S,X)).(g#y),R.s); registration let S,X; let R be terminating with_UN_property invariant stable ManySortedRelation of Free(S,X); cluster NFAlgebra R -> (X,S)-terms; end; registration let S,X; let R be NF-var terminating with_UN_property invariant stable ManySortedRelation of Free(S,X); cluster NFAlgebra R -> all_vars_including inheriting_operations free_in_itself; end;