:: Full Adder Circuit. Part { I }
:: by Grzegorz Bancerek and Yatsuka Nakamura
::
:: Received August 10, 1995
:: Copyright (c) 1995-2012 Association of Mizar Users


begin

registration
cluster pair -> non empty for set ;
coherence
for b1 being set st b1 is pair holds
not b1 is empty
proof end;
end;

registration
cluster non pair for set ;
existence
not for b1 being set holds b1 is pair
proof end;
end;

registration
cluster V13() -> non pair for set ;
coherence
for b1 being Nat holds not b1 is pair
proof end;
end;

definition
canceled;
let IT be set ;
attr IT is with_pair means :Def2: :: FACIRC_1:def 2
ex x being pair set st x in IT;
end;

:: deftheorem FACIRC_1:def 1 :
canceled;

:: deftheorem Def2 defines with_pair FACIRC_1:def 2 :
for IT being set holds
( IT is with_pair iff ex x being pair set st x in IT );

notation
let IT be set ;
antonym without_pairs IT for with_pair ;
end;

registration
cluster empty -> without_pairs for set ;
coherence
for b1 being set st b1 is empty holds
b1 is without_pairs
proof end;
let x be non pair set ;
cluster {x} -> without_pairs ;
coherence
not {x} is with_pair
proof end;
let y be non pair set ;
cluster {x,y} -> without_pairs ;
coherence
not {x,y} is with_pair
proof end;
let z be non pair set ;
cluster {x,y,z} -> without_pairs ;
coherence
not {x,y,z} is with_pair
proof end;
end;

registration
cluster non empty without_pairs for set ;
existence
ex b1 being non empty set st b1 is without_pairs
proof end;
end;

registration
let X, Y be without_pairs set ;
cluster X \/ Y -> without_pairs ;
coherence
not X \/ Y is with_pair
proof end;
end;

registration
let X be without_pairs set ;
let Y be set ;
cluster X \ Y -> without_pairs ;
coherence
not X \ Y is with_pair
proof end;
cluster X /\ Y -> without_pairs ;
coherence
not X /\ Y is with_pair
proof end;
cluster Y /\ X -> without_pairs ;
coherence
not Y /\ X is with_pair
;
end;

registration
let x be pair set ;
cluster {x} -> Relation-like ;
coherence
{x} is Relation-like
proof end;
let y be pair set ;
cluster {x,y} -> Relation-like ;
coherence
{x,y} is Relation-like
proof end;
let z be pair set ;
cluster {x,y,z} -> Relation-like ;
coherence
{x,y,z} is Relation-like
proof end;
end;

registration
cluster Relation-like without_pairs -> empty for set ;
coherence
for b1 being set st b1 is without_pairs & b1 is Relation-like holds
b1 is empty
proof end;
end;

definition
let IT be Function;
attr IT is nonpair-yielding means :: FACIRC_1:def 3
for x being set st x in dom IT holds
not IT . x is pair ;
end;

:: deftheorem defines nonpair-yielding FACIRC_1:def 3 :
for IT being Function holds
( IT is nonpair-yielding iff for x being set st x in dom IT holds
not IT . x is pair );

registration
let x be non pair set ;
cluster <*x*> -> nonpair-yielding ;
coherence
<*x*> is nonpair-yielding
proof end;
let y be non pair set ;
cluster <*x,y*> -> nonpair-yielding ;
coherence
<*x,y*> is nonpair-yielding
proof end;
let z be non pair set ;
cluster <*x,y,z*> -> nonpair-yielding ;
coherence
<*x,y,z*> is nonpair-yielding
proof end;
end;

theorem Th1: :: FACIRC_1:1
for f being Function st f is nonpair-yielding holds
rng f is without_pairs
proof end;

registration
let n be Nat;
cluster Relation-like NAT -defined Function-like one-to-one finite V46(n) FinSequence-like FinSubsequence-like countable nonpair-yielding for set ;
existence
ex b1 being FinSeqLen of n st
( b1 is one-to-one & b1 is nonpair-yielding )
proof end;
end;

registration
cluster Relation-like NAT -defined Function-like one-to-one finite FinSequence-like FinSubsequence-like countable nonpair-yielding for set ;
existence
ex b1 being FinSequence st
( b1 is one-to-one & b1 is nonpair-yielding )
proof end;
end;

registration
let f be nonpair-yielding Function;
cluster proj2 f -> without_pairs ;
coherence
not rng f is with_pair
by Th1;
end;

theorem Th2: :: FACIRC_1:2
for S1, S2 being non empty ManySortedSign st S1 tolerates S2 & InnerVertices S1 is Relation & InnerVertices S2 is Relation holds
InnerVertices (S1 +* S2) is Relation
proof end;

theorem :: FACIRC_1:3
for S1, S2 being non empty unsplit gate`1=arity ManySortedSign st InnerVertices S1 is Relation & InnerVertices S2 is Relation holds
InnerVertices (S1 +* S2) is Relation by Th2, CIRCCOMB:47;

theorem Th4: :: FACIRC_1:4
for S1, S2 being non empty ManySortedSign st S1 tolerates S2 & InnerVertices S2 misses InputVertices S1 holds
( InputVertices S1 c= InputVertices (S1 +* S2) & InputVertices (S1 +* S2) = (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) )
proof end;

theorem Th5: :: FACIRC_1:5
for X, R being set st X is without_pairs & R is Relation holds
X misses R
proof end;

theorem Th6: :: FACIRC_1:6
for S1, S2 being non empty unsplit gate`1=arity ManySortedSign st InputVertices S1 is without_pairs & InnerVertices S2 is Relation holds
( InputVertices S1 c= InputVertices (S1 +* S2) & InputVertices (S1 +* S2) = (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) )
proof end;

