:: MSAFREE2 semantic presentation

definition

let c₁ be ManySortedSign ;
mode Vertex of a₁ is Element of a₁;

end;

definition

let c₁ be non empty ManySortedSign ;
func SortsWithConstants c₁ -> Subset of a₁ equals :Def1: :: MSAFREE2:def 1
{ b₁ where B is SortSymbol of a₁ : b₁ is with_const_op } if not a₁ is void
otherwise {} ;
coherence

proof end;

consistency ;

end;

:: deftheorem Def1 defines SortsWithConstants MSAFREE2:def 1 :

definition

let c₁ be non empty ManySortedSign ;
func InputVertices c₁ -> Subset of a₁ equals :: MSAFREE2:def 2
the carrier of a₁ \ (rng the ResultSort of a₁);
coherence by XBOOLE_1:36;
func InnerVertices c₁ -> Subset of a₁ equals :: MSAFREE2:def 3
rng the ResultSort of a₁;
coherence ;

end;

:: deftheorem Def2 defines InputVertices MSAFREE2:def 2 :

:: deftheorem Def3 defines InnerVertices MSAFREE2:def 3 :

theorem Th1: :: MSAFREE2:1

for b₁ being non empty void ManySortedSign holds InputVertices b₁ = the carrier of b₁

proof end;

theorem Th2: :: MSAFREE2:2

for b₁ being non empty non void ManySortedSign
for b₂ being Vertex of b₁ st b₂ in InputVertices b₁ holds
for b₃ being OperSymbol of b₁ holds not the_result_sort_of b₃ = b₂

proof end;

theorem Th3: :: MSAFREE2:3

for b₁ being non empty ManySortedSign holds (InputVertices b₁) \/ (InnerVertices b₁) = the carrier of b₁ by XBOOLE_1:45;

theorem Th4: :: MSAFREE2:4

for b₁ being non empty ManySortedSign holds InputVertices b₁ misses InnerVertices b₁ by PROB_1:13;

theorem Th5: :: MSAFREE2:5

for b₁ being non empty ManySortedSign holds SortsWithConstants b₁ c= InnerVertices b₁

proof end;

theorem Th6: :: MSAFREE2:6

for b₁ being non empty ManySortedSign holds InputVertices b₁ misses SortsWithConstants b₁

proof end;

definition

let c₁ be non empty ManySortedSign ;
attr a₁ is with_input_V means :Def4: :: MSAFREE2:def 4
InputVertices a₁ <> {} ;

end;

:: deftheorem Def4 defines with_input_V MSAFREE2:def 4 :

registration

cluster non empty non void with_input_V ManySortedSign ;
existence

proof end;

end;

registration

let c₁ be non empty with_input_V ManySortedSign ;
cluster InputVertices a₁ -> non empty ;
coherence by Def4;

end;

definition

let c₁ be non empty non void ManySortedSign ;
redefine func InnerVertices as InnerVertices c₁ -> non empty Subset of a₁;
coherence

proof end;

end;

definition

let c₁ be non empty ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
mode InputValues of c₂ -> ManySortedSet of InputVertices a₁ means :: MSAFREE2:def 5
for b₁ being Vertex of a₁ st b₁ in InputVertices a₁ holds
a₃ . b₁ in the Sorts of a₂ . b₁;
existence

proof end;

end;

:: deftheorem Def5 defines InputValues MSAFREE2:def 5 :

definition

let c₁ be non empty ManySortedSign ;
attr a₁ is Circuit-like means :Def6: :: MSAFREE2:def 6
for b₁ being non empty non void ManySortedSign st b₁ = a₁ holds
for b₂, b₃ being OperSymbol of b₁ st the_result_sort_of b₂ = the_result_sort_of b₃ holds
b₂ = b₃;

end;

:: deftheorem Def6 defines Circuit-like MSAFREE2:def 6 :

registration

cluster non empty void -> non empty Circuit-like ManySortedSign ;
coherence

proof end;

end;

registration

cluster non empty strict non void Circuit-like ManySortedSign ;
existence

proof end;

end;

definition

let c₁ be non empty non void Circuit-like ManySortedSign ;
let c₂ be Vertex of c₁;
assume E7: c₂ in InnerVertices c₁ ;
func action_at c₂ -> OperSymbol of a₁ means :: MSAFREE2:def 7
the_result_sort_of a₃ = a₂;
existence

proof end;

uniqueness by Def6;

end;

:: deftheorem Def7 defines action_at MSAFREE2:def 7 :

theorem Th7: :: MSAFREE2:7

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁
for b₃ being OperSymbol of b₁
for b₄ being FinSequence st len b₄ = len (the_arity_of b₃) & ( for b₅ being Nat st b₅ in dom b₄ holds
b₄ . b₅ in the Sorts of b₂ . ((the_arity_of b₃) /. b₅) ) holds
b₄ in Args b₃,b₂

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
func FreeEnv c₂ -> strict non-empty free MSAlgebra of a₁ equals :: MSAFREE2:def 8
FreeMSA the Sorts of a₂;
coherence by MSAFREE:18;

end;

:: deftheorem Def8 defines FreeEnv MSAFREE2:def 8 :

