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


begin

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

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

theorem :: MSAFREE2:4
for G being non empty ManySortedSign holds InputVertices G misses SortsWithConstants G
proofend;

definition
let IT be non empty ManySortedSign ;
attrIT 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 V55() with_input_V for ManySortedSign ;
existence
 ex b1 being non empty ManySortedSign st
( not b1 is void &amp; b1 is with_input_V )
proofend;
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
proofend;
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
proofend;
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 ;
attrS 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
proofend;
end;

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

definition
let IIG be non empty non void Circuit-like ManySortedSign ;
let v be Vertex of IIG;
assume B1: 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
proofend;
uniqueness
 for b1, b2 being OperSymbol of IIG st the_result_sort_of b1 = v &amp; 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 );

begin

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

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 &amp; ( for s being SortSymbol of S
for x, y being set st y in FreeSort ( the Sorts of MSA,s) &amp; y = root-tree [x,s] &amp; 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 &amp; ( for s being SortSymbol of S
for x, y being set st y in FreeSort ( the Sorts of MSA,s) &amp; y = root-tree [x,s] &amp; x in the Sorts of MSA . s holds
(b1 . s) . y = x ) )
proofend;
uniqueness
 for b1, b2 being ManySortedFunction of (FreeEnv MSA),MSA st b1 is_homomorphism FreeEnv MSA,MSA &amp; ( for s being SortSymbol of S
for x, y being set st y in FreeSort ( the Sorts of MSA,s) &amp; y = root-tree [x,s] &amp; x in the Sorts of MSA . s holds
(b1 . s) . y = x ) &amp; b2 is_homomorphism FreeEnv MSA,MSA &amp; ( for s being SortSymbol of S
for x, y being set st y in FreeSort ( the Sorts of MSA,s) &amp; y = root-tree [x,s] &amp; x in the Sorts of MSA . s holds
(b2 . s) . y = x ) holds
b1 = b2
proofend;
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 &amp; ( for s being SortSymbol of S
for x, y being set st y in FreeSort ( the Sorts of MSA,s) &amp; y = root-tree [x,s] &amp; 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
proofend;

definition
let S be non empty ManySortedSign ;
let IT be MSAlgebra over S;
attrIT 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 V33() if  not S is void
otherwise  the Sorts of IT is V33();
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 V33() ) ) &amp; ( S is void implies ( IT is finitely-generated iff the Sorts of IT is V33() ) ) );

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

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

registration
let S be non empty ManySortedSign ;
cluster non-empty finite-yielding  ->  non-empty finitely-generated for MSAlgebra over S;
coherence
 for b1 being non-empty MSAlgebra over S st b1 is finite-yielding holds
b1 is finitely-generated
proofend;
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 --> {0};
existence
 ex b1 being strict MSAlgebra over S st the Sorts of b1 = the carrier of S --> {0}
proofend;
uniqueness
 for b1, b2 being strict MSAlgebra over S st the Sorts of b1 = the carrier of S --> {0} &amp; the Sorts of b2 = the carrier of S --> {0} holds
b1 = b2
proofend;
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 --> {0} );

registration
let S be non empty ManySortedSign ;
cluster strict non-empty finite-yielding for MSAlgebra over S;
existence
 ex b1 being MSAlgebra over S st
( b1 is finite-yielding &amp; b1 is non-empty &amp; b1 is strict )
proofend;
end;

definition
let IT be non empty ManySortedSign ;
attrIT 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
cluster non empty finite non void V55() Circuit-like monotonic for ManySortedSign ;
existence
 ex b1 being non empty ManySortedSign st
( not b1 is void &amp; b1 is finite &amp; b1 is monotonic &amp; b1 is Circuit-like )
proofend;
end;

theorem Th7: :: MSAFREE2:7
for S being non empty non void ManySortedSign
for X being V16() 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
proofend;

theorem :: MSAFREE2:8
for S being non empty non void ManySortedSign
for X being V16() V33() ManySortedSet of the carrier of S holds FreeMSA X is finitely-generated
proofend;

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]
proofend;

theorem Th10: :: MSAFREE2:10
for S being non empty non void ManySortedSign
for X being V16() 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)
proofend;

theorem Th11: :: MSAFREE2:11
for S being non empty non void ManySortedSign
for X being V16() 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)
proofend;

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

registration
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
let v be Vertex of S;
cluster non empty Relation-like Function-like finite countable for 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 &amp; b1 is Relation-like )
proofend;
end;

registration
let S be non empty non void ManySortedSign ;
let X be V16() 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 b1 being Relation-like Function-like Element of the Sorts of (FreeMSA X) . v holds b1 is DecoratedTree-like by Th7;
end;

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

theorem :: MSAFREE2:12
for S being non empty non void ManySortedSign
for X being V16() 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) &amp; ( for i being Nat st i in dom p holds
p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) ) )
proofend;

definition
let S be non empty non void ManySortedSign ;
let X be V16() 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 &amp; t = dom dt &amp; it = height t );
existence
 ex b1 being Nat ex dt being finite DecoratedTree ex t being finite Tree st
( dt = e &amp; t = dom dt &amp; b1 = height t )
proofend;
uniqueness
 for b1, b2 being Nat st ex dt being finite DecoratedTree ex t being finite Tree st
( dt = e &amp; t = dom dt &amp; b1 = height t ) &amp; ex dt being finite DecoratedTree ex t being finite Tree st
( dt = e &amp; t = dom dt &amp; b2 = height t ) holds
b1 = b2 ;
end;

:: deftheorem  defines depth MSAFREE2:def_14_:_
 for S being non empty non void ManySortedSign
for X being V16() 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 &amp; t = dom dt &amp; b5 = height t ) );