let x1, x2, x3, x5, x6, x7 be non pair set ; :: thesis: for x4 being set st x4 <> [<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2] & x4 <> [<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2] & not x4 in InnerVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) holds
InputVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) = {x1,x2,x3,x4,x5,x6,x7}
let x4 be set ; :: thesis: ( x4 <> [<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2] & x4 <> [<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2] & not x4 in InnerVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) implies InputVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) = {x1,x2,x3,x4,x5,x6,x7} )
set S = STC0IStr (x1,x2,x3,x4,x5,x6,x7);
set S1 = STC0IIStr (x1,x2,x3,x5,x6,x7);
set A1 = GFA0AdderOutput (x1,x2,x3);
set C1 = GFA0CarryOutput (x1,x2,x3);
set A2 = GFA0AdderOutput (x5,x6,x7);
set C2 = GFA0CarryOutput (x5,x6,x7);
set x1x20 = [<*x1,x2*>,xor2];
set x1x2 = [<*x1,x2*>,and2];
set x2x3 = [<*x2,x3*>,and2];
set x3x1 = [<*x3,x1*>,and2];
set x5x60 = [<*x5,x6*>,xor2];
set x5x6 = [<*x5,x6*>,and2];
set x6x7 = [<*x6,x7*>,and2];
set x7x5 = [<*x7,x5*>,and2];
set S2 = BitGFA0Str ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4);
set A1A20 = [<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2];
set A1A2 = [<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2];
set A2x4 = [<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2];
set x4A1 = [<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2];
assume that
A0: x4 <> [<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2] and
A1: x4 <> [<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2] and
A2: not x4 in InnerVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) ; :: thesis: InputVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) = {x1,x2,x3,x4,x5,x6,x7}
A5: InnerVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) = (({[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3))} \/ {[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2],(GFA0CarryOutput (x1,x2,x3))}) \/ {[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7))}) \/ {[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2],(GFA0CarryOutput (x5,x6,x7))} by ThSTC0IIS1
.= (({(GFA0AdderOutput (x1,x2,x3)),[<*x1,x2*>,xor2]} \/ {(GFA0AdderOutput (x5,x6,x7)),[<*x5,x6*>,xor2]}) \/ {[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2],(GFA0CarryOutput (x1,x2,x3))}) \/ {[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2],(GFA0CarryOutput (x5,x6,x7))} by XBOOLE_1:4
.= ({(GFA0AdderOutput (x1,x2,x3)),[<*x1,x2*>,xor2],(GFA0AdderOutput (x5,x6,x7)),[<*x5,x6*>,xor2]} \/ {[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2],(GFA0CarryOutput (x1,x2,x3))}) \/ {[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2],(GFA0CarryOutput (x5,x6,x7))} by ENUMSET1:5
.= ({(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),[<*x1,x2*>,xor2],[<*x5,x6*>,xor2]} \/ {[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2],(GFA0CarryOutput (x1,x2,x3))}) \/ {[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2],(GFA0CarryOutput (x5,x6,x7))} by ENUMSET1:62
.= (({(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))} \/ {[<*x1,x2*>,xor2],[<*x5,x6*>,xor2]}) \/ {[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2],(GFA0CarryOutput (x1,x2,x3))}) \/ {[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2],(GFA0CarryOutput (x5,x6,x7))} by ENUMSET1:5
.= ({(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))} \/ ({[<*x1,x2*>,xor2],[<*x5,x6*>,xor2]} \/ {[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2],(GFA0CarryOutput (x1,x2,x3))})) \/ {[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2],(GFA0CarryOutput (x5,x6,x7))} by XBOOLE_1:4
.= ({(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))} \/ (({[<*x1,x2*>,xor2]} \/ {[<*x5,x6*>,xor2]}) \/ {[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2],(GFA0CarryOutput (x1,x2,x3))})) \/ {[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2],(GFA0CarryOutput (x5,x6,x7))} by ENUMSET1:1
.= ({(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))} \/ ({[<*x1,x2*>,xor2]} \/ ({[<*x5,x6*>,xor2]} \/ {[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2],(GFA0CarryOutput (x1,x2,x3))}))) \/ {[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2],(GFA0CarryOutput (x5,x6,x7))} by XBOOLE_1:4
.= ({(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))} \/ ({[<*x1,x2*>,xor2]} \/ {[<*x5,x6*>,xor2],[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2],(GFA0CarryOutput (x1,x2,x3))})) \/ {[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2],(GFA0CarryOutput (x5,x6,x7))} by ENUMSET1:7
.= {(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))} \/ (({[<*x1,x2*>,xor2]} \/ {[<*x5,x6*>,xor2],[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2],(GFA0CarryOutput (x1,x2,x3))}) \/ {[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2],(GFA0CarryOutput (x5,x6,x7))}) by XBOOLE_1:4
.= {(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))} \/ ({[<*x1,x2*>,xor2]} \/ ({[<*x5,x6*>,xor2],[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2],(GFA0CarryOutput (x1,x2,x3))} \/ {[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2],(GFA0CarryOutput (x5,x6,x7))})) by XBOOLE_1:4
.= {(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))} \/ ({[<*x1,x2*>,xor2]} \/ {[<*x5,x6*>,xor2],[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2],(GFA0CarryOutput (x1,x2,x3)),[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2],(GFA0CarryOutput (x5,x6,x7))}) by ENUMSET1:81
.= {(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))} \/ {[<*x5,x6*>,xor2],[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2],(GFA0CarryOutput (x1,x2,x3)),[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2],(GFA0CarryOutput (x5,x6,x7)),[<*x1,x2*>,xor2]} by ENUMSET1:85 ;
A6: {(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4} \ (InnerVertices (STC0IIStr (x1,x2,x3,x5,x6,x7))) = ({(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))} \/ {x4}) \ (InnerVertices (STC0IIStr (x1,x2,x3,x5,x6,x7))) by ENUMSET1:3
.= ({(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))} \ (InnerVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)))) \/ ({x4} \ (InnerVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)))) by XBOOLE_1:42
.= ({(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))} \ (InnerVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)))) \/ {x4} by A2, ZFMISC_1:59
.= {} \/ {x4} by A5, XBOOLE_1:46
.= {x4} ;
A7: ( GFA0AdderOutput (x1,x2,x3) <> [<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2] & GFA0AdderOutput (x5,x6,x7) <> [<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2] ) by LmSTC0IS1;
( InnerVertices (BitGFA0Str ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)) misses InputVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) & STC0IIStr (x1,x2,x3,x5,x6,x7) tolerates BitGFA0Str ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4) ) by LmSTC0IS2b, CIRCCOMB:47;
hence InputVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) = (InputVertices (STC0IIStr (x1,x2,x3,x5,x6,x7))) \/ ((InputVertices (BitGFA0Str ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))) \ (InnerVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)))) by FACIRC_1:4
.= {x1,x2,x3,x5,x6,x7} \/ ((InputVertices (BitGFA0Str ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))) \ (InnerVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)))) by ThSTC0IIS4
.= {x1,x2,x3,x5,x6,x7} \/ {x4} by A0, A1, A7, GFACIRC1:33, A6
.= ({x1,x2,x3} \/ {x5,x6,x7}) \/ {x4} by ENUMSET1:13
.= {x1,x2,x3} \/ ({x5,x6,x7} \/ {x4}) by XBOOLE_1:4
.= {x1,x2,x3} \/ {x4,x5,x6,x7} by ENUMSET1:4
.= {x1,x2,x3,x4,x5,x6,x7} by ENUMSET1:18 ;
:: thesis: verum