let ap, bm, cp be FinSequence; :: thesis: 0 -BitFTA1Layer1Str (ap,bm,cp) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))
set S0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE));
consider f being ManySortedSet of NAT such that
A1: 0 -BitFTA1Layer1Str (ap,bm,cp) = f . 0 and
A2: f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and
for k being Nat
for S being non empty ManySortedSign st S = f . k holds
f . (k + 1) = S +* (BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) by Def11;
thus 0 -BitFTA1Layer1Str (ap,bm,cp) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) by A1, A2; :: thesis: verum