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

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

theorem ThFTA0S1: :: 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;

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

proof end;

LemmaX12: 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 ThFTA0S4: :: 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;

theorem ThFTA0S6: :: 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 ThFTA0S7: :: 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 ThFTA0S8: :: 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;

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 ThFTA0S7;
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 ThFTA0S7;
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 ThFTA0S7;
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 ThFTA0S7;

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;

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;

theorem ThFTA0S11: :: 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;

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

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

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

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

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

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

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

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

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 LmFTA0S15p, LmFTA0S15q;

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;

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

theorem ThFTA1S1: :: 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)}

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;

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

proof end;

LemmaX22: 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 ThFTA1S4: :: 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}

proof end;

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

proof end;

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

proof end;

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

proof end;

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 ThFTA1S7;
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 ThFTA1S7;
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 ThFTA1S7;
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 ThFTA1S7;

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;

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;

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

proof end;

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

proof end;

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

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

proof end;

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

proof end;

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

proof end;

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

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

proof end;

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

proof end;

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 LmFTA1S15p, LmFTA1S15q;

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

proof end;

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

theorem ThFTA2S1: :: 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)}

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;

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

proof end;

LemmaX32: 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 ThFTA2S4: :: 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;

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

proof end;

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

proof end;

theorem ThFTA2S8: :: 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;

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 ThFTA2S7;
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 ThFTA2S7;
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 ThFTA2S7;
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 ThFTA2S7;

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;

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;

theorem ThFTA2S11: :: 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;

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

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

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

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

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

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

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

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

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 LmFTA2S15p, LmFTA2S15q;

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;

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

theorem ThFTA3S1: :: 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)}

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;

LemmaX41: for x, y, z, p being set holds GFA3AdderOutput x,y,z <> [p,and2b ]

proof end;

LemmaX42: 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 ThFTA3S4: :: 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}

proof end;

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

proof end;

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

proof end;

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

proof end;

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 ThFTA3S7;
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 ThFTA3S7;
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 ThFTA3S7;
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 ThFTA3S7;

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;

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;

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

proof end;

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

proof end;

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

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

proof end;

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

proof end;

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

proof end;

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

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

proof end;

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

proof end;

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 LmFTA3S15p, LmFTA3S15q;

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

proof end;