FACIRC_1: Full Adder Circuit. Part { I }

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

definition

let IT be set ;
attr IT is pair means :Def1: :: FACIRC_1:def 1
ex x, y being set st IT = [x,y];

end;

:: deftheorem Def1 defines pair FACIRC_1:def 1 :

registration

cluster pair -> non empty set ;
coherence

proof end;

end;

registration

let x, y be set ;
cluster [x,y] -> pair ;
coherence

proof end;

end;

registration

cluster pair set ;
existence

proof end;

cluster non pair set ;
existence

proof end;

end;

registration

cluster -> non pair set ;
coherence

proof end;

end;

definition

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 Def2 defines with_pair FACIRC_1:def 2 :

notation

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

end;

registration

cluster empty -> without_pairs set ;
coherence

proof end;

let x be non pair set ;
cluster {x} -> without_pairs ;
coherence

proof end;

let y be non pair set ;
cluster {x,y} -> without_pairs ;
coherence

proof end;

let z be non pair set ;
cluster {x,y,z} -> without_pairs ;
coherence

proof end;

end;

registration

cluster non empty without_pairs set ;
existence

proof end;

end;

registration

let X, Y be without_pairs set ;
cluster X \/ Y -> without_pairs ;
coherence

proof end;

end;

registration

let X be without_pairs set ;
let Y be set ;
cluster X \ Y -> without_pairs ;
coherence

proof end;

cluster X /\ Y -> without_pairs ;
coherence

proof end;

cluster Y /\ X -> without_pairs ;
coherence ;

end;

registration

let x be pair set ;
cluster {x} -> Relation-like ;
coherence

proof end;

let y be pair set ;
cluster {x,y} -> Relation-like ;
coherence

proof end;

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

proof end;

end;

registration

cluster Relation-like without_pairs -> empty set ;
coherence

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 :

registration

let x be non pair set ;
cluster <*x*> -> nonpair-yielding ;
coherence

proof end;

let y be non pair set ;
cluster <*x,y*> -> nonpair-yielding ;
coherence

proof end;

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

proof end;

end;

theorem Th1: :: FACIRC_1:1

for f being Function st f is nonpair-yielding holds
not rng f is with_pair

proof end;

registration

let n be Nat;
cluster one-to-one nonpair-yielding FinSeqLen of n;
existence

proof end;

end;

registration

cluster one-to-one nonpair-yielding set ;
existence

proof end;

end;

registration

let f be nonpair-yielding Function;
cluster rng f -> without_pairs ;
coherence 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 Th3: :: 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:55;

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 not X is with_pair & 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 not InputVertices S1 is with_pair & 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 not InputVertices S1 is with_pair & InnerVertices S1 is Relation & not InputVertices S2 is with_pair & 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 & not InputVertices S1 is with_pair & not InputVertices S2 is with_pair holds
not InputVertices (S1 +* S2) is with_pair

proof end;

theorem :: FACIRC_1:9

