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


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

scheme :: GFACIRC1:sch 2
1AryBooleUniq{ F1( 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*> = F1(x) ) & ( for x being Element of BOOLEAN holds f2 . <*x*> = F1(x) ) holds
f1 = f2
proof end;

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

::-------------------------------------
:: 1-Input Operators (inv1, buf1)
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 b1 being Function of (1 -tuples_on BOOLEAN),BOOLEAN st
for x being Element of BOOLEAN holds b1 . <*x*> = 'not' x
proof end;
uniqueness
for b1, b2 being Function of (1 -tuples_on BOOLEAN),BOOLEAN st ( for x being Element of BOOLEAN holds b1 . <*x*> = 'not' x ) & ( for x being Element of BOOLEAN holds b2 . <*x*> = 'not' x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines inv1 GFACIRC1:def 1 :
for b1 being Function of (1 -tuples_on BOOLEAN),BOOLEAN holds
( b1 = inv1 iff for x being Element of BOOLEAN holds b1 . <*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 b1 being Function of (1 -tuples_on BOOLEAN),BOOLEAN st
for x being Element of BOOLEAN holds b1 . <*x*> = x
proof end;
uniqueness
for b1, b2 being Function of (1 -tuples_on BOOLEAN),BOOLEAN st ( for x being Element of BOOLEAN holds b1 . <*x*> = x ) & ( for x being Element of BOOLEAN holds b2 . <*x*> = x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines buf1 GFACIRC1:def 2 :
for b1 being Function of (1 -tuples_on BOOLEAN),BOOLEAN holds
( b1 = buf1 iff for x being Element of BOOLEAN holds b1 . <*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;

::-------------------------------------
:: 2-Input Operators (and2c, xor2c)
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 b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x '&' ('not' y)
proof end;
uniqueness
for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x '&' ('not' y) ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x '&' ('not' y) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines and2c GFACIRC1:def 3 :
for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds
( b1 = and2c iff for x, y being Element of BOOLEAN holds b1 . <*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 b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'xor' ('not' y)
proof end;
uniqueness
for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'xor' ('not' y) ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x 'xor' ('not' y) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines xor2c GFACIRC1:def 4 :
for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds
( b1 = xor2c iff for x, y being Element of BOOLEAN holds b1 . <*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 . <*(nor2 . <*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
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:6
for x, y, z being Element of BOOLEAN holds inv1 . <*(xor2 . <*(xor2c . <*x,y*>),z*>)*> = xor2c . <*(xor2c . <*x,y*>),z*>
proof end;

theorem :: GFACIRC1:7
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:8
for x, y, z being Element of BOOLEAN holds xor2c . <*(xor2a . <*x,y*>),z*> = xor2c . <*(xor2c . <*x,y*>),z*> by Th4;

theorem :: GFACIRC1:9
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;

::========================================================================
:: << GFA TYPE-0 >>
::------------------------------------------------------------------------
:: Name : Generalized Full Adder Type-0 (GFA0)
:: Function : x + y + z = 2 * c + s
::
:: Logic Symbol : x y Combined : GFA0CarryIStr(x,y,z)
:: | / GFA0CarryStr(x,y,z)
:: | / GFA0AdderStr(x,y,z)
:: +---*---* --->
:: | GFA *-----z BitGFA0Str(x,y,z)
:: | TYPE0 |
:: *---*---+ Outputs : BitGFA0CarryOutput(x,y,z)
:: / | BitGFA0AdderOutput(x,y,z)
:: / |
:: c s Calculation : Following(s,2) is stable.
::=========================================================================
::-------------------------------------------------
:: GFA0 Carry : Circuit Definition of Carry Output
::-------------------------------------------------
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];

::-------------------------------------------------------
:: GFA0 Carry : Carrier, InnerVertices and InputVertices
::-------------------------------------------------------
::-------------------------------------------------------
:: InnerVertices
theorem Th10: :: GFACIRC1:10
for x, y, z being set holds InnerVertices (GFA0CarryIStr (x,y,z)) = {[<*x,y*>,and2],[<*y,z*>,and2],[<*z,x*>,and2]}
proof end;

theorem Th11: :: GFACIRC1:11
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 Th12: :: GFACIRC1:12
for x, y, z being set holds InnerVertices (GFA0CarryStr (x,y,z)) is Relation
proof end;

::-------------------------------------------------------
:: InputVertices
theorem Th13: :: GFACIRC1:13
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 Th14: :: GFACIRC1:14
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:15
for x, y, z being non pair set holds InputVertices (GFA0CarryStr (x,y,z)) is without_pairs
proof end;

::-------------------------------------------------------
:: Carrier and misc.
theorem Th16: :: GFACIRC1:16
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 Th17: :: GFACIRC1:17
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 Th18: :: GFACIRC1:18
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 Th19: :: GFACIRC1:19
for x, y, z being non pair set holds InputVertices (GFA0CarryStr (x,y,z)) = {x,y,z}
proof end;

::----------------------------------------------------
:: GFA0 Carry : Stability of the Carry Output Circuit
::----------------------------------------------------
theorem Th20: :: GFACIRC1:20
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 Th21: :: GFACIRC1:21
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 Th22: :: GFACIRC1:22
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 Th23: :: GFACIRC1:23
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;

::=========================================================================
::-------------------------------------------------
:: GFA0 Adder : Circuit Definition of Adder Output
::-------------------------------------------------
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);

::-------------------------------------------------------
:: GFA0 Adder : Carrier, InnerVertices and InputVertices
::-------------------------------------------------------
::-------------------------------------------------------
:: InnerVertices
theorem Th24: :: GFACIRC1:24
for x, y, z being set holds InnerVertices (GFA0AdderStr (x,y,z)) = {[<*x,y*>,xor2]} \/ {(GFA0AdderOutput (x,y,z))}
proof end;

::-------------------------------------------------------
:: Carrier and misc.
theorem :: GFACIRC1:25
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 Th26: :: GFACIRC1:26
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 Th27: :: GFACIRC1:27
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;

::----------------------------------------------------
:: GFA0 Adder : Stability of the Adder Output Circuit
::----------------------------------------------------
theorem Th28: :: GFACIRC1:28
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 Th29: :: GFACIRC1:29
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 Th30: :: GFACIRC1:30
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;

::=====================================================================
::---------------------------------------------------
:: GFA0 : Circuit Definition of GFA Combined Circuit
::---------------------------------------------------
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));

::----------------------------------------------------------
:: GFA0 Combined : Carrier, InnerVertices and InputVertices
::----------------------------------------------------------
::-------------------------------------------------------
:: InnerVertices
theorem Th31: :: GFACIRC1:31
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:32
for x, y, z being set holds InnerVertices (BitGFA0Str (x,y,z)) is Relation
proof end;

::-------------------------------------------------------
:: InputVertices
theorem Th33: :: GFACIRC1:33
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 Th34: :: GFACIRC1:34
for x, y, z being non pair set holds InputVertices (BitGFA0Str (x,y,z)) = {x,y,z}
proof end;

theorem :: GFACIRC1:35
for x, y, z being non pair set holds InputVertices (BitGFA0Str (x,y,z)) is without_pairs
proof end;

::-------------------------------------------------------
:: Carrier and misc.
theorem :: GFACIRC1:36
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 Th37: :: GFACIRC1:37
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:38
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;

::------------------------------------------------------------------
:: GFA0 : Carry and Adder Output Definition of GFA Combined Circuit
::------------------------------------------------------------------
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);

::-------------------------------------------------------------
:: GFA0 Combined : Stability of the Adder/Carry Output Circuit
::-------------------------------------------------------------
theorem :: GFACIRC1:39
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:40
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;

::========================================================================
:: << GFA TYPE-1 >>
::------------------------------------------------------------------------
:: Name : Generalized Full Adder Type-1 (GFA1)
:: Function : x - y + z = 2 * c - s
::
:: Logic Symbol : x -y Combined : GFA1CarryIStr(x,y,z)
:: | / GFA1CarryStr(x,y,z)
:: | / GFA1AdderStr(x,y,z)
:: +---*---O --->
:: | GFA *-----z BitGFA1Str(x,y,z)
:: | TYPE1 |
:: *---O---+ Outputs : BitGFA1CarryOutput(x,y,z)
:: / | BitGFA1AdderOutput(x,y,z)
:: / |
:: c -s Calculation : Following(s,2) is stable.
::=========================================================================
::-------------------------------------------------
:: GFA1 Carry : Circuit Definition of Carry Output
::-------------------------------------------------
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];

::-------------------------------------------------------
:: GFA1 Carry : Carrier, InnerVertices and InputVertices
::-------------------------------------------------------
::-------------------------------------------------------
:: InnerVertices
theorem Th41: :: GFACIRC1:41
for x, y, z being set holds InnerVertices (GFA1CarryIStr (x,y,z)) = {[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]}
proof end;

theorem Th42: :: GFACIRC1:42
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 Th43: :: GFACIRC1:43
for x, y, z being set holds InnerVertices (GFA1CarryStr (x,y,z)) is Relation
proof end;

::-------------------------------------------------------
:: InputVertices
theorem Th44: :: GFACIRC1:44
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 Th45: :: GFACIRC1:45
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:46
for x, y, z being non pair set holds InputVertices (GFA1CarryStr (x,y,z)) is without_pairs
proof end;

::-------------------------------------------------------
:: Carrier and misc.
theorem Th47: :: GFACIRC1:47
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 Th48: :: GFACIRC1:48
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 Th49: :: GFACIRC1:49
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 Th50: :: GFACIRC1:50
for x, y, z being non pair set holds InputVertices (GFA1CarryStr (x,y,z)) = {x,y,z}
proof end;

::----------------------------------------------------
:: GFA1 Carry : Stability of the Carry Output Circuit
::----------------------------------------------------
theorem Th51: :: GFACIRC1:51
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 Th52: :: GFACIRC1:52
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 Th53: :: GFACIRC1:53
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 Th54: :: GFACIRC1:54
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;

::=========================================================================
::-------------------------------------------------
:: GFA1 Adder : Circuit Definition of Adder Output
::-------------------------------------------------
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);

::-------------------------------------------------------
:: GFA1 Adder : Carrier, InnerVertices and InputVertices
::-------------------------------------------------------
::-------------------------------------------------------
:: InnerVertices
theorem Th55: :: GFACIRC1:55
for x, y, z being set holds InnerVertices (GFA1AdderStr (x,y,z)) = {[<*x,y*>,xor2c]} \/ {(GFA1AdderOutput (x,y,z))}
proof end;

::-------------------------------------------------------
:: Carrier and misc.
theorem :: GFACIRC1:56
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 Th57: :: GFACIRC1:57
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 Th58: :: GFACIRC1:58
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;

::----------------------------------------------------
:: GFA1 Adder : Stability of the Adder Output Circuit
::----------------------------------------------------
theorem Th59: :: GFACIRC1:59
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 Th60: :: GFACIRC1:60
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 Th61: :: GFACIRC1:61
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 Th62: :: GFACIRC1:62
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;

::=====================================================================
::---------------------------------------------------
:: GFA1 : Circuit Definition of GFA Combined Circuit
::---------------------------------------------------
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));

