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

begin

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

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;

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

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

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;

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;

begin

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 Th11: :: FTACELL1:11

for ap, bm, cp, dm, cin being set holds InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) = (({[<*ap,bm*>,xor2c],(GFA1AdderOutput (ap,bm,cp))} \/ {[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))}) \/ {[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c],(GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))}) \/ {[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a],[<*cin,dm*>,and2c],[<*dm,(GFA1AdderOutput (ap,bm,cp))*>,and2b],(GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))}

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))*>,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 Th14: :: FTACELL1:14

for ap, bm, cp, dm, cin being set holds
( ap in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & bm in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & cp in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & dm in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & cin in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*ap,bm*>,xor2c] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA1AdderOutput (ap,bm,cp) in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*ap,bm*>,and2c] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*bm,cp*>,and2a] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*cp,ap*>,and2] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA1CarryOutput (ap,bm,cp) in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm) in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*cin,dm*>,and2c] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,and2b] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm) in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) )

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))*>,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 Th16: :: FTACELL1:16

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

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

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 Th18: :: FTACELL1:18

for ap, bm, cp, dm being non pair set
for cin being set st cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,and2b] & not cin in InnerVertices (BitGFA1Str (ap,bm,cp)) holds
for s being State of (BitFTA1Circ (ap,bm,cp,dm,cin))
for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . ap & a2 = s . bm & a3 = s . cp & a4 = s . dm & a5 = s . cin holds
( (Following (s,2)) . (GFA1AdderOutput (ap,bm,cp)) = 'not' ((a1 'xor' ('not' a2)) 'xor' a3) & (Following (s,2)) . ap = a1 & (Following (s,2)) . bm = a2 & (Following (s,2)) . cp = a3 & (Following (s,2)) . dm = a4 & (Following (s,2)) . cin = a5 )

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))*>,and2b] = ('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))*>,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;

Lm16: for ap, bm, cp, dm being non pair set
for cin being set st cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,and2b] & not cin in InnerVertices (BitGFA1Str (ap,bm,cp)) holds
for s being State of (BitFTA1Circ (ap,bm,cp,dm,cin))
for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . ap & a2 = s . bm & a3 = s . cp & a4 = s . dm & a5 = s . cin holds
( (Following (s,3)) . [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c] = ('not' ((a1 'xor' ('not' a2)) 'xor' a3)) 'xor' ('not' a5) & (Following (s,3)) . ap = a1 & (Following (s,3)) . bm = a2 & (Following (s,3)) . cp = a3 & (Following (s,3)) . dm = a4 & (Following (s,3)) . cin = a5 )

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

Lm20: for ap, bm, cp, dm being non pair set
for cin being set st cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,and2b] & not cin in InnerVertices (BitGFA1Str (ap,bm,cp)) holds
for s being State of (BitFTA1Circ (ap,bm,cp,dm,cin))
for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . ap & a2 = s . bm & a3 = s . cp & a4 = s . dm & a5 = s . cin holds
( (Following (s,4)) . (GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm)) = (((a1 'xor' ('not' a2)) 'xor' a3) 'xor' ('not' a4)) 'xor' a5 & (Following (s,4)) . ap = a1 & (Following (s,4)) . bm = a2 & (Following (s,4)) . cp = a3 & (Following (s,4)) . dm = a4 & (Following (s,4)) . cin = a5 )

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 Lm19, Lm20;

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;

begin

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 Th21: :: FTACELL1:21

for am, bp, cm, dp, cin being set holds InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) = (({[<*am,bp*>,xor2c],(GFA2AdderOutput (am,bp,cm))} \/ {[<*am,bp*>,and2a],[<*bp,cm*>,and2c],[<*cm,am*>,and2b],(GFA2CarryOutput (am,bp,cm))}) \/ {[<*(GFA2AdderOutput (am,bp,cm)),cin*>,xor2c],(GFA1AdderOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp))}) \/ {[<*(GFA2AdderOutput (am,bp,cm)),cin*>,and2c],[<*cin,dp*>,and2a],[<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2],(GFA1CarryOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp))}

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;

theorem Th24: :: FTACELL1:24

