Copyright (c) 2002 Association of Mizar Users
environ vocabulary FUNCT_1, PBOOLE, TDGROUP, CARD_3, RELAT_1, MSUALG_2, PRALG_1, REALSET1, BOOLE, ZF_REFLE, PROB_1, TARSKI, AMI_1, MSUALG_1, ALG_1, FINSEQ_1, QC_LANG1, LANG1, DTCONSTR, TREES_4, TREES_2, TREES_3, FUNCT_6, MCART_1, UNIALG_2, GROUP_6, MSUALG_3, MSAFREE, MSUALG_4, NATTRA_1, FINSEQ_4, OSALG_1, SEQM_3, YELLOW18, COH_SP, EQREL_1, RELAT_2, FUNCT_5, CARD_LAR, CARD_5, OSALG_2, OSALG_4, OSAFREE, PARTFUN1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, NAT_1, RELAT_1, RELSET_1, STRUCT_0, FUNCT_1, MCART_1, PARTFUN1, FUNCT_2, FINSEQ_1, FINSEQ_2, RELAT_2, TREES_2, PROB_1, CARD_3, EQREL_1, FINSEQ_4, LANG1, TREES_3, FUNCT_6, TREES_4, FUNCT_5, DTCONSTR, ORDERS_1, ORDERS_3, PBOOLE, PRALG_1, MSUALG_1, MSUALG_2, MSUALG_3, MSUALG_4, OSALG_1, OSALG_2, OSALG_3, OSALG_4, MSAFREE, YELLOW18; constructors NAT_1, MSUALG_3, FINSOP_1, FINSEQ_4, FINSEQOP, ORDERS_3, OSALG_2, OSALG_3, OSALG_4, MSAFREE3, MEMBERED, YELLOW18; clusters SUBSET_1, PBOOLE, TREES_3, TREES_4, DTCONSTR, PRALG_1, MSUALG_1, RELSET_1, STRUCT_0, XBOOLE_0, MSUALG_4, MSUALG_9, OSALG_1, OSALG_4, MSAFREE, NAT_1, MEMBERED, PARTFUN1, NUMBERS, ORDINAL2; requirements NUMERALS, BOOLE, SUBSET; definitions TARSKI, XBOOLE_0, PBOOLE, MSUALG_3, STRUCT_0, OSALG_1, OSALG_3, OSALG_4; theorems TARSKI, FUNCT_1, FUNCT_2, MCART_1, ZFMISC_1, PBOOLE, CARD_3, MSUALG_1, MSUALG_2, MSUALG_3, PRALG_1, RELAT_1, LANG1, DTCONSTR, FINSEQ_1, TREES_4, FINSEQ_4, TREES_1, TREES_2, ALG_1, DOMAIN_1, PROB_1, RELSET_1, XBOOLE_0, XBOOLE_1, OSALG_1, OSALG_2, OSALG_3, OSALG_4, MSAFREE, MSUALG_6, MSAFREE2, CARD_5, FINSEQ_2, FINSEQ_3, MSUALG_9, MSUALG_4, EQREL_1, FUNCT_5, ORDERS_1, RELAT_2, PARTFUN1; schemes ZFREFLE1, FUNCT_1, RELSET_1, MSUALG_2, DTCONSTR, COMPTS_1, XBOOLE_0, FUNCT_2, MSUALG_1; begin reserve S for OrderSortedSign; :: REVISE: should rather be attribute :: changing to MSSubset and its OSCl, to make free algebras easier :: no good way how to retypeOSCL into OSSubset now? definition let S be OrderSortedSign, U0 be OSAlgebra of S; mode OSGeneratorSet of U0 -> MSSubset of U0 means :Def1: for O being OSSubset of U0 st O = OSCl it holds the Sorts of GenOSAlg(O) = the Sorts of U0; existence proof set A = the Sorts of U0; reconsider A as MSSubset of U0 by MSUALG_2:def 1; A1: A is OrderSortedSet of S by OSALG_1:17; then reconsider A as OSSubset of U0 by OSALG_2:def 2; take A; A2: A = OSCl A by A1,OSALG_2:14; set G = GenOSAlg(A); A is OSSubset of G by OSALG_2:def 13; then A3: A c= the Sorts of G by MSUALG_2:def 1; the Sorts of G is MSSubset of U0 by MSUALG_2:def 10; then the Sorts of G c= A by MSUALG_2:def 1; hence thesis by A2,A3,PBOOLE:def 13; end; end; theorem for S be OrderSortedSign, U0 be strict non-empty OSAlgebra of S, A be MSSubset of U0 holds A is OSGeneratorSet of U0 iff for O being OSSubset of U0 st O = OSCl A holds GenOSAlg(O) = U0 proof let S be OrderSortedSign, U0 be strict non-empty OSAlgebra of S, A be MSSubset of U0; thus A is OSGeneratorSet of U0 implies for O being OSSubset of U0 st O = OSCl A holds GenOSAlg(O) = U0 proof assume A1: A is OSGeneratorSet of U0; let O be OSSubset of U0 such that A2: O = OSCl A; reconsider U1 = U0 as MSSubAlgebra of U0 by MSUALG_2:6; the Sorts of GenOSAlg(O) = the Sorts of U1 by A1,A2,Def1; hence thesis by MSUALG_2:10; end; assume A3: for O being OSSubset of U0 st O = OSCl A holds GenOSAlg(O) = U0; let O be OSSubset of U0 such that A4: O = OSCl A; thus the Sorts of GenOSAlg(O) = the Sorts of U0 by A3,A4; end; :: renaming to osfree - if OSGeneratorSet and GeneratorSet become :: attributes, Mizar would be puzzled :: we do this for monotone osas only, though more general approach is possible definition let S; let U0 be monotone OSAlgebra of S; let IT be OSGeneratorSet of U0; attr IT is osfree means for U1 be monotone non-empty OSAlgebra of S for f be ManySortedFunction of IT,the Sorts of U1 ex h be ManySortedFunction of U0,U1 st h is_homomorphism U0,U1 & h is order-sorted & h || IT = f; end; definition let S be OrderSortedSign; let IT be monotone OSAlgebra of S; attr IT is osfree means ex G being OSGeneratorSet of IT st G is osfree; end; begin :: :: Construction of Free Order Sorted Algebras for Given Signature :: definition let S be OrderSortedSign, X be ManySortedSet of S; func OSREL(X) -> Relation of ([:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X)), (([:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X))*) means :Def4: for a be Element of [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X), b be Element of ([:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X))* holds [a,b] in it iff a in [:the OperSymbols of S,{the carrier of S}:] & for o be OperSymbol of S st [o,the carrier of S] = a holds len b = len (the_arity_of o) & for x be set st x in dom b holds (b.x in [:the OperSymbols of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = b.x holds (the_result_sort_of o1) <= (the_arity_of o)/.x) & (b.x in Union (coprod X) implies ex i being Element of S st i <= (the_arity_of o)/.x & b.x in coprod(i,X)); existence proof set O = [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X); defpred P[Element of O, Element of O*] means $1 in [:the OperSymbols of S,{the carrier of S}:] & for o be OperSymbol of S st [o,the carrier of S] = $1 holds len $2 = len (the_arity_of o) & for x be set st x in dom $2 holds ($2.x in [:the OperSymbols of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = $2.x holds the_result_sort_of o1 <= (the_arity_of o)/.x) & ($2.x in Union (coprod X) implies ex i being Element of S st i <= (the_arity_of o)/.x & $2.x in coprod(i,X)); consider R be Relation of O,O* such that A1: for a be Element of O, b be Element of O* holds [a,b] in R iff P[a,b] from Rel_On_Dom_Ex; take R; let a be Element of O, b be Element of O*; thus [a,b] in R implies a in [:the OperSymbols of S,{the carrier of S}:] & for o be OperSymbol of S st [o,the carrier of S] = a holds len b = len (the_arity_of o) & for x be set st x in dom b holds (b.x in [:the OperSymbols of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = b.x holds the_result_sort_of o1 <= (the_arity_of o)/.x) & (b.x in Union (coprod X) implies ex i being Element of S st i <= (the_arity_of o)/.x & b.x in coprod(i,X)) by A1; assume a in [:the OperSymbols of S,{the carrier of S}:] & for o be OperSymbol of S st [o,the carrier of S] = a holds len b = len (the_arity_of o) & for x be set st x in dom b holds (b.x in [:the OperSymbols of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = b.x holds the_result_sort_of o1 <= (the_arity_of o)/.x) & (b.x in Union (coprod X) implies ex i being Element of S st i <= (the_arity_of o)/.x & b.x in coprod(i,X)); hence thesis by A1; end; uniqueness proof set O = [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X); let R,P be Relation of O,O*; assume that A2: for a be Element of O, b be Element of O* holds [a,b] in R iff a in [:the OperSymbols of S,{the carrier of S}:] & for o be OperSymbol of S st [o,the carrier of S] = a holds len b = len (the_arity_of o) & for x be set st x in dom b holds (b.x in [:the OperSymbols of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = b.x holds the_result_sort_of o1 <= (the_arity_of o)/.x) & (b.x in Union (coprod X) implies ex i being Element of S st i <= (the_arity_of o)/.x & b.x in coprod(i,X)) and A3: for a be Element of O, b be Element of O* holds [a,b] in P iff a in [:the OperSymbols of S,{the carrier of S}:] & for o be OperSymbol of S st [o,the carrier of S] = a holds len b = len (the_arity_of o) & for x be set st x in dom b holds (b.x in [:the OperSymbols of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = b.x holds the_result_sort_of o1 <= (the_arity_of o)/.x) & (b.x in Union (coprod X) implies ex i being Element of S st i <= (the_arity_of o)/.x & b.x in coprod(i,X)); for x,y be set holds [x,y] in R iff [x,y] in P proof let x,y be set; thus [x,y] in R implies [x,y] in P proof assume A4: [x,y] in R; then reconsider a = x as Element of O by ZFMISC_1:106; reconsider b = y as Element of O* by A4,ZFMISC_1:106; [a,b] in R by A4; then a in [:the OperSymbols of S,{the carrier of S}:] & for o be OperSymbol of S st [o,the carrier of S] = a holds len b = len (the_arity_of o) & for x be set st x in dom b holds (b.x in [:the OperSymbols of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = b.x holds the_result_sort_of o1 <= (the_arity_of o)/.x) & (b.x in Union (coprod X) implies ex i being Element of S st i <= (the_arity_of o)/.x & b.x in coprod(i,X)) by A2; hence thesis by A3; end; assume A5: [x,y] in P; then reconsider a = x as Element of O by ZFMISC_1:106; reconsider b = y as Element of O* by A5,ZFMISC_1:106; [a,b] in P by A5; then a in [:the OperSymbols of S,{the carrier of S}:] & for o be OperSymbol of S st [o,the carrier of S] = a holds len b = len (the_arity_of o) & for x be set st x in dom b holds (b.x in [:the OperSymbols of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = b.x holds the_result_sort_of o1 <= (the_arity_of o)/.x) & (b.x in Union (coprod X) implies ex i being Element of S st i <= (the_arity_of o)/.x & b.x in coprod(i,X)) by A3; hence thesis by A2; end; hence thesis by RELAT_1:def 2; end; end; reserve S for OrderSortedSign, X for ManySortedSet of S, o for OperSymbol of S, b for Element of ([:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X))*; theorem Th2: [[o,the carrier of S],b] in OSREL(X) iff len b = len (the_arity_of o) & for x be set st x in dom b holds (b.x in [:the OperSymbols of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = b.x holds (the_result_sort_of o1) <= (the_arity_of o)/.x) & (b.x in Union (coprod X) implies ex i being Element of S st i <= (the_arity_of o)/.x & b.x in coprod(i,X)) proof defpred P[OperSymbol of S,Element of ([:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X))*] means len $2 = len (the_arity_of $1) & for x be set st x in dom $2 holds ($2.x in [:the OperSymbols of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = $2.x holds the_result_sort_of o1 <= (the_arity_of $1)/.x) & ($2.x in Union (coprod X) implies ex i being Element of S st i <= (the_arity_of $1)/.x & b.x in coprod(i,X)); set a = [o,the carrier of S]; the carrier of S in {the carrier of S} by TARSKI:def 1; then A1: a in [:the OperSymbols of S,{the carrier of S}:] by ZFMISC_1:106; then reconsider a as Element of [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X) by XBOOLE_0:def 2; thus [[o,the carrier of S],b] in OSREL(X) implies P[o,b] proof assume [[o,the carrier of S],b] in OSREL(X); then for o1 be OperSymbol of S st [o1,the carrier of S] = a holds P[o1,b] by Def4; hence thesis; end; assume A2: P[o,b]; now let o1 be OperSymbol of S; assume [o1,the carrier of S] = a; then o1 = o by ZFMISC_1:33; hence P[o1,b] by A2; end; hence thesis by A1,Def4; end; definition let S be OrderSortedSign, X be ManySortedSet of S; func DTConOSA(X) -> DTConstrStr equals :Def5: DTConstrStr (# [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X), OSREL(X) #); correctness; end; definition let S be OrderSortedSign, X be ManySortedSet of S; cluster DTConOSA(X) -> strict non empty; coherence proof DTConOSA(X) = DTConstrStr (# [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X), OSREL(X) #) by Def5; hence DTConOSA X is strict & the carrier of DTConOSA(X) is non empty; end; end; theorem Th3: for S be OrderSortedSign, X be non-empty ManySortedSet of S holds NonTerminals(DTConOSA(X)) = [:the OperSymbols of S,{the carrier of S}:] & Terminals (DTConOSA(X)) = Union (coprod X) proof let S be OrderSortedSign, X be non-empty ManySortedSet of S; A1: Union(coprod X) misses [:the OperSymbols of S,{the carrier of S}:] by MSAFREE:4; set D = DTConOSA(X), A = [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod (X qua ManySortedSet of S)); A2: D = DTConstrStr (# A , OSREL(X) #) by Def5; A3: the carrier of D = (Terminals D) \/ (NonTerminals D) & (Terminals D) misses (NonTerminals D) by DTCONSTR:8,LANG1:1; thus A4: NonTerminals D c= [:the OperSymbols of S,{the carrier of S}:] proof let x be set; assume x in NonTerminals D; then x in { s where s is Symbol of D: ex n being FinSequence st s ==> n} by LANG1:def 3; then consider s be Symbol of D such that A5: s = x & ex n being FinSequence st s ==> n; consider n be FinSequence such that A6: s ==> n by A5; A7: [s,n] in the Rules of D by A6,LANG1:def 1; reconsider s as Element of A by A2; reconsider n as Element of A* by A2,A7,ZFMISC_1:106; [s,n] in OSREL X by A2,A6,LANG1:def 1; hence thesis by A5,Def4; end; thus A8: [:the OperSymbols of S,{the carrier of S}:] c= NonTerminals D proof let x be set; assume A9: x in [:the OperSymbols of S,{the carrier of S}:]; then consider o being Element of the OperSymbols of S, x2 being Element of {the carrier of S} such that A10: x = [o,x2] by DOMAIN_1:9; A11: the carrier of S = x2 by TARSKI:def 1; then reconsider xa = [o,the carrier of S] as Element of (the carrier of D) by A2,A9,A10,XBOOLE_0:def 2; set O = the_arity_of o; defpred P[set,set] means ex i being Element of S st i <= O/.$1 & $2 in coprod(i,X); A12: for a be set st a in Seg len O ex b be set st P[a,b] proof let a be set; assume a in Seg len O; then A13: a in dom O by FINSEQ_1:def 3; then A14: O.a in rng O & rng O c= the carrier of S by FINSEQ_1:def 4,FUNCT_1:def 5; then X.(O.a) is non empty by PBOOLE:def 16; then consider x be set such that A15: x in X.(O.a) by XBOOLE_0:def 1; take y = [x,O.a]; A16: y in coprod(O.a,X) by A14,A15,MSAFREE:def 2; take O/.a; thus thesis by A13,A16,FINSEQ_4:def 4; end; consider b be Function such that A17: dom b = Seg len O & for a be set st a in Seg len O holds P[a,b.a] from NonUniqFuncEx(A12); reconsider b as FinSequence by A17,FINSEQ_1:def 2; rng b c= A proof let a be set; assume a in rng b; then consider c be set such that A18: c in dom b & b.c = a by FUNCT_1:def 5; consider i being Element of S such that A19: i <= O/.c & a in coprod(i,X) by A17,A18; dom coprod(X) = the carrier of S by PBOOLE:def 3; then (coprod(X)).(i) in rng coprod(X) by FUNCT_1:def 5; then coprod(i,X) in rng coprod(X) by MSAFREE:def 3; then a in union rng coprod(X) by A19,TARSKI:def 4; then a in Union coprod(X) by PROB_1:def 3; hence thesis by XBOOLE_0:def 2; end; then reconsider b as FinSequence of A by FINSEQ_1:def 4; reconsider b as Element of A* by FINSEQ_1:def 11; A20: len b = len O by A17,FINSEQ_1:def 3; now let c be set; assume c in dom b; then consider i being Element of S such that A21: i <= O/.c & b.c in coprod(i,X) by A17; dom coprod(X) = the carrier of S by PBOOLE:def 3; then (coprod(X)).(i) in rng coprod(X) by FUNCT_1:def 5; then coprod(i,X) in rng coprod(X) by MSAFREE:def 3; then b.c in union rng coprod(X) by A21,TARSKI:def 4; then b.c in Union coprod(X) by PROB_1:def 3; hence b.c in [:the OperSymbols of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = b.c holds the_result_sort_of o1 <= O/.c by A1,XBOOLE_0:3; assume b.c in Union (coprod X); thus ex i being Element of S st i <= O/.c & b.c in coprod(i,X) by A21; end; then [xa,b] in OSREL(X) by A20,Th2; then xa ==> b by A2,LANG1:def 1; then xa in { t where t is Symbol of D: ex n be FinSequence st t ==> n}; hence thesis by A10,A11,LANG1:def 3; end; thus Terminals D c= Union (coprod X) proof let x be set; assume A22: x in Terminals D; then A23: x in A by A2,A3,XBOOLE_0:def 2; not x in [:the OperSymbols of S,{the carrier of S}:] by A3,A8,A22,XBOOLE_0:3; hence thesis by A23,XBOOLE_0:def 2; end; let x be set; assume A24: x in Union (coprod X); then x in A by XBOOLE_0:def 2; then x in Terminals D or x in NonTerminals D by A2,A3,XBOOLE_0:def 2; hence thesis by A1,A4,A24,XBOOLE_0:3; end; reserve x for set; definition let S be OrderSortedSign, X be non-empty ManySortedSet of S; cluster DTConOSA(X) -> with_terminals with_nonterminals with_useful_nonterminals; coherence proof set D = DTConOSA(X), A = [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod (X qua ManySortedSet of S)); A1: Union (coprod X) misses [:the OperSymbols of S,{the carrier of S}:] by MSAFREE:4; A2: Terminals D = Union (coprod X) & NonTerminals D = [:the OperSymbols of S,{the carrier of S}:] by Th3; A3: D = DTConstrStr (# A , OSREL(X) #) by Def5; for nt being Symbol of D st nt in NonTerminals D ex p being FinSequence of TS(D) st nt ==> roots p proof let nt be Symbol of D; assume nt in NonTerminals D; then consider o being Element of the OperSymbols of S, x2 being Element of {the carrier of S} such that A4: nt = [o,x2] by A2,DOMAIN_1:9; A5: the carrier of S = x2 by TARSKI:def 1; set O = the_arity_of o; defpred P[set,set] means ex i being Element of S st i <= O/.$1 & $2 in coprod(i,X); A6: for a be set st a in Seg len O ex b be set st P[a,b] proof let a be set; assume a in Seg len O; then A7: a in dom O by FINSEQ_1:def 3; then A8: O.a in rng O & rng O c= the carrier of S by FINSEQ_1:def 4,FUNCT_1:def 5; then X.(O.a) is non empty by PBOOLE:def 16; then consider x be set such that A9: x in X.(O.a) by XBOOLE_0:def 1; take y = [x,O.a]; A10: y in coprod(O.a,X) by A8,A9,MSAFREE:def 2; take O/.a; thus thesis by A7,A10,FINSEQ_4:def 4; end; consider b be Function such that A11: dom b = Seg len O & for a be set st a in Seg len O holds P[a,b.a] from NonUniqFuncEx(A6); reconsider b as FinSequence by A11,FINSEQ_1:def 2; A12: rng b c= A proof let a be set; assume a in rng b; then consider c be set such that A13: c in dom b & b.c = a by FUNCT_1:def 5; consider i being Element of S such that A14: i <= O/.c & a in coprod(i,X) by A11,A13; dom coprod(X) = the carrier of S by PBOOLE:def 3; then (coprod(X)).i in rng coprod(X) by FUNCT_1:def 5; then coprod(i,X) in rng coprod(X) by MSAFREE:def 3; then a in union rng coprod(X) by A14,TARSKI:def 4; then a in Union coprod(X) by PROB_1:def 3; hence thesis by XBOOLE_0:def 2; end; then reconsider b as FinSequence of A by FINSEQ_1:def 4; reconsider b as Element of A* by FINSEQ_1:def 11; A15: len b = len O by A11,FINSEQ_1:def 3; now let c be set; assume c in dom b; then consider i being Element of S such that A16: i <= O/.c & b.c in coprod(i,X) by A11; dom coprod(X) = the carrier of S by PBOOLE:def 3; then (coprod(X)).i in rng coprod(X) by FUNCT_1:def 5; then coprod(i,X) in rng coprod(X) by MSAFREE:def 3; then b.c in union rng coprod(X) by A16,TARSKI:def 4; then b.c in Union coprod(X) by PROB_1:def 3; hence b.c in [:the OperSymbols of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = b.c holds the_result_sort_of o1 <= O/.c by A1,XBOOLE_0:3; assume b.c in Union (coprod X); thus ex i being Element of S st i <= O/.c & b.c in coprod(i,X) by A16; end; then [nt,b] in OSREL(X) by A4,A5,A15,Th2; then A17: nt ==> b by A3,LANG1:def 1; deffunc F(set) = root-tree (b.$1); consider f be Function such that A18: dom f = dom b & for x st x in dom b holds f.x = F(x) from Lambda; reconsider f as FinSequence by A11,A18,FINSEQ_1:def 2; rng f c= TS(D) proof let x; assume x in rng f; then consider y be set such that A19: y in dom f & f.y = x by FUNCT_1:def 5; A20: x = root-tree(b.y) by A18,A19; b.y in rng b by A18,A19,FUNCT_1:def 5; then reconsider a = b.y as Symbol of D by A3,A12; consider i being Element of S such that A21: i <= O/.y & b.y in coprod(i,X) by A11,A18,A19; dom coprod(X) = the carrier of S by PBOOLE:def 3; then (coprod(X)).(i) in rng coprod(X) by FUNCT_1:def 5; then coprod(i,X) in rng coprod(X) by MSAFREE:def 3; then b.y in union rng coprod(X) by A21,TARSKI:def 4; then a in Terminals D by A2,PROB_1:def 3; hence thesis by A20,DTCONSTR:def 4; end; then reconsider f as FinSequence of TS(D) by FINSEQ_1:def 4; take f; A22: dom (roots f) = dom f by DTCONSTR:def 1; for x st x in dom b holds (roots f).x = b.x proof let x; assume A23: x in dom b; then A24: f.x = root-tree (b.x) by A18; reconsider i = x as Nat by A23; consider T be DecoratedTree such that A25: T = f.i & (roots f).i = T.{} by A18,A23,DTCONSTR:def 1; thus thesis by A24,A25,TREES_4:3; end; hence thesis by A17,A18,A22,FUNCT_1:9; end; hence thesis by A2,DTCONSTR:def 6,def 7,def 8; end; end; theorem Th4: for S be OrderSortedSign, X be non-empty ManySortedSet of S, t be set holds t in Terminals DTConOSA(X) iff ex s be Element of S, x be set st x in X.s & t = [x,s] proof let S be OrderSortedSign, X be non-empty ManySortedSet of S, t be set; set D = DTConOSA(X); A1: Terminals D = Union (coprod X) by Th3 .= union rng (coprod X) by PROB_1:def 3; thus t in Terminals D implies ex s be Element of S, x be set st x in X.s & t = [x,s] proof assume t in Terminals D; then consider A be set such that A2: t in A & A in rng(coprod X) by A1,TARSKI:def 4; consider s be set such that A3: s in dom (coprod X) & (coprod X).s = A by A2,FUNCT_1:def 5; reconsider s as Element of S by A3,PBOOLE:def 3; take s; (coprod X).s = coprod(s,X) by MSAFREE:def 3; then consider x be set such that A4: x in X.s & t = [x,s] by A2,A3,MSAFREE:def 2; take x; thus thesis by A4; end; given s be Element of S, x be set such that A5: x in X.s & t = [x,s]; t in coprod(s,X) by A5,MSAFREE:def 2; then A6: t in (coprod X).s by MSAFREE:def 3; dom(coprod X) = the carrier of S by PBOOLE:def 3; then (coprod X).s in rng (coprod X) by FUNCT_1:def 5; hence thesis by A1,A6,TARSKI:def 4; end; :: have to rename definition let S be OrderSortedSign, X be non-empty ManySortedSet of S, o be OperSymbol of S; func OSSym(o,X) ->Symbol of DTConOSA(X) equals :Def6: [o,the carrier of S]; coherence proof the carrier of S in {the carrier of S} by TARSKI:def 1; then [o,the carrier of S] in [:the OperSymbols of S,{the carrier of S}:] by ZFMISC_1:106; then [o,the carrier of S] in NonTerminals (DTConOSA X) by Th3; hence [o,the carrier of S] is Symbol of DTConOSA(X); end; end; :: originally FreeSort, but it is not a good name in order-sorted context definition let S be OrderSortedSign, X be non-empty ManySortedSet of S, s be Element of S; func ParsedTerms(X,s) -> Subset of TS(DTConOSA(X)) equals :Def7: {a where a is Element of TS(DTConOSA(X)): (ex s1 being Element of S, x be set st s1 <= s & x in X.s1 & a = root-tree [x,s1]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o <= s}; coherence proof set A = {a where a is Element of TS(DTConOSA(X)): (ex s1 being Element of S, x be set st s1 <= s & x in X.s1 & a = root-tree [x,s1]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o <= s}; A c= TS(DTConOSA(X)) proof let x be set; assume x in A; then consider a be Element of TS(DTConOSA(X)) such that A1: x = a and (ex s1 being Element of S, x be set st s1 <= s & x in X.s1 & a = root-tree [x,s1]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o <= s; thus thesis by A1; end; hence thesis; end; end; definition let S be OrderSortedSign, X be non-empty ManySortedSet of S, s be Element of S; cluster ParsedTerms(X,s) -> non empty; coherence proof set A = {a where a is Element of TS(DTConOSA(X)): (ex s1 being Element of S, x be set st s1 <= s & x in X.s1 & a = root-tree [x,s1]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o <= s}; consider x be set such that A1: x in X.s by XBOOLE_0:def 1; set a = [x,s]; A2: a in coprod(s,X) by A1,MSAFREE:def 2; A3: (Terminals (DTConOSA(X))) = Union (coprod X) by Th3; dom coprod(X) = the carrier of S by PBOOLE:def 3; then (coprod(X)).s in rng coprod(X) by FUNCT_1:def 5; then coprod(s,X) in rng coprod(X) by MSAFREE:def 3; then a in union rng coprod(X) by A2,TARSKI:def 4; then A4: a in Terminals (DTConOSA X) by A3,PROB_1:def 3; then reconsider a as Symbol of DTConOSA(X); reconsider b = root-tree a as Element of TS(DTConOSA X) by A4,DTCONSTR:def 4; b in A by A1; hence thesis by Def7; end; end; definition let S be OrderSortedSign, X be non-empty ManySortedSet of S; func ParsedTerms(X) -> OrderSortedSet of S means :Def8: for s be Element of S holds it.s = ParsedTerms(X,s); existence proof deffunc F(Element of S) = ParsedTerms(X,$1); consider f be Function such that A1: dom f = the carrier of S & for d be Element of S holds f.d = F(d) from LambdaB; reconsider f as ManySortedSet of S by A1,PBOOLE:def 3; f is order-sorted proof let s1,s2 be Element of S such that A2: s1 <= s2; thus f.s1 c= f.s2 proof let x1 be set such that A3: x1 in f.s1; x1 in ParsedTerms(X,s1) by A1,A3; then x1 in {a where a is Element of TS(DTConOSA(X)): (ex s3 being Element of S, x be set st s3 <= s1 & x in X.s3 & a = root-tree [x,s3]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o <= s1} by Def7; then consider a being Element of TS(DTConOSA(X)) such that A4: x1 = a and A5: (ex s3 being Element of S, x be set st s3 <= s1 & x in X.s3 & a = root-tree [x,s3]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o <= s1; (ex s3 being Element of S, x be set st s3 <= s2 & x in X.s3 & a = root-tree [x,s3]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o <= s2 proof per cases by A5; suppose ex s3 being Element of S, x be set st s3 <= s1 & x in X.s3 & a = root-tree [x,s3]; then consider s3 being Element of S, x be set such that A6: s3 <= s1 & x in X.s3 & a = root-tree [x,s3]; reconsider s2_1 = s2 , s3_1 = s3 as Element of S ; s3_1 <= s2_1 by A2,A6,ORDERS_1:26; hence thesis by A6; suppose ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o <= s1; then consider o be OperSymbol of S such that A7: [o,the carrier of S] = a.{} & the_result_sort_of o <= s1; reconsider s2_1 = s2 as Element of S; the_result_sort_of o <= s2_1 by A2,A7,ORDERS_1:26; hence thesis by A7; end; then x1 in {b where b is Element of TS(DTConOSA(X)): (ex s3 being Element of S, x be set st s3 <= s2 & x in X.s3 & b = root-tree [x,s3]) or ex o be OperSymbol of S st [o,the carrier of S] = b.{} & the_result_sort_of o <= s2} by A4; then x1 in ParsedTerms(X,s2) by Def7; hence thesis by A1; end; end; then reconsider f as OrderSortedSet of S; take f; thus thesis by A1; end; uniqueness proof let A,B be OrderSortedSet of S; assume that A8: for s be Element of S holds A.s = ParsedTerms(X,s) and A9: for s be Element of S holds B.s = ParsedTerms(X,s); for i be set st i in the carrier of S holds A.i = B.i proof let i be set; assume i in the carrier of S; then reconsider s = i as Element of S; A.s = ParsedTerms(X,s) & B.s = ParsedTerms(X,s) by A8,A9; hence thesis; end; hence thesis by PBOOLE:3; end; end; definition let S be OrderSortedSign, X be non-empty ManySortedSet of S; cluster ParsedTerms(X) -> non-empty; coherence proof let i be set; assume i in the carrier of S; then reconsider s = i as Element of S; (ParsedTerms(X)).s = ParsedTerms(X,s) by Def8; hence thesis; end; end; theorem Th5: for S be OrderSortedSign, X be non-empty ManySortedSet of S, o be OperSymbol of S, x be set st x in ((ParsedTerms X)# * (the Arity of S)).o holds x is FinSequence of TS(DTConOSA(X)) proof let S be OrderSortedSign, X be non-empty ManySortedSet of S, o be OperSymbol of S, x be set; assume A1: x in ((ParsedTerms X)# * (the Arity of S)).o; set D = DTConOSA(X), ar = the_arity_of o; (the Arity of S).o = ar by MSUALG_1:def 6; then x in product ((ParsedTerms X) * ar) by A1,MSAFREE:1; then consider f be Function such that A2: x = f & dom f = dom ((ParsedTerms X) * ar) & for y be set st y in dom ((ParsedTerms X)* ar) holds f.y in ((ParsedTerms X) * ar).y by CARD_3:def 5; A3: dom ((ParsedTerms X) * ar) = dom ar by PBOOLE:def 3; dom ar = Seg len ar by FINSEQ_1:def 3; then reconsider f as FinSequence by A2,A3,FINSEQ_1:def 2; rng f c= TS D proof let a be set; assume a in rng f; then consider b be set such that A4: b in dom f & f.b = a by FUNCT_1:def 5; A5: a in ((ParsedTerms X) * ar).b by A2,A4; reconsider b as Nat by A4; ((ParsedTerms X) * ar).b = (ParsedTerms X).(ar.b) by A2,A4,FUNCT_1:22 .= (ParsedTerms X). (ar/.b) by A2,A3,A4,FINSEQ_4:def 4 .= ParsedTerms(X,ar/.b) by Def8 .= { s where s is Element of TS D: (ex s1 being Element of S, x be set st s1 <= ar/.b & x in X.(s1) & s = root-tree [x,s1]) or ex o1 be OperSymbol of S st [o1,the carrier of S] = s.{} & the_result_sort_of o1 <= ar/.b} by Def7; then consider e be Element of TS D such that A6: a = e and (ex s1 being Element of S, x be set st s1 <= ar/.b & x in X.(s1) & e = root-tree [x,s1]) or ex o be OperSymbol of S st [o,the carrier of S] = e.{} & the_result_sort_of o <= ar/.b by A5; thus thesis by A6; end; then reconsider f as FinSequence of TS(D) by FINSEQ_1:def 4; f = x by A2; hence thesis; end; theorem Th6: for S be OrderSortedSign, X be non-empty ManySortedSet of S, o be OperSymbol of S, p be FinSequence of TS(DTConOSA(X)) holds p in ((ParsedTerms X)# * (the Arity of S)).o iff dom p = dom (the_arity_of o) & for n be Nat st n in dom p holds p.n in ParsedTerms(X,(the_arity_of o)/.n) proof let S be OrderSortedSign, X be non-empty ManySortedSet of S, o be OperSymbol of S, p be FinSequence of TS(DTConOSA(X)); set AR = the Arity of S, ar = the_arity_of o; thus p in ((ParsedTerms X)# * AR).o implies dom p = dom (the_arity_of o) & for n be Nat st n in dom p holds p.n in ParsedTerms(X,(the_arity_of o)/.n) proof assume A1: p in ((ParsedTerms X)# * (the Arity of S)).o; AR.o = ar by MSUALG_1:def 6; then p in product ((ParsedTerms X) * ar) by A1,MSAFREE:1; then A2: dom p = dom ((ParsedTerms X) * ar) & for x be set st x in dom ((ParsedTerms X) * ar) holds p.x in ((ParsedTerms X) * ar).x by CARD_3:18; A3: dom ((ParsedTerms X) * ar) = dom ar by PBOOLE:def 3; thus dom p = dom ar by A2,PBOOLE:def 3; let n be Nat; assume A4: n in dom p; then ((ParsedTerms X) * ar).n = (ParsedTerms X).(ar.n) by A2,FUNCT_1:22 .= (ParsedTerms X). (ar/.n) by A2,A3,A4,FINSEQ_4:def 4 .= ParsedTerms(X,ar/.n) by Def8; hence thesis by A2,A4; end; assume A5: dom p = dom (the_arity_of o) & for n be Nat st n in dom p holds p.n in ParsedTerms(X,(the_arity_of o)/.n); AR.o = ar by MSUALG_1:def 6; then A6: ((ParsedTerms X)# * AR).o = product ((ParsedTerms X) * ar) by MSAFREE:1; A7: dom p = dom ((ParsedTerms X) * ar) by A5,PBOOLE:def 3; for x be set st x in dom((ParsedTerms X) * ar) holds p.x in ((ParsedTerms X) * ar).x proof let x be set; assume A8: x in dom ((ParsedTerms X) * ar); then reconsider n = x as Nat; ParsedTerms(X,ar/.n) = (ParsedTerms X). (ar/.n) by Def8 .= (ParsedTerms X).(ar.n) by A5,A7,A8,FINSEQ_4:def 4 .= ((ParsedTerms X) * ar).x by A8,FUNCT_1:22; hence thesis by A5,A7,A8; end; hence thesis by A6,A7,CARD_3:18; end; theorem Th7: for S be OrderSortedSign, X be non-empty ManySortedSet of S, o be OperSymbol of S, p be FinSequence of TS(DTConOSA(X)) holds OSSym(o,X) ==> roots p iff p in ((ParsedTerms X)# * (the Arity of S)).o proof let S be OrderSortedSign, X be non-empty ManySortedSet of S, o be OperSymbol of S, p be FinSequence of TS(DTConOSA(X)); set D = DTConOSA(X), ar = the_arity_of o; A1: Union (coprod X) misses [:the OperSymbols of S,{the carrier of S}:] by MSAFREE:4; A2: OSSym(o,X) = [o,the carrier of S] by Def6; A3: D = DTConstrStr (# [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod (X qua ManySortedSet of S)), OSREL(X) #) & (Terminals (DTConOSA(X))) = Union (coprod X) & NonTerminals(DTConOSA(X)) = [:the OperSymbols of S,{the carrier of S}:] by Def5,Th3; thus OSSym(o,X) ==> roots p implies p in ((ParsedTerms X)# * (the Arity of S)).o proof assume OSSym(o,X) ==> roots p; then A4: [[o,the carrier of S],roots p] in OSREL(X) by A2,A3,LANG1:def 1; then reconsider r = roots p as Element of ([:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X))* by ZFMISC_1:106; A5: len r = len ar & for x be set st x in dom r holds (r.x in [:the OperSymbols of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = r.x holds the_result_sort_of o1 <= ar/.x) & (r.x in Union (coprod X) implies ex i being Element of S st i <= ar/.x & r.x in coprod(i,X)) by A4,Th2; A6: dom p = dom r by DTCONSTR:def 1; A7: dom r = Seg len r & Seg len ar = dom ar by FINSEQ_1:def 3; for n be Nat st n in dom p holds p.n in ParsedTerms(X,ar/.n) proof let n be Nat; set s = ar/.n, A = {a where a is Element of TS D: (ex s1 being Element of S, x be set st s1 <= s & x in X.s1 & a = root-tree [x,s1]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o <= s}; A8: A = ParsedTerms(X,s) by Def7; assume A9: n in dom p; then consider T be DecoratedTree such that A10: T = p.n & r.n = T.{} by DTCONSTR:def 1; A11: rng r c= [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X) by FINSEQ_1:def 4; A12: r.n in rng r by A6,A9,FUNCT_1:def 5; A13: rng p c= TS D by FINSEQ_1:def 4; p.n in rng p by A9,FUNCT_1:def 5; then reconsider T as Element of TS(D) by A10,A13; per cases by A11,A12,XBOOLE_0:def 2; suppose A14: r.n in [:the OperSymbols of S,{the carrier of S}:]; then consider o1 being Element of the OperSymbols of S, x2 being Element of {the carrier of S} such that A15: r.n = [o1,x2] by DOMAIN_1:9; A16: x2 = the carrier of S by TARSKI:def 1; then the_result_sort_of o1 <= ar/.n by A4,A6,A9,A14,A15,Th2; then ex o be OperSymbol of S st [o,the carrier of S] = T.{} & the_result_sort_of o <= s by A10,A15,A16; hence thesis by A8,A10; suppose A17: r.n in Union (coprod X); then consider i being Element of S such that A18: i <= ar/.n & r.n in coprod(i,X) by A4,A6,A9,Th2; consider a be set such that A19: a in X.i & r.n = [a,i] by A18,MSAFREE:def 2; reconsider t = r.n as Terminal of D by A17,Th3; T = root-tree t by A10,DTCONSTR:9; hence thesis by A8,A10,A18,A19; end; hence thesis by A5,A6,A7,Th6; end; set r = roots p, OU = [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X); assume A20: p in ((ParsedTerms X)# * (the Arity of S)).o; then A21: dom p = dom ar & for n be Nat st n in dom p holds p.n in ParsedTerms(X,ar/.n) by Th6; A22: dom p = dom r by DTCONSTR:def 1; A23: dom r = Seg len r & Seg len ar = dom ar by FINSEQ_1:def 3; rng r c= [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X) proof let x be set; assume x in rng r; then consider n be set such that A24: n in dom r & r.n = x by FUNCT_1:def 5; reconsider n as Nat by A24; set s = ar/.n, A = {a where a is Element of TS D: (ex s1 being Element of S, x be set st s1 <= s & x in X.s1 & a = root-tree [x,s1]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o <= s}; A25: A = ParsedTerms(X,s) by Def7; p.n in ParsedTerms(X,s) by A20,A22,A24,Th6; then consider a be Element of TS D such that A26: a = p.n and A27: (ex s1 being Element of S, x be set st s1 <= s & x in X.s1 & a = root-tree [x,s1]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o <= s by A25; consider T be DecoratedTree such that A28: T = p.n & r.n = T.{} by A22,A24,DTCONSTR:def 1; per cases by A27; suppose ex s1 being Element of S, x be set st s1 <= s & x in X.s1 & a = root-tree [x,s1]; then consider s1 being Element of S, y be set such that A29: s1 <= s & y in X.s1 & a = root-tree [y,s1]; A30: a.{} = [y,s1] by A29,TREES_4:3; A31: [y,s1] in coprod(s1,X) by A29,MSAFREE:def 2; dom coprod(X) = the carrier of S by PBOOLE:def 3; then (coprod(X)).s1 in rng coprod(X) by FUNCT_1:def 5; then coprod(s1,X) in rng coprod(X) by MSAFREE:def 3; then [y,s1] in union rng coprod(X) by A31,TARSKI:def 4; then [y,s1] in Union (coprod X) by PROB_1:def 3; hence thesis by A24,A26,A28,A30,XBOOLE_0:def 2; suppose ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o <= s; then consider o1 be OperSymbol of S such that A32: [o1,the carrier of S] = a.{} & the_result_sort_of o1 <= s; the carrier of S in {the carrier of S} by TARSKI:def 1; then [o1,the carrier of S] in [:the OperSymbols of S,{the carrier of S} :] by ZFMISC_1:106; hence thesis by A24,A26,A28,A32,XBOOLE_0:def 2; end; then reconsider r as FinSequence of OU by FINSEQ_1:def 4; reconsider r as Element of OU* by FINSEQ_1:def 11; A33: len r = len ar by A21,A22,A23,FINSEQ_1:8; for x be set st x in dom r holds (r.x in [:the OperSymbols of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = r.x holds the_result_sort_of o1 <= ar/.x) & (r.x in Union (coprod X) implies ex i being Element of S st i <= ar/.x & r.x in coprod(i,X)) proof let x be set; assume A34: x in dom r; then reconsider n = x as Nat; set s = ar/.n, A = {a where a is Element of TS D: (ex s1 being Element of S, x be set st s1 <= s & x in X.s1 & a = root-tree [x,s1]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o <= s}; A35: A = ParsedTerms(X,s) by Def7; p.n in ParsedTerms(X,s) by A20,A22,A34,Th6; then consider a be Element of TS D such that A36: a = p.n and A37: (ex s1 being Element of S, x be set st s1 <= s & x in X.s1 & a = root-tree [x,s1]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o <= s by A35; consider T be DecoratedTree such that A38: T = p.n & r.n = T.{} by A22,A34,DTCONSTR:def 1; thus r.x in [:the OperSymbols of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = r.x holds the_result_sort_of o1 <= ar/.x proof assume A39: r.x in [:the OperSymbols of S,{the carrier of S}:]; let o1 be OperSymbol of S; assume A40: [o1,the carrier of S] = r.x; now given s1 being Element of S, y be set such that A41: s1 <= s & y in X.s1 & a = root-tree [y,s1]; A42: r.x = [y,s1] by A36,A38,A41,TREES_4:3; A43: [y,s1] in coprod(s1,X) by A41,MSAFREE:def 2; dom coprod(X) = the carrier of S by PBOOLE:def 3; then (coprod(X)).s1 in rng coprod(X) by FUNCT_1:def 5; then coprod(s1,X) in rng coprod(X) by MSAFREE:def 3; then r.x in union rng coprod(X) by A42,A43,TARSKI:def 4; then r.x in Union (coprod X) by PROB_1:def 3; hence contradiction by A1,A39,XBOOLE_0:3; end; then consider o2 be OperSymbol of S such that A44: [o2,the carrier of S] = a.{} & the_result_sort_of o2 <= s by A37; thus thesis by A36,A38,A40,A44,ZFMISC_1:33; end; assume A45: r.x in Union (coprod X); now given o1 be OperSymbol of S such that A46: [o1,the carrier of S] = a.{} & the_result_sort_of o1 <= s; the carrier of S in {the carrier of S} by TARSKI:def 1; then [o1,the carrier of S] in [:the OperSymbols of S,{the carrier of S}:] by ZFMISC_1:106; hence contradiction by A1,A36,A38,A45,A46,XBOOLE_0:3; end; then consider s1 being Element of S, y be set such that A47: s1 <= s & y in X.s1 & a = root-tree [y,s1] by A37; A48: r.x = [y,s1] by A36,A38,A47,TREES_4:3; take s1; thus thesis by A47,A48,MSAFREE:def 2; end; then [[o,the carrier of S],r] in OSREL X by A33,Th2; hence thesis by A2,A3,LANG1:def 1; end; theorem Th8: for S be OrderSortedSign, X be non-empty ManySortedSet of S holds union rng (ParsedTerms X) = TS (DTConOSA(X)) proof let S be OrderSortedSign, X be non-empty ManySortedSet of S; set D = DTConOSA(X); A1: dom (ParsedTerms X) = the carrier of S & dom (coprod X) = the carrier of S by PBOOLE:def 3; thus union rng (ParsedTerms X) c= TS D proof let x; assume x in union rng (ParsedTerms X); then consider A be set such that A2: x in A & A in rng (ParsedTerms X) by TARSKI:def 4; consider s be set such that A3: s in dom (ParsedTerms X) & (ParsedTerms X).s = A by A2,FUNCT_1:def 5; reconsider s as Element of S by A3,PBOOLE:def 3; A = ParsedTerms(X,s) by A3,Def8 .= {a where a is Element of TS(D): (ex s1 being Element of S, x be set st s1 <= s & x in X.s1 & a = root-tree [x,s1]) or ex o1 be OperSymbol of S st [o1,the carrier of S] = a.{} & the_result_sort_of o1 <= s} by Def7; then consider a be Element of TS(D) such that A4: a = x and (ex s1 being Element of S, x be set st s1 <= s & x in X.s1 & a = root-tree [x,s1]) or ex o1 be OperSymbol of S st [o1,the carrier of S]=a.{} & the_result_sort_of o1 <= s by A2; thus thesis by A4; end; let x; assume x in TS D; then reconsider t = x as Element of TS(D); A5: rng t c= the carrier of D by TREES_2:def 9; {} in dom t by TREES_1:47; then A6: t.{} in rng t by FUNCT_1:def 5; A7: the carrier of D = (Terminals D) \/ (NonTerminals D) by LANG1:1; A8: Terminals D = Union (coprod X) & NonTerminals D = [:the OperSymbols of S,{the carrier of S}:] by Th3; per cases by A5,A6,A7,XBOOLE_0:def 2; suppose A9: t.{} in Terminals D; then reconsider a = t.{} as Terminal of D; A10: t = root-tree a by DTCONSTR:9; a in union rng(coprod X) by A8,A9,PROB_1:def 3; then consider A be set such that A11: a in A & A in rng(coprod X) by TARSKI:def 4; consider s be set such that A12: s in dom(coprod X) & (coprod X).s = A by A11,FUNCT_1:def 5; reconsider s as Element of S by A12,PBOOLE:def 3; A = coprod(s,X) by A12,MSAFREE:def 3; then consider b be set such that A13: b in X.s & a = [b,s] by A11,MSAFREE:def 2; t in {aa where aa is Element of TS(D): (ex s1 being Element of S, x be set st s1 <= s & x in X.s1 & aa = root-tree [x,s1]) or ex o1 be OperSymbol of S st [o1,the carrier of S] =aa.{} & the_result_sort_of o1 <= s} by A10,A13 ; then t in ParsedTerms(X,s) by Def7; then A14: t in (ParsedTerms X).s by Def8; (ParsedTerms X).s in rng (ParsedTerms X) by A1,FUNCT_1:def 5; hence thesis by A14,TARSKI:def 4; suppose t.{} in NonTerminals D; then reconsider a = t.{} as NonTerminal of D; consider o being Element of the OperSymbols of S, x2 being Element of {the carrier of S} such that A15: a = [o,x2] by A8,DOMAIN_1:9; A16: x2 = the carrier of S by TARSKI:def 1; set rs = the_result_sort_of o; t in {aa where aa is Element of TS(D): (ex s1 being Element of S, x be set st s1 <= rs & x in X.s1 & aa = root-tree [x,s1]) or ex o1 be OperSymbol of S st [o1,the carrier of S] =aa.{} & the_result_sort_of o1 <= rs} by A15,A16; then t in ParsedTerms(X,rs) by Def7; then A17: t in (ParsedTerms X).rs by Def8; (ParsedTerms X).rs in rng (ParsedTerms X) by A1,FUNCT_1:def 5; hence thesis by A17,TARSKI:def 4; end; definition let S be OrderSortedSign, X be non-empty ManySortedSet of S, o be OperSymbol of S; func PTDenOp(o,X) -> Function of ((ParsedTerms X)# * (the Arity of S)).o, ((ParsedTerms X) * (the ResultSort of S)).o means:Def9: for p be FinSequence of TS(DTConOSA(X)) st OSSym(o,X) ==> roots p holds it.p = (OSSym(o,X))-tree p; existence proof set AL = ((ParsedTerms X)# * (the Arity of S)).o, AX = ((ParsedTerms X) * (the ResultSort of S)).o, D = DTConOSA(X), O = the OperSymbols of S, rs = the_result_sort_of o, RS = the ResultSort of S; defpred P[set,set] means for p be FinSequence of TS D st p = $1 holds $2 = (OSSym(o,X))-tree p; A1: for x be set st x in AL ex y be set st y in AX & P[x,y] proof let x be set; assume A2: x in AL; then reconsider p = x as FinSequence of TS(D) by Th5; take y = (OSSym(o,X))-tree p; o in O; then o in dom ((ParsedTerms X) * RS) by PBOOLE:def 3; then A3: AX =(ParsedTerms X).(RS.o) by FUNCT_1:22 .= (ParsedTerms X).rs by MSUALG_1:def 7 .= ParsedTerms(X,rs) by Def8; set A = {a where a is Element of TS(D): (ex s1 being Element of S, x be set st s1 <= rs & x in X.s1 & a = root-tree [x,s1]) or ex o1 be OperSymbol of S st [o1,the carrier of S] = a.{} & the_result_sort_of o1 <= rs}; A4: A = AX by A3,Def7; OSSym(o,X) ==> roots p by A2,Th7; then reconsider a = (OSSym(o,X))-tree p as Element of TS D by DTCONSTR:def 4; (ex q being DTree-yielding FinSequence st p = q & dom a = tree doms q) & a.{} = OSSym(o,X) & for n be Nat st n < len p holds a|<*n*> = p.(n+1) by TREES_4:def 4; then consider q being DTree-yielding FinSequence such that A5: p = q & dom a = tree doms q & a.{} = OSSym(o,X) & for n be Nat st n < len p holds a|<*n*> = p.(n+1); OSSym(o,X) = [o,the carrier of S] by Def6; hence y in AX by A4,A5; thus P[x,y]; end; consider f be Function such that A6: dom f = AL & rng f c= AX & for x be set st x in AL holds P[x,f.x] from NonUniqBoundFuncEx(A1); reconsider g = f as Function of AL,rng f by A6,FUNCT_2:3; reconsider g as Function of AL,AX by A6,FUNCT_2:4; take g; let p be FinSequence of TS D; assume OSSym(o,X) ==> roots p; then p in AL by Th7; hence thesis by A6; end; uniqueness proof set AL = ((ParsedTerms X)# * (the Arity of S)).o, AX = ((ParsedTerms X) * (the ResultSort of S)).o, D = DTConOSA(X); let f,g be Function of AL, AX; assume that A7: for p be FinSequence of TS D st OSSym(o,X) ==> roots p holds f.p = (OSSym(o,X))-tree p and A8: for p be FinSequence of TS D st OSSym(o,X) ==> roots p holds g.p = (OSSym(o,X))-tree p; A9: dom f = AL & dom g = AL by FUNCT_2:def 1; for x be set st x in AL holds f.x = g.x proof let x be set; assume A10: x in AL; then reconsider p = x as FinSequence of TS(D) by Th5; OSSym(o,X) ==> roots p by A10,Th7; then f.p = (OSSym(o,X))-tree p & g.p = (OSSym(o,X))-tree p by A7,A8; hence thesis; end; hence thesis by A9,FUNCT_1:9; end; end; definition let S be OrderSortedSign, X be non-empty ManySortedSet of S; func PTOper(X) -> ManySortedFunction of (ParsedTerms X)# * (the Arity of S), (ParsedTerms X) * (the ResultSort of S) means :Def10: for o be OperSymbol of S holds it.o = PTDenOp(o,X); existence proof set Y = the OperSymbols of S; defpred P[set,set] means for o be OperSymbol of S st $1 = o holds $2 = PTDenOp(o,X); A1: for x be set st x in Y ex y be set st P[x,y] proof let x be set; assume x in Y; then reconsider o = x as OperSymbol of S; take PTDenOp(o,X); thus thesis; end; consider f be Function such that A2: dom f = Y & for x be set st x in Y holds P[x,f.x] from NonUniqFuncEx(A1); reconsider f as ManySortedSet of Y by A2,PBOOLE:def 3; for x be set st x in dom f holds f.x is Function proof let x be set; assume x in dom f; then reconsider o = x as OperSymbol of S by A2; f.o = PTDenOp(o,X) by A2; hence thesis; end; then reconsider f as ManySortedFunction of Y by PRALG_1:def 15; for x be set st x in Y holds f.x is Function of ((ParsedTerms X)# * (the Arity of S)).x, ((ParsedTerms X) * (the ResultSort of S)).x proof let x be set; assume x in Y; then reconsider o = x as OperSymbol of S; f.o = PTDenOp(o,X) by A2; hence thesis; end; then reconsider f as ManySortedFunction of (ParsedTerms X)# * (the Arity of S), (ParsedTerms X) * (the ResultSort of S) by MSUALG_1:def 2; take f; let o be OperSymbol of S; thus thesis by A2; end; uniqueness proof let A,B be ManySortedFunction of (ParsedTerms X)# * (the Arity of S), (ParsedTerms X) * (the ResultSort of S); assume that A3: for o be OperSymbol of S holds A.o = PTDenOp(o,X) and A4: for o be OperSymbol of S holds B.o = PTDenOp(o,X); for i be set st i in the OperSymbols of S holds A.i = B.i proof let i be set; assume i in the OperSymbols of S; then reconsider s = i as OperSymbol of S; A.s = PTDenOp(s,X) & B.s = PTDenOp(s,X) by A3,A4; hence thesis; end; hence thesis by PBOOLE:3; end; end; definition let S be OrderSortedSign, X be non-empty ManySortedSet of S; func ParsedTermsOSA(X) -> OSAlgebra of S equals :Def11: MSAlgebra (# ParsedTerms(X), PTOper(X) #); coherence by OSALG_1:17; end; definition let S be OrderSortedSign, X be non-empty ManySortedSet of S; cluster ParsedTermsOSA(X) -> strict non-empty; coherence proof MSAlgebra (# ParsedTerms(X), PTOper(X) #) = ParsedTermsOSA X by Def11; hence thesis by MSUALG_1:def 8; end; end; definition let S be OrderSortedSign; let X be non-empty ManySortedSet of S; let o be OperSymbol of S; redefine func OSSym(o, X) -> NonTerminal of DTConOSA X; coherence proof A1: OSSym(o, X) = [o,the carrier of S] & NonTerminals DTConOSA X = [:the OperSymbols of S,{the carrier of S}:] by Def6,Th3; the carrier of S in { the carrier of S } by TARSKI:def 1; hence thesis by A1,ZFMISC_1:106; end; end; theorem Th9: for S being OrderSortedSign, X being non-empty ManySortedSet of S, s being Element of S holds (the Sorts of ParsedTermsOSA(X)).s = {a where a is Element of TS(DTConOSA(X)): (ex s1 being Element of S, x be set st s1 <= s & x in X.s1 & a = root-tree [x,s1]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o <= s} proof let S being OrderSortedSign, X being non-empty ManySortedSet of S, s being Element of S; set PTA = ParsedTermsOSA(X); A1: PTA = MSAlgebra (# ParsedTerms(X), PTOper(X) #) by Def11; {a where a is Element of TS(DTConOSA(X)): (ex s1 being Element of S, x be set st s1 <= s & x in X.s1 & a = root-tree [x,s1]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o <= s} = ParsedTerms(X,s) by Def7 .= (the Sorts of PTA).s by A1,Def8; hence thesis; end; theorem Th10: for S being OrderSortedSign, X being non-empty ManySortedSet of S, s,s1 being Element of S, x being set st x in X.s holds root-tree [x,s] is Element of TS DTConOSA(X) & ( for z being set holds [z,the carrier of S] <> (root-tree [x,s]).{} ) & ( root-tree [x,s] in (the Sorts of ParsedTermsOSA(X)).s1 iff s <= s1 ) proof let S be OrderSortedSign, X be non-empty ManySortedSet of S, s,s1 be Element of S, x be set such that A1: x in X.s; set PTA = ParsedTermsOSA(X), D = DTConOSA(X); reconsider s0 = s, s1_1 = s1 as Element of S; reconsider SPTA = the Sorts of PTA as OrderSortedSet of S by OSALG_1:17; reconsider t = [x,s] as Terminal of D by A1,Th4; root-tree t is Element of TS D; hence root-tree [x,s] is Element of TS D; root-tree t in {a where a is Element of TS(DTConOSA(X)): (ex s1 being Element of S, x be set st s1 <= s & x in X.s1 & a = root-tree [x,s1]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o <= s} by A1; then A2: root-tree [x,s] in SPTA.s0 by Th9; thus A3: for z being set holds [z,the carrier of S] <> (root-tree [x,s]).{} proof let z be set; A4: (root-tree [x,s]).{} = [x,s] by TREES_4:3; assume [z,the carrier of S] = (root-tree [x,s]).{}; then s = the carrier of S by A4,ZFMISC_1:33; then s in s; hence contradiction; end; hereby assume root-tree [x,s] in (the Sorts of PTA).s1; then root-tree [x,s] in {a where a is Element of TS(DTConOSA(X)): (ex s2 being Element of S, x be set st s2 <= s1 & x in X.s2 & a = root-tree [x,s2]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o <= s1} by Th9; then consider a being Element of TS D such that A5: a = root-tree [x,s] and A6: (ex s2 being Element of S, x be set st s2 <= s1 & x in X.s2 & a = root-tree [x,s2]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o <= s1; consider s2 being Element of S,x1 be set such that A7: s2 <= s1 & x1 in X.s2 & a = root-tree [x1,s2] by A3,A5,A6; [x1,s2] = [x,s] by A5,A7,TREES_4:4; hence s <= s1 by A7,ZFMISC_1:33; end; assume s <= s1; then SPTA.s0 c= SPTA.s1_1 by OSALG_1:def 18; hence thesis by A2; end; theorem Th11: for S being OrderSortedSign, X being non-empty ManySortedSet of S, t being Element of TS (DTConOSA X), o being OperSymbol of S st t.{} = [o,the carrier of S] holds (ex p being SubtreeSeq of OSSym(o,X) st t = OSSym(o,X)-tree p & OSSym(o,X) ==> roots p & p in Args(o,ParsedTermsOSA(X)) & t = Den(o,ParsedTermsOSA(X)).p ) & ( for s2 being Element of S, x being set holds t <> root-tree [x,s2] ) & for s1 being Element of S holds t in (the Sorts of ParsedTermsOSA(X)).s1 iff the_result_sort_of o <= s1 proof let S be OrderSortedSign, X be non-empty ManySortedSet of S, t be Element of TS (DTConOSA X), o be OperSymbol of S such that A1: t.{} = [o,the carrier of S]; set G = DTConOSA X, PTA = ParsedTermsOSA(X); A2: PTA = MSAlgebra (# ParsedTerms(X), PTOper(X) #) by Def11; reconsider SPTA = the Sorts of PTA as OrderSortedSet of S by OSALG_1:17; [o,the carrier of S] = OSSym(o, X) by Def6; then consider p being FinSequence of TS G such that A3: t = OSSym(o,X)-tree p & OSSym(o,X) ==> roots p by A1,DTCONSTR:10; reconsider p as SubtreeSeq of OSSym(o,X) by A3,DTCONSTR:def 9; p in ((ParsedTerms X)# * (the Arity of S)).o by A3,Th7; then A4: p in Args(o,ParsedTermsOSA(X)) by A2,MSUALG_1:def 9; Den(o,PTA).p = ((the Charact of PTA).o).p by MSUALG_1:def 11 .= PTDenOp(o,X).p by A2,Def10 .= t by A3,Def9; hence ex p being SubtreeSeq of OSSym(o,X) st t = OSSym(o,X)-tree p & OSSym(o,X) ==> roots p & p in Args(o,ParsedTermsOSA(X)) & t = Den(o,ParsedTermsOSA(X)).p by A3,A4; set s = the_result_sort_of o; t in {a where a is Element of TS(DTConOSA(X)): (ex s1 being Element of S, x be set st s1 <= s & x in X.s1 & a = root-tree [x,s1]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o <= s} by A1; then A5: t in SPTA.s by Th9; thus A6: for s2 being Element of S, x being set holds t <> root-tree [x,s2] proof let s2 be Element of S, x be set; assume t = root-tree [x,s2]; then [x,s2] = [o, the carrier of S] by A1,TREES_4:3; then s2 = the carrier of S by ZFMISC_1:33; then s2 in s2; hence contradiction; end; let s1 be Element of S; reconsider s0 = s, s1_1 = s1 as Element of S; hereby assume t in (the Sorts of PTA).s1; then t in {a where a is Element of TS(DTConOSA(X)): (ex s2 being Element of S, x be set st s2 <= s1 & x in X.s2 & a = root-tree [x,s2]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o <= s1} by Th9; then consider a being Element of TS DTConOSA(X) such that A7: a = t and A8: (ex s2 being Element of S, x be set st s2 <= s1 & x in X.s2 & a = root-tree [x,s2]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o <= s1; consider o1 being OperSymbol of S such that A9: [o1,the carrier of S] = a.{} & the_result_sort_of o1 <= s1 by A6,A7,A8; thus s <= s1 by A1,A7,A9,ZFMISC_1:33; end; assume the_result_sort_of o <= s1; then SPTA.s0 c= SPTA.s1_1 by OSALG_1:def 18; hence thesis by A5; end; theorem Th12: for S being OrderSortedSign, X being non-empty ManySortedSet of S, nt being Symbol of DTConOSA(X), ts being FinSequence of TS(DTConOSA(X)) st nt ==> roots ts holds nt in NonTerminals DTConOSA(X) & nt-tree ts in TS DTConOSA(X) & ex o being OperSymbol of S st nt = [o,the carrier of S] & ts in Args(o,ParsedTermsOSA(X)) & nt-tree ts = Den(o,ParsedTermsOSA(X)).ts & for s1 being Element of S holds nt-tree ts in (the Sorts of ParsedTermsOSA(X)).s1 iff the_result_sort_of o <= s1 proof let S be OrderSortedSign, X be non-empty ManySortedSet of S, nt be Symbol of DTConOSA(X), ts be FinSequence of TS(DTConOSA(X)) such that A1: nt ==> roots ts; set D = DTConOSA(X), PTA = ParsedTermsOSA(X); A2: nt in { s where s is Symbol of D: ex n being FinSequence st s ==> n} by A1; hence nt in NonTerminals D by LANG1:def 3; then nt in [:the OperSymbols of S,{the carrier of S}:] by Th3; then consider o1,b1 being set such that A3: o1 in the OperSymbols of S & b1 in {the carrier of S} & nt = [o1,b1] by ZFMISC_1:def 2; reconsider o1 as OperSymbol of S by A3; reconsider nt1 = nt as NonTerminal of D by A2,LANG1:def 3; reconsider ts1 = ts as SubtreeSeq of nt1 by A1,DTCONSTR:def 9; nt1-tree ts1 in TS D; hence nt-tree ts in TS DTConOSA(X); A4: b1 = the carrier of S by A3,TARSKI:def 1; take o1; thus nt = [o1,the carrier of S] by A3,TARSKI:def 1; A5: (nt1-tree ts).{} = [o1,the carrier of S] by A3,A4,TREES_4:def 4; then consider p being SubtreeSeq of OSSym(o1,X) such that A6: (nt1-tree ts1) = OSSym(o1,X)-tree p & OSSym(o1,X) ==> roots p & p in Args(o1,PTA) & (nt1-tree ts1) = Den(o1,PTA).p by Th11; thus thesis by A5,A6,Th11,TREES_4:15; end; :: Element of Args is FinSequence (if clusters MSUALG_9) theorem Th13: for S being OrderSortedSign, X being non-empty ManySortedSet of S, o be OperSymbol of S, x being FinSequence holds x in Args(o,ParsedTermsOSA(X)) iff x is FinSequence of TS(DTConOSA(X)) & OSSym(o,X) ==> roots x proof let S be OrderSortedSign, X be non-empty ManySortedSet of S, o be OperSymbol of S, x be FinSequence; set PTA = ParsedTermsOSA(X); A1: PTA = MSAlgebra(# ParsedTerms(X), PTOper(X) #) by Def11; hereby assume A2: x in Args(o,PTA); then A3: x in ((the Sorts of PTA)# * the Arity of S).o by MSUALG_1:def 9; A4: x in ((ParsedTerms X)# * (the Arity of S)).o by A1,A2,MSUALG_1:def 9; thus x is FinSequence of TS(DTConOSA(X)) by A1,A3,Th5; reconsider x1 = x as FinSequence of TS(DTConOSA(X)) by A4,Th5; OSSym(o,X) ==> roots x1 by A1,A3,Th7; hence OSSym(o,X) ==> roots x; end; assume A5: x is FinSequence of TS(DTConOSA(X)) & OSSym(o,X) ==> roots x; then reconsider x1 = x as FinSequence of TS(DTConOSA(X)); x1 in ((ParsedTerms X)# * (the Arity of S)).o by A5,Th7; hence thesis by A1,MSUALG_1:def 9; end; theorem Th14: for S be OrderSortedSign, X be non-empty ManySortedSet of S, t be Element of TS DTConOSA(X) ex s being SortSymbol of S st t in (the Sorts of ParsedTermsOSA(X)).s & for s1 being Element of S st t in (the Sorts of ParsedTermsOSA(X)).s1 holds s <= s1 proof let S be OrderSortedSign, X be non-empty ManySortedSet of S, t be Element of TS DTConOSA(X); set D = DTConOSA(X); defpred P[set] means ex s being SortSymbol of S st $1 in (the Sorts of ParsedTermsOSA(X)).s & for s1 being Element of S st $1 in (the Sorts of ParsedTermsOSA(X)).s1 holds s <= s1; A1: for s being Symbol of D st s in Terminals D holds P[root-tree s] proof let sy be Symbol of D such that A2: sy in Terminals D; consider s being Element of S, x being set such that A3: x in X.s & sy = [x,s] by A2,Th4; reconsider s as SortSymbol of S; take s; thus thesis by A3,Th10; end; A4: for nt being Symbol of D, ts being FinSequence of TS(D) st nt ==> roots ts & for t being DecoratedTree of the carrier of D st t in rng ts holds P[t] holds P[nt-tree ts] proof let nt be Symbol of D, ts be FinSequence of TS(D) such that A5: nt ==> roots ts and for t being DecoratedTree of the carrier of D st t in rng ts holds P[t]; consider o being OperSymbol of S such that nt = [o,the carrier of S] & ts in Args(o,ParsedTermsOSA(X)) & nt-tree ts = Den(o,ParsedTermsOSA(X)).ts and A6: for s1 being Element of S holds nt-tree ts in (the Sorts of ParsedTermsOSA(X)).s1 iff the_result_sort_of o <= s1 by A5,Th12; reconsider s = the_result_sort_of o as SortSymbol of S; take s; thus thesis by A6; end; for t being DecoratedTree of the carrier of D st t in TS(D) holds P[t] from DTConstrInd(A1,A4); hence thesis; end; :: this should be done more generally for leastsorted osas (and :: then remove the LeastSorts func), however, it is better here :: to have it defined for terms (and not Elements of osa) definition let S be OrderSortedSign, X be non-empty ManySortedSet of S, t be Element of TS DTConOSA(X); func LeastSort t -> SortSymbol of S means :Def12: t in (the Sorts of ParsedTermsOSA(X)).it & for s1 being Element of S st t in (the Sorts of ParsedTermsOSA(X)).s1 holds it <= s1; existence by Th14; uniqueness proof let s2,s3 be SortSymbol of S such that A1: t in (the Sorts of ParsedTermsOSA(X)).s2 & for s1 being Element of S st t in (the Sorts of ParsedTermsOSA(X)).s1 holds s2 <= s1 and A2: t in (the Sorts of ParsedTermsOSA(X)).s3 & for s1 being Element of S st t in (the Sorts of ParsedTermsOSA(X)).s1 holds s3 <= s1; s3 <= s2 & s2 <= s3 by A1,A2; hence s2 = s3 by ORDERS_1:25; end; end; :: REVISE: the clusters needed to make the def from MSAFREE3 work :: are too demanding, make it more easily accessible (or include :: the clusters if it is too hard) definition let S be non empty non void ManySortedSign; let A be non-empty MSAlgebra over S; mode Element of A is Element of Union the Sorts of A; canceled; end; theorem Th15: for S being OrderSortedSign, X being non-empty ManySortedSet of S, x being set holds x is Element of ParsedTermsOSA(X) iff x is Element of TS DTConOSA(X) proof let S being OrderSortedSign, X being non-empty ManySortedSet of S, x being set; A1: ParsedTermsOSA(X) = MSAlgebra (# ParsedTerms(X), PTOper(X) #) by Def11; TS DTConOSA X = union rng (ParsedTerms X) by Th8 .= Union (the Sorts of ParsedTermsOSA(X)) by A1,PROB_1:def 3; hence thesis; end; theorem Th16: for S being OrderSortedSign, X being non-empty ManySortedSet of S, s be Element of S, x being set st x in (the Sorts of ParsedTermsOSA(X)).s holds x is Element of TS DTConOSA(X) proof let S being OrderSortedSign, X being non-empty ManySortedSet of S, s be Element of S, x being set such that A1: x in (the Sorts of ParsedTermsOSA(X)).s; set PTA = ParsedTermsOSA(X), SPTA = the Sorts of PTA; s in the carrier of S; then s in dom SPTA by PBOOLE:def 3; then SPTA.s in rng SPTA by FUNCT_1:def 5; then x in union rng SPTA by A1,TARSKI:def 4; then reconsider x1=x as Element of Union SPTA by PROB_1:def 3; x1 is Element of PTA; hence x is Element of TS DTConOSA(X) by Th15; end; theorem for S being OrderSortedSign, X being non-empty ManySortedSet of S, s being Element of S, x being set st x in X.s for t being Element of TS DTConOSA(X) st t = root-tree [x,s] holds LeastSort t = s proof let S being OrderSortedSign, X being non-empty ManySortedSet of S, s being Element of S, x being set such that A1: x in X.s; reconsider s2 = s as Element of S; let t being Element of TS DTConOSA(X) such that A2: t = root-tree [x,s]; A3: t in (the Sorts of ParsedTermsOSA(X)).s2 by A1,A2,Th10; for s1 being Element of S st t in (the Sorts of ParsedTermsOSA(X)).s1 holds s2 <= s1 by A1,A2,Th10; hence thesis by A3,Def12; end; theorem Th18: for S being OrderSortedSign, X being non-empty ManySortedSet of S, o be OperSymbol of S, x being Element of Args(o,ParsedTermsOSA(X)) holds for t being Element of TS DTConOSA(X) st t = Den(o,ParsedTermsOSA(X)).x holds LeastSort t = the_result_sort_of o proof let S being OrderSortedSign, X being non-empty ManySortedSet of S, o be OperSymbol of S, x being Element of Args(o,ParsedTermsOSA(X)); set PTA = ParsedTermsOSA(X); A1: OSSym(o,X) = [o,the carrier of S] by Def6; let t being Element of TS DTConOSA(X) such that A2: t = Den(o,ParsedTermsOSA(X)).x; A3: x is FinSequence of TS(DTConOSA(X)) & OSSym(o,X) ==> roots x by Th13; reconsider x1 = x as FinSequence of TS(DTConOSA(X)) by Th13; consider o1 being OperSymbol of S such that A4: OSSym(o,X) = [o1,the carrier of S] & x1 in Args(o1,ParsedTermsOSA(X)) & OSSym(o,X)-tree x1 = Den(o1,ParsedTermsOSA(X)).x1 & for s1 being Element of S holds OSSym(o,X)-tree x1 in (the Sorts of ParsedTermsOSA(X)).s1 iff the_result_sort_of o1 <= s1 by A3,Th12; A5: o = o1 by A1,A4,ZFMISC_1:33; then t in (the Sorts of PTA).(the_result_sort_of o) by A2,A4; hence LeastSort t = the_result_sort_of o by A2,A4,A5,Def12; end; :: WHY is this necessary??? bug? definition let S be OrderSortedSign, X be non-empty ManySortedSet of S; let o2 be OperSymbol of S; cluster Args(o2,ParsedTermsOSA(X)) -> non empty; coherence; end; :: REVISE: was probably needed for casting, but try if :: LeastSort * x does the work and if so, remove this definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, x be FinSequence of TS DTConOSA(X); func LeastSorts x -> Element of (the carrier of S)* means :Def14: dom it = dom x & for y being Nat st y in dom x holds ex t being Element of TS DTConOSA(X) st t = x.y & it.y = LeastSort t; existence proof set D = DTConOSA(X); defpred P[set,set] means ex t being Element of TS D st t = $1 & LeastSort t = $2; A1: for x being set st x in TS D ex y being set st y in the carrier of S & P[x,y] proof let x being set such that A2: x in TS D; reconsider t = x as Element of TS D by A2; take LeastSort t; thus LeastSort t in the carrier of S; take t; thus thesis; end; consider f being Function of TS D,(the carrier of S) such that A3: for x being set st x in TS D holds P[x,f.x] from FuncEx1(A1); take f*x; thus dom (f*x) = dom x by ALG_1:1; A4: rng x c= TS D by FINSEQ_1:def 4; let y being Nat such that A5: y in dom x; A6: y in dom (f*x) by A5,ALG_1:1; x.y in rng x by A5,FUNCT_1:12; then reconsider t1 = x.y as Element of TS D by A4; take t1; thus t1 = x.y; consider t2 being Element of TS D such that A7: t2 = t1 & LeastSort t2 = f.t1 by A3; thus (f*x).y = LeastSort t1 by A6,A7,ALG_1:1; end; uniqueness proof set D = DTConOSA(X); let f1,f2 be Element of (the carrier of S)* such that A8: dom f1 = dom x & for y being Nat st y in dom x holds ex t being Element of TS DTConOSA(X) st t = x.y & f1.y = LeastSort t and A9: dom f2 = dom x & for y being Nat st y in dom x holds ex t being Element of TS DTConOSA(X) st t = x.y & f2.y = LeastSort t; for k being Nat st k in dom f1 holds f1.k = f2.k proof let k be Nat such that A10: k in dom f1; consider t1 being Element of TS D such that A11: t1 = x.k & f1.k = LeastSort t1 by A8,A10; consider t2 being Element of TS D such that A12: t2 = x.k & f2.k = LeastSort t2 by A8,A9,A10; thus f1.k = f2.k by A11,A12; end; hence f1 = f2 by A8,A9,FINSEQ_1:17; end; end; :: all these should be generalized to any leastsorted osa theorem Th19: for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, o be OperSymbol of S, x be FinSequence of TS DTConOSA(X) holds LeastSorts x <= the_arity_of o iff x in Args(o,ParsedTermsOSA(X)) proof let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, o be OperSymbol of S, x be FinSequence of TS DTConOSA(X); set PTA = ParsedTermsOSA(X), D = DTConOSA(X), w = the_arity_of o, LSx = LeastSorts x; A1: dom LSx = dom x & for y being Nat st y in dom x holds ex t being Element of TS DTConOSA(X) st t = x.y & LSx.y = LeastSort t by Def14; reconsider SPTA = the Sorts of PTA as OrderSortedSet of S by OSALG_1:17; hereby assume A2: LeastSorts x <= w; then len LSx = len w & for i being set st i in dom LSx for s1,s2 being Element of S st s1 = LSx.i & s2 = w.i holds s1 <= s2 by OSALG_1:def 7; then A3: dom LSx = dom w & len x = len w by A1,FINSEQ_3:31; for k be Nat st k in dom x holds x.k in (the Sorts of PTA).(w/.k) proof let k be Nat such that A4: k in dom x; A5: (w/.k) = w.k by A1,A3,A4,FINSEQ_4:def 4; reconsider wk = (w/.k) as Element of S; consider t2 being Element of TS DTConOSA(X) such that A6: t2 = x.k & LSx.k = LeastSort t2 by A4,Def14; A7: t2 in (the Sorts of PTA).(LeastSort t2) by Def12; LeastSort t2 <= wk by A1,A2,A4,A5,A6,OSALG_1:def 7; then SPTA.(LeastSort t2) c= SPTA.wk by OSALG_1:def 18; hence x.k in (the Sorts of PTA).(w/.k) by A6,A7; end; hence x in Args(o,PTA) by A3,MSAFREE2:7; end; assume A8: x in Args(o,PTA); then A9: dom x = dom w & for i being Nat st i in dom w holds x.i in (the Sorts of PTA).(w/.i) by MSUALG_6:2; hence len LSx = len w by A1,FINSEQ_3:31; let i be set such that A10: i in dom LSx; A11: i in dom w & i in dom x by A9,A10,Def14; reconsider k = i as Nat by A10; let s1,s2 be Element of S such that A12: s1 = LSx.i & s2 = w.i; consider t2 being Element of TS D such that A13: t2 = x.k & LSx.k = LeastSort t2 by A11,Def14; A14: w/.k = w.k by A1,A9,A10,FINSEQ_4:def 4; x.k in (the Sorts of PTA).(w/.k) by A8,A11,MSUALG_6:2; hence s1 <= s2 by A12,A13,A14,Def12; end; definition cluster locally_directed regular (monotone OrderSortedSign); existence proof consider S1 being discrete op-discrete OrderSortedSign; take S1; thus thesis; end; end; :: just casting funcs necessary for the usage of schemes, definition let S be locally_directed regular (monotone OrderSortedSign), X be non-empty ManySortedSet of S, o be OperSymbol of S, x be FinSequence of TS DTConOSA(X); assume A1: OSSym(LBound(o,LeastSorts x),X) ==> roots x; func pi(o,x) -> Element of TS DTConOSA(X) equals :Def15: OSSym(LBound(o,LeastSorts x),X)-tree x; correctness by A1,Th12; end; definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, t be Symbol of DTConOSA(X); assume A1: ex p be FinSequence st t ==> p; func @(X,t) -> OperSymbol of S means:Def16: [it,the carrier of S] = t; existence proof set D = DTConOSA(X), OU = [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod (X qua ManySortedSet of S)); consider p be FinSequence such that A2: t ==> p by A1; A3: [t,p] in the Rules of D by A2,LANG1:def 1; A4: D = DTConstrStr (# OU, OSREL(X) #) by Def5; then reconsider a = t as Element of OU; reconsider p as Element of OU* by A3,A4,ZFMISC_1:106; [a,p] in OSREL(X) by A2,A4,LANG1:def 1; then a in [:the OperSymbols of S,{the carrier of S}:] by Def4; then consider o being Element of the OperSymbols of S, x2 being Element of {the carrier of S} such that A5: a = [o,x2] by DOMAIN_1:9; take o; thus thesis by A5,TARSKI:def 1; end; uniqueness by ZFMISC_1:33; end; definition let S be OrderSortedSign, X be non-empty ManySortedSet of S; let t be Symbol of DTConOSA(X); assume A1: t in Terminals DTConOSA(X); func pi t -> Element of TS(DTConOSA(X)) equals :Def17: root-tree t; correctness by A1,DTCONSTR:def 4; end; :: the least monotone OSCongruence definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S; func LCongruence X -> monotone OSCongruence of ParsedTermsOSA(X) means:Def18: for R be monotone OSCongruence of ParsedTermsOSA(X) holds it c= R; existence proof :: I could do the equivalence using MSUALG_8:11, but preparing all :: seems too painful set PTA = ParsedTermsOSA(X), D = DTConOSA(X), SPTA=the Sorts of PTA; defpred MC[set,set,set] means for R being monotone OSCongruence of PTA holds [$1,$2] in R.$3; deffunc F(set) = {[x,y] where x,y is Element of TS D: x in SPTA.$1 & y in SPTA.$1 & for R being monotone OSCongruence of PTA holds [x,y] in R.$1}; consider f being ManySortedSet of the carrier of S such that A1: for i being set st i in the carrier of S holds f.i = F(i) from MSSLambda; A2: for i be set st i in the carrier of S holds f.i is Equivalence_Relation of SPTA.i proof let i be set such that A3: i in the carrier of S; reconsider s = i as Element of S by A3; A4: f.i = {[x,y] where x,y is Element of TS D: x in SPTA.i & y in SPTA.i & for R being monotone OSCongruence of PTA holds [x,y] in R.i} by A1,A3; now let z be set such that A5: z in f.i; consider x,y being Element of TS D such that A6: z = [x,y] & x in SPTA.i & y in SPTA.i & MC[x,y,i] by A4,A5; thus z in [:SPTA.i,SPTA.i:] by A6,ZFMISC_1:106; end; then f.i c= [:SPTA.i,SPTA.i:] by TARSKI:def 3; then reconsider fi = f.i as Relation of SPTA.i by RELSET_1:def 1; now let x be set such that A7: x in SPTA.s; thus [x,x] in fi proof reconsider t1 = x as Element of TS D by A7,Th16; now let R be monotone OSCongruence of PTA; field(R.s) = SPTA.s by ORDERS_1:97; then R.s is_reflexive_in SPTA.s by RELAT_2:def 9; hence [t1,t1] in R.s by A7,RELAT_2:def 1; end; hence thesis by A4,A7; end; end; then fi is_reflexive_in SPTA.s by RELAT_2:def 1; then A8: dom fi = SPTA.s & field fi = SPTA.s by ORDERS_1:98; then A9: fi is total by PARTFUN1:def 4; now let x,y be set such that A10: x in SPTA.s & y in SPTA.s & [x,y] in fi; thus [y,x] in fi proof reconsider t1=x,t2=y as Element of TS D by A10,Th16; consider t3,t4 being Element of TS D such that A11: [t1,t2] = [t3,t4] & t3 in SPTA.i & t4 in SPTA.i & MC[t3,t4,i] by A4,A10; now let R be monotone OSCongruence of PTA; A12: [t1,t2] in R.s by A11; field(R.s) = SPTA.s by ORDERS_1:97; then R.s is_symmetric_in SPTA.s by RELAT_2:def 11; hence [t2,t1] in R.s by A10,A12,RELAT_2:def 3; end; hence thesis by A4,A10; end; end; then A13: fi is_symmetric_in SPTA.s by RELAT_2:def 3; now let x,y,z be set such that A14: x in SPTA.s & y in SPTA.s & z in SPTA.s & [x,y] in fi & [y,z] in fi; thus [x,z] in fi proof reconsider t1=x,t2=y,t3=z as Element of TS D by A14,Th16; consider t4,t5 being Element of TS D such that A15: [t1,t2] = [t4,t5] & t4 in SPTA.i & t5 in SPTA.i & MC[t4,t5,i] by A4,A14; consider t6,t7 being Element of TS D such that A16: [t2,t3] = [t6,t7] & t6 in SPTA.i & t7 in SPTA.i & MC[t6,t7,i] by A4,A14; now let R be monotone OSCongruence of PTA; A17: [t1,t2] in R.s & [t2,t3] in R.s by A15,A16; field(R.s) = SPTA.s by ORDERS_1:97; then R.s is_transitive_in SPTA.s by RELAT_2:def 16; hence [t1,t3] in R.s by A14,A17,RELAT_2:def 8; end; hence thesis by A4,A14; end; end; then fi is_transitive_in SPTA.s by RELAT_2:def 8; hence f.i is Equivalence_Relation of SPTA.i by A8,A9,A13,RELAT_2:def 11,def 16; end; then for i be set st i in the carrier of S holds f.i is Relation of SPTA.i,SPTA.i; then reconsider f as ManySortedRelation of the Sorts of PTA by MSUALG_4:def 2; reconsider f as ManySortedRelation of PTA; for i be set, R be Relation of SPTA.i st i in the carrier of S & f.i = R holds R is Equivalence_Relation of SPTA.i by A2; then f is MSEquivalence_Relation-like by MSUALG_4:def 3; then reconsider f as MSEquivalence-like ManySortedRelation of PTA by MSUALG_4:def 5; f is os-compatible proof let s1,s2 being Element of S such that A18: s1 <= s2; A19: f.s1 = {[x,y] where x,y is Element of TS D: x in SPTA.s1 & y in SPTA.s1 & MC[x,y,s1]} by A1; A20: f.s2 = {[x,y] where x,y is Element of TS D: x in SPTA.s2 & y in SPTA.s2 & MC[x,y,s2]} by A1; let x,y being set such that A21: x in SPTA.s1 & y in SPTA.s1; hereby assume [x,y] in f.s1; then consider t1,t2 being Element of TS D such that A22: [x,y]=[t1,t2] & t1 in SPTA.s1 & t2 in SPTA.s1 & MC[t1,t2,s1] by A19; now let R be monotone OSCongruence of PTA; A23: R is os-compatible by OSALG_4:def 3; [t1,t2] in R.s1 by A22; then [t1,t2] in R.s2 by A18,A22,A23,OSALG_4:def 1; hence t1 in SPTA.s2 & t2 in SPTA.s2 & [t1,t2] in R.s2 by ZFMISC_1:106; end; hence [x,y] in f.s2 by A20,A22; end; assume [x,y] in f.s2; then consider t1,t2 being Element of TS D such that A24: [x,y]=[t1,t2] & t1 in SPTA.s2 & t2 in SPTA.s2 & MC[t1,t2,s2] by A20; A25: x = t1 & y = t2 by A24,ZFMISC_1:33; now let R be monotone OSCongruence of PTA; A26: R is os-compatible by OSALG_4:def 3; [t1,t2] in R.s2 by A24; hence [t1,t2] in R.s1 by A18,A21,A24,A26,OSALG_4:def 1; end; hence [x,y] in f.s1 by A19,A21,A25; end; then reconsider f as MSEquivalence-like OrderSortedRelation of PTA by OSALG_4:def 3; f is monotone proof let o1,o2 being OperSymbol of S such that A27: o1 <= o2; set w2 = the_arity_of o2, rs2 = the_result_sort_of o2; let x1 being Element of Args(o1,PTA), x2 being Element of Args(o2,PTA) such that A28: for y being Nat st y in dom x1 holds [x1.y,x2.y] in f.(w2/.y); A29: f.rs2 = {[x,y] where x,y is Element of TS D: x in SPTA.rs2 & y in SPTA.rs2 & MC[x,y,rs2]} by A1; set D1 = Den(o1,PTA).x1, D2 = Den(o2,PTA).x2; now let R be monotone OSCongruence of PTA; now let y being Nat such that A30: y in dom x1; A31: f.(w2/.y) = {[x,z] where x,z is Element of TS D: x in SPTA.(w2/.y) & z in SPTA.(w2/.y) & MC[x,z,w2/.y]} by A1; [x1.y,x2.y] in f.(w2/.y) by A28,A30; then consider x,z being Element of TS D such that A32: [x1.y,x2.y] = [x,z] & x in SPTA.(w2/.y) & z in SPTA.(w2/.y) & MC[x,z,w2/.y] by A31; thus [x1.y,x2.y] in R.(w2/.y) by A32; end; then [D1,D2] in R.rs2 by A27,OSALG_4:def 28; then D1 in SPTA.rs2 & D2 in SPTA.rs2 & [D1,D2] in R.rs2 by ZFMISC_1:106; hence D1 in SPTA.rs2 & D2 in SPTA.rs2 & [D1,D2] in R.rs2 & D1 is Element of TS D & D2 is Element of TS D by Th16; end; hence [D1,D2] in f.rs2 by A29; end; then reconsider f as monotone (MSEquivalence-like OrderSortedRelation of PTA) ; take f; let R be monotone OSCongruence of PTA; let i be set such that A33: i in the carrier of S; reconsider s = i as Element of S by A33; A34: f.s = {[x,y] where x,y is Element of TS D: x in SPTA.s & y in SPTA.s & MC[x,y,s]} by A1; let z be set such that A35: z in f.i; consider x,y being Element of TS D such that A36: z = [x,y] & x in SPTA.s & y in SPTA.s & MC[x,y,s] by A34,A35; thus thesis by A36; end; uniqueness proof set PTA = ParsedTermsOSA(X); let L1,L2 be monotone OSCongruence of PTA such that A37: for R be monotone OSCongruence of ParsedTermsOSA(X) holds L1 c= R and A38: for R be monotone OSCongruence of ParsedTermsOSA(X) holds L2 c= R; L1 c= L2 & L2 c= L1 by A37,A38; hence thesis by PBOOLE:def 13; end; end; definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S; func FreeOSA(X) -> strict non-empty monotone OSAlgebra of S equals :Def19: QuotOSAlg(ParsedTermsOSA(X),LCongruence(X)); correctness; end; :: now we need an explicit description of a sufficiently small :: monotone OSCongruence on PTA; the PTCongruence turns out to :: be LCongruence on regular signatures, and is also used to describe :: minimal terms there :: just casting funcs necessary for the usage of schemes, :: remove when Frankel behaves better definition let S be OrderSortedSign, X be non-empty ManySortedSet of S; let t be Symbol of DTConOSA(X); func @ t -> Subset of [:TS(DTConOSA(X)), the carrier of S:] equals:Def20: {[root-tree t,s1] where s1 is Element of S: ex s be Element of S, x be set st x in X.s & t = [x,s] & s <= s1}; correctness proof set RT = {[root-tree t,s1] where s1 is Element of S: ex s be Element of S, x be set st x in X.s & t = [x,s] & s <= s1}; RT c= [:TS(DTConOSA(X)), the carrier of S:] proof let y be set such that A1: y in RT; consider s1 being Element of S such that A2: y = [root-tree t,s1] and A3: ex s be Element of S, x be set st x in X.s & t = [x,s] & s <= s1 by A1; consider s being Element of S, x be set such that A4: x in X.s & t = [x,s] & s <= s1 by A3; root-tree [x,s] is Element of TS DTConOSA(X) by A4,Th10; hence y in [:TS(DTConOSA(X)), the carrier of S:] by A2,A4,ZFMISC_1:def 2; end; hence thesis; end; end; definition let S be OrderSortedSign, X be non-empty ManySortedSet of S; let nt be Symbol of DTConOSA(X), x be FinSequence of bool [:TS(DTConOSA(X)), the carrier of S:]; func @ (nt,x) -> Subset of [:TS(DTConOSA(X)), the carrier of S:] equals :Def21: {[Den(o2,ParsedTermsOSA(X)).x2,s3] where o2 is OperSymbol of S, x2 is Element of Args(o2,ParsedTermsOSA(X)), s3 is Element of S : ( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] & o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3) & ex w3 being Element of (the carrier of S)* st dom w3 = dom x & for y being Nat st y in dom x holds [x2.y,w3/.y] in x.y }; correctness proof set NT = {[Den(o2,ParsedTermsOSA(X)).x2,s3] where o2 is OperSymbol of S, x2 is Element of Args(o2,ParsedTermsOSA(X)), s3 is Element of S : ( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] & o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3) & ex w3 being Element of (the carrier of S)* st dom w3 = dom x & for y being Nat st y in dom x holds [x2.y,w3/.y] in x.y }; NT c= [:TS(DTConOSA(X)), the carrier of S:] proof let y be set such that A1: y in NT; consider o2 being OperSymbol of S, x2 being Element of Args(o2,ParsedTermsOSA(X)), s3 being Element of S such that A2: y = [Den(o2,ParsedTermsOSA(X)).x2,s3] and ( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] & o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3) & ex w3 being Element of (the carrier of S)* st dom w3 = dom x & for y being Nat st y in dom x holds [x2.y,w3/.y] in x.y by A1; A3: x2 is FinSequence of TS(DTConOSA(X)) & OSSym(o2,X) ==> roots x2 by Th13; then A4: OSSym(o2,X)-tree x2 in TS DTConOSA(X) by Th12; consider o being OperSymbol of S such that A5: OSSym(o2,X) = [o,the carrier of S] & x2 in Args(o,ParsedTermsOSA(X)) & OSSym(o2,X)-tree x2 = Den(o,ParsedTermsOSA(X)).x2 & for s1 being Element of S holds OSSym(o2,X)-tree x2 in (the Sorts of ParsedTermsOSA(X)).s1 iff the_result_sort_of o <= s1 by A3,Th12; [o2,the carrier of S] = [o,the carrier of S] by A5,Def6; then o2 = o by ZFMISC_1:33; hence y in [:TS(DTConOSA(X)), the carrier of S:] by A2,A4,A5,ZFMISC_1:def 2; end; hence thesis; end; end; :: a bit technical, to create the PTCongruence definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S; func PTClasses X -> Function of TS(DTConOSA(X)), bool [:TS(DTConOSA(X)), the carrier of S:] means :Def22: (for t being Symbol of DTConOSA(X) st t in Terminals DTConOSA(X) holds it.(root-tree t) = @(t) ) & (for nt being Symbol of DTConOSA(X), ts being FinSequence of TS(DTConOSA(X)) st nt ==> roots ts holds it.(nt-tree ts) = @(nt,it * ts) ); existence proof set G = DTConOSA(X), D = bool [:TS(DTConOSA(X)), the carrier of S:]; deffunc TermVal(Symbol of G) = @ $1; deffunc NTermVal(Symbol of G,FinSequence of TS(G), FinSequence of D) = @($1,$3); thus ex f being Function of TS(G), D st (for t being Symbol of G st t in Terminals G holds f.(root-tree t) = TermVal(t)) & (for nt being Symbol of G, ts being FinSequence of TS(G) st nt ==> roots ts holds f.(nt-tree ts) = NTermVal(nt, roots ts, f*ts)) from DTConstrIndDef; end; uniqueness proof set G = DTConOSA(X), D = bool [:TS(DTConOSA(X)), the carrier of S:]; deffunc TermVal(Symbol of G) = @ $1; deffunc NTermVal(Symbol of G,FinSequence of TS(G), FinSequence of D) = @($1,$3); let f1,f2 be Function of TS(DTConOSA(X)), bool [:TS(DTConOSA(X)), the carrier of S:] such that A1: (for t being Symbol of DTConOSA(X) st t in Terminals DTConOSA(X) holds f1.(root-tree t) = TermVal(t) ) & (for nt being Symbol of DTConOSA(X), ts being FinSequence of TS(DTConOSA(X)) st nt ==> roots ts holds f1.(nt-tree ts) = NTermVal(nt, roots ts, f1*ts) ) and A2: (for t being Symbol of DTConOSA(X) st t in Terminals DTConOSA(X) holds f2.(root-tree t) = TermVal(t) ) & (for nt being Symbol of DTConOSA(X), ts being FinSequence of TS(DTConOSA(X)) st nt ==> roots ts holds f2.(nt-tree ts) = NTermVal(nt, roots ts, f2 * ts) ); thus f1 = f2 from DTConstrUniqDef(A1,A2); end; end; theorem Th20: for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, t being Element of TS DTConOSA(X) holds ( for s being Element of S holds t in (the Sorts of ParsedTermsOSA(X)).s iff [t,s] in (PTClasses X).t ) & ( for s being Element of S, y being Element of TS(DTConOSA X) holds [y,s] in (PTClasses X).t implies [t,s] in (PTClasses X).y ) proof let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, t be Element of TS DTConOSA(X); set PTA = ParsedTermsOSA(X), SPTA = the Sorts of PTA, D = DTConOSA(X), C = bool [:TS(D), the carrier of S:], F = PTClasses X; defpred R1[set] means for s being Element of S holds $1 in SPTA.s iff [$1,s] in F.$1; :: switched to have easier prooving defpred R2[set] means for s being Element of S, y being Element of TS(D) holds [y,s] in F.$1 implies [$1,s] in F.y; reconsider SPTA1 = SPTA as OrderSortedSet of S by OSALG_1:17; A1: for s1,s2 being Element of S st s1 <= s2 holds SPTA.s1 c= SPTA.s2 proof let s1,s2 be Element of S such that A2: s1 <= s2; reconsider s11 = s1, s21= s2 as Element of S; SPTA1.s11 c= SPTA1.s21 by A2,OSALG_1:def 18; hence SPTA.s1 c= SPTA.s2; end; defpred P[DecoratedTree of the carrier of D] means R1[$1] & R2[$1]; A3: for s being Symbol of D st s in Terminals D holds P[root-tree s] proof let sy be Symbol of D such that A4: sy in Terminals D; reconsider sy1 = sy as Terminal of D by A4; consider s being Element of S, x being set such that A5: x in X.s & sy = [x,s] by A4,Th4; root-tree sy1 in {a where a is Element of TS(DTConOSA(X)): (ex s1 being Element of S, x be set st s1 <= s & x in X.s1 & a = root-tree [x,s1]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o <= s} by A5; then A6: root-tree sy1 in SPTA.s by Th9; A7: F.(root-tree sy) = @(sy) by A4,Def22 .= {[root-tree sy,s1] where s1 is Element of S: ex s2 be Element of S, x be set st x in X.s2 & sy = [x,s2] & s2 <= s1} by Def20; thus R1[root-tree sy] proof let s1 be Element of S; hereby assume root-tree sy in SPTA.s1; then s <= s1 by A5,Th10; hence [root-tree sy,s1] in F.(root-tree sy) by A5,A7; end; assume [root-tree sy,s1] in F.(root-tree sy); then consider s3 being Element of S such that A8: [root-tree sy,s1] = [root-tree sy,s3] and A9: ex s2 be Element of S, x be set st x in X.s2 & sy = [x,s2] & s2 <= s3 by A7; A10: s1 = s3 by A8,ZFMISC_1:33; consider s2 be Element of S, x2 be set such that A11: x2 in X.s2 & sy = [x2,s2] & s2 <= s3 by A9; x2 = x & s2 = s by A5,A11,ZFMISC_1:33; then SPTA.s c= SPTA.s1 by A1,A10,A11; hence root-tree sy in SPTA.s1 by A6; end; thus R2[root-tree sy] proof let s1 be Element of S, y be Element of TS(D); assume A12: [y,s1] in F.(root-tree sy); then consider s2 being Element of S such that A13: [y,s1] = [root-tree sy,s2] and ex s3 be Element of S, x be set st x in X.s3 & sy = [x,s3] & s3 <= s2 by A7; y = root-tree sy & s1 = s2 by A13,ZFMISC_1:33; hence [root-tree sy,s1] in F.y by A12; end; end; A14: for nt being Symbol of D, ts being FinSequence of TS(D) st nt ==> roots ts & for t being DecoratedTree of the carrier of D st t in rng ts holds P[t] holds P[nt-tree ts] proof let nt be Symbol of D, ts be FinSequence of TS(D) such that A15: nt ==> roots ts and A16: for t being DecoratedTree of the carrier of D st t in rng ts holds R1[t] & R2[t]; consider o being OperSymbol of S such that A17: nt = [o,the carrier of S] & ts in Args(o,PTA) & nt-tree ts = Den(o,PTA).ts & for s1 being Element of S holds nt-tree ts in (the Sorts of PTA).s1 iff the_result_sort_of o <= s1 by A15,Th12; reconsider ts1 = ts as Element of Args(o,PTA) by A17; set w = the_arity_of o; reconsider x = F * ts as FinSequence of C; A18: rng ts c= TS D & dom F = TS D by FINSEQ_1:def 4,FUNCT_2:def 1; then len x = len ts by FINSEQ_2:33; then A19: dom x = dom ts & dom w = dom ts by A17,FINSEQ_3:31,MSUALG_3:6; A20: for y being Nat st y in dom x holds [ts1.y,w/.y] in x.y proof let y being Nat such that A21: y in dom x; A22: ts1.y in rng ts1 by A19,A21,FUNCT_1:12; then reconsider t1 = ts1.y as Element of TS D by A18; ts1.y in SPTA.(w/.y) by A19,A21,MSUALG_6:2; then [t1,w/.y] in F.t1 by A16,A22; hence [ts1.y,w/.y] in x.y by A19,A21,FUNCT_1:23; end; A23: F.(nt-tree ts) = @(nt,x) by A15,Def22 .= {[Den(o2,ParsedTermsOSA(X)).x2,s3] where o2 is OperSymbol of S, x2 is Element of Args(o2,ParsedTermsOSA(X)), s3 is Element of S : ( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] & o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of (the carrier of S)* st dom w3 = dom x & for y being Nat st y in dom x holds [x2.y,w3/.y] in x.y} by Def21; thus R1[nt-tree ts] proof let s1 be Element of S; hereby assume nt-tree ts in SPTA.s1; then o ~= o & len the_arity_of o = len the_arity_of o & the_result_sort_of o <= s1 & the_result_sort_of o <= s1 by A17; hence [nt-tree ts,s1] in F.(nt-tree ts) by A17,A19,A20,A23; end; assume [nt-tree ts,s1] in F.(nt-tree ts); then consider o2 being OperSymbol of S, x2 being Element of Args(o2,PTA), s3 being Element of S such that A24: [nt-tree ts,s1] = [Den(o2,PTA).x2,s3] and A25: ( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] & o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of (the carrier of S)* st dom w3 = dom x & for y being Nat st y in dom x holds [x2.y,w3/.y] in x.y by A23; A26: nt-tree ts = Den(o2,PTA).x2 & s1 = s3 by A24,ZFMISC_1:33; consider o1 being OperSymbol of S such that A27: nt = [o1,the carrier of S] & o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 by A25; A28: Den(o2,PTA).x2 in SPTA.(the_result_sort_of o2) by MSUALG_9:19; SPTA.(the_result_sort_of o2) c= SPTA.s1 by A1,A26,A27; hence nt-tree ts in SPTA.s1 by A26,A28; end; thus R2[nt-tree ts] proof let s1 be Element of S, y be Element of TS(D); assume [y,s1] in F.(nt-tree ts); then consider o2 being OperSymbol of S, x2 being Element of Args(o2,PTA), s3 being Element of S such that A29: [y,s1] = [Den(o2,PTA).x2,s3] and A30: ( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] & o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of (the carrier of S)* st dom w3 = dom x & for y being Nat st y in dom x holds [x2.y,w3/.y] in x.y by A23; A31: y = Den(o2,PTA).x2 & s1 = s3 by A29,ZFMISC_1:33; consider o1 being OperSymbol of S such that A32: nt = [o1,the carrier of S] & o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 by A30; A33: o1 = o by A17,A32,ZFMISC_1:33; A34: x2 is FinSequence of TS D & OSSym(o2,X) ==> roots x2 by Th13; reconsider x3 = x2 as FinSequence of TS D by Th13; consider o3 being OperSymbol of S such that A35: OSSym(o2,X) = [o3,the carrier of S] & x3 in Args(o3,PTA) & OSSym(o2,X)-tree x3 = Den(o3,PTA).x3 & for s2 being Element of S holds OSSym(o2,X)-tree x3 in (the Sorts of PTA).s2 iff the_result_sort_of o3 <= s2 by A34,Th12; [o2,the carrier of S] = [o3,the carrier of S] by A35,Def6; then A36: o2 = o3 by ZFMISC_1:33; A37: dom the_arity_of o2 = dom the_arity_of o by A32,A33,FINSEQ_3:31; consider w3 being Element of (the carrier of S)* such that A38: dom w3 = dom x & for y being Nat st y in dom x holds [x2.y,w3/.y] in x.y by A30; reconsider xy = F * x3 as FinSequence of C; A39: rng x3 c= TS D by FINSEQ_1:def 4; then rng x3 c= dom F by FUNCT_2:def 1; then len xy = len x3 by FINSEQ_2:33; then A40: dom x3 = dom xy by FINSEQ_3:31; A41: dom x2 = dom x by A19,A37,MSUALG_3:6; A42: dom w3 = dom xy & dom xy = dom x3 by A19,A37,A38,A40,MSUALG_3:6; A43: for y being Nat st y in dom xy holds [ts1.y,w3/.y] in xy.y proof let y be Nat such that A44: y in dom xy; A45: ts1.y in rng ts1 & x2.y in rng x3 by A19,A38,A42,A44,FUNCT_1:12; then reconsider t1 = ts1.y,t2 = x2.y as Element of TS D by A18,A39; [x2.y,w3/.y] in x.y by A38,A40,A41,A44; then [x2.y,w3/.y] in F.(ts1.y) by A19,A38,A42,A44,FUNCT_1:23; then [t1,w3/.y] in F.(t2) by A16,A45; hence [ts1.y,w3/.y] in xy.y by A44,FUNCT_1:22; end; A46: F.y = @(OSSym(o2,X),xy) by A31,A34,A35,A36,Def22 .= {[Den(o4,PTA).x4,s4] where o4 is OperSymbol of S, x4 is Element of Args(o4,PTA), s4 is Element of S : ( ex o1 being OperSymbol of S st OSSym(o2,X) = [o1,the carrier of S] & o1 ~= o4 & len the_arity_of o1 = len the_arity_of o4 & the_result_sort_of o1 <= s4 & the_result_sort_of o4 <= s4 ) & ex w4 being Element of (the carrier of S)* st dom w4 = dom xy & for y being Nat st y in dom xy holds [x4.y,w4/.y] in xy.y} by Def21; OSSym(o2,X) = [o2,the carrier of S] & o2 ~= o & len the_arity_of o2 = len the_arity_of o & the_result_sort_of o2 <= s1 & the_result_sort_of o <= s1 by A29,A32,A33,Def6,ZFMISC_1:33; hence [nt-tree ts,s1] in F.y by A17,A42,A43,A46; end; end; for t being DecoratedTree of the carrier of D st t in TS(D) holds P[t] from DTConstrInd(A3,A14); hence thesis; end; theorem Th21: for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, t being Element of TS DTConOSA(X), s being Element of S holds ( ex y being Element of TS(DTConOSA X) st [y,s] in (PTClasses X).t ) implies [t,s] in (PTClasses X).t proof let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S; set D = DTConOSA(X), PTA = ParsedTermsOSA(X), C = bool [:TS(D), the carrier of S:], SPTA = the Sorts of PTA, F = PTClasses X; defpred R3[set] means for s being Element of S holds ( ex y being Element of TS(DTConOSA X) st [y,s] in (PTClasses X).$1 ) implies [$1,s] in (PTClasses X).$1; A1: for s being Symbol of D st s in Terminals D holds R3[root-tree s] proof let sy be Symbol of D such that A2: sy in Terminals D; A3: F.(root-tree sy) = @(sy) by A2,Def22 .= {[root-tree sy,s1] where s1 is Element of S: ex s2 be Element of S, x be set st x in X.s2 & sy = [x,s2] & s2 <= s1} by Def20; let s1 be Element of S; assume ex y being Element of TS(DTConOSA X) st [y,s1] in F.(root-tree sy); then consider y being Element of TS(DTConOSA X) such that A4: [y,s1] in F.(root-tree sy); consider s3 being Element of S such that A5: [y,s1] = [root-tree sy,s3] and ex s2 be Element of S, x be set st x in X.s2 & sy = [x,s2] & s2 <= s3 by A3,A4; thus [root-tree sy,s1] in (PTClasses X).(root-tree sy) by A4,A5,ZFMISC_1:33 ; end; A6: for nt being Symbol of D, ts being FinSequence of TS(D) st nt ==> roots ts & for t being DecoratedTree of the carrier of D st t in rng ts holds R3[t] holds R3[nt-tree ts] proof let nt be Symbol of D, ts be FinSequence of TS(D) such that A7: nt ==> roots ts and for t being DecoratedTree of the carrier of D st t in rng ts holds R3[t]; consider o being OperSymbol of S such that A8: nt = [o,the carrier of S] & ts in Args(o,PTA) & nt-tree ts = Den(o,PTA).ts & for s1 being Element of S holds nt-tree ts in (the Sorts of PTA).s1 iff the_result_sort_of o <= s1 by A7,Th12; reconsider ts1 = ts as Element of Args(o,PTA) by A8; set w = the_arity_of o; reconsider x = F * ts as FinSequence of C; A9: rng ts c= TS D & dom F = TS D by FINSEQ_1:def 4,FUNCT_2:def 1; then len x = len ts by FINSEQ_2:33; then A10: dom x = dom ts & dom w = dom ts by A8,FINSEQ_3:31,MSUALG_3:6; A11: for y being Nat st y in dom x holds [ts1.y,w/.y] in x.y proof let y being Nat such that A12: y in dom x; ts1.y in rng ts1 by A10,A12,FUNCT_1:12; then reconsider t1 = ts1.y as Element of TS D by A9; ts1.y in SPTA.(w/.y) by A10,A12,MSUALG_6:2; then [t1,w/.y] in F.t1 by Th20; hence [ts1.y,w/.y] in x.y by A10,A12,FUNCT_1:23; end; A13: F.(nt-tree ts) = @(nt,x) by A7,Def22 .= {[Den(o2,ParsedTermsOSA(X)).x2,s3] where o2 is OperSymbol of S, x2 is Element of Args(o2,ParsedTermsOSA(X)), s3 is Element of S : ( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] & o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of (the carrier of S)* st dom w3 = dom x & for y being Nat st y in dom x holds [x2.y,w3/.y] in x.y} by Def21; let s1 be Element of S; assume ex y being Element of TS(DTConOSA X) st [y,s1] in F.(nt-tree ts); then consider y being Element of TS(DTConOSA X) such that A14: [y,s1] in F.(nt-tree ts); consider o2 being OperSymbol of S, x2 being Element of Args(o2,PTA), s3 being Element of S such that A15: [y,s1] = [Den(o2,PTA).x2,s3] and A16: ( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] & o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of (the carrier of S)* st dom w3 = dom x & for y being Nat st y in dom x holds [x2.y,w3/.y] in x.y by A13,A14; A17: y = Den(o2,PTA).x2 & s1 = s3 by A15,ZFMISC_1:33; consider o1 being OperSymbol of S such that A18: nt = [o1,the carrier of S] & o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 by A16; o ~= o & len the_arity_of o = len the_arity_of o & the_result_sort_of o <= s3 & the_result_sort_of o <= s3 by A8,A18,ZFMISC_1:33; hence [nt-tree ts,s1] in F.(nt-tree ts) by A8,A10,A11,A13,A17; end; for t being DecoratedTree of the carrier of D st t in TS(D) holds R3[t] from DTConstrInd(A1,A6); hence thesis; end; theorem Th22: for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, x,y being Element of TS DTConOSA(X), s1,s2 being Element of S st s1 <= s2 & x in (the Sorts of ParsedTermsOSA(X)).s1 & y in (the Sorts of ParsedTermsOSA(X)).s1 holds [y,s1] in (PTClasses X).x iff [y,s2] in (PTClasses X).x proof let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S; set D = DTConOSA(X), PTA = ParsedTermsOSA(X), C = bool [:TS(D), the carrier of S:], SPTA = the Sorts of PTA, F = PTClasses X; defpred R3[set] means for s1,s2 being Element of S, y being Element of TS(DTConOSA X) st s1 <= s2 & $1 in SPTA.s1 & y in SPTA.s1 holds ([y,s1] in (PTClasses X).$1 iff [y,s2] in (PTClasses X).$1); reconsider SPTA1 = SPTA as OrderSortedSet of S by OSALG_1:17; A1: for s1,s2 being Element of S st s1 <= s2 holds SPTA.s1 c= SPTA.s2 proof let s1,s2 be Element of S such that A2: s1 <= s2; reconsider s11 = s1, s21= s2 as Element of S; SPTA1.s11 c= SPTA1.s21 by A2,OSALG_1:def 18; hence SPTA.s1 c= SPTA.s2; end; A3: for s being Symbol of D st s in Terminals D holds R3[root-tree s] proof let sy be Symbol of D such that A4: sy in Terminals D; reconsider sy1 = sy as Terminal of D by A4; A5: F.(root-tree sy) = @(sy) by A4,Def22 .= {[root-tree sy,s1] where s1 is Element of S: ex s2 be Element of S, x be set st x in X.s2 & sy = [x,s2] & s2 <= s1} by Def20; let s1,s2 be Element of S, y be Element of TS D such that A6: s1 <= s2 & root-tree sy in SPTA.s1 & y in SPTA.s1; A7: [root-tree sy1,s1] in F.(root-tree sy) by A6,Th20; SPTA.s1 c= SPTA.s2 by A1,A6; then A8: [root-tree sy1,s2] in F.(root-tree sy) by A6,Th20; hereby assume [y,s1] in F.(root-tree sy); then consider s3 being Element of S such that A9: [y,s1] = [root-tree sy,s3] and ex s2 be Element of S, x be set st x in X.s2 & sy = [x,s2] & s2 <= s3 by A5; thus [y,s2] in F.(root-tree sy) by A8,A9,ZFMISC_1:33; end; assume [y,s2] in F.(root-tree sy); then consider s3 being Element of S such that A10: [y,s2] = [root-tree sy,s3] and ex s4 be Element of S, x be set st x in X.s4 & sy = [x,s4] & s4 <= s3 by A5; thus [y,s1] in F.(root-tree sy) by A7,A10,ZFMISC_1:33; end; A11: for nt being Symbol of D, ts being FinSequence of TS(D) st nt ==> roots ts & for t being DecoratedTree of the carrier of D st t in rng ts holds R3[t] holds R3[nt-tree ts] proof let nt be Symbol of D, ts be FinSequence of TS(D) such that A12: nt ==> roots ts and for t being DecoratedTree of the carrier of D st t in rng ts holds R3[t]; consider o being OperSymbol of S such that A13: nt = [o,the carrier of S] & ts in Args(o,PTA) & nt-tree ts = Den(o,PTA).ts & for s1 being Element of S holds nt-tree ts in (the Sorts of PTA).s1 iff the_result_sort_of o <= s1 by A12,Th12; reconsider x = F * ts as FinSequence of C; A14: F.(nt-tree ts) = @(nt,x) by A12,Def22 .= {[Den(o2,ParsedTermsOSA(X)).x2,s3] where o2 is OperSymbol of S, x2 is Element of Args(o2,ParsedTermsOSA(X)), s3 is Element of S : ( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] & o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of (the carrier of S)* st dom w3 = dom x & for y being Nat st y in dom x holds [x2.y,w3/.y] in x.y} by Def21; let s1,s2 be Element of S, y be Element of TS D such that A15: s1 <= s2 & nt-tree ts in SPTA.s1 & y in SPTA.s1; A16: the_result_sort_of o <= s1 by A13,A15; hereby assume [y,s1] in F.(nt-tree ts); then consider o2 being OperSymbol of S, x2 being Element of Args(o2,PTA), s3 being Element of S such that A17: [y,s1] = [Den(o2,PTA).x2,s3] and A18: ( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] & o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of (the carrier of S)* st dom w3 = dom x & for y being Nat st y in dom x holds [x2.y,w3/.y] in x.y by A14; A19: y = Den(o2,PTA).x2 & s1 = s3 by A17,ZFMISC_1:33; consider o1 being OperSymbol of S such that A20: nt = [o1,the carrier of S] & o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 by A18; reconsider s21 = s2 as Element of S; the_result_sort_of o1 <= s21 & the_result_sort_of o2 <= s21 by A15,A19,A20,ORDERS_1:26; hence [y,s2] in F.(nt-tree ts) by A14,A18,A19,A20; end; assume [y,s2] in F.(nt-tree ts); then consider o2 being OperSymbol of S, x2 being Element of Args(o2,PTA), s3 being Element of S such that A21: [y,s2] = [Den(o2,PTA).x2,s3] and A22: ( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] & o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of (the carrier of S)* st dom w3 = dom x & for y being Nat st y in dom x holds [x2.y,w3/.y] in x.y by A14; A23: y = Den(o2,PTA).x2 & s2 = s3 by A21,ZFMISC_1:33; consider o1 being OperSymbol of S such that A24: nt = [o1,the carrier of S] & o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 by A22; A25: the_result_sort_of o1 <= s1 by A13,A16,A24,ZFMISC_1:33; A26: x2 is FinSequence of TS D & OSSym(o2,X) ==> roots x2 by Th13; reconsider x3 = x2 as FinSequence of TS D by Th13; consider o3 being OperSymbol of S such that A27: OSSym(o2,X) = [o3,the carrier of S] & x3 in Args(o3,PTA) & OSSym(o2,X)-tree x3 = Den(o3,PTA).x3 & for s2 being Element of S holds OSSym(o2,X)-tree x3 in (the Sorts of PTA).s2 iff the_result_sort_of o3 <= s2 by A26,Th12; [o2,the carrier of S] = [o3,the carrier of S] by A27,Def6; then o2 = o3 by ZFMISC_1:33; then the_result_sort_of o2 <= s1 by A15,A23,A27; hence [y,s1] in F.(nt-tree ts) by A14,A22,A23,A24,A25; end; for t being DecoratedTree of the carrier of D st t in TS(D) holds R3[t] from DTConstrInd(A3,A11); hence thesis; end; theorem Th23: for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, x,y,z being Element of TS DTConOSA(X), s being Element of S holds [y,s] in (PTClasses X).x & [z,s] in (PTClasses X).y implies [x,s] in (PTClasses X).z proof let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S; set D = DTConOSA(X), PTA = ParsedTermsOSA(X), C = bool [:TS(D), the carrier of S:], SPTA = the Sorts of PTA, F = PTClasses X; defpred R3[set] means for s being Element of S, y,z being Element of TS(D) holds [y,s] in F.$1 & [z,s] in F.y implies [$1,s] in F.z; A1: for s being Symbol of D st s in Terminals D holds R3[root-tree s] proof let sy be Symbol of D such that A2: sy in Terminals D; A3: F.(root-tree sy) = @(sy) by A2,Def22 .= {[root-tree sy,s1] where s1 is Element of S: ex s2 be Element of S, x be set st x in X.s2 & sy = [x,s2] & s2 <= s1} by Def20; thus R3[root-tree sy] proof let s1 be Element of S, y,z be Element of TS(D); assume A4: [y,s1] in F.(root-tree sy) & [z,s1] in F.y; then consider s2 being Element of S such that A5: [y,s1] = [root-tree sy,s2] and ex s0 be Element of S, x be set st x in X.s0 & sy = [x,s0] & s0 <= s2 by A3; A6: y = root-tree sy & s1 = s2 by A5,ZFMISC_1:33; then consider s3 being Element of S such that A7: [z,s1] = [root-tree sy,s3] and ex s0 be Element of S, x be set st x in X.s0 & sy = [x,s0] & s0 <= s3 by A3,A4; thus [root-tree sy,s1] in F.z by A4,A6,A7,ZFMISC_1:33; end; end; A8: for nt being Symbol of D, ts being FinSequence of TS(D) st nt ==> roots ts & for t being DecoratedTree of the carrier of D st t in rng ts holds R3[t] holds R3[nt-tree ts] proof let nt be Symbol of D, ts be FinSequence of TS(D) such that A9: nt ==> roots ts and A10: for t being DecoratedTree of the carrier of D st t in rng ts holds R3[t]; consider o being OperSymbol of S such that A11: nt = [o,the carrier of S] & ts in Args(o,PTA) & nt-tree ts = Den(o,PTA).ts & for s1 being Element of S holds nt-tree ts in (the Sorts of PTA).s1 iff the_result_sort_of o <= s1 by A9,Th12; reconsider ts1 = ts as Element of Args(o,PTA) by A11; set w = the_arity_of o; reconsider x = F * ts as FinSequence of C; A12: rng ts c= TS D & dom F = TS D by FINSEQ_1:def 4,FUNCT_2:def 1; then len x = len ts by FINSEQ_2:33; then A13: dom x = dom ts & dom w = dom ts by A11,FINSEQ_3:31,MSUALG_3:6; A14: F.(nt-tree ts) = @(nt,x) by A9,Def22 .= {[Den(o2,ParsedTermsOSA(X)).x2,s3] where o2 is OperSymbol of S, x2 is Element of Args(o2,ParsedTermsOSA(X)), s3 is Element of S : ( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] & o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of (the carrier of S)* st dom w3 = dom x & for y being Nat st y in dom x holds [x2.y,w3/.y] in x.y} by Def21; thus R3[nt-tree ts] proof let s1 be Element of S, y,z be Element of TS(D); assume A15: [y,s1] in F.(nt-tree ts) & [z,s1] in F.y; then consider o2 being OperSymbol of S, x2 being Element of Args(o2,PTA), s3 being Element of S such that A16: [y,s1] = [Den(o2,PTA).x2,s3] and A17: ( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] & o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of (the carrier of S)* st dom w3 = dom x & for y being Nat st y in dom x holds [x2.y,w3/.y] in x.y by A14; A18: y = Den(o2,PTA).x2 & s1 = s3 by A16,ZFMISC_1:33; consider o1 being OperSymbol of S such that A19: nt = [o1,the carrier of S] & o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 by A17; A20: o1 = o by A11,A19,ZFMISC_1:33; A21: x2 is FinSequence of TS D & OSSym(o2,X) ==> roots x2 by Th13; reconsider x3 = x2 as FinSequence of TS D by Th13; consider o3 being OperSymbol of S such that A22: OSSym(o2,X) = [o3,the carrier of S] & x3 in Args(o3,PTA) & OSSym(o2,X)-tree x3 = Den(o3,PTA).x3 & for s2 being Element of S holds OSSym(o2,X)-tree x3 in (the Sorts of PTA).s2 iff the_result_sort_of o3 <= s2 by A21,Th12; [o2,the carrier of S] = [o3,the carrier of S] by A22,Def6; then A23: o2 = o3 by ZFMISC_1:33; A24: dom the_arity_of o2 = dom the_arity_of o by A19,A20,FINSEQ_3:31; consider w3 being Element of (the carrier of S)* such that A25: dom w3 = dom x & for y being Nat st y in dom x holds [x2.y,w3/.y] in x.y by A17; reconsider xy = F * x3 as FinSequence of C; rng x3 c= TS D by FINSEQ_1:def 4; then rng x3 c= dom F by FUNCT_2:def 1; then len xy = len x3 by FINSEQ_2:33; then A26: dom x3 = dom xy by FINSEQ_3:31; A27: dom x2 = dom x by A13,A24,MSUALG_3:6; A28: F.y = @(OSSym(o2,X),xy) by A18,A21,A22,A23,Def22 .= {[Den(o4,PTA).x4,s4] where o4 is OperSymbol of S, x4 is Element of Args(o4,PTA), s4 is Element of S : ( ex o1 being OperSymbol of S st OSSym(o2,X) = [o1,the carrier of S] & o1 ~= o4 & len the_arity_of o1 = len the_arity_of o4 & the_result_sort_of o1 <= s4 & the_result_sort_of o4 <= s4 ) & ex w4 being Element of (the carrier of S)* st dom w4 = dom xy & for y being Nat st y in dom xy holds [x4.y,w4/.y] in xy.y} by Def21; A29: OSSym(o2,X) = [o2,the carrier of S] by Def6; consider o5 being OperSymbol of S, x5 being Element of Args(o5,PTA), s5 being Element of S such that A30: [z,s1] = [Den(o5,PTA).x5,s5] and A31: ( ex o1 being OperSymbol of S st OSSym(o2,X) = [o1,the carrier of S] & o1 ~= o5 & len the_arity_of o1 = len the_arity_of o5 & the_result_sort_of o1 <= s5 & the_result_sort_of o5 <= s5 ) & ex w3 being Element of (the carrier of S)* st dom w3 = dom xy & for y being Nat st y in dom xy holds [x5.y,w3/.y] in xy.y by A15,A28; A32: z = Den(o5,PTA).x5 & s1 = s5 by A30,ZFMISC_1:33; consider o6 being OperSymbol of S such that A33: OSSym(o2,X) = [o6,the carrier of S] & o6 ~= o5 & len the_arity_of o6 = len the_arity_of o5 & the_result_sort_of o6 <= s5 & the_result_sort_of o5 <= s5 by A31; A34: o6 = o2 by A29,A33,ZFMISC_1:33; A35: x5 is FinSequence of TS D & OSSym(o5,X) ==> roots x5 by Th13; reconsider x6 = x5 as FinSequence of TS D by Th13; consider o7 being OperSymbol of S such that A36: OSSym(o5,X) = [o7,the carrier of S] & x6 in Args(o7,PTA) & OSSym(o5,X)-tree x6 = Den(o7,PTA).x6 & for s2 being Element of S holds OSSym(o5,X)-tree x6 in (the Sorts of PTA).s2 iff the_result_sort_of o7 <= s2 by A35,Th12; [o5,the carrier of S] = [o7,the carrier of S] by A36,Def6; then A37: o5 = o7 by ZFMISC_1:33; A38: dom the_arity_of o5 = dom the_arity_of o2 by A33,A34,FINSEQ_3:31; consider w5 being Element of (the carrier of S)* such that A39: dom w5 = dom xy & for y being Nat st y in dom xy holds [x5.y,w5/.y] in xy.y by A31; reconsider xz = F * x6 as FinSequence of C; A40: rng x6 c= TS D & rng x3 c= TS D by FINSEQ_1:def 4; then rng x6 c= dom F by FUNCT_2:def 1; then len xz = len x6 by FINSEQ_2:33; then A41: dom x6 = dom xz by FINSEQ_3:31; A42: dom x5 = dom (the_arity_of o2) by A38,MSUALG_3:6 .= dom xy by A26,MSUALG_3:6; defpred P[set,set] means [ts1.$1,$2] in xz.$1; A43: for y being set st y in dom xz ex sy being set st sy in the carrier of S & P[y,sy] proof let y be set such that A44: y in dom xz; A45: y in dom ts1 & y in dom x5 & y in dom x2 & y in dom x by A13,A24,A26,A41,A42,A44,MSUALG_3:6; A46: ts1.y in rng ts1 & x5.y in rng x6 & x2.y in rng x3 by A13,A26,A27,A41,A42,A44,FUNCT_1:12; then reconsider t1 = ts1.y,t2 = x3.y,t3 = x5.y as Element of TS D by A12,A40; [x5.y,w5/.y] in xy.y by A39,A41,A42,A44; then A47: [t3,w5/.y] in F.(t2) by A26,A41,A42,A44,FUNCT_1:23; then A48: [t2,w5/.y] in F.(t2) & [t2,w5/.y] in F.t3 by Th20,Th21; then [t3,w5/.y] in F.t3 by Th21; then A49: t2 in SPTA.(w5/.y) & t3 in SPTA.(w5/.y) by A48,Th20; then A50: LeastSort t2 <= w5/.y by Def12; A51: [x2.y,w3/.y] in x.y by A25,A26,A27,A41,A42,A44; then A52: [x2.y,w3/.y] in F.(ts1.y) by A13,A26,A27,A41,A42,A44,FUNCT_1 :23; [t2,w3/.y] in F.(t1) by A45,A51,FUNCT_1:23; then A53: [t1,w3/.y] in F.t2 & [t1,w3/.y] in F.t1 by Th20,Th21; then [t2,w3/.y] in F.t2 by Th21; then A54: t2 in SPTA.(w3/.y) & t1 in SPTA.(w3/.y) by A53,Th20; then LeastSort t2 <= w3/.y by Def12; then consider s7 being Element of S such that A55: w5/.y <= s7 & w3/.y <= s7 by A50,OSALG_4:12; A56: [t2,s7] in F.t1 by A52,A54,A55,Th22; [t3,s7] in F.t2 by A47,A49,A55,Th22; then A57: [t1,s7] in F.t3 by A10,A46,A56; take s7; thus s7 in the carrier of S; thus [ts1.y,s7] in xz.y by A44,A57,FUNCT_1:22; end; consider f being Function of dom xz,(the carrier of S) such that A58: for y being set st y in dom xz holds P[y,f.y] from FuncEx1(A43); A59: dom f = dom xz by FUNCT_2:def 1; then ex n being Nat st dom f = Seg n by FINSEQ_1:def 2; then reconsider f1 = f as FinSequence by FINSEQ_1:def 2; rng f c= the carrier of S by RELSET_1:12; then f1 is FinSequence of the carrier of S by FINSEQ_1:def 4; then reconsider f as Element of (the carrier of S)* by FINSEQ_1:def 11; A60: dom f = dom xz & for y being Nat st y in dom xz holds [ts1.y,f/.y] in xz.y proof thus dom f = dom xz by FUNCT_2:def 1; let y be Nat such that A61: y in dom xz; [ts1.y,f.y] in xz.y by A58,A61; hence [ts1.y,f/.y] in xz.y by A59,A61,FINSEQ_4:def 4; end; A62: F.z = @(OSSym(o5,X),xz) by A32,A35,A36,A37,Def22 .= {[Den(o4,PTA).x4,s4] where o4 is OperSymbol of S, x4 is Element of Args(o4,PTA), s4 is Element of S : ( ex o1 being OperSymbol of S st OSSym(o5,X) = [o1,the carrier of S] & o1 ~= o4 & len the_arity_of o1 = len the_arity_of o4 & the_result_sort_of o1 <= s4 & the_result_sort_of o4 <= s4 ) & ex w4 being Element of (the carrier of S)* st dom w4 = dom xz & for y being Nat st y in dom xz holds [x4.y,w4/.y] in xz.y} by Def21; OSSym(o5,X) = [o5,the carrier of S] & o5 ~= o & len the_arity_of o5 = len the_arity_of o & the_result_sort_of o5 <= s1 & the_result_sort_of o <= s1 by A16,A19,A20,A30,A33,A34,Def6,OSALG_1:2,ZFMISC_1:33; hence [nt-tree ts,s1] in F.z by A11,A60,A62; end; end; for t being DecoratedTree of the carrier of D st t in TS(D) holds R3[t] from DTConstrInd(A1,A8); hence thesis; end; definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S; func PTCongruence(X) -> MSEquivalence-like OrderSortedRelation of ParsedTermsOSA(X) means :Def23: for i being set st i in the carrier of S holds it.i = {[x,y] where x,y is Element of TS(DTConOSA(X)): [x,i] in (PTClasses X).y}; existence proof set PTA = ParsedTermsOSA(X), SPTA = the Sorts of PTA, D = DTConOSA(X), F = PTClasses X; deffunc F(set) = {[x,y] where x,y is Element of TS(D): [x,$1] in F.y}; consider R being ManySortedSet of the carrier of S such that A1: for i being set st i in the carrier of S holds R.i = F(i) from MSSLambda; defpred IRREL[Element of TS D,Element of S] means (ex s1 being Element of S, x be set st s1 <= $2 & x in X.s1 & $1 = root-tree [x,s1]) or ex o be OperSymbol of S st [o,the carrier of S] = $1.{} & the_result_sort_of o <= $2; for i be set st i in the carrier of S holds R.i is Relation of SPTA.i proof let i be set such that A2: i in the carrier of S; reconsider s = i as Element of S by A2; A3: R.i = {[x,y] where x,y is Element of TS(D): [x,i] in F.y} by A1,A2; R.s c= [:SPTA.s,SPTA.s:] proof let z be set such that A4: z in R.s; consider x,y being Element of TS D such that A5: z = [x,y] and A6: [x,s] in F.y by A3,A4; [y,s] in F.x by A6,Th20; then [x,s] in F.x & [y,s] in F.y by A6,Th21; then x in SPTA.s & y in SPTA.s by Th20; hence thesis by A5,ZFMISC_1:106; end; hence R.i is Relation of SPTA.i,SPTA.i by RELSET_1:def 1; end; then R is ManySortedRelation of SPTA,SPTA by MSUALG_4:def 2; then reconsider R as ManySortedRelation of PTA; for s1,s2 being Element of S st s1 <= s2 for x,y being set st x in SPTA.s1 & y in SPTA.s1 holds [x,y] in R.s1 iff [x,y] in R.s2 proof let s1,s2 be Element of S such that A7: s1 <= s2; A8: R.s1 = {[x,y] where x,y is Element of TS(D): [x,s1] in F.y} by A1; A9: R.s2 = {[x,y] where x,y is Element of TS(D): [x,s2] in F.y} by A1; let x,y be set such that A10: x in SPTA.s1 & y in SPTA.s1; hereby assume [x,y] in R.s1; then consider t1,t2 being Element of TS D such that A11: [x,y] = [t1,t2] & [t1,s1] in F.t2 by A8; x = t1 & y = t2 by A11,ZFMISC_1:33; then [t1,s2] in F.t2 by A7,A10,A11,Th22; hence [x,y] in R.s2 by A9,A11; end; assume [x,y] in R.s2; then consider t1,t2 being Element of TS D such that A12: [x,y] = [t1,t2] & [t1,s2] in F.t2 by A9; x = t1 & y = t2 by A12,ZFMISC_1:33; then [t1,s1] in F.t2 by A7,A10,A12,Th22; hence [x,y] in R.s1 by A8,A12; end; then R is os-compatible by OSALG_4:def 1; then reconsider R as OrderSortedRelation of PTA by OSALG_4:def 3; for i be set, Ri be Relation of SPTA.i st i in the carrier of S & R.i = Ri holds Ri is total symmetric transitive Relation of SPTA.i proof let i be set, Ri be Relation of SPTA.i such that A13: i in the carrier of S & R.i = Ri; reconsider s = i as Element of S by A13; A14: Ri = {[x,y] where x,y is Element of TS(D): [x,i] in F.y} by A1,A13; A15: SPTA.s = {a where a is Element of TS(DTConOSA(X)): IRREL[a,s]} by Th9; now let x be set such that A16: x in SPTA.i; consider t being Element of TS D such that A17: x = t and IRREL[t,s] by A15,A16; [t,s] in F.t by A16,A17,Th20; hence [x,x] in Ri by A14,A17; end; then Ri is_reflexive_in SPTA.i by RELAT_2:def 1; then A18: dom Ri = SPTA.i & field Ri = SPTA.i by ORDERS_1:98; then A19: Ri is total by PARTFUN1:def 4; for x,y being set holds x in SPTA.i & y in SPTA.i & [x,y] in Ri implies [y,x] in Ri proof let x,y be set such that A20: x in SPTA.i & y in SPTA.i & [x,y] in Ri; consider t1,t2 being Element of TS D such that A21: [x,y] = [t1,t2] & [t1,s] in F.t2 by A14,A20; A22: x = t1 & y = t2 by A21,ZFMISC_1:33; [t2,s] in F.t1 by A21,Th20; hence [y,x] in Ri by A14,A22; end; then A23: Ri is_symmetric_in SPTA.i by RELAT_2:def 3; now let x,y,z be set such that x in SPTA.i & y in SPTA.i & z in SPTA.i and A24: [x,y] in Ri & [y,z] in Ri; consider t1,t2 being Element of TS D such that A25: [x,y] = [t1,t2] & [t1,s] in F.t2 by A14,A24; A26: x = t1 & y = t2 by A25,ZFMISC_1:33; consider t22,t3 being Element of TS D such that A27: [y,z] = [t22,t3] & [t22,s] in F.t3 by A14,A24; A28: z = t3 & y = t22 by A27,ZFMISC_1:33; then [t2,s] in F.t1 & [t3,s] in F.t2 by A25,A26,A27,Th20; then [t1,s] in F.t3 by Th23; hence [x,z] in Ri by A14,A26,A28; end; then Ri is_transitive_in SPTA.i by RELAT_2:def 8; hence thesis by A18,A19,A23,RELAT_2:def 11,def 16; end; then R is MSEquivalence_Relation-like by MSUALG_4:def 3; then reconsider R as MSEquivalence-like OrderSortedRelation of PTA by MSUALG_4:def 5; take R; thus thesis by A1; end; uniqueness proof set D = DTConOSA(X), F = PTClasses X; let R1,R2 be MSEquivalence-like OrderSortedRelation of ParsedTermsOSA(X) such that A29: for i being set st i in the carrier of S holds R1.i = {[x,y] where x,y is Element of TS(D): [x,i] in F.y} and A30: for i being set st i in the carrier of S holds R2.i = {[x,y] where x,y is Element of TS(D): [x,i] in F.y}; now let i be set such that A31: i in the carrier of S; R1.i = {[x,y] where x,y is Element of TS(D): [x,i] in F.y} & R2.i = {[x,y] where x,y is Element of TS(D): [x,i] in F.y} by A29,A30,A31; hence R1.i = R2.i; end; hence R1 = R2 by PBOOLE:3; end; end; theorem Th24: for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, x,y,s being set st [x,s] in (PTClasses X).y holds x in TS DTConOSA(X) & y in TS DTConOSA(X) & s in the carrier of S proof let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S; set D = DTConOSA(X), F = PTClasses X; let x,y,s being set such that A1: [x,s] in (PTClasses X).y; A2: dom F = TS(D) & rng F c= bool [:TS(D), the carrier of S:] by FUNCT_2:def 1,RELSET_1:12; A3: y in TS D proof assume not y in TS D; then not y in dom F; hence contradiction by A1,FUNCT_1:def 4; end; then F.y in rng F by A2,FUNCT_1:12; hence thesis by A1,A2,A3,ZFMISC_1:106; end; theorem Th25: for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, C be Component of S, x,y being set holds [x,y] in CompClass(PTCongruence X,C) iff ex s1 being Element of S st s1 in C & [x,s1] in (PTClasses X).y proof let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, C be Component of S, x,y being set; hereby assume [x,y] in CompClass(PTCongruence X,C); then consider s1 being Element of S such that A1: s1 in C & [x,y] in (PTCongruence X).s1 by OSALG_4:def 11; [x,y] in {[x1,y1] where x1,y1 is Element of TS(DTConOSA(X)): [x1,s1] in (PTClasses X).y1} by A1,Def23; then consider x1,y1 being Element of TS(DTConOSA(X)) such that A2: [x,y] = [x1,y1] and A3: [x1,s1] in (PTClasses X).y1; take s1; x = x1 & y = y1 by A2,ZFMISC_1:33; hence s1 in C & [x,s1] in (PTClasses X).y by A1,A3; end; given s1 being Element of S such that A4: s1 in C & [x,s1] in (PTClasses X).y; reconsider x2 = x, y2 = y as Element of TS(DTConOSA(X)) by A4,Th24; [x2,y2] in {[x1,y1] where x1,y1 is Element of TS(DTConOSA(X)): [x1,s1] in (PTClasses X).y1} by A4; then [x2,y2] in (PTCongruence(X)).s1 by Def23; hence thesis by A4,OSALG_4:def 11; end; theorem Th26: for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, s be Element of S, x be Element of (the Sorts of ParsedTermsOSA(X)).s holds OSClass(PTCongruence X,x) = proj1((PTClasses X).x) proof let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, s be Element of S, x be Element of (the Sorts of ParsedTermsOSA(X)).s; set R = PTCongruence X, PTA = ParsedTermsOSA(X), D = DTConOSA(X); A1: OSClass(R,x) = Class( CompClass(R, CComp(s)), x) by OSALG_4:def 14; for z being set holds z in OSClass(R,x) iff z in proj1((PTClasses X).x) proof let z be set; hereby assume z in OSClass(R,x); then [z,x] in CompClass(R, CComp(s)) by A1,EQREL_1:27; then consider s1 being Element of S such that A2: s1 in CComp(s) & [z,s1] in (PTClasses X).x by Th25; thus z in proj1((PTClasses X).x) by A2,FUNCT_5:def 1; end; assume z in proj1((PTClasses X).x); then consider s1 being set such that A3: [z,s1] in (PTClasses X).x by FUNCT_5:def 1; reconsider x1=x,z1=z as Element of TS(D) by A3,Th24; reconsider s2 = s1 as Element of S by A3,Th24; [z1,s2] in (PTClasses X).x1 by A3; then [x1,s2] in (PTClasses X).x1 by Th21; then x in (the Sorts of PTA).s1 by Th20; then A4: LeastSort x1 <= s2 & LeastSort x1 <= s by Def12; then CComp(s2) = CComp(LeastSort x1) by OSALG_4:5 .= CComp(s) by A4,OSALG_4:5; then s2 in CComp(s) by OSALG_4:4; then [z,x] in CompClass(R,CComp(s)) by A3,Th25; hence z in OSClass(R,x) by A1,EQREL_1:27; end; hence thesis by TARSKI:2; end; :: more explicit description of PTCongruence theorem Th27: for S being locally_directed OrderSortedSign, X being non-empty ManySortedSet of S, R being ManySortedRelation of ParsedTermsOSA(X) holds R = PTCongruence(X) iff ( for s1,s2 being Element of S, x being set st x in X.s1 holds ( s1 <= s2 implies [root-tree [x,s1],root-tree[x,s1]] in R.s2 ) & for y being set holds ( [root-tree [x,s1],y] in R.s2 or [y,root-tree [x,s1]] in R.s2) implies s1 <= s2 & y = root-tree [x,s1] ) & for o1,o2 being OperSymbol of S, x1 being Element of Args(o1,ParsedTermsOSA(X)), x2 being Element of Args(o2,ParsedTermsOSA(X)), s3 being Element of S holds [Den(o1,ParsedTermsOSA(X)).x1,Den(o2,ParsedTermsOSA(X)).x2] in R.s3 iff o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 & ex w3 being Element of (the carrier of S)* st dom w3 = dom x1 & ( for y being Nat st y in dom w3 holds [x1.y,x2.y] in R.(w3/.y) ) proof let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, R be ManySortedRelation of ParsedTermsOSA(X); set PTA = ParsedTermsOSA(X), SPTA = the Sorts of PTA, D = DTConOSA(X), OU = [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod (X qua ManySortedSet of S)), C = bool [:TS(D), the carrier of S:], F = PTClasses X; A1: PTA = MSAlgebra (# ParsedTerms(X), PTOper(X) #) by Def11; defpred T[ ManySortedSet of the carrier of S] means ( for s1,s2 being Element of S, x being set st x in X.s1 holds ( s1 <= s2 implies [root-tree [x,s1],root-tree[x,s1]] in $1.s2 ) & for y being set holds ( [root-tree [x,s1],y] in $1.s2 or [y,root-tree [x,s1]] in $1.s2) implies s1 <= s2 & y = root-tree [x,s1] ); defpred NT[ ManySortedSet of the carrier of S] means for o1,o2 being OperSymbol of S, x1 being Element of Args(o1,ParsedTermsOSA(X)), x2 being Element of Args(o2,ParsedTermsOSA(X)), s3 being Element of S holds [Den(o1,ParsedTermsOSA(X)).x1,Den(o2,ParsedTermsOSA(X)).x2] in $1.s3 iff o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 & ex w3 being Element of (the carrier of S)* st dom w3 = dom x1 & ( for y being Nat st y in dom w3 holds [x1.y,x2.y] in $1.(w3/.y) ); A2: for R1,R2 be ManySortedRelation of PTA st T[R1] & NT[R1] & T[R2] & NT[R2] holds R1 = R2 proof let R1,R2 be ManySortedRelation of PTA; assume that A3: T[R1] & NT[R1] and A4: T[R2] & NT[R2]; defpred P[set] means for x being set, s being Element of S holds [$1,x] in R1.s iff [$1,x] in R2.s; A5: for s being Symbol of D st s in Terminals D holds P[root-tree s] proof let sy be Symbol of D such that A6: sy in Terminals D; consider s being Element of S, x being set such that A7: x in X.s & sy = [x,s] by A6,Th4; let y be set, s1 be Element of S; hereby assume [root-tree sy,y] in R1.s1; then s <= s1 & y = root-tree [x,s] by A3,A7; hence [root-tree sy,y] in R2.s1 by A4,A7; end; assume [root-tree sy,y] in R2.s1; then s <= s1 & y = root-tree [x,s] by A4,A7; hence [root-tree sy,y] in R1.s1 by A3,A7; end; A8: for nt being Symbol of D, ts being FinSequence of TS(D) st nt ==> roots ts & for t being DecoratedTree of the carrier of D st t in rng ts holds P[t] holds P[nt-tree ts] proof let nt be Symbol of D, ts be FinSequence of TS(D) such that A9: nt ==> roots ts and A10: for t being DecoratedTree of the carrier of D st t in rng ts holds P[t]; nt in { s where s is Symbol of D: ex n being FinSequence st s ==> n} by A9; then reconsider nt1 = nt as NonTerminal of D by LANG1:def 3; reconsider tss = ts as SubtreeSeq of nt1 by A9,DTCONSTR:def 9; let x be set, s be Element of S; A11: (the Sorts of PTA).s = ParsedTerms(X,s) by A1,Def8 .= {a1 where a1 is Element of TS(DTConOSA(X)): (ex s1 being Element of S, x be set st s1 <= s & x in X.s1 & a1 = root-tree [x,s1]) or ex o be OperSymbol of S st [o,the carrier of S] = a1.{} & the_result_sort_of o <= s} by Def7; A12: [nt,roots ts] in the Rules of D by A9,LANG1:def 1; A13: D = DTConstrStr (# OU, OSREL(X)#) & Terminals D = Union (coprod X) by Def5,Th3; then reconsider sy = nt as Element of OU; reconsider rt = roots ts as Element of OU* by A12,A13,ZFMISC_1:106; [sy,rt] in OSREL(X) by A9,A13,LANG1:def 1; then sy in [:the OperSymbols of S,{the carrier of S}:] by Def4; then consider o being Element of the OperSymbols of S, x2 being Element of {the carrier of S} such that A14: sy = [o,x2] by DOMAIN_1:9; A15: x2 = the carrier of S by TARSKI:def 1; then A16: (nt-tree tss).{} = [o,the carrier of S] by A14,TREES_4:def 4; A17: rng ts c= TS D by FINSEQ_1:def 4; hereby assume A18: [nt-tree ts,x] in R1.s; then nt-tree ts in (the Sorts of PTA).s & x in (the Sorts of PTA).s by ZFMISC_1:106; then consider a1 being Element of TS(DTConOSA(X)) such that A19: x = a1 and A20: (ex s1 being Element of S, y be set st s1 <= s & y in X.s1 & a1 = root-tree [y,s1]) or ex o be OperSymbol of S st [o,the carrier of S] = a1.{} & the_result_sort_of o <= s by A11; not ex s1 being Element of S, y be set st s1 <= s & y in X.s1 & a1 = root-tree [y,s1] proof given s1 being Element of S, y be set such that A21: s1 <= s & y in X.s1 & a1 = root-tree [y,s1]; nt-tree ts = root-tree [y,s1] by A3,A18,A19,A21; then [y,s1] = nt & ts = {} by TREES_4:17; then the carrier of S = s1 by A14,A15,ZFMISC_1:33; then s1 in s1; hence contradiction; end; then consider o1 be OperSymbol of S such that A22: [o1,the carrier of S] = a1.{} & the_result_sort_of o1 <= s by A20; consider ts1 being SubtreeSeq of OSSym(o1,X) such that A23: a1 = OSSym(o1,X)-tree ts1 & OSSym(o1,X) ==> roots ts1 & ts1 in Args(o1,PTA) & a1 = Den(o1,PTA).ts1 by A22,Th11; consider ts2 being SubtreeSeq of OSSym(o,X) such that A24: nt1-tree tss = OSSym(o,X)-tree ts2 & OSSym(o,X) ==> roots ts2 & ts2 in Args(o,PTA) & nt1-tree tss = Den(o,PTA).ts2 by A16,Th11; A25: ts2 = tss by A24,TREES_4:15; reconsider tsa = ts1 as Element of Args(o1,PTA) by A23; reconsider tsb = ts2 as Element of Args(o,PTA) by A24; A26: o ~= o1 & len the_arity_of o = len the_arity_of o1 & the_result_sort_of o <= s & the_result_sort_of o1 <= s & ex w3 being Element of (the carrier of S)* st dom w3 = dom tsb & ( for y being Nat st y in dom w3 holds [tsb.y,tsa.y] in R1.(w3/.y) ) by A3,A18,A19,A23,A24; consider w3 being Element of (the carrier of S)* such that A27: dom w3 = dom tsb & ( for y being Nat st y in dom w3 holds [tsb.y,tsa.y] in R1.(w3/.y) ) by A3,A18,A19,A23,A24; ( for y being Nat st y in dom w3 holds [tsb.y,tsa.y] in R2.(w3/.y) ) proof let y be Nat such that A28: y in dom w3; A29: tsb.y in rng ts by A25,A27,A28,FUNCT_1:12; then reconsider t = tsb.y as Element of TS(D) by A17; [t,tsa.y] in R1.(w3/.y) by A27,A28; hence [tsb.y,tsa.y] in R2.(w3/.y) by A10,A29; end; hence [nt-tree ts,x] in R2.s by A4,A19,A23,A24,A26,A27; end; assume A30: [nt-tree ts,x] in R2.s; then nt-tree ts in (the Sorts of PTA).s & x in (the Sorts of PTA).s by ZFMISC_1:106; then consider a1 being Element of TS(DTConOSA(X)) such that A31: x = a1 and A32: (ex s1 being Element of S, y be set st s1 <= s & y in X.s1 & a1 = root-tree [y,s1]) or ex o be OperSymbol of S st [o,the carrier of S] = a1.{} & the_result_sort_of o <= s by A11; not ex s1 being Element of S, y be set st s1 <= s & y in X.s1 & a1 = root-tree [y,s1] proof given s1 being Element of S, y be set such that A33: s1 <= s & y in X.s1 & a1 = root-tree [y,s1]; nt-tree ts = root-tree [y,s1] by A4,A30,A31,A33; then [y,s1] = nt & ts = {} by TREES_4:17; then the carrier of S = s1 by A14,A15,ZFMISC_1:33; then s1 in s1; hence contradiction; end; then consider o1 be OperSymbol of S such that A34: [o1,the carrier of S] = a1.{} & the_result_sort_of o1 <= s by A32; consider ts1 being SubtreeSeq of OSSym(o1,X) such that A35: a1 = OSSym(o1,X)-tree ts1 & OSSym(o1,X) ==> roots ts1 & ts1 in Args(o1,PTA) & a1 = Den(o1,PTA).ts1 by A34,Th11; consider ts2 being SubtreeSeq of OSSym(o,X) such that A36: nt1-tree tss = OSSym(o,X)-tree ts2 & OSSym(o,X) ==> roots ts2 & ts2 in Args(o,PTA) & nt1-tree tss = Den(o,PTA).ts2 by A16,Th11; A37: ts2 = tss by A36,TREES_4:15; reconsider tsa = ts1 as Element of Args(o1,PTA) by A35; reconsider tsb = ts2 as Element of Args(o,PTA) by A36; A38: o ~= o1 & len the_arity_of o = len the_arity_of o1 & the_result_sort_of o <= s & the_result_sort_of o1 <= s & ex w3 being Element of (the carrier of S)* st dom w3 = dom tsb & ( for y being Nat st y in dom w3 holds [tsb.y,tsa.y] in R2.(w3/.y) ) by A4,A30,A31,A35,A36; consider w3 being Element of (the carrier of S)* such that A39: dom w3 = dom tsb & ( for y being Nat st y in dom w3 holds [tsb.y,tsa.y] in R2.(w3/.y) ) by A4,A30,A31,A35,A36; ( for y being Nat st y in dom w3 holds [tsb.y,tsa.y] in R1.(w3/.y) ) proof let y be Nat such that A40: y in dom w3; A41: tsb.y in rng ts by A37,A39,A40,FUNCT_1:12; then reconsider t = tsb.y as Element of TS(D) by A17; [t,tsa.y] in R2.(w3/.y) by A39,A40; hence [tsb.y,tsa.y] in R1.(w3/.y) by A10,A41; end; hence [nt-tree ts,x] in R1.s by A3,A31,A35,A36,A38,A39; end; A42: for t being DecoratedTree of the carrier of D st t in TS(D) holds P[t] from DTConstrInd(A5,A8); for i being set st i in the carrier of S holds R1.i = R2.i proof let i be set such that A43: i in the carrier of S; reconsider s = i as Element of S by A43; for a,b being set holds [a,b] in R1.s iff [a,b] in R2.s proof let a,b be set; A44: (the Sorts of PTA).s = ParsedTerms(X,s) by A1,Def8 .= {a1 where a1 is Element of TS(DTConOSA(X)): (ex s1 being Element of S, x be set st s1 <= s & x in X.s1 & a1 = root-tree [x,s1]) or ex o be OperSymbol of S st [o,the carrier of S] = a1.{} & the_result_sort_of o <= s} by Def7; hereby assume A45: [a,b] in R1.s; then a in (the Sorts of PTA).s & b in (the Sorts of PTA).s by ZFMISC_1:106; then consider a1 being Element of TS(DTConOSA(X)) such that A46: a = a1 and (ex s1 being Element of S, x be set st s1 <= s & x in X.s1 & a1 = root-tree [x,s1]) or ex o be OperSymbol of S st [o,the carrier of S] = a1.{} & the_result_sort_of o <= s by A44; thus [a,b] in R2.s by A42,A45,A46; end; assume A47: [a,b] in R2.s; then a in (the Sorts of PTA).s & b in (the Sorts of PTA).s by ZFMISC_1:106; then consider a1 being Element of TS(DTConOSA(X)) such that A48: a = a1 and (ex s1 being Element of S, x be set st s1 <= s & x in X.s1 & a1 = root-tree [x,s1]) or ex o be OperSymbol of S st [o,the carrier of S] = a1.{} & the_result_sort_of o <= s by A44; thus [a,b] in R1.s by A42,A47,A48; end; hence R1.i = R2.i by RELAT_1:def 2; end; hence R1 = R2 by PBOOLE:3; end; set P = PTCongruence X; A49: T[P] proof let s1,s2 be Element of S, x be set such that A50: x in X.s1; A51: P.s2 = {[x1,y] where x1,y is Element of TS(DTConOSA(X)): [x1,s2] in F.y} by Def23; reconsider sy = [x,s1] as Terminal of D by A50,Th4; A52: root-tree [x,s1] in SPTA.s1 by A50,Th10; A53: F.(root-tree sy) = @(sy) by Def22 .= {[root-tree sy,s3] where s3 is Element of S: ex s4 be Element of S, x be set st x in X.s4 & sy = [x,s4] & s4 <= s3} by Def20; hereby assume A54: s1 <= s2; [root-tree sy,s1] in F.(root-tree sy) by A52,Th20; then [root-tree sy,s2] in F.(root-tree sy) by A52,A54,Th22; hence [root-tree [x,s1],root-tree[x,s1]] in P.s2 by A51; end; field(P.s2) = SPTA.s2 by ORDERS_1:97; then A55: P.s2 is_symmetric_in SPTA.s2 by RELAT_2:def 11; let y be set; assume A56: [root-tree [x,s1],y] in P.s2 or [y,root-tree [x,s1]] in P.s2; then y in SPTA.s2 & root-tree [x,s1] in SPTA.s2 by ZFMISC_1:106; then [y,root-tree sy] in P.s2 by A55,A56,RELAT_2:def 3; then consider y1,r1 being Element of TS D such that A57: [y,root-tree sy] = [y1,r1] and A58: [y1,s2] in F.(r1) by A51; A59: y = y1 & root-tree sy = r1 by A57,ZFMISC_1:33; then consider s3 being Element of S such that A60: [y1,s2] = [root-tree sy,s3] and A61: ex s4 be Element of S, x be set st x in X.s4 & sy = [x,s4] & s4 <= s3 by A53,A58; consider s4 be Element of S, x be set such that A62: x in X.s4 & sy = [x,s4] & s4 <= s3 by A61; y = root-tree sy & s2 = s3 by A59,A60,ZFMISC_1:33; hence thesis by A62,ZFMISC_1:33; end; NT[PTCongruence X] proof let o1,o2 be OperSymbol of S, x1 be Element of Args(o1,ParsedTermsOSA(X)), x2 be Element of Args(o2,ParsedTermsOSA(X)), s3 be Element of S; A63: P.s3 = {[x3,y] where x3,y is Element of TS(DTConOSA(X)): [x3,s3] in F.y} by Def23; A64: x1 is FinSequence of TS(D) & OSSym(o1,X) ==> roots x1 by Th13; reconsider ts1 = x1 as FinSequence of TS(D) by Th13; A65: Den(o1,PTA).x1 = ((PTOper(X)).o1).x1 by A1,MSUALG_1:def 11 .= PTDenOp(o1,X).ts1 by Def10 .= OSSym(o1,X)-tree ts1 by A64,Def9; A66: x2 is FinSequence of TS(D) & OSSym(o2,X) ==> roots x2 by Th13; reconsider ts2 = x2 as FinSequence of TS(D) by Th13; A67: Den(o2,PTA).x2 = ((PTOper(X)).o2).x2 by A1,MSUALG_1:def 11 .= PTDenOp(o2,X).ts2 by Def10 .= OSSym(o2,X)-tree ts2 by A66,Def9; reconsider x = F * ts1, y = F * ts2 as FinSequence of C; A68: rng ts1 c= TS D & rng ts2 c= TS D & dom F = TS D by FINSEQ_1:def 4,FUNCT_2:def 1; then A69: len x = len ts1 & len y = len ts2 by FINSEQ_2:33; then A70: dom x = dom ts1 & dom y = dom ts2 by FINSEQ_3:31; A71: F.(OSSym(o1,X)-tree ts1) = @(OSSym(o1,X),x) by A64,Def22 .= {[Den(o3,ParsedTermsOSA(X)).x3,s4] where o3 is OperSymbol of S, x3 is Element of Args(o3,ParsedTermsOSA(X)), s4 is Element of S : ( ex o4 being OperSymbol of S st OSSym(o1,X) = [o4,the carrier of S] & o4 ~= o3 & len the_arity_of o4 = len the_arity_of o3 & the_result_sort_of o4 <= s4 & the_result_sort_of o3 <= s4 ) & ex w3 being Element of (the carrier of S)* st dom w3 = dom x & for y being Nat st y in dom x holds [x3.y,w3/.y] in x.y} by Def21; A72: OSSym(o1,X) = [o1,the carrier of S] & OSSym(o2,X) = [o2,the carrier of S] by Def6; A73: dom (the_arity_of o1) = dom x1 & dom (the_arity_of o2) = dom x2 by MSUALG_3:6; reconsider tx = OSSym(o1,X)-tree ts1, ty = OSSym(o2,X)-tree ts2 as Element of TS D by A64,A66,Th12; hereby assume [Den(o1,PTA).x1,Den(o2,PTA).x2] in P.s3; then consider t1,t2 being Element of TS D such that A74: [Den(o1,PTA).x1,Den(o2,PTA).x2] = [t1,t2] and A75: [t1,s3] in F.t2 by A63; A76: Den(o1,PTA).x1 = t1 & Den(o2,PTA).x2 = t2 by A74,ZFMISC_1:33; [t2,s3] in F.t1 by A75,Th20; then consider o3 being OperSymbol of S, x3 being Element of Args(o3,ParsedTermsOSA(X)), s4 being Element of S such that A77: [t2,s3] = [Den(o3,PTA).x3,s4] and A78: ex o4 being OperSymbol of S st OSSym(o1,X) = [o4,the carrier of S] & o4 ~= o3 & len the_arity_of o4 = len the_arity_of o3 & the_result_sort_of o4 <= s4 & the_result_sort_of o3 <= s4 and A79: ex w3 being Element of (the carrier of S)* st dom w3 = dom x & for y being Nat st y in dom x holds [x3.y,w3/.y] in x.y by A65,A71,A76; consider o4 being OperSymbol of S such that A80: OSSym(o1,X) = [o4,the carrier of S] & o4 ~= o3 & len the_arity_of o4 = len the_arity_of o3 & the_result_sort_of o4 <= s4 & the_result_sort_of o3 <= s4 by A78; A81: o1 = o4 & t2 = Den(o3,PTA).x3 & s3 = s4 by A72,A77,A80,ZFMISC_1:33; A82: x3 is FinSequence of TS(D) & OSSym(o3,X) ==> roots x3 by Th13; reconsider ts3 = x3 as FinSequence of TS(D) by Th13; A83: OSSym(o3,X) = [o3,the carrier of S] by Def6; Den(o3,PTA).x3 = ((PTOper(X)).o3).x3 by A1,MSUALG_1:def 11 .= PTDenOp(o3,X).ts3 by Def10 .= OSSym(o3,X)-tree ts3 by A82,Def9; then A84: OSSym(o3,X) = OSSym(o2,X) & ts3 = ts2 by A67,A76,A81,TREES_4:15; then A85: o3 = o2 & x3 = x2 by A72,A83,ZFMISC_1:33; thus o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 by A72,A80,A81,A83,A84,ZFMISC_1:33; A86: dom the_arity_of o1 = dom the_arity_of o2 by A80,A81,A85,FINSEQ_3:31; consider w3 being Element of (the carrier of S)* such that A87: dom w3 = dom x and A88: for y being Nat st y in dom x holds [x3.y,w3/.y] in x.y by A79; take w3; thus dom w3 = dom x1 by A69,A87,FINSEQ_3:31; let y be Nat such that A89: y in dom w3; A90: P.(w3/.y) = {[x5,y5] where x5,y5 is Element of TS(DTConOSA(X)): [x5,w3/.y] in F.y5} by Def23; ts1.y in rng ts1 & ts2.y in rng ts2 by A70,A73,A86,A87,A89,FUNCT_1:12; then reconsider t22 = ts2.y,t11=ts1.y as Element of TS D by A68; [x3.y,w3/.y] in x.y by A87,A88,A89; then [ts2.y,w3/.y] in F.(ts1.y) by A84,A87,A89,FUNCT_1:22; then [t11,w3/.y] in F.(t22) by Th20; hence [x1.y,x2.y] in P.(w3/.y) by A90; end; assume A91: o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 & ex w3 being Element of (the carrier of S)* st dom w3 = dom x1 & ( for y being Nat st y in dom w3 holds [x1.y,x2.y] in P.(w3/.y) ); then consider w3 being Element of (the carrier of S)* such that A92: dom w3 = dom x1 and A93: for y being Nat st y in dom w3 holds [x1.y,x2.y] in P.(w3/.y); for y being Nat st y in dom x holds [x2.y,w3/.y] in x.y proof let y being Nat such that A94: y in dom x; A95: P.(w3/.y) = {[x5,y5] where x5,y5 is Element of TS(DTConOSA(X)): [x5,w3/.y] in F.y5} by Def23; [x1.y,x2.y] in P.(w3/.y) by A70,A92,A93,A94; then consider x5,y5 being Element of TS(DTConOSA(X)) such that A96: [x1.y,x2.y] = [x5,y5] and A97: [x5,w3/.y] in F.y5 by A95; A98: x1.y = x5 & x2.y = y5 by A96,ZFMISC_1:33; [y5,w3/.y] in F.x5 by A97,Th20; hence [x2.y,w3/.y] in x.y by A94,A98,FUNCT_1:22; end; then [Den(o2,PTA).x2,s3] in F.(OSSym(o1,X)-tree ts1) by A70,A71,A72,A91,A92 ; then [tx,s3] in F.(ty) by A67,Th20; hence [Den(o1,PTA).x1,Den(o2,PTA).x2] in P.s3 by A63,A65,A67; end; hence thesis by A2,A49; end; :: the minimality for regular oss is done later theorem Th28: for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S holds PTCongruence(X) is monotone proof let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S; set PTA = ParsedTermsOSA(X), P = PTCongruence X; thus P is monotone proof let o1,o2 be OperSymbol of S such that A1: o1 <= o2; let x1 be Element of Args(o1,PTA), x2 be Element of Args(o2,PTA) such that A2: for y being Nat st y in dom x1 holds [x1.y,x2.y] in P.((the_arity_of o2)/.y); A3: o1 ~= o2 & (the_arity_of o1) <= (the_arity_of o2) & the_result_sort_of o1 <= the_result_sort_of o2 by A1,OSALG_1:def 22; then A4: len (the_arity_of o1) = len (the_arity_of o2) by OSALG_1:def 7; then dom (the_arity_of o2) = dom (the_arity_of o1) by FINSEQ_3:31; then dom the_arity_of o2 = dom x1 by MSUALG_3:6; hence [Den(o1,PTA).x1,Den(o2,PTA).x2] in P.(the_result_sort_of o2) by A2,A3,A4,Th27; end; end; :: MSCongruence-like is ensured by the OSALG_4 cluster definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S; cluster PTCongruence(X) -> monotone; coherence by Th28; end; definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, s be Element of S; func PTVars(s,X) -> Subset of (the Sorts of ParsedTermsOSA(X)).s means:Def24: for x be set holds x in it iff ex a be set st a in X.s & x = root-tree [a,s]; existence proof set D = DTConOSA(X), PTA = ParsedTermsOSA(X), SO = the Sorts of PTA; A1: PTA = MSAlgebra (# ParsedTerms(X), PTOper(X) #) by Def11; defpred P[set] means ex a be set st a in X.s & $1 = root-tree [a,s]; consider A be set such that A2: for x holds x in A iff x in SO.s & P[x] from Separation; A c= SO.s proof let x; assume x in A; hence thesis by A2; end; then reconsider A as Subset of SO.s; for x holds x in A iff P[x] proof let x; thus x in A implies P[x] by A2; assume A3: P[x]; then consider a be set such that A4: a in X.s & x = root-tree [a,s]; A5: (ParsedTerms X).s = ParsedTerms(X,s) by Def8; set A1 = {aa where aa is Element of TS(D): (ex s1 being Element of S,x be set st s1 <= s & x in X.s1 & aa = root-tree [x,s1]) or ex o1 be OperSymbol of S st [o1,the carrier of S] = aa.{} & the_result_sort_of o1 <= s}; A6: A1 = (ParsedTerms X).s by A5,Def7; set sa = [a,s]; A7: sa in coprod(s,X) by A4,MSAFREE:def 2; A8: Terminals D = Union (coprod X) by Th3; dom coprod(X) = the carrier of S by PBOOLE:def 3; then (coprod(X)).s in rng coprod(X) by FUNCT_1:def 5; then coprod(s,X) in rng coprod(X) by MSAFREE:def 3; then sa in union rng coprod(X) by A7,TARSKI:def 4; then A9: sa in Terminals D by A8,PROB_1:def 3; then reconsider sa as Symbol of D; reconsider b = root-tree sa as Element of TS(D) by A9,DTCONSTR:def 4; b in A1 & b = x by A4; hence thesis by A1,A2,A3,A6; end; hence thesis; end; uniqueness proof set PTA = ParsedTermsOSA(X), SO = the Sorts of PTA; let A,B be Subset of SO.s; assume that A10: for x be set holds x in A iff ex a be set st a in X.s & x = root-tree [a,s] and A11: for x be set holds x in B iff ex a be set st a in X.s & x = root-tree [a,s]; thus A c= B proof let x be set; assume x in A; then ex a be set st a in X.s & x =root-tree [a,s] by A10; hence thesis by A11; end; let x be set; assume x in B; then ex a be set st a in X.s & x = root-tree [a,s] by A11; hence thesis by A10; end; end; definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, s be Element of S; cluster PTVars(s,X) -> non empty; coherence proof consider x such that A1: x in X.s by XBOOLE_0:def 1; ex a be set st a in X.s & root-tree [x,s] = root-tree [a,s] by A1; hence thesis by Def24; end; end; theorem Th29: for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, s be Element of S holds PTVars(s,X) = { root-tree t where t is Symbol of DTConOSA(X): t in Terminals DTConOSA(X) & t`2 = s} proof let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, s be Element of S; set D = DTConOSA(X), A = {root-tree t where t is Symbol of D : t in Terminals D & t`2 = s}; thus PTVars(s,X) c= A proof let x be set; assume x in PTVars(s,X); then consider a be set such that A1: a in X.s & x = root-tree [a,s] by Def24; A2: [a,s] in Terminals D by A1,Th4; then reconsider t = [a,s] as Symbol of D; t`2 = s by MCART_1:7; hence thesis by A1,A2; end; let x be set; assume x in A; then consider t be Symbol of D such that A3: x = root-tree t & t in Terminals D & t`2 = s; consider s1 be Element of S, a be set such that A4: a in X.s1 & t = [a,s1] by A3,Th4; s = s1 by A3,A4,MCART_1:7; hence thesis by A3,A4,Def24; end; definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S; func PTVars(X) -> MSSubset of ParsedTermsOSA(X) means :Def25: for s be Element of S holds it.s = PTVars(s,X); existence proof set PTA = ParsedTermsOSA(X), SO = the Sorts of PTA; deffunc F(Element of S) = PTVars($1,X); consider f be Function such that A1: dom f = the carrier of S & for s be Element of S holds f.s = F(s) from LambdaB; reconsider f as ManySortedSet of the carrier of S by A1,PBOOLE:def 3; f c= the Sorts of PTA proof let x; assume x in the carrier of S; then reconsider s = x as Element of S; f.s = PTVars(s,X) & PTVars(s,X) c= SO.s by A1; hence thesis; end; then reconsider f as MSSubset of PTA by MSUALG_2:def 1; take f; thus thesis by A1; end; uniqueness proof let A,B be MSSubset of ParsedTermsOSA(X); assume that A2: for s be Element of S holds A.s = PTVars(s,X) and A3: for s be Element of S holds B.s = PTVars(s,X); for i be set st i in the carrier of S holds A.i = B.i proof let i be set; assume i in the carrier of S; then reconsider s = i as SortSymbol of S; A.s = PTVars(s,X) & B.s = PTVars(s,X) by A2,A3; hence thesis; end; hence thesis by PBOOLE:3; end; end; theorem for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S holds PTVars(X) is non-empty proof let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S; let x; assume x in the carrier of S; then reconsider s = x as Element of S; (PTVars(X)).s = PTVars(s,X) by Def25; hence thesis; end; definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, s be Element of S; func OSFreeGen(s,X) -> Subset of (the Sorts of FreeOSA(X)).s means :Def26: for x be set holds x in it iff ex a be set st a in X.s & x = (OSNat_Hom(ParsedTermsOSA(X),LCongruence(X)).s).(root-tree [a,s]); existence proof set D = DTConOSA(X), PTA = ParsedTermsOSA(X), PTC = LCongruence(X), SO = the Sorts of FreeOSA(X), NH = OSNat_Hom(ParsedTermsOSA(X),LCongruence(X)); A1: PTA = MSAlgebra (# ParsedTerms(X), PTOper(X) #) by Def11; defpred P[set] means ex a be set st a in X.s & $1 = (NH.s).(root-tree [a,s]); consider A be set such that A2: for x holds x in A iff x in SO.s & P[x] from Separation; A c= SO.s proof let x; assume x in A; hence thesis by A2; end; then reconsider A as Subset of SO.s; for x holds x in A iff P[x] proof let x; thus x in A implies P[x] by A2; assume A3: P[x]; then consider a be set such that A4: a in X.s & x = (NH.s).(root-tree [a,s]); A5: (ParsedTerms X).s = ParsedTerms(X,s) by Def8; set A1 = {aa where aa is Element of TS(D): (ex s1 being Element of S,x be set st s1 <= s & x in X.s1 & aa = root-tree [x,s1]) or ex o1 be OperSymbol of S st [o1,the carrier of S] = aa.{} & the_result_sort_of o1 <= s}; A6: A1 = (ParsedTerms X).s by A5,Def7; set sa = [a,s]; A7: sa in coprod(s,X) by A4,MSAFREE:def 2; A8: Terminals D = Union (coprod X) by Th3; dom coprod(X) = the carrier of S by PBOOLE:def 3; then (coprod(X)).s in rng coprod(X) by FUNCT_1:def 5; then coprod(s,X) in rng coprod(X) by MSAFREE:def 3; then sa in union rng coprod(X) by A7,TARSKI:def 4; then A9: sa in Terminals D by A8,PROB_1:def 3; then reconsider sa as Symbol of D; reconsider b = root-tree sa as Element of TS(D) by A9,DTCONSTR:def 4; b in A1 & (NH.s).b = x by A4; then (NH.s).b in (the Sorts of QuotOSAlg(PTA,PTC)).s by A1,A6,FUNCT_2:7; then x in SO.s by A4,Def19; hence thesis by A2,A3; end; hence thesis; end; uniqueness proof set SO = the Sorts of FreeOSA(X), NH = OSNat_Hom(ParsedTermsOSA(X),LCongruence(X)); let A,B be Subset of SO.s; assume that A10: for x be set holds x in A iff ex a be set st a in X.s & x = (NH.s).root-tree [a,s] and A11: for x be set holds x in B iff ex a be set st a in X.s & x = (NH.s).root-tree [a,s]; thus A c= B proof let x be set; assume x in A; then ex a be set st a in X.s & x = (NH.s).root-tree [a,s] by A10; hence thesis by A11; end; let x be set; assume x in B; then ex a be set st a in X.s & x = (NH.s).root-tree [a,s] by A11; hence thesis by A10; end; end; definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, s be Element of S; cluster OSFreeGen(s,X) -> non empty; coherence proof set NH = OSNat_Hom(ParsedTermsOSA(X),LCongruence(X)); defpred P[set] means ex a be set st a in X.s & $1 = (NH.s).(root-tree [a,s]); consider x such that A1: x in X.s by XBOOLE_0:def 1; P[(NH.s).root-tree [x,s]] by A1; hence thesis by Def26; end; end; theorem Th31: for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, s be Element of S holds OSFreeGen(s,X) = { (OSNat_Hom(ParsedTermsOSA(X),LCongruence(X)).s).root-tree t where t is Symbol of DTConOSA(X): t in Terminals DTConOSA(X) & t`2 = s} proof let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, s be Element of S; set D = DTConOSA(X), NH = OSNat_Hom(ParsedTermsOSA(X),LCongruence(X)), A = {(NH.s).root-tree t where t is Symbol of D : t in Terminals D & t`2 = s}; thus OSFreeGen(s,X) c= A proof let x be set; assume x in OSFreeGen(s,X); then consider a be set such that A1: a in X.s & x = (NH.s).root-tree [a,s] by Def26; A2: [a,s] in Terminals D by A1,Th4; then reconsider t = [a,s] as Symbol of D; t`2 = s by MCART_1:7; hence thesis by A1,A2; end; let x be set; assume x in A; then consider t be Symbol of D such that A3: x = (NH.s).root-tree t & t in Terminals D & t`2 = s; consider s1 be Element of S, a be set such that A4: a in X.s1 & t = [a,s1] by A3,Th4; s = s1 by A3,A4,MCART_1:7; hence thesis by A3,A4,Def26; end; definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S; func OSFreeGen(X) -> OSGeneratorSet of FreeOSA(X) means :Def27: for s be Element of S holds it.s = OSFreeGen(s,X); existence proof set FM = FreeOSA(X), D = DTConOSA(X), PTA = ParsedTermsOSA(X), PTC = LCongruence(X), SO = the Sorts of FreeOSA(X), NH = OSNat_Hom(ParsedTermsOSA(X),LCongruence(X)); A1: PTA = MSAlgebra (# ParsedTerms(X), PTOper(X) #) by Def11; A2: FM = QuotOSAlg(PTA, PTC) by Def19; reconsider NH1 = NH as ManySortedFunction of PTA,FM by Def19; A3: NH1 is_epimorphism PTA, FM & NH1 is order-sorted by A2,OSALG_4:16; then A4: NH1 is_homomorphism PTA,FM & NH1 is "onto" by MSUALG_3:def 10; reconsider SOS = SO as OrderSortedSet of S by OSALG_1:17; deffunc F(Element of S) = OSFreeGen($1,X); consider f be Function such that A5: dom f = the carrier of S & for s be Element of S holds f.s = F(s) from LambdaB; reconsider f as ManySortedSet of the carrier of S by A5,PBOOLE:def 3; A6: f c= the Sorts of FM proof let x; assume x in the carrier of S; then reconsider s = x as SortSymbol of S; f.s = OSFreeGen(s,X) & OSFreeGen(s,X) c= SO.s by A5; hence thesis; end; then reconsider f as MSSubset of FM by MSUALG_2:def 1; OSCl f c= SOS by A6,OSALG_2:13; then OSCl f is ManySortedSubset of the Sorts of FM by MSUALG_2:def 1; then reconsider O = OSCl f as OSSubset of FM by OSALG_2:def 2; O is OSSubset of GenOSAlg(O) by OSALG_2:def 13; then A7: O c= the Sorts of GenOSAlg(O) by MSUALG_2:def 1; f c= O by OSALG_2:12; then A8: f c= the Sorts of GenOSAlg(O) by A7,PBOOLE:15; A9: the Sorts of GenOSAlg(O) = the Sorts of FM proof the Sorts of GenOSAlg(O) is MSSubset of FM by MSUALG_2:def 10; hence the Sorts of GenOSAlg(O) c= the Sorts of FM by MSUALG_2:def 1; reconsider O2 = (the Sorts of GenOSAlg(O)) as OrderSortedSet of S by OSALG_1:17; defpred P[set] means for s1 being Element of S st $1 in dom (NH1.s1) holds (NH1.s1).$1 in (the Sorts of GenOSAlg(O)).s1; A10: for s be Symbol of D st s in Terminals D holds P[root-tree s] proof let t be Symbol of D; assume A11: t in Terminals D; let s1 be Element of S; assume (root-tree t) in dom (NH1.s1); then root-tree t in (the Sorts of PTA).s1; then (root-tree t) in ParsedTerms(X,s1) by A1,Def8; then root-tree t in {a where a is Element of TS(DTConOSA(X)) : (ex s2 being Element of S, x be set st s2 <= s1 & x in X.s2 & a = root-tree [x,s2]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o <= s1} by Def7; then consider a being Element of TS(D) such that A12: root-tree t = a and A13: (ex s2 being Element of S, x be set st s2 <= s1 & x in X.s2 & a = root-tree [x,s2]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o <= s1; not ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o <= s1 proof given o be OperSymbol of S such that A14: [o,the carrier of S] = a.{} & the_result_sort_of o <= s1; A15: [o,the carrier of S] = t by A12,A14,TREES_4:3; consider s3 being Element of S, x3 being set such that A16: x3 in X.s3 & t = [x3,s3] by A11,Th4; o = x3 & the carrier of S = s3 by A15,A16,ZFMISC_1:33; then s3 in s3; hence contradiction; end; then consider s2 being Element of S, x be set such that A17: s2 <= s1 & x in X.s2 & a = root-tree [x,s2] by A13; reconsider s1_1 = s1, s2_1 = s2 as Element of S; A18: O2.s2_1 c= O2.s1_1 by A17,OSALG_1:def 18; A19: (NH1.s2).(root-tree [x,s2]) in OSFreeGen(s2,X) by A17,Def26; a in {a1 where a1 is Element of TS(DTConOSA(X)): (ex s3 being Element of S, x be set st s3 <= s2 & x in X.s3 & a1 = root-tree [x,s3]) or ex o be OperSymbol of S st [o,the carrier of S] = a1.{} & the_result_sort_of o <= s2} by A17; then a in ParsedTerms(X,s2) by Def7; then a in (ParsedTerms(X)).s2 by Def8; then (root-tree [x,s2]) in dom (NH1.s2) by A1,A17,FUNCT_2:def 1; then A20: (NH1.s2_1).(root-tree [x,s2]) = (NH1.s1_1).(root-tree [x,s2]) by A3,A17,OSALG_3:def 1; f.s2 c= (the Sorts of GenOSAlg(O)).s2 by A8,PBOOLE:def 5; then OSFreeGen(s2,X) c= (the Sorts of GenOSAlg(O)).s2 by A5; then OSFreeGen(s2,X) c= (the Sorts of GenOSAlg(O)).s1 by A18,XBOOLE_1:1 ; hence (NH1.s1).(root-tree t) in (the Sorts of GenOSAlg(O)).s1 by A12,A17,A19,A20; end; A21: for nt being Symbol of D, ts being FinSequence of TS(D) st nt ==> roots ts & for t being DecoratedTree of the carrier of D st t in rng ts holds P[t] holds P[nt-tree ts] proof let nt be Symbol of D, ts be FinSequence of TS(D); assume A22: nt ==> roots ts & for t being DecoratedTree of the carrier of D st t in rng ts holds P[t]; set G = GenOSAlg(O), OU = [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod (X qua ManySortedSet of S)); A23: [nt,roots ts] in the Rules of D by A22,LANG1:def 1; A24: D = DTConstrStr (# OU, OSREL(X)#) & Terminals D = Union (coprod X) by Def5,Th3; then A25: [nt,roots ts] in OSREL(X) by A22,LANG1:def 1; reconsider sy = nt as Element of OU by A24; reconsider rt = roots ts as Element of OU* by A23,A24,ZFMISC_1:106; [sy,rt] in OSREL(X) by A22,A24,LANG1:def 1; then sy in [:the OperSymbols of S,{the carrier of S}:] by Def4; then consider o being Element of the OperSymbols of S, x2 being Element of {the carrier of S} such that A26: sy = [o,x2] by DOMAIN_1:9; A27: x2 = the carrier of S by TARSKI:def 1; set ar = the_arity_of o, rs = the_result_sort_of o; let s1 be Element of S such that A28: (nt-tree ts) in dom (NH1.s1); (nt-tree ts) in (the Sorts of PTA).s1 by A28; then (nt-tree ts) in ParsedTerms(X,s1) by A1,Def8; then (nt-tree ts) in {a1 where a1 is Element of TS(DTConOSA(X)): (ex s2 being Element of S, x be set st s2 <= s1 & x in X.s2 & a1 = root-tree [x,s2]) or ex o be OperSymbol of S st [o,the carrier of S] = a1.{} & the_result_sort_of o <= s1} by Def7; then consider a1 being Element of TS D such that A29: (nt-tree ts) = a1 and A30: (ex s2 being Element of S, x be set st s2 <= s1 & x in X.s2 & a1 = root-tree [x,s2]) or ex o be OperSymbol of S st [o,the carrier of S] = a1.{} & the_result_sort_of o <= s1; not ex s2 being Element of S, x be set st s2 <= s1 & x in X.s2 & a1 = root-tree [x,s2] proof given s2 being Element of S, x be set such that A31: s2 <= s1 & x in X.s2 & a1 = root-tree [x,s2]; [x,s2] = (nt-tree ts).{} by A29,A31,TREES_4:3 .= [o,x2] by A26,TREES_4:def 4; then s2 = the carrier of S by A27,ZFMISC_1:33; then s2 in s2; hence contradiction; end; then consider o1 being OperSymbol of S such that A32: [o1,the carrier of S] = a1.{} & the_result_sort_of o1 <= s1 by A30; [o1,the carrier of S] = [o,x2] by A26,A29,A32,TREES_4:def 4; then A33: o1 = o by ZFMISC_1:33; reconsider B = the Sorts of G as MSSubset of FM by MSUALG_2:def 10; reconsider B1 = B as OrderSortedSet of S by OSALG_1:17; reconsider rs1 = rs,s1_1 = s1 as Element of S; A34: B1.rs1 c= B1.s1_1 by A32,A33,OSALG_1:def 18; set AR = the Arity of S, RS = the ResultSort of S, BH = B# * the Arity of S, Op = the OperSymbols of S; B is opers_closed by MSUALG_2:def 10; then B is_closed_on o by MSUALG_2:def 7; then A35: rng ((Den(o,FM))|(BH.o)) c= (B * RS).o by MSUALG_2:def 6; A36: OSSym(o,X) = [o,the carrier of S] & nt = [o,the carrier of S] by A26,Def6,TARSKI:def 1; A37: Den(o,PTA) = (PTOper X).o by A1,MSUALG_1:def 11 .= PTDenOp(o,X) by Def10; A38: dom (ParsedTerms X) = the carrier of S & o in Op & dom B = the carrier of S & dom RS = Op & rng RS c= the carrier of S & AR.o = ar & RS.o = rs by FUNCT_2:def 1,MSUALG_1:def 6,def 7,PBOOLE:def 3,RELSET_1:12; A39: ts in ((ParsedTerms X)# * (the Arity of S)).o by A22,A36,Th7; then A40: ts in Args(o,PTA) by A1,MSUALG_1:def 9; reconsider ts1 = ts as Element of Args(o,PTA) by A1,A39,MSUALG_1:def 9; A41: (NH1.rs).(Den(o,PTA).ts1) = Den(o,FM).(NH1#ts1) by A4,MSUALG_3:def 9; A42: (Den(o,PTA).ts) = nt-tree ts by A22,A36,A37,Def9; NH1#ts1 in Args(o,FM); then A43: NH1#ts1 in dom Den(o,FM) by FUNCT_2:def 1; A44: BH.o = product (B * ar) by A38,MSAFREE:1; rng ar c= the carrier of S by FINSEQ_1:def 4; then A45: dom (B * ar) = dom ar & dom ((the Sorts of PTA) * ar) = dom ar by A1,A38,RELAT_1:46; A46: dom (roots ts) = dom ts by DTCONSTR:def 1; A47: len rt = len ar & for x st x in dom rt holds (rt.x in [:the OperSymbols of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = rt.x holds the_result_sort_of o1 <= ar/.x) & (rt.x in Union (coprod X) implies ex i being Element of S st i <= ar/.x & rt.x in coprod(i,X)) by A25,A26,A27,Th2; A48: Seg len rt = dom rt & Seg len ar = dom ar by FINSEQ_1:def 3; A49: dom (NH1#ts1) = dom ar by MSUALG_3:6; for x st x in dom (B * ar) holds (NH1#ts1).x in (B * ar).x proof let x such that A50: x in dom (B * ar); reconsider x1 = x as Nat by A50; A51: rng ts c= TS D by FINSEQ_1:def 4; A52: ts.x1 in rng ts by A45,A46,A47,A48,A50,FUNCT_1:def 5; then reconsider t = ts.x as Element of TS(D) by A51; A53: (NH1#ts1).x1 = (NH1.(ar/.x1)).(ts1.x1) by A45,A46,A47,A48,A50, MSUALG_3:def 8; ts1.x in ((the Sorts of PTA) * ar).x by A45,A50,MSUALG_3:6; then ts1.x in (the Sorts of PTA).(ar.x) by A45,A50,FUNCT_1:22; then ts1.x in (the Sorts of PTA).(ar/.x) by A45,A50,FINSEQ_4:def 4; then ts1.x1 in dom (NH1.(ar/.x1)) by FUNCT_2:def 1; then (NH1.(ar/.x1)).t in (the Sorts of GenOSAlg(O)).(ar/.x1) by A22,A52; then (NH1.(ar/.x1)).(ts1.x1) in B.(ar.x) by A45,A50,FINSEQ_4:def 4; hence thesis by A50,A53,FUNCT_1:22; end; then (NH1#ts1) in BH.o by A44,A45,A49,CARD_3:18; then Den(o,FM).(NH1#ts1) in rng ((Den(o,FM))|(BH.o)) by A43,FUNCT_1:73; then Den(o,FM).(NH1#ts1) in (B * RS).o by A35; then A54: (NH1.rs).(nt-tree ts) in B.rs by A38,A41,A42,FUNCT_2:21; Den(o,PTA).ts in Result(o,PTA) by A40,FUNCT_2:7; then Den(o,PTA).ts in ((the Sorts of PTA) * RS).o by MSUALG_1:def 10; then Den(o,PTA).ts in (the Sorts of PTA).rs by A38,FUNCT_2:21; then (nt-tree ts) in dom (NH1.rs) by A42,FUNCT_2:def 1; then (NH1.s1_1).(nt-tree ts) = (NH1.rs1).(nt-tree ts) by A3,A32,A33,OSALG_3:def 1; hence (NH1.s1).(nt-tree ts) in (the Sorts of GenOSAlg(O)).s1 by A34,A54 ; end; A55: for t being DecoratedTree of the carrier of D st t in TS D holds P[t] from DTConstrInd(A10,A21); let x; assume A56: x in the carrier of S; then reconsider s = x as SortSymbol of S; (the Sorts of FM).s c= (the Sorts of GenOSAlg(O)).s proof let x1 be set; assume A57: x1 in (the Sorts of FM).s; rng(NH1.x) = (the Sorts of FM).x by A4,A56,MSUALG_3:def 3; then consider x2 being set such that A58: x2 in dom (NH1.s) & x1 = (NH1.s).x2 by A57,FUNCT_1:def 5; A59: x2 in (the Sorts of PTA).s by A58; (the Sorts of PTA).s = ParsedTerms(X,s) by A1,Def8 .= {a where a is Element of TS(D): (ex s2 being Element of S, x be set st s2 <= s & x in X.s2 & a = root-tree [x,s2]) or ex o1 be OperSymbol of S st [o1,the carrier of S] = a.{} & the_result_sort_of o1 <= s} by Def7; then consider a be Element of TS(D) such that A60: a = x2 and (ex s2 being Element of S, x be set st s2 <= s & x in X.s2 & a = root-tree [x,s2]) or ex o1 be OperSymbol of S st [o1,the carrier of S]=a.{} & the_result_sort_of o1 <= s by A59; thus thesis by A55,A58,A60; end; hence thesis; end; f is OSGeneratorSet of FM proof let O1 be OSSubset of FM such that A61: O1 = OSCl f; thus thesis by A9,A61; end; then reconsider f as OSGeneratorSet of FM; take f; thus thesis by A5; end; uniqueness proof let A,B be OSGeneratorSet of FreeOSA(X); assume that A62: for s be Element of S holds A.s = OSFreeGen(s,X) and A63: for s be Element of S holds B.s = OSFreeGen(s,X); for i be set st i in the carrier of S holds A.i = B.i proof let i be set; assume i in the carrier of S; then reconsider s = i as SortSymbol of S; A.s = OSFreeGen(s,X) & B.s = OSFreeGen(s,X) by A62,A63; hence thesis; end; hence thesis by PBOOLE:3; end; end; theorem Th32: for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S holds OSFreeGen(X) is non-empty proof let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S; let x; assume x in the carrier of S; then reconsider s = x as Element of S; (OSFreeGen(X)).s = OSFreeGen(s,X) by Def27; hence thesis; end; definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S; cluster OSFreeGen(X) -> non-empty; coherence by Th32; end; definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, R be OSCongruence of ParsedTermsOSA(X), t be Element of TS DTConOSA(X); func OSClass(R,t) -> Element of OSClass(R,LeastSort t) means :Def28: for s being Element of S, x being Element of (the Sorts of ParsedTermsOSA(X)).s st t = x holds it = OSClass(R,x); existence proof set LS = LeastSort t, PTA = ParsedTermsOSA(X); reconsider x1 = t as Element of (the Sorts of PTA).LS by Def12; take OSClass(R,x1); let s being Element of S, x being Element of (the Sorts of ParsedTermsOSA(X)).s such that A1: t = x; LS <= s by A1,Def12; hence OSClass(R,x1) = OSClass(R,x) by A1,OSALG_4:14; end; uniqueness proof set LS = LeastSort t, PTA = ParsedTermsOSA(X); reconsider x1 = t as Element of (the Sorts of PTA).LS by Def12; let O1,O2 be Element of OSClass(R,LeastSort t) such that A2: for s being Element of S, x being Element of (the Sorts of ParsedTermsOSA(X)).s st t = x holds O1 = OSClass(R,x) and A3: for s being Element of S, x being Element of (the Sorts of ParsedTermsOSA(X)).s st t = x holds O2 = OSClass(R,x); thus O1 = OSClass(R,x1) by A2 .= O2 by A3; end; end; theorem Th33: for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, R be OSCongruence of ParsedTermsOSA(X), t be Element of TS DTConOSA(X) holds t in OSClass(R,t) proof let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, R be OSCongruence of ParsedTermsOSA(X), t be Element of TS DTConOSA(X); set PTA = ParsedTermsOSA(X); reconsider x = t as Element of (the Sorts of PTA).(LeastSort t) by Def12; A1: OSClass(R,t) = OSClass(R,x) by Def28 .= Class( CompClass(R, CComp(LeastSort t)), x) by OSALG_4:def 14; x in (the Sorts of PTA)-carrier_of CComp(LeastSort t) by OSALG_4:6; hence thesis by A1,EQREL_1:28; end; theorem Th34: for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, s be Element of S, t being Element of TS DTConOSA(X), x,x1 being set st x in X.s & t = root-tree [x,s] holds x1 in OSClass(PTCongruence(X),t) iff x1 = t proof let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, s be Element of S, t being Element of TS DTConOSA(X); set PTA = ParsedTermsOSA(X), D = DTConOSA(X),R= PTCongruence(X); reconsider y = t as Element of (the Sorts of PTA).(LeastSort t) by Def12; A1: OSClass(R,t) = OSClass(PTCongruence X,y) by Def28 .= proj1((PTClasses X).y) by Th26; let x,x1 being set such that A2: x in X.s & t = root-tree [x,s]; A3: [x,s] in Terminals D by A2,Th4; then reconsider sy = [x,s] as Symbol of D; A4: (PTClasses X).(root-tree sy) = @(sy) by A3,Def22 .= {[root-tree sy,s1] where s1 is Element of S: ex s2 be Element of S, x2 be set st x2 in X.s2 & sy = [x2,s2] & s2 <= s1} by Def20; hereby assume x1 in OSClass(R,t); then consider z being set such that A5: [x1,z] in (PTClasses X).y by A1,FUNCT_5:def 1; consider s1 being Element of S such that A6: [x1,z] = [root-tree sy,s1] and ex s2 be Element of S, x2 be set st x2 in X.s2 & sy = [x2,s2] & s2 <= s1 by A2,A4,A5; thus x1 = t by A2,A6,ZFMISC_1:33; end; assume x1 = t; then [x1,s] in (PTClasses X).y by A2,A4; hence x1 in OSClass(R,t) by A1,FUNCT_5:def 1; end; theorem Th35: for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, R be OSCongruence of ParsedTermsOSA(X), t1,t2 be Element of TS DTConOSA(X) holds t2 in OSClass(R,t1) iff OSClass(R,t1) = OSClass(R,t2) proof let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, R be OSCongruence of ParsedTermsOSA(X), t1,t2 be Element of TS DTConOSA(X); set PTA = ParsedTermsOSA(X), SPTA = (the Sorts of PTA); reconsider x1=t1 as Element of SPTA.(LeastSort t1) by Def12; A1: OSClass(R,t1) = OSClass(R,x1) by Def28 .= Class( CompClass(R, CComp(LeastSort t1)), x1) by OSALG_4:def 14; set CC1 = CComp(LeastSort t1), CR1 = CompClass(R,CC1); hereby assume t2 in OSClass(R,t1); then [t2,x1] in CR1 by A1,EQREL_1:27; then consider s2 being Element of S such that A2: s2 in CC1 & [t2,x1] in R.s2 by OSALG_4:def 11; reconsider x11=x1,x22=t2 as Element of SPTA.s2 by A2,ZFMISC_1:106; thus OSClass(R,t1) = OSClass(R,x11) by Def28 .= OSClass(R,x22) by A2,OSALG_4:13 .= OSClass(R,t2) by Def28; end; assume OSClass(R,t1) = OSClass(R,t2); hence t2 in OSClass(R,t1) by Th33; end; theorem Th36: for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, R1,R2 be OSCongruence of ParsedTermsOSA(X), t be Element of TS DTConOSA(X) holds R1 c= R2 implies OSClass(R1,t) c= OSClass(R2,t) proof let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, R1,R2 be OSCongruence of ParsedTermsOSA(X), t be Element of TS DTConOSA(X); assume A1: R1 c= R2; set s = LeastSort t, PTA = ParsedTermsOSA(X), SPTA = the Sorts of PTA, D = DTConOSA(X); let x be set such that A2: x in OSClass(R1,t); reconsider xa=t as Element of SPTA.s by Def12; A3: OSClass(R1,t) = OSClass(R1,xa) by Def28 .= Class( CompClass(R1, CComp(s)), xa) by OSALG_4:def 14; set CC1 = CComp(s), CR1 = CompClass(R1,CC1); [x,xa] in CR1 by A2,A3,EQREL_1:27; then consider s1 being Element of S such that A4: s1 in CC1 & [x,xa] in R1.s1 by OSALG_4:def 11; A5: x in SPTA.s1 & xa in SPTA.s1 by A4,ZFMISC_1:106; reconsider xa = t, xb = x as Element of SPTA.s1 by A4,ZFMISC_1:106; reconsider t1 = x as Element of TS D by A5,Th16; A6: R1.s1 c= R2.s1 by A1,PBOOLE:def 5; OSClass(R2,t1) = OSClass(R2,xb) by Def28 .= OSClass(R2,xa) by A4,A6,OSALG_4:13 .= OSClass(R2,t) by Def28; hence thesis by Th35; end; theorem Th37: for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, s be Element of S, t being Element of TS DTConOSA(X), x,x1 being set st x in X.s & t = root-tree [x,s] holds x1 in OSClass(LCongruence(X),t) iff x1 = t proof let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, s be Element of S, t being Element of TS DTConOSA(X); set R = LCongruence(X),R1 = PTCongruence(X); R c= R1 by Def18; then A1: OSClass(R,t) c= OSClass(R1,t) by Th36; let x,x1 being set such that A2: x in X.s & t = root-tree [x,s]; thus x1 in OSClass(R,t) implies x1 = t by A1,A2,Th34; assume x1 = t; hence thesis by Th33; end; definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, A be non-empty ManySortedSet of the carrier of S, F be ManySortedFunction of PTVars(X), A, t be Symbol of DTConOSA(X); assume A1: t in Terminals (DTConOSA(X)); func pi(F,A,t) -> Element of Union A means :Def29: for f be Function st f = F.(t`2) holds it = f.(root-tree t); existence proof set FG = PTVars(X), D = DTConOSA(X); consider s be Element of S, x be set such that A2: x in X.s & t = [x,s] by A1,Th4; FG.s = PTVars(s,X) by Def25; then A3: dom (F.s) = PTVars(s,X) by FUNCT_2:def 1 .= {root-tree tt where tt is Symbol of D: tt in Terminals D & tt`2 = s} by Th29; t`2 = s by A2,MCART_1:7; then root-tree t in dom (F.s) by A1,A3; then A4: (F.s).(root-tree t) in rng (F.s) by FUNCT_1:def 5; A5: rng (F.s) c= A.s by RELSET_1:12; dom A = the carrier of S by PBOOLE:def 3; then A.s in rng A by FUNCT_1:def 5; then (F.s).(root-tree t) in union rng A by A4,A5,TARSKI:def 4; then reconsider eu = (F.s).(root-tree t) as Element of Union A by PROB_1:def 3; take eu; let f be Function; assume f = F.(t`2); hence thesis by A2,MCART_1:7; end; uniqueness proof let a,b be Element of Union A; assume that A6: for f be Function st f = F.(t`2) holds a = f.(root-tree t) and A7: for f be Function st f = F.(t`2) holds b = f.(root-tree t); consider s be Element of S, x be set such that A8: x in X.s & t = [x,s] by A1,Th4; reconsider f = F.s as Function; f = F.(t`2) by A8,MCART_1:7; then a = f.(root-tree t) & b = f.(root-tree t) by A6,A7; hence thesis; end; end; theorem Th38: for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, U1 be monotone non-empty OSAlgebra of S, f be ManySortedFunction of PTVars(X),the Sorts of U1 ex h be ManySortedFunction of ParsedTermsOSA(X),U1 st h is_homomorphism ParsedTermsOSA(X),U1 & h is order-sorted & h || PTVars(X) = f proof let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S; set D = DTConOSA(X), PTA = ParsedTermsOSA(X), PV = PTVars(X), SPTA = the Sorts of PTA; let U1 be non-empty monotone OSAlgebra of S, F be ManySortedFunction of PV,the Sorts of U1; set SA =the Sorts of PTA, AR = the Arity of S, S1 = the Sorts of U1, O = the OperSymbols of S, RS = the ResultSort of S; A1: PTA = MSAlgebra (# ParsedTerms(X), PTOper(X) #) by Def11; reconsider SAO=SA,S1O=S1 as OrderSortedSet of S by OSALG_1:17; deffunc TermVal(Symbol of D) = pi(F,the Sorts of U1,$1); deffunc NTermVal(Symbol of D,FinSequence of TS(D), FinSequence of D) = pi(@(X,$1),U1,$3); consider G being Function of TS(D), Union (the Sorts of U1) such that A2: for t being Symbol of D st t in Terminals D holds G.(root-tree t) = TermVal(t) and A3: for nt be Symbol of D, ts be FinSequence of TS(D) st nt ==> roots ts holds G.(nt-tree ts) = NTermVal(nt,roots ts,G * ts) from DTConstrIndDef; deffunc F(set) = G | ((the Sorts of PTA).$1); consider h be Function such that A4: dom h = the carrier of S & for s be set st s in the carrier of S holds h.s = F(s) from Lambda; reconsider h as ManySortedSet of the carrier of S by A4,PBOOLE:def 3; for s be set st s in dom h holds h.s is Function proof let s be set; assume s in dom h; then h.s = G | ((the Sorts of PTA).s) by A4; hence thesis; end; then reconsider h as ManySortedFunction of the carrier of S by PRALG_1:def 15; defpred P[set] means for s be Element of S st $1 in (the Sorts of PTA).s holds (h.s).$1 in (the Sorts of U1).s; A5: for t being Symbol of D st t in Terminals D holds P[root-tree t] proof let t be Symbol of D; assume A6: t in Terminals D; then consider s be Element of S, x be set such that A7: x in X.s & t = [x,s] by Th4; reconsider s as SortSymbol of S; set E = {root-tree tt where tt is Symbol of D: tt in Terminals D & tt`2 = s}, a = root-tree t; A8: t`2 = s by A7,MCART_1:7; then A9: a in E by A6; A10: E = PTVars(s,X) & PTVars(s,X) c= (ParsedTerms X).s by A1,Th29; reconsider f = F.s as Function of PV.s,S1.s; A11: PV.s = E by A10,Def25; A12: dom f = PV.s & rng f c= S1.s by FUNCT_2:def 1,RELSET_1:12; then f.a in rng f by A9,A11,FUNCT_1:def 5; then A13: f.a in S1.s by A12; A14: h.s = G | (SA.s) by A4; then A15: (h.s).a = G.a by A9,A10,FUNCT_1:72 .= pi(F,S1,t) by A2,A6 .= f.a by A6,A8,Def29; let s1 be Element of S; reconsider s0=s,s11=s1 as Element of S; assume A16: a in SA.s1; then s <= s1 by A7,Th10; then A17: S1O.s0 c= S1O.s11 by OSALG_1:def 18; h.s1 = G | (SA.s1) by A4; then (h.s1).a = G.a by A16,FUNCT_1:72 .= f.a by A9,A10,A14,A15,FUNCT_1:72; hence thesis by A13,A17; end; A18: for nt being Symbol of D, ts being FinSequence of TS(D) st nt ==> roots ts & for t being DecoratedTree of the carrier of D st t in rng ts holds P[t] holds P[nt-tree ts] proof let nt be Symbol of D, ts be FinSequence of TS(D); assume A19: nt ==> roots ts & for t being DecoratedTree of the carrier of D st t in rng ts holds P[t]; set p = G * ts, o = @(X,nt), ar = the_arity_of o, rs = the_result_sort_of o, OU = [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod (X qua ManySortedSet of S)), rt = roots ts; A20: o in O & ar = AR.o by MSUALG_1:def 6; A21: Args(o,U1) = (S1# * AR).o by MSUALG_1:def 9 .= product (S1 * ar) by A20,MSAFREE:1; A22: dom p = dom ts & len p = len ts & for n be Nat st n in dom p holds p.n = G.(ts.n) by ALG_1:1; A23: dom rt = dom ts by DTCONSTR:def 1; A24: [o,the carrier of S] = nt by A19,Def16; A25: [o,the carrier of S] = OSSym(o,X) by Def6; A26: rng ar c= the carrier of S & dom S1 = the carrier of S & dom SA = the carrier of S by FINSEQ_1:def 4,PBOOLE:def 3; A27: dom(S1* ar) = dom ar & dom(SA* ar) = dom ar by PBOOLE:def 3; A28: [[o,the carrier of S],rt] in the Rules of D by A19,A24,LANG1:def 1; A29: D = DTConstrStr (# OU, OSREL(X) #) by Def5; then reconsider rt as Element of OU* by A28,ZFMISC_1:106; A30: len rt = len ar by A28,A29,Th2; A31: dom rt = Seg len rt & Seg len ar = dom ar by FINSEQ_1:def 3; then A32: dom p = dom (S1 * ar) by A22,A23,A27,A28,A29,Th2; for x st x in dom (S1 * ar) holds p.x in (S1 * ar).x proof let x; assume A33: x in dom (S1 * ar); then reconsider n = x as Nat; A34: p.n = G.(ts.n) by A32,A33,ALG_1:1; A35: rng ts c= TS D by FINSEQ_1:def 4; A36: ts.n in rng ts by A23,A27,A30,A31,A33,FUNCT_1:def 5; then reconsider t = ts.n as Element of TS(D) by A35; ts in ((ParsedTerms X)# * AR).o by A19,A24,A25,Th7; then ts in product ((ParsedTerms X) * ar) by A20,MSAFREE:1; then ts.x in ((ParsedTerms X) * ar).x by A1,A27,A33,CARD_3:18; then A37: ts.x in (ParsedTerms X).(ar.x) by A1,A27,A33,FUNCT_1:22; ar.x in rng ar by A27,A33,FUNCT_1:def 5; then reconsider s = ar.x as Element of S by A26; A38: (h.s).t in S1.s by A1,A19,A36,A37; A39: h.s = G | (SA.s) by A4; A40: dom G = TS D by FUNCT_2:def 1 .= union rng SA by A1,Th8; dom SA = the carrier of S by PBOOLE:def 3; then SA.s in rng SA by FUNCT_1:def 5; then SA.s c= dom G by A40,ZFMISC_1:92; then dom (h.s) = SA.s by A39,RELAT_1:91; then G.t in S1.s by A1,A37,A38,A39,FUNCT_1:70; hence thesis by A33,A34,FUNCT_1:22; end; then A41: p in Args(o,U1) by A21,A22,A23,A27,A30,A31,CARD_3:18; then A42: pi(o,U1,p) = Den(o,U1).p by MSAFREE:def 23; set ppi = pi(o,U1,p); A43: dom Den(o,U1) = Args(o,U1) & rng Den(o,U1) c= Result(o,U1) by FUNCT_2:def 1,RELSET_1:12; then ppi in rng Den(o,U1) by A41,A42,FUNCT_1:def 5; then A44: ppi in Result(o,U1) by A43; dom S1 = the carrier of S & rng RS c= the carrier of S & dom SA = the carrier of S by PBOOLE:def 3,RELSET_1:12; then A45: dom (S1 *RS) = dom RS & dom RS = O & dom (SA * RS) = dom RS by FUNCT_2:def 1,RELAT_1:46; A46: Result(o,U1) = (S1 *RS).o by MSUALG_1:def 10 .= S1.(RS.o) by A45,FUNCT_1:22 .= S1.rs by MSUALG_1:def 7; A47: G.(nt-tree ts) = ppi by A3,A19; A48: (PTDenOp(o,X)).ts = nt-tree ts by A19,A24,A25,Def9; A49: dom (PTDenOp (o,X)) = ((ParsedTerms X)# * AR).o & rng (PTDenOp (o,X)) c= ((ParsedTerms X) * RS).o by FUNCT_2:def 1,RELSET_1:12; then ts in dom (PTDenOp(o,X)) by A19,A24,A25,Th7; then nt-tree ts in rng (PTDenOp(o,X)) by A48,FUNCT_1:def 5; then nt-tree ts in (SA * RS).o by A1,A49; then nt-tree ts in SA.(RS.o) by A45,FUNCT_1:22; then A50: nt-tree ts in SA.rs by MSUALG_1:def 7; then A51: ppi = (G | (SA.rs)).(nt-tree ts) by A47,FUNCT_1:72; let s be Element of S; reconsider s2=s as Element of S; A52: h.rs = (G | (SA.rs)) & h.s = (G | (SA.s)) by A4; assume A53: nt-tree ts in SA.s; consider op being OperSymbol of S such that A54: nt = [op,the carrier of S] & ts in Args(op,PTA) & nt-tree ts = Den(op,PTA).ts & for s1 being Element of S holds nt-tree ts in SA.s1 iff the_result_sort_of op <= s1 by A19,Th12; op = o by A19,A54,Def16; then rs <= s by A53,A54; then S1O.rs c= S1O.s2 by OSALG_1:def 18; then A55: (h.rs).(nt-tree ts) in S1.s by A44,A46,A51,A52; (h.s).(nt-tree ts) = G.(nt-tree ts) by A52,A53,FUNCT_1:72; hence thesis by A50,A52,A55,FUNCT_1:72; end; A56: for t being DecoratedTree of the carrier of D st t in TS(D) holds P[t] from DTConstrInd(A5,A18); for s be set st s in the carrier of S holds h.s is Function of (the Sorts of PTA).s, (the Sorts of U1).s proof let x be set; assume x in the carrier of S; then reconsider s = x as Element of S; A57: h.s = G | (SA.s) by A4; A58: dom G = TS D by FUNCT_2:def 1 .= union rng SA by A1,Th8; dom SA = the carrier of S by PBOOLE:def 3; then SA.s in rng SA by FUNCT_1:def 5; then A59: SA.s c= dom G by A58,ZFMISC_1:92; then A60: dom (h.s) = SA.s by A57,RELAT_1:91; rng (h.s) c= S1.s proof let a be set; assume a in rng (h.s); then consider T be set such that A61: T in dom (h.s) & (h.s).T = a by FUNCT_1:def 5; reconsider T as Element of TS(D) by A59,A60,A61,FUNCT_2:def 1; T in SA.s by A57,A59,A61,RELAT_1:91; hence thesis by A56,A61; end; hence thesis by A60,FUNCT_2:def 1,RELSET_1:11; end; then reconsider h as ManySortedFunction of PTA,U1 by MSUALG_1:def 2; take h; thus h is_homomorphism PTA,U1 proof let op be Element of the OperSymbols of S such that Args(op,PTA) <> {}; reconsider o=op as OperSymbol of S; let x be Element of Args(op,PTA); set rs = the_result_sort_of o, DA = Den(o,PTA), D1 = Den(o,U1), OU = [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod (X qua ManySortedSet of S)), ar = the_arity_of o; A62: DA = (PTOper(X)).o by A1,MSUALG_1:def 11 .= PTDenOp(o,X) by Def10; A63: Args(o,PTA) = ((ParsedTerms X)# * AR).o by A1,MSUALG_1:def 9; then A64: x in ((ParsedTerms X)# * AR).o; reconsider p = x as FinSequence of TS(D) by A63,Th5; A65: OSSym(o,X) ==> roots p by A63,Th7; then A66: DA.x = (OSSym(o,X))-tree p by A62,Def9; A67: o in O & ar = AR.o & dom AR = O by FUNCT_2:def 1,MSUALG_1:def 6; A68: OSSym(o,X) = [o,the carrier of S] & [@(X,OSSym(o,X)),the carrier of S] = OSSym(o,X) by A65,Def6,Def16; then A69: @(X,OSSym(o,X)) = o by ZFMISC_1:33; rng RS c= the carrier of S & dom SA = the carrier of S by PBOOLE:def 3,RELSET_1:12; then A70: dom RS = O & dom (SA * RS) = dom RS by FUNCT_2:def 1,RELAT_1:46; A71: (PTDenOp(o,X)).p = (OSSym(o,X))-tree p by A65,Def9; A72: dom (PTDenOp (o,X)) = ((ParsedTerms X)# * AR).o & rng (PTDenOp (o,X)) c= ((ParsedTerms X) * RS).o by FUNCT_2:def 1,RELSET_1:12; then (OSSym(o,X))-tree p in rng (PTDenOp(o,X)) by A63,A71,FUNCT_1:def 5; then (OSSym(o,X))-tree p in (SA * RS).o by A1,A72; then (OSSym(o,X))-tree p in SA.(RS.o) by A70,FUNCT_1:22; then A73: (OSSym(o,X))-tree p in SA.rs by MSUALG_1:def 7; A74: h.rs = G | (SA.rs) by A4; A75: dom G = TS D by FUNCT_2:def 1 .= union rng SA by A1,Th8; A76: dom (G *p) = dom p & len (G*p) = len p & for n be Nat st n in dom(G*p) holds (G*p).n = G.(p.n) by ALG_1:1; A77: dom (h#x) = dom ar & dom x = dom ar by MSUALG_3:6; for a be set st a in dom p holds (G*p).a = (h#x).a proof let a be set; assume A78: a in dom p; then reconsider n = a as Nat; A79: (G*p).n = G.(x.n) by A76,A78; A80: (h#x).n = (h.(ar/.n)).(x.n) by A78,MSUALG_3:def 8; A81: h.(ar/.n) = G | (SA.(ar/.n)) by A4; A82: p in product((ParsedTerms X) * ar) by A64,A67,MSAFREE:1; A83: dom(S1* ar) = dom ar & dom(SA* ar) = dom ar by PBOOLE:def 3; set rt = roots p; A84: dom rt = dom p by DTCONSTR:def 1; A85: [[o,the carrier of S],rt] in the Rules of D by A65,A68,LANG1:def 1; A86: D = DTConstrStr (# OU, OSREL(X) #) by Def5; then reconsider rt as Element of OU* by A85,ZFMISC_1:106; A87: len rt = len ar by A85,A86,Th2; A88: Seg len rt = dom rt & Seg len ar = dom ar by FINSEQ_1:def 3; then A89: p.n in ((ParsedTerms X) * ar).n by A1,A78,A82,A83,A84,A87,CARD_3 :18; ((ParsedTerms X) * ar).n = SA.(ar.n) by A1,A78,A83,A84,A87,A88,FUNCT_1: 22 .= SA.(ar/.n) by A78,A84,A87,A88,FINSEQ_4:def 4; hence thesis by A79,A80,A81,A89,FUNCT_1:72; end; then A90: G*p = h#x by A76,A77,FUNCT_1:9; dom SA = the carrier of S by PBOOLE:def 3; then SA.rs in rng SA by FUNCT_1:def 5; then SA.rs c= dom G by A75,ZFMISC_1:92; then dom (h.rs) = SA.rs by A74,RELAT_1:91; then (h.rs).(DA.x) = G.((OSSym(o,X))-tree p) by A66,A73,A74,FUNCT_1:70 .= pi(@(X,OSSym(o,X)),U1,G*p) by A3,A65 .= D1.(h#x) by A69,A90,MSAFREE:def 23; hence thesis; end; thus h is order-sorted proof let s1,s2 being Element of S such that A91: s1 <= s2; A92: SAO.s1 c= SAO.s2 by A91,OSALG_1:def 18; let a1 being set such that A93: a1 in dom (h.s1); A94: a1 in SAO.s1 by A93; then a1 in SA.s2 by A92; hence a1 in dom (h.s2) by FUNCT_2:def 1; A95: h.s1 = G | (SPTA.s1) & h.s2 = G | (SPTA.s2) by A4; hence (h.s1).a1 = G.a1 by A93,FUNCT_1:72 .= (h.s2).a1 by A92,A94,A95,FUNCT_1:72; end; for x st x in the carrier of S holds (h || PV).x = F.x proof let x; assume x in the carrier of S; then reconsider s = x as Element of S; set hf = h || PV; A96: hf.s = (h.s) | (PV.s) by MSAFREE:def 1; A97: dom (h.s) = SA.s by FUNCT_2:def 1; A98: PV.s = PTVars(s,X) by Def25; A99: dom (hf.s) = PV.s by FUNCT_2:def 1; A100: dom (F.s) = PV.s by FUNCT_2:def 1; for a be set st a in PV.s holds (hf.s).a = (F.s).a proof let a be set; assume A101: a in PV.s; then a in {root-tree t where t is Symbol of D: t in Terminals D & t`2 = s } by A98,Th29; then consider t be Symbol of D such that A102: a = root-tree t & t in Terminals D & t`2 = s; A103: h.s = G | (SA.s) by A4; thus (hf.s).a = (h.s).a by A96,A99,A101,FUNCT_1:70 .= G.a by A97,A98,A101,A103,FUNCT_1:70 .= pi(F,S1,t) by A2,A102 .= (F.s).a by A102,Def29; end; hence thesis by A99,A100,FUNCT_1:9; end; hence h || PV = F by PBOOLE:3; end; :: NH stanbds for NatHom definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, s be Element of S; func NHReverse(s,X) -> Function of OSFreeGen(s,X),PTVars(s,X) means for t be Symbol of DTConOSA(X) st (OSNat_Hom(ParsedTermsOSA(X),LCongruence(X)).s).(root-tree t) in OSFreeGen(s,X) holds it.((OSNat_Hom(ParsedTermsOSA(X),LCongruence(X)).s).(root-tree t)) = root-tree t; existence proof set NH = OSNat_Hom(ParsedTermsOSA(X),LCongruence(X)); set A = OSFreeGen(s,X), R = LCongruence(X), PTA = ParsedTermsOSA(X), SPTA = the Sorts of PTA, NHs = OSNat_Hom(PTA,R,s), D = DTConOSA(X); A1: NH.s = OSNat_Hom(PTA,R,s) by OSALG_4:def 24; defpred P[set,set] means for t be Symbol of D st $1 = (NH.s).(root-tree t) holds $2 = root-tree t; A2: for x be set st x in A ex a be set st a in PTVars(s,X) & P[x,a] proof let x be set; assume x in A; then x in {(NH.s).(root-tree t) where t is Symbol of D: t in Terminals D & t`2 = s} by Th31; then consider t be Symbol of D such that A3: x = (NH.s).(root-tree t) & t in Terminals D & t`2 = s; consider s1 be Element of S, a be set such that A4: a in X.s1 & t = [a,s1] by A3,Th4; A5: s = s1 by A3,A4,MCART_1:7; take root-tree t; thus root-tree t in PTVars(s,X) by A4,A5,Def24; reconsider rt = root-tree t as Element of SPTA.s by A4,A5,Th10; reconsider tt = root-tree t as Element of TS D by A4,Th10; A6: OSClass(R,tt) = OSClass(R,rt) by Def28; A7: OSClass(R,tt) <> {} by Th33; A8: x = NHs.(root-tree t) by A3,OSALG_4:def 24; A9: NHs.rt = OSClass(R,rt) by OSALG_4:def 23; A10: x <> {} by A6,A7,A8,OSALG_4:def 23; let t1 be Symbol of D; assume A11: x = (NH.s).(root-tree t1); then A12: x = NHs.(root-tree t1) by OSALG_4:def 24; root-tree t1 in dom NHs by A1,A10,A11,FUNCT_1:def 4; then reconsider rt1 = root-tree t1 as Element of SPTA.s; reconsider tt2 = rt1 as Element of TS D by Th16; A13: OSClass(R,rt1) = OSClass(R,rt) by A8,A9,A12,OSALG_4:def 23; OSClass(R,tt2) = OSClass(R,rt1) by Def28; then tt2 in OSClass(R,tt) by A6,A13,Th35; hence thesis by A4,Th37; end; consider f be Function such that A14: dom f = A & rng f c= PTVars(s,X) & for x be set st x in A holds P[x,f.x] from NonUniqBoundFuncEx(A2); reconsider f as Function of A,PTVars(s,X) by A14,FUNCT_2:4; take f; let t be Symbol of D; assume (NH.s).(root-tree t) in A; hence thesis by A14; end; uniqueness proof set NH = OSNat_Hom(ParsedTermsOSA(X),LCongruence(X)); let A,B be Function of OSFreeGen(s,X),PTVars(s,X); assume that A15: for t be Symbol of DTConOSA(X) st (NH.s).(root-tree t) in OSFreeGen(s,X) holds A.((NH.s).(root-tree t)) = root-tree t and A16: for t be Symbol of DTConOSA(X) st (NH.s).(root-tree t) in OSFreeGen(s,X) holds B.((NH.s).(root-tree t)) = root-tree t; set D = DTConOSA(X), C = {(NH.s).(root-tree t) where t is Symbol of D : t in Terminals D & t`2 = s}; A17: OSFreeGen(s,X) = C by Th31; then A18: dom A = C & dom B = C by FUNCT_2:def 1; for i be set st i in C holds A.i = B.i proof let i be set; assume A19: i in C; then consider t be Symbol of D such that A20: i = (NH.s).(root-tree t) & t in Terminals D & t`2 = s; A.((NH.s).(root-tree t)) = root-tree t & B.((NH.s).(root-tree t)) = root-tree t by A15,A16,A17,A19,A20; hence thesis by A20; end; hence thesis by A18,FUNCT_1:9; end; end; definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S; func NHReverse(X) -> ManySortedFunction of OSFreeGen(X),PTVars(X) means for s be Element of S holds it.s = NHReverse(s,X); existence proof set I = the carrier of S, FG = OSFreeGen(X); defpred P[set,set] means for s be Element of S st s = $1 holds $2 = NHReverse(s,X); A1: for i be set st i in I ex u be set st P[i,u] proof let i be set; assume i in I; then reconsider s = i as SortSymbol of S; take NHReverse(s,X); let s1 be Element of S; assume s1 = i; hence thesis; end; consider H be Function such that A2: dom H = I & for i be set st i in I holds P[i,H.i] from NonUniqFuncEx(A1); reconsider H as ManySortedSet of I by A2,PBOOLE:def 3; for x be set st x in dom H holds H.x is Function proof let i be set; assume i in dom H; then reconsider s = i as SortSymbol of S by A2; H.s = NHReverse(s,X) by A2; hence thesis; end; then reconsider H as ManySortedFunction of I by PRALG_1:def 15; for i be set st i in I holds H.i is Function of FG.i,(PTVars(X)).i proof let i be set; assume i in I; then reconsider s = i as SortSymbol of S; A3: (OSFreeGen X).s = OSFreeGen(s,X) & (PTVars X).s = PTVars(s,X) by Def25,Def27; H.i = NHReverse(s,X) by A2; hence thesis by A3; end; then reconsider H as ManySortedFunction of FG,PTVars(X) by MSUALG_1:def 2; take H; let s be Element of S; thus thesis by A2; end; uniqueness proof let A,B be ManySortedFunction of OSFreeGen(X),PTVars(X);assume that A4: for s be Element of S holds A.s = NHReverse(s,X) and A5: for s be Element of S holds B.s =NHReverse(s,X); for i be set st i in the carrier of S holds A.i = B.i proof let i be set; assume i in the carrier of S; then reconsider s = i as SortSymbol of S; A.s = NHReverse(s,X) & B.s = NHReverse(s,X) by A4,A5; hence thesis; end; hence thesis by PBOOLE:3; end; end; theorem Th39: for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S holds OSFreeGen(X) is osfree proof let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S; set FA = FreeOSA(X), PTA = ParsedTermsOSA(X), SPTA = the Sorts of PTA, FG = OSFreeGen(X); let U1 be non-empty monotone OSAlgebra of S, F be ManySortedFunction of FG,the Sorts of U1; set SA =the Sorts of FA, S1 = the Sorts of U1, R = LCongruence(X), NH = OSNat_Hom(PTA,R); A1: FA = QuotOSAlg(ParsedTermsOSA(X),LCongruence(X)) by Def19; reconsider NH1= NH as ManySortedFunction of PTA, FA by Def19; set NHP = (NH1 || PTVars(X)); A2: now let s be Element of S; A3: (PTVars(X)).s = PTVars(s,X) by Def25; A4: NHP.s = (NH1.s) | ((PTVars(X)).s) by MSAFREE:def 1; hence NHP.s = (NH1.s) | (PTVars(s,X)) by Def25; thus PTVars(s,X) c= SPTA.s; thus dom (NH1.s) = SPTA.s & rng (NH1.s) c= SA.s by FUNCT_2:def 1,RELSET_1:12; thus A5: dom (NHP.s) = PTVars(s,X) by A3,FUNCT_2:def 1; for y being set holds ( y in FG.s iff ex x being set st x in dom (NHP.s) & y = (NHP.s).x) proof let y be set; thus y in FG.s implies ex x being set st x in dom (NHP.s) & y = (NHP.s).x proof assume y in FG.s; then y in OSFreeGen(s,X) by Def27; then consider a be set such that A6: a in X.s & y = (NH.s).(root-tree [a,s]) by Def26; take x = root-tree [a,s]; root-tree [a,s] in dom (NHP.s) by A5,A6,Def24; hence x in dom (NHP.s) & y = (NHP.s).(x) by A4,A6,FUNCT_1:70; end; given x being set such that A7: x in dom (NHP.s) & y = (NHP.s).x; consider a be set such that A8: a in X.s & x = root-tree [a,s] by A3,A7,Def24; y = (NH.s).(root-tree [a,s]) by A4,A7,A8,FUNCT_1:70; then y in OSFreeGen(s,X) by A8,Def26; hence y in FG.s by Def27; end; hence A9: rng (NHP.s) = FG.s by FUNCT_1:def 5; hence NHP.s is Function of PTVars(s,X),FG.s by A5,FUNCT_2:3; thus NHP.s is Function of (PTVars(X)).s,FG.s by A3,A5,A9,FUNCT_2:3; end; then for i being set st i in the carrier of S holds NHP.i is Function of (PTVars(X)).i, FG.i; then reconsider NHP = (NH1 || PTVars(X)) as ManySortedFunction of PTVars(X),FG by MSUALG_1:def 2; consider h being ManySortedFunction of PTA,U1 such that A10: h is_homomorphism PTA,U1 & h is order-sorted & h || PTVars(X) = F ** NHP by Th38; reconsider hCng = OSCng(h) as monotone OSCongruence of PTA by A10,OSALG_4:26; A11: R c= hCng by Def18; reconsider H = OSHomQuot(h,R) as ManySortedFunction of FA,U1 by Def19; take H; thus H is_homomorphism FA,U1 & H is order-sorted by A1,A10,A11,OSALG_4:27; for s be Element of S for f be Function of SA.s,S1.s st f = H.s holds F.s = f | (FG.s) proof let s be Element of S; let f be Function of SA.s,S1.s such that A12: f = H.s; A13: FG.s = OSFreeGen(s,X) by Def27; then FG.s c= SA.s; then FG.s c= dom OSHomQuot(h,R,s) by A1,FUNCT_2:def 1; then A14: dom (OSHomQuot(h,R,s) | (FG.s)) = FG.s & rng (OSHomQuot(h,R,s) | (FG.s)) c= rng (OSHomQuot(h,R,s)) by FUNCT_1:76,RELAT_1:91; rng (OSHomQuot(h,R,s) | (FG.s)) c= S1.s by RELSET_1:12; then reconsider OSF = OSHomQuot(h,R,s) | (FG.s) as Function of FG.s,S1.s by A14,FUNCT_2:4; now let x be set such that A15: x in FG.s; consider a being set such that A16: a in X.s & x = (NH.s).(root-tree [a,s]) by A13,A15,Def26; A17: root-tree [a,s] in PTVars(s,X) by A16,Def24; reconsider xa = root-tree [a,s] as Element of SPTA.s by A16,Th10; A18: xa in (PTVars(X)).s by A17,Def25; A19: OSClass(R,xa) = (OSNat_Hom(PTA,R,s)).xa by OSALG_4:def 23 .= x by A16,OSALG_4:def 24; A20: (NHP.s).xa = ((NH.s) | (PTVars(s,X))).xa by A2 .= (NH.s).xa by A17,FUNCT_1:72; A21: (OSHomQuot(h,R,s)).(OSClass(R,xa)) = (h.s).xa by A10,A11,OSALG_4:def 29; A22: ((h.s) | ((PTVars(X)).s)) = (F ** NHP).s by A10,MSAFREE:def 1 .= (F.s )*(NHP.s) by MSUALG_3:2; A23: (h.s).xa = (h.s | ((PTVars(X)).s)).xa by A18,FUNCT_1:72; dom (NHP.s) = PTVars(s,X) by A2; then (h.s).xa = (F.s).x by A16,A17,A20,A22,A23,FUNCT_1:23; hence (F.s).x = (OSHomQuot(h,R,s) | (FG.s)).x by A15,A19,A21,FUNCT_1:72; end; then F.s = OSF by FUNCT_2:18; hence F.s = f | (FG.s) by A12,OSALG_4:def 30; end; then for i be set st i in the carrier of S for f be Function of SA.i,S1.i st f = H.i holds F.i = f | (FG.i); hence H || FG = F by MSAFREE:def 1; end; theorem Th40: for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S holds FreeOSA(X) is osfree proof let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S; take OSFreeGen(X); thus thesis by Th39; end; definition let S be locally_directed OrderSortedSign; cluster osfree strict (non-empty monotone OSAlgebra of S); existence proof consider U1 be non-empty OSAlgebra of S; reconsider X = the Sorts of U1 as non-empty ManySortedSet of S; take FreeOSA(X); thus thesis by Th40; end; end; begin :: PTMin ... minimality of PTCongruence on regular signatures :: minimal terms definition let S be locally_directed regular (monotone OrderSortedSign), X be non-empty ManySortedSet of S; func PTMin X -> Function of TS(DTConOSA(X)), TS(DTConOSA(X)) means :Def32: (for t being Symbol of DTConOSA(X) st t in Terminals DTConOSA(X) holds it.(root-tree t) = pi t ) & (for nt being Symbol of DTConOSA(X), ts being FinSequence of TS(DTConOSA(X)) st nt ==> roots ts holds it.(nt-tree ts) = pi(@(X,nt),it * ts) ); existence proof set G = DTConOSA(X); set D = TS G; deffunc TermVal(Symbol of G) = pi $1; deffunc NTermVal(Symbol of G,FinSequence of TS(G), FinSequence of D) = pi(@(X,$1),$3); thus ex f being Function of TS(G), D st (for t being Symbol of G st t in Terminals G holds f.(root-tree t) = TermVal(t)) & (for nt being Symbol of G, ts being FinSequence of TS(G) st nt ==> roots ts holds f.(nt-tree ts) = NTermVal(nt, roots ts, f*ts)) from DTConstrIndDef; end; uniqueness proof set G = DTConOSA(X); set D = TS G; deffunc TermVal(Symbol of G) = pi $1; deffunc NTermVal(Symbol of G,FinSequence of TS(G), FinSequence of D) = pi(@(X,$1),$3); let M1,M2 be Function of TS(DTConOSA(X)), TS(DTConOSA(X)) such that A1: (for t being Symbol of DTConOSA(X) st t in Terminals DTConOSA(X) holds M1.(root-tree t) = TermVal(t) ) & (for nt being Symbol of DTConOSA(X), ts being FinSequence of TS(DTConOSA(X)) st nt ==> roots ts holds M1.(nt-tree ts) = NTermVal(nt, roots ts, M1 * ts) ) and A2: (for t being Symbol of DTConOSA(X) st t in Terminals DTConOSA(X) holds M2.(root-tree t) = TermVal(t) ) & (for nt being Symbol of DTConOSA(X), ts being FinSequence of TS(DTConOSA(X)) st nt ==> roots ts holds M2.(nt-tree ts) = NTermVal(nt, roots ts, M2 * ts) ); thus M1 = M2 from DTConstrUniqDef(A1,A2); end; end; theorem Th41: for S be locally_directed regular (monotone OrderSortedSign), X be non-empty ManySortedSet of S, t being Element of TS DTConOSA(X) holds (PTMin X).t in OSClass(PTCongruence(X),t) & LeastSort ((PTMin X).t) <= LeastSort t & (for s being Element of S, x being set st x in X.s & t = root-tree [x,s] holds (PTMin X).t = t ) & (for o being OperSymbol of S, ts being FinSequence of TS(DTConOSA(X)) st OSSym(o,X) ==> roots ts & t = OSSym(o,X)-tree ts holds LeastSorts ((PTMin X)*ts) <= the_arity_of o & OSSym(o,X) ==> roots ((PTMin X)*ts) & OSSym(LBound(o,LeastSorts ((PTMin X)*ts)),X) ==> roots ((PTMin X)*ts) & (PTMin X).t = OSSym(LBound(o,LeastSorts ((PTMin X)*ts)),X)-tree ((PTMin X)*ts)) proof let S be locally_directed regular (monotone OrderSortedSign), X be non-empty ManySortedSet of S, t be Element of TS DTConOSA(X); set PTA = ParsedTermsOSA(X), D = DTConOSA(X), R = PTCongruence(X), SPTA = (the Sorts of PTA), M = PTMin(X), F = PTClasses(X); defpred P1[Element of TS D] means (PTMin X).$1 in OSClass(R,$1); defpred P2[Element of TS D] means LeastSort ((PTMin X).$1) <= LeastSort $1; defpred P4[Element of TS D] means (for s being Element of S, x being set st x in X.s & $1 = root-tree [x,s] holds (PTMin X).$1 = $1 ); defpred P5[Element of TS D] means for o being OperSymbol of S, ts being FinSequence of TS(DTConOSA(X)) st OSSym(o,X) ==> roots ts & $1 = OSSym(o,X)-tree ts holds LeastSorts ((PTMin X)*ts) <= the_arity_of o & OSSym(o,X) ==> roots ((PTMin X)*ts) & OSSym(LBound(o,LeastSorts ((PTMin X)*ts)),X) ==> roots ((PTMin X)*ts) & (PTMin X).$1 = OSSym(LBound(o,LeastSorts ((PTMin X)*ts)),X)-tree ((PTMin X)*ts); defpred P[DecoratedTree of the carrier of D] means ex t1 being Element of TS D st t1 = $1 & P1[t1] & P2[t1] & P4[t1] & P5[t1]; A1: for s being Symbol of D st s in Terminals D holds P[root-tree s] proof let sy be Symbol of D such that A2: sy in Terminals D; reconsider t1 = root-tree sy as Element of TS DTConOSA(X) by A2,DTCONSTR:def 4; take t1; thus t1 = root-tree sy; consider s be Element of S, x be set such that A3: x in X.s & sy = [x,s] by A2,Th4; A4: M.(root-tree sy) = pi sy by A2,Def32 .= root-tree sy by A2,Def17; hence M.t1 in OSClass(R,t1) by Th33; thus LeastSort (M.t1) <= LeastSort t1 by A4; thus for s1 being Element of S, x1 being set st x1 in X.s1 & t1 = root-tree [x1,s1] holds M.t1 = t1 by A4; hereby let o being OperSymbol of S, ts being FinSequence of TS(DTConOSA(X)) such that A5: OSSym(o,X) ==> roots ts & t1 = OSSym(o,X)-tree ts; t1.{} = OSSym(o,X) by A5,TREES_4:def 4 .= [o,the carrier of S] by Def6; hence LeastSorts ((PTMin X)*ts) <= the_arity_of o & OSSym(o,X) ==> roots ((PTMin X)*ts) & OSSym(LBound(o,LeastSorts ((PTMin X)*ts)),X) ==> roots ((PTMin X)*ts) & (PTMin X).t1 = OSSym(LBound(o,LeastSorts ((PTMin X)*ts)),X)-tree ((PTMin X)*ts) by A3, Th10; end; end; A6: for nt being Symbol of D, ts1 being FinSequence of TS(D) st nt ==> roots ts1 & (for dt1 being DecoratedTree of the carrier of D st dt1 in rng ts1 holds P[dt1]) holds P[nt-tree ts1] proof let nt being Symbol of D, ts1 being FinSequence of TS(D) such that A7: nt ==> roots ts1 and A8: (for dt1 being DecoratedTree of the carrier of D st dt1 in rng ts1 ex t2 being Element of TS D st t2 = dt1 & P1[t2] & P2[t2] & P4[t2] & P5[t2]); reconsider t1 = nt-tree ts1 as Element of TS D by A7,Th12; take t1; thus t1 = nt-tree ts1; reconsider ta1 = t1 as Element of SPTA.(LeastSort t1) by Def12; consider o being OperSymbol of S such that A9: nt = [o,the carrier of S] & ts1 in Args(o,PTA) & nt-tree ts1 = Den(o,PTA).ts1 & for s1 being Element of S holds nt-tree ts1 in SPTA.s1 iff the_result_sort_of o <= s1 by A7,Th12; A10: OSClass(R,t1) = OSClass(R,ta1) by Def28 .= proj1(F.t1) by Th26; set Ms = (PTMin X)*ts1, LSMs = LeastSorts Ms, w = the_arity_of o, so = the_result_sort_of o, Lo = LBound(o,LSMs); A11: dom (F*ts1) = dom ts1 & dom ((PTMin X)*ts1) = dom ts1 & dom (LeastSorts ts1) = dom ts1 & dom ts1 = dom w by A9,Def14,ALG_1:1,MSUALG_3:6; then A12: dom LSMs = dom ts1 by Def14; A13: rng ts1 c= TS D by FINSEQ_1:def 4; @(X,nt) = o by A7,A9,Def16; then A14: M.(nt-tree ts1) = pi(o,M*ts1) by A7,Def32; A15: nt = OSSym(o,X) by A9,Def6; A16: LeastSort t1 = so by A9,Th18; consider l being Nat such that A17: dom ts1 = Seg l by FINSEQ_1:def 2; A18: F.t1 = @(nt,F*ts1) by A7,Def22 .= {[Den(o2,ParsedTermsOSA(X)).x2,s3] where o2 is OperSymbol of S, x2 is Element of Args(o2,ParsedTermsOSA(X)), s3 is Element of S : ( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] & o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of (the carrier of S)* st dom w3 = dom (F*ts1) & for y being Nat st y in dom (F*ts1) holds [x2.y,w3/.y] in (F*ts1).y} by Def21; A19: P5[t1] proof let o2 be OperSymbol of S, ts be FinSequence of TS(DTConOSA(X)) such that A20: OSSym(o2,X) ==> roots ts & t1 = OSSym(o2,X)-tree ts; A21: OSSym(o2,X) = [o2,the carrier of S] by Def6; A22: OSSym(o2,X) = nt & ts = ts1 by A20,TREES_4:15; then A23: o2 = o by A9,A21,ZFMISC_1:33; set Ms1 = (PTMin X)*ts, LSMs1 = LeastSorts Ms1, Lo2 = LBound(o2,LSMs1); A24: LeastSorts ((PTMin X)*ts1) <= the_arity_of o proof thus len LSMs = len w by A11,A12,FINSEQ_3:31; let i be set such that A25: i in dom LSMs; reconsider k = i as Nat by A25; A26: ts1.k in rng ts1 by A12,A25,FUNCT_1:12; then reconsider tr = ts1.k as Element of TS D by A13; consider tr1 being Element of TS D such that A27: tr1 = tr & P1[tr1] & P2[tr1] & P4[tr1] & P5[tr1] by A8,A26; let s1,s2 be Element of S such that A28: s1 = LSMs.i & s2 = w.i; consider t3 being Element of TS D such that A29: t3 = Ms.k & LSMs.k = LeastSort t3 by A11,A12,A25,Def14; A30: Ms.k = (PTMin X).tr by A11,A12,A25,ALG_1:1; ts1.k in SPTA.(w/.k) by A9,A11,A12,A25,MSUALG_6:2; then A31: LeastSort (tr) <= (w/.k) by Def12; w/.k = w.i by A11,A12,A25,FINSEQ_4:def 4; hence s1 <= s2 by A27,A28,A29,A30,A31,ORDERS_1:26; end; hence LeastSorts ((PTMin X)*ts) <= the_arity_of o2 by A9,A21,A22,ZFMISC_1 :33; LBound(o2,LSMs1) has_least_rank_for o2,LSMs1 by A22,A23,A24,OSALG_1:14; then LBound(o2,LSMs1) has_least_args_for o2,LSMs1 & LBound(o2,LSMs1) has_least_sort_for o2,LSMs1 by OSALG_1:def 12; then o2 ~= Lo2 & LSMs1 <= the_arity_of Lo2 & for o3 being OperSymbol of S st o2 ~= o3 & LSMs1 <= the_arity_of o3 holds the_arity_of Lo2 <= the_arity_of o3 by OSALG_1:def 10; then Ms1 in Args(Lo2,PTA) & Ms1 in Args(o2,PTA) by A22,A23,A24,Th19; hence OSSym(o2,X) ==> roots Ms1 & OSSym(Lo2,X) ==> roots Ms1 by Th13; hence M.t1 = OSSym(LBound(o2,LSMs1),X)-tree Ms1 by A14,A22,A23,Def15; end; then A32: LeastSorts ((PTMin X)*ts1) <= the_arity_of o & OSSym(o,X) ==> roots ((PTMin X)*ts1) & OSSym(LBound(o,LeastSorts ((PTMin X)*ts1)),X) ==> roots ((PTMin X)*ts1) & (PTMin X).t1 = OSSym(LBound(o,LeastSorts ((PTMin X)*ts1)),X)-tree ((PTMin X)*ts1) by A7,A15; then consider o3 being OperSymbol of S such that A33: OSSym(Lo,X) = [o3,the carrier of S] & Ms in Args(o3,ParsedTermsOSA(X)) & OSSym(Lo,X)-tree Ms = Den(o3,ParsedTermsOSA(X)).Ms & for s1 being Element of S holds OSSym(Lo,X)-tree Ms in (the Sorts of PTA).s1 iff the_result_sort_of o3 <= s1 by Th12; A34: OSSym(Lo,X) = [Lo,the carrier of S] by Def6; then A35: Lo = o3 by A33,ZFMISC_1:33; reconsider Msr = Ms as Element of Args(Lo,PTA) by A33,A34,ZFMISC_1:33; A36: M.t1 = Den(Lo,PTA).(Msr) by A7,A15,A19,A33,A35; A37: LeastSort (M.t1) = the_result_sort_of Lo by A32,A33,A35,Th18; Lo has_least_rank_for o,LSMs by A32,OSALG_1:14; then A38: Lo has_least_args_for o,LSMs & Lo has_least_sort_for o,LSMs by OSALG_1:def 12; then A39: o ~= Lo & LSMs <= the_arity_of Lo & for o3 being OperSymbol of S st o ~= o3 & LSMs <= the_arity_of o3 holds the_result_sort_of Lo <= the_result_sort_of o3 by OSALG_1:def 11; A40: the_result_sort_of Lo <= so & the_arity_of Lo <= w by A32,A38,OSALG_1:def 10,def 11; then A41: len the_arity_of Lo = len w by OSALG_1:def 7; A42: M.t1 in OSClass(R,t1) proof defpred P[set,set] means [Ms.$1,$2] in (F*ts1).$1; A43: for i being set st i in dom (F*ts1) ex s4 being set st s4 in the carrier of S & P[i,s4] proof let i be set such that A44: i in dom (F*ts1); A45: Ms.i = M.(ts1.i) & (F*ts1).i = F.(ts1.i) & ts1.i in rng ts1 by A11,A44,FUNCT_1:12,23; then reconsider td1 = ts1.i as Element of TS D by A13; reconsider tda = td1 as Element of SPTA.(LeastSort td1) by Def12; consider td2 being Element of TS D such that A46: td2 = td1 & M.td2 in OSClass(R,td2) & P2[td2] & P4[td2] & P5[td2] by A8,A45; OSClass(R,td1) = OSClass(R,tda) by Def28 .= proj1((F*ts1).i) by A45,Th26; then consider s4 being set such that A47: [Ms.i,s4] in (F*ts1).i by A45,A46,FUNCT_5:def 1; s4 in the carrier of S by A45,A47,Th24; hence thesis by A47; end; consider f being Function such that A48: dom f = dom (F*ts1) & rng f c= the carrier of S & for z being set st z in dom (F*ts1) holds P[z,f.z] from NonUniqBoundFuncEx(A43); reconsider wa = f as FinSequence by A11,A17,A48,FINSEQ_1:def 2; reconsider wa as FinSequence of the carrier of S by A48,FINSEQ_1:def 4; reconsider wa as Element of (the carrier of S)* by FINSEQ_1:def 11; for y being Nat st y in dom (F*ts1) holds [Msr.y,wa/.y] in (F*ts1).y proof let y be Nat such that A49: y in dom (F*ts1); (wa/.y) = wa.y by A48,A49,FINSEQ_4:def 4; hence thesis by A48,A49; end; then [Den(Lo,PTA).Msr,so] in F.t1 by A9,A18,A39,A40,A41,A48; hence M.t1 in OSClass(R,t1) by A10,A36,FUNCT_5:4; end; for s being Element of S, x being set st x in X.s & t1 = root-tree [x,s] holds M.t1 = t1 proof let s being Element of S, x being set such that A50: x in X.s & t1 = root-tree [x,s]; t1.{} = [o,the carrier of S] by A9,TREES_4:def 4; hence thesis by A50,Th10; end; hence P1[t1] & P2[t1] & P4[t1] & P5[t1] by A16,A19,A32,A37,A38,A42,OSALG_1: def 11; end; for dt being DecoratedTree of the carrier of D st dt in TS(D) holds P[dt] from DTConstrInd(A1,A6); then consider t1 being Element of TS D such that A51: t1 = t & P1[t1] & P2[t1] & P4[t1] & P5[t1]; thus P1[t] & P2[t] & P4[t] & P5[t] by A51; end; theorem Th42: for S be locally_directed regular (monotone OrderSortedSign), X be non-empty ManySortedSet of S, t,t1 being Element of TS DTConOSA(X) st t1 in OSClass(PTCongruence(X),t) holds (PTMin X).t1 = (PTMin X).t proof let S be locally_directed regular (monotone OrderSortedSign), X be non-empty ManySortedSet of S, t be Element of TS DTConOSA(X); set PTA = ParsedTermsOSA(X), D = DTConOSA(X), R = PTCongruence(X), SPTA = (the Sorts of PTA), M = PTMin(X), F = PTClasses(X); defpred P3[Element of TS D] means (for t1 being Element of TS DTConOSA(X) st t1 in OSClass(R,$1) holds (PTMin X).t1 = (PTMin X).$1 ); defpred P[DecoratedTree of the carrier of D] means ex t1 being Element of TS D st t1 = $1 & P3[t1]; A1: for s being Symbol of D st s in Terminals D holds P[root-tree s] proof let sy be Symbol of D such that A2: sy in Terminals D; reconsider t1 = root-tree sy as Element of TS DTConOSA(X) by A2,DTCONSTR:def 4; take t1; thus t1 = root-tree sy; consider s be Element of S, x be set such that A3: x in X.s & sy = [x,s] by A2,Th4; let t2 be Element of TS DTConOSA(X) such that A4: t2 in OSClass(R,t1); thus M.t2 = M.t1 by A3,A4,Th34; end; A5: for nt being Symbol of D, ts1 being FinSequence of TS(D) st nt ==> roots ts1 & (for dt1 being DecoratedTree of the carrier of D st dt1 in rng ts1 holds P[dt1]) holds P[nt-tree ts1] proof let nt being Symbol of D, ts1 being FinSequence of TS(D) such that A6: nt ==> roots ts1 and A7: for dt1 being DecoratedTree of the carrier of D st dt1 in rng ts1 ex t2 being Element of TS D st t2 = dt1 & P3[t2]; reconsider t1 = nt-tree ts1 as Element of TS D by A6,Th12; take t1; thus t1 = nt-tree ts1; reconsider ta1 = t1 as Element of SPTA.(LeastSort t1) by Def12; consider o being OperSymbol of S such that A8: nt = [o,the carrier of S] & ts1 in Args(o,PTA) & nt-tree ts1 = Den(o,PTA).ts1 & for s1 being Element of S holds nt-tree ts1 in SPTA.s1 iff the_result_sort_of o <= s1 by A6,Th12; A9: OSClass(R,t1) = OSClass(R,ta1) by Def28 .= proj1(F.t1) by Th26; set Ms = (PTMin X)*ts1, w = the_arity_of o; A10: dom (F*ts1) = dom ts1 & dom ((PTMin X)*ts1) = dom ts1 & dom (LeastSorts ts1) = dom ts1 & dom ts1 = dom w by A8,Def14,ALG_1:1,MSUALG_3:6; A11: rng ts1 c= TS D by FINSEQ_1:def 4; t1 = OSSym(o,X)-tree ts1 & OSSym(o,X) ==> roots ts1 by A6,A8,Def6; then A12: M.t1 = OSSym(LBound(o,LeastSorts (M*ts1)),X)-tree (M*ts1) & LeastSorts (M*ts1) <= the_arity_of o by Th41; A13: F.t1 = @(nt,F*ts1) by A6,Def22 .= {[Den(o2,ParsedTermsOSA(X)).x2,s3] where o2 is OperSymbol of S, x2 is Element of Args(o2,ParsedTermsOSA(X)), s3 is Element of S : ( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] & o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of (the carrier of S)* st dom w3 = dom (F*ts1) & for y being Nat st y in dom (F*ts1) holds [x2.y,w3/.y] in (F*ts1).y} by Def21; thus for t3 being Element of TS DTConOSA(X) st t3 in OSClass(R,t1) holds (PTMin X).t3 = (PTMin X).t1 proof let t3 be Element of TS D such that A14: t3 in OSClass(R,t1); consider s4 being set such that A15: [t3,s4] in F.t1 by A9,A14,FUNCT_5:def 1; consider o2 being OperSymbol of S, x2 being Element of Args(o2,ParsedTermsOSA(X)), s3 being Element of S such that A16: [t3,s4] = [Den(o2,ParsedTermsOSA(X)).x2,s3] and A17: ex o1 being OperSymbol of S st nt = [o1,the carrier of S] & o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 and A18: ex w3 being Element of (the carrier of S)* st dom w3 = dom (F*ts1) & for y being Nat st y in dom (F*ts1) holds [x2.y,w3/.y] in (F*ts1).y by A13,A15; consider o1 being OperSymbol of S such that A19: nt = [o1,the carrier of S] & o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 by A17; A20: o1 = o by A8,A19,ZFMISC_1:33; A21: x2 is FinSequence of TS(D) & OSSym(o2,X) ==> roots x2 by Th13; reconsider ts3 = x2 as FinSequence of TS(D) by Th13; OSSym(o2,X) in NonTerminals D & OSSym(o2,X)-tree ts3 in TS D & ex o3 being OperSymbol of S st OSSym(o2,X) = [o3,the carrier of S] & ts3 in Args(o3,PTA) & OSSym(o2,X)-tree ts3 = Den(o3,PTA).ts3 & for s1 being Element of S holds OSSym(o2,X)-tree ts3 in SPTA.s1 iff the_result_sort_of o3 <= s1 by A21,Th12; then consider o3 being OperSymbol of S such that A22: OSSym(o2,X) = [o3,the carrier of S] & ts3 in Args(o3,PTA) & OSSym(o2,X)-tree ts3 = Den(o3,PTA).ts3; OSSym(o2,X) = [o2,the carrier of S] by Def6; then o2 = o3 by A22,ZFMISC_1:33; then A23: t3 = OSSym(o2,X)-tree ts3 by A16,A22,ZFMISC_1:33; A24:dom w = dom the_arity_of o2 & dom ts3 = dom the_arity_of o2 & dom (M*ts3) = dom ts3 by A19,A20,ALG_1:1,FINSEQ_3:31,MSUALG_3:6; A25: rng ts3 c= TS D by FINSEQ_1:def 4; for k being Nat st k in dom (M*ts3) holds (M*ts3).k = Ms.k proof let k being Nat such that A26: k in dom (M*ts3); A27: ts1.k in rng ts1 & ts3.k in rng ts3 by A10,A24,A26,FUNCT_1:12; then reconsider tk1 = ts1.k, tk3 = ts3.k as Element of TS D by A11,A25; consider tk2 be Element of TS D such that A28: tk2 = tk1 and A29: for t4 being Element of TS D st t4 in OSClass(R,tk2) holds M.t4 = M.tk2 by A7,A27; reconsider tak = tk1 as Element of SPTA.(LeastSort tk1) by Def12; A30: OSClass(R,tk1) = OSClass(R,tak) by Def28 .= proj1(F.tk1) by Th26; consider w3 being Element of (the carrier of S)* such that dom w3 = dom (F*ts1) and A31: for y being Nat st y in dom (F*ts1) holds [x2.y,w3/.y] in (F*ts1).y by A18; [tk3,w3/.k] in (F*ts1).k by A10,A24,A26,A31; then [tk3,w3/.k] in F.tk1 by A10,A24,A26,ALG_1:1; then tk3 in proj1(F.tk1) by FUNCT_5:4; then M.tk3 = M.tk1 by A28,A29,A30; then M.tk3 = Ms.k by A10,A24,A26,ALG_1:1; hence (M*ts3).k = Ms.k by A26,ALG_1:1; end; then A32: M*ts3 = M*ts1 by A10,A24,FINSEQ_1:17; M.t3 = OSSym(LBound(o2,LeastSorts (M*ts3)),X)-tree (M*ts3) & LeastSorts (M*ts3) <= the_arity_of o2 by A21,A23,Th41; hence M.t3 = M.t1 by A12,A19,A20,A32,OSALG_1:34; end; end; for dt being DecoratedTree of the carrier of D st dt in TS(D) holds P[dt] from DTConstrInd(A1,A5); then consider t1 being Element of TS D such that A33: t1 = t & P3[t1]; thus P3[t] by A33; end; theorem Th43: for S be locally_directed regular (monotone OrderSortedSign), X be non-empty ManySortedSet of S, t1,t2 be Element of TS DTConOSA(X) holds t2 in OSClass(PTCongruence(X),t1) iff (PTMin X).t2 = (PTMin X).t1 proof let S be locally_directed regular (monotone OrderSortedSign), X be non-empty ManySortedSet of S, t1,t2 be Element of TS DTConOSA(X); set R = PTCongruence(X),M = PTMin(X); thus t2 in OSClass(R,t1) implies M.t2 = M.t1 by Th42; assume A1: M.t2 = M.t1; M.t2 in OSClass(R,t2) & M.t1 in OSClass(R,t1) by Th41; then OSClass(R,t1) = OSClass(R,M.t1) & OSClass(R,t2) = OSClass(R,M.t2) by Th35; hence thesis by A1,Th33; end; theorem Th44: for S be locally_directed regular (monotone OrderSortedSign), X be non-empty ManySortedSet of S, t1 be Element of TS DTConOSA(X) holds (PTMin X).((PTMin X).t1) = (PTMin X).t1 proof let S be locally_directed regular (monotone OrderSortedSign), X be non-empty ManySortedSet of S, t1 be Element of TS DTConOSA(X); (PTMin X).t1 in OSClass(PTCongruence(X),t1) by Th41; hence thesis by Th43; end; theorem Th45: for S be locally_directed regular (monotone OrderSortedSign), X be non-empty ManySortedSet of S, R be monotone (MSEquivalence-like OrderSortedRelation of ParsedTermsOSA(X)), t be Element of TS DTConOSA(X) holds [t,(PTMin X).t] in R.(LeastSort t) proof let S be locally_directed regular (monotone OrderSortedSign), X be non-empty ManySortedSet of S; set PTA = ParsedTermsOSA(X), SPTA = the Sorts of PTA, D = DTConOSA(X), F = PTClasses X, M = PTMin X; let R be monotone (MSEquivalence-like OrderSortedRelation of PTA); A1: R is os-compatible by OSALG_4:def 3; defpred P3[set] means ex t1 being Element of TS D st t1 = $1 & [t1,M.t1] in R.(LeastSort t1); A2: for s being Symbol of D st s in Terminals D holds P3[root-tree s] proof let sy being Symbol of D such that A3: sy in Terminals D; consider s be Element of S, x be set such that A4: x in X.s & sy = [x,s] by A3,Th4; reconsider t1 = root-tree sy as Element of TS D by A4,Th10; take t1; A5: t1 = M.t1 by A4,Th41; A6: t1 in SPTA.(LeastSort t1) by Def12; field(R.(LeastSort t1)) = SPTA.(LeastSort t1) by ORDERS_1:97; then R.(LeastSort t1) is_reflexive_in SPTA.(LeastSort t1) by RELAT_2:def 9; hence thesis by A5,A6,RELAT_2:def 1; end; A7: for nt being Symbol of D, ts1 being FinSequence of TS(D) st nt ==> roots ts1 & (for dt1 being DecoratedTree of the carrier of D st dt1 in rng ts1 holds P3[dt1] ) holds P3[nt-tree ts1] proof let nt being Symbol of D, ts1 being FinSequence of TS(D) such that A8: nt ==> roots ts1 and A9: for dt1 being DecoratedTree of the carrier of D st dt1 in rng ts1 holds P3[dt1]; reconsider t1 = nt-tree ts1 as Element of TS D by A8,Th12; take t1; thus t1 = nt-tree ts1; consider o being OperSymbol of S such that A10: nt = [o,the carrier of S] & ts1 in Args(o,PTA) & nt-tree ts1 = Den(o,PTA).ts1 & for s1 being Element of S holds nt-tree ts1 in SPTA.s1 iff the_result_sort_of o <= s1 by A8,Th12; set w = the_arity_of o; A11: dom (F*ts1) = dom ts1 & dom ((PTMin X)*ts1) = dom ts1 & dom (LeastSorts ts1) = dom ts1 & dom ts1 = dom w by A10,Def14,ALG_1:1,MSUALG_3:6; A12: rng ts1 c= TS D by FINSEQ_1:def 4; A13: OSSym(o,X) ==> roots ts1 & t1 = OSSym(o,X)-tree ts1 by A8,A10,Def6; then A14: LeastSort (M.t1) <= LeastSort t1 & LeastSorts (M*ts1) <= the_arity_of o & OSSym(o,X) ==> roots (M*ts1) & OSSym(LBound(o,LeastSorts (M*ts1)),X) ==> roots (M*ts1) & M.t1 = OSSym(LBound(o,LeastSorts(M*ts1)),X)-tree (M*ts1) by Th41; set lo = LBound(o,LeastSorts (M*ts1)), rs1 = the_result_sort_of o; A15: lo <= o by A14,OSALG_1:35; reconsider tsa =ts1 as Element of Args(o,PTA) by A10; reconsider tsm =M*ts1 as Element of Args(lo,PTA) by A14,Th13; for y being Nat st y in dom tsm holds [tsm.y,tsa.y] in R.((the_arity_of o)/.y) proof let y being Nat such that A16: y in dom tsm; A17: ts1.y in rng ts1 by A11,A16,FUNCT_1:12; then reconsider td1=ts1.y as Element of TS D by A12; consider t2 being Element of TS D such that A18: t2 = td1 and A19: [t2,M.t2] in R.(LeastSort t2) by A9,A17; A20: t2 in SPTA.(LeastSort t2) & M.t2 in SPTA.(LeastSort t2) by A19,ZFMISC_1:106; field(R.(LeastSort t2)) = SPTA.(LeastSort t2) by ORDERS_1:97; then R.(LeastSort t2) is_symmetric_in SPTA.(LeastSort t2) by RELAT_2:def 11; then A21: [M.t2,t2] in R.(LeastSort t2) by A19,A20,RELAT_2:def 3; A22: M.t2 = tsm.y by A16,A18,ALG_1:1; tsa.y in SPTA.(w/.y) by A11,A16,MSUALG_6:2; then LeastSort t2 <= w/.y by A18,Def12; hence [tsm.y,tsa.y] in R.(w/.y) by A1,A18,A20,A21,A22,OSALG_4:def 1; end; then A23: [Den(lo,PTA).tsm,Den(o,PTA).tsa] in R.(the_result_sort_of o) by A15,OSALG_4:def 28; then A24: Den(lo,PTA).tsm in SPTA.rs1 & Den(o,PTA).tsa in SPTA.rs1 by ZFMISC_1:106; field(R.rs1) = SPTA.rs1 by ORDERS_1:97; then R.rs1 is_symmetric_in SPTA.rs1 by RELAT_2:def 11; then A25: [Den(o,PTA).tsa,Den(lo,PTA).tsm] in R.rs1 by A23,A24,RELAT_2:def 3; A26: LeastSort t1 = the_result_sort_of o by A10,Th18; consider o4 being OperSymbol of S such that A27: OSSym(lo,X) = [o4,the carrier of S] & M*ts1 in Args(o4,PTA) & OSSym(lo,X)-tree (M*ts1) = Den(o4,PTA).(M*ts1) & for s1 being Element of S holds OSSym(lo,X)-tree (M*ts1) in SPTA.s1 iff the_result_sort_of o4 <= s1 by A14,Th12; OSSym(lo,X) = [lo,the carrier of S] by Def6; then lo = o4 by A27,ZFMISC_1:33; hence [t1,M.t1] in R.(LeastSort t1) by A10,A13,A25,A26,A27,Th41; end; A28: for dt being DecoratedTree of the carrier of D st dt in TS(D) holds P3[dt] from DTConstrInd(A2,A7); let t be Element of TS D; consider t1 being Element of TS D such that A29: t = t1 & [t1,M.t1] in R.(LeastSort t1) by A28; thus thesis by A29; end; theorem Th46: for S be locally_directed regular (monotone OrderSortedSign), X be non-empty ManySortedSet of S, R be monotone (MSEquivalence-like OrderSortedRelation of ParsedTermsOSA(X)) holds PTCongruence(X) c= R proof let S be locally_directed regular (monotone OrderSortedSign), X be non-empty ManySortedSet of S; set PTA = ParsedTermsOSA(X), SPTA = the Sorts of PTA, D = DTConOSA(X), M = PTMin X, P = PTCongruence X; reconsider O1 = SPTA as OrderSortedSet of S by OSALG_1:17; let R be monotone (MSEquivalence-like OrderSortedRelation of PTA); A1: R is os-compatible by OSALG_4:def 3; let i be set such that A2: i in the carrier of S; reconsider s = i as Element of S by A2; for a,b being set holds [a,b] in P.s implies [a,b] in R.s proof let a,b be set such that A3: [a,b] in P.s; A4: a in SPTA.i & b in SPTA.i by A3,ZFMISC_1:106; reconsider ta=a,tb=b as Element of SPTA.s by A3,ZFMISC_1:106; dom SPTA = the carrier of S by PBOOLE:def 3; then a in Union SPTA & b in Union SPTA by A2,A4,CARD_5:10; then reconsider t1=a,t2=b as Element of PTA; reconsider t1,t2 as Element of TS D by Th15; A5: t1 in SPTA.(LeastSort t1) & t2 in SPTA.(LeastSort t2) & M.t1 in SPTA.(LeastSort M.t1) & M.t2 in SPTA.(LeastSort M.t2) & LeastSort t1 <= s & LeastSort t2 <= s by A4,Def12; A6: OSClass(P,ta) = OSClass(P,tb) by A3,OSALG_4:13; OSClass(P,t1) = OSClass(P,ta) & OSClass(P,t2) = OSClass(P,tb) by Def28; then t1 in OSClass(P,t2) by A6,Th35; then A7: M.t1 = M.t2 by Th43; LeastSort (M.t1) <= LeastSort t1 & LeastSort (M.t2) <= LeastSort t2 by Th41; then A8: O1.(LeastSort (M.t1)) c= O1.(LeastSort t1) & O1.(LeastSort (M.t2)) c= O1.(LeastSort t2) by OSALG_1:def 18; [t1,M.t1] in R.(LeastSort t1) & [t2,M.t2] in R.(LeastSort t2) by Th45; then A9: [t1,M.t1] in R.s & [t2,M.t2] in R.s by A1,A5,A8,OSALG_4:def 1; then A10: M.t1 in SPTA.s & M.t2 in SPTA.s by ZFMISC_1:106; field(R.s) = SPTA.s by ORDERS_1:97; then A11: R.s is_transitive_in SPTA.s & R.s is_symmetric_in SPTA.s by RELAT_2:def 11,def 16; then [M.t2,t2] in R.s by A4,A9,A10,RELAT_2:def 3; hence thesis by A4,A7,A9,A10,A11,RELAT_2:def 8; end; hence P.i c= R.i by RELAT_1:def 3; end; :: minimality of PTCongruence theorem for S be locally_directed regular (monotone OrderSortedSign), X be non-empty ManySortedSet of S holds LCongruence(X) = PTCongruence(X) proof let S be locally_directed regular (monotone OrderSortedSign), X be non-empty ManySortedSet of S; LCongruence(X) c= PTCongruence(X) & PTCongruence(X) c= LCongruence(X) by Def18,Th46; hence thesis by PBOOLE:def 13; end; :: I would prefer attribute "minimal", but non-clusterable definition let S be locally_directed regular (monotone OrderSortedSign), X be non-empty ManySortedSet of S; mode MinTerm of S,X -> Element of TS DTConOSA(X) means :Def33: (PTMin X).it = it; existence proof consider t being Element of TS DTConOSA(X); take (PTMin X).t; thus thesis by Th44; end; end; definition let S be locally_directed regular (monotone OrderSortedSign), X be non-empty ManySortedSet of S; func MinTerms X -> Subset of TS DTConOSA(X) equals :Def34: rng (PTMin X); correctness by RELSET_1:12; end; theorem for S be locally_directed regular (monotone OrderSortedSign), X be non-empty ManySortedSet of S, x being set holds x is MinTerm of S,X iff x in MinTerms X proof let S be locally_directed regular (monotone OrderSortedSign), X be non-empty ManySortedSet of S, x be set; hereby assume x is MinTerm of S,X; then reconsider t =x as MinTerm of S,X; (PTMin X).t = t by Def33; then t in rng (PTMin X) by FUNCT_2:6; hence x in MinTerms X by Def34; end; assume x in MinTerms X; then x in rng (PTMin X) by Def34; then consider y being set such that A1: y in dom (PTMin X) & x = (PTMin X).y by FUNCT_1:def 5; reconsider t = y as Element of TS DTConOSA(X) by A1; (PTMin X).t is Element of TS DTConOSA(X); then reconsider tx = x as Element of TS DTConOSA(X) by A1; (PTMin X).tx = tx by A1,Th44; hence thesis by Def33; end;