for S1, S2 being non empty unsplit gate`1=arity ManySortedSign st not InputVertices S1 is with_pair & not InputVertices S2 is with_pair holds
not InputVertices (S1 +* S2) is with_pair by Th8, CIRCCOMB:55;

scheme :: FACIRC_1:sch 1
2AryBooleEx{ F₁( 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*> = F₁(x,y)

proof end;

scheme :: FACIRC_1:sch 2
2AryBooleUniq{ F₁( 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*> = F₁(x,y) ) & ( for x, y being Element of BOOLEAN holds f2 . <*x,y*> = F₁(x,y) ) holds
f1 = f2

proof end;

scheme :: FACIRC_1:sch 3
2AryBooleDef{ F₁( 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*> = F₁(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*> = F₁(x,y) ) & ( for x, y being Element of BOOLEAN holds f2 . <*x,y*> = F₁(x,y) ) holds
f1 = f2 ) )

proof end;

scheme :: FACIRC_1:sch 4
3AryBooleEx{ F₁( 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*> = F₁(x,y,z)

proof end;

scheme :: FACIRC_1:sch 5
3AryBooleUniq{ F₁( 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*> = F₁(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds f2 . <*x,y,z*> = F₁(x,y,z) ) holds
f1 = f2

proof end;

scheme :: FACIRC_1:sch 6
3AryBooleDef{ F₁( 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*> = F₁(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*> = F₁(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds f2 . <*x,y,z*> = F₁(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

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

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

proof end;

end;

:: deftheorem Def4 defines 'xor' FACIRC_1:def 4 :

:: deftheorem Def5 defines 'or' FACIRC_1:def 5 :

:: deftheorem Def6 defines '&' FACIRC_1:def 6 :

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

proof end;

end;

:: deftheorem Def7 defines or3 FACIRC_1:def 7 :

definition

let x be set ;
:: original: <*
redefine func <*x*> -> FinSeqLen of 1;
coherence

proof end;

let y be set ;
:: original: <*
redefine func <*x,y*> -> FinSeqLen of 2;
coherence

proof end;

let z be set ;
:: original: <*
redefine func <*x,y,z*> -> FinSeqLen of 3;
coherence

proof end;

end;

definition

let n, m be Nat;
let p be FinSeqLen of n;
let q be FinSeqLen of m;
:: original: ^
redefine func p ^ q -> FinSeqLen of n + m;
coherence

proof end;

end;

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

proof end;

end;

:: deftheorem Def8 defines Following FACIRC_1:def 8 :

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 :

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;

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:9, CIRCCOMB:55;

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:26, CIRCCOMB:68;

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

proof end;

theorem Th31: :: FACIRC_1:31

proof end;

theorem Th32: :: FACIRC_1:32

proof end;

theorem Th33: :: FACIRC_1:33

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

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

proof end;

theorem Th37: :: FACIRC_1:37

for S being non empty unsplit ManySortedSign holds InnerVertices S = the carrier' of S

proof end;

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 not InputVertices (1GateCircStr p,f) is with_pair

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 not InputVertices (1GateCircStr <*x,y*>,f) is with_pair

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 by CIRCCOMB:69;

end;

:: deftheorem defines 1GateCircuit FACIRC_1:def 10 :

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 by CIRCCOMB:69;

end;

:: deftheorem defines 1GateCircuit FACIRC_1:def 11 :

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;

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 ;

end;

:: deftheorem defines 2GatesCircStr FACIRC_1:def 12 :

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

proof end;

correctness ;

end;

:: deftheorem defines 2GatesCircOutput FACIRC_1:def 13 :

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 ;

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 ;

end;

:: deftheorem defines 2GatesCircuit FACIRC_1:def 14 :

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 not InputVertices (2GatesCircStr x,y,c,f) is with_pair

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

proof end;

end;

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

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 ;

end;

:: deftheorem defines BitAdderOutput FACIRC_1:def 15 :

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 ;

end;

:: deftheorem defines BitAdderCirc FACIRC_1:def 16 :

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 ;

end;

:: deftheorem defines MajorityIStr FACIRC_1:def 17 :

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 ;

end;

:: deftheorem defines MajorityStr FACIRC_1:def 18 :

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 ;

end;

:: deftheorem defines MajorityICirc FACIRC_1:def 19 :

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 not InputVertices (MajorityStr x,y,c) is with_pair

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

proof end;

correctness ;

end;

:: deftheorem defines MajorityOutput FACIRC_1:def 20 :

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 ;

end;

:: deftheorem defines MajorityCirc FACIRC_1:def 21 :

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;

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) . [<*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;

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

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 ;

end;

:: deftheorem defines BitAdderWithOverflowStr FACIRC_1:def 22 :

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 ;

end;

:: deftheorem defines BitAdderWithOverflowCirc FACIRC_1:def 23 :

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 not InputVertices (BitAdderWithOverflowStr x,y,c) is with_pair

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;