:: Circuit Generated by Terms and Circuit Calculating Terms
:: by Grzegorz Bancerek
::
:: Received April 10, 2001
:: Copyright (c) 2001-2021 Association of Mizar Users

theorem Th1: :: 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
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 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 V2() 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)) #);

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
X -CircuitStr is unsplit ;

end;

theorem :: 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 carrier' of S,{ the carrier of S}:] ) ) by TREES_9:25;

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 non void strict ;

coherence
not X -CircuitStr is void 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 carrier' 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 carrier' of (X -CircuitStr) iff t is CompoundTerm of S,V )

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;
let g be Gate of (X -CircuitStr);

cluster the_arity_of g -> DTree-yielding ;

coherence
the_arity_of g is DTree-yielding ;

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 for Element of the carrier of (X -CircuitStr);

coherence
for b₁ being Vertex of (X -CircuitStr) holds
( b₁ is finite & b₁ is Function-like & b₁ is Relation-like ) 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 -> DecoratedTree-like for Element of the carrier of (X -CircuitStr);

coherence
for b₁ being Vertex of (X -CircuitStr) holds b₁ is DecoratedTree-like ;

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 for Element of the carrier' of (X -CircuitStr);

coherence
for b₁ being Gate of (X -CircuitStr) holds
( b₁ is finite & b₁ is Function-like & b₁ is Relation-like ) 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 -> DecoratedTree-like for Element of the carrier' of (X -CircuitStr);

coherence
for b₁ being Gate of (X -CircuitStr) holds b₁ is DecoratedTree-like ;

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 Th6: :: CIRCTRM1:6

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
X \/ Y is constituted-DTrees by TREES_3:9;

end;

theorem Th7: :: CIRCTRM1:7

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

proof end;

theorem Th8: :: CIRCTRM1:8

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 Th9: :: CIRCTRM1:9

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 Th10: :: CIRCTRM1:10

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 Th11: :: CIRCTRM1:11

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 Th12: :: CIRCTRM1:12

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 over 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
for b₁, b₂ being set st ( for u being Term of S,V st u = v holds
b₁ = the Sorts of A . (the_sort_of u) ) & ( for u being Term of S,V st u = v holds
b₂ = the Sorts of A . (the_sort_of u) ) holds
b₁ = b₂

proof end;

existence
ex b₁ being set st
for u being Term of S,V st u = v holds
b₁ = the Sorts of A . (the_sort_of u)

proof end;

end;

:: deftheorem Def2 defines the_sort_of CIRCTRM1:def 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)
for v being Vertex of (X -CircuitStr)
for A being MSAlgebra over S
for b₆ being set holds
( b₆ = the_sort_of (v,A) iff for u being Term of S,V st u = v holds
b₆ = the Sorts of A . (the_sort_of u) );

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 over S;

cluster the_sort_of (v,A) -> non empty ;

coherence
not the_sort_of (v,A) is empty

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 over S;

