:: by Yatsuka Nakamura and Grzegorz Bancerek

::

:: Received May 11, 1995

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

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;

definition
end;

:: deftheorem 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 :: CIRCCOMB:18

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;

definition

let f be object ;

let p be FinSequence;

let x be object ;

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

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 object

for p being FinSequence

for x being object

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 object

for p being FinSequence

for x being object

for b

( b

registration

let f be object ;

let p be FinSequence;

let x be object ;

coherence

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

end;
let p be FinSequence;

let x be object ;

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

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 object

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 object

for p being FinSequence

for b

( b

registration
end;

theorem Th40: :: CIRCCOMB:40

for f being object

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 object

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;

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

MSSLambdaWeak{ F_{1}() -> set , F_{2}() -> set , F_{3}() -> Function of F_{1}(),F_{2}(), F_{4}( object , object ) -> object } :

MSSLambdaWeak{ F

ex f being ManySortedSet of F_{1}() st

for a being set

for b being Element of F_{2}() st a in F_{1}() & b = F_{3}() . a holds

f . a = F_{4}(a,b)

for a being set

for b being Element of F

f . a = F

proof end;

scheme :: CIRCCOMB:sch 2

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

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 object st o in the carrier' of S holds

the ResultSort of S . o = o )

( S is unsplit iff for o being object 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 object

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

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;

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 A1: ( 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 A1: ( 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;

:: 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 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 by Th47, Th48, Th59;

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 by Th47, Th48, Th59;

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