:: by Grzegorz Bancerek

::

:: Received April 10, 2001

:: Copyright (c) 2001-2017 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

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

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

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 ;

;

:: 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)) #);

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

coherence

X -CircuitStr is unsplit ;

end;
let V be V2() ManySortedSet of the carrier of S;

let X be non empty Subset of (S -Terms V);

coherence

X -CircuitStr is unsplit ;

theorem :: CIRCTRM1:2

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 )

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;

coherence

not X -CircuitStr is void by Th3;

end;
let V be V2() ManySortedSet of the carrier of S;

let X be SetWithCompoundTerm of S,V;

coherence

not X -CircuitStr is void by Th3;

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

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 )

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

coherence

the_arity_of g is DTree-yielding ;

end;
let V be V2() ManySortedSet of the carrier of S;

let X be SetWithCompoundTerm of S,V;

let g be Gate of (X -CircuitStr);

coherence

the_arity_of g is DTree-yielding ;

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

coherence

for b_{1} being Vertex of (X -CircuitStr) holds

( b_{1} is finite & b_{1} is Function-like & b_{1} is Relation-like )
by Th4;

end;
let V be V2() ManySortedSet of the carrier of S;

let X be non empty Subset of (S -Terms V);

coherence

for b

( b

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

coherence

for b_{1} being Vertex of (X -CircuitStr) holds b_{1} is DecoratedTree-like
;

end;
let V be V2() ManySortedSet of the carrier of S;

let X be non empty Subset of (S -Terms V);

coherence

for b

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;

coherence

for b_{1} being Gate of (X -CircuitStr) holds

( b_{1} is finite & b_{1} is Function-like & b_{1} is Relation-like )
by Th4;

end;
let V be V2() ManySortedSet of the carrier of S;

let X be SetWithCompoundTerm of S,V;

coherence

for b

( b

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;

coherence

for b_{1} being Gate of (X -CircuitStr) holds b_{1} is DecoratedTree-like
;

end;
let V be V2() ManySortedSet of the carrier of S;

let X be SetWithCompoundTerm of S,V;

coherence

for b

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

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

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)

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)

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

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)

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;

for b_{1}, b_{2} being set st ( for u being Term of S,V st u = v holds

b_{1} = the Sorts of A . (the_sort_of u) ) & ( for u being Term of S,V st u = v holds

b_{2} = the Sorts of A . (the_sort_of u) ) holds

b_{1} = b_{2}

ex b_{1} being set st

for u being Term of S,V st u = v holds

b_{1} = the Sorts of A . (the_sort_of u)

end;
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 u being Term of S,V st u = v holds

it = the Sorts of A . (the_sort_of u);

for b

b

b

b

proof end;

existence ex b

for u being Term of S,V st u = v holds

b

proof 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_{6} being set holds

( b_{6} = the_sort_of (v,A) iff for u being Term of S,V st u = v holds

b_{6} = the Sorts of A . (the_sort_of u) );

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

