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;