:: Stability of the 4-2 Binary Addition Circuit Cells. Part {I} :: by Katsumi Wasaki :: :: Received August 28, 2008 :: Copyright (c) 2008-2012 Association of Mizar Users begin ::======================================================================== :: [4-2 Binary Addition Cell_i : TYPE-0] :: :: Cell Module Symbol : :: :: a+ b+ c+ d+ Input : a+,b+,c+,d+ (non pair set) :: | | | | cin+ (pair) :: +-*--*--*--*-+ cin+ :: | | / :: +--* FTA TYPE-0 *--+ Output : p+,q+,cout+ (pair) :: / | | :: cout+ +---*----*---+ :: | | :: p+ q+ :: :: Composition : Cascade by Adder Output together with two GFA TYPE-0 :: Function : p[i+1] + q[i] + Intermediate_Carry_out :: = a[i] + b[i] + c[i] + d[i] + Intermediate_Carry_in :: :: a^{+}[i] b^{+}[i] :: | / :: | / :: +---*---* :: | GFA *---- c^{+}[i] Circuit Composition : :: | TYPE0 | BitGFA0Str(a+,b+,c+) :: *---*---+ BitGFA0Str(A1,cin,d+) :: / | cin[i] ---> :: / A1| / FTA0Str(a+,b+,c+,d+,cin) :: cout[i+1] | / :: +---*---* Intermediate Addition and Carry: :: | GFA *---- d^{+}[i] A1 <= GFA0AdderOutput :: | TYPE0 | cout[i+1] <= GFA0CarryOutput :: *---*---+ q[i] <= GFA0AdderOutput :: / | p[i+1] <= GFA0CarryOutput :: / | :: p^{+}[i+1] q^{+}[i] :: :: Calculation Stability : Following(s,2+2) is stable. :: ::========================================================================= ::--------------------------------------------------------------- :: 1-1. Circuit Definition for Intermediate Addition and Carry Circuit (TYPE-0) ::--------------------------------------------------------------- :: Def. Combined Circuit Structure of 1-bit FTA TYPE-0 definition let ap, bp, cp, dp, cin be set ; func BitFTA0Str (ap,bp,cp,dp,cin) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: FTACELL1:def 1 (BitGFA0Str (ap,bp,cp)) +* (BitGFA0Str ((GFA0AdderOutput (ap,bp,cp)),cin,dp)); coherence (BitGFA0Str (ap,bp,cp)) +* (BitGFA0Str ((GFA0AdderOutput (ap,bp,cp)),cin,dp)) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ; end; :: deftheorem defines BitFTA0Str FTACELL1:def_1_:_ for ap, bp, cp, dp, cin being set holds BitFTA0Str (ap,bp,cp,dp,cin) = (BitGFA0Str (ap,bp,cp)) +* (BitGFA0Str ((GFA0AdderOutput (ap,bp,cp)),cin,dp)); definition let ap, bp, cp, dp, cin be set ; func BitFTA0Circ (ap,bp,cp,dp,cin) -> strict gate`2=den Boolean Circuit of BitFTA0Str (ap,bp,cp,dp,cin) equals :: FTACELL1:def 2 (BitGFA0Circ (ap,bp,cp)) +* (BitGFA0Circ ((GFA0AdderOutput (ap,bp,cp)),cin,dp)); coherence (BitGFA0Circ (ap,bp,cp)) +* (BitGFA0Circ ((GFA0AdderOutput (ap,bp,cp)),cin,dp)) is strict gate`2=den Boolean Circuit of BitFTA0Str (ap,bp,cp,dp,cin) ; end; :: deftheorem defines BitFTA0Circ FTACELL1:def_2_:_ for ap, bp, cp, dp, cin being set holds BitFTA0Circ (ap,bp,cp,dp,cin) = (BitGFA0Circ (ap,bp,cp)) +* (BitGFA0Circ ((GFA0AdderOutput (ap,bp,cp)),cin,dp)); ::----------------------------------------------- :: 1-2. Properties of 1-bit FTA Circuit Structure (TYPE-0) ::----------------------------------------------- :: InnerVertices and InputVertices of 1-bit FTA Circuit Structure (FTA0) theorem Th1: :: FTACELL1:1 for ap, bp, cp, dp, cin being set holds InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) = (({[<*ap,bp*>,xor2],(GFA0AdderOutput (ap,bp,cp))} \/ {[<*ap,bp*>,and2],[<*bp,cp*>,and2],[<*cp,ap*>,and2],(GFA0CarryOutput (ap,bp,cp))}) \/ {[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp))}) \/ {[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,and2],[<*cin,dp*>,and2],[<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2],(GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp))} proofend; theorem :: FTACELL1:2 for ap, bp, cp, dp, cin being set holds InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) is Relation proofend; Lm1: for x, y, z, p being set holds GFA0AdderOutput (x,y,z) <> [p,and2] proofend; Lm2: for ap, bp, cp being non pair set for x, y, z being set holds InputVertices (BitGFA0Str (ap,bp,cp)) misses InnerVertices (BitGFA0Str (x,y,z)) proofend; theorem Th3: :: FTACELL1:3 for ap, bp, cp, dp being non pair set for cin being set st cin <> [<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2] & not cin in InnerVertices (BitGFA0Str (ap,bp,cp)) holds InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) = {ap,bp,cp,dp,cin} proofend; :: The Element of Carriers, InnerVertices and InputVertices (FTA0) theorem Th4: :: FTACELL1:4 for ap, bp, cp, dp, cin being set holds ( ap in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & bp in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & cp in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & dp in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & cin in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*ap,bp*>,xor2] in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & GFA0AdderOutput (ap,bp,cp) in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*ap,bp*>,and2] in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*bp,cp*>,and2] in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*cp,ap*>,and2] in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & GFA0CarryOutput (ap,bp,cp) in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*(GFA0AdderOutput (ap,bp,cp)),cin*>,xor2] in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp) in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*(GFA0AdderOutput (ap,bp,cp)),cin*>,and2] in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*cin,dp*>,and2] in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2] in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp) in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) ) proofend; theorem Th5: :: FTACELL1:5 for ap, bp, cp, dp, cin being set holds ( [<*ap,bp*>,xor2] in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & GFA0AdderOutput (ap,bp,cp) in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*ap,bp*>,and2] in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*bp,cp*>,and2] in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*cp,ap*>,and2] in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & GFA0CarryOutput (ap,bp,cp) in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*(GFA0AdderOutput (ap,bp,cp)),cin*>,xor2] in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp) in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*(GFA0AdderOutput (ap,bp,cp)),cin*>,and2] in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*cin,dp*>,and2] in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2] in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp) in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) ) proofend; theorem Th6: :: FTACELL1:6 for ap, bp, cp, dp being non pair set for cin being set st cin <> [<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2] & not cin in InnerVertices (BitGFA0Str (ap,bp,cp)) holds ( ap in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & bp in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & cp in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & dp in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & cin in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) ) proofend; ::------------------------------------------- :: 1-3. Output Definitions of the Combined Circuit ::------------------------------------------- :: Def. External/Internal Signal Outputs of 1-bit FTA TYPE-0 definition let ap, bp, cp, dp, cin be set ; func BitFTA0CarryOutput (ap,bp,cp,dp,cin) -> Element of InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) equals :: FTACELL1:def 3 GFA0CarryOutput (ap,bp,cp); coherence GFA0CarryOutput (ap,bp,cp) is Element of InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) by Th5; func BitFTA0AdderOutputI (ap,bp,cp,dp,cin) -> Element of InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) equals :: FTACELL1:def 4 GFA0AdderOutput (ap,bp,cp); coherence GFA0AdderOutput (ap,bp,cp) is Element of InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) by Th5; func BitFTA0AdderOutputP (ap,bp,cp,dp,cin) -> Element of InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) equals :: FTACELL1:def 5 GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp); coherence GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp) is Element of InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) by Th5; func BitFTA0AdderOutputQ (ap,bp,cp,dp,cin) -> Element of InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) equals :: FTACELL1:def 6 GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp); coherence GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp) is Element of InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) by Th5; end; :: deftheorem defines BitFTA0CarryOutput FTACELL1:def_3_:_ for ap, bp, cp, dp, cin being set holds BitFTA0CarryOutput (ap,bp,cp,dp,cin) = GFA0CarryOutput (ap,bp,cp); :: deftheorem defines BitFTA0AdderOutputI FTACELL1:def_4_:_ for ap, bp, cp, dp, cin being set holds BitFTA0AdderOutputI (ap,bp,cp,dp,cin) = GFA0AdderOutput (ap,bp,cp); :: deftheorem defines BitFTA0AdderOutputP FTACELL1:def_5_:_ for ap, bp, cp, dp, cin being set holds BitFTA0AdderOutputP (ap,bp,cp,dp,cin) = GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp); :: deftheorem defines BitFTA0AdderOutputQ FTACELL1:def_6_:_ for ap, bp, cp, dp, cin being set holds BitFTA0AdderOutputQ (ap,bp,cp,dp,cin) = GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp); ::---------------------------------------------------- :: 1-4. Stability of the Combined Circuit and its Outputs ::---------------------------------------------------- :: Intermediate (External/Internal) Carry/Adder Outputs after Two-steps theorem :: FTACELL1:7 for ap, bp, cp being non pair set for dp, cin being set for s being State of (BitFTA0Circ (ap,bp,cp,dp,cin)) for a1, a2, a3 being Element of BOOLEAN st a1 = s . ap & a2 = s . bp & a3 = s . cp holds ( (Following (s,2)) . (BitFTA0CarryOutput (ap,bp,cp,dp,cin)) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1) & (Following (s,2)) . (BitFTA0AdderOutputI (ap,bp,cp,dp,cin)) = (a1 'xor' a2) 'xor' a3 ) proofend; :: Temporal (Internal) Calculations after Two-steps theorem Th8: :: FTACELL1:8 for ap, bp, cp, dp being non pair set for cin being set st cin <> [<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2] & not cin in InnerVertices (BitGFA0Str (ap,bp,cp)) holds for s being State of (BitFTA0Circ (ap,bp,cp,dp,cin)) for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . ap & a2 = s . bp & a3 = s . cp & a4 = s . dp & a5 = s . cin holds ( (Following (s,2)) . (GFA0AdderOutput (ap,bp,cp)) = (a1 'xor' a2) 'xor' a3 & (Following (s,2)) . ap = a1 & (Following (s,2)) . bp = a2 & (Following (s,2)) . cp = a3 & (Following (s,2)) . dp = a4 & (Following (s,2)) . cin = a5 ) proofend; Lm3: for ap, bp, cp, dp being non pair set for cin being set for s being State of (BitFTA0Circ (ap,bp,cp,dp,cin)) for a123, a4, a5 being Element of BOOLEAN st a123 = s . (GFA0AdderOutput (ap,bp,cp)) & a4 = s . dp & a5 = s . cin holds ( (Following s) . [<*(GFA0AdderOutput (ap,bp,cp)),cin*>,and2] = a123 '&' a5 & (Following s) . [<*cin,dp*>,and2] = a5 '&' a4 & (Following s) . [<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2] = a4 '&' a123 ) proofend; Lm4: for ap, bp, cp, dp being non pair set for cin being set for s being State of (BitFTA0Circ (ap,bp,cp,dp,cin)) for a123, a5 being Element of BOOLEAN st a123 = s . (GFA0AdderOutput (ap,bp,cp)) & a5 = s . cin holds (Following s) . [<*(GFA0AdderOutput (ap,bp,cp)),cin*>,xor2] = a123 'xor' a5 proofend; Lm5: for ap, bp, cp, dp being non pair set for cin being set st cin <> [<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2] & not cin in InnerVertices (BitGFA0Str (ap,bp,cp)) holds for s being State of (BitFTA0Circ (ap,bp,cp,dp,cin)) for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . ap & a2 = s . bp & a3 = s . cp & a4 = s . dp & a5 = s . cin holds ( (Following (s,3)) . [<*(GFA0AdderOutput (ap,bp,cp)),cin*>,and2] = ((a1 'xor' a2) 'xor' a3) '&' a5 & (Following (s,3)) . [<*cin,dp*>,and2] = a5 '&' a4 & (Following (s,3)) . [<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2] = a4 '&' ((a1 'xor' a2) 'xor' a3) & (Following (s,3)) . ap = a1 & (Following (s,3)) . bp = a2 & (Following (s,3)) . cp = a3 & (Following (s,3)) . dp = a4 & (Following (s,3)) . cin = a5 ) proofend; Lm6: for ap, bp, cp, dp being non pair set for cin being set st cin <> [<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2] & not cin in InnerVertices (BitGFA0Str (ap,bp,cp)) holds for s being State of (BitFTA0Circ (ap,bp,cp,dp,cin)) for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . ap & a2 = s . bp & a3 = s . cp & a4 = s . dp & a5 = s . cin holds ( (Following (s,3)) . [<*(GFA0AdderOutput (ap,bp,cp)),cin*>,xor2] = ((a1 'xor' a2) 'xor' a3) 'xor' a5 & (Following (s,3)) . ap = a1 & (Following (s,3)) . bp = a2 & (Following (s,3)) . cp = a3 & (Following (s,3)) . dp = a4 & (Following (s,3)) . cin = a5 ) proofend; Lm7: for ap, bp, cp, dp being non pair set for cin being set for s being State of (BitFTA0Circ (ap,bp,cp,dp,cin)) for a123x, a123y, a123z being Element of BOOLEAN st a123x = s . [<*(GFA0AdderOutput (ap,bp,cp)),cin*>,and2] & a123y = s . [<*cin,dp*>,and2] & a123z = s . [<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2] holds (Following s) . (GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp)) = (a123x 'or' a123y) 'or' a123z proofend; Lm8: for ap, bp, cp, dp being non pair set for cin being set for s being State of (BitFTA0Circ (ap,bp,cp,dp,cin)) for a1235, a4 being Element of BOOLEAN st a1235 = s . [<*(GFA0AdderOutput (ap,bp,cp)),cin*>,xor2] & a4 = s . dp holds (Following s) . (GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp)) = a1235 'xor' a4 proofend; Lm9: for ap, bp, cp, dp being non pair set for cin being set st cin <> [<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2] & not cin in InnerVertices (BitGFA0Str (ap,bp,cp)) holds for s being State of (BitFTA0Circ (ap,bp,cp,dp,cin)) for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . ap & a2 = s . bp & a3 = s . cp & a4 = s . dp & a5 = s . cin holds ( (Following (s,4)) . (GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp)) = ((((a1 'xor' a2) 'xor' a3) '&' a5) 'or' (a5 '&' a4)) 'or' (a4 '&' ((a1 'xor' a2) 'xor' a3)) & (Following (s,4)) . ap = a1 & (Following (s,4)) . bp = a2 & (Following (s,4)) . cp = a3 & (Following (s,4)) . dp = a4 & (Following (s,4)) . cin = a5 ) proofend; Lm10: for ap, bp, cp, dp being non pair set for cin being set st cin <> [<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2] & not cin in InnerVertices (BitGFA0Str (ap,bp,cp)) holds for s being State of (BitFTA0Circ (ap,bp,cp,dp,cin)) for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . ap & a2 = s . bp & a3 = s . cp & a4 = s . dp & a5 = s . cin holds ( (Following (s,4)) . (GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp)) = (((a1 'xor' a2) 'xor' a3) 'xor' a4) 'xor' a5 & (Following (s,4)) . ap = a1 & (Following (s,4)) . bp = a2 & (Following (s,4)) . cp = a3 & (Following (s,4)) . dp = a4 & (Following (s,4)) . cin = a5 ) proofend; :: Main Proposition #1-1 (External Circuit Outputs after Four-steps) FTA0 theorem :: FTACELL1:9 for ap, bp, cp, dp being non pair set for cin being set st cin <> [<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2] & not cin in InnerVertices (BitGFA0Str (ap,bp,cp)) holds for s being State of (BitFTA0Circ (ap,bp,cp,dp,cin)) for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . ap & a2 = s . bp & a3 = s . cp & a4 = s . dp & a5 = s . cin holds ( (Following (s,4)) . (BitFTA0AdderOutputP (ap,bp,cp,dp,cin)) = ((((a1 'xor' a2) 'xor' a3) '&' a5) 'or' (a5 '&' a4)) 'or' (a4 '&' ((a1 'xor' a2) 'xor' a3)) & (Following (s,4)) . (BitFTA0AdderOutputQ (ap,bp,cp,dp,cin)) = (((a1 'xor' a2) 'xor' a3) 'xor' a4) 'xor' a5 ) by Lm9, Lm10; :: Main Proposition #1-2 (The Whole Circuit Stability after Four-steps) FTA0 theorem :: FTACELL1:10 for ap, bp, cp, dp being non pair set for cin being set st cin <> [<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2] holds for s being State of (BitFTA0Circ (ap,bp,cp,dp,cin)) holds Following (s,4) is stable proofend; begin ::======================================================================== :: [4-2 Binary Addition Cell_i : TYPE-1] :: :: Cell Module Symbol : :: :: a+ b- c+ d- Input : a+,b-,c+,d- (non pair set) :: | | | | cin+ (pair) :: +-*--O--*--O-+ cin+ :: | | / :: +--* FTA TYPE-1 *--+ Output : p-,q+,cout+ (pair) :: / | | :: cout+ +---O----*---+ :: | | :: p- q+ :: :: Composition : Cascade by Adder Output together with GFA TYPE-1 and TYPE-2 :: Function : -p[i+1] + q[i] + Intermediate_Carry_out :: = a[i] - b[i] + c[i] - d[i] + Intermediate_Carry_in :: :: a^{+}[i] b^{-}[i] :: | / :: | / :: +---*---O :: | GFA *---- c^{+}[i] Circuit Composition : :: | TYPE1 | BitGFA1Str(a+,b-,c+) :: *---O---+ BitGFA2Str(A1,cin,d-) :: / | cin[i] ---> :: / A1| / FTA1Str(a+,b-,c+,d-,cin) :: cout[i+1] | / :: +---O---* Intermediate Addition and Carry: :: | GFA O---- d^{-}[i] A1 <= GFA1AdderOutput :: | TYPE2 | cout[i+1] <= GFA1CarryOutput :: O---*---+ q[i] <= GFA2AdderOutput :: / | p[i+1] <= GFA2CarryOutput :: / | :: p^{-}[i+1] q^{+}[i] :: :: Calculation Stability : Following(s,2+2) is stable. :: ::========================================================================= ::--------------------------------------------------------------- :: 2-1. Circuit Definition for Intermediate Addition and Carry Circuit (TYPE-1) ::--------------------------------------------------------------- :: Def. Combined Circuit Structure of 1-bit FTA TYPE-1 definition let ap, bm, cp, dm, cin be set ; func BitFTA1Str (ap,bm,cp,dm,cin) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: FTACELL1:def 7 (BitGFA1Str (ap,bm,cp)) +* (BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm)); coherence (BitGFA1Str (ap,bm,cp)) +* (BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm)) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ; end; :: deftheorem defines BitFTA1Str FTACELL1:def_7_:_ for ap, bm, cp, dm, cin being set holds BitFTA1Str (ap,bm,cp,dm,cin) = (BitGFA1Str (ap,bm,cp)) +* (BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm)); definition let ap, bm, cp, dm, cin be set ; func BitFTA1Circ (ap,bm,cp,dm,cin) -> strict gate`2=den Boolean Circuit of BitFTA1Str (ap,bm,cp,dm,cin) equals :: FTACELL1:def 8 (BitGFA1Circ (ap,bm,cp)) +* (BitGFA2Circ ((GFA1AdderOutput (ap,bm,cp)),cin,dm)); coherence (BitGFA1Circ (ap,bm,cp)) +* (BitGFA2Circ ((GFA1AdderOutput (ap,bm,cp)),cin,dm)) is strict gate`2=den Boolean Circuit of BitFTA1Str (ap,bm,cp,dm,cin) ; end; :: deftheorem defines BitFTA1Circ FTACELL1:def_8_:_ for ap, bm, cp, dm, cin being set holds BitFTA1Circ (ap,bm,cp,dm,cin) = (BitGFA1Circ (ap,bm,cp)) +* (BitGFA2Circ ((GFA1AdderOutput (ap,bm,cp)),cin,dm)); ::----------------------------------------------- :: 2-2. Properties of 1-bit FTA Structure and Circuit (TYPE-1) ::----------------------------------------------- :: InnerVertices and InputVertices of 1-bit FTA Circuit Structure (FTA1) theorem Th11: :: FTACELL1:11 for ap, bm, cp, dm, cin being set holds InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) = (({[<*ap,bm*>,xor2c],(GFA1AdderOutput (ap,bm,cp))} \/ {[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))}) \/ {[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c],(GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))}) \/ {[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a],[<*cin,dm*>,and2c],[<*dm,(GFA1AdderOutput (ap,bm,cp))*>,and2b],(GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))} proofend; theorem :: FTACELL1:12 for ap, bm, cp, dm, cin being set holds InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) is Relation proofend; Lm11: for x, y, z, p being set holds GFA1AdderOutput (x,y,z) <> [p,and2c] proofend; Lm12: for ap, bm, cp being non pair set for x, y, z being set holds InputVertices (BitGFA1Str (ap,bm,cp)) misses InnerVertices (BitGFA2Str (x,y,z)) proofend; theorem Th13: :: FTACELL1:13 for ap, bm, cp, dm being non pair set for cin being set st cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,and2b] & not cin in InnerVertices (BitGFA1Str (ap,bm,cp)) holds InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) = {ap,bm,cp,dm,cin} proofend; :: The Element of Carriers, InnerVertices and InputVertices (FTA1) theorem Th14: :: FTACELL1:14 for ap, bm, cp, dm, cin being set holds ( ap in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & bm in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & cp in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & dm in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & cin in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*ap,bm*>,xor2c] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA1AdderOutput (ap,bm,cp) in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*ap,bm*>,and2c] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*bm,cp*>,and2a] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*cp,ap*>,and2] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA1CarryOutput (ap,bm,cp) in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm) in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*cin,dm*>,and2c] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,and2b] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm) in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) ) proofend; theorem Th15: :: FTACELL1:15 for ap, bm, cp, dm, cin being set holds ( [<*ap,bm*>,xor2c] in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA1AdderOutput (ap,bm,cp) in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*ap,bm*>,and2c] in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*bm,cp*>,and2a] in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*cp,ap*>,and2] in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA1CarryOutput (ap,bm,cp) in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c] in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm) in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a] in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*cin,dm*>,and2c] in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,and2b] in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm) in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) ) proofend; theorem Th16: :: FTACELL1:16 for ap, bm, cp, dm being non pair set for cin being set st cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,and2b] & not cin in InnerVertices (BitGFA1Str (ap,bm,cp)) holds ( ap in InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & bm in InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & cp in InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & dm in InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & cin in InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) ) proofend; ::------------------------------------------- :: 2-3. Output Definitions of the Combined Circuit ::------------------------------------------- :: Def. External/Internal Signal Outputs of 1-bit FTA TYPE-1 definition let ap, bm, cp, dm, cin be set ; func BitFTA1CarryOutput (ap,bm,cp,dm,cin) -> Element of InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) equals :: FTACELL1:def 9 GFA1CarryOutput (ap,bm,cp); coherence GFA1CarryOutput (ap,bm,cp) is Element of InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) by Th15; func BitFTA1AdderOutputI (ap,bm,cp,dm,cin) -> Element of InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) equals :: FTACELL1:def 10 GFA1AdderOutput (ap,bm,cp); coherence GFA1AdderOutput (ap,bm,cp) is Element of InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) by Th15; func BitFTA1AdderOutputP (ap,bm,cp,dm,cin) -> Element of InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) equals :: FTACELL1:def 11 GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm); coherence GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm) is Element of InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) by Th15; func BitFTA1AdderOutputQ (ap,bm,cp,dm,cin) -> Element of InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) equals :: FTACELL1:def 12 GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm); coherence GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm) is Element of InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) by Th15; end; :: deftheorem defines BitFTA1CarryOutput FTACELL1:def_9_:_ for ap, bm, cp, dm, cin being set holds BitFTA1CarryOutput (ap,bm,cp,dm,cin) = GFA1CarryOutput (ap,bm,cp); :: deftheorem defines BitFTA1AdderOutputI FTACELL1:def_10_:_ for ap, bm, cp, dm, cin being set holds BitFTA1AdderOutputI (ap,bm,cp,dm,cin) = GFA1AdderOutput (ap,bm,cp); :: deftheorem defines BitFTA1AdderOutputP FTACELL1:def_11_:_ for ap, bm, cp, dm, cin being set holds BitFTA1AdderOutputP (ap,bm,cp,dm,cin) = GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm); :: deftheorem defines BitFTA1AdderOutputQ FTACELL1:def_12_:_ for ap, bm, cp, dm, cin being set holds BitFTA1AdderOutputQ (ap,bm,cp,dm,cin) = GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm); ::----------------------------------- :: 2-4. Stability of the Combined Circuit and its Outputs ::----------------------------------- :: Intermediate (External/Internal) Carry/Adder Outputs after Two-steps theorem :: FTACELL1:17 for ap, bm, cp being non pair set for dm, cin being set for s being State of (BitFTA1Circ (ap,bm,cp,dm,cin)) for a1, a2, a3 being Element of BOOLEAN st a1 = s . ap & a2 = s . bm & a3 = s . cp holds ( (Following (s,2)) . (BitFTA1CarryOutput (ap,bm,cp,dm,cin)) = ((a1 '&' ('not' a2)) 'or' (('not' a2) '&' a3)) 'or' (a3 '&' a1) & (Following (s,2)) . (BitFTA1AdderOutputI (ap,bm,cp,dm,cin)) = 'not' ((a1 'xor' ('not' a2)) 'xor' a3) ) proofend; :: Temporal (Internal) Calculations after Two-steps theorem Th18: :: FTACELL1:18 for ap, bm, cp, dm being non pair set for cin being set st cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,and2b] & not cin in InnerVertices (BitGFA1Str (ap,bm,cp)) holds for s being State of (BitFTA1Circ (ap,bm,cp,dm,cin)) for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . ap & a2 = s . bm & a3 = s . cp & a4 = s . dm & a5 = s . cin holds ( (Following (s,2)) . (GFA1AdderOutput (ap,bm,cp)) = 'not' ((a1 'xor' ('not' a2)) 'xor' a3) & (Following (s,2)) . ap = a1 & (Following (s,2)) . bm = a2 & (Following (s,2)) . cp = a3 & (Following (s,2)) . dm = a4 & (Following (s,2)) . cin = a5 ) proofend; Lm13: for ap, bm, cp, dm being non pair set for cin being set for s being State of (BitFTA1Circ (ap,bm,cp,dm,cin)) for a123, a4, a5 being Element of BOOLEAN st a123 = s . (GFA1AdderOutput (ap,bm,cp)) & a4 = s . dm & a5 = s . cin holds ( (Following s) . [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a] = ('not' a123) '&' a5 & (Following s) . [<*cin,dm*>,and2c] = a5 '&' ('not' a4) & (Following s) . [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,and2b] = ('not' a4) '&' ('not' a123) ) proofend; Lm14: for ap, bm, cp, dm being non pair set for cin being set for s being State of (BitFTA1Circ (ap,bm,cp,dm,cin)) for a123, a5 being Element of BOOLEAN st a123 = s . (GFA1AdderOutput (ap,bm,cp)) & a5 = s . cin holds (Following s) . [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c] = a123 'xor' ('not' a5) proofend; Lm15: for ap, bm, cp, dm being non pair set for cin being set st cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,and2b] & not cin in InnerVertices (BitGFA1Str (ap,bm,cp)) holds for s being State of (BitFTA1Circ (ap,bm,cp,dm,cin)) for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . ap & a2 = s . bm & a3 = s . cp & a4 = s . dm & a5 = s . cin holds ( (Following (s,3)) . [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a] = ((a1 'xor' ('not' a2)) 'xor' a3) '&' a5 & (Following (s,3)) . [<*cin,dm*>,and2c] = a5 '&' ('not' a4) & (Following (s,3)) . [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,and2b] = ('not' a4) '&' ((a1 'xor' ('not' a2)) 'xor' a3) & (Following (s,3)) . ap = a1 & (Following (s,3)) . bm = a2 & (Following (s,3)) . cp = a3 & (Following (s,3)) . dm = a4 & (Following (s,3)) . cin = a5 ) proofend; Lm16: for ap, bm, cp, dm being non pair set for cin being set st cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,and2b] & not cin in InnerVertices (BitGFA1Str (ap,bm,cp)) holds for s being State of (BitFTA1Circ (ap,bm,cp,dm,cin)) for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . ap & a2 = s . bm & a3 = s . cp & a4 = s . dm & a5 = s . cin holds ( (Following (s,3)) . [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c] = ('not' ((a1 'xor' ('not' a2)) 'xor' a3)) 'xor' ('not' a5) & (Following (s,3)) . ap = a1 & (Following (s,3)) . bm = a2 & (Following (s,3)) . cp = a3 & (Following (s,3)) . dm = a4 & (Following (s,3)) . cin = a5 ) proofend; Lm17: for ap, bm, cp, dm being non pair set for cin being set for s being State of (BitFTA1Circ (ap,bm,cp,dm,cin)) for a123x, a123y, a123z being Element of BOOLEAN st a123x = s . [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a] & a123y = s . [<*cin,dm*>,and2c] & a123z = s . [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,and2b] holds (Following s) . (GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm)) = 'not' ((a123x 'or' a123y) 'or' a123z) proofend; Lm18: for ap, bm, cp, dm being non pair set for cin being set for s being State of (BitFTA1Circ (ap,bm,cp,dm,cin)) for a1235, a4 being Element of BOOLEAN st a1235 = s . [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c] & a4 = s . dm holds (Following s) . (GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm)) = a1235 'xor' ('not' a4) proofend; Lm19: for ap, bm, cp, dm being non pair set for cin being set st cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,and2b] & not cin in InnerVertices (BitGFA1Str (ap,bm,cp)) holds for s being State of (BitFTA1Circ (ap,bm,cp,dm,cin)) for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . ap & a2 = s . bm & a3 = s . cp & a4 = s . dm & a5 = s . cin holds ( (Following (s,4)) . (GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm)) = 'not' (((((a1 'xor' ('not' a2)) 'xor' a3) '&' a5) 'or' (a5 '&' ('not' a4))) 'or' (('not' a4) '&' ((a1 'xor' ('not' a2)) 'xor' a3))) & (Following (s,4)) . ap = a1 & (Following (s,4)) . bm = a2 & (Following (s,4)) . cp = a3 & (Following (s,4)) . dm = a4 & (Following (s,4)) . cin = a5 ) proofend; Lm20: for ap, bm, cp, dm being non pair set for cin being set st cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,and2b] & not cin in InnerVertices (BitGFA1Str (ap,bm,cp)) holds for s being State of (BitFTA1Circ (ap,bm,cp,dm,cin)) for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . ap & a2 = s . bm & a3 = s . cp & a4 = s . dm & a5 = s . cin holds ( (Following (s,4)) . (GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm)) = (((a1 'xor' ('not' a2)) 'xor' a3) 'xor' ('not' a4)) 'xor' a5 & (Following (s,4)) . ap = a1 & (Following (s,4)) . bm = a2 & (Following (s,4)) . cp = a3 & (Following (s,4)) . dm = a4 & (Following (s,4)) . cin = a5 ) proofend; :: Main Proposition #2-1 (External Circuit Outputs after Four-steps) FTA1 theorem :: FTACELL1:19 for ap, bm, cp, dm being non pair set for cin being set st cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,and2b] & not cin in InnerVertices (BitGFA1Str (ap,bm,cp)) holds for s being State of (BitFTA1Circ (ap,bm,cp,dm,cin)) for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . ap & a2 = s . bm & a3 = s . cp & a4 = s . dm & a5 = s . cin holds ( (Following (s,4)) . (BitFTA1AdderOutputP (ap,bm,cp,dm,cin)) = 'not' (((((a1 'xor' ('not' a2)) 'xor' a3) '&' a5) 'or' (a5 '&' ('not' a4))) 'or' (('not' a4) '&' ((a1 'xor' ('not' a2)) 'xor' a3))) & (Following (s,4)) . (BitFTA1AdderOutputQ (ap,bm,cp,dm,cin)) = (((a1 'xor' ('not' a2)) 'xor' a3) 'xor' ('not' a4)) 'xor' a5 ) by Lm19, Lm20; :: Main Proposition #2-2 (The Whole Circuit Stability after Four-steps) FTA1 theorem :: FTACELL1:20 for ap, bm, cp, dm being non pair set for cin being set st cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,and2b] holds for s being State of (BitFTA1Circ (ap,bm,cp,dm,cin)) holds Following (s,4) is stable proofend; begin ::======================================================================== :: [4-2 Binary Addition Cell_i : TYPE-2] :: :: Cell Module Symbol : :: :: a- b+ c- d+ Input : a-,b+,c-,d+ (non pair set) :: | | | | cin- (pair) :: +-O--*--O--*-+ cin- :: | | / :: +--O FTA TYPE-2 O--+ Output : p+,q-,cout- (pair) :: / | | :: cout- +---*----O---+ :: | | :: p+ q- :: :: Composition : Cascade by Adder Output together with GFA TYPE-2 and TYPE-1 :: Function : p[i+1] - q[i] - Intermediate_Carry_out :: = -a[i] + b[i] - c[i] + d[i] - Intermediate_Carry_in :: :: a^{-}[i] b^{+}[i] :: | / :: | / :: +---O---* :: | GFA O---- c^{-}[i] Circuit Composition : :: | TYPE2 | BitGFA2Str(a-,b+,c-) :: O---*---+ BitGFA1Str(A1,cin,d+) :: / | cin[i] ---> :: / A1| / FTA2Str(a-,b+,c-,d+,cin) :: cout[i+1] | / :: +---*---O Intermediate Addition and Carry: :: | GFA *---- d^{+}[i] A1 <= GFA2AdderOutput :: | TYPE1 | cout[i+1] <= GFA2CarryOutput :: *---O---+ q[i] <= GFA1AdderOutput :: / | p[i+1] <= GFA1CarryOutput :: / | :: p^{+}[i+1] q^{-}[i] :: :: Calculation Stability : Following(s,2+2) is stable. :: ::========================================================================= ::--------------------------------------------------------------- :: 3-1. Circuit Definition for Intermediate Addition and Carry Circuit (TYPE-2) ::--------------------------------------------------------------- :: Def. Combined Circuit Structure of 1-bit FTA TYPE-2 definition let am, bp, cm, dp, cin be set ; func BitFTA2Str (am,bp,cm,dp,cin) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: FTACELL1:def 13 (BitGFA2Str (am,bp,cm)) +* (BitGFA1Str ((GFA2AdderOutput (am,bp,cm)),cin,dp)); coherence (BitGFA2Str (am,bp,cm)) +* (BitGFA1Str ((GFA2AdderOutput (am,bp,cm)),cin,dp)) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ; end; :: deftheorem defines BitFTA2Str FTACELL1:def_13_:_ for am, bp, cm, dp, cin being set holds BitFTA2Str (am,bp,cm,dp,cin) = (BitGFA2Str (am,bp,cm)) +* (BitGFA1Str ((GFA2AdderOutput (am,bp,cm)),cin,dp)); definition let am, bp, cm, dp, cin be set ; func BitFTA2Circ (am,bp,cm,dp,cin) -> strict gate`2=den Boolean Circuit of BitFTA2Str (am,bp,cm,dp,cin) equals :: FTACELL1:def 14 (BitGFA2Circ (am,bp,cm)) +* (BitGFA1Circ ((GFA2AdderOutput (am,bp,cm)),cin,dp)); coherence (BitGFA2Circ (am,bp,cm)) +* (BitGFA1Circ ((GFA2AdderOutput (am,bp,cm)),cin,dp)) is strict gate`2=den Boolean Circuit of BitFTA2Str (am,bp,cm,dp,cin) ; end; :: deftheorem defines BitFTA2Circ FTACELL1:def_14_:_ for am, bp, cm, dp, cin being set holds BitFTA2Circ (am,bp,cm,dp,cin) = (BitGFA2Circ (am,bp,cm)) +* (BitGFA1Circ ((GFA2AdderOutput (am,bp,cm)),cin,dp)); ::----------------------------------------------- :: 3-2. Properties of 1-bit FTA Structure and Circuit (TYPE-2) ::----------------------------------------------- :: InnerVertices and InputVertices of 1-bit FTA Circuit Structure (FTA2) theorem Th21: :: FTACELL1:21 for am, bp, cm, dp, cin being set holds InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) = (({[<*am,bp*>,xor2c],(GFA2AdderOutput (am,bp,cm))} \/ {[<*am,bp*>,and2a],[<*bp,cm*>,and2c],[<*cm,am*>,and2b],(GFA2CarryOutput (am,bp,cm))}) \/ {[<*(GFA2AdderOutput (am,bp,cm)),cin*>,xor2c],(GFA1AdderOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp))}) \/ {[<*(GFA2AdderOutput (am,bp,cm)),cin*>,and2c],[<*cin,dp*>,and2a],[<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2],(GFA1CarryOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp))} proofend; theorem :: FTACELL1:22 for am, bp, cm, dp, cin being set holds InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) is Relation proofend; Lm21: for x, y, z, p being set holds GFA2AdderOutput (x,y,z) <> [p,and2a] proofend; Lm22: for am, bp, cm being non pair set for x, y, z being set holds InputVertices (BitGFA2Str (am,bp,cm)) misses InnerVertices (BitGFA1Str (x,y,z)) proofend; theorem Th23: :: FTACELL1:23 for am, bp, cm, dp being non pair set for cin being set st cin <> [<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2] & not cin in InnerVertices (BitGFA2Str (am,bp,cm)) holds InputVertices (BitFTA2Str (am,bp,cm,dp,cin)) = {am,bp,cm,dp,cin} proofend; :: The Element of Carriers, InnerVertices and InputVertices (FTA2) theorem Th24: :: FTACELL1:24 for am, bp, cm, dp, cin being set holds ( am in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & bp in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & cm in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & dp in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & cin in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*am,bp*>,xor2c] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & GFA2AdderOutput (am,bp,cm) in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*am,bp*>,and2a] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*bp,cm*>,and2c] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*cm,am*>,and2b] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & GFA2CarryOutput (am,bp,cm) in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*(GFA2AdderOutput (am,bp,cm)),cin*>,xor2c] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & GFA1AdderOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp) in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*(GFA2AdderOutput (am,bp,cm)),cin*>,and2c] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*cin,dp*>,and2a] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & GFA1CarryOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp) in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) ) proofend; theorem Th25: :: FTACELL1:25 for am, bp, cm, dp, cin being set holds ( [<*am,bp*>,xor2c] in InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) & GFA2AdderOutput (am,bp,cm) in InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) & [<*am,bp*>,and2a] in InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) & [<*bp,cm*>,and2c] in InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) & [<*cm,am*>,and2b] in InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) & GFA2CarryOutput (am,bp,cm) in InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) & [<*(GFA2AdderOutput (am,bp,cm)),cin*>,xor2c] in InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) & GFA1AdderOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp) in InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) & [<*(GFA2AdderOutput (am,bp,cm)),cin*>,and2c] in InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) & [<*cin,dp*>,and2a] in InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) & [<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2] in InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) & GFA1CarryOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp) in InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) ) proofend; theorem Th26: :: FTACELL1:26 for am, bp, cm, dp being non pair set for cin being set st cin <> [<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2] & not cin in InnerVertices (BitGFA2Str (am,bp,cm)) holds ( am in InputVertices (BitFTA2Str (am,bp,cm,dp,cin)) & bp in InputVertices (BitFTA2Str (am,bp,cm,dp,cin)) & cm in InputVertices (BitFTA2Str (am,bp,cm,dp,cin)) & dp in InputVertices (BitFTA2Str (am,bp,cm,dp,cin)) & cin in InputVertices (BitFTA2Str (am,bp,cm,dp,cin)) ) proofend; ::------------------------------------------- :: 3-3. Output Definitions of the Combined Circuit ::------------------------------------------- :: Def. External/Internal Signal Outputs of 1-bit FTA TYPE-2 definition let am, bp, cm, dp, cin be set ; func BitFTA2CarryOutput (am,bp,cm,dp,cin) -> Element of InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) equals :: FTACELL1:def 15 GFA2CarryOutput (am,bp,cm); coherence GFA2CarryOutput (am,bp,cm) is Element of InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) by Th25; func BitFTA2AdderOutputI (am,bp,cm,dp,cin) -> Element of InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) equals :: FTACELL1:def 16 GFA2AdderOutput (am,bp,cm); coherence GFA2AdderOutput (am,bp,cm) is Element of InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) by Th25; func BitFTA2AdderOutputP (am,bp,cm,dp,cin) -> Element of InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) equals :: FTACELL1:def 17 GFA1CarryOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp); coherence GFA1CarryOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp) is Element of InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) by Th25; func BitFTA2AdderOutputQ (am,bp,cm,dp,cin) -> Element of InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) equals :: FTACELL1:def 18 GFA1AdderOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp); coherence GFA1AdderOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp) is Element of InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) by Th25; end; :: deftheorem defines BitFTA2CarryOutput FTACELL1:def_15_:_ for am, bp, cm, dp, cin being set holds BitFTA2CarryOutput (am,bp,cm,dp,cin) = GFA2CarryOutput (am,bp,cm); :: deftheorem defines BitFTA2AdderOutputI FTACELL1:def_16_:_ for am, bp, cm, dp, cin being set holds BitFTA2AdderOutputI (am,bp,cm,dp,cin) = GFA2AdderOutput (am,bp,cm); :: deftheorem defines BitFTA2AdderOutputP FTACELL1:def_17_:_ for am, bp, cm, dp, cin being set holds BitFTA2AdderOutputP (am,bp,cm,dp,cin) = GFA1CarryOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp); :: deftheorem defines BitFTA2AdderOutputQ FTACELL1:def_18_:_ for am, bp, cm, dp, cin being set holds BitFTA2AdderOutputQ (am,bp,cm,dp,cin) = GFA1AdderOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp); ::----------------------------------- :: 3-4. Stability of the Combined Circuit and its Outputs ::----------------------------------- :: Intermediate (External/Internal) Carry/Adder Outputs after Two-steps theorem :: FTACELL1:27 for am, bp, cm being non pair set for dp, cin being set for s being State of (BitFTA2Circ (am,bp,cm,dp,cin)) for a1, a2, a3 being Element of BOOLEAN st a1 = s . am & a2 = s . bp & a3 = s . cm holds ( (Following (s,2)) . (BitFTA2CarryOutput (am,bp,cm,dp,cin)) = 'not' (((('not' a1) '&' a2) 'or' (a2 '&' ('not' a3))) 'or' (('not' a3) '&' ('not' a1))) & (Following (s,2)) . (BitFTA2AdderOutputI (am,bp,cm,dp,cin)) = (('not' a1) 'xor' a2) 'xor' ('not' a3) ) proofend; :: Temporal (Internal) Calculations after Two-steps theorem Th28: :: FTACELL1:28 for am, bp, cm, dp being non pair set for cin being set st cin <> [<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2] & not cin in InnerVertices (BitGFA2Str (am,bp,cm)) holds for s being State of (BitFTA2Circ (am,bp,cm,dp,cin)) for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . am & a2 = s . bp & a3 = s . cm & a4 = s . dp & a5 = s . cin holds ( (Following (s,2)) . (GFA2AdderOutput (am,bp,cm)) = (('not' a1) 'xor' a2) 'xor' ('not' a3) & (Following (s,2)) . am = a1 & (Following (s,2)) . bp = a2 & (Following (s,2)) . cm = a3 & (Following (s,2)) . dp = a4 & (Following (s,2)) . cin = a5 ) proofend; Lm23: for am, bp, cm, dp being non pair set for cin being set for s being State of (BitFTA2Circ (am,bp,cm,dp,cin)) for a123, a4, a5 being Element of BOOLEAN st a123 = s . (GFA2AdderOutput (am,bp,cm)) & a4 = s . dp & a5 = s . cin holds ( (Following s) . [<*(GFA2AdderOutput (am,bp,cm)),cin*>,and2c] = a123 '&' ('not' a5) & (Following s) . [<*cin,dp*>,and2a] = ('not' a5) '&' a4 & (Following s) . [<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2] = a4 '&' a123 ) proofend; Lm24: for am, bp, cm, dp being non pair set for cin being set for s being State of (BitFTA2Circ (am,bp,cm,dp,cin)) for a123, a5 being Element of BOOLEAN st a123 = s . (GFA2AdderOutput (am,bp,cm)) & a5 = s . cin holds (Following s) . [<*(GFA2AdderOutput (am,bp,cm)),cin*>,xor2c] = a123 'xor' ('not' a5) proofend; Lm25: for am, bp, cm, dp being non pair set for cin being set st cin <> [<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2] & not cin in InnerVertices (BitGFA2Str (am,bp,cm)) holds for s being State of (BitFTA2Circ (am,bp,cm,dp,cin)) for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . am & a2 = s . bp & a3 = s . cm & a4 = s . dp & a5 = s . cin holds ( (Following (s,3)) . [<*(GFA2AdderOutput (am,bp,cm)),cin*>,and2c] = ((('not' a1) 'xor' a2) 'xor' ('not' a3)) '&' ('not' a5) & (Following (s,3)) . [<*cin,dp*>,and2a] = ('not' a5) '&' a4 & (Following (s,3)) . [<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2] = a4 '&' ((('not' a1) 'xor' a2) 'xor' ('not' a3)) & (Following (s,3)) . am = a1 & (Following (s,3)) . bp = a2 & (Following (s,3)) . cm = a3 & (Following (s,3)) . dp = a4 & (Following (s,3)) . cin = a5 ) proofend; Lm26: for am, bp, cm, dp being non pair set for cin being set st cin <> [<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2] & not cin in InnerVertices (BitGFA2Str (am,bp,cm)) holds for s being State of (BitFTA2Circ (am,bp,cm,dp,cin)) for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . am & a2 = s . bp & a3 = s . cm & a4 = s . dp & a5 = s . cin holds ( (Following (s,3)) . [<*(GFA2AdderOutput (am,bp,cm)),cin*>,xor2c] = ((('not' a1) 'xor' a2) 'xor' ('not' a3)) 'xor' ('not' a5) & (Following (s,3)) . am = a1 & (Following (s,3)) . bp = a2 & (Following (s,3)) . cm = a3 & (Following (s,3)) . dp = a4 & (Following (s,3)) . cin = a5 ) proofend; Lm27: for am, bp, cm, dp being non pair set for cin being set for s being State of (BitFTA2Circ (am,bp,cm,dp,cin)) for a123x, a123y, a123z being Element of BOOLEAN st a123x = s . [<*(GFA2AdderOutput (am,bp,cm)),cin*>,and2c] & a123y = s . [<*cin,dp*>,and2a] & a123z = s . [<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2] holds (Following s) . (GFA1CarryOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp)) = (a123x 'or' a123y) 'or' a123z proofend; Lm28: for am, bp, cm, dp being non pair set for cin being set for s being State of (BitFTA2Circ (am,bp,cm,dp,cin)) for a1235, a4 being Element of BOOLEAN st a1235 = s . [<*(GFA2AdderOutput (am,bp,cm)),cin*>,xor2c] & a4 = s . dp holds (Following s) . (GFA1AdderOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp)) = a1235 'xor' ('not' a4) proofend; Lm29: for am, bp, cm, dp being non pair set for cin being set st cin <> [<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2] & not cin in InnerVertices (BitGFA2Str (am,bp,cm)) holds for s being State of (BitFTA2Circ (am,bp,cm,dp,cin)) for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . am & a2 = s . bp & a3 = s . cm & a4 = s . dp & a5 = s . cin holds ( (Following (s,4)) . (GFA1CarryOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp)) = ((((('not' a1) 'xor' a2) 'xor' ('not' a3)) '&' ('not' a5)) 'or' (('not' a5) '&' a4)) 'or' (a4 '&' ((('not' a1) 'xor' a2) 'xor' ('not' a3))) & (Following (s,4)) . am = a1 & (Following (s,4)) . bp = a2 & (Following (s,4)) . cm = a3 & (Following (s,4)) . dp = a4 & (Following (s,4)) . cin = a5 ) proofend; Lm30: for am, bp, cm, dp being non pair set for cin being set st cin <> [<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2] & not cin in InnerVertices (BitGFA2Str (am,bp,cm)) holds for s being State of (BitFTA2Circ (am,bp,cm,dp,cin)) for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . am & a2 = s . bp & a3 = s . cm & a4 = s . dp & a5 = s . cin holds ( (Following (s,4)) . (GFA1AdderOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp)) = 'not' ((((('not' a1) 'xor' a2) 'xor' ('not' a3)) 'xor' a4) 'xor' ('not' a5)) & (Following (s,4)) . am = a1 & (Following (s,4)) . bp = a2 & (Following (s,4)) . cm = a3 & (Following (s,4)) . dp = a4 & (Following (s,4)) . cin = a5 ) proofend; :: Main Proposition #3-1 (External Circuit Outputs after Four-steps) FTA2 theorem :: FTACELL1:29 for am, bp, cm, dp being non pair set for cin being set st cin <> [<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2] & not cin in InnerVertices (BitGFA2Str (am,bp,cm)) holds for s being State of (BitFTA2Circ (am,bp,cm,dp,cin)) for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . am & a2 = s . bp & a3 = s . cm & a4 = s . dp & a5 = s . cin holds ( (Following (s,4)) . (BitFTA2AdderOutputP (am,bp,cm,dp,cin)) = ((((('not' a1) 'xor' a2) 'xor' ('not' a3)) '&' ('not' a5)) 'or' (('not' a5) '&' a4)) 'or' (a4 '&' ((('not' a1) 'xor' a2) 'xor' ('not' a3))) & (Following (s,4)) . (BitFTA2AdderOutputQ (am,bp,cm,dp,cin)) = 'not' ((((('not' a1) 'xor' a2) 'xor' ('not' a3)) 'xor' a4) 'xor' ('not' a5)) ) by Lm29, Lm30; :: Main Proposition #3-2 (The Whole Circuit Stability after Four-steps) FTA2 theorem :: FTACELL1:30 for am, bp, cm, dp being non pair set for cin being set st cin <> [<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2] holds for s being State of (BitFTA2Circ (am,bp,cm,dp,cin)) holds Following (s,4) is stable proofend; begin ::======================================================================== :: [4-2 Binary Addition Cell_i : TYPE-3] :: :: Cell Module Symbol : :: :: a- b- c- d- Input : a-,b-,c-,d- (non pair set) :: | | | | cin- (pair) :: +-O--O--O--O-+ cin- :: | | / :: +--O FTA TYPE-3 O--+ Output : p-,q-,cout- (pair) :: / | | :: cout- +---O----O---+ :: | | :: p- q- :: :: Composition : Cascade by Adder Output together with two GFA TYPE-3 :: Function : -p[i+1] - q[i] - Intermediate_Carry_out :: = -a[i] - b[i] - c[i] - d[i] - Intermediate_Carry_in :: :: a^{-}[i] b^{-}[i] :: | / :: | / :: +---O---O :: | GFA O---- c^{-}[i] Circuit Composition : :: | TYPE3 | BitGFA3Str(a-,b-,c-) :: O---O---+ BitGFA3Str(A1,cin,d-) :: / | cin[i] ---> :: / A1| / FTA3Str(a-,b-,c-,d-,cin) :: cout[i+1] | / :: +---O---O Intermediate Addition and Carry: :: | GFA O---- d^{-}[i] A1 <= GFA3AdderOutput :: | TYPE3 | cout[i+1] <= GFA3CarryOutput :: O---O---+ q[i] <= GFA3AdderOutput :: / | p[i+1] <= GFA3CarryOutput :: / | :: p^{-}[i+1] q^{-}[i] :: :: Calculation Stability : Following(s,2+2) is stable. :: ::========================================================================= ::--------------------------------------------------------------- :: 4-1. Circuit Definition for Intermediate Addition and Carry Circuit (TYPE-3) ::--------------------------------------------------------------- :: Def. Combined Circuit Structure of 1-bit FTA TYPE-2 definition let am, bm, cm, dm, cin be set ; func BitFTA3Str (am,bm,cm,dm,cin) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: FTACELL1:def 19 (BitGFA3Str (am,bm,cm)) +* (BitGFA3Str ((GFA3AdderOutput (am,bm,cm)),cin,dm)); coherence (BitGFA3Str (am,bm,cm)) +* (BitGFA3Str ((GFA3AdderOutput (am,bm,cm)),cin,dm)) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ; end; :: deftheorem defines BitFTA3Str FTACELL1:def_19_:_ for am, bm, cm, dm, cin being set holds BitFTA3Str (am,bm,cm,dm,cin) = (BitGFA3Str (am,bm,cm)) +* (BitGFA3Str ((GFA3AdderOutput (am,bm,cm)),cin,dm)); definition let am, bm, cm, dm, cin be set ; func BitFTA3Circ (am,bm,cm,dm,cin) -> strict gate`2=den Boolean Circuit of BitFTA3Str (am,bm,cm,dm,cin) equals :: FTACELL1:def 20 (BitGFA3Circ (am,bm,cm)) +* (BitGFA3Circ ((GFA3AdderOutput (am,bm,cm)),cin,dm)); coherence (BitGFA3Circ (am,bm,cm)) +* (BitGFA3Circ ((GFA3AdderOutput (am,bm,cm)),cin,dm)) is strict gate`2=den Boolean Circuit of BitFTA3Str (am,bm,cm,dm,cin) ; end; :: deftheorem defines BitFTA3Circ FTACELL1:def_20_:_ for am, bm, cm, dm, cin being set holds BitFTA3Circ (am,bm,cm,dm,cin) = (BitGFA3Circ (am,bm,cm)) +* (BitGFA3Circ ((GFA3AdderOutput (am,bm,cm)),cin,dm)); ::----------------------------------------------- :: 4-2. Properties of 1-bit FTA Structure and Circuit (TYPE-3) ::----------------------------------------------- :: InnerVertices and InputVertices of 1-bit FTA Circuit Structure (FTA3) theorem Th31: :: FTACELL1:31 for am, bm, cm, dm, cin being set holds InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) = (({[<*am,bm*>,xor2],(GFA3AdderOutput (am,bm,cm))} \/ {[<*am,bm*>,and2b],[<*bm,cm*>,and2b],[<*cm,am*>,and2b],(GFA3CarryOutput (am,bm,cm))}) \/ {[<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2],(GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))}) \/ {[<*(GFA3AdderOutput (am,bm,cm)),cin*>,and2b],[<*cin,dm*>,and2b],[<*dm,(GFA3AdderOutput (am,bm,cm))*>,and2b],(GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))} proofend; theorem :: FTACELL1:32 for am, bm, cm, dm, cin being set holds InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) is Relation proofend; Lm31: for x, y, z, p being set holds GFA3AdderOutput (x,y,z) <> [p,and2b] proofend; Lm32: for am, bm, cm being non pair set for x, y, z being set holds InputVertices (BitGFA3Str (am,bm,cm)) misses InnerVertices (BitGFA3Str (x,y,z)) proofend; theorem Th33: :: FTACELL1:33 for am, bm, cm, dm being non pair set for cin being set st cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,and2b] & not cin in InnerVertices (BitGFA3Str (am,bm,cm)) holds InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) = {am,bm,cm,dm,cin} proofend; :: The Element of Carriers, InnerVertices and InputVertices (FTA3) theorem Th34: :: FTACELL1:34 for am, bm, cm, dm, cin being set holds ( am in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & bm in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & cm in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & dm in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & cin in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*am,bm*>,xor2] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3AdderOutput (am,bm,cm) in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*am,bm*>,and2b] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*bm,cm*>,and2b] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*cm,am*>,and2b] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3CarryOutput (am,bm,cm) in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm) in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*(GFA3AdderOutput (am,bm,cm)),cin*>,and2b] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*cin,dm*>,and2b] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*dm,(GFA3AdderOutput (am,bm,cm))*>,and2b] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm) in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) ) proofend; theorem Th35: :: FTACELL1:35 for am, bm, cm, dm, cin being set holds ( [<*am,bm*>,xor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3AdderOutput (am,bm,cm) in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*am,bm*>,and2b] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*bm,cm*>,and2b] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*cm,am*>,and2b] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3CarryOutput (am,bm,cm) in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm) in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*(GFA3AdderOutput (am,bm,cm)),cin*>,and2b] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*cin,dm*>,and2b] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*dm,(GFA3AdderOutput (am,bm,cm))*>,and2b] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm) in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) ) proofend; theorem Th36: :: FTACELL1:36 for am, bm, cm, dm being non pair set for cin being set st cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,and2b] & not cin in InnerVertices (BitGFA3Str (am,bm,cm)) holds ( am in InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) & bm in InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) & cm in InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) & dm in InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) & cin in InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) ) proofend; ::------------------------------------------- :: 4-3. Output Definitions of the Combined Circuit ::------------------------------------------- :: Def. External/Internal Signal Outputs of 1-bit FTA TYPE-3 definition let am, bm, cm, dm, cin be set ; func BitFTA3CarryOutput (am,bm,cm,dm,cin) -> Element of InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) equals :: FTACELL1:def 21 GFA3CarryOutput (am,bm,cm); coherence GFA3CarryOutput (am,bm,cm) is Element of InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) by Th35; func BitFTA3AdderOutputI (am,bm,cm,dm,cin) -> Element of InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) equals :: FTACELL1:def 22 GFA3AdderOutput (am,bm,cm); coherence GFA3AdderOutput (am,bm,cm) is Element of InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) by Th35; func BitFTA3AdderOutputP (am,bm,cm,dm,cin) -> Element of InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) equals :: FTACELL1:def 23 GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm); coherence GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm) is Element of InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) by Th35; func BitFTA3AdderOutputQ (am,bm,cm,dm,cin) -> Element of InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) equals :: FTACELL1:def 24 GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm); coherence GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm) is Element of InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) by Th35; end; :: deftheorem defines BitFTA3CarryOutput FTACELL1:def_21_:_ for am, bm, cm, dm, cin being set holds BitFTA3CarryOutput (am,bm,cm,dm,cin) = GFA3CarryOutput (am,bm,cm); :: deftheorem defines BitFTA3AdderOutputI FTACELL1:def_22_:_ for am, bm, cm, dm, cin being set holds BitFTA3AdderOutputI (am,bm,cm,dm,cin) = GFA3AdderOutput (am,bm,cm); :: deftheorem defines BitFTA3AdderOutputP FTACELL1:def_23_:_ for am, bm, cm, dm, cin being set holds BitFTA3AdderOutputP (am,bm,cm,dm,cin) = GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm); :: deftheorem defines BitFTA3AdderOutputQ FTACELL1:def_24_:_ for am, bm, cm, dm, cin being set holds BitFTA3AdderOutputQ (am,bm,cm,dm,cin) = GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm); ::----------------------------------- :: 4-4. Stability of the Combined Circuit and its Outputs ::----------------------------------- :: Intermediate (External/Internal) Carry/Adder Outputs after Two-steps theorem :: FTACELL1:37 for am, bm, cm being non pair set for dm, cin being set for s being State of (BitFTA3Circ (am,bm,cm,dm,cin)) for a1, a2, a3 being Element of BOOLEAN st a1 = s . am & a2 = s . bm & a3 = s . cm holds ( (Following (s,2)) . (BitFTA3CarryOutput (am,bm,cm,dm,cin)) = 'not' (((('not' a1) '&' ('not' a2)) 'or' (('not' a2) '&' ('not' a3))) 'or' (('not' a3) '&' ('not' a1))) & (Following (s,2)) . (BitFTA3AdderOutputI (am,bm,cm,dm,cin)) = 'not' ((('not' a1) 'xor' ('not' a2)) 'xor' ('not' a3)) ) proofend; :: Temporal (Internal) Calculations after Two-steps theorem Th38: :: FTACELL1:38 for am, bm, cm, dm being non pair set for cin being set st cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,and2b] & not cin in InnerVertices (BitGFA3Str (am,bm,cm)) holds for s being State of (BitFTA3Circ (am,bm,cm,dm,cin)) for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . am & a2 = s . bm & a3 = s . cm & a4 = s . dm & a5 = s . cin holds ( (Following (s,2)) . (GFA3AdderOutput (am,bm,cm)) = 'not' ((('not' a1) 'xor' ('not' a2)) 'xor' ('not' a3)) & (Following (s,2)) . am = a1 & (Following (s,2)) . bm = a2 & (Following (s,2)) . cm = a3 & (Following (s,2)) . dm = a4 & (Following (s,2)) . cin = a5 ) proofend; Lm33: for am, bm, cm, dm being non pair set for cin being set for s being State of (BitFTA3Circ (am,bm,cm,dm,cin)) for a123, a4, a5 being Element of BOOLEAN st a123 = s . (GFA3AdderOutput (am,bm,cm)) & a4 = s . dm & a5 = s . cin holds ( (Following s) . [<*(GFA3AdderOutput (am,bm,cm)),cin*>,and2b] = ('not' a123) '&' ('not' a5) & (Following s) . [<*cin,dm*>,and2b] = ('not' a5) '&' ('not' a4) & (Following s) . [<*dm,(GFA3AdderOutput (am,bm,cm))*>,and2b] = ('not' a4) '&' ('not' a123) ) proofend; Lm34: for am, bm, cm, dm being non pair set for cin being set for s being State of (BitFTA3Circ (am,bm,cm,dm,cin)) for a123, a5 being Element of BOOLEAN st a123 = s . (GFA3AdderOutput (am,bm,cm)) & a5 = s . cin holds (Following s) . [<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2] = a123 'xor' a5 proofend; Lm35: for am, bm, cm, dm being non pair set for cin being set st cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,and2b] & not cin in InnerVertices (BitGFA3Str (am,bm,cm)) holds for s being State of (BitFTA3Circ (am,bm,cm,dm,cin)) for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . am & a2 = s . bm & a3 = s . cm & a4 = s . dm & a5 = s . cin holds ( (Following (s,3)) . [<*(GFA3AdderOutput (am,bm,cm)),cin*>,and2b] = ((('not' a1) 'xor' ('not' a2)) 'xor' ('not' a3)) '&' ('not' a5) & (Following (s,3)) . [<*cin,dm*>,and2b] = ('not' a5) '&' ('not' a4) & (Following (s,3)) . [<*dm,(GFA3AdderOutput (am,bm,cm))*>,and2b] = ('not' a4) '&' ((('not' a1) 'xor' ('not' a2)) 'xor' ('not' a3)) & (Following (s,3)) . am = a1 & (Following (s,3)) . bm = a2 & (Following (s,3)) . cm = a3 & (Following (s,3)) . dm = a4 & (Following (s,3)) . cin = a5 ) proofend; Lm36: for am, bm, cm, dm being non pair set for cin being set st cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,and2b] & not cin in InnerVertices (BitGFA3Str (am,bm,cm)) holds for s being State of (BitFTA3Circ (am,bm,cm,dm,cin)) for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . am & a2 = s . bm & a3 = s . cm & a4 = s . dm & a5 = s . cin holds ( (Following (s,3)) . [<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2] = ('not' ((('not' a1) 'xor' ('not' a2)) 'xor' ('not' a3))) 'xor' a5 & (Following (s,3)) . am = a1 & (Following (s,3)) . bm = a2 & (Following (s,3)) . cm = a3 & (Following (s,3)) . dm = a4 & (Following (s,3)) . cin = a5 ) proofend; Lm37: for am, bm, cm, dm being non pair set for cin being set for s being State of (BitFTA3Circ (am,bm,cm,dm,cin)) for a123x, a123y, a123z being Element of BOOLEAN st a123x = s . [<*(GFA3AdderOutput (am,bm,cm)),cin*>,and2b] & a123y = s . [<*cin,dm*>,and2b] & a123z = s . [<*dm,(GFA3AdderOutput (am,bm,cm))*>,and2b] holds (Following s) . (GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm)) = 'not' ((a123x 'or' a123y) 'or' a123z) proofend; Lm38: for am, bm, cm, dm being non pair set for cin being set for s being State of (BitFTA3Circ (am,bm,cm,dm,cin)) for a1235, a4 being Element of BOOLEAN st a1235 = s . [<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2] & a4 = s . dm holds (Following s) . (GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm)) = a1235 'xor' a4 proofend; Lm39: for am, bm, cm, dm being non pair set for cin being set st cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,and2b] & not cin in InnerVertices (BitGFA3Str (am,bm,cm)) holds for s being State of (BitFTA3Circ (am,bm,cm,dm,cin)) for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . am & a2 = s . bm & a3 = s . cm & a4 = s . dm & a5 = s . cin holds ( (Following (s,4)) . (GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm)) = 'not' (((((('not' a1) 'xor' ('not' a2)) 'xor' ('not' a3)) '&' ('not' a5)) 'or' (('not' a5) '&' ('not' a4))) 'or' (('not' a4) '&' ((('not' a1) 'xor' ('not' a2)) 'xor' ('not' a3)))) & (Following (s,4)) . am = a1 & (Following (s,4)) . bm = a2 & (Following (s,4)) . cm = a3 & (Following (s,4)) . dm = a4 & (Following (s,4)) . cin = a5 ) proofend; Lm40: for am, bm, cm, dm being non pair set for cin being set st cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,and2b] & not cin in InnerVertices (BitGFA3Str (am,bm,cm)) holds for s being State of (BitFTA3Circ (am,bm,cm,dm,cin)) for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . am & a2 = s . bm & a3 = s . cm & a4 = s . dm & a5 = s . cin holds ( (Following (s,4)) . (GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm)) = 'not' ((((('not' a1) 'xor' ('not' a2)) 'xor' ('not' a3)) 'xor' ('not' a4)) 'xor' ('not' a5)) & (Following (s,4)) . am = a1 & (Following (s,4)) . bm = a2 & (Following (s,4)) . cm = a3 & (Following (s,4)) . dm = a4 & (Following (s,4)) . cin = a5 ) proofend; :: Main Proposition #4-1 (External Circuit Outputs after Four-steps) FTA3 theorem :: FTACELL1:39 for am, bm, cm, dm being non pair set for cin being set st cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,and2b] & not cin in InnerVertices (BitGFA3Str (am,bm,cm)) holds for s being State of (BitFTA3Circ (am,bm,cm,dm,cin)) for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . am & a2 = s . bm & a3 = s . cm & a4 = s . dm & a5 = s . cin holds ( (Following (s,4)) . (BitFTA3AdderOutputP (am,bm,cm,dm,cin)) = 'not' (((((('not' a1) 'xor' ('not' a2)) 'xor' ('not' a3)) '&' ('not' a5)) 'or' (('not' a5) '&' ('not' a4))) 'or' (('not' a4) '&' ((('not' a1) 'xor' ('not' a2)) 'xor' ('not' a3)))) & (Following (s,4)) . (BitFTA3AdderOutputQ (am,bm,cm,dm,cin)) = 'not' ((((('not' a1) 'xor' ('not' a2)) 'xor' ('not' a3)) 'xor' ('not' a4)) 'xor' ('not' a5)) ) by Lm39, Lm40; :: Main Proposition #4-2 (The Whole Circuit Stability after Four-steps) FTA3 theorem :: FTACELL1:40 for am, bm, cm, dm being non pair set for cin being set st cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,and2b] holds for s being State of (BitFTA3Circ (am,bm,cm,dm,cin)) holds Following (s,4) is stable proofend;