func the_action_of (o,A) -> Function means :Def3: :: CIRCTRM1:def 3
for X9 being SetWithCompoundTerm of S,V st X9 = X holds
for o9 being Gate of (X9 -CircuitStr) st o9 = o holds
it = the Charact of A . ((o9 . {}) `1);

uniqueness
for b₁, b₂ being Function st ( for X9 being SetWithCompoundTerm of S,V st X9 = X holds
for o9 being Gate of (X9 -CircuitStr) st o9 = o holds
b₁ = the Charact of A . ((o9 . {}) `1) ) & ( for X9 being SetWithCompoundTerm of S,V st X9 = X holds
for o9 being Gate of (X9 -CircuitStr) st o9 = o holds
b<sub>2</sub> = the Charact of A . ((o9 . {}) `1) ) holds
b₁ = b₂

proof end;

existence
ex b₁ being Function st
for X9 being SetWithCompoundTerm of S,V st X9 = X holds
for o9 being Gate of (X9 -CircuitStr) st o9 = o holds
b₁ = the Charact of A . ((o9 . {}) `1)

proof end;

end;

:: deftheorem Def3 defines the_action_of CIRCTRM1:def 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) st X is SetWithCompoundTerm of S,V holds
for o being Gate of (X -CircuitStr)
for A being MSAlgebra over S
for b₆ being Function holds
( b₆ = 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
b₆ = the Charact of A . ((o9 . {}) `1) );

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

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 over 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
for b₁, b₂ being ManySortedSet of the carrier of (X -CircuitStr) st ( for v being Vertex of (X -CircuitStr) holds b₁ . v = the_sort_of (v,A) ) & ( for v being Vertex of (X -CircuitStr) holds b₂ . v = the_sort_of (v,A) ) holds
b₁ = b₂

proof end;

existence
ex b₁ being ManySortedSet of the carrier of (X -CircuitStr) st
for v being Vertex of (X -CircuitStr) holds b₁ . v = the_sort_of (v,A)

proof end;

end;

:: deftheorem Def4 defines -CircuitSorts CIRCTRM1:def 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)
for A being MSAlgebra over S
for b₅ being ManySortedSet of the carrier of (X -CircuitStr) holds
( b₅ = X -CircuitSorts A iff for v being Vertex of (X -CircuitStr) holds b₅ . v = the_sort_of (v,A) );

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 A be non-empty MSAlgebra over S;

cluster X -CircuitSorts A -> V2() ;

coherence
X -CircuitSorts A is non-empty

proof end;

end;

theorem Th13: :: CIRCTRM1:13

for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for A being non-empty MSAlgebra over 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 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 :Def5: :: 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);

uniqueness
for b₁, b₂ being ManySortedFunction of ((X -CircuitSorts A) #) * the Arity of (X -CircuitStr),(X -CircuitSorts A) * the ResultSort of (X -CircuitStr) st ( for g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds
b₁ . g = the_action_of (g,A) ) & ( for g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds
b₂ . g = the_action_of (g,A) ) holds
b₁ = b₂

proof end;

existence
ex b₁ being ManySortedFunction of ((X -CircuitSorts A) #) * the Arity of (X -CircuitStr),(X -CircuitSorts A) * the ResultSort of (X -CircuitStr) st
for g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds
b₁ . g = the_action_of (g,A)

proof end;

end;

:: deftheorem Def5 defines -CircuitCharact CIRCTRM1:def 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 A being non-empty MSAlgebra over S
for b₅ being ManySortedFunction of ((X -CircuitSorts A) #) * the Arity of (X -CircuitStr),(X -CircuitSorts A) * the ResultSort of (X -CircuitStr) holds
( b₅ = X -CircuitCharact A iff for g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds
b₅ . g = the_action_of (g,A) );

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 over S;

func X -Circuit A -> strict non-empty MSAlgebra over X -CircuitStr equals :: CIRCTRM1:def 6
MSAlgebra(# (X -CircuitSorts A),(X -CircuitCharact A) #);

correctness
coherence
MSAlgebra(# (X -CircuitSorts A),(X -CircuitCharact A) #) is strict non-empty MSAlgebra over X -CircuitStr ;
by MSUALG_1:def 3;

end;

:: deftheorem defines -Circuit CIRCTRM1:def 6 :
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 A being non-empty MSAlgebra over S holds X -Circuit A = MSAlgebra(# (X -CircuitSorts A),(X -CircuitCharact A) #);

theorem :: 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 over 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 :: 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 finite-yielding 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) by Def5;

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 finite-yielding MSAlgebra over 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 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 finite-yielding MSAlgebra over S
for X being non empty Subset of (S -Terms V) holds X -Circuit A is finite-yielding

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;
let A be non-empty finite-yielding MSAlgebra over S;

cluster X -Circuit A -> strict non-empty finite-yielding ;

coherence
X -Circuit A is finite-yielding by Th17;

end;

theorem Th18: :: CIRCTRM1:18

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 over S holds X1 -Circuit A tolerates X2 -Circuit A

proof end;

theorem :: 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 over 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 over 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 t9 being c-Term of A,V st
( t9 = t & it = t9 @ f );

correctness
existence
ex b₁ being set ex t9 being c-Term of A,V st
( t9 = t & b₁ = t9 @ f );
uniqueness
for b₁, b₂ being set st ex t9 being c-Term of A,V st
( t9 = t & b₁ = t9 @ f ) & ex t9 being c-Term of A,V st
( t9 = t & b₂ = t9 @ f ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def7 defines @ CIRCTRM1:def 7 :
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 DecoratedTree st t is Term of S,V holds
for f being ManySortedFunction of V, the Sorts of A
for b₆ being set holds
( b₆ = t @ (f,A) iff ex t9 being c-Term of A,V st
( t9 = t & b₆ = t9 @ f ) );

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 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
ex b₁ 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
(b₁ . x) . v = s . (root-tree [v,x])

proof end;

end;

:: deftheorem Def8 defines CompatibleValuation CIRCTRM1:def 8 :
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 A being non-empty finite-yielding MSAlgebra over S
for s being State of (X -Circuit A)
for b₆ being ManySortedFunction of V, the Sorts of A holds
( b₆ 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
(b₆ . x) . v = s . (root-tree [v,x]) );

theorem :: CIRCTRM1:20

for S being non empty non void ManySortedSign
for A being non-empty finite-yielding MSAlgebra over 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 Element of NAT holds f is CompatibleValuation of Following (s,n)

proof end;

registration

let x be object ;
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
x -tree p is finite

proof end;

end;

theorem Th21: :: CIRCTRM1:21

for S being non empty non void ManySortedSign
for A being non-empty finite-yielding MSAlgebra over 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:22

for S being non empty non void ManySortedSign
for A being non-empty finite-yielding MSAlgebra over 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;

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;

:: deftheorem 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 Th23: :: CIRCTRM1:23

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 carrier' of S2 = g .: the carrier' of S1 )

proof end;

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
( rng f = the carrier of S2 & rng g = the carrier' of S2 )

proof end;

theorem Th25: :: CIRCTRM1:25

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

proof end;

theorem Th26: :: CIRCTRM1:26

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 Th27: :: CIRCTRM1:27

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 Th28: :: CIRCTRM1:28

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
for S1 being non empty ManySortedSign ex f, g being one-to-one Function st S1,S1 are_equivalent_wrt f,g

proof end;

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 by Th26;

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 :: CIRCTRM1:29

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 :
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 Th30: :: CIRCTRM1:30

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 Th31: :: CIRCTRM1:31

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 Th32: :: 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

proof end;

theorem Th33: :: CIRCTRM1:33

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 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;

:: deftheorem 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 over S1
for C2 being non-empty MSAlgebra over 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 Th34: :: 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

proof end;

theorem Th35: :: 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 by PUA2MSS1:29, RELAT_1:36;

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;

:: deftheorem 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 over S1
for C2 being non-empty MSAlgebra over 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 Th36: :: 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

proof end;

theorem Th37: :: 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 ) )

proof end;

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

proof end;

theorem Th39: :: 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 "

proof end;

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

proof end;

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;

:: deftheorem defines are_similar CIRCTRM1:def 14 :
for S1, S2 being non empty ManySortedSign
for C1 being non-empty MSAlgebra over S1
for C2 being non-empty MSAlgebra over S2 holds
( C1,C2 are_similar iff ex f, g being Function st C1,C2 are_similar_wrt f,g );

theorem Th41: :: CIRCTRM1:41

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 carrier' of G1 & rng g c= the carrier' of G2 )

proof end;

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
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 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
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 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 s being State of C2 holds s * f is State of C1

proof end;

theorem Th45: :: CIRCTRM1:45

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 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 Th46: :: CIRCTRM1:46

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 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
for n being Nat holds Following (s1,n) = (Following (s2,n)) * f

proof end;

theorem :: 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 & s2 is stable holds
s1 is stable by Th46;

theorem Th49: :: 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 holds
for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 )

proof end;

theorem :: 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 C1,C2 are_similar_wrt f,g holds
for s being State of C2 holds s * f is State of C1 by Th44;

theorem Th51: :: 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 s1 being State of C1
for s2 being State of C2 holds
( s1 = s2 * f iff s2 = s1 * (f ") )

proof end;

theorem Th52: :: CIRCTRM1:52

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
( f .: (InputVertices G1) = InputVertices G2 & f .: (InnerVertices G1) = InnerVertices G2 )

proof end;

theorem Th53: :: CIRCTRM1:53

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
f preserves_inputs_of G1,G2 by Th52;

theorem Th54: :: CIRCTRM1:54

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 s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
Following s1 = (Following s2) * f by Th46, Th53;

theorem Th55: :: CIRCTRM1:55

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 s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f by Th47, Th53;

theorem :: CIRCTRM1:56

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 s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
( s1 is stable iff s2 is stable )

proof end;

theorem :: CIRCTRM1:57

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 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 over 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 :: 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 defines calculates CIRCTRM1:def 15 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being V2() 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 over S
for V being V2() 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 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 ;

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
ex b₁ being one-to-one Function st
( b₁ preserves_inputs_of X -CircuitStr ,G & ex g being Function st b₁,g form_embedding_of X -Circuit A,C ) by A1, A2;

end;

:: deftheorem Def17 defines SortMap CIRCTRM1:def 17 :
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for A being non-empty MSAlgebra over 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 b₇ being one-to-one Function holds
( b₇ is SortMap of X,A,C iff ( b₇ preserves_inputs_of X -CircuitStr ,G & ex g being Function st b₇,g form_embedding_of X -Circuit A,C ) );

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 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;

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
ex b₁ being one-to-one Function st f,b₁ form_embedding_of X -Circuit A,C by A2;

end;

:: deftheorem defines OperMap CIRCTRM1:def 18 :
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for A being non-empty MSAlgebra over 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 b₈ being one-to-one Function holds
( b₈ is OperMap of X,A,C,f iff f,b₈ form_embedding_of X -Circuit A,C );

theorem Th58: :: CIRCTRM1:58

for S being non empty non void ManySortedSign
for A being non-empty finite-yielding MSAlgebra over 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
C calculates X,A

proof end;

theorem Th59: :: CIRCTRM1:59

for S being non empty non void ManySortedSign
for A being non-empty finite-yielding MSAlgebra over 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 s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) )

proof end;

theorem Th60: :: CIRCTRM1:60

for S being non empty non void ManySortedSign
for A being non-empty finite-yielding MSAlgebra over 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 s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) )

proof end;

theorem :: CIRCTRM1:61

for S being non empty non void ManySortedSign
for A being non-empty finite-yielding MSAlgebra over 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 s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) )

proof end;

theorem :: CIRCTRM1:62

for S being non empty non void ManySortedSign
for A being non-empty finite-yielding MSAlgebra over 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 s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) ) by Th58, Th60;