:: CIRCTRM1 semantic presentation

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 Term of S,V
for T being c-Term of A,V st T = t holds
the_sort_of T = the_sort_of t

proof end;

definition

let S be non empty non void ManySortedSign ;
let V be V2 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),(incl ([:the OperSymbols of S,{the carrier of S}:] -Subtrees X)) #);
correctness ;

end;

:: deftheorem defines -CircuitStr CIRCTRM1:def 1 :

registration

let S be non empty non void ManySortedSign ;
let V be V2 ManySortedSet of the carrier of S;
let X be non empty Subset of (S -Terms V);
cluster X -CircuitStr -> non empty strict unsplit ;
coherence

proof end;

end;

theorem Th2: :: CIRCTRM1:2

for S being non empty non void ManySortedSign
for V being V2 ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V) holds
( 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}:] ) )

proof end;

theorem Th3: :: CIRCTRM1:3

for S being non empty non void ManySortedSign
for V being V2 ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V) holds
( X is SetWithCompoundTerm of S,V iff not X -CircuitStr is void )

proof end;

registration

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;
cluster X -CircuitStr -> non empty strict non void unsplit ;
coherence by Th3;

end;

theorem Th4: :: CIRCTRM1:4

for S being non empty non void ManySortedSign
for V being V2 ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V) holds
( ( 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 ) )

proof end;

theorem Th5: :: CIRCTRM1:5

for S being non empty non void ManySortedSign
for V being V2 ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V)
for t being Vertex of (X -CircuitStr ) holds
( t in the OperSymbols of (X -CircuitStr ) iff t is CompoundTerm of S,V )

proof end;

theorem Th6: :: CIRCTRM1:6

for S being non empty non void ManySortedSign
for V being V2 ManySortedSet of the carrier of S
for X being SetWithCompoundTerm of S,V
for g being Gate of (X -CircuitStr ) holds
( the ResultSort of (X -CircuitStr ) . g = g & the_result_sort_of g = g ) by FUNCT_1:35;

registration

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 g be Gate of (X -CircuitStr );
cluster the_arity_of g -> DTree-yielding ;
coherence

proof end;

end;

registration

let S be non empty non void ManySortedSign ;
let V be V2 ManySortedSet of the carrier of S;
let X be non empty Subset of (S -Terms V);
cluster -> Relation-like Function-like finite Element of the carrier of (X -CircuitStr );
coherence by Th4;

end;

registration

let S be non empty non void ManySortedSign ;
let V be V2 ManySortedSet of the carrier of S;
let X be non empty Subset of (S -Terms V);
cluster -> Relation-like Function-like finite DecoratedTree-like Element of the carrier of (X -CircuitStr );
coherence by Th4;

end;

registration

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;
cluster -> Relation-like Function-like finite Element of the OperSymbols of (X -CircuitStr );
coherence by Th4;

end;

registration

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;
cluster -> Relation-like Function-like finite DecoratedTree-like Element of the OperSymbols of (X -CircuitStr );
coherence by Th4;

end;

theorem Th7: :: CIRCTRM1:7

for S being non empty non void ManySortedSign
for V being V2 ManySortedSet of the carrier of S
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 ) )

proof end;

registration

let X, Y be constituted-DTrees set ;
cluster X \/ Y -> constituted-DTrees ;
coherence by TREES_3:9;

end;

theorem Th8: :: CIRCTRM1:8

for X1, X2 being non empty constituted-DTrees set holds Subtrees (X1 \/ X2) = (Subtrees X1) \/ (Subtrees X2)

proof end;

theorem Th9: :: CIRCTRM1:9

for X1, X2 being non empty constituted-DTrees set
for C being set holds C -Subtrees (X1 \/ X2) = (C -Subtrees X1) \/ (C -Subtrees X2)

proof end;

theorem Th10: :: CIRCTRM1:10

for X1, X2 being non empty constituted-DTrees set st ( for t being Element of X1 holds t is finite ) & ( for t being Element of X2 holds t is finite ) holds
for C being set holds C -ImmediateSubtrees (X1 \/ X2) = (C -ImmediateSubtrees X1) +* (C -ImmediateSubtrees X2)

proof end;

theorem Th11: :: CIRCTRM1:11

for S being non empty non void ManySortedSign
for V being V2 ManySortedSet of the carrier of S
for X1, X2 being non empty Subset of (S -Terms V) holds (X1 \/ X2) -CircuitStr = (X1 -CircuitStr ) +* (X2 -CircuitStr )