theorem Th8: :: MSAFREE2:8

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁ holds FreeGen the Sorts of b₂ is free GeneratorSet of FreeEnv b₂ by MSAFREE:17;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
func Eval c₂ -> ManySortedFunction of (FreeEnv a₂),a₂ means :: MSAFREE2:def 9
( a₃ is_homomorphism FreeEnv a₂,a₂ & ( for b₁ being SortSymbol of a₁
for b₂, b₃ being set st b₃ in FreeSort the Sorts of a₂,b₁ & b₃ = root-tree [b₂,b₁] & b₂ in the Sorts of a₂ . b₁ holds
(a₃ . b₁) . b₃ = b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines Eval MSAFREE2:def 9 :

theorem Th9: :: MSAFREE2:9

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁ holds the Sorts of b₂ is GeneratorSet of b₂

proof end;

definition

let c₁ be non empty ManySortedSign ;
let c₂ be MSAlgebra of c₁;
attr a₂ is finitely-generated means :Def10: :: MSAFREE2:def 10
for b₁ being non empty non void ManySortedSign st b₁ = a₁ holds
for b₂ being MSAlgebra of b₁ st b₂ = a₂ holds
ex b₃ being GeneratorSet of b₂ st b₃ is locally-finite if not a₁ is void
otherwise the Sorts of a₂ is locally-finite;
consistency ;

end;

:: deftheorem Def10 defines finitely-generated MSAFREE2:def 10 :

definition

let c₁ be non empty ManySortedSign ;
let c₂ be MSAlgebra of c₁;
attr a₂ is locally-finite means :Def11: :: MSAFREE2:def 11
the Sorts of a₂ is locally-finite;

end;

:: deftheorem Def11 defines locally-finite MSAFREE2:def 11 :

registration

let c₁ be non empty ManySortedSign ;
cluster non-empty locally-finite -> non-empty finitely-generated MSAlgebra of a₁;
coherence

proof end;

end;

definition

let c₁ be non empty ManySortedSign ;
func Trivial_Algebra c₁ -> strict MSAlgebra of a₁ means :Def12: :: MSAFREE2:def 12
the Sorts of a₂ = the carrier of a₁ --> {0};
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines Trivial_Algebra MSAFREE2:def 12 :

registration

let c₁ be non empty ManySortedSign ;
cluster strict non-empty finitely-generated locally-finite MSAlgebra of a₁;
existence

proof end;

end;

definition

let c₁ be non empty ManySortedSign ;
attr a₁ is monotonic means :: MSAFREE2:def 13
for b₁ being non-empty finitely-generated MSAlgebra of a₁ holds b₁ is locally-finite;

end;

:: deftheorem Def13 defines monotonic MSAFREE2:def 13 :

registration

cluster non empty finite non void Circuit-like monotonic ManySortedSign ;
existence

proof end;

end;

theorem Th10: :: MSAFREE2:10

for b₁ being non empty non void ManySortedSign
for b₂ being V3 ManySortedSet of the carrier of b₁
for b₃ being SortSymbol of b₁
for b₄ being Element of the Sorts of (FreeMSA b₂) . b₃ holds b₄ is finite DecoratedTree

proof end;

theorem Th11: :: MSAFREE2:11

for b₁ being non empty non void ManySortedSign
for b₂ being V3 locally-finite ManySortedSet of the carrier of b₁ holds FreeMSA b₂ is finitely-generated

proof end;

theorem Th12: :: MSAFREE2:12

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being Vertex of b₁
for b₄ being Element of the Sorts of (FreeEnv b₂) . b₃ st b₃ in InputVertices b₁ holds
ex b₅ being Element of the Sorts of b₂ . b₃ st b₄ = root-tree [b₅,b₃]

proof end;

theorem Th13: :: MSAFREE2:13

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 DTree-yielding FinSequence st [b₃,the carrier of b₁] -tree b₄ in the Sorts of (FreeMSA b₂) . (the_result_sort_of b₃) holds
len b₄ = len (the_arity_of b₃)

proof end;

theorem Th14: :: MSAFREE2:14

proof end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be V3 ManySortedSet of the carrier of c₁;
let c₃ be Vertex of c₁;
cluster -> non empty Relation-like Function-like finite Element of the Sorts of (FreeMSA a₂) . a₃;
coherence

proof end;

end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be V3 ManySortedSet of the carrier of c₁;
let c₃ be Vertex of c₁;
cluster non empty Relation-like Function-like finite Element of the Sorts of (FreeMSA a₂) . a₃;
existence

proof end;

end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be V3 ManySortedSet of the carrier of c₁;
let c₃ be Vertex of c₁;
cluster Relation-like Function-like -> non empty Relation-like Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA a₂) . a₃;
coherence by Th10;

end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be V3 ManySortedSet of the carrier of c₁;
let c₃ be Vertex of c₁;
cluster non empty Relation-like Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA a₂) . a₃;
existence

proof end;

end;

theorem Th15: :: MSAFREE2:15

for b₁ being non empty non void ManySortedSign
for b₂ being V3 ManySortedSet of the carrier of b₁
for b₃ being Vertex of b₁
for b₄ being OperSymbol of b₁
for b₅ being Element of the Sorts of (FreeMSA b₂) . b₃ st b₃ in InnerVertices b₁ & b₅ . {} = [b₄,the carrier of b₁] holds
ex b₆ being DTree-yielding FinSequence st
( len b₆ = len (the_arity_of b₄) & ( for b₇ being Nat st b₇ in dom b₆ holds
b₆ . b₇ in the Sorts of (FreeMSA b₂) . ((the_arity_of 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 SortSymbol of c₁;
let c₄ be Element of the Sorts of (FreeMSA c₂) . c₃;
func depth c₄ -> Nat means :: MSAFREE2:def 14
ex b₁ being finite DecoratedTreeex b₂ being finite Tree st
( b₁ = a₄ & b₂ = dom b₁ & a₅ = height b₂ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def14 defines depth MSAFREE2:def 14 :