:: MSAFREE semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: MSAFREE:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
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;
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
ex b1 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
b1 . i = f | (C . i)
proof end;
uniqueness
for b1, b2 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
b1 . 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
b2 . i = f | (C . i) ) holds
b1 = b2
proof end;
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 b6 being ManySortedFunction of C,B holds
( b6 = 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
b6 . i = f | (C . i) );

definition
let I be set ;
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
ex b1 being set st
for x being set holds
( x in b1 iff ex a being set st
( a in X . i & x = [a,i] ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex a being set st
( a in X . i & x = [a,i] ) ) ) & ( for x being set holds
( x in b2 iff ex a being set st
( a in X . i & x = [a,i] ) ) ) holds
b1 = b2
proof end;
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 b4 being set holds
( b4 = coprod i,X iff for x being set holds
( x in b4 iff ex a being set st
( a in X . i & x = [a,i] ) ) );

notation
let I be set ;
let X be ManySortedSet of I;
synonym coprod X for disjoin I;
end;

definition
let I be set ;
let X be ManySortedSet of I;
:: original: coprod
redefine func coprod X -> ManySortedSet of I means :Def3: :: MSAFREE:def 3
for i being set st i in I holds
it . i = coprod i,X;
coherence
coprod is ManySortedSet of I
proof end;
compatibility
for b1 being ManySortedSet of I holds
( b1 = coprod iff for i being set st i in I holds
b1 . i = coprod i,X )
proof end;
end;

:: deftheorem Def3 defines coprod MSAFREE:def 3 :
for I being set
for X, b3 being ManySortedSet of I holds
( b3 = coprod X iff for i being set st i in I holds
b3 . i = coprod i,X );

registration
let I be non empty set ;
let X be V3 ManySortedSet of I;
cluster coprod -> non-empty ;
coherence
coprod X is non-empty
proof end;
end;

registration
let I be non empty set ;
let X be V3 ManySortedSet of I;
cluster Union X -> non empty ;
coherence
not Union X is empty
proof end;
end;

theorem :: MSAFREE:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 <> {} )
proof end;

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
mode GeneratorSet of U0 -> MSSubset of U0 means :Def4: :: MSAFREE:def 4
the Sorts of (GenMSAlg it) = the Sorts of U0;
existence
ex b1 being MSSubset of U0 st the Sorts of (GenMSAlg b1) = the Sorts of U0
proof end;
end;

:: deftheorem Def4 defines GeneratorSet MSAFREE:def 4 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for b3 being MSSubset of U0 holds
( b3 is GeneratorSet of U0 iff the Sorts of (GenMSAlg b3) = the Sorts of U0 );

theorem :: MSAFREE:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being strict non-empty MSAlgebra of 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 of S;
let IT be GeneratorSet of U0;
attr IT is free means :Def5: :: MSAFREE:def 5
for U1 being non-empty MSAlgebra of 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 );
end;

:: deftheorem Def5 defines free MSAFREE:def 5 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for IT being GeneratorSet of U0 holds
( IT is free iff for U1 being non-empty MSAlgebra of 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 ) );

definition
let S be non empty non void ManySortedSign ;
let IT be MSAlgebra of S;
attr IT is free means :Def6: :: MSAFREE:def 6
ex G being GeneratorSet of IT st G is free;
end;

:: deftheorem Def6 defines free MSAFREE:def 6 :
for S being non empty non void ManySortedSign
for IT being MSAlgebra of S holds
( IT is free iff ex G being GeneratorSet of IT st G is free );

theorem Th4: :: MSAFREE:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S holds Union (coprod X) misses [:the OperSymbols of S,{the carrier of S}:]
proof end;

registration
let S be non void ManySortedSign ;
cluster the OperSymbols of S -> non empty ;
coherence
not the OperSymbols of S is empty
by MSUALG_1:def 5;
end;

