:: Introduction to Circuits, II :: by Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec and Pauline N. Kawamoto :: :: Received April 10, 1995 :: Copyright (c) 1995-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 MSAFREE2, STRUCT_0, XBOOLE_0, MSUALG_1, RELAT_1, PBOOLE, MSAFREE, FUNCOP_1, FUNCT_1, TREES_3, FINSEQ_1, SUBSET_1, TREES_4, MSUALG_3, MARGREL1, FINSEQ_4, TARSKI, DTCONSTR, NAT_1, NUMBERS, TREES_2, CARD_3, PARTFUN1, ZFMISC_1, TDGROUP, CIRCUIT1, FSM_1, FUNCT_4, GLIB_000, UNIALG_2, MSATERM, PRELAMB, REALSET1, CARD_1, XXREAL_0, ARYTM_3, FUNCT_6, TREES_A, FINSET_1, CIRCUIT2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4, XXREAL_0, XCMPLX_0, NAT_1, FINSEQ_1, FINSEQ_2, FINSET_1, TREES_2, TREES_3, TREES_4, CARD_3, FUNCT_6, LANG1, DTCONSTR, PBOOLE, FUNCOP_1, XXREAL_2, STRUCT_0, PRALG_1, MSUALG_1, MSUALG_2, MSUALG_3, MSAFREE, MSAFREE2, CIRCUIT1, MSATERM; constructors PRALG_1, MSUALG_3, MSATERM, CIRCUIT1, SEQ_4, RELSET_1, FUNCT_4; registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1, XREAL_0, MEMBERED, FINSEQ_1, CARD_3, TREES_3, PRE_CIRC, STRUCT_0, MSUALG_1, MSUALG_3, MSAFREE, MSAFREE2, CIRCUIT1, XXREAL_2, CARD_1, RELSET_1, PBOOLE; requirements NUMERALS, BOOLE, SUBSET; begin reserve IIG for monotonic Circuit-like non void non empty ManySortedSign; theorem :: CIRCUIT2:1 for X being non-empty ManySortedSet of the carrier of IIG, H being ManySortedFunction of FreeMSA X, FreeMSA X, HH being Function-yielding Function, v being SortSymbol of IIG, p being DTree-yielding FinSequence, t being Element of (the Sorts of FreeMSA X).v st v in InnerVertices IIG & t = [action_at v,the carrier of IIG]-tree p & H is_homomorphism FreeMSA X, FreeMSA X & HH = H * the_arity_of action_at v ex HHp being DTree-yielding FinSequence st HHp = HH..p & H.v.t = [action_at v,the carrier of IIG]-tree HHp; definition let IIG; let SCS be non-empty Circuit of IIG, s be State of SCS, iv be InputValues of SCS; redefine func s +* iv -> State of SCS; end; definition let IIG; let A be non-empty Circuit of IIG, iv be InputValues of A; func Fix_inp iv -> ManySortedFunction of FreeGen the Sorts of A, the Sorts of FreeEnv A means :: CIRCUIT2:def 1 for v being Vertex of IIG holds (v in InputVertices IIG implies it.v = FreeGen(v, the Sorts of A) --> root-tree[iv.v, v]) & (v in SortsWithConstants IIG implies it.v = FreeGen(v, the Sorts of A) --> root-tree [action_at v,the carrier of IIG]) & (v in (InnerVertices IIG \ SortsWithConstants IIG) implies it.v = id FreeGen(v, the Sorts of A)); end; definition let IIG; let A be non-empty Circuit of IIG, iv be InputValues of A; func Fix_inp_ext iv -> ManySortedFunction of FreeEnv A, FreeEnv A means :: CIRCUIT2:def 2 it is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= it; end; theorem :: CIRCUIT2:2 for A being non-empty Circuit of IIG, iv being InputValues of A, v being Vertex of IIG, e being Element of (the Sorts of FreeEnv A).v, x being set st v in InnerVertices IIG \ SortsWithConstants IIG & e = root-tree[x,v] holds (Fix_inp_ext iv).v.e = e; theorem :: CIRCUIT2:3 for A being non-empty Circuit of IIG, iv being InputValues of A, v being Vertex of IIG, x being Element of (the Sorts of A).v st v in InputVertices IIG holds (Fix_inp_ext iv).v.(root-tree[x,v]) = root-tree[iv.v,v] ; theorem :: CIRCUIT2:4 for A being non-empty Circuit of IIG, iv being InputValues of A, v being Vertex of IIG, e being Element of (the Sorts of FreeEnv A).v, p, q being DTree-yielding FinSequence st v in InnerVertices IIG & e = [action_at v, the carrier of IIG]-tree p & dom p = dom q & for k being Element of NAT st k in dom p holds q.k = (Fix_inp_ext iv).((the_arity_of action_at v)/.k).(p.k) holds (Fix_inp_ext iv).v.e = [action_at v,the carrier of IIG]-tree q; theorem :: CIRCUIT2:5 for A being non-empty Circuit of IIG, iv being InputValues of A, v being Vertex of IIG, e being Element of (the Sorts of FreeEnv A).v st v in SortsWithConstants IIG holds (Fix_inp_ext iv).v.e = root-tree[action_at v,the carrier of IIG]; theorem :: CIRCUIT2:6 for A being non-empty Circuit of IIG, iv being InputValues of A, v being Vertex of IIG, e, e1 being Element of (the Sorts of FreeEnv A).v, t, t1 being DecoratedTree st t = e & t1 = e1 & e1 = (Fix_inp_ext iv).v.e holds dom t = dom t1; theorem :: CIRCUIT2:7 for A being non-empty Circuit of IIG, iv being InputValues of A, v being Vertex of IIG, e, e1 being Element of (the Sorts of FreeEnv A).v st e1 = (Fix_inp_ext iv).v.e holds card e = card e1; definition let IIG; let SCS be non-empty Circuit of IIG, v be Vertex of IIG, iv be InputValues of SCS; func IGTree(v,iv) -> Element of (the Sorts of FreeEnv SCS).v means :: CIRCUIT2:def 3 ex e being Element of (the Sorts of FreeEnv SCS).v st card e = size(v,SCS) & it = (Fix_inp_ext iv).v.e; end; theorem :: CIRCUIT2:8 for SCS being non-empty Circuit of IIG, v being Vertex of IIG, iv being InputValues of SCS holds IGTree(v,iv) = (Fix_inp_ext iv).v.IGTree(v,iv); theorem :: CIRCUIT2:9 for SCS being non-empty Circuit of IIG, v being Vertex of IIG, iv being InputValues of SCS, p being DTree-yielding FinSequence st v in InnerVertices IIG & dom p = dom the_arity_of action_at v & for k being Element of NAT st k in dom p holds p.k = IGTree((the_arity_of action_at v)/.k, iv) holds IGTree(v,iv) = [action_at v,the carrier of IIG]-tree p; definition let IIG; let SCS be non-empty Circuit of IIG, v be Vertex of IIG, iv be InputValues of SCS; func IGValue(v,iv) -> Element of (the Sorts of SCS).v equals :: CIRCUIT2:def 4 (Eval SCS).v.(IGTree(v,iv)); end; theorem :: CIRCUIT2:10 for SCS being non-empty Circuit of IIG, v being Vertex of IIG, iv being InputValues of SCS st v in InputVertices IIG holds IGValue(v,iv) = iv. v; theorem :: CIRCUIT2:11 for SCS being non-empty Circuit of IIG, v being Vertex of IIG, iv being InputValues of SCS st v in SortsWithConstants IIG holds IGValue(v,iv) = (Set-Constants SCS).v; begin ::--------------------------------------------------------------------------- :: Computations ::--------------------------------------------------------------------------- definition let IIG be Circuit-like non void non empty ManySortedSign; let SCS be non-empty Circuit of IIG, s be State of SCS; func Following s -> State of SCS means :: CIRCUIT2:def 5 for v being Vertex of IIG holds (v in InputVertices IIG implies it.v = s.v) & (v in InnerVertices IIG implies it.v = (Den(action_at v,SCS)).(action_at v depends_on_in s)); end; theorem :: CIRCUIT2:12 for SCS being non-empty Circuit of IIG, s being State of SCS, iv being InputValues of SCS st iv c= s holds iv c= Following s; definition let IIG be Circuit-like non void non empty ManySortedSign; let SCS be non-empty Circuit of IIG; let IT be State of SCS; attr IT is stable means :: CIRCUIT2:def 6 IT = Following IT; end; definition let IIG; let SCS be non-empty Circuit of IIG, s be State of SCS, iv be InputValues of SCS; func Following(s,iv) -> State of SCS equals :: CIRCUIT2:def 7 Following(s+*iv); end; definition let IIG; let SCS be non-empty Circuit of IIG, InpFs be InputFuncs of SCS, s be State of SCS; func InitialComp(s,InpFs) -> State of SCS equals :: CIRCUIT2:def 8 s +* (0-th_InputValues InpFs) +* Set-Constants SCS; end; definition let IIG; let SCS be non-empty Circuit of IIG, InpFs be InputFuncs of SCS, s be State of SCS; func Computation(s,InpFs) -> sequence of (product the Sorts of SCS) means :: CIRCUIT2:def 9 it.0 = InitialComp(s,InpFs) & for i being Nat holds it.(i+1) = Following(it.i,(i+1)-th_InputValues InpFs); end; reserve SCS for non-empty Circuit of IIG; reserve s for State of SCS; reserve iv for InputValues of SCS; theorem :: CIRCUIT2:13 for k being Nat st for v being Vertex of IIG st depth (v,SCS) <= k holds s.v = IGValue(v,iv) holds for v1 being Vertex of IIG st depth(v1,SCS) <= k+1 holds (Following s).v1 = IGValue(v1,iv); reserve IIG for finite monotonic Circuit-like non void non empty ManySortedSign; reserve SCS for non-empty Circuit of IIG; reserve InpFs for InputFuncs of SCS; reserve s for State of SCS; reserve iv for InputValues of SCS; theorem :: CIRCUIT2:14 commute InpFs is constant & InputVertices IIG is non empty implies for s, iv st iv = (commute InpFs).0 for k being Nat holds iv c= (Computation(s,InpFs)).k; theorem :: CIRCUIT2:15 for n being Element of NAT st commute InpFs is constant & InputVertices IIG is non empty & (Computation(s,InpFs)).n is stable for m being Nat st n <= m holds (Computation(s,InpFs)).n = (Computation(s,InpFs)).m; theorem :: CIRCUIT2:16 commute InpFs is constant & InputVertices IIG is non empty implies for s, iv st iv = (commute InpFs).0 for k being Nat, v being Vertex of IIG st depth(v,SCS) <= k holds ((Computation(s,InpFs)).k qua Element of product the Sorts of SCS).v = IGValue(v,iv); theorem :: CIRCUIT2:17 commute InpFs is constant & InputVertices IIG is non empty & iv = (commute InpFs).0 implies for s being State of SCS, v being Vertex of IIG, n being Element of NAT st n = depth SCS holds ((Computation(s,InpFs)).n qua State of SCS).v = IGValue(v,iv); theorem :: CIRCUIT2:18 commute InpFs is constant & InputVertices IIG is non empty implies for s being State of SCS, n be Element of NAT st n = depth SCS holds (Computation(s ,InpFs)).n is stable; theorem :: CIRCUIT2:19 commute InpFs is constant & InputVertices IIG is non empty implies for s1, s2 being State of SCS holds (Computation(s1,InpFs)).(depth SCS) = ( Computation(s2,InpFs)).(depth SCS);