begin
:: 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 = {} ) );
:: 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
theorem Th2:
theorem
canceled;
theorem
canceled;
theorem Th5:
theorem
:: deftheorem Def4 defines with_input_V MSAFREE2:def 4 :
for IT being non empty ManySortedSign holds
( IT is with_input_V iff InputVertices IT <> {} );
:: deftheorem defines InputValues MSAFREE2:def 5 :
for S being non empty ManySortedSign
for MSA being non-empty MSAlgebra of 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 );
:: 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 );
:: 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
:: deftheorem defines FreeEnv MSAFREE2:def 8 :
for S being non empty non void ManySortedSign
for MSA being non-empty MSAlgebra of S holds FreeEnv MSA = FreeMSA the Sorts of MSA;
definition
let S be non
empty non
void ManySortedSign ;
let MSA be
non-empty MSAlgebra of
S;
func Eval MSA -> ManySortedFunction of
(FreeEnv MSA),
MSA means
(
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 ) )
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
end;
:: deftheorem defines Eval MSAFREE2:def 9 :
for S being non empty non void ManySortedSign
for MSA being non-empty MSAlgebra of 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
canceled;
theorem Th9:
:: deftheorem Def10 defines finitely-generated MSAFREE2:def 10 :
for S being non empty ManySortedSign
for IT being MSAlgebra of 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 of S9 st A = IT holds
ex G being GeneratorSet of A st G is finite-yielding ) ) & ( S is void implies ( IT is finitely-generated iff the Sorts of IT is finite-yielding ) ) );
:: deftheorem Def11 defines finite-yielding MSAFREE2:def 11 :
for S being non empty ManySortedSign
for IT being MSAlgebra of S holds
( IT is finite-yielding iff the Sorts of IT is finite-yielding );
:: deftheorem Def12 defines Trivial_Algebra MSAFREE2:def 12 :
for S being non empty ManySortedSign
for b2 being strict MSAlgebra of S holds
( b2 = Trivial_Algebra S iff the Sorts of b2 = the carrier of S --> {0} );
:: 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 of IT holds A is finite-yielding );
theorem Th10:
theorem
theorem
theorem Th13:
theorem Th14:
theorem
:: 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 ) );