begin
theorem Th1:
definition
let S be non
empty non
void ManySortedSign ;
let V be
V5()
ManySortedSet of the
carrier of
S;
let X be non
empty Subset of
(S -Terms V);
func X -CircuitStr -> non
empty strict ManySortedSign equals
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)) #);
correctness
coherence
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)) #) is non empty strict ManySortedSign ;
;
end;
:: deftheorem defines -CircuitStr CIRCTRM1:def 1 :
for S being non empty non void ManySortedSign
for V being V5() ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V) holds X -CircuitStr = 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)) #);
theorem
theorem Th3:
theorem Th4:
theorem Th5:
theorem
canceled;
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
begin
:: deftheorem Def2 defines the_sort_of CIRCTRM1:def 2 :
for S being non empty non void ManySortedSign
for V being V5() ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V)
for v being Vertex of (X -CircuitStr )
for A being MSAlgebra of S
for b6 being set holds
( b6 = the_sort_of v,A iff for u being Term of S,V st u = v holds
b6 = the Sorts of A . (the_sort_of u) );
:: deftheorem Def3 defines the_action_of CIRCTRM1:def 3 :
for S being non empty non void ManySortedSign
for V being V5() ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V) st X is SetWithCompoundTerm of S,V holds
for o being Gate of (X -CircuitStr )
for A being MSAlgebra of S
for b6 being Function holds
( b6 = the_action_of o,A iff for X9 being SetWithCompoundTerm of S,V st X9 = X holds
for o9 being Gate of (X9 -CircuitStr ) st o9 = o holds
b6 = the Charact of A . ((o9 . {} ) `1 ) );
:: deftheorem Def4 defines -CircuitSorts CIRCTRM1:def 4 :
for S being non empty non void ManySortedSign
for V being V5() ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V)
for A being MSAlgebra of S
for b5 being ManySortedSet of the carrier of (X -CircuitStr ) holds
( b5 = X -CircuitSorts A iff for v being Vertex of (X -CircuitStr ) holds b5 . v = the_sort_of v,A );
theorem Th14:
:: deftheorem Def5 defines -CircuitCharact CIRCTRM1:def 5 :
for S being non empty non void ManySortedSign
for V being V5() ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V)
for A being non-empty MSAlgebra of S
for b5 being ManySortedFunction of ((X -CircuitSorts A) # ) * the Arity of (X -CircuitStr ),(X -CircuitSorts A) * the ResultSort of (X -CircuitStr ) holds
( b5 = X -CircuitCharact A iff for g being Gate of (X -CircuitStr ) st g in the carrier' of (X -CircuitStr ) holds
b5 . g = the_action_of g,A );
:: deftheorem defines -Circuit CIRCTRM1:def 6 :
for S being non empty non void ManySortedSign
for V being V5() ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V)
for A being non-empty MSAlgebra of S holds X -Circuit A = MSAlgebra(# (X -CircuitSorts A),(X -CircuitCharact A) #);
theorem
theorem
theorem Th17:
theorem Th18:
theorem Th19:
theorem
begin
:: deftheorem Def7 defines @ CIRCTRM1:def 7 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for V being Variables of A
for t being DecoratedTree st t is Term of S,V holds
for f being ManySortedFunction of V,the Sorts of A
for b6 being set holds
( b6 = t @ f,A iff ex t9 being c-Term of A,V st
( t9 = t & b6 = t9 @ f ) );
definition
let S be non
empty non
void ManySortedSign ;
let V be
V5()
ManySortedSet of the
carrier of
S;
let X be
SetWithCompoundTerm of
S,
V;
let A be
non-empty finite-yielding MSAlgebra of
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]
mode CompatibleValuation of
s -> ManySortedFunction of
V,the
Sorts of
A means :
Def8:
for
x being
Vertex of
S for
v being
Element of
V . x st
root-tree [v,x] in Subtrees X holds
(it . x) . v = s . (root-tree [v,x]);
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;
:: deftheorem Def8 defines CompatibleValuation CIRCTRM1:def 8 :
for S being non empty non void ManySortedSign
for V being V5() ManySortedSet of the carrier of S
for X being SetWithCompoundTerm of S,V
for A being non-empty finite-yielding MSAlgebra of S
for s being State of (X -Circuit A)
for b6 being ManySortedFunction of V,the Sorts of A holds
( b6 is CompatibleValuation of s iff for x being Vertex of S
for v being Element of V . x st root-tree [v,x] in Subtrees X holds
(b6 . x) . v = s . (root-tree [v,x]) );
theorem
theorem Th22:
theorem
begin
:: deftheorem Def9 defines are_equivalent_wrt CIRCTRM1:def 9 :
for S1, S2 being non empty ManySortedSign
for f, g being Function holds
( S1,S2 are_equivalent_wrt f,g iff ( f is one-to-one & g is one-to-one & f,g form_morphism_between S1,S2 & f " ,g " form_morphism_between S2,S1 ) );
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
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
theorem Th29:
definition
let S1,
S2 be non
empty ManySortedSign ;
pred S1,
S2 are_equivalent means
ex
f,
g being
one-to-one Function st
S1,
S2 are_equivalent_wrt f,
g;
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;
:: deftheorem defines are_equivalent CIRCTRM1:def 10 :
for S1, S2 being non empty ManySortedSign holds
( S1,S2 are_equivalent iff ex f, g being one-to-one Function st S1,S2 are_equivalent_wrt f,g );
theorem
:: deftheorem defines preserves_inputs_of CIRCTRM1:def 11 :
for S1, S2 being non empty ManySortedSign
for f being Function holds
( f preserves_inputs_of S1,S2 iff f .: (InputVertices S1) c= InputVertices S2 );
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
:: deftheorem Def12 defines form_embedding_of CIRCTRM1:def 12 :
for S1, S2 being non empty ManySortedSign
for f, g being Function
for C1 being non-empty MSAlgebra of S1
for C2 being non-empty MSAlgebra of S2 holds
( f,g form_embedding_of C1,C2 iff ( 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 ) );
theorem Th35:
theorem Th36:
for
S1,
S2,
S3 being non
empty ManySortedSign for
f1,
g1,
f2,
g2 being
Function for
C1 being
non-empty MSAlgebra of
S1 for
C2 being
non-empty MSAlgebra of
S2 for
C3 being
non-empty MSAlgebra of
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
:: deftheorem Def13 defines are_similar_wrt CIRCTRM1:def 13 :
for S1, S2 being non empty ManySortedSign
for f, g being Function
for C1 being non-empty MSAlgebra of S1
for C2 being non-empty MSAlgebra of S2 holds
( C1,C2 are_similar_wrt f,g iff ( f,g form_embedding_of C1,C2 & f " ,g " form_embedding_of C2,C1 ) );
theorem Th37:
theorem Th38:
theorem
theorem Th40:
theorem
for
S1,
S2,
S3 being non
empty ManySortedSign for
f1,
g1,
f2,
g2 being
Function for
C1 being
non-empty MSAlgebra of
S1 for
C2 being
non-empty MSAlgebra of
S2 for
C3 being
non-empty MSAlgebra of
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
:: deftheorem defines are_similar CIRCTRM1:def 14 :
for S1, S2 being non empty ManySortedSign
for C1 being non-empty MSAlgebra of S1
for C2 being non-empty MSAlgebra of S2 holds
( C1,C2 are_similar iff ex f, g being Function st C1,C2 are_similar_wrt f,g );
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem
theorem Th50:
theorem
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem Th56:
theorem
theorem
begin
:: deftheorem Def15 defines calculates CIRCTRM1:def 15 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for V being V5() ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V)
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G holds
( C calculates X,A iff ex f, g being Function st
( f,g form_embedding_of X -Circuit A,C & f preserves_inputs_of X -CircuitStr ,G ) );
:: deftheorem defines specifies CIRCTRM1:def 16 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for V being V5() ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V)
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G holds
( X,A specifies C iff C,X -Circuit A are_similar );
definition
let S be non
empty non
void ManySortedSign ;
let V be
V5()
ManySortedSet of the
carrier of
S;
let A be
non-empty MSAlgebra of
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;
mode SortMap of
X,
A,
C -> one-to-one Function means :
Def17:
(
it preserves_inputs_of X -CircuitStr ,
G & ex
g being
Function st
it,
g form_embedding_of X -Circuit A,
C );
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;
:: deftheorem Def17 defines SortMap CIRCTRM1:def 17 :
for S being non empty non void ManySortedSign
for V being V5() ManySortedSet of the carrier of S
for A being non-empty MSAlgebra of S
for X being non empty Subset of (S -Terms V)
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st C calculates X,A holds
for b7 being one-to-one Function holds
( b7 is SortMap of X,A,C iff ( b7 preserves_inputs_of X -CircuitStr ,G & ex g being Function st b7,g form_embedding_of X -Circuit A,C ) );
definition
let S be non
empty non
void ManySortedSign ;
let V be
V5()
ManySortedSet of the
carrier of
S;
let A be
non-empty MSAlgebra of
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 A1:
C calculates X,
A
;
let f be
SortMap of
X,
A,
C;
consider g being
Function such that A2:
f,
g form_embedding_of X -Circuit A,
C
by A1, Def17;
A3:
g is
one-to-one
by A2, Def12;
mode OperMap of
X,
A,
C,
f -> one-to-one Function means
f,
it form_embedding_of X -Circuit A,
C;
existence
ex b1 being one-to-one Function st f,b1 form_embedding_of X -Circuit A,C
by A2, A3;
end;
:: deftheorem defines OperMap CIRCTRM1:def 18 :
for S being non empty non void ManySortedSign
for V being V5() ManySortedSet of the carrier of S
for A being non-empty MSAlgebra of S
for X being non empty Subset of (S -Terms V)
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st C calculates X,A holds
for f being SortMap of X,A,C
for b8 being one-to-one Function holds
( b8 is OperMap of X,A,C,f iff f,b8 form_embedding_of X -Circuit A,C );
theorem Th59:
theorem Th60:
theorem Th61:
theorem
theorem