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

definition
let S be ManySortedSign ;
mode Vertex of S is Element of S;
end;

definition
let S be non empty ManySortedSign ;
func SortsWithConstants S -> Subset of S equals :Def1: :: MSAFREE2:def 1
{ v where v is SortSymbol of S : v is with_const_op } if not S is void
otherwise {} ;
coherence
( ( not S is void implies { v where v is SortSymbol of S : v is with_const_op } is Subset of S ) & ( S is void implies {} is Subset of S ) )
proof end;
consistency
for b1 being Subset of S holds verum ;
end;

:: deftheorem Def1 defines SortsWithConstants MSAFREE2:def 1 :
for S being non empty ManySortedSign holds
( ( not S is void implies SortsWithConstants S = { v where v is SortSymbol of S : v is with_const_op } ) & ( S is void implies SortsWithConstants S = {} ) );

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

:: deftheorem defines InputVertices MSAFREE2:def 2 :
for G being non empty ManySortedSign holds InputVertices G = the carrier of G \ (rng the ResultSort of G);

:: deftheorem defines InnerVertices MSAFREE2:def 3 :
for G being non empty ManySortedSign holds InnerVertices G = rng the ResultSort of G;

theorem :: MSAFREE2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty void ManySortedSign holds InputVertices G = the carrier of G
proof end;

theorem Th2: :: MSAFREE2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty non void ManySortedSign
for v being Vertex of G st v in InputVertices G holds
for o being OperSymbol of G holds not the_result_sort_of o = v
proof end;

theorem :: MSAFREE2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty ManySortedSign holds (InputVertices G) \/ (InnerVertices G) = the carrier of G by XBOOLE_1:45;

theorem Th4: :: MSAFREE2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty ManySortedSign holds InputVertices G misses InnerVertices G by PROB_1:13;

theorem Th5: :: MSAFREE2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty ManySortedSign holds SortsWithConstants G c= InnerVertices G
proof end;

theorem :: MSAFREE2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty ManySortedSign holds InputVertices G misses SortsWithConstants G
proof end;

definition
let IT be non empty ManySortedSign ;
attr IT is with_input_V means :Def4: :: MSAFREE2:def 4
 InputVertices IT <> {} ;
end;

:: deftheorem Def4 defines with_input_V MSAFREE2:def 4 :
for IT being non empty ManySortedSign holds
( IT is with_input_V iff InputVertices IT <> {} );

registration
cluster non empty non void with_input_V ManySortedSign ;
existence
ex b1 being non empty ManySortedSign st
( not b1 is void & b1 is with_input_V )
proof end;
end;

registration
let G be non empty with_input_V ManySortedSign ;
cluster InputVertices G -> non empty ;
coherence
not InputVertices G is empty by Def4;
end;

definition
let G be non empty non void ManySortedSign ;
:: original: InnerVertices
redefine func InnerVertices G -> non empty Subset of G;
coherence
InnerVertices G is non empty Subset of G
proof end;
end;

definition
let S be non empty ManySortedSign ;
let MSA be non-empty MSAlgebra of S;
mode InputValues of MSA -> ManySortedSet of InputVertices S means :: MSAFREE2:def 5
for v being Vertex of S st v in InputVertices S holds
it . v in the Sorts of MSA . v;
existence
ex b1 being ManySortedSet of InputVertices S st
for v being Vertex of S st v in InputVertices S holds
b1 . v in the Sorts of MSA . v
proof end;
end;

:: deftheorem defines InputValues MSAFREE2:def 5 :
for S being non empty ManySortedSign
for MSA being non-empty MSAlgebra of S
for b3 being ManySortedSet of InputVertices S holds
( b3 is InputValues of MSA iff for v being Vertex of S st v in InputVertices S holds
b3 . v in the Sorts of MSA . v );

definition
let S be non empty ManySortedSign ;
attr S is Circuit-like means :Def6: :: MSAFREE2:def 6
for S' being non empty non void ManySortedSign st S' = S holds
for o1, o2 being OperSymbol of S' st the_result_sort_of o1 = the_result_sort_of o2 holds
o1 = o2;
end;