::----------------------------------------------------------
:: GFA1 Combined : Carrier, InnerVertices and InputVertices
::----------------------------------------------------------
::-------------------------------------------------------
:: InnerVertices
theorem Th63: :: GFACIRC1:63
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:64
for x, y, z being set holds InnerVertices (BitGFA1Str (x,y,z)) is Relation
proof end;

::-------------------------------------------------------
:: InputVertices
theorem Th65: :: GFACIRC1:65
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 Th66: :: GFACIRC1:66
for x, y, z being non pair set holds InputVertices (BitGFA1Str (x,y,z)) = {x,y,z}
proof end;

theorem :: GFACIRC1:67
for x, y, z being non pair set holds InputVertices (BitGFA1Str (x,y,z)) is without_pairs
proof end;

::-------------------------------------------------------
:: Carrier and misc.
theorem :: GFACIRC1:68
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 Th69: :: GFACIRC1:69
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:70
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;

::------------------------------------------------------------------
:: GFA1 : Carry and Adder Output Definition of GFA Combined Circuit
::------------------------------------------------------------------
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);

::-------------------------------------------------------------
:: GFA1 Combined : Stability of the Adder/Carry Output Circuit
::-------------------------------------------------------------
theorem :: GFACIRC1:71
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:72
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;

::========================================================================
:: << GFA TYPE-2 >>
::------------------------------------------------------------------------
:: Name : Generalized Full Adder Type-2 (GFA2)
:: Function : - x + y - z = - 2 * c + s
::
:: Logic Symbol : -x y Combined : GFA2CarryIStr(x,y,z)
:: | / GFA2CarryStr(x,y,z)
:: | / GFA2AdderStr(x,y,z)
:: +---O---* --->
:: | GFA O---- -z BitGFA2Str(x,y,z)
:: | TYPE2 |
:: O---*---+ Outputs : BitGFA2CarryOutput(x,y,z)
:: / | BitGFA2AdderOutput(x,y,z)
:: / |
:: -c s Calculation : Following(s,2) is stable.
::=========================================================================
::-------------------------------------------------
:: GFA2 Carry : Circuit Definition of Carry Output
::-------------------------------------------------
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*>,nor2));
coherence
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,z*>,and2c))) +* (1GateCircStr (<*z,x*>,nor2)) 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*>,nor2));

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,nor2));
coherence
((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,z,and2c))) +* (1GateCircuit (z,x,nor2)) 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,nor2));

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*>,nor2]*>,nor3));
coherence
(GFA2CarryIStr (x,y,z)) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2]*>,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*>,nor2]*>,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*>,nor2],nor3));
coherence
(GFA2CarryICirc (x,y,z)) +* (1GateCircuit ([<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2],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*>,nor2],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*>,nor2]*>,nor3];
coherence
[<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2]*>,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*>,nor2]*>,nor3];

