Volume 13, 2001

University of Bialystok

Copyright (c) 2001 Association of Mizar Users

### The abstract of the Mizar article:

### Circuit Generated by Terms and Circuit Calculating Terms

**by****Grzegorz Bancerek**- Received April 10, 2001
- MML identifier: CIRCTRM1

- [ Mizar article, MML identifier index ]

environ vocabulary AMI_1, MSUALG_1, ZF_REFLE, MSATERM, FUNCT_1, TREES_4, FREEALG, RELAT_1, BOOLE, PBOOLE, TREES_9, CIRCCOMB, MSAFREE2, TREES_1, FINSEQ_1, QC_LANG1, TREES_3, FINSET_1, TREES_2, PARTFUN1, FUNCT_4, MCART_1, PRALG_1, TDGROUP, CARD_3, PRE_CIRC, FACIRC_1, FUNCT_6, PUA2MSS1, ISOCAT_1, CQC_SIM1, CIRCUIT1, CIRCUIT2, CIRCTRM1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSET_1, PARTFUN1, MCART_1, FUNCT_4, CARD_3, STRUCT_0, PRALG_1, PBOOLE, MSUALG_1, PRE_CIRC, MSAFREE2, CIRCUIT1, CIRCUIT2, CIRCCOMB, FACIRC_1, TREES_1, TREES_2, TREES_3, TREES_4, TREES_9, MSATERM, PUA2MSS1; constructors TREES_9, MSATERM, FINSEQ_4, MSUALG_3, CIRCUIT1, CIRCUIT2, FACIRC_1, PUA2MSS1, INSTALG1; clusters ARYTM_3, SUBSET_1, STRUCT_0, PRELAMB, FUNCT_1, RELSET_1, FINSEQ_1, MSUALG_1, MSUALG_2, TREES_2, TREES_3, XBOOLE_0, TREES_9, PRALG_1, MSAFREE, MSATERM, PRE_CIRC, CIRCCOMB, INSTALG1, MEMBERED; requirements NUMERALS, BOOLE, SUBSET; begin :: <section1>Circuit structure generated by terms</section1> 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 D be non empty set; let X be Subset of D; redefine func id X -> Function of X, D; 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; func X-CircuitStr -> non empty strict ManySortedSign equals :: CIRCTRM1:def 1 ManySortedSign(# Subtrees X, [:the OperSymbols of S,{the carrier of S}:]-Subtrees X, [:the OperSymbols of S,{the carrier of S}:]-ImmediateSubtrees X, id ([:the OperSymbols of S,{the carrier of S}:]-Subtrees X) #); 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; 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 OperSymbols of S, {the carrier of S}:]; theorem :: CIRCTRM1:3 X is SetWithCompoundTerm of S,V iff X-CircuitStr is non void; 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; 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 OperSymbols of X-CircuitStr holds s is CompoundTerm of S,V); theorem :: CIRCTRM1:5 for t being Vertex of X-CircuitStr holds t in the OperSymbols of X-CircuitStr iff t is CompoundTerm of S,V; theorem :: CIRCTRM1:6 for X being SetWithCompoundTerm of S,V, g being Gate of X-CircuitStr holds (the ResultSort of X-CircuitStr).g = g & the_result_sort_of g = g; definition let S,V; let X be SetWithCompoundTerm of S,V, g be Gate of X-CircuitStr; cluster the_arity_of g -> DTree-yielding; 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; cluster -> finite Function-like Relation-like Vertex of X-CircuitStr; 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; cluster -> DecoratedTree-like Vertex of X-CircuitStr; 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; cluster -> finite Function-like Relation-like Gate of X-CircuitStr; 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; cluster -> DecoratedTree-like 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:7 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; definition let X,Y be constituted-DTrees set; cluster X \/ Y -> constituted-DTrees; end; theorem :: CIRCTRM1:8 for X1,X2 being constituted-DTrees non empty set holds Subtrees (X1 \/ X2) = (Subtrees X1) \/ (Subtrees X2); theorem :: CIRCTRM1:9 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:10 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:11 for X1,X2 being non empty Subset of S-Terms V holds (X1 \/ X2)-CircuitStr = (X1-CircuitStr)+*(X2-CircuitStr); theorem :: CIRCTRM1:12 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:13 for X being SetWithCompoundTerm of S,V, g being Gate of X-CircuitStr holds g = (g.{})-tree the_arity_of g; begin :: <section2>Circuit genereted by terms</section2> 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) 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; 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 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 X' being SetWithCompoundTerm of S,V st X' = X for o' being Gate of X'-CircuitStr st o' = o holds it = (the Charact of A).(o'.{})`1; end; scheme MSFuncEx {I() -> non empty set, A,B() -> non-empty ManySortedSet of I(), P[set,set,set]}: 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; 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; cluster X-CircuitSorts A -> non-empty; end; theorem :: CIRCTRM1:14 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 OperSymbols 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:15 for v being Vertex of X-CircuitStr holds (the Sorts of X-Circuit A).v = the_sort_of (v, A); theorem :: CIRCTRM1:16 for A being locally-finite 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:17 for A being locally-finite 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:18 for A being locally-finite non-empty MSAlgebra over S, X being non empty Subset of S-Terms V holds X-Circuit A is locally-finite; 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 locally-finite non-empty MSAlgebra over S; cluster X-Circuit A -> locally-finite; end; 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-Circuit A tolerates X2-Circuit A; theorem :: CIRCTRM1:20 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 :: <section3>Correctness of a Term Circuit</section3> reserve S for non empty non void ManySortedSign, A for non-empty locally-finite 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) means :: CIRCTRM1:def 7 ex t' being c-Term of A,V st t' = t & it = t'@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 locally-finite 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:21 for s being State of X-Circuit A for f being CompatibleValuation of s, n being Nat holds f is CompatibleValuation of Following(s,n); definition let x be set; 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:22 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:23 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 :: <section4>Circuit similarity</section4> definition let X be set; cluster id X -> one-to-one; end; definition let f be one-to-one Function; cluster f" -> one-to-one; let g be one-to-one Function; cluster g*f -> one-to-one; end; 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:24 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 OperSymbols of S2 = g.:the OperSymbols of S1; theorem :: CIRCTRM1:25 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 OperSymbols of S2; theorem :: CIRCTRM1:26 for S being non empty ManySortedSign holds S, S are_equivalent_wrt id the carrier of S, id the OperSymbols of S; theorem :: CIRCTRM1:27 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:28 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:29 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:30 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:31 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:32 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:33 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:34 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:35 for S being non empty ManySortedSign for C being non-empty MSAlgebra over S holds id the carrier of S, id the OperSymbols of S form_embedding_of C, C; theorem :: CIRCTRM1:36 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: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 st C1, C2 are_similar_wrt f, g holds S1, S2 are_equivalent_wrt f, g; theorem :: CIRCTRM1:38 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:39 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 OperSymbols of S; theorem :: CIRCTRM1:40 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:41 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:42 f, g form_embedding_of C1, C2 implies dom f = the carrier of G1 & rng f c= the carrier of G2 & dom g = the OperSymbols of G1 & rng g c= the OperSymbols of G2; 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 holds Den(o2, C2) = Den(o1, C1); theorem :: CIRCTRM1:44 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:45 f, g form_embedding_of C1, C2 implies for s being State of C2 holds s*f is State of C1; theorem :: CIRCTRM1:46 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: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 holds Following s1 = (Following s2)*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 for n being Nat holds Following(s1,n) = Following(s2,n)*f; 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 holds s2 is stable implies s1 is stable; theorem :: CIRCTRM1:50 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:51 C1, C2 are_similar_wrt f, g implies for s being State of C2 holds s*f is State of C1; theorem :: CIRCTRM1:52 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:53 C1, C2 are_similar_wrt f, g implies f.:InputVertices G1 = InputVertices G2 & f.:InnerVertices G1 = InnerVertices G2; theorem :: CIRCTRM1:54 C1, C2 are_similar_wrt f, g implies f preserves_inputs_of G1, G2; 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 holds Following s1 = (Following s2)*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 for n being Nat holds Following(s1,n) = Following(s2,n)*f; 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 holds s1 is stable iff s2 is stable; theorem :: CIRCTRM1:58 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 :: <section5>Term specification</section5> 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:59 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: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 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 s' being State of X-Circuit A st s' = s*f for h being CompatibleValuation of s' holds Following(s, 1+height dom t).(f.t) = 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 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 s' being State of X-Circuit A st s' = s*f for h being CompatibleValuation of s' holds Following(s, 1+height dom t).v = 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 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 s' being State of X-Circuit A st s' = s*f for h being CompatibleValuation of s' holds Following(s, 1+height dom t).(f.t) = t@(h, A); theorem :: CIRCTRM1:63 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 s' being State of X-Circuit A st s' = s*f for h being CompatibleValuation of s' holds Following(s, 1+height dom t).v = t@(h, A);

Back to top