begin
begin
begin
definition
let S be non
empty non
void ManySortedSign ;
let V be
V2()
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);
defpred S1[
set ,
set ,
set ]
means (
root-tree [$2,$1] in Subtrees X implies $3
= s . (root-tree [$2,$1]) );
A1:
for
x being
Vertex of
S for
v being
Element of
V . x ex
a being
Element of the
Sorts of
A . x st
S1[
x,
v,
a]
existence
ex b1 being ManySortedFunction of V, the Sorts of A st
for x being Vertex of S
for v being Element of V . x st root-tree [v,x] in Subtrees X holds
(b1 . x) . v = s . (root-tree [v,x])
end;
begin
theorem Th27:
for
S1,
S2,
S3 being non
empty ManySortedSign for
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
definition
let S1,
S2 be non
empty ManySortedSign ;
reflexivity
for S1 being non empty ManySortedSign ex f, g being one-to-one Function st S1,S1 are_equivalent_wrt f,g
symmetry
for S1, S2 being non empty ManySortedSign st ex f, g being one-to-one Function st S1,S2 are_equivalent_wrt f,g holds
ex f, g being one-to-one Function st S2,S1 are_equivalent_wrt f,g
end;
theorem Th35:
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
theorem
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
begin
definition
let S be non
empty non
void ManySortedSign ;
let V be
V2()
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 non
empty non
void Circuit-like ManySortedSign ;
let C be
non-empty Circuit of
G;
assume
C calculates X,
A
;
then consider f,
g being
Function such that A1:
f,
g form_embedding_of X -Circuit A,
C
and A2:
f preserves_inputs_of X -CircuitStr ,
G
by Def15;
A3:
f is
one-to-one
by A1, Def12;
existence
ex b1 being one-to-one Function st
( b1 preserves_inputs_of X -CircuitStr ,G & ex g being Function st b1,g form_embedding_of X -Circuit A,C )
by A1, A2, A3;
end;
definition
let S be non
empty non
void ManySortedSign ;
let V be
V2()
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 non
empty non
void Circuit-like ManySortedSign ;
let C be
non-empty Circuit of
G;
assume B1:
C calculates X,
A
;
let f be
SortMap of
X,
A,
C;
consider g being
Function such that A1:
f,
g form_embedding_of X -Circuit A,
C
by B1, Def17;
A2:
g is
one-to-one
by A1, Def12;
existence
ex b1 being one-to-one Function st f,b1 form_embedding_of X -Circuit A,C
by A1, A2;
end;
:: 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