theorem Th20: :: FTACELL2:20

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