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


begin

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

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);
funcX -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);
clusterX -CircuitStr  ->  non empty strict unsplit ;
coherence
 X -CircuitStr is unsplit
proofend;
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 )
proofend;

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;
clusterX -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 ) )
proofend;

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

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

registration
let X, Y be constituted-DTrees set ;
clusterX \/ 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)
proofend;

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

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

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

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] ) )
proofend;

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

begin

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
proofend;
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)
proofend;
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
proofend;
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
proofend;
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)
proofend;
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[ set , set , set ] } :
 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]
proofend;

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;
funcX -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
proofend;
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)
proofend;
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;
clusterX -CircuitSorts A -> V2() ;
coherence
 X -CircuitSorts A is non-empty
proofend;
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)
proofend;

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;
funcX -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
proofend;
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)
proofend;
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;
funcX -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)
proofend;

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

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

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

begin

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;
funct @ (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;
proofend;
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]
proofend;
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])
proofend;
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)
proofend;

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;
clusterx -tree p ->  finite ;
coherence
 x -tree p is finite
proofend;
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) )
proofend;

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

begin

definition
let S1, S2 be non empty ManySortedSign ;
let f, g be Function;
predS1,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_:_
 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 )
proofend;

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

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

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

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

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

definition
let S1, S2 be non empty ManySortedSign ;
predS1,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
proofend;
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
proofend;
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
proofend;

definition
let S1, S2 be non empty ManySortedSign ;
let f be Function;
predf 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
proofend;

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

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

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

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;
predf,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_:_
 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
proofend;

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

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;
predC1,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_:_
 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
proofend;

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

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

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

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

definition
let S1, S2 be non empty ManySortedSign ;
let C1 be non-empty MSAlgebra over S1;
let C2 be non-empty MSAlgebra over S2;
predC1,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 )
proofend;

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

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

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

theorem Th45: :: CIRCTRM1:45
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
proofend;

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

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 Element of NAT holds Following (s1,n) = (Following (s2,n)) * f
proofend;

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

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

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

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 ") )
proofend;

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

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

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

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

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

theorem :: CIRCTRM1:57
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 )
proofend;

begin

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;
predC 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 );
predX,A specifies C means :: CIRCTRM1:def 16
C,X -Circuit A are_similar ;
end;

:: deftheorem Def15 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 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
 ex b1 being one-to-one Function st
( b1 preserves_inputs_of X -CircuitStr ,G & ex g being Function st b1,g form_embedding_of X -Circuit A,C ) by A1, A2, A3;
end;

:: deftheorem Def17 defines SortMap CIRCTRM1:def_17_:_
 for S being non empty non void ManySortedSign
for V being 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 B1: C calculates X,A ;
let f be SortMap of X,A,C;
consider g being Function such that
A1: f,g form_embedding_of X -Circuit A,C by B1, Def17;
A2: g is one-to-one by A1, 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
 ex b1 being one-to-one Function st f,b1 form_embedding_of X -Circuit A,C by A1, 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
proofend;

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

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

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

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;