::-------------------------------------------------------
:: GFA2 Carry : Carrier, InnerVertices and InputVertices
::-------------------------------------------------------
::-------------------------------------------------------
:: InnerVertices
theorem Th73: :: GFACIRC1:73
for x, y, z being set holds InnerVertices (GFA2CarryIStr (x,y,z)) = {[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2]}
proof end;

theorem Th74: :: GFACIRC1:74
for x, y, z being set holds InnerVertices (GFA2CarryStr (x,y,z)) = {[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2]} \/ {(GFA2CarryOutput (x,y,z))}
proof end;

theorem Th75: :: GFACIRC1:75
for x, y, z being set holds InnerVertices (GFA2CarryStr (x,y,z)) is Relation
proof end;

::-------------------------------------------------------
:: InputVertices
theorem Th76: :: GFACIRC1:76
for x, y, z being set st x <> [<*y,z*>,and2c] & y <> [<*z,x*>,nor2] & z <> [<*x,y*>,and2a] holds
InputVertices (GFA2CarryIStr (x,y,z)) = {x,y,z}
proof end;

theorem Th77: :: GFACIRC1:77
for x, y, z being set st x <> [<*y,z*>,and2c] & y <> [<*z,x*>,nor2] & z <> [<*x,y*>,and2a] holds
InputVertices (GFA2CarryStr (x,y,z)) = {x,y,z}
proof end;

