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