let ap, bp, cp be FinSequence; :: thesis: 0 -BitFTA0Layer1Str (ap,bp,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 -BitFTA0Layer1Str (ap,bp,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 +* (BitGFA0Str ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) by Def4;
thus 0 -BitFTA0Layer1Str (ap,bp,cp) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) by A1, A2; :: thesis: verum