theorem :: GFACIRC1:78
for x, y, z being non pair set holds InputVertices (GFA2CarryStr (x,y,z)) is without_pairs
proof end;

::-------------------------------------------------------
:: Carrier and misc.
theorem Th79: :: GFACIRC1:79
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*>,nor2] in the carrier of (GFA2CarryStr (x,y,z)) & [<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2]*>,nor3] in the carrier of (GFA2CarryStr (x,y,z)) )
proof end;

theorem Th80: :: GFACIRC1:80
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*>,nor2] in InnerVertices (GFA2CarryStr (x,y,z)) & GFA2CarryOutput (x,y,z) in InnerVertices (GFA2CarryStr (x,y,z)) )
proof end;

theorem Th81: :: GFACIRC1:81
for x, y, z being set st x <> [<*y,z*>,and2c] & y <> [<*z,x*>,nor2] & 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 Th82: :: GFACIRC1:82
for x, y, z being non pair set holds InputVertices (GFA2CarryStr (x,y,z)) = {x,y,z}
proof end;

::----------------------------------------------------
:: GFA2 Carry : Stability of the Carry Output Circuit
::----------------------------------------------------
theorem Th83: :: GFACIRC1:83
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*>,nor2] = ('not' a3) '&' ('not' a1) )
proof end;

