theorem ThSTC0S6:
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set holds
(
x1 in the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) &
x2 in the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) &
x3 in the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) &
x4 in the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) &
x5 in the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) &
x6 in the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) &
x7 in the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) &
[<*x1,x2*>,xor2] in the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) &
[<*x1,x2*>,and2] in the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) &
[<*x2,x3*>,and2] in the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) &
[<*x3,x1*>,and2] in the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) &
[<*x5,x6*>,xor2] in the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) &
[<*x5,x6*>,and2] in the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) &
[<*x6,x7*>,and2] in the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) &
[<*x7,x5*>,and2] in the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) &
GFA0AdderOutput (
x1,
x2,
x3)
in the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) &
GFA0CarryOutput (
x1,
x2,
x3)
in the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) &
GFA0AdderOutput (
x5,
x6,
x7)
in the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) &
GFA0CarryOutput (
x5,
x6,
x7)
in the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) &
[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2] in the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) &
[<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2] in the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) &
[<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2] in the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) &
[<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2] in the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) &
GFA0AdderOutput (
(GFA0AdderOutput (x1,x2,x3)),
(GFA0AdderOutput (x5,x6,x7)),
x4)
in the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) &
GFA0CarryOutput (
(GFA0AdderOutput (x1,x2,x3)),
(GFA0AdderOutput (x5,x6,x7)),
x4)
in the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) &
[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2] in the
carrier of
(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 the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) &
[<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2] in the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) &
[<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2] in the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) &
[<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2] in the
carrier of
(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 the
carrier of
(STC0Str (x1,x2,x3,x4,x5,x6,x7)) )