proof end;

theorem Th12: :: CIRCTRM1:12

for S being non empty non void ManySortedSign
for V being V2 ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V)
for x being set holds
( x in InputVertices (X -CircuitStr ) iff ( x in Subtrees X & ex s being SortSymbol of S ex v being Element of V . s st x = root-tree [v,s] ) )

proof end;

theorem Th13: :: CIRCTRM1:13

for S being non empty non void ManySortedSign
for V being V2 ManySortedSet of the carrier of S
for X being SetWithCompoundTerm of S,V
for g being Gate of (X -CircuitStr ) holds g = (g . {} ) -tree (the_arity_of g)

proof end;

definition

let S be non empty non void ManySortedSign ;
let V be V2 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 of S;
func the_sort_of v,A -> set means :Def2: :: CIRCTRM1:def 2
for u being Term of S,V st u = v holds
it = the Sorts of A . (the_sort_of u);
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def2 defines the_sort_of CIRCTRM1:def 2 :

registration

let S be non empty non void ManySortedSign ;
let V be V2 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 of S;
cluster the_sort_of v,A -> non empty ;
coherence

proof end;

end;

definition

let S be non empty non void ManySortedSign ;
let V be V2 ManySortedSet of the carrier of S;
let X be non empty Subset of (S -Terms V);
assume A1: X is SetWithCompoundTerm of S,V ;
let o be Gate of (X -CircuitStr );
let A be MSAlgebra of S;
func the_action_of o,A -> Function means :Def3: :: CIRCTRM1:def 3
for X' being SetWithCompoundTerm of S,V st X' = X holds
for o' being Gate of (X' -CircuitStr ) st o' = o holds
it = the Charact of A . ((o' . {} ) `1 );
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def3 defines the_action_of CIRCTRM1:def 3 :

scheme :: CIRCTRM1:sch 1
MSFuncEx{ F₁() -> non empty set , F₂() -> V2 ManySortedSet of F₁(), F₃() -> V2 ManySortedSet of F₁(), P₁[ set , set , set ] } :

ex f being ManySortedFunction of F₂(),F₃() st
for i being Element of F₁()
for a being Element of F₂() . i holds P₁[i,a,(f . i) . a]

provided

A1: for i being Element of F₁()
for a being Element of F₂() . i ex b being Element of F₃() . i st P₁[i,a,b]

proof end;

definition

let S be non empty non void ManySortedSign ;
let V be V2 ManySortedSet of the carrier of S;
let X be non empty Subset of (S -Terms V);
let A be MSAlgebra of S;
func X -CircuitSorts A -> ManySortedSet of the carrier of (X -CircuitStr ) means :Def4: :: CIRCTRM1:def 4
for v being Vertex of (X -CircuitStr ) holds it . v = the_sort_of v,A;
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def4 defines -CircuitSorts CIRCTRM1:def 4 :

registration

proof end;

end;

theorem Th14: :: CIRCTRM1:14

for S being non empty non void ManySortedSign
for V being V2 ManySortedSet of the carrier of S
for A being non-empty MSAlgebra of S
for X being SetWithCompoundTerm of S,V
for 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)

proof end;

definition

let S be non empty non void ManySortedSign ;
let V be V2 ManySortedSet of the carrier of S;
let X be non empty Subset of (S -Terms V);
let A be non-empty MSAlgebra of S;
func X -CircuitCharact A -> ManySortedFunction of ((X -CircuitSorts A) # ) * the Arity of (X -CircuitStr ),(X -CircuitSorts A) * the ResultSort of (X -CircuitStr ) means :Def5: :: 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;
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def5 defines -CircuitCharact CIRCTRM1:def 5 :

definition

let S be non empty non void ManySortedSign ;
let V be V2 ManySortedSet of the carrier of S;
let X be non empty Subset of (S -Terms V);
let A be non-empty MSAlgebra of S;
func X -Circuit A -> strict non-empty MSAlgebra of X -CircuitStr equals :: CIRCTRM1:def 6
MSAlgebra(# (X -CircuitSorts A),(X -CircuitCharact A) #);
correctness

proof end;

end;

:: deftheorem defines -Circuit CIRCTRM1:def 6 :

theorem :: CIRCTRM1:15

for S being non empty non void ManySortedSign
for V being V2 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 v being Vertex of (X -CircuitStr ) holds the Sorts of (X -Circuit A) . v = the_sort_of v,A by Def4;

theorem Th16: :: CIRCTRM1:16

for S being non empty non void ManySortedSign
for V being V2 ManySortedSet of the carrier of S
for A being non-empty locally-finite MSAlgebra of 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 by Def5;

theorem Th17: :: CIRCTRM1:17

for S being non empty non void ManySortedSign
for V being V2 ManySortedSet of the carrier of S
for A being non-empty locally-finite MSAlgebra of S
for X being SetWithCompoundTerm of S,V
for g being OperSymbol of (X -CircuitStr )
for o being OperSymbol of S st g . {} = [o,the carrier of S] holds
Den g,(X -Circuit A) = Den o,A

proof end;

theorem Th18: :: CIRCTRM1:18

for S being non empty non void ManySortedSign
for V being V2 ManySortedSet of the carrier of S
for A being non-empty locally-finite MSAlgebra of S
for X being non empty Subset of (S -Terms V) holds X -Circuit A is locally-finite

proof end;

registration

end;

theorem Th19: :: CIRCTRM1:19

for S being non empty non void ManySortedSign
for V being V2 ManySortedSet of the carrier of S
for X1, X2 being SetWithCompoundTerm of S,V
for A being non-empty MSAlgebra of S holds X1 -Circuit A tolerates X2 -Circuit A

proof end;

theorem :: CIRCTRM1:20

for S being non empty non void ManySortedSign
for V being V2 ManySortedSet of the carrier of S
for X1, X2 being SetWithCompoundTerm of S,V
for A being non-empty MSAlgebra of S holds (X1 \/ X2) -Circuit A = (X1 -Circuit A) +* (X2 -Circuit A)

proof end;

definition

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra of S;
let V be Variables of A;
let t be DecoratedTree;
assume A1: t is Term of S,V ;
let f be ManySortedFunction of V,the Sorts of A;
func t @ f,A -> set means :Def7: :: CIRCTRM1:def 7
ex t' being c-Term of A,V st
( t' = t & it = t' @ f );
correctness

proof end;

end;

:: deftheorem Def7 defines @ CIRCTRM1:def 7 :

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 locally-finite MSAlgebra of S;
let s be State of (X -Circuit A);
set C = [:the OperSymbols of S,{the carrier of S}:];
defpred S₁[ 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 S₁[x,v,a]

proof end;

mode CompatibleValuation of s -> ManySortedFunction of V,the Sorts of A means :Def8: :: CIRCTRM1:def 8
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

proof end;

end;

:: deftheorem Def8 defines CompatibleValuation CIRCTRM1:def 8 :

theorem :: CIRCTRM1:21

for S being non empty non void ManySortedSign
for A being non-empty locally-finite MSAlgebra of S
for V being Variables of A
for X being SetWithCompoundTerm of S,V
for s being State of (X -Circuit A)
for f being CompatibleValuation of s
for n being Nat holds f is CompatibleValuation of Following s,n

proof end;

registration

let x be set ;
let S be non empty non void ManySortedSign ;
let V be V2 ManySortedSet of the carrier of S;
let p be FinSequence of S -Terms V;
cluster x -tree p -> finite ;
coherence

proof end;

end;

theorem Th22: :: CIRCTRM1:22

for S being non empty non void ManySortedSign
for A being non-empty locally-finite MSAlgebra of S
for V being Variables of A
for X being SetWithCompoundTerm of S,V
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 )

proof end;

theorem :: CIRCTRM1:23

for S being non empty non void ManySortedSign
for A being non-empty locally-finite MSAlgebra of S
for V being Variables of A
for X being SetWithCompoundTerm of S,V st ( for t being Term of S,V
for o being OperSymbol of S holds
( not t in Subtrees X or not t . {} = [o,the carrier of S] or not the_arity_of o = {} ) ) holds
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 )

proof end;

registration

let X be set ;
cluster id X -> one-to-one ;
coherence by FUNCT_1:52;

end;

registration

let f be one-to-one Function;
cluster f " -> one-to-one ;
coherence by FUNCT_1:62;
let g be one-to-one Function;
cluster f * g -> one-to-one ;
coherence by FUNCT_1:46;

end;

definition

let S1, S2 be non empty ManySortedSign ;
let f, g be Function;
pred S1,S2 are_equivalent_wrt f,g means :Def9: :: 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;

:: deftheorem Def9 defines are_equivalent_wrt CIRCTRM1:def 9 :

theorem Th24: :: CIRCTRM1:24

for S1, S2 being non empty ManySortedSign
for 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 )

proof end;

theorem Th25: :: CIRCTRM1:25

for S1, S2 being non empty ManySortedSign
for 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 )

