FACIRC_1: Full Adder Circuit. Part { I }

proof end;

end;

registration

cluster non pair for object ;

proof end;

end;

registration

cluster natural -> non pair for set ;

proof end;

end;

definition

let IT be set ;

attr IT is with_pair means :Def1: :: FACIRC_1:def 2
ex x being pair object st x in IT;

end;

:: deftheorem FACIRC_1:def 1 :

:: deftheorem Def1 defines with_pair FACIRC_1:def 2 :

notation

let IT be set ;
antonym without_pairs IT for with_pair ;

end;

registration

cluster empty -> without_pairs for set ;

coherence ;
let x be non pair object ;

cluster {x} -> without_pairs ;

coherence by TARSKI:def 1;
let y be non pair object ;

cluster {x,y} -> without_pairs ;

coherence by TARSKI:def 2;
let z be non pair object ;

cluster {x,y,z} -> without_pairs ;

coherence by ENUMSET1:def 1;

end;

registration

cluster non empty without_pairs for set ;

proof end;

end;

registration

let X, Y be without_pairs set ;

cluster X \/ Y -> without_pairs ;

proof end;

end;

registration

let X be without_pairs set ;
let Y be set ;

cluster X \ Y -> without_pairs ;

coherence by Def1;

cluster X /\ Y -> without_pairs ;

proof end;

cluster Y /\ X -> without_pairs ;

end;

registration

let x be pair object ;

cluster {x} -> Relation-like ;

proof end;

let y be pair object ;

cluster {x,y} -> Relation-like ;

proof end;

let z be pair object ;

cluster {x,y,z} -> Relation-like ;

proof end;

end;

registration

cluster Relation-like without_pairs -> empty for set ;

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

cluster <*x*> -> nonpair-yielding ;

proof end;

let y be non pair object ;

cluster <*x,y*> -> nonpair-yielding ;

proof end;

let z be non pair object ;

cluster <*x,y,z*> -> 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 omega -defined Function-like one-to-one finite n -element FinSequence-like FinSubsequence-like countable nonpair-yielding for set ;

proof end;

end;

registration

cluster Relation-like omega -defined Function-like one-to-one finite FinSequence-like FinSubsequence-like countable nonpair-yielding for set ;

proof end;

end;

registration

let f be nonpair-yielding Function;

cluster proj2 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 :: 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 ;

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;

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{ 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 :Def3: :: FACIRC_1:def 4
for x, y being Element of BOOLEAN holds it . <*x,y*> = x 'xor' y;

proof end;

func 'or' -> Function of (2 -tuples_on BOOLEAN),BOOLEAN means :Def4: :: FACIRC_1:def 5
for x, y being Element of BOOLEAN holds it . <*x,y*> = x 'or' y;

proof end;

func '&' -> Function of (2 -tuples_on BOOLEAN),BOOLEAN means :Def5: :: FACIRC_1:def 6
for x, y being Element of BOOLEAN holds it . <*x,y*> = x '&' y;

proof end;

end;

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

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

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

definition

func or3 -> Function of (3 -tuples_on BOOLEAN),BOOLEAN means :Def6: :: FACIRC_1:def 7
for x, y, z being Element of BOOLEAN holds it . <*x,y,z*> = (x 'or' y) 'or' z;

proof end;

end;

:: deftheorem Def6 defines or3 FACIRC_1:def 7 :

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 natural Number ;

func Following (s,n) -> State of A means :Def7: :: FACIRC_1:def 8
ex f being sequence of (product the Sorts of A) st
( it = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) );

proof end;

end;

:: deftheorem Def7 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 object ;

pred s is_stable_at x means :: FACIRC_1:def 9
for n being Nat holds (Following (s,n)) . x = s . x;

end;

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

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 for set ;

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

proof end;

theorem Th40: :: FACIRC_1:40

for f, x, y being object 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 object holds InputVertices (1GateCircStr (<*x,y*>,f)) is without_pairs

proof end;

theorem Th42: :: FACIRC_1:42

