:: Preliminaries to Circuits, II
:: by Yatsuka Nakamura , Piotr Rudnicki , Andrzej Trybulec and Pauline N. Kawamoto
::
:: Received December 13, 1994
:: Copyright (c) 1994-2018 Association of Mizar Users

::---------------------------------------------------------------------------
:: Many Sorted Signatures
::---------------------------------------------------------------------------
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
;
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
for G being non empty void ManySortedSign holds InputVertices G = the carrier of G ;

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

theorem Th3: :: MSAFREE2:3
for G being non empty ManySortedSign holds SortsWithConstants G c= InnerVertices G
proof end;

theorem :: MSAFREE2:4
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 V61() with_input_V for 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;

registration
let G be non empty non void ManySortedSign ;
cluster InnerVertices G -> non empty ;
coherence
not InnerVertices G is empty
proof end;
end;

definition
let S be non empty ManySortedSign ;
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
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 over 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 );

:: Generalize this for arbitrary subset of the carrier
definition
let S be non empty ManySortedSign ;
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;
end;

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

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

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

::---------------------------------------------------------------------------
:: 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 () & ( for k being Nat st k in dom p holds
p . k in the Sorts of A . (() /. 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;
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 is strict non-empty free MSAlgebra over S
by MSAFREE:17;
end;

:: 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;

definition
let S be non empty non void ManySortedSign ;
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
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 over 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 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
proof end;

definition
let S be non empty ManySortedSign ;
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
verum
;
end;

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

definition
let S be non empty ManySortedSign ;
let IT be MSAlgebra over S;
attr IT is finite-yielding means :: MSAFREE2:def 11
the Sorts of IT is V39();
end;

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

registration
let S be non empty ManySortedSign ;
coherence
for b1 being non-empty MSAlgebra over S st b1 is finite-yielding holds
b1 is finitely-generated
proof end;
end;

definition
let S be non empty ManySortedSign ;
func Trivial_Algebra S -> strict MSAlgebra over S means :Def12: :: MSAFREE2:def 12
the Sorts of it = the carrier of S --> ;
existence
ex b1 being strict MSAlgebra over S st the Sorts of b1 = the carrier of S -->
proof end;
uniqueness
for b1, b2 being strict MSAlgebra over S st the Sorts of b1 = the carrier of S --> & the Sorts of b2 = the carrier of S --> 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 over S holds
( b2 = Trivial_Algebra S iff the Sorts of b2 = the carrier of S --> );

registration
let S be non empty ManySortedSign ;
existence
ex b1 being MSAlgebra over S st
( b1 is finite-yielding & 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 over IT holds A is finite-yielding ;
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 over IT holds A is finite-yielding );

registration
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 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 () . 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
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 () . 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 () . holds
len p = len ()
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 () . holds
for i being Nat st i in dom () holds
p . i in the Sorts of () . (() . 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;
cluster -> Relation-like non empty Function-like finite for Element of the Sorts of () . v;
coherence
for b1 being Element of the Sorts of () . 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 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 () . v;
existence
ex b1 being Element of the Sorts of () . 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 V5() ManySortedSet of the carrier of S;
let v be Vertex of S;
coherence
for b1 being Relation-like Function-like Element of the Sorts of () . v holds b1 is DecoratedTree-like
by Th7;
end;

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;
existence
ex b1 being Element of the Sorts of () . v st b1 is finite
proof end;
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 () . v st e . {} = [o, the carrier of S] holds
ex p being DTree-yielding FinSequence st
( len p = len () & ( for i being Nat st i in dom p holds
p . i in the Sorts of () . (() . 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 () . 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 V5() ManySortedSet of the carrier of S
for v being SortSymbol of S
for e being Element of the Sorts of () . 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 ) );