definition
let S be non empty non void ManySortedSign ;
let X be ManySortedSet of the carrier of S;
canceled;
canceled;
func REL X -> Relation of [:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X)),([:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))) * means :Def9: :: MSAFREE:def 9
for a being Element of [:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in it iff ( a in [:the OperSymbols 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 OperSymbols 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
ex b1 being Relation of [:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X)),([:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))) * st
for a being Element of [:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in b1 iff ( a in [:the OperSymbols 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 OperSymbols 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 b1, b2 being Relation of [:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X)),([:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))) * st ( for a being Element of [:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in b1 iff ( a in [:the OperSymbols 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 OperSymbols 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 OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in b2 iff ( a in [:the OperSymbols 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 OperSymbols 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
b1 = b2
proof end;
end;

:: deftheorem MSAFREE:def 7 :
canceled;

:: deftheorem MSAFREE:def 8 :
canceled;

:: deftheorem Def9 defines REL MSAFREE:def 9 :
for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S
for b3 being Relation of [:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X)),([:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))) * holds
( b3 = REL X iff for a being Element of [:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in b3 iff ( a in [:the OperSymbols 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 OperSymbols 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 OperSymbols 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 OperSymbols 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;
func DTConMSA X -> DTConstrStr equals :: MSAFREE:def 10
DTConstrStr(# ([:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))),(REL X) #);
correctness
coherence
DTConstrStr(# ([:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))),(REL X) #) is DTConstrStr
;
;
end;

:: deftheorem defines DTConMSA MSAFREE:def 10 :
for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S holds DTConMSA X = DTConstrStr(# ([:the OperSymbols 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;
cluster DTConMSA X -> non empty strict ;
coherence
( DTConMSA X is strict & not DTConMSA X is empty )
;
end;

theorem Th6: :: MSAFREE:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for X being V3 ManySortedSet of the carrier of S holds
( NonTerminals (DTConMSA X) = [:the OperSymbols 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 V3 ManySortedSet of the carrier of S;
cluster DTConMSA X -> non empty strict with_terminals with_nonterminals with_useful_nonterminals ;
coherence
( DTConMSA X is with_terminals & DTConMSA X is with_nonterminals & DTConMSA X is with_useful_nonterminals )
proof end;
end;

theorem Th7: :: MSAFREE:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for X being V3 ManySortedSet of the carrier of S
for t being set holds
( t in Terminals (DTConMSA X) iff ex s being SortSymbol of S ex x being set st
( x in X . s & t = [x,s] ) )
proof end;

definition
let S be non empty non void ManySortedSign ;
let X be V3 ManySortedSet of the carrier of S;
let o be OperSymbol of S;
func Sym o,X -> Symbol of (DTConMSA X) equals :: MSAFREE:def 11
[o,the carrier of S];
coherence
[o,the carrier of S] is Symbol of (DTConMSA X)
proof end;
end;

:: deftheorem defines Sym MSAFREE:def 11 :
for S being non empty non void ManySortedSign
for X being V3 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 V3 ManySortedSet of the carrier of S;
let s be SortSymbol of S;
func FreeSort X,s -> Subset of (TS (DTConMSA X)) equals :: MSAFREE:def 12
{ 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 ) )
}
is Subset of (TS (DTConMSA X))
proof end;
end;

:: deftheorem defines FreeSort MSAFREE:def 12 :
for S being non empty non void ManySortedSign
for X being V3 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 V3 ManySortedSet of the carrier of S;
let s be SortSymbol of S;
cluster FreeSort X,s -> non empty ;
coherence
not FreeSort X,s is empty
proof end;
end;

definition
let S be non empty non void ManySortedSign ;
let X be V3 ManySortedSet of the carrier of S;
func FreeSort X -> ManySortedSet of the carrier of S means :Def13: :: MSAFREE:def 13
for s being SortSymbol of S holds it . s = FreeSort X,s;
existence
ex b1 being ManySortedSet of the carrier of S st
for s being SortSymbol of S holds b1 . s = FreeSort X,s
proof end;
uniqueness
for b1, b2 being ManySortedSet of the carrier of S st ( for s being SortSymbol of S holds b1 . s = FreeSort X,s ) & ( for s being SortSymbol of S holds b2 . s = FreeSort X,s ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines FreeSort MSAFREE:def 13 :
for S being non empty non void ManySortedSign
for X being V3 ManySortedSet of the carrier of S
for b3 being ManySortedSet of the carrier of S holds
( b3 = FreeSort X iff for s being SortSymbol of S holds b3 . s = FreeSort X,s );

registration
let S be non empty non void ManySortedSign ;
let X be V3 ManySortedSet of the carrier of S;
cluster FreeSort X -> V3 ;
coherence
FreeSort X is non-empty
proof end;
end;

theorem Th8: :: MSAFREE:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for X being V3 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for X being V3 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for X being V3 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 :: MSAFREE:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th12: :: MSAFREE:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for X being V3 ManySortedSet of the carrier of S holds union (rng (FreeSort X)) = TS (DTConMSA X)
proof end;

theorem Th13: :: MSAFREE:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for X being V3 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 V3 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 :Def14: :: MSAFREE:def 14
for p being FinSequence of TS (DTConMSA X) st Sym o,X ==> roots p holds
it . p = (Sym o,X) -tree p;
existence
ex b1 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
b1 . p = (Sym o,X) -tree p
proof end;
uniqueness
for b1, b2 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
b1 . p = (Sym o,X) -tree p ) & ( for p being FinSequence of TS (DTConMSA X) st Sym o,X ==> roots p holds
b2 . p = (Sym o,X) -tree p ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines DenOp MSAFREE:def 14 :
for S being non empty non void ManySortedSign
for X being V3 ManySortedSet of the carrier of S
for o being OperSymbol of S
for b4 being Function of (((FreeSort X) # ) * the Arity of S) . o,((FreeSort X) * the ResultSort of S) . o holds
( b4 = DenOp o,X iff for p being FinSequence of TS (DTConMSA X) st Sym o,X ==> roots p holds
b4 . p = (Sym o,X) -tree p );

definition
let S be non empty non void ManySortedSign ;
let X be V3 ManySortedSet of the carrier of S;
func FreeOper X -> ManySortedFunction of ((FreeSort X) # ) * the Arity of S,(FreeSort X) * the ResultSort of S means :Def15: :: MSAFREE:def 15
for o being OperSymbol of S holds it . o = DenOp o,X;
existence
ex b1 being ManySortedFunction of ((FreeSort X) # ) * the Arity of S,(FreeSort X) * the ResultSort of S st
for o being OperSymbol of S holds b1 . o = DenOp o,X
proof end;
uniqueness
for b1, b2 being ManySortedFunction of ((FreeSort X) # ) * the Arity of S,(FreeSort X) * the ResultSort of S st ( for o being OperSymbol of S holds b1 . o = DenOp o,X ) & ( for o being OperSymbol of S holds b2 . o = DenOp o,X ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines FreeOper MSAFREE:def 15 :
for S being non empty non void ManySortedSign
for X being V3 ManySortedSet of the carrier of S
for b3 being ManySortedFunction of ((FreeSort X) # ) * the Arity of S,(FreeSort X) * the ResultSort of S holds
( b3 = FreeOper X iff for o being OperSymbol of S holds b3 . o = DenOp o,X );

definition
let S be non empty non void ManySortedSign ;
let X be V3 ManySortedSet of the carrier of S;
func FreeMSA X -> MSAlgebra of S equals :: MSAFREE:def 16
MSAlgebra(# (FreeSort X),(FreeOper X) #);
coherence
MSAlgebra(# (FreeSort X),(FreeOper X) #) is MSAlgebra of S
;
end;

:: deftheorem defines FreeMSA MSAFREE:def 16 :
for S being non empty non void ManySortedSign
for X being V3 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 V3 ManySortedSet of the carrier of S;
cluster FreeMSA X -> strict non-empty ;
coherence
( FreeMSA X is strict & FreeMSA X is non-empty )
by MSUALG_1:def 8;
end;

definition
let S be non empty non void ManySortedSign ;
let X be V3 ManySortedSet of the carrier of S;
let s be SortSymbol of S;
func FreeGen s,X -> Subset of ((FreeSort X) . s) means :Def17: :: MSAFREE:def 17
for x being set holds
( x in it iff ex a being set st
( a in X . s & x = root-tree [a,s] ) );
existence
ex b1 being Subset of ((FreeSort X) . s) st
for x being set holds
( x in b1 iff ex a being set st
( a in X . s & x = root-tree [a,s] ) )
proof end;
uniqueness
for b1, b2 being Subset of ((FreeSort X) . s) st ( for x being set holds
( x in b1 iff ex a being set st
( a in X . s & x = root-tree [a,s] ) ) ) & ( for x being set holds
( x in b2 iff ex a being set st
( a in X . s & x = root-tree [a,s] ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def17 defines FreeGen MSAFREE:def 17 :
for S being non empty non void ManySortedSign
for X being V3 ManySortedSet of the carrier of S
for s being SortSymbol of S
for b4 being Subset of ((FreeSort X) . s) holds
( b4 = FreeGen s,X iff for x being set holds
( x in b4 iff ex a being set st
( a in X . s & x = root-tree [a,s] ) ) );

registration
let S be non empty non void ManySortedSign ;
let X be V3 ManySortedSet of the carrier of S;
let s be SortSymbol of S;
cluster FreeGen s,X -> non empty ;
coherence
not FreeGen s,X is empty
proof end;
end;

theorem Th14: :: MSAFREE:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for X being V3 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 V3 ManySortedSet of the carrier of S;
func FreeGen X -> GeneratorSet of FreeMSA X means :Def18: :: MSAFREE:def 18
for s being SortSymbol of S holds it . s = FreeGen s,X;
existence
ex b1 being GeneratorSet of FreeMSA X st
for s being SortSymbol of S holds b1 . s = FreeGen s,X
proof end;
uniqueness
for b1, b2 being GeneratorSet of FreeMSA X st ( for s being SortSymbol of S holds b1 . s = FreeGen s,X ) & ( for s being SortSymbol of S holds b2 . s = FreeGen s,X ) holds
b1 = b2
proof end;
end;

:: deftheorem Def18 defines FreeGen MSAFREE:def 18 :
for S being non empty non void ManySortedSign
for X being V3 ManySortedSet of the carrier of S
for b3 being GeneratorSet of FreeMSA X holds
( b3 = FreeGen X iff for s being SortSymbol of S holds b3 . s = FreeGen s,X );

theorem :: MSAFREE:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for X being V3 ManySortedSet of the carrier of S holds FreeGen X is non-empty
proof end;

theorem :: MSAFREE:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for X being V3 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 V3 ManySortedSet of the carrier of S;
let s be SortSymbol of S;
func Reverse s,X -> Function of FreeGen s,X,X . s means :Def19: :: MSAFREE:def 19
for t being Symbol of (DTConMSA X) st root-tree t in FreeGen s,X holds
it . (root-tree t) = t `1 ;
existence
ex b1 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
b1 . (root-tree t) = t `1
proof end;
uniqueness
for b1, b2 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
b1 . (root-tree t) = t `1 ) & ( for t being Symbol of (DTConMSA X) st root-tree t in FreeGen s,X holds
b2 . (root-tree t) = t `1 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def19 defines Reverse MSAFREE:def 19 :
for S being non empty non void ManySortedSign
for X being V3 ManySortedSet of the carrier of S
for s being SortSymbol of S
for b4 being Function of FreeGen s,X,X . s holds
( b4 = Reverse s,X iff for t being Symbol of (DTConMSA X) st root-tree t in FreeGen s,X holds
b4 . (root-tree t) = t `1 );

definition
let S be non empty non void ManySortedSign ;
let X be V3 ManySortedSet of the carrier of S;
func Reverse X -> ManySortedFunction of FreeGen X,X means :Def20: :: MSAFREE:def 20
for s being SortSymbol of S holds it . s = Reverse s,X;
existence
ex b1 being ManySortedFunction of FreeGen X,X st
for s being SortSymbol of S holds b1 . s = Reverse s,X
proof end;
uniqueness
for b1, b2 being ManySortedFunction of FreeGen X,X st ( for s being SortSymbol of S holds b1 . s = Reverse s,X ) & ( for s being SortSymbol of S holds b2 . s = Reverse s,X ) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines Reverse MSAFREE:def 20 :
for S being non empty non void ManySortedSign
for X being V3 ManySortedSet of the carrier of S
for b3 being ManySortedFunction of FreeGen X,X holds
( b3 = Reverse X iff for s being SortSymbol of S holds b3 . s = Reverse s,X );

definition
let S be non empty non void ManySortedSign ;
let X, A be V3 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 :Def21: :: MSAFREE:def 21
for f being Function st f = F . (t `2 ) holds
it = f . (root-tree t);
existence
ex b1 being Element of Union A st
for f being Function st f = F . (t `2 ) holds
b1 = f . (root-tree t)
proof end;
uniqueness
for b1, b2 being Element of Union A st ( for f being Function st f = F . (t `2 ) holds
b1 = f . (root-tree t) ) & ( for f being Function st f = F . (t `2 ) holds
b2 = f . (root-tree t) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def21 defines pi MSAFREE:def 21 :
for S being non empty non void ManySortedSign
for X, A being V3 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 b6 being Element of Union A holds
( b6 = pi F,A,t iff for f being Function st f = F . (t `2 ) holds
b6 = f . (root-tree t) );

definition
let S be non empty non void ManySortedSign ;
let X be V3 ManySortedSet of the carrier of S;
let t be Symbol of (DTConMSA X);
assume A1: ex p being FinSequence st t ==> p ;
func @ X,t -> OperSymbol of S means :Def22: :: MSAFREE:def 22
[it,the carrier of S] = t;
existence
ex b1 being OperSymbol of S st [b1,the carrier of S] = t
proof end;
uniqueness
for b1, b2 being OperSymbol of S st [b1,the carrier of S] = t & [b2,the carrier of S] = t holds
b1 = b2
by ZFMISC_1:33;
end;

:: deftheorem Def22 defines @ MSAFREE:def 22 :
for S being non empty non void ManySortedSign
for X being V3 ManySortedSet of the carrier of S
for t being Symbol of (DTConMSA X) st ex p being FinSequence st t ==> p holds
for b4 being OperSymbol of S holds
( b4 = @ X,t iff [b4,the carrier of S] = t );

definition
let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra of 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 :Def23: :: MSAFREE:def 23
(Den o,U0) . p;
coherence
(Den o,U0) . p is Element of Union the Sorts of U0
proof end;
end;

:: deftheorem Def23 defines pi MSAFREE:def 23 :
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of 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 Th17: :: MSAFREE:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for X being V3 ManySortedSet of the carrier of S holds FreeGen X is free
proof end;

theorem Th18: :: MSAFREE:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for X being V3 ManySortedSet of the carrier of S holds FreeMSA X is free
proof end;

registration
let S be non empty non void ManySortedSign ;
cluster strict non-empty free MSAlgebra of S;
existence
ex b1 being non-empty MSAlgebra of S st
( b1 is free & b1 is strict )
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
let U0 be free MSAlgebra of S;
cluster free GeneratorSet of U0;
existence
ex b1 being GeneratorSet of U0 st b1 is free
by Def6;
end;

theorem Th19: :: MSAFREE:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S ex U0 being strict non-empty free MSAlgebra of S ex F being ManySortedFunction of U0,U1 st F is_epimorphism U0,U1
proof end;

theorem :: MSAFREE:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U1 being strict non-empty MSAlgebra of S ex U0 being strict non-empty free MSAlgebra of S ex F being ManySortedFunction of U0,U1 st
( F is_epimorphism U0,U1 & Image F = U1 )
proof end;