:: deftheorem Def6 defines Circuit-like MSAFREE2:def 6 :
for S being non empty ManySortedSign holds
( S is Circuit-like iff for S' being non empty non void ManySortedSign st S' = S holds
for o1, o2 being OperSymbol of S' st the_result_sort_of o1 = the_result_sort_of o2 holds
o1 = o2 );

registration
cluster non empty void -> non empty Circuit-like ManySortedSign ;
coherence
for b1 being non empty ManySortedSign st b1 is void holds
b1 is Circuit-like
proof end;
end;

registration
cluster non empty strict non void Circuit-like ManySortedSign ;
existence
ex b1 being non empty ManySortedSign st
( not b1 is void & b1 is Circuit-like & b1 is strict )
proof end;
end;

definition
let IIG be non empty non void Circuit-like ManySortedSign ;
let v be Vertex of IIG;
assume A1: v in InnerVertices IIG ;
func action_at v -> OperSymbol of IIG means :: MSAFREE2:def 7
 the_result_sort_of it = v;
existence
ex b1 being OperSymbol of IIG st the_result_sort_of b1 = v
proof end;
uniqueness
for b1, b2 being OperSymbol of IIG st the_result_sort_of b1 = v & the_result_sort_of b2 = v holds
b1 = b2 by Def6;
end;

:: deftheorem defines action_at MSAFREE2:def 7 :
for IIG being non empty non void Circuit-like ManySortedSign
for v being Vertex of IIG st v in InnerVertices IIG holds
for b3 being OperSymbol of IIG holds
( b3 = action_at v iff the_result_sort_of b3 = v );

theorem :: MSAFREE2: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 A being MSAlgebra of S
for o being OperSymbol of S
for p being FinSequence st len p = len (the_arity_of o) & ( for k being Nat st k in dom p holds
p . k in the Sorts of A . ((the_arity_of o) /. k) ) holds
p in Args o,A
proof end;

definition
let S be non empty non void ManySortedSign ;
let MSA be non-empty MSAlgebra of S;
func FreeEnv MSA -> strict non-empty free MSAlgebra of S equals :: MSAFREE2:def 8
 FreeMSA the Sorts of MSA;
coherence
FreeMSA the Sorts of MSA is strict non-empty free MSAlgebra of S by MSAFREE:18;
end;

:: deftheorem defines FreeEnv MSAFREE2:def 8 :
for S being non empty non void ManySortedSign
for MSA being non-empty MSAlgebra of S holds FreeEnv MSA = FreeMSA the Sorts of MSA;

theorem :: MSAFREE2: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 MSA being non-empty MSAlgebra of S holds FreeGen the Sorts of MSA is free GeneratorSet of FreeEnv MSA by MSAFREE:17;

definition
let S be non empty non void ManySortedSign ;
let MSA be non-empty MSAlgebra of S;
func Eval MSA -> ManySortedFunction of (FreeEnv MSA),MSA means :: MSAFREE2:def 9
( it is_homomorphism FreeEnv MSA,MSA & ( for s being SortSymbol of S
for x, y being set st y in FreeSort the Sorts of MSA,s & y = root-tree [x,s] & x in the Sorts of MSA . s holds
(it . s) . y = x ) );
existence
ex b1 being ManySortedFunction of (FreeEnv MSA),MSA st
( b1 is_homomorphism FreeEnv MSA,MSA & ( for s being SortSymbol of S
for x, y being set st y in FreeSort the Sorts of MSA,s & y = root-tree [x,s] & x in the Sorts of MSA . s holds
(b1 . s) . y = x ) )
proof end;
uniqueness
for b1, b2 being ManySortedFunction of (FreeEnv MSA),MSA st b1 is_homomorphism FreeEnv MSA,MSA & ( for s being SortSymbol of S
for x, y being set st y in FreeSort the Sorts of MSA,s & y = root-tree [x,s] & x in the Sorts of MSA . s holds
(b1 . s) . y = x ) & b2 is_homomorphism FreeEnv MSA,MSA & ( for s being SortSymbol of S
for x, y being set st y in FreeSort the Sorts of MSA,s & y = root-tree [x,s] & x in the Sorts of MSA . s holds
(b2 . s) . y = x ) holds
b1 = b2
proof end;
end;