proof end;

theorem Th26: :: CIRCTRM1:26

for S being non empty ManySortedSign holds S,S are_equivalent_wrt id the carrier of S, id the OperSymbols of S

proof end;

theorem Th27: :: CIRCTRM1:27

for S1, S2 being non empty ManySortedSign
for f, g being Function st S1,S2 are_equivalent_wrt f,g holds
S2,S1 are_equivalent_wrt f " ,g "

proof end;

theorem Th28: :: CIRCTRM1:28

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

proof end;

theorem Th29: :: CIRCTRM1:29

for S1, S2 being non empty ManySortedSign
for f, g being Function st S1,S2 are_equivalent_wrt f,g holds
( f .: (InputVertices S1) = InputVertices S2 & f .: (InnerVertices S1) = InnerVertices S2 )

proof end;

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

proof end;

symmetry

proof end;

end;

:: deftheorem defines are_equivalent CIRCTRM1:def 10 :

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

proof end;

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;

:: deftheorem defines preserves_inputs_of CIRCTRM1:def 11 :

theorem Th31: :: CIRCTRM1:31

for S1, S2 being non empty ManySortedSign
for f, g being Function st f,g form_morphism_between S1,S2 holds
for v being Vertex of S1 holds f . v is Vertex of S2

proof end;

