theorem Th13: :: FTACELL2:13

for ap, bm, cp, dm being FinSequence holds
( 0 -BitFTA1Str (ap,bm,cp,dm) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & 0 -BitFTA1Circ (ap,bm,cp,dm) = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & 0 -BitFTA1CarryOutput (ap,bm,cp,dm) = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] )