theorem Th84: :: GFACIRC1:84
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*>,nor2] holds
(Following s) . (GFA2CarryOutput (x,y,z)) = 'not' ((a1 'or' a2) 'or' a3)
proof end;

theorem Th85: :: GFACIRC1:85
for x, y, z being set st x <> [<*y,z*>,and2c] & y <> [<*z,x*>,nor2] & 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*>,nor2] = ('not' a3) '&' ('not' a1) )
proof end;

theorem Th86: :: GFACIRC1:86
for x, y, z being set st x <> [<*y,z*>,and2c] & y <> [<*z,x*>,nor2] & z <> [<*x,y*>,and2a] holds
for s being State of (GFA2CarryCirc (x,y,z)) holds Following (s,2) is stable
proof end;

::=========================================================================
::-------------------------------------------------
:: GFA2 Adder : Circuit Definition of Adder Output
::-------------------------------------------------
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);

::-------------------------------------------------------
:: GFA2 Adder : Carrier, InnerVertices and InputVertices
::-------------------------------------------------------
::-------------------------------------------------------
:: InnerVertices
theorem Th87: :: GFACIRC1:87
for x, y, z being set holds InnerVertices (GFA2AdderStr (x,y,z)) = {[<*x,y*>,xor2c]} \/ {(GFA2AdderOutput (x,y,z))}
proof end;

::-------------------------------------------------------
:: Carrier and misc.
theorem :: GFACIRC1:88
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:89
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:90
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;

::----------------------------------------------------
:: GFA2 Adder : Stability of the Adder Output Circuit
::----------------------------------------------------
theorem :: GFACIRC1:91
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:92
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 Th93: :: GFACIRC1:93
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 Th94: :: GFACIRC1:94
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;

::=====================================================================
::---------------------------------------------------
:: GFA2 : Circuit Definition of GFA Combined Circuit
::---------------------------------------------------
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));

::----------------------------------------------------------
:: GFA2 Combined : Carrier, InnerVertices and InputVertices
::----------------------------------------------------------
::-------------------------------------------------------
:: InnerVertices
theorem Th95: :: GFACIRC1:95
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*>,nor2]}) \/ {(GFA2CarryOutput (x,y,z))}
proof end;

theorem :: GFACIRC1:96
for x, y, z being set holds InnerVertices (BitGFA2Str (x,y,z)) is Relation
proof end;

::-------------------------------------------------------
:: InputVertices
theorem Th97: :: GFACIRC1:97
for x, y, z being set st z <> [<*x,y*>,xor2c] & x <> [<*y,z*>,and2c] & y <> [<*z,x*>,nor2] & z <> [<*x,y*>,and2a] holds
InputVertices (BitGFA2Str (x,y,z)) = {x,y,z}
proof end;

theorem Th98: :: GFACIRC1:98
for x, y, z being non pair set holds InputVertices (BitGFA2Str (x,y,z)) = {x,y,z}
proof end;

theorem :: GFACIRC1:99
for x, y, z being non pair set holds InputVertices (BitGFA2Str (x,y,z)) is without_pairs
proof end;

::-------------------------------------------------------
:: Carrier and misc.
theorem :: GFACIRC1:100
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*>,nor2] in the carrier of (BitGFA2Str (x,y,z)) & [<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2]*>,nor3] in the carrier of (BitGFA2Str (x,y,z)) )
proof end;

theorem Th101: :: GFACIRC1:101
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*>,nor2] in InnerVertices (BitGFA2Str (x,y,z)) & GFA2CarryOutput (x,y,z) in InnerVertices (BitGFA2Str (x,y,z)) )
proof end;