for f, x, y, z being object holds InputVertices (1GateCircStr (<*x,y,z*>,f)) = {x,y,z}

proof end;

theorem Th43: :: FACIRC_1:43

for x, y, f being object 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 object 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 object ;
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:61;

end;

:: deftheorem defines 1GateCircuit FACIRC_1:def 10 :

theorem Th48: :: FACIRC_1:48

for x, y being object
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 object
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 object
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 object
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 object ;
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:61;

end;

:: deftheorem defines 1GateCircuit FACIRC_1:def 11 :

theorem Th52: :: FACIRC_1:52

for x, y, z being object
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 object
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 object
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 object
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 object ;
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));

end;

:: deftheorem defines 2GatesCircStr FACIRC_1:def 12 :

definition

let x, y, c be object ;
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];

proof end;

end;

:: deftheorem defines 2GatesCircOutput FACIRC_1:def 13 :

registration

let x, y, c be object ;
let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN;

cluster 2GatesCircOutput (x,y,c,f) -> pair ;

end;

theorem Th56: :: FACIRC_1:56

for x, y, c being object
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 x, y, c being object
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 object ;
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));

end;

:: deftheorem defines 2GatesCircuit FACIRC_1:def 14 :

theorem Th58: :: FACIRC_1:58

for x, y, c being object
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 object holds InputVertices (2GatesCircStr (x,y,c,f)) is without_pairs

proof end;

theorem Th60: :: FACIRC_1:60

for x, y, c being object
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 object
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;

Lm1: for x, y, c being object
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 x, y, c being object
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 x, y, c being object
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 x, y, c being object 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 x, y, c being object 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 x, y, c being object 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 object ;

func BitAdderOutput (x,y,c) -> Element of InnerVertices (2GatesCircStr (x,y,c,'xor')) equals :: FACIRC_1:def 15
2GatesCircOutput (x,y,c,'xor');

end;

:: deftheorem defines BitAdderOutput FACIRC_1:def 15 :

definition

let x, y, c be object ;

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');

end;

:: deftheorem defines BitAdderCirc FACIRC_1:def 16 :

definition

let x, y, c be object ;

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*>,'&'));

end;

:: deftheorem defines MajorityIStr FACIRC_1:def 17 :

definition

let x, y, c be object ;

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

end;

:: deftheorem defines MajorityStr FACIRC_1:def 18 :

definition

let x, y, c be object ;

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,'&'));

end;

:: deftheorem defines MajorityICirc FACIRC_1:def 19 :

theorem Th67: :: FACIRC_1:67

for x, y, c being object holds InnerVertices (MajorityStr (x,y,c)) is Relation

proof end;

theorem Th68: :: FACIRC_1:68

for x, y, c being non pair object holds InputVertices (MajorityStr (x,y,c)) is without_pairs

proof end;

theorem :: FACIRC_1:69

for x, y, c being object
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 object
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 object
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 object ;

func MajorityOutput (x,y,c) -> Element of InnerVertices (MajorityStr (x,y,c)) equals :: FACIRC_1:def 20
[<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3];

proof end;

end;

:: deftheorem defines MajorityOutput FACIRC_1:def 20 :

definition

let x, y, c be object ;

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

end;

:: deftheorem defines MajorityCirc FACIRC_1:def 21 :

theorem Th72: :: FACIRC_1:72

for x, y, c being object 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 object 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 object 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 object 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 object
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 object
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 object
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 object
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 object
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 object
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 object
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 object
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 object
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 object
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 object
for s being State of (MajorityCirc (x,y,c)) holds Following (s,2) is stable

proof end;

definition

let x, y, c be object ;

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

end;

:: deftheorem defines BitAdderWithOverflowStr FACIRC_1:def 22 :

theorem Th85: :: FACIRC_1:85

for x, y, c being non pair object holds InputVertices (BitAdderWithOverflowStr (x,y,c)) = {x,y,c}

proof end;

theorem :: FACIRC_1:86

for x, y, c being non pair object 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 object
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 object ;

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