for am, bp, cm, dp, cin being set holds
( am in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & bp in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & cm in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & dp in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & cin in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*am,bp*>,xor2c] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & GFA2AdderOutput (am,bp,cm) in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*am,bp*>,and2a] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*bp,cm*>,and2c] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*cm,am*>,and2b] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & GFA2CarryOutput (am,bp,cm) in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*(GFA2AdderOutput (am,bp,cm)),cin*>,xor2c] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & GFA1AdderOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp) in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*(GFA2AdderOutput (am,bp,cm)),cin*>,and2c] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*cin,dp*>,and2a] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & GFA1CarryOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp) in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) )

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*>,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 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;

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

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

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;

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;

begin

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 Th31: :: FTACELL1:31

for am, bm, cm, dm, cin being set holds InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) = (({[<*am,bm*>,xor2],(GFA3AdderOutput (am,bm,cm))} \/ {[<*am,bm*>,and2b],[<*bm,cm*>,and2b],[<*cm,am*>,and2b],(GFA3CarryOutput (am,bm,cm))}) \/ {[<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2],(GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))}) \/ {[<*(GFA3AdderOutput (am,bm,cm)),cin*>,and2b],[<*cin,dm*>,and2b],[<*dm,(GFA3AdderOutput (am,bm,cm))*>,and2b],(GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))}

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,and2b]

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))*>,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 Th34: :: FTACELL1:34

for am, bm, cm, dm, cin being set holds
( am in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & bm in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & cm in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & dm in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & cin in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*am,bm*>,xor2] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3AdderOutput (am,bm,cm) in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*am,bm*>,and2b] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*bm,cm*>,and2b] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*cm,am*>,and2b] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3CarryOutput (am,bm,cm) in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm) in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*(GFA3AdderOutput (am,bm,cm)),cin*>,and2b] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*cin,dm*>,and2b] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*dm,(GFA3AdderOutput (am,bm,cm))*>,and2b] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm) in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) )

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*>,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 Th36: :: FTACELL1:36

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

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

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 Th38: :: FTACELL1:38

for am, bm, cm, dm being non pair set
for cin being set st cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,and2b] & not cin in InnerVertices (BitGFA3Str (am,bm,cm)) holds
for s being State of (BitFTA3Circ (am,bm,cm,dm,cin))
for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . am & a2 = s . bm & a3 = s . cm & a4 = s . dm & a5 = s . cin holds
( (Following (s,2)) . (GFA3AdderOutput (am,bm,cm)) = 'not' ((('not' a1) 'xor' ('not' a2)) 'xor' ('not' a3)) & (Following (s,2)) . am = a1 & (Following (s,2)) . bm = a2 & (Following (s,2)) . cm = a3 & (Following (s,2)) . dm = a4 & (Following (s,2)) . cin = a5 )

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*>,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;

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

Lm36: for am, bm, cm, dm being non pair set
for cin being set st cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,and2b] & not cin in InnerVertices (BitGFA3Str (am,bm,cm)) holds
for s being State of (BitFTA3Circ (am,bm,cm,dm,cin))
for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . am & a2 = s . bm & a3 = s . cm & a4 = s . dm & a5 = s . cin holds
( (Following (s,3)) . [<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2] = ('not' ((('not' a1) 'xor' ('not' a2)) 'xor' ('not' a3))) 'xor' a5 & (Following (s,3)) . am = a1 & (Following (s,3)) . bm = a2 & (Following (s,3)) . cm = a3 & (Following (s,3)) . dm = a4 & (Following (s,3)) . cin = a5 )

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*>,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;

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

Lm40: for am, bm, cm, dm being non pair set
for cin being set st cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,and2b] & not cin in InnerVertices (BitGFA3Str (am,bm,cm)) holds
for s being State of (BitFTA3Circ (am,bm,cm,dm,cin))
for a1, a2, a3, a4, a5 being Element of BOOLEAN st a1 = s . am & a2 = s . bm & a3 = s . cm & a4 = s . dm & a5 = s . cin holds
( (Following (s,4)) . (GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm)) = 'not' ((((('not' a1) 'xor' ('not' a2)) 'xor' ('not' a3)) 'xor' ('not' a4)) 'xor' ('not' a5)) & (Following (s,4)) . am = a1 & (Following (s,4)) . bm = a2 & (Following (s,4)) . cm = a3 & (Following (s,4)) . dm = a4 & (Following (s,4)) . cin = a5 )

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 Lm39, Lm40;

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;