begin
:: deftheorem Def1 defines SortsWithConstants MSAFREE2:def 1 :
:: deftheorem defines InputVertices MSAFREE2:def 2 :
:: deftheorem defines InnerVertices MSAFREE2:def 3 :
theorem
theorem Th2:
theorem
canceled;
theorem
canceled;
theorem Th5:
theorem
:: deftheorem Def4 defines with_input_V MSAFREE2:def 4 :
:: deftheorem defines InputValues MSAFREE2:def 5 :
:: deftheorem Def6 defines Circuit-like MSAFREE2:def 6 :
:: deftheorem defines action_at MSAFREE2:def 7 :
begin
theorem
:: deftheorem defines FreeEnv MSAFREE2:def 8 :
definition
let S be non
empty non
void ManySortedSign ;
let MSA be
non-empty MSAlgebra of
S;
func Eval MSA -> ManySortedFunction of ,
(FreeEnv MSA) means
(
it is_homomorphism FreeEnv MSA,
MSA & ( for
s being
SortSymbol of
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) st
( b1 is_homomorphism FreeEnv MSA,MSA & ( for s being SortSymbol of
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) st b1 is_homomorphism FreeEnv MSA,MSA & ( for s being SortSymbol of
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
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 :
theorem
canceled;
theorem Th9:
:: deftheorem Def10 defines finitely-generated MSAFREE2:def 10 :
:: deftheorem Def11 defines finite-yielding MSAFREE2:def 11 :
:: deftheorem Def12 defines Trivial_Algebra MSAFREE2:def 12 :
:: deftheorem defines monotonic MSAFREE2:def 13 :
theorem Th10:
theorem
theorem
theorem Th13:
theorem Th14:
theorem
:: deftheorem defines depth MSAFREE2:def 14 :