let x1, x2, x3, x5, x6, x7 be set ; :: thesis: ( x1 in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & x2 in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & x3 in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & x5 in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & x6 in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & x7 in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & [<*x1,x2*>,xor2] in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & GFA0AdderOutput (x1,x2,x3) in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & [<*x1,x2*>,and2] in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & [<*x2,x3*>,and2] in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & [<*x3,x1*>,and2] in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & GFA0CarryOutput (x1,x2,x3) in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & [<*x5,x6*>,xor2] in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & GFA0AdderOutput (x5,x6,x7) in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & [<*x5,x6*>,and2] in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & [<*x6,x7*>,and2] in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & [<*x7,x5*>,and2] in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & GFA0CarryOutput (x5,x6,x7) in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) )
set S = STC0IIStr (x1,x2,x3,x5,x6,x7);
set S1 = BitGFA0Str (x1,x2,x3);
set A1 = GFA0AdderOutput (x1,x2,x3);
set C1 = GFA0CarryOutput (x1,x2,x3);
set S2 = BitGFA0Str (x5,x6,x7);
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];
A1: ( x1 in the carrier of (BitGFA0Str (x1,x2,x3)) & x2 in the carrier of (BitGFA0Str (x1,x2,x3)) & x3 in the carrier of (BitGFA0Str (x1,x2,x3)) & [<*x1,x2*>,xor2] in the carrier of (BitGFA0Str (x1,x2,x3)) & GFA0AdderOutput (x1,x2,x3) in the carrier of (BitGFA0Str (x1,x2,x3)) & [<*x1,x2*>,and2] in the carrier of (BitGFA0Str (x1,x2,x3)) & [<*x2,x3*>,and2] in the carrier of (BitGFA0Str (x1,x2,x3)) & [<*x3,x1*>,and2] in the carrier of (BitGFA0Str (x1,x2,x3)) & GFA0CarryOutput (x1,x2,x3) in the carrier of (BitGFA0Str (x1,x2,x3)) ) by GFACIRC1:36;
( x5 in the carrier of (BitGFA0Str (x5,x6,x7)) & x6 in the carrier of (BitGFA0Str (x5,x6,x7)) & x7 in the carrier of (BitGFA0Str (x5,x6,x7)) & [<*x5,x6*>,xor2] in the carrier of (BitGFA0Str (x5,x6,x7)) & GFA0AdderOutput (x5,x6,x7) in the carrier of (BitGFA0Str (x5,x6,x7)) & [<*x5,x6*>,and2] in the carrier of (BitGFA0Str (x5,x6,x7)) & [<*x6,x7*>,and2] in the carrier of (BitGFA0Str (x5,x6,x7)) & [<*x7,x5*>,and2] in the carrier of (BitGFA0Str (x5,x6,x7)) & GFA0CarryOutput (x5,x6,x7) in the carrier of (BitGFA0Str (x5,x6,x7)) ) by GFACIRC1:36;
hence ( x1 in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & x2 in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & x3 in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & x5 in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & x6 in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & x7 in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & [<*x1,x2*>,xor2] in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & GFA0AdderOutput (x1,x2,x3) in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & [<*x1,x2*>,and2] in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & [<*x2,x3*>,and2] in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & [<*x3,x1*>,and2] in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & GFA0CarryOutput (x1,x2,x3) in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & [<*x5,x6*>,xor2] in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & GFA0AdderOutput (x5,x6,x7) in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & [<*x5,x6*>,and2] in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & [<*x6,x7*>,and2] in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & [<*x7,x5*>,and2] in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & GFA0CarryOutput (x5,x6,x7) in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) ) by A1, FACIRC_1:20; :: thesis: verum