theorem :: GFACIRC1:102
for x, y, z being set st z <> [<*x,y*>,xor2c] & x <> [<*y,z*>,and2c] & y <> [<*z,x*>,nor2] & 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;

::------------------------------------------------------------------
:: GFA2 : Carry and Adder Output Definition of GFA Combined Circuit
::------------------------------------------------------------------
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*>,nor2]*>,nor3];
coherence
[<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2]*>,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*>,nor2]*>,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);

::-------------------------------------------------------------
:: GFA2 Combined : Stability of the Adder/Carry Output Circuit
::-------------------------------------------------------------
theorem :: GFACIRC1:103
for x, y, z being set st z <> [<*x,y*>,xor2c] & x <> [<*y,z*>,and2c] & y <> [<*z,x*>,nor2] & 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:104
for x, y, z being set st z <> [<*x,y*>,xor2c] & x <> [<*y,z*>,and2c] & y <> [<*z,x*>,nor2] & z <> [<*x,y*>,and2a] holds
for s being State of (BitGFA2Circ (x,y,z)) holds Following (s,2) is stable
proof end;

::========================================================================
:: << GFA TYPE-3 >>
::------------------------------------------------------------------------
:: Name : Generalized Full Adder Type-3 (GFA3)
:: Function : - x - y - z = - 2 * c - s
::
:: Logic Symbol : -x -y Combined : GFA3CarryIStr(x,y,z)
:: | / GFA3CarryStr(x,y,z)
:: | / GFA3AdderStr(x,y,z)
:: +---O---O --->
:: | GFA O---- -z BitGFA3Str(x,y,z)
:: | TYPE3 |
:: O---O---+ Outputs : BitGFA3CarryOutput(x,y,z)
:: / | BitGFA3AdderOutput(x,y,z)
:: / |
:: -c -s Calculation : Following(s,2) is stable.
::=========================================================================
::-------------------------------------------------
:: GFA3 Carry : Circuit Definition of Carry Output
::-------------------------------------------------
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*>,nor2)) +* (1GateCircStr (<*y,z*>,nor2))) +* (1GateCircStr (<*z,x*>,nor2));
coherence
((1GateCircStr (<*x,y*>,nor2)) +* (1GateCircStr (<*y,z*>,nor2))) +* (1GateCircStr (<*z,x*>,nor2)) 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*>,nor2)) +* (1GateCircStr (<*y,z*>,nor2))) +* (1GateCircStr (<*z,x*>,nor2));

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,nor2)) +* (1GateCircuit (y,z,nor2))) +* (1GateCircuit (z,x,nor2));
coherence
((1GateCircuit (x,y,nor2)) +* (1GateCircuit (y,z,nor2))) +* (1GateCircuit (z,x,nor2)) 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,nor2)) +* (1GateCircuit (y,z,nor2))) +* (1GateCircuit (z,x,nor2));

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*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,nor3));
coherence
(GFA3CarryIStr (x,y,z)) +* (1GateCircStr (<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,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*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,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*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2],nor3));
coherence
(GFA3CarryICirc (x,y,z)) +* (1GateCircuit ([<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2],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*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2],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*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,nor3];
coherence
[<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,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*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,nor3];

::-------------------------------------------------------
:: GFA3 Carry : Carrier, InnerVertices and InputVertices
::-------------------------------------------------------
::-------------------------------------------------------
:: InnerVertices
theorem Th105: :: GFACIRC1:105
for x, y, z being set holds InnerVertices (GFA3CarryIStr (x,y,z)) = {[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]}
proof end;

theorem Th106: :: GFACIRC1:106
for x, y, z being set holds InnerVertices (GFA3CarryStr (x,y,z)) = {[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]} \/ {(GFA3CarryOutput (x,y,z))}
proof end;

theorem Th107: :: GFACIRC1:107
for x, y, z being set holds InnerVertices (GFA3CarryStr (x,y,z)) is Relation
proof end;

::-------------------------------------------------------
:: InputVertices
theorem Th108: :: GFACIRC1:108
for x, y, z being set st x <> [<*y,z*>,nor2] & y <> [<*z,x*>,nor2] & z <> [<*x,y*>,nor2] holds
InputVertices (GFA3CarryIStr (x,y,z)) = {x,y,z}
proof end;

