:: Generalized Full Adder Circuits (GFAs). {P}art {I} :: by Shin'nosuke Yamaguchi , Katsumi Wasaki and Nobuhiro Shimoi :: :: Received December 7, 2005 :: Copyright (c) 2005-2012 Association of Mizar Users begin 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) proofend; 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 proofend; 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 ) ) proofend; ::------------------------------------- :: 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 proofend; 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 proofend; 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 ) proofend; 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 proofend; 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 proofend; 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 ) proofend; ::------------------------------------- :: 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) proofend; 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 proofend; 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 ) proofend; 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) proofend; 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 proofend; 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 . <*(and2b . <*x,y*>),(and2 . <*x,y*>)*> & xor2c . <*0,0*> = 1 & xor2c . <*0,1*> = 0 & xor2c . <*1,0*> = 0 & xor2c . <*1,1*> = 1 ) proofend; 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*> ) proofend; theorem :: GFACIRC1:6 for x, y, z being Element of BOOLEAN holds inv1 . <*(xor2 . <*(xor2c . <*x,y*>),z*>)*> = xor2c . <*(xor2c . <*x,y*>),z*> proofend; 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*> proofend; 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} ) proofend; 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} proofend; 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 ) proofend; begin ::======================================================================== :: << 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)) proofend; 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]} proofend; 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))} proofend; theorem Th12: :: GFACIRC1:12 for x, y, z being set holds InnerVertices (GFA0CarryStr (x,y,z)) is Relation proofend; ::------------------------------------------------------- :: 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} proofend; 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} proofend; theorem :: GFACIRC1:15 for x, y, z being non pair set holds InputVertices (GFA0CarryStr (x,y,z)) is without_pairs proofend; ::------------------------------------------------------- :: 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)) ) proofend; 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)) ) proofend; 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)) ) proofend; theorem Th19: :: GFACIRC1:19 for x, y, z being non pair set holds InputVertices (GFA0CarryStr (x,y,z)) = {x,y,z} proofend; ::---------------------------------------------------- :: 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 ) proofend; 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 proofend; 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 ) proofend; 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 proofend; ::========================================================================= ::------------------------------------------------- :: 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))} proofend; ::------------------------------------------------------- :: 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)) ) proofend; 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)) ) proofend; ::---------------------------------------------------- :: 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 ) proofend; 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 proofend; 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 ) proofend; ::===================================================================== ::--------------------------------------------------- :: 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))} proofend; theorem :: GFACIRC1:32 for x, y, z being set holds InnerVertices (BitGFA0Str (x,y,z)) is Relation proofend; ::------------------------------------------------------- :: 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} proofend; theorem Th34: :: GFACIRC1:34 for x, y, z being non pair set holds InputVertices (BitGFA0Str (x,y,z)) = {x,y,z} proofend; theorem :: GFACIRC1:35 for x, y, z being non pair set holds InputVertices (BitGFA0Str (x,y,z)) is without_pairs proofend; ::------------------------------------------------------- :: 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)) ) proofend; 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)) ) proofend; 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)) ) proofend; ::------------------------------------------------------------------ :: 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)) proofend; 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)) proofend; 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) ) proofend; 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 proofend; begin ::======================================================================== :: << 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)) proofend; 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]} proofend; 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))} proofend; theorem Th43: :: GFACIRC1:43 for x, y, z being set holds InnerVertices (GFA1CarryStr (x,y,z)) is Relation proofend; ::------------------------------------------------------- :: 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} proofend; 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} proofend; theorem :: GFACIRC1:46 for x, y, z being non pair set holds InputVertices (GFA1CarryStr (x,y,z)) is without_pairs proofend; ::------------------------------------------------------- :: 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)) ) proofend; 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)) ) proofend; 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)) ) proofend; theorem Th50: :: GFACIRC1:50 for x, y, z being non pair set holds InputVertices (GFA1CarryStr (x,y,z)) = {x,y,z} proofend; ::---------------------------------------------------- :: 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 ) proofend; 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 proofend; 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 ) proofend; 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 proofend; ::========================================================================= ::------------------------------------------------- :: 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))} proofend; ::------------------------------------------------------- :: 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)) ) proofend; 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)) ) proofend; ::---------------------------------------------------- :: 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 ) proofend; 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) proofend; 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 ) proofend; 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) proofend; ::===================================================================== ::--------------------------------------------------- :: 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))} proofend; theorem :: GFACIRC1:64 for x, y, z being set holds InnerVertices (BitGFA1Str (x,y,z)) is Relation proofend; ::------------------------------------------------------- :: 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} proofend; theorem Th66: :: GFACIRC1:66 for x, y, z being non pair set holds InputVertices (BitGFA1Str (x,y,z)) = {x,y,z} proofend; theorem :: GFACIRC1:67 for x, y, z being non pair set holds InputVertices (BitGFA1Str (x,y,z)) is without_pairs proofend; ::------------------------------------------------------- :: 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)) ) proofend; 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)) ) proofend; 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)) ) proofend; ::------------------------------------------------------------------ :: 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)) proofend; 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)) proofend; 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) ) proofend; 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 proofend; begin ::======================================================================== :: << 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*>,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)) proofend; 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]; ::------------------------------------------------------- :: 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*>,and2b]} proofend; theorem Th74: :: GFACIRC1:74 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))} proofend; theorem Th75: :: GFACIRC1:75 for x, y, z being set holds InnerVertices (GFA2CarryStr (x,y,z)) is Relation proofend; ::------------------------------------------------------- :: InputVertices theorem Th76: :: GFACIRC1:76 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} proofend; theorem Th77: :: GFACIRC1:77 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} proofend; theorem :: GFACIRC1:78 for x, y, z being non pair set holds InputVertices (GFA2CarryStr (x,y,z)) is without_pairs proofend; ::------------------------------------------------------- :: 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*>,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)) ) proofend; 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*>,and2b] in InnerVertices (GFA2CarryStr (x,y,z)) & GFA2CarryOutput (x,y,z) in InnerVertices (GFA2CarryStr (x,y,z)) ) proofend; theorem Th81: :: GFACIRC1:81 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)) ) proofend; theorem Th82: :: GFACIRC1:82 for x, y, z being non pair set holds InputVertices (GFA2CarryStr (x,y,z)) = {x,y,z} proofend; ::---------------------------------------------------- :: 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*>,and2b] = ('not' a3) '&' ('not' a1) ) proofend; 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*>,and2b] holds (Following s) . (GFA2CarryOutput (x,y,z)) = 'not' ((a1 'or' a2) 'or' a3) proofend; theorem Th85: :: GFACIRC1:85 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) ) proofend; theorem Th86: :: GFACIRC1:86 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 proofend; ::========================================================================= ::------------------------------------------------- :: 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))} proofend; ::------------------------------------------------------- :: 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)) ) proofend; 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)) ) proofend; ::---------------------------------------------------- :: 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 ) proofend; 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) proofend; 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 ) proofend; 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) proofend; ::===================================================================== ::--------------------------------------------------- :: 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*>,and2b]}) \/ {(GFA2CarryOutput (x,y,z))} proofend; theorem :: GFACIRC1:96 for x, y, z being set holds InnerVertices (BitGFA2Str (x,y,z)) is Relation proofend; ::------------------------------------------------------- :: InputVertices theorem Th97: :: GFACIRC1:97 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} proofend; theorem Th98: :: GFACIRC1:98 for x, y, z being non pair set holds InputVertices (BitGFA2Str (x,y,z)) = {x,y,z} proofend; theorem :: GFACIRC1:99 for x, y, z being non pair set holds InputVertices (BitGFA2Str (x,y,z)) is without_pairs proofend; ::------------------------------------------------------- :: 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*>,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)) ) proofend; 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*>,and2b] in InnerVertices (BitGFA2Str (x,y,z)) & GFA2CarryOutput (x,y,z) in InnerVertices (BitGFA2Str (x,y,z)) ) proofend; theorem :: GFACIRC1:102 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)) ) proofend; ::------------------------------------------------------------------ :: 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*>,and2b]*>,nor3]; coherence [<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,and2b]*>,nor3] is Element of InnerVertices (BitGFA2Str (x,y,z)) proofend; 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)) proofend; 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*>,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))) ) proofend; theorem :: GFACIRC1:104 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 proofend; begin ::======================================================================== :: << 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*>,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)) proofend; 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]; ::------------------------------------------------------- :: 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*>,and2b],[<*y,z*>,and2b],[<*z,x*>,and2b]} proofend; theorem Th106: :: GFACIRC1:106 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))} proofend; theorem Th107: :: GFACIRC1:107 for x, y, z being set holds InnerVertices (GFA3CarryStr (x,y,z)) is Relation proofend; ::------------------------------------------------------- :: InputVertices theorem Th108: :: GFACIRC1:108 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} proofend; theorem Th109: :: GFACIRC1:109 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} proofend; theorem :: GFACIRC1:110 for x, y, z being non pair set holds InputVertices (GFA3CarryStr (x,y,z)) is without_pairs proofend; ::------------------------------------------------------- :: 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*>,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)) ) proofend; theorem Th112: :: GFACIRC1:112 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)) ) proofend; theorem Th113: :: GFACIRC1:113 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)) ) proofend; theorem Th114: :: GFACIRC1:114 for x, y, z being non pair set holds InputVertices (GFA3CarryStr (x,y,z)) = {x,y,z} proofend; ::---------------------------------------------------- :: 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*>,and2b] = ('not' a1) '&' ('not' a2) & (Following s) . [<*y,z*>,and2b] = ('not' a2) '&' ('not' a3) & (Following s) . [<*z,x*>,and2b] = ('not' a3) '&' ('not' a1) ) proofend; 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*>,and2b] & a2 = s . [<*y,z*>,and2b] & a3 = s . [<*z,x*>,and2b] holds (Following s) . (GFA3CarryOutput (x,y,z)) = 'not' ((a1 'or' a2) 'or' a3) proofend; theorem Th117: :: GFACIRC1:117 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) ) proofend; theorem Th118: :: GFACIRC1:118 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 proofend; ::========================================================================= ::------------------------------------------------- :: 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))} proofend; ::------------------------------------------------------- :: 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)) ) proofend; 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)) ) proofend; ::---------------------------------------------------- :: 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 ) proofend; 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 proofend; 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 ) proofend; 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)) proofend; ::===================================================================== ::--------------------------------------------------- :: 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*>,and2b],[<*y,z*>,and2b],[<*z,x*>,and2b]}) \/ {(GFA3CarryOutput (x,y,z))} proofend; theorem :: GFACIRC1:128 for x, y, z being set holds InnerVertices (BitGFA3Str (x,y,z)) is Relation proofend; ::------------------------------------------------------- :: InputVertices theorem Th129: :: GFACIRC1:129 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} proofend; theorem Th130: :: GFACIRC1:130 for x, y, z being non pair set holds InputVertices (BitGFA3Str (x,y,z)) = {x,y,z} proofend; theorem :: GFACIRC1:131 for x, y, z being non pair set holds InputVertices (BitGFA3Str (x,y,z)) is without_pairs proofend; ::------------------------------------------------------- :: 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*>,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)) ) proofend; 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*>,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)) ) proofend; theorem :: GFACIRC1:134 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)) ) proofend; ::------------------------------------------------------------------ :: 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*>,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)) proofend; 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)) proofend; 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*>,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))) ) proofend; theorem :: GFACIRC1:136 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 proofend;