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;