let x1, x2, x3, x4, x5, x6, x7 be non pair set ; InputVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) = {x1,x2,x3,x4,x5,x6,x7}
set S = STC0Str (x1,x2,x3,x4,x5,x6,x7);
set S1 = STC0IStr (x1,x2,x3,x4,x5,x6,x7);
set S11 = STC0IIStr (x1,x2,x3,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 A1 = GFA0AdderOutput (x1,x2,x3);
set A2 = GFA0AdderOutput (x5,x6,x7);
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];
set A3 = GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4);
set C1 = GFA0CarryOutput (x1,x2,x3);
set C2 = GFA0CarryOutput (x5,x6,x7);
set C3 = GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4);
set S2 = BitGFA0Str ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)));
set C1C2x = [<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2];
set C1C2a = [<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2];
set C2C3a = [<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2];
set C3C1a = [<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2];
set Aout = GFA0AdderOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)));
set Cout = GFA0CarryOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)));
A2: InnerVertices (STC0IStr (x1,x2,x3,x4,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))}) \/ {[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))}) \/ {[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2],[<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2],[<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2],(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))}
by ThSTC0IS1
.=
(((({[<*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))}) \/ {[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))}) \/ {[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2],[<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2],[<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2],(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))}
by ENUMSET1:6
.=
((((({[<*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))}) \/ {[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))}) \/ {[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2],[<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2],[<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2],(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))}
by XBOOLE_1:4
.=
(((({(GFA0CarryOutput (x1,x2,x3))} \/ ({[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3))} \/ {[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2]})) \/ {[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7))}) \/ ({[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2]} \/ {(GFA0CarryOutput (x5,x6,x7))})) \/ {[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))}) \/ {[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2],[<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2],[<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2],(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))}
by ENUMSET1:6
.=
(((({(GFA0CarryOutput (x1,x2,x3))} \/ {[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3)),[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2]}) \/ {[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7))}) \/ ({[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2]} \/ {(GFA0CarryOutput (x5,x6,x7))})) \/ {[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))}) \/ {[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2],[<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2],[<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2],(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))}
by ENUMSET1:8
.=
((((({(GFA0CarryOutput (x1,x2,x3))} \/ {[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3)),[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2]}) \/ {[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7))}) \/ {[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2]}) \/ {(GFA0CarryOutput (x5,x6,x7))}) \/ {[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))}) \/ {[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2],[<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2],[<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2],(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))}
by XBOOLE_1:4
.=
(({(GFA0CarryOutput (x5,x6,x7))} \/ ((({(GFA0CarryOutput (x1,x2,x3))} \/ {[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3)),[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2]}) \/ {[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7))}) \/ {[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2]})) \/ {[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))}) \/ ({[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2],[<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2],[<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2]} \/ {(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))})
by ENUMSET1:6
.=
(({(GFA0CarryOutput (x5,x6,x7))} \/ (({(GFA0CarryOutput (x1,x2,x3))} \/ {[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3)),[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2]}) \/ ({[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7))} \/ {[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2]}))) \/ {[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))}) \/ ({[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2],[<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2],[<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2]} \/ {(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))})
by XBOOLE_1:4
.=
(({(GFA0CarryOutput (x5,x6,x7))} \/ (({(GFA0CarryOutput (x1,x2,x3))} \/ {[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3)),[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2]}) \/ {[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7)),[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2]})) \/ {[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))}) \/ ({[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2],[<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2],[<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2]} \/ {(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))})
by ENUMSET1:8
.=
((({(GFA0CarryOutput (x5,x6,x7))} \/ (({(GFA0CarryOutput (x1,x2,x3))} \/ {[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3)),[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2]}) \/ {[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7)),[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2]})) \/ {[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))}) \/ {[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2],[<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2],[<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2]}) \/ {(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))}
by XBOOLE_1:4
.=
{(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))} \/ (({(GFA0CarryOutput (x5,x6,x7))} \/ (({(GFA0CarryOutput (x1,x2,x3))} \/ {[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3)),[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2]}) \/ {[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7)),[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2]})) \/ ({[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))} \/ {[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2],[<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2],[<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2]}))
by XBOOLE_1:4
.=
{(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))} \/ (({(GFA0CarryOutput (x5,x6,x7))} \/ (({(GFA0CarryOutput (x1,x2,x3))} \/ {[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3)),[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2]}) \/ {[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7)),[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2]})) \/ {[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2],[<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2],[<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2]})
by ENUMSET1:8
.=
{(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))} \/ ({(GFA0CarryOutput (x5,x6,x7))} \/ ((({(GFA0CarryOutput (x1,x2,x3))} \/ {[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3)),[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2]}) \/ {[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7)),[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2]}) \/ {[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2],[<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2],[<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2]}))
by XBOOLE_1:4
.=
({(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))} \/ {(GFA0CarryOutput (x5,x6,x7))}) \/ ((({(GFA0CarryOutput (x1,x2,x3))} \/ {[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3)),[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2]}) \/ {[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7)),[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2]}) \/ {[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2],[<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2],[<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2]})
by XBOOLE_1:4
.=
{(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x5,x6,x7))} \/ ((({(GFA0CarryOutput (x1,x2,x3))} \/ {[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3)),[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2]}) \/ {[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7)),[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2]}) \/ {[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2],[<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2],[<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2]})
by ENUMSET1:1
.=
{(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x5,x6,x7))} \/ (({(GFA0CarryOutput (x1,x2,x3))} \/ ({[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3)),[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2]} \/ {[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7)),[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2]})) \/ {[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2],[<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2],[<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2]})
by XBOOLE_1:4
.=
{(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x5,x6,x7))} \/ ({(GFA0CarryOutput (x1,x2,x3))} \/ (({[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3)),[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2]} \/ {[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7)),[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2]}) \/ {[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2],[<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2],[<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2]}))
by XBOOLE_1:4
.=
({(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x5,x6,x7))} \/ {(GFA0CarryOutput (x1,x2,x3))}) \/ (({[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3)),[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2]} \/ {[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7)),[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2]}) \/ {[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2],[<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2],[<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2]})
by XBOOLE_1:4
.=
{(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))} \/ (({[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3)),[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2]} \/ {[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7)),[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2]}) \/ {[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2],[<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2],[<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2]})
by ENUMSET1:2
;
A3:
( GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4) <> [<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2] & GFA0CarryOutput (x1,x2,x3) <> [<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2] & GFA0CarryOutput (x5,x6,x7) <> [<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2] & GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4) <> [<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2] )
by LmSTC0S1;
( InnerVertices (BitGFA0Str ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)))) is Relation & InputVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) is without_pairs )
by ThSTC0IS5;
then A5:
InnerVertices (BitGFA0Str ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)))) misses InputVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7))
;
STC0IStr (x1,x2,x3,x4,x5,x6,x7) tolerates BitGFA0Str ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)))
by CIRCCOMB:47;
hence InputVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) =
(InputVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7))) \/ ((InputVertices (BitGFA0Str ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))) \ (InnerVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7))))
by A5, FACIRC_1:4
.=
{x1,x2,x3,x4,x5,x6,x7} \/ ((InputVertices (BitGFA0Str ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))) \ (InnerVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7))))
by ThSTC0IS4
.=
{x1,x2,x3,x4,x5,x6,x7} \/ ({(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))} \ (InnerVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7))))
by A3, GFACIRC1:33
.=
{x1,x2,x3,x4,x5,x6,x7} \/ {}
by A2, XBOOLE_1:46
.=
{x1,x2,x3,x4,x5,x6,x7}
;
verum