:: by Yatsuka Nakamura and Grzegorz Bancerek

::

:: Received May 11, 1995

:: Copyright (c) 1995-2012 Association of Mizar Users

begin

Lm1: now :: thesis: for i being Element of NAT

for X being non empty set holds product ((Seg i) --> X) = i -tuples_on X

for X being non empty set holds product ((Seg i) --> X) = i -tuples_on X

let i be Element of NAT ; :: thesis: for X being non empty set holds product ((Seg i) --> X) = i -tuples_on X

let X be non empty set ; :: thesis: product ((Seg i) --> X) = i -tuples_on X

thus product ((Seg i) --> X) = product (i |-> X) by FINSEQ_2:def 2

.= i -tuples_on X by FINSEQ_3:131 ; :: thesis: verum

end;
let X be non empty set ; :: thesis: product ((Seg i) --> X) = i -tuples_on X

thus product ((Seg i) --> X) = product (i |-> X) by FINSEQ_2:def 2

.= i -tuples_on X by FINSEQ_3:131 ; :: thesis: verum

registration

let A, B be set ;

let f be ManySortedSet of A;

let g be ManySortedSet of B;

coherence

f +* g is A \/ B -defined

end;
let f be ManySortedSet of A;

let g be ManySortedSet of B;

coherence

f +* g is A \/ B -defined

proof end;

registration

let A, B be set ;

let f be ManySortedSet of A;

let g be ManySortedSet of B;

coherence

for b_{1} being A \/ B -defined Function st b_{1} = f +* g holds

b_{1} is total

end;
let f be ManySortedSet of A;

let g be ManySortedSet of B;

coherence

for b

b

proof end;

registration
end;

registration

let A, B be set ;

coherence

for b_{1} being {A} -defined Function st b_{1} = A .--> B holds

b_{1} is total
;

end;
coherence

for b

b

registration
end;

theorem Th1: :: CIRCCOMB:1

for A, B being set

for f being ManySortedSet of A

for g being ManySortedSet of B st f c= g holds

f # c= g #

for f being ManySortedSet of A

for g being ManySortedSet of B st f c= g holds

f # c= g #

proof end;

theorem Th2: :: CIRCCOMB:2

for X being set

for Y being non empty set

