:: MSAFREE3 semantic presentation begin registration let S be non empty non void ManySortedSign ; let A be non empty MSAlgebra over S; cluster Union the Sorts of A -> non empty ; coherence not Union the Sorts of A is empty proof A1: dom the Sorts of A = the carrier of S by PARTFUN1:def_2; consider i being set such that A2: i in the carrier of S and A3: not the Sorts of A . i is empty by PBOOLE:def_12; set x = the Element of the Sorts of A . i; the Element of the Sorts of A . i in the Sorts of A . i by A3; hence not Union the Sorts of A is empty by A2, A1, CARD_5:2; ::_thesis: verum end; end; 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; end; theorem :: MSAFREE3:1 for I being set for A being ManySortedSet of I for F being ManySortedFunction of I st F is "1-1" & A c= doms F holds F "" (F .:.: A) = A proof let I be set ; ::_thesis: for A being ManySortedSet of I for F being ManySortedFunction of I st F is "1-1" & A c= doms F holds F "" (F .:.: A) = A let A be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of I st F is "1-1" & A c= doms F holds F "" (F .:.: A) = A let F be ManySortedFunction of I; ::_thesis: ( F is "1-1" & A c= doms F implies F "" (F .:.: A) = A ) assume that A1: F is "1-1" and A2: A c= doms F ; ::_thesis: F "" (F .:.: A) = A A3: dom F = I by PARTFUN1:def_2; now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (F_""_(F_.:.:_A))_._i_=_A_._i let i be set ; ::_thesis: ( i in I implies (F "" (F .:.: A)) . i = A . i ) assume A4: i in I ; ::_thesis: (F "" (F .:.: A)) . i = A . i then A5: F . i is one-to-one by A1, A3, MSUALG_3:def_2; A . i c= (doms F) . i by A2, A4, PBOOLE:def_2; then A6: A . i c= dom (F . i) by A3, A4, FUNCT_6:22; thus (F "" (F .:.: A)) . i = (F . i) " ((F .:.: A) . i) by A4, EQUATION:def_1 .= (F . i) " ((F . i) .: (A . i)) by A4, PBOOLE:def_20 .= A . i by A6, A5, FUNCT_1:94 ; ::_thesis: verum end; hence F "" (F .:.: A) = A by PBOOLE:3; ::_thesis: verum end; definition let S be non void Signature; let X be ManySortedSet of the carrier of S; func Free (S,X) -> strict MSAlgebra over S means :Def1: :: MSAFREE3:def 1 ex A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st ( it = GenMSAlg A & A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X ); uniqueness for b1, b2 being strict MSAlgebra over S st ex A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st ( b1 = GenMSAlg A & A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X ) & ex A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st ( b2 = GenMSAlg A & A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X ) holds b1 = b2 ; existence ex b1 being strict MSAlgebra over S ex A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st ( b1 = GenMSAlg A & A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X ) proof set I = the carrier of S; set Y = X \/ ( the carrier of S --> {0}); set R = Reverse (X \/ ( the carrier of S --> {0})); (Reverse (X \/ ( the carrier of S --> {0}))) "" X is ManySortedSubset of FreeGen (X \/ ( the carrier of S --> {0})) by EQUATION:8; then A1: (Reverse (X \/ ( the carrier of S --> {0}))) "" X c= FreeGen (X \/ ( the carrier of S --> {0})) by PBOOLE:def_18; FreeGen (X \/ ( the carrier of S --> {0})) c= the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) by PBOOLE:def_18; then (Reverse (X \/ ( the carrier of S --> {0}))) "" X c= the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) by A1, PBOOLE:13; then reconsider Z = (Reverse (X \/ ( the carrier of S --> {0}))) "" X as MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) by PBOOLE:def_18; take GenMSAlg Z ; ::_thesis: ex A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st ( GenMSAlg Z = GenMSAlg A & A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X ) take Z ; ::_thesis: ( GenMSAlg Z = GenMSAlg Z & Z = (Reverse (X \/ ( the carrier of S --> {0}))) "" X ) thus ( GenMSAlg Z = GenMSAlg Z & Z = (Reverse (X \/ ( the carrier of S --> {0}))) "" X ) ; ::_thesis: verum end; end; :: deftheorem Def1 defines Free MSAFREE3:def_1_:_ for S being non void Signature for X being ManySortedSet of the carrier of S for b3 being strict MSAlgebra over S holds ( b3 = Free (S,X) iff ex A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st ( b3 = GenMSAlg A & A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X ) ); theorem Th2: :: MSAFREE3:2 for x being set for S being non void Signature for X being ManySortedSet of the carrier of S for s being SortSymbol of S holds ( [x,s] in the carrier of (DTConMSA X) iff x in X . s ) proof let x be set ; ::_thesis: for S being non void Signature for X being ManySortedSet of the carrier of S for s being SortSymbol of S holds ( [x,s] in the carrier of (DTConMSA X) iff x in X . s ) let S be non void Signature; ::_thesis: for X being ManySortedSet of the carrier of S for s being SortSymbol of S holds ( [x,s] in the carrier of (DTConMSA X) iff x in X . s ) let X be ManySortedSet of the carrier of S; ::_thesis: for s being SortSymbol of S holds ( [x,s] in the carrier of (DTConMSA X) iff x in X . s ) let s be SortSymbol of S; ::_thesis: ( [x,s] in the carrier of (DTConMSA X) iff x in X . s ) A1: DTConMSA X = DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(REL X) #) by MSAFREE:def_8; A2: dom (coprod X) = the carrier of S by PARTFUN1:def_2; s in the carrier of S ; then s <> the carrier of S ; then not s in { the carrier of S} by TARSKI:def_1; then A3: not [x,s] in [: the carrier' of S,{ the carrier of S}:] by ZFMISC_1:87; hereby ::_thesis: ( x in X . s implies [x,s] in the carrier of (DTConMSA X) ) assume [x,s] in the carrier of (DTConMSA X) ; ::_thesis: x in X . s then [x,s] in Union (coprod X) by A1, A3, XBOOLE_0:def_3; then consider y being set such that A4: y in dom (coprod X) and A5: [x,s] in (coprod X) . y by CARD_5:2; (coprod X) . y = coprod (y,X) by A4, MSAFREE:def_3; then consider z being set such that A6: z in X . y and A7: [x,s] = [z,y] by A4, A5, MSAFREE:def_2; x = z by A7, XTUPLE_0:1; hence x in X . s by A6, A7, XTUPLE_0:1; ::_thesis: verum end; assume x in X . s ; ::_thesis: [x,s] in the carrier of (DTConMSA X) then [x,s] in coprod (s,X) by MSAFREE:def_2; then [x,s] in (coprod X) . s by MSAFREE:def_3; then [x,s] in Union (coprod X) by A2, CARD_5:2; hence [x,s] in the carrier of (DTConMSA X) by A1, XBOOLE_0:def_3; ::_thesis: verum end; theorem Th3: :: MSAFREE3:3 for x being set for S being non void Signature for Y being V8() ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S for s being SortSymbol of S holds ( ( x in X . s & x in Y . s ) iff root-tree [x,s] in ((Reverse Y) "" X) . s ) proof let x be set ; ::_thesis: for S being non void Signature for Y being V8() ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S for s being SortSymbol of S holds ( ( x in X . s & x in Y . s ) iff root-tree [x,s] in ((Reverse Y) "" X) . s ) let S be non void Signature; ::_thesis: for Y being V8() ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S for s being SortSymbol of S holds ( ( x in X . s & x in Y . s ) iff root-tree [x,s] in ((Reverse Y) "" X) . s ) let Y be V8() ManySortedSet of the carrier of S; ::_thesis: for X being ManySortedSet of the carrier of S for s being SortSymbol of S holds ( ( x in X . s & x in Y . s ) iff root-tree [x,s] in ((Reverse Y) "" X) . s ) let X be ManySortedSet of the carrier of S; ::_thesis: for s being SortSymbol of S holds ( ( x in X . s & x in Y . s ) iff root-tree [x,s] in ((Reverse Y) "" X) . s ) let s be SortSymbol of S; ::_thesis: ( ( x in X . s & x in Y . s ) iff root-tree [x,s] in ((Reverse Y) "" X) . s ) A1: (Reverse Y) . s = Reverse (s,Y) by MSAFREE:def_18; A2: dom (Reverse (s,Y)) = FreeGen (s,Y) by FUNCT_2:def_1; hereby ::_thesis: ( root-tree [x,s] in ((Reverse Y) "" X) . s implies ( x in X . s & x in Y . s ) ) assume that A3: x in X . s and A4: x in Y . s ; ::_thesis: root-tree [x,s] in ((Reverse Y) "" X) . s A5: root-tree [x,s] in FreeGen (s,Y) by A4, MSAFREE:def_15; [x,s] in the carrier of (DTConMSA Y) by A4, Th2; then ((Reverse Y) . s) . (root-tree [x,s]) = [x,s] `1 by A1, A5, MSAFREE:def_17 .= x ; then root-tree [x,s] in ((Reverse Y) . s) " (X . s) by A1, A2, A3, A5, FUNCT_1:def_7; hence root-tree [x,s] in ((Reverse Y) "" X) . s by EQUATION:def_1; ::_thesis: verum end; assume root-tree [x,s] in ((Reverse Y) "" X) . s ; ::_thesis: ( x in X . s & x in Y . s ) then A6: root-tree [x,s] in ((Reverse Y) . s) " (X . s) by EQUATION:def_1; then A7: (Reverse (s,Y)) . (root-tree [x,s]) in X . s by A1, FUNCT_1:def_7; A8: root-tree [x,s] in FreeGen (s,Y) by A1, A2, A6, FUNCT_1:def_7; then consider z being set such that A9: z in Y . s and A10: root-tree [x,s] = root-tree [z,s] by MSAFREE:def_15; A11: [x,s] = [z,s] by A10, TREES_4:4; then [x,s] in the carrier of (DTConMSA Y) by A9, Th2; then [x,s] `1 in X . s by A8, A7, MSAFREE:def_17; hence ( x in X . s & x in Y . s ) by A9, A11, MCART_1:7; ::_thesis: verum end; theorem Th4: :: MSAFREE3:4 for x being set for S being non void Signature for X being ManySortedSet of the carrier of S for s being SortSymbol of S st x in X . s holds root-tree [x,s] in the Sorts of (Free (S,X)) . s proof let x be set ; ::_thesis: for S being non void Signature for X being ManySortedSet of the carrier of S for s being SortSymbol of S st x in X . s holds root-tree [x,s] in the Sorts of (Free (S,X)) . s let S be non void Signature; ::_thesis: for X being ManySortedSet of the carrier of S for s being SortSymbol of S st x in X . s holds root-tree [x,s] in the Sorts of (Free (S,X)) . s let X be ManySortedSet of the carrier of S; ::_thesis: for s being SortSymbol of S st x in X . s holds root-tree [x,s] in the Sorts of (Free (S,X)) . s let s be SortSymbol of S; ::_thesis: ( x in X . s implies root-tree [x,s] in the Sorts of (Free (S,X)) . s ) assume A1: x in X . s ; ::_thesis: root-tree [x,s] in the Sorts of (Free (S,X)) . s set Y = X \/ ( the carrier of S --> {0}); consider A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) such that A2: Free (S,X) = GenMSAlg A and A3: A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X by Def1; A is MSSubset of (Free (S,X)) by A2, MSUALG_2:def_17; then A c= the Sorts of (Free (S,X)) by PBOOLE:def_18; then A4: A . s c= the Sorts of (Free (S,X)) . s by PBOOLE:def_2; X c= X \/ ( the carrier of S --> {0}) by PBOOLE:14; then X . s c= (X \/ ( the carrier of S --> {0})) . s by PBOOLE:def_2; then root-tree [x,s] in A . s by A1, A3, Th3; hence root-tree [x,s] in the Sorts of (Free (S,X)) . s by A4; ::_thesis: verum end; theorem Th5: :: MSAFREE3:5 for S being non void Signature for X being ManySortedSet of the carrier of S for o being OperSymbol of S st the_arity_of o = {} holds root-tree [o, the carrier of S] in the Sorts of (Free (S,X)) . (the_result_sort_of o) proof let S be non void Signature; ::_thesis: for X being ManySortedSet of the carrier of S for o being OperSymbol of S st the_arity_of o = {} holds root-tree [o, the carrier of S] in the Sorts of (Free (S,X)) . (the_result_sort_of o) let X be ManySortedSet of the carrier of S; ::_thesis: for o being OperSymbol of S st the_arity_of o = {} holds root-tree [o, the carrier of S] in the Sorts of (Free (S,X)) . (the_result_sort_of o) let o be OperSymbol of S; ::_thesis: ( the_arity_of o = {} implies root-tree [o, the carrier of S] in the Sorts of (Free (S,X)) . (the_result_sort_of o) ) assume A1: the_arity_of o = {} ; ::_thesis: root-tree [o, the carrier of S] in the Sorts of (Free (S,X)) . (the_result_sort_of o) set Y = X \/ ( the carrier of S --> {0}); A2: Args (o,(FreeMSA (X \/ ( the carrier of S --> {0})))) = (( the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) #) * the Arity of S) . o by MSUALG_1:def_4 .= ( the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) #) . ( the Arity of S . o) by FUNCT_2:15 .= ( the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) #) . (<*> the carrier of S) by A1, MSUALG_1:def_1 .= {{}} by PRE_CIRC:2 ; then A3: dom (Den (o,(FreeMSA (X \/ ( the carrier of S --> {0}))))) c= {{}} ; A4: ex A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st ( Free (S,X) = GenMSAlg A & A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X ) by Def1; then reconsider FX = the Sorts of (Free (S,X)) as MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) by MSUALG_2:def_9; ((FX #) * the Arity of S) . o = (FX #) . ( the Arity of S . o) by FUNCT_2:15 .= (FX #) . (<*> the carrier of S) by A1, MSUALG_1:def_1 .= {{}} by PRE_CIRC:2 ; then A5: (Den (o,(FreeMSA (X \/ ( the carrier of S --> {0}))))) | (((FX #) * the Arity of S) . o) = Den (o,(FreeMSA (X \/ ( the carrier of S --> {0})))) by A3, RELAT_1:68; set a = the ArgumentSeq of Sym (o,(X \/ ( the carrier of S --> {0}))); reconsider a = the ArgumentSeq of Sym (o,(X \/ ( the carrier of S --> {0}))) as Element of Args (o,(FreeMSA (X \/ ( the carrier of S --> {0})))) by INSTALG1:1; a = {} by A2, TARSKI:def_1; then root-tree [o, the carrier of S] = [o, the carrier of S] -tree a by TREES_4:20; then (Den (o,(FreeMSA (X \/ ( the carrier of S --> {0}))))) . a = root-tree [o, the carrier of S] by INSTALG1:3; then A6: root-tree [o, the carrier of S] in rng (Den (o,(FreeMSA (X \/ ( the carrier of S --> {0}))))) by FUNCT_2:4; FX is opers_closed by A4, MSUALG_2:def_9; then FX is_closed_on o by MSUALG_2:def_6; then A7: rng ((Den (o,(FreeMSA (X \/ ( the carrier of S --> {0}))))) | (((FX #) * the Arity of S) . o)) c= (FX * the ResultSort of S) . o by MSUALG_2:def_5; (FX * the ResultSort of S) . o = FX . ( the ResultSort of S . o) by FUNCT_2:15 .= FX . (the_result_sort_of o) by MSUALG_1:def_2 ; hence root-tree [o, the carrier of S] in the Sorts of (Free (S,X)) . (the_result_sort_of o) by A7, A5, A6; ::_thesis: verum end; registration let S be non void Signature; let X be V9() ManySortedSet of the carrier of S; cluster Free (S,X) -> strict non empty ; coherence not Free (S,X) is empty proof consider s being set such that A1: s in the carrier of S and A2: not X . s is empty by PBOOLE:def_12; reconsider s = s as SortSymbol of S by A1; set x = the Element of X . s; root-tree [ the Element of X . s,s] in the Sorts of (Free (S,X)) . s by A2, Th4; hence the Sorts of (Free (S,X)) is V9() ; :: according to CATALG_1:def_2 ::_thesis: verum end; end; theorem :: MSAFREE3:6 for x being set for S being non void Signature for X being V8() ManySortedSet of the carrier of S holds ( x is Element of (FreeMSA X) iff x is Term of S,X ) proof let x be set ; ::_thesis: for S being non void Signature for X being V8() ManySortedSet of the carrier of S holds ( x is Element of (FreeMSA X) iff x is Term of S,X ) let S be non void Signature; ::_thesis: for X being V8() ManySortedSet of the carrier of S holds ( x is Element of (FreeMSA X) iff x is Term of S,X ) let X be V8() ManySortedSet of the carrier of S; ::_thesis: ( x is Element of (FreeMSA X) iff x is Term of S,X ) A1: S -Terms X = TS (DTConMSA X) by MSATERM:def_1 .= union (rng (FreeSort X)) by MSAFREE:11 .= Union (FreeSort X) by CARD_3:def_4 ; FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def_14; hence ( x is Element of (FreeMSA X) iff x is Term of S,X ) by A1; ::_thesis: verum end; theorem Th7: :: MSAFREE3:7 for S being non void Signature for X being V8() ManySortedSet of the carrier of S for s being SortSymbol of S for x being Term of S,X holds ( x in the Sorts of (FreeMSA X) . s iff the_sort_of x = s ) proof let S be non void Signature; ::_thesis: for X being V8() ManySortedSet of the carrier of S for s being SortSymbol of S for x being Term of S,X holds ( x in the Sorts of (FreeMSA X) . s iff the_sort_of x = s ) let X be V8() ManySortedSet of the carrier of S; ::_thesis: for s being SortSymbol of S for x being Term of S,X holds ( x in the Sorts of (FreeMSA X) . s iff the_sort_of x = s ) let s be SortSymbol of S; ::_thesis: for x being Term of S,X holds ( x in the Sorts of (FreeMSA X) . s iff the_sort_of x = s ) FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def_14; then the Sorts of (FreeMSA X) . s = FreeSort (X,s) by MSAFREE:def_11; hence for x being Term of S,X holds ( x in the Sorts of (FreeMSA X) . s iff the_sort_of x = s ) by MSATERM:def_5; ::_thesis: verum end; theorem Th8: :: MSAFREE3:8 for S being non void Signature for X being V9() ManySortedSet of the carrier of S for x being Element of (Free (S,X)) holds x is Term of S,(X \/ ( the carrier of S --> {0})) proof let S be non void Signature; ::_thesis: for X being V9() ManySortedSet of the carrier of S for x being Element of (Free (S,X)) holds x is Term of S,(X \/ ( the carrier of S --> {0})) let X be V9() ManySortedSet of the carrier of S; ::_thesis: for x being Element of (Free (S,X)) holds x is Term of S,(X \/ ( the carrier of S --> {0})) set Y = X \/ ( the carrier of S --> {0}); let x be Element of (Free (S,X)); ::_thesis: x is Term of S,(X \/ ( the carrier of S --> {0})) A1: S -Terms (X \/ ( the carrier of S --> {0})) = TS (DTConMSA (X \/ ( the carrier of S --> {0}))) by MSATERM:def_1 .= union (rng (FreeSort (X \/ ( the carrier of S --> {0})))) by MSAFREE:11 .= Union (FreeSort (X \/ ( the carrier of S --> {0}))) by CARD_3:def_4 ; A2: ( FreeMSA (X \/ ( the carrier of S --> {0})) = MSAlgebra(# (FreeSort (X \/ ( the carrier of S --> {0}))),(FreeOper (X \/ ( the carrier of S --> {0}))) #) & dom the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) = the carrier of S ) by MSAFREE:def_14, PARTFUN1:def_2; consider y being set such that A3: y in dom the Sorts of (Free (S,X)) and A4: x in the Sorts of (Free (S,X)) . y by CARD_5:2; ex A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st ( Free (S,X) = GenMSAlg A & A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X ) by Def1; then the Sorts of (Free (S,X)) is MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) by MSUALG_2:def_9; then the Sorts of (Free (S,X)) c= the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) by PBOOLE:def_18; then the Sorts of (Free (S,X)) . y c= the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) . y by A3, PBOOLE:def_2; hence x is Term of S,(X \/ ( the carrier of S --> {0})) by A1, A3, A4, A2, CARD_5:2; ::_thesis: verum end; registration let S be non empty non void ManySortedSign ; let X be V9() ManySortedSet of the carrier of S; cluster -> Relation-like Function-like for Element of Union the Sorts of (Free (S,X)); coherence for b1 being Element of (Free (S,X)) holds ( b1 is Relation-like & b1 is Function-like ) by Th8; end; registration let S be non empty non void ManySortedSign ; let X be V9() ManySortedSet of the carrier of S; cluster -> finite DecoratedTree-like for Element of Union the Sorts of (Free (S,X)); coherence for b1 being Element of (Free (S,X)) holds ( b1 is finite & b1 is DecoratedTree-like ) by Th8; end; registration let S be non empty non void ManySortedSign ; let X be V9() ManySortedSet of the carrier of S; cluster -> finite-branching for Element of Union the Sorts of (Free (S,X)); coherence for b1 being Element of (Free (S,X)) holds b1 is finite-branching ; end; registration cluster Relation-like Function-like DecoratedTree-like -> non empty for set ; coherence for b1 being DecoratedTree holds not b1 is empty by RELAT_1:38; end; definition let S be ManySortedSign ; let t be non empty Relation; funcS variables_in t -> ManySortedSet of the carrier of S means :Def2: :: MSAFREE3:def 2 for s being set st s in the carrier of S holds it . s = { (a `1) where a is Element of rng t : a `2 = s } ; existence ex b1 being ManySortedSet of the carrier of S st for s being set st s in the carrier of S holds b1 . s = { (a `1) where a is Element of rng t : a `2 = s } proof deffunc H1( set ) -> set = { (a `1) where a is Element of rng t : a `2 = \$1 } ; ex f being ManySortedSet of the carrier of S st for i being set st i in the carrier of S holds f . i = H1(i) from PBOOLE:sch_4(); hence ex b1 being ManySortedSet of the carrier of S st for s being set st s in the carrier of S holds b1 . s = { (a `1) where a is Element of rng t : a `2 = s } ; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedSet of the carrier of S st ( for s being set st s in the carrier of S holds b1 . s = { (a `1) where a is Element of rng t : a `2 = s } ) & ( for s being set st s in the carrier of S holds b2 . s = { (a `1) where a is Element of rng t : a `2 = s } ) holds b1 = b2 proof let V1, V2 be ManySortedSet of the carrier of S; ::_thesis: ( ( for s being set st s in the carrier of S holds V1 . s = { (a `1) where a is Element of rng t : a `2 = s } ) & ( for s being set st s in the carrier of S holds V2 . s = { (a `1) where a is Element of rng t : a `2 = s } ) implies V1 = V2 ) assume that A1: for s being set st s in the carrier of S holds V1 . s = { (a `1) where a is Element of rng t : a `2 = s } and A2: for s being set st s in the carrier of S holds V2 . s = { (a `1) where a is Element of rng t : a `2 = s } ; ::_thesis: V1 = V2 now__::_thesis:_for_s_being_set_st_s_in_the_carrier_of_S_holds_ V1_._s_=_V2_._s let s be set ; ::_thesis: ( s in the carrier of S implies V1 . s = V2 . s ) assume A3: s in the carrier of S ; ::_thesis: V1 . s = V2 . s hence V1 . s = { (a `1) where a is Element of rng t : a `2 = s } by A1 .= V2 . s by A2, A3 ; ::_thesis: verum end; hence V1 = V2 by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def2 defines variables_in MSAFREE3:def_2_:_ for S being ManySortedSign for t being non empty Relation for b3 being ManySortedSet of the carrier of S holds ( b3 = S variables_in t iff for s being set st s in the carrier of S holds b3 . s = { (a `1) where a is Element of rng t : a `2 = s } ); definition let S be ManySortedSign ; let X be ManySortedSet of the carrier of S; let t be non empty Relation; funcX variables_in t -> ManySortedSubset of X equals :: MSAFREE3:def 3 X /\ (S variables_in t); coherence X /\ (S variables_in t) is ManySortedSubset of X proof thus X /\ (S variables_in t) c= X by PBOOLE:15; :: according to PBOOLE:def_18 ::_thesis: verum end; end; :: deftheorem defines variables_in MSAFREE3:def_3_:_ for S being ManySortedSign for X being ManySortedSet of the carrier of S for t being non empty Relation holds X variables_in t = X /\ (S variables_in t); theorem Th9: :: MSAFREE3:9 for S being ManySortedSign for X being ManySortedSet of the carrier of S for t being non empty Relation for V being ManySortedSubset of X holds ( V = X variables_in t iff for s being set st s in the carrier of S holds V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s } ) proof let S be ManySortedSign ; ::_thesis: for X being ManySortedSet of the carrier of S for t being non empty Relation for V being ManySortedSubset of X holds ( V = X variables_in t iff for s being set st s in the carrier of S holds V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s } ) let X be ManySortedSet of the carrier of S; ::_thesis: for t being non empty Relation for V being ManySortedSubset of X holds ( V = X variables_in t iff for s being set st s in the carrier of S holds V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s } ) let t be non empty Relation; ::_thesis: for V being ManySortedSubset of X holds ( V = X variables_in t iff for s being set st s in the carrier of S holds V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s } ) let V be ManySortedSubset of X; ::_thesis: ( V = X variables_in t iff for s being set st s in the carrier of S holds V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s } ) hereby ::_thesis: ( ( for s being set st s in the carrier of S holds V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s } ) implies V = X variables_in t ) assume A1: V = X variables_in t ; ::_thesis: for s being set st s in the carrier of S holds V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s } let s be set ; ::_thesis: ( s in the carrier of S implies V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s } ) assume A2: s in the carrier of S ; ::_thesis: V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s } then V . s = (X . s) /\ ((S variables_in t) . s) by A1, PBOOLE:def_5; hence V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s } by A2, Def2; ::_thesis: verum end; assume A3: for s being set st s in the carrier of S holds V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s } ; ::_thesis: V = X variables_in t now__::_thesis:_for_s_being_set_st_s_in_the_carrier_of_S_holds_ V_._s_=_(X_._s)_/\_((S_variables_in_t)_._s) let s be set ; ::_thesis: ( s in the carrier of S implies V . s = (X . s) /\ ((S variables_in t) . s) ) assume A4: s in the carrier of S ; ::_thesis: V . s = (X . s) /\ ((S variables_in t) . s) hence V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s } by A3 .= (X . s) /\ ((S variables_in t) . s) by A4, Def2 ; ::_thesis: verum end; hence V = X variables_in t by PBOOLE:def_5; ::_thesis: verum end; theorem Th10: :: MSAFREE3:10 for S being ManySortedSign for s, x being set holds ( ( s in the carrier of S implies (S variables_in (root-tree [x,s])) . s = {x} ) & ( for s9 being set st ( s9 <> s or not s in the carrier of S ) holds (S variables_in (root-tree [x,s])) . s9 = {} ) ) proof let S be ManySortedSign ; ::_thesis: for s, x being set holds ( ( s in the carrier of S implies (S variables_in (root-tree [x,s])) . s = {x} ) & ( for s9 being set st ( s9 <> s or not s in the carrier of S ) holds (S variables_in (root-tree [x,s])) . s9 = {} ) ) let s, x be set ; ::_thesis: ( ( s in the carrier of S implies (S variables_in (root-tree [x,s])) . s = {x} ) & ( for s9 being set st ( s9 <> s or not s in the carrier of S ) holds (S variables_in (root-tree [x,s])) . s9 = {} ) ) reconsider t = root-tree [x,s] as DecoratedTree ; A1: [x,s] `2 = s ; t = {[{},[x,s]]} by TREES_4:6; then A2: rng t = {[x,s]} by RELAT_1:9; A3: [x,s] `1 = x ; hereby ::_thesis: for s9 being set st ( s9 <> s or not s in the carrier of S ) holds (S variables_in (root-tree [x,s])) . s9 = {} assume s in the carrier of S ; ::_thesis: (S variables_in (root-tree [x,s])) . s = {x} then A4: (S variables_in t) . s = { (a `1) where a is Element of rng t : a `2 = s } by Def2; thus (S variables_in (root-tree [x,s])) . s = {x} ::_thesis: verum proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {x} c= (S variables_in (root-tree [x,s])) . s let y be set ; ::_thesis: ( y in (S variables_in (root-tree [x,s])) . s implies y in {x} ) assume y in (S variables_in (root-tree [x,s])) . s ; ::_thesis: y in {x} then consider a being Element of rng t such that A5: y = a `1 and a `2 = s by A4; a = [x,s] by A2, TARSKI:def_1; hence y in {x} by A3, A5, TARSKI:def_1; ::_thesis: verum end; [x,s] in rng t by A2, TARSKI:def_1; then x in { (a `1) where a is Element of rng t : a `2 = s } by A3, A1; hence {x} c= (S variables_in (root-tree [x,s])) . s by A4, ZFMISC_1:31; ::_thesis: verum end; end; let s9 be set ; ::_thesis: ( ( s9 <> s or not s in the carrier of S ) implies (S variables_in (root-tree [x,s])) . s9 = {} ) assume A6: ( s9 <> s or not s in the carrier of S ) ; ::_thesis: (S variables_in (root-tree [x,s])) . s9 = {} set y = the Element of (S variables_in (root-tree [x,s])) . s9; assume A7: (S variables_in (root-tree [x,s])) . s9 <> {} ; ::_thesis: contradiction then A8: the Element of (S variables_in (root-tree [x,s])) . s9 in (S variables_in t) . s9 ; dom (S variables_in t) = the carrier of S by PARTFUN1:def_2; then A9: s9 in the carrier of S by A7, FUNCT_1:def_2; then (S variables_in t) . s9 = { (a `1) where a is Element of rng t : a `2 = s9 } by Def2; then ex a being Element of rng t st ( the Element of (S variables_in (root-tree [x,s])) . s9 = a `1 & a `2 = s9 ) by A8; hence contradiction by A2, A1, A6, A9, TARSKI:def_1; ::_thesis: verum end; theorem Th11: :: MSAFREE3:11 for x, z being set for S being ManySortedSign for s being set st s in the carrier of S holds for p being DTree-yielding FinSequence holds ( x in (S variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st ( t in rng p & x in (S variables_in t) . s ) ) proof let x, z be set ; ::_thesis: for S being ManySortedSign for s being set st s in the carrier of S holds for p being DTree-yielding FinSequence holds ( x in (S variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st ( t in rng p & x in (S variables_in t) . s ) ) let S be ManySortedSign ; ::_thesis: for s being set st s in the carrier of S holds for p being DTree-yielding FinSequence holds ( x in (S variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st ( t in rng p & x in (S variables_in t) . s ) ) let s be set ; ::_thesis: ( s in the carrier of S implies for p being DTree-yielding FinSequence holds ( x in (S variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st ( t in rng p & x in (S variables_in t) . s ) ) ) assume A1: s in the carrier of S ; ::_thesis: for p being DTree-yielding FinSequence holds ( x in (S variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st ( t in rng p & x in (S variables_in t) . s ) ) let p be DTree-yielding FinSequence; ::_thesis: ( x in (S variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st ( t in rng p & x in (S variables_in t) . s ) ) reconsider q = [z, the carrier of S] -tree p as DecoratedTree ; A2: (S variables_in q) . s = { (a `1) where a is Element of rng q : a `2 = s } by A1, Def2; A3: dom q = tree (doms p) by TREES_4:10; A4: dom (doms p) = dom p by TREES_3:37; then A5: len p = len (doms p) by FINSEQ_3:29; hereby ::_thesis: ( ex t being DecoratedTree st ( t in rng p & x in (S variables_in t) . s ) implies x in (S variables_in ([z, the carrier of S] -tree p)) . s ) assume x in (S variables_in ([z, the carrier of S] -tree p)) . s ; ::_thesis: ex t being DecoratedTree st ( t in rng p & x in (S variables_in t) . s ) then consider a being Element of rng q such that A6: x = a `1 and A7: a `2 = s by A2; consider y being set such that A8: y in dom q and A9: a = q . y by FUNCT_1:def_3; reconsider y = y as Element of dom q by A8; ( q . {} = [z, the carrier of S] & s <> the carrier of S ) by A1, TREES_4:def_4; then y <> {} by A7, A9, MCART_1:7; then consider n being Element of NAT , r being FinSequence such that A10: n < len (doms p) and A11: r in (doms p) . (n + 1) and A12: y = <*n*> ^ r by A3, TREES_3:def_15; ( 1 <= n + 1 & n + 1 <= len (doms p) ) by A10, NAT_1:11, NAT_1:13; then A13: n + 1 in dom (doms p) by FINSEQ_3:25; then reconsider t = p . (n + 1) as DecoratedTree by A4, TREES_3:24; reconsider r = r as FinSequence of NAT by A12, FINSEQ_1:36; take t = t; ::_thesis: ( t in rng p & x in (S variables_in t) . s ) thus t in rng p by A4, A13, FUNCT_1:def_3; ::_thesis: x in (S variables_in t) . s A14: (doms p) . (n + 1) = dom t by A4, A13, FUNCT_6:22; A15: t = q | <*n*> by A5, A10, TREES_4:def_4; then dom t = (dom q) | <*n*> by TREES_2:def_10; then a = t . r by A9, A11, A12, A15, A14, TREES_2:def_10; then a in rng t by A11, A14, FUNCT_1:def_3; then x in { (b `1) where b is Element of rng t : b `2 = s } by A6, A7; hence x in (S variables_in t) . s by A1, Def2; ::_thesis: verum end; given t being DecoratedTree such that A16: t in rng p and A17: x in (S variables_in t) . s ; ::_thesis: x in (S variables_in ([z, the carrier of S] -tree p)) . s consider y being set such that A18: y in dom p and A19: t = p . y by A16, FUNCT_1:def_3; reconsider y = y as Element of NAT by A18; y >= 1 by A18, FINSEQ_3:25; then consider n being Nat such that A20: y = 1 + n by NAT_1:10; reconsider n = n as Element of NAT by ORDINAL1:def_12; y <= len p by A18, FINSEQ_3:25; then A21: n < len p by A20, NAT_1:13; then A22: t = q | <*n*> by A19, A20, TREES_4:def_4; A23: ( {} in dom t & <*n*> ^ {} = <*n*> ) by FINSEQ_1:34, TREES_1:22; dom t = (doms p) . (n + 1) by A18, A19, A20, FUNCT_6:22; then <*n*> in dom q by A3, A5, A21, A23, TREES_3:def_15; then A24: rng t c= rng q by A22, TREES_2:32; x in { (b `1) where b is Element of rng t : b `2 = s } by A1, A17, Def2; then consider b being Element of rng t such that A25: ( x = b `1 & b `2 = s ) ; b in rng t ; hence x in (S variables_in ([z, the carrier of S] -tree p)) . s by A2, A25, A24; ::_thesis: verum end; theorem Th12: :: MSAFREE3:12 for S being ManySortedSign for X being ManySortedSet of the carrier of S for s, x being set holds ( ( x in X . s implies (X variables_in (root-tree [x,s])) . s = {x} ) & ( for s9 being set st ( s9 <> s or not x in X . s ) holds (X variables_in (root-tree [x,s])) . s9 = {} ) ) proof let S be ManySortedSign ; ::_thesis: for X being ManySortedSet of the carrier of S for s, x being set holds ( ( x in X . s implies (X variables_in (root-tree [x,s])) . s = {x} ) & ( for s9 being set st ( s9 <> s or not x in X . s ) holds (X variables_in (root-tree [x,s])) . s9 = {} ) ) let X be ManySortedSet of the carrier of S; ::_thesis: for s, x being set holds ( ( x in X . s implies (X variables_in (root-tree [x,s])) . s = {x} ) & ( for s9 being set st ( s9 <> s or not x in X . s ) holds (X variables_in (root-tree [x,s])) . s9 = {} ) ) let s, x be set ; ::_thesis: ( ( x in X . s implies (X variables_in (root-tree [x,s])) . s = {x} ) & ( for s9 being set st ( s9 <> s or not x in X . s ) holds (X variables_in (root-tree [x,s])) . s9 = {} ) ) reconsider t = root-tree [x,s] as DecoratedTree ; A1: ( [x,s] `1 = x & [x,s] `2 = s ) ; hereby ::_thesis: for s9 being set st ( s9 <> s or not x in X . s ) holds (X variables_in (root-tree [x,s])) . s9 = {} assume A2: x in X . s ; ::_thesis: (X variables_in (root-tree [x,s])) . s = {x} then A3: {x} c= X . s by ZFMISC_1:31; dom X = the carrier of S by PARTFUN1:def_2; then A4: s in the carrier of S by A2, FUNCT_1:def_2; then (S variables_in (root-tree [x,s])) . s = {x} by Th10; then (X . s) /\ ((S variables_in (root-tree [x,s])) . s) = {x} by A3, XBOOLE_1:28; hence (X variables_in (root-tree [x,s])) . s = {x} by A4, PBOOLE:def_5; ::_thesis: verum end; let s9 be set ; ::_thesis: ( ( s9 <> s or not x in X . s ) implies (X variables_in (root-tree [x,s])) . s9 = {} ) assume A5: ( s9 <> s or not x in X . s ) ; ::_thesis: (X variables_in (root-tree [x,s])) . s9 = {} set y = the Element of (X variables_in (root-tree [x,s])) . s9; assume A6: (X variables_in (root-tree [x,s])) . s9 <> {} ; ::_thesis: contradiction dom (X variables_in t) = the carrier of S by PARTFUN1:def_2; then s9 in the carrier of S by A6, FUNCT_1:def_2; then A7: (X variables_in t) . s9 = (X . s9) /\ { (a `1) where a is Element of rng t : a `2 = s9 } by Th9; then the Element of (X variables_in (root-tree [x,s])) . s9 in { (a `1) where a is Element of rng t : a `2 = s9 } by A6, XBOOLE_0:def_4; then consider a being Element of rng t such that A8: ( the Element of (X variables_in (root-tree [x,s])) . s9 = a `1 & a `2 = s9 ) ; t = {[{},[x,s]]} by TREES_4:6; then rng t = {[x,s]} by RELAT_1:9; then a = [x,s] by TARSKI:def_1; hence contradiction by A1, A5, A6, A7, A8, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th13: :: MSAFREE3:13 for x, z being set for S being ManySortedSign for X being ManySortedSet of the carrier of S for s being set st s in the carrier of S holds for p being DTree-yielding FinSequence holds ( x in (X variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st ( t in rng p & x in (X variables_in t) . s ) ) proof let x, z be set ; ::_thesis: for S being ManySortedSign for X being ManySortedSet of the carrier of S for s being set st s in the carrier of S holds for p being DTree-yielding FinSequence holds ( x in (X variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st ( t in rng p & x in (X variables_in t) . s ) ) let S be ManySortedSign ; ::_thesis: for X being ManySortedSet of the carrier of S for s being set st s in the carrier of S holds for p being DTree-yielding FinSequence holds ( x in (X variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st ( t in rng p & x in (X variables_in t) . s ) ) let X be ManySortedSet of the carrier of S; ::_thesis: for s being set st s in the carrier of S holds for p being DTree-yielding FinSequence holds ( x in (X variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st ( t in rng p & x in (X variables_in t) . s ) ) let s be set ; ::_thesis: ( s in the carrier of S implies for p being DTree-yielding FinSequence holds ( x in (X variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st ( t in rng p & x in (X variables_in t) . s ) ) ) assume A1: s in the carrier of S ; ::_thesis: for p being DTree-yielding FinSequence holds ( x in (X variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st ( t in rng p & x in (X variables_in t) . s ) ) let p be DTree-yielding FinSequence; ::_thesis: ( x in (X variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st ( t in rng p & x in (X variables_in t) . s ) ) reconsider q = [z, the carrier of S] -tree p as DecoratedTree ; (X variables_in q) . s = (X . s) /\ ((S variables_in q) . s) by A1, PBOOLE:def_5; then A2: ( x in (X variables_in ([z, the carrier of S] -tree p)) . s iff ( x in X . s & x in (S variables_in ([z, the carrier of S] -tree p)) . s ) ) by XBOOLE_0:def_4; then A3: ( x in (X variables_in ([z, the carrier of S] -tree p)) . s iff ( x in X . s & ex t being DecoratedTree st ( t in rng p & x in (S variables_in t) . s ) ) ) by A1, Th11; hereby ::_thesis: ( ex t being DecoratedTree st ( t in rng p & x in (X variables_in t) . s ) implies x in (X variables_in ([z, the carrier of S] -tree p)) . s ) assume x in (X variables_in ([z, the carrier of S] -tree p)) . s ; ::_thesis: ex t being DecoratedTree st ( t in rng p & x in (X variables_in t) . s ) then consider t being DecoratedTree such that A4: t in rng p and A5: ( x in X . s & x in (S variables_in t) . s ) by A3; take t = t; ::_thesis: ( t in rng p & x in (X variables_in t) . s ) thus t in rng p by A4; ::_thesis: x in (X variables_in t) . s x in (X . s) /\ ((S variables_in t) . s) by A5, XBOOLE_0:def_4; hence x in (X variables_in t) . s by A1, PBOOLE:def_5; ::_thesis: verum end; given t being DecoratedTree such that A6: t in rng p and A7: x in (X variables_in t) . s ; ::_thesis: x in (X variables_in ([z, the carrier of S] -tree p)) . s A8: (X variables_in t) . s = (X . s) /\ ((S variables_in t) . s) by A1, PBOOLE:def_5; then x in (S variables_in t) . s by A7, XBOOLE_0:def_4; hence x in (X variables_in ([z, the carrier of S] -tree p)) . s by A1, A2, A6, A7, A8, Th11, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th14: :: MSAFREE3:14 for S being non void Signature for X being V8() ManySortedSet of the carrier of S for t being Term of S,X holds S variables_in t c= X proof let S be non void Signature; ::_thesis: for X being V8() ManySortedSet of the carrier of S for t being Term of S,X holds S variables_in t c= X let X be V8() ManySortedSet of the carrier of S; ::_thesis: for t being Term of S,X holds S variables_in t c= X defpred S1[ DecoratedTree] means S variables_in \$1 c= X; A1: for o being OperSymbol of S for p being ArgumentSeq of Sym (o,X) st ( for t being Term of S,X st t in rng p holds S1[t] ) holds S1[[o, the carrier of S] -tree p] proof let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of Sym (o,X) st ( for t being Term of S,X st t in rng p holds S1[t] ) holds S1[[o, the carrier of S] -tree p] let p be ArgumentSeq of Sym (o,X); ::_thesis: ( ( for t being Term of S,X st t in rng p holds S1[t] ) implies S1[[o, the carrier of S] -tree p] ) assume A2: for t being Term of S,X st t in rng p holds S variables_in t c= X ; ::_thesis: S1[[o, the carrier of S] -tree p] set q = [o, the carrier of S] -tree p; thus S variables_in ([o, the carrier of S] -tree p) c= X ::_thesis: verum proof let s9 be set ; :: according to PBOOLE:def_2 ::_thesis: ( not s9 in the carrier of S or (S variables_in ([o, the carrier of S] -tree p)) . s9 c= X . s9 ) assume s9 in the carrier of S ; ::_thesis: (S variables_in ([o, the carrier of S] -tree p)) . s9 c= X . s9 then reconsider z = s9 as SortSymbol of S ; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (S variables_in ([o, the carrier of S] -tree p)) . s9 or x in X . s9 ) assume x in (S variables_in ([o, the carrier of S] -tree p)) . s9 ; ::_thesis: x in X . s9 then consider t being DecoratedTree such that A3: t in rng p and A4: x in (S variables_in t) . z by Th11; consider i being set such that A5: i in dom p and A6: t = p . i by A3, FUNCT_1:def_3; reconsider i = i as Nat by A5; reconsider t = p . i as Term of S,X by A5, MSATERM:22; S variables_in t c= X by A2, A3, A6; then (S variables_in t) . z c= X . z by PBOOLE:def_2; hence x in X . s9 by A4, A6; ::_thesis: verum end; end; A7: for s being SortSymbol of S for v being Element of X . s holds S1[ root-tree [v,s]] proof let s be SortSymbol of S; ::_thesis: for v being Element of X . s holds S1[ root-tree [v,s]] let v be Element of X . s; ::_thesis: S1[ root-tree [v,s]] thus S variables_in (root-tree [v,s]) c= X ::_thesis: verum proof let s9 be set ; :: according to PBOOLE:def_2 ::_thesis: ( not s9 in the carrier of S or (S variables_in (root-tree [v,s])) . s9 c= X . s9 ) assume s9 in the carrier of S ; ::_thesis: (S variables_in (root-tree [v,s])) . s9 c= X . s9 then reconsider z = s9 as SortSymbol of S ; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (S variables_in (root-tree [v,s])) . s9 or x in X . s9 ) assume A8: x in (S variables_in (root-tree [v,s])) . s9 ; ::_thesis: x in X . s9 then A9: ( s <> z implies x in {} ) by Th10; ( s = z implies x in {v} ) by A8, Th10; hence x in X . s9 by A9; ::_thesis: verum end; end; for t being Term of S,X holds S1[t] from MSATERM:sch_1(A7, A1); hence for t being Term of S,X holds S variables_in t c= X ; ::_thesis: verum end; definition let S be non void Signature; let X be V8() ManySortedSet of the carrier of S; let t be Term of S,X; func variables_in t -> ManySortedSubset of X equals :: MSAFREE3:def 4 S variables_in t; correctness coherence S variables_in t is ManySortedSubset of X; proof S variables_in t c= X by Th14; then S variables_in t = X variables_in t by PBOOLE:23; hence S variables_in t is ManySortedSubset of X ; ::_thesis: verum end; end; :: deftheorem defines variables_in MSAFREE3:def_4_:_ for S being non void Signature for X being V8() ManySortedSet of the carrier of S for t being Term of S,X holds variables_in t = S variables_in t; theorem Th15: :: MSAFREE3:15 for S being non void Signature for X being V8() ManySortedSet of the carrier of S for t being Term of S,X holds variables_in t = X variables_in t by Th14, PBOOLE:23; definition let S be non void Signature; let Y be V8() ManySortedSet of the carrier of S; let X be ManySortedSet of the carrier of S; funcS -Terms (X,Y) -> MSSubset of (FreeMSA Y) means :Def5: :: MSAFREE3:def 5 for s being SortSymbol of S holds it . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } ; existence ex b1 being MSSubset of (FreeMSA Y) st for s being SortSymbol of S holds b1 . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } proof deffunc H1( SortSymbol of S) -> set = { t where t is Term of S,Y : ( the_sort_of t = \$1 & variables_in t c= X ) } ; consider T being ManySortedSet of the carrier of S such that A1: for s being SortSymbol of S holds T . s = H1(s) from PBOOLE:sch_5(); T c= the Sorts of (FreeMSA Y) proof let s be set ; :: according to PBOOLE:def_2 ::_thesis: ( not s in the carrier of S or T . s c= the Sorts of (FreeMSA Y) . s ) assume s in the carrier of S ; ::_thesis: T . s c= the Sorts of (FreeMSA Y) . s then reconsider s9 = s as SortSymbol of S ; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T . s or x in the Sorts of (FreeMSA Y) . s ) assume A2: x in T . s ; ::_thesis: x in the Sorts of (FreeMSA Y) . s T . s9 = { t where t is Term of S,Y : ( the_sort_of t = s9 & variables_in t c= X ) } by A1; then ex t being Term of S,Y st ( x = t & the_sort_of t = s9 & variables_in t c= X ) by A2; hence x in the Sorts of (FreeMSA Y) . s by Th7; ::_thesis: verum end; then reconsider T = T as MSSubset of (FreeMSA Y) by PBOOLE:def_18; take T ; ::_thesis: for s being SortSymbol of S holds T . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } thus for s being SortSymbol of S holds T . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } by A1; ::_thesis: verum end; correctness uniqueness for b1, b2 being MSSubset of (FreeMSA Y) st ( for s being SortSymbol of S holds b1 . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } ) & ( for s being SortSymbol of S holds b2 . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } ) holds b1 = b2; proof let T1, T2 be MSSubset of (FreeMSA Y); ::_thesis: ( ( for s being SortSymbol of S holds T1 . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } ) & ( for s being SortSymbol of S holds T2 . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } ) implies T1 = T2 ) assume that A3: for s being SortSymbol of S holds T1 . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } and A4: for s being SortSymbol of S holds T2 . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } ; ::_thesis: T1 = T2 now__::_thesis:_for_s_being_set_st_s_in_the_carrier_of_S_holds_ T1_._s_=_T2_._s let s be set ; ::_thesis: ( s in the carrier of S implies T1 . s = T2 . s ) assume A5: s in the carrier of S ; ::_thesis: T1 . s = T2 . s hence T1 . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } by A3 .= T2 . s by A4, A5 ; ::_thesis: verum end; hence T1 = T2 by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def5 defines -Terms MSAFREE3:def_5_:_ for S being non void Signature for Y being V8() ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S for b4 being MSSubset of (FreeMSA Y) holds ( b4 = S -Terms (X,Y) iff for s being SortSymbol of S holds b4 . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } ); theorem Th16: :: MSAFREE3:16 for x being set for S being non void Signature for Y being V8() ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S for s being SortSymbol of S st x in (S -Terms (X,Y)) . s holds x is Term of S,Y proof let x be set ; ::_thesis: for S being non void Signature for Y being V8() ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S for s being SortSymbol of S st x in (S -Terms (X,Y)) . s holds x is Term of S,Y let S be non void Signature; ::_thesis: for Y being V8() ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S for s being SortSymbol of S st x in (S -Terms (X,Y)) . s holds x is Term of S,Y let Y be V8() ManySortedSet of the carrier of S; ::_thesis: for X being ManySortedSet of the carrier of S for s being SortSymbol of S st x in (S -Terms (X,Y)) . s holds x is Term of S,Y let X be ManySortedSet of the carrier of S; ::_thesis: for s being SortSymbol of S st x in (S -Terms (X,Y)) . s holds x is Term of S,Y let s be SortSymbol of S; ::_thesis: ( x in (S -Terms (X,Y)) . s implies x is Term of S,Y ) assume x in (S -Terms (X,Y)) . s ; ::_thesis: x is Term of S,Y then x in { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } by Def5; then ex t being Term of S,Y st ( x = t & the_sort_of t = s & variables_in t c= X ) ; hence x is Term of S,Y ; ::_thesis: verum end; theorem Th17: :: MSAFREE3:17 for S being non void Signature for Y being V8() ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S for t being Term of S,Y for s being SortSymbol of S st t in (S -Terms (X,Y)) . s holds ( the_sort_of t = s & variables_in t c= X ) proof let S be non void Signature; ::_thesis: for Y being V8() ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S for t being Term of S,Y for s being SortSymbol of S st t in (S -Terms (X,Y)) . s holds ( the_sort_of t = s & variables_in t c= X ) let Y be V8() ManySortedSet of the carrier of S; ::_thesis: for X being ManySortedSet of the carrier of S for t being Term of S,Y for s being SortSymbol of S st t in (S -Terms (X,Y)) . s holds ( the_sort_of t = s & variables_in t c= X ) let X be ManySortedSet of the carrier of S; ::_thesis: for t being Term of S,Y for s being SortSymbol of S st t in (S -Terms (X,Y)) . s holds ( the_sort_of t = s & variables_in t c= X ) let q be Term of S,Y; ::_thesis: for s being SortSymbol of S st q in (S -Terms (X,Y)) . s holds ( the_sort_of q = s & variables_in q c= X ) let s be SortSymbol of S; ::_thesis: ( q in (S -Terms (X,Y)) . s implies ( the_sort_of q = s & variables_in q c= X ) ) assume A1: q in (S -Terms (X,Y)) . s ; ::_thesis: ( the_sort_of q = s & variables_in q c= X ) (S -Terms (X,Y)) . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } by Def5; then ex t being Term of S,Y st ( q = t & the_sort_of t = s & variables_in t c= X ) by A1; hence ( the_sort_of q = s & variables_in q c= X ) ; ::_thesis: verum end; theorem Th18: :: MSAFREE3:18 for x being set for S being non void Signature for Y being V8() ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S for s being SortSymbol of S holds ( root-tree [x,s] in (S -Terms (X,Y)) . s iff ( x in X . s & x in Y . s ) ) proof let x be set ; ::_thesis: for S being non void Signature for Y being V8() ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S for s being SortSymbol of S holds ( root-tree [x,s] in (S -Terms (X,Y)) . s iff ( x in X . s & x in Y . s ) ) let S be non void Signature; ::_thesis: for Y being V8() ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S for s being SortSymbol of S holds ( root-tree [x,s] in (S -Terms (X,Y)) . s iff ( x in X . s & x in Y . s ) ) let Y be V8() ManySortedSet of the carrier of S; ::_thesis: for X being ManySortedSet of the carrier of S for s being SortSymbol of S holds ( root-tree [x,s] in (S -Terms (X,Y)) . s iff ( x in X . s & x in Y . s ) ) let X be ManySortedSet of the carrier of S; ::_thesis: for s being SortSymbol of S holds ( root-tree [x,s] in (S -Terms (X,Y)) . s iff ( x in X . s & x in Y . s ) ) let s be SortSymbol of S; ::_thesis: ( root-tree [x,s] in (S -Terms (X,Y)) . s iff ( x in X . s & x in Y . s ) ) A1: (S -Terms (X,Y)) . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } by Def5; hereby ::_thesis: ( x in X . s & x in Y . s implies root-tree [x,s] in (S -Terms (X,Y)) . s ) assume root-tree [x,s] in (S -Terms (X,Y)) . s ; ::_thesis: ( x in X . s & x in Y . s ) then consider t being Term of S,Y such that A2: root-tree [x,s] = t and the_sort_of t = s and A3: variables_in t c= X by A1; A4: t . {} = [x,s] by A2, TREES_4:3; s in the carrier of S ; then s <> the carrier of S ; then not s in { the carrier of S} by TARSKI:def_1; then not t . {} in [: the carrier' of S,{ the carrier of S}:] by A4, ZFMISC_1:87; then consider s9 being SortSymbol of S, v being Element of Y . s9 such that A5: t . {} = [v,s9] by MSATERM:2; A6: ( s = s9 & x = v ) by A4, A5, XTUPLE_0:1; ( (S variables_in t) . s = {x} & (variables_in t) . s c= X . s ) by A2, A3, Th10, PBOOLE:def_2; hence ( x in X . s & x in Y . s ) by A6, ZFMISC_1:31; ::_thesis: verum end; assume that A7: x in X . s and A8: x in Y . s ; ::_thesis: root-tree [x,s] in (S -Terms (X,Y)) . s reconsider t = root-tree [x,s] as Term of S,Y by A8, MSATERM:4; A9: variables_in t c= X proof let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S or (variables_in t) . i c= X . i ) assume i in the carrier of S ; ::_thesis: (variables_in t) . i c= X . i A10: (S variables_in t) . s = {x} by Th10; ( i <> s implies (S variables_in t) . i = {} ) by Th10; hence (variables_in t) . i c= X . i by A7, A10, XBOOLE_1:2, ZFMISC_1:31; ::_thesis: verum end; the_sort_of t = s by A8, MSATERM:14; hence root-tree [x,s] in (S -Terms (X,Y)) . s by A1, A9; ::_thesis: verum end; theorem Th19: :: MSAFREE3:19 for S being non void Signature for Y being V8() ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S for o being OperSymbol of S for p being ArgumentSeq of Sym (o,Y) holds ( (Sym (o,Y)) -tree p in (S -Terms (X,Y)) . (the_result_sort_of o) iff rng p c= Union (S -Terms (X,Y)) ) proof let S be non void Signature; ::_thesis: for Y being V8() ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S for o being OperSymbol of S for p being ArgumentSeq of Sym (o,Y) holds ( (Sym (o,Y)) -tree p in (S -Terms (X,Y)) . (the_result_sort_of o) iff rng p c= Union (S -Terms (X,Y)) ) let Y be V8() ManySortedSet of the carrier of S; ::_thesis: for X being ManySortedSet of the carrier of S for o being OperSymbol of S for p being ArgumentSeq of Sym (o,Y) holds ( (Sym (o,Y)) -tree p in (S -Terms (X,Y)) . (the_result_sort_of o) iff rng p c= Union (S -Terms (X,Y)) ) let X be ManySortedSet of the carrier of S; ::_thesis: for o being OperSymbol of S for p being ArgumentSeq of Sym (o,Y) holds ( (Sym (o,Y)) -tree p in (S -Terms (X,Y)) . (the_result_sort_of o) iff rng p c= Union (S -Terms (X,Y)) ) let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of Sym (o,Y) holds ( (Sym (o,Y)) -tree p in (S -Terms (X,Y)) . (the_result_sort_of o) iff rng p c= Union (S -Terms (X,Y)) ) let p be ArgumentSeq of Sym (o,Y); ::_thesis: ( (Sym (o,Y)) -tree p in (S -Terms (X,Y)) . (the_result_sort_of o) iff rng p c= Union (S -Terms (X,Y)) ) set s = the_result_sort_of o; A1: dom (S -Terms (X,Y)) = the carrier of S by PARTFUN1:def_2; A2: Sym (o,Y) = [o, the carrier of S] by MSAFREE:def_9; A3: (S -Terms (X,Y)) . (the_result_sort_of o) = { t where t is Term of S,Y : ( the_sort_of t = the_result_sort_of o & variables_in t c= X ) } by Def5; hereby ::_thesis: ( rng p c= Union (S -Terms (X,Y)) implies (Sym (o,Y)) -tree p in (S -Terms (X,Y)) . (the_result_sort_of o) ) assume (Sym (o,Y)) -tree p in (S -Terms (X,Y)) . (the_result_sort_of o) ; ::_thesis: rng p c= Union (S -Terms (X,Y)) then consider t being Term of S,Y such that A4: [o, the carrier of S] -tree p = t and the_sort_of t = the_result_sort_of o and A5: variables_in t c= X by A3, A2; thus rng p c= Union (S -Terms (X,Y)) ::_thesis: verum proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng p or y in Union (S -Terms (X,Y)) ) assume A6: y in rng p ; ::_thesis: y in Union (S -Terms (X,Y)) then consider x being set such that A7: x in dom p and A8: y = p . x by FUNCT_1:def_3; reconsider x = x as Nat by A7; reconsider q = p . x as Term of S,Y by A7, MSATERM:22; A9: variables_in q c= X proof let z be set ; :: according to PBOOLE:def_2 ::_thesis: ( not z in the carrier of S or (variables_in q) . z c= X . z ) assume A10: z in the carrier of S ; ::_thesis: (variables_in q) . z c= X . z let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (variables_in q) . z or a in X . z ) assume a in (variables_in q) . z ; ::_thesis: a in X . z then A11: a in (variables_in t) . z by A4, A6, A8, A10, Th11; (variables_in t) . z c= X . z by A5, A10, PBOOLE:def_2; hence a in X . z by A11; ::_thesis: verum end; set sq = the_sort_of q; (S -Terms (X,Y)) . (the_sort_of q) = { t9 where t9 is Term of S,Y : ( the_sort_of t9 = the_sort_of q & variables_in t9 c= X ) } by Def5; then q in (S -Terms (X,Y)) . (the_sort_of q) by A9; hence y in Union (S -Terms (X,Y)) by A1, A8, CARD_5:2; ::_thesis: verum end; end; set t = (Sym (o,Y)) -tree p; assume A12: rng p c= Union (S -Terms (X,Y)) ; ::_thesis: (Sym (o,Y)) -tree p in (S -Terms (X,Y)) . (the_result_sort_of o) A13: variables_in ((Sym (o,Y)) -tree p) c= X proof let z be set ; :: according to PBOOLE:def_2 ::_thesis: ( not z in the carrier of S or (variables_in ((Sym (o,Y)) -tree p)) . z c= X . z ) assume A14: z in the carrier of S ; ::_thesis: (variables_in ((Sym (o,Y)) -tree p)) . z c= X . z let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (variables_in ((Sym (o,Y)) -tree p)) . z or x in X . z ) assume x in (variables_in ((Sym (o,Y)) -tree p)) . z ; ::_thesis: x in X . z then consider q being DecoratedTree such that A15: q in rng p and A16: x in (S variables_in q) . z by A2, A14, Th11; consider y being set such that A17: y in the carrier of S and A18: q in (S -Terms (X,Y)) . y by A1, A12, A15, CARD_5:2; (S -Terms (X,Y)) . y = { t9 where t9 is Term of S,Y : ( the_sort_of t9 = y & variables_in t9 c= X ) } by A17, Def5; then consider t9 being Term of S,Y such that A19: q = t9 and the_sort_of t9 = y and A20: variables_in t9 c= X by A18; (variables_in t9) . z c= X . z by A14, A20, PBOOLE:def_2; hence x in X . z by A16, A19; ::_thesis: verum end; the_sort_of ((Sym (o,Y)) -tree p) = the_result_sort_of o by MSATERM:20; hence (Sym (o,Y)) -tree p in (S -Terms (X,Y)) . (the_result_sort_of o) by A3, A13; ::_thesis: verum end; theorem Th20: :: MSAFREE3:20 for S being non void Signature for X being V8() ManySortedSet of the carrier of S for A being MSSubset of (FreeMSA X) holds ( A is opers_closed iff for o being OperSymbol of S for p being ArgumentSeq of Sym (o,X) st rng p c= Union A holds (Sym (o,X)) -tree p in A . (the_result_sort_of o) ) proof let S be non void Signature; ::_thesis: for X being V8() ManySortedSet of the carrier of S for A being MSSubset of (FreeMSA X) holds ( A is opers_closed iff for o being OperSymbol of S for p being ArgumentSeq of Sym (o,X) st rng p c= Union A holds (Sym (o,X)) -tree p in A . (the_result_sort_of o) ) let X be V8() ManySortedSet of the carrier of S; ::_thesis: for A being MSSubset of (FreeMSA X) holds ( A is opers_closed iff for o being OperSymbol of S for p being ArgumentSeq of Sym (o,X) st rng p c= Union A holds (Sym (o,X)) -tree p in A . (the_result_sort_of o) ) set A = FreeMSA X; let T be MSSubset of (FreeMSA X); ::_thesis: ( T is opers_closed iff for o being OperSymbol of S for p being ArgumentSeq of Sym (o,X) st rng p c= Union T holds (Sym (o,X)) -tree p in T . (the_result_sort_of o) ) hereby ::_thesis: ( ( for o being OperSymbol of S for p being ArgumentSeq of Sym (o,X) st rng p c= Union T holds (Sym (o,X)) -tree p in T . (the_result_sort_of o) ) implies T is opers_closed ) assume A1: T is opers_closed ; ::_thesis: for o being OperSymbol of S for p being ArgumentSeq of Sym (o,X) st rng p c= Union T holds (Sym (o,X)) -tree p in T . (the_result_sort_of o) let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of Sym (o,X) st rng p c= Union T holds (Sym (o,X)) -tree p in T . (the_result_sort_of o) let p be ArgumentSeq of Sym (o,X); ::_thesis: ( rng p c= Union T implies (Sym (o,X)) -tree p in T . (the_result_sort_of o) ) T is_closed_on o by A1, MSUALG_2:def_6; then A2: rng ((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o)) c= (T * the ResultSort of S) . o by MSUALG_2:def_5; A3: p is Element of Args (o,(FreeMSA X)) by INSTALG1:1; A4: dom p = dom (the_arity_of o) by MSATERM:22; A5: dom T = the carrier of S by PARTFUN1:def_2; assume A6: rng p c= Union T ; ::_thesis: (Sym (o,X)) -tree p in T . (the_result_sort_of o) A7: now__::_thesis:_for_x_being_set_st_x_in_dom_(the_arity_of_o)_holds_ p_._x_in_(T_*_(the_arity_of_o))_._x let x be set ; ::_thesis: ( x in dom (the_arity_of o) implies p . x in (T * (the_arity_of o)) . x ) assume A8: x in dom (the_arity_of o) ; ::_thesis: p . x in (T * (the_arity_of o)) . x then reconsider i = x as Nat ; reconsider t = p . i as Term of S,X by A4, A8, MSATERM:22; A9: ( the_sort_of t = (the_arity_of o) . x & (T * (the_arity_of o)) . x = T . ((the_arity_of o) . x) ) by A4, A8, FUNCT_1:13, MSATERM:23; p . x in rng p by A4, A8, FUNCT_1:def_3; then consider y being set such that A10: y in dom T and A11: p . x in T . y by A6, CARD_5:2; T c= the Sorts of (FreeMSA X) by PBOOLE:def_18; then T . y c= the Sorts of (FreeMSA X) . y by A10, PBOOLE:def_2; hence p . x in (T * (the_arity_of o)) . x by A10, A11, A9, Th7; ::_thesis: verum end; rng (the_arity_of o) c= dom T by A5; then dom (T * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27; then A12: p in product (T * (the_arity_of o)) by A4, A7, CARD_3:9; A13: ((T #) * the Arity of S) . o = (T #) . ( the Arity of S . o) by FUNCT_2:15 .= (T #) . (the_arity_of o) by MSUALG_1:def_1 .= product (T * (the_arity_of o)) by FINSEQ_2:def_5 ; then A14: ((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o)) . p = (Den (o,(FreeMSA X))) . p by A12, FUNCT_1:49; dom (Den (o,(FreeMSA X))) = Args (o,(FreeMSA X)) by FUNCT_2:def_1; then p in dom ((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o)) by A13, A3, A12, RELAT_1:57; then A15: (Den (o,(FreeMSA X))) . p in rng ((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o)) by A14, FUNCT_1:def_3; (T * the ResultSort of S) . o = T . ( the ResultSort of S . o) by FUNCT_2:15 .= T . (the_result_sort_of o) by MSUALG_1:def_2 ; then ( [o, the carrier of S] = Sym (o,X) & (Den (o,(FreeMSA X))) . p in T . (the_result_sort_of o) ) by A2, A15, MSAFREE:def_9; hence (Sym (o,X)) -tree p in T . (the_result_sort_of o) by A3, INSTALG1:3; ::_thesis: verum end; assume A16: for o being OperSymbol of S for p being ArgumentSeq of Sym (o,X) st rng p c= Union T holds (Sym (o,X)) -tree p in T . (the_result_sort_of o) ; ::_thesis: T is opers_closed let o be OperSymbol of S; :: according to MSUALG_2:def_6 ::_thesis: T is_closed_on o let x be set ; :: according to TARSKI:def_3,MSUALG_2:def_5 ::_thesis: ( not x in proj2 ((Den (o,(FreeMSA X))) | (( the Arity of S * (T #)) . o)) or x in ( the ResultSort of S * T) . o ) A17: (T * the ResultSort of S) . o = T . ( the ResultSort of S . o) by FUNCT_2:15 .= T . (the_result_sort_of o) by MSUALG_1:def_2 ; assume x in rng ((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o)) ; ::_thesis: x in ( the ResultSort of S * T) . o then consider y being set such that A18: y in dom ((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o)) and A19: x = ((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o)) . y by FUNCT_1:def_3; y in dom (Den (o,(FreeMSA X))) by A18, RELAT_1:57; then reconsider y = y as Element of Args (o,(FreeMSA X)) ; reconsider p = y as ArgumentSeq of Sym (o,X) by INSTALG1:1; A20: ((T #) * the Arity of S) . o = (T #) . ( the Arity of S . o) by FUNCT_2:15 .= (T #) . (the_arity_of o) by MSUALG_1:def_1 .= product (T * (the_arity_of o)) by FINSEQ_2:def_5 ; A21: rng p c= Union T proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng p or z in Union T ) A22: dom T = the carrier of S by PARTFUN1:def_2; assume z in rng p ; ::_thesis: z in Union T then consider a being set such that A23: a in dom p and A24: z = p . a by FUNCT_1:def_3; A25: dom p = dom (T * (the_arity_of o)) by A18, A20, CARD_3:9; then A26: ( z in (T * (the_arity_of o)) . a & (T * (the_arity_of o)) . a = T . ((the_arity_of o) . a) ) by A18, A20, A23, A24, CARD_3:9, FUNCT_1:12; rng (the_arity_of o) c= the carrier of S ; then dom (T * (the_arity_of o)) = dom (the_arity_of o) by A22, RELAT_1:27; then (the_arity_of o) . a in rng (the_arity_of o) by A23, A25, FUNCT_1:def_3; hence z in Union T by A22, A26, CARD_5:2; ::_thesis: verum end; x = (Den (o,(FreeMSA X))) . y by A18, A19, FUNCT_1:47 .= [o, the carrier of S] -tree y by INSTALG1:3 .= (Sym (o,X)) -tree p by MSAFREE:def_9 ; hence x in ( the ResultSort of S * T) . o by A16, A17, A21; ::_thesis: verum end; theorem Th21: :: MSAFREE3:21 for S being non void Signature for Y being V8() ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S holds S -Terms (X,Y) is opers_closed proof let S be non void Signature; ::_thesis: for Y being V8() ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S holds S -Terms (X,Y) is opers_closed let Y be V8() ManySortedSet of the carrier of S; ::_thesis: for X being ManySortedSet of the carrier of S holds S -Terms (X,Y) is opers_closed let X be ManySortedSet of the carrier of S; ::_thesis: S -Terms (X,Y) is opers_closed for o being OperSymbol of S for p being ArgumentSeq of Sym (o,Y) st rng p c= Union (S -Terms (X,Y)) holds (Sym (o,Y)) -tree p in (S -Terms (X,Y)) . (the_result_sort_of o) by Th19; hence S -Terms (X,Y) is opers_closed by Th20; ::_thesis: verum end; theorem Th22: :: MSAFREE3:22 for S being non void Signature for Y being V8() ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S holds (Reverse Y) "" X c= S -Terms (X,Y) proof let S be non void Signature; ::_thesis: for Y being V8() ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S holds (Reverse Y) "" X c= S -Terms (X,Y) let Y be V8() ManySortedSet of the carrier of S; ::_thesis: for X being ManySortedSet of the carrier of S holds (Reverse Y) "" X c= S -Terms (X,Y) let X be ManySortedSet of the carrier of S; ::_thesis: (Reverse Y) "" X c= S -Terms (X,Y) let s be set ; :: according to PBOOLE:def_2 ::_thesis: ( not s in the carrier of S or ((Reverse Y) "" X) . s c= (S -Terms (X,Y)) . s ) assume s in the carrier of S ; ::_thesis: ((Reverse Y) "" X) . s c= (S -Terms (X,Y)) . s then reconsider s9 = s as SortSymbol of S ; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((Reverse Y) "" X) . s or x in (S -Terms (X,Y)) . s ) assume x in ((Reverse Y) "" X) . s ; ::_thesis: x in (S -Terms (X,Y)) . s then A1: x in ((Reverse Y) . s9) " (X . s9) by EQUATION:def_1; then A2: x in dom ((Reverse Y) . s) by FUNCT_1:def_7; A3: ((Reverse Y) . s) . x in X . s by A1, FUNCT_1:def_7; A4: (Reverse Y) . s = Reverse (s9,Y) by MSAFREE:def_18; then A5: dom ((Reverse Y) . s) = FreeGen (s9,Y) by FUNCT_2:def_1; then consider b being set such that A6: b in Y . s9 and A7: x = root-tree [b,s9] by A2, MSAFREE:def_15; FreeGen (s9,Y) = { (root-tree t) where t is Symbol of (DTConMSA Y) : ( t in Terminals (DTConMSA Y) & t `2 = s ) } by MSAFREE:13; then consider a being Symbol of (DTConMSA Y) such that A8: x = root-tree a and a in Terminals (DTConMSA Y) and a `2 = s by A2, A5; (Reverse (s9,Y)) . x = a `1 by A2, A5, A8, MSAFREE:def_17 .= [b,s] `1 by A8, A7, TREES_4:4 .= b ; hence x in (S -Terms (X,Y)) . s by A3, A4, A6, A7, Th18; ::_thesis: verum end; theorem Th23: :: MSAFREE3:23 for S being non void Signature for X being ManySortedSet of the carrier of S for t being Term of S,(X \/ ( the carrier of S --> {0})) for s being SortSymbol of S st t in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s holds t in the Sorts of (Free (S,X)) . s proof let S be non empty non void ManySortedSign ; ::_thesis: for X being ManySortedSet of the carrier of S for t being Term of S,(X \/ ( the carrier of S --> {0})) for s being SortSymbol of S st t in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s holds t in the Sorts of (Free (S,X)) . s let X be ManySortedSet of the carrier of S; ::_thesis: for t being Term of S,(X \/ ( the carrier of S --> {0})) for s being SortSymbol of S st t in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s holds t in the Sorts of (Free (S,X)) . s set Y = X \/ ( the carrier of S --> {0}); set T = the Sorts of (Free (S,X)); defpred S1[ set ] means for s being SortSymbol of S st \$1 in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s holds \$1 in the Sorts of (Free (S,X)) . s; A1: ex A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st ( Free (S,X) = GenMSAlg A & A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X ) by Def1; then reconsider TT = the Sorts of (Free (S,X)) as MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) by MSUALG_2:def_9; A2: now__::_thesis:_for_o_being_OperSymbol_of_S for_p_being_ArgumentSeq_of_Sym_(o,(X_\/_(_the_carrier_of_S_-->_{0})))_st_(_for_t_being_Term_of_S,(X_\/_(_the_carrier_of_S_-->_{0}))_st_t_in_rng_p_holds_ S1[t]_)_holds_ S1[[o,_the_carrier_of_S]_-tree_p] let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of Sym (o,(X \/ ( the carrier of S --> {0}))) st ( for t being Term of S,(X \/ ( the carrier of S --> {0})) st t in rng p holds S1[t] ) holds S1[[o, the carrier of S] -tree p] let p be ArgumentSeq of Sym (o,(X \/ ( the carrier of S --> {0}))); ::_thesis: ( ( for t being Term of S,(X \/ ( the carrier of S --> {0})) st t in rng p holds S1[t] ) implies S1[[o, the carrier of S] -tree p] ) assume A3: for t being Term of S,(X \/ ( the carrier of S --> {0})) st t in rng p holds S1[t] ; ::_thesis: S1[[o, the carrier of S] -tree p] thus S1[[o, the carrier of S] -tree p] ::_thesis: verum proof let s be SortSymbol of S; ::_thesis: ( [o, the carrier of S] -tree p in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s implies [o, the carrier of S] -tree p in the Sorts of (Free (S,X)) . s ) assume A4: [o, the carrier of S] -tree p in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s ; ::_thesis: [o, the carrier of S] -tree p in the Sorts of (Free (S,X)) . s A5: Sym (o,(X \/ ( the carrier of S --> {0}))) = [o, the carrier of S] by MSAFREE:def_9; the_sort_of ((Sym (o,(X \/ ( the carrier of S --> {0})))) -tree p) = the_result_sort_of o by MSATERM:20; then A6: s = the_result_sort_of o by A4, A5, Th17; then A7: rng p c= Union (S -Terms (X,(X \/ ( the carrier of S --> {0})))) by A4, A5, Th19; A8: rng p c= Union TT proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in Union TT ) assume A9: x in rng p ; ::_thesis: x in Union TT then consider y being set such that A10: y in dom (S -Terms (X,(X \/ ( the carrier of S --> {0})))) and A11: x in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . y by A7, CARD_5:2; reconsider y = y as SortSymbol of S by A10; (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . y = (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . y ; then reconsider x = x as Term of S,(X \/ ( the carrier of S --> {0})) by A11, Th16; ( dom the Sorts of (Free (S,X)) = the carrier of S & x in the Sorts of (Free (S,X)) . y ) by A3, A9, A11, PARTFUN1:def_2; hence x in Union TT by CARD_5:2; ::_thesis: verum end; TT is opers_closed by A1, MSUALG_2:def_9; hence [o, the carrier of S] -tree p in the Sorts of (Free (S,X)) . s by A5, A6, A8, Th20; ::_thesis: verum end; end; A12: S -Terms (X,(X \/ ( the carrier of S --> {0}))) c= the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) by PBOOLE:def_18; A13: now__::_thesis:_for_s1_being_SortSymbol_of_S for_v_being_Element_of_(X_\/_(_the_carrier_of_S_-->_{0}))_._s1_holds_S1[_root-tree_[v,s1]] let s1 be SortSymbol of S; ::_thesis: for v being Element of (X \/ ( the carrier of S --> {0})) . s1 holds S1[ root-tree [v,s1]] let v be Element of (X \/ ( the carrier of S --> {0})) . s1; ::_thesis: S1[ root-tree [v,s1]] thus S1[ root-tree [v,s1]] ::_thesis: verum proof reconsider t = root-tree [v,s1] as Term of S,(X \/ ( the carrier of S --> {0})) by MSATERM:4; let s be SortSymbol of S; ::_thesis: ( root-tree [v,s1] in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s implies root-tree [v,s1] in the Sorts of (Free (S,X)) . s ) assume A14: root-tree [v,s1] in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s ; ::_thesis: root-tree [v,s1] in the Sorts of (Free (S,X)) . s (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s c= the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) . s by A12, PBOOLE:def_2; then A15: the_sort_of t = s by A14, Th7; A16: the_sort_of t = s1 by MSATERM:14; then v in X . s by A14, A15, Th18; hence root-tree [v,s1] in the Sorts of (Free (S,X)) . s by A15, A16, Th4; ::_thesis: verum end; end; thus for t being Term of S,(X \/ ( the carrier of S --> {0})) holds S1[t] from MSATERM:sch_1(A13, A2); ::_thesis: verum end; theorem Th24: :: MSAFREE3:24 for S being non void Signature for X being ManySortedSet of the carrier of S holds the Sorts of (Free (S,X)) = S -Terms (X,(X \/ ( the carrier of S --> {0}))) proof let S be non void Signature; ::_thesis: for X being ManySortedSet of the carrier of S holds the Sorts of (Free (S,X)) = S -Terms (X,(X \/ ( the carrier of S --> {0}))) let X be ManySortedSet of the carrier of S; ::_thesis: the Sorts of (Free (S,X)) = S -Terms (X,(X \/ ( the carrier of S --> {0}))) set Y = X \/ ( the carrier of S --> {0}); set B = MSAlgebra(# (S -Terms (X,(X \/ ( the carrier of S --> {0})))),(Opers ((FreeMSA (X \/ ( the carrier of S --> {0}))),(S -Terms (X,(X \/ ( the carrier of S --> {0})))))) #); for Z being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st Z = the Sorts of MSAlgebra(# (S -Terms (X,(X \/ ( the carrier of S --> {0})))),(Opers ((FreeMSA (X \/ ( the carrier of S --> {0}))),(S -Terms (X,(X \/ ( the carrier of S --> {0})))))) #) holds ( Z is opers_closed & the Charact of MSAlgebra(# (S -Terms (X,(X \/ ( the carrier of S --> {0})))),(Opers ((FreeMSA (X \/ ( the carrier of S --> {0}))),(S -Terms (X,(X \/ ( the carrier of S --> {0})))))) #) = Opers ((FreeMSA (X \/ ( the carrier of S --> {0}))),Z) ) by Th21; then reconsider B = MSAlgebra(# (S -Terms (X,(X \/ ( the carrier of S --> {0})))),(Opers ((FreeMSA (X \/ ( the carrier of S --> {0}))),(S -Terms (X,(X \/ ( the carrier of S --> {0})))))) #) as MSSubAlgebra of FreeMSA (X \/ ( the carrier of S --> {0})) by MSUALG_2:def_9; A1: ( FreeMSA (X \/ ( the carrier of S --> {0})) = MSAlgebra(# (FreeSort (X \/ ( the carrier of S --> {0}))),(FreeOper (X \/ ( the carrier of S --> {0}))) #) & dom (FreeSort (X \/ ( the carrier of S --> {0}))) = the carrier of S ) by MSAFREE:def_14, PARTFUN1:def_2; (Reverse (X \/ ( the carrier of S --> {0}))) "" X c= S -Terms (X,(X \/ ( the carrier of S --> {0}))) by Th22; then A2: (Reverse (X \/ ( the carrier of S --> {0}))) "" X is MSSubset of B by PBOOLE:def_18; let s be Element of S; :: according to PBOOLE:def_21 ::_thesis: the Sorts of (Free (S,X)) . s = (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s ex A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st ( Free (S,X) = GenMSAlg A & A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X ) by Def1; then Free (S,X) is MSSubAlgebra of B by A2, MSUALG_2:def_17; then the Sorts of (Free (S,X)) is MSSubset of B by MSUALG_2:def_9; then the Sorts of (Free (S,X)) c= S -Terms (X,(X \/ ( the carrier of S --> {0}))) by PBOOLE:def_18; hence the Sorts of (Free (S,X)) . s c= (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s by PBOOLE:def_2; :: according to XBOOLE_0:def_10 ::_thesis: (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s c= the Sorts of (Free (S,X)) . s let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s or x in the Sorts of (Free (S,X)) . s ) assume A3: x in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s ; ::_thesis: x in the Sorts of (Free (S,X)) . s S -Terms (X,(X \/ ( the carrier of S --> {0}))) c= the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) by PBOOLE:def_18; then (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s c= the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) . s by PBOOLE:def_2; then x in Union (FreeSort (X \/ ( the carrier of S --> {0}))) by A3, A1, CARD_5:2; then x is Term of S,(X \/ ( the carrier of S --> {0})) by MSATERM:13; hence x in the Sorts of (Free (S,X)) . s by A3, Th23; ::_thesis: verum end; theorem :: MSAFREE3:25 for S being non void Signature for X being ManySortedSet of the carrier of S holds (FreeMSA (X \/ ( the carrier of S --> {0}))) | (S -Terms (X,(X \/ ( the carrier of S --> {0})))) = Free (S,X) proof let S be non void Signature; ::_thesis: for X being ManySortedSet of the carrier of S holds (FreeMSA (X \/ ( the carrier of S --> {0}))) | (S -Terms (X,(X \/ ( the carrier of S --> {0})))) = Free (S,X) let X be ManySortedSet of the carrier of S; ::_thesis: (FreeMSA (X \/ ( the carrier of S --> {0}))) | (S -Terms (X,(X \/ ( the carrier of S --> {0})))) = Free (S,X) set Y = X \/ ( the carrier of S --> {0}); ( (FreeMSA (X \/ ( the carrier of S --> {0}))) | (S -Terms (X,(X \/ ( the carrier of S --> {0})))) = MSAlgebra(# (S -Terms (X,(X \/ ( the carrier of S --> {0})))),(Opers ((FreeMSA (X \/ ( the carrier of S --> {0}))),(S -Terms (X,(X \/ ( the carrier of S --> {0})))))) #) & ex A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st ( Free (S,X) = GenMSAlg A & A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X ) ) by Def1, Th21, MSUALG_2:def_15; hence (FreeMSA (X \/ ( the carrier of S --> {0}))) | (S -Terms (X,(X \/ ( the carrier of S --> {0})))) = Free (S,X) by Th24, MSUALG_2:9; ::_thesis: verum end; theorem Th26: :: MSAFREE3:26 for S being non void Signature for X, Y being V8() ManySortedSet of the carrier of S for A being MSSubAlgebra of FreeMSA X for B being MSSubAlgebra of FreeMSA Y st the Sorts of A = the Sorts of B holds MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) proof let S be non void Signature; ::_thesis: for X, Y being V8() ManySortedSet of the carrier of S for A being MSSubAlgebra of FreeMSA X for B being MSSubAlgebra of FreeMSA Y st the Sorts of A = the Sorts of B holds MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) let X, Y be V8() ManySortedSet of the carrier of S; ::_thesis: for A being MSSubAlgebra of FreeMSA X for B being MSSubAlgebra of FreeMSA Y st the Sorts of A = the Sorts of B holds MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) let A be MSSubAlgebra of FreeMSA X; ::_thesis: for B being MSSubAlgebra of FreeMSA Y st the Sorts of A = the Sorts of B holds MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) let B be MSSubAlgebra of FreeMSA Y; ::_thesis: ( the Sorts of A = the Sorts of B implies MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) ) assume A1: the Sorts of A = the Sorts of B ; ::_thesis: MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) reconsider SB = the Sorts of B as MSSubset of (FreeMSA Y) by MSUALG_2:def_9; reconsider SA = the Sorts of A as MSSubset of (FreeMSA X) by MSUALG_2:def_9; A2: SA is opers_closed by MSUALG_2:def_9; A3: SB is opers_closed by MSUALG_2:def_9; now__::_thesis:_for_x_being_set_st_x_in_the_carrier'_of_S_holds_ the_Charact_of_A_._x_=_the_Charact_of_B_._x let x be set ; ::_thesis: ( x in the carrier' of S implies the Charact of A . x = the Charact of B . x ) A4: ( SA c= the Sorts of (FreeMSA X) & the Sorts of (FreeMSA X) is MSSubset of (FreeMSA X) ) by PBOOLE:def_18; assume x in the carrier' of S ; ::_thesis: the Charact of A . x = the Charact of B . x then reconsider o = x as OperSymbol of S ; A5: SA is_closed_on o by A2, MSUALG_2:def_6; A6: the Charact of A . o = (Opers ((FreeMSA X),SA)) . o by MSUALG_2:def_9 .= o /. SA by MSUALG_2:def_8 .= (Den (o,(FreeMSA X))) | (((SA #) * the Arity of S) . o) by A5, MSUALG_2:def_7 ; Args (o,(FreeMSA X)) = (( the Sorts of (FreeMSA X) #) * the Arity of S) . o by MSUALG_1:def_4; then dom (Den (o,(FreeMSA X))) = (( the Sorts of (FreeMSA X) #) * the Arity of S) . o by FUNCT_2:def_1; then A7: dom ( the Charact of A . o) = ((SA #) * the Arity of S) . o by A6, A4, MSUALG_2:2, RELAT_1:62; A8: ( SB c= the Sorts of (FreeMSA Y) & the Sorts of (FreeMSA Y) is MSSubset of (FreeMSA Y) ) by PBOOLE:def_18; then A9: ((SB #) * the Arity of S) . o c= (( the Sorts of (FreeMSA Y) #) * the Arity of S) . o by MSUALG_2:2; A10: SB is_closed_on o by A3, MSUALG_2:def_6; A11: the Charact of B . o = (Opers ((FreeMSA Y),SB)) . o by MSUALG_2:def_9 .= o /. SB by MSUALG_2:def_8 .= (Den (o,(FreeMSA Y))) | (((SB #) * the Arity of S) . o) by A10, MSUALG_2:def_7 ; Args (o,(FreeMSA Y)) = (( the Sorts of (FreeMSA Y) #) * the Arity of S) . o by MSUALG_1:def_4; then dom (Den (o,(FreeMSA Y))) = (( the Sorts of (FreeMSA Y) #) * the Arity of S) . o by FUNCT_2:def_1; then A12: dom ( the Charact of B . o) = ((SB #) * the Arity of S) . o by A11, A8, MSUALG_2:2, RELAT_1:62; A13: ((SA #) * the Arity of S) . o c= (( the Sorts of (FreeMSA X) #) * the Arity of S) . o by A4, MSUALG_2:2; now__::_thesis:_for_x_being_set_st_x_in_((SA_#)_*_the_Arity_of_S)_._o_holds_ (_the_Charact_of_A_._o)_._x_=_(_the_Charact_of_B_._o)_._x let x be set ; ::_thesis: ( x in ((SA #) * the Arity of S) . o implies ( the Charact of A . o) . x = ( the Charact of B . o) . x ) assume A14: x in ((SA #) * the Arity of S) . o ; ::_thesis: ( the Charact of A . o) . x = ( the Charact of B . o) . x then reconsider p1 = x as Element of Args (o,(FreeMSA X)) by A13, MSUALG_1:def_4; reconsider p2 = x as Element of Args (o,(FreeMSA Y)) by A1, A9, A14, MSUALG_1:def_4; thus ( the Charact of A . o) . x = (Den (o,(FreeMSA X))) . p1 by A6, A7, A14, FUNCT_1:47 .= [o, the carrier of S] -tree p1 by INSTALG1:3 .= (Den (o,(FreeMSA Y))) . p2 by INSTALG1:3 .= ( the Charact of B . o) . x by A1, A11, A12, A14, FUNCT_1:47 ; ::_thesis: verum end; hence the Charact of A . x = the Charact of B . x by A1, A7, A12, FUNCT_1:2; ::_thesis: verum end; hence MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) by A1, PBOOLE:3; ::_thesis: verum end; theorem Th27: :: MSAFREE3:27 for S being non void Signature for X being V9() ManySortedSet of the carrier of S for Y being ManySortedSet of the carrier of S for t being Element of (Free (S,X)) holds S variables_in t c= X proof let S be non void Signature; ::_thesis: for X being V9() ManySortedSet of the carrier of S for Y being ManySortedSet of the carrier of S for t being Element of (Free (S,X)) holds S variables_in t c= X let X be V9() ManySortedSet of the carrier of S; ::_thesis: for Y being ManySortedSet of the carrier of S for t being Element of (Free (S,X)) holds S variables_in t c= X let Y be ManySortedSet of the carrier of S; ::_thesis: for t being Element of (Free (S,X)) holds S variables_in t c= X let t be Element of (Free (S,X)); ::_thesis: S variables_in t c= X set Z = X \/ ( the carrier of S --> {0}); reconsider t = t as Term of S,(X \/ ( the carrier of S --> {0})) by Th8; t in Union the Sorts of (Free (S,X)) ; then A1: t in Union (S -Terms (X,(X \/ ( the carrier of S --> {0})))) by Th24; dom (S -Terms (X,(X \/ ( the carrier of S --> {0})))) = the carrier of S by PARTFUN1:def_2; then ex s being set st ( s in the carrier of S & t in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s ) by A1, CARD_5:2; then variables_in t c= X by Th17; hence S variables_in t c= X ; ::_thesis: verum end; theorem Th28: :: MSAFREE3:28 for S being non void Signature for X being V8() ManySortedSet of the carrier of S for t being Term of S,X holds variables_in t c= X proof let S be non void Signature; ::_thesis: for X being V8() ManySortedSet of the carrier of S for t being Term of S,X holds variables_in t c= X let X be V8() ManySortedSet of the carrier of S; ::_thesis: for t being Term of S,X holds variables_in t c= X defpred S1[ DecoratedTree] means S variables_in \$1 c= X; let t be Term of S,X; ::_thesis: variables_in t c= X A1: for o being OperSymbol of S for p being ArgumentSeq of Sym (o,X) st ( for t being Term of S,X st t in rng p holds S1[t] ) holds S1[[o, the carrier of S] -tree p] proof let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of Sym (o,X) st ( for t being Term of S,X st t in rng p holds S1[t] ) holds S1[[o, the carrier of S] -tree p] let p be ArgumentSeq of Sym (o,X); ::_thesis: ( ( for t being Term of S,X st t in rng p holds S1[t] ) implies S1[[o, the carrier of S] -tree p] ) assume A2: for t being Term of S,X st t in rng p holds S variables_in t c= X ; ::_thesis: S1[[o, the carrier of S] -tree p] thus S variables_in ([o, the carrier of S] -tree p) c= X ::_thesis: verum proof let s be set ; :: according to PBOOLE:def_2 ::_thesis: ( not s in the carrier of S or (S variables_in ([o, the carrier of S] -tree p)) . s c= X . s ) assume A3: s in the carrier of S ; ::_thesis: (S variables_in ([o, the carrier of S] -tree p)) . s c= X . s let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (S variables_in ([o, the carrier of S] -tree p)) . s or x in X . s ) assume x in (S variables_in ([o, the carrier of S] -tree p)) . s ; ::_thesis: x in X . s then consider t being DecoratedTree such that A4: t in rng p and A5: x in (S variables_in t) . s by A3, Th11; consider i being set such that A6: i in dom p and A7: t = p . i by A4, FUNCT_1:def_3; reconsider i = i as Nat by A6; reconsider t = p . i as Term of S,X by A6, MSATERM:22; S variables_in t c= X by A2, A4, A7; then (S variables_in t) . s c= X . s by A3, PBOOLE:def_2; hence x in X . s by A5, A7; ::_thesis: verum end; end; A8: for s being SortSymbol of S for v being Element of X . s holds S1[ root-tree [v,s]] proof let s be SortSymbol of S; ::_thesis: for v being Element of X . s holds S1[ root-tree [v,s]] let x be Element of X . s; ::_thesis: S1[ root-tree [x,s]] thus S variables_in (root-tree [x,s]) c= X ::_thesis: verum proof let y be set ; :: according to PBOOLE:def_2 ::_thesis: ( not y in the carrier of S or (S variables_in (root-tree [x,s])) . y c= X . y ) assume y in the carrier of S ; ::_thesis: (S variables_in (root-tree [x,s])) . y c= X . y A9: ( y <> s implies (S variables_in (root-tree [x,s])) . y = {} ) by Th10; (S variables_in (root-tree [x,s])) . s = {x} by Th10; hence (S variables_in (root-tree [x,s])) . y c= X . y by A9, XBOOLE_1:2; ::_thesis: verum end; end; for t being Term of S,X holds S1[t] from MSATERM:sch_1(A8, A1); hence variables_in t c= X ; ::_thesis: verum end; theorem Th29: :: MSAFREE3:29 for S being non void Signature for X, Y being V8() ManySortedSet of the carrier of S for t1 being Term of S,X for t2 being Term of S,Y st t1 = t2 holds the_sort_of t1 = the_sort_of t2 proof let S be non void Signature; ::_thesis: for X, Y being V8() ManySortedSet of the carrier of S for t1 being Term of S,X for t2 being Term of S,Y st t1 = t2 holds the_sort_of t1 = the_sort_of t2 let X, Y be V8() ManySortedSet of the carrier of S; ::_thesis: for t1 being Term of S,X for t2 being Term of S,Y st t1 = t2 holds the_sort_of t1 = the_sort_of t2 let t1 be Term of S,X; ::_thesis: for t2 being Term of S,Y st t1 = t2 holds the_sort_of t1 = the_sort_of t2 let t2 be Term of S,Y; ::_thesis: ( t1 = t2 implies the_sort_of t1 = the_sort_of t2 ) assume A1: t1 = t2 ; ::_thesis: the_sort_of t1 = the_sort_of t2 percases ( ex s being SortSymbol of S ex v being Element of X . s st t1 . {} = [v,s] or t1 . {} in [: the carrier' of S,{ the carrier of S}:] ) by MSATERM:2; suppose ex s being SortSymbol of S ex v being Element of X . s st t1 . {} = [v,s] ; ::_thesis: the_sort_of t1 = the_sort_of t2 then consider s being SortSymbol of S, x being Element of X . s such that A2: t1 . {} = [x,s] ; s in the carrier of S ; then s <> the carrier of S ; then not s in { the carrier of S} by TARSKI:def_1; then not [x,s] in [: the carrier' of S,{ the carrier of S}:] by ZFMISC_1:87; then consider s9 being SortSymbol of S, y being Element of Y . s9 such that A3: t2 . {} = [y,s9] by A1, A2, MSATERM:2; t1 = root-tree [x,s] by A2, MSATERM:5; then A4: the_sort_of t1 = s by MSATERM:14; t2 = root-tree [y,s9] by A3, MSATERM:5; then the_sort_of t2 = s9 by MSATERM:14; hence the_sort_of t1 = the_sort_of t2 by A1, A2, A3, A4, XTUPLE_0:1; ::_thesis: verum end; suppose t1 . {} in [: the carrier' of S,{ the carrier of S}:] ; ::_thesis: the_sort_of t1 = the_sort_of t2 then consider o, z being set such that A5: o in the carrier' of S and A6: z in { the carrier of S} and A7: t1 . {} = [o,z] by ZFMISC_1:def_2; reconsider o = o as OperSymbol of S by A5; A8: z = the carrier of S by A6, TARSKI:def_1; then the_sort_of t1 = the_result_sort_of o by A7, MSATERM:17; hence the_sort_of t1 = the_sort_of t2 by A1, A7, A8, MSATERM:17; ::_thesis: verum end; end; end; theorem Th30: :: MSAFREE3:30 for S being non void Signature for X, Y being V8() ManySortedSet of the carrier of S for t being Term of S,Y st variables_in t c= X holds t is Term of S,X proof let S be non void Signature; ::_thesis: for X, Y being V8() ManySortedSet of the carrier of S for t being Term of S,Y st variables_in t c= X holds t is Term of S,X let X, Y be V8() ManySortedSet of the carrier of S; ::_thesis: for t being Term of S,Y st variables_in t c= X holds t is Term of S,X defpred S1[ DecoratedTree] means ( Y variables_in \$1 c= X implies \$1 is Term of S,X ); let t be Term of S,Y; ::_thesis: ( variables_in t c= X implies t is Term of S,X ) A1: for o being OperSymbol of S for p being ArgumentSeq of Sym (o,Y) st ( for t being Term of S,Y st t in rng p holds S1[t] ) holds S1[[o, the carrier of S] -tree p] proof let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of Sym (o,Y) st ( for t being Term of S,Y st t in rng p holds S1[t] ) holds S1[[o, the carrier of S] -tree p] let p be ArgumentSeq of Sym (o,Y); ::_thesis: ( ( for t being Term of S,Y st t in rng p holds S1[t] ) implies S1[[o, the carrier of S] -tree p] ) assume that A2: for t being Term of S,Y st t in rng p & Y variables_in t c= X holds t is Term of S,X and A3: Y variables_in ([o, the carrier of S] -tree p) c= X ; ::_thesis: [o, the carrier of S] -tree p is Term of S,X A4: now__::_thesis:_for_i_being_Nat_st_i_in_dom_p_holds_ ex_t9_being_Term_of_S,X_st_ (_t9_=_p_._i_&_the_sort_of_t9_=_(the_arity_of_o)_._i_) let i be Nat; ::_thesis: ( i in dom p implies ex t9 being Term of S,X st ( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i ) ) assume A5: i in dom p ; ::_thesis: ex t9 being Term of S,X st ( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i ) then reconsider t = p . i as Term of S,Y by MSATERM:22; A6: t in rng p by A5, FUNCT_1:def_3; Y variables_in t c= X proof let y be set ; :: according to PBOOLE:def_2 ::_thesis: ( not y in the carrier of S or (Y variables_in t) . y c= X . y ) assume y in the carrier of S ; ::_thesis: (Y variables_in t) . y c= X . y then reconsider s = y as SortSymbol of S ; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Y variables_in t) . y or x in X . y ) assume x in (Y variables_in t) . y ; ::_thesis: x in X . y then A7: x in (Y variables_in ([o, the carrier of S] -tree p)) . s by A6, Th13; (Y variables_in ([o, the carrier of S] -tree p)) . s c= X . s by A3, PBOOLE:def_2; hence x in X . y by A7; ::_thesis: verum end; then reconsider t9 = t as Term of S,X by A2, A6; take t9 = t9; ::_thesis: ( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i ) thus t9 = p . i ; ::_thesis: the_sort_of t9 = (the_arity_of o) . i the_sort_of t = (the_arity_of o) . i by A5, MSATERM:23; hence the_sort_of t9 = (the_arity_of o) . i by Th29; ::_thesis: verum end; len p = len (the_arity_of o) by MSATERM:22; then reconsider p = p as ArgumentSeq of Sym (o,X) by A4, MSATERM:24; (Sym (o,X)) -tree p is Term of S,X ; hence [o, the carrier of S] -tree p is Term of S,X by MSAFREE:def_9; ::_thesis: verum end; assume variables_in t c= X ; ::_thesis: t is Term of S,X then A8: Y variables_in t c= X by Th15; A9: for s being SortSymbol of S for x being Element of Y . s holds S1[ root-tree [x,s]] proof let s be SortSymbol of S; ::_thesis: for x being Element of Y . s holds S1[ root-tree [x,s]] let x be Element of Y . s; ::_thesis: S1[ root-tree [x,s]] assume Y variables_in (root-tree [x,s]) c= X ; ::_thesis: root-tree [x,s] is Term of S,X then A10: (Y variables_in (root-tree [x,s])) . s c= X . s by PBOOLE:def_2; (Y variables_in (root-tree [x,s])) . s = {x} by Th12; then x in X . s by A10, ZFMISC_1:31; hence root-tree [x,s] is Term of S,X by MSATERM:4; ::_thesis: verum end; for t being Term of S,Y holds S1[t] from MSATERM:sch_1(A9, A1); hence t is Term of S,X by A8; ::_thesis: verum end; theorem :: MSAFREE3:31 for S being non void Signature for X being V8() ManySortedSet of the carrier of S holds Free (S,X) = FreeMSA X proof let S be non void Signature; ::_thesis: for X being V8() ManySortedSet of the carrier of S holds Free (S,X) = FreeMSA X let X be V8() ManySortedSet of the carrier of S; ::_thesis: Free (S,X) = FreeMSA X set Y = X \/ ( the carrier of S --> {0}); A1: the Sorts of (Free (S,X)) = S -Terms (X,(X \/ ( the carrier of S --> {0}))) by Th24; A2: FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def_14; A3: the Sorts of (Free (S,X)) = the Sorts of (FreeMSA X) proof let s be Element of S; :: according to PBOOLE:def_21 ::_thesis: the Sorts of (Free (S,X)) . s = the Sorts of (FreeMSA X) . s reconsider s9 = s as SortSymbol of S ; thus the Sorts of (Free (S,X)) . s c= the Sorts of (FreeMSA X) . s :: according to XBOOLE_0:def_10 ::_thesis: the Sorts of (FreeMSA X) . s c= the Sorts of (Free (S,X)) . s proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Sorts of (Free (S,X)) . s or x in the Sorts of (FreeMSA X) . s ) assume A4: x in the Sorts of (Free (S,X)) . s ; ::_thesis: x in the Sorts of (FreeMSA X) . s then reconsider t = x as Term of S,(X \/ ( the carrier of S --> {0})) by A1, Th16; variables_in t c= X by A1, A4, Th17; then reconsider t9 = t as Term of S,X by Th30; the_sort_of t = s by A1, A4, Th17; then the_sort_of t9 = s by Th29; then x in FreeSort (X,s9) by MSATERM:def_5; hence x in the Sorts of (FreeMSA X) . s by A2, MSAFREE:def_11; ::_thesis: verum end; reconsider s9 = s as SortSymbol of S ; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Sorts of (FreeMSA X) . s or x in the Sorts of (Free (S,X)) . s ) assume x in the Sorts of (FreeMSA X) . s ; ::_thesis: x in the Sorts of (Free (S,X)) . s then A5: x in FreeSort (X,s9) by A2, MSAFREE:def_11; FreeSort (X,s9) c= S -Terms X by MSATERM:12; then reconsider t = x as Term of S,X by A5; X c= X \/ ( the carrier of S --> {0}) by PBOOLE:14; then reconsider t9 = t as Term of S,(X \/ ( the carrier of S --> {0})) by MSATERM:26; variables_in t = S variables_in t ; then A6: variables_in t9 c= X by Th28; the_sort_of t = s by A5, MSATERM:def_5; then the_sort_of t9 = s by Th29; then t in { q where q is Term of S,(X \/ ( the carrier of S --> {0})) : ( the_sort_of q = s9 & variables_in q c= X ) } by A6; hence x in the Sorts of (Free (S,X)) . s by A1, Def5; ::_thesis: verum end; ( FreeMSA X is MSSubAlgebra of FreeMSA X & ex A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st ( Free (S,X) = GenMSAlg A & A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X ) ) by Def1, MSUALG_2:5; hence Free (S,X) = FreeMSA X by A3, Th26; ::_thesis: verum end; theorem Th32: :: MSAFREE3:32 for S being non void Signature for Y being V8() ManySortedSet of the carrier of S for t being Term of S,Y for p being Element of dom t holds variables_in (t | p) c= variables_in t proof let S be non void Signature; ::_thesis: for Y being V8() ManySortedSet of the carrier of S for t being Term of S,Y for p being Element of dom t holds variables_in (t | p) c= variables_in t let Y be V8() ManySortedSet of the carrier of S; ::_thesis: for t being Term of S,Y for p being Element of dom t holds variables_in (t | p) c= variables_in t let t be Term of S,Y; ::_thesis: for p being Element of dom t holds variables_in (t | p) c= variables_in t let p be Element of dom t; ::_thesis: variables_in (t | p) c= variables_in t reconsider q = t | p as Term of S,Y ; let s be set ; :: according to PBOOLE:def_2 ::_thesis: ( not s in the carrier of S or (variables_in (t | p)) . s c= (variables_in t) . s ) assume A1: s in the carrier of S ; ::_thesis: (variables_in (t | p)) . s c= (variables_in t) . s let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (variables_in (t | p)) . s or x in (variables_in t) . s ) assume x in (variables_in (t | p)) . s ; ::_thesis: x in (variables_in t) . s then x in { (a `1) where a is Element of rng q : a `2 = s } by A1, Def2; then consider a being Element of rng (t | p) such that A2: ( x = a `1 & a `2 = s ) ; ( rng (t | p) c= rng t & a in rng (t | p) ) by TREES_2:32; then x in { (b `1) where b is Element of rng t : b `2 = s } by A2; hence x in (variables_in t) . s by A1, Def2; ::_thesis: verum end; theorem Th33: :: MSAFREE3:33 for S being non void Signature for X being V9() ManySortedSet of the carrier of S for t being Element of (Free (S,X)) for p being Element of dom t holds t | p is Element of (Free (S,X)) proof let S be non void Signature; ::_thesis: for X being V9() ManySortedSet of the carrier of S for t being Element of (Free (S,X)) for p being Element of dom t holds t | p is Element of (Free (S,X)) let X be V9() ManySortedSet of the carrier of S; ::_thesis: for t being Element of (Free (S,X)) for p being Element of dom t holds t | p is Element of (Free (S,X)) let t be Element of (Free (S,X)); ::_thesis: for p being Element of dom t holds t | p is Element of (Free (S,X)) let p be Element of dom t; ::_thesis: t | p is Element of (Free (S,X)) set Y = X \/ ( the carrier of S --> {0}); reconsider t = t as Term of S,(X \/ ( the carrier of S --> {0})) by Th8; reconsider p = p as Element of dom t ; A1: variables_in (t | p) c= variables_in t by Th32; A2: ( the Sorts of (Free (S,X)) = S -Terms (X,(X \/ ( the carrier of S --> {0}))) & dom (S -Terms (X,(X \/ ( the carrier of S --> {0})))) = the carrier of S ) by Th24, PARTFUN1:def_2; then ex x being set st ( x in the carrier of S & t in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . x ) by CARD_5:2; then variables_in t c= X by Th17; then variables_in (t | p) c= X by A1, PBOOLE:13; then t | p in { q where q is Term of S,(X \/ ( the carrier of S --> {0})) : ( the_sort_of q = the_sort_of (t | p) & variables_in q c= X ) } ; then t | p in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . (the_sort_of (t | p)) by Def5; hence t | p is Element of (Free (S,X)) by A2, CARD_5:2; ::_thesis: verum end; theorem Th34: :: MSAFREE3:34 for S being non void Signature for X being V8() ManySortedSet of the carrier of S for t being Term of S,X for a being Element of rng t holds a = [(a `1),(a `2)] proof let S be non void Signature; ::_thesis: for X being V8() ManySortedSet of the carrier of S for t being Term of S,X for a being Element of rng t holds a = [(a `1),(a `2)] let X be V8() ManySortedSet of the carrier of S; ::_thesis: for t being Term of S,X for a being Element of rng t holds a = [(a `1),(a `2)] let t be Term of S,X; ::_thesis: for a being Element of rng t holds a = [(a `1),(a `2)] let a be Element of rng t; ::_thesis: a = [(a `1),(a `2)] consider x being set such that A1: x in dom t and A2: a = t . x by FUNCT_1:def_3; reconsider x = x as Element of dom t by A1; a = (t | x) . {} by A2, TREES_9:35; then ( ex s being SortSymbol of S ex v being Element of X . s st a = [v,s] or a in [: the carrier' of S,{ the carrier of S}:] ) by MSATERM:2; hence a = [(a `1),(a `2)] by MCART_1:21; ::_thesis: verum end; theorem :: MSAFREE3:35 for x being set for S being non void Signature for X being V9() ManySortedSet of the carrier of S for t being Element of (Free (S,X)) for s being SortSymbol of S holds ( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) ) proof let x be set ; ::_thesis: for S being non void Signature for X being V9() ManySortedSet of the carrier of S for t being Element of (Free (S,X)) for s being SortSymbol of S holds ( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) ) let S be non void Signature; ::_thesis: for X being V9() ManySortedSet of the carrier of S for t being Element of (Free (S,X)) for s being SortSymbol of S holds ( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) ) let X be V9() ManySortedSet of the carrier of S; ::_thesis: for t being Element of (Free (S,X)) for s being SortSymbol of S holds ( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) ) let t be Element of (Free (S,X)); ::_thesis: for s being SortSymbol of S holds ( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) ) let s be SortSymbol of S; ::_thesis: ( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) ) set Y = X \/ ( the carrier of S --> {0}); hereby ::_thesis: ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) assume x in (S variables_in t) . s ; ::_thesis: [x,s] in rng t then x in { (a `1) where a is Element of rng t : a `2 = s } by Def2; then consider a being Element of rng t such that A1: ( x = a `1 & a `2 = s ) ; ( t is Term of S,(X \/ ( the carrier of S --> {0})) & a in rng t ) by Th8; hence [x,s] in rng t by A1, Th34; ::_thesis: verum end; assume A2: [x,s] in rng t ; ::_thesis: ( x in (S variables_in t) . s & x in X . s ) then consider z being set such that A3: z in dom t and A4: [x,s] = t . z by FUNCT_1:def_3; reconsider z = z as Element of dom t by A3; reconsider q = t | z as Element of (Free (S,X)) by Th33; A5: [x,s] = q . {} by A4, TREES_9:35; ( [x,s] `1 = x & [x,s] `2 = s ) ; then A6: x in { (a `1) where a is Element of rng t : a `2 = s } by A2; A7: q is Term of S,(X \/ ( the carrier of S --> {0})) by Th8; s in the carrier of S ; then s <> the carrier of S ; then not s in { the carrier of S} by TARSKI:def_1; then not [x,s] in [: the carrier' of S,{ the carrier of S}:] by ZFMISC_1:87; then consider s9 being SortSymbol of S, v being Element of (X \/ ( the carrier of S --> {0})) . s9 such that A8: [x,s] = [v,s9] by A5, A7, MSATERM:2; S variables_in q c= X by Th27; then A9: (S variables_in q) . s9 c= X . s9 by PBOOLE:def_2; q = root-tree [v,s9] by A5, A7, A8, MSATERM:5; then (S variables_in q) . s9 = {v} by Th10; then A10: v in X . s9 by A9, ZFMISC_1:31; x = v by A8, XTUPLE_0:1; hence ( x in (S variables_in t) . s & x in X . s ) by A8, A10, A6, Def2, XTUPLE_0:1; ::_thesis: verum end; theorem :: MSAFREE3:36 for S being non void Signature for X being ManySortedSet of the carrier of S st ( for s being SortSymbol of S st X . s = {} holds ex o being OperSymbol of S st ( the_result_sort_of o = s & the_arity_of o = {} ) ) holds Free (S,X) is non-empty proof let C be non void Signature; ::_thesis: for X being ManySortedSet of the carrier of C st ( for s being SortSymbol of C st X . s = {} holds ex o being OperSymbol of C st ( the_result_sort_of o = s & the_arity_of o = {} ) ) holds Free (C,X) is non-empty let X be ManySortedSet of the carrier of C; ::_thesis: ( ( for s being SortSymbol of C st X . s = {} holds ex o being OperSymbol of C st ( the_result_sort_of o = s & the_arity_of o = {} ) ) implies Free (C,X) is non-empty ) assume A1: for s being SortSymbol of C st X . s = {} holds ex o being OperSymbol of C st ( the_result_sort_of o = s & the_arity_of o = {} ) ; ::_thesis: Free (C,X) is non-empty now__::_thesis:_not_{}_in_rng_the_Sorts_of_(Free_(C,X)) assume {} in rng the Sorts of (Free (C,X)) ; ::_thesis: contradiction then consider s being set such that A2: s in dom the Sorts of (Free (C,X)) and A3: {} = the Sorts of (Free (C,X)) . s by FUNCT_1:def_3; reconsider s = s as SortSymbol of C by A2; set x = the Element of X . s; percases ( X . s = {} or X . s <> {} ) ; suppose X . s = {} ; ::_thesis: contradiction then ex m being OperSymbol of C st ( the_result_sort_of m = s & the_arity_of m = {} ) by A1; hence contradiction by A3, Th5; ::_thesis: verum end; suppose X . s <> {} ; ::_thesis: contradiction then root-tree [ the Element of X . s,s] in the Sorts of (Free (C,X)) . s by Th4; hence contradiction by A3; ::_thesis: verum end; end; end; then the Sorts of (Free (C,X)) is V8() by RELAT_1:def_9; hence Free (C,X) is non-empty by MSUALG_1:def_3; ::_thesis: verum end; theorem Th37: :: MSAFREE3:37 for S being non empty non void ManySortedSign for A being MSAlgebra over S for B being MSSubAlgebra of A for o being OperSymbol of S holds Args (o,B) c= Args (o,A) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra over S for B being MSSubAlgebra of A for o being OperSymbol of S holds Args (o,B) c= Args (o,A) let A be MSAlgebra over S; ::_thesis: for B being MSSubAlgebra of A for o being OperSymbol of S holds Args (o,B) c= Args (o,A) let B be MSSubAlgebra of A; ::_thesis: for o being OperSymbol of S holds Args (o,B) c= Args (o,A) reconsider SB = the Sorts of B as MSSubset of A by MSUALG_2:def_9; let o be OperSymbol of S; ::_thesis: Args (o,B) c= Args (o,A) reconsider SA = the Sorts of A as MSSubset of A by PBOOLE:def_18; A1: Args (o,B) = ((SB #) * the Arity of S) . o by MSUALG_1:def_4; ( SB c= SA & Args (o,A) = ((SA #) * the Arity of S) . o ) by MSUALG_1:def_4, PBOOLE:def_18; hence Args (o,B) c= Args (o,A) by A1, MSUALG_2:2; ::_thesis: verum end; theorem Th38: :: MSAFREE3:38 for S being non void Signature for A being feasible MSAlgebra over S for B being MSSubAlgebra of A holds B is feasible proof let S be non void Signature; ::_thesis: for A being feasible MSAlgebra over S for B being MSSubAlgebra of A holds B is feasible let A be feasible MSAlgebra over S; ::_thesis: for B being MSSubAlgebra of A holds B is feasible let B be MSSubAlgebra of A; ::_thesis: B is feasible reconsider SB = the Sorts of B as MSSubset of A by MSUALG_2:def_9; let o be OperSymbol of S; :: according to MSUALG_6:def_1 ::_thesis: ( Args (o,B) = {} or not Result (o,B) = {} ) set a = the Element of Args (o,B); assume Args (o,B) <> {} ; ::_thesis: not Result (o,B) = {} then A1: the Element of Args (o,B) in Args (o,B) ; A2: Args (o,B) c= Args (o,A) by Th37; then Result (o,A) <> {} by A1, MSUALG_6:def_1; then dom (Den (o,A)) = Args (o,A) by FUNCT_2:def_1; then the Element of Args (o,B) in dom ((Den (o,A)) | (Args (o,B))) by A1, A2, RELAT_1:57; then A3: ( Result (o,B) = (SB * the ResultSort of S) . o & ((Den (o,A)) | (Args (o,B))) . the Element of Args (o,B) in rng ((Den (o,A)) | (Args (o,B))) ) by FUNCT_1:def_3, MSUALG_1:def_5; SB is opers_closed by MSUALG_2:def_9; then SB is_closed_on o by MSUALG_2:def_6; then rng ((Den (o,A)) | (((SB #) * the Arity of S) . o)) c= (SB * the ResultSort of S) . o by MSUALG_2:def_5; hence not Result (o,B) = {} by A3, MSUALG_1:def_4; ::_thesis: verum end; registration let S be non void Signature; let A be feasible MSAlgebra over S; cluster -> feasible for MSSubAlgebra of A; coherence for b1 being MSSubAlgebra of A holds b1 is feasible by Th38; end; theorem Th39: :: MSAFREE3:39 for S being non void Signature for X being ManySortedSet of the carrier of S holds ( Free (S,X) is feasible & Free (S,X) is free ) proof let S be non void Signature; ::_thesis: for X being ManySortedSet of the carrier of S holds ( Free (S,X) is feasible & Free (S,X) is free ) let X be ManySortedSet of the carrier of S; ::_thesis: ( Free (S,X) is feasible & Free (S,X) is free ) set Y = X \/ ( the carrier of S --> {0}); consider A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) such that A1: Free (S,X) = GenMSAlg A and A2: A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X by Def1; thus Free (S,X) is feasible by A1; ::_thesis: Free (S,X) is free A is ManySortedSubset of FreeGen (X \/ ( the carrier of S --> {0})) by A2, EQUATION:8; then A c= FreeGen (X \/ ( the carrier of S --> {0})) by PBOOLE:def_18; hence Free (S,X) is free by A1, EQUATION:28; ::_thesis: verum end; registration let S be non void Signature; let X be ManySortedSet of the carrier of S; cluster Free (S,X) -> strict free feasible ; coherence ( Free (S,X) is feasible & Free (S,X) is free ) by Th39; end;