:: Stability of the 4-2 Binary Addition Circuit Cells. Part {I}
:: by Katsumi Wasaki
::
:: Received August 28, 2008
:: Copyright (c) 2008-2021 Association of Mizar Users

::========================================================================
:: [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))}

proof end;

theorem :: FTACELL1:2

for ap, bp, cp, dp, cin being set holds InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) is Relation

proof end;

Lm1: for x, y, z, p being set holds GFA0AdderOutput (x,y,z) <> [p,and2]

proof end;

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

proof end;

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}

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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 )

proof end;

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

proof end;

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 )

proof end;

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 )

proof end;

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

proof end;

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

proof end;

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 )

proof end;

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 )

proof end;

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

proof end;

::========================================================================
:: [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))*>,nor2],(GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))}

proof end;

theorem :: FTACELL1:12

for ap, bm, cp, dm, cin being set holds InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) is Relation

proof end;

Lm11: for x, y, z, p being set holds GFA1AdderOutput (x,y,z) <> [p,and2c]

proof end;

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

proof end;

theorem Th13: :: FTACELL1:13

for ap, bm, cp, dm being non pair set
for cin being set st cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2] & not cin in InnerVertices (BitGFA1Str (ap,bm,cp)) holds
InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) = {ap,bm,cp,dm,cin}

proof end;

:: 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))*>,nor2] 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)) )

proof end;

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))*>,nor2] in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm) in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) )

proof end;

theorem Th16: :: FTACELL1:16

for ap, bm, cp, dm being non pair set
for cin being set st cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2] & 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)) )

proof end;

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

proof end;

:: 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))*>,nor2] & 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 )

proof end;

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))*>,nor2] = ('not' a4) '&' ('not' a123) )

proof end;

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)

proof end;

Lm15: for ap, bm, cp, dm being non pair set
for cin being set st cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2] & 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))*>,nor2] = ('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 )

proof end;

Lm16: for ap, bm, cp, dm being non pair set
for cin being set st cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2] & 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 )

proof end;

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))*>,nor2] holds
(Following s) . (GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm)) = 'not' ((a123x 'or' a123y) 'or' a123z)

proof end;

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)

proof end;

Lm19: for ap, bm, cp, dm being non pair set
for cin being set st cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2] & 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 )

proof end;

Lm20: for ap, bm, cp, dm being non pair set
for cin being set st cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2] & 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 )

proof end;

:: 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))*>,nor2] & 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))*>,nor2] holds
for s being State of (BitFTA1Circ (ap,bm,cp,dm,cin)) holds Following (s,4) is stable

proof end;

::========================================================================
:: [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*>,nor2],(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))}

proof end;

theorem :: FTACELL1:22

for am, bp, cm, dp, cin being set holds InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) is Relation

proof end;

Lm21: for x, y, z, p being set holds GFA2AdderOutput (x,y,z) <> [p,and2a]

proof end;

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

proof end;

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}

proof end;

:: 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*>,nor2] 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)) )

proof end;

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*>,nor2] 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)) )

proof end;

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

proof end;

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

proof end;

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

proof end;

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 )

proof end;

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)

proof end;

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 )

proof end;

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 )

proof end;

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

proof end;

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)

proof end;

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 )

proof end;

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 )

proof end;

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

proof end;

::========================================================================
:: [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*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))}) \/ {[<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2],(GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))}) \/ {[<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2],[<*cin,dm*>,nor2],[<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2],(GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))}

proof end;

theorem :: FTACELL1:32

for am, bm, cm, dm, cin being set holds InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) is Relation

proof end;

Lm31: for x, y, z, p being set holds GFA3AdderOutput (x,y,z) <> [p,nor2]

proof end;

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

proof end;

theorem Th33: :: FTACELL1:33

for am, bm, cm, dm being non pair set
for cin being set st cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2] & not cin in InnerVertices (BitGFA3Str (am,bm,cm)) holds
InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) = {am,bm,cm,dm,cin}

proof end;

:: 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*>,nor2] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*bm,cm*>,nor2] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*cm,am*>,nor2] 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*>,nor2] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*cin,dm*>,nor2] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2] 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)) )

proof end;

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*>,nor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*bm,cm*>,nor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*cm,am*>,nor2] 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*>,nor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*cin,dm*>,nor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm) in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) )

proof end;

theorem Th36: :: FTACELL1:36

for am, bm, cm, dm being non pair set
for cin being set st cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2] & 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)) )

proof end;

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

proof end;

:: 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))*>,nor2] & 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 )

proof end;

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*>,nor2] = ('not' a123) '&' ('not' a5) & (Following s) . [<*cin,dm*>,nor2] = ('not' a5) '&' ('not' a4) & (Following s) . [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2] = ('not' a4) '&' ('not' a123) )

proof end;

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

proof end;

Lm35: for am, bm, cm, dm being non pair set
for cin being set st cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2] & 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*>,nor2] = ((('not' a1) 'xor' ('not' a2)) 'xor' ('not' a3)) '&' ('not' a5) & (Following (s,3)) . [<*cin,dm*>,nor2] = ('not' a5) '&' ('not' a4) & (Following (s,3)) . [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2] = ('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 )

proof end;

Lm36: for am, bm, cm, dm being non pair set
for cin being set st cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2] & 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 )

proof end;

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*>,nor2] & a123y = s . [<*cin,dm*>,nor2] & a123z = s . [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2] holds
(Following s) . (GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm)) = 'not' ((a123x 'or' a123y) 'or' a123z)

proof end;

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

proof end;

Lm39: for am, bm, cm, dm being non pair set
for cin being set st cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2] & 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 )

proof end;

Lm40: for am, bm, cm, dm being non pair set
for cin being set st cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2] & 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 )

proof end;

:: 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))*>,nor2] & 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))*>,nor2] holds
for s being State of (BitFTA3Circ (am,bm,cm,dm,cin)) holds Following (s,4) is stable

proof end;