theorem Th7: :: FACIRC_1:7
for S1, S2 being non empty unsplit gate`1=arity ManySortedSign st InputVertices S1 is without_pairs & InnerVertices S1 is Relation & InputVertices S2 is without_pairs & InnerVertices S2 is Relation holds
InputVertices (S1 +* S2) = (InputVertices S1) \/ (InputVertices S2)
proof end;

theorem Th8: :: FACIRC_1:8
for S1, S2 being non empty ManySortedSign st S1 tolerates S2 & InputVertices S1 is without_pairs & InputVertices S2 is without_pairs holds
InputVertices (S1 +* S2) is without_pairs
proof end;

theorem :: FACIRC_1:9
for S1, S2 being non empty unsplit gate`1=arity ManySortedSign st InputVertices S1 is without_pairs & InputVertices S2 is without_pairs holds
InputVertices (S1 +* S2) is without_pairs by Th8, CIRCCOMB:47;

begin

definition
let i be Nat;
let D be non empty set ;
mode Tuple of i,D is Element of i -tuples_on D;
end;

scheme :: FACIRC_1:sch 1
2AryBooleEx{ F1( set , set ) -> Element of BOOLEAN } :
ex f being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds f . <*x,y*> = F1(x,y)
proof end;

scheme :: FACIRC_1:sch 2
2AryBooleUniq{ F1( set , set ) -> Element of BOOLEAN } :
for f1, f2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds f1 . <*x,y*> = F1(x,y) ) & ( for x, y being Element of BOOLEAN holds f2 . <*x,y*> = F1(x,y) ) holds
f1 = f2
proof end;

scheme :: FACIRC_1:sch 3
2AryBooleDef{ F1( set , set ) -> Element of BOOLEAN } :
( ex f being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds f . <*x,y*> = F1(x,y) & ( for f1, f2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds f1 . <*x,y*> = F1(x,y) ) & ( for x, y being Element of BOOLEAN holds f2 . <*x,y*> = F1(x,y) ) holds
f1 = f2 ) )
proof end;

scheme :: FACIRC_1:sch 4
3AryBooleEx{ F1( set , set , set ) -> Element of BOOLEAN } :
ex f being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds f . <*x,y,z*> = F1(x,y,z)
proof end;

scheme :: FACIRC_1:sch 5
3AryBooleUniq{ F1( set , set , set ) -> Element of BOOLEAN } :
for f1, f2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds f1 . <*x,y,z*> = F1(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds f2 . <*x,y,z*> = F1(x,y,z) ) holds
f1 = f2
proof end;

scheme :: FACIRC_1:sch 6
3AryBooleDef{ F1( set , set , set ) -> Element of BOOLEAN } :
( ex f being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds f . <*x,y,z*> = F1(x,y,z) & ( for f1, f2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds f1 . <*x,y,z*> = F1(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds f2 . <*x,y,z*> = F1(x,y,z) ) holds
f1 = f2 ) )
proof end;

definition
func 'xor' -> Function of (2 -tuples_on BOOLEAN),BOOLEAN means :Def4: :: FACIRC_1:def 4
for x, y being Element of BOOLEAN holds it . <*x,y*> = x 'xor' y;
correctness
existence
ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'xor' y
;
uniqueness
for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'xor' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x 'xor' y ) holds
b1 = b2
;
proof end;
func 'or' -> Function of (2 -tuples_on BOOLEAN),BOOLEAN means :Def5: :: FACIRC_1:def 5
for x, y being Element of BOOLEAN holds it . <*x,y*> = x 'or' y;
correctness
existence
ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'or' y
;
uniqueness
for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'or' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x 'or' y ) holds
b1 = b2
;
proof end;
func '&' -> Function of (2 -tuples_on BOOLEAN),BOOLEAN means :Def6: :: FACIRC_1:def 6
for x, y being Element of BOOLEAN holds it . <*x,y*> = x '&' y;
correctness
existence
ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x '&' y
;
uniqueness
for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x '&' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x '&' y ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def4 defines 'xor' FACIRC_1:def 4 :
for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds
( b1 = 'xor' iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'xor' y );

:: deftheorem Def5 defines 'or' FACIRC_1:def 5 :
for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds
( b1 = 'or' iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'or' y );

:: deftheorem Def6 defines '&' FACIRC_1:def 6 :
for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds
( b1 = '&' iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x '&' y );

definition
func or3 -> Function of (3 -tuples_on BOOLEAN),BOOLEAN means :Def7: :: FACIRC_1:def 7
for x, y, z being Element of BOOLEAN holds it . <*x,y,z*> = (x 'or' y) 'or' z;
correctness
existence
ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x 'or' y) 'or' z
;
uniqueness
for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x 'or' y) 'or' z ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = (x 'or' y) 'or' z ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def7 defines or3 FACIRC_1:def 7 :
for b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN holds
( b1 = or3 iff for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x 'or' y) 'or' z );

begin

theorem Th10: :: FACIRC_1:10
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for g being Gate of S holds (Following s) . (the_result_sort_of g) = (Den (g,A)) . (s * (the_arity_of g))
proof end;

