:: Circuit Generated by Terms and Circuit Calculating Terms
:: by Grzegorz Bancerek
::
:: Received April 10, 2001
:: Copyright (c) 2001-2017 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);