:: by Yatsuka Nakamura , Piotr Rudnicki , Andrzej Trybulec and Pauline N. Kawamoto

::

:: Received December 13, 1994

:: Copyright (c) 1994-2019 Association of Mizar Users

definition

let S be non empty ManySortedSign ;

( ( 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 ) )

for b_{1} being Subset of S holds verum
;

end;
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 { v where v is SortSymbol of S : v is with_const_op } if not S is void

otherwise {} ;

( ( 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 b

:: 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 = {} ) );

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 ;

the carrier of G \ (rng the ResultSort of G) is Subset of G ;

coherence

rng the ResultSort of G is Subset of G ;

end;
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);

the carrier of G \ (rng the ResultSort of G) is Subset of G ;

coherence

rng the ResultSort of G is Subset of G ;

:: deftheorem defines InputVertices MSAFREE2:def 2 :

for G being non empty ManySortedSign holds InputVertices G = the carrier of G \ (rng the ResultSort of G);

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;

for G being non empty ManySortedSign holds InnerVertices G = rng the ResultSort of G;

theorem :: MSAFREE2:1

theorem Th2: :: MSAFREE2:2

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

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;

:: deftheorem Def4 defines with_input_V MSAFREE2:def 4 :

for IT being non empty ManySortedSign holds

( IT is with_input_V iff InputVertices IT <> {} );

for IT being non empty ManySortedSign holds

( IT is with_input_V iff InputVertices IT <> {} );

registration

existence

ex b_{1} being non empty ManySortedSign st

( not b_{1} is void & b_{1} is with_input_V )

end;
ex b

( not b

proof end;

registration
end;

registration
end;

definition

let S be non empty ManySortedSign ;

let MSA be non-empty MSAlgebra over S;

ex b_{1} being ManySortedSet of InputVertices S st

for v being Vertex of S st v in InputVertices S holds

b_{1} . v in the Sorts of MSA . v

end;
let MSA be non-empty MSAlgebra over 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 for v being Vertex of S st v in InputVertices S holds

it . v in the Sorts of MSA . v;

ex b

for v being Vertex of S st v in InputVertices S holds

b

proof end;

:: deftheorem defines InputValues MSAFREE2:def 5 :

for S being non empty ManySortedSign

for MSA being non-empty MSAlgebra over S

for b_{3} being ManySortedSet of InputVertices S holds

( b_{3} is InputValues of MSA iff for v being Vertex of S st v in InputVertices S holds

b_{3} . v in the Sorts of MSA . v );

for S being non empty ManySortedSign

for MSA being non-empty MSAlgebra over S

for b

( b

b

:: Generalize this for arbitrary subset of the carrier

definition

let S be non empty ManySortedSign ;

end;
attr S is Circuit-like means :Def6: :: MSAFREE2:def 6

for S9 being non empty non void ManySortedSign st S9 = S holds

for o1, o2 being OperSymbol of S9 st the_result_sort_of o1 = the_result_sort_of o2 holds

o1 = o2;

for S9 being non empty non void ManySortedSign st S9 = S holds

for o1, o2 being OperSymbol of S9 st the_result_sort_of o1 = the_result_sort_of o2 holds

o1 = o2;

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

for S being non empty ManySortedSign holds

( S is Circuit-like iff for S9 being non empty non void ManySortedSign st S9 = S holds

for o1, o2 being OperSymbol of S9 st the_result_sort_of o1 = the_result_sort_of o2 holds

o1 = o2 );

for S being non empty ManySortedSign holds

( S is Circuit-like iff for S9 being non empty non void ManySortedSign st S9 = S holds

for o1, o2 being OperSymbol of S9 st the_result_sort_of o1 = the_result_sort_of o2 holds

o1 = o2 );

registration
end;

registration

existence

ex b_{1} being non empty ManySortedSign st

( not b_{1} is void & b_{1} is Circuit-like & b_{1} is strict )

end;
ex b

( not b

proof end;

definition

let IIG be non empty non void Circuit-like ManySortedSign ;

let v be Vertex of IIG;

assume A1: v in InnerVertices IIG ;

existence

ex b_{1} being OperSymbol of IIG st the_result_sort_of b_{1} = v

for b_{1}, b_{2} being OperSymbol of IIG st the_result_sort_of b_{1} = v & the_result_sort_of b_{2} = v holds

b_{1} = b_{2}
by Def6;

end;
let v be Vertex of IIG;

assume A1: v in InnerVertices IIG ;

existence

ex b

proof end;

uniqueness for b

b

:: 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 b_{3} being OperSymbol of IIG holds

( b_{3} = action_at v iff the_result_sort_of b_{3} = v );

for IIG being non empty non void Circuit-like ManySortedSign

for v being Vertex of IIG st v in InnerVertices IIG holds

for b

( b

::---------------------------------------------------------------------------

:: Free Many Sorted Algebras

::---------------------------------------------------------------------------

:: Free Many Sorted Algebras

::---------------------------------------------------------------------------

theorem :: MSAFREE2:5

for S being non empty non void ManySortedSign

for A being MSAlgebra over 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)

for A being MSAlgebra over 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 over S;

FreeMSA the Sorts of MSA is strict non-empty free MSAlgebra over S by MSAFREE:17;

end;
let MSA be non-empty MSAlgebra over S;

func FreeEnv MSA -> strict non-empty free MSAlgebra over S equals :: MSAFREE2:def 8

FreeMSA the Sorts of MSA;

coherence FreeMSA the Sorts of MSA;

FreeMSA the Sorts of MSA is strict non-empty free MSAlgebra over S by MSAFREE:17;

:: deftheorem defines FreeEnv MSAFREE2:def 8 :

for S being non empty non void ManySortedSign

for MSA being non-empty MSAlgebra over S holds FreeEnv MSA = FreeMSA the Sorts of MSA;

for S being non empty non void ManySortedSign

for MSA being non-empty MSAlgebra over S holds FreeEnv MSA = FreeMSA the Sorts of MSA;

definition

let S be non empty non void ManySortedSign ;

let MSA be non-empty MSAlgebra over S;

ex b_{1} being ManySortedFunction of (FreeEnv MSA),MSA st

( b_{1} 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

(b_{1} . s) . y = x ) )

for b_{1}, b_{2} being ManySortedFunction of (FreeEnv MSA),MSA st b_{1} 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

(b_{1} . s) . y = x ) & b_{2} 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

(b_{2} . s) . y = x ) holds