theorem Th109: :: GFACIRC1:109
for x, y, z being set st x <> [<*y,z*>,nor2] & y <> [<*z,x*>,nor2] & z <> [<*x,y*>,nor2] holds
InputVertices (GFA3CarryStr (x,y,z)) = {x,y,z}
proof end;

theorem :: GFACIRC1:110
for x, y, z being non pair set holds InputVertices (GFA3CarryStr (x,y,z)) is without_pairs
proof end;

::-------------------------------------------------------
:: Carrier and misc.
theorem Th111: :: GFACIRC1:111
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*>,nor2] in the carrier of (GFA3CarryStr (x,y,z)) & [<*y,z*>,nor2] in the carrier of (GFA3CarryStr (x,y,z)) & [<*z,x*>,nor2] in the carrier of (GFA3CarryStr (x,y,z)) & [<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,nor3] in the carrier of (GFA3CarryStr (x,y,z)) )
proof end;

theorem Th112: :: GFACIRC1:112
for x, y, z being set holds
( [<*x,y*>,nor2] in InnerVertices (GFA3CarryStr (x,y,z)) & [<*y,z*>,nor2] in InnerVertices (GFA3CarryStr (x,y,z)) & [<*z,x*>,nor2] in InnerVertices (GFA3CarryStr (x,y,z)) & GFA3CarryOutput (x,y,z) in InnerVertices (GFA3CarryStr (x,y,z)) )
proof end;

theorem Th113: :: GFACIRC1:113
for x, y, z being set st x <> [<*y,z*>,nor2] & y <> [<*z,x*>,nor2] & z <> [<*x,y*>,nor2] 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 Th114: :: GFACIRC1:114
for x, y, z being non pair set holds InputVertices (GFA3CarryStr (x,y,z)) = {x,y,z}
proof end;

::----------------------------------------------------
:: GFA3 Carry : Stability of the Carry Output Circuit
::----------------------------------------------------
theorem Th115: :: GFACIRC1:115
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*>,nor2] = ('not' a1) '&' ('not' a2) & (Following s) . [<*y,z*>,nor2] = ('not' a2) '&' ('not' a3) & (Following s) . [<*z,x*>,nor2] = ('not' a3) '&' ('not' a1) )
proof end;

theorem Th116: :: GFACIRC1:116
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*>,nor2] & a2 = s . [<*y,z*>,nor2] & a3 = s . [<*z,x*>,nor2] holds
(Following s) . (GFA3CarryOutput (x,y,z)) = 'not' ((a1 'or' a2) 'or' a3)
proof end;

theorem Th117: :: GFACIRC1:117
for x, y, z being set st x <> [<*y,z*>,nor2] & y <> [<*z,x*>,nor2] & z <> [<*x,y*>,nor2] 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*>,nor2] = ('not' a1) '&' ('not' a2) & (Following (s,2)) . [<*y,z*>,nor2] = ('not' a2) '&' ('not' a3) & (Following (s,2)) . [<*z,x*>,nor2] = ('not' a3) '&' ('not' a1) )
proof end;

theorem Th118: :: GFACIRC1:118
for x, y, z being set st x <> [<*y,z*>,nor2] & y <> [<*z,x*>,nor2] & z <> [<*x,y*>,nor2] holds
for s being State of (GFA3CarryCirc (x,y,z)) holds Following (s,2) is stable
proof end;

::=========================================================================
::-------------------------------------------------
:: GFA3 Adder : Circuit Definition of Adder Output
::-------------------------------------------------
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);

::-------------------------------------------------------
:: GFA3 Adder : Carrier, InnerVertices and InputVertices
::-------------------------------------------------------
::-------------------------------------------------------
:: InnerVertices
theorem Th119: :: GFACIRC1:119
for x, y, z being set holds InnerVertices (GFA3AdderStr (x,y,z)) = {[<*x,y*>,xor2]} \/ {(GFA3AdderOutput (x,y,z))}
proof end;

