:: FREEALG semantic presentation

definition

let c₁ be set ;
attr a₁ is missing_with_Nat means :Def1: :: FREEALG:def 1
a₁ misses NAT ;

end;

:: deftheorem Def1 defines missing_with_Nat FREEALG:def 1 :

registration

cluster non empty missing_with_Nat set ;
existence

proof end;

end;

Lemma2: ( not 0 in rng <*1*> & 0 in rng <*0*> )

proof end;

notation

let c₁ be Relation;
antonym with_zero c₁ for non-empty c₁;
synonym without_zero c₁ for non-empty c₁;

end;

definition

let c₁ be Relation;
redefine attr a₁ is non-empty means :Def2: :: FREEALG:def 2
not 0 in rng a₁;
compatibility by RELAT_1:def 9;

end;

:: deftheorem Def2 defines with_zero FREEALG:def 2 :

registration

cluster non empty with_zero FinSequence of NAT ;
existence

proof end;

cluster non empty without_zero FinSequence of NAT ;
existence

proof end;

end;

definition

let c₁ be Universal_Algebra;
let c₂ be Nat;
assume E4: c₂ in dom the charact of c₁ ;
canceled;
func oper c₂,c₁ -> operation of a₁ equals :Def4: :: FREEALG:def 4
the charact of a₁ . a₂;
coherence by E4, UNIALG_2:6;

end;

:: deftheorem Def3 FREEALG:def 3 :

:: deftheorem Def4 defines oper FREEALG:def 4 :

definition

let c₁ be Universal_Algebra;
mode GeneratorSet of c₁ -> Subset of a₁ means :Def5: :: FREEALG:def 5
the carrier of (GenUnivAlg a₂) = the carrier of a₁;
existence

proof end;

end;

:: deftheorem Def5 defines GeneratorSet FREEALG:def 5 :

definition

let c₁ be Universal_Algebra;
let c₂ be GeneratorSet of c₁;
attr a₂ is free means :Def6: :: FREEALG:def 6
for b₁ being Universal_Algebra st a₁,b₁ are_similar holds
for b₂ being Function of a₂,the carrier of b₁ ex b₃ being Function of a₁,b₁ st
( b₃ is_homomorphism a₁,b₁ & b₃ | a₂ = b₂ );

end;

:: deftheorem Def6 defines free FREEALG:def 6 :

definition

let c₁ be Universal_Algebra;
attr a₁ is free means :Def7: :: FREEALG:def 7
ex b₁ being GeneratorSet of a₁ st b₁ is free;

end;

:: deftheorem Def7 defines free FREEALG:def 7 :

registration

cluster strict free UAStr ;
existence

proof end;

end;

registration

let c₁ be free Universal_Algebra;
cluster free GeneratorSet of a₁;
existence by Def7;

end;

theorem Th1: :: FREEALG:1

for b₁ being strict Universal_Algebra
for b₂ being Subset of b₁ holds
( b₂ is GeneratorSet of b₁ iff GenUnivAlg b₂ = b₁ )

proof end;

definition

