:: Preliminaries to Circuits, II
:: by Yatsuka Nakamura , Piotr Rudnicki , Andrzej Trybulec and Pauline N. Kawamoto
::
:: Received December 13, 1994
:: Copyright (c) 1994-2021 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 b₁ 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 b₁ being non empty ManySortedSign st
( not b₁ is void & b₁ 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 b₁ being ManySortedSet of InputVertices S st
for v being Vertex of S st v in InputVertices S holds
b₁ . 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 b₃ being ManySortedSet of InputVertices S holds
( b₃ is InputValues of MSA iff for v being Vertex of S st v in InputVertices S holds
b₃ . 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 b₁ being non empty ManySortedSign st b₁ is void holds
b₁ is Circuit-like ;

end;

registration

cluster non empty non void V61() strict Circuit-like for ManySortedSign ;

existence
ex b₁ being non empty ManySortedSign st
( not b₁ is void & b₁ is Circuit-like & b₁ 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 b₁ being OperSymbol of IIG st the_result_sort_of b₁ = v

proof end;

uniqueness
for b₁, b₂ being OperSymbol of IIG st the_result_sort_of b₁ = v & the_result_sort_of b₂ = v holds
b₁ = b₂ 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 b₃ being OperSymbol of IIG holds
( b₃ = action_at v iff the_result_sort_of b₃ = 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 (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;

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 b₁ being ManySortedFunction of (FreeEnv MSA),MSA st
( b₁ 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₁ . s) . y = x ) )

proof end;

uniqueness
for b₁, b₂ being ManySortedFunction of (FreeEnv MSA),MSA st b₁ 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₁ . s) . y = x ) & b₂ 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₂ . s) . y = x ) holds
b₁ = b₂

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 b₃ being ManySortedFunction of (FreeEnv MSA),MSA holds
( b₃ = Eval MSA iff ( b₃ 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₃ . 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 ;

cluster non-empty finite-yielding -> non-empty finitely-generated for MSAlgebra over S;

coherence
for b₁ being non-empty MSAlgebra over S st b₁ is finite-yielding holds
b₁ 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 --> {0};

existence
ex b₁ being strict MSAlgebra over S st the Sorts of b₁ = the carrier of S --> {0}

proof end;

uniqueness
for b₁, b₂ being strict MSAlgebra over S st the Sorts of b₁ = the carrier of S --> {0} & the Sorts of b₂ = the carrier of S --> {0} holds
b₁ = b₂

proof end;

end;

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

registration

let S be non empty ManySortedSign ;

cluster strict non-empty finite-yielding for MSAlgebra over S;

existence
ex b₁ being MSAlgebra over S st
( b₁ is finite-yielding & b₁ is non-empty & b₁ 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

cluster non empty finite non void V61() Circuit-like monotonic for ManySortedSign ;

existence
ex b₁ being non empty ManySortedSign st
( not b₁ is void & b₁ is finite & b₁ is monotonic & b₁ 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 (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

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]

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)

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)

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 (FreeMSA X) . v;

coherence
for b₁ being Element of the Sorts of (FreeMSA X) . v holds
( b₁ is finite & not b₁ is empty & b₁ is Function-like & b₁ 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 (FreeMSA X) . v;

existence
ex b₁ being Element of the Sorts of (FreeMSA X) . v st
( b₁ is Function-like & b₁ 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 Function-like -> Relation-like Function-like DecoratedTree-like for Element of the Sorts of (FreeMSA X) . v;

coherence
for b₁ being Relation-like Function-like Element of the Sorts of (FreeMSA X) . v holds b₁ 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;

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

existence
ex b₁ being Element of the Sorts of (FreeMSA X) . v st b₁ 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 (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;

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 b₁ being Nat ex dt being finite DecoratedTree ex t being finite Tree st
( dt = e & t = dom dt & b₁ = height t )

proof end;

uniqueness
for b₁, b₂ being Nat st ex dt being finite DecoratedTree ex t being finite Tree st
( dt = e & t = dom dt & b₁ = height t ) & ex dt being finite DecoratedTree ex t being finite Tree st
( dt = e & t = dom dt & b₂ = height t ) holds
b₁ = b₂ ;

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 (FreeMSA X) . v
for b₅ being Nat holds
( b₅ = depth e iff ex dt being finite DecoratedTree ex t being finite Tree st
( dt = e & t = dom dt & b₅ = height t ) );