let k be Nat; :: thesis: for ap, bm, cp, dm being nonpair-yielding FinSequence holds InputVertices (k -BitFTA1Layer2Str (ap,bm,cp,dm)) misses InnerVertices (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))))
let ap, bm, cp, dm be nonpair-yielding FinSequence; :: thesis: InputVertices (k -BitFTA1Layer2Str (ap,bm,cp,dm)) misses InnerVertices (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))))
set X = GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)));
set Y = k -BitFTA1CarryOutput (ap,bm,cp,dm);
set d = dm . (k + 1);
set B = BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)));
set bA = GFA2AdderOutput ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)));
set bC = GFA2CarryOutput ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)));
A1: k -BitFTA1CarryOutput (ap,bm,cp,dm) is pair by LmT1COp;
assume InputVertices (k -BitFTA1Layer2Str (ap,bm,cp,dm)) meets InnerVertices (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)))) ; :: thesis: contradiction
then consider w being object such that
A2: w in InputVertices (k -BitFTA1Layer2Str (ap,bm,cp,dm)) and
A3: w in InnerVertices (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)))) by XBOOLE_0:3;
reconsider w = w as set by TARSKI:1;

per cases ( not w is pair or ex u, v, x being non pair set st w = GFA1AdderOutput (u,v,x) or ex u, v, x being non pair set st w = GFA1CarryOutput (u,v,x) ) by A2, LmT1InAcc;

suppose A4: not w is pair ; :: thesis: contradiction

w in (({[<*(GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm))*>,xor2c]} \/ {(GFA2AdderOutput ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))))}) \/ {[<*(GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm))*>,and2a],[<*(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))*>,and2c],[<*(dm . (k + 1)),(GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))))*>,nor2]}) \/ {(GFA2CarryOutput ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))))} by A3, GFACIRC1:95;
then ( w in ({[<*(GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm))*>,xor2c]} \/ {(GFA2AdderOutput ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))))}) \/ {[<*(GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm))*>,and2a],[<*(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))*>,and2c],[<*(dm . (k + 1)),(GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))))*>,nor2]} or w in {(GFA2CarryOutput ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))))} ) by XBOOLE_0:def 3;
then ( w in {[<*(GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm))*>,xor2c]} \/ {(GFA2AdderOutput ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))))} or w in {[<*(GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm))*>,and2a],[<*(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))*>,and2c],[<*(dm . (k + 1)),(GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))))*>,nor2]} or w in {(GFA2CarryOutput ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))))} ) by XBOOLE_0:def 3;
then B1: ( w in {[<*(GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm))*>,xor2c]} or w in {(GFA2AdderOutput ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))))} or w in {[<*(GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm))*>,and2a],[<*(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))*>,and2c],[<*(dm . (k + 1)),(GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))))*>,nor2]} or w in {(GFA2CarryOutput ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))))} ) by XBOOLE_0:def 3;

per cases ( w = [<*(GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm))*>,xor2c] or w = GFA2AdderOutput ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))) or w = [<*(GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm))*>,and2a] or w = [<*(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))*>,and2c] or w = [<*(dm . (k + 1)),(GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))))*>,nor2] or w = GFA2CarryOutput ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))) ) by B1, TARSKI:def 1, ENUMSET1:def 1;

suppose w = [<*(GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm))*>,xor2c] ; :: thesis: contradiction

hence contradiction by A4; :: thesis: verum

end;

suppose w = GFA2AdderOutput ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))) ; :: thesis: contradiction

hence contradiction by A4; :: thesis: verum

end;

suppose w = [<*(GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm))*>,and2a] ; :: thesis: contradiction

hence contradiction by A4; :: thesis: verum

end;

suppose w = [<*(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))*>,and2c] ; :: thesis: contradiction

hence contradiction by A4; :: thesis: verum

end;

suppose w = [<*(dm . (k + 1)),(GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))))*>,nor2] ; :: thesis: contradiction

hence contradiction by A4; :: thesis: verum

end;

suppose w = GFA2CarryOutput ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))) ; :: thesis: contradiction

hence contradiction by A4; :: thesis: verum

end;

end;

end;

suppose ex u, v, x being non pair set st w = GFA1AdderOutput (u,v,x) ; :: thesis: contradiction

hence contradiction by A3, A1, LmT1W1; :: thesis: verum

end;

suppose ex u, v, x being non pair set st w = GFA1CarryOutput (u,v,x) ; :: thesis: contradiction

hence contradiction by A3, A1, LmT1W2; :: thesis: verum

end;

end;