:: 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 ) );