let n be Nat; :: thesis: for ap, bp, cp being nonpair-yielding FinSequence holds InputVertices (n -BitFTA0Layer1Str (ap,bp,cp)) is without_pairs
let ap, bp, cp be nonpair-yielding FinSequence; :: thesis: InputVertices (n -BitFTA0Layer1Str (ap,bp,cp)) is without_pairs
deffunc H₁( Nat) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign = $1 -BitFTA0Layer1Str (ap,bp,cp);
defpred S₁[ Nat] means InputVertices H₁($1) is without_pairs ;
H₁( 0 ) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) by LmT00L1;
then A1: S₁[ 0 ] by FACIRC_1:39;

A2: now :: thesis: for i being Nat st S₁[i] holds
S₁[i + 1]

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume B1: S₁[i] ; :: thesis: S₁[i + 1]
set B = BitGFA0Str ((ap . (i + 1)),(bp . (i + 1)),(cp . (i + 1)));
B2: H₁(i + 1) = H₁(i) +* (BitGFA0Str ((ap . (i + 1)),(bp . (i + 1)),(cp . (i + 1)))) by LmT05A;
reconsider w1 = InputVertices H₁(i) as without_pairs set by B1;
reconsider w2 = InputVertices (BitGFA0Str ((ap . (i + 1)),(bp . (i + 1)),(cp . (i + 1)))) as without_pairs set by GFACIRC1:35;
InputVertices H₁(i + 1) = (w1 \ (InnerVertices (BitGFA0Str ((ap . (i + 1)),(bp . (i + 1)),(cp . (i + 1)))))) \/ (w2 \ (InnerVertices H₁(i))) by B2, CIRCCOMB:47, CIRCCMB2:5;
hence S₁[i + 1] ; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A1, A2);
hence InputVertices (n -BitFTA0Layer1Str (ap,bp,cp)) is without_pairs ; :: thesis: verum