theorem Th32: :: CIRCTRM1:32

for S1, S2 being non empty non void ManySortedSign
for f, g being Function st f,g form_morphism_between S1,S2 holds
for v being Gate of S1 holds g . v is Gate of S2

proof end;

theorem Th33: :: 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

proof end;

theorem Th34: :: CIRCTRM1:34

for S1, S2 being non empty non void Circuit-like ManySortedSign
for f, g being Function st f,g form_morphism_between S1,S2 holds
for v1 being Vertex of S1 st v1 in InnerVertices S1 holds
for v2 being Vertex of S2 st v2 = f . v1 holds
action_at v2 = g . (action_at v1)

proof end;

definition

let S1, S2 be non empty ManySortedSign ;
let f, g be Function;
let C1 be non-empty MSAlgebra of S1;
let C2 be non-empty MSAlgebra of S2;
pred f,g form_embedding_of C1,C2 means :Def12: :: 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;

:: deftheorem Def12 defines form_embedding_of CIRCTRM1:def 12 :

theorem Th35: :: CIRCTRM1:35

for S being non empty ManySortedSign
for C being non-empty MSAlgebra of S holds id the carrier of S, id the OperSymbols of S form_embedding_of C,C

proof end;

theorem Th36: :: CIRCTRM1:36

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

proof end;

definition

let S1, S2 be non empty ManySortedSign ;
let f, g be Function;
let C1 be non-empty MSAlgebra of S1;
let C2 be non-empty MSAlgebra of S2;
pred C1,C2 are_similar_wrt f,g means :Def13: :: CIRCTRM1:def 13
( f,g form_embedding_of C1,C2 & f " ,g " form_embedding_of C2,C1 );

end;

:: deftheorem Def13 defines are_similar_wrt CIRCTRM1:def 13 :

theorem Th37: :: CIRCTRM1:37

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 st C1,C2 are_similar_wrt f,g holds
S1,S2 are_equivalent_wrt f,g

proof end;

theorem Th38: :: CIRCTRM1:38

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 ( 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 ) )

proof end;

theorem :: CIRCTRM1:39

for S being non empty ManySortedSign
for C being non-empty MSAlgebra of S holds C,C are_similar_wrt id the carrier of S, id the OperSymbols of S

proof end;

theorem Th40: :: CIRCTRM1:40

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 st C1,C2 are_similar_wrt f,g holds
C2,C1 are_similar_wrt f " ,g "

proof end;

theorem :: CIRCTRM1:41

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

proof end;

definition

let S1, S2 be non empty ManySortedSign ;
let C1 be non-empty MSAlgebra of S1;
let C2 be non-empty MSAlgebra of S2;
pred C1,C2 are_similar means :: CIRCTRM1:def 14
ex f, g being Function st C1,C2 are_similar_wrt f,g;

end;

:: deftheorem defines are_similar CIRCTRM1:def 14 :

theorem Th42: :: CIRCTRM1:42

