:: Generalized Full Adder Circuits (GFAs). {P}art {I}
:: by Shin'nosuke Yamaguchi , Katsumi Wasaki and Nobuhiro Shimoi
::
:: Received December 7, 2005
:: Copyright (c) 2005 Association of Mizar Users

scheme :: GFACIRC1:sch 1
1AryBooleEx{ F₁( set ) -> Element of BOOLEAN } :

ex f being Function of (1 -tuples_on BOOLEAN ),BOOLEAN st
for x being Element of BOOLEAN holds f . <*x*> = F₁(x)

proof end;

scheme :: GFACIRC1:sch 2
1AryBooleUniq{ F₁( set ) -> Element of BOOLEAN } :

for f1, f2 being Function of (1 -tuples_on BOOLEAN ),BOOLEAN st ( for x being Element of BOOLEAN holds f1 . <*x*> = F₁(x) ) & ( for x being Element of BOOLEAN holds f2 . <*x*> = F₁(x) ) holds
f1 = f2

proof end;

scheme :: GFACIRC1:sch 3
1AryBooleDef{ F₁( set ) -> Element of BOOLEAN } :

( ex f being Function of (1 -tuples_on BOOLEAN ),BOOLEAN st
for x being Element of BOOLEAN holds f . <*x*> = F₁(x) & ( for f1, f2 being Function of (1 -tuples_on BOOLEAN ),BOOLEAN st ( for x being Element of BOOLEAN holds f1 . <*x*> = F₁(x) ) & ( for x being Element of BOOLEAN holds f2 . <*x*> = F₁(x) ) holds
f1 = f2 ) )

proof end;

definition

func inv1 -> Function of (1 -tuples_on BOOLEAN ),BOOLEAN means :Def1: :: GFACIRC1:def 1
for x being Element of BOOLEAN holds it . <*x*> = 'not' x;
existence
ex b₁ being Function of (1 -tuples_on BOOLEAN ),BOOLEAN st
for x being Element of BOOLEAN holds b₁ . <*x*> = 'not' x

proof end;