for p being FinSequence of X holds ((X --> Y) #) . p = (len p) -tuples_on Y

for Y being non empty set

for p being FinSequence of X holds ((X --> Y) #) . p = (len p) -tuples_on Y

proof end;

definition

let A be set ;

let f1, g1 be V2() ManySortedSet of A;

let B be set ;

let f2, g2 be V2() ManySortedSet of B;

let h1 be ManySortedFunction of f1,g1;

let h2 be ManySortedFunction of f2,g2;

:: original: +*

redefine func h1 +* h2 -> ManySortedFunction of f1 +* f2,g1 +* g2;

coherence

h1 +* h2 is ManySortedFunction of f1 +* f2,g1 +* g2

end;
let f1, g1 be V2() ManySortedSet of A;

let B be set ;

let f2, g2 be V2() ManySortedSet of B;

let h1 be ManySortedFunction of f1,g1;

let h2 be ManySortedFunction of f2,g2;

:: original: +*

redefine func h1 +* h2 -> ManySortedFunction of f1 +* f2,g1 +* g2;

coherence

h1 +* h2 is ManySortedFunction of f1 +* f2,g1 +* g2

proof end;

definition

let S1, S2 be ManySortedSign ;

for S1 being ManySortedSign holds

( the Arity of S1 tolerates the Arity of S1 & the ResultSort of S1 tolerates the ResultSort of S1 ) ;

symmetry

for S1, S2 being ManySortedSign st the Arity of S1 tolerates the Arity of S2 & the ResultSort of S1 tolerates the ResultSort of S2 holds

( the Arity of S2 tolerates the Arity of S1 & the ResultSort of S2 tolerates the ResultSort of S1 ) ;

end;
pred S1 tolerates S2 means :: CIRCCOMB:def 1

( the Arity of S1 tolerates the Arity of S2 & the ResultSort of S1 tolerates the ResultSort of S2 );

reflexivity ( the Arity of S1 tolerates the Arity of S2 & the ResultSort of S1 tolerates the ResultSort of S2 );

for S1 being ManySortedSign holds

( the Arity of S1 tolerates the Arity of S1 & the ResultSort of S1 tolerates the ResultSort of S1 ) ;

symmetry

for S1, S2 being ManySortedSign st the Arity of S1 tolerates the Arity of S2 & the ResultSort of S1 tolerates the ResultSort of S2 holds

( the Arity of S2 tolerates the Arity of S1 & the ResultSort of S2 tolerates the ResultSort of S1 ) ;

:: deftheorem defines tolerates CIRCCOMB:def 1 :

for S1, S2 being ManySortedSign holds

( S1 tolerates S2 iff ( the Arity of S1 tolerates the Arity of S2 & the ResultSort of S1 tolerates the ResultSort of S2 ) );

for S1, S2 being ManySortedSign holds

( S1 tolerates S2 iff ( the Arity of S1 tolerates the Arity of S2 & the ResultSort of S1 tolerates the ResultSort of S2 ) );

definition

let S1, S2 be non empty ManySortedSign ;

ex b_{1} being non empty strict ManySortedSign st

( the carrier of b_{1} = the carrier of S1 \/ the carrier of S2 & the carrier' of b_{1} = the carrier' of S1 \/ the carrier' of S2 & the Arity of b_{1} = the Arity of S1 +* the Arity of S2 & the ResultSort of b_{1} = the ResultSort of S1 +* the ResultSort of S2 )

for b_{1}, b_{2} being non empty strict ManySortedSign st the carrier of b_{1} = the carrier of S1 \/ the carrier of S2 & the carrier' of b_{1} = the carrier' of S1 \/ the carrier' of S2 & the Arity of b_{1} = the Arity of S1 +* the Arity of S2 & the ResultSort of b_{1} = the ResultSort of S1 +* the ResultSort of S2 & the carrier of b_{2} = the carrier of S1 \/ the carrier of S2 & the carrier' of b_{2} = the carrier' of S1 \/ the carrier' of S2 & the Arity of b_{2} = the Arity of S1 +* the Arity of S2 & the ResultSort of b_{2} = the ResultSort of S1 +* the ResultSort of S2 holds

b_{1} = b_{2}
;

end;
func S1 +* S2 -> non empty strict ManySortedSign means :Def2: :: CIRCCOMB:def 2

( the carrier of it = the carrier of S1 \/ the carrier of S2 & the carrier' of it = the carrier' of S1 \/ the carrier' of S2 & the Arity of it = the Arity of S1 +* the Arity of S2 & the ResultSort of it = the ResultSort of S1 +* the ResultSort of S2 );

existence ( the carrier of it = the carrier of S1 \/ the carrier of S2 & the carrier' of it = the carrier' of S1 \/ the carrier' of S2 & the Arity of it = the Arity of S1 +* the Arity of S2 & the ResultSort of it = the ResultSort of S1 +* the ResultSort of S2 );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def2 defines +* CIRCCOMB:def 2 :

for S1, S2 being non empty ManySortedSign

for b_{3} being non empty strict ManySortedSign holds

( b_{3} = S1 +* S2 iff ( the carrier of b_{3} = the carrier of S1 \/ the carrier of S2 & the carrier' of b_{3} = the carrier' of S1 \/ the carrier' of S2 & the Arity of b_{3} = the Arity of S1 +* the Arity of S2 & the ResultSort of b_{3} = the ResultSort of S1 +* the ResultSort of S2 ) );

for S1, S2 being non empty ManySortedSign

for b

( b

theorem Th3: :: CIRCCOMB:3

for S1, S2, S3 being non empty ManySortedSign st S1 tolerates S2 & S2 tolerates S3 & S3 tolerates S1 holds

S1 +* S2 tolerates S3

S1 +* S2 tolerates S3

proof end;

theorem :: CIRCCOMB:4

for S being non empty ManySortedSign holds S +* S = ManySortedSign(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S #)

proof end;

theorem :: CIRCCOMB:7

for f being one-to-one Function

for S1, S2 being non empty Circuit-like ManySortedSign st the ResultSort of S1 c= f & the ResultSort of S2 c= f holds

S1 +* S2 is Circuit-like

for S1, S2 being non empty Circuit-like ManySortedSign st the ResultSort of S1 c= f & the ResultSort of S2 c= f holds

S1 +* S2 is Circuit-like

proof end;

theorem :: CIRCCOMB:8

for S1, S2 being non empty Circuit-like ManySortedSign st InnerVertices S1 misses InnerVertices S2 holds

S1 +* S2 is Circuit-like

S1 +* S2 is Circuit-like

proof end;

theorem Th9: :: CIRCCOMB:9

for S1, S2 being non empty ManySortedSign st ( not S1 is void or not S2 is void ) holds

not S1 +* S2 is void

not S1 +* S2 is void

proof end;

registration

let S1 be non empty non void ManySortedSign ;

let S2 be non empty ManySortedSign ;

coherence

not S1 +* S2 is void by Th9;

coherence

not S2 +* S1 is void by Th9;

end;
let S2 be non empty ManySortedSign ;

coherence

not S1 +* S2 is void by Th9;

coherence

not S2 +* S1 is void by Th9;

theorem Th11: :: CIRCCOMB:11

for S1, S2 being non empty ManySortedSign st S1 tolerates S2 holds

( InnerVertices (S1 +* S2) = (InnerVertices S1) \/ (InnerVertices S2) & InputVertices (S1 +* S2) c= (InputVertices S1) \/ (InputVertices S2) )

( InnerVertices (S1 +* S2) = (InnerVertices S1) \/ (InnerVertices S2) & InputVertices (S1 +* S2) c= (InputVertices S1) \/ (InputVertices S2) )

proof end;

theorem Th12: :: CIRCCOMB:12

for S1, S2 being non empty ManySortedSign

for v2 being Vertex of S2 st v2 in InputVertices (S1 +* S2) holds

v2 in InputVertices S2

for v2 being Vertex of S2 st v2 in InputVertices (S1 +* S2) holds

v2 in InputVertices S2

proof end;

theorem Th13: :: CIRCCOMB:13

for S1, S2 being non empty ManySortedSign st S1 tolerates S2 holds

for v1 being Vertex of S1 st v1 in InputVertices (S1 +* S2) holds

v1 in InputVertices S1

for v1 being Vertex of S1 st v1 in InputVertices (S1 +* S2) holds

v1 in InputVertices S1

proof end;

theorem Th14: :: CIRCCOMB:14

for S1 being non empty ManySortedSign

for S2 being non empty non void ManySortedSign

for o2 being OperSymbol of S2

for o being OperSymbol of (S1 +* S2) st o2 = o holds

( the_arity_of o = the_arity_of o2 & the_result_sort_of o = the_result_sort_of o2 )

for S2 being non empty non void ManySortedSign

for o2 being OperSymbol of S2

for o being OperSymbol of (S1 +* S2) st o2 = o holds

( the_arity_of o = the_arity_of o2 & the_result_sort_of o = the_result_sort_of o2 )

proof end;

theorem Th15: :: CIRCCOMB:15

for S1 being non empty ManySortedSign

for S2, S being non empty non void Circuit-like ManySortedSign st S = S1 +* S2 holds

for v2 being Vertex of S2 st v2 in InnerVertices S2 holds

for v being Vertex of S st v2 = v holds

( v in InnerVertices S & action_at v = action_at v2 )

for S2, S being non empty non void Circuit-like ManySortedSign st S = S1 +* S2 holds

for v2 being Vertex of S2 st v2 in InnerVertices S2 holds

for v being Vertex of S st v2 = v holds

( v in InnerVertices S & action_at v = action_at v2 )

proof end;

theorem Th16: :: CIRCCOMB:16

for S1 being non empty non void ManySortedSign

for S2 being non empty ManySortedSign st S1 tolerates S2 holds

for o1 being OperSymbol of S1

for o being OperSymbol of (S1 +* S2) st o1 = o holds

( the_arity_of o = the_arity_of o1 & the_result_sort_of o = the_result_sort_of o1 )

for S2 being non empty ManySortedSign st S1 tolerates S2 holds

for o1 being OperSymbol of S1

for o being OperSymbol of (S1 +* S2) st o1 = o holds

( the_arity_of o = the_arity_of o1 & the_result_sort_of o = the_result_sort_of o1 )

proof end;

theorem Th17: :: CIRCCOMB:17

for S1, S being non empty non void Circuit-like ManySortedSign

for S2 being non empty ManySortedSign st S1 tolerates S2 & S = S1 +* S2 holds

for v1 being Vertex of S1 st v1 in InnerVertices S1 holds

for v being Vertex of S st v1 = v holds

( v in InnerVertices S & action_at v = action_at v1 )

for S2 being non empty ManySortedSign st S1 tolerates S2 & S = S1 +* S2 holds

for v1 being Vertex of S1 st v1 in InnerVertices S1 holds

for v being Vertex of S st v1 = v holds

( v in InnerVertices S & action_at v = action_at v1 )

proof end;

begin

definition
end;

:: deftheorem Def3 defines tolerates CIRCCOMB:def 3 :

for S1, S2 being non empty ManySortedSign

for A1 being MSAlgebra over S1

for A2 being MSAlgebra over S2 holds

( A1 tolerates A2 iff ( S1 tolerates S2 & the Sorts of A1 tolerates the Sorts of A2 & the Charact of A1 tolerates the Charact of A2 ) );

for S1, S2 being non empty ManySortedSign

for A1 being MSAlgebra over S1

for A2 being MSAlgebra over S2 holds

( A1 tolerates A2 iff ( S1 tolerates S2 & the Sorts of A1 tolerates the Sorts of A2 & the Charact of A1 tolerates the Charact of A2 ) );

definition

let S1, S2 be non empty ManySortedSign ;

let A1 be non-empty MSAlgebra over S1;

let A2 be non-empty MSAlgebra over S2;

assume A1: the Sorts of A1 tolerates the Sorts of A2 ;

for b_{1}, b_{2} being strict non-empty MSAlgebra over S1 +* S2 st the Sorts of b_{1} = the Sorts of A1 +* the Sorts of A2 & the Charact of b_{1} = the Charact of A1 +* the Charact of A2 & the Sorts of b_{2} = the Sorts of A1 +* the Sorts of A2 & the Charact of b_{2} = the Charact of A1 +* the Charact of A2 holds

b_{1} = b_{2}
;

existence

ex b_{1} being strict non-empty MSAlgebra over S1 +* S2 st

( the Sorts of b_{1} = the Sorts of A1 +* the Sorts of A2 & the Charact of b_{1} = the Charact of A1 +* the Charact of A2 )

end;
let A1 be non-empty MSAlgebra over S1;

let A2 be non-empty MSAlgebra over S2;

assume A1: the Sorts of A1 tolerates the Sorts of A2 ;

func A1 +* A2 -> strict non-empty MSAlgebra over S1 +* S2 means :Def4: :: CIRCCOMB:def 4

( the Sorts of it = the Sorts of A1 +* the Sorts of A2 & the Charact of it = the Charact of A1 +* the Charact of A2 );

uniqueness ( the Sorts of it = the Sorts of A1 +* the Sorts of A2 & the Charact of it = the Charact of A1 +* the Charact of A2 );

for b

b

existence

ex b

( the Sorts of b

proof end;

:: deftheorem Def4 defines +* CIRCCOMB:def 4 :

for S1, S2 being non empty ManySortedSign

for A1 being non-empty MSAlgebra over S1

for A2 being non-empty MSAlgebra over S2 st the Sorts of A1 tolerates the Sorts of A2 holds

for b_{5} being strict non-empty MSAlgebra over S1 +* S2 holds

( b_{5} = A1 +* A2 iff ( the Sorts of b_{5} = the Sorts of A1 +* the Sorts of A2 & the Charact of b_{5} = the Charact of A1 +* the Charact of A2 ) );

for S1, S2 being non empty ManySortedSign

for A1 being non-empty MSAlgebra over S1

for A2 being non-empty MSAlgebra over S2 st the Sorts of A1 tolerates the Sorts of A2 holds

for b

( b

theorem Th19: :: CIRCCOMB:19

for S1, S2 being non empty non void ManySortedSign

for A1 being MSAlgebra over S1

for A2 being MSAlgebra over S2 st A1 tolerates A2 holds

A2 tolerates A1

for A1 being MSAlgebra over S1

for A2 being MSAlgebra over S2 st A1 tolerates A2 holds

A2 tolerates A1

proof end;

theorem :: CIRCCOMB:20

for S1, S2, S3 being non empty ManySortedSign

for A1 being non-empty MSAlgebra over S1

for A2 being non-empty MSAlgebra over S2

for A3 being MSAlgebra over S3 st A1 tolerates A2 & A2 tolerates A3 & A3 tolerates A1 holds

A1 +* A2 tolerates A3

for A1 being non-empty MSAlgebra over S1

for A2 being non-empty MSAlgebra over S2

for A3 being MSAlgebra over S3 st A1 tolerates A2 & A2 tolerates A3 & A3 tolerates A1 holds

A1 +* A2 tolerates A3

proof end;

theorem :: CIRCCOMB:21

for S being non empty strict ManySortedSign

for A being non-empty MSAlgebra over S holds A +* A = MSAlgebra(# the Sorts of A, the Charact of A #)

for A being non-empty MSAlgebra over S holds A +* A = MSAlgebra(# the Sorts of A, the Charact of A #)

proof end;

theorem Th22: :: CIRCCOMB:22

for S1, S2 being non empty ManySortedSign

for A1 being non-empty MSAlgebra over S1

for A2 being non-empty MSAlgebra over S2 st A1 tolerates A2 holds

A1 +* A2 = A2 +* A1

for A1 being non-empty MSAlgebra over S1

for A2 being non-empty MSAlgebra over S2 st A1 tolerates A2 holds

A1 +* A2 = A2 +* A1

proof end;

theorem :: CIRCCOMB:23

for S1, S2, S3 being non empty ManySortedSign

for A1 being non-empty MSAlgebra over S1

for A2 being non-empty MSAlgebra over S2

for A3 being non-empty MSAlgebra over S3 st the Sorts of A1 tolerates the Sorts of A2 & the Sorts of A2 tolerates the Sorts of A3 & the Sorts of A3 tolerates the Sorts of A1 holds

(A1 +* A2) +* A3 = A1 +* (A2 +* A3)

for A1 being non-empty MSAlgebra over S1

for A2 being non-empty MSAlgebra over S2

for A3 being non-empty MSAlgebra over S3 st the Sorts of A1 tolerates the Sorts of A2 & the Sorts of A2 tolerates the Sorts of A3 & the Sorts of A3 tolerates the Sorts of A1 holds

(A1 +* A2) +* A3 = A1 +* (A2 +* A3)

proof end;

theorem :: CIRCCOMB:24

for S1, S2 being non empty ManySortedSign

for A1 being non-empty finite-yielding MSAlgebra over S1

for A2 being non-empty finite-yielding MSAlgebra over S2 st the Sorts of A1 tolerates the Sorts of A2 holds

A1 +* A2 is finite-yielding

for A1 being non-empty finite-yielding MSAlgebra over S1

for A2 being non-empty finite-yielding MSAlgebra over S2 st the Sorts of A1 tolerates the Sorts of A2 holds

A1 +* A2 is finite-yielding

proof end;

theorem :: CIRCCOMB:25

for S1, S2 being non empty ManySortedSign

for A1 being non-empty MSAlgebra over S1

for s1 being Element of product the Sorts of A1

for A2 being non-empty MSAlgebra over S2

for s2 being Element of product the Sorts of A2 st the Sorts of A1 tolerates the Sorts of A2 holds

s1 +* s2 in product the Sorts of (A1 +* A2)

for A1 being non-empty MSAlgebra over S1

for s1 being Element of product the Sorts of A1

for A2 being non-empty MSAlgebra over S2

for s2 being Element of product the Sorts of A2 st the Sorts of A1 tolerates the Sorts of A2 holds

s1 +* s2 in product the Sorts of (A1 +* A2)

proof end;

theorem :: CIRCCOMB:26

for S1, S2 being non empty ManySortedSign

for A1 being non-empty MSAlgebra over S1

for A2 being non-empty MSAlgebra over S2 st the Sorts of A1 tolerates the Sorts of A2 holds

for s being Element of product the Sorts of (A1 +* A2) holds

( s | the carrier of S1 in product the Sorts of A1 & s | the carrier of S2 in product the Sorts of A2 )

for A1 being non-empty MSAlgebra over S1

for A2 being non-empty MSAlgebra over S2 st the Sorts of A1 tolerates the Sorts of A2 holds

for s being Element of product the Sorts of (A1 +* A2) holds

( s | the carrier of S1 in product the Sorts of A1 & s | the carrier of S2 in product the Sorts of A2 )

proof end;

theorem Th27: :: CIRCCOMB:27

for S1, S2 being non empty non void ManySortedSign

for A1 being non-empty MSAlgebra over S1

for A2 being non-empty MSAlgebra over S2 st the Sorts of A1 tolerates the Sorts of A2 holds

for o being OperSymbol of (S1 +* S2)

for o2 being OperSymbol of S2 st o = o2 holds

Den (o,(A1 +* A2)) = Den (o2,A2)

for A1 being non-empty MSAlgebra over S1

for A2 being non-empty MSAlgebra over S2 st the Sorts of A1 tolerates the Sorts of A2 holds

for o being OperSymbol of (S1 +* S2)

for o2 being OperSymbol of S2 st o = o2 holds

Den (o,(A1 +* A2)) = Den (o2,A2)

proof end;

theorem Th28: :: CIRCCOMB:28

for S1, S2 being non empty non void ManySortedSign

for A1 being non-empty MSAlgebra over S1

for A2 being non-empty MSAlgebra over S2 st the Sorts of A1 tolerates the Sorts of A2 & the Charact of A1 tolerates the Charact of A2 holds

for o being OperSymbol of (S1 +* S2)

for o1 being OperSymbol of S1 st o = o1 holds

Den (o,(A1 +* A2)) = Den (o1,A1)

for A1 being non-empty MSAlgebra over S1

for A2 being non-empty MSAlgebra over S2 st the Sorts of A1 tolerates the Sorts of A2 & the Charact of A1 tolerates the Charact of A2 holds

for o being OperSymbol of (S1 +* S2)

for o1 being OperSymbol of S1 st o = o1 holds

Den (o,(A1 +* A2)) = Den (o1,A1)

proof end;

theorem Th29: :: CIRCCOMB:29

for S1, S2, S being non empty non void Circuit-like ManySortedSign st S = S1 +* S2 holds

for A1 being non-empty Circuit of S1

for A2 being non-empty Circuit of S2

for A being non-empty Circuit of S

for s being State of A

for s2 being State of A2 st s2 = s | the carrier of S2 holds

for g being Gate of S

for g2 being Gate of S2 st g = g2 holds

g depends_on_in s = g2 depends_on_in s2

for A1 being non-empty Circuit of S1

for A2 being non-empty Circuit of S2

for A being non-empty Circuit of S

for s being State of A

for s2 being State of A2 st s2 = s | the carrier of S2 holds

for g being Gate of S

for g2 being Gate of S2 st g = g2 holds

g depends_on_in s = g2 depends_on_in s2

proof end;

theorem Th30: :: CIRCCOMB:30

for S1, S2, S being non empty non void Circuit-like ManySortedSign st S = S1 +* S2 & S1 tolerates S2 holds

for A1 being non-empty Circuit of S1

for A2 being non-empty Circuit of S2

for A being non-empty Circuit of S

for s being State of A

for s1 being State of A1 st s1 = s | the carrier of S1 holds

for g being Gate of S

for g1 being Gate of S1 st g = g1 holds

g depends_on_in s = g1 depends_on_in s1

for A1 being non-empty Circuit of S1

for A2 being non-empty Circuit of S2

for A being non-empty Circuit of S

for s being State of A

for s1 being State of A1 st s1 = s | the carrier of S1 holds

for g being Gate of S

for g1 being Gate of S1 st g = g1 holds

g depends_on_in s = g1 depends_on_in s1

proof end;

theorem Th31: :: CIRCCOMB:31

for S1, S2, S being non empty non void Circuit-like ManySortedSign st S = S1 +* S2 holds

for A1 being non-empty Circuit of S1

for A2 being non-empty Circuit of S2

for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds

for s being State of A

for v being Vertex of S holds

( ( for s1 being State of A1 st s1 = s | the carrier of S1 & ( v in InnerVertices S1 or ( v in the carrier of S1 & v in InputVertices S ) ) holds

(Following s) . v = (Following s1) . v ) & ( for s2 being State of A2 st s2 = s | the carrier of S2 & ( v in InnerVertices S2 or ( v in the carrier of S2 & v in InputVertices S ) ) holds

(Following s) . v = (Following s2) . v ) )

for A1 being non-empty Circuit of S1

for A2 being non-empty Circuit of S2

for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds

for s being State of A

for v being Vertex of S holds

( ( for s1 being State of A1 st s1 = s | the carrier of S1 & ( v in InnerVertices S1 or ( v in the carrier of S1 & v in InputVertices S ) ) holds

(Following s) . v = (Following s1) . v ) & ( for s2 being State of A2 st s2 = s | the carrier of S2 & ( v in InnerVertices S2 or ( v in the carrier of S2 & v in InputVertices S ) ) holds

(Following s) . v = (Following s2) . v ) )

proof end;

theorem Th32: :: CIRCCOMB:32

for S1, S2, S being non empty non void Circuit-like ManySortedSign st InnerVertices S1 misses InputVertices S2 & S = S1 +* S2 holds

for A1 being non-empty Circuit of S1

for A2 being non-empty Circuit of S2

for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds

for s being State of A

for s1 being State of A1

for s2 being State of A2 st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 holds

Following s = (Following s1) +* (Following s2)

for A1 being non-empty Circuit of S1

for A2 being non-empty Circuit of S2

for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds

for s being State of A

for s1 being State of A1

for s2 being State of A2 st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 holds

Following s = (Following s1) +* (Following s2)

proof end;

theorem Th33: :: CIRCCOMB:33

for S1, S2, S being non empty non void Circuit-like ManySortedSign st InnerVertices S2 misses InputVertices S1 & S = S1 +* S2 holds

for A1 being non-empty Circuit of S1

for A2 being non-empty Circuit of S2

for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds

for s being State of A

for s1 being State of A1

for s2 being State of A2 st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 holds

Following s = (Following s2) +* (Following s1)

for A1 being non-empty Circuit of S1

for A2 being non-empty Circuit of S2

for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds

for s being State of A

for s1 being State of A1

for s2 being State of A2 st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 holds

Following s = (Following s2) +* (Following s1)

proof end;

theorem :: CIRCCOMB:34

for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S1 c= InputVertices S2 & S = S1 +* S2 holds

for A1 being non-empty Circuit of S1

for A2 being non-empty Circuit of S2

for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds

for s being State of A

for s1 being State of A1

for s2 being State of A2 st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 holds

Following s = (Following s2) +* (Following s1)

for A1 being non-empty Circuit of S1

for A2 being non-empty Circuit of S2

for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds

for s being State of A

for s1 being State of A1

for s2 being State of A2 st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 holds

Following s = (Following s2) +* (Following s1)

proof end;

theorem :: CIRCCOMB:35

for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S2 c= InputVertices S1 & S = S1 +* S2 holds

for A1 being non-empty Circuit of S1

for A2 being non-empty Circuit of S2

for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds

for s being State of A

for s1 being State of A1

for s2 being State of A2 st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 holds

Following s = (Following s1) +* (Following s2)

for A1 being non-empty Circuit of S1

for A2 being non-empty Circuit of S2

for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds

for s being State of A

for s1 being State of A1

for s2 being State of A2 st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 holds

Following s = (Following s1) +* (Following s2)

proof end;

begin

definition

let f be set ;

let p be FinSequence;

let x be set ;

ex b_{1} being non void strict ManySortedSign st

( the carrier of b_{1} = (rng p) \/ {x} & the carrier' of b_{1} = {[p,f]} & the Arity of b_{1} . [p,f] = p & the ResultSort of b_{1} . [p,f] = x )

for b_{1}, b_{2} being non void strict ManySortedSign st the carrier of b_{1} = (rng p) \/ {x} & the carrier' of b_{1} = {[p,f]} & the Arity of b_{1} . [p,f] = p & the ResultSort of b_{1} . [p,f] = x & the carrier of b_{2} = (rng p) \/ {x} & the carrier' of b_{2} = {[p,f]} & the Arity of b_{2} . [p,f] = p & the ResultSort of b_{2} . [p,f] = x holds

b_{1} = b_{2}

end;
let p be FinSequence;

let x be set ;

func 1GateCircStr (p,f,x) -> non void strict ManySortedSign means :Def5: :: CIRCCOMB:def 5

( the carrier of it = (rng p) \/ {x} & the carrier' of it = {[p,f]} & the Arity of it . [p,f] = p & the ResultSort of it . [p,f] = x );

existence ( the carrier of it = (rng p) \/ {x} & the carrier' of it = {[p,f]} & the Arity of it . [p,f] = p & the ResultSort of it . [p,f] = x );

ex b

( the carrier of b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines 1GateCircStr CIRCCOMB:def 5 :

for f being set

for p being FinSequence

for x being set

for b_{4} being non void strict ManySortedSign holds

( b_{4} = 1GateCircStr (p,f,x) iff ( the carrier of b_{4} = (rng p) \/ {x} & the carrier' of b_{4} = {[p,f]} & the Arity of b_{4} . [p,f] = p & the ResultSort of b_{4} . [p,f] = x ) );

for f being set

for p being FinSequence

for x being set

for b

( b

registration

let f be set ;

let p be FinSequence;

let x be set ;

coherence

not 1GateCircStr (p,f,x) is empty

end;
let p be FinSequence;

let x be set ;

coherence

not 1GateCircStr (p,f,x) is empty

proof end;

theorem Th36: :: CIRCCOMB:36

for f, x being set

for p being FinSequence holds

( the Arity of (1GateCircStr (p,f,x)) = (p,f) .--> p & the ResultSort of (1GateCircStr (p,f,x)) = (p,f) .--> x )

for p being FinSequence holds

( the Arity of (1GateCircStr (p,f,x)) = (p,f) .--> p & the ResultSort of (1GateCircStr (p,f,x)) = (p,f) .--> x )

proof end;

theorem :: CIRCCOMB:37

for f, x being set

for p being FinSequence

for g being Gate of (1GateCircStr (p,f,x)) holds

( g = [p,f] & the_arity_of g = p & the_result_sort_of g = x )

for p being FinSequence

for g being Gate of (1GateCircStr (p,f,x)) holds

( g = [p,f] & the_arity_of g = p & the_result_sort_of g = x )

proof end;

theorem :: CIRCCOMB:38

for f, x being set

for p being FinSequence holds

( InputVertices (1GateCircStr (p,f,x)) = (rng p) \ {x} & InnerVertices (1GateCircStr (p,f,x)) = {x} )

for p being FinSequence holds

( InputVertices (1GateCircStr (p,f,x)) = (rng p) \ {x} & InnerVertices (1GateCircStr (p,f,x)) = {x} )

proof end;

definition

let f be set ;

let p be FinSequence;

ex b_{1} being non void strict ManySortedSign st

( the carrier of b_{1} = (rng p) \/ {[p,f]} & the carrier' of b_{1} = {[p,f]} & the Arity of b_{1} . [p,f] = p & the ResultSort of b_{1} . [p,f] = [p,f] )

for b_{1}, b_{2} being non void strict ManySortedSign st the carrier of b_{1} = (rng p) \/ {[p,f]} & the carrier' of b_{1} = {[p,f]} & the Arity of b_{1} . [p,f] = p & the ResultSort of b_{1} . [p,f] = [p,f] & the carrier of b_{2} = (rng p) \/ {[p,f]} & the carrier' of b_{2} = {[p,f]} & the Arity of b_{2} . [p,f] = p & the ResultSort of b_{2} . [p,f] = [p,f] holds

b_{1} = b_{2}

end;
let p be FinSequence;

func 1GateCircStr (p,f) -> non void strict ManySortedSign means :Def6: :: CIRCCOMB:def 6

( the carrier of it = (rng p) \/ {[p,f]} & the carrier' of it = {[p,f]} & the Arity of it . [p,f] = p & the ResultSort of it . [p,f] = [p,f] );

existence ( the carrier of it = (rng p) \/ {[p,f]} & the carrier' of it = {[p,f]} & the Arity of it . [p,f] = p & the ResultSort of it . [p,f] = [p,f] );

ex b

( the carrier of b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines 1GateCircStr CIRCCOMB:def 6 :

for f being set

for p being FinSequence

for b_{3} being non void strict ManySortedSign holds

( b_{3} = 1GateCircStr (p,f) iff ( the carrier of b_{3} = (rng p) \/ {[p,f]} & the carrier' of b_{3} = {[p,f]} & the Arity of b_{3} . [p,f] = p & the ResultSort of b_{3} . [p,f] = [p,f] ) );

for f being set

for p being FinSequence

for b

( b

registration
end;

theorem Th40: :: CIRCCOMB:40

for f being set

for p being FinSequence holds

( the Arity of (1GateCircStr (p,f)) = (p,f) .--> p & the ResultSort of (1GateCircStr (p,f)) = (p,f) .--> [p,f] )

for p being FinSequence holds

( the Arity of (1GateCircStr (p,f)) = (p,f) .--> p & the ResultSort of (1GateCircStr (p,f)) = (p,f) .--> [p,f] )

proof end;

theorem Th41: :: CIRCCOMB:41

for f being set

for p being FinSequence

for g being Gate of (1GateCircStr (p,f)) holds

( g = [p,f] & the_arity_of g = p & the_result_sort_of g = g )

for p being FinSequence

for g being Gate of (1GateCircStr (p,f)) holds

( g = [p,f] & the_arity_of g = p & the_result_sort_of g = g )

proof end;

theorem Th42: :: CIRCCOMB:42

for f being set

for p being FinSequence holds

( InputVertices (1GateCircStr (p,f)) = rng p & InnerVertices (1GateCircStr (p,f)) = {[p,f]} )

for p being FinSequence holds

( InputVertices (1GateCircStr (p,f)) = rng p & InnerVertices (1GateCircStr (p,f)) = {[p,f]} )

proof end;

begin

definition

let IT be ManySortedSign ;

end;
attr IT is gate`1=arity means :Def8: :: CIRCCOMB:def 8

for g being set st g in the carrier' of IT holds

g = [( the Arity of IT . g),(g `2)];

for g being set st g in the carrier' of IT holds

g = [( the Arity of IT . g),(g `2)];

attr IT is gate`2isBoolean means :Def9: :: CIRCCOMB:def 9

for g being set st g in the carrier' of IT holds

for p being FinSequence st p = the Arity of IT . g holds

ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f];

for g being set st g in the carrier' of IT holds

for p being FinSequence st p = the Arity of IT . g holds

ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f];

:: deftheorem Def7 defines unsplit CIRCCOMB:def 7 :

for IT being ManySortedSign holds

( IT is unsplit iff the ResultSort of IT = id the carrier' of IT );

for IT being ManySortedSign holds

( IT is unsplit iff the ResultSort of IT = id the carrier' of IT );

:: deftheorem Def8 defines gate`1=arity CIRCCOMB:def 8 :

for IT being ManySortedSign holds

( IT is gate`1=arity iff for g being set st g in the carrier' of IT holds

g = [( the Arity of IT . g),(g `2)] );

for IT being ManySortedSign holds

( IT is gate`1=arity iff for g being set st g in the carrier' of IT holds

g = [( the Arity of IT . g),(g `2)] );

:: deftheorem Def9 defines gate`2isBoolean CIRCCOMB:def 9 :

for IT being ManySortedSign holds

( IT is gate`2isBoolean iff for g being set st g in the carrier' of IT holds

for p being FinSequence st p = the Arity of IT . g holds

ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f] );

for IT being ManySortedSign holds

( IT is gate`2isBoolean iff for g being set st g in the carrier' of IT holds

for p being FinSequence st p = the Arity of IT . g holds

ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f] );

:: deftheorem Def10 defines gate`2=den CIRCCOMB:def 10 :

for S being non empty ManySortedSign

for IT being MSAlgebra over S holds

( IT is gate`2=den iff for g being set st g in the carrier' of S holds

g = [(g `1),( the Charact of IT . g)] );

for S being non empty ManySortedSign

for IT being MSAlgebra over S holds

( IT is gate`2=den iff for g being set st g in the carrier' of S holds

g = [(g `1),( the Charact of IT . g)] );

:: deftheorem defines gate`2=den CIRCCOMB:def 11 :

for IT being non empty ManySortedSign holds

( IT is gate`2=den iff ex A being MSAlgebra over IT st A is gate`2=den );

for IT being non empty ManySortedSign holds

( IT is gate`2=den iff ex A being MSAlgebra over IT st A is gate`2=den );

scheme :: CIRCCOMB:sch 2

Lemma{ F_{1}() -> non empty ManySortedSign , F_{2}( set , set ) -> set } :

Lemma{ F

ex A being strict MSAlgebra over F_{1}() st

( the Sorts of A = the carrier of F_{1}() --> BOOLEAN & ( for g being set

for p being Element of the carrier of F_{1}() * st g in the carrier' of F_{1}() & p = the Arity of F_{1}() . g holds

the Charact of A . g = F_{2}(g,p) ) )

provided( the Sorts of A = the carrier of F

for p being Element of the carrier of F

the Charact of A . g = F

A1:
for g being set

for p being Element of the carrier of F_{1}() * st g in the carrier' of F_{1}() & p = the Arity of F_{1}() . g holds

F_{2}(g,p) is Function of ((len p) -tuples_on BOOLEAN),BOOLEAN

for p being Element of the carrier of F

F

proof end;

registration

coherence

for b_{1} being non empty ManySortedSign st b_{1} is gate`2isBoolean holds

b_{1} is gate`2=den

end;
for b

b

proof end;

theorem Th44: :: CIRCCOMB:44

for S being non empty ManySortedSign holds

( S is unsplit iff for o being set st o in the carrier' of S holds

the ResultSort of S . o = o )

( S is unsplit iff for o being set st o in the carrier' of S holds

the ResultSort of S . o = o )

proof end;

registration

coherence

for b_{1} being non empty ManySortedSign st b_{1} is unsplit holds

b_{1} is Circuit-like

end;
for b

b

proof end;

theorem Th46: :: CIRCCOMB:46

for f being set

for p being FinSequence holds

( 1GateCircStr (p,f) is unsplit & 1GateCircStr (p,f) is gate`1=arity )

for p being FinSequence holds

( 1GateCircStr (p,f) is unsplit & 1GateCircStr (p,f) is gate`1=arity )

proof end;

registration

let f be set ;

let p be FinSequence;

coherence

( 1GateCircStr (p,f) is unsplit & 1GateCircStr (p,f) is gate`1=arity ) by Th46;

end;
let p be FinSequence;

coherence

( 1GateCircStr (p,f) is unsplit & 1GateCircStr (p,f) is gate`1=arity ) by Th46;

registration

existence

ex b_{1} being ManySortedSign st

( b_{1} is unsplit & b_{1} is gate`1=arity & not b_{1} is void & b_{1} is strict & not b_{1} is empty )

end;
ex b

( b

proof end;

theorem Th48: :: CIRCCOMB:48

for S1, S2 being non empty ManySortedSign

for A1 being MSAlgebra over S1

for A2 being MSAlgebra over S2 st A1 is gate`2=den & A2 is gate`2=den holds

the Charact of A1 tolerates the Charact of A2

for A1 being MSAlgebra over S1

for A2 being MSAlgebra over S2 st A1 is gate`2=den & A2 is gate`2=den holds

the Charact of A1 tolerates the Charact of A2

proof end;

registration
end;

registration
end;

theorem Th51: :: CIRCCOMB:51

for S1, S2 being non empty ManySortedSign st S1 is gate`2isBoolean & S2 is gate`2isBoolean holds

S1 +* S2 is gate`2isBoolean

S1 +* S2 is gate`2isBoolean

proof end;

begin

definition

let n be Nat;

let X, Y be non empty set ;

let f be Function of (n -tuples_on X),Y;

let p be FinSeqLen of n;

let x be set ;

assume B1: ( x in rng p implies X = Y ) ;

ex b_{1} being strict non-empty MSAlgebra over 1GateCircStr (p,f,x) st

( the Sorts of b_{1} = ((rng p) --> X) +* (x .--> Y) & the Charact of b_{1} . [p,f] = f )

for b_{1}, b_{2} being strict non-empty MSAlgebra over 1GateCircStr (p,f,x) st the Sorts of b_{1} = ((rng p) --> X) +* (x .--> Y) & the Charact of b_{1} . [p,f] = f & the Sorts of b_{2} = ((rng p) --> X) +* (x .--> Y) & the Charact of b_{2} . [p,f] = f holds

b_{1} = b_{2}

end;
let X, Y be non empty set ;

let f be Function of (n -tuples_on X),Y;

let p be FinSeqLen of n;

let x be set ;

assume B1: ( x in rng p implies X = Y ) ;

func 1GateCircuit (p,f,x) -> strict non-empty MSAlgebra over 1GateCircStr (p,f,x) means :: CIRCCOMB:def 12

( the Sorts of it = ((rng p) --> X) +* (x .--> Y) & the Charact of it . [p,f] = f );

existence ( the Sorts of it = ((rng p) --> X) +* (x .--> Y) & the Charact of it . [p,f] = f );

ex b

( the Sorts of b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines 1GateCircuit CIRCCOMB:def 12 :

for n being Nat

for X, Y being non empty set

for f being Function of (n -tuples_on X),Y

for p being FinSeqLen of n

for x being set st ( x in rng p implies X = Y ) holds

for b_{7} being strict non-empty MSAlgebra over 1GateCircStr (p,f,x) holds

( b_{7} = 1GateCircuit (p,f,x) iff ( the Sorts of b_{7} = ((rng p) --> X) +* (x .--> Y) & the Charact of b_{7} . [p,f] = f ) );

for n being Nat

for X, Y being non empty set

for f being Function of (n -tuples_on X),Y

for p being FinSeqLen of n

for x being set st ( x in rng p implies X = Y ) holds

for b

( b

definition

let n be Nat;

let X be non empty set ;

let f be Function of (n -tuples_on X),X;

let p be FinSeqLen of n;

ex b_{1} being strict non-empty MSAlgebra over 1GateCircStr (p,f) st

( the Sorts of b_{1} = the carrier of (1GateCircStr (p,f)) --> X & the Charact of b_{1} . [p,f] = f )

for b_{1}, b_{2} being strict non-empty MSAlgebra over 1GateCircStr (p,f) st the Sorts of b_{1} = the carrier of (1GateCircStr (p,f)) --> X & the Charact of b_{1} . [p,f] = f & the Sorts of b_{2} = the carrier of (1GateCircStr (p,f)) --> X & the Charact of b_{2} . [p,f] = f holds

b_{1} = b_{2}

end;
let X be non empty set ;

let f be Function of (n -tuples_on X),X;

let p be FinSeqLen of n;

func 1GateCircuit (p,f) -> strict non-empty MSAlgebra over 1GateCircStr (p,f) means :Def13: :: CIRCCOMB:def 13

( the Sorts of it = the carrier of (1GateCircStr (p,f)) --> X & the Charact of it . [p,f] = f );

existence ( the Sorts of it = the carrier of (1GateCircStr (p,f)) --> X & the Charact of it . [p,f] = f );

ex b

( the Sorts of b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def13 defines 1GateCircuit CIRCCOMB:def 13 :

for n being Nat

for X being non empty set

for f being Function of (n -tuples_on X),X

for p being FinSeqLen of n

for b_{5} being strict non-empty MSAlgebra over 1GateCircStr (p,f) holds

( b_{5} = 1GateCircuit (p,f) iff ( the Sorts of b_{5} = the carrier of (1GateCircStr (p,f)) --> X & the Charact of b_{5} . [p,f] = f ) );

for n being Nat

for X being non empty set

for f being Function of (n -tuples_on X),X

for p being FinSeqLen of n

for b

( b

theorem Th52: :: CIRCCOMB:52

for n being Nat

for X being non empty set

for f being Function of (n -tuples_on X),X

for p being FinSeqLen of n holds

( 1GateCircuit (p,f) is gate`2=den & 1GateCircStr (p,f) is gate`2=den )

for X being non empty set

for f being Function of (n -tuples_on X),X

for p being FinSeqLen of n holds

( 1GateCircuit (p,f) is gate`2=den & 1GateCircStr (p,f) is gate`2=den )

proof end;

registration

let n be Nat;

let X be non empty set ;

let f be Function of (n -tuples_on X),X;

let p be FinSeqLen of n;

coherence

1GateCircuit (p,f) is gate`2=den by Th52;

coherence

1GateCircStr (p,f) is gate`2=den by Th52;

end;
let X be non empty set ;

let f be Function of (n -tuples_on X),X;

let p be FinSeqLen of n;

coherence

1GateCircuit (p,f) is gate`2=den by Th52;

coherence

1GateCircStr (p,f) is gate`2=den by Th52;

theorem Th53: :: CIRCCOMB:53

for n being Nat

for p being FinSeqLen of n

for f being Function of (n -tuples_on BOOLEAN),BOOLEAN holds 1GateCircStr (p,f) is gate`2isBoolean

for p being FinSeqLen of n

for f being Function of (n -tuples_on BOOLEAN),BOOLEAN holds 1GateCircStr (p,f) is gate`2isBoolean

proof end;

registration

let n be Nat;

let f be Function of (n -tuples_on BOOLEAN),BOOLEAN;

let p be FinSeqLen of n;

coherence

1GateCircStr (p,f) is gate`2isBoolean by Th53;

end;
let f be Function of (n -tuples_on BOOLEAN),BOOLEAN;

let p be FinSeqLen of n;

coherence

1GateCircStr (p,f) is gate`2isBoolean by Th53;

registration

existence

ex b_{1} being ManySortedSign st

( b_{1} is gate`2isBoolean & not b_{1} is empty )

end;
ex b

( b

proof end;

registration

let S1, S2 be non empty gate`2isBoolean ManySortedSign ;

coherence

S1 +* S2 is gate`2isBoolean by Th51;

end;
coherence

S1 +* S2 is gate`2isBoolean by Th51;

theorem Th54: :: CIRCCOMB:54

for n being Nat

for X being non empty set

for f being Function of (n -tuples_on X),X

for p being FinSeqLen of n holds

( the Charact of (1GateCircuit (p,f)) = (p,f) .--> f & ( for v being Vertex of (1GateCircStr (p,f)) holds the Sorts of (1GateCircuit (p,f)) . v = X ) )

for X being non empty set

for f being Function of (n -tuples_on X),X

for p being FinSeqLen of n holds

( the Charact of (1GateCircuit (p,f)) = (p,f) .--> f & ( for v being Vertex of (1GateCircStr (p,f)) holds the Sorts of (1GateCircuit (p,f)) . v = X ) )

proof end;

registration

let n be Nat;

let X be non empty finite set ;

let f be Function of (n -tuples_on X),X;

let p be FinSeqLen of n;

coherence

1GateCircuit (p,f) is finite-yielding

end;
let X be non empty finite set ;

let f be Function of (n -tuples_on X),X;

let p be FinSeqLen of n;

coherence

1GateCircuit (p,f) is finite-yielding

proof end;

theorem :: CIRCCOMB:55

for n being Nat

for X being non empty set

for f being Function of (n -tuples_on X),X

for p, q being FinSeqLen of n holds 1GateCircuit (p,f) tolerates 1GateCircuit (q,f)

for X being non empty set

for f being Function of (n -tuples_on X),X

for p, q being FinSeqLen of n holds 1GateCircuit (p,f) tolerates 1GateCircuit (q,f)

proof end;

theorem :: CIRCCOMB:56

for n being Nat

for X being non empty finite set

for f being Function of (n -tuples_on X),X

for p being FinSeqLen of n

for s being State of (1GateCircuit (p,f)) holds (Following s) . [p,f] = f . (s * p)

for X being non empty finite set

for f being Function of (n -tuples_on X),X

for p being FinSeqLen of n

for s being State of (1GateCircuit (p,f)) holds (Following s) . [p,f] = f . (s * p)

proof end;

begin

:: definition

:: redefine func BOOLEAN -> Subset of NAT;

:: coherence by MARGREL1:def 12,ZFMISC_1:38;

:: end;

:: redefine func BOOLEAN -> Subset of NAT;

:: coherence by MARGREL1:def 12,ZFMISC_1:38;

:: end;

:: deftheorem Def14 defines Boolean CIRCCOMB:def 14 :

for S being non empty ManySortedSign

for IT being MSAlgebra over S holds

( IT is Boolean iff for v being Vertex of S holds the Sorts of IT . v = BOOLEAN );

for S being non empty ManySortedSign

for IT being MSAlgebra over S holds

( IT is Boolean iff for v being Vertex of S holds the Sorts of IT . v = BOOLEAN );

theorem Th57: :: CIRCCOMB:57

for S being non empty ManySortedSign

for A being MSAlgebra over S holds

( A is Boolean iff the Sorts of A = the carrier of S --> BOOLEAN )

for A being MSAlgebra over S holds

( A is Boolean iff the Sorts of A = the carrier of S --> BOOLEAN )

proof end;

registration

let S be non empty ManySortedSign ;

coherence

for b_{1} being MSAlgebra over S st b_{1} is Boolean holds

( b_{1} is non-empty & b_{1} is finite-yielding )

end;
coherence

for b

( b

proof end;

theorem :: CIRCCOMB:58

for S being non empty ManySortedSign

for A being MSAlgebra over S holds

( A is Boolean iff rng the Sorts of A c= {BOOLEAN} )

for A being MSAlgebra over S holds

( A is Boolean iff rng the Sorts of A c= {BOOLEAN} )

proof end;

theorem Th59: :: CIRCCOMB:59

for S1, S2 being non empty ManySortedSign

for A1 being MSAlgebra over S1

for A2 being MSAlgebra over S2 st A1 is Boolean & A2 is Boolean holds

the Sorts of A1 tolerates the Sorts of A2

for A1 being MSAlgebra over S1

for A2 being MSAlgebra over S2 st A1 is Boolean & A2 is Boolean holds

the Sorts of A1 tolerates the Sorts of A2

proof end;

theorem Th60: :: CIRCCOMB:60

for S1, S2 being non empty unsplit gate`1=arity ManySortedSign

for A1 being MSAlgebra over S1

for A2 being MSAlgebra over S2 st A1 is Boolean & A1 is gate`2=den & A2 is Boolean & A2 is gate`2=den holds

A1 tolerates A2

for A1 being MSAlgebra over S1

for A2 being MSAlgebra over S2 st A1 is Boolean & A1 is gate`2=den & A2 is Boolean & A2 is gate`2=den holds

A1 tolerates A2

proof end;

registration

let S be non empty ManySortedSign ;

existence

ex b_{1} being strict MSAlgebra over S st b_{1} is Boolean

end;
existence

ex b

proof end;

theorem :: CIRCCOMB:61

for n being Nat

for f being Function of (n -tuples_on BOOLEAN),BOOLEAN

for p being FinSeqLen of n holds 1GateCircuit (p,f) is Boolean

for f being Function of (n -tuples_on BOOLEAN),BOOLEAN

for p being FinSeqLen of n holds 1GateCircuit (p,f) is Boolean

proof end;

theorem Th62: :: CIRCCOMB:62

for S1, S2 being non empty ManySortedSign

for A1 being Boolean MSAlgebra over S1

for A2 being Boolean MSAlgebra over S2 holds A1 +* A2 is Boolean

for A1 being Boolean MSAlgebra over S1

for A2 being Boolean MSAlgebra over S2 holds A1 +* A2 is Boolean

proof end;

theorem Th63: :: CIRCCOMB:63

for S1, S2 being non empty ManySortedSign

for A1 being non-empty MSAlgebra over S1

for A2 being non-empty MSAlgebra over S2 st A1 is gate`2=den & A2 is gate`2=den & the Sorts of A1 tolerates the Sorts of A2 holds

A1 +* A2 is gate`2=den

for A1 being non-empty MSAlgebra over S1

for A2 being non-empty MSAlgebra over S2 st A1 is gate`2=den & A2 is gate`2=den & the Sorts of A1 tolerates the Sorts of A2 holds

A1 +* A2 is gate`2=den

proof end;

registration

ex b_{1} being non empty ManySortedSign st

( b_{1} is unsplit & b_{1} is gate`1=arity & b_{1} is gate`2=den & b_{1} is gate`2isBoolean & not b_{1} is void & b_{1} is strict )
end;

cluster non empty non void V65() strict unsplit gate`1=arity gate`2isBoolean gate`2=den for ManySortedSign ;

existence ex b

( b

proof end;

registration

let S be non empty gate`2isBoolean ManySortedSign ;

existence

ex b_{1} being strict MSAlgebra over S st

( b_{1} is Boolean & b_{1} is gate`2=den )

end;
existence

ex b

( b

proof end;

registration

let S1, S2 be non empty non void unsplit gate`2isBoolean ManySortedSign ;

let A1 be gate`2=den Boolean Circuit of S1;

let A2 be gate`2=den Boolean Circuit of S2;

coherence

( A1 +* A2 is Boolean & A1 +* A2 is gate`2=den )

end;
let A1 be gate`2=den Boolean Circuit of S1;

let A2 be gate`2=den Boolean Circuit of S2;

coherence

( A1 +* A2 is Boolean & A1 +* A2 is gate`2=den )

proof end;

registration

let n be Nat;

let X be non empty finite set ;

let f be Function of (n -tuples_on X),X;

let p be FinSeqLen of n;

existence

ex b_{1} being Circuit of 1GateCircStr (p,f) st

( b_{1} is gate`2=den & b_{1} is strict & b_{1} is non-empty )

end;
let X be non empty finite set ;

let f be Function of (n -tuples_on X),X;

let p be FinSeqLen of n;

existence

ex b

( b

proof end;

registration

let n be Nat;

let X be non empty finite set ;

let f be Function of (n -tuples_on X),X;

let p be FinSeqLen of n;

coherence

1GateCircuit (p,f) is gate`2=den ;

end;
let X be non empty finite set ;

let f be Function of (n -tuples_on X),X;

let p be FinSeqLen of n;

coherence

1GateCircuit (p,f) is gate`2=den ;

theorem :: CIRCCOMB:64

for S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign

for A1 being gate`2=den Boolean Circuit of S1

for A2 being gate`2=den Boolean Circuit of S2

for s being State of (A1 +* A2)

for v being Vertex of (S1 +* S2) holds

( ( for s1 being State of A1 st s1 = s | the carrier of S1 & ( v in InnerVertices S1 or ( v in the carrier of S1 & v in InputVertices (S1 +* S2) ) ) holds

(Following s) . v = (Following s1) . v ) & ( for s2 being State of A2 st s2 = s | the carrier of S2 & ( v in InnerVertices S2 or ( v in the carrier of S2 & v in InputVertices (S1 +* S2) ) ) holds

(Following s) . v = (Following s2) . v ) )

for A1 being gate`2=den Boolean Circuit of S1

for A2 being gate`2=den Boolean Circuit of S2

for s being State of (A1 +* A2)

for v being Vertex of (S1 +* S2) holds

( ( for s1 being State of A1 st s1 = s | the carrier of S1 & ( v in InnerVertices S1 or ( v in the carrier of S1 & v in InputVertices (S1 +* S2) ) ) holds

(Following s) . v = (Following s1) . v ) & ( for s2 being State of A2 st s2 = s | the carrier of S2 & ( v in InnerVertices S2 or ( v in the carrier of S2 & v in InputVertices (S1 +* S2) ) ) holds

(Following s) . v = (Following s2) . v ) )

proof end;

:: for S1,S2 being monotonic (non void ManySortedSign) st

:: InputVertices S1 misses InnerVertices S2 or

:: InputVertices S2 misses InnerVertices S1

:: holds S1+*S2 is monotonic;