::-------------------------------------------------------
:: Carrier and misc.
theorem :: GFACIRC1:120
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:121
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:122
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;

::----------------------------------------------------
:: GFA3 Adder : Stability of the Adder Output Circuit
::----------------------------------------------------
theorem :: GFACIRC1:123
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:124
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 Th125: :: GFACIRC1:125
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 Th126: :: GFACIRC1:126
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;

::=====================================================================
::---------------------------------------------------
:: GFA3 : Circuit Definition of GFA Combined Circuit
::---------------------------------------------------
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));

::----------------------------------------------------------
:: GFA3 Combined : Carrier, InnerVertices and InputVertices
::----------------------------------------------------------
::-------------------------------------------------------
:: InnerVertices
theorem Th127: :: GFACIRC1:127
for x, y, z being set holds InnerVertices (BitGFA3Str (x,y,z)) = (({[<*x,y*>,xor2]} \/ {(GFA3AdderOutput (x,y,z))}) \/ {[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]}) \/ {(GFA3CarryOutput (x,y,z))}
proof end;

theorem :: GFACIRC1:128
for x, y, z being set holds InnerVertices (BitGFA3Str (x,y,z)) is Relation
proof end;

::-------------------------------------------------------
:: InputVertices
theorem Th129: :: GFACIRC1:129
for x, y, z being set st z <> [<*x,y*>,xor2] & x <> [<*y,z*>,nor2] & y <> [<*z,x*>,nor2] & z <> [<*x,y*>,nor2] holds
InputVertices (BitGFA3Str (x,y,z)) = {x,y,z}
proof end;

theorem Th130: :: GFACIRC1:130
for x, y, z being non pair set holds InputVertices (BitGFA3Str (x,y,z)) = {x,y,z}
proof end;

theorem :: GFACIRC1:131
for x, y, z being non pair set holds InputVertices (BitGFA3Str (x,y,z)) is without_pairs
proof end;

::-------------------------------------------------------
:: Carrier and misc.
theorem :: GFACIRC1:132
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*>,nor2] in the carrier of (BitGFA3Str (x,y,z)) & [<*y,z*>,nor2] in the carrier of (BitGFA3Str (x,y,z)) & [<*z,x*>,nor2] in the carrier of (BitGFA3Str (x,y,z)) & [<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,nor3] in the carrier of (BitGFA3Str (x,y,z)) )
proof end;

theorem Th133: :: GFACIRC1:133
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*>,nor2] in InnerVertices (BitGFA3Str (x,y,z)) & [<*y,z*>,nor2] in InnerVertices (BitGFA3Str (x,y,z)) & [<*z,x*>,nor2] in InnerVertices (BitGFA3Str (x,y,z)) & GFA3CarryOutput (x,y,z) in InnerVertices (BitGFA3Str (x,y,z)) )
proof end;

theorem :: GFACIRC1:134
for x, y, z being set st z <> [<*x,y*>,xor2] & x <> [<*y,z*>,nor2] & y <> [<*z,x*>,nor2] & z <> [<*x,y*>,nor2] holds
( x in InputVertices (BitGFA3Str (x,y,z)) & y in InputVertices (BitGFA3Str (x,y,z)) & z in InputVertices (BitGFA3Str (x,y,z)) )
proof end;

::------------------------------------------------------------------
:: GFA3 : Carry and Adder Output Definition of GFA Combined Circuit
::------------------------------------------------------------------
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*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,nor3];
coherence
[<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,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*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,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);

::-------------------------------------------------------------
:: GFA3 Combined : Stability of the Adder/Carry Output Circuit
::-------------------------------------------------------------
theorem :: GFACIRC1:135
for x, y, z being set st z <> [<*x,y*>,xor2] & x <> [<*y,z*>,nor2] & y <> [<*z,x*>,nor2] & z <> [<*x,y*>,nor2] 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:136
for x, y, z being set st z <> [<*x,y*>,xor2] & x <> [<*y,z*>,nor2] & y <> [<*z,x*>,nor2] & z <> [<*x,y*>,nor2] holds
for s being State of (BitGFA3Circ (x,y,z)) holds Following (s,2) is stable
proof end;