:: Introduction to Circuits, I :: by Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec and Pauline N. Kawamoto :: :: Received December 15, 1994 :: Copyright (c) 1994-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, STRUCT_0, MSAFREE2, XBOOLE_0, MSUALG_1, FINSET_1, RELAT_1, PBOOLE, GLIB_000, FUNCT_1, UNIALG_2, SUBSET_1, FINSEQ_1, FUNCOP_1, FUNCT_6, FSM_1, CARD_3, MARGREL1, TREES_3, TREES_4, PARTFUN1, MSAFREE, TREES_2, ARYTM_3, TREES_1, ZFMISC_1, LANG1, DTCONSTR, TREES_A, TDGROUP, TARSKI, NAT_1, ORDINAL4, CARD_1, XXREAL_0, MEMBERED, ARYTM_1, FUNCT_4, REAL_1, CIRCUIT1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, MEMBERED, RELAT_1, FUNCT_1, PBOOLE, PARTFUN1, FINSEQ_1, FINSEQ_2, RELSET_1, FINSET_1, CARD_3, FUNCT_4, FUNCT_6, TREES_1, TREES_2, TREES_3, TREES_4, STRUCT_0, LANG1, DTCONSTR, MSUALG_1, MSUALG_2, MSAFREE, XXREAL_2, FUNCOP_1, MSAFREE2, XXREAL_0; constructors FUNCT_4, REAL_1, MSUALG_2, MSAFREE2, SEQ_4, RELSET_1, NUMBERS; registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, TREES_1, CARD_3, PBOOLE, TREES_2, TREES_3, PRE_CIRC, STRUCT_0, DTCONSTR, MSUALG_1, MSAFREE, MSAFREE2, FUNCT_2, XXREAL_2, CARD_1, RELSET_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin ::--------------------------------------------------------------------------- :: Circuits ::--------------------------------------------------------------------------- definition let S be non void Circuit-like non empty ManySortedSign; mode Circuit of S is finite-yielding MSAlgebra over S; end; reserve IIG for Circuit-like non void non empty ManySortedSign; definition let IIG; let SCS be non-empty Circuit of IIG; func Set-Constants SCS -> ManySortedSet of SortsWithConstants IIG means :: CIRCUIT1:def 1 for x being Vertex of IIG st x in dom it holds it.x in Constants (SCS, x); end; theorem :: CIRCUIT1:1 for IIG for SCS being non-empty Circuit of IIG, v being Vertex of IIG, e being Element of (the Sorts of SCS).v st v in SortsWithConstants IIG & e in Constants (SCS, v) holds (Set-Constants SCS).v = e; definition let IIG; let CS be Circuit of IIG; mode InputFuncs of CS is ManySortedFunction of ((InputVertices IIG) --> NAT qua ManySortedSet of InputVertices IIG), ((the Sorts of CS) | InputVertices IIG qua ManySortedSet of InputVertices IIG); end; theorem :: CIRCUIT1:2 for IIG for SCS being non-empty Circuit of IIG, InpFs being InputFuncs of SCS, n being Nat st IIG is with_input_V holds (commute InpFs).n is InputValues of SCS; definition let IIG such that IIG is with_input_V; let SCS be non-empty Circuit of IIG, InpFs be InputFuncs of SCS, n be Nat; func n-th_InputValues InpFs -> InputValues of SCS equals :: CIRCUIT1:def 2 (commute InpFs).n; end; definition let IIG; let SCS be Circuit of IIG; mode State of SCS is Element of product (the Sorts of SCS); end; theorem :: CIRCUIT1:3 for IIG for SCS being non-empty Circuit of IIG, s being State of SCS holds dom s = the carrier of IIG; theorem :: CIRCUIT1:4 for IIG for SCS being non-empty Circuit of IIG, s being State of SCS, v being Vertex of IIG holds s.v in (the Sorts of SCS).v; definition let IIG; let SCS be non-empty Circuit of IIG, s be State of SCS, o be OperSymbol of IIG; func o depends_on_in s -> Element of Args (o, SCS) equals :: CIRCUIT1:def 3 s * (the_arity_of o); end; reserve IIG for monotonic Circuit-like non void non empty ManySortedSign; theorem :: CIRCUIT1:5 for IIG for SCS being finite-yielding non-empty MSAlgebra over IIG, v, w being Vertex of IIG, e1 being Element of (the Sorts of FreeEnv SCS).v , q1 being DTree-yielding FinSequence st v in InnerVertices IIG & e1 = [ action_at v,the carrier of IIG]-tree q1 holds for k being Element of NAT st k in dom q1 & q1.k in (the Sorts of FreeEnv SCS).w holds w = (the_arity_of action_at v)/.k; registration let IIG; let SCS be finite-yielding non-empty MSAlgebra over IIG, v be Vertex of IIG; cluster -> finite non empty Function-like Relation-like for Element of (the Sorts of FreeEnv SCS).v; end; registration let IIG; let SCS be finite-yielding non-empty MSAlgebra over IIG, v be Vertex of IIG; cluster -> DecoratedTree-like for Element of (the Sorts of FreeEnv SCS).v; end; theorem :: CIRCUIT1:6 for IIG for SCS being finite-yielding non-empty MSAlgebra over IIG, v, w being Vertex of IIG, e1 being Element of (the Sorts of FreeEnv SCS).v , e2 being Element of (the Sorts of FreeEnv SCS).w, q1 being DTree-yielding FinSequence, k1 being Element of NAT st v in InnerVertices IIG \ SortsWithConstants IIG & e1 = [action_at v,the carrier of IIG]-tree q1 & k1+1 in dom q1 & q1.(k1+1) in (the Sorts of FreeEnv SCS).w holds e1 with-replacement (<*k1*>,e2) in (the Sorts of FreeEnv SCS).v; theorem :: CIRCUIT1:7 for IIG for A being finite-yielding non-empty MSAlgebra over IIG, v being Element of IIG, e being Element of (the Sorts of FreeEnv A).v st 1 < card e ex o being OperSymbol of IIG st e.{} = [o,the carrier of IIG]; theorem :: CIRCUIT1:8 for IIG being non void Circuit-like non empty ManySortedSign for SCS being non-empty Circuit of IIG, s being State of SCS, o being OperSymbol of IIG holds (Den(o,SCS)).(o depends_on_in s) in (the Sorts of SCS).( the_result_sort_of o); theorem :: CIRCUIT1:9 for IIG for A being non-empty Circuit of IIG, v being Vertex of IIG, e being Element of (the Sorts of FreeEnv A).v st e.{} = [action_at v,the carrier of IIG] ex p being DTree-yielding FinSequence st e = [action_at v,the carrier of IIG]-tree p; begin :: Size registration let IIG be monotonic non void non empty ManySortedSign; let A be finite-yielding non-empty MSAlgebra over IIG; let v be SortSymbol of IIG; cluster (the Sorts of FreeEnv A).v -> finite; end; definition let IIG; let A be finite-yielding non-empty MSAlgebra over IIG; let v be SortSymbol of IIG; func size(v,A) -> Nat means :: CIRCUIT1:def 4 ex s being finite non empty Subset of NAT st s = the set of all card t where t is Element of (the Sorts of FreeEnv A).v & it = max s; end; theorem :: CIRCUIT1:10 for IIG for A being finite-yielding non-empty MSAlgebra over IIG , v being Element of IIG holds size(v,A) = 1 iff v in InputVertices IIG \/ SortsWithConstants IIG; theorem :: CIRCUIT1:11 for IIG for SCS being finite-yielding non-empty MSAlgebra over IIG, v, w being Vertex of IIG, e1 being Element of (the Sorts of FreeEnv SCS).v, e2 being Element of (the Sorts of FreeEnv SCS).w, q1 being DTree-yielding FinSequence st v in InnerVertices IIG \ SortsWithConstants IIG & card e1 = size (v,SCS) & e1 = [action_at v,the carrier of IIG]-tree q1 & e2 in rng q1 holds card e2 = size(w,SCS); theorem :: CIRCUIT1:12 for IIG for A being finite-yielding non-empty MSAlgebra over IIG , v being Vertex of IIG, e being Element of (the Sorts of FreeEnv A).v st v in (InnerVertices IIG \ SortsWithConstants IIG) & card e = size(v,A) ex q being DTree-yielding FinSequence st e = [action_at v,the carrier of IIG]-tree q; theorem :: CIRCUIT1:13 for IIG for A being finite-yielding non-empty MSAlgebra over IIG, v being Vertex of IIG, e being Element of (the Sorts of FreeEnv A).v st v in ( InnerVertices IIG \ SortsWithConstants IIG) & card e = size(v,A) ex o being OperSymbol of IIG st e.{} = [o,the carrier of IIG]; definition let S be non void non empty ManySortedSign, A be finite-yielding non-empty MSAlgebra over S, v be SortSymbol of S, e be Element of (the Sorts of FreeEnv A ).v; func depth e -> Element of NAT means :: CIRCUIT1:def 5 ex e9 being Element of (the Sorts of FreeMSA the Sorts of A).v st e = e9 & it = depth e9; end; theorem :: CIRCUIT1:14 for IIG for A being finite-yielding non-empty MSAlgebra over IIG , v, w being Element of IIG st v in InnerVertices IIG & w in rng the_arity_of action_at v holds size(w,A) < size(v,A); theorem :: CIRCUIT1:15 for IIG for A being finite-yielding non-empty MSAlgebra over IIG , v being SortSymbol of IIG holds size(v,A) > 0; theorem :: CIRCUIT1:16 for IIG for A being non-empty Circuit of IIG, v being Vertex of IIG, e being Element of (the Sorts of FreeEnv A).v, p being DTree-yielding FinSequence st v in InnerVertices IIG & e = [action_at v,the carrier of IIG]-tree p & for k being Element of NAT st k in dom p ex ek being Element of (the Sorts of FreeEnv A) .((the_arity_of action_at v)/.k) st ek = p.k & card ek = size ((the_arity_of action_at v)/.k, A) holds card e = size(v,A); begin :: Depth definition let S be monotonic non void non empty ManySortedSign, A be finite-yielding non-empty MSAlgebra over S, v be SortSymbol of S; func depth(v,A) -> Nat means :: CIRCUIT1:def 6 ex s being finite non empty Subset of NAT st s = the set of all depth t where t is Element of (the Sorts of FreeEnv A).v & it = max s; end; definition let IIG be finite monotonic Circuit-like non void non empty ManySortedSign , A be non-empty Circuit of IIG; func depth A -> Nat means :: CIRCUIT1:def 7 ex Ds being finite non empty Subset of NAT st Ds = { depth(v,A) where v is Element of IIG : v in the carrier of IIG } & it = max Ds; end; theorem :: CIRCUIT1:17 for IIG being finite monotonic Circuit-like non void non empty ManySortedSign, A being non-empty Circuit of IIG, v being Vertex of IIG holds depth(v,A) <= depth A; theorem :: CIRCUIT1:18 for IIG for A being non-empty Circuit of IIG, v being Vertex of IIG holds depth(v,A) = 0 iff v in InputVertices IIG or v in SortsWithConstants IIG; theorem :: CIRCUIT1:19 for IIG for A being finite-yielding non-empty MSAlgebra over IIG, v, v1 being SortSymbol of IIG st v in InnerVertices IIG & v1 in rng the_arity_of action_at v holds depth(v1,A) < depth(v,A);