( b

b

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;

coherence

not the_sort_of (v,A) is empty

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

coherence

not the_sort_of (v,A) is empty

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

assume A1: X is SetWithCompoundTerm of S,V ;

let o be Gate of (X -CircuitStr);

let A be MSAlgebra over S;

for b_{1}, b_{2} 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_{1} = 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_{2} = the Charact of A . ((o9 . {}) `1) ) holds

b_{1} = b_{2}

ex b_{1} 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_{1} = the Charact of A . ((o9 . {}) `1)

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

for b

for o9 being Gate of (X9 -CircuitStr) st o9 = o holds

b

for o9 being Gate of (X9 -CircuitStr) st o9 = o holds

b

b

proof end;

existence ex b

for X9 being SetWithCompoundTerm of S,V st X9 = X holds

for o9 being Gate of (X9 -CircuitStr) st o9 = o holds

b

proof 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_{6} being Function holds

( b_{6} = 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_{6} = the Charact of A . ((o9 . {}) `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) st X is SetWithCompoundTerm of S,V holds

for o being Gate of (X -CircuitStr)

for A being MSAlgebra over S

for b

( b

for o9 being Gate of (X9 -CircuitStr) st o9 = o holds

b

scheme :: CIRCTRM1:sch 1

MSFuncEx{ F_{1}() -> non empty set , F_{2}() -> V2() ManySortedSet of F_{1}(), F_{3}() -> V2() ManySortedSet of F_{1}(), P_{1}[ object , object , object ] } :

MSFuncEx{ F

ex f being ManySortedFunction of F_{2}(),F_{3}() st

for i being Element of F_{1}()

for a being Element of F_{2}() . i holds P_{1}[i,a,(f . i) . a]

providedfor i being Element of F

for a being Element of F

A1:
for i being Element of F_{1}()

for a being Element of F_{2}() . i ex b being Element of F_{3}() . i st P_{1}[i,a,b]

for a being Element of F

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;

for b_{1}, b_{2} being ManySortedSet of the carrier of (X -CircuitStr) st ( for v being Vertex of (X -CircuitStr) holds b_{1} . v = the_sort_of (v,A) ) & ( for v being Vertex of (X -CircuitStr) holds b_{2} . v = the_sort_of (v,A) ) holds

b_{1} = b_{2}

ex b_{1} being ManySortedSet of the carrier of (X -CircuitStr) st

for v being Vertex of (X -CircuitStr) holds b_{1} . v = the_sort_of (v,A)

end;
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 v being Vertex of (X -CircuitStr) holds it . v = the_sort_of (v,A);

for b

b

proof end;

existence ex b

for v being Vertex of (X -CircuitStr) holds b

proof 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_{5} being ManySortedSet of the carrier of (X -CircuitStr) holds

( b_{5} = X -CircuitSorts A iff for v being Vertex of (X -CircuitStr) holds b_{5} . v = the_sort_of (v,A) );

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

( b

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;

coherence

X -CircuitSorts A is non-empty

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

coherence

X -CircuitSorts A is non-empty

proof end;

theorem Th13: :: CIRCTRM1:13

for S being non empty non void ManySortedSign

for V being V2() ManySortedSet of the carrier of S

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

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;

for b_{1}, b_{2} 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_{1} . g = the_action_of (g,A) ) & ( for g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds

b_{2} . g = the_action_of (g,A) ) holds

b_{1} = b_{2}

ex b_{1} 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_{1} . g = the_action_of (g,A)

end;
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 g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds

it . g = the_action_of (g,A);

for b

b

b

b

proof end;

existence ex b

for g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds

b

proof 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_{5} being ManySortedFunction of ((X -CircuitSorts A) #) * the Arity of (X -CircuitStr),(X -CircuitSorts A) * the ResultSort of (X -CircuitStr) holds

( b_{5} = X -CircuitCharact A iff for g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds

b_{5} . g = the_action_of (g,A) );

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

( b

b

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;

coherence

MSAlgebra(# (X -CircuitSorts A),(X -CircuitCharact A) #) is strict non-empty MSAlgebra over X -CircuitStr ;

by MSUALG_1:def 3;

end;
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 MSAlgebra(# (X -CircuitSorts A),(X -CircuitCharact A) #);

coherence

MSAlgebra(# (X -CircuitSorts A),(X -CircuitCharact A) #) is strict non-empty MSAlgebra over X -CircuitStr ;

by MSUALG_1:def 3;

:: 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) #);

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;

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;

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)

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

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;

coherence

X -Circuit A is finite-yielding by Th17;

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

coherence

X -Circuit A is finite-yielding by Th17;

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

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)

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;

existence

ex b_{1} being set ex t9 being c-Term of A,V st

( t9 = t & b_{1} = t9 @ f );

uniqueness

for b_{1}, b_{2} being set st ex t9 being c-Term of A,V st

( t9 = t & b_{1} = t9 @ f ) & ex t9 being c-Term of A,V st

( t9 = t & b_{2} = t9 @ f ) holds

b_{1} = b_{2};

end;
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 ex t9 being c-Term of A,V st

( t9 = t & it = t9 @ f );

existence

ex b

( t9 = t & b

uniqueness

for b

( t9 = t & b

( t9 = t & b

b

proof 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_{6} being set holds

( b_{6} = t @ (f,A) iff ex t9 being c-Term of A,V st

( t9 = t & b_{6} = t9 @ f ) );

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

( b

( t9 = t & b

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_{1}[ 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_{1}[x,v,a]

ex b_{1} 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_{1} . x) . v = s . (root-tree [v,x])

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

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

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

ex b

for x being Vertex of S

for v being Element of V . x st root-tree [v,x] in Subtrees X holds

(b

proof 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_{6} being ManySortedFunction of V, the Sorts of A holds

( b_{6} 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_{6} . x) . v = s . (root-tree [v,x]) );

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

( b

for v being Element of V . x st root-tree [v,x] in Subtrees X holds

(b

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)

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;

coherence

x -tree p is finite

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

coherence

x -tree p is finite

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

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

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;

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

( f is one-to-one & g is one-to-one & f,g form_morphism_between S1,S2 & f " ,g " form_morphism_between S2,S1 );

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

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 )

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 )

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 "

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

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 )

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 ;

for S1 being non empty ManySortedSign ex f, g being one-to-one Function st S1,S1 are_equivalent_wrt f,g

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;
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 ex f, g being one-to-one Function st S1,S2 are_equivalent_wrt f,g;

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;

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

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

S1,S3 are_equivalent

proof end;

definition

let S1, S2 be non empty ManySortedSign ;

let f be Function;

end;
let f be Function;

pred f preserves_inputs_of S1,S2 means :: CIRCTRM1:def 11

f .: (InputVertices S1) c= InputVertices S2;

f .: (InputVertices S1) c= InputVertices S2;

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

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

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

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

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)

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;

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

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

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

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

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;

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;

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

( f,g form_embedding_of C1,C2 & f " ,g " form_embedding_of C2,C1 );

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

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

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

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

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 "

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

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;

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

ex f, g being Function st C1,C2 are_similar_wrt f,g;

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

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 )

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)

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

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

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

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

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

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;

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 )

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;

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

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 )

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;

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;

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;

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 )

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 )

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;

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

ex f, g being Function st

( f,g form_embedding_of X -Circuit A,C & f preserves_inputs_of X -CircuitStr ,G );

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

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

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 ;

ex b_{1} being one-to-one Function st

( b_{1} preserves_inputs_of X -CircuitStr ,G & ex g being Function st b_{1},g form_embedding_of X -Circuit A,C )
by A1, A2;

end;
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 ( it preserves_inputs_of X -CircuitStr ,G & ex g being Function st it,g form_embedding_of X -Circuit A,C );

ex b

( b

:: 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_{7} being one-to-one Function holds

( b_{7} is SortMap of X,A,C iff ( b_{7} preserves_inputs_of X -CircuitStr ,G & ex g being Function st b_{7},g form_embedding_of X -Circuit A,C ) );

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

( b

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;

ex b_{1} being one-to-one Function st f,b_{1} form_embedding_of X -Circuit A,C
by A2;

end;
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 f,it form_embedding_of X -Circuit A,C;

ex b

:: 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_{8} being one-to-one Function holds

( b_{8} is OperMap of X,A,C,f iff f,b_{8} form_embedding_of X -Circuit A,C );

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

( b

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

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

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

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

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;

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;

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