theorem Th10: :: FTACELL2:10

for n being Nat
for ap, bp, cp, dp being nonpair-yielding FinSequence
for s being State of (n -BitFTA0Layer2Circ (ap,bp,cp,dp)) st s . [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] = FALSE holds
Following (s,2) is stable