let n be Nat; :: thesis: for ap, bp, cp, dp being nonpair-yielding FinSequence
for u, v, x being non pair set holds
( not GFA0AdderOutput (u,v,x) in InnerVertices (n -BitFTA0Layer2Str (ap,bp,cp,dp)) & not GFA0CarryOutput (u,v,x) in InnerVertices (n -BitFTA0Layer2Str (ap,bp,cp,dp)) )
let ap, bp, cp, dp be nonpair-yielding FinSequence; :: thesis: for u, v, x being non pair set holds
( not GFA0AdderOutput (u,v,x) in InnerVertices (n -BitFTA0Layer2Str (ap,bp,cp,dp)) & not GFA0CarryOutput (u,v,x) in InnerVertices (n -BitFTA0Layer2Str (ap,bp,cp,dp)) )
let u, v, x be non pair set ; :: thesis: ( not GFA0AdderOutput (u,v,x) in InnerVertices (n -BitFTA0Layer2Str (ap,bp,cp,dp)) & not GFA0CarryOutput (u,v,x) in InnerVertices (n -BitFTA0Layer2Str (ap,bp,cp,dp)) )
set c0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)];
set wA = GFA0AdderOutput (u,v,x);
set wC = GFA0CarryOutput (u,v,x);
A1: GFA0AdderOutput (u,v,x) <> [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] by XTUPLE_0:1;
A2: GFA0CarryOutput (u,v,x) <> [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] by XTUPLE_0:1;
defpred S₁[ Nat] means ( not GFA0AdderOutput (u,v,x) in InnerVertices ($1 -BitFTA0Layer2Str (ap,bp,cp,dp)) & not GFA0CarryOutput (u,v,x) in InnerVertices ($1 -BitFTA0Layer2Str (ap,bp,cp,dp)) );
0 -BitFTA0Layer2Str (ap,bp,cp,dp) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) by LmT00L2;
then InnerVertices (0 -BitFTA0Layer2Str (ap,bp,cp,dp)) = {[<*>,((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 = BitGFA0Str ((GFA0AdderOutput ((ap . (i + 1)),(bp . (i + 1)),(cp . (i + 1)))),(i -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (i + 1)));
B2: i -BitFTA0CarryOutput (ap,bp,cp,dp) is pair by LmT0COp;
B3: ( not GFA0AdderOutput (u,v,x) in InnerVertices (BitGFA0Str ((GFA0AdderOutput ((ap . (i + 1)),(bp . (i + 1)),(cp . (i + 1)))),(i -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (i + 1)))) & not GFA0CarryOutput (u,v,x) in InnerVertices (BitGFA0Str ((GFA0AdderOutput ((ap . (i + 1)),(bp . (i + 1)),(cp . (i + 1)))),(i -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (i + 1)))) ) by B2, LmT0W1, LmT0W2;
B4: InnerVertices ((i + 1) -BitFTA0Layer2Str (ap,bp,cp,dp)) = (InnerVertices (i -BitFTA0Layer2Str (ap,bp,cp,dp))) \/ (InnerVertices (BitGFA0Str ((GFA0AdderOutput ((ap . (i + 1)),(bp . (i + 1)),(cp . (i + 1)))),(i -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (i + 1))))) by LmT0L2inner;
thus not GFA0AdderOutput (u,v,x) in InnerVertices ((i + 1) -BitFTA0Layer2Str (ap,bp,cp,dp)) by B4, B1, B3, XBOOLE_0:def 3; :: thesis: not GFA0CarryOutput (u,v,x) in InnerVertices ((i + 1) -BitFTA0Layer2Str (ap,bp,cp,dp))
thus not GFA0CarryOutput (u,v,x) in InnerVertices ((i + 1) -BitFTA0Layer2Str (ap,bp,cp,dp)) 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 GFA0AdderOutput (u,v,x) in InnerVertices (n -BitFTA0Layer2Str (ap,bp,cp,dp)) & not GFA0CarryOutput (u,v,x) in InnerVertices (n -BitFTA0Layer2Str (ap,bp,cp,dp)) ) ; :: thesis: verum