MSAFREE2: Preliminaries to Circuits, II

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

environ

vocabularies HIDDEN, MSUALG_1, GLIB_000, SUBSET_1, XBOOLE_0, UNIALG_2, STRUCT_0, RELAT_1, TARSKI, FUNCT_1, FUNCOP_1, PBOOLE, CARD_3, FINSEQ_1, MARGREL1, NAT_1, PARTFUN1, PRELAMB, MSAFREE, MSUALG_3, TREES_4, REALSET1, MSUALG_2, FINSET_1, PRALG_1, CARD_1, TREES_2, DTCONSTR, TREES_3, ZFMISC_1, LANG1, TDGROUP, TREES_1, MSAFREE2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NAT_1, CARD_1, RELAT_1, FUNCT_1, PARTFUN1, FINSET_1, FINSEQ_1, FUNCT_2, CARD_3, TREES_1, TREES_2, TREES_3, TREES_4, PBOOLE, STRUCT_0, MSUALG_1, FINSEQ_2, MSAFREE, MSUALG_2, FUNCOP_1, DTCONSTR, LANG1, PRE_POLY, RELSET_1, MSUALG_3;
definitions TARSKI, FINSET_1, MSUALG_2, FUNCT_1, PBOOLE;
theorems TARSKI, ZFMISC_1, FINSEQ_1, FINSEQ_3, FUNCT_1, FUNCT_2, TREES_3, TREES_4, SUBSET_1, CARD_3, FUNCOP_1, PBOOLE, MSUALG_1, MSUALG_2, MSAFREE, CARD_2, CARD_1, DTCONSTR, LANG1, PRE_CIRC, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, FINSET_1, PARTFUN1, FINSEQ_2, XTUPLE_0;
schemes DOMAIN_1, PBOOLE, MSAFREE1, FUNCT_1;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCOP_1, FINSET_1, TREES_1, CARD_3, TREES_2, TREES_3, PRE_CIRC, STRUCT_0, DTCONSTR, RELAT_1, MSUALG_1, MSUALG_2, MSAFREE, ORDINAL1, PBOOLE, FINSEQ_1;
constructors HIDDEN, XXREAL_0, NAT_1, MSUALG_3, MSAFREE, SEQ_4, RELSET_1, PRE_POLY, FINSEQ_2, NUMBERS;
requirements HIDDEN, BOOLE, SUBSET;
equalities MSUALG_1, FUNCOP_1;
expansions MSUALG_1, FINSET_1, MSUALG_2, PBOOLE;

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

proof end;

consistency ;

end;

:: deftheorem Def1 defines SortsWithConstants MSAFREE2:def 1 :

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 ;

func InnerVertices G -> Subset of G equals :: MSAFREE2:def 3
rng the ResultSort of G;

coherence ;

end;

:: deftheorem defines InputVertices MSAFREE2:def 2 :

:: deftheorem defines InnerVertices MSAFREE2:def 3 :

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 :

registration

cluster non empty non void V61() with_input_V for ManySortedSign ;

existence

proof end;

end;

registration

let G be non empty with_input_V ManySortedSign ;

cluster InputVertices G -> non empty ;

coherence by Def4;

end;

registration

let G be non empty non void ManySortedSign ;

cluster InnerVertices G -> non empty ;

coherence

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

proof end;

end;

:: deftheorem defines InputValues MSAFREE2:def 5 :

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

registration

cluster non empty void -> non empty Circuit-like for ManySortedSign ;

coherence ;

end;

registration

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

existence

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

proof end;

uniqueness by Def6;

end;

:: deftheorem defines action_at MSAFREE2:def 7 :

::---------------------------------------------------------------------------
:: 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 by MSAFREE:17;

end;

:: deftheorem defines FreeEnv MSAFREE2:def 8 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem defines Eval MSAFREE2:def 9 :

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 ;

end;

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

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 :

registration

let S be non empty ManySortedSign ;

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

coherence

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines Trivial_Algebra MSAFREE2:def 12 :

registration

let S be non empty ManySortedSign ;

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

existence

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 :

registration

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

existence

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

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

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

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

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

proof end;

uniqueness ;

end;

:: deftheorem defines depth MSAFREE2:def 14 :