:: CIRCTRM1 semantic presentation

theorem Th1: :: CIRCTRM1:1

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being Variables of b₂
for b₄ being Term of b₁,b₃
for b₅ being c-Term of b₂,b₃ st b₅ = b₄ holds
the_sort_of b₅ = the_sort_of b₄

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be V2 ManySortedSet of the carrier of c₁;
let c₃ be non empty Subset of (c₁ -Terms c₂);
func c₃ -CircuitStr -> non empty strict ManySortedSign equals :: CIRCTRM1:def 1
ManySortedSign(# (Subtrees a₃),([:the OperSymbols of a₁,{the carrier of a₁}:] -Subtrees a₃),([:the OperSymbols of a₁,{the carrier of a₁}:] -ImmediateSubtrees a₃),(incl ([:the OperSymbols of a₁,{the carrier of a₁}:] -Subtrees a₃)) #);
correctness ;

end;

:: deftheorem Def1 defines -CircuitStr CIRCTRM1:def 1 :

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be V2 ManySortedSet of the carrier of c₁;
let c₃ be non empty Subset of (c₁ -Terms c₂);
cluster a₃ -CircuitStr -> non empty strict unsplit ;
coherence

proof end;

end;

theorem Th2: :: CIRCTRM1:2

for b₁ being non empty non void ManySortedSign
for b₂ being V2 ManySortedSet of the carrier of b₁
for b₃ being non empty Subset of (b₁ -Terms b₂) holds
( b₃ -CircuitStr is void iff for b₄ being Element of b₃ holds
( b₄ is root & not b₄ . {} in [:the OperSymbols of b₁,{the carrier of b₁}:] ) )

proof end;

theorem Th3: :: CIRCTRM1:3

for b₁ being non empty non void ManySortedSign
for b₂ being V2 ManySortedSet of the carrier of b₁
for b₃ being non empty Subset of (b₁ -Terms b₂) holds
( b₃ is SetWithCompoundTerm of b₁,b₂ iff not b₃ -CircuitStr is void )

proof end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be V2 ManySortedSet of the carrier of c₁;
let c₃ be SetWithCompoundTerm of c₁,c₂;
cluster a₃ -CircuitStr -> non empty strict non void unsplit ;
coherence by Th3;

end;

theorem Th4: :: CIRCTRM1:4

for b₁ being non empty non void ManySortedSign
for b₂ being V2 ManySortedSet of the carrier of b₁
for b₃ being non empty Subset of (b₁ -Terms b₂) holds
( ( for b₄ being Vertex of (b₃ -CircuitStr ) holds b₄ is Term of b₁,b₂ ) & ( for b₄ being set st b₄ in the OperSymbols of (b₃ -CircuitStr ) holds
b₄ is CompoundTerm of b₁,b₂ ) )

proof end;

theorem Th5: :: CIRCTRM1:5

for b₁ being non empty non void ManySortedSign
for b₂ being V2 ManySortedSet of the carrier of b₁
for b₃ being non empty Subset of (b₁ -Terms b₂)
for b₄ being Vertex of (b₃ -CircuitStr ) holds
( b₄ in the OperSymbols of (b₃ -CircuitStr ) iff b₄ is CompoundTerm of b₁,b₂ )

proof end;

theorem Th6: :: CIRCTRM1:6

for b₁ being non empty non void ManySortedSign
for b₂ being V2 ManySortedSet of the carrier of b₁
for b₃ being SetWithCompoundTerm of b₁,b₂
for b₄ being Gate of (b₃ -CircuitStr ) holds
( the ResultSort of (b₃ -CircuitStr ) . b₄ = b₄ & the_result_sort_of b₄ = b₄ ) by FUNCT_1:35;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be V2 ManySortedSet of the carrier of c₁;
let c₃ be SetWithCompoundTerm of c₁,c₂;
let c₄ be Gate of (c₃ -CircuitStr );
cluster the_arity_of a₄ -> DTree-yielding ;
coherence

proof end;

end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be V2 ManySortedSet of the carrier of c₁;
let c₃ be non empty Subset of (c₁ -Terms c₂);
cluster -> Relation-like Function-like finite Element of the carrier of (a₃ -CircuitStr );
coherence by Th4;

end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be V2 ManySortedSet of the carrier of c₁;
let c₃ be non empty Subset of (c₁ -Terms c₂);
cluster -> Relation-like Function-like finite DecoratedTree-like Element of the carrier of (a₃ -CircuitStr );
coherence by Th4;

end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be V2 ManySortedSet of the carrier of c₁;
let c₃ be SetWithCompoundTerm of c₁,c₂;
cluster -> Relation-like Function-like finite Element of the OperSymbols of (a₃ -CircuitStr );
coherence by Th4;

end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be V2 ManySortedSet of the carrier of c₁;
let c₃ be SetWithCompoundTerm of c₁,c₂;
cluster -> Relation-like Function-like finite DecoratedTree-like Element of the OperSymbols of (a₃ -CircuitStr );
coherence by Th4;

end;

theorem Th7: :: CIRCTRM1:7

for b₁ being non empty non void ManySortedSign
for b₂ being V2 ManySortedSet of the carrier of b₁
for b₃, b₄ being non empty Subset of (b₁ -Terms b₂) holds
( the Arity of (b₃ -CircuitStr ) tolerates the Arity of (b₄ -CircuitStr ) & the ResultSort of (b₃ -CircuitStr ) tolerates the ResultSort of (b₄ -CircuitStr ) )

proof end;

registration

let c₁, c₂ be constituted-DTrees set ;
cluster a₁ \/ a₂ -> constituted-DTrees ;
coherence by TREES_3:9;

end;

theorem Th8: :: CIRCTRM1:8

for b₁, b₂ being non empty constituted-DTrees set holds Subtrees (b₁ \/ b₂) = (Subtrees b₁) \/ (Subtrees b₂)

proof end;

theorem Th9: :: CIRCTRM1:9

for b₁, b₂ being non empty constituted-DTrees set
for b₃ being set holds b₃ -Subtrees (b₁ \/ b₂) = (b₃ -Subtrees b₁) \/ (b₃ -Subtrees b₂)

proof end;

theorem Th10: :: CIRCTRM1:10

for b₁, b₂ being non empty constituted-DTrees set st ( for b₃ being Element of b₁ holds b₃ is finite ) & ( for b₃ being Element of b₂ holds b₃ is finite ) holds
for b₃ being set holds b₃ -ImmediateSubtrees (b₁ \/ b₂) = (b₃ -ImmediateSubtrees b₁) +* (b₃ -ImmediateSubtrees b₂)

proof end;

theorem Th11: :: CIRCTRM1:11

for b₁ being non empty non void ManySortedSign
for b₂ being V2 ManySortedSet of the carrier of b₁
for b₃, b₄ being non empty Subset of (b₁ -Terms b₂) holds (b₃ \/ b₄) -CircuitStr = (b₃ -CircuitStr ) +* (b₄ -CircuitStr )

proof end;

theorem Th12: :: CIRCTRM1:12

for b₁ being non empty non void ManySortedSign
for b₂ being V2 ManySortedSet of the carrier of b₁
for b₃ being non empty Subset of (b₁ -Terms b₂)
for b₄ being set holds
( b₄ in InputVertices (b₃ -CircuitStr ) iff ( b₄ in Subtrees b₃ & ex b₅ being SortSymbol of b₁ex b₆ being Element of b₂ . b₅ st b₄ = root-tree [b₆,b₅] ) )

proof end;

theorem Th13: :: CIRCTRM1:13

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be V2 ManySortedSet of the carrier of c₁;
let c₃ be non empty Subset of (c₁ -Terms c₂);
let c₄ be Vertex of (c₃ -CircuitStr );
let c₅ be MSAlgebra of c₁;
func the_sort_of c₄,c₅ -> set means :Def2: :: CIRCTRM1:def 2
for b₁ being Term of a₁,a₂ st b₁ = a₄ holds
a₆ = the Sorts of a₅ . (the_sort_of b₁);
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def2 defines the_sort_of CIRCTRM1:def 2 :

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be V2 ManySortedSet of the carrier of c₁;
let c₃ be non empty Subset of (c₁ -Terms c₂);
let c₄ be Vertex of (c₃ -CircuitStr );
let c₅ be non-empty MSAlgebra of c₁;
cluster the_sort_of a₄,a₅ -> non empty ;
coherence

proof end;

end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be V2 ManySortedSet of the carrier of c₁;
let c₃ be non empty Subset of (c₁ -Terms c₂);
assume E15: c₃ is SetWithCompoundTerm of c₁,c₂ ;
let c₄ be Gate of (c₃ -CircuitStr );
let c₅ be MSAlgebra of c₁;
func the_action_of c₄,c₅ -> Function means :Def3: :: CIRCTRM1:def 3
for b₁ being SetWithCompoundTerm of a₁,a₂ st b₁ = a₃ holds
for b₂ being Gate of (b₁ -CircuitStr ) st b₂ = a₄ holds
a₆ = the Charact of a₅ . ((b₂ . {} ) `1 );
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def3 defines the_action_of CIRCTRM1:def 3 :

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

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

provided

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

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be V2 ManySortedSet of the carrier of c₁;
let c₃ be non empty Subset of (c₁ -Terms c₂);
let c₄ be MSAlgebra of c₁;
func c₃ -CircuitSorts c₄ -> ManySortedSet of the carrier of (a₃ -CircuitStr ) means :Def4: :: CIRCTRM1:def 4
for b₁ being Vertex of (a₃ -CircuitStr ) holds a₅ . b₁ = the_sort_of b₁,a₄;
uniqueness

proof end;

existence

proof end;

end;

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

registration

proof end;

end;

theorem Th14: :: CIRCTRM1:14

for b₁ being non empty non void ManySortedSign
for b₂ being V2 ManySortedSet of the carrier of b₁
for b₃ being non-empty MSAlgebra of b₁
for b₄ being SetWithCompoundTerm of b₁,b₂
for b₅ being Gate of (b₄ -CircuitStr )
for b₆ being OperSymbol of b₁ st b₅ . {} = [b₆,the carrier of b₁] holds
(b₄ -CircuitSorts b₃) * (the_arity_of b₅) = the Sorts of b₃ * (the_arity_of b₆)

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be V2 ManySortedSet of the carrier of c₁;
let c₃ be non empty Subset of (c₁ -Terms c₂);
let c₄ be non-empty MSAlgebra of c₁;
func c₃ -CircuitCharact c₄ -> ManySortedFunction of ((a₃ -CircuitSorts a₄) # ) * the Arity of (a₃ -CircuitStr ),(a₃ -CircuitSorts a₄) * the ResultSort of (a₃ -CircuitStr ) means :Def5: :: CIRCTRM1:def 5
for b₁ being Gate of (a₃ -CircuitStr ) st b₁ in the OperSymbols of (a₃ -CircuitStr ) holds
a₅ . b₁ = the_action_of b₁,a₄;
uniqueness

proof end;

existence

proof end;

end;

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

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be V2 ManySortedSet of the carrier of c₁;
let c₃ be non empty Subset of (c₁ -Terms c₂);
let c₄ be non-empty MSAlgebra of c₁;
func c₃ -Circuit c₄ -> strict non-empty MSAlgebra of a₃ -CircuitStr equals :: CIRCTRM1:def 6
MSAlgebra(# (a₃ -CircuitSorts a₄),(a₃ -CircuitCharact a₄) #);
correctness

proof end;

end;

:: deftheorem Def6 defines -Circuit CIRCTRM1:def 6 :

theorem Th15: :: CIRCTRM1:15

for b₁ being non empty non void ManySortedSign
for b₂ being V2 ManySortedSet of the carrier of b₁
for b₃ being non-empty MSAlgebra of b₁
for b₄ being non empty Subset of (b₁ -Terms b₂)
for b₅ being Vertex of (b₄ -CircuitStr ) holds the Sorts of (b₄ -Circuit b₃) . b₅ = the_sort_of b₅,b₃ by Def4;

theorem Th16: :: CIRCTRM1:16

for b₁ being non empty non void ManySortedSign
for b₂ being V2 ManySortedSet of the carrier of b₁
for b₃ being non-empty locally-finite MSAlgebra of b₁
for b₄ being SetWithCompoundTerm of b₁,b₂
for b₅ being OperSymbol of (b₄ -CircuitStr ) holds Den b₅,(b₄ -Circuit b₃) = the_action_of b₅,b₃ by Def5;

theorem Th17: :: CIRCTRM1:17

for b₁ being non empty non void ManySortedSign
for b₂ being V2 ManySortedSet of the carrier of b₁
for b₃ being non-empty locally-finite MSAlgebra of b₁
for b₄ being SetWithCompoundTerm of b₁,b₂
for b₅ being OperSymbol of (b₄ -CircuitStr )
for b₆ being OperSymbol of b₁ st b₅ . {} = [b₆,the carrier of b₁] holds
Den b₅,(b₄ -Circuit b₃) = Den b₆,b₃

proof end;

theorem Th18: :: CIRCTRM1:18

for b₁ being non empty non void ManySortedSign
for b₂ being V2 ManySortedSet of the carrier of b₁
for b₃ being non-empty locally-finite MSAlgebra of b₁
for b₄ being non empty Subset of (b₁ -Terms b₂) holds b₄ -Circuit b₃ is locally-finite

proof end;

registration

end;

theorem Th19: :: CIRCTRM1:19

for b₁ being non empty non void ManySortedSign
for b₂ being V2 ManySortedSet of the carrier of b₁
for b₃, b₄ being SetWithCompoundTerm of b₁,b₂
for b₅ being non-empty MSAlgebra of b₁ holds b₃ -Circuit b₅ tolerates b₄ -Circuit b₅

proof end;

theorem Th20: :: CIRCTRM1:20

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
let c₃ be Variables of c₂;
let c₄ be DecoratedTree;
assume E23: c₄ is Term of c₁,c₃ ;
let c₅ be ManySortedFunction of c₃,the Sorts of c₂;
func c₄ @ c₅,c₂ -> set means :Def7: :: CIRCTRM1:def 7
ex b₁ being c-Term of a₂,a₃ st
( b₁ = a₄ & a₆ = b₁ @ a₅ );
correctness

proof end;

end;

:: deftheorem Def7 defines @ CIRCTRM1:def 7 :

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be V2 ManySortedSet of the carrier of c₁;
let c₃ be SetWithCompoundTerm of c₁,c₂;
let c₄ be non-empty locally-finite MSAlgebra of c₁;
let c₅ be State of (c₃ -Circuit c₄);
set c₆ = [:the OperSymbols of c₁,{the carrier of c₁}:];
defpred S₁[ set , set , set ] means ( root-tree [a₂,a₁] in Subtrees c₃ implies a₃ = c₅ . (root-tree [a₂,a₁]) );
E24: for b₁ being Vertex of c₁
for b₂ being Element of c₂ . b₁ ex b₃ being Element of the Sorts of c₄ . b₁ st S₁[b₁,b₂,b₃]

proof end;

mode CompatibleValuation of c₅ -> ManySortedFunction of a₂,the Sorts of a₄ means :Def8: :: CIRCTRM1:def 8
for b₁ being Vertex of a₁
for b₂ being Element of a₂ . b₁ st root-tree [b₂,b₁] in Subtrees a₃ holds
(a₆ . b₁) . b₂ = a₅ . (root-tree [b₂,b₁]);
existence

proof end;

end;

:: deftheorem Def8 defines CompatibleValuation CIRCTRM1:def 8 :

theorem Th21: :: CIRCTRM1:21

proof end;

registration

let c₁ be set ;
let c₂ be non empty non void ManySortedSign ;
let c₃ be V2 ManySortedSet of the carrier of c₂;
let c₄ be FinSequence of c₂ -Terms c₃;
cluster a₁ -tree a₄ -> finite ;
coherence

proof end;

end;

theorem Th22: :: CIRCTRM1:22

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty locally-finite MSAlgebra of b₁
for b₃ being Variables of b₂
for b₄ being SetWithCompoundTerm of b₁,b₃
for b₅ being State of (b₄ -Circuit b₂)
for b₆ being CompatibleValuation of b₅
for b₇ being Term of b₁,b₃ st b₇ in Subtrees b₄ holds
( Following b₅,(1 + (height (dom b₇))) is_stable_at b₇ & (Following b₅,(1 + (height (dom b₇)))) . b₇ = b₇ @ b₆,b₂ )

proof end;

theorem Th23: :: CIRCTRM1:23

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty locally-finite MSAlgebra of b₁
for b₃ being Variables of b₂
for b₄ being SetWithCompoundTerm of b₁,b₃ st ( for b₅ being Term of b₁,b₃
for b₆ being OperSymbol of b₁ holds
( not b₅ in Subtrees b₄ or not b₅ . {} = [b₆,the carrier of b₁] or not the_arity_of b₆ = {} ) ) holds
for b₅ being State of (b₄ -Circuit b₂)
for b₆ being CompatibleValuation of b₅
for b₇ being Term of b₁,b₃ st b₇ in Subtrees b₄ holds
( Following b₅,(height (dom b₇)) is_stable_at b₇ & (Following b₅,(height (dom b₇))) . b₇ = b₇ @ b₆,b₂ )

proof end;

registration

let c₁ be set ;
cluster id a₁ -> one-to-one ;
coherence by FUNCT_1:52;

end;

registration

let c₁ be one-to-one Function;
cluster a₁ " -> one-to-one ;
coherence by FUNCT_1:62;
let c₂ be one-to-one Function;
cluster a₁ * a₂ -> one-to-one ;
coherence by FUNCT_1:46;

end;

definition

let c₁, c₂ be non empty ManySortedSign ;
let c₃, c₄ be Function;
pred c₁,c₂ are_equivalent_wrt c₃,c₄ means :Def9: :: CIRCTRM1:def 9
( a₃ is one-to-one & a₄ is one-to-one & a₃,a₄ form_morphism_between a₁,a₂ & a₃ " ,a₄ " form_morphism_between a₂,a₁ );

end;

:: deftheorem Def9 defines are_equivalent_wrt CIRCTRM1:def 9 :

theorem Th24: :: CIRCTRM1:24

for b₁, b₂ being non empty ManySortedSign
for b₃, b₄ being Function st b₁,b₂ are_equivalent_wrt b₃,b₄ holds
( the carrier of b₂ = b₃ .: the carrier of b₁ & the OperSymbols of b₂ = b₄ .: the OperSymbols of b₁ )

proof end;

theorem Th25: :: CIRCTRM1:25

for b₁, b₂ being non empty ManySortedSign
for b₃, b₄ being Function st b₁,b₂ are_equivalent_wrt b₃,b₄ holds
( rng b₃ = the carrier of b₂ & rng b₄ = the OperSymbols of b₂ )

proof end;

theorem Th26: :: CIRCTRM1:26

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

proof end;

theorem Th27: :: CIRCTRM1:27

for b₁, b₂ being non empty ManySortedSign
for b₃, b₄ being Function st b₁,b₂ are_equivalent_wrt b₃,b₄ holds
b₂,b₁ are_equivalent_wrt b₃ " ,b₄ "

proof end;

theorem Th28: :: CIRCTRM1:28

for b₁, b₂, b₃ being non empty ManySortedSign
for b₄, b₅, b₆, b₇ being Function st b₁,b₂ are_equivalent_wrt b₄,b₅ & b₂,b₃ are_equivalent_wrt b₆,b₇ holds
b₁,b₃ are_equivalent_wrt b₆ * b₄,b₇ * b₅

proof end;

theorem Th29: :: CIRCTRM1:29

for b₁, b₂ being non empty ManySortedSign
for b₃, b₄ being Function st b₁,b₂ are_equivalent_wrt b₃,b₄ holds
( b₃ .: (InputVertices b₁) = InputVertices b₂ & b₃ .: (InnerVertices b₁) = InnerVertices b₂ )

proof end;

definition

let c₁, c₂ be non empty ManySortedSign ;
pred c₁,c₂ are_equivalent means :: CIRCTRM1:def 10
ex b₁, b₂ being one-to-one Function st a₁,a₂ are_equivalent_wrt b₁,b₂;
reflexivity

proof end;

symmetry

proof end;

end;

:: deftheorem Def10 defines are_equivalent CIRCTRM1:def 10 :

theorem Th30: :: CIRCTRM1:30

for b₁, b₂, b₃ being non empty ManySortedSign st b₁,b₂ are_equivalent & b₂,b₃ are_equivalent holds
b₁,b₃ are_equivalent

proof end;

definition

let c₁, c₂ be non empty ManySortedSign ;
let c₃ be Function;
pred c₃ preserves_inputs_of c₁,c₂ means :: CIRCTRM1:def 11
a₃ .: (InputVertices a₁) c= InputVertices a₂;

end;

:: deftheorem Def11 defines preserves_inputs_of CIRCTRM1:def 11 :

theorem Th31: :: CIRCTRM1:31

for b₁, b₂ being non empty ManySortedSign
for b₃, b₄ being Function st b₃,b₄ form_morphism_between b₁,b₂ holds
for b₅ being Vertex of b₁ holds b₃ . b₅ is Vertex of b₂

proof end;

theorem Th32: :: CIRCTRM1:32

for b₁, b₂ being non empty non void ManySortedSign
for b₃, b₄ being Function st b₃,b₄ form_morphism_between b₁,b₂ holds
for b₅ being Gate of b₁ holds b₄ . b₅ is Gate of b₂

proof end;

theorem Th33: :: CIRCTRM1:33

for b₁, b₂ being non empty ManySortedSign
for b₃, b₄ being Function st b₃,b₄ form_morphism_between b₁,b₂ holds
b₃ .: (InnerVertices b₁) c= InnerVertices b₂

proof end;

theorem Th34: :: CIRCTRM1:34

for b₁, b₂ being non empty non void Circuit-like ManySortedSign
for b₃, b₄ being Function st b₃,b₄ form_morphism_between b₁,b₂ holds
for b₅ being Vertex of b₁ st b₅ in InnerVertices b₁ holds
for b₆ being Vertex of b₂ st b₆ = b₃ . b₅ holds
action_at b₆ = b₄ . (action_at b₅)

proof end;

definition

let c₁, c₂ be non empty ManySortedSign ;
let c₃, c₄ be Function;
let c₅ be non-empty MSAlgebra of c₁;
let c₆ be non-empty MSAlgebra of c₂;
pred c₃,c₄ form_embedding_of c₅,c₆ means :Def12: :: CIRCTRM1:def 12
( a₃ is one-to-one & a₄ is one-to-one & a₃,a₄ form_morphism_between a₁,a₂ & the Sorts of a₅ = the Sorts of a₆ * a₃ & the Charact of a₅ = the Charact of a₆ * a₄ );

end;

:: deftheorem Def12 defines form_embedding_of CIRCTRM1:def 12 :

theorem Th35: :: CIRCTRM1:35

for b₁ being non empty ManySortedSign
for b₂ being non-empty MSAlgebra of b₁ holds id the carrier of b₁, id the OperSymbols of b₁ form_embedding_of b₂,b₂

proof end;

theorem Th36: :: CIRCTRM1:36

for b₁, b₂, b₃ being non empty ManySortedSign
for b₄, b₅, b₆, b₇ being Function
for b₈ being non-empty MSAlgebra of b₁
for b₉ being non-empty MSAlgebra of b₂
for b₁₀ being non-empty MSAlgebra of b₃ st b₄,b₅ form_embedding_of b₈,b₉ & b₆,b₇ form_embedding_of b₉,b₁₀ holds
b₆ * b₄,b₇ * b₅ form_embedding_of b₈,b₁₀

proof end;

definition

let c₁, c₂ be non empty ManySortedSign ;
let c₃, c₄ be Function;
let c₅ be non-empty MSAlgebra of c₁;
let c₆ be non-empty MSAlgebra of c₂;
pred c₅,c₆ are_similar_wrt c₃,c₄ means :Def13: :: CIRCTRM1:def 13
( a₃,a₄ form_embedding_of a₅,a₆ & a₃ " ,a₄ " form_embedding_of a₆,a₅ );

end;

:: deftheorem Def13 defines are_similar_wrt CIRCTRM1:def 13 :

theorem Th37: :: CIRCTRM1:37

for b₁, b₂ being non empty ManySortedSign
for b₃, b₄ being Function
for b₅ being non-empty MSAlgebra of b₁
for b₆ being non-empty MSAlgebra of b₂ st b₅,b₆ are_similar_wrt b₃,b₄ holds
b₁,b₂ are_equivalent_wrt b₃,b₄

proof end;

theorem Th38: :: CIRCTRM1:38

for b₁, b₂ being non empty ManySortedSign
for b₃, b₄ being Function
for b₅ being non-empty MSAlgebra of b₁
for b₆ being non-empty MSAlgebra of b₂ holds
( b₅,b₆ are_similar_wrt b₃,b₄ iff ( b₁,b₂ are_equivalent_wrt b₃,b₄ & the Sorts of b₅ = the Sorts of b₆ * b₃ & the Charact of b₅ = the Charact of b₆ * b₄ ) )

proof end;

theorem Th39: :: CIRCTRM1:39

for b₁ being non empty ManySortedSign
for b₂ being non-empty MSAlgebra of b₁ holds b₂,b₂ are_similar_wrt id the carrier of b₁, id the OperSymbols of b₁

proof end;

theorem Th40: :: CIRCTRM1:40

proof end;

theorem Th41: :: CIRCTRM1:41

for b₁, b₂, b₃ being non empty ManySortedSign
for b₄, b₅, b₆, b₇ being Function
for b₈ being non-empty MSAlgebra of b₁
for b₉ being non-empty MSAlgebra of b₂
for b₁₀ being non-empty MSAlgebra of b₃ st b₈,b₉ are_similar_wrt b₄,b₅ & b₉,b₁₀ are_similar_wrt b₆,b₇ holds
b₈,b₁₀ are_similar_wrt b₆ * b₄,b₇ * b₅

proof end;

definition

let c₁, c₂ be non empty ManySortedSign ;
let c₃ be non-empty MSAlgebra of c₁;
let c₄ be non-empty MSAlgebra of c₂;
pred c₃,c₄ are_similar means :: CIRCTRM1:def 14
ex b₁, b₂ being Function st a₃,a₄ are_similar_wrt b₁,b₂;

end;

:: deftheorem Def14 defines are_similar CIRCTRM1:def 14 :

theorem Th42: :: CIRCTRM1:42

for b₁, b₂ being non empty non void Circuit-like ManySortedSign
for b₃, b₄ being Function
for b₅ being non-empty Circuit of b₁
for b₆ being non-empty Circuit of b₂ st b₃,b₄ form_embedding_of b₅,b₆ holds
( dom b₃ = the carrier of b₁ & rng b₃ c= the carrier of b₂ & dom b₄ = the OperSymbols of b₁ & rng b₄ c= the OperSymbols of b₂ )

proof end;

theorem Th43: :: CIRCTRM1:43

for b₁, b₂ being non empty non void Circuit-like ManySortedSign
for b₃, b₄ being Function
for b₅ being non-empty Circuit of b₁
for b₆ being non-empty Circuit of b₂ st b₃,b₄ form_embedding_of b₅,b₆ holds
for b₇ being Gate of b₁
for b₈ being Gate of b₂ st b₈ = b₄ . b₇ holds
Den b₈,b₆ = Den b₇,b₅

proof end;

theorem Th44: :: CIRCTRM1:44

for b₁, b₂ being non empty non void Circuit-like ManySortedSign
for b₃, b₄ being Function
for b₅ being non-empty Circuit of b₁
for b₆ being non-empty Circuit of b₂ st b₃,b₄ form_embedding_of b₅,b₆ holds
for b₇ being Gate of b₁
for b₈ being Gate of b₂ st b₈ = b₄ . b₇ holds
for b₉ being State of b₅
for b₁₀ being State of b₆ st b₉ = b₁₀ * b₃ holds
b₈ depends_on_in b₁₀ = b₇ depends_on_in b₉

proof end;

theorem Th45: :: CIRCTRM1:45

proof end;

theorem Th46: :: CIRCTRM1:46

for b₁, b₂ being non empty non void Circuit-like ManySortedSign
for b₃, b₄ being Function
for b₅ being non-empty Circuit of b₂
for b₆ being non-empty Circuit of b₁ st b₃,b₄ form_embedding_of b₅,b₆ holds
for b₇ being State of b₆
for b₈ being State of b₅ st b₈ = b₇ * b₃ & ( for b₉ being Vertex of b₂ st b₉ in InputVertices b₂ holds
b₇ is_stable_at b₃ . b₉ ) holds
Following b₈ = (Following b₇) * b₃

proof end;

theorem Th47: :: CIRCTRM1:47

for b₁, b₂ being non empty non void Circuit-like ManySortedSign
for b₃, b₄ being Function
for b₅ being non-empty Circuit of b₁
for b₆ being non-empty Circuit of b₂ st b₃,b₄ form_embedding_of b₅,b₆ & b₃ preserves_inputs_of b₁,b₂ holds
for b₇ being State of b₆
for b₈ being State of b₅ st b₈ = b₇ * b₃ holds
Following b₈ = (Following b₇) * b₃

proof end;

theorem Th48: :: CIRCTRM1:48

for b₁, b₂ being non empty non void Circuit-like ManySortedSign
for b₃, b₄ being Function
for b₅ being non-empty Circuit of b₁
for b₆ being non-empty Circuit of b₂ st b₃,b₄ form_embedding_of b₅,b₆ & b₃ preserves_inputs_of b₁,b₂ holds
for b₇ being State of b₆
for b₈ being State of b₅ st b₈ = b₇ * b₃ holds
for b₉ being Nat holds Following b₈,b₉ = (Following b₇,b₉) * b₃

proof end;

theorem Th49: :: CIRCTRM1:49

for b₁, b₂ being non empty non void Circuit-like ManySortedSign
for b₃, b₄ being Function
for b₅ being non-empty Circuit of b₁
for b₆ being non-empty Circuit of b₂ st b₃,b₄ form_embedding_of b₅,b₆ & b₃ preserves_inputs_of b₁,b₂ holds
for b₇ being State of b₆
for b₈ being State of b₅ st b₈ = b₇ * b₃ & b₇ is stable holds
b₈ is stable

proof end;

theorem Th50: :: CIRCTRM1:50

for b₁, b₂ being non empty non void Circuit-like ManySortedSign
for b₃, b₄ being Function
for b₅ being non-empty Circuit of b₁
for b₆ being non-empty Circuit of b₂ st b₃,b₄ form_embedding_of b₅,b₆ & b₃ preserves_inputs_of b₁,b₂ holds
for b₇ being State of b₆
for b₈ being State of b₅ st b₈ = b₇ * b₃ holds
for b₉ being Vertex of b₁ holds
( b₈ is_stable_at b₉ iff b₇ is_stable_at b₃ . b₉ )

proof end;

theorem Th51: :: CIRCTRM1:51

for b₁, b₂ being non empty non void Circuit-like ManySortedSign
for b₃, b₄ being Function
for b₅ being non-empty Circuit of b₁
for b₆ being non-empty Circuit of b₂ st b₅,b₆ are_similar_wrt b₃,b₄ holds
for b₇ being State of b₆ holds b₇ * b₃ is State of b₅

proof end;

theorem Th52: :: CIRCTRM1:52

proof end;

theorem Th53: :: CIRCTRM1:53

for b₁, b₂ being non empty non void Circuit-like ManySortedSign
for b₃, b₄ being Function
for b₅ being non-empty Circuit of b₁
for b₆ being non-empty Circuit of b₂ st b₅,b₆ are_similar_wrt b₃,b₄ holds
( b₃ .: (InputVertices b₁) = InputVertices b₂ & b₃ .: (InnerVertices b₁) = InnerVertices b₂ )

proof end;

theorem Th54: :: CIRCTRM1:54

proof end;

theorem Th55: :: CIRCTRM1:55

proof end;

theorem Th56: :: CIRCTRM1:56

proof end;

theorem Th57: :: CIRCTRM1:57

proof end;

theorem Th58: :: CIRCTRM1:58

for b₁, b₂ being non empty non void Circuit-like ManySortedSign
for b₃, b₄ being Function
for b₅ being non-empty Circuit of b₂
for b₆ being non-empty Circuit of b₁ st b₅,b₆ are_similar_wrt b₃,b₄ holds
for b₇ being State of b₅
for b₈ being State of b₆ st b₇ = b₈ * b₃ holds
for b₉ being Vertex of b₂ holds
( b₇ is_stable_at b₉ iff b₈ is_stable_at b₃ . b₉ )

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
let c₃ be V2 ManySortedSet of the carrier of c₁;
let c₄ be non empty Subset of (c₁ -Terms c₃);
let c₅ be non empty non void Circuit-like ManySortedSign ;
let c₆ be non-empty Circuit of c₅;
pred c₆ calculates c₄,c₂ means :Def15: :: CIRCTRM1:def 15
ex b₁, b₂ being Function st
( b₁,b₂ form_embedding_of a₄ -Circuit a₂,a₆ & b₁ preserves_inputs_of a₄ -CircuitStr ,a₅ );
pred c₄,c₂ specifies c₆ means :: CIRCTRM1:def 16
a₆,a₄ -Circuit a₂ are_similar ;

end;

:: deftheorem Def15 defines calculates CIRCTRM1:def 15 :

:: deftheorem Def16 defines specifies CIRCTRM1:def 16 :

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be V2 ManySortedSet of the carrier of c₁;
let c₃ be non-empty MSAlgebra of c₁;
let c₄ be non empty Subset of (c₁ -Terms c₂);
let c₅ be non empty non void Circuit-like ManySortedSign ;
let c₆ be non-empty Circuit of c₅;
assume c₆ calculates c₄,c₃ ;
then consider c₇, c₈ being Function such that
E58: c₇,c₈ form_embedding_of c₄ -Circuit c₃,c₆ and
E59: c₇ preserves_inputs_of c₄ -CircuitStr ,c₅ by Def15;
E60: c₇ is one-to-one by E58, Def12;
mode SortMap of c₄,c₃,c₆ -> one-to-one Function means :Def17: :: CIRCTRM1:def 17
( a₇ preserves_inputs_of a₄ -CircuitStr ,a₅ & ex b₁ being Function st a₇,b₁ form_embedding_of a₄ -Circuit a₃,a₆ );
existence by E58, E59, E60;

end;

:: deftheorem Def17 defines SortMap CIRCTRM1:def 17 :

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be V2 ManySortedSet of the carrier of c₁;
let c₃ be non-empty MSAlgebra of c₁;
let c₄ be non empty Subset of (c₁ -Terms c₂);
let c₅ be non empty non void Circuit-like ManySortedSign ;
let c₆ be non-empty Circuit of c₅;
assume E59: c₆ calculates c₄,c₃ ;
let c₇ be SortMap of c₄,c₃,c₆;
consider c₈ being Function such that
E60: c₇,c₈ form_embedding_of c₄ -Circuit c₃,c₆ by E59, Def17;
E61: c₈ is one-to-one by E60, Def12;
mode OperMap of c₄,c₃,c₆,c₇ -> one-to-one Function means :: CIRCTRM1:def 18
a₇,a₈ form_embedding_of a₄ -Circuit a₃,a₆;
existence by E60, E61;

end;

:: deftheorem Def18 defines OperMap CIRCTRM1:def 18 :

theorem Th59: :: CIRCTRM1:59

proof end;

theorem Th60: :: CIRCTRM1:60

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty locally-finite MSAlgebra of b₁
for b₃ being Variables of b₂
for b₄ being SetWithCompoundTerm of b₁,b₃
for b₅ being non empty non void Circuit-like ManySortedSign
for b₆ being non-empty Circuit of b₅ st b₆ calculates b₄,b₂ holds
for b₇ being SortMap of b₄,b₂,b₆
for b₈ being Term of b₁,b₃ st b₈ in Subtrees b₄ holds
for b₉ being State of b₆ holds
( Following b₉,(1 + (height (dom b₈))) is_stable_at b₇ . b₈ & ( for b₁₀ being State of (b₄ -Circuit b₂) st b₁₀ = b₉ * b₇ holds
for b₁₁ being CompatibleValuation of b₁₀ holds (Following b₉,(1 + (height (dom b₈)))) . (b₇ . b₈) = b₈ @ b₁₁,b₂ ) )

proof end;

theorem Th61: :: CIRCTRM1:61

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty locally-finite MSAlgebra of b₁
for b₃ being Variables of b₂
for b₄ being SetWithCompoundTerm of b₁,b₃
for b₅ being non empty non void Circuit-like ManySortedSign
for b₆ being non-empty Circuit of b₅ st b₆ calculates b₄,b₂ holds
for b₇ being Term of b₁,b₃ st b₇ in Subtrees b₄ holds
ex b₈ being Vertex of b₅ st
for b₉ being State of b₆ holds
( Following b₉,(1 + (height (dom b₇))) is_stable_at b₈ & ex b₁₀ being SortMap of b₄,b₂,b₆ st
for b₁₁ being State of (b₄ -Circuit b₂) st b₁₁ = b₉ * b₁₀ holds
for b₁₂ being CompatibleValuation of b₁₁ holds (Following b₉,(1 + (height (dom b₇)))) . b₈ = b₇ @ b₁₂,b₂ )

proof end;

theorem Th62: :: CIRCTRM1:62

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty locally-finite MSAlgebra of b₁
for b₃ being Variables of b₂
for b₄ being SetWithCompoundTerm of b₁,b₃
for b₅ being non empty non void Circuit-like ManySortedSign
for b₆ being non-empty Circuit of b₅ st b₄,b₂ specifies b₆ holds
for b₇ being SortMap of b₄,b₂,b₆
for b₈ being State of b₆
for b₉ being Term of b₁,b₃ st b₉ in Subtrees b₄ holds
( Following b₈,(1 + (height (dom b₉))) is_stable_at b₇ . b₉ & ( for b₁₀ being State of (b₄ -Circuit b₂) st b₁₀ = b₈ * b₇ holds
for b₁₁ being CompatibleValuation of b₁₀ holds (Following b₈,(1 + (height (dom b₉)))) . (b₇ . b₉) = b₉ @ b₁₁,b₂ ) )

proof end;

theorem Th63: :: CIRCTRM1:63

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty locally-finite MSAlgebra of b₁
for b₃ being Variables of b₂
for b₄ being SetWithCompoundTerm of b₁,b₃
for b₅ being non empty non void Circuit-like ManySortedSign
for b₆ being non-empty Circuit of b₅ st b₄,b₂ specifies b₆ holds
for b₇ being Term of b₁,b₃ st b₇ in Subtrees b₄ holds
ex b₈ being Vertex of b₅ st
for b₉ being State of b₆ holds
( Following b₉,(1 + (height (dom b₇))) is_stable_at b₈ & ex b₁₀ being SortMap of b₄,b₂,b₆ st
for b₁₁ being State of (b₄ -Circuit b₂) st b₁₁ = b₉ * b₁₀ holds
for b₁₂ being CompatibleValuation of b₁₁ holds (Following b₉,(1 + (height (dom b₇)))) . b₈ = b₇ @ b₁₂,b₂ )

proof end;