let n be Nat; :: thesis: for ap, bm, cp, dm being nonpair-yielding FinSequence
for u, v, x being non pair set holds
( not GFA1AdderOutput (u,v,x) in InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm)) & not GFA1CarryOutput (u,v,x) in InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm)) )
let ap, bm, cp, dm be nonpair-yielding FinSequence; :: thesis: for u, v, x being non pair set holds
( not GFA1AdderOutput (u,v,x) in InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm)) & not GFA1CarryOutput (u,v,x) in InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm)) )
let u, v, x be non pair set ; :: thesis: ( not GFA1AdderOutput (u,v,x) in InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm)) & not GFA1CarryOutput (u,v,x) in InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm)) )
set c0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)];
set wA = GFA1AdderOutput (u,v,x);
set wC = GFA1CarryOutput (u,v,x);
A1: GFA1AdderOutput (u,v,x) <> [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] by XTUPLE_0:1;
A2: GFA1CarryOutput (u,v,x) <> [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] by XTUPLE_0:1;
defpred S₁[ Nat] means ( not GFA1AdderOutput (u,v,x) in InnerVertices ($1 -BitFTA1Layer2Str (ap,bm,cp,dm)) & not GFA1CarryOutput (u,v,x) in InnerVertices ($1 -BitFTA1Layer2Str (ap,bm,cp,dm)) );
0 -BitFTA1Layer2Str (ap,bm,cp,dm) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) by LmT10L2;
then InnerVertices (0 -BitFTA1Layer2Str (ap,bm,cp,dm)) = {[<*>,((0 -tuples_on BOOLEAN) --> FALSE)]} by CIRCCOMB:42;
then A3: S₁[ 0 ] by A1, A2, TARSKI:def 1;
A4: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume B1: S₁[i] ; :: thesis: S₁[i + 1]
set B = BitGFA2Str ((GFA1AdderOutput ((ap . (i + 1)),(bm . (i + 1)),(cp . (i + 1)))),(i -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (i + 1)));
B2: i -BitFTA1CarryOutput (ap,bm,cp,dm) is pair by LmT1COp;
B3: ( not GFA1AdderOutput (u,v,x) in InnerVertices (BitGFA2Str ((GFA1AdderOutput ((ap . (i + 1)),(bm . (i + 1)),(cp . (i + 1)))),(i -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (i + 1)))) & not GFA1CarryOutput (u,v,x) in InnerVertices (BitGFA2Str ((GFA1AdderOutput ((ap . (i + 1)),(bm . (i + 1)),(cp . (i + 1)))),(i -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (i + 1)))) ) by B2, LmT1W1, LmT1W2;
B4: InnerVertices ((i + 1) -BitFTA1Layer2Str (ap,bm,cp,dm)) = (InnerVertices (i -BitFTA1Layer2Str (ap,bm,cp,dm))) \/ (InnerVertices (BitGFA2Str ((GFA1AdderOutput ((ap . (i + 1)),(bm . (i + 1)),(cp . (i + 1)))),(i -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (i + 1))))) by LmT1L2inner;
thus not GFA1AdderOutput (u,v,x) in InnerVertices ((i + 1) -BitFTA1Layer2Str (ap,bm,cp,dm)) by B4, B1, B3, XBOOLE_0:def 3; :: thesis: not GFA1CarryOutput (u,v,x) in InnerVertices ((i + 1) -BitFTA1Layer2Str (ap,bm,cp,dm))
thus not GFA1CarryOutput (u,v,x) in InnerVertices ((i + 1) -BitFTA1Layer2Str (ap,bm,cp,dm)) by B4, B1, B3, XBOOLE_0:def 3; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A3, A4);
hence ( not GFA1AdderOutput (u,v,x) in InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm)) & not GFA1CarryOutput (u,v,x) in InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm)) ) ; :: thesis: verum