:: 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 b1 being Vertex of (X -CircuitStr) holds
( b1 is finite & b1 is Function-like & b1 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 b1 being Vertex of (X -CircuitStr) holds b1 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 b1 being Gate of (X -CircuitStr) holds
( b1 is finite & b1 is Function-like & b1 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 b1 being Gate of (X -CircuitStr) holds b1 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 b1, b2 being set st ( for u being Term of S,V st u = v holds
b1 = the Sorts of A . (the_sort_of u) ) & ( for u being Term of S,V st u = v holds
b2 = the Sorts of A . (the_sort_of u) ) holds
b1 = b2
proof end;
existence
ex b1 being set st
for u being Term of S,V st u = v holds
b1 = 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 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) );

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 b1, b2 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
b1 = 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
b2 = the Charact of A . ((o9 . {}) `1) ) holds
b1 = b2
proof end;
existence
ex b1 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
b1 = 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 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) );

scheme :: CIRCTRM1:sch 1
MSFuncEx{ F1() -> non empty set , F2() -> V2() ManySortedSet of F1(), F3() -> V2() ManySortedSet of F1(), P1[ object , object , object ] } :
ex f being ManySortedFunction of F2(),F3() st
for i being Element of F1()
for a being Element of F2() . i holds P1[i,a,(f . i) . a]
provided
A1: for i being Element of F1()
for a being Element of F2() . i ex b being Element of F3() . i st P1[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 b1, b2 being ManySortedSet of the carrier of (X -CircuitStr) st ( for v being Vertex of (X -CircuitStr) holds b1 . v = the_sort_of (v,A) ) & ( for v being Vertex of (X -CircuitStr) holds b2 . v = the_sort_of (v,A) ) holds
b1 = b2
proof end;
existence
ex b1 being ManySortedSet of the carrier of (X -CircuitStr) st
for v being Vertex of (X -CircuitStr) holds b1 . 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 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) );

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 b1, b2 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
b1 . g = the_action_of (g,A) ) & ( for g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds
b2 . g = the_action_of (g,A) ) holds
b1 = b2
proof end;
existence
ex b1 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
b1 . 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 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) );

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 b1 being set ex t9 being c-Term of A,V st
( t9 = t & b1 = t9 @ f );
uniqueness
for b1, b2 being set st ex t9 being c-Term of A,V st
( t9 = t & b1 = t9 @ f ) & ex t9 being c-Term of A,V st
( t9 = t & b2 = t9 @ f ) holds
b1 = b2;
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 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 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]
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 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])
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 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 :: 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 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;
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 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 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 b1 being one-to-one Function st f,b1 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 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 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;