:: Circuit Generated by Terms and Circuit Calculating Terms :: by Grzegorz Bancerek :: :: Received April 10, 2001 :: Copyright (c) 2001-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 XBOOLE_0, STRUCT_0, MSUALG_1, RELAT_1, MSATERM, SUBSET_1, FUNCT_1, TREES_4, MSAFREE, PBOOLE, TREES_9, ZFMISC_1, FUNCT_3, CIRCCOMB, GLIB_000, TREES_1, FINSEQ_1, NUMBERS, ORDINAL4, MARGREL1, TREES_3, FINSET_1, TREES_2, PARTFUN1, FUNCT_4, MSAFREE2, MCART_1, TARSKI, FUNCOP_1, CARD_3, QC_LANG1, FSM_1, CIRCUIT2, FACIRC_1, FUNCT_6, TREES_A, ARYTM_3, XXREAL_0, NAT_1, CARD_1, PUA2MSS1, REWRITE1, CQC_SIM1, CIRCUIT1, CIRCTRM1, SETLIM_2; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSET_1, PARTFUN1, MCART_1, FINSEQ_2, FUNCT_4, CARD_3, FUNCOP_1, FUNCT_3, STRUCT_0, PBOOLE, MSUALG_1, MSAFREE2, CIRCUIT1, CIRCUIT2, CIRCCOMB, FACIRC_1, TREES_1, TREES_2, TREES_3, TREES_4, TREES_9, MSATERM, PUA2MSS1, XXREAL_0; constructors TREES_9, MSUALG_3, MSATERM, CIRCUIT1, CIRCUIT2, FACIRC_1, PUA2MSS1, INSTALG1, NAT_1, XREAL_0, RELSET_1, XTUPLE_0, NUMBERS; registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCOP_1, XREAL_0, FINSEQ_1, CARD_3, PBOOLE, TREES_2, TREES_3, TREES_9, STRUCT_0, MSUALG_1, MSUALG_2, MSAFREE, MSATERM, CIRCCOMB, INSTALG1, ORDINAL1, FINSET_1, CARD_1, RELSET_1, NAT_1, XTUPLE_0; requirements NUMERALS, BOOLE, SUBSET; begin :: Circuit structure generated by terms theorem :: CIRCTRM1:1 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for V being Variables of A for t being Term of S,V, T being c-Term of A,V st T = t holds the_sort_of T = the_sort_of t; definition let S be non empty non void ManySortedSign; let V be non-empty ManySortedSet of the carrier of S; let X be non empty Subset of S-Terms V; func X-CircuitStr -> non empty strict ManySortedSign equals :: CIRCTRM1:def 1 ManySortedSign(# Subtrees X, [:the carrier' of S,{the carrier of S}:]-Subtrees X, [:the carrier' of S,{the carrier of S}:]-ImmediateSubtrees X, incl([:the carrier' of S,{the carrier of S}:]-Subtrees X) #); end; registration let S be non empty non void ManySortedSign; let V be non-empty ManySortedSet of the carrier of S; let X be non empty Subset of S-Terms V; cluster X-CircuitStr -> unsplit; end; reserve S for non empty non void ManySortedSign, V for non-empty ManySortedSet of the carrier of S, A for non-empty MSAlgebra over S, X for non empty Subset of S-Terms V, t for Element of X; theorem :: CIRCTRM1:2 X-CircuitStr is void iff for t being Element of X holds t is root & not t.{} in [:the carrier' of S, {the carrier of S}:]; theorem :: CIRCTRM1:3 X is SetWithCompoundTerm of S,V iff X-CircuitStr is non void; registration let S be non empty non void ManySortedSign; let V be non-empty ManySortedSet of the carrier of S; let X be SetWithCompoundTerm of S,V; cluster X-CircuitStr -> non void; end; theorem :: CIRCTRM1:4 (for v being Vertex of X-CircuitStr holds v is Term of S,V) & for s being set st s in the carrier' of X-CircuitStr holds s is CompoundTerm of S,V; theorem :: CIRCTRM1:5 for t being Vertex of X-CircuitStr holds t in the carrier' of X-CircuitStr iff t is CompoundTerm of S,V; registration let S,V; let X be SetWithCompoundTerm of S,V, g be Gate of X-CircuitStr; cluster the_arity_of g -> DTree-yielding; end; registration let S be non empty non void ManySortedSign; let V be non-empty ManySortedSet of the carrier of S; let X be non empty Subset of S-Terms V; cluster -> finite Function-like Relation-like for Vertex of X-CircuitStr; end; registration let S be non empty non void ManySortedSign; let V be non-empty ManySortedSet of the carrier of S; let X be non empty Subset of S-Terms V; cluster -> DecoratedTree-like for Vertex of X-CircuitStr; end; registration let S be non empty non void ManySortedSign; let V be non-empty ManySortedSet of the carrier of S; let X be SetWithCompoundTerm of S,V; cluster -> finite Function-like Relation-like for Gate of X-CircuitStr; end; registration let S be non empty non void ManySortedSign; let V be non-empty ManySortedSet of the carrier of S; let X be SetWithCompoundTerm of S,V; cluster -> DecoratedTree-like for Gate of X-CircuitStr; end; ::theorem :: for X being SetWithCompoundTerm of A,V, g being Gate of X-CircuitStr :: for t being Term of A,V st t = g holds :: the_arity_of g = subs t ? subs g theorem :: CIRCTRM1:6 for X1,X2 being non empty Subset of S-Terms V holds the Arity of X1-CircuitStr tolerates the Arity of X2-CircuitStr & the ResultSort of X1-CircuitStr tolerates the ResultSort of X2-CircuitStr; registration let X,Y be constituted-DTrees set; cluster X \/ Y -> constituted-DTrees; end; theorem :: CIRCTRM1:7 for X1,X2 being constituted-DTrees non empty set holds Subtrees (X1 \/ X2) = (Subtrees X1) \/ (Subtrees X2); theorem :: CIRCTRM1:8 for X1,X2 being constituted-DTrees non empty set, C be set holds C-Subtrees (X1 \/ X2) = (C-Subtrees X1) \/ (C-Subtrees X2); theorem :: CIRCTRM1:9 for X1,X2 being constituted-DTrees non empty set st (for t being Element of X1 holds t is finite) & (for t being Element of X2 holds t is finite) for C be set holds C-ImmediateSubtrees (X1 \/ X2) = (C-ImmediateSubtrees X1)+*(C-ImmediateSubtrees X2); theorem :: CIRCTRM1:10 for X1,X2 being non empty Subset of S-Terms V holds (X1 \/ X2)-CircuitStr = (X1-CircuitStr)+*(X2-CircuitStr); theorem :: CIRCTRM1:11 for x being set holds x in InputVertices (X-CircuitStr) iff x in Subtrees X & ex s being SortSymbol of S, v being Element of V.s st x = root-tree [v,s]; theorem :: CIRCTRM1:12 for X being SetWithCompoundTerm of S,V, g being Gate of X-CircuitStr holds g = (g.{})-tree the_arity_of g; begin :: Circuit genereted by terms definition let S be non empty non void ManySortedSign; let V be non-empty ManySortedSet of the carrier of S; let X be non empty Subset of S-Terms V; let v be Vertex of X-CircuitStr; let A be MSAlgebra over S; func the_sort_of (v, A) -> set means :: CIRCTRM1:def 2 for u being Term of S,V st u = v holds it = (the Sorts of A).the_sort_of u; end; registration let S be non empty non void ManySortedSign; let V be non-empty ManySortedSet of the carrier of S; let X be non empty Subset of S-Terms V; let v be Vertex of X-CircuitStr; let A be non-empty MSAlgebra over S; cluster the_sort_of (v, A) -> non empty; end; definition let S be non empty non void ManySortedSign; let V be non-empty ManySortedSet of the carrier of S; let X be non empty Subset of S-Terms V; assume X is SetWithCompoundTerm of S,V; let o be Gate of X-CircuitStr; let A be MSAlgebra over S; func the_action_of (o, A) -> Function means :: CIRCTRM1:def 3 for X9 being SetWithCompoundTerm of S,V st X9 = X for o9 being Gate of X9-CircuitStr st o9 = o holds it = (the Charact of A).(o9.{})`1; end; scheme :: CIRCTRM1:sch 1 MSFuncEx {I() -> non empty set, A,B() -> non-empty ManySortedSet of I(), P[object,object,object]}: ex f being ManySortedFunction of A(),B() st for i being Element of I(), a being Element of A().i holds P[i,a,f.i.a] provided for i being Element of I(), a being Element of A().i ex b being Element of B().i st P[i,a,b]; definition let S be non empty non void ManySortedSign; let V be non-empty ManySortedSet of the carrier of S; let X be non empty Subset of S-Terms V; let A be MSAlgebra over S; func X-CircuitSorts A -> ManySortedSet of the carrier of X-CircuitStr means :: CIRCTRM1:def 4 for v being Vertex of X-CircuitStr holds it.v = the_sort_of (v, A); end; registration let S be non empty non void ManySortedSign; let V be non-empty ManySortedSet of the carrier of S; let X be non empty Subset of S-Terms V; let A be non-empty MSAlgebra over S; cluster X-CircuitSorts A -> non-empty; end; theorem :: CIRCTRM1:13 for X being SetWithCompoundTerm of S,V, g being Gate of X-CircuitStr for o being OperSymbol of S st g.{} = [o,the carrier of S] holds (X-CircuitSorts A)*the_arity_of g = (the Sorts of A)*the_arity_of o; definition let S be non empty non void ManySortedSign; let V be non-empty ManySortedSet of the carrier of S; let X be non empty Subset of S-Terms V; let A be non-empty MSAlgebra over S; func X-CircuitCharact A -> ManySortedFunction of (X-CircuitSorts A)#*(the Arity of X-CircuitStr), (X-CircuitSorts A)*(the ResultSort of X-CircuitStr) means :: CIRCTRM1:def 5 for g being Gate of X-CircuitStr st g in the carrier' of X-CircuitStr holds it.g = the_action_of (g, A); end; definition let S be non empty non void ManySortedSign; let V be non-empty ManySortedSet of the carrier of S; let X be non empty Subset of S-Terms V; let A be non-empty MSAlgebra over S; func X-Circuit A -> non-empty strict MSAlgebra over X-CircuitStr equals :: CIRCTRM1:def 6 MSAlgebra(#X-CircuitSorts A, X-CircuitCharact A#); end; theorem :: CIRCTRM1:14 for v being Vertex of X-CircuitStr holds (the Sorts of X-Circuit A).v = the_sort_of (v, A); theorem :: CIRCTRM1:15 for A being finite-yielding non-empty MSAlgebra over S for X being SetWithCompoundTerm of S,V for g being OperSymbol of X-CircuitStr holds Den(g, X-Circuit A) = the_action_of (g, A); theorem :: CIRCTRM1:16 for A being finite-yielding non-empty MSAlgebra over S for X being SetWithCompoundTerm of S,V for g being OperSymbol of X-CircuitStr, o being OperSymbol of S st g.{} = [o, the carrier of S] holds Den(g, X-Circuit A) = Den(o,A); theorem :: CIRCTRM1:17 for A being finite-yielding non-empty MSAlgebra over S, X being non empty Subset of S-Terms V holds X-Circuit A is finite-yielding; registration let S be non empty non void ManySortedSign; let V be non-empty ManySortedSet of the carrier of S; let X be SetWithCompoundTerm of S,V; let A be finite-yielding non-empty MSAlgebra over S; cluster X-Circuit A -> finite-yielding; end; theorem :: CIRCTRM1:18 for S being non empty non void ManySortedSign for V being non-empty ManySortedSet of the carrier of S for X1,X2 being SetWithCompoundTerm of S,V for A being non-empty MSAlgebra over S holds X1-Circuit A tolerates X2-Circuit A; theorem :: CIRCTRM1:19 for S being non empty non void ManySortedSign for V being non-empty ManySortedSet of the carrier of S for X1,X2 being SetWithCompoundTerm of S,V for A being non-empty MSAlgebra over S holds (X1 \/ X2)-Circuit A = (X1-Circuit A)+*(X2-Circuit A); begin :: Correctness of a Term Circuit reserve S for non empty non void ManySortedSign, A for non-empty finite-yielding MSAlgebra over S, V for Variables of A, X for SetWithCompoundTerm of S,V; definition let S be non empty non void ManySortedSign; let A be non-empty MSAlgebra over S; let V be Variables of A; let t be DecoratedTree such that t is Term of S,V; let f be ManySortedFunction of V, the Sorts of A; func t@(f,A) -> set means :: CIRCTRM1:def 7 ex t9 being c-Term of A,V st t9 = t & it = t9@f; end; definition let S be non empty non void ManySortedSign; let V be non-empty ManySortedSet of the carrier of S; let X be SetWithCompoundTerm of S,V; let A be non-empty finite-yielding MSAlgebra over S; let s be State of X-Circuit A; mode CompatibleValuation of s -> ManySortedFunction of V, the Sorts of A means :: CIRCTRM1:def 8 for x being Vertex of S, v being Element of V.x st root-tree [v,x] in Subtrees X holds it.x.v = s.root-tree [v,x]; end; theorem :: CIRCTRM1:20 for s being State of X-Circuit A for f being CompatibleValuation of s, n being Element of NAT holds f is CompatibleValuation of Following(s,n); registration let x be object; let S be non empty non void ManySortedSign; let V be non-empty ManySortedSet of the carrier of S; let p be FinSequence of S-Terms V; cluster x-tree p -> finite; end; theorem :: CIRCTRM1:21 for s being State of X-Circuit A for f being CompatibleValuation of s for t being Term of S,V st t in Subtrees X holds Following(s, 1+height dom t) is_stable_at t & Following(s, 1+height dom t).t = t@(f,A); theorem :: CIRCTRM1:22 not (ex t being Term of S,V, o being OperSymbol of S st t in Subtrees X & t.{} = [o,the carrier of S] & the_arity_of o = {}) implies for s being State of X-Circuit A for f being CompatibleValuation of s for t being Term of S,V st t in Subtrees X holds Following(s, height dom t) is_stable_at t & Following(s, height dom t).t = t@(f, A); begin :: Circuit similarity definition let S1, S2 be non empty ManySortedSign; let f,g be Function; pred S1, S2 are_equivalent_wrt f, g means :: CIRCTRM1:def 9 f is one-to-one & g is one-to-one & f, g form_morphism_between S1, S2 & f", g" form_morphism_between S2, S1; end; theorem :: CIRCTRM1:23 for S1, S2 being non empty ManySortedSign, f,g being Function st S1, S2 are_equivalent_wrt f, g holds the carrier of S2 = f.:the carrier of S1 & the carrier' of S2 = g.:the carrier' of S1; theorem :: CIRCTRM1:24 for S1, S2 being non empty ManySortedSign, f,g being Function st S1, S2 are_equivalent_wrt f, g holds rng f = the carrier of S2 & rng g = the carrier' of S2; theorem :: CIRCTRM1:25 for S being non empty ManySortedSign holds S, S are_equivalent_wrt id the carrier of S, id the carrier' of S; theorem :: CIRCTRM1:26 for S1, S2 being non empty ManySortedSign, f,g being Function st S1, S2 are_equivalent_wrt f, g holds S2, S1 are_equivalent_wrt f", g"; theorem :: CIRCTRM1:27 for S1, S2, S3 being non empty ManySortedSign, f1,g1, f2,g2 being Function st S1, S2 are_equivalent_wrt f1, g1 & S2, S3 are_equivalent_wrt f2, g2 holds S1, S3 are_equivalent_wrt f2*f1, g2*g1; theorem :: CIRCTRM1:28 for S1, S2 being non empty ManySortedSign, f,g being Function st S1, S2 are_equivalent_wrt f, g holds f.:InputVertices S1 = InputVertices S2 & f.:InnerVertices S1 = InnerVertices S2; definition let S1, S2 be non empty ManySortedSign; pred S1, S2 are_equivalent means :: CIRCTRM1:def 10 ex f,g being one-to-one Function st S1, S2 are_equivalent_wrt f, g; reflexivity; symmetry; end; theorem :: CIRCTRM1:29 for S1, S2, S3 being non empty ManySortedSign st S1, S2 are_equivalent & S2, S3 are_equivalent holds S1, S3 are_equivalent; definition let S1, S2 be non empty ManySortedSign; let f be Function; pred f preserves_inputs_of S1, S2 means :: CIRCTRM1:def 11 f.:InputVertices S1 c= InputVertices S2; end; theorem :: CIRCTRM1:30 for S1, S2 being non empty ManySortedSign for f, g being Function st f, g form_morphism_between S1, S2 for v being Vertex of S1 holds f.v is Vertex of S2; theorem :: CIRCTRM1:31 for S1, S2 being non empty non void ManySortedSign for f, g being Function st f, g form_morphism_between S1, S2 for v being Gate of S1 holds g.v is Gate of S2; theorem :: CIRCTRM1:32 for S1, S2 being non empty ManySortedSign for f, g being Function st f, g form_morphism_between S1, S2 holds f.:InnerVertices S1 c= InnerVertices S2; theorem :: CIRCTRM1:33 for S1, S2 being Circuit-like non void non empty ManySortedSign for f, g being Function st f, g form_morphism_between S1, S2 for v1 being Vertex of S1 st v1 in InnerVertices S1 for v2 being Vertex of S2 st v2 = f.v1 holds action_at v2 = g.action_at v1; definition let S1, S2 be non empty ManySortedSign; let f,g be Function; let C1 be non-empty MSAlgebra over S1; let C2 be non-empty MSAlgebra over S2; pred f, g form_embedding_of C1, C2 means :: CIRCTRM1:def 12 f is one-to-one & g is one-to-one & f, g form_morphism_between S1, S2 & the Sorts of C1 = (the Sorts of C2)*f & the Charact of C1 = (the Charact of C2)*g; end; theorem :: CIRCTRM1:34 for S being non empty ManySortedSign for C being non-empty MSAlgebra over S holds id the carrier of S, id the carrier' of S form_embedding_of C, C; theorem :: CIRCTRM1:35 for S1,S2,S3 being non empty ManySortedSign for f1,g1, f2,g2 being Function for C1 being non-empty MSAlgebra over S1 for C2 being non-empty MSAlgebra over S2 for C3 being non-empty MSAlgebra over S3 st f1,g1 form_embedding_of C1,C2 & f2,g2 form_embedding_of C2,C3 holds f2*f1, g2*g1 form_embedding_of C1, C3; definition let S1, S2 be non empty ManySortedSign; let f,g be Function; let C1 be non-empty MSAlgebra over S1; let C2 be non-empty MSAlgebra over S2; pred C1, C2 are_similar_wrt f, g means :: CIRCTRM1:def 13 f, g form_embedding_of C1, C2 & f", g" form_embedding_of C2, C1; end; theorem :: CIRCTRM1:36 for S1, S2 being non empty ManySortedSign for f, g being Function for C1 being non-empty MSAlgebra over S1 for C2 being non-empty MSAlgebra over S2 st C1, C2 are_similar_wrt f, g holds S1, S2 are_equivalent_wrt f, g; theorem :: CIRCTRM1:37 for S1, S2 being non empty ManySortedSign for f, g being Function for C1 being non-empty MSAlgebra over S1 for C2 being non-empty MSAlgebra over S2 holds C1, C2 are_similar_wrt f, g iff S1, S2 are_equivalent_wrt f, g & the Sorts of C1 = (the Sorts of C2)*f & the Charact of C1 = (the Charact of C2)*g; theorem :: CIRCTRM1:38 for S being non empty ManySortedSign for C being non-empty MSAlgebra over S holds C, C are_similar_wrt id the carrier of S, id the carrier' of S; theorem :: CIRCTRM1:39 for S1, S2 being non empty ManySortedSign for f, g being Function for C1 being non-empty MSAlgebra over S1 for C2 being non-empty MSAlgebra over S2 st C1, C2 are_similar_wrt f, g holds C2, C1 are_similar_wrt f", g"; theorem :: CIRCTRM1:40 for S1, S2, S3 being non empty ManySortedSign for f1, g1, f2, g2 being Function for C1 being non-empty MSAlgebra over S1 for C2 being non-empty MSAlgebra over S2 for C3 being non-empty MSAlgebra over S3 st C1, C2 are_similar_wrt f1, g1 & C2, C3 are_similar_wrt f2, g2 holds C1, C3 are_similar_wrt f2*f1, g2*g1; definition let S1, S2 be non empty ManySortedSign; let C1 be non-empty MSAlgebra over S1; let C2 be non-empty MSAlgebra over S2; pred C1, C2 are_similar means :: CIRCTRM1:def 14 ex f, g being Function st C1, C2 are_similar_wrt f, g; end; reserve G1, G2 for Circuit-like non void non empty ManySortedSign, f, g for Function, C1 for non-empty Circuit of G1, C2 for non-empty Circuit of G2; theorem :: CIRCTRM1:41 f, g form_embedding_of C1, C2 implies dom f = the carrier of G1 & rng f c= the carrier of G2 & dom g = the carrier' of G1 & rng g c= the carrier' of G2; theorem :: CIRCTRM1:42 f, g form_embedding_of C1, C2 implies for o1 being Gate of G1, o2 being Gate of G2 st o2 = g.o1 holds Den(o2, C2) = Den(o1, C1); theorem :: CIRCTRM1:43 f, g form_embedding_of C1, C2 implies for o1 being Gate of G1, o2 being Gate of G2 st o2 = g.o1 for s1 being State of C1, s2 being State of C2 st s1 = s2*f holds o2 depends_on_in s2 = o1 depends_on_in s1; theorem :: CIRCTRM1:44 f, g form_embedding_of C1, C2 implies for s being State of C2 holds s*f is State of C1; theorem :: CIRCTRM1:45 f, g form_embedding_of C1, C2 implies for s2 being State of C2, s1 being State of C1 st s1 = s2*f & for v being Vertex of G1 st v in InputVertices G1 holds s2 is_stable_at f.v holds Following s1 = (Following s2)*f; theorem :: CIRCTRM1:46 f, g form_embedding_of C1, C2 & f preserves_inputs_of G1, G2 implies for s2 being State of C2, s1 being State of C1 st s1 = s2*f holds Following s1 = (Following s2)*f; theorem :: CIRCTRM1:47 f, g form_embedding_of C1, C2 & f preserves_inputs_of G1, G2 implies for s2 being State of C2, s1 being State of C1 st s1 = s2*f for n being Nat holds Following(s1,n) = Following(s2,n)*f; theorem :: CIRCTRM1:48 f, g form_embedding_of C1, C2 & f preserves_inputs_of G1, G2 implies for s2 being State of C2, s1 being State of C1 st s1 = s2*f holds s2 is stable implies s1 is stable; theorem :: CIRCTRM1:49 f, g form_embedding_of C1, C2 & f preserves_inputs_of G1, G2 implies for s2 being State of C2, s1 being State of C1 st s1 = s2*f for v1 being Vertex of G1 holds s1 is_stable_at v1 iff s2 is_stable_at f.v1; theorem :: CIRCTRM1:50 C1, C2 are_similar_wrt f, g implies for s being State of C2 holds s*f is State of C1; theorem :: CIRCTRM1:51 C1, C2 are_similar_wrt f, g implies for s1 being State of C1, s2 being State of C2 holds s1 = s2*f iff s2 = s1*f"; theorem :: CIRCTRM1:52 C1, C2 are_similar_wrt f, g implies f.:InputVertices G1 = InputVertices G2 & f.:InnerVertices G1 = InnerVertices G2; theorem :: CIRCTRM1:53 C1, C2 are_similar_wrt f, g implies f preserves_inputs_of G1, G2; theorem :: CIRCTRM1:54 C1, C2 are_similar_wrt f, g implies for s1 being State of C1, s2 being State of C2 st s1 = s2*f holds Following s1 = (Following s2)*f; theorem :: CIRCTRM1:55 C1, C2 are_similar_wrt f, g implies for s1 being State of C1, s2 being State of C2 st s1 = s2*f for n being Element of NAT holds Following(s1,n) = Following(s2,n)*f; theorem :: CIRCTRM1:56 C1, C2 are_similar_wrt f, g implies for s1 being State of C1, s2 being State of C2 st s1 = s2*f holds s1 is stable iff s2 is stable; theorem :: CIRCTRM1:57 C1, C2 are_similar_wrt f, g implies for s1 being State of C1, s2 being State of C2 st s1 = s2*f for v1 being Vertex of G1 holds s1 is_stable_at v1 iff s2 is_stable_at f.v1; begin :: Term specification definition let S be non empty non void ManySortedSign; let A be non-empty MSAlgebra over S; let V be non-empty ManySortedSet of the carrier of S; let X be non empty Subset of S-Terms V; let G be Circuit-like non void non empty ManySortedSign; let C be non-empty Circuit of G; pred C calculates X, A means :: CIRCTRM1:def 15 ex f, g st f, g form_embedding_of X-Circuit A, C & f preserves_inputs_of X-CircuitStr, G; pred X, A specifies C means :: CIRCTRM1:def 16 C, X-Circuit A are_similar; end; definition let S be non empty non void ManySortedSign; let V be non-empty ManySortedSet of the carrier of S; let A be non-empty MSAlgebra over S; let X be non empty Subset of S-Terms V; let G be Circuit-like non void non empty ManySortedSign; let C be non-empty Circuit of G; assume C calculates X, A; mode SortMap of X, A, C -> one-to-one Function means :: CIRCTRM1:def 17 it preserves_inputs_of X-CircuitStr, G & ex g st it, g form_embedding_of X-Circuit A, C; end; definition let S be non empty non void ManySortedSign; let V be non-empty ManySortedSet of the carrier of S; let A be non-empty MSAlgebra over S; let X be non empty Subset of S-Terms V; let G be Circuit-like non void non empty ManySortedSign; let C be non-empty Circuit of G such that C calculates X, A; let f be SortMap of X, A, C; mode OperMap of X, A, C, f -> one-to-one Function means :: CIRCTRM1:def 18 f, it form_embedding_of X-Circuit A, C; end; theorem :: CIRCTRM1:58 for G being Circuit-like non void non empty ManySortedSign for C being non-empty Circuit of G st X, A specifies C holds C calculates X, A; theorem :: CIRCTRM1:59 for G being Circuit-like non void non empty ManySortedSign for C being non-empty Circuit of G st C calculates X, A for f being SortMap of X, A, C for t being Term of S,V st t in Subtrees X for s being State of C holds Following(s, 1+height dom t) is_stable_at f.t & for s9 being State of X-Circuit A st s9 = s*f for h being CompatibleValuation of s9 holds Following(s, 1+height dom t).(f.t) = t@(h, A); theorem :: CIRCTRM1:60 for G being Circuit-like non void non empty ManySortedSign for C being non-empty Circuit of G st C calculates X, A for t being Term of S,V st t in Subtrees X ex v being Vertex of G st for s being State of C holds Following(s, 1+height dom t) is_stable_at v & ex f being SortMap of X, A, C st for s9 being State of X-Circuit A st s9 = s*f for h being CompatibleValuation of s9 holds Following(s, 1+height dom t).v = t@(h, A); theorem :: CIRCTRM1:61 for G being Circuit-like non void non empty ManySortedSign for C being non-empty Circuit of G st X, A specifies C for f being SortMap of X, A, C for s being State of C, t being Term of S,V st t in Subtrees X holds Following(s, 1+height dom t) is_stable_at f.t & for s9 being State of X-Circuit A st s9 = s*f for h being CompatibleValuation of s9 holds Following(s, 1+height dom t).(f.t) = t@(h, A); theorem :: CIRCTRM1:62 for G being Circuit-like non void non empty ManySortedSign for C being non-empty Circuit of G st X, A specifies C for t being Term of S,V st t in Subtrees X ex v being Vertex of G st for s being State of C holds Following(s, 1+height dom t) is_stable_at v & ex f being SortMap of X, A, C st for s9 being State of X-Circuit A st s9 = s*f for h being CompatibleValuation of s9 holds Following(s, 1+height dom t).v = t@(h, A);