let x1, x2, x3, x4, x5, x6, x7 be set ; :: thesis: ( [<*x1,x2*>,xor2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*x1,x2*>,and2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*x2,x3*>,and2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*x3,x1*>,and2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*x5,x6*>,xor2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*x5,x6*>,and2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*x6,x7*>,and2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*x7,x5*>,and2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & GFA0AdderOutput (x1,x2,x3) in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & GFA0CarryOutput (x1,x2,x3) in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & GFA0AdderOutput (x5,x6,x7) in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & GFA0CarryOutput (x5,x6,x7) in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4) in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4) in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & GFA0AdderOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))) in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & GFA0CarryOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))) in InnerVertices (STC0Str (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 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)));
set p1 = {[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3)),[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2],(GFA0CarryOutput (x1,x2,x3))};
set p2 = {[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7)),[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2],(GFA0CarryOutput (x5,x6,x7))};
set p3 = {[<*(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))};
set p4 = {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)))),[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2],[<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2],[<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2],(GFA0CarryOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))};
A1: ( [<*x1,x2*>,xor2] in {[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3)),[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2],(GFA0CarryOutput (x1,x2,x3))} & GFA0AdderOutput (x1,x2,x3) in {[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3)),[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2],(GFA0CarryOutput (x1,x2,x3))} & [<*x1,x2*>,and2] in {[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3)),[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2],(GFA0CarryOutput (x1,x2,x3))} & [<*x2,x3*>,and2] in {[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3)),[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2],(GFA0CarryOutput (x1,x2,x3))} & [<*x3,x1*>,and2] in {[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3)),[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2],(GFA0CarryOutput (x1,x2,x3))} & GFA0CarryOutput (x1,x2,x3) in {[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3)),[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2],(GFA0CarryOutput (x1,x2,x3))} ) by ENUMSET1:def 4;
A2: ( [<*x5,x6*>,xor2] in {[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7)),[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2],(GFA0CarryOutput (x5,x6,x7))} & GFA0AdderOutput (x5,x6,x7) in {[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7)),[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2],(GFA0CarryOutput (x5,x6,x7))} & [<*x5,x6*>,and2] in {[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7)),[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2],(GFA0CarryOutput (x5,x6,x7))} & [<*x6,x7*>,and2] in {[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7)),[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2],(GFA0CarryOutput (x5,x6,x7))} & [<*x7,x5*>,and2] in {[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7)),[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2],(GFA0CarryOutput (x5,x6,x7))} & GFA0CarryOutput (x5,x6,x7) in {[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7)),[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2],(GFA0CarryOutput (x5,x6,x7))} ) by ENUMSET1:def 4;
A3: ( [<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2] in {[<*(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))} & GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4) in {[<*(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))} & [<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2] in {[<*(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))} & [<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2] in {[<*(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))} & [<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2] in {[<*(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))} & GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4) in {[<*(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:def 4;
A4: ( [<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2] in {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)))),[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2],[<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2],[<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2],(GFA0CarryOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))} & [<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2] in {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)))),[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2],[<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2],[<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2],(GFA0CarryOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))} & [<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2] in {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)))),[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2],[<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2],[<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2],(GFA0CarryOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))} & [<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2] in {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)))),[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2],[<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2],[<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2],(GFA0CarryOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))} & GFA0AdderOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))) in {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)))),[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2],[<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2],[<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2],(GFA0CarryOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))} & GFA0CarryOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))) in {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)))),[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2],[<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2],[<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2],(GFA0CarryOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))} ) by ENUMSET1:def 4;
InnerVertices (STC0Str (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))}) \/ {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))}) \/ {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2],[<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2],[<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2],(GFA0CarryOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))} by ThSTC0S1
.= ((((({[<*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))}) \/ {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))}) \/ {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2],[<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2],[<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2],(GFA0CarryOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))} by ENUMSET1:12
.= (((({[<*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))}) \/ {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))}) \/ {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2],[<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2],[<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2],(GFA0CarryOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))} by XBOOLE_1:4
.= (((({[<*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))}) \/ {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))}) \/ {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2],[<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2],[<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2],(GFA0CarryOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))} by ENUMSET1:12
.= ((({[<*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))}) \/ {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))}) \/ {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2],[<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2],[<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2],(GFA0CarryOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))} by XBOOLE_1:4
.= (({[<*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))})) \/ {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))}) \/ {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2],[<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2],[<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2],(GFA0CarryOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))} by XBOOLE_1:4
.= (({[<*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))}))) \/ {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))}) \/ {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2],[<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2],[<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2],(GFA0CarryOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))} by XBOOLE_1:4
.= (({[<*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))})) \/ {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))}) \/ {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2],[<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2],[<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2],(GFA0CarryOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))} by ENUMSET1:12
.= ({[<*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))}) \/ {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))})) \/ {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2],[<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2],[<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2],(GFA0CarryOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))} by XBOOLE_1:4
.= {[<*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))}) \/ {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))}) \/ {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2],[<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2],[<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2],(GFA0CarryOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))}) by XBOOLE_1:4
.= {[<*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))}) \/ ({[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))} \/ {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2],[<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2],[<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2],(GFA0CarryOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))})) by XBOOLE_1:4
.= {[<*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))}) \/ {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)))),[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2],[<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2],[<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2],(GFA0CarryOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))}) by ENUMSET1:12
.= ({[<*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))})) \/ {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)))),[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2],[<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2],[<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2],(GFA0CarryOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))} by XBOOLE_1:4
.= (({[<*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))}) \/ {[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2],(GFA0AdderOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)))),[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2],[<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2],[<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2],(GFA0CarryOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))} by XBOOLE_1:4 ;
hence ( [<*x1,x2*>,xor2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*x1,x2*>,and2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*x2,x3*>,and2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*x3,x1*>,and2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*x5,x6*>,xor2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*x5,x6*>,and2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*x6,x7*>,and2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*x7,x5*>,and2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & GFA0AdderOutput (x1,x2,x3) in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & GFA0CarryOutput (x1,x2,x3) in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & GFA0AdderOutput (x5,x6,x7) in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & GFA0CarryOutput (x5,x6,x7) in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4) in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4) in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & GFA0AdderOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))) in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & [<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2] in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) & GFA0CarryOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))) in InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) ) by A1, A2, A3, A4, LmSTC0S7a; :: thesis: verum