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 )