:: by Beata Perkowska

::

:: Received April 27, 1994

:: Copyright (c) 1994-2012 Association of Mizar Users

begin

theorem Th1: :: MSAFREE:1

for I being set

for J being non empty set

for f being Function of I,(J *)

for X being ManySortedSet of J

for p being Element of J *

for x being set st x in I & p = f . x holds

((X #) * f) . x = product (X * p)

for J being non empty set

for f being Function of I,(J *)

for X being ManySortedSet of J

for p being Element of J *

for x being set st x in I & p = f . x holds

((X #) * f) . x = product (X * p)

proof end;

definition

let I be set ;

let A, B be ManySortedSet of I;

let C be ManySortedSubset of A;

let F be ManySortedFunction of A,B;

ex b_{1} being ManySortedFunction of C,B st

for i being set st i in I holds

for f being Function of (A . i),(B . i) st f = F . i holds

b_{1} . i = f | (C . i)

for b_{1}, b_{2} being ManySortedFunction of C,B st ( for i being set st i in I holds

for f being Function of (A . i),(B . i) st f = F . i holds

b_{1} . i = f | (C . i) ) & ( for i being set st i in I holds

for f being Function of (A . i),(B . i) st f = F . i holds

b_{2} . i = f | (C . i) ) holds

b_{1} = b_{2}

end;
let A, B be ManySortedSet of I;

let C be ManySortedSubset of A;

let F be ManySortedFunction of A,B;

func F || C -> ManySortedFunction of C,B means :Def1: :: MSAFREE:def 1

for i being set st i in I holds

for f being Function of (A . i),(B . i) st f = F . i holds

it . i = f | (C . i);

existence for i being set st i in I holds

for f being Function of (A . i),(B . i) st f = F . i holds

it . i = f | (C . i);

ex b

for i being set st i in I holds

for f being Function of (A . i),(B . i) st f = F . i holds

b

proof end;

uniqueness for b

for f being Function of (A . i),(B . i) st f = F . i holds

b

for f being Function of (A . i),(B . i) st f = F . i holds

b

b

proof end;

:: deftheorem Def1 defines || MSAFREE:def 1 :

for I being set

for A, B being ManySortedSet of I

for C being ManySortedSubset of A

for F being ManySortedFunction of A,B

for b_{6} being ManySortedFunction of C,B holds

( b_{6} = F || C iff for i being set st i in I holds

for f being Function of (A . i),(B . i) st f = F . i holds

b_{6} . i = f | (C . i) );

for I being set

for A, B being ManySortedSet of I

for C being ManySortedSubset of A

for F being ManySortedFunction of A,B

for b

( b

for f being Function of (A . i),(B . i) st f = F . i holds

b

definition

let I be set ;

let X be ManySortedSet of I;

let i be set ;

assume A1: i in I ;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ex a being set st

( a in X . i & x = [a,i] ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ex a being set st

( a in X . i & x = [a,i] ) ) ) & ( for x being set holds

( x in b_{2} iff ex a being set st

( a in X . i & x = [a,i] ) ) ) holds

b_{1} = b_{2}

end;
let X be ManySortedSet of I;

let i be set ;

assume A1: i in I ;

func coprod (i,X) -> set means :Def2: :: MSAFREE:def 2

for x being set holds

( x in it iff ex a being set st

( a in X . i & x = [a,i] ) );

existence for x being set holds

( x in it iff ex a being set st

( a in X . i & x = [a,i] ) );

ex b

for x being set holds

( x in b

( a in X . i & x = [a,i] ) )

proof end;

uniqueness for b

( x in b

( a in X . i & x = [a,i] ) ) ) & ( for x being set holds

( x in b

( a in X . i & x = [a,i] ) ) ) holds

b

proof end;

:: deftheorem Def2 defines coprod MSAFREE:def 2 :

for I being set

for X being ManySortedSet of I

for i being set st i in I holds

for b_{4} being set holds

( b_{4} = coprod (i,X) iff for x being set holds

( x in b_{4} iff ex a being set st

( a in X . i & x = [a,i] ) ) );

for I being set

for X being ManySortedSet of I

for i being set st i in I holds

for b

( b

( x in b

( a in X . i & x = [a,i] ) ) );

registration
end;

definition

let I be set ;

let X be ManySortedSet of I;

for b_{1} being set holds

( b_{1} = coprod iff ( dom b_{1} = I & ( for i being set st i in I holds

b_{1} . i = coprod (i,X) ) ) )

end;
let X be ManySortedSet of I;

:: original: coprod

redefine func coprod X -> set means :Def3: :: MSAFREE:def 3

( dom it = I & ( for i being set st i in I holds

it . i = coprod (i,X) ) );

compatibility redefine func coprod X -> set means :Def3: :: MSAFREE:def 3

( dom it = I & ( for i being set st i in I holds

it . i = coprod (i,X) ) );

for b

( b

b

proof end;

:: deftheorem Def3 defines coprod MSAFREE:def 3 :

for I being set

for X being ManySortedSet of I

for b_{3} being set holds

( b_{3} = coprod X iff ( dom b_{3} = I & ( for i being set st i in I holds

b_{3} . i = coprod (i,X) ) ) );

for I being set

for X being ManySortedSet of I

for b

( b

b

registration

let I be non empty set ;

let X be V16() ManySortedSet of I;

coherence

coprod X is non-empty

end;
let X be V16() ManySortedSet of I;

coherence

coprod X is non-empty

proof end;

registration

let I be non empty set ;

let X be V16() ManySortedSet of I;

coherence

not Union X is empty

end;
let X be V16() ManySortedSet of I;

coherence

not Union X is empty

proof end;

theorem :: MSAFREE:2

for I being set

for X being ManySortedSet of I

for i being set st i in I holds

( X . i <> {} iff (coprod X) . i <> {} )

for X being ManySortedSet of I

for i being set st i in I holds

( X . i <> {} iff (coprod X) . i <> {} )

proof end;

begin

definition

let S be non empty non void ManySortedSign ;

let U0 be MSAlgebra over S;

ex b_{1} being MSSubset of U0 st the Sorts of (GenMSAlg b_{1}) = the Sorts of U0

end;
let U0 be MSAlgebra over S;

mode GeneratorSet of U0 -> MSSubset of U0 means :Def4: :: MSAFREE:def 4

the Sorts of (GenMSAlg it) = the Sorts of U0;

existence the Sorts of (GenMSAlg it) = the Sorts of U0;

ex b

proof end;

:: deftheorem Def4 defines GeneratorSet MSAFREE:def 4 :

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for b_{3} being MSSubset of U0 holds

( b_{3} is GeneratorSet of U0 iff the Sorts of (GenMSAlg b_{3}) = the Sorts of U0 );

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for b

( b

theorem :: MSAFREE:3

for S being non empty non void ManySortedSign

for U0 being strict non-empty MSAlgebra over S

for A being MSSubset of U0 holds

( A is GeneratorSet of U0 iff GenMSAlg A = U0 )

for U0 being strict non-empty MSAlgebra over S

for A being MSSubset of U0 holds

( A is GeneratorSet of U0 iff GenMSAlg A = U0 )

proof end;

definition

let S be non empty non void ManySortedSign ;

let U0 be MSAlgebra over S;

let IT be GeneratorSet of U0;

end;
let U0 be MSAlgebra over S;

let IT be GeneratorSet of U0;

attr IT is free means :Def5: :: MSAFREE:def 5

for U1 being non-empty MSAlgebra over S

for f being ManySortedFunction of IT, the Sorts of U1 ex h being ManySortedFunction of U0,U1 st

( h is_homomorphism U0,U1 & h || IT = f );

for U1 being non-empty MSAlgebra over S

for f being ManySortedFunction of IT, the Sorts of U1 ex h being ManySortedFunction of U0,U1 st

( h is_homomorphism U0,U1 & h || IT = f );

:: deftheorem Def5 defines free MSAFREE:def 5 :

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for IT being GeneratorSet of U0 holds

( IT is free iff for U1 being non-empty MSAlgebra over S

for f being ManySortedFunction of IT, the Sorts of U1 ex h being ManySortedFunction of U0,U1 st

( h is_homomorphism U0,U1 & h || IT = f ) );

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for IT being GeneratorSet of U0 holds

( IT is free iff for U1 being non-empty MSAlgebra over S

for f being ManySortedFunction of IT, the Sorts of U1 ex h being ManySortedFunction of U0,U1 st

( h is_homomorphism U0,U1 & h || IT = f ) );

:: deftheorem Def6 defines free MSAFREE:def 6 :

for S being non empty non void ManySortedSign

for IT being MSAlgebra over S holds

( IT is free iff ex G being GeneratorSet of IT st G is free );

for S being non empty non void ManySortedSign

for IT being MSAlgebra over S holds

( IT is free iff ex G being GeneratorSet of IT st G is free );

theorem Th4: :: MSAFREE:4

for S being non empty non void ManySortedSign

for X being ManySortedSet of the carrier of S holds Union (coprod X) misses [: the carrier' of S,{ the carrier of S}:]

for X being ManySortedSet of the carrier of S holds Union (coprod X) misses [: the carrier' of S,{ the carrier of S}:]

proof end;

begin

::

:: Construction of Free Many Sorted Algebras for Given Signature

::

:: Construction of Free Many Sorted Algebras for Given Signature

::

definition

let S be non empty non void ManySortedSign ;

let X be ManySortedSet of the carrier of S;

ex b_{1} being Relation of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *) st

for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))

for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds

( [a,b] in b_{1} iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds

( len b = len (the_arity_of o) & ( for x being set st x in dom b holds

( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds

the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) )

for b_{1}, b_{2} being Relation of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *) st ( for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))

for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds

( [a,b] in b_{1} iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds

( len b = len (the_arity_of o) & ( for x being set st x in dom b holds

( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds

the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) ) ) & ( for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))

for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds

( [a,b] in b_{2} iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds

( len b = len (the_arity_of o) & ( for x being set st x in dom b holds

( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds

the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) ) ) holds

b_{1} = b_{2}

end;
let X be ManySortedSet of the carrier of S;

func REL X -> Relation of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *) means :Def7: :: MSAFREE:def 7

for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))

for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds

( [a,b] in it iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds

( len b = len (the_arity_of o) & ( for x being set st x in dom b holds

( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds

the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) );

existence for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))

for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds

( [a,b] in it iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds

( len b = len (the_arity_of o) & ( for x being set st x in dom b holds

( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds

the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) );

ex b

for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))

for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds

( [a,b] in b

( len b = len (the_arity_of o) & ( for x being set st x in dom b holds

( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds

the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) )

proof end;

uniqueness for b

for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds

( [a,b] in b

( len b = len (the_arity_of o) & ( for x being set st x in dom b holds

( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds

the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) ) ) & ( for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))

for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds

( [a,b] in b

( len b = len (the_arity_of o) & ( for x being set st x in dom b holds

( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds

the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) ) ) holds

b

proof end;

:: deftheorem Def7 defines REL MSAFREE:def 7 :

for S being non empty non void ManySortedSign

for X being ManySortedSet of the carrier of S

for b_{3} being Relation of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *) holds

( b_{3} = REL X iff for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))

for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds

( [a,b] in b_{3} iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds

( len b = len (the_arity_of o) & ( for x being set st x in dom b holds

( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds

the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) ) );

for S being non empty non void ManySortedSign

for X being ManySortedSet of the carrier of S

for b

( b

for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds

( [a,b] in b

( len b = len (the_arity_of o) & ( for x being set st x in dom b holds

( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds

the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) ) );

theorem Th5: :: MSAFREE:5

for S being non empty non void ManySortedSign

for X being ManySortedSet of the carrier of S

for o being OperSymbol of S

for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds

( [[o, the carrier of S],b] in REL X iff ( len b = len (the_arity_of o) & ( for x being set st x in dom b holds

( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds

the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) )

for X being ManySortedSet of the carrier of S

for o being OperSymbol of S

for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds

( [[o, the carrier of S],b] in REL X iff ( len b = len (the_arity_of o) & ( for x being set st x in dom b holds

( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds

the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) )

proof end;

definition

let S be non empty non void ManySortedSign ;

let X be ManySortedSet of the carrier of S;

coherence

DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(REL X) #) is DTConstrStr ;

;

end;
let X be ManySortedSet of the carrier of S;

func DTConMSA X -> DTConstrStr equals :: MSAFREE:def 8

DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(REL X) #);

correctness DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(REL X) #);

coherence

DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(REL X) #) is DTConstrStr ;

;

:: deftheorem defines DTConMSA MSAFREE:def 8 :

for S being non empty non void ManySortedSign

for X being ManySortedSet of the carrier of S holds DTConMSA X = DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(REL X) #);

for S being non empty non void ManySortedSign

for X being ManySortedSet of the carrier of S holds DTConMSA X = DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(REL X) #);

registration

let S be non empty non void ManySortedSign ;

let X be ManySortedSet of the carrier of S;

coherence

( DTConMSA X is strict & not DTConMSA X is empty ) ;

end;
let X be ManySortedSet of the carrier of S;

coherence

( DTConMSA X is strict & not DTConMSA X is empty ) ;

theorem Th6: :: MSAFREE:6

for S being non empty non void ManySortedSign

for X being ManySortedSet of the carrier of S holds

( NonTerminals (DTConMSA X) c= [: the carrier' of S,{ the carrier of S}:] & Union (coprod X) c= Terminals (DTConMSA X) & ( X is V16() implies ( NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConMSA X) = Union (coprod X) ) ) )

for X being ManySortedSet of the carrier of S holds

( NonTerminals (DTConMSA X) c= [: the carrier' of S,{ the carrier of S}:] & Union (coprod X) c= Terminals (DTConMSA X) & ( X is V16() implies ( NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConMSA X) = Union (coprod X) ) ) )

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V16() ManySortedSet of the carrier of S;

coherence

( DTConMSA X is with_terminals & DTConMSA X is with_nonterminals & DTConMSA X is with_useful_nonterminals )

end;
let X be V16() ManySortedSet of the carrier of S;

coherence

( DTConMSA X is with_terminals & DTConMSA X is with_nonterminals & DTConMSA X is with_useful_nonterminals )

proof end;

theorem Th7: :: MSAFREE:7

for S being non empty non void ManySortedSign

for X being ManySortedSet of the carrier of S

for t being set holds

( ( t in Terminals (DTConMSA X) & X is V16() implies ex s being SortSymbol of S ex x being set st

( x in X . s & t = [x,s] ) ) & ( for s being SortSymbol of S

for x being set st x in X . s holds

[x,s] in Terminals (DTConMSA X) ) )

for X being ManySortedSet of the carrier of S

for t being set holds

( ( t in Terminals (DTConMSA X) & X is V16() implies ex s being SortSymbol of S ex x being set st

( x in X . s & t = [x,s] ) ) & ( for s being SortSymbol of S

for x being set st x in X . s holds

[x,s] in Terminals (DTConMSA X) ) )

proof end;

definition

let S be non empty non void ManySortedSign ;

let X be V16() ManySortedSet of the carrier of S;

let o be OperSymbol of S;

coherence

[o, the carrier of S] is Symbol of (DTConMSA X)

end;
let X be V16() ManySortedSet of the carrier of S;

let o be OperSymbol of S;

coherence

[o, the carrier of S] is Symbol of (DTConMSA X)

proof end;

:: deftheorem defines Sym MSAFREE:def 9 :

for S being non empty non void ManySortedSign

for X being V16() ManySortedSet of the carrier of S

for o being OperSymbol of S holds Sym (o,X) = [o, the carrier of S];

for S being non empty non void ManySortedSign

for X being V16() ManySortedSet of the carrier of S

for o being OperSymbol of S holds Sym (o,X) = [o, the carrier of S];

definition

let S be non empty non void ManySortedSign ;

let X be V16() ManySortedSet of the carrier of S;

let s be SortSymbol of S;

{ a where a is Element of TS (DTConMSA X) : ( ex x being set st

( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) ) } is Subset of (TS (DTConMSA X))

end;
let X be V16() ManySortedSet of the carrier of S;

let s be SortSymbol of S;

func FreeSort (X,s) -> Subset of (TS (DTConMSA X)) equals :: MSAFREE:def 10

{ a where a is Element of TS (DTConMSA X) : ( ex x being set st

( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) ) } ;

coherence { a where a is Element of TS (DTConMSA X) : ( ex x being set st

( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) ) } ;

{ a where a is Element of TS (DTConMSA X) : ( ex x being set st

( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) ) } is Subset of (TS (DTConMSA X))

proof end;

:: deftheorem defines FreeSort MSAFREE:def 10 :

for S being non empty non void ManySortedSign

for X being V16() ManySortedSet of the carrier of S

for s being SortSymbol of S holds FreeSort (X,s) = { a where a is Element of TS (DTConMSA X) : ( ex x being set st

( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) ) } ;

for S being non empty non void ManySortedSign

for X being V16() ManySortedSet of the carrier of S

for s being SortSymbol of S holds FreeSort (X,s) = { a where a is Element of TS (DTConMSA X) : ( ex x being set st

( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) ) } ;

registration

let S be non empty non void ManySortedSign ;

let X be V16() ManySortedSet of the carrier of S;

let s be SortSymbol of S;

coherence

not FreeSort (X,s) is empty

end;
let X be V16() ManySortedSet of the carrier of S;

let s be SortSymbol of S;

coherence

not FreeSort (X,s) is empty

proof end;

definition

let S be non empty non void ManySortedSign ;

let X be V16() ManySortedSet of the carrier of S;

ex b_{1} being ManySortedSet of the carrier of S st

for s being SortSymbol of S holds b_{1} . s = FreeSort (X,s)

for b_{1}, b_{2} being ManySortedSet of the carrier of S st ( for s being SortSymbol of S holds b_{1} . s = FreeSort (X,s) ) & ( for s being SortSymbol of S holds b_{2} . s = FreeSort (X,s) ) holds

b_{1} = b_{2}

end;
let X be V16() ManySortedSet of the carrier of S;

func FreeSort X -> ManySortedSet of the carrier of S means :Def11: :: MSAFREE:def 11

for s being SortSymbol of S holds it . s = FreeSort (X,s);

existence for s being SortSymbol of S holds it . s = FreeSort (X,s);

ex b

for s being SortSymbol of S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def11 defines FreeSort MSAFREE:def 11 :

for S being non empty non void ManySortedSign

for X being V16() ManySortedSet of the carrier of S

for b_{3} being ManySortedSet of the carrier of S holds

( b_{3} = FreeSort X iff for s being SortSymbol of S holds b_{3} . s = FreeSort (X,s) );

for S being non empty non void ManySortedSign

for X being V16() ManySortedSet of the carrier of S

for b

( b

registration

let S be non empty non void ManySortedSign ;

let X be V16() ManySortedSet of the carrier of S;

coherence

FreeSort X is non-empty

end;
let X be V16() ManySortedSet of the carrier of S;

coherence

FreeSort X is non-empty

proof end;

theorem Th8: :: MSAFREE:8

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 x being set st x in (((FreeSort X) #) * the Arity of S) . o holds

x is FinSequence of TS (DTConMSA X)

for X being V16() ManySortedSet of the carrier of S

for o being OperSymbol of S

for x being set st x in (((FreeSort X) #) * the Arity of S) . o holds

x is FinSequence of TS (DTConMSA X)

proof end;

theorem Th9: :: MSAFREE:9

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 FinSequence of TS (DTConMSA X) holds

( p in (((FreeSort X) #) * the Arity of S) . o iff ( dom p = dom (the_arity_of o) & ( for n being Nat st n in dom p holds

p . n in FreeSort (X,((the_arity_of o) /. n)) ) ) )

for X being V16() ManySortedSet of the carrier of S

for o being OperSymbol of S

for p being FinSequence of TS (DTConMSA X) holds

( p in (((FreeSort X) #) * the Arity of S) . o iff ( dom p = dom (the_arity_of o) & ( for n being Nat st n in dom p holds

p . n in FreeSort (X,((the_arity_of o) /. n)) ) ) )

proof end;

theorem Th10: :: MSAFREE: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 FinSequence of TS (DTConMSA X) holds

( Sym (o,X) ==> roots p iff p in (((FreeSort X) #) * the Arity of S) . o )

for X being V16() ManySortedSet of the carrier of S

for o being OperSymbol of S

for p being FinSequence of TS (DTConMSA X) holds

( Sym (o,X) ==> roots p iff p in (((FreeSort X) #) * the Arity of S) . o )

proof end;

theorem Th11: :: MSAFREE:11

for S being non empty non void ManySortedSign

for X being V16() ManySortedSet of the carrier of S holds union (rng (FreeSort X)) = TS (DTConMSA X)

for X being V16() ManySortedSet of the carrier of S holds union (rng (FreeSort X)) = TS (DTConMSA X)

proof end;

theorem Th12: :: MSAFREE:12

for S being non empty non void ManySortedSign

for X being V16() ManySortedSet of the carrier of S

for s1, s2 being SortSymbol of S st s1 <> s2 holds

(FreeSort X) . s1 misses (FreeSort X) . s2

for X being V16() ManySortedSet of the carrier of S

for s1, s2 being SortSymbol of S st s1 <> s2 holds

(FreeSort X) . s1 misses (FreeSort X) . s2

proof end;

definition

let S be non empty non void ManySortedSign ;

let X be V16() ManySortedSet of the carrier of S;

let o be OperSymbol of S;

ex b_{1} being Function of ((((FreeSort X) #) * the Arity of S) . o),(((FreeSort X) * the ResultSort of S) . o) st

for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds

b_{1} . p = (Sym (o,X)) -tree p

for b_{1}, b_{2} being Function of ((((FreeSort X) #) * the Arity of S) . o),(((FreeSort X) * the ResultSort of S) . o) st ( for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds

b_{1} . p = (Sym (o,X)) -tree p ) & ( for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds

b_{2} . p = (Sym (o,X)) -tree p ) holds

b_{1} = b_{2}

end;
let X be V16() ManySortedSet of the carrier of S;

let o be OperSymbol of S;

func DenOp (o,X) -> Function of ((((FreeSort X) #) * the Arity of S) . o),(((FreeSort X) * the ResultSort of S) . o) means :Def12: :: MSAFREE:def 12

for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds

it . p = (Sym (o,X)) -tree p;

existence for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds

it . p = (Sym (o,X)) -tree p;

ex b

for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def12 defines DenOp MSAFREE:def 12 :

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 b_{4} being Function of ((((FreeSort X) #) * the Arity of S) . o),(((FreeSort X) * the ResultSort of S) . o) holds

( b_{4} = DenOp (o,X) iff for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds

b_{4} . p = (Sym (o,X)) -tree p );

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 b

( b

b

definition

let S be non empty non void ManySortedSign ;

let X be V16() ManySortedSet of the carrier of S;

ex b_{1} being ManySortedFunction of ((FreeSort X) #) * the Arity of S,(FreeSort X) * the ResultSort of S st

for o being OperSymbol of S holds b_{1} . o = DenOp (o,X)

for b_{1}, b_{2} being ManySortedFunction of ((FreeSort X) #) * the Arity of S,(FreeSort X) * the ResultSort of S st ( for o being OperSymbol of S holds b_{1} . o = DenOp (o,X) ) & ( for o being OperSymbol of S holds b_{2} . o = DenOp (o,X) ) holds

b_{1} = b_{2}

end;
let X be V16() ManySortedSet of the carrier of S;

func FreeOper X -> ManySortedFunction of ((FreeSort X) #) * the Arity of S,(FreeSort X) * the ResultSort of S means :Def13: :: MSAFREE:def 13

for o being OperSymbol of S holds it . o = DenOp (o,X);

existence for o being OperSymbol of S holds it . o = DenOp (o,X);

ex b

for o being OperSymbol of S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def13 defines FreeOper MSAFREE:def 13 :

for S being non empty non void ManySortedSign

for X being V16() ManySortedSet of the carrier of S

for b_{3} being ManySortedFunction of ((FreeSort X) #) * the Arity of S,(FreeSort X) * the ResultSort of S holds

( b_{3} = FreeOper X iff for o being OperSymbol of S holds b_{3} . o = DenOp (o,X) );

for S being non empty non void ManySortedSign

for X being V16() ManySortedSet of the carrier of S

for b

( b

definition

let S be non empty non void ManySortedSign ;

let X be V16() ManySortedSet of the carrier of S;

MSAlgebra(# (FreeSort X),(FreeOper X) #) is MSAlgebra over S ;

end;
let X be V16() ManySortedSet of the carrier of S;

func FreeMSA X -> MSAlgebra over S equals :: MSAFREE:def 14

MSAlgebra(# (FreeSort X),(FreeOper X) #);

coherence MSAlgebra(# (FreeSort X),(FreeOper X) #);

MSAlgebra(# (FreeSort X),(FreeOper X) #) is MSAlgebra over S ;

:: deftheorem defines FreeMSA MSAFREE:def 14 :

for S being non empty non void ManySortedSign

for X being V16() ManySortedSet of the carrier of S holds FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #);

for S being non empty non void ManySortedSign

for X being V16() ManySortedSet of the carrier of S holds FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #);

registration

let S be non empty non void ManySortedSign ;

let X be V16() ManySortedSet of the carrier of S;

coherence

( FreeMSA X is strict & FreeMSA X is non-empty ) by MSUALG_1:def 3;

end;
let X be V16() ManySortedSet of the carrier of S;

coherence

( FreeMSA X is strict & FreeMSA X is non-empty ) by MSUALG_1:def 3;

definition

let S be non empty non void ManySortedSign ;

let X be V16() ManySortedSet of the carrier of S;

let s be SortSymbol of S;

ex b_{1} being Subset of ((FreeSort X) . s) st

for x being set holds

( x in b_{1} iff ex a being set st

( a in X . s & x = root-tree [a,s] ) )

for b_{1}, b_{2} being Subset of ((FreeSort X) . s) st ( for x being set holds

( x in b_{1} iff ex a being set st

( a in X . s & x = root-tree [a,s] ) ) ) & ( for x being set holds

( x in b_{2} iff ex a being set st

( a in X . s & x = root-tree [a,s] ) ) ) holds

b_{1} = b_{2}

end;
let X be V16() ManySortedSet of the carrier of S;

let s be SortSymbol of S;

func FreeGen (s,X) -> Subset of ((FreeSort X) . s) means :Def15: :: MSAFREE:def 15

for x being set holds

( x in it iff ex a being set st

( a in X . s & x = root-tree [a,s] ) );

existence for x being set holds

( x in it iff ex a being set st

( a in X . s & x = root-tree [a,s] ) );

ex b

for x being set holds

( x in b

( a in X . s & x = root-tree [a,s] ) )

proof end;

uniqueness for b

( x in b

( a in X . s & x = root-tree [a,s] ) ) ) & ( for x being set holds

( x in b

( a in X . s & x = root-tree [a,s] ) ) ) holds

b

proof end;

:: deftheorem Def15 defines FreeGen MSAFREE:def 15 :

for S being non empty non void ManySortedSign

for X being V16() ManySortedSet of the carrier of S

for s being SortSymbol of S

for b_{4} being Subset of ((FreeSort X) . s) holds

( b_{4} = FreeGen (s,X) iff for x being set holds

( x in b_{4} iff ex a being set st

( a in X . s & x = root-tree [a,s] ) ) );

for S being non empty non void ManySortedSign

for X being V16() ManySortedSet of the carrier of S

for s being SortSymbol of S

for b

( b

( x in b

( a in X . s & x = root-tree [a,s] ) ) );

registration

let S be non empty non void ManySortedSign ;

let X be V16() ManySortedSet of the carrier of S;

let s be SortSymbol of S;

coherence

not FreeGen (s,X) is empty

end;
let X be V16() ManySortedSet of the carrier of S;

let s be SortSymbol of S;

coherence

not FreeGen (s,X) is empty

proof end;

theorem Th13: :: MSAFREE:13

for S being non empty non void ManySortedSign

for X being V16() ManySortedSet of the carrier of S

for s being SortSymbol of S holds FreeGen (s,X) = { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) }

for X being V16() ManySortedSet of the carrier of S

for s being SortSymbol of S holds FreeGen (s,X) = { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) }

proof end;

definition

let S be non empty non void ManySortedSign ;

let X be V16() ManySortedSet of the carrier of S;

ex b_{1} being GeneratorSet of FreeMSA X st

for s being SortSymbol of S holds b_{1} . s = FreeGen (s,X)

for b_{1}, b_{2} being GeneratorSet of FreeMSA X st ( for s being SortSymbol of S holds b_{1} . s = FreeGen (s,X) ) & ( for s being SortSymbol of S holds b_{2} . s = FreeGen (s,X) ) holds

b_{1} = b_{2}

end;
let X be V16() ManySortedSet of the carrier of S;

func FreeGen X -> GeneratorSet of FreeMSA X means :Def16: :: MSAFREE:def 16

for s being SortSymbol of S holds it . s = FreeGen (s,X);

existence for s being SortSymbol of S holds it . s = FreeGen (s,X);

ex b

for s being SortSymbol of S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def16 defines FreeGen MSAFREE:def 16 :

for S being non empty non void ManySortedSign

for X being V16() ManySortedSet of the carrier of S

for b_{3} being GeneratorSet of FreeMSA X holds

( b_{3} = FreeGen X iff for s being SortSymbol of S holds b_{3} . s = FreeGen (s,X) );

for S being non empty non void ManySortedSign

for X being V16() ManySortedSet of the carrier of S

for b

( b

theorem :: MSAFREE:14

for S being non empty non void ManySortedSign

for X being V16() ManySortedSet of the carrier of S holds FreeGen X is V16()

for X being V16() ManySortedSet of the carrier of S holds FreeGen X is V16()

proof end;

theorem :: MSAFREE:15

for S being non empty non void ManySortedSign

for X being V16() ManySortedSet of the carrier of S holds union (rng (FreeGen X)) = { (root-tree t) where t is Symbol of (DTConMSA X) : t in Terminals (DTConMSA X) }

for X being V16() ManySortedSet of the carrier of S holds union (rng (FreeGen X)) = { (root-tree t) where t is Symbol of (DTConMSA X) : t in Terminals (DTConMSA X) }

proof end;

definition

let S be non empty non void ManySortedSign ;

let X be V16() ManySortedSet of the carrier of S;

let s be SortSymbol of S;

ex b_{1} being Function of (FreeGen (s,X)),(X . s) st

for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds

b_{1} . (root-tree t) = t `1

for b_{1}, b_{2} being Function of (FreeGen (s,X)),(X . s) st ( for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds

b_{1} . (root-tree t) = t `1 ) & ( for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds

b_{2} . (root-tree t) = t `1 ) holds

b_{1} = b_{2}

end;
let X be V16() ManySortedSet of the carrier of S;

let s be SortSymbol of S;

func Reverse (s,X) -> Function of (FreeGen (s,X)),(X . s) means :Def17: :: MSAFREE:def 17

for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds

it . (root-tree t) = t `1 ;

existence for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds

it . (root-tree t) = t `1 ;

ex b

for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def17 defines Reverse MSAFREE:def 17 :

for S being non empty non void ManySortedSign

for X being V16() ManySortedSet of the carrier of S

for s being SortSymbol of S

for b_{4} being Function of (FreeGen (s,X)),(X . s) holds

( b_{4} = Reverse (s,X) iff for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds

b_{4} . (root-tree t) = t `1 );

for S being non empty non void ManySortedSign

for X being V16() ManySortedSet of the carrier of S

for s being SortSymbol of S

for b

( b

b

definition

let S be non empty non void ManySortedSign ;

let X be V16() ManySortedSet of the carrier of S;

ex b_{1} being ManySortedFunction of FreeGen X,X st

for s being SortSymbol of S holds b_{1} . s = Reverse (s,X)

for b_{1}, b_{2} being ManySortedFunction of FreeGen X,X st ( for s being SortSymbol of S holds b_{1} . s = Reverse (s,X) ) & ( for s being SortSymbol of S holds b_{2} . s = Reverse (s,X) ) holds

b_{1} = b_{2}

end;
let X be V16() ManySortedSet of the carrier of S;

func Reverse X -> ManySortedFunction of FreeGen X,X means :Def18: :: MSAFREE:def 18

for s being SortSymbol of S holds it . s = Reverse (s,X);

existence for s being SortSymbol of S holds it . s = Reverse (s,X);

ex b

for s being SortSymbol of S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def18 defines Reverse MSAFREE:def 18 :

for S being non empty non void ManySortedSign

for X being V16() ManySortedSet of the carrier of S

for b_{3} being ManySortedFunction of FreeGen X,X holds

( b_{3} = Reverse X iff for s being SortSymbol of S holds b_{3} . s = Reverse (s,X) );

for S being non empty non void ManySortedSign

for X being V16() ManySortedSet of the carrier of S

for b

( b

definition

let S be non empty non void ManySortedSign ;

let X, A be V16() ManySortedSet of the carrier of S;

let F be ManySortedFunction of FreeGen X,A;

let t be Symbol of (DTConMSA X);

assume A1: t in Terminals (DTConMSA X) ;

ex b_{1} being Element of Union A st

for f being Function st f = F . (t `2) holds

b_{1} = f . (root-tree t)

for b_{1}, b_{2} being Element of Union A st ( for f being Function st f = F . (t `2) holds

b_{1} = f . (root-tree t) ) & ( for f being Function st f = F . (t `2) holds

b_{2} = f . (root-tree t) ) holds

b_{1} = b_{2}

end;
let X, A be V16() ManySortedSet of the carrier of S;

let F be ManySortedFunction of FreeGen X,A;

let t be Symbol of (DTConMSA X);

assume A1: t in Terminals (DTConMSA X) ;

func pi (F,A,t) -> Element of Union A means :Def19: :: MSAFREE:def 19

for f being Function st f = F . (t `2) holds

it = f . (root-tree t);

existence for f being Function st f = F . (t `2) holds

it = f . (root-tree t);

ex b

for f being Function st f = F . (t `2) holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def19 defines pi MSAFREE:def 19 :

for S being non empty non void ManySortedSign

for X, A being V16() ManySortedSet of the carrier of S

for F being ManySortedFunction of FreeGen X,A

for t being Symbol of (DTConMSA X) st t in Terminals (DTConMSA X) holds

for b_{6} being Element of Union A holds

( b_{6} = pi (F,A,t) iff for f being Function st f = F . (t `2) holds

b_{6} = f . (root-tree t) );

for S being non empty non void ManySortedSign

for X, A being V16() ManySortedSet of the carrier of S

for F being ManySortedFunction of FreeGen X,A

for t being Symbol of (DTConMSA X) st t in Terminals (DTConMSA X) holds

for b

( b

b

definition

let S be non empty non void ManySortedSign ;

let X be V16() ManySortedSet of the carrier of S;

let t be Symbol of (DTConMSA X);

assume A1: ex p being FinSequence st t ==> p ;

existence

ex b_{1} being OperSymbol of S st [b_{1}, the carrier of S] = t

for b_{1}, b_{2} being OperSymbol of S st [b_{1}, the carrier of S] = t & [b_{2}, the carrier of S] = t holds

b_{1} = b_{2}
by XTUPLE_0:1;

end;
let X be V16() ManySortedSet of the carrier of S;

let t be Symbol of (DTConMSA X);

assume A1: ex p being FinSequence st t ==> p ;

existence

ex b

proof end;

uniqueness for b

b

:: deftheorem Def20 defines @ MSAFREE:def 20 :

for S being non empty non void ManySortedSign

for X being V16() ManySortedSet of the carrier of S

for t being Symbol of (DTConMSA X) st ex p being FinSequence st t ==> p holds

for b_{4} being OperSymbol of S holds

( b_{4} = @ (X,t) iff [b_{4}, the carrier of S] = t );

for S being non empty non void ManySortedSign

for X being V16() ManySortedSet of the carrier of S

for t being Symbol of (DTConMSA X) st ex p being FinSequence st t ==> p holds

for b

( b

definition

let S be non empty non void ManySortedSign ;

let U0 be non-empty MSAlgebra over S;

let o be OperSymbol of S;

let p be FinSequence;

assume A1: p in Args (o,U0) ;

(Den (o,U0)) . p is Element of Union the Sorts of U0

end;
let U0 be non-empty MSAlgebra over S;

let o be OperSymbol of S;

let p be FinSequence;

assume A1: p in Args (o,U0) ;

func pi (o,U0,p) -> Element of Union the Sorts of U0 equals :Def21: :: MSAFREE:def 21

(Den (o,U0)) . p;

coherence (Den (o,U0)) . p;

(Den (o,U0)) . p is Element of Union the Sorts of U0

proof end;

:: deftheorem Def21 defines pi MSAFREE:def 21 :

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S

for o being OperSymbol of S

for p being FinSequence st p in Args (o,U0) holds

pi (o,U0,p) = (Den (o,U0)) . p;

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S

for o being OperSymbol of S

for p being FinSequence st p in Args (o,U0) holds

pi (o,U0,p) = (Den (o,U0)) . p;

theorem Th16: :: MSAFREE:16

for S being non empty non void ManySortedSign

for X being V16() ManySortedSet of the carrier of S holds FreeGen X is free

for X being V16() ManySortedSet of the carrier of S holds FreeGen X is free

proof end;

theorem Th17: :: MSAFREE:17

for S being non empty non void ManySortedSign

for X being V16() ManySortedSet of the carrier of S holds FreeMSA X is free

for X being V16() ManySortedSet of the carrier of S holds FreeMSA X is free

proof end;

registration

let S be non empty non void ManySortedSign ;

existence

ex b_{1} being non-empty MSAlgebra over S st

( b_{1} is free & b_{1} is strict )

end;
existence

ex b

( b

proof end;

registration

let S be non empty non void ManySortedSign ;

let U0 be free MSAlgebra over S;

ex b_{1} being GeneratorSet of U0 st b_{1} is free
by Def6;

end;
let U0 be free MSAlgebra over S;

cluster non empty Relation-like the carrier of S -defined Function-like total free for GeneratorSet of U0;

existence ex b

theorem Th18: :: MSAFREE:18

for S being non empty non void ManySortedSign

for U1 being non-empty MSAlgebra over S ex U0 being strict non-empty free MSAlgebra over S ex F being ManySortedFunction of U0,U1 st F is_epimorphism U0,U1

for U1 being non-empty MSAlgebra over S ex U0 being strict non-empty free MSAlgebra over S ex F being ManySortedFunction of U0,U1 st F is_epimorphism U0,U1

proof end;

theorem :: MSAFREE:19

for S being non empty non void ManySortedSign

for U1 being strict non-empty MSAlgebra over S ex U0 being strict non-empty free MSAlgebra over S ex F being ManySortedFunction of U0,U1 st

( F is_epimorphism U0,U1 & Image F = U1 )

for U1 being strict non-empty MSAlgebra over S ex U0 being strict non-empty free MSAlgebra over S ex F being ManySortedFunction of U0,U1 st

( F is_epimorphism U0,U1 & Image F = U1 )

proof end;

:: Preliminaries

::