:: deftheorem defines Eval MSAFREE2:def 9 :
for S being non empty non void ManySortedSign
for MSA being non-empty MSAlgebra of S
for b3 being ManySortedFunction of (FreeEnv MSA),MSA holds
( b3 = Eval MSA iff ( b3 is_homomorphism FreeEnv MSA,MSA & ( for s being SortSymbol of S
for x, y being set st y in FreeSort the Sorts of MSA,s & y = root-tree [x,s] & x in the Sorts of MSA . s holds
(b3 . s) . y = x ) ) );

theorem Th9: :: MSAFREE2: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 A being non-empty MSAlgebra of S holds the Sorts of A is GeneratorSet of A
proof end;

definition
let S be non empty ManySortedSign ;
let IT be MSAlgebra of S;
attr IT is finitely-generated means :Def10: :: MSAFREE2:def 10
for S' being non empty non void ManySortedSign st S' = S holds
for A being MSAlgebra of S' st A = IT holds
ex G being GeneratorSet of A st G is locally-finite if not S is void
otherwise the Sorts of IT is locally-finite;
consistency
verum ;
end;

:: deftheorem Def10 defines finitely-generated MSAFREE2:def 10 :
for S being non empty ManySortedSign
for IT being MSAlgebra of S holds
( ( not S is void implies ( IT is finitely-generated iff for S' being non empty non void ManySortedSign st S' = S holds
for A being MSAlgebra of S' st A = IT holds
ex G being GeneratorSet of A st G is locally-finite ) ) & ( S is void implies ( IT is finitely-generated iff the Sorts of IT is locally-finite ) ) );

definition
let S be non empty ManySortedSign ;
let IT be MSAlgebra of S;
attr IT is locally-finite means :Def11: :: MSAFREE2:def 11
the Sorts of IT is locally-finite;
end;

:: deftheorem Def11 defines locally-finite MSAFREE2:def 11 :
for S being non empty ManySortedSign
for IT being MSAlgebra of S holds
( IT is locally-finite iff the Sorts of IT is locally-finite );

registration
let S be non empty ManySortedSign ;
cluster non-empty locally-finite -> non-empty finitely-generated MSAlgebra of S;
coherence
for b1 being non-empty MSAlgebra of S st b1 is locally-finite holds
b1 is finitely-generated
proof end;
end;

definition
let S be non empty ManySortedSign ;
func Trivial_Algebra S -> strict MSAlgebra of S means :Def12: :: MSAFREE2:def 12
the Sorts of it = the carrier of S --> {0};
existence
ex b1 being strict MSAlgebra of S st the Sorts of b1 = the carrier of S --> {0}
proof end;
uniqueness
for b1, b2 being strict MSAlgebra of S st the Sorts of b1 = the carrier of S --> {0} & the Sorts of b2 = the carrier of S --> {0} holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines Trivial_Algebra MSAFREE2:def 12 :
for S being non empty ManySortedSign
for b2 being strict MSAlgebra of S holds
( b2 = Trivial_Algebra S iff the Sorts of b2 = the carrier of S --> {0} );

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

definition
let IT be non empty ManySortedSign ;
attr IT is monotonic means :: MSAFREE2:def 13
for A being non-empty finitely-generated MSAlgebra of IT holds A is locally-finite;
end;

:: deftheorem defines monotonic MSAFREE2:def 13 :
for IT being non empty ManySortedSign holds
( IT is monotonic iff for A being non-empty finitely-generated MSAlgebra of IT holds A is locally-finite );

registration
cluster non empty finite non void Circuit-like monotonic ManySortedSign ;
existence
ex b1 being non empty ManySortedSign st
( not b1 is void & b1 is finite & b1 is monotonic & b1 is Circuit-like )
proof end;
end;

