begin
theorem Th1:
definition
let S be non
empty non
void ManySortedSign ;
let V be
V5()
ManySortedSet of ;
let X be non
empty Subset of ;
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 :
theorem
theorem Th3:
theorem Th4:
theorem Th5:
theorem
canceled;
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
begin
definition
let S be non
empty non
void ManySortedSign ;
let V be
V5()
ManySortedSet of ;
let X be non
empty Subset of ;
let v be
Vertex of ;
let A be
MSAlgebra of
S;
func the_sort_of v,
A -> set means :
Def2:
for
u being
Term of the
carrier of
K345(
S,
V), st
u = v holds
it = the
Sorts of
A . (the_sort_of u);
uniqueness
for b1, b2 being set st ( for u being Term of the carrier of K345(S,V), st u = v holds
b1 = the Sorts of A . (the_sort_of u) ) & ( for u being Term of the carrier of K345(S,V), st u = v holds
b2 = the Sorts of A . (the_sort_of u) ) holds
b1 = b2
existence
ex b1 being set st
for u being Term of the carrier of K345(S,V), st u = v holds
b1 = the Sorts of A . (the_sort_of u)
end;
:: deftheorem Def2 defines the_sort_of CIRCTRM1:def 2 :
:: deftheorem Def3 defines the_action_of CIRCTRM1:def 3 :
:: deftheorem Def4 defines -CircuitSorts CIRCTRM1:def 4 :
theorem Th14:
:: deftheorem Def5 defines -CircuitCharact CIRCTRM1:def 5 :
:: deftheorem defines -Circuit CIRCTRM1:def 6 :
theorem
theorem
theorem Th17:
theorem Th18:
theorem Th19:
theorem
begin
:: deftheorem Def7 defines @ CIRCTRM1:def 7 :
definition
let S be non
empty non
void ManySortedSign ;
let V be
V5()
ManySortedSet of ;
let X be
SetWithCompoundTerm of
S,
V;
let A be
non-empty finite-yielding MSAlgebra of
S;
let s be
State of ;
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
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
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
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 :
theorem
theorem Th22:
theorem
begin
:: deftheorem Def9 defines are_equivalent_wrt CIRCTRM1:def 9 :
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 :
theorem
:: deftheorem defines preserves_inputs_of CIRCTRM1:def 11 :
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
:: deftheorem Def12 defines form_embedding_of CIRCTRM1:def 12 :
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 :
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 :
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 :
:: deftheorem defines specifies CIRCTRM1:def 16 :
definition
let S be non
empty non
void ManySortedSign ;
let V be
V5()
ManySortedSet of ;
let A be
non-empty MSAlgebra of
S;
let X be non
empty Subset of ;
let G be non
empty non
void Circuit-like ManySortedSign ;
let C be
non-empty Circuit of
non-empty ;
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 :
definition
let S be non
empty non
void ManySortedSign ;
let V be
V5()
ManySortedSet of ;
let A be
non-empty MSAlgebra of
S;
let X be non
empty Subset of ;
let G be non
empty non
void Circuit-like ManySortedSign ;
let C be
non-empty Circuit of
non-empty ;
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 :
theorem Th59:
theorem Th60:
theorem Th61:
theorem
theorem
for
S being non
empty non
void ManySortedSign for
A being
non-empty finite-yielding MSAlgebra of
S for
V being
Variables of
A for
X being
SetWithCompoundTerm of
S,
V for
G being non
empty non
void Circuit-like ManySortedSign for
C being
non-empty Circuit of
non-empty st
X,
A specifies C holds
for
t being
Term of the
carrier of
K345(
b1,
b3), st
t in Subtrees X holds
ex
v being
Vertex of st
for
s being
State of 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 st
s' = s * f holds
for
h being
CompatibleValuation of
s' holds
(Following s,(1 + (height (dom t)))) . v = t @ h,
A )
by Th59, Th61;