b_{1} = b_{2}

end;
let MSA be non-empty MSAlgebra over 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 ( 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 ) );

ex b

( b

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

(b

proof end;

uniqueness for b

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

(b

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

(b

b

proof end;

:: deftheorem defines Eval MSAFREE2:def 9 :

for S being non empty non void ManySortedSign

for MSA being non-empty MSAlgebra over S

for b_{3} being ManySortedFunction of (FreeEnv MSA),MSA holds

( b_{3} = Eval MSA iff ( b_{3} 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

(b_{3} . s) . y = x ) ) );

for S being non empty non void ManySortedSign

for MSA being non-empty MSAlgebra over S

for b

( b

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

(b

theorem Th6: :: MSAFREE2:6

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S holds the Sorts of A is GeneratorSet of A

for A being non-empty MSAlgebra over S holds the Sorts of A is GeneratorSet of A

proof end;

definition

let S be non empty ManySortedSign ;

let IT be MSAlgebra over S;

verum ;

end;
let IT be MSAlgebra over S;

attr IT is finitely-generated means :Def10: :: MSAFREE2:def 10

for S9 being non empty non void ManySortedSign st S9 = S holds

for A being MSAlgebra over S9 st A = IT holds

ex G being GeneratorSet of A st G is V39() if not S is void

otherwise the Sorts of IT is V39();

consistency for S9 being non empty non void ManySortedSign st S9 = S holds

for A being MSAlgebra over S9 st A = IT holds

ex G being GeneratorSet of A st G is V39() if not S is void

otherwise the Sorts of IT is V39();

verum ;

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

for S being non empty ManySortedSign

for IT being MSAlgebra over S holds

( ( not S is void implies ( IT is finitely-generated iff for S9 being non empty non void ManySortedSign st S9 = S holds

for A being MSAlgebra over S9 st A = IT holds

ex G being GeneratorSet of A st G is V39() ) ) & ( S is void implies ( IT is finitely-generated iff the Sorts of IT is V39() ) ) );

for S being non empty ManySortedSign

for IT being MSAlgebra over S holds

( ( not S is void implies ( IT is finitely-generated iff for S9 being non empty non void ManySortedSign st S9 = S holds

for A being MSAlgebra over S9 st A = IT holds

ex G being GeneratorSet of A st G is V39() ) ) & ( S is void implies ( IT is finitely-generated iff the Sorts of IT is V39() ) ) );

:: deftheorem defines finite-yielding MSAFREE2:def 11 :

for S being non empty ManySortedSign

for IT being MSAlgebra over S holds

( IT is finite-yielding iff the Sorts of IT is V39() );

for S being non empty ManySortedSign

for IT being MSAlgebra over S holds

( IT is finite-yielding iff the Sorts of IT is V39() );

registration

let S be non empty ManySortedSign ;

coherence

for b_{1} being non-empty MSAlgebra over S st b_{1} is finite-yielding holds

b_{1} is finitely-generated

end;
coherence

for b

b

proof end;

definition

let S be non empty ManySortedSign ;

ex b_{1} being strict MSAlgebra over S st the Sorts of b_{1} = the carrier of S --> {0}

for b_{1}, b_{2} being strict MSAlgebra over S st the Sorts of b_{1} = the carrier of S --> {0} & the Sorts of b_{2} = the carrier of S --> {0} holds

b_{1} = b_{2}

end;
func Trivial_Algebra S -> strict MSAlgebra over S means :Def12: :: MSAFREE2:def 12

the Sorts of it = the carrier of S --> {0};

existence the Sorts of it = the carrier of S --> {0};

ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def12 defines Trivial_Algebra MSAFREE2:def 12 :

for S being non empty ManySortedSign

for b_{2} being strict MSAlgebra over S holds

( b_{2} = Trivial_Algebra S iff the Sorts of b_{2} = the carrier of S --> {0} );

for S being non empty ManySortedSign

for b

( b

registration

let S be non empty ManySortedSign ;

existence

ex b_{1} being MSAlgebra over S st

( b_{1} is finite-yielding & b_{1} is non-empty & b_{1} is strict )

end;
existence

ex b

( b

proof end;

definition

let IT be non empty ManySortedSign ;

end;
attr IT is monotonic means :: MSAFREE2:def 13

for A being non-empty finitely-generated MSAlgebra over IT holds A is finite-yielding ;

for A being non-empty finitely-generated MSAlgebra over IT holds A is finite-yielding ;

:: 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 over IT holds A is finite-yielding );

for IT being non empty ManySortedSign holds

( IT is monotonic iff for A being non-empty finitely-generated MSAlgebra over IT holds A is finite-yielding );

registration

existence

ex b_{1} being non empty ManySortedSign st

( not b_{1} is void & b_{1} is finite & b_{1} is monotonic & b_{1} is Circuit-like )

end;
ex b

( not b

proof end;

theorem Th7: :: MSAFREE2:7

for S being non empty non void ManySortedSign

for X being V5() 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

for X being V5() 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:8

for S being non empty non void ManySortedSign

for X being V5() V39() ManySortedSet of the carrier of S holds FreeMSA X is finitely-generated

for X being V5() V39() ManySortedSet of the carrier of S holds FreeMSA X is finitely-generated

proof end;

theorem :: MSAFREE2:9

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over 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]

for A being non-empty MSAlgebra over 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 Th10: :: MSAFREE2:10

for S being non empty non void ManySortedSign

for X being V5() 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)

for X being V5() 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 Th11: :: MSAFREE2:11

for S being non empty non void ManySortedSign

for X being V5() 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)

for X being V5() 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 V5() ManySortedSet of the carrier of S;

let v be Vertex of S;

for b_{1} being Element of the Sorts of (FreeMSA X) . v holds

( b_{1} is finite & not b_{1} is empty & b_{1} is Function-like & b_{1} is Relation-like )

end;
let X be V5() ManySortedSet of the carrier of S;

let v be Vertex of S;

cluster -> Relation-like non empty Function-like finite for Element of the Sorts of (FreeMSA X) . v;

coherence for b

( b

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let v be Vertex of S;

ex b_{1} being Element of the Sorts of (FreeMSA X) . v st

( b_{1} is Function-like & b_{1} is Relation-like )

end;
let X be V5() ManySortedSet of the carrier of S;

let v be Vertex of S;

cluster Relation-like non empty Function-like finite countable for Element of the Sorts of (FreeMSA X) . v;

existence ex b

( b

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let v be Vertex of S;

for b_{1} being Relation-like Function-like Element of the Sorts of (FreeMSA X) . v holds b_{1} is DecoratedTree-like
by Th7;

end;
let X be V5() ManySortedSet of the carrier of S;

let v be Vertex of S;

cluster Relation-like Function-like -> Relation-like Function-like DecoratedTree-like for Element of the Sorts of (FreeMSA X) . v;

coherence for b

registration

let IIG be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of IIG;

let v be Vertex of IIG;

ex b_{1} being Element of the Sorts of (FreeMSA X) . v st b_{1} is finite

end;
let X be V5() ManySortedSet of the carrier of IIG;

let v be Vertex of IIG;

cluster Relation-like non empty Function-like finite countable DecoratedTree-like for Element of the Sorts of (FreeMSA X) . v;

existence ex b

proof end;

theorem :: MSAFREE2:12

for S being non empty non void ManySortedSign

for X being V5() 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 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) ) )

for X being V5() 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 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 V5() ManySortedSet of the carrier of S;

let v be SortSymbol of S;

let e be Element of the Sorts of (FreeMSA X) . v;

ex b_{1} being Nat ex dt being finite DecoratedTree ex t being finite Tree st

( dt = e & t = dom dt & b_{1} = height t )

for b_{1}, b_{2} being Nat st ex dt being finite DecoratedTree ex t being finite Tree st

( dt = e & t = dom dt & b_{1} = height t ) & ex dt being finite DecoratedTree ex t being finite Tree st

( dt = e & t = dom dt & b_{2} = height t ) holds

b_{1} = b_{2}
;

end;
let X be V5() 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 dt being finite DecoratedTree ex t being finite Tree st

( dt = e & t = dom dt & it = height t );

ex b

( dt = e & t = dom dt & b

proof end;

uniqueness for b

( dt = e & t = dom dt & b

( dt = e & t = dom dt & b

b

:: deftheorem defines depth MSAFREE2:def 14 :

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for v being SortSymbol of S

for e being Element of the Sorts of (FreeMSA X) . v

for b_{5} being Nat holds

( b_{5} = depth e iff ex dt being finite DecoratedTree ex t being finite Tree st

( dt = e & t = dom dt & b_{5} = height t ) );

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for v being SortSymbol of S

for e being Element of the Sorts of (FreeMSA X) . v

for b

( b

( dt = e & t = dom dt & b

:: Many Sorted Signatures

::---------------------------------------------------------------------------