uniqueness
for b₁, b₂ being Function of (1 -tuples_on BOOLEAN ),BOOLEAN st ( for x being Element of BOOLEAN holds b₁ . <*x*> = 'not' x ) & ( for x being Element of BOOLEAN holds b₂ . <*x*> = 'not' x ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines inv1 GFACIRC1:def 1 :

for b₁ being Function of (1 -tuples_on BOOLEAN ),BOOLEAN holds
( b₁ = inv1 iff for x being Element of BOOLEAN holds b₁ . <*x*> = 'not' x );

theorem Th1: :: GFACIRC1:1

for x being Element of BOOLEAN holds
( inv1 . <*x*> = 'not' x & inv1 . <*x*> = nand2 . <*x,x*> & inv1 . <*0 *> = 1 & inv1 . <*1*> = 0 )

proof end;

definition

func buf1 -> Function of (1 -tuples_on BOOLEAN ),BOOLEAN means :Def2: :: GFACIRC1:def 2
for x being Element of BOOLEAN holds it . <*x*> = x;
existence
ex b₁ being Function of (1 -tuples_on BOOLEAN ),BOOLEAN st
for x being Element of BOOLEAN holds b₁ . <*x*> = x

proof end;

uniqueness
for b₁, b₂ being Function of (1 -tuples_on BOOLEAN ),BOOLEAN st ( for x being Element of BOOLEAN holds b₁ . <*x*> = x ) & ( for x being Element of BOOLEAN holds b₂ . <*x*> = x ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines buf1 GFACIRC1:def 2 :

for b₁ being Function of (1 -tuples_on BOOLEAN ),BOOLEAN holds
( b₁ = buf1 iff for x being Element of BOOLEAN holds b₁ . <*x*> = x );

theorem :: GFACIRC1:2

for x being Element of BOOLEAN holds
( buf1 . <*x*> = x & buf1 . <*x*> = and2 . <*x,x*> & buf1 . <*0 *> = 0 & buf1 . <*1*> = 1 )

proof end;

definition

func and2c -> Function of (2 -tuples_on BOOLEAN ),BOOLEAN means :Def3: :: GFACIRC1:def 3
for x, y being Element of BOOLEAN holds it . <*x,y*> = x '&' ('not' y);
existence
ex b₁ being Function of (2 -tuples_on BOOLEAN ),BOOLEAN st
for x, y being Element of BOOLEAN holds b₁ . <*x,y*> = x '&' ('not' y)

proof end;

uniqueness
for b₁, b₂ being Function of (2 -tuples_on BOOLEAN ),BOOLEAN st ( for x, y being Element of BOOLEAN holds b₁ . <*x,y*> = x '&' ('not' y) ) & ( for x, y being Element of BOOLEAN holds b₂ . <*x,y*> = x '&' ('not' y) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines and2c GFACIRC1:def 3 :

for b₁ being Function of (2 -tuples_on BOOLEAN ),BOOLEAN holds
( b₁ = and2c iff for x, y being Element of BOOLEAN holds b₁ . <*x,y*> = x '&' ('not' y) );

theorem :: GFACIRC1:3

for x, y being Element of BOOLEAN holds
( and2c . <*x,y*> = x '&' ('not' y) & and2c . <*x,y*> = and2a . <*y,x*> & and2c . <*x,y*> = nor2a . <*x,y*> & and2c . <*0 ,0 *> = 0 & and2c . <*0 ,1*> = 0 & and2c . <*1,0 *> = 1 & and2c . <*1,1*> = 0 )

proof end;

definition

func xor2c -> Function of (2 -tuples_on BOOLEAN ),BOOLEAN means :Def4: :: GFACIRC1:def 4
for x, y being Element of BOOLEAN holds it . <*x,y*> = x 'xor' ('not' y);
existence
ex b₁ being Function of (2 -tuples_on BOOLEAN ),BOOLEAN st
for x, y being Element of BOOLEAN holds b₁ . <*x,y*> = x 'xor' ('not' y)

proof end;

uniqueness
for b₁, b₂ being Function of (2 -tuples_on BOOLEAN ),BOOLEAN st ( for x, y being Element of BOOLEAN holds b₁ . <*x,y*> = x 'xor' ('not' y) ) & ( for x, y being Element of BOOLEAN holds b₂ . <*x,y*> = x 'xor' ('not' y) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines xor2c GFACIRC1:def 4 :

for b₁ being Function of (2 -tuples_on BOOLEAN ),BOOLEAN holds
( b₁ = xor2c iff for x, y being Element of BOOLEAN holds b₁ . <*x,y*> = x 'xor' ('not' y) );

theorem Th4: :: GFACIRC1:4

for x, y being Element of BOOLEAN holds
( xor2c . <*x,y*> = x 'xor' ('not' y) & xor2c . <*x,y*> = xor2a . <*x,y*> & xor2c . <*x,y*> = or2 . <*(and2b . <*x,y*>),(and2 . <*x,y*>)*> & xor2c . <*0 ,0 *> = 1 & xor2c . <*0 ,1*> = 0 & xor2c . <*1,0 *> = 0 & xor2c . <*1,1*> = 1 )

proof end;

theorem :: GFACIRC1:5

canceled;

theorem :: GFACIRC1:6

for x, y being Element of BOOLEAN holds
( inv1 . <*(xor2 . <*x,y*>)*> = xor2a . <*x,y*> & inv1 . <*(xor2 . <*x,y*>)*> = xor2c . <*x,y*> & xor2 . <*(inv1 . <*x*>),(inv1 . <*y*>)*> = xor2 . <*x,y*> )

proof end;

theorem :: GFACIRC1:7

canceled;

theorem :: GFACIRC1:8

for x, y, z being Element of BOOLEAN holds inv1 . <*(xor2 . <*(xor2c . <*x,y*>),z*>)*> = xor2c . <*(xor2c . <*x,y*>),z*>

proof end;

theorem :: GFACIRC1:9

for x, y, z being Element of BOOLEAN holds (('not' x) 'xor' y) 'xor' ('not' z) = (x 'xor' ('not' y)) 'xor' ('not' z) ;

theorem :: GFACIRC1:10

for x, y, z being Element of BOOLEAN holds xor2c . <*(xor2a . <*x,y*>),z*> = xor2c . <*(xor2c . <*x,y*>),z*> by Th4;

theorem :: GFACIRC1:11

canceled;

theorem :: GFACIRC1:12

for x, y, z being Element of BOOLEAN holds inv1 . <*(xor2c . <*(xor2b . <*x,y*>),z*>)*> = xor2 . <*(xor2 . <*x,y*>),z*>

proof end;

Lm1: for f1, f2, f3 being Function of (2 -tuples_on BOOLEAN ),BOOLEAN
for x, y, z being set st x <> [<*y,z*>,f2] & y <> [<*z,x*>,f3] & z <> [<*x,y*>,f1] holds
( not [<*x,y*>,f1] in {y,z} & not z in {[<*x,y*>,f1],[<*y,z*>,f2]} & not x in {[<*x,y*>,f1],[<*y,z*>,f2]} & not [<*z,x*>,f3] in {x,y,z} )

proof end;

Lm2: for f1, f2, f3 being Function of (2 -tuples_on BOOLEAN ),BOOLEAN
for f4 being Function of (3 -tuples_on BOOLEAN ),BOOLEAN
for x, y, z being set holds {x,y,z} \ {[<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>,f4]} = {x,y,z}

proof end;

Lm3: for f being Function of (2 -tuples_on BOOLEAN ),BOOLEAN
for x, y, c being set st c <> [<*x,y*>,f] holds
for s being State of (2GatesCircuit x,y,c,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;

definition

let x, y, z be set ;
func GFA0CarryIStr x,y,z -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: GFACIRC1:def 5
((1GateCircStr <*x,y*>,and2 ) +* (1GateCircStr <*y,z*>,and2 )) +* (1GateCircStr <*z,x*>,and2 );
coherence
((1GateCircStr <*x,y*>,and2 ) +* (1GateCircStr <*y,z*>,and2 )) +* (1GateCircStr <*z,x*>,and2 ) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;

end;

:: deftheorem defines GFA0CarryIStr GFACIRC1:def 5 :

for x, y, z being set holds GFA0CarryIStr x,y,z = ((1GateCircStr <*x,y*>,and2 ) +* (1GateCircStr <*y,z*>,and2 )) +* (1GateCircStr <*z,x*>,and2 );

definition

let x, y, z be set ;
func GFA0CarryICirc x,y,z -> strict gate`2=den Boolean Circuit of GFA0CarryIStr x,y,z equals :: GFACIRC1:def 6
((1GateCircuit x,y,and2 ) +* (1GateCircuit y,z,and2 )) +* (1GateCircuit z,x,and2 );
coherence
((1GateCircuit x,y,and2 ) +* (1GateCircuit y,z,and2 )) +* (1GateCircuit z,x,and2 ) is strict gate`2=den Boolean Circuit of GFA0CarryIStr x,y,z ;

end;

:: deftheorem defines GFA0CarryICirc GFACIRC1:def 6 :

for x, y, z being set holds GFA0CarryICirc x,y,z = ((1GateCircuit x,y,and2 ) +* (1GateCircuit y,z,and2 )) +* (1GateCircuit z,x,and2 );

definition

let x, y, z be set ;
func GFA0CarryStr x,y,z -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: GFACIRC1:def 7
(GFA0CarryIStr x,y,z) +* (1GateCircStr <*[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]*>,or3 );
coherence
(GFA0CarryIStr x,y,z) +* (1GateCircStr <*[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]*>,or3 ) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;

end;

:: deftheorem defines GFA0CarryStr GFACIRC1:def 7 :

for x, y, z being set holds GFA0CarryStr x,y,z = (GFA0CarryIStr x,y,z) +* (1GateCircStr <*[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]*>,or3 );

definition

let x, y, z be set ;
func GFA0CarryCirc x,y,z -> strict gate`2=den Boolean Circuit of GFA0CarryStr x,y,z equals :: GFACIRC1:def 8
(GFA0CarryICirc x,y,z) +* (1GateCircuit [<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ],or3 );
coherence
(GFA0CarryICirc x,y,z) +* (1GateCircuit [<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ],or3 ) is strict gate`2=den Boolean Circuit of GFA0CarryStr x,y,z ;

end;

:: deftheorem defines GFA0CarryCirc GFACIRC1:def 8 :

for x, y, z being set holds GFA0CarryCirc x,y,z = (GFA0CarryICirc x,y,z) +* (1GateCircuit [<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ],or3 );

definition

let x, y, z be set ;
func GFA0CarryOutput x,y,z -> Element of InnerVertices (GFA0CarryStr x,y,z) equals :: GFACIRC1:def 9
[<*[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]*>,or3 ];
coherence
[<*[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]*>,or3 ] is Element of InnerVertices (GFA0CarryStr x,y,z)

proof end;

end;

:: deftheorem defines GFA0CarryOutput GFACIRC1:def 9 :

for x, y, z being set holds GFA0CarryOutput x,y,z = [<*[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]*>,or3 ];

theorem Th13: :: GFACIRC1:13

for x, y, z being set holds InnerVertices (GFA0CarryIStr x,y,z) = {[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]}

proof end;

theorem Th14: :: GFACIRC1:14

for x, y, z being set holds InnerVertices (GFA0CarryStr x,y,z) = {[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]} \/ {(GFA0CarryOutput x,y,z)}

proof end;

theorem Th15: :: GFACIRC1:15

for x, y, z being set holds InnerVertices (GFA0CarryStr x,y,z) is Relation

proof end;

theorem Th16: :: GFACIRC1:16

for x, y, z being set st x <> [<*y,z*>,and2 ] & y <> [<*z,x*>,and2 ] & z <> [<*x,y*>,and2 ] holds
InputVertices (GFA0CarryIStr x,y,z) = {x,y,z}

proof end;

theorem Th17: :: GFACIRC1:17

for x, y, z being set st x <> [<*y,z*>,and2 ] & y <> [<*z,x*>,and2 ] & z <> [<*x,y*>,and2 ] holds
InputVertices (GFA0CarryStr x,y,z) = {x,y,z}

proof end;

theorem :: GFACIRC1:18

for x, y, z being non pair set holds not InputVertices (GFA0CarryStr x,y,z) is with_pair

proof end;

theorem Th19: :: GFACIRC1:19

for x, y, z being set holds
( x in the carrier of (GFA0CarryStr x,y,z) & y in the carrier of (GFA0CarryStr x,y,z) & z in the carrier of (GFA0CarryStr x,y,z) & [<*x,y*>,and2 ] in the carrier of (GFA0CarryStr x,y,z) & [<*y,z*>,and2 ] in the carrier of (GFA0CarryStr x,y,z) & [<*z,x*>,and2 ] in the carrier of (GFA0CarryStr x,y,z) & [<*[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]*>,or3 ] in the carrier of (GFA0CarryStr x,y,z) )

proof end;

theorem Th20: :: GFACIRC1:20

for x, y, z being set holds
( [<*x,y*>,and2 ] in InnerVertices (GFA0CarryStr x,y,z) & [<*y,z*>,and2 ] in InnerVertices (GFA0CarryStr x,y,z) & [<*z,x*>,and2 ] in InnerVertices (GFA0CarryStr x,y,z) & GFA0CarryOutput x,y,z in InnerVertices (GFA0CarryStr x,y,z) )

proof end;

theorem Th21: :: GFACIRC1:21

for x, y, z being set st x <> [<*y,z*>,and2 ] & y <> [<*z,x*>,and2 ] & z <> [<*x,y*>,and2 ] holds
( x in InputVertices (GFA0CarryStr x,y,z) & y in InputVertices (GFA0CarryStr x,y,z) & z in InputVertices (GFA0CarryStr x,y,z) )

proof end;

theorem Th22: :: GFACIRC1:22

for x, y, z being non pair set holds InputVertices (GFA0CarryStr x,y,z) = {x,y,z}

proof end;

theorem Th23: :: GFACIRC1:23

for x, y, z being set
for s being State of (GFA0CarryCirc x,y,z)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . z holds
( (Following s) . [<*x,y*>,and2 ] = a1 '&' a2 & (Following s) . [<*y,z*>,and2 ] = a2 '&' a3 & (Following s) . [<*z,x*>,and2 ] = a3 '&' a1 )

proof end;

theorem Th24: :: GFACIRC1:24

for x, y, z being set
for s being State of (GFA0CarryCirc x,y,z)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . [<*x,y*>,and2 ] & a2 = s . [<*y,z*>,and2 ] & a3 = s . [<*z,x*>,and2 ] holds
(Following s) . (GFA0CarryOutput x,y,z) = (a1 'or' a2) 'or' a3

proof end;

theorem Th25: :: GFACIRC1:25

for x, y, z being set st x <> [<*y,z*>,and2 ] & y <> [<*z,x*>,and2 ] & z <> [<*x,y*>,and2 ] holds
for s being State of (GFA0CarryCirc x,y,z)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . z holds
( (Following s,2) . (GFA0CarryOutput x,y,z) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1) & (Following s,2) . [<*x,y*>,and2 ] = a1 '&' a2 & (Following s,2) . [<*y,z*>,and2 ] = a2 '&' a3 & (Following s,2) . [<*z,x*>,and2 ] = a3 '&' a1 )

proof end;

theorem Th26: :: GFACIRC1:26

for x, y, z being set st x <> [<*y,z*>,and2 ] & y <> [<*z,x*>,and2 ] & z <> [<*x,y*>,and2 ] holds
for s being State of (GFA0CarryCirc x,y,z) holds Following s,2 is stable

proof end;

definition

let x, y, z be set ;
func GFA0AdderStr x,y,z -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: GFACIRC1:def 10
2GatesCircStr x,y,z,xor2 ;
coherence
2GatesCircStr x,y,z,xor2 is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;

end;

:: deftheorem defines GFA0AdderStr GFACIRC1:def 10 :

for x, y, z being set holds GFA0AdderStr x,y,z = 2GatesCircStr x,y,z,xor2 ;

definition

let x, y, z be set ;
func GFA0AdderCirc x,y,z -> strict gate`2=den Boolean Circuit of GFA0AdderStr x,y,z equals :: GFACIRC1:def 11
2GatesCircuit x,y,z,xor2 ;
coherence
2GatesCircuit x,y,z,xor2 is strict gate`2=den Boolean Circuit of GFA0AdderStr x,y,z ;

end;

:: deftheorem defines GFA0AdderCirc GFACIRC1:def 11 :

for x, y, z being set holds GFA0AdderCirc x,y,z = 2GatesCircuit x,y,z,xor2 ;

definition

let x, y, z be set ;
func GFA0AdderOutput x,y,z -> Element of InnerVertices (GFA0AdderStr x,y,z) equals :: GFACIRC1:def 12
2GatesCircOutput x,y,z,xor2 ;
coherence
2GatesCircOutput x,y,z,xor2 is Element of InnerVertices (GFA0AdderStr x,y,z) ;

end;

:: deftheorem defines GFA0AdderOutput GFACIRC1:def 12 :

for x, y, z being set holds GFA0AdderOutput x,y,z = 2GatesCircOutput x,y,z,xor2 ;

theorem Th27: :: GFACIRC1:27

for x, y, z being set holds InnerVertices (GFA0AdderStr x,y,z) = {[<*x,y*>,xor2 ]} \/ {(GFA0AdderOutput x,y,z)}

proof end;

theorem :: GFACIRC1:28

canceled;

theorem :: GFACIRC1:29

canceled;

theorem :: GFACIRC1:30

canceled;

theorem :: GFACIRC1:31

for x, y, z being set holds
( x in the carrier of (GFA0AdderStr x,y,z) & y in the carrier of (GFA0AdderStr x,y,z) & z in the carrier of (GFA0AdderStr x,y,z) & [<*x,y*>,xor2 ] in the carrier of (GFA0AdderStr x,y,z) & [<*[<*x,y*>,xor2 ],z*>,xor2 ] in the carrier of (GFA0AdderStr x,y,z) ) by FACIRC_1:60, FACIRC_1:61;

theorem Th32: :: GFACIRC1:32

for x, y, z being set holds
( [<*x,y*>,xor2 ] in InnerVertices (GFA0AdderStr x,y,z) & GFA0AdderOutput x,y,z in InnerVertices (GFA0AdderStr x,y,z) )

proof end;

theorem Th33: :: GFACIRC1:33

for x, y, z being set st z <> [<*x,y*>,xor2 ] holds
( x in InputVertices (GFA0AdderStr x,y,z) & y in InputVertices (GFA0AdderStr x,y,z) & z in InputVertices (GFA0AdderStr x,y,z) )

proof end;

theorem :: GFACIRC1:34

canceled;

theorem Th35: :: GFACIRC1:35

for x, y, z being set st z <> [<*x,y*>,xor2 ] holds
for s being State of (GFA0AdderCirc x,y,z)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . z holds
( (Following s) . [<*x,y*>,xor2 ] = a1 'xor' a2 & (Following s) . x = a1 & (Following s) . y = a2 & (Following s) . z = a3 )

proof end;

theorem Th36: :: GFACIRC1:36

for x, y, z being set st z <> [<*x,y*>,xor2 ] holds
for s being State of (GFA0AdderCirc x,y,z)
for a1a2, a1, a2, a3 being Element of BOOLEAN st a1a2 = s . [<*x,y*>,xor2 ] & a3 = s . z holds
(Following s) . (GFA0AdderOutput x,y,z) = a1a2 'xor' a3

proof end;

theorem Th37: :: GFACIRC1:37

for x, y, z being set st z <> [<*x,y*>,xor2 ] holds
for s being State of (GFA0AdderCirc x,y,z)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . z holds
( (Following s,2) . (GFA0AdderOutput x,y,z) = (a1 'xor' a2) 'xor' a3 & (Following s,2) . [<*x,y*>,xor2 ] = a1 'xor' a2 & (Following s,2) . x = a1 & (Following s,2) . y = a2 & (Following s,2) . z = a3 )

proof end;

definition

let x, y, z be set ;
func BitGFA0Str x,y,z -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: GFACIRC1:def 13
(GFA0AdderStr x,y,z) +* (GFA0CarryStr x,y,z);
coherence
(GFA0AdderStr x,y,z) +* (GFA0CarryStr x,y,z) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;

end;

:: deftheorem defines BitGFA0Str GFACIRC1:def 13 :

for x, y, z being set holds BitGFA0Str x,y,z = (GFA0AdderStr x,y,z) +* (GFA0CarryStr x,y,z);

definition

let x, y, z be set ;
func BitGFA0Circ x,y,z -> strict gate`2=den Boolean Circuit of BitGFA0Str x,y,z equals :: GFACIRC1:def 14
(GFA0AdderCirc x,y,z) +* (GFA0CarryCirc x,y,z);
coherence
(GFA0AdderCirc x,y,z) +* (GFA0CarryCirc x,y,z) is strict gate`2=den Boolean Circuit of BitGFA0Str x,y,z ;

end;

:: deftheorem defines BitGFA0Circ GFACIRC1:def 14 :

for x, y, z being set holds BitGFA0Circ x,y,z = (GFA0AdderCirc x,y,z) +* (GFA0CarryCirc x,y,z);

theorem :: GFACIRC1:38

canceled;

theorem Th39: :: GFACIRC1:39

for x, y, z being set holds InnerVertices (BitGFA0Str x,y,z) = (({[<*x,y*>,xor2 ]} \/ {(GFA0AdderOutput x,y,z)}) \/ {[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]}) \/ {(GFA0CarryOutput x,y,z)}

proof end;

theorem :: GFACIRC1:40

for x, y, z being set holds InnerVertices (BitGFA0Str x,y,z) is Relation

proof end;

theorem Th41: :: GFACIRC1:41

for x, y, z being set st z <> [<*x,y*>,xor2 ] & x <> [<*y,z*>,and2 ] & y <> [<*z,x*>,and2 ] & z <> [<*x,y*>,and2 ] holds
InputVertices (BitGFA0Str x,y,z) = {x,y,z}

proof end;

theorem Th42: :: GFACIRC1:42

for x, y, z being non pair set holds InputVertices (BitGFA0Str x,y,z) = {x,y,z}

proof end;

theorem :: GFACIRC1:43

for x, y, z being non pair set holds not InputVertices (BitGFA0Str x,y,z) is with_pair

proof end;

theorem :: GFACIRC1:44

for x, y, z being set holds
( x in the carrier of (BitGFA0Str x,y,z) & y in the carrier of (BitGFA0Str x,y,z) & z in the carrier of (BitGFA0Str x,y,z) & [<*x,y*>,xor2 ] in the carrier of (BitGFA0Str x,y,z) & [<*[<*x,y*>,xor2 ],z*>,xor2 ] in the carrier of (BitGFA0Str x,y,z) & [<*x,y*>,and2 ] in the carrier of (BitGFA0Str x,y,z) & [<*y,z*>,and2 ] in the carrier of (BitGFA0Str x,y,z) & [<*z,x*>,and2 ] in the carrier of (BitGFA0Str x,y,z) & [<*[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]*>,or3 ] in the carrier of (BitGFA0Str x,y,z) )

proof end;

theorem Th45: :: GFACIRC1:45

for x, y, z being set holds
( [<*x,y*>,xor2 ] in InnerVertices (BitGFA0Str x,y,z) & GFA0AdderOutput x,y,z in InnerVertices (BitGFA0Str x,y,z) & [<*x,y*>,and2 ] in InnerVertices (BitGFA0Str x,y,z) & [<*y,z*>,and2 ] in InnerVertices (BitGFA0Str x,y,z) & [<*z,x*>,and2 ] in InnerVertices (BitGFA0Str x,y,z) & GFA0CarryOutput x,y,z in InnerVertices (BitGFA0Str x,y,z) )

proof end;

theorem :: GFACIRC1:46

for x, y, z being set st z <> [<*x,y*>,xor2 ] & x <> [<*y,z*>,and2 ] & y <> [<*z,x*>,and2 ] & z <> [<*x,y*>,and2 ] holds
( x in InputVertices (BitGFA0Str x,y,z) & y in InputVertices (BitGFA0Str x,y,z) & z in InputVertices (BitGFA0Str x,y,z) )

proof end;

definition

let x, y, z be set ;
func BitGFA0CarryOutput x,y,z -> Element of InnerVertices (BitGFA0Str x,y,z) equals :: GFACIRC1:def 15
[<*[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]*>,or3 ];
coherence
[<*[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]*>,or3 ] is Element of InnerVertices (BitGFA0Str x,y,z)

proof end;

end;

:: deftheorem defines BitGFA0CarryOutput GFACIRC1:def 15 :

for x, y, z being set holds BitGFA0CarryOutput x,y,z = [<*[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]*>,or3 ];

definition

let x, y, z be set ;
func BitGFA0AdderOutput x,y,z -> Element of InnerVertices (BitGFA0Str x,y,z) equals :: GFACIRC1:def 16
2GatesCircOutput x,y,z,xor2 ;
coherence
2GatesCircOutput x,y,z,xor2 is Element of InnerVertices (BitGFA0Str x,y,z)

proof end;

end;

:: deftheorem defines BitGFA0AdderOutput GFACIRC1:def 16 :

for x, y, z being set holds BitGFA0AdderOutput x,y,z = 2GatesCircOutput x,y,z,xor2 ;

theorem :: GFACIRC1:47

for x, y, z being set st z <> [<*x,y*>,xor2 ] & x <> [<*y,z*>,and2 ] & y <> [<*z,x*>,and2 ] & z <> [<*x,y*>,and2 ] holds
for s being State of (BitGFA0Circ x,y,z)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . z holds
( (Following s,2) . (GFA0AdderOutput x,y,z) = (a1 'xor' a2) 'xor' a3 & (Following s,2) . (GFA0CarryOutput x,y,z) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1) )

proof end;

theorem :: GFACIRC1:48

for x, y, z being set st z <> [<*x,y*>,xor2 ] & x <> [<*y,z*>,and2 ] & y <> [<*z,x*>,and2 ] & z <> [<*x,y*>,and2 ] holds
for s being State of (BitGFA0Circ x,y,z) holds Following s,2 is stable

proof end;

definition

let x, y, z be set ;
func GFA1CarryIStr x,y,z -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: GFACIRC1:def 17
((1GateCircStr <*x,y*>,and2c ) +* (1GateCircStr <*y,z*>,and2a )) +* (1GateCircStr <*z,x*>,and2 );
coherence
((1GateCircStr <*x,y*>,and2c ) +* (1GateCircStr <*y,z*>,and2a )) +* (1GateCircStr <*z,x*>,and2 ) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;

end;

:: deftheorem defines GFA1CarryIStr GFACIRC1:def 17 :

for x, y, z being set holds GFA1CarryIStr x,y,z = ((1GateCircStr <*x,y*>,and2c ) +* (1GateCircStr <*y,z*>,and2a )) +* (1GateCircStr <*z,x*>,and2 );

definition

let x, y, z be set ;
func GFA1CarryICirc x,y,z -> strict gate`2=den Boolean Circuit of GFA1CarryIStr x,y,z equals :: GFACIRC1:def 18
((1GateCircuit x,y,and2c ) +* (1GateCircuit y,z,and2a )) +* (1GateCircuit z,x,and2 );
coherence
((1GateCircuit x,y,and2c ) +* (1GateCircuit y,z,and2a )) +* (1GateCircuit z,x,and2 ) is strict gate`2=den Boolean Circuit of GFA1CarryIStr x,y,z ;

end;

:: deftheorem defines GFA1CarryICirc GFACIRC1:def 18 :

for x, y, z being set holds GFA1CarryICirc x,y,z = ((1GateCircuit x,y,and2c ) +* (1GateCircuit y,z,and2a )) +* (1GateCircuit z,x,and2 );

definition

let x, y, z be set ;
func GFA1CarryStr x,y,z -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: GFACIRC1:def 19
(GFA1CarryIStr x,y,z) +* (1GateCircStr <*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 );
coherence
(GFA1CarryIStr x,y,z) +* (1GateCircStr <*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 ) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;

end;

:: deftheorem defines GFA1CarryStr GFACIRC1:def 19 :

for x, y, z being set holds GFA1CarryStr x,y,z = (GFA1CarryIStr x,y,z) +* (1GateCircStr <*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 );

definition

let x, y, z be set ;
func GFA1CarryCirc x,y,z -> strict gate`2=den Boolean Circuit of GFA1CarryStr x,y,z equals :: GFACIRC1:def 20
(GFA1CarryICirc x,y,z) +* (1GateCircuit [<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ],or3 );
coherence
(GFA1CarryICirc x,y,z) +* (1GateCircuit [<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ],or3 ) is strict gate`2=den Boolean Circuit of GFA1CarryStr x,y,z ;

end;

:: deftheorem defines GFA1CarryCirc GFACIRC1:def 20 :

for x, y, z being set holds GFA1CarryCirc x,y,z = (GFA1CarryICirc x,y,z) +* (1GateCircuit [<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ],or3 );

definition

let x, y, z be set ;
func GFA1CarryOutput x,y,z -> Element of InnerVertices (GFA1CarryStr x,y,z) equals :: GFACIRC1:def 21
[<*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 ];
coherence
[<*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 ] is Element of InnerVertices (GFA1CarryStr x,y,z)

proof end;

end;

:: deftheorem defines GFA1CarryOutput GFACIRC1:def 21 :

for x, y, z being set holds GFA1CarryOutput x,y,z = [<*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 ];

theorem Th49: :: GFACIRC1:49

for x, y, z being set holds InnerVertices (GFA1CarryIStr x,y,z) = {[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]}

proof end;

theorem Th50: :: GFACIRC1:50

for x, y, z being set holds InnerVertices (GFA1CarryStr x,y,z) = {[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]} \/ {(GFA1CarryOutput x,y,z)}

proof end;

theorem Th51: :: GFACIRC1:51

for x, y, z being set holds InnerVertices (GFA1CarryStr x,y,z) is Relation

proof end;

theorem Th52: :: GFACIRC1:52

for x, y, z being set st x <> [<*y,z*>,and2a ] & y <> [<*z,x*>,and2 ] & z <> [<*x,y*>,and2c ] holds
InputVertices (GFA1CarryIStr x,y,z) = {x,y,z}

proof end;

theorem Th53: :: GFACIRC1:53

for x, y, z being set st x <> [<*y,z*>,and2a ] & y <> [<*z,x*>,and2 ] & z <> [<*x,y*>,and2c ] holds
InputVertices (GFA1CarryStr x,y,z) = {x,y,z}

proof end;

theorem :: GFACIRC1:54

for x, y, z being non pair set holds not InputVertices (GFA1CarryStr x,y,z) is with_pair

proof end;

theorem Th55: :: GFACIRC1:55

for x, y, z being set holds
( x in the carrier of (GFA1CarryStr x,y,z) & y in the carrier of (GFA1CarryStr x,y,z) & z in the carrier of (GFA1CarryStr x,y,z) & [<*x,y*>,and2c ] in the carrier of (GFA1CarryStr x,y,z) & [<*y,z*>,and2a ] in the carrier of (GFA1CarryStr x,y,z) & [<*z,x*>,and2 ] in the carrier of (GFA1CarryStr x,y,z) & [<*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 ] in the carrier of (GFA1CarryStr x,y,z) )

proof end;

theorem Th56: :: GFACIRC1:56

for x, y, z being set holds
( [<*x,y*>,and2c ] in InnerVertices (GFA1CarryStr x,y,z) & [<*y,z*>,and2a ] in InnerVertices (GFA1CarryStr x,y,z) & [<*z,x*>,and2 ] in InnerVertices (GFA1CarryStr x,y,z) & GFA1CarryOutput x,y,z in InnerVertices (GFA1CarryStr x,y,z) )

proof end;

theorem Th57: :: GFACIRC1:57

for x, y, z being set st x <> [<*y,z*>,and2a ] & y <> [<*z,x*>,and2 ] & z <> [<*x,y*>,and2c ] holds
( x in InputVertices (GFA1CarryStr x,y,z) & y in InputVertices (GFA1CarryStr x,y,z) & z in InputVertices (GFA1CarryStr x,y,z) )

proof end;

theorem Th58: :: GFACIRC1:58

for x, y, z being non pair set holds InputVertices (GFA1CarryStr x,y,z) = {x,y,z}

proof end;

theorem Th59: :: GFACIRC1:59

for x, y, z being set
for s being State of (GFA1CarryCirc x,y,z)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . z holds
( (Following s) . [<*x,y*>,and2c ] = a1 '&' ('not' a2) & (Following s) . [<*y,z*>,and2a ] = ('not' a2) '&' a3 & (Following s) . [<*z,x*>,and2 ] = a3 '&' a1 )

proof end;

theorem Th60: :: GFACIRC1:60

for x, y, z being set
for s being State of (GFA1CarryCirc x,y,z)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . [<*x,y*>,and2c ] & a2 = s . [<*y,z*>,and2a ] & a3 = s . [<*z,x*>,and2 ] holds
(Following s) . (GFA1CarryOutput x,y,z) = (a1 'or' a2) 'or' a3

proof end;

theorem Th61: :: GFACIRC1:61

for x, y, z being set st x <> [<*y,z*>,and2a ] & y <> [<*z,x*>,and2 ] & z <> [<*x,y*>,and2c ] holds
for s being State of (GFA1CarryCirc x,y,z)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . z holds
( (Following s,2) . (GFA1CarryOutput x,y,z) = ((a1 '&' ('not' a2)) 'or' (('not' a2) '&' a3)) 'or' (a3 '&' a1) & (Following s,2) . [<*x,y*>,and2c ] = a1 '&' ('not' a2) & (Following s,2) . [<*y,z*>,and2a ] = ('not' a2) '&' a3 & (Following s,2) . [<*z,x*>,and2 ] = a3 '&' a1 )

proof end;

theorem Th62: :: GFACIRC1:62

for x, y, z being set st x <> [<*y,z*>,and2a ] & y <> [<*z,x*>,and2 ] & z <> [<*x,y*>,and2c ] holds
for s being State of (GFA1CarryCirc x,y,z) holds Following s,2 is stable

proof end;

definition

let x, y, z be set ;
func GFA1AdderStr x,y,z -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: GFACIRC1:def 22
2GatesCircStr x,y,z,xor2c ;
coherence
2GatesCircStr x,y,z,xor2c is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;

end;

:: deftheorem defines GFA1AdderStr GFACIRC1:def 22 :

for x, y, z being set holds GFA1AdderStr x,y,z = 2GatesCircStr x,y,z,xor2c ;

definition

let x, y, z be set ;
func GFA1AdderCirc x,y,z -> strict gate`2=den Boolean Circuit of GFA1AdderStr x,y,z equals :: GFACIRC1:def 23
2GatesCircuit x,y,z,xor2c ;
coherence
2GatesCircuit x,y,z,xor2c is strict gate`2=den Boolean Circuit of GFA1AdderStr x,y,z ;

end;

:: deftheorem defines GFA1AdderCirc GFACIRC1:def 23 :

for x, y, z being set holds GFA1AdderCirc x,y,z = 2GatesCircuit x,y,z,xor2c ;

definition

let x, y, z be set ;
func GFA1AdderOutput x,y,z -> Element of InnerVertices (GFA1AdderStr x,y,z) equals :: GFACIRC1:def 24
2GatesCircOutput x,y,z,xor2c ;
coherence
2GatesCircOutput x,y,z,xor2c is Element of InnerVertices (GFA1AdderStr x,y,z) ;

end;

:: deftheorem defines GFA1AdderOutput GFACIRC1:def 24 :

for x, y, z being set holds GFA1AdderOutput x,y,z = 2GatesCircOutput x,y,z,xor2c ;

theorem Th63: :: GFACIRC1:63

for x, y, z being set holds InnerVertices (GFA1AdderStr x,y,z) = {[<*x,y*>,xor2c ]} \/ {(GFA1AdderOutput x,y,z)}

proof end;

theorem :: GFACIRC1:64

canceled;

theorem :: GFACIRC1:65

canceled;

theorem :: GFACIRC1:66

canceled;

theorem :: GFACIRC1:67

for x, y, z being set holds
( x in the carrier of (GFA1AdderStr x,y,z) & y in the carrier of (GFA1AdderStr x,y,z) & z in the carrier of (GFA1AdderStr x,y,z) & [<*x,y*>,xor2c ] in the carrier of (GFA1AdderStr x,y,z) & [<*[<*x,y*>,xor2c ],z*>,xor2c ] in the carrier of (GFA1AdderStr x,y,z) ) by FACIRC_1:60, FACIRC_1:61;

theorem Th68: :: GFACIRC1:68

for x, y, z being set holds
( [<*x,y*>,xor2c ] in InnerVertices (GFA1AdderStr x,y,z) & GFA1AdderOutput x,y,z in InnerVertices (GFA1AdderStr x,y,z) )

proof end;

theorem Th69: :: GFACIRC1:69

for x, y, z being set st z <> [<*x,y*>,xor2c ] holds
( x in InputVertices (GFA1AdderStr x,y,z) & y in InputVertices (GFA1AdderStr x,y,z) & z in InputVertices (GFA1AdderStr x,y,z) )

proof end;

theorem :: GFACIRC1:70

canceled;

theorem Th71: :: GFACIRC1:71

for x, y, z being set st z <> [<*x,y*>,xor2c ] holds
for s being State of (GFA1AdderCirc x,y,z)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . z holds
( (Following s) . [<*x,y*>,xor2c ] = a1 'xor' ('not' a2) & (Following s) . x = a1 & (Following s) . y = a2 & (Following s) . z = a3 )

proof end;

theorem Th72: :: GFACIRC1:72

for x, y, z being set st z <> [<*x,y*>,xor2c ] holds
for s being State of (GFA1AdderCirc x,y,z)
for a1a2, a1, a2, a3 being Element of BOOLEAN st a1a2 = s . [<*x,y*>,xor2c ] & a3 = s . z holds
(Following s) . (GFA1AdderOutput x,y,z) = a1a2 'xor' ('not' a3)

proof end;

theorem Th73: :: GFACIRC1:73

for x, y, z being set st z <> [<*x,y*>,xor2c ] holds
for s being State of (GFA1AdderCirc x,y,z)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . z holds
( (Following s,2) . (GFA1AdderOutput x,y,z) = (a1 'xor' ('not' a2)) 'xor' ('not' a3) & (Following s,2) . [<*x,y*>,xor2c ] = a1 'xor' ('not' a2) & (Following s,2) . x = a1 & (Following s,2) . y = a2 & (Following s,2) . z = a3 )

proof end;

theorem Th74: :: GFACIRC1:74

for x, y, z being set st z <> [<*x,y*>,xor2c ] holds
for s being State of (GFA1AdderCirc x,y,z)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . z holds
(Following s,2) . (GFA1AdderOutput x,y,z) = 'not' ((a1 'xor' ('not' a2)) 'xor' a3)

proof end;

definition

let x, y, z be set ;
func BitGFA1Str x,y,z -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: GFACIRC1:def 25
(GFA1AdderStr x,y,z) +* (GFA1CarryStr x,y,z);
coherence
(GFA1AdderStr x,y,z) +* (GFA1CarryStr x,y,z) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;

end;

:: deftheorem defines BitGFA1Str GFACIRC1:def 25 :

for x, y, z being set holds BitGFA1Str x,y,z = (GFA1AdderStr x,y,z) +* (GFA1CarryStr x,y,z);

definition

let x, y, z be set ;
func BitGFA1Circ x,y,z -> strict gate`2=den Boolean Circuit of BitGFA1Str x,y,z equals :: GFACIRC1:def 26
(GFA1AdderCirc x,y,z) +* (GFA1CarryCirc x,y,z);
coherence
(GFA1AdderCirc x,y,z) +* (GFA1CarryCirc x,y,z) is strict gate`2=den Boolean Circuit of BitGFA1Str x,y,z ;

end;

:: deftheorem defines BitGFA1Circ GFACIRC1:def 26 :

for x, y, z being set holds BitGFA1Circ x,y,z = (GFA1AdderCirc x,y,z) +* (GFA1CarryCirc x,y,z);

theorem :: GFACIRC1:75

canceled;

theorem Th76: :: GFACIRC1:76

for x, y, z being set holds InnerVertices (BitGFA1Str x,y,z) = (({[<*x,y*>,xor2c ]} \/ {(GFA1AdderOutput x,y,z)}) \/ {[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]}) \/ {(GFA1CarryOutput x,y,z)}

proof end;

theorem :: GFACIRC1:77

for x, y, z being set holds InnerVertices (BitGFA1Str x,y,z) is Relation

proof end;

theorem Th78: :: GFACIRC1:78

for x, y, z being set st z <> [<*x,y*>,xor2c ] & x <> [<*y,z*>,and2a ] & y <> [<*z,x*>,and2 ] & z <> [<*x,y*>,and2c ] holds
InputVertices (BitGFA1Str x,y,z) = {x,y,z}

proof end;

theorem Th79: :: GFACIRC1:79

for x, y, z being non pair set holds InputVertices (BitGFA1Str x,y,z) = {x,y,z}

proof end;

theorem :: GFACIRC1:80

for x, y, z being non pair set holds not InputVertices (BitGFA1Str x,y,z) is with_pair

proof end;

theorem :: GFACIRC1:81

for x, y, z being set holds
( x in the carrier of (BitGFA1Str x,y,z) & y in the carrier of (BitGFA1Str x,y,z) & z in the carrier of (BitGFA1Str x,y,z) & [<*x,y*>,xor2c ] in the carrier of (BitGFA1Str x,y,z) & [<*[<*x,y*>,xor2c ],z*>,xor2c ] in the carrier of (BitGFA1Str x,y,z) & [<*x,y*>,and2c ] in the carrier of (BitGFA1Str x,y,z) & [<*y,z*>,and2a ] in the carrier of (BitGFA1Str x,y,z) & [<*z,x*>,and2 ] in the carrier of (BitGFA1Str x,y,z) & [<*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 ] in the carrier of (BitGFA1Str x,y,z) )

proof end;

theorem Th82: :: GFACIRC1:82

for x, y, z being set holds
( [<*x,y*>,xor2c ] in InnerVertices (BitGFA1Str x,y,z) & GFA1AdderOutput x,y,z in InnerVertices (BitGFA1Str x,y,z) & [<*x,y*>,and2c ] in InnerVertices (BitGFA1Str x,y,z) & [<*y,z*>,and2a ] in InnerVertices (BitGFA1Str x,y,z) & [<*z,x*>,and2 ] in InnerVertices (BitGFA1Str x,y,z) & GFA1CarryOutput x,y,z in InnerVertices (BitGFA1Str x,y,z) )

proof end;

theorem :: GFACIRC1:83

for x, y, z being set st z <> [<*x,y*>,xor2c ] & x <> [<*y,z*>,and2a ] & y <> [<*z,x*>,and2 ] & z <> [<*x,y*>,and2c ] holds
( x in InputVertices (BitGFA1Str x,y,z) & y in InputVertices (BitGFA1Str x,y,z) & z in InputVertices (BitGFA1Str x,y,z) )

proof end;

definition

let x, y, z be set ;
func BitGFA1CarryOutput x,y,z -> Element of InnerVertices (BitGFA1Str x,y,z) equals :: GFACIRC1:def 27
[<*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 ];
coherence
[<*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 ] is Element of InnerVertices (BitGFA1Str x,y,z)

proof end;

end;

:: deftheorem defines BitGFA1CarryOutput GFACIRC1:def 27 :

for x, y, z being set holds BitGFA1CarryOutput x,y,z = [<*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 ];

definition

let x, y, z be set ;
func BitGFA1AdderOutput x,y,z -> Element of InnerVertices (BitGFA1Str x,y,z) equals :: GFACIRC1:def 28
2GatesCircOutput x,y,z,xor2c ;
coherence
2GatesCircOutput x,y,z,xor2c is Element of InnerVertices (BitGFA1Str x,y,z)

proof end;

end;

:: deftheorem defines BitGFA1AdderOutput GFACIRC1:def 28 :

for x, y, z being set holds BitGFA1AdderOutput x,y,z = 2GatesCircOutput x,y,z,xor2c ;

theorem :: GFACIRC1:84

for x, y, z being set st z <> [<*x,y*>,xor2c ] & x <> [<*y,z*>,and2a ] & y <> [<*z,x*>,and2 ] & z <> [<*x,y*>,and2c ] holds
for s being State of (BitGFA1Circ x,y,z)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . z holds
( (Following s,2) . (GFA1AdderOutput x,y,z) = 'not' ((a1 'xor' ('not' a2)) 'xor' a3) & (Following s,2) . (GFA1CarryOutput x,y,z) = ((a1 '&' ('not' a2)) 'or' (('not' a2) '&' a3)) 'or' (a3 '&' a1) )

proof end;

theorem :: GFACIRC1:85

for x, y, z being set st z <> [<*x,y*>,xor2c ] & x <> [<*y,z*>,and2a ] & y <> [<*z,x*>,and2 ] & z <> [<*x,y*>,and2c ] holds
for s being State of (BitGFA1Circ x,y,z) holds Following s,2 is stable

proof end;

definition

let x, y, z be set ;
func GFA2CarryIStr x,y,z -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: GFACIRC1:def 29
((1GateCircStr <*x,y*>,and2a ) +* (1GateCircStr <*y,z*>,and2c )) +* (1GateCircStr <*z,x*>,and2b );
coherence
((1GateCircStr <*x,y*>,and2a ) +* (1GateCircStr <*y,z*>,and2c )) +* (1GateCircStr <*z,x*>,and2b ) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;

end;

:: deftheorem defines GFA2CarryIStr GFACIRC1:def 29 :

for x, y, z being set holds GFA2CarryIStr x,y,z = ((1GateCircStr <*x,y*>,and2a ) +* (1GateCircStr <*y,z*>,and2c )) +* (1GateCircStr <*z,x*>,and2b );

definition

let x, y, z be set ;
func GFA2CarryICirc x,y,z -> strict gate`2=den Boolean Circuit of GFA2CarryIStr x,y,z equals :: GFACIRC1:def 30
((1GateCircuit x,y,and2a ) +* (1GateCircuit y,z,and2c )) +* (1GateCircuit z,x,and2b );
coherence
((1GateCircuit x,y,and2a ) +* (1GateCircuit y,z,and2c )) +* (1GateCircuit z,x,and2b ) is strict gate`2=den Boolean Circuit of GFA2CarryIStr x,y,z ;

end;

:: deftheorem defines GFA2CarryICirc GFACIRC1:def 30 :

for x, y, z being set holds GFA2CarryICirc x,y,z = ((1GateCircuit x,y,and2a ) +* (1GateCircuit y,z,and2c )) +* (1GateCircuit z,x,and2b );

definition

let x, y, z be set ;
func GFA2CarryStr x,y,z -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: GFACIRC1:def 31
(GFA2CarryIStr x,y,z) +* (1GateCircStr <*[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]*>,nor3 );
coherence
(GFA2CarryIStr x,y,z) +* (1GateCircStr <*[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]*>,nor3 ) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;

end;

:: deftheorem defines GFA2CarryStr GFACIRC1:def 31 :

for x, y, z being set holds GFA2CarryStr x,y,z = (GFA2CarryIStr x,y,z) +* (1GateCircStr <*[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]*>,nor3 );

definition

let x, y, z be set ;
func GFA2CarryCirc x,y,z -> strict gate`2=den Boolean Circuit of GFA2CarryStr x,y,z equals :: GFACIRC1:def 32
(GFA2CarryICirc x,y,z) +* (1GateCircuit [<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ],nor3 );
coherence
(GFA2CarryICirc x,y,z) +* (1GateCircuit [<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ],nor3 ) is strict gate`2=den Boolean Circuit of GFA2CarryStr x,y,z ;

end;

:: deftheorem defines GFA2CarryCirc GFACIRC1:def 32 :

for x, y, z being set holds GFA2CarryCirc x,y,z = (GFA2CarryICirc x,y,z) +* (1GateCircuit [<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ],nor3 );

definition

let x, y, z be set ;
func GFA2CarryOutput x,y,z -> Element of InnerVertices (GFA2CarryStr x,y,z) equals :: GFACIRC1:def 33
[<*[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]*>,nor3 ];
coherence
[<*[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]*>,nor3 ] is Element of InnerVertices (GFA2CarryStr x,y,z)

proof end;

end;

:: deftheorem defines GFA2CarryOutput GFACIRC1:def 33 :

for x, y, z being set holds GFA2CarryOutput x,y,z = [<*[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]*>,nor3 ];

theorem Th86: :: GFACIRC1:86

for x, y, z being set holds InnerVertices (GFA2CarryIStr x,y,z) = {[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]}

proof end;

theorem Th87: :: GFACIRC1:87

for x, y, z being set holds InnerVertices (GFA2CarryStr x,y,z) = {[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]} \/ {(GFA2CarryOutput x,y,z)}

proof end;

theorem Th88: :: GFACIRC1:88

for x, y, z being set holds InnerVertices (GFA2CarryStr x,y,z) is Relation

proof end;

theorem Th89: :: GFACIRC1:89

for x, y, z being set st x <> [<*y,z*>,and2c ] & y <> [<*z,x*>,and2b ] & z <> [<*x,y*>,and2a ] holds
InputVertices (GFA2CarryIStr x,y,z) = {x,y,z}

proof end;

theorem Th90: :: GFACIRC1:90

for x, y, z being set st x <> [<*y,z*>,and2c ] & y <> [<*z,x*>,and2b ] & z <> [<*x,y*>,and2a ] holds
InputVertices (GFA2CarryStr x,y,z) = {x,y,z}

proof end;

theorem :: GFACIRC1:91

for x, y, z being non pair set holds not InputVertices (GFA2CarryStr x,y,z) is with_pair

proof end;

theorem Th92: :: GFACIRC1:92

for x, y, z being set holds
( x in the carrier of (GFA2CarryStr x,y,z) & y in the carrier of (GFA2CarryStr x,y,z) & z in the carrier of (GFA2CarryStr x,y,z) & [<*x,y*>,and2a ] in the carrier of (GFA2CarryStr x,y,z) & [<*y,z*>,and2c ] in the carrier of (GFA2CarryStr x,y,z) & [<*z,x*>,and2b ] in the carrier of (GFA2CarryStr x,y,z) & [<*[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]*>,nor3 ] in the carrier of (GFA2CarryStr x,y,z) )

proof end;

theorem Th93: :: GFACIRC1:93

for x, y, z being set holds
( [<*x,y*>,and2a ] in InnerVertices (GFA2CarryStr x,y,z) & [<*y,z*>,and2c ] in InnerVertices (GFA2CarryStr x,y,z) & [<*z,x*>,and2b ] in InnerVertices (GFA2CarryStr x,y,z) & GFA2CarryOutput x,y,z in InnerVertices (GFA2CarryStr x,y,z) )

proof end;

theorem Th94: :: GFACIRC1:94

for x, y, z being set st x <> [<*y,z*>,and2c ] & y <> [<*z,x*>,and2b ] & z <> [<*x,y*>,and2a ] holds
( x in InputVertices (GFA2CarryStr x,y,z) & y in InputVertices (GFA2CarryStr x,y,z) & z in InputVertices (GFA2CarryStr x,y,z) )

proof end;

theorem Th95: :: GFACIRC1:95

for x, y, z being non pair set holds InputVertices (GFA2CarryStr x,y,z) = {x,y,z}

proof end;

theorem Th96: :: GFACIRC1:96

for x, y, z being set
for s being State of (GFA2CarryCirc x,y,z)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . z holds
( (Following s) . [<*x,y*>,and2a ] = ('not' a1) '&' a2 & (Following s) . [<*y,z*>,and2c ] = a2 '&' ('not' a3) & (Following s) . [<*z,x*>,and2b ] = ('not' a3) '&' ('not' a1) )

proof end;

theorem Th97: :: GFACIRC1:97

for x, y, z being set
for s being State of (GFA2CarryCirc x,y,z)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . [<*x,y*>,and2a ] & a2 = s . [<*y,z*>,and2c ] & a3 = s . [<*z,x*>,and2b ] holds
(Following s) . (GFA2CarryOutput x,y,z) = 'not' ((a1 'or' a2) 'or' a3)

proof end;

theorem Th98: :: GFACIRC1:98

for x, y, z being set st x <> [<*y,z*>,and2c ] & y <> [<*z,x*>,and2b ] & z <> [<*x,y*>,and2a ] holds
for s being State of (GFA2CarryCirc x,y,z)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . z holds
( (Following s,2) . (GFA2CarryOutput x,y,z) = 'not' (((('not' a1) '&' a2) 'or' (a2 '&' ('not' a3))) 'or' (('not' a3) '&' ('not' a1))) & (Following s,2) . [<*x,y*>,and2a ] = ('not' a1) '&' a2 & (Following s,2) . [<*y,z*>,and2c ] = a2 '&' ('not' a3) & (Following s,2) . [<*z,x*>,and2b ] = ('not' a3) '&' ('not' a1) )

proof end;

theorem Th99: :: GFACIRC1:99

for x, y, z being set st x <> [<*y,z*>,and2c ] & y <> [<*z,x*>,and2b ] & z <> [<*x,y*>,and2a ] holds
for s being State of (GFA2CarryCirc x,y,z) holds Following s,2 is stable

proof end;

definition

let x, y, z be set ;
func GFA2AdderStr x,y,z -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: GFACIRC1:def 34
2GatesCircStr x,y,z,xor2c ;
coherence
2GatesCircStr x,y,z,xor2c is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;

end;

:: deftheorem defines GFA2AdderStr GFACIRC1:def 34 :

for x, y, z being set holds GFA2AdderStr x,y,z = 2GatesCircStr x,y,z,xor2c ;

definition

let x, y, z be set ;
func GFA2AdderCirc x,y,z -> strict gate`2=den Boolean Circuit of GFA2AdderStr x,y,z equals :: GFACIRC1:def 35
2GatesCircuit x,y,z,xor2c ;
coherence
2GatesCircuit x,y,z,xor2c is strict gate`2=den Boolean Circuit of GFA2AdderStr x,y,z ;

end;

:: deftheorem defines GFA2AdderCirc GFACIRC1:def 35 :

for x, y, z being set holds GFA2AdderCirc x,y,z = 2GatesCircuit x,y,z,xor2c ;

definition

let x, y, z be set ;
func GFA2AdderOutput x,y,z -> Element of InnerVertices (GFA2AdderStr x,y,z) equals :: GFACIRC1:def 36
2GatesCircOutput x,y,z,xor2c ;
coherence
2GatesCircOutput x,y,z,xor2c is Element of InnerVertices (GFA2AdderStr x,y,z) ;

end;

:: deftheorem defines GFA2AdderOutput GFACIRC1:def 36 :

for x, y, z being set holds GFA2AdderOutput x,y,z = 2GatesCircOutput x,y,z,xor2c ;

theorem Th100: :: GFACIRC1:100

for x, y, z being set holds InnerVertices (GFA2AdderStr x,y,z) = {[<*x,y*>,xor2c ]} \/ {(GFA2AdderOutput x,y,z)}

proof end;

theorem :: GFACIRC1:101

canceled;

theorem :: GFACIRC1:102

canceled;

theorem :: GFACIRC1:103

canceled;

theorem :: GFACIRC1:104

for x, y, z being set holds
( x in the carrier of (GFA2AdderStr x,y,z) & y in the carrier of (GFA2AdderStr x,y,z) & z in the carrier of (GFA2AdderStr x,y,z) & [<*x,y*>,xor2c ] in the carrier of (GFA2AdderStr x,y,z) & [<*[<*x,y*>,xor2c ],z*>,xor2c ] in the carrier of (GFA2AdderStr x,y,z) ) by FACIRC_1:60, FACIRC_1:61;

theorem :: GFACIRC1:105

for x, y, z being set holds
( [<*x,y*>,xor2c ] in InnerVertices (GFA2AdderStr x,y,z) & GFA2AdderOutput x,y,z in InnerVertices (GFA2AdderStr x,y,z) )

proof end;

theorem :: GFACIRC1:106

for x, y, z being set st z <> [<*x,y*>,xor2c ] holds
( x in InputVertices (GFA2AdderStr x,y,z) & y in InputVertices (GFA2AdderStr x,y,z) & z in InputVertices (GFA2AdderStr x,y,z) )

proof end;

theorem :: GFACIRC1:107

canceled;

theorem :: GFACIRC1:108

for x, y, z being set st z <> [<*x,y*>,xor2c ] holds
for s being State of (GFA2AdderCirc x,y,z)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . z holds
( (Following s) . [<*x,y*>,xor2c ] = a1 'xor' ('not' a2) & (Following s) . x = a1 & (Following s) . y = a2 & (Following s) . z = a3 )

proof end;

theorem :: GFACIRC1:109

for x, y, z being set st z <> [<*x,y*>,xor2c ] holds
for s being State of (GFA2AdderCirc x,y,z)
for a1a2, a1, a2, a3 being Element of BOOLEAN st a1a2 = s . [<*x,y*>,xor2c ] & a1 = s . x & a2 = s . y & a3 = s . z holds
(Following s) . (GFA2AdderOutput x,y,z) = a1a2 'xor' ('not' a3)

proof end;

theorem Th110: :: GFACIRC1:110

for x, y, z being set st z <> [<*x,y*>,xor2c ] holds
for s being State of (GFA2AdderCirc x,y,z)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . z holds
( (Following s,2) . (GFA2AdderOutput x,y,z) = (a1 'xor' ('not' a2)) 'xor' ('not' a3) & (Following s,2) . [<*x,y*>,xor2c ] = a1 'xor' ('not' a2) & (Following s,2) . x = a1 & (Following s,2) . y = a2 & (Following s,2) . z = a3 )

proof end;

theorem Th111: :: GFACIRC1:111

for x, y, z being set st z <> [<*x,y*>,xor2c ] holds
for s being State of (GFA2AdderCirc x,y,z)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . z holds
(Following s,2) . (GFA2AdderOutput x,y,z) = (('not' a1) 'xor' a2) 'xor' ('not' a3)

proof end;

definition

let x, y, z be set ;
func BitGFA2Str x,y,z -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: GFACIRC1:def 37
(GFA2AdderStr x,y,z) +* (GFA2CarryStr x,y,z);
coherence
(GFA2AdderStr x,y,z) +* (GFA2CarryStr x,y,z) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;

end;

:: deftheorem defines BitGFA2Str GFACIRC1:def 37 :

for x, y, z being set holds BitGFA2Str x,y,z = (GFA2AdderStr x,y,z) +* (GFA2CarryStr x,y,z);

definition

let x, y, z be set ;
func BitGFA2Circ x,y,z -> strict gate`2=den Boolean Circuit of BitGFA2Str x,y,z equals :: GFACIRC1:def 38
(GFA2AdderCirc x,y,z) +* (GFA2CarryCirc x,y,z);
coherence
(GFA2AdderCirc x,y,z) +* (GFA2CarryCirc x,y,z) is strict gate`2=den Boolean Circuit of BitGFA2Str x,y,z ;

end;

:: deftheorem defines BitGFA2Circ GFACIRC1:def 38 :

for x, y, z being set holds BitGFA2Circ x,y,z = (GFA2AdderCirc x,y,z) +* (GFA2CarryCirc x,y,z);

theorem :: GFACIRC1:112

canceled;

theorem Th113: :: GFACIRC1:113

for x, y, z being set holds InnerVertices (BitGFA2Str x,y,z) = (({[<*x,y*>,xor2c ]} \/ {(GFA2AdderOutput x,y,z)}) \/ {[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]}) \/ {(GFA2CarryOutput x,y,z)}

proof end;

theorem :: GFACIRC1:114

for x, y, z being set holds InnerVertices (BitGFA2Str x,y,z) is Relation

proof end;

theorem Th115: :: GFACIRC1:115

for x, y, z being set st z <> [<*x,y*>,xor2c ] & x <> [<*y,z*>,and2c ] & y <> [<*z,x*>,and2b ] & z <> [<*x,y*>,and2a ] holds
InputVertices (BitGFA2Str x,y,z) = {x,y,z}

proof end;

theorem Th116: :: GFACIRC1:116

for x, y, z being non pair set holds InputVertices (BitGFA2Str x,y,z) = {x,y,z}

proof end;

theorem :: GFACIRC1:117

for x, y, z being non pair set holds not InputVertices (BitGFA2Str x,y,z) is with_pair

proof end;

theorem :: GFACIRC1:118

for x, y, z being set holds
( x in the carrier of (BitGFA2Str x,y,z) & y in the carrier of (BitGFA2Str x,y,z) & z in the carrier of (BitGFA2Str x,y,z) & [<*x,y*>,xor2c ] in the carrier of (BitGFA2Str x,y,z) & [<*[<*x,y*>,xor2c ],z*>,xor2c ] in the carrier of (BitGFA2Str x,y,z) & [<*x,y*>,and2a ] in the carrier of (BitGFA2Str x,y,z) & [<*y,z*>,and2c ] in the carrier of (BitGFA2Str x,y,z) & [<*z,x*>,and2b ] in the carrier of (BitGFA2Str x,y,z) & [<*[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]*>,nor3 ] in the carrier of (BitGFA2Str x,y,z) )

proof end;

theorem Th119: :: GFACIRC1:119

for x, y, z being set holds
( [<*x,y*>,xor2c ] in InnerVertices (BitGFA2Str x,y,z) & GFA2AdderOutput x,y,z in InnerVertices (BitGFA2Str x,y,z) & [<*x,y*>,and2a ] in InnerVertices (BitGFA2Str x,y,z) & [<*y,z*>,and2c ] in InnerVertices (BitGFA2Str x,y,z) & [<*z,x*>,and2b ] in InnerVertices (BitGFA2Str x,y,z) & GFA2CarryOutput x,y,z in InnerVertices (BitGFA2Str x,y,z) )

proof end;

theorem :: GFACIRC1:120

for x, y, z being set st z <> [<*x,y*>,xor2c ] & x <> [<*y,z*>,and2c ] & y <> [<*z,x*>,and2b ] & z <> [<*x,y*>,and2a ] holds
( x in InputVertices (BitGFA2Str x,y,z) & y in InputVertices (BitGFA2Str x,y,z) & z in InputVertices (BitGFA2Str x,y,z) )

proof end;

definition

let x, y, z be set ;
func BitGFA2CarryOutput x,y,z -> Element of InnerVertices (BitGFA2Str x,y,z) equals :: GFACIRC1:def 39
[<*[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]*>,nor3 ];
coherence
[<*[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]*>,nor3 ] is Element of InnerVertices (BitGFA2Str x,y,z)

proof end;

end;

:: deftheorem defines BitGFA2CarryOutput GFACIRC1:def 39 :

for x, y, z being set holds BitGFA2CarryOutput x,y,z = [<*[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]*>,nor3 ];

definition

let x, y, z be set ;
func BitGFA2AdderOutput x,y,z -> Element of InnerVertices (BitGFA2Str x,y,z) equals :: GFACIRC1:def 40
2GatesCircOutput x,y,z,xor2c ;
coherence
2GatesCircOutput x,y,z,xor2c is Element of InnerVertices (BitGFA2Str x,y,z)

proof end;

end;

:: deftheorem defines BitGFA2AdderOutput GFACIRC1:def 40 :

for x, y, z being set holds BitGFA2AdderOutput x,y,z = 2GatesCircOutput x,y,z,xor2c ;

theorem :: GFACIRC1:121

for x, y, z being set st z <> [<*x,y*>,xor2c ] & x <> [<*y,z*>,and2c ] & y <> [<*z,x*>,and2b ] & z <> [<*x,y*>,and2a ] holds
for s being State of (BitGFA2Circ x,y,z)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . z holds
( (Following s,2) . (GFA2AdderOutput x,y,z) = (('not' a1) 'xor' a2) 'xor' ('not' a3) & (Following s,2) . (GFA2CarryOutput x,y,z) = 'not' (((('not' a1) '&' a2) 'or' (a2 '&' ('not' a3))) 'or' (('not' a3) '&' ('not' a1))) )

proof end;

theorem :: GFACIRC1:122

for x, y, z being set st z <> [<*x,y*>,xor2c ] & x <> [<*y,z*>,and2c ] & y <> [<*z,x*>,and2b ] & z <> [<*x,y*>,and2a ] holds
for s being State of (BitGFA2Circ x,y,z) holds Following s,2 is stable

proof end;

definition

let x, y, z be set ;
func GFA3CarryIStr x,y,z -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: GFACIRC1:def 41
((1GateCircStr <*x,y*>,and2b ) +* (1GateCircStr <*y,z*>,and2b )) +* (1GateCircStr <*z,x*>,and2b );
coherence
((1GateCircStr <*x,y*>,and2b ) +* (1GateCircStr <*y,z*>,and2b )) +* (1GateCircStr <*z,x*>,and2b ) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;

end;

:: deftheorem defines GFA3CarryIStr GFACIRC1:def 41 :

for x, y, z being set holds GFA3CarryIStr x,y,z = ((1GateCircStr <*x,y*>,and2b ) +* (1GateCircStr <*y,z*>,and2b )) +* (1GateCircStr <*z,x*>,and2b );

definition

let x, y, z be set ;
func GFA3CarryICirc x,y,z -> strict gate`2=den Boolean Circuit of GFA3CarryIStr x,y,z equals :: GFACIRC1:def 42
((1GateCircuit x,y,and2b ) +* (1GateCircuit y,z,and2b )) +* (1GateCircuit z,x,and2b );
coherence
((1GateCircuit x,y,and2b ) +* (1GateCircuit y,z,and2b )) +* (1GateCircuit z,x,and2b ) is strict gate`2=den Boolean Circuit of GFA3CarryIStr x,y,z ;

end;

:: deftheorem defines GFA3CarryICirc GFACIRC1:def 42 :

for x, y, z being set holds GFA3CarryICirc x,y,z = ((1GateCircuit x,y,and2b ) +* (1GateCircuit y,z,and2b )) +* (1GateCircuit z,x,and2b );

definition

let x, y, z be set ;
func GFA3CarryStr x,y,z -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: GFACIRC1:def 43
(GFA3CarryIStr x,y,z) +* (1GateCircStr <*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 );
coherence
(GFA3CarryIStr x,y,z) +* (1GateCircStr <*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;

end;

:: deftheorem defines GFA3CarryStr GFACIRC1:def 43 :

for x, y, z being set holds GFA3CarryStr x,y,z = (GFA3CarryIStr x,y,z) +* (1GateCircStr <*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 );

definition

let x, y, z be set ;
func GFA3CarryCirc x,y,z -> strict gate`2=den Boolean Circuit of GFA3CarryStr x,y,z equals :: GFACIRC1:def 44
(GFA3CarryICirc x,y,z) +* (1GateCircuit [<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ],nor3 );
coherence
(GFA3CarryICirc x,y,z) +* (1GateCircuit [<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ],nor3 ) is strict gate`2=den Boolean Circuit of GFA3CarryStr x,y,z ;

end;

:: deftheorem defines GFA3CarryCirc GFACIRC1:def 44 :

for x, y, z being set holds GFA3CarryCirc x,y,z = (GFA3CarryICirc x,y,z) +* (1GateCircuit [<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ],nor3 );

definition

let x, y, z be set ;
func GFA3CarryOutput x,y,z -> Element of InnerVertices (GFA3CarryStr x,y,z) equals :: GFACIRC1:def 45
[<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ];
coherence
[<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ] is Element of InnerVertices (GFA3CarryStr x,y,z)

proof end;

end;

:: deftheorem defines GFA3CarryOutput GFACIRC1:def 45 :

for x, y, z being set holds GFA3CarryOutput x,y,z = [<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ];

theorem Th123: :: GFACIRC1:123

for x, y, z being set holds InnerVertices (GFA3CarryIStr x,y,z) = {[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]}

proof end;

theorem Th124: :: GFACIRC1:124

for x, y, z being set holds InnerVertices (GFA3CarryStr x,y,z) = {[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]} \/ {(GFA3CarryOutput x,y,z)}

proof end;

theorem Th125: :: GFACIRC1:125

for x, y, z being set holds InnerVertices (GFA3CarryStr x,y,z) is Relation

proof end;

theorem Th126: :: GFACIRC1:126

for x, y, z being set st x <> [<*y,z*>,and2b ] & y <> [<*z,x*>,and2b ] & z <> [<*x,y*>,and2b ] holds
InputVertices (GFA3CarryIStr x,y,z) = {x,y,z}

proof end;

theorem Th127: :: GFACIRC1:127

for x, y, z being set st x <> [<*y,z*>,and2b ] & y <> [<*z,x*>,and2b ] & z <> [<*x,y*>,and2b ] holds
InputVertices (GFA3CarryStr x,y,z) = {x,y,z}

proof end;

theorem :: GFACIRC1:128

for x, y, z being non pair set holds not InputVertices (GFA3CarryStr x,y,z) is with_pair

proof end;

theorem Th129: :: GFACIRC1:129

for x, y, z being set holds
( x in the carrier of (GFA3CarryStr x,y,z) & y in the carrier of (GFA3CarryStr x,y,z) & z in the carrier of (GFA3CarryStr x,y,z) & [<*x,y*>,and2b ] in the carrier of (GFA3CarryStr x,y,z) & [<*y,z*>,and2b ] in the carrier of (GFA3CarryStr x,y,z) & [<*z,x*>,and2b ] in the carrier of (GFA3CarryStr x,y,z) & [<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ] in the carrier of (GFA3CarryStr x,y,z) )

proof end;

theorem Th130: :: GFACIRC1:130

for x, y, z being set holds
( [<*x,y*>,and2b ] in InnerVertices (GFA3CarryStr x,y,z) & [<*y,z*>,and2b ] in InnerVertices (GFA3CarryStr x,y,z) & [<*z,x*>,and2b ] in InnerVertices (GFA3CarryStr x,y,z) & GFA3CarryOutput x,y,z in InnerVertices (GFA3CarryStr x,y,z) )

proof end;

theorem Th131: :: GFACIRC1:131

for x, y, z being set st x <> [<*y,z*>,and2b ] & y <> [<*z,x*>,and2b ] & z <> [<*x,y*>,and2b ] holds
( x in InputVertices (GFA3CarryStr x,y,z) & y in InputVertices (GFA3CarryStr x,y,z) & z in InputVertices (GFA3CarryStr x,y,z) )

proof end;

theorem Th132: :: GFACIRC1:132

for x, y, z being non pair set holds InputVertices (GFA3CarryStr x,y,z) = {x,y,z}

proof end;

theorem Th133: :: GFACIRC1:133

for x, y, z being set
for s being State of (GFA3CarryCirc x,y,z)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . z holds
( (Following s) . [<*x,y*>,and2b ] = ('not' a1) '&' ('not' a2) & (Following s) . [<*y,z*>,and2b ] = ('not' a2) '&' ('not' a3) & (Following s) . [<*z,x*>,and2b ] = ('not' a3) '&' ('not' a1) )

proof end;

theorem Th134: :: GFACIRC1:134

for x, y, z being set
for s being State of (GFA3CarryCirc x,y,z)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . [<*x,y*>,and2b ] & a2 = s . [<*y,z*>,and2b ] & a3 = s . [<*z,x*>,and2b ] holds
(Following s) . (GFA3CarryOutput x,y,z) = 'not' ((a1 'or' a2) 'or' a3)

proof end;

theorem Th135: :: GFACIRC1:135

for x, y, z being set st x <> [<*y,z*>,and2b ] & y <> [<*z,x*>,and2b ] & z <> [<*x,y*>,and2b ] holds
for s being State of (GFA3CarryCirc x,y,z)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . z holds
( (Following s,2) . (GFA3CarryOutput x,y,z) = 'not' (((('not' a1) '&' ('not' a2)) 'or' (('not' a2) '&' ('not' a3))) 'or' (('not' a3) '&' ('not' a1))) & (Following s,2) . [<*x,y*>,and2b ] = ('not' a1) '&' ('not' a2) & (Following s,2) . [<*y,z*>,and2b ] = ('not' a2) '&' ('not' a3) & (Following s,2) . [<*z,x*>,and2b ] = ('not' a3) '&' ('not' a1) )

proof end;

theorem Th136: :: GFACIRC1:136

for x, y, z being set st x <> [<*y,z*>,and2b ] & y <> [<*z,x*>,and2b ] & z <> [<*x,y*>,and2b ] holds
for s being State of (GFA3CarryCirc x,y,z) holds Following s,2 is stable

proof end;

definition

let x, y, z be set ;
func GFA3AdderStr x,y,z -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: GFACIRC1:def 46
2GatesCircStr x,y,z,xor2 ;
coherence
2GatesCircStr x,y,z,xor2 is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;

end;

:: deftheorem defines GFA3AdderStr GFACIRC1:def 46 :

for x, y, z being set holds GFA3AdderStr x,y,z = 2GatesCircStr x,y,z,xor2 ;

definition

let x, y, z be set ;
func GFA3AdderCirc x,y,z -> strict gate`2=den Boolean Circuit of GFA3AdderStr x,y,z equals :: GFACIRC1:def 47
2GatesCircuit x,y,z,xor2 ;
coherence
2GatesCircuit x,y,z,xor2 is strict gate`2=den Boolean Circuit of GFA3AdderStr x,y,z ;

end;

:: deftheorem defines GFA3AdderCirc GFACIRC1:def 47 :

for x, y, z being set holds GFA3AdderCirc x,y,z = 2GatesCircuit x,y,z,xor2 ;

definition

let x, y, z be set ;
func GFA3AdderOutput x,y,z -> Element of InnerVertices (GFA3AdderStr x,y,z) equals :: GFACIRC1:def 48
2GatesCircOutput x,y,z,xor2 ;
coherence
2GatesCircOutput x,y,z,xor2 is Element of InnerVertices (GFA3AdderStr x,y,z) ;

end;

:: deftheorem defines GFA3AdderOutput GFACIRC1:def 48 :

for x, y, z being set holds GFA3AdderOutput x,y,z = 2GatesCircOutput x,y,z,xor2 ;

theorem Th137: :: GFACIRC1:137

for x, y, z being set holds InnerVertices (GFA3AdderStr x,y,z) = {[<*x,y*>,xor2 ]} \/ {(GFA3AdderOutput x,y,z)}

proof end;

theorem :: GFACIRC1:138

canceled;

theorem :: GFACIRC1:139

canceled;

theorem :: GFACIRC1:140

canceled;

theorem :: GFACIRC1:141

for x, y, z being set holds
( x in the carrier of (GFA3AdderStr x,y,z) & y in the carrier of (GFA3AdderStr x,y,z) & z in the carrier of (GFA3AdderStr x,y,z) & [<*x,y*>,xor2 ] in the carrier of (GFA3AdderStr x,y,z) & [<*[<*x,y*>,xor2 ],z*>,xor2 ] in the carrier of (GFA3AdderStr x,y,z) ) by FACIRC_1:60, FACIRC_1:61;

theorem :: GFACIRC1:142

for x, y, z being set holds
( [<*x,y*>,xor2 ] in InnerVertices (GFA3AdderStr x,y,z) & GFA3AdderOutput x,y,z in InnerVertices (GFA3AdderStr x,y,z) )

proof end;

theorem :: GFACIRC1:143

for x, y, z being set st z <> [<*x,y*>,xor2 ] holds
( x in InputVertices (GFA3AdderStr x,y,z) & y in InputVertices (GFA3AdderStr x,y,z) & z in InputVertices (GFA3AdderStr x,y,z) )

proof end;

theorem :: GFACIRC1:144

canceled;

theorem :: GFACIRC1:145

for x, y, z being set st z <> [<*x,y*>,xor2 ] holds
for s being State of (GFA3AdderCirc x,y,z)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . z holds
( (Following s) . [<*x,y*>,xor2 ] = a1 'xor' a2 & (Following s) . x = a1 & (Following s) . y = a2 & (Following s) . z = a3 )

proof end;

theorem :: GFACIRC1:146

for x, y, z being set st z <> [<*x,y*>,xor2 ] holds
for s being State of (GFA3AdderCirc x,y,z)
for a1a2, a1, a2, a3 being Element of BOOLEAN st a1a2 = s . [<*x,y*>,xor2 ] & a1 = s . x & a2 = s . y & a3 = s . z holds
(Following s) . (GFA3AdderOutput x,y,z) = a1a2 'xor' a3

proof end;

theorem Th147: :: GFACIRC1:147

for x, y, z being set st z <> [<*x,y*>,xor2 ] holds
for s being State of (GFA3AdderCirc x,y,z)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . z holds
( (Following s,2) . (GFA3AdderOutput x,y,z) = (a1 'xor' a2) 'xor' a3 & (Following s,2) . [<*x,y*>,xor2 ] = a1 'xor' a2 & (Following s,2) . x = a1 & (Following s,2) . y = a2 & (Following s,2) . z = a3 )

proof end;

theorem Th148: :: GFACIRC1:148

for x, y, z being set st z <> [<*x,y*>,xor2 ] holds
for s being State of (GFA3AdderCirc x,y,z)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . z holds
(Following s,2) . (GFA3AdderOutput x,y,z) = 'not' ((('not' a1) 'xor' ('not' a2)) 'xor' ('not' a3))

proof end;

definition

let x, y, z be set ;
func BitGFA3Str x,y,z -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: GFACIRC1:def 49
(GFA3AdderStr x,y,z) +* (GFA3CarryStr x,y,z);
coherence
(GFA3AdderStr x,y,z) +* (GFA3CarryStr x,y,z) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;

end;

:: deftheorem defines BitGFA3Str GFACIRC1:def 49 :

for x, y, z being set holds BitGFA3Str x,y,z = (GFA3AdderStr x,y,z) +* (GFA3CarryStr x,y,z);

definition

let x, y, z be set ;
func BitGFA3Circ x,y,z -> strict gate`2=den Boolean Circuit of BitGFA3Str x,y,z equals :: GFACIRC1:def 50
(GFA3AdderCirc x,y,z) +* (GFA3CarryCirc x,y,z);
coherence
(GFA3AdderCirc x,y,z) +* (GFA3CarryCirc x,y,z) is strict gate`2=den Boolean Circuit of BitGFA3Str x,y,z ;

end;

:: deftheorem defines BitGFA3Circ GFACIRC1:def 50 :

for x, y, z being set holds BitGFA3Circ x,y,z = (GFA3AdderCirc x,y,z) +* (GFA3CarryCirc x,y,z);

theorem :: GFACIRC1:149

canceled;

theorem Th150: :: GFACIRC1:150

for x, y, z being set holds InnerVertices (BitGFA3Str x,y,z) = (({[<*x,y*>,xor2 ]} \/ {(GFA3AdderOutput x,y,z)}) \/ {[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]}) \/ {(GFA3CarryOutput x,y,z)}

proof end;

theorem :: GFACIRC1:151

for x, y, z being set holds InnerVertices (BitGFA3Str x,y,z) is Relation

proof end;

theorem Th152: :: GFACIRC1:152

for x, y, z being set st z <> [<*x,y*>,xor2 ] & x <> [<*y,z*>,and2b ] & y <> [<*z,x*>,and2b ] & z <> [<*x,y*>,and2b ] holds
InputVertices (BitGFA3Str x,y,z) = {x,y,z}

proof end;

theorem Th153: :: GFACIRC1:153

for x, y, z being non pair set holds InputVertices (BitGFA3Str x,y,z) = {x,y,z}

proof end;

theorem :: GFACIRC1:154

for x, y, z being non pair set holds not InputVertices (BitGFA3Str x,y,z) is with_pair

proof end;

theorem :: GFACIRC1:155

for x, y, z being set holds
( x in the carrier of (BitGFA3Str x,y,z) & y in the carrier of (BitGFA3Str x,y,z) & z in the carrier of (BitGFA3Str x,y,z) & [<*x,y*>,xor2 ] in the carrier of (BitGFA3Str x,y,z) & [<*[<*x,y*>,xor2 ],z*>,xor2 ] in the carrier of (BitGFA3Str x,y,z) & [<*x,y*>,and2b ] in the carrier of (BitGFA3Str x,y,z) & [<*y,z*>,and2b ] in the carrier of (BitGFA3Str x,y,z) & [<*z,x*>,and2b ] in the carrier of (BitGFA3Str x,y,z) & [<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ] in the carrier of (BitGFA3Str x,y,z) )

proof end;

theorem Th156: :: GFACIRC1:156

for x, y, z being set holds
( [<*x,y*>,xor2 ] in InnerVertices (BitGFA3Str x,y,z) & GFA3AdderOutput x,y,z in InnerVertices (BitGFA3Str x,y,z) & [<*x,y*>,and2b ] in InnerVertices (BitGFA3Str x,y,z) & [<*y,z*>,and2b ] in InnerVertices (BitGFA3Str x,y,z) & [<*z,x*>,and2b ] in InnerVertices (BitGFA3Str x,y,z) & GFA3CarryOutput x,y,z in InnerVertices (BitGFA3Str x,y,z) )

proof end;

theorem :: GFACIRC1:157

for x, y, z being set st z <> [<*x,y*>,xor2 ] & x <> [<*y,z*>,and2b ] & y <> [<*z,x*>,and2b ] & z <> [<*x,y*>,and2b ] holds
( x in InputVertices (BitGFA3Str x,y,z) & y in InputVertices (BitGFA3Str x,y,z) & z in InputVertices (BitGFA3Str x,y,z) )

proof end;

definition

let x, y, z be set ;
func BitGFA3CarryOutput x,y,z -> Element of InnerVertices (BitGFA3Str x,y,z) equals :: GFACIRC1:def 51
[<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ];
coherence
[<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ] is Element of InnerVertices (BitGFA3Str x,y,z)

proof end;

end;

:: deftheorem defines BitGFA3CarryOutput GFACIRC1:def 51 :

for x, y, z being set holds BitGFA3CarryOutput x,y,z = [<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ];

definition

let x, y, z be set ;
func BitGFA3AdderOutput x,y,z -> Element of InnerVertices (BitGFA3Str x,y,z) equals :: GFACIRC1:def 52
2GatesCircOutput x,y,z,xor2 ;
coherence
2GatesCircOutput x,y,z,xor2 is Element of InnerVertices (BitGFA3Str x,y,z)

proof end;

end;

:: deftheorem defines BitGFA3AdderOutput GFACIRC1:def 52 :

for x, y, z being set holds BitGFA3AdderOutput x,y,z = 2GatesCircOutput x,y,z,xor2 ;

theorem :: GFACIRC1:158

for x, y, z being set st z <> [<*x,y*>,xor2 ] & x <> [<*y,z*>,and2b ] & y <> [<*z,x*>,and2b ] & z <> [<*x,y*>,and2b ] holds
for s being State of (BitGFA3Circ x,y,z)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . z holds
( (Following s,2) . (GFA3AdderOutput x,y,z) = 'not' ((('not' a1) 'xor' ('not' a2)) 'xor' ('not' a3)) & (Following s,2) . (GFA3CarryOutput x,y,z) = 'not' (((('not' a1) '&' ('not' a2)) 'or' (('not' a2) '&' ('not' a3))) 'or' (('not' a3) '&' ('not' a1))) )

proof end;

theorem :: GFACIRC1:159

for x, y, z being set st z <> [<*x,y*>,xor2 ] & x <> [<*y,z*>,and2b ] & y <> [<*z,x*>,and2b ] & z <> [<*x,y*>,and2b ] holds
for s being State of (BitGFA3Circ x,y,z) holds Following s,2 is stable

proof end;