theorem Th10: :: MSAFREE2: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 v being SortSymbol of S
for e being Element of the Sorts of (FreeMSA X) . v holds e is finite DecoratedTree
proof end;

theorem :: MSAFREE2:11  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 locally-finite ManySortedSet of the carrier of S holds FreeMSA X is finitely-generated
proof end;

theorem :: MSAFREE2: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 A being non-empty MSAlgebra of S
for v being Vertex of S
for e being Element of the Sorts of (FreeEnv A) . v st v in InputVertices S holds
ex x being Element of the Sorts of A . v st e = root-tree [x,v]
proof end;

theorem Th13: :: MSAFREE2: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 o being OperSymbol of S
for p being DTree-yielding FinSequence st [o,the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) holds
len p = len (the_arity_of o)
proof end;

theorem Th14: :: MSAFREE2: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 o being OperSymbol of S
for p being DTree-yielding FinSequence st [o,the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) holds
for i being Nat st i in dom (the_arity_of o) holds
p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i)
proof end;

registration
let S be non empty non void ManySortedSign ;
let X be V3 ManySortedSet of the carrier of S;
let v be Vertex of S;
cluster -> non empty Relation-like Function-like finite Element of the Sorts of (FreeMSA X) . v;
coherence
for b1 being Element of the Sorts of (FreeMSA X) . v holds
( b1 is finite & not b1 is empty & b1 is Function-like & b1 is Relation-like )
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
let X be V3 ManySortedSet of the carrier of S;
let v be Vertex of S;
cluster non empty Relation-like Function-like finite Element of the Sorts of (FreeMSA X) . v;
existence
ex b1 being Element of the Sorts of (FreeMSA X) . v st
( b1 is Function-like & b1 is Relation-like )
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
let X be V3 ManySortedSet of the carrier of S;
let v be Vertex of S;
cluster Relation-like Function-like -> non empty Relation-like Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA X) . v;
coherence
for b1 being Relation-like Function-like Element of the Sorts of (FreeMSA X) . v holds b1 is DecoratedTree-like by Th10;
end;

registration
let IIG be non empty non void ManySortedSign ;
let X be V3 ManySortedSet of the carrier of IIG;
let v be Vertex of IIG;
cluster non empty Relation-like Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA X) . v;
existence
ex b1 being Element of the Sorts of (FreeMSA X) . v st b1 is finite
proof end;
end;

theorem :: MSAFREE2: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
for v being Vertex of S
for o being OperSymbol of S
for e being Element of the Sorts of (FreeMSA X) . v st v in InnerVertices S & e . {} = [o,the carrier of S] holds
ex p being DTree-yielding FinSequence st
( len p = len (the_arity_of o) & ( for i being Nat st i in dom p holds
p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) ) )
proof end;

definition
let S be non empty non void ManySortedSign ;
let X be V3 ManySortedSet of the carrier of S;
let v be SortSymbol of S;
let e be Element of the Sorts of (FreeMSA X) . v;
func depth e -> Nat means :: MSAFREE2:def 14
 ex dt being finite DecoratedTree ex t being finite Tree st
( dt = e & t = dom dt & it = height t );
existence
ex b1 being Nat ex dt being finite DecoratedTree ex t being finite Tree st
( dt = e & t = dom dt & b1 = height t )
proof end;
uniqueness
for b1, b2 being Nat st ex dt being finite DecoratedTree ex t being finite Tree st
( dt = e & t = dom dt & b1 = height t ) & ex dt being finite DecoratedTree ex t being finite Tree st
( dt = e & t = dom dt & b2 = height t ) holds
b1 = b2 ;
end;

:: deftheorem defines depth MSAFREE2:def 14 :
for S being non empty non void ManySortedSign
for X being V3 ManySortedSet of the carrier of S
for v being SortSymbol of S
for e being Element of the Sorts of (FreeMSA X) . v
for b5 being Nat holds
( b5 = depth e iff ex dt being finite DecoratedTree ex t being finite Tree st
( dt = e & t = dom dt & b5 = height t ) );