:: MSAFREE2 semantic presentation begin definition let S be ManySortedSign ; mode Vertex of S is Element of S; end; definition let S be non empty ManySortedSign ; func SortsWithConstants S -> Subset of S equals :Def1: :: MSAFREE2:def 1 { v where v is SortSymbol of S : v is with_const_op } if not S is void otherwise {} ; coherence ( ( not S is void implies { v where v is SortSymbol of S : v is with_const_op } is Subset of S ) & ( S is void implies {} is Subset of S ) ) proof hereby ::_thesis: ( S is void implies {} is Subset of S ) defpred S1[ SortSymbol of S] means \$1 is with_const_op ; assume not S is void ; ::_thesis: { v where v is SortSymbol of S : v is with_const_op } is Subset of S { v where v is SortSymbol of S : S1[v] } is Subset of S from DOMAIN_1:sch_7(); hence { v where v is SortSymbol of S : v is with_const_op } is Subset of S ; ::_thesis: verum end; assume S is void ; ::_thesis: {} is Subset of S thus {} is Subset of S by SUBSET_1:1; ::_thesis: verum end; consistency for b1 being Subset of S holds verum ; end; :: deftheorem Def1 defines SortsWithConstants MSAFREE2:def_1_:_ for S being non empty ManySortedSign holds ( ( not S is void implies SortsWithConstants S = { v where v is SortSymbol of S : v is with_const_op } ) & ( S is void implies SortsWithConstants S = {} ) ); definition let G be non empty ManySortedSign ; func InputVertices G -> Subset of G equals :: MSAFREE2:def 2 the carrier of G \ (rng the ResultSort of G); coherence the carrier of G \ (rng the ResultSort of G) is Subset of G ; func InnerVertices G -> Subset of G equals :: MSAFREE2:def 3 rng the ResultSort of G; coherence rng the ResultSort of G is Subset of G ; end; :: deftheorem defines InputVertices MSAFREE2:def_2_:_ for G being non empty ManySortedSign holds InputVertices G = the carrier of G \ (rng the ResultSort of G); :: deftheorem defines InnerVertices MSAFREE2:def_3_:_ for G being non empty ManySortedSign holds InnerVertices G = rng the ResultSort of G; theorem :: MSAFREE2:1 for G being non empty void ManySortedSign holds InputVertices G = the carrier of G ; theorem Th2: :: MSAFREE2:2 for G being non empty non void ManySortedSign for v being Vertex of G st v in InputVertices G holds for o being OperSymbol of G holds not the_result_sort_of o = v proof let G be non empty non void ManySortedSign ; ::_thesis: for v being Vertex of G st v in InputVertices G holds for o being OperSymbol of G holds not the_result_sort_of o = v let v be Vertex of G; ::_thesis: ( v in InputVertices G implies for o being OperSymbol of G holds not the_result_sort_of o = v ) assume A1: v in InputVertices G ; ::_thesis: for o being OperSymbol of G holds not the_result_sort_of o = v let o be OperSymbol of G; ::_thesis: not the_result_sort_of o = v assume A2: the_result_sort_of o = v ; ::_thesis: contradiction o in the carrier' of G ; then o in dom the ResultSort of G by FUNCT_2:def_1; then v in rng the ResultSort of G by A2, FUNCT_1:def_3; hence contradiction by A1, XBOOLE_0:def_5; ::_thesis: verum end; theorem Th3: :: MSAFREE2:3 for G being non empty ManySortedSign holds SortsWithConstants G c= InnerVertices G proof let G be non empty ManySortedSign ; ::_thesis: SortsWithConstants G c= InnerVertices G percases ( G is void or not G is void ) ; suppose G is void ; ::_thesis: SortsWithConstants G c= InnerVertices G hence SortsWithConstants G c= InnerVertices G by Def1; ::_thesis: verum end; supposeA1: not G is void ; ::_thesis: SortsWithConstants G c= InnerVertices G let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SortsWithConstants G or x in InnerVertices G ) assume A2: x in SortsWithConstants G ; ::_thesis: x in InnerVertices G SortsWithConstants G = { v where v is SortSymbol of G : v is with_const_op } by A1, Def1; then consider x9 being SortSymbol of G such that A3: x9 = x and A4: x9 is with_const_op by A2; ex o being OperSymbol of G st ( the Arity of G . o = {} & the ResultSort of G . o = x9 ) by A4, MSUALG_2:def_1; hence x in InnerVertices G by A1, A3, FUNCT_2:4; ::_thesis: verum end; end; end; theorem :: MSAFREE2:4 for G being non empty ManySortedSign holds InputVertices G misses SortsWithConstants G proof let G be non empty ManySortedSign ; ::_thesis: InputVertices G misses SortsWithConstants G InputVertices G misses InnerVertices G by XBOOLE_1:79; hence InputVertices G misses SortsWithConstants G by Th3, XBOOLE_1:63; ::_thesis: verum end; definition let IT be non empty ManySortedSign ; attrIT is with_input_V means :Def4: :: MSAFREE2:def 4 InputVertices IT <> {} ; end; :: deftheorem Def4 defines with_input_V MSAFREE2:def_4_:_ for IT being non empty ManySortedSign holds ( IT is with_input_V iff InputVertices IT <> {} ); registration cluster non empty non void V55() with_input_V for ManySortedSign ; existence ex b1 being non empty ManySortedSign st ( not b1 is void & b1 is with_input_V ) proof {} in {{},{{}}} by TARSKI:def_2; then reconsider g = {{}} --> {} as Function of {{}},{{},{{}}} by FUNCOP_1:46; {} in {{},{{}}} * by FINSEQ_1:49; then reconsider f = {{}} --> {} as Function of {{}},({{},{{}}} *) by FUNCOP_1:46; take c = ManySortedSign(# {{},{{}}},{{}},f,g #); ::_thesis: ( not c is void & c is with_input_V ) rng the ResultSort of c = {{}} by FUNCOP_1:8; then ( {{}} in the carrier of c & not {{}} in rng the ResultSort of c ) by TARSKI:def_2; then InputVertices c <> {} by XBOOLE_0:def_5; hence ( not c is void & c is with_input_V ) by Def4; ::_thesis: verum end; end; registration let G be non empty with_input_V ManySortedSign ; cluster InputVertices G -> non empty ; coherence not InputVertices G is empty by Def4; end; registration let G be non empty non void ManySortedSign ; cluster InnerVertices G -> non empty ; coherence not InnerVertices G is empty proof dom the ResultSort of G = the carrier' of G by FUNCT_2:def_1; hence not InnerVertices G is empty by RELAT_1:42; ::_thesis: verum end; end; definition let S be non empty ManySortedSign ; let MSA be non-empty MSAlgebra over S; mode InputValues of MSA -> ManySortedSet of InputVertices S means :: MSAFREE2:def 5 for v being Vertex of S st v in InputVertices S holds it . v in the Sorts of MSA . v; existence ex b1 being ManySortedSet of InputVertices S st for v being Vertex of S st v in InputVertices S holds b1 . v in the Sorts of MSA . v proof set e = the Element of product the Sorts of MSA; set p = the Element of product the Sorts of MSA | (InputVertices S); A1: ( dom the Sorts of MSA = the carrier of S & ex g being Function st ( the Element of product the Sorts of MSA = g & dom g = dom the Sorts of MSA & ( for x being set st x in dom the Sorts of MSA holds g . x in the Sorts of MSA . x ) ) ) by CARD_3:def_5, PARTFUN1:def_2; reconsider p = the Element of product the Sorts of MSA | (InputVertices S) as ManySortedSet of InputVertices S ; take p ; ::_thesis: for v being Vertex of S st v in InputVertices S holds p . v in the Sorts of MSA . v let v be Vertex of S; ::_thesis: ( v in InputVertices S implies p . v in the Sorts of MSA . v ) assume v in InputVertices S ; ::_thesis: p . v in the Sorts of MSA . v then p . v = the Element of product the Sorts of MSA . v by FUNCT_1:49; hence p . v in the Sorts of MSA . v by A1; ::_thesis: verum end; end; :: deftheorem defines InputValues MSAFREE2:def_5_:_ for S being non empty ManySortedSign for MSA being non-empty MSAlgebra over S for b3 being ManySortedSet of InputVertices S holds ( b3 is InputValues of MSA iff for v being Vertex of S st v in InputVertices S holds b3 . v in the Sorts of MSA . v ); definition let S be non empty ManySortedSign ; attrS is Circuit-like means :Def6: :: MSAFREE2:def 6 for S9 being non empty non void ManySortedSign st S9 = S holds for o1, o2 being OperSymbol of S9 st the_result_sort_of o1 = the_result_sort_of o2 holds o1 = o2; end; :: deftheorem Def6 defines Circuit-like MSAFREE2:def_6_:_ for S being non empty ManySortedSign holds ( S is Circuit-like iff for S9 being non empty non void ManySortedSign st S9 = S holds for o1, o2 being OperSymbol of S9 st the_result_sort_of o1 = the_result_sort_of o2 holds o1 = o2 ); registration cluster non empty void -> non empty Circuit-like for ManySortedSign ; coherence for b1 being non empty ManySortedSign st b1 is void holds b1 is Circuit-like proof let S be non empty ManySortedSign ; ::_thesis: ( S is void implies S is Circuit-like ) assume A1: S is void ; ::_thesis: S is Circuit-like let S9 be non empty non void ManySortedSign ; :: according to MSAFREE2:def_6 ::_thesis: ( S9 = S implies for o1, o2 being OperSymbol of S9 st the_result_sort_of o1 = the_result_sort_of o2 holds o1 = o2 ) thus ( S9 = S implies for o1, o2 being OperSymbol of S9 st the_result_sort_of o1 = the_result_sort_of o2 holds o1 = o2 ) by A1; ::_thesis: verum end; end; registration cluster non empty non void V55() strict Circuit-like for ManySortedSign ; existence ex b1 being non empty ManySortedSign st ( not b1 is void & b1 is Circuit-like & b1 is strict ) proof {} in {{}} * by FINSEQ_1:49; then reconsider f = {{}} --> {} as Function of {{}},({{}} *) by FUNCOP_1:46; reconsider g = {{}} --> {} as Function of {{}},{{}} ; take c = ManySortedSign(# {{}},{{}},f,g #); ::_thesis: ( not c is void & c is Circuit-like & c is strict ) c is Circuit-like proof let S be non empty non void ManySortedSign ; :: according to MSAFREE2:def_6 ::_thesis: ( S = c implies for o1, o2 being OperSymbol of S st the_result_sort_of o1 = the_result_sort_of o2 holds o1 = o2 ) assume A1: S = c ; ::_thesis: for o1, o2 being OperSymbol of S st the_result_sort_of o1 = the_result_sort_of o2 holds o1 = o2 let v1, v2 be OperSymbol of S; ::_thesis: ( the_result_sort_of v1 = the_result_sort_of v2 implies v1 = v2 ) assume the_result_sort_of v1 = the_result_sort_of v2 ; ::_thesis: v1 = v2 thus v1 = {} by A1, TARSKI:def_1 .= v2 by A1, TARSKI:def_1 ; ::_thesis: verum end; hence ( not c is void & c is Circuit-like & c is strict ) ; ::_thesis: verum end; end; definition let IIG be non empty non void Circuit-like ManySortedSign ; let v be Vertex of IIG; assume B1: v in InnerVertices IIG ; func action_at v -> OperSymbol of IIG means :: MSAFREE2:def 7 the_result_sort_of it = v; existence ex b1 being OperSymbol of IIG st the_result_sort_of b1 = v proof consider x being set such that A1: x in dom the ResultSort of IIG and A2: the ResultSort of IIG . x = v by B1, FUNCT_1:def_3; reconsider x = x as OperSymbol of IIG by A1; take x ; ::_thesis: the_result_sort_of x = v thus the_result_sort_of x = v by A2; ::_thesis: verum end; uniqueness for b1, b2 being OperSymbol of IIG st the_result_sort_of b1 = v & the_result_sort_of b2 = v holds b1 = b2 by Def6; end; :: deftheorem defines action_at MSAFREE2:def_7_:_ for IIG being non empty non void Circuit-like ManySortedSign for v being Vertex of IIG st v in InnerVertices IIG holds for b3 being OperSymbol of IIG holds ( b3 = action_at v iff the_result_sort_of b3 = v ); begin theorem :: MSAFREE2:5 for S being non empty non void ManySortedSign for A being MSAlgebra over S for o being OperSymbol of S for p being FinSequence st len p = len (the_arity_of o) & ( for k being Nat st k in dom p holds p . k in the Sorts of A . ((the_arity_of o) /. k) ) holds p in Args (o,A) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra over S for o being OperSymbol of S for p being FinSequence st len p = len (the_arity_of o) & ( for k being Nat st k in dom p holds p . k in the Sorts of A . ((the_arity_of o) /. k) ) holds p in Args (o,A) let A be MSAlgebra over S; ::_thesis: for o being OperSymbol of S for p being FinSequence st len p = len (the_arity_of o) & ( for k being Nat st k in dom p holds p . k in the Sorts of A . ((the_arity_of o) /. k) ) holds p in Args (o,A) let o be OperSymbol of S; ::_thesis: for p being FinSequence st len p = len (the_arity_of o) & ( for k being Nat st k in dom p holds p . k in the Sorts of A . ((the_arity_of o) /. k) ) holds p in Args (o,A) let p be FinSequence; ::_thesis: ( len p = len (the_arity_of o) & ( for k being Nat st k in dom p holds p . k in the Sorts of A . ((the_arity_of o) /. k) ) implies p in Args (o,A) ) assume that A1: len p = len (the_arity_of o) and A2: for k being Nat st k in dom p holds p . k in the Sorts of A . ((the_arity_of o) /. k) ; ::_thesis: p in Args (o,A) set D = the Sorts of A * (the_arity_of o); A3: dom p = dom (the_arity_of o) by A1, FINSEQ_3:29; rng (the_arity_of o) c= the carrier of S ; then rng (the_arity_of o) c= dom the Sorts of A by PARTFUN1:def_2; then A4: dom p = dom ( the Sorts of A * (the_arity_of o)) by A3, RELAT_1:27; A5: now__::_thesis:_for_x_being_set_st_x_in_dom_(_the_Sorts_of_A_*_(the_arity_of_o))_holds_ p_._x_in_(_the_Sorts_of_A_*_(the_arity_of_o))_._x let x be set ; ::_thesis: ( x in dom ( the Sorts of A * (the_arity_of o)) implies p . x in ( the Sorts of A * (the_arity_of o)) . x ) assume A6: x in dom ( the Sorts of A * (the_arity_of o)) ; ::_thesis: p . x in ( the Sorts of A * (the_arity_of o)) . x then reconsider k = x as Nat ; ( the Sorts of A * (the_arity_of o)) . k = the Sorts of A . ((the_arity_of o) . k) by A6, FUNCT_1:12 .= the Sorts of A . ((the_arity_of o) /. k) by A3, A4, A6, PARTFUN1:def_6 ; hence p . x in ( the Sorts of A * (the_arity_of o)) . x by A2, A4, A6; ::_thesis: verum end; dom the Arity of S = the carrier' of S by FUNCT_2:def_1; then (( the Sorts of A #) * the Arity of S) . o = ( the Sorts of A #) . (the_arity_of o) by FUNCT_1:13 .= product ( the Sorts of A * (the_arity_of o)) by FINSEQ_2:def_5 ; hence p in Args (o,A) by A4, A5, CARD_3:def_5; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let MSA be non-empty MSAlgebra over S; func FreeEnv MSA -> strict non-empty free MSAlgebra over S equals :: MSAFREE2:def 8 FreeMSA the Sorts of MSA; coherence FreeMSA the Sorts of MSA is strict non-empty free MSAlgebra over S by MSAFREE:17; end; :: deftheorem defines FreeEnv MSAFREE2:def_8_:_ for S being non empty non void ManySortedSign for MSA being non-empty MSAlgebra over S holds FreeEnv MSA = FreeMSA the Sorts of MSA; definition let S be non empty non void ManySortedSign ; let MSA be non-empty MSAlgebra over S; func Eval MSA -> ManySortedFunction of (FreeEnv MSA),MSA means :: MSAFREE2:def 9 ( it is_homomorphism FreeEnv MSA,MSA & ( for s being SortSymbol of S for x, y being set st y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s holds (it . s) . y = x ) ); existence ex b1 being ManySortedFunction of (FreeEnv MSA),MSA st ( b1 is_homomorphism FreeEnv MSA,MSA & ( for s being SortSymbol of S for x, y being set st y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s holds (b1 . s) . y = x ) ) proof reconsider A = FreeGen the Sorts of MSA as free GeneratorSet of FreeEnv MSA by MSAFREE:16; defpred S1[ set , set ] means ex s being SortSymbol of S ex f being Function of (A . s),( the Sorts of MSA . s) st ( f = \$2 & s = \$1 & ( for x, y being set st y in A . s & y = root-tree [x,s] & x in the Sorts of MSA . s holds f . y = x ) ); A1: for i being set st i in the carrier of S holds ex j being set st S1[i,j] proof let i be set ; ::_thesis: ( i in the carrier of S implies ex j being set st S1[i,j] ) assume i in the carrier of S ; ::_thesis: ex j being set st S1[i,j] then reconsider s = i as SortSymbol of S ; defpred S2[ set , set ] means \$1 = root-tree [\$2,s]; A2: for e being set st e in A . s holds ex u being set st ( u in the Sorts of MSA . s & S2[e,u] ) proof let e be set ; ::_thesis: ( e in A . s implies ex u being set st ( u in the Sorts of MSA . s & S2[e,u] ) ) assume e in A . s ; ::_thesis: ex u being set st ( u in the Sorts of MSA . s & S2[e,u] ) then e in FreeGen (s, the Sorts of MSA) by MSAFREE:def_16; hence ex u being set st ( u in the Sorts of MSA . s & S2[e,u] ) by MSAFREE:def_15; ::_thesis: verum end; consider j being Function such that A3: ( dom j = A . s & rng j c= the Sorts of MSA . s & ( for e being set st e in A . s holds S2[e,j . e] ) ) from FUNCT_1:sch_5(A2); reconsider f = j as Function of (A . s),( the Sorts of MSA . s) by A3, FUNCT_2:def_1, RELSET_1:4; take j ; ::_thesis: S1[i,j] take s ; ::_thesis: ex f being Function of (A . s),( the Sorts of MSA . s) st ( f = j & s = i & ( for x, y being set st y in A . s & y = root-tree [x,s] & x in the Sorts of MSA . s holds f . y = x ) ) take f ; ::_thesis: ( f = j & s = i & ( for x, y being set st y in A . s & y = root-tree [x,s] & x in the Sorts of MSA . s holds f . y = x ) ) thus ( f = j & s = i ) ; ::_thesis: for x, y being set st y in A . s & y = root-tree [x,s] & x in the Sorts of MSA . s holds f . y = x let x, y be set ; ::_thesis: ( y in A . s & y = root-tree [x,s] & x in the Sorts of MSA . s implies f . y = x ) assume that A4: y in A . s and A5: y = root-tree [x,s] and x in the Sorts of MSA . s ; ::_thesis: f . y = x y = root-tree [(j . y),s] by A3, A4; then [x,s] = [(j . y),s] by A5, TREES_4:4; hence f . y = x by XTUPLE_0:1; ::_thesis: verum end; consider f being ManySortedSet of the carrier of S such that A6: for i being set st i in the carrier of S holds S1[i,f . i] from PBOOLE:sch_3(A1); now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ f_._x_is_Function let x be set ; ::_thesis: ( x in dom f implies f . x is Function ) assume x in dom f ; ::_thesis: f . x is Function then x in the carrier of S ; then S1[x,f . x] by A6; hence f . x is Function ; ::_thesis: verum end; then reconsider f = f as ManySortedFunction of the carrier of S by FUNCOP_1:def_6; now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_ f_._i_is_Function_of_(A_._i),(_the_Sorts_of_MSA_._i) let i be set ; ::_thesis: ( i in the carrier of S implies f . i is Function of (A . i),( the Sorts of MSA . i) ) assume i in the carrier of S ; ::_thesis: f . i is Function of (A . i),( the Sorts of MSA . i) then S1[i,f . i] by A6; hence f . i is Function of (A . i),( the Sorts of MSA . i) ; ::_thesis: verum end; then reconsider f = f as ManySortedFunction of A, the Sorts of MSA by PBOOLE:def_15; consider IT being ManySortedFunction of (FreeEnv MSA),MSA such that A7: IT is_homomorphism FreeEnv MSA,MSA and A8: IT || A = f by MSAFREE:def_5; take IT ; ::_thesis: ( IT is_homomorphism FreeEnv MSA,MSA & ( for s being SortSymbol of S for x, y being set st y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s holds (IT . s) . y = x ) ) thus IT is_homomorphism FreeEnv MSA,MSA by A7; ::_thesis: for s being SortSymbol of S for x, y being set st y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s holds (IT . s) . y = x let s be SortSymbol of S; ::_thesis: for x, y being set st y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s holds (IT . s) . y = x let x, y be set ; ::_thesis: ( y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s implies (IT . s) . y = x ) A9: ex t being SortSymbol of S ex g being Function of (A . t),( the Sorts of MSA . t) st ( g = f . s & t = s & ( for x, y being set st y in A . t & y = root-tree [x,t] & x in the Sorts of MSA . t holds g . y = x ) ) by A6; assume that y in FreeSort ( the Sorts of MSA,s) and A10: ( y = root-tree [x,s] & x in the Sorts of MSA . s ) ; ::_thesis: (IT . s) . y = x y in FreeGen (s, the Sorts of MSA) by A10, MSAFREE:def_15; then A11: y in A . s by MSAFREE:def_16; hence (IT . s) . y = ((IT . s) | (A . s)) . y by FUNCT_1:49 .= (f . s) . y by A8, MSAFREE:def_1 .= x by A10, A11, A9 ; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedFunction of (FreeEnv MSA),MSA st b1 is_homomorphism FreeEnv MSA,MSA & ( for s being SortSymbol of S for x, y being set st y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s holds (b1 . s) . y = x ) & b2 is_homomorphism FreeEnv MSA,MSA & ( for s being SortSymbol of S for x, y being set st y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s holds (b2 . s) . y = x ) holds b1 = b2 proof defpred S1[ set , set , set ] means \$3 = root-tree [\$2,\$1]; let IT1, IT2 be ManySortedFunction of (FreeEnv MSA),MSA; ::_thesis: ( IT1 is_homomorphism FreeEnv MSA,MSA & ( for s being SortSymbol of S for x, y being set st y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s holds (IT1 . s) . y = x ) & IT2 is_homomorphism FreeEnv MSA,MSA & ( for s being SortSymbol of S for x, y being set st y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s holds (IT2 . s) . y = x ) implies IT1 = IT2 ) reconsider IT19 = IT1, IT29 = IT2 as ManySortedFunction of (FreeMSA the Sorts of MSA),MSA ; assume IT1 is_homomorphism FreeEnv MSA,MSA ; ::_thesis: ( ex s being SortSymbol of S ex x, y being set st ( y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s & not (IT1 . s) . y = x ) or not IT2 is_homomorphism FreeEnv MSA,MSA or ex s being SortSymbol of S ex x, y being set st ( y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s & not (IT2 . s) . y = x ) or IT1 = IT2 ) then A12: IT19 is_homomorphism FreeMSA the Sorts of MSA,MSA ; assume A13: for s being SortSymbol of S for x, y being set st y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s holds (IT1 . s) . y = x ; ::_thesis: ( not IT2 is_homomorphism FreeEnv MSA,MSA or ex s being SortSymbol of S ex x, y being set st ( y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s & not (IT2 . s) . y = x ) or IT1 = IT2 ) A14: for s being SortSymbol of S for x, y being set st y in FreeGen (s, the Sorts of MSA) holds ( (IT19 . s) . y = x iff S1[s,x,y] ) proof let s be SortSymbol of S; ::_thesis: for x, y being set st y in FreeGen (s, the Sorts of MSA) holds ( (IT19 . s) . y = x iff S1[s,x,y] ) let x, y be set ; ::_thesis: ( y in FreeGen (s, the Sorts of MSA) implies ( (IT19 . s) . y = x iff S1[s,x,y] ) ) assume A15: y in FreeGen (s, the Sorts of MSA) ; ::_thesis: ( (IT19 . s) . y = x iff S1[s,x,y] ) then consider a being set such that A16: a in the Sorts of MSA . s and A17: y = root-tree [a,s] by MSAFREE:def_15; y in (FreeSort the Sorts of MSA) . s by A15; then A18: y in FreeSort ( the Sorts of MSA,s) by MSAFREE:def_11; hence ( (IT19 . s) . y = x implies y = root-tree [x,s] ) by A13, A16, A17; ::_thesis: ( S1[s,x,y] implies (IT19 . s) . y = x ) assume y = root-tree [x,s] ; ::_thesis: (IT19 . s) . y = x then [x,s] = [a,s] by A17, TREES_4:4; then x = a by XTUPLE_0:1; hence (IT19 . s) . y = x by A13, A18, A16, A17; ::_thesis: verum end; assume IT2 is_homomorphism FreeEnv MSA,MSA ; ::_thesis: ( ex s being SortSymbol of S ex x, y being set st ( y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s & not (IT2 . s) . y = x ) or IT1 = IT2 ) then A19: IT29 is_homomorphism FreeMSA the Sorts of MSA,MSA ; assume A20: for s being SortSymbol of S for x, y being set st y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s holds (IT2 . s) . y = x ; ::_thesis: IT1 = IT2 A21: for s being SortSymbol of S for x, y being set st y in FreeGen (s, the Sorts of MSA) holds ( (IT29 . s) . y = x iff S1[s,x,y] ) proof let s be SortSymbol of S; ::_thesis: for x, y being set st y in FreeGen (s, the Sorts of MSA) holds ( (IT29 . s) . y = x iff S1[s,x,y] ) let x, y be set ; ::_thesis: ( y in FreeGen (s, the Sorts of MSA) implies ( (IT29 . s) . y = x iff S1[s,x,y] ) ) assume A22: y in FreeGen (s, the Sorts of MSA) ; ::_thesis: ( (IT29 . s) . y = x iff S1[s,x,y] ) then consider a being set such that A23: a in the Sorts of MSA . s and A24: y = root-tree [a,s] by MSAFREE:def_15; y in (FreeSort the Sorts of MSA) . s by A22; then A25: y in FreeSort ( the Sorts of MSA,s) by MSAFREE:def_11; hence ( (IT29 . s) . y = x implies y = root-tree [x,s] ) by A20, A23, A24; ::_thesis: ( S1[s,x,y] implies (IT29 . s) . y = x ) assume y = root-tree [x,s] ; ::_thesis: (IT29 . s) . y = x then [x,s] = [a,s] by A24, TREES_4:4; then x = a by XTUPLE_0:1; hence (IT29 . s) . y = x by A20, A25, A23, A24; ::_thesis: verum end; IT19 = IT29 from MSAFREE1:sch_3(A12, A14, A19, A21); hence IT1 = IT2 ; ::_thesis: verum end; end; :: deftheorem defines Eval MSAFREE2:def_9_:_ for S being non empty non void ManySortedSign for MSA being non-empty MSAlgebra over S for b3 being ManySortedFunction of (FreeEnv MSA),MSA holds ( b3 = Eval MSA iff ( b3 is_homomorphism FreeEnv MSA,MSA & ( for s being SortSymbol of S for x, y being set st y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s holds (b3 . s) . y = x ) ) ); theorem Th6: :: MSAFREE2:6 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S holds the Sorts of A is GeneratorSet of A proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S holds the Sorts of A is GeneratorSet of A let A be non-empty MSAlgebra over S; ::_thesis: the Sorts of A is GeneratorSet of A reconsider theA = MSAlgebra(# the Sorts of A, the Charact of A #) as non-empty MSAlgebra over S ; reconsider AA = the Sorts of A as V16() MSSubset of theA by PBOOLE:def_18; set GAA = GenMSAlg AA; A1: the Sorts of (GenMSAlg AA) is MSSubset of A by MSUALG_2:def_9; now__::_thesis:_for_B_being_MSSubset_of_A_st_B_=_the_Sorts_of_(GenMSAlg_AA)_holds_ (_B_is_opers_closed_&_the_Charact_of_(GenMSAlg_AA)_=_Opers_(A,B)_) let B be MSSubset of A; ::_thesis: ( B = the Sorts of (GenMSAlg AA) implies ( B is opers_closed & the Charact of (GenMSAlg AA) = Opers (A,B) ) ) assume A2: B = the Sorts of (GenMSAlg AA) ; ::_thesis: ( B is opers_closed & the Charact of (GenMSAlg AA) = Opers (A,B) ) reconsider C = B as MSSubset of theA ; A3: C is opers_closed by A2, MSUALG_2:def_9; A4: now__::_thesis:_for_o_being_OperSymbol_of_S_holds_B_is_closed_on_o let o be OperSymbol of S; ::_thesis: B is_closed_on o C is_closed_on o by A3, MSUALG_2:def_6; then A5: rng ((Den (o,MSAlgebra(# the Sorts of A, the Charact of A #))) | (((C #) * the Arity of S) . o)) c= (C * the ResultSort of S) . o by MSUALG_2:def_5; Den (o,A) = Den (o,MSAlgebra(# the Sorts of A, the Charact of A #)) ; hence B is_closed_on o by A5, MSUALG_2:def_5; ::_thesis: verum end; hence B is opers_closed by MSUALG_2:def_6; ::_thesis: the Charact of (GenMSAlg AA) = Opers (A,B) reconsider OAB = Opers (A,B) as ManySortedFunction of (C #) * the Arity of S,C * the ResultSort of S ; A6: now__::_thesis:_for_o_being_OperSymbol_of_S_holds_OAB_._o_=_o_/._C let o be OperSymbol of S; ::_thesis: OAB . o = o /. C A7: ( C is_closed_on o & Den (o,A) = Den (o,MSAlgebra(# the Sorts of A, the Charact of A #)) ) by A3, MSUALG_2:def_6; thus OAB . o = o /. B by MSUALG_2:def_8 .= (Den (o,A)) | (((B #) * the Arity of S) . o) by A4, MSUALG_2:def_7 .= o /. C by A7, MSUALG_2:def_7 ; ::_thesis: verum end; the Charact of (GenMSAlg AA) = Opers (theA,C) by A2, MSUALG_2:def_9; hence the Charact of (GenMSAlg AA) = Opers (A,B) by A6, MSUALG_2:def_8; ::_thesis: verum end; then reconsider GAA = GenMSAlg AA as strict non-empty MSSubAlgebra of A by A1, MSUALG_2:def_9; reconsider BB = the Sorts of A as MSSubset of A by PBOOLE:def_18; A8: now__::_thesis:_for_U1_being_MSSubAlgebra_of_A_st_BB_is_MSSubset_of_U1_holds_ GAA_is_MSSubAlgebra_of_U1 let U1 be MSSubAlgebra of A; ::_thesis: ( BB is MSSubset of U1 implies GAA is MSSubAlgebra of U1 ) A9: now__::_thesis:_for_B_being_MSSubset_of_theA_st_B_=_the_Sorts_of_U1_holds_ (_B_is_opers_closed_&_the_Charact_of_U1_=_Opers_(theA,B)_) let B be MSSubset of theA; ::_thesis: ( B = the Sorts of U1 implies ( B is opers_closed & the Charact of U1 = Opers (theA,B) ) ) assume A10: B = the Sorts of U1 ; ::_thesis: ( B is opers_closed & the Charact of U1 = Opers (theA,B) ) reconsider C = B as MSSubset of A ; A11: C is opers_closed by A10, MSUALG_2:def_9; A12: now__::_thesis:_for_o_being_OperSymbol_of_S_holds_B_is_closed_on_o let o be OperSymbol of S; ::_thesis: B is_closed_on o C is_closed_on o by A11, MSUALG_2:def_6; then A13: rng ((Den (o,A)) | (((C #) * the Arity of S) . o)) c= (C * the ResultSort of S) . o by MSUALG_2:def_5; Den (o,MSAlgebra(# the Sorts of A, the Charact of A #)) = Den (o,A) ; hence B is_closed_on o by A13, MSUALG_2:def_5; ::_thesis: verum end; hence B is opers_closed by MSUALG_2:def_6; ::_thesis: the Charact of U1 = Opers (theA,B) reconsider OAB = Opers (theA,B) as ManySortedFunction of (C #) * the Arity of S,C * the ResultSort of S ; A14: now__::_thesis:_for_o_being_OperSymbol_of_S_holds_OAB_._o_=_o_/._C let o be OperSymbol of S; ::_thesis: OAB . o = o /. C A15: Den (o,A) = Den (o,MSAlgebra(# the Sorts of A, the Charact of A #)) ; A16: C is_closed_on o by A11, MSUALG_2:def_6; thus OAB . o = o /. B by MSUALG_2:def_8 .= (Den (o,A)) | (((B #) * the Arity of S) . o) by A12, A15, MSUALG_2:def_7 .= o /. C by A16, MSUALG_2:def_7 ; ::_thesis: verum end; the Charact of U1 = Opers (A,C) by A10, MSUALG_2:def_9; hence the Charact of U1 = Opers (theA,B) by A14, MSUALG_2:def_8; ::_thesis: verum end; the Sorts of U1 is MSSubset of MSAlgebra(# the Sorts of A, the Charact of A #) by MSUALG_2:def_9; then reconsider U2 = U1 as MSSubAlgebra of theA by A9, MSUALG_2:def_9; assume BB is MSSubset of U1 ; ::_thesis: GAA is MSSubAlgebra of U1 then GAA is MSSubAlgebra of U2 by MSUALG_2:def_17; hence GAA is MSSubAlgebra of U1 ; ::_thesis: verum end; BB is MSSubset of (GenMSAlg AA) by MSUALG_2:def_17; then GenMSAlg AA = GenMSAlg BB by A8, MSUALG_2:def_17; then the Sorts of (GenMSAlg BB) = the Sorts of A by MSUALG_2:21; hence the Sorts of A is GeneratorSet of A by MSAFREE:def_4; ::_thesis: verum end; definition let S be non empty ManySortedSign ; let IT be MSAlgebra over S; attrIT is finitely-generated means :Def10: :: MSAFREE2:def 10 for S9 being non empty non void ManySortedSign st S9 = S holds for A being MSAlgebra over S9 st A = IT holds ex G being GeneratorSet of A st G is V33() if not S is void otherwise the Sorts of IT is V33(); consistency verum ; end; :: deftheorem Def10 defines finitely-generated MSAFREE2:def_10_:_ for S being non empty ManySortedSign for IT being MSAlgebra over S holds ( ( not S is void implies ( IT is finitely-generated iff for S9 being non empty non void ManySortedSign st S9 = S holds for A being MSAlgebra over S9 st A = IT holds ex G being GeneratorSet of A st G is V33() ) ) & ( S is void implies ( IT is finitely-generated iff the Sorts of IT is V33() ) ) ); definition let S be non empty ManySortedSign ; let IT be MSAlgebra over S; attrIT is finite-yielding means :Def11: :: MSAFREE2:def 11 the Sorts of IT is V33(); end; :: deftheorem Def11 defines finite-yielding MSAFREE2:def_11_:_ for S being non empty ManySortedSign for IT being MSAlgebra over S holds ( IT is finite-yielding iff the Sorts of IT is V33() ); registration let S be non empty ManySortedSign ; cluster non-empty finite-yielding -> non-empty finitely-generated for MSAlgebra over S; coherence for b1 being non-empty MSAlgebra over S st b1 is finite-yielding holds b1 is finitely-generated proof let A be non-empty MSAlgebra over S; ::_thesis: ( A is finite-yielding implies A is finitely-generated ) assume A1: A is finite-yielding ; ::_thesis: A is finitely-generated percases ( not S is void or S is void ) ; :: according to MSAFREE2:def_10 case not S is void ; ::_thesis: for S9 being non empty non void ManySortedSign st S9 = S holds for A being MSAlgebra over S9 st A = A holds ex G being GeneratorSet of A st G is V33() let S9 be non empty non void ManySortedSign ; ::_thesis: ( S9 = S implies for A being MSAlgebra over S9 st A = A holds ex G being GeneratorSet of A st G is V33() ) assume A2: S9 = S ; ::_thesis: for A being MSAlgebra over S9 st A = A holds ex G being GeneratorSet of A st G is V33() let A9 be MSAlgebra over S9; ::_thesis: ( A9 = A implies ex G being GeneratorSet of A9 st G is V33() ) assume A9 = A ; ::_thesis: not for G being GeneratorSet of A9 holds G is V33() then reconsider G = the Sorts of A as GeneratorSet of A9 by A2, Th6; take G ; ::_thesis: G is V33() thus G is V33() by A1, Def11; ::_thesis: verum end; case S is void ; ::_thesis: the Sorts of A is V33() thus the Sorts of A is V33() by A1, Def11; ::_thesis: verum end; end; end; end; definition let S be non empty ManySortedSign ; func Trivial_Algebra S -> strict MSAlgebra over S means :Def12: :: MSAFREE2:def 12 the Sorts of it = the carrier of S --> {0}; existence ex b1 being strict MSAlgebra over S st the Sorts of b1 = the carrier of S --> {0} proof reconsider f = the carrier of S --> {0} as ManySortedSet of the carrier of S ; set Ch = the ManySortedFunction of (f #) * the Arity of S,f * the ResultSort of S; take MSAlgebra(# f, the ManySortedFunction of (f #) * the Arity of S,f * the ResultSort of S #) ; ::_thesis: the Sorts of MSAlgebra(# f, the ManySortedFunction of (f #) * the Arity of S,f * the ResultSort of S #) = the carrier of S --> {0} thus the Sorts of MSAlgebra(# f, the ManySortedFunction of (f #) * the Arity of S,f * the ResultSort of S #) = the carrier of S --> {0} ; ::_thesis: verum end; uniqueness for b1, b2 being strict MSAlgebra over S st the Sorts of b1 = the carrier of S --> {0} & the Sorts of b2 = the carrier of S --> {0} holds b1 = b2 proof let A1, A2 be strict MSAlgebra over S; ::_thesis: ( the Sorts of A1 = the carrier of S --> {0} & the Sorts of A2 = the carrier of S --> {0} implies A1 = A2 ) assume that A1: the Sorts of A1 = the carrier of S --> {0} and A2: the Sorts of A2 = the carrier of S --> {0} ; ::_thesis: A1 = A2 set B = the Sorts of A1; A3: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1; now__::_thesis:_for_i_being_set_st_i_in_the_carrier'_of_S_holds_ the_Charact_of_A1_._i_=_the_Charact_of_A2_._i let i be set ; ::_thesis: ( i in the carrier' of S implies the Charact of A1 . i = the Charact of A2 . i ) set A = ( the Sorts of A1 * the ResultSort of S) . i; assume A4: i in the carrier' of S ; ::_thesis: the Charact of A1 . i = the Charact of A2 . i then A5: ( the Sorts of A1 * the ResultSort of S) . i = the Sorts of A1 . ( the ResultSort of S . i) by A3, FUNCT_1:13 .= {0} by A1, A4, FUNCOP_1:7, FUNCT_2:5 ; then reconsider A = ( the Sorts of A1 * the ResultSort of S) . i as non empty set ; reconsider f1 = the Charact of A1 . i, f2 = the Charact of A2 . i as Function of ((( the Sorts of A1 #) * the Arity of S) . i),A by A1, A2, A4, PBOOLE:def_15; now__::_thesis:_for_x_being_set_st_x_in_((_the_Sorts_of_A1_#)_*_the_Arity_of_S)_._i_holds_ f1_._x_=_f2_._x let x be set ; ::_thesis: ( x in (( the Sorts of A1 #) * the Arity of S) . i implies f1 . x = f2 . x ) assume A6: x in (( the Sorts of A1 #) * the Arity of S) . i ; ::_thesis: f1 . x = f2 . x then f1 . x in A by FUNCT_2:5; then A7: f1 . x = 0 by A5, TARSKI:def_1; f2 . x in A by A6, FUNCT_2:5; hence f1 . x = f2 . x by A5, A7, TARSKI:def_1; ::_thesis: verum end; hence the Charact of A1 . i = the Charact of A2 . i by FUNCT_2:12; ::_thesis: verum end; hence A1 = A2 by A1, A2, PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def12 defines Trivial_Algebra MSAFREE2:def_12_:_ for S being non empty ManySortedSign for b2 being strict MSAlgebra over S holds ( b2 = Trivial_Algebra S iff the Sorts of b2 = the carrier of S --> {0} ); registration let S be non empty ManySortedSign ; cluster strict non-empty finite-yielding for MSAlgebra over S; existence ex b1 being MSAlgebra over S st ( b1 is finite-yielding & b1 is non-empty & b1 is strict ) proof take T = Trivial_Algebra S; ::_thesis: ( T is finite-yielding & T is non-empty & T is strict ) A1: the Sorts of T = the carrier of S --> {0} by Def12; the Sorts of T is V33() proof let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in the carrier of S or the Sorts of T . i is finite ) assume i in the carrier of S ; ::_thesis: the Sorts of T . i is finite hence the Sorts of T . i is finite by A1, FUNCOP_1:7; ::_thesis: verum end; hence T is finite-yielding by Def11; ::_thesis: ( T is non-empty & T is strict ) thus T is non-empty by A1, MSUALG_1:def_3; ::_thesis: T is strict thus T is strict ; ::_thesis: verum end; end; definition let IT be non empty ManySortedSign ; attrIT is monotonic means :: MSAFREE2:def 13 for A being non-empty finitely-generated MSAlgebra over IT holds A is finite-yielding ; end; :: deftheorem defines monotonic MSAFREE2:def_13_:_ for IT being non empty ManySortedSign holds ( IT is monotonic iff for A being non-empty finitely-generated MSAlgebra over IT holds A is finite-yielding ); registration cluster non empty finite non void V55() Circuit-like monotonic for ManySortedSign ; existence ex b1 being non empty ManySortedSign st ( not b1 is void & b1 is finite & b1 is monotonic & b1 is Circuit-like ) proof {} in {{}} * by FINSEQ_1:49; then reconsider f = {[{},{{}}]} --> {} as Function of {[{},{{}}]},({{}} *) by FUNCOP_1:46; reconsider g = {[{},{{}}]} --> {} as Function of {[{},{{}}]},{{}} ; take S = ManySortedSign(# {{}},{[{},{{}}]},f,g #); ::_thesis: ( not S is void & S is finite & S is monotonic & S is Circuit-like ) thus not S is void ; ::_thesis: ( S is finite & S is monotonic & S is Circuit-like ) thus S is finite ; ::_thesis: ( S is monotonic & S is Circuit-like ) thus S is monotonic ::_thesis: S is Circuit-like proof reconsider S9 = S as non empty non void ManySortedSign ; let A be non-empty finitely-generated MSAlgebra over S; :: according to MSAFREE2:def_13 ::_thesis: A is finite-yielding reconsider A9 = A as non-empty MSAlgebra over S9 ; set s = the SortSymbol of S9; consider G being GeneratorSet of A9 such that A1: G is V33() by Def10; reconsider Gs = G . the SortSymbol of S9 as finite set by A1; set o = the OperSymbol of S9; set T = the SortSymbol of S9 .--> ((G . the SortSymbol of S9) \/ {((Den ( the OperSymbol of S9,A9)) . {})}); set O = the OperSymbol of S9 .--> (Den ( the OperSymbol of S9,A9)); reconsider G9 = G as MSSubset of A9 ; let i be set ; :: according to FINSET_1:def_5,MSAFREE2:def_11 ::_thesis: ( not i in the carrier of S or the Sorts of A . i is finite ) A2: the SortSymbol of S9 = {} by TARSKI:def_1; then reconsider T = the SortSymbol of S9 .--> ((G . the SortSymbol of S9) \/ {((Den ( the OperSymbol of S9,A9)) . {})}) as V16() ManySortedSet of the carrier of S ; assume i in the carrier of S ; ::_thesis: the Sorts of A . i is finite then A3: i = the SortSymbol of S9 by A2, TARSKI:def_1; reconsider T9 = T as ManySortedSet of the carrier of S9 ; A4: Args ( the OperSymbol of S9,A9) = ( the Sorts of A9 #) . ( the Arity of S . the OperSymbol of S9) by FUNCT_2:15 .= ( the Sorts of A9 #) . (<*> the carrier of S9) by FUNCOP_1:7 .= {{}} by PRE_CIRC:2 ; then A5: dom (Den ( the OperSymbol of S9,A9)) = {{}} by FUNCT_2:def_1; A6: now__::_thesis:_for_i_being_set_st_i_in_the_carrier'_of_S_holds_ (_the_OperSymbol_of_S9_.-->_(Den_(_the_OperSymbol_of_S9,A9)))_._i_is_Function_of_(((T_#)_*_the_Arity_of_S)_._i),((T_*_the_ResultSort_of_S)_._i) let i be set ; ::_thesis: ( i in the carrier' of S implies ( the OperSymbol of S9 .--> (Den ( the OperSymbol of S9,A9))) . i is Function of (((T #) * the Arity of S) . i),((T * the ResultSort of S) . i) ) assume A7: i in the carrier' of S ; ::_thesis: ( the OperSymbol of S9 .--> (Den ( the OperSymbol of S9,A9))) . i is Function of (((T #) * the Arity of S) . i),((T * the ResultSort of S) . i) then i = [{},{{}}] by TARSKI:def_1; then A8: i = the OperSymbol of S9 by TARSKI:def_1; ((T #) * the Arity of S) . i = (T #) . ( the Arity of S . i) by A7, FUNCT_2:15 .= (T #) . (<*> the carrier of S) by A7, FUNCOP_1:7 .= {{}} by PRE_CIRC:2 ; then reconsider Oi = ( the OperSymbol of S9 .--> (Den ( the OperSymbol of S9,A9))) . i as Function of (((T #) * the Arity of S) . i),(Result ( the OperSymbol of S9,A9)) by A4, A8, FUNCOP_1:72; ( the OperSymbol of S9 .--> (Den ( the OperSymbol of S9,A9))) . i = Den ( the OperSymbol of S9,A9) by A8, FUNCOP_1:72; then A9: rng Oi = {((Den ( the OperSymbol of S9,A9)) . {})} by A5, FUNCT_1:4; (T * the ResultSort of S) . i = T . ( the ResultSort of S . i) by A7, FUNCT_2:15 .= T . the SortSymbol of S9 by A2, A7, FUNCOP_1:7 .= (G . the SortSymbol of S9) \/ {((Den ( the OperSymbol of S9,A9)) . {})} by FUNCOP_1:72 ; then rng Oi c= (T * the ResultSort of S) . i by A9, XBOOLE_1:7; hence ( the OperSymbol of S9 .--> (Den ( the OperSymbol of S9,A9))) . i is Function of (((T #) * the Arity of S) . i),((T * the ResultSort of S) . i) by FUNCT_2:6; ::_thesis: verum end; A10: the OperSymbol of S9 = [{},{{}}] by TARSKI:def_1; then reconsider O = the OperSymbol of S9 .--> (Den ( the OperSymbol of S9,A9)) as ManySortedFunction of (T #) * the Arity of S,T * the ResultSort of S by A6, PBOOLE:def_15; A11: now__::_thesis:_for_B_being_MSSubset_of_A9_st_B_=_the_Sorts_of_MSAlgebra(#_T,O_#)_holds_ (_B_is_opers_closed_&_the_Charact_of_MSAlgebra(#_T,O_#)_=_Opers_(A9,B)_) let B be MSSubset of A9; ::_thesis: ( B = the Sorts of MSAlgebra(# T,O #) implies ( B is opers_closed & the Charact of MSAlgebra(# T,O #) = Opers (A9,B) ) ) assume A12: B = the Sorts of MSAlgebra(# T,O #) ; ::_thesis: ( B is opers_closed & the Charact of MSAlgebra(# T,O #) = Opers (A9,B) ) thus A13: B is opers_closed ::_thesis: the Charact of MSAlgebra(# T,O #) = Opers (A9,B) proof let o9 be OperSymbol of S9; :: according to MSUALG_2:def_6 ::_thesis: B is_closed_on o9 let x be set ; :: according to TARSKI:def_3,MSUALG_2:def_5 ::_thesis: ( not x in rng ((Den (o9,A9)) | (( the Arity of S9 * (B #)) . o9)) or x in ( the ResultSort of S9 * B) . o9 ) assume A14: x in rng ((Den (o9,A9)) | (((B #) * the Arity of S9) . o9)) ; ::_thesis: x in ( the ResultSort of S9 * B) . o9 A15: o9 = the OperSymbol of S9 by A10, TARSKI:def_1; A16: ( dom the ResultSort of S9 = {[{},{{}}]} & the ResultSort of S9 . the OperSymbol of S9 = the SortSymbol of S9 ) by A2, FUNCOP_1:7, FUNCOP_1:13; A17: (Den ( the OperSymbol of S9,A9)) | {{}} = Den ( the OperSymbol of S9,A9) by A5, RELAT_1:68; ((B #) * the Arity of S) . the OperSymbol of S9 = (B #) . ( the Arity of S . the OperSymbol of S9) by FUNCT_2:15 .= (T #) . (<*> the carrier of S) by A12, FUNCOP_1:7 .= {{}} by PRE_CIRC:2 ; then ex y being set st ( y in dom (Den ( the OperSymbol of S9,A9)) & x = (Den ( the OperSymbol of S9,A9)) . y ) by A15, A17, A14, FUNCT_1:def_3; then x = (Den ( the OperSymbol of S9,A9)) . {} by A4, TARSKI:def_1; then A18: x in {((Den ( the OperSymbol of S9,A9)) . {})} by TARSKI:def_1; B . the SortSymbol of S9 = (G . the SortSymbol of S9) \/ {((Den ( the OperSymbol of S9,A9)) . {})} by A12, FUNCOP_1:72; then x in B . the SortSymbol of S9 by A18, XBOOLE_0:def_3; hence x in ( the ResultSort of S9 * B) . o9 by A15, A16, FUNCT_1:13; ::_thesis: verum end; now__::_thesis:_for_o9_being_OperSymbol_of_S9_holds_the_Charact_of_MSAlgebra(#_T,O_#)_._o9_=_o9_/._B let o9 be OperSymbol of S9; ::_thesis: the Charact of MSAlgebra(# T,O #) . o9 = o9 /. B ((B #) * the Arity of S9) . the OperSymbol of S9 = (B #) . ( the Arity of S9 . the OperSymbol of S9) by FUNCT_2:15 .= (T #) . (<*> the carrier of S9) by A12, FUNCOP_1:7 .= {{}} by PRE_CIRC:2 ; then (Den ( the OperSymbol of S9,A9)) | (((B #) * the Arity of S9) . the OperSymbol of S9) = Den ( the OperSymbol of S9,A9) by A5, RELAT_1:68; then A19: the Charact of MSAlgebra(# T,O #) . the OperSymbol of S9 = (Den ( the OperSymbol of S9,A9)) | (((B #) * the Arity of S9) . the OperSymbol of S9) by FUNCOP_1:72; ( o9 = the OperSymbol of S9 & B is_closed_on the OperSymbol of S9 ) by A10, A13, MSUALG_2:def_6, TARSKI:def_1; hence the Charact of MSAlgebra(# T,O #) . o9 = o9 /. B by A19, MSUALG_2:def_7; ::_thesis: verum end; hence the Charact of MSAlgebra(# T,O #) = Opers (A9,B) by A12, MSUALG_2:def_8; ::_thesis: verum end; reconsider A99 = MSAlgebra(# T,O #) as non-empty MSAlgebra over S9 by MSUALG_1:def_3; A20: Result ( the OperSymbol of S9,A9) = the Sorts of A9 . ( the ResultSort of S . the OperSymbol of S9) by FUNCT_2:15 .= the Sorts of A9 . {} by FUNCOP_1:7 ; T9 c= the Sorts of A9 proof let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S9 or T9 . i c= the Sorts of A9 . i ) assume i in the carrier of S9 ; ::_thesis: T9 . i c= the Sorts of A9 . i then A21: i = {} by TARSKI:def_1; then A22: T9 . i = (G . the SortSymbol of S9) \/ {((Den ( the OperSymbol of S9,A9)) . {})} by A2, FUNCOP_1:72; G c= the Sorts of A9 by PBOOLE:def_18; then A23: G . the SortSymbol of S9 c= the Sorts of A9 . i by A2, A21, PBOOLE:def_2; dom (Den ( the OperSymbol of S9,A9)) = Args ( the OperSymbol of S9,A9) by FUNCT_2:def_1; then {} in dom (Den ( the OperSymbol of S9,A9)) by A4, TARSKI:def_1; then (Den ( the OperSymbol of S9,A9)) . {} in rng (Den ( the OperSymbol of S9,A9)) by FUNCT_1:def_3; then {((Den ( the OperSymbol of S9,A9)) . {})} c= the Sorts of A9 . i by A20, A21, ZFMISC_1:31; hence T9 . i c= the Sorts of A9 . i by A22, A23, XBOOLE_1:8; ::_thesis: verum end; then the Sorts of MSAlgebra(# T,O #) is MSSubset of A9 by PBOOLE:def_18; then reconsider A99 = A99 as strict MSSubAlgebra of A9 by A11, MSUALG_2:def_9; A24: now__::_thesis:_for_U1_being_MSSubAlgebra_of_A9_st_G9_is_MSSubset_of_U1_holds_ A99_is_MSSubAlgebra_of_U1 let U1 be MSSubAlgebra of A9; ::_thesis: ( G9 is MSSubset of U1 implies A99 is MSSubAlgebra of U1 ) assume A25: G9 is MSSubset of U1 ; ::_thesis: A99 is MSSubAlgebra of U1 now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S9_holds_ the_Sorts_of_A99_._i_c=_the_Sorts_of_U1_._i Constants A9 is MSSubset of U1 by MSUALG_2:10; then Constants A9 c= the Sorts of U1 by PBOOLE:def_18; then (Constants A9) . the SortSymbol of S9 c= the Sorts of U1 . the SortSymbol of S9 by PBOOLE:def_2; then A26: Constants (A9, the SortSymbol of S9) c= the Sorts of U1 . the SortSymbol of S9 by MSUALG_2:def_4; A27: {} in dom (Den ( the OperSymbol of S9,A9)) by A5, TARSKI:def_1; then (Den ( the OperSymbol of S9,A9)) . {} in rng (Den ( the OperSymbol of S9,A9)) by FUNCT_1:def_3; then reconsider b = (Den ( the OperSymbol of S9,A9)) . {} as Element of the Sorts of A9 . the SortSymbol of S9 by A20, TARSKI:def_1; let i be set ; ::_thesis: ( i in the carrier of S9 implies the Sorts of A99 . i c= the Sorts of U1 . i ) A28: ( the Arity of S9 . the OperSymbol of S9 = {} & ex X being non empty set st ( X = the Sorts of A9 . the SortSymbol of S9 & Constants (A9, the SortSymbol of S9) = { a where a is Element of X : ex o being OperSymbol of S9 st ( the Arity of S9 . o = {} & the ResultSort of S9 . o = the SortSymbol of S9 & a in rng (Den (o,A9)) ) } ) ) by FUNCOP_1:7, MSUALG_2:def_3; b in rng (Den ( the OperSymbol of S9,A9)) by A27, FUNCT_1:def_3; then (Den ( the OperSymbol of S9,A9)) . {} in Constants (A9, the SortSymbol of S9) by A2, A28; then A29: {((Den ( the OperSymbol of S9,A9)) . {})} c= the Sorts of U1 . the SortSymbol of S9 by A26, ZFMISC_1:31; G c= the Sorts of U1 by A25, PBOOLE:def_18; then A30: ( the Sorts of A99 . the SortSymbol of S9 = (G . the SortSymbol of S9) \/ {((Den ( the OperSymbol of S9,A9)) . {})} & G . the SortSymbol of S9 c= the Sorts of U1 . the SortSymbol of S9 ) by FUNCOP_1:72, PBOOLE:def_2; assume i in the carrier of S9 ; ::_thesis: the Sorts of A99 . i c= the Sorts of U1 . i then i = the SortSymbol of S9 by A2, TARSKI:def_1; hence the Sorts of A99 . i c= the Sorts of U1 . i by A30, A29, XBOOLE_1:8; ::_thesis: verum end; then the Sorts of A99 c= the Sorts of U1 by PBOOLE:def_2; hence A99 is MSSubAlgebra of U1 by MSUALG_2:8; ::_thesis: verum end; now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S9_holds_ G9_._i_c=_the_Sorts_of_A99_._i let i be set ; ::_thesis: ( i in the carrier of S9 implies G9 . i c= the Sorts of A99 . i ) assume i in the carrier of S9 ; ::_thesis: G9 . i c= the Sorts of A99 . i then A31: i = the SortSymbol of S9 by A2, TARSKI:def_1; the Sorts of A99 . the SortSymbol of S9 = (G . the SortSymbol of S9) \/ {((Den ( the OperSymbol of S9,A9)) . {})} by FUNCOP_1:72; hence G9 . i c= the Sorts of A99 . i by A31, XBOOLE_1:7; ::_thesis: verum end; then G9 c= the Sorts of A99 by PBOOLE:def_2; then G9 is MSSubset of A99 by PBOOLE:def_18; then the SortSymbol of S9 .--> ((G . the SortSymbol of S9) \/ {((Den ( the OperSymbol of S9,A9)) . {})}) = the Sorts of (GenMSAlg G) by A24, MSUALG_2:def_17 .= the Sorts of A9 by MSAFREE:def_4 ; then the Sorts of A . i = Gs \/ {((Den ( the OperSymbol of S9,A9)) . {})} by A3, FUNCOP_1:72; hence the Sorts of A . i is finite ; ::_thesis: verum end; thus S is Circuit-like ::_thesis: verum proof let S9 be non empty non void ManySortedSign ; :: according to MSAFREE2:def_6 ::_thesis: ( S9 = S implies for o1, o2 being OperSymbol of S9 st the_result_sort_of o1 = the_result_sort_of o2 holds o1 = o2 ) assume A32: S9 = S ; ::_thesis: for o1, o2 being OperSymbol of S9 st the_result_sort_of o1 = the_result_sort_of o2 holds o1 = o2 let o1, o2 be OperSymbol of S9; ::_thesis: ( the_result_sort_of o1 = the_result_sort_of o2 implies o1 = o2 ) assume the_result_sort_of o1 = the_result_sort_of o2 ; ::_thesis: o1 = o2 o1 = [{},{{}}] by A32, TARSKI:def_1; hence o1 = o2 by A32, TARSKI:def_1; ::_thesis: verum end; end; end; theorem Th7: :: MSAFREE2:7 for S being non empty non void ManySortedSign for X being V16() ManySortedSet of the carrier of S for v being SortSymbol of S for e being Element of the Sorts of (FreeMSA X) . v holds e is finite DecoratedTree proof let S be non empty non void ManySortedSign ; ::_thesis: for X being V16() ManySortedSet of the carrier of S for v being SortSymbol of S for e being Element of the Sorts of (FreeMSA X) . v holds e is finite DecoratedTree let X be V16() ManySortedSet of the carrier of S; ::_thesis: for v being SortSymbol of S for e being Element of the Sorts of (FreeMSA X) . v holds e is finite DecoratedTree let v be SortSymbol of S; ::_thesis: for e being Element of the Sorts of (FreeMSA X) . v holds e is finite DecoratedTree let e be Element of the Sorts of (FreeMSA X) . v; ::_thesis: e is finite DecoratedTree FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def_14; then the Sorts of (FreeMSA X) . v = FreeSort (X,v) by MSAFREE:def_11; then A1: e in TS (DTConMSA X) by TARSKI:def_3; then reconsider e9 = e as DecoratedTree ; dom e9 is finite by A1; hence e is finite DecoratedTree by FINSET_1:10; ::_thesis: verum end; theorem :: MSAFREE2:8 for S being non empty non void ManySortedSign for X being V16() V33() ManySortedSet of the carrier of S holds FreeMSA X is finitely-generated proof let S be non empty non void ManySortedSign ; ::_thesis: for X being V16() V33() ManySortedSet of the carrier of S holds FreeMSA X is finitely-generated let X be V16() V33() ManySortedSet of the carrier of S; ::_thesis: FreeMSA X is finitely-generated percases ( not S is void or S is void ) ; :: according to MSAFREE2:def_10 case not S is void ; ::_thesis: for S9 being non empty non void ManySortedSign st S9 = S holds for A being MSAlgebra over S9 st A = FreeMSA X holds ex G being GeneratorSet of A st G is V33() reconsider G = FreeGen X as GeneratorSet of FreeMSA X ; let S9 be non empty non void ManySortedSign ; ::_thesis: ( S9 = S implies for A being MSAlgebra over S9 st A = FreeMSA X holds ex G being GeneratorSet of A st G is V33() ) assume A1: S9 = S ; ::_thesis: for A being MSAlgebra over S9 st A = FreeMSA X holds ex G being GeneratorSet of A st G is V33() let A be MSAlgebra over S9; ::_thesis: ( A = FreeMSA X implies ex G being GeneratorSet of A st G is V33() ) assume A = FreeMSA X ; ::_thesis: not for G being GeneratorSet of A holds G is V33() then reconsider G = G as GeneratorSet of A by A1; take G ; ::_thesis: G is V33() thus G is V33() ::_thesis: verum proof let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in the carrier of S9 or G . i is finite ) reconsider Gi = G . i as set ; assume i in the carrier of S9 ; ::_thesis: G . i is finite then reconsider iS = i as SortSymbol of S by A1; reconsider Xi = X . iS as non empty finite set ; now__::_thesis:_ex_f,_f_being_Function_st_ (_f_is_one-to-one_&_dom_f_=_Gi_&_rng_f_c=_Xi_) defpred S1[ set , set ] means \$1 = root-tree [\$2,i]; A2: for e being set st e in Gi holds ex u being set st ( u in Xi & S1[e,u] ) proof A3: Gi = FreeGen (iS,X) by MSAFREE:def_16; let e be set ; ::_thesis: ( e in Gi implies ex u being set st ( u in Xi & S1[e,u] ) ) assume e in Gi ; ::_thesis: ex u being set st ( u in Xi & S1[e,u] ) then consider u being set such that A4: ( u in Xi & e = root-tree [u,i] ) by A3, MSAFREE:def_15; take u ; ::_thesis: ( u in Xi & S1[e,u] ) thus ( u in Xi & S1[e,u] ) by A4; ::_thesis: verum end; consider f being Function such that A5: dom f = Gi and A6: rng f c= Xi and A7: for e being set st e in Gi holds S1[e,f . e] from FUNCT_1:sch_5(A2); take f = f; ::_thesis: ex f being Function st ( f is one-to-one & dom f = Gi & rng f c= Xi ) f is one-to-one proof let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 ) assume that A8: x1 in dom f and A9: x2 in dom f and A10: f . x1 = f . x2 ; ::_thesis: x1 = x2 thus x1 = root-tree [(f . x2),i] by A5, A7, A8, A10 .= x2 by A5, A7, A9 ; ::_thesis: verum end; hence ex f being Function st ( f is one-to-one & dom f = Gi & rng f c= Xi ) by A5, A6; ::_thesis: verum end; then ( card Gi c= card Xi or card Gi in card Xi ) by CARD_1:10; hence G . i is finite by CARD_2:49; ::_thesis: verum end; end; case S is void ; ::_thesis: the Sorts of (FreeMSA X) is V33() hence the Sorts of (FreeMSA X) is V33() ; ::_thesis: verum end; end; end; theorem :: MSAFREE2:9 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for v being Vertex of S for e being Element of the Sorts of (FreeEnv A) . v st v in InputVertices S holds ex x being Element of the Sorts of A . v st e = root-tree [x,v] proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for v being Vertex of S for e being Element of the Sorts of (FreeEnv A) . v st v in InputVertices S holds ex x being Element of the Sorts of A . v st e = root-tree [x,v] let A be non-empty MSAlgebra over S; ::_thesis: for v being Vertex of S for e being Element of the Sorts of (FreeEnv A) . v st v in InputVertices S holds ex x being Element of the Sorts of A . v st e = root-tree [x,v] let v be Vertex of S; ::_thesis: for e being Element of the Sorts of (FreeEnv A) . v st v in InputVertices S holds ex x being Element of the Sorts of A . v st e = root-tree [x,v] let e be Element of the Sorts of (FreeEnv A) . v; ::_thesis: ( v in InputVertices S implies ex x being Element of the Sorts of A . v st e = root-tree [x,v] ) FreeEnv A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) by MSAFREE:def_14; then e in (FreeSort the Sorts of A) . v ; then e in FreeSort ( the Sorts of A,v) by MSAFREE:def_11; then e in { a where a is Element of TS (DTConMSA the Sorts of A) : ( ex x being set st ( x in the Sorts of A . v & a = root-tree [x,v] ) or ex o being OperSymbol of S st ( [o, the carrier of S] = a . {} & the_result_sort_of o = v ) ) } by MSAFREE:def_10; then consider a being Element of TS (DTConMSA the Sorts of A) such that A1: a = e and A2: ( ex x being set st ( x in the Sorts of A . v & a = root-tree [x,v] ) or ex o being OperSymbol of S st ( [o, the carrier of S] = a . {} & the_result_sort_of o = v ) ) ; assume v in InputVertices S ; ::_thesis: ex x being Element of the Sorts of A . v st e = root-tree [x,v] then consider x being set such that A3: x in the Sorts of A . v and A4: a = root-tree [x,v] by A2, Th2; reconsider x = x as Element of the Sorts of A . v by A3; take x ; ::_thesis: e = root-tree [x,v] thus e = root-tree [x,v] by A1, A4; ::_thesis: verum end; theorem Th10: :: MSAFREE2:10 for S being non empty non void ManySortedSign for X being V16() ManySortedSet of the carrier of S for o being OperSymbol of S for p being DTree-yielding FinSequence st [o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) holds len p = len (the_arity_of o) proof let S be non empty non void ManySortedSign ; ::_thesis: for X being V16() ManySortedSet of the carrier of S for o being OperSymbol of S for p being DTree-yielding FinSequence st [o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) holds len p = len (the_arity_of o) let X be V16() ManySortedSet of the carrier of S; ::_thesis: for o being OperSymbol of S for p being DTree-yielding FinSequence st [o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) holds len p = len (the_arity_of o) let o be OperSymbol of S; ::_thesis: for p being DTree-yielding FinSequence st [o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) holds len p = len (the_arity_of o) let p be DTree-yielding FinSequence; ::_thesis: ( [o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) implies len p = len (the_arity_of o) ) set s = the_result_sort_of o; assume A1: [o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) ; ::_thesis: len p = len (the_arity_of o) FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def_14; then [o, the carrier of S] -tree p in FreeSort (X,(the_result_sort_of o)) by A1, MSAFREE:def_11; then A2: [o, the carrier of S] -tree p in { a where a is Element of TS (DTConMSA X) : ( ex x being set st ( x in X . (the_result_sort_of o) & a = root-tree [x,(the_result_sort_of o)] ) or ex o being OperSymbol of S st ( [o, the carrier of S] = a . {} & the_result_sort_of o = the_result_sort_of o ) ) } by MSAFREE:def_10; the carrier of S in { the carrier of S} by TARSKI:def_1; then [o, the carrier of S] in [: the carrier' of S,{ the carrier of S}:] by ZFMISC_1:87; then reconsider nt = [o, the carrier of S] as NonTerminal of (DTConMSA X) by MSAFREE:6; reconsider O = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) as non empty set ; reconsider R = REL X as Relation of O,(O *) ; A3: DTConMSA X = DTConstrStr(# O,R #) by MSAFREE:def_8; then reconsider TSDT = TS (DTConMSA X) as Subset of (FinTrees O) ; reconsider c = nt as Element of O by A3; for x being set st x in TSDT holds x is DecoratedTree of O ; then reconsider TSDT = TSDT as DTree-set of O by TREES_3:def_6; consider a being Element of TS (DTConMSA X) such that A4: a = [o, the carrier of S] -tree p and ( ex x being set st ( x in X . (the_result_sort_of o) & a = root-tree [x,(the_result_sort_of o)] ) or ex o being OperSymbol of S st ( [o, the carrier of S] = a . {} & the_result_sort_of o = the_result_sort_of o ) ) by A2; a . {} = [o, the carrier of S] by A4, TREES_4:def_4; then consider ts being FinSequence of TS (DTConMSA X) such that A5: a = nt -tree ts and A6: nt ==> roots ts by DTCONSTR:10; reconsider ts9 = ts as FinSequence of TSDT ; reconsider b = roots ts9 as FinSequence of O ; reconsider b = b as Element of O * by FINSEQ_1:def_11; [c,b] in R by A6, A3, LANG1:def_1; then A7: len (roots ts) = len (the_arity_of o) by MSAFREE:def_7; reconsider ts = ts as DTree-yielding FinSequence ; A8: dom (roots ts) = dom ts by TREES_3:def_18; ts = p by A4, A5, TREES_4:15; hence len p = len (the_arity_of o) by A7, A8, FINSEQ_3:29; ::_thesis: verum end; theorem Th11: :: MSAFREE2:11 for S being non empty non void ManySortedSign for X being V16() ManySortedSet of the carrier of S for o being OperSymbol of S for p being DTree-yielding FinSequence st [o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) holds for i being Nat st i in dom (the_arity_of o) holds p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) proof let S be non empty non void ManySortedSign ; ::_thesis: for X being V16() ManySortedSet of the carrier of S for o being OperSymbol of S for p being DTree-yielding FinSequence st [o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) holds for i being Nat st i in dom (the_arity_of o) holds p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) let X be V16() ManySortedSet of the carrier of S; ::_thesis: for o being OperSymbol of S for p being DTree-yielding FinSequence st [o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) holds for i being Nat st i in dom (the_arity_of o) holds p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) let o be OperSymbol of S; ::_thesis: for p being DTree-yielding FinSequence st [o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) holds for i being Nat st i in dom (the_arity_of o) holds p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) let p be DTree-yielding FinSequence; ::_thesis: ( [o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) implies for i being Nat st i in dom (the_arity_of o) holds p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) ) A1: FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def_14; assume A2: [o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) ; ::_thesis: for i being Nat st i in dom (the_arity_of o) holds p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) now__::_thesis:_for_i_being_Nat_st_i_in_dom_(the_arity_of_o)_holds_ p_._i_in_the_Sorts_of_(FreeMSA_X)_._((the_arity_of_o)_._i) the carrier of S in { the carrier of S} by TARSKI:def_1; then [o, the carrier of S] in [: the carrier' of S,{ the carrier of S}:] by ZFMISC_1:87; then reconsider nt = [o, the carrier of S] as NonTerminal of (DTConMSA X) by MSAFREE:6; set rso = the_result_sort_of o; reconsider ao = the_arity_of o as Element of the carrier of S * ; let i be Nat; ::_thesis: ( i in dom (the_arity_of o) implies p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) ) assume A3: i in dom (the_arity_of o) ; ::_thesis: p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) then ao . i in rng ao by FUNCT_1:def_3; then reconsider s = ao . i as SortSymbol of S ; A4: the Sorts of (FreeMSA X) . s = FreeSort (X,s) by A1, MSAFREE:def_11 .= FreeSort (X,((the_arity_of o) /. i)) by A3, PARTFUN1:def_6 ; [o, the carrier of S] -tree p in FreeSort (X,(the_result_sort_of o)) by A2, A1, MSAFREE:def_11; then [o, the carrier of S] -tree p in { a where a is Element of TS (DTConMSA X) : ( ex x being set st ( x in X . (the_result_sort_of o) & a = root-tree [x,(the_result_sort_of o)] ) or ex o being OperSymbol of S st ( [o, the carrier of S] = a . {} & the_result_sort_of o = the_result_sort_of o ) ) } by MSAFREE:def_10; then consider a being Element of TS (DTConMSA X) such that A5: a = [o, the carrier of S] -tree p and ( ex x being set st ( x in X . (the_result_sort_of o) & a = root-tree [x,(the_result_sort_of o)] ) or ex o being OperSymbol of S st ( [o, the carrier of S] = a . {} & the_result_sort_of o = the_result_sort_of o ) ) ; a . {} = [o, the carrier of S] by A5, TREES_4:def_4; then consider ts being FinSequence of TS (DTConMSA X) such that A6: a = nt -tree ts and A7: nt ==> roots ts by DTCONSTR:10; nt = Sym (o,X) by MSAFREE:def_9; then A8: ts in (((FreeSort X) #) * the Arity of S) . o by A7, MSAFREE:10; ( dom p = Seg (len p) & dom (the_arity_of o) = Seg (len (the_arity_of o)) ) by FINSEQ_1:def_3; then A9: i in dom p by A2, A3, Th10; reconsider ts = ts as DTree-yielding FinSequence ; ts = p by A5, A6, TREES_4:15; hence p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) by A9, A8, A4, MSAFREE:9; ::_thesis: verum end; hence for i being Nat st i in dom (the_arity_of o) holds p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) ; ::_thesis: verum end; registration let S be non empty non void ManySortedSign ; let X be V16() ManySortedSet of the carrier of S; let v be Vertex of S; cluster -> non empty Relation-like Function-like finite for Element of the Sorts of (FreeMSA X) . v; coherence for b1 being Element of the Sorts of (FreeMSA X) . v holds ( b1 is finite & not b1 is empty & b1 is Function-like & b1 is Relation-like ) proof let e be Element of the Sorts of (FreeMSA X) . v; ::_thesis: ( e is finite & not e is empty & e is Function-like & e is Relation-like ) reconsider e9 = e as DecoratedTree by Th7; thus e is finite by Th7; ::_thesis: ( not e is empty & e is Function-like & e is Relation-like ) dom e9 is Tree ; hence not e is empty ; ::_thesis: ( e is Function-like & e is Relation-like ) thus ( e is Function-like & e is Relation-like ) by Th7; ::_thesis: verum end; end; registration let S be non empty non void ManySortedSign ; let X be V16() ManySortedSet of the carrier of S; let v be Vertex of S; cluster non empty Relation-like Function-like finite countable for Element of the Sorts of (FreeMSA X) . v; existence ex b1 being Element of the Sorts of (FreeMSA X) . v st ( b1 is Function-like & b1 is Relation-like ) proof set e = the Element of the Sorts of (FreeMSA X) . v; take the Element of the Sorts of (FreeMSA X) . v ; ::_thesis: ( the Element of the Sorts of (FreeMSA X) . v is Function-like & the Element of the Sorts of (FreeMSA X) . v is Relation-like ) thus ( the Element of the Sorts of (FreeMSA X) . v is Function-like & the Element of the Sorts of (FreeMSA X) . v is Relation-like ) ; ::_thesis: verum end; end; registration let S be non empty non void ManySortedSign ; let X be V16() ManySortedSet of the carrier of S; let v be Vertex of S; cluster Relation-like Function-like -> Relation-like Function-like DecoratedTree-like for Element of the Sorts of (FreeMSA X) . v; coherence for b1 being Relation-like Function-like Element of the Sorts of (FreeMSA X) . v holds b1 is DecoratedTree-like by Th7; end; registration let IIG be non empty non void ManySortedSign ; let X be V16() ManySortedSet of the carrier of IIG; let v be Vertex of IIG; cluster non empty Relation-like Function-like finite countable DecoratedTree-like for Element of the Sorts of (FreeMSA X) . v; existence ex b1 being Element of the Sorts of (FreeMSA X) . v st b1 is finite proof set e = the Element of the Sorts of (FreeMSA X) . v; take the Element of the Sorts of (FreeMSA X) . v ; ::_thesis: the Element of the Sorts of (FreeMSA X) . v is finite thus the Element of the Sorts of (FreeMSA X) . v is finite ; ::_thesis: verum end; end; theorem :: MSAFREE2:12 for S being non empty non void ManySortedSign for X being V16() ManySortedSet of the carrier of S for v being Vertex of S for o being OperSymbol of S for e being Element of the Sorts of (FreeMSA X) . v st e . {} = [o, the carrier of S] holds ex p being DTree-yielding FinSequence st ( len p = len (the_arity_of o) & ( for i being Nat st i in dom p holds p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) ) ) proof let S be non empty non void ManySortedSign ; ::_thesis: for X being V16() ManySortedSet of the carrier of S for v being Vertex of S for o being OperSymbol of S for e being Element of the Sorts of (FreeMSA X) . v st e . {} = [o, the carrier of S] holds ex p being DTree-yielding FinSequence st ( len p = len (the_arity_of o) & ( for i being Nat st i in dom p holds p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) ) ) let X be V16() ManySortedSet of the carrier of S; ::_thesis: for v being Vertex of S for o being OperSymbol of S for e being Element of the Sorts of (FreeMSA X) . v st e . {} = [o, the carrier of S] holds ex p being DTree-yielding FinSequence st ( len p = len (the_arity_of o) & ( for i being Nat st i in dom p holds p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) ) ) let v be Vertex of S; ::_thesis: for o being OperSymbol of S for e being Element of the Sorts of (FreeMSA X) . v st e . {} = [o, the carrier of S] holds ex p being DTree-yielding FinSequence st ( len p = len (the_arity_of o) & ( for i being Nat st i in dom p holds p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) ) ) let o be OperSymbol of S; ::_thesis: for e being Element of the Sorts of (FreeMSA X) . v st e . {} = [o, the carrier of S] holds ex p being DTree-yielding FinSequence st ( len p = len (the_arity_of o) & ( for i being Nat st i in dom p holds p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) ) ) let e be Element of the Sorts of (FreeMSA X) . v; ::_thesis: ( e . {} = [o, the carrier of S] implies ex p being DTree-yielding FinSequence st ( len p = len (the_arity_of o) & ( for i being Nat st i in dom p holds p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) ) ) ) assume A1: e . {} = [o, the carrier of S] ; ::_thesis: ex p being DTree-yielding FinSequence st ( len p = len (the_arity_of o) & ( for i being Nat st i in dom p holds p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) ) ) the carrier of S in { the carrier of S} by TARSKI:def_1; then [o, the carrier of S] in [: the carrier' of S,{ the carrier of S}:] by ZFMISC_1:87; then reconsider nt = [o, the carrier of S] as NonTerminal of (DTConMSA X) by MSAFREE:6; FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def_14; then the Sorts of (FreeMSA X) . v = FreeSort (X,v) by MSAFREE:def_11; then e in FreeSort (X,v) ; then e in { a where a is Element of TS (DTConMSA X) : ( ex x being set st ( x in X . v & a = root-tree [x,v] ) or ex o being OperSymbol of S st ( [o, the carrier of S] = a . {} & the_result_sort_of o = v ) ) } by MSAFREE:def_10; then consider a being Element of TS (DTConMSA X) such that A2: a = e and A3: ( ex x being set st ( x in X . v & a = root-tree [x,v] ) or ex o being OperSymbol of S st ( [o, the carrier of S] = a . {} & the_result_sort_of o = v ) ) ; consider x being set such that A4: ( ( x in X . v & a = root-tree [x,v] ) or ex o being OperSymbol of S st ( [o, the carrier of S] = a . {} & the_result_sort_of o = v ) ) by A3; consider p being FinSequence of TS (DTConMSA X) such that A5: a = nt -tree p and nt ==> roots p by A1, A2, DTCONSTR:10; now__::_thesis:_not_a_=_root-tree_[x,v] assume a = root-tree [x,v] ; ::_thesis: contradiction then A6: a . {} = [x,v] by TREES_4:3; A7: for X being set holds not X in X ; a . {} = [o, the carrier of S] by A5, TREES_4:def_4; then the carrier of S = v by A6, XTUPLE_0:1; hence contradiction by A7; ::_thesis: verum end; then consider o9 being OperSymbol of S such that A8: [o9, the carrier of S] = a . {} and A9: the_result_sort_of o9 = v by A4; A10: o = o9 by A1, A2, A8, XTUPLE_0:1; then A11: len p = len (the_arity_of o) by A2, A5, A9, Th10; then dom p = Seg (len (the_arity_of o)) by FINSEQ_1:def_3 .= dom (the_arity_of o) by FINSEQ_1:def_3 ; then for i being Nat st i in dom p holds p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) by A2, A5, A9, A10, Th11; hence ex p being DTree-yielding FinSequence st ( len p = len (the_arity_of o) & ( for i being Nat st i in dom p holds p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) ) ) by A11; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let X be V16() ManySortedSet of the carrier of S; let v be SortSymbol of S; let e be Element of the Sorts of (FreeMSA X) . v; func depth e -> Nat means :: MSAFREE2:def 14 ex dt being finite DecoratedTree ex t being finite Tree st ( dt = e & t = dom dt & it = height t ); existence ex b1 being Nat ex dt being finite DecoratedTree ex t being finite Tree st ( dt = e & t = dom dt & b1 = height t ) proof reconsider dt = e as finite DecoratedTree ; reconsider domdt = dom dt as finite Tree ; take height domdt ; ::_thesis: ex dt being finite DecoratedTree ex t being finite Tree st ( dt = e & t = dom dt & height domdt = height t ) take dt ; ::_thesis: ex t being finite Tree st ( dt = e & t = dom dt & height domdt = height t ) take domdt ; ::_thesis: ( dt = e & domdt = dom dt & height domdt = height domdt ) thus ( dt = e & domdt = dom dt & height domdt = height domdt ) ; ::_thesis: verum end; uniqueness for b1, b2 being Nat st ex dt being finite DecoratedTree ex t being finite Tree st ( dt = e & t = dom dt & b1 = height t ) & ex dt being finite DecoratedTree ex t being finite Tree st ( dt = e & t = dom dt & b2 = height t ) holds b1 = b2 ; end; :: deftheorem defines depth MSAFREE2:def_14_:_ for S being non empty non void ManySortedSign for X being V16() ManySortedSet of the carrier of S for v being SortSymbol of S for e being Element of the Sorts of (FreeMSA X) . v for b5 being Nat holds ( b5 = depth e iff ex dt being finite DecoratedTree ex t being finite Tree st ( dt = e & t = dom dt & b5 = height t ) );