:: MSAFREE semantic presentation

theorem Th1: :: MSAFREE:1

for b₁ being set
for b₂ being non empty set
for b₃ being Function of b₁,b₂ *
for b₄ being ManySortedSet of b₂
for b₅ being Element of b₂ *
for b₆ being set st b₆ in b₁ & b₅ = b₃ . b₆ holds
((b₄ # ) * b₃) . b₆ = product (b₄ * b₅)

proof end;

definition

let c₁ be set ;
let c₂, c₃ be ManySortedSet of c₁;
let c₄ be ManySortedSubset of c₂;
let c₅ be ManySortedFunction of c₂,c₃;
func c₅ || c₄ -> ManySortedFunction of a₄,a₃ means :Def1: :: MSAFREE:def 1
for b₁ being set st b₁ in a₁ holds
for b₂ being Function of a₂ . b₁,a₃ . b₁ st b₂ = a₅ . b₁ holds
a₆ . b₁ = b₂ | (a₄ . b₁);
existence

proof end;

uniqueness

proof end;

end;

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

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
let c₃ be set ;
assume E3: c₃ in c₁ ;
func coprod c₃,c₂ -> set means :Def2: :: MSAFREE:def 2
for b₁ being set holds
( b₁ in a₄ iff ex b₂ being set st
( b₂ in a₂ . a₃ & b₁ = [b₂,a₃] ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines coprod MSAFREE:def 2 :

notation

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
synonym coprod c₂ for disjoin c₁;

end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
redefine func coprod as coprod c₂ -> ManySortedSet of a₁ means :Def3: :: MSAFREE:def 3
for b₁ being set st b₁ in a₁ holds
a₃ . b₁ = coprod b₁,a₂;
coherence

proof end;

compatibility

proof end;

end;

:: deftheorem Def3 defines coprod MSAFREE:def 3 :

registration

let c₁ be non empty set ;
let c₂ be V3 ManySortedSet of c₁;
cluster coprod -> non-empty ;
coherence

proof end;

end;

registration

let c₁ be non empty set ;
let c₂ be V3 ManySortedSet of c₁;
cluster Union a₂ -> non empty ;
coherence

proof end;

end;

theorem Th2: :: MSAFREE:2

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being set st b₃ in b₁ holds
( b₂ . b₃ <> {} iff (coprod b₂) . b₃ <> {} )

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
mode GeneratorSet of c₂ -> MSSubset of a₂ means :Def4: :: MSAFREE:def 4
the Sorts of (GenMSAlg a₃) = the Sorts of a₂;
existence

proof end;

end;

:: deftheorem Def4 defines GeneratorSet MSAFREE:def 4 :

theorem Th3: :: MSAFREE:3

for b₁ being non empty non void ManySortedSign
for b₂ being strict non-empty MSAlgebra of b₁
for b₃ being MSSubset of b₂ holds
( b₃ is GeneratorSet of b₂ iff GenMSAlg b₃ = b₂ )

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
let c₃ be GeneratorSet of c₂;
attr a₃ is free means :Def5: :: MSAFREE:def 5
for b₁ being non-empty MSAlgebra of a₁
for b₂ being ManySortedFunction of a₃,the Sorts of b₁ ex b₃ being ManySortedFunction of a₂,b₁ st
( b₃ is_homomorphism a₂,b₁ & b₃ || a₃ = b₂ );

end;

:: deftheorem Def5 defines free MSAFREE:def 5 :

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
attr a₂ is free means :Def6: :: MSAFREE:def 6
ex b₁ being GeneratorSet of a₂ st b₁ is free;

end;

:: deftheorem Def6 defines free MSAFREE:def 6 :

theorem Th4: :: MSAFREE:4

for b₁ being non empty non void ManySortedSign
for b₂ being ManySortedSet of the carrier of b₁ holds Union (coprod b₂) misses [:the OperSymbols of b₁,{the carrier of b₁}:]

proof end;

registration

let c₁ be non void ManySortedSign ;
cluster the OperSymbols of a₁ -> non empty ;
coherence by MSUALG_1:def 5;

end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be ManySortedSet of the carrier of c₁;
canceled;
canceled;
func REL c₂ -> Relation of [:the OperSymbols of a₁,{the carrier of a₁}:] \/ (Union (coprod a₂)),([:the OperSymbols of a₁,{the carrier of a₁}:] \/ (Union (coprod a₂))) * means :Def9: :: MSAFREE:def 9
for b₁ being Element of [:the OperSymbols of a₁,{the carrier of a₁}:] \/ (Union (coprod a₂))
for b₂ being Element of ([:the OperSymbols of a₁,{the carrier of a₁}:] \/ (Union (coprod a₂))) * holds
( [b₁,b₂] in a₃ iff ( b₁ in [:the OperSymbols of a₁,{the carrier of a₁}:] & ( for b₃ being OperSymbol of a₁ st [b₃,the carrier of a₁] = b₁ holds
( len b₂ = len (the_arity_of b₃) & ( for b₄ being set st b₄ in dom b₂ holds
( ( b₂ . b₄ in [:the OperSymbols of a₁,{the carrier of a₁}:] implies for b₅ being OperSymbol of a₁ st [b₅,the carrier of a₁] = b₂ . b₄ holds
the_result_sort_of b₅ = (the_arity_of b₃) . b₄ ) & ( b₂ . b₄ in Union (coprod a₂) implies b₂ . b₄ in coprod ((the_arity_of b₃) . b₄),a₂ ) ) ) ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 MSAFREE:def 7 :

:: deftheorem Def8 MSAFREE:def 8 :

:: deftheorem Def9 defines REL MSAFREE:def 9 :

theorem Th5: :: MSAFREE:5

for b₁ being non empty non void ManySortedSign
for b₂ being ManySortedSet of the carrier of b₁
for b₃ being OperSymbol of b₁
for b₄ being Element of ([:the OperSymbols of b₁,{the carrier of b₁}:] \/ (Union (coprod b₂))) * holds
( [[b₃,the carrier of b₁],b₄] in REL b₂ iff ( len b₄ = len (the_arity_of b₃) & ( for b₅ being set st b₅ in dom b₄ holds
( ( b₄ . b₅ in [:the OperSymbols of b₁,{the carrier of b₁}:] implies for b₆ being OperSymbol of b₁ st [b₆,the carrier of b₁] = b₄ . b₅ holds
the_result_sort_of b₆ = (the_arity_of b₃) . b₅ ) & ( b₄ . b₅ in Union (coprod b₂) implies b₄ . b₅ in coprod ((the_arity_of b₃) . b₅),b₂ ) ) ) ) )

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be ManySortedSet of the carrier of c₁;
func DTConMSA c₂ -> DTConstrStr equals :: MSAFREE:def 10
DTConstrStr(# ([:the OperSymbols of a₁,{the carrier of a₁}:] \/ (Union (coprod a₂))),(REL a₂) #);
correctness ;

end;

:: deftheorem Def10 defines DTConMSA MSAFREE:def 10 :

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be ManySortedSet of the carrier of c₁;
cluster DTConMSA a₂ -> non empty strict ;
coherence ;

end;

theorem Th6: :: MSAFREE:6

for b₁ being non empty non void ManySortedSign
for b₂ being V3 ManySortedSet of the carrier of b₁ holds
( NonTerminals (DTConMSA b₂) = [:the OperSymbols of b₁,{the carrier of b₁}:] & Terminals (DTConMSA b₂) = Union (coprod b₂) )

proof end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be V3 ManySortedSet of the carrier of c₁;
cluster DTConMSA a₂ -> non empty strict with_terminals with_nonterminals with_useful_nonterminals ;
coherence

proof end;

end;

theorem Th7: :: MSAFREE:7

for b₁ being non empty non void ManySortedSign
for b₂ being V3 ManySortedSet of the carrier of b₁
for b₃ being set holds
( b₃ in Terminals (DTConMSA b₂) iff ex b₄ being SortSymbol of b₁ex b₅ being set st
( b₅ in b₂ . b₄ & b₃ = [b₅,b₄] ) )

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be V3 ManySortedSet of the carrier of c₁;
let c₃ be OperSymbol of c₁;
func Sym c₃,c₂ -> Symbol of (DTConMSA a₂) equals :: MSAFREE:def 11
[a₃,the carrier of a₁];
coherence

proof end;

end;

:: deftheorem Def11 defines Sym MSAFREE:def 11 :

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be V3 ManySortedSet of the carrier of c₁;
let c₃ be SortSymbol of c₁;
func FreeSort c₂,c₃ -> Subset of (TS (DTConMSA a₂)) equals :: MSAFREE:def 12
{ b₁ where B is Element of TS (DTConMSA a₂) : ( ex b₁ being set st
( b₂ in a₂ . a₃ & b₁ = root-tree [b₂,a₃] ) or ex b₁ being OperSymbol of a₁ st
( [b₂,the carrier of a₁] = b₁ . {} & the_result_sort_of b₂ = a₃ ) ) } ;
coherence

proof end;

end;

:: deftheorem Def12 defines FreeSort MSAFREE:def 12 :

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be V3 ManySortedSet of the carrier of c₁;
let c₃ be SortSymbol of c₁;
cluster FreeSort a₂,a₃ -> non empty ;
coherence

proof end;

end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be V3 ManySortedSet of the carrier of c₁;
func FreeSort c₂ -> ManySortedSet of the carrier of a₁ means :Def13: :: MSAFREE:def 13
for b₁ being SortSymbol of a₁ holds a₃ . b₁ = FreeSort a₂,b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines FreeSort MSAFREE:def 13 :

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be V3 ManySortedSet of the carrier of c₁;
cluster FreeSort a₂ -> V3 ;
coherence

proof end;

end;

theorem Th8: :: MSAFREE:8

for b₁ being non empty non void ManySortedSign
for b₂ being V3 ManySortedSet of the carrier of b₁
for b₃ being OperSymbol of b₁
for b₄ being set st b₄ in (((FreeSort b₂) # ) * the Arity of b₁) . b₃ holds
b₄ is FinSequence of TS (DTConMSA b₂)

proof end;

theorem Th9: :: MSAFREE:9

for b₁ being non empty non void ManySortedSign
for b₂ being V3 ManySortedSet of the carrier of b₁
for b₃ being OperSymbol of b₁
for b₄ being FinSequence of TS (DTConMSA b₂) holds
( b₄ in (((FreeSort b₂) # ) * the Arity of b₁) . b₃ iff ( dom b₄ = dom (the_arity_of b₃) & ( for b₅ being Nat st b₅ in dom b₄ holds
b₄ . b₅ in FreeSort b₂,((the_arity_of b₃) /. b₅) ) ) )

proof end;

theorem Th10: :: MSAFREE:10

for b₁ being non empty non void ManySortedSign
for b₂ being V3 ManySortedSet of the carrier of b₁
for b₃ being OperSymbol of b₁
for b₄ being FinSequence of TS (DTConMSA b₂) holds
( Sym b₃,b₂ ==> roots b₄ iff b₄ in (((FreeSort b₂) # ) * the Arity of b₁) . b₃ )

proof end;

theorem Th11: :: MSAFREE:11

canceled;

theorem Th12: :: MSAFREE:12

for b₁ being non empty non void ManySortedSign
for b₂ being V3 ManySortedSet of the carrier of b₁ holds union (rng (FreeSort b₂)) = TS (DTConMSA b₂)

proof end;

theorem Th13: :: MSAFREE:13

for b₁ being non empty non void ManySortedSign
for b₂ being V3 ManySortedSet of the carrier of b₁
for b₃, b₄ being SortSymbol of b₁ st b₃ <> b₄ holds
(FreeSort b₂) . b₃ misses (FreeSort b₂) . b₄

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be V3 ManySortedSet of the carrier of c₁;
let c₃ be OperSymbol of c₁;
func DenOp c₃,c₂ -> Function of (((FreeSort a₂) # ) * the Arity of a₁) . a₃,((FreeSort a₂) * the ResultSort of a₁) . a₃ means :Def14: :: MSAFREE:def 14
for b₁ being FinSequence of TS (DTConMSA a₂) st Sym a₃,a₂ ==> roots b₁ holds
a₄ . b₁ = (Sym a₃,a₂) -tree b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines DenOp MSAFREE:def 14 :

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be V3 ManySortedSet of the carrier of c₁;
func FreeOper c₂ -> ManySortedFunction of ((FreeSort a₂) # ) * the Arity of a₁,(FreeSort a₂) * the ResultSort of a₁ means :Def15: :: MSAFREE:def 15
for b₁ being OperSymbol of a₁ holds a₃ . b₁ = DenOp b₁,a₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines FreeOper MSAFREE:def 15 :

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be V3 ManySortedSet of the carrier of c₁;
func FreeMSA c₂ -> MSAlgebra of a₁ equals :: MSAFREE:def 16
MSAlgebra(# (FreeSort a₂),(FreeOper a₂) #);
coherence ;

end;

:: deftheorem Def16 defines FreeMSA MSAFREE:def 16 :

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be V3 ManySortedSet of the carrier of c₁;
cluster FreeMSA a₂ -> strict non-empty ;
coherence by MSUALG_1:def 8;

end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be V3 ManySortedSet of the carrier of c₁;
let c₃ be SortSymbol of c₁;
func FreeGen c₃,c₂ -> Subset of ((FreeSort a₂) . a₃) means :Def17: :: MSAFREE:def 17
for b₁ being set holds
( b₁ in a₄ iff ex b₂ being set st
( b₂ in a₂ . a₃ & b₁ = root-tree [b₂,a₃] ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines FreeGen MSAFREE:def 17 :

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be V3 ManySortedSet of the carrier of c₁;
let c₃ be SortSymbol of c₁;
cluster FreeGen a₃,a₂ -> non empty ;
coherence

proof end;

end;

theorem Th14: :: MSAFREE:14

for b₁ being non empty non void ManySortedSign
for b₂ being V3 ManySortedSet of the carrier of b₁
for b₃ being SortSymbol of b₁ holds FreeGen b₃,b₂ = { (root-tree b₄) where B is Symbol of (DTConMSA b₂) : ( b₄ in Terminals (DTConMSA b₂) & b₄ `2 = b₃ ) }

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be V3 ManySortedSet of the carrier of c₁;
func FreeGen c₂ -> GeneratorSet of FreeMSA a₂ means :Def18: :: MSAFREE:def 18
for b₁ being SortSymbol of a₁ holds a₃ . b₁ = FreeGen b₁,a₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines FreeGen MSAFREE:def 18 :

theorem Th15: :: MSAFREE:15

for b₁ being non empty non void ManySortedSign
for b₂ being V3 ManySortedSet of the carrier of b₁ holds FreeGen b₂ is non-empty

proof end;

theorem Th16: :: MSAFREE:16

for b₁ being non empty non void ManySortedSign
for b₂ being V3 ManySortedSet of the carrier of b₁ holds union (rng (FreeGen b₂)) = { (root-tree b₃) where B is Symbol of (DTConMSA b₂) : b₃ in Terminals (DTConMSA b₂) }

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be V3 ManySortedSet of the carrier of c₁;
let c₃ be SortSymbol of c₁;
func Reverse c₃,c₂ -> Function of FreeGen a₃,a₂,a₂ . a₃ means :Def19: :: MSAFREE:def 19
for b₁ being Symbol of (DTConMSA a₂) st root-tree b₁ in FreeGen a₃,a₂ holds
a₄ . (root-tree b₁) = b₁ `1 ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def19 defines Reverse MSAFREE:def 19 :

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be V3 ManySortedSet of the carrier of c₁;
func Reverse c₂ -> ManySortedFunction of FreeGen a₂,a₂ means :Def20: :: MSAFREE:def 20
for b₁ being SortSymbol of a₁ holds a₃ . b₁ = Reverse b₁,a₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def20 defines Reverse MSAFREE:def 20 :

definition

let c₁ be non empty non void ManySortedSign ;
let c₂, c₃ be V3 ManySortedSet of the carrier of c₁;
let c₄ be ManySortedFunction of FreeGen c₂,c₃;
let c₅ be Symbol of (DTConMSA c₂);
assume E26: c₅ in Terminals (DTConMSA c₂) ;
func pi c₄,c₃,c₅ -> Element of Union a₃ means :Def21: :: MSAFREE:def 21
for b₁ being Function st b₁ = a₄ . (a₅ `2 ) holds
a₆ = b₁ . (root-tree a₅);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def21 defines pi MSAFREE:def 21 :

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be V3 ManySortedSet of the carrier of c₁;
let c₃ be Symbol of (DTConMSA c₂);
assume E27: ex b₁ being FinSequence st c₃ ==> b₁ ;
func @ c₂,c₃ -> OperSymbol of a₁ means :Def22: :: MSAFREE:def 22
[a₄,the carrier of a₁] = a₃;
existence

proof end;

uniqueness by ZFMISC_1:33;

end;

:: deftheorem Def22 defines @ MSAFREE:def 22 :

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
let c₃ be OperSymbol of c₁;
let c₄ be FinSequence;
assume E28: c₄ in Args c₃,c₂ ;
func pi c₃,c₂,c₄ -> Element of Union the Sorts of a₂ equals :Def23: :: MSAFREE:def 23
(Den a₃,a₂) . a₄;
coherence

proof end;

end;

:: deftheorem Def23 defines pi MSAFREE:def 23 :

theorem Th17: :: MSAFREE:17

for b₁ being non empty non void ManySortedSign
for b₂ being V3 ManySortedSet of the carrier of b₁ holds FreeGen b₂ is free

proof end;

theorem Th18: :: MSAFREE:18

for b₁ being non empty non void ManySortedSign
for b₂ being V3 ManySortedSet of the carrier of b₁ holds FreeMSA b₂ is free

proof end;

registration

let c₁ be non empty non void ManySortedSign ;
cluster strict non-empty free MSAlgebra of a₁;
existence

proof end;

end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be free MSAlgebra of c₁;
cluster free GeneratorSet of a₂;
existence by Def6;

end;

theorem Th19: :: MSAFREE:19

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁ ex b₃ being strict non-empty free MSAlgebra of b₁ex b₄ being ManySortedFunction of b₃,b₂ st b₄ is_epimorphism b₃,b₂

proof end;

theorem Th20: :: MSAFREE:20

for b₁ being non empty non void ManySortedSign
for b₂ being strict non-empty MSAlgebra of b₁ ex b₃ being strict non-empty free MSAlgebra of b₁ex b₄ being ManySortedFunction of b₃,b₂ st
( b₄ is_epimorphism b₃,b₂ & Image b₄ = b₂ )

proof end;