theorem Th2: :: FTACELL2:2

for ap, bp, cp, dp being FinSequence holds
( 0 -BitFTA0Str (ap,bp,cp,dp) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & 0 -BitFTA0Circ (ap,bp,cp,dp) = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & 0 -BitFTA0CarryOutput (ap,bp,cp,dp) = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] )