let c₁ be non empty FinSequence of NAT ;
let c₂ be set ;
func REL c₁,c₂ -> Relation of (dom a₁) \/ a₂,((dom a₁) \/ a₂) * means :Def8: :: FREEALG:def 8
for b₁ being Element of (dom a₁) \/ a₂
for b₂ being Element of ((dom a₁) \/ a₂) * holds
( [b₁,b₂] in a₃ iff ( b₁ in dom a₁ & a₁ . b₁ = len b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines REL FREEALG:def 8 :

definition

let c₁ be non empty FinSequence of NAT ;
let c₂ be set ;
func DTConUA c₁,c₂ -> strict DTConstrStr equals :: FREEALG:def 9
DTConstrStr(# ((dom a₁) \/ a₂),(REL a₁,a₂) #);
correctness ;

end;

:: deftheorem Def9 defines DTConUA FREEALG:def 9 :

registration

let c₁ be non empty FinSequence of NAT ;
let c₂ be set ;
cluster DTConUA a₁,a₂ -> non empty strict ;
coherence ;

end;

theorem Th2: :: FREEALG:2

for b₁ being non empty FinSequence of NAT
for b₂ being set holds
( Terminals (DTConUA b₁,b₂) c= b₂ & NonTerminals (DTConUA b₁,b₂) = dom b₁ )

proof end;

theorem Th3: :: FREEALG:3

for b₁ being non empty FinSequence of NAT
for b₂ being missing_with_Nat set holds Terminals (DTConUA b₁,b₂) = b₂

proof end;

registration

let c₁ be non empty FinSequence of NAT ;
let c₂ be set ;
cluster DTConUA a₁,a₂ -> non empty strict with_nonterminals ;
coherence

proof end;

end;

registration

let c₁ be non empty with_zero FinSequence of NAT ;
let c₂ be set ;
cluster DTConUA a₁,a₂ -> non empty strict with_nonterminals with_useful_nonterminals ;
coherence

proof end;

end;

registration

let c₁ be non empty FinSequence of NAT ;
let c₂ be non empty missing_with_Nat set ;
cluster DTConUA a₁,a₂ -> non empty strict with_terminals with_nonterminals with_useful_nonterminals ;
coherence

proof end;

end;

definition

let c₁ be non empty FinSequence of NAT ;
let c₂ be set ;
let c₃ be Nat;
assume E11: c₃ in dom c₁ ;
func Sym c₃,c₁,c₂ -> Symbol of (DTConUA a₁,a₂) equals :Def10: :: FREEALG:def 10
a₃;
coherence by E11, XBOOLE_0:def 2;

end;

:: deftheorem Def10 defines Sym FREEALG:def 10 :

definition

let c₁ be non empty FinSequence of NAT ;
let c₂ be non empty missing_with_Nat set ;
let c₃ be Nat;
assume E12: c₃ in dom c₁ ;
func FreeOpNSG c₃,c₁,c₂ -> non empty homogeneous quasi_total PartFunc of (TS (DTConUA a₁,a₂)) * , TS (DTConUA a₁,a₂) means :Def11: :: FREEALG:def 11
( dom a₄ = (a₁ /. a₃) -tuples_on (TS (DTConUA a₁,a₂)) & ( for b₁ being FinSequence of TS (DTConUA a₁,a₂) st b₁ in dom a₄ holds
a₄ . b₁ = (Sym a₃,a₁,a₂) -tree b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines FreeOpNSG FREEALG:def 11 :

definition

let c₁ be non empty FinSequence of NAT ;
let c₂ be non empty missing_with_Nat set ;
func FreeOpSeqNSG c₁,c₂ -> PFuncFinSequence of (TS (DTConUA a₁,a₂)) means :Def12: :: FREEALG:def 12
( len a₃ = len a₁ & ( for b₁ being Nat st b₁ in dom a₃ holds
a₃ . b₁ = FreeOpNSG b₁,a₁,a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines FreeOpSeqNSG FREEALG:def 12 :

definition

let c₁ be non empty FinSequence of NAT ;
let c₂ be non empty missing_with_Nat set ;
func FreeUnivAlgNSG c₁,c₂ -> strict Universal_Algebra equals :: FREEALG:def 13
UAStr(# (TS (DTConUA a₁,a₂)),(FreeOpSeqNSG a₁,a₂) #);
coherence

proof end;

end;

:: deftheorem Def13 defines FreeUnivAlgNSG FREEALG:def 13 :

theorem Th4: :: FREEALG:4

for b₁ being non empty FinSequence of NAT
for b₂ being non empty missing_with_Nat set holds signature (FreeUnivAlgNSG b₁,b₂) = b₁

proof end;

definition

let c₁ be non empty FinSequence of NAT ;
let c₂ be non empty missing_with_Nat set ;
func FreeGenSetNSG c₁,c₂ -> Subset of (FreeUnivAlgNSG a₁,a₂) equals :: FREEALG:def 14
{ (root-tree b₁) where B is Symbol of (DTConUA a₁,a₂) : b₁ in Terminals (DTConUA a₁,a₂) } ;
coherence

proof end;

end;

:: deftheorem Def14 defines FreeGenSetNSG FREEALG:def 14 :

theorem Th5: :: FREEALG:5

for b₁ being non empty FinSequence of NAT
for b₂ being non empty missing_with_Nat set holds not FreeGenSetNSG b₁,b₂ is empty

proof end;

definition

let c₁ be non empty FinSequence of NAT ;
let c₂ be non empty missing_with_Nat set ;
redefine func FreeGenSetNSG as FreeGenSetNSG c₁,c₂ -> GeneratorSet of FreeUnivAlgNSG a₁,a₂;
coherence

proof end;

end;

definition

let c₁ be non empty FinSequence of NAT ;
let c₂ be non empty missing_with_Nat set ;
let c₃ be non empty set ;
let c₄ be Symbol of (DTConUA c₁,c₂);
let c₅ be Function of FreeGenSetNSG c₁,c₂,c₃;
assume E16: c₄ in Terminals (DTConUA c₁,c₂) ;
func pi c₅,c₄ -> Element of a₃ equals :Def15: :: FREEALG:def 15
a₅ . (root-tree a₄);
coherence

proof end;

end;

:: deftheorem Def15 defines pi FREEALG:def 15 :

definition

let c₁ be non empty FinSequence of NAT ;
let c₂ be set ;
let c₃ be Symbol of (DTConUA c₁,c₂);
given c₄ being FinSequence such that E17: c₃ ==> c₄ ;
func @ c₃ -> Nat equals :Def16: :: FREEALG:def 16
a₃;
coherence

proof end;

end;

:: deftheorem Def16 defines @ FREEALG:def 16 :

theorem Th6: :: FREEALG:6

for b₁ being non empty FinSequence of NAT
for b₂ being non empty missing_with_Nat set holds FreeGenSetNSG b₁,b₂ is free

proof end;

registration

let c₁ be non empty FinSequence of NAT ;
let c₂ be non empty missing_with_Nat set ;
cluster FreeUnivAlgNSG a₁,a₂ -> strict free ;
coherence

proof end;

end;

definition

let c₁ be non empty FinSequence of NAT ;
let c₂ be non empty missing_with_Nat set ;
redefine func FreeGenSetNSG as FreeGenSetNSG c₁,c₂ -> free GeneratorSet of FreeUnivAlgNSG a₁,a₂;
coherence by Th6;

end;

definition

let c₁ be non empty with_zero FinSequence of NAT ;
let c₂ be missing_with_Nat set ;
let c₃ be Nat;
assume E19: c₃ in dom c₁ ;
func FreeOpZAO c₃,c₁,c₂ -> non empty homogeneous quasi_total PartFunc of (TS (DTConUA a₁,a₂)) * , TS (DTConUA a₁,a₂) means :Def17: :: FREEALG:def 17
( dom a₄ = (a₁ /. a₃) -tuples_on (TS (DTConUA a₁,a₂)) & ( for b₁ being FinSequence of TS (DTConUA a₁,a₂) st b₁ in dom a₄ holds
a₄ . b₁ = (Sym a₃,a₁,a₂) -tree b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines FreeOpZAO FREEALG:def 17 :

definition

let c₁ be non empty with_zero FinSequence of NAT ;
let c₂ be missing_with_Nat set ;
func FreeOpSeqZAO c₁,c₂ -> PFuncFinSequence of (TS (DTConUA a₁,a₂)) means :Def18: :: FREEALG:def 18
( len a₃ = len a₁ & ( for b₁ being Nat st b₁ in dom a₃ holds
a₃ . b₁ = FreeOpZAO b₁,a₁,a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines FreeOpSeqZAO FREEALG:def 18 :

definition

let c₁ be non empty with_zero FinSequence of NAT ;
let c₂ be missing_with_Nat set ;
func FreeUnivAlgZAO c₁,c₂ -> strict Universal_Algebra equals :: FREEALG:def 19
UAStr(# (TS (DTConUA a₁,a₂)),(FreeOpSeqZAO a₁,a₂) #);
coherence

proof end;

end;

:: deftheorem Def19 defines FreeUnivAlgZAO FREEALG:def 19 :

theorem Th7: :: FREEALG:7

for b₁ being non empty with_zero FinSequence of NAT
for b₂ being missing_with_Nat set holds signature (FreeUnivAlgZAO b₁,b₂) = b₁

proof end;

theorem Th8: :: FREEALG:8

for b₁ being non empty with_zero FinSequence of NAT
for b₂ being missing_with_Nat set holds FreeUnivAlgZAO b₁,b₂ is with_const_op

proof end;

theorem Th9: :: FREEALG:9

for b₁ being non empty with_zero FinSequence of NAT
for b₂ being missing_with_Nat set holds Constants (FreeUnivAlgZAO b₁,b₂) <> {}

proof end;

definition

let c₁ be non empty with_zero FinSequence of NAT ;
let c₂ be missing_with_Nat set ;
func FreeGenSetZAO c₁,c₂ -> Subset of (FreeUnivAlgZAO a₁,a₂) equals :: FREEALG:def 20
{ (root-tree b₁) where B is Symbol of (DTConUA a₁,a₂) : b₁ in Terminals (DTConUA a₁,a₂) } ;
coherence

proof end;

end;

:: deftheorem Def20 defines FreeGenSetZAO FREEALG:def 20 :

definition

let c₁ be non empty with_zero FinSequence of NAT ;
let c₂ be missing_with_Nat set ;
redefine func FreeGenSetZAO as FreeGenSetZAO c₁,c₂ -> GeneratorSet of FreeUnivAlgZAO a₁,a₂;
coherence

proof end;

end;

definition

let c₁ be non empty with_zero FinSequence of NAT ;
let c₂ be missing_with_Nat set ;
let c₃ be non empty set ;
let c₄ be Symbol of (DTConUA c₁,c₂);
let c₅ be Function of FreeGenSetZAO c₁,c₂,c₃;
assume E24: c₄ in Terminals (DTConUA c₁,c₂) ;
func pi c₅,c₄ -> Element of a₃ equals :Def21: :: FREEALG:def 21
a₅ . (root-tree a₄);
coherence

proof end;

end;

:: deftheorem Def21 defines pi FREEALG:def 21 :

theorem Th10: :: FREEALG:10

for b₁ being non empty with_zero FinSequence of NAT
for b₂ being missing_with_Nat set holds FreeGenSetZAO b₁,b₂ is free

proof end;

registration

let c₁ be non empty with_zero FinSequence of NAT ;
let c₂ be missing_with_Nat set ;
cluster FreeUnivAlgZAO a₁,a₂ -> strict free ;
coherence

proof end;

end;

definition

let c₁ be non empty with_zero FinSequence of NAT ;
let c₂ be missing_with_Nat set ;
redefine func FreeGenSetZAO as FreeGenSetZAO c₁,c₂ -> free GeneratorSet of FreeUnivAlgZAO a₁,a₂;
coherence by Th10;

end;

registration

cluster strict with_const_op free UAStr ;
existence

proof end;

end;