for G1, G2 being non empty non void Circuit-like ManySortedSign
for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
( 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 )

proof end;

theorem Th43: :: CIRCTRM1:43

for G1, G2 being non empty non void Circuit-like ManySortedSign
for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
for o1 being Gate of G1
for o2 being Gate of G2 st o2 = g . o1 holds
Den o2,C2 = Den o1,C1

proof end;

theorem Th44: :: CIRCTRM1:44

for G1, G2 being non empty non void Circuit-like ManySortedSign
for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
for o1 being Gate of G1
for o2 being Gate of G2 st o2 = g . o1 holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1

proof end;

theorem Th45: :: CIRCTRM1:45

proof end;

theorem Th46: :: CIRCTRM1:46

for G2, G1 being non empty non void Circuit-like ManySortedSign
for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
for s2 being State of C2
for 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

proof end;

theorem Th47: :: CIRCTRM1:47

for G1, G2 being non empty non void Circuit-like ManySortedSign
for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f holds
Following s1 = (Following s2) * f

proof end;

theorem Th48: :: CIRCTRM1:48

for G1, G2 being non empty non void Circuit-like ManySortedSign
for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f holds
for n being Nat holds Following s1,n = (Following s2,n) * f

proof end;

theorem :: CIRCTRM1:49

for G1, G2 being non empty non void Circuit-like ManySortedSign
for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f & s2 is stable holds
s1 is stable

proof end;

theorem Th50: :: CIRCTRM1:50

for G1, G2 being non empty non void Circuit-like ManySortedSign
for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f holds
for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 )

proof end;

theorem :: CIRCTRM1:51

for G1, G2 being non empty non void Circuit-like ManySortedSign
for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s being State of C2 holds s * f is State of C1

proof end;

theorem Th52: :: CIRCTRM1:52

proof end;

theorem Th53: :: CIRCTRM1:53

proof end;

theorem Th54: :: CIRCTRM1:54

proof end;

theorem Th55: :: CIRCTRM1:55

proof end;

theorem Th56: :: CIRCTRM1:56

proof end;

theorem :: CIRCTRM1:57

proof end;

theorem :: CIRCTRM1:58

for G2, G1 being non empty non void Circuit-like ManySortedSign
for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 )

proof end;

definition

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra of S;
let V be V2 ManySortedSet of the carrier 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;
pred C calculates X,A means :Def15: :: CIRCTRM1:def 15
ex f, g being Function 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;

:: 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 V2 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: :: CIRCTRM1:def 17
( it preserves_inputs_of X -CircuitStr ,G & ex g being Function st it,g form_embedding_of X -Circuit A,C );
existence by A1, A2, A3;

end;

:: deftheorem Def17 defines SortMap CIRCTRM1:def 17 :

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 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 :: CIRCTRM1:def 18
f,it form_embedding_of X -Circuit A,C;
existence by A2, A3;

end;

:: deftheorem defines OperMap CIRCTRM1:def 18 :

theorem Th59: :: CIRCTRM1:59

proof end;

theorem Th60: :: CIRCTRM1:60

for S being non empty non void ManySortedSign
for A being non-empty locally-finite 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 G st C calculates X,A holds
for f being SortMap of X,A,C
for t being Term of S,V st t in Subtrees X holds
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 holds
for h being CompatibleValuation of s' holds (Following s,(1 + (height (dom t)))) . (f . t) = t @ h,A ) )

proof end;

theorem Th61: :: CIRCTRM1:61

for S being non empty non void ManySortedSign
for A being non-empty locally-finite 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 G st C calculates X,A holds
for t being Term of S,V st t in Subtrees X holds
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 holds
for h being CompatibleValuation of s' holds (Following s,(1 + (height (dom t)))) . v = t @ h,A )

proof end;

theorem :: CIRCTRM1:62

for S being non empty non void ManySortedSign
for A being non-empty locally-finite 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 G st X,A specifies C holds
for f being SortMap of X,A,C
for s being State of C
for 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 holds
for h being CompatibleValuation of s' holds (Following s,(1 + (height (dom t)))) . (f . t) = t @ h,A ) )

proof end;

theorem :: CIRCTRM1:63

for S being non empty non void ManySortedSign
for A being non-empty locally-finite 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 G st X,A specifies C holds
for t being Term of S,V st t in Subtrees X holds
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 holds
for h being CompatibleValuation of s' holds (Following s,(1 + (height (dom t)))) . v = t @ h,A )

proof end;