definition
let S be non empty non void Circuit-like ManySortedSign ;
let A be non-empty Circuit of S;
let s be State of A;
let n be Nat;
func Following (s,n) -> State of A means :Def8: :: FACIRC_1:def 8
ex f being Function of NAT,(product the Sorts of A) st
( it = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) );
correctness
existence
ex b1 being State of A ex f being Function of NAT,(product the Sorts of A) st
( b1 = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) )
;
uniqueness
for b1, b2 being State of A st ex f being Function of NAT,(product the Sorts of A) st
( b1 = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) ) & ex f being Function of NAT,(product the Sorts of A) st
( b2 = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def8 defines Following FACIRC_1:def 8 :
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for n being Nat
for b5 being State of A holds
( b5 = Following (s,n) iff ex f being Function of NAT,(product the Sorts of A) st
( b5 = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) ) );

theorem Th11: :: FACIRC_1:11
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A holds Following (s,0) = s
proof end;

theorem Th12: :: FACIRC_1:12
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for n being Nat holds Following (s,(n + 1)) = Following (Following (s,n))
proof end;

theorem Th13: :: FACIRC_1:13
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for n, m being Nat holds Following (s,(n + m)) = Following ((Following (s,n)),m)
proof end;

theorem Th14: :: FACIRC_1:14
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A holds Following (s,1) = Following s
proof end;

theorem Th15: :: FACIRC_1:15
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A holds Following (s,2) = Following (Following s)
proof end;

theorem Th16: :: FACIRC_1:16
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for n being Nat holds Following (s,(n + 1)) = Following ((Following s),n)
proof end;

definition
let S be non empty non void Circuit-like ManySortedSign ;
let A be non-empty Circuit of S;
let s be State of A;
let x be set ;
pred s is_stable_at x means :Def9: :: FACIRC_1:def 9
for n being Nat holds (Following (s,n)) . x = s . x;
end;

:: deftheorem Def9 defines is_stable_at FACIRC_1:def 9 :
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for x being set holds
( s is_stable_at x iff for n being Nat holds (Following (s,n)) . x = s . x );

theorem :: FACIRC_1:17
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for x being set st s is_stable_at x holds
for n being Nat holds Following (s,n) is_stable_at x
proof end;

theorem :: FACIRC_1:18
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for x being set st x in InputVertices S holds
s is_stable_at x
proof end;

theorem Th19: :: FACIRC_1:19
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for g being Gate of S st ( for x being set st x in rng (the_arity_of g) holds
s is_stable_at x ) holds
Following s is_stable_at the_result_sort_of g
proof end;

begin

theorem Th20: :: FACIRC_1:20
for S1, S2 being non empty ManySortedSign
for v being Vertex of S1 holds
( v in the carrier of (S1 +* S2) & v in the carrier of (S2 +* S1) )
proof end;

theorem Th21: :: FACIRC_1:21
for S1, S2 being non empty unsplit gate`1=arity ManySortedSign
for x being set st x in InnerVertices S1 holds
( x in InnerVertices (S1 +* S2) & x in InnerVertices (S2 +* S1) )
proof end;

theorem :: FACIRC_1:22
for S1, S2 being non empty ManySortedSign
for x being set st x in InnerVertices S2 holds
x in InnerVertices (S1 +* S2)
proof end;

theorem :: FACIRC_1:23
for S1, S2 being non empty unsplit gate`1=arity ManySortedSign holds S1 +* S2 = S2 +* S1 by CIRCCOMB:5, CIRCCOMB:47;

theorem :: FACIRC_1:24
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 holds A1 +* A2 = A2 +* A1 by CIRCCOMB:22, CIRCCOMB:60;

theorem Th25: :: FACIRC_1:25
for S1, S2, S3 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
for A1 being Boolean Circuit of S1
for A2 being Boolean Circuit of S2
for A3 being Boolean Circuit of S3 holds (A1 +* A2) +* A3 = A1 +* (A2 +* A3)
proof end;

theorem Th26: :: FACIRC_1:26
for S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
for A1 being non-empty gate`2=den Boolean Circuit of S1
for A2 being non-empty gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2) holds
( s | the carrier of S1 is State of A1 & s | the carrier of S2 is State of A2 )
proof end;

theorem Th27: :: FACIRC_1:27
for S1, S2 being non empty unsplit gate`1=arity ManySortedSign holds InnerVertices (S1 +* S2) = (InnerVertices S1) \/ (InnerVertices S2)
proof end;

theorem Th28: :: FACIRC_1:28
for S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st InnerVertices S2 misses InputVertices S1 holds
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 s1 being State of A1 st s1 = s | the carrier of S1 holds
(Following s) | the carrier of S1 = Following s1
proof end;

theorem Th29: :: FACIRC_1:29
for S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st InnerVertices S1 misses InputVertices S2 holds
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 s2 being State of A2 st s2 = s | the carrier of S2 holds
(Following s) | the carrier of S2 = Following s2
proof end;

theorem Th30: :: FACIRC_1:30
for S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st InnerVertices S2 misses InputVertices S1 holds
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 s1 being State of A1 st s1 = s | the carrier of S1 holds
for n being Nat holds (Following (s,n)) | the carrier of S1 = Following (s1,n)
proof end;

theorem Th31: :: FACIRC_1:31
for S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st InnerVertices S1 misses InputVertices S2 holds
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 s2 being State of A2 st s2 = s | the carrier of S2 holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
proof end;

theorem Th32: :: FACIRC_1:32
for S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st InnerVertices S2 misses InputVertices S1 holds
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 s1 being State of A1 st s1 = s | the carrier of S1 holds
for v being set st v in the carrier of S1 holds
for n being Nat holds (Following (s,n)) . v = (Following (s1,n)) . v
proof end;

theorem Th33: :: FACIRC_1:33
for S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st InnerVertices S1 misses InputVertices S2 holds
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 s2 being State of A2 st s2 = s | the carrier of S2 holds
for v being set st v in the carrier of S2 holds
for n being Nat holds (Following (s,n)) . v = (Following (s2,n)) . v
proof end;

registration
let S be non empty non void gate`2=den ManySortedSign ;
let g be Gate of S;
cluster g `2 -> Relation-like Function-like ;
coherence
( g `2 is Function-like & g `2 is Relation-like )
proof end;
end;

theorem Th34: :: FACIRC_1:34
for S being non empty non void Circuit-like gate`2=den ManySortedSign
for A being non-empty Circuit of S st A is gate`2=den holds
for s being State of A
for g being Gate of S holds (Following s) . (the_result_sort_of g) = (g `2) . (s * (the_arity_of g))
proof end;

theorem Th35: :: FACIRC_1:35
for S being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
for A being non-empty gate`2=den Boolean Circuit of S
for s being State of A
for p being FinSequence
for f being Function st [p,f] in the carrier' of S holds
(Following s) . [p,f] = f . (s * p)
proof end;

theorem :: FACIRC_1:36
for S being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
for A being non-empty gate`2=den Boolean Circuit of S
for s being State of A
for p being FinSequence
for f being Function st [p,f] in the carrier' of S & ( for x being set st x in rng p holds
s is_stable_at x ) holds
Following s is_stable_at [p,f]
proof end;

theorem Th37: :: FACIRC_1:37
for S being non empty unsplit ManySortedSign holds InnerVertices S = the carrier' of S
proof end;

begin

theorem Th38: :: FACIRC_1:38
for f being set
for p being FinSequence holds InnerVertices (1GateCircStr (p,f)) is Relation
proof end;

theorem :: FACIRC_1:39
for f being set
for p being nonpair-yielding FinSequence holds InputVertices (1GateCircStr (p,f)) is without_pairs
proof end;

theorem Th40: :: FACIRC_1:40
for f, x, y being set holds InputVertices (1GateCircStr (<*x,y*>,f)) = {x,y}
proof end;

theorem Th41: :: FACIRC_1:41
for f being set
for x, y being non pair set holds InputVertices (1GateCircStr (<*x,y*>,f)) is without_pairs
proof end;

theorem Th42: :: FACIRC_1:42
for f, x, y, z being set holds InputVertices (1GateCircStr (<*x,y,z*>,f)) = {x,y,z}
proof end;

theorem Th43: :: FACIRC_1:43
for x, y, f being set holds
( x in the carrier of (1GateCircStr (<*x,y*>,f)) & y in the carrier of (1GateCircStr (<*x,y*>,f)) & [<*x,y*>,f] in the carrier of (1GateCircStr (<*x,y*>,f)) )
proof end;

theorem Th44: :: FACIRC_1:44
for x, y, z, f being set holds
( x in the carrier of (1GateCircStr (<*x,y,z*>,f)) & y in the carrier of (1GateCircStr (<*x,y,z*>,f)) & z in the carrier of (1GateCircStr (<*x,y,z*>,f)) )
proof end;

theorem :: FACIRC_1:45
for f, x being set
for p being FinSequence holds
( x in the carrier of (1GateCircStr (p,f,x)) & ( for y being set st y in rng p holds
y in the carrier of (1GateCircStr (p,f,x)) ) )
proof end;

theorem :: FACIRC_1:46
for f, x being set
for p being FinSequence holds
( 1GateCircStr (p,f,x) is gate`1=arity & 1GateCircStr (p,f,x) is Circuit-like )
proof end;

theorem Th47: :: FACIRC_1:47
for p being FinSequence
for f being set holds [p,f] in InnerVertices (1GateCircStr (p,f))
proof end;

definition
let x, y be set ;
let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN;
func 1GateCircuit (x,y,f) -> strict gate`2=den Boolean Circuit of 1GateCircStr (<*x,y*>,f) equals :: FACIRC_1:def 10
1GateCircuit (<*x,y*>,f);
coherence
1GateCircuit (<*x,y*>,f) is strict gate`2=den Boolean Circuit of 1GateCircStr (<*x,y*>,f)
by CIRCCOMB:61;
end;

:: deftheorem defines 1GateCircuit FACIRC_1:def 10 :
for x, y being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds 1GateCircuit (x,y,f) = 1GateCircuit (<*x,y*>,f);

theorem Th48: :: FACIRC_1:48
for x, y being set
for X being non empty finite set
for f being Function of (2 -tuples_on X),X
for s being State of (1GateCircuit (<*x,y*>,f)) holds
( (Following s) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following s) . x = s . x & (Following s) . y = s . y )
proof end;

theorem Th49: :: FACIRC_1:49
for x, y being set
for X being non empty finite set
for f being Function of (2 -tuples_on X),X
for s being State of (1GateCircuit (<*x,y*>,f)) holds Following s is stable
proof end;

theorem :: FACIRC_1:50
for x, y being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN
for s being State of (1GateCircuit (x,y,f)) holds
( (Following s) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following s) . x = s . x & (Following s) . y = s . y ) by Th48;

theorem :: FACIRC_1:51
for x, y being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN
for s being State of (1GateCircuit (x,y,f)) holds Following s is stable by Th49;

definition
let x, y, z be set ;
let f be Function of (3 -tuples_on BOOLEAN),BOOLEAN;
func 1GateCircuit (x,y,z,f) -> strict gate`2=den Boolean Circuit of 1GateCircStr (<*x,y,z*>,f) equals :: FACIRC_1:def 11
1GateCircuit (<*x,y,z*>,f);
coherence
1GateCircuit (<*x,y,z*>,f) is strict gate`2=den Boolean Circuit of 1GateCircStr (<*x,y,z*>,f)
by CIRCCOMB:61;
end;

:: deftheorem defines 1GateCircuit FACIRC_1:def 11 :
for x, y, z being set
for f being Function of (3 -tuples_on BOOLEAN),BOOLEAN holds 1GateCircuit (x,y,z,f) = 1GateCircuit (<*x,y,z*>,f);

theorem Th52: :: FACIRC_1:52
for x, y, z being set
for X being non empty finite set
for f being Function of (3 -tuples_on X),X
for s being State of (1GateCircuit (<*x,y,z*>,f)) holds
( (Following s) . [<*x,y,z*>,f] = f . <*(s . x),(s . y),(s . z)*> & (Following s) . x = s . x & (Following s) . y = s . y & (Following s) . z = s . z )
proof end;

theorem Th53: :: FACIRC_1:53
for x, y, z being set
for X being non empty finite set
for f being Function of (3 -tuples_on X),X
for s being State of (1GateCircuit (<*x,y,z*>,f)) holds Following s is stable
proof end;

theorem :: FACIRC_1:54
for x, y, z being set
for f being Function of (3 -tuples_on BOOLEAN),BOOLEAN
for s being State of (1GateCircuit (x,y,z,f)) holds
( (Following s) . [<*x,y,z*>,f] = f . <*(s . x),(s . y),(s . z)*> & (Following s) . x = s . x & (Following s) . y = s . y & (Following s) . z = s . z ) by Th52;

theorem :: FACIRC_1:55
for x, y, z being set
for f being Function of (3 -tuples_on BOOLEAN),BOOLEAN
for s being State of (1GateCircuit (x,y,z,f)) holds Following s is stable by Th53;

begin

definition
let x, y, c be set ;
let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN;
func 2GatesCircStr (x,y,c,f) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: FACIRC_1:def 12
(1GateCircStr (<*x,y*>,f)) +* (1GateCircStr (<*[<*x,y*>,f],c*>,f));
correctness
coherence
(1GateCircStr (<*x,y*>,f)) +* (1GateCircStr (<*[<*x,y*>,f],c*>,f)) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
;
;
end;

:: deftheorem defines 2GatesCircStr FACIRC_1:def 12 :
for x, y, c being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds 2GatesCircStr (x,y,c,f) = (1GateCircStr (<*x,y*>,f)) +* (1GateCircStr (<*[<*x,y*>,f],c*>,f));

definition
let x, y, c be set ;
let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN;
func 2GatesCircOutput (x,y,c,f) -> Element of InnerVertices (2GatesCircStr (x,y,c,f)) equals :: FACIRC_1:def 13
[<*[<*x,y*>,f],c*>,f];
coherence
[<*[<*x,y*>,f],c*>,f] is Element of InnerVertices (2GatesCircStr (x,y,c,f))
proof end;
correctness
;
end;

:: deftheorem defines 2GatesCircOutput FACIRC_1:def 13 :
for x, y, c being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds 2GatesCircOutput (x,y,c,f) = [<*[<*x,y*>,f],c*>,f];

registration
let x, y, c be set ;
let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN;
cluster 2GatesCircOutput (x,y,c,f) -> pair ;
coherence
2GatesCircOutput (x,y,c,f) is pair
;
end;

theorem Th56: :: FACIRC_1:56
for x, y, c being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds InnerVertices (2GatesCircStr (x,y,c,f)) = {[<*x,y*>,f],(2GatesCircOutput (x,y,c,f))}
proof end;

theorem Th57: :: FACIRC_1:57
for c, x, y being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN st c <> [<*x,y*>,f] holds
InputVertices (2GatesCircStr (x,y,c,f)) = {x,y,c}
proof end;

definition
let x, y, c be set ;
let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN;
func 2GatesCircuit (x,y,c,f) -> strict gate`2=den Boolean Circuit of 2GatesCircStr (x,y,c,f) equals :: FACIRC_1:def 14
(1GateCircuit (x,y,f)) +* (1GateCircuit ([<*x,y*>,f],c,f));
coherence
(1GateCircuit (x,y,f)) +* (1GateCircuit ([<*x,y*>,f],c,f)) is strict gate`2=den Boolean Circuit of 2GatesCircStr (x,y,c,f)
;
end;

:: deftheorem defines 2GatesCircuit FACIRC_1:def 14 :
for x, y, c being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds 2GatesCircuit (x,y,c,f) = (1GateCircuit (x,y,f)) +* (1GateCircuit ([<*x,y*>,f],c,f));

theorem Th58: :: FACIRC_1:58
for x, y, c being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds InnerVertices (2GatesCircStr (x,y,c,f)) is Relation
proof end;

theorem Th59: :: FACIRC_1:59
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN
for x, y, c being non pair set holds InputVertices (2GatesCircStr (x,y,c,f)) is without_pairs
proof end;

theorem Th60: :: FACIRC_1:60
for x, y, c being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds
( x in the carrier of (2GatesCircStr (x,y,c,f)) & y in the carrier of (2GatesCircStr (x,y,c,f)) & c in the carrier of (2GatesCircStr (x,y,c,f)) )
proof end;

theorem :: FACIRC_1:61
for x, y, c being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds
( [<*x,y*>,f] in the carrier of (2GatesCircStr (x,y,c,f)) & [<*[<*x,y*>,f],c*>,f] in the carrier of (2GatesCircStr (x,y,c,f)) )
proof end;

definition
let S be non empty non void unsplit ManySortedSign ;
let A be Boolean Circuit of S;
let s be State of A;
let v be Vertex of S;
:: original: .
redefine func s . v -> Element of BOOLEAN ;
coherence
s . v is Element of BOOLEAN
proof end;
end;

Lm1: for c, x, y being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN
for s being State of (2GatesCircuit (x,y,c,f)) st c <> [<*x,y*>,f] holds
( (Following s) . (2GatesCircOutput (x,y,c,f)) = f . <*(s . [<*x,y*>,f]),(s . c)*> & (Following s) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following s) . x = s . x & (Following s) . y = s . y & (Following s) . c = s . c )

proof end;

theorem Th62: :: FACIRC_1:62
for c, x, y being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN
for s being State of (2GatesCircuit (x,y,c,f)) st c <> [<*x,y*>,f] holds
( (Following (s,2)) . (2GatesCircOutput (x,y,c,f)) = f . <*(f . <*(s . x),(s . y)*>),(s . c)*> & (Following (s,2)) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following (s,2)) . x = s . x & (Following (s,2)) . y = s . y & (Following (s,2)) . c = s . c )
proof end;

theorem Th63: :: FACIRC_1:63
for c, x, y being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN
for s being State of (2GatesCircuit (x,y,c,f)) st c <> [<*x,y*>,f] holds
Following (s,2) is stable
proof end;

theorem Th64: :: FACIRC_1:64
for c, x, y being set st c <> [<*x,y*>,'xor'] holds
for s being State of (2GatesCircuit (x,y,c,'xor'))
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
(Following (s,2)) . (2GatesCircOutput (x,y,c,'xor')) = (a1 'xor' a2) 'xor' a3
proof end;

theorem :: FACIRC_1:65
for c, x, y being set st c <> [<*x,y*>,'or'] holds
for s being State of (2GatesCircuit (x,y,c,'or'))
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
(Following (s,2)) . (2GatesCircOutput (x,y,c,'or')) = (a1 'or' a2) 'or' a3
proof end;

theorem :: FACIRC_1:66
for c, x, y being set st c <> [<*x,y*>,'&'] holds
for s being State of (2GatesCircuit (x,y,c,'&'))
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
(Following (s,2)) . (2GatesCircOutput (x,y,c,'&')) = (a1 '&' a2) '&' a3
proof end;

begin

definition
let x, y, c be set ;
func BitAdderOutput (x,y,c) -> Element of InnerVertices (2GatesCircStr (x,y,c,'xor')) equals :: FACIRC_1:def 15
2GatesCircOutput (x,y,c,'xor');
coherence
2GatesCircOutput (x,y,c,'xor') is Element of InnerVertices (2GatesCircStr (x,y,c,'xor'))
;
end;

:: deftheorem defines BitAdderOutput FACIRC_1:def 15 :
for x, y, c being set holds BitAdderOutput (x,y,c) = 2GatesCircOutput (x,y,c,'xor');

definition
let x, y, c be set ;
func BitAdderCirc (x,y,c) -> strict gate`2=den Boolean Circuit of 2GatesCircStr (x,y,c,'xor') equals :: FACIRC_1:def 16
2GatesCircuit (x,y,c,'xor');
coherence
2GatesCircuit (x,y,c,'xor') is strict gate`2=den Boolean Circuit of 2GatesCircStr (x,y,c,'xor')
;
end;

:: deftheorem defines BitAdderCirc FACIRC_1:def 16 :
for x, y, c being set holds BitAdderCirc (x,y,c) = 2GatesCircuit (x,y,c,'xor');

definition
let x, y, c be set ;
func MajorityIStr (x,y,c) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: FACIRC_1:def 17
((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&'))) +* (1GateCircStr (<*c,x*>,'&'));
correctness
coherence
((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&'))) +* (1GateCircStr (<*c,x*>,'&')) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
;
;
end;

:: deftheorem defines MajorityIStr FACIRC_1:def 17 :
for x, y, c being set holds MajorityIStr (x,y,c) = ((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&'))) +* (1GateCircStr (<*c,x*>,'&'));

definition
let x, y, c be set ;
func MajorityStr (x,y,c) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: FACIRC_1:def 18
(MajorityIStr (x,y,c)) +* (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3));
correctness
coherence
(MajorityIStr (x,y,c)) +* (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
;
;
end;

:: deftheorem defines MajorityStr FACIRC_1:def 18 :
for x, y, c being set holds MajorityStr (x,y,c) = (MajorityIStr (x,y,c)) +* (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3));

definition
let x, y, c be set ;
func MajorityICirc (x,y,c) -> strict gate`2=den Boolean Circuit of MajorityIStr (x,y,c) equals :: FACIRC_1:def 19
((1GateCircuit (x,y,'&')) +* (1GateCircuit (y,c,'&'))) +* (1GateCircuit (c,x,'&'));
coherence
((1GateCircuit (x,y,'&')) +* (1GateCircuit (y,c,'&'))) +* (1GateCircuit (c,x,'&')) is strict gate`2=den Boolean Circuit of MajorityIStr (x,y,c)
;
end;

:: deftheorem defines MajorityICirc FACIRC_1:def 19 :
for x, y, c being set holds MajorityICirc (x,y,c) = ((1GateCircuit (x,y,'&')) +* (1GateCircuit (y,c,'&'))) +* (1GateCircuit (c,x,'&'));

theorem Th67: :: FACIRC_1:67
for x, y, c being set holds InnerVertices (MajorityStr (x,y,c)) is Relation
proof end;

theorem Th68: :: FACIRC_1:68
for x, y, c being non pair set holds InputVertices (MajorityStr (x,y,c)) is without_pairs
proof end;

theorem :: FACIRC_1:69
for x, y, c being set
for s being State of (MajorityICirc (x,y,c))
for a, b being Element of BOOLEAN st a = s . x & b = s . y holds
(Following s) . [<*x,y*>,'&'] = a '&' b
proof end;

theorem :: FACIRC_1:70
for x, y, c being set
for s being State of (MajorityICirc (x,y,c))
for a, b being Element of BOOLEAN st a = s . y & b = s . c holds
(Following s) . [<*y,c*>,'&'] = a '&' b
proof end;

theorem :: FACIRC_1:71
for x, y, c being set
for s being State of (MajorityICirc (x,y,c))
for a, b being Element of BOOLEAN st a = s . c & b = s . x holds
(Following s) . [<*c,x*>,'&'] = a '&' b
proof end;

definition
let x, y, c be set ;
func MajorityOutput (x,y,c) -> Element of InnerVertices (MajorityStr (x,y,c)) equals :: FACIRC_1:def 20
[<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3];
coherence
[<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3] is Element of InnerVertices (MajorityStr (x,y,c))
proof end;
correctness
;
end;

:: deftheorem defines MajorityOutput FACIRC_1:def 20 :
for x, y, c being set holds MajorityOutput (x,y,c) = [<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3];

definition
let x, y, c be set ;
func MajorityCirc (x,y,c) -> strict gate`2=den Boolean Circuit of MajorityStr (x,y,c) equals :: FACIRC_1:def 21
(MajorityICirc (x,y,c)) +* (1GateCircuit ([<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&'],or3));
coherence
(MajorityICirc (x,y,c)) +* (1GateCircuit ([<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&'],or3)) is strict gate`2=den Boolean Circuit of MajorityStr (x,y,c)
;
end;

:: deftheorem defines MajorityCirc FACIRC_1:def 21 :
for x, y, c being set holds MajorityCirc (x,y,c) = (MajorityICirc (x,y,c)) +* (1GateCircuit ([<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&'],or3));

theorem Th72: :: FACIRC_1:72
for x, y, c being set holds
( x in the carrier of (MajorityStr (x,y,c)) & y in the carrier of (MajorityStr (x,y,c)) & c in the carrier of (MajorityStr (x,y,c)) )
proof end;

theorem Th73: :: FACIRC_1:73
for x, y, c being set holds
( [<*x,y*>,'&'] in InnerVertices (MajorityStr (x,y,c)) & [<*y,c*>,'&'] in InnerVertices (MajorityStr (x,y,c)) & [<*c,x*>,'&'] in InnerVertices (MajorityStr (x,y,c)) )
proof end;

theorem Th74: :: FACIRC_1:74
for x, y, c being non pair set holds
( x in InputVertices (MajorityStr (x,y,c)) & y in InputVertices (MajorityStr (x,y,c)) & c in InputVertices (MajorityStr (x,y,c)) )
proof end;

theorem Th75: :: FACIRC_1:75
for x, y, c being non pair set holds
( InputVertices (MajorityStr (x,y,c)) = {x,y,c} & InnerVertices (MajorityStr (x,y,c)) = {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} \/ {(MajorityOutput (x,y,c))} )
proof end;

Lm2: for x, y, c being non pair set
for s being State of (MajorityCirc (x,y,c))
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
( (Following s) . [<*x,y*>,'&'] = a1 '&' a2 & (Following s) . [<*y,c*>,'&'] = a2 '&' a3 & (Following s) . [<*c,x*>,'&'] = a3 '&' a1 )

proof end;

theorem :: FACIRC_1:76
for x, y, c being non pair set
for s being State of (MajorityCirc (x,y,c))
for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . y holds
(Following s) . [<*x,y*>,'&'] = a1 '&' a2
proof end;

theorem :: FACIRC_1:77
for x, y, c being non pair set
for s being State of (MajorityCirc (x,y,c))
for a2, a3 being Element of BOOLEAN st a2 = s . y & a3 = s . c holds
(Following s) . [<*y,c*>,'&'] = a2 '&' a3
proof end;

theorem :: FACIRC_1:78
for x, y, c being non pair set
for s being State of (MajorityCirc (x,y,c))
for a1, a3 being Element of BOOLEAN st a1 = s . x & a3 = s . c holds
(Following s) . [<*c,x*>,'&'] = a3 '&' a1
proof end;

theorem Th79: :: FACIRC_1:79
for x, y, c being non pair set
for s being State of (MajorityCirc (x,y,c))
for a1, a2, a3 being Element of BOOLEAN st a1 = s . [<*x,y*>,'&'] & a2 = s . [<*y,c*>,'&'] & a3 = s . [<*c,x*>,'&'] holds
(Following s) . (MajorityOutput (x,y,c)) = (a1 'or' a2) 'or' a3
proof end;

Lm3: for x, y, c being non pair set
for s being State of (MajorityCirc (x,y,c))
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
( (Following (s,2)) . (MajorityOutput (x,y,c)) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1) & (Following (s,2)) . [<*x,y*>,'&'] = a1 '&' a2 & (Following (s,2)) . [<*y,c*>,'&'] = a2 '&' a3 & (Following (s,2)) . [<*c,x*>,'&'] = a3 '&' a1 )

proof end;

theorem :: FACIRC_1:80
for x, y, c being non pair set
for s being State of (MajorityCirc (x,y,c))
for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . y holds
(Following (s,2)) . [<*x,y*>,'&'] = a1 '&' a2
proof end;

theorem :: FACIRC_1:81
for x, y, c being non pair set
for s being State of (MajorityCirc (x,y,c))
for a2, a3 being Element of BOOLEAN st a2 = s . y & a3 = s . c holds
(Following (s,2)) . [<*y,c*>,'&'] = a2 '&' a3
proof end;

theorem :: FACIRC_1:82
for x, y, c being non pair set
for s being State of (MajorityCirc (x,y,c))
for a1, a3 being Element of BOOLEAN st a1 = s . x & a3 = s . c holds
(Following (s,2)) . [<*c,x*>,'&'] = a3 '&' a1
proof end;

theorem :: FACIRC_1:83
for x, y, c being non pair set
for s being State of (MajorityCirc (x,y,c))
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
(Following (s,2)) . (MajorityOutput (x,y,c)) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1) by Lm3;

theorem Th84: :: FACIRC_1:84
for x, y, c being non pair set
for s being State of (MajorityCirc (x,y,c)) holds Following (s,2) is stable
proof end;

definition
let x, y, c be set ;
func BitAdderWithOverflowStr (x,y,c) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: FACIRC_1:def 22
(2GatesCircStr (x,y,c,'xor')) +* (MajorityStr (x,y,c));
coherence
(2GatesCircStr (x,y,c,'xor')) +* (MajorityStr (x,y,c)) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
;
end;

:: deftheorem defines BitAdderWithOverflowStr FACIRC_1:def 22 :
for x, y, c being set holds BitAdderWithOverflowStr (x,y,c) = (2GatesCircStr (x,y,c,'xor')) +* (MajorityStr (x,y,c));

theorem Th85: :: FACIRC_1:85
for x, y, c being non pair set holds InputVertices (BitAdderWithOverflowStr (x,y,c)) = {x,y,c}
proof end;

theorem :: FACIRC_1:86
for x, y, c being non pair set holds InnerVertices (BitAdderWithOverflowStr (x,y,c)) = ({[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} \/ {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']}) \/ {(MajorityOutput (x,y,c))}
proof end;

theorem :: FACIRC_1:87
for x, y, c being set
for S being non empty ManySortedSign st S = BitAdderWithOverflowStr (x,y,c) holds
( x in the carrier of S & y in the carrier of S & c in the carrier of S )
proof end;

definition
let x, y, c be set ;
func BitAdderWithOverflowCirc (x,y,c) -> strict gate`2=den Boolean Circuit of BitAdderWithOverflowStr (x,y,c) equals :: FACIRC_1:def 23
(BitAdderCirc (x,y,c)) +* (MajorityCirc (x,y,c));
coherence
(BitAdderCirc (x,y,c)) +* (MajorityCirc (x,y,c)) is strict gate`2=den Boolean Circuit of BitAdderWithOverflowStr (x,y,c)
;
end;

:: deftheorem defines BitAdderWithOverflowCirc FACIRC_1:def 23 :
for x, y, c being set holds BitAdderWithOverflowCirc (x,y,c) = (BitAdderCirc (x,y,c)) +* (MajorityCirc (x,y,c));

theorem :: FACIRC_1:88
for x, y, c being set holds InnerVertices (BitAdderWithOverflowStr (x,y,c)) is Relation
proof end;

theorem :: FACIRC_1:89
for x, y, c being non pair set holds InputVertices (BitAdderWithOverflowStr (x,y,c)) is without_pairs
proof end;

theorem :: FACIRC_1:90
for x, y, c being set holds
( BitAdderOutput (x,y,c) in InnerVertices (BitAdderWithOverflowStr (x,y,c)) & MajorityOutput (x,y,c) in InnerVertices (BitAdderWithOverflowStr (x,y,c)) ) by Th21;

theorem :: FACIRC_1:91
for x, y, c being non pair set
for s being State of (BitAdderWithOverflowCirc (x,y,c))
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
( (Following (s,2)) . (BitAdderOutput (x,y,c)) = (a1 'xor' a2) 'xor' a3 & (Following (s,2)) . (MajorityOutput (x,y,c)) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1) )
proof end;

theorem :: FACIRC_1:92
for x, y, c being non pair set
for s being State of (BitAdderWithOverflowCirc (x,y,c)) holds Following (s,2) is stable
proof end;