wallace1.miz
begin
registration
let x1,x2,x3,x4 be non
pair
object;
cluster
{x1, x2, x3, x4} ->
without_pairs;
coherence by
ENUMSET1:def 2;
let x5 be non
pair
object;
cluster
{x1, x2, x3, x4, x5} ->
without_pairs;
coherence by
ENUMSET1:def 3;
let x6 be non
pair
object;
cluster
{x1, x2, x3, x4, x5, x6} ->
without_pairs;
coherence by
ENUMSET1:def 4;
let x7 be non
pair
object;
cluster
{x1, x2, x3, x4, x5, x6, x7} ->
without_pairs;
coherence by
ENUMSET1:def 5;
end
definition
let x1,x2,x3,x5,x6,x7 be
set;
::
WALLACE1:def1
func
STC0IIStr (x1,x2,x3,x5,x6,x7) ->
unsplit
gate`1=arity
gate`2isBoolean non
void
strict non
empty
ManySortedSign equals ((
BitGFA0Str (x1,x2,x3))
+* (
BitGFA0Str (x5,x6,x7)));
coherence ;
end
definition
let x1,x2,x3,x5,x6,x7 be
set;
::
WALLACE1:def2
func
STC0IICirc (x1,x2,x3,x5,x6,x7) ->
strict
Boolean
gate`2=den
Circuit of (
STC0IIStr (x1,x2,x3,x5,x6,x7)) equals ((
BitGFA0Circ (x1,x2,x3))
+* (
BitGFA0Circ (x5,x6,x7)));
coherence ;
end
theorem ::
WALLACE1:1
ThSTC0IIS1: for x1,x2,x3,x5,x6,x7 be
set holds (
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))})
proof
let x1,x2,x3,x5,x6,x7 be
set;
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 ];
S1
tolerates S2 by
CIRCCOMB: 47;
hence (
InnerVertices S)
= ((
InnerVertices S1)
\/ (
InnerVertices S2)) by
CIRCCOMB: 11
.= ((((
{x1x20}
\/
{A1})
\/
{x1x2, x2x3, x3x1})
\/
{C1})
\/ (
InnerVertices S2)) by
GFACIRC1: 31
.= (((
{x1x20, A1}
\/
{x1x2, x2x3, x3x1})
\/
{C1})
\/ (
InnerVertices S2)) by
ENUMSET1: 1
.= ((
{x1x20, A1}
\/ (
{x1x2, x2x3, x3x1}
\/
{C1}))
\/ (
InnerVertices S2)) by
XBOOLE_1: 4
.= ((
{x1x20, A1}
\/
{x1x2, x2x3, x3x1, C1})
\/ (
InnerVertices S2)) by
ENUMSET1: 6
.= ((
{x1x20, A1}
\/
{x1x2, x2x3, x3x1, C1})
\/ (((
{x5x60}
\/
{A2})
\/
{x5x6, x6x7, x7x5})
\/
{C2})) by
GFACIRC1: 31
.= ((
{x1x20, A1}
\/
{x1x2, x2x3, x3x1, C1})
\/ ((
{x5x60, A2}
\/
{x5x6, x6x7, x7x5})
\/
{C2})) by
ENUMSET1: 1
.= ((
{x1x20, A1}
\/
{x1x2, x2x3, x3x1, C1})
\/ (
{x5x60, A2}
\/ (
{x5x6, x6x7, x7x5}
\/
{C2}))) by
XBOOLE_1: 4
.= ((
{x1x20, A1}
\/
{x1x2, x2x3, x3x1, C1})
\/ (
{x5x60, A2}
\/
{x5x6, x6x7, x7x5, C2})) by
ENUMSET1: 6
.= (((
{x1x20, A1}
\/
{x1x2, x2x3, x3x1, C1})
\/
{x5x60, A2})
\/
{x5x6, x6x7, x7x5, C2}) by
XBOOLE_1: 4;
end;
theorem ::
WALLACE1:2
for x1,x2,x3,x5,x6,x7 be
set holds (
InnerVertices (
STC0IIStr (x1,x2,x3,x5,x6,x7))) is
Relation;
theorem ::
WALLACE1:3
ThSTC0IIS4: for x1,x2,x3,x5,x6,x7 be non
pair
set holds (
InputVertices (
STC0IIStr (x1,x2,x3,x5,x6,x7)))
=
{x1, x2, x3, x5, x6, x7}
proof
let x1,x2,x3,x5,x6,x7 be non
pair
set;
set S = (
STC0IIStr (x1,x2,x3,x5,x6,x7));
set S1 = (
BitGFA0Str (x1,x2,x3));
set S2 = (
BitGFA0Str (x5,x6,x7));
A1: (
InputVertices S1)
=
{x1, x2, x3} & (
InputVertices S2)
=
{x5, x6, x7} by
GFACIRC1: 34;
(
InnerVertices S1) is
Relation & (
InnerVertices S2) is
Relation;
hence (
InputVertices S)
= (
{x1, x2, x3}
\/
{x5, x6, x7}) by
A1,
FACIRC_1: 7
.=
{x1, x2, x3, x5, x6, x7} by
ENUMSET1: 13;
end;
theorem ::
WALLACE1:4
ThSTC0IIS5: for x1,x2,x3,x5,x6,x7 be non
pair
set holds (
InputVertices (
STC0IIStr (x1,x2,x3,x5,x6,x7))) is
without_pairs
proof
let x1,x2,x3,x5,x6,x7 be non
pair
set;
(
InputVertices (
BitGFA0Str (x1,x2,x3))) is
without_pairs & (
InputVertices (
BitGFA0Str (x5,x6,x7))) is
without_pairs by
GFACIRC1: 35;
hence thesis by
CIRCCOMB: 47,
FACIRC_1: 8;
end;
theorem ::
WALLACE1:5
ThSTC0IIS6: for x1,x2,x3,x5,x6,x7 be
set holds 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))
proof
let x1,x2,x3,x5,x6,x7 be
set;
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 S1 & x2
in the
carrier of S1 & x3
in the
carrier of S1 & x1x20
in the
carrier of S1 & A1
in the
carrier of S1 & x1x2
in the
carrier of S1 & x2x3
in the
carrier of S1 & x3x1
in the
carrier of S1 & C1
in the
carrier of S1 by
GFACIRC1: 36;
x5
in the
carrier of S2 & x6
in the
carrier of S2 & x7
in the
carrier of S2 & x5x60
in the
carrier of S2 & A2
in the
carrier of S2 & x5x6
in the
carrier of S2 & x6x7
in the
carrier of S2 & x7x5
in the
carrier of S2 & C2
in the
carrier of S2 by
GFACIRC1: 36;
hence thesis by
A1,
FACIRC_1: 20;
end;
theorem ::
WALLACE1:6
ThSTC0IIS7: for x1,x2,x3,x5,x6,x7 be
set holds
[
<*x1, x2*>,
xor2 ]
in (
InnerVertices (
STC0IIStr (x1,x2,x3,x5,x6,x7))) & (
GFA0AdderOutput (x1,x2,x3))
in (
InnerVertices (
STC0IIStr (x1,x2,x3,x5,x6,x7))) &
[
<*x1, x2*>,
and2 ]
in (
InnerVertices (
STC0IIStr (x1,x2,x3,x5,x6,x7))) &
[
<*x2, x3*>,
and2 ]
in (
InnerVertices (
STC0IIStr (x1,x2,x3,x5,x6,x7))) &
[
<*x3, x1*>,
and2 ]
in (
InnerVertices (
STC0IIStr (x1,x2,x3,x5,x6,x7))) & (
GFA0CarryOutput (x1,x2,x3))
in (
InnerVertices (
STC0IIStr (x1,x2,x3,x5,x6,x7))) &
[
<*x5, x6*>,
xor2 ]
in (
InnerVertices (
STC0IIStr (x1,x2,x3,x5,x6,x7))) & (
GFA0AdderOutput (x5,x6,x7))
in (
InnerVertices (
STC0IIStr (x1,x2,x3,x5,x6,x7))) &
[
<*x5, x6*>,
and2 ]
in (
InnerVertices (
STC0IIStr (x1,x2,x3,x5,x6,x7))) &
[
<*x6, x7*>,
and2 ]
in (
InnerVertices (
STC0IIStr (x1,x2,x3,x5,x6,x7))) &
[
<*x7, x5*>,
and2 ]
in (
InnerVertices (
STC0IIStr (x1,x2,x3,x5,x6,x7))) & (
GFA0CarryOutput (x5,x6,x7))
in (
InnerVertices (
STC0IIStr (x1,x2,x3,x5,x6,x7)))
proof
let x1,x2,x3,x5,x6,x7 be
set;
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 ];
set p1 =
{x1x20, A1, x1x2, x2x3, x3x1, C1};
set p2 =
{x5x60, A2, x5x6, x6x7, x7x5, C2};
A1: x1x20
in p1 & A1
in p1 & x1x2
in p1 & x2x3
in p1 & x3x1
in p1 & C1
in p1 by
ENUMSET1:def 4;
A2: x5x60
in p2 & A2
in p2 & x5x6
in p2 & x6x7
in p2 & x7x5
in p2 & C2
in p2 by
ENUMSET1:def 4;
(
InnerVertices S)
= (((
{x1x20, A1}
\/
{x1x2, x2x3, x3x1, C1})
\/
{x5x60, A2})
\/
{x5x6, x6x7, x7x5, C2}) by
ThSTC0IIS1
.= ((p1
\/
{x5x60, A2})
\/
{x5x6, x6x7, x7x5, C2}) by
ENUMSET1: 12
.= (p1
\/ (
{x5x60, A2}
\/
{x5x6, x6x7, x7x5, C2})) by
XBOOLE_1: 4
.= (p1
\/ p2) by
ENUMSET1: 12;
hence thesis by
A1,
A2,
XBOOLE_0:def 3;
end;
theorem ::
WALLACE1:7
ThSTC0IIS8: for x1,x2,x3,x5,x6,x7 be non
pair
set holds x1
in (
InputVertices (
STC0IIStr (x1,x2,x3,x5,x6,x7))) & x2
in (
InputVertices (
STC0IIStr (x1,x2,x3,x5,x6,x7))) & x3
in (
InputVertices (
STC0IIStr (x1,x2,x3,x5,x6,x7))) & x5
in (
InputVertices (
STC0IIStr (x1,x2,x3,x5,x6,x7))) & x6
in (
InputVertices (
STC0IIStr (x1,x2,x3,x5,x6,x7))) & x7
in (
InputVertices (
STC0IIStr (x1,x2,x3,x5,x6,x7)))
proof
let x1,x2,x3,x5,x6,x7 be non
pair
set;
set S = (
STC0IIStr (x1,x2,x3,x5,x6,x7));
(
InputVertices S)
=
{x1, x2, x3, x5, x6, x7} by
ThSTC0IIS4;
hence thesis by
ENUMSET1:def 4;
end;
definition
let x1,x2,x3,x5,x6,x7 be
set;
::
WALLACE1:def3
func
STC0IICarryOutputC1 (x1,x2,x3,x5,x6,x7) ->
Element of (
InnerVertices (
STC0IIStr (x1,x2,x3,x5,x6,x7))) equals (
GFA0CarryOutput (x1,x2,x3));
coherence by
ThSTC0IIS7;
::
WALLACE1:def4
func
STC0IIAdderOutputA1 (x1,x2,x3,x5,x6,x7) ->
Element of (
InnerVertices (
STC0IIStr (x1,x2,x3,x5,x6,x7))) equals (
GFA0AdderOutput (x1,x2,x3));
coherence by
ThSTC0IIS7;
::
WALLACE1:def5
func
STC0IICarryOutputC2 (x1,x2,x3,x5,x6,x7) ->
Element of (
InnerVertices (
STC0IIStr (x1,x2,x3,x5,x6,x7))) equals (
GFA0CarryOutput (x5,x6,x7));
coherence by
ThSTC0IIS7;
::
WALLACE1:def6
func
STC0IIAdderOutputA2 (x1,x2,x3,x5,x6,x7) ->
Element of (
InnerVertices (
STC0IIStr (x1,x2,x3,x5,x6,x7))) equals (
GFA0AdderOutput (x5,x6,x7));
coherence by
ThSTC0IIS7;
end
LmSTC0IIS09a: for a,b,c be non
pair
set holds for x,y,z be
set holds (
InputVertices (
BitGFA0Str (a,b,c)))
misses (
InnerVertices (
BitGFA0Str (x,y,z)))
proof
let a,b,c be non
pair
set;
let x,y,z be
set;
set S1 = (
BitGFA0Str (a,b,c));
set S2 = (
BitGFA0Str (x,y,z));
(
InputVertices S1) is
without_pairs & (
InnerVertices S2) is
Relation by
GFACIRC1: 35;
hence thesis;
end;
theorem ::
WALLACE1:8
ThSTC0IIS10: for x1,x2,x3,x5,x6,x7 be non
pair
set holds for s be
State of (
STC0IICirc (x1,x2,x3,x5,x6,x7)) holds for a1,a2,a3,a5,a6,a7 be
Element of
BOOLEAN st a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7) holds ((
Following (s,2))
. (
STC0IICarryOutputC1 (x1,x2,x3,x5,x6,x7)))
= (((a1
'&' a2)
'or' (a2
'&' a3))
'or' (a3
'&' a1)) & ((
Following (s,2))
. (
STC0IIAdderOutputA1 (x1,x2,x3,x5,x6,x7)))
= ((a1
'xor' a2)
'xor' a3) & ((
Following (s,2))
. (
STC0IICarryOutputC2 (x1,x2,x3,x5,x6,x7)))
= (((a5
'&' a6)
'or' (a6
'&' a7))
'or' (a7
'&' a5)) & ((
Following (s,2))
. (
STC0IIAdderOutputA2 (x1,x2,x3,x5,x6,x7)))
= ((a5
'xor' a6)
'xor' a7) & ((
Following (s,2))
. x1)
= a1 & ((
Following (s,2))
. x2)
= a2 & ((
Following (s,2))
. x3)
= a3 & ((
Following (s,2))
. x5)
= a5 & ((
Following (s,2))
. x6)
= a6 & ((
Following (s,2))
. x7)
= a7
proof
let x1,x2,x3,x5,x6,x7 be non
pair
set;
set S = (
STC0IIStr (x1,x2,x3,x5,x6,x7));
set S1 = (
BitGFA0Str (x1,x2,x3));
set S2 = (
BitGFA0Str (x5,x6,x7));
set C = (
STC0IICirc (x1,x2,x3,x5,x6,x7));
set C1 = (
BitGFA0Circ (x1,x2,x3));
set C2 = (
BitGFA0Circ (x5,x6,x7));
set C1out = (
STC0IICarryOutputC1 (x1,x2,x3,x5,x6,x7));
set A1out = (
STC0IIAdderOutputA1 (x1,x2,x3,x5,x6,x7));
set C2out = (
STC0IICarryOutputC2 (x1,x2,x3,x5,x6,x7));
set A2out = (
STC0IIAdderOutputA2 (x1,x2,x3,x5,x6,x7));
let s be
State of C;
let a1,a2,a3,a5,a6,a7 be
Element of
BOOLEAN such that
A1: a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7);
A2: x1
in (
InputVertices S) & x2
in (
InputVertices S) & x3
in (
InputVertices S) & x5
in (
InputVertices S) & x6
in (
InputVertices S) & x7
in (
InputVertices S) by
ThSTC0IIS8;
reconsider t = s as
State of (C1
+* C2);
reconsider s1 = (s
| the
carrier of S1) as
State of C1 by
FACIRC_1: 26;
A10: (
dom s1)
= the
carrier of S1 by
CIRCUIT1: 3;
C1out
in the
carrier of S1 & A1out
in the
carrier of S1 & (
InputVertices S1)
misses (
InnerVertices S2) by
GFACIRC1: 36,
LmSTC0IIS09a;
then
A11: ((
Following (t,2))
. C1out)
= ((
Following (s1,2))
. C1out) & ((
Following (t,2))
. A1out)
= ((
Following (s1,2))
. A1out) by
FACIRC_1: 32;
A3: a1
= (s1
. x1) & a2
= (s1
. x2) & a3
= (s1
. x3) by
GFACIRC1: 36,
A1,
A10,
FUNCT_1: 47;
reconsider s2 = (s
| the
carrier of S2) as
State of C2 by
FACIRC_1: 26;
A13: (
dom s2)
= the
carrier of S2 by
CIRCUIT1: 3;
C2out
in the
carrier of S2 & A2out
in the
carrier of S2 & (
InnerVertices S1)
misses (
InputVertices S2) by
GFACIRC1: 36,
LmSTC0IIS09a;
then
A14: ((
Following (t,2))
. C2out)
= ((
Following (s2,2))
. C2out) & ((
Following (t,2))
. A2out)
= ((
Following (s2,2))
. A2out) by
FACIRC_1: 33;
a5
= (s2
. x5) & a6
= (s2
. x6) & a7
= (s2
. x7) by
GFACIRC1: 36,
A1,
A13,
FUNCT_1: 47;
hence thesis by
A1,
A2,
CIRCCMB3: 1,
A3,
A11,
A14,
GFACIRC1: 39;
end;
theorem ::
WALLACE1:9
ThSTC0IIS12: for x1,x2,x3,x5,x6,x7 be non
pair
set holds for s be
State of (
STC0IICirc (x1,x2,x3,x5,x6,x7)) holds (
Following (s,2)) is
stable
proof
let x1,x2,x3,x5,x6,x7 be non
pair
set;
set S1 = (
BitGFA0Str (x1,x2,x3));
set S2 = (
BitGFA0Str (x5,x6,x7));
set C = (
STC0IICirc (x1,x2,x3,x5,x6,x7));
set C1 = (
BitGFA0Circ (x1,x2,x3));
set C2 = (
BitGFA0Circ (x5,x6,x7));
set n1 = 2, n2 = 2;
A1: (
InputVertices S1)
misses (
InnerVertices S2) & (
InputVertices S2)
misses (
InnerVertices S1) by
LmSTC0IIS09a;
let s be
State of C;
reconsider s1 = (s
| the
carrier of S1) as
State of C1 by
FACIRC_1: 26;
reconsider s2 = (s
| the
carrier of S2) as
State of C2 by
FACIRC_1: 26;
(
Following (s1,n1)) is
stable & (
Following (s2,n2)) is
stable by
GFACIRC1: 40;
then (
Following (s,(
max (n1,n2)))) is
stable by
A1,
CIRCCOMB: 60,
CIRCCMB2: 22;
hence thesis;
end;
begin
definition
let x1,x2,x3,x4,x5,x6,x7 be
set;
::
WALLACE1:def7
func
STC0IStr (x1,x2,x3,x4,x5,x6,x7) ->
unsplit
gate`1=arity
gate`2isBoolean non
void
strict non
empty
ManySortedSign equals ((
STC0IIStr (x1,x2,x3,x5,x6,x7))
+* (
BitGFA0Str ((
GFA0AdderOutput (x1,x2,x3)),(
GFA0AdderOutput (x5,x6,x7)),x4)));
coherence ;
end
definition
let x1,x2,x3,x4,x5,x6,x7 be
set;
::
WALLACE1:def8
func
STC0ICirc (x1,x2,x3,x4,x5,x6,x7) ->
strict
Boolean
gate`2=den
Circuit of (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)) equals ((
STC0IICirc (x1,x2,x3,x5,x6,x7))
+* (
BitGFA0Circ ((
GFA0AdderOutput (x1,x2,x3)),(
GFA0AdderOutput (x5,x6,x7)),x4)));
coherence ;
end
theorem ::
WALLACE1:10
ThSTC0IS1: for x1,x2,x3,x4,x5,x6,x7 be
set holds (
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))})
proof
let x1,x2,x3,x4,x5,x6,x7 be
set;
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 (A1,A2,x4));
set A3 = (
GFA0AdderOutput (A1,A2,x4));
set C3 = (
GFA0CarryOutput (A1,A2,x4));
set A1A20 =
[
<*A1, A2*>,
xor2 ];
set A1A2 =
[
<*A1, A2*>,
and2 ];
set A2x4 =
[
<*A2, x4*>,
and2 ];
set x4A1 =
[
<*x4, A1*>,
and2 ];
S1
tolerates S2 by
CIRCCOMB: 47;
hence (
InnerVertices S)
= ((
InnerVertices S1)
\/ (
InnerVertices S2)) by
CIRCCOMB: 11
.= ((((
{x1x20, A1}
\/
{x1x2, x2x3, x3x1, C1})
\/
{x5x60, A2})
\/
{x5x6, x6x7, x7x5, C2})
\/ (
InnerVertices S2)) by
ThSTC0IIS1
.= ((((
{x1x20, A1}
\/
{x1x2, x2x3, x3x1, C1})
\/
{x5x60, A2})
\/
{x5x6, x6x7, x7x5, C2})
\/ (((
{A1A20}
\/
{A3})
\/
{A1A2, A2x4, x4A1})
\/
{C3})) by
GFACIRC1: 31
.= ((((
{x1x20, A1}
\/
{x1x2, x2x3, x3x1, C1})
\/
{x5x60, A2})
\/
{x5x6, x6x7, x7x5, C2})
\/ ((
{A1A20, A3}
\/
{A1A2, A2x4, x4A1})
\/
{C3})) by
ENUMSET1: 1
.= ((((
{x1x20, A1}
\/
{x1x2, x2x3, x3x1, C1})
\/
{x5x60, A2})
\/
{x5x6, x6x7, x7x5, C2})
\/ (
{A1A20, A3}
\/ (
{A1A2, A2x4, x4A1}
\/
{C3}))) by
XBOOLE_1: 4
.= ((((
{x1x20, A1}
\/
{x1x2, x2x3, x3x1, C1})
\/
{x5x60, A2})
\/
{x5x6, x6x7, x7x5, C2})
\/ (
{A1A20, A3}
\/
{A1A2, A2x4, x4A1, C3})) by
ENUMSET1: 6
.= (((((
{x1x20, A1}
\/
{x1x2, x2x3, x3x1, C1})
\/
{x5x60, A2})
\/
{x5x6, x6x7, x7x5, C2})
\/
{A1A20, A3})
\/
{A1A2, A2x4, x4A1, C3}) by
XBOOLE_1: 4;
end;
theorem ::
WALLACE1:11
for x1,x2,x3,x4,x5,x6,x7 be
set holds (
InnerVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) is
Relation;
LmSTC0IS1: for x,y,z be
set holds for p be
set holds (
GFA0AdderOutput (x,y,z))
<>
[p,
and2 ]
proof
let x,y,z be
set, p be
set;
((
GFA0AdderOutput (x,y,z))
`2 )
=
xor2 ;
hence thesis by
TWOSCOMP: 9,
TWOSCOMP: 11;
end;
LmSTC0IS2b: for x1,x2,x3,x5,x6,x7 be non
pair
set holds for a,b,c be
set holds (
InputVertices (
STC0IIStr (x1,x2,x3,x5,x6,x7)))
misses (
InnerVertices (
BitGFA0Str (a,b,c)))
proof
let x1,x2,x3,x5,x6,x7 be non
pair
set;
let a,b,c be
set;
set S1 = (
STC0IIStr (x1,x2,x3,x5,x6,x7));
set S2 = (
BitGFA0Str (a,b,c));
(
InputVertices S1) is
without_pairs & (
InnerVertices S2) is
Relation by
ThSTC0IIS5;
hence thesis;
end;
theorem ::
WALLACE1:12
ThSTC0IS3: for x1,x2,x3,x5,x6,x7 be non
pair
set holds for x4 be
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}
proof
let x1,x2,x3,x5,x6,x7 be non
pair
set;
let x4 be
set;
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 (A1,A2,x4));
set A1A20 =
[
<*A1, A2*>,
xor2 ];
set A1A2 =
[
<*A1, A2*>,
and2 ];
set A2x4 =
[
<*A2, x4*>,
and2 ];
set x4A1 =
[
<*x4, A1*>,
and2 ];
assume that
A0: x4
<> A1A20 and
A1: x4
<> A1A2 and
A2: not x4
in (
InnerVertices S1);
A5: (
InnerVertices S1)
= (((
{x1x20, A1}
\/
{x1x2, x2x3, x3x1, C1})
\/
{x5x60, A2})
\/
{x5x6, x6x7, x7x5, C2}) by
ThSTC0IIS1
.= (((
{A1, x1x20}
\/
{A2, x5x60})
\/
{x1x2, x2x3, x3x1, C1})
\/
{x5x6, x6x7, x7x5, C2}) by
XBOOLE_1: 4
.= ((
{A1, x1x20, A2, x5x60}
\/
{x1x2, x2x3, x3x1, C1})
\/
{x5x6, x6x7, x7x5, C2}) by
ENUMSET1: 5
.= ((
{A1, A2, x1x20, x5x60}
\/
{x1x2, x2x3, x3x1, C1})
\/
{x5x6, x6x7, x7x5, C2}) by
ENUMSET1: 62
.= (((
{A1, A2}
\/
{x1x20, x5x60})
\/
{x1x2, x2x3, x3x1, C1})
\/
{x5x6, x6x7, x7x5, C2}) by
ENUMSET1: 5
.= ((
{A1, A2}
\/ (
{x1x20, x5x60}
\/
{x1x2, x2x3, x3x1, C1}))
\/
{x5x6, x6x7, x7x5, C2}) by
XBOOLE_1: 4
.= ((
{A1, A2}
\/ ((
{x1x20}
\/
{x5x60})
\/
{x1x2, x2x3, x3x1, C1}))
\/
{x5x6, x6x7, x7x5, C2}) by
ENUMSET1: 1
.= ((
{A1, A2}
\/ (
{x1x20}
\/ (
{x5x60}
\/
{x1x2, x2x3, x3x1, C1})))
\/
{x5x6, x6x7, x7x5, C2}) by
XBOOLE_1: 4
.= ((
{A1, A2}
\/ (
{x1x20}
\/
{x5x60, x1x2, x2x3, x3x1, C1}))
\/
{x5x6, x6x7, x7x5, C2}) by
ENUMSET1: 7
.= (
{A1, A2}
\/ ((
{x1x20}
\/
{x5x60, x1x2, x2x3, x3x1, C1})
\/
{x5x6, x6x7, x7x5, C2})) by
XBOOLE_1: 4
.= (
{A1, A2}
\/ (
{x1x20}
\/ (
{x5x60, x1x2, x2x3, x3x1, C1}
\/
{x5x6, x6x7, x7x5, C2}))) by
XBOOLE_1: 4
.= (
{A1, A2}
\/ (
{x1x20}
\/
{x5x60, x1x2, x2x3, x3x1, C1, x5x6, x6x7, x7x5, C2})) by
ENUMSET1: 81
.= (
{A1, A2}
\/
{x5x60, x1x2, x2x3, x3x1, C1, x5x6, x6x7, x7x5, C2, x1x20}) by
ENUMSET1: 85;
A6: (
{A1, A2, x4}
\ (
InnerVertices S1))
= ((
{A1, A2}
\/
{x4})
\ (
InnerVertices S1)) by
ENUMSET1: 3
.= ((
{A1, A2}
\ (
InnerVertices S1))
\/ (
{x4}
\ (
InnerVertices S1))) by
XBOOLE_1: 42
.= ((
{A1, A2}
\ (
InnerVertices S1))
\/
{x4}) by
A2,
ZFMISC_1: 59
.= (
{}
\/
{x4}) by
A5,
XBOOLE_1: 46
.=
{x4};
A7: A1
<> A2x4 & A2
<> x4A1 by
LmSTC0IS1;
(
InnerVertices S2)
misses (
InputVertices S1) & S1
tolerates S2 by
LmSTC0IS2b,
CIRCCOMB: 47;
hence (
InputVertices S)
= ((
InputVertices S1)
\/ ((
InputVertices S2)
\ (
InnerVertices S1))) by
FACIRC_1: 4
.= (
{x1, x2, x3, x5, x6, x7}
\/ ((
InputVertices S2)
\ (
InnerVertices S1))) 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;
end;
theorem ::
WALLACE1:13
ThSTC0IS4: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds (
InputVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)))
=
{x1, x2, x3, x4, x5, x6, x7}
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
set S1 = (
STC0IIStr (x1,x2,x3,x5,x6,x7));
{x4}
misses (
InnerVertices S1);
then (
{x4}
\ (
InnerVertices S1))
=
{x4} by
XBOOLE_1: 83;
hence thesis by
ZFMISC_1: 59,
ThSTC0IS3;
end;
theorem ::
WALLACE1:14
ThSTC0IS5: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds (
InputVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) is
without_pairs
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
(
InputVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)))
=
{x1, x2, x3, x4, x5, x6, x7} by
ThSTC0IS4;
hence thesis;
end;
theorem ::
WALLACE1:15
ThSTC0IS6: for x1,x2,x3,x4,x5,x6,x7 be
set holds x1
in the
carrier of (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)) & x2
in the
carrier of (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)) & x3
in the
carrier of (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)) & x4
in the
carrier of (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)) & x5
in the
carrier of (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)) & x6
in the
carrier of (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)) & x7
in the
carrier of (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)) &
[
<*x1, x2*>,
xor2 ]
in the
carrier of (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)) & (
GFA0AdderOutput (x1,x2,x3))
in the
carrier of (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)) &
[
<*x1, x2*>,
and2 ]
in the
carrier of (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)) &
[
<*x2, x3*>,
and2 ]
in the
carrier of (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)) &
[
<*x3, x1*>,
and2 ]
in the
carrier of (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)) & (
GFA0CarryOutput (x1,x2,x3))
in the
carrier of (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)) &
[
<*(
GFA0AdderOutput (x1,x2,x3)), (
GFA0AdderOutput (x5,x6,x7))*>,
xor2 ]
in the
carrier of (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)) & (
GFA0AdderOutput ((
GFA0AdderOutput (x1,x2,x3)),(
GFA0AdderOutput (x5,x6,x7)),x4))
in the
carrier of (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)) &
[
<*(
GFA0AdderOutput (x1,x2,x3)), (
GFA0AdderOutput (x5,x6,x7))*>,
and2 ]
in the
carrier of (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)) &
[
<*(
GFA0AdderOutput (x5,x6,x7)), x4*>,
and2 ]
in the
carrier of (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)) &
[
<*x4, (
GFA0AdderOutput (x1,x2,x3))*>,
and2 ]
in the
carrier of (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)) & (
GFA0CarryOutput ((
GFA0AdderOutput (x1,x2,x3)),(
GFA0AdderOutput (x5,x6,x7)),x4))
in the
carrier of (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)) &
[
<*x5, x6*>,
xor2 ]
in the
carrier of (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)) & (
GFA0AdderOutput (x5,x6,x7))
in the
carrier of (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)) &
[
<*x5, x6*>,
and2 ]
in the
carrier of (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)) &
[
<*x6, x7*>,
and2 ]
in the
carrier of (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)) &
[
<*x7, x5*>,
and2 ]
in the
carrier of (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)) & (
GFA0CarryOutput (x5,x6,x7))
in the
carrier of (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))
proof
let x1,x2,x3,x4,x5,x6,x7 be
set;
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 (A1,A2,x4));
set A1A20 =
[
<*A1, A2*>,
xor2 ];
set A1A2 =
[
<*A1, A2*>,
and2 ];
set A2x4 =
[
<*A2, x4*>,
and2 ];
set x4A1 =
[
<*x4, A1*>,
and2 ];
set A3 = (
GFA0AdderOutput (A1,A2,x4));
set C3 = (
GFA0CarryOutput (A1,A2,x4));
A1: x1
in the
carrier of S1 & x2
in the
carrier of S1 & x3
in the
carrier of S1 & x1x20
in the
carrier of S1 & A1
in the
carrier of S1 & x1x2
in the
carrier of S1 & x2x3
in the
carrier of S1 & x3x1
in the
carrier of S1 & C1
in the
carrier of S1 & x5
in the
carrier of S1 & x6
in the
carrier of S1 & x7
in the
carrier of S1 & x5x60
in the
carrier of S1 & A2
in the
carrier of S1 & x5x6
in the
carrier of S1 & x6x7
in the
carrier of S1 & x7x5
in the
carrier of S1 & C2
in the
carrier of S1 by
ThSTC0IIS6;
x4
in the
carrier of S2 & A1A20
in the
carrier of S2 & A3
in the
carrier of S2 & A1A2
in the
carrier of S2 & A2x4
in the
carrier of S2 & x4A1
in the
carrier of S2 & C3
in the
carrier of S2 by
GFACIRC1: 36;
hence thesis by
A1,
FACIRC_1: 20;
end;
LmSTC0IS7a: for x,X1,X2,X3 be
set holds x
in ((X1
\/ X2)
\/ X3) iff x
in X1 or x
in X2 or x
in X3
proof
let x,X1,X2,X3 be
set;
set W = ((X1
\/ X2)
\/ X3);
x
in W iff (x
in (X1
\/ X2)) or x
in X3 by
XBOOLE_0:def 3;
hence thesis by
XBOOLE_0:def 3;
end;
theorem ::
WALLACE1:16
ThSTC0IS7: for x1,x2,x3,x4,x5,x6,x7 be
set holds
[
<*x1, x2*>,
xor2 ]
in (
InnerVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) & (
GFA0AdderOutput (x1,x2,x3))
in (
InnerVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) &
[
<*x1, x2*>,
and2 ]
in (
InnerVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) &
[
<*x2, x3*>,
and2 ]
in (
InnerVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) &
[
<*x3, x1*>,
and2 ]
in (
InnerVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) & (
GFA0CarryOutput (x1,x2,x3))
in (
InnerVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) &
[
<*(
GFA0AdderOutput (x1,x2,x3)), (
GFA0AdderOutput (x5,x6,x7))*>,
xor2 ]
in (
InnerVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) & (
GFA0AdderOutput ((
GFA0AdderOutput (x1,x2,x3)),(
GFA0AdderOutput (x5,x6,x7)),x4))
in (
InnerVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) &
[
<*(
GFA0AdderOutput (x1,x2,x3)), (
GFA0AdderOutput (x5,x6,x7))*>,
and2 ]
in (
InnerVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) &
[
<*(
GFA0AdderOutput (x5,x6,x7)), x4*>,
and2 ]
in (
InnerVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) &
[
<*x4, (
GFA0AdderOutput (x1,x2,x3))*>,
and2 ]
in (
InnerVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) & (
GFA0CarryOutput ((
GFA0AdderOutput (x1,x2,x3)),(
GFA0AdderOutput (x5,x6,x7)),x4))
in (
InnerVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) &
[
<*x5, x6*>,
xor2 ]
in (
InnerVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) & (
GFA0AdderOutput (x5,x6,x7))
in (
InnerVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) &
[
<*x5, x6*>,
and2 ]
in (
InnerVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) &
[
<*x6, x7*>,
and2 ]
in (
InnerVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) &
[
<*x7, x5*>,
and2 ]
in (
InnerVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) & (
GFA0CarryOutput (x5,x6,x7))
in (
InnerVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)))
proof
let x1,x2,x3,x4,x5,x6,x7 be
set;
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 (A1,A2,x4));
set A1A20 =
[
<*A1, A2*>,
xor2 ];
set A1A2 =
[
<*A1, A2*>,
and2 ];
set A2x4 =
[
<*A2, x4*>,
and2 ];
set x4A1 =
[
<*x4, A1*>,
and2 ];
set A3 = (
GFA0AdderOutput (A1,A2,x4));
set C3 = (
GFA0CarryOutput (A1,A2,x4));
set p1 =
{x1x20, A1, x1x2, x2x3, x3x1, C1};
set p2 =
{x5x60, A2, x5x6, x6x7, x7x5, C2};
set p3 =
{A1A20, A3, A1A2, A2x4, x4A1, C3};
A1: x1x20
in p1 & A1
in p1 & x1x2
in p1 & x2x3
in p1 & x3x1
in p1 & C1
in p1 by
ENUMSET1:def 4;
A2: x5x60
in p2 & A2
in p2 & x5x6
in p2 & x6x7
in p2 & x7x5
in p2 & C2
in p2 by
ENUMSET1:def 4;
A3: A1A20
in p3 & A3
in p3 & A1A2
in p3 & A2x4
in p3 & x4A1
in p3 & C3
in p3 by
ENUMSET1:def 4;
(
InnerVertices S)
= (((((
{x1x20, A1}
\/
{x1x2, x2x3, x3x1, C1})
\/
{x5x60, A2})
\/
{x5x6, x6x7, x7x5, C2})
\/
{A1A20, A3})
\/
{A1A2, A2x4, x4A1, C3}) by
ThSTC0IS1
.= ((((p1
\/
{x5x60, A2})
\/
{x5x6, x6x7, x7x5, C2})
\/
{A1A20, A3})
\/
{A1A2, A2x4, x4A1, C3}) by
ENUMSET1: 12
.= (((p1
\/ (
{x5x60, A2}
\/
{x5x6, x6x7, x7x5, C2}))
\/
{A1A20, A3})
\/
{A1A2, A2x4, x4A1, C3}) by
XBOOLE_1: 4
.= (((p1
\/ p2)
\/
{A1A20, A3})
\/
{A1A2, A2x4, x4A1, C3}) by
ENUMSET1: 12
.= ((p1
\/ (p2
\/
{A1A20, A3}))
\/
{A1A2, A2x4, x4A1, C3}) by
XBOOLE_1: 4
.= (p1
\/ ((p2
\/
{A1A20, A3})
\/
{A1A2, A2x4, x4A1, C3})) by
XBOOLE_1: 4
.= (p1
\/ (p2
\/ (
{A1A20, A3}
\/
{A1A2, A2x4, x4A1, C3}))) by
XBOOLE_1: 4
.= (p1
\/ (p2
\/
{A1A20, A3, A1A2, A2x4, x4A1, C3})) by
ENUMSET1: 12
.= ((p1
\/ p2)
\/ p3) by
XBOOLE_1: 4;
hence thesis by
A1,
A2,
A3,
LmSTC0IS7a;
end;
theorem ::
WALLACE1:17
for x1,x2,x3,x5,x6,x7 be non
pair
set holds for x4 be
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 x1
in (
InputVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) & x2
in (
InputVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) & x3
in (
InputVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) & x4
in (
InputVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) & x5
in (
InputVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) & x6
in (
InputVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) & x7
in (
InputVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)))
proof
let x1,x2,x3,x5,x6,x7 be non
pair
set;
let x4 be
set;
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 A2 = (
GFA0AdderOutput (x5,x6,x7));
set A1A20 =
[
<*A1, A2*>,
xor2 ];
set A1A2 =
[
<*A1, A2*>,
and2 ];
assume x4
<> A1A20 & x4
<> A1A2 & not x4
in (
InnerVertices S1);
then (
InputVertices S)
=
{x1, x2, x3, x4, x5, x6, x7} by
ThSTC0IS3;
hence thesis by
ENUMSET1:def 5;
end;
theorem ::
WALLACE1:18
ThSTC0IS9: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds x1
in (
InputVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) & x2
in (
InputVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) & x3
in (
InputVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) & x4
in (
InputVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) & x5
in (
InputVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) & x6
in (
InputVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) & x7
in (
InputVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)))
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
set S = (
STC0IStr (x1,x2,x3,x4,x5,x6,x7));
(
InputVertices S)
=
{x1, x2, x3, x4, x5, x6, x7} by
ThSTC0IS4;
hence thesis by
ENUMSET1:def 5;
end;
definition
let x1,x2,x3,x4,x5,x6,x7 be
set;
::
WALLACE1:def9
func
STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7) ->
Element of (
InnerVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) equals (
GFA0CarryOutput (x1,x2,x3));
coherence by
ThSTC0IS7;
::
WALLACE1:def10
func
STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7) ->
Element of (
InnerVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) equals (
GFA0CarryOutput (x5,x6,x7));
coherence by
ThSTC0IS7;
::
WALLACE1:def11
func
STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7) ->
Element of (
InnerVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) equals (
GFA0CarryOutput ((
GFA0AdderOutput (x1,x2,x3)),(
GFA0AdderOutput (x5,x6,x7)),x4));
coherence by
ThSTC0IS7;
::
WALLACE1:def12
func
STC0IAdderOutputA3 (x1,x2,x3,x4,x5,x6,x7) ->
Element of (
InnerVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7))) equals (
GFA0AdderOutput ((
GFA0AdderOutput (x1,x2,x3)),(
GFA0AdderOutput (x5,x6,x7)),x4));
coherence by
ThSTC0IS7;
end
LmSTC0IS15s2: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds for s be
State of (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7)) holds for a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN st a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7) holds ((
Following (s,2))
. (
STC0IICarryOutputC1 (x1,x2,x3,x5,x6,x7)))
= (((a1
'&' a2)
'or' (a2
'&' a3))
'or' (a3
'&' a1)) & ((
Following (s,2))
. (
STC0IICarryOutputC2 (x1,x2,x3,x5,x6,x7)))
= (((a5
'&' a6)
'or' (a6
'&' a7))
'or' (a7
'&' a5)) & ((
Following (s,2))
. (
STC0IIAdderOutputA1 (x1,x2,x3,x5,x6,x7)))
= ((a1
'xor' a2)
'xor' a3) & ((
Following (s,2))
. (
STC0IIAdderOutputA2 (x1,x2,x3,x5,x6,x7)))
= ((a5
'xor' a6)
'xor' a7) & ((
Following (s,2))
. x1)
= a1 & ((
Following (s,2))
. x2)
= a2 & ((
Following (s,2))
. x3)
= a3 & ((
Following (s,2))
. x4)
= a4 & ((
Following (s,2))
. x5)
= a5 & ((
Following (s,2))
. x6)
= a6 & ((
Following (s,2))
. x7)
= a7
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
set S = (
STC0IStr (x1,x2,x3,x4,x5,x6,x7));
set C = (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7));
set S1 = (
STC0IIStr (x1,x2,x3,x5,x6,x7));
set C1 = (
STC0IICirc (x1,x2,x3,x5,x6,x7));
set A1out = (
GFA0AdderOutput (x1,x2,x3));
set A2out = (
GFA0AdderOutput (x5,x6,x7));
set C1out = (
GFA0CarryOutput (x1,x2,x3));
set C2out = (
GFA0CarryOutput (x5,x6,x7));
set S2 = (
BitGFA0Str (A1out,A2out,x4));
set C2 = (
BitGFA0Circ (A1out,A2out,x4));
let s be
State of C;
let a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN such that
A2: a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7);
A3: x1
in (
InputVertices S) & x2
in (
InputVertices S) & x3
in (
InputVertices S) & x4
in (
InputVertices S) & x5
in (
InputVertices S) & x6
in (
InputVertices S) & x7
in (
InputVertices S) by
ThSTC0IS9;
reconsider t = s as
State of (C1
+* C2);
reconsider s1 = (s
| the
carrier of S1) as
State of C1 by
FACIRC_1: 26;
A4: (
dom s1)
= the
carrier of S1 by
CIRCUIT1: 3;
C1out
in the
carrier of S1 & C2out
in the
carrier of S1 & A1out
in the
carrier of S1 & A2out
in the
carrier of S1 & (
InputVertices S1)
misses (
InnerVertices S2) by
ThSTC0IIS6,
LmSTC0IS2b;
then
A5: ((
Following (t,2))
. C1out)
= ((
Following (s1,2))
. C1out) & ((
Following (t,2))
. C2out)
= ((
Following (s1,2))
. C2out) & ((
Following (t,2))
. A1out)
= ((
Following (s1,2))
. A1out) & ((
Following (t,2))
. A2out)
= ((
Following (s1,2))
. A2out) by
FACIRC_1: 32;
a1
= (s1
. x1) & a2
= (s1
. x2) & a3
= (s1
. x3) & a5
= (s1
. x5) & a6
= (s1
. x6) & a7
= (s1
. x7) by
ThSTC0IIS6,
A2,
A4,
FUNCT_1: 47;
hence thesis by
A2,
A3,
CIRCCMB3: 1,
A5,
ThSTC0IIS10;
end;
LmSTC0IS15C1: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds for s be
State of (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7)) holds for a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN st a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7) holds ((
Following (s,2))
. (
STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)))
= (((a1
'&' a2)
'or' (a2
'&' a3))
'or' (a3
'&' a1))
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
set C = (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7));
set S1 = (
STC0IIStr (x1,x2,x3,x5,x6,x7));
set C1 = (
STC0IICirc (x1,x2,x3,x5,x6,x7));
set A1out = (
GFA0AdderOutput (x1,x2,x3));
set A2out = (
GFA0AdderOutput (x5,x6,x7));
set S2 = (
BitGFA0Str (A1out,A2out,x4));
set C2 = (
BitGFA0Circ (A1out,A2out,x4));
set C1out = (
STC0IICarryOutputC1 (x1,x2,x3,x5,x6,x7));
let s be
State of C;
let a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN such that
A2: a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7);
reconsider t = s as
State of (C1
+* C2);
reconsider s1 = (s
| the
carrier of S1) as
State of C1 by
FACIRC_1: 26;
A3: (
dom s1)
= the
carrier of S1 by
CIRCUIT1: 3;
C1out
in the
carrier of S1 & (
InputVertices S1)
misses (
InnerVertices S2) by
LmSTC0IS2b;
then
A4: ((
Following (t,2))
. C1out)
= ((
Following (s1,2))
. C1out) by
FACIRC_1: 32;
a1
= (s1
. x1) & a2
= (s1
. x2) & a3
= (s1
. x3) & a5
= (s1
. x5) & a6
= (s1
. x6) & a7
= (s1
. x7) by
ThSTC0IIS6,
A2,
A3,
FUNCT_1: 47;
hence thesis by
A4,
ThSTC0IIS10;
end;
LmSTC0IS15C2: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds for s be
State of (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7)) holds for a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN st a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7) holds ((
Following (s,2))
. (
STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)))
= (((a5
'&' a6)
'or' (a6
'&' a7))
'or' (a7
'&' a5))
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
set C = (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7));
set S1 = (
STC0IIStr (x1,x2,x3,x5,x6,x7));
set C1 = (
STC0IICirc (x1,x2,x3,x5,x6,x7));
set A1out = (
GFA0AdderOutput (x1,x2,x3));
set A2out = (
GFA0AdderOutput (x5,x6,x7));
set S2 = (
BitGFA0Str (A1out,A2out,x4));
set C2 = (
BitGFA0Circ (A1out,A2out,x4));
set C2out = (
STC0IICarryOutputC2 (x1,x2,x3,x5,x6,x7));
let s be
State of C;
let a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN such that
A2: a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7);
reconsider t = s as
State of (C1
+* C2);
reconsider s1 = (s
| the
carrier of S1) as
State of C1 by
FACIRC_1: 26;
A3: (
dom s1)
= the
carrier of S1 by
CIRCUIT1: 3;
C2out
in the
carrier of S1 & (
InputVertices S1)
misses (
InnerVertices S2) by
LmSTC0IS2b;
then
A4: ((
Following (t,2))
. C2out)
= ((
Following (s1,2))
. C2out) by
FACIRC_1: 32;
a1
= (s1
. x1) & a2
= (s1
. x2) & a3
= (s1
. x3) & a5
= (s1
. x5) & a6
= (s1
. x6) & a7
= (s1
. x7) by
ThSTC0IIS6,
A2,
A3,
FUNCT_1: 47;
hence thesis by
A4,
ThSTC0IIS10;
end;
LmSTC0IS15C3s4: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds for s be
State of (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7)) holds for a123,a567,a4 be
Element of
BOOLEAN st a123
= (s
. (
GFA0AdderOutput (x1,x2,x3))) & a567
= (s
. (
GFA0AdderOutput (x5,x6,x7))) & a4
= (s
. x4) holds ((
Following s)
.
[
<*(
GFA0AdderOutput (x1,x2,x3)), (
GFA0AdderOutput (x5,x6,x7))*>,
and2 ])
= (a123
'&' a567) & ((
Following s)
.
[
<*(
GFA0AdderOutput (x5,x6,x7)), x4*>,
and2 ])
= (a567
'&' a4) & ((
Following s)
.
[
<*x4, (
GFA0AdderOutput (x1,x2,x3))*>,
and2 ])
= (a4
'&' a123)
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
set S = (
STC0IStr (x1,x2,x3,x4,x5,x6,x7));
set C = (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7));
set A1out = (
GFA0AdderOutput (x1,x2,x3));
set A2out = (
GFA0AdderOutput (x5,x6,x7));
set A1A2 =
[
<*A1out, A2out*>,
and2 ];
set A2x4 =
[
<*A2out, x4*>,
and2 ];
set x4A1 =
[
<*x4, A1out*>,
and2 ];
let s be
State of C;
let a123,a567,a4 be
Element of
BOOLEAN such that
A1: a123
= (s
. A1out) and
A2: a567
= (s
. A2out) and
A3: a4
= (s
. x4);
A4: (
dom s)
= the
carrier of S by
CIRCUIT1: 3;
A5: A1out
in the
carrier of S by
ThSTC0IS6;
A6: A2out
in the
carrier of S by
ThSTC0IS6;
A7: (
InnerVertices S)
= the
carrier' of S by
FACIRC_1: 37;
hence ((
Following s)
. A1A2)
= (
and2
. (s
*
<*A1out, A2out*>)) by
ThSTC0IS7,
FACIRC_1: 35
.= (
and2
.
<*a123, a567*>) by
A1,
A2,
A5,
A6,
A4,
FINSEQ_2: 125
.= (a123
'&' a567) by
FACIRC_1:def 6;
A8: x4
in the
carrier of S by
ThSTC0IS6;
thus ((
Following s)
. A2x4)
= (
and2
. (s
*
<*A2out, x4*>)) by
A7,
ThSTC0IS7,
FACIRC_1: 35
.= (
and2
.
<*a567, a4*>) by
A2,
A3,
A6,
A8,
A4,
FINSEQ_2: 125
.= (a567
'&' a4) by
FACIRC_1:def 6;
thus ((
Following s)
. x4A1)
= (
and2
. (s
*
<*x4, A1out*>)) by
A7,
ThSTC0IS7,
FACIRC_1: 35
.= (
and2
.
<*a4, a123*>) by
A3,
A1,
A8,
A5,
A4,
FINSEQ_2: 125
.= (a4
'&' a123) by
FACIRC_1:def 6;
end;
LmSTC0IS15C3s6: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds for s be
State of (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7)) holds for a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN st a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7) holds ((
Following (s,3))
.
[
<*(
GFA0AdderOutput (x1,x2,x3)), (
GFA0AdderOutput (x5,x6,x7))*>,
and2 ])
= (((a1
'xor' a2)
'xor' a3)
'&' ((a5
'xor' a6)
'xor' a7)) & ((
Following (s,3))
.
[
<*(
GFA0AdderOutput (x5,x6,x7)), x4*>,
and2 ])
= (((a5
'xor' a6)
'xor' a7)
'&' a4) & ((
Following (s,3))
.
[
<*x4, (
GFA0AdderOutput (x1,x2,x3))*>,
and2 ])
= (a4
'&' ((a1
'xor' a2)
'xor' a3)) & ((
Following (s,3))
. x1)
= a1 & ((
Following (s,3))
. x2)
= a2 & ((
Following (s,3))
. x3)
= a3 & ((
Following (s,3))
. x4)
= a4 & ((
Following (s,3))
. x5)
= a5 & ((
Following (s,3))
. x6)
= a6 & ((
Following (s,3))
. x7)
= a7
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
set S = (
STC0IStr (x1,x2,x3,x4,x5,x6,x7));
set C = (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7));
set A1out = (
GFA0AdderOutput (x1,x2,x3));
set A2out = (
GFA0AdderOutput (x5,x6,x7));
let s be
State of C;
let a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN such that
A2: a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7);
A3: x1
in (
InputVertices S) & x2
in (
InputVertices S) & x3
in (
InputVertices S) & x4
in (
InputVertices S) & x5
in (
InputVertices S) & x6
in (
InputVertices S) & x7
in (
InputVertices S) by
ThSTC0IS9;
A4: (
Following (s,(2
+ 1)))
= (
Following (
Following (s,2))) by
FACIRC_1: 12;
((
Following (s,2))
. (
STC0IIAdderOutputA1 (x1,x2,x3,x5,x6,x7)))
= ((a1
'xor' a2)
'xor' a3) & ((
Following (s,2))
. (
STC0IIAdderOutputA2 (x1,x2,x3,x5,x6,x7)))
= ((a5
'xor' a6)
'xor' a7) by
A2,
LmSTC0IS15s2;
then ((
Following (s,2))
. A1out)
= ((a1
'xor' a2)
'xor' a3) & ((
Following (s,2))
. A2out)
= ((a5
'xor' a6)
'xor' a7) & ((
Following (s,2))
. x4)
= a4 by
A2,
LmSTC0IS15s2;
hence thesis by
A2,
A3,
CIRCCMB3: 1,
A4,
LmSTC0IS15C3s4;
end;
LmSTC0IS15C3s8: for x1,x2,x3,x5,x6,x7 be non
pair
set holds for x4 be
set holds for s be
State of (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7)) holds for a123567,a567x4,ax4123 be
Element of
BOOLEAN st a123567
= (s
.
[
<*(
GFA0AdderOutput (x1,x2,x3)), (
GFA0AdderOutput (x5,x6,x7))*>,
and2 ]) & a567x4
= (s
.
[
<*(
GFA0AdderOutput (x5,x6,x7)), x4*>,
and2 ]) & ax4123
= (s
.
[
<*x4, (
GFA0AdderOutput (x1,x2,x3))*>,
and2 ]) holds ((
Following s)
. (
GFA0CarryOutput ((
GFA0AdderOutput (x1,x2,x3)),(
GFA0AdderOutput (x5,x6,x7)),x4)))
= ((a123567
'or' a567x4)
'or' ax4123)
proof
let x1,x2,x3,x5,x6,x7 be non
pair
set;
let x4 be
set;
set S = (
STC0IStr (x1,x2,x3,x4,x5,x6,x7));
set C = (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7));
set A1out = (
GFA0AdderOutput (x1,x2,x3));
set A2out = (
GFA0AdderOutput (x5,x6,x7));
set A1A2 =
[
<*A1out, A2out*>,
and2 ];
set A2x4 =
[
<*A2out, x4*>,
and2 ];
set x4A1 =
[
<*x4, A1out*>,
and2 ];
let s be
State of C;
let a123567,a567x4,ax4123 be
Element of
BOOLEAN such that
A1: a123567
= (s
. A1A2) & a567x4
= (s
. A2x4) & ax4123
= (s
. x4A1);
A2: (
dom s)
= the
carrier of S by
CIRCUIT1: 3;
A3: A1A2
in the
carrier of S & A2x4
in the
carrier of S & x4A1
in the
carrier of S by
ThSTC0IS6;
(
InnerVertices S)
= the
carrier' of S by
FACIRC_1: 37;
hence ((
Following s)
. (
GFA0CarryOutput (A1out,A2out,x4)))
= (
or3
. (s
*
<*A1A2, A2x4, x4A1*>)) by
ThSTC0IS7,
FACIRC_1: 35
.= (
or3
.
<*a123567, a567x4, ax4123*>) by
A1,
A3,
A2,
FINSEQ_2: 126
.= ((a123567
'or' a567x4)
'or' ax4123) by
FACIRC_1:def 7;
end;
LmSTC0IS15C3: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds for s be
State of (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7)) holds for a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN st a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7) holds ((
Following (s,4))
. (
STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7)))
= (((((a1
'xor' a2)
'xor' a3)
'&' ((a5
'xor' a6)
'xor' a7))
'or' (((a5
'xor' a6)
'xor' a7)
'&' a4))
'or' (a4
'&' ((a1
'xor' a2)
'xor' a3))) & ((
Following (s,4))
. x1)
= a1 & ((
Following (s,4))
. x2)
= a2 & ((
Following (s,4))
. x3)
= a3 & ((
Following (s,4))
. x4)
= a4 & ((
Following (s,4))
. x5)
= a5 & ((
Following (s,4))
. x6)
= a6 & ((
Following (s,4))
. x7)
= a7
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
set S = (
STC0IStr (x1,x2,x3,x4,x5,x6,x7));
set C = (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7));
set A1out = (
GFA0AdderOutput (x1,x2,x3));
set A2out = (
GFA0AdderOutput (x5,x6,x7));
set A1A2 =
[
<*A1out, A2out*>,
and2 ];
set A2x4 =
[
<*A2out, x4*>,
and2 ];
set x4A1 =
[
<*x4, A1out*>,
and2 ];
let s be
State of C;
let a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN such that
A2: a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7);
A3: x1
in (
InputVertices S) & x2
in (
InputVertices S) & x3
in (
InputVertices S) & x4
in (
InputVertices S) & x5
in (
InputVertices S) & x6
in (
InputVertices S) & x7
in (
InputVertices S) by
ThSTC0IS9;
A4: (
Following (s,(3
+ 1)))
= (
Following (
Following (s,3))) by
FACIRC_1: 12;
((
Following (s,3))
. A1A2)
= (((a1
'xor' a2)
'xor' a3)
'&' ((a5
'xor' a6)
'xor' a7)) & ((
Following (s,3))
. A2x4)
= (((a5
'xor' a6)
'xor' a7)
'&' a4) & ((
Following (s,3))
. x4A1)
= (a4
'&' ((a1
'xor' a2)
'xor' a3)) & ((
Following (s,3))
. x4)
= a4 by
A2,
LmSTC0IS15C3s6;
hence thesis by
A2,
A3,
CIRCCMB3: 1,
A4,
LmSTC0IS15C3s8;
end;
LmSTC0IS15A3s4: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds for s be
State of (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7)) holds for a123,a567 be
Element of
BOOLEAN st a123
= (s
. (
GFA0AdderOutput (x1,x2,x3))) & a567
= (s
. (
GFA0AdderOutput (x5,x6,x7))) holds ((
Following s)
.
[
<*(
GFA0AdderOutput (x1,x2,x3)), (
GFA0AdderOutput (x5,x6,x7))*>,
xor2 ])
= (a123
'xor' a567)
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
set S = (
STC0IStr (x1,x2,x3,x4,x5,x6,x7));
set C = (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7));
set A1out = (
GFA0AdderOutput (x1,x2,x3));
set A2out = (
GFA0AdderOutput (x5,x6,x7));
set A1A20 =
[
<*A1out, A2out*>,
xor2 ];
let s be
State of C;
let a123,a567 be
Element of
BOOLEAN such that
A1: a123
= (s
. A1out) & a567
= (s
. A2out);
A2: (
dom s)
= the
carrier of S by
CIRCUIT1: 3;
A3: A1out
in the
carrier of S & A2out
in the
carrier of S by
ThSTC0IS6;
(
InnerVertices S)
= the
carrier' of S by
FACIRC_1: 37;
hence ((
Following s)
. A1A20)
= (
xor2
. (s
*
<*A1out, A2out*>)) by
ThSTC0IS7,
FACIRC_1: 35
.= (
xor2
.
<*a123, a567*>) by
A1,
A3,
A2,
FINSEQ_2: 125
.= (a123
'xor' a567) by
FACIRC_1:def 4;
end;
LmSTC0IS15A3s6: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds for s be
State of (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7)) holds for a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN st a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7) holds ((
Following (s,3))
.
[
<*(
GFA0AdderOutput (x1,x2,x3)), (
GFA0AdderOutput (x5,x6,x7))*>,
xor2 ])
= (((a1
'xor' a2)
'xor' a3)
'xor' ((a5
'xor' a6)
'xor' a7)) & ((
Following (s,3))
. x1)
= a1 & ((
Following (s,3))
. x2)
= a2 & ((
Following (s,3))
. x3)
= a3 & ((
Following (s,3))
. x4)
= a4 & ((
Following (s,3))
. x5)
= a5 & ((
Following (s,3))
. x6)
= a6 & ((
Following (s,3))
. x7)
= a7
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
set S = (
STC0IStr (x1,x2,x3,x4,x5,x6,x7));
set C = (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7));
let s be
State of C;
let a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN such that
A2: a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7);
A3: x1
in (
InputVertices S) & x2
in (
InputVertices S) & x3
in (
InputVertices S) & x4
in (
InputVertices S) & x5
in (
InputVertices S) & x6
in (
InputVertices S) & x7
in (
InputVertices S) by
ThSTC0IS9;
A4: (
Following (s,(2
+ 1)))
= (
Following (
Following (s,2))) by
FACIRC_1: 12;
((
Following (s,2))
. (
STC0IIAdderOutputA1 (x1,x2,x3,x5,x6,x7)))
= ((a1
'xor' a2)
'xor' a3) & ((
Following (s,2))
. (
STC0IIAdderOutputA2 (x1,x2,x3,x5,x6,x7)))
= ((a5
'xor' a6)
'xor' a7) by
A2,
LmSTC0IS15s2;
hence thesis by
A2,
A3,
CIRCCMB3: 1,
A4,
LmSTC0IS15A3s4;
end;
LmSTC0IS15A3s8: for x1,x2,x3,x5,x6,x7 be non
pair
set holds for x4 be
set holds for s be
State of (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7)) holds for a123567,a4 be
Element of
BOOLEAN st a123567
= (s
.
[
<*(
GFA0AdderOutput (x1,x2,x3)), (
GFA0AdderOutput (x5,x6,x7))*>,
xor2 ]) & a4
= (s
. x4) holds ((
Following s)
. (
GFA0AdderOutput ((
GFA0AdderOutput (x1,x2,x3)),(
GFA0AdderOutput (x5,x6,x7)),x4)))
= (a123567
'xor' a4)
proof
let x1,x2,x3,x5,x6,x7 be non
pair
set;
let x4 be
set;
set S = (
STC0IStr (x1,x2,x3,x4,x5,x6,x7));
set C = (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7));
set A1out = (
GFA0AdderOutput (x1,x2,x3));
set A2out = (
GFA0AdderOutput (x5,x6,x7));
set A1A20 =
[
<*A1out, A2out*>,
xor2 ];
let s be
State of C;
let a123567,a4 be
Element of
BOOLEAN such that
A1: a123567
= (s
. A1A20) & a4
= (s
. x4);
A2: (
dom s)
= the
carrier of S by
CIRCUIT1: 3;
A3: A1A20
in the
carrier of S & x4
in the
carrier of S by
ThSTC0IS6;
(
InnerVertices S)
= the
carrier' of S by
FACIRC_1: 37;
hence ((
Following s)
. (
GFA0AdderOutput (A1out,A2out,x4)))
= (
xor2
. (s
*
<*A1A20, x4*>)) by
ThSTC0IS7,
FACIRC_1: 35
.= (
xor2
.
<*a123567, a4*>) by
A1,
A2,
A3,
FINSEQ_2: 125
.= (a123567
'xor' a4) by
FACIRC_1:def 4;
end;
LmSTC0IS15A3: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds for s be
State of (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7)) holds for a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN st a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7) holds ((
Following (s,4))
. (
STC0IAdderOutputA3 (x1,x2,x3,x4,x5,x6,x7)))
= ((((((a1
'xor' a2)
'xor' a3)
'xor' a4)
'xor' a5)
'xor' a6)
'xor' a7) & ((
Following (s,4))
. x1)
= a1 & ((
Following (s,4))
. x2)
= a2 & ((
Following (s,4))
. x3)
= a3 & ((
Following (s,4))
. x4)
= a4 & ((
Following (s,4))
. x5)
= a5 & ((
Following (s,4))
. x6)
= a6 & ((
Following (s,4))
. x7)
= a7
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
set S = (
STC0IStr (x1,x2,x3,x4,x5,x6,x7));
set C = (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7));
set A1out = (
GFA0AdderOutput (x1,x2,x3));
set A2out = (
GFA0AdderOutput (x5,x6,x7));
set A1A20 =
[
<*A1out, A2out*>,
xor2 ];
set A3out = (
STC0IAdderOutputA3 (x1,x2,x3,x4,x5,x6,x7));
let s be
State of C;
let a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN such that
A2: a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7);
A3: x1
in (
InputVertices S) & x2
in (
InputVertices S) & x3
in (
InputVertices S) & x4
in (
InputVertices S) & x5
in (
InputVertices S) & x6
in (
InputVertices S) & x7
in (
InputVertices S) by
ThSTC0IS9;
A4: (
Following (s,(3
+ 1)))
= (
Following (
Following (s,3))) by
FACIRC_1: 12;
A5: ((
Following (s,3))
. A1A20)
= (((a1
'xor' a2)
'xor' a3)
'xor' ((a5
'xor' a6)
'xor' a7)) & ((
Following (s,3))
. x4)
= a4 by
A2,
LmSTC0IS15A3s6;
((
Following (s,4))
. A3out)
= ((((a1
'xor' a2)
'xor' a3)
'xor' ((a5
'xor' a6)
'xor' a7))
'xor' a4) by
A4,
A5,
LmSTC0IS15A3s8
.= (((((a1
'xor' a2)
'xor' a3)
'xor' (a5
'xor' a6))
'xor' a7)
'xor' a4) by
XBOOLEAN: 73
.= ((((((a1
'xor' a2)
'xor' a3)
'xor' a5)
'xor' a6)
'xor' a7)
'xor' a4) by
XBOOLEAN: 73
.= ((((((a1
'xor' a2)
'xor' a3)
'xor' a5)
'xor' a6)
'xor' a4)
'xor' a7) by
XBOOLEAN: 73
.= ((((((a1
'xor' a2)
'xor' a3)
'xor' a5)
'xor' a4)
'xor' a6)
'xor' a7) by
XBOOLEAN: 73
.= ((((((a1
'xor' a2)
'xor' a3)
'xor' a4)
'xor' a5)
'xor' a6)
'xor' a7) by
XBOOLEAN: 73;
hence thesis by
A2,
A3,
CIRCCMB3: 1;
end;
theorem ::
WALLACE1:19
for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds for s be
State of (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7)) holds for a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN st a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7) holds ((
Following (s,2))
. (
STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)))
= (((a1
'&' a2)
'or' (a2
'&' a3))
'or' (a3
'&' a1)) & ((
Following (s,2))
. (
STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)))
= (((a5
'&' a6)
'or' (a6
'&' a7))
'or' (a7
'&' a5)) & ((
Following (s,4))
. (
STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7)))
= (((((a1
'xor' a2)
'xor' a3)
'&' ((a5
'xor' a6)
'xor' a7))
'or' (((a5
'xor' a6)
'xor' a7)
'&' a4))
'or' (a4
'&' ((a1
'xor' a2)
'xor' a3))) & ((
Following (s,4))
. (
STC0IAdderOutputA3 (x1,x2,x3,x4,x5,x6,x7)))
= ((((((a1
'xor' a2)
'xor' a3)
'xor' a4)
'xor' a5)
'xor' a6)
'xor' a7) & ((
Following (s,4))
. x1)
= a1 & ((
Following (s,4))
. x2)
= a2 & ((
Following (s,4))
. x3)
= a3 & ((
Following (s,4))
. x4)
= a4 & ((
Following (s,4))
. x5)
= a5 & ((
Following (s,4))
. x6)
= a6 & ((
Following (s,4))
. x7)
= a7 by
LmSTC0IS15C1,
LmSTC0IS15C2,
LmSTC0IS15C3,
LmSTC0IS15A3;
theorem ::
WALLACE1:20
ThSTC0IS18: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds for s be
State of (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7)) holds (
Following (s,4)) is
stable
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
set C = (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7));
set S1 = (
STC0IIStr (x1,x2,x3,x5,x6,x7));
set C1 = (
STC0IICirc (x1,x2,x3,x5,x6,x7));
set A1out = (
GFA0AdderOutput (x1,x2,x3));
set A2out = (
GFA0AdderOutput (x5,x6,x7));
set S2 = (
BitGFA0Str (A1out,A2out,x4));
set C2 = (
BitGFA0Circ (A1out,A2out,x4));
set n1 = 2, n2 = 2;
let s be
State of C;
C1
tolerates C2 by
CIRCCOMB: 60;
then
A2: the
Sorts of C1
tolerates the
Sorts of C2 by
CIRCCOMB:def 3;
then
reconsider s1 = (s
| the
carrier of S1) as
State of C1 by
CIRCCOMB: 26;
reconsider s2 = ((
Following (s,n1))
| the
carrier of S2) as
State of C2 by
A2,
CIRCCOMB: 26;
A3: (
InputVertices S1)
misses (
InnerVertices S2) & (
Following (s1,n1)) is
stable by
LmSTC0IS2b,
ThSTC0IIS12;
A1out
<>
[
<*A2out, x4*>,
and2 ] & A2out
<>
[
<*x4, A1out*>,
and2 ] by
LmSTC0IS1;
then (
Following (s2,n2)) is
stable by
GFACIRC1: 40;
then (
Following (s,(n1
+ n2))) is
stable by
A3,
CIRCCMB2: 19,
CIRCCOMB: 60;
hence thesis;
end;
begin
definition
let x1,x2,x3,x4,x5,x6,x7 be
set;
::
WALLACE1:def13
func
STC0Str (x1,x2,x3,x4,x5,x6,x7) ->
unsplit
gate`1=arity
gate`2isBoolean non
void
strict non
empty
ManySortedSign equals ((
STC0IStr (x1,x2,x3,x4,x5,x6,x7))
+* (
BitGFA0Str ((
STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(
STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)),(
STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7)))));
coherence ;
end
definition
let x1,x2,x3,x4,x5,x6,x7 be
set;
::
WALLACE1:def14
func
STC0Circ (x1,x2,x3,x4,x5,x6,x7) ->
strict
Boolean
gate`2=den
Circuit of (
STC0Str (x1,x2,x3,x4,x5,x6,x7)) equals ((
STC0ICirc (x1,x2,x3,x4,x5,x6,x7))
+* (
BitGFA0Circ ((
STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(
STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)),(
STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7)))));
coherence ;
end
theorem ::
WALLACE1:21
ThSTC0S1a: for x1,x2,x3,x4,x5,x6,x7 be
set holds (
InnerVertices (
STC0Str (x1,x2,x3,x4,x5,x6,x7)))
= (((
InnerVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)))
\/
{
[
<*(
STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)), (
STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7))*>,
xor2 ], (
GFA0AdderOutput ((
STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(
STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)),(
STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7))))})
\/
{
[
<*(
STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)), (
STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7))*>,
and2 ],
[
<*(
STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)), (
STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7))*>,
and2 ],
[
<*(
STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7)), (
STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7))*>,
and2 ], (
GFA0CarryOutput ((
STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(
STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)),(
STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7))))})
proof
let x1,x2,x3,x4,x5,x6,x7 be
set;
set S = (
STC0Str (x1,x2,x3,x4,x5,x6,x7));
set S1 = (
STC0IStr (x1,x2,x3,x4,x5,x6,x7));
set C1 = (
STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7));
set C2 = (
STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7));
set C3 = (
STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7));
set S2 = (
BitGFA0Str (C1,C2,C3));
set C1C2x =
[
<*C1, C2*>,
xor2 ];
set C1C2a =
[
<*C1, C2*>,
and2 ];
set C2C3a =
[
<*C2, C3*>,
and2 ];
set C3C1a =
[
<*C3, C1*>,
and2 ];
set Aout = (
GFA0AdderOutput (C1,C2,C3));
set Cout = (
GFA0CarryOutput (C1,C2,C3));
S1
tolerates S2 by
CIRCCOMB: 47;
hence (
InnerVertices S)
= ((
InnerVertices S1)
\/ (
InnerVertices S2)) by
CIRCCOMB: 11
.= ((
InnerVertices S1)
\/ (((
{C1C2x}
\/
{Aout})
\/
{C1C2a, C2C3a, C3C1a})
\/
{Cout})) by
GFACIRC1: 31
.= ((
InnerVertices S1)
\/ ((
{C1C2x, Aout}
\/
{C1C2a, C2C3a, C3C1a})
\/
{Cout})) by
ENUMSET1: 1
.= ((
InnerVertices S1)
\/ (
{C1C2x, Aout}
\/ (
{C1C2a, C2C3a, C3C1a}
\/
{Cout}))) by
XBOOLE_1: 4
.= ((
InnerVertices S1)
\/ (
{C1C2x, Aout}
\/
{C1C2a, C2C3a, C3C1a, Cout})) by
ENUMSET1: 6
.= (((
InnerVertices S1)
\/
{C1C2x, Aout})
\/
{C1C2a, C2C3a, C3C1a, Cout}) by
XBOOLE_1: 4;
end;
theorem ::
WALLACE1:22
ThSTC0S1: for x1,x2,x3,x4,x5,x6,x7 be
set holds (
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))))})
proof
let x1,x2,x3,x4,x5,x6,x7 be
set;
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 =
[
<*A1, A2*>,
xor2 ];
set A1A2 =
[
<*A1, A2*>,
and2 ];
set A2x4 =
[
<*A2, x4*>,
and2 ];
set x4A1 =
[
<*x4, A1*>,
and2 ];
set A3 = (
GFA0AdderOutput (A1,A2,x4));
set C1 = (
GFA0CarryOutput (x1,x2,x3));
set C2 = (
GFA0CarryOutput (x5,x6,x7));
set C3 = (
GFA0CarryOutput (A1,A2,x4));
set S2 = (
BitGFA0Str (C1,C2,C3));
set C1C2x =
[
<*C1, C2*>,
xor2 ];
set C1C2a =
[
<*C1, C2*>,
and2 ];
set C2C3a =
[
<*C2, C3*>,
and2 ];
set C3C1a =
[
<*C3, C1*>,
and2 ];
set Aout = (
GFA0AdderOutput (C1,C2,C3));
set Cout = (
GFA0CarryOutput (C1,C2,C3));
thus (
InnerVertices S)
= (((
InnerVertices S1)
\/
{C1C2x, Aout})
\/
{C1C2a, C2C3a, C3C1a, Cout}) by
ThSTC0S1a
.= (((((((
{x1x20, A1}
\/
{x1x2, x2x3, x3x1, C1})
\/
{x5x60, A2})
\/
{x5x6, x6x7, x7x5, C2})
\/
{A1A20, A3})
\/
{A1A2, A2x4, x4A1, C3})
\/
{C1C2x, Aout})
\/
{C1C2a, C2C3a, C3C1a, Cout}) by
ThSTC0IS1;
end;
theorem ::
WALLACE1:23
for x1,x2,x3,x4,x5,x6,x7 be
set holds (
InnerVertices (
STC0Str (x1,x2,x3,x4,x5,x6,x7))) is
Relation;
LmSTC0S1: for f1 be
Function of (2
-tuples_on
BOOLEAN ),
BOOLEAN holds for x,y,z be
set holds for a,b be
set holds (
GFA0CarryOutput (x,y,z))
<>
[
<*a, b*>, f1]
proof
let f1 be
Function of (2
-tuples_on
BOOLEAN ),
BOOLEAN ;
let x,y,z be
set, a,b be
set;
set xy =
[
<*x, y*>,
and2 ], yz =
[
<*y, z*>,
and2 ], zx =
[
<*z, x*>,
and2 ];
set A1 = (
GFA0CarryOutput (x,y,z));
A1: (A1
`1 )
=
<*xy, yz, zx*>;
(
len
<*xy, yz, zx*>)
= 3 & (
len
<*a, b*>)
= 2 by
FINSEQ_1: 44,
FINSEQ_1: 45;
hence thesis by
A1;
end;
LmSTC0S2b: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds for C1,C2,C3 be
set holds (
InputVertices (
STC0IStr (x1,x2,x3,x4,x5,x6,x7)))
misses (
InnerVertices (
BitGFA0Str (C1,C2,C3)))
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
let C1,C2,C3 be
set;
set S1 = (
STC0IStr (x1,x2,x3,x4,x5,x6,x7));
set S2 = (
BitGFA0Str (C1,C2,C3));
(
InputVertices S1) is
without_pairs & (
InnerVertices S2) is
Relation by
ThSTC0IS5;
hence thesis;
end;
theorem ::
WALLACE1:24
ThSTC0S4: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds (
InputVertices (
STC0Str (x1,x2,x3,x4,x5,x6,x7)))
=
{x1, x2, x3, x4, x5, x6, x7}
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
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 =
[
<*A1, A2*>,
xor2 ];
set A1A2 =
[
<*A1, A2*>,
and2 ];
set A2x4 =
[
<*A2, x4*>,
and2 ];
set x4A1 =
[
<*x4, A1*>,
and2 ];
set A3 = (
GFA0AdderOutput (A1,A2,x4));
set C1 = (
GFA0CarryOutput (x1,x2,x3));
set C2 = (
GFA0CarryOutput (x5,x6,x7));
set C3 = (
GFA0CarryOutput (A1,A2,x4));
set S2 = (
BitGFA0Str (C1,C2,C3));
set C1C2x =
[
<*C1, C2*>,
xor2 ];
set C1C2a =
[
<*C1, C2*>,
and2 ];
set C2C3a =
[
<*C2, C3*>,
and2 ];
set C3C1a =
[
<*C3, C1*>,
and2 ];
set Aout = (
GFA0AdderOutput (C1,C2,C3));
set Cout = (
GFA0CarryOutput (C1,C2,C3));
A2: (
InnerVertices S1)
= (((((
{x1x20, A1}
\/
{x1x2, x2x3, x3x1, C1})
\/
{x5x60, A2})
\/
{x5x6, x6x7, x7x5, C2})
\/
{A1A20, A3})
\/
{A1A2, A2x4, x4A1, C3}) by
ThSTC0IS1
.= (((((
{x1x20, A1}
\/ (
{x1x2, x2x3, x3x1}
\/
{C1}))
\/
{x5x60, A2})
\/
{x5x6, x6x7, x7x5, C2})
\/
{A1A20, A3})
\/
{A1A2, A2x4, x4A1, C3}) by
ENUMSET1: 6
.= ((((((
{x1x20, A1}
\/
{x1x2, x2x3, x3x1})
\/
{C1})
\/
{x5x60, A2})
\/
{x5x6, x6x7, x7x5, C2})
\/
{A1A20, A3})
\/
{A1A2, A2x4, x4A1, C3}) by
XBOOLE_1: 4
.= (((((
{C1}
\/ (
{x1x20, A1}
\/
{x1x2, x2x3, x3x1}))
\/
{x5x60, A2})
\/ (
{x5x6, x6x7, x7x5}
\/
{C2}))
\/
{A1A20, A3})
\/
{A1A2, A2x4, x4A1, C3}) by
ENUMSET1: 6
.= (((((
{C1}
\/
{x1x20, A1, x1x2, x2x3, x3x1})
\/
{x5x60, A2})
\/ (
{x5x6, x6x7, x7x5}
\/
{C2}))
\/
{A1A20, A3})
\/
{A1A2, A2x4, x4A1, C3}) by
ENUMSET1: 8
.= ((((((
{C1}
\/
{x1x20, A1, x1x2, x2x3, x3x1})
\/
{x5x60, A2})
\/
{x5x6, x6x7, x7x5})
\/
{C2})
\/
{A1A20, A3})
\/
{A1A2, A2x4, x4A1, C3}) by
XBOOLE_1: 4
.= (((
{C2}
\/ (((
{C1}
\/
{x1x20, A1, x1x2, x2x3, x3x1})
\/
{x5x60, A2})
\/
{x5x6, x6x7, x7x5}))
\/
{A1A20, A3})
\/ (
{A1A2, A2x4, x4A1}
\/
{C3})) by
ENUMSET1: 6
.= (((
{C2}
\/ ((
{C1}
\/
{x1x20, A1, x1x2, x2x3, x3x1})
\/ (
{x5x60, A2}
\/
{x5x6, x6x7, x7x5})))
\/
{A1A20, A3})
\/ (
{A1A2, A2x4, x4A1}
\/
{C3})) by
XBOOLE_1: 4
.= (((
{C2}
\/ ((
{C1}
\/
{x1x20, A1, x1x2, x2x3, x3x1})
\/
{x5x60, A2, x5x6, x6x7, x7x5}))
\/
{A1A20, A3})
\/ (
{A1A2, A2x4, x4A1}
\/
{C3})) by
ENUMSET1: 8
.= ((((
{C2}
\/ ((
{C1}
\/
{x1x20, A1, x1x2, x2x3, x3x1})
\/
{x5x60, A2, x5x6, x6x7, x7x5}))
\/
{A1A20, A3})
\/
{A1A2, A2x4, x4A1})
\/
{C3}) by
XBOOLE_1: 4
.= (
{C3}
\/ ((
{C2}
\/ ((
{C1}
\/
{x1x20, A1, x1x2, x2x3, x3x1})
\/
{x5x60, A2, x5x6, x6x7, x7x5}))
\/ (
{A1A20, A3}
\/
{A1A2, A2x4, x4A1}))) by
XBOOLE_1: 4
.= (
{C3}
\/ ((
{C2}
\/ ((
{C1}
\/
{x1x20, A1, x1x2, x2x3, x3x1})
\/
{x5x60, A2, x5x6, x6x7, x7x5}))
\/
{A1A20, A3, A1A2, A2x4, x4A1})) by
ENUMSET1: 8
.= (
{C3}
\/ (
{C2}
\/ (((
{C1}
\/
{x1x20, A1, x1x2, x2x3, x3x1})
\/
{x5x60, A2, x5x6, x6x7, x7x5})
\/
{A1A20, A3, A1A2, A2x4, x4A1}))) by
XBOOLE_1: 4
.= ((
{C3}
\/
{C2})
\/ (((
{C1}
\/
{x1x20, A1, x1x2, x2x3, x3x1})
\/
{x5x60, A2, x5x6, x6x7, x7x5})
\/
{A1A20, A3, A1A2, A2x4, x4A1})) by
XBOOLE_1: 4
.= (
{C3, C2}
\/ (((
{C1}
\/
{x1x20, A1, x1x2, x2x3, x3x1})
\/
{x5x60, A2, x5x6, x6x7, x7x5})
\/
{A1A20, A3, A1A2, A2x4, x4A1})) by
ENUMSET1: 1
.= (
{C3, C2}
\/ ((
{C1}
\/ (
{x1x20, A1, x1x2, x2x3, x3x1}
\/
{x5x60, A2, x5x6, x6x7, x7x5}))
\/
{A1A20, A3, A1A2, A2x4, x4A1})) by
XBOOLE_1: 4
.= (
{C3, C2}
\/ (
{C1}
\/ ((
{x1x20, A1, x1x2, x2x3, x3x1}
\/
{x5x60, A2, x5x6, x6x7, x7x5})
\/
{A1A20, A3, A1A2, A2x4, x4A1}))) by
XBOOLE_1: 4
.= ((
{C3, C2}
\/
{C1})
\/ ((
{x1x20, A1, x1x2, x2x3, x3x1}
\/
{x5x60, A2, x5x6, x6x7, x7x5})
\/
{A1A20, A3, A1A2, A2x4, x4A1})) by
XBOOLE_1: 4
.= (
{C1, C2, C3}
\/ ((
{x1x20, A1, x1x2, x2x3, x3x1}
\/
{x5x60, A2, x5x6, x6x7, x7x5})
\/
{A1A20, A3, A1A2, A2x4, x4A1})) by
ENUMSET1: 2;
A3: C3
<> C1C2x & C1
<> C2C3a & C2
<> C3C1a & C3
<> C1C2a by
LmSTC0S1;
(
InnerVertices S2) is
Relation & (
InputVertices S1) is
without_pairs by
ThSTC0IS5;
then
A5: (
InnerVertices S2)
misses (
InputVertices S1);
S1
tolerates S2 by
CIRCCOMB: 47;
hence (
InputVertices S)
= ((
InputVertices S1)
\/ ((
InputVertices S2)
\ (
InnerVertices S1))) by
A5,
FACIRC_1: 4
.= (
{x1, x2, x3, x4, x5, x6, x7}
\/ ((
InputVertices S2)
\ (
InnerVertices S1))) by
ThSTC0IS4
.= (
{x1, x2, x3, x4, x5, x6, x7}
\/ (
{C1, C2, C3}
\ (
InnerVertices S1))) by
A3,
GFACIRC1: 33
.= (
{x1, x2, x3, x4, x5, x6, x7}
\/
{} ) by
A2,
XBOOLE_1: 46
.=
{x1, x2, x3, x4, x5, x6, x7};
end;
theorem ::
WALLACE1:25
for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds (
InputVertices (
STC0Str (x1,x2,x3,x4,x5,x6,x7))) is
without_pairs
proof
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} by
ThSTC0S4;
hence thesis;
end;
theorem ::
WALLACE1:26
ThSTC0S6: for x1,x2,x3,x4,x5,x6,x7 be
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))
proof
let x1,x2,x3,x4,x5,x6,x7 be
set;
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 =
[
<*A1, A2*>,
xor2 ];
set A1A2 =
[
<*A1, A2*>,
and2 ];
set A2x4 =
[
<*A2, x4*>,
and2 ];
set x4A1 =
[
<*x4, A1*>,
and2 ];
set A3 = (
GFA0AdderOutput (A1,A2,x4));
set C1 = (
GFA0CarryOutput (x1,x2,x3));
set C2 = (
GFA0CarryOutput (x5,x6,x7));
set C3 = (
GFA0CarryOutput (A1,A2,x4));
set S2 = (
BitGFA0Str (C1,C2,C3));
set C1C2x =
[
<*C1, C2*>,
xor2 ];
set C1C2a =
[
<*C1, C2*>,
and2 ];
set C2C3a =
[
<*C2, C3*>,
and2 ];
set C3C1a =
[
<*C3, C1*>,
and2 ];
set Aout = (
GFA0AdderOutput (C1,C2,C3));
set Cout = (
GFA0CarryOutput (C1,C2,C3));
A1: x1
in the
carrier of S1 & x2
in the
carrier of S1 & x3
in the
carrier of S1 & x1x20
in the
carrier of S1 & A1
in the
carrier of S1 & x1x2
in the
carrier of S1 & x2x3
in the
carrier of S1 & x3x1
in the
carrier of S1 & C1
in the
carrier of S1 & x5
in the
carrier of S1 & x6
in the
carrier of S1 & x7
in the
carrier of S1 & x5x60
in the
carrier of S1 & A2
in the
carrier of S1 & x5x6
in the
carrier of S1 & x6x7
in the
carrier of S1 & x7x5
in the
carrier of S1 & C2
in the
carrier of S1 & x4
in the
carrier of S1 & A1A20
in the
carrier of S1 & A3
in the
carrier of S1 & A1A2
in the
carrier of S1 & A2x4
in the
carrier of S1 & x4A1
in the
carrier of S1 & C3
in the
carrier of S1 by
ThSTC0IS6;
C1C2x
in the
carrier of S2 & C1C2a
in the
carrier of S2 & C2C3a
in the
carrier of S2 & C3C1a
in the
carrier of S2 & Aout
in the
carrier of S2 & Cout
in the
carrier of S2 by
GFACIRC1: 36;
hence thesis by
A1,
FACIRC_1: 20;
end;
LmSTC0S7a: for x,X1,X2,X3,X4 be
set holds x
in (((X1
\/ X2)
\/ X3)
\/ X4) iff x
in X1 or x
in X2 or x
in X3 or x
in X4
proof
let x,X1,X2,X3,X4 be
set;
set W = (((X1
\/ X2)
\/ X3)
\/ X4);
x
in W iff (x
in ((X1
\/ X2)
\/ X3)) or x
in X4 by
XBOOLE_0:def 3;
hence thesis by
LmSTC0IS7a;
end;
theorem ::
WALLACE1:27
ThSTC0S7: for x1,x2,x3,x4,x5,x6,x7 be
set holds
[
<*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)))
proof
let x1,x2,x3,x4,x5,x6,x7 be
set;
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 =
[
<*A1, A2*>,
xor2 ];
set A1A2 =
[
<*A1, A2*>,
and2 ];
set A2x4 =
[
<*A2, x4*>,
and2 ];
set x4A1 =
[
<*x4, A1*>,
and2 ];
set A3 = (
GFA0AdderOutput (A1,A2,x4));
set C1 = (
GFA0CarryOutput (x1,x2,x3));
set C2 = (
GFA0CarryOutput (x5,x6,x7));
set C3 = (
GFA0CarryOutput (A1,A2,x4));
set S2 = (
BitGFA0Str (C1,C2,C3));
set C1C2x =
[
<*C1, C2*>,
xor2 ];
set C1C2a =
[
<*C1, C2*>,
and2 ];
set C2C3a =
[
<*C2, C3*>,
and2 ];
set C3C1a =
[
<*C3, C1*>,
and2 ];
set Aout = (
GFA0AdderOutput (C1,C2,C3));
set Cout = (
GFA0CarryOutput (C1,C2,C3));
set p1 =
{x1x20, A1, x1x2, x2x3, x3x1, C1};
set p2 =
{x5x60, A2, x5x6, x6x7, x7x5, C2};
set p3 =
{A1A20, A3, A1A2, A2x4, x4A1, C3};
set p4 =
{C1C2x, Aout, C1C2a, C2C3a, C3C1a, Cout};
A1: x1x20
in p1 & A1
in p1 & x1x2
in p1 & x2x3
in p1 & x3x1
in p1 & C1
in p1 by
ENUMSET1:def 4;
A2: x5x60
in p2 & A2
in p2 & x5x6
in p2 & x6x7
in p2 & x7x5
in p2 & C2
in p2 by
ENUMSET1:def 4;
A3: A1A20
in p3 & A3
in p3 & A1A2
in p3 & A2x4
in p3 & x4A1
in p3 & C3
in p3 by
ENUMSET1:def 4;
A4: C1C2x
in p4 & C1C2a
in p4 & C2C3a
in p4 & C3C1a
in p4 & Aout
in p4 & Cout
in p4 by
ENUMSET1:def 4;
(
InnerVertices S)
= (((((((
{x1x20, A1}
\/
{x1x2, x2x3, x3x1, C1})
\/
{x5x60, A2})
\/
{x5x6, x6x7, x7x5, C2})
\/
{A1A20, A3})
\/
{A1A2, A2x4, x4A1, C3})
\/
{C1C2x, Aout})
\/
{C1C2a, C2C3a, C3C1a, Cout}) by
ThSTC0S1
.= ((((((p1
\/
{x5x60, A2})
\/
{x5x6, x6x7, x7x5, C2})
\/
{A1A20, A3})
\/
{A1A2, A2x4, x4A1, C3})
\/
{C1C2x, Aout})
\/
{C1C2a, C2C3a, C3C1a, Cout}) by
ENUMSET1: 12
.= (((((p1
\/ (
{x5x60, A2}
\/
{x5x6, x6x7, x7x5, C2}))
\/
{A1A20, A3})
\/
{A1A2, A2x4, x4A1, C3})
\/
{C1C2x, Aout})
\/
{C1C2a, C2C3a, C3C1a, Cout}) by
XBOOLE_1: 4
.= (((((p1
\/ p2)
\/
{A1A20, A3})
\/
{A1A2, A2x4, x4A1, C3})
\/
{C1C2x, Aout})
\/
{C1C2a, C2C3a, C3C1a, Cout}) by
ENUMSET1: 12
.= ((((p1
\/ (p2
\/
{A1A20, A3}))
\/
{A1A2, A2x4, x4A1, C3})
\/
{C1C2x, Aout})
\/
{C1C2a, C2C3a, C3C1a, Cout}) by
XBOOLE_1: 4
.= (((p1
\/ ((p2
\/
{A1A20, A3})
\/
{A1A2, A2x4, x4A1, C3}))
\/
{C1C2x, Aout})
\/
{C1C2a, C2C3a, C3C1a, Cout}) by
XBOOLE_1: 4
.= (((p1
\/ (p2
\/ (
{A1A20, A3}
\/
{A1A2, A2x4, x4A1, C3})))
\/
{C1C2x, Aout})
\/
{C1C2a, C2C3a, C3C1a, Cout}) by
XBOOLE_1: 4
.= (((p1
\/ (p2
\/ p3))
\/
{C1C2x, Aout})
\/
{C1C2a, C2C3a, C3C1a, Cout}) by
ENUMSET1: 12
.= ((p1
\/ ((p2
\/ p3)
\/
{C1C2x, Aout}))
\/
{C1C2a, C2C3a, C3C1a, Cout}) by
XBOOLE_1: 4
.= (p1
\/ (((p2
\/ p3)
\/
{C1C2x, Aout})
\/
{C1C2a, C2C3a, C3C1a, Cout})) by
XBOOLE_1: 4
.= (p1
\/ ((p2
\/ p3)
\/ (
{C1C2x, Aout}
\/
{C1C2a, C2C3a, C3C1a, Cout}))) by
XBOOLE_1: 4
.= (p1
\/ ((p2
\/ p3)
\/ p4)) by
ENUMSET1: 12
.= ((p1
\/ (p2
\/ p3))
\/ p4) by
XBOOLE_1: 4
.= (((p1
\/ p2)
\/ p3)
\/ p4) by
XBOOLE_1: 4;
hence thesis by
A1,
A2,
A3,
A4,
LmSTC0S7a;
end;
theorem ::
WALLACE1:28
ThSTC0S9: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds x1
in (
InputVertices (
STC0Str (x1,x2,x3,x4,x5,x6,x7))) & x2
in (
InputVertices (
STC0Str (x1,x2,x3,x4,x5,x6,x7))) & x3
in (
InputVertices (
STC0Str (x1,x2,x3,x4,x5,x6,x7))) & x4
in (
InputVertices (
STC0Str (x1,x2,x3,x4,x5,x6,x7))) & x5
in (
InputVertices (
STC0Str (x1,x2,x3,x4,x5,x6,x7))) & x6
in (
InputVertices (
STC0Str (x1,x2,x3,x4,x5,x6,x7))) & x7
in (
InputVertices (
STC0Str (x1,x2,x3,x4,x5,x6,x7)))
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
set S = (
STC0Str (x1,x2,x3,x4,x5,x6,x7));
(
InputVertices S)
=
{x1, x2, x3, x4, x5, x6, x7} by
ThSTC0S4;
hence thesis by
ENUMSET1:def 5;
end;
definition
let x1,x2,x3,x4,x5,x6,x7 be
set;
::
WALLACE1:def15
func
STC0OutputS0 (x1,x2,x3,x4,x5,x6,x7) ->
Element of (
InnerVertices (
STC0Str (x1,x2,x3,x4,x5,x6,x7))) equals (
GFA0AdderOutput ((
GFA0AdderOutput (x1,x2,x3)),(
GFA0AdderOutput (x5,x6,x7)),x4));
coherence by
ThSTC0S7;
::
WALLACE1:def16
func
STC0OutputS1 (x1,x2,x3,x4,x5,x6,x7) ->
Element of (
InnerVertices (
STC0Str (x1,x2,x3,x4,x5,x6,x7))) equals (
GFA0AdderOutput ((
GFA0CarryOutput (x1,x2,x3)),(
GFA0CarryOutput (x5,x6,x7)),(
GFA0CarryOutput ((
GFA0AdderOutput (x1,x2,x3)),(
GFA0AdderOutput (x5,x6,x7)),x4))));
coherence by
ThSTC0S7;
::
WALLACE1:def17
func
STC0OutputS2 (x1,x2,x3,x4,x5,x6,x7) ->
Element of (
InnerVertices (
STC0Str (x1,x2,x3,x4,x5,x6,x7))) equals (
GFA0CarryOutput ((
GFA0CarryOutput (x1,x2,x3)),(
GFA0CarryOutput (x5,x6,x7)),(
GFA0CarryOutput ((
GFA0AdderOutput (x1,x2,x3)),(
GFA0AdderOutput (x5,x6,x7)),x4))));
coherence by
ThSTC0S7;
end
LmSTC0S15s0: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds for s be
State of (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7)) holds for a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN st a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7) holds ((
Following (s,4))
. (
STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)))
= (((a1
'&' a2)
'or' (a2
'&' a3))
'or' (a3
'&' a1)) & ((
Following (s,4))
. (
STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)))
= (((a5
'&' a6)
'or' (a6
'&' a7))
'or' (a7
'&' a5))
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
set C = (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7));
set S1 = (
STC0IIStr (x1,x2,x3,x5,x6,x7));
set C1 = (
STC0IICirc (x1,x2,x3,x5,x6,x7));
set A1out = (
GFA0AdderOutput (x1,x2,x3));
set A2out = (
GFA0AdderOutput (x5,x6,x7));
set S2 = (
BitGFA0Str (A1out,A2out,x4));
set C2 = (
BitGFA0Circ (A1out,A2out,x4));
set C1out = (
STC0IICarryOutputC1 (x1,x2,x3,x5,x6,x7));
set C2out = (
STC0IICarryOutputC2 (x1,x2,x3,x5,x6,x7));
set n1 = 2, n2 = 4;
let s be
State of C;
let a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN such that
A2: a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7);
reconsider t = s as
State of (C1
+* C2);
reconsider s1 = (s
| the
carrier of S1) as
State of C1 by
FACIRC_1: 26;
A3: (
dom s1)
= the
carrier of S1 by
CIRCUIT1: 3;
A4: (
Following (s1,n2))
= (
Following (s1,n1)) by
ThSTC0IIS12,
CIRCCMB2: 4;
C1out
in the
carrier of S1 & C2out
in the
carrier of S1 & (
InputVertices S1)
misses (
InnerVertices S2) by
LmSTC0IS2b;
then
A5: ((
Following (t,n2))
. C1out)
= ((
Following (s1,n1))
. C1out) & ((
Following (t,n2))
. C2out)
= ((
Following (s1,n1))
. C2out) by
A4,
FACIRC_1: 32;
a1
= (s1
. x1) & a2
= (s1
. x2) & a3
= (s1
. x3) & a5
= (s1
. x5) & a6
= (s1
. x6) & a7
= (s1
. x7) by
ThSTC0IIS6,
A2,
A3,
FUNCT_1: 47;
hence thesis by
A5,
ThSTC0IIS10;
end;
LmSTC0S15s4a: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds for s be
State of (
STC0Circ (x1,x2,x3,x4,x5,x6,x7)) holds for a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN st a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7) holds ((
Following (s,4))
. (
STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)))
= (((a1
'&' a2)
'or' (a2
'&' a3))
'or' (a3
'&' a1)) & ((
Following (s,4))
. (
STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)))
= (((a5
'&' a6)
'or' (a6
'&' a7))
'or' (a7
'&' a5)) & ((
Following (s,4))
. x1)
= a1 & ((
Following (s,4))
. x2)
= a2 & ((
Following (s,4))
. x3)
= a3 & ((
Following (s,4))
. x4)
= a4 & ((
Following (s,4))
. x5)
= a5 & ((
Following (s,4))
. x6)
= a6 & ((
Following (s,4))
. x7)
= a7
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
set S = (
STC0Str (x1,x2,x3,x4,x5,x6,x7));
set C = (
STC0Circ (x1,x2,x3,x4,x5,x6,x7));
set S1 = (
STC0IStr (x1,x2,x3,x4,x5,x6,x7));
set C1 = (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7));
set A1out = (
GFA0AdderOutput (x1,x2,x3));
set A2out = (
GFA0AdderOutput (x5,x6,x7));
set C1out = (
GFA0CarryOutput (x1,x2,x3));
set C2out = (
GFA0CarryOutput (x5,x6,x7));
set C3out = (
GFA0CarryOutput (A1out,A2out,x4));
set S2 = (
BitGFA0Str (C1out,C2out,C3out));
set C2 = (
BitGFA0Circ (C1out,C2out,C3out));
let s be
State of C;
let a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN such that
A2: a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7);
A3: x1
in (
InputVertices S) & x2
in (
InputVertices S) & x3
in (
InputVertices S) & x4
in (
InputVertices S) & x5
in (
InputVertices S) & x6
in (
InputVertices S) & x7
in (
InputVertices S) by
ThSTC0S9;
reconsider t = s as
State of (C1
+* C2);
reconsider s1 = (s
| the
carrier of S1) as
State of C1 by
FACIRC_1: 26;
A4: (
dom s1)
= the
carrier of S1 by
CIRCUIT1: 3;
C1out
in the
carrier of S1 & C2out
in the
carrier of S1 & (
InputVertices S1)
misses (
InnerVertices S2) by
ThSTC0IS6,
LmSTC0S2b;
then
A5: ((
Following (t,4))
. C1out)
= ((
Following (s1,4))
. C1out) & ((
Following (t,4))
. C2out)
= ((
Following (s1,4))
. C2out) by
FACIRC_1: 32;
a1
= (s1
. x1) & a2
= (s1
. x2) & a3
= (s1
. x3) & a4
= (s1
. x4) & a5
= (s1
. x5) & a6
= (s1
. x6) & a7
= (s1
. x7) by
ThSTC0IS6,
A2,
A4,
FUNCT_1: 47;
hence thesis by
A2,
A3,
CIRCCMB3: 1,
A5,
LmSTC0S15s0;
end;
LmSTC0S15s4b: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds for s be
State of (
STC0Circ (x1,x2,x3,x4,x5,x6,x7)) holds for a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN st a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7) holds ((
Following (s,4))
. (
STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7)))
= (((((a1
'xor' a2)
'xor' a3)
'&' ((a5
'xor' a6)
'xor' a7))
'or' (((a5
'xor' a6)
'xor' a7)
'&' a4))
'or' (a4
'&' ((a1
'xor' a2)
'xor' a3))) & ((
Following (s,4))
. (
STC0IAdderOutputA3 (x1,x2,x3,x4,x5,x6,x7)))
= ((((((a1
'xor' a2)
'xor' a3)
'xor' a4)
'xor' a5)
'xor' a6)
'xor' a7) & ((
Following (s,4))
. x1)
= a1 & ((
Following (s,4))
. x2)
= a2 & ((
Following (s,4))
. x3)
= a3 & ((
Following (s,4))
. x4)
= a4 & ((
Following (s,4))
. x5)
= a5 & ((
Following (s,4))
. x6)
= a6 & ((
Following (s,4))
. x7)
= a7
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
set S = (
STC0Str (x1,x2,x3,x4,x5,x6,x7));
set C = (
STC0Circ (x1,x2,x3,x4,x5,x6,x7));
set S1 = (
STC0IStr (x1,x2,x3,x4,x5,x6,x7));
set C1 = (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7));
set A1out = (
GFA0AdderOutput (x1,x2,x3));
set A2out = (
GFA0AdderOutput (x5,x6,x7));
set A3out = (
GFA0AdderOutput (A1out,A2out,x4));
set C1out = (
GFA0CarryOutput (x1,x2,x3));
set C2out = (
GFA0CarryOutput (x5,x6,x7));
set C3out = (
GFA0CarryOutput (A1out,A2out,x4));
set S2 = (
BitGFA0Str (C1out,C2out,C3out));
set C2 = (
BitGFA0Circ (C1out,C2out,C3out));
let s be
State of C;
let a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN such that
A2: a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7);
A3: x1
in (
InputVertices S) & x2
in (
InputVertices S) & x3
in (
InputVertices S) & x4
in (
InputVertices S) & x5
in (
InputVertices S) & x6
in (
InputVertices S) & x7
in (
InputVertices S) by
ThSTC0S9;
reconsider t = s as
State of (C1
+* C2);
reconsider s1 = (s
| the
carrier of S1) as
State of C1 by
FACIRC_1: 26;
A4: (
dom s1)
= the
carrier of S1 by
CIRCUIT1: 3;
C3out
in the
carrier of S1 & A3out
in the
carrier of S1 & (
InputVertices S1)
misses (
InnerVertices S2) by
ThSTC0IS6,
LmSTC0S2b;
then
A5: ((
Following (t,4))
. C3out)
= ((
Following (s1,4))
. C3out) & ((
Following (t,4))
. A3out)
= ((
Following (s1,4))
. A3out) by
FACIRC_1: 32;
a1
= (s1
. x1) & a2
= (s1
. x2) & a3
= (s1
. x3) & a4
= (s1
. x4) & a5
= (s1
. x5) & a6
= (s1
. x6) & a7
= (s1
. x7) by
ThSTC0IS6,
A2,
A4,
FUNCT_1: 47;
hence thesis by
A2,
A3,
CIRCCMB3: 1,
A5,
LmSTC0IS15C3,
LmSTC0IS15A3;
end;
LmSTC0S15S0: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds for s be
State of (
STC0Circ (x1,x2,x3,x4,x5,x6,x7)) holds for a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN st a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7) holds ((
Following (s,4))
. (
STC0OutputS0 (x1,x2,x3,x4,x5,x6,x7)))
= ((((((a1
'xor' a2)
'xor' a3)
'xor' a4)
'xor' a5)
'xor' a6)
'xor' a7)
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
set A1out = (
GFA0AdderOutput (x1,x2,x3));
set A2out = (
GFA0AdderOutput (x5,x6,x7));
set A3out = (
GFA0AdderOutput (A1out,A2out,x4));
A3out
= (
STC0IAdderOutputA3 (x1,x2,x3,x4,x5,x6,x7)) & A3out
= (
STC0OutputS0 (x1,x2,x3,x4,x5,x6,x7));
hence thesis by
LmSTC0S15s4b;
end;
LmSTC0S15S1s4: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds for s be
State of (
STC0Circ (x1,x2,x3,x4,x5,x6,x7)) holds for aC1,aC2 be
Element of
BOOLEAN st aC1
= (s
. (
GFA0CarryOutput (x1,x2,x3))) & aC2
= (s
. (
GFA0CarryOutput (x5,x6,x7))) holds ((
Following s)
.
[
<*(
GFA0CarryOutput (x1,x2,x3)), (
GFA0CarryOutput (x5,x6,x7))*>,
xor2 ])
= (aC1
'xor' aC2)
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
set S = (
STC0Str (x1,x2,x3,x4,x5,x6,x7));
set C = (
STC0Circ (x1,x2,x3,x4,x5,x6,x7));
set C1out = (
GFA0CarryOutput (x1,x2,x3));
set C2out = (
GFA0CarryOutput (x5,x6,x7));
set C1C2x =
[
<*C1out, C2out*>,
xor2 ];
let s be
State of C;
let aC1,aC2 be
Element of
BOOLEAN such that
A1: aC1
= (s
. C1out) & aC2
= (s
. C2out);
A2: (
dom s)
= the
carrier of S by
CIRCUIT1: 3;
A3: C1out
in the
carrier of S & C2out
in the
carrier of S by
ThSTC0S6;
(
InnerVertices S)
= the
carrier' of S by
FACIRC_1: 37;
hence ((
Following s)
. C1C2x)
= (
xor2
. (s
*
<*C1out, C2out*>)) by
ThSTC0S7,
FACIRC_1: 35
.= (
xor2
.
<*aC1, aC2*>) by
A1,
A2,
A3,
FINSEQ_2: 125
.= (aC1
'xor' aC2) by
FACIRC_1:def 4;
end;
LmSTC0S15S1s6a: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds for s be
State of (
STC0Circ (x1,x2,x3,x4,x5,x6,x7)) holds for a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN st a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7) holds ((
Following (s,5))
.
[
<*(
GFA0CarryOutput (x1,x2,x3)), (
GFA0CarryOutput (x5,x6,x7))*>,
xor2 ])
= ((((a1
'&' a2)
'or' (a2
'&' a3))
'or' (a3
'&' a1))
'xor' (((a5
'&' a6)
'or' (a6
'&' a7))
'or' (a7
'&' a5)))
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
set C = (
STC0Circ (x1,x2,x3,x4,x5,x6,x7));
set C1out = (
GFA0CarryOutput (x1,x2,x3));
set C2out = (
GFA0CarryOutput (x5,x6,x7));
set C1C2x =
[
<*C1out, C2out*>,
xor2 ];
let s be
State of C;
let a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN such that
A2: a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7);
A5: ((
Following (s,4))
. C1out)
= (((a1
'&' a2)
'or' (a2
'&' a3))
'or' (a3
'&' a1)) & ((
Following (s,4))
. C2out)
= (((a5
'&' a6)
'or' (a6
'&' a7))
'or' (a7
'&' a5)) by
A2,
LmSTC0S15s4a;
(
Following (s,(4
+ 1)))
= (
Following (
Following (s,4))) by
FACIRC_1: 12;
hence thesis by
A5,
LmSTC0S15S1s4;
end;
LmSTC0S15S1s6b: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds for s be
State of (
STC0Circ (x1,x2,x3,x4,x5,x6,x7)) holds for a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN st a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7) holds ((
Following (s,5))
. (
GFA0CarryOutput ((
GFA0AdderOutput (x1,x2,x3)),(
GFA0AdderOutput (x5,x6,x7)),x4)))
= (((((a1
'xor' a2)
'xor' a3)
'&' ((a5
'xor' a6)
'xor' a7))
'or' (((a5
'xor' a6)
'xor' a7)
'&' a4))
'or' (a4
'&' ((a1
'xor' a2)
'xor' a3)))
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
set S = (
STC0Str (x1,x2,x3,x4,x5,x6,x7));
set C = (
STC0Circ (x1,x2,x3,x4,x5,x6,x7));
set S1 = (
STC0IStr (x1,x2,x3,x4,x5,x6,x7));
set C1 = (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7));
set A1out = (
GFA0AdderOutput (x1,x2,x3));
set A2out = (
GFA0AdderOutput (x5,x6,x7));
set C1out = (
GFA0CarryOutput (x1,x2,x3));
set C2out = (
GFA0CarryOutput (x5,x6,x7));
set C3out = (
GFA0CarryOutput (A1out,A2out,x4));
set S2 = (
BitGFA0Str (C1out,C2out,C3out));
set C2 = (
BitGFA0Circ (C1out,C2out,C3out));
set n1 = 4, n2 = 5;
let s be
State of C;
let a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN such that
A2: a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7);
reconsider t = s as
State of (C1
+* C2);
reconsider s1 = (s
| the
carrier of S1) as
State of C1 by
FACIRC_1: 26;
A3: (
dom s1)
= the
carrier of S1 by
CIRCUIT1: 3;
A4: (
Following (s1,n2))
= (
Following (s1,n1)) by
ThSTC0IS18,
CIRCCMB2: 4;
C3out
in the
carrier of S1 & (
InputVertices S1)
misses (
InnerVertices S2) by
ThSTC0IS6,
LmSTC0S2b;
then
A5: ((
Following (t,n2))
. C3out)
= ((
Following (s1,n1))
. C3out) by
A4,
FACIRC_1: 32;
a1
= (s1
. x1) & a2
= (s1
. x2) & a3
= (s1
. x3) & a4
= (s1
. x4) & a5
= (s1
. x5) & a6
= (s1
. x6) & a7
= (s1
. x7) by
ThSTC0IS6,
A2,
A3,
FUNCT_1: 47;
hence thesis by
A5,
LmSTC0IS15C3;
end;
LmSTC0S15S1s8: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds for s be
State of (
STC0Circ (x1,x2,x3,x4,x5,x6,x7)) holds for aC1C2x,aC3 be
Element of
BOOLEAN st aC1C2x
= (s
.
[
<*(
GFA0CarryOutput (x1,x2,x3)), (
GFA0CarryOutput (x5,x6,x7))*>,
xor2 ]) & aC3
= (s
. (
GFA0CarryOutput ((
GFA0AdderOutput (x1,x2,x3)),(
GFA0AdderOutput (x5,x6,x7)),x4))) holds ((
Following s)
. (
GFA0AdderOutput ((
GFA0CarryOutput (x1,x2,x3)),(
GFA0CarryOutput (x5,x6,x7)),(
GFA0CarryOutput ((
GFA0AdderOutput (x1,x2,x3)),(
GFA0AdderOutput (x5,x6,x7)),x4)))))
= (aC1C2x
'xor' aC3)
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
set S = (
STC0Str (x1,x2,x3,x4,x5,x6,x7));
set C = (
STC0Circ (x1,x2,x3,x4,x5,x6,x7));
set A1out = (
GFA0AdderOutput (x1,x2,x3));
set A2out = (
GFA0AdderOutput (x5,x6,x7));
set C1out = (
GFA0CarryOutput (x1,x2,x3));
set C2out = (
GFA0CarryOutput (x5,x6,x7));
set C3out = (
GFA0CarryOutput (A1out,A2out,x4));
set C1C2x =
[
<*C1out, C2out*>,
xor2 ];
let s be
State of C;
let aC1C2x,aC3 be
Element of
BOOLEAN such that
A1: aC1C2x
= (s
. C1C2x) & aC3
= (s
. C3out);
A2: (
dom s)
= the
carrier of S by
CIRCUIT1: 3;
A3: C1C2x
in the
carrier of S & C3out
in the
carrier of S by
ThSTC0S6;
(
InnerVertices S)
= the
carrier' of S by
FACIRC_1: 37;
hence ((
Following s)
. (
GFA0AdderOutput (C1out,C2out,C3out)))
= (
xor2
. (s
*
<*C1C2x, C3out*>)) by
ThSTC0S7,
FACIRC_1: 35
.= (
xor2
.
<*aC1C2x, aC3*>) by
A1,
A2,
A3,
FINSEQ_2: 125
.= (aC1C2x
'xor' aC3) by
FACIRC_1:def 4;
end;
LmSTC0S15S1: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds for s be
State of (
STC0Circ (x1,x2,x3,x4,x5,x6,x7)) holds for a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN st a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7) holds ((
Following (s,6))
. (
STC0OutputS1 (x1,x2,x3,x4,x5,x6,x7)))
= (((((a1
'&' a2)
'or' (a2
'&' a3))
'or' (a3
'&' a1))
'xor' (((a5
'&' a6)
'or' (a6
'&' a7))
'or' (a7
'&' a5)))
'xor' (((((a1
'xor' a2)
'xor' a3)
'&' ((a5
'xor' a6)
'xor' a7))
'or' (((a5
'xor' a6)
'xor' a7)
'&' a4))
'or' (a4
'&' ((a1
'xor' a2)
'xor' a3)))) & ((
Following (s,6))
. x1)
= a1 & ((
Following (s,6))
. x2)
= a2 & ((
Following (s,6))
. x3)
= a3 & ((
Following (s,6))
. x4)
= a4 & ((
Following (s,6))
. x5)
= a5 & ((
Following (s,6))
. x6)
= a6 & ((
Following (s,6))
. x7)
= a7
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
set S = (
STC0Str (x1,x2,x3,x4,x5,x6,x7));
set C = (
STC0Circ (x1,x2,x3,x4,x5,x6,x7));
set A1out = (
GFA0AdderOutput (x1,x2,x3));
set A2out = (
GFA0AdderOutput (x5,x6,x7));
set C1out = (
GFA0CarryOutput (x1,x2,x3));
set C2out = (
GFA0CarryOutput (x5,x6,x7));
set C3out = (
GFA0CarryOutput (A1out,A2out,x4));
set C1C2x =
[
<*C1out, C2out*>,
xor2 ];
set S1out = (
STC0OutputS1 (x1,x2,x3,x4,x5,x6,x7));
let s be
State of C;
let a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN such that
A2: a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7);
A3: x1
in (
InputVertices S) & x2
in (
InputVertices S) & x3
in (
InputVertices S) & x4
in (
InputVertices S) & x5
in (
InputVertices S) & x6
in (
InputVertices S) & x7
in (
InputVertices S) by
ThSTC0S9;
A5: ((
Following (s,5))
. C1C2x)
= ((((a1
'&' a2)
'or' (a2
'&' a3))
'or' (a3
'&' a1))
'xor' (((a5
'&' a6)
'or' (a6
'&' a7))
'or' (a7
'&' a5))) & ((
Following (s,5))
. C3out)
= (((((a1
'xor' a2)
'xor' a3)
'&' ((a5
'xor' a6)
'xor' a7))
'or' (((a5
'xor' a6)
'xor' a7)
'&' a4))
'or' (a4
'&' ((a1
'xor' a2)
'xor' a3))) by
A2,
LmSTC0S15S1s6a,
LmSTC0S15S1s6b;
(
Following (s,(5
+ 1)))
= (
Following (
Following (s,5))) by
FACIRC_1: 12;
hence thesis by
A2,
A3,
CIRCCMB3: 1,
A5,
LmSTC0S15S1s8;
end;
LmSTC0S15S2s4: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds for s be
State of (
STC0Circ (x1,x2,x3,x4,x5,x6,x7)) holds for aC1,aC2,aC3 be
Element of
BOOLEAN st aC1
= (s
. (
GFA0CarryOutput (x1,x2,x3))) & aC2
= (s
. (
GFA0CarryOutput (x5,x6,x7))) & aC3
= (s
. (
GFA0CarryOutput ((
GFA0AdderOutput (x1,x2,x3)),(
GFA0AdderOutput (x5,x6,x7)),x4))) holds ((
Following s)
.
[
<*(
GFA0CarryOutput (x1,x2,x3)), (
GFA0CarryOutput (x5,x6,x7))*>,
and2 ])
= (aC1
'&' aC2) & ((
Following s)
.
[
<*(
GFA0CarryOutput (x5,x6,x7)), (
GFA0CarryOutput ((
GFA0AdderOutput (x1,x2,x3)),(
GFA0AdderOutput (x5,x6,x7)),x4))*>,
and2 ])
= (aC2
'&' aC3) & ((
Following s)
.
[
<*(
GFA0CarryOutput ((
GFA0AdderOutput (x1,x2,x3)),(
GFA0AdderOutput (x5,x6,x7)),x4)), (
GFA0CarryOutput (x1,x2,x3))*>,
and2 ])
= (aC3
'&' aC1)
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
set S = (
STC0Str (x1,x2,x3,x4,x5,x6,x7));
set C = (
STC0Circ (x1,x2,x3,x4,x5,x6,x7));
set A1out = (
GFA0AdderOutput (x1,x2,x3));
set A2out = (
GFA0AdderOutput (x5,x6,x7));
set C1out = (
GFA0CarryOutput (x1,x2,x3));
set C2out = (
GFA0CarryOutput (x5,x6,x7));
set C3out = (
GFA0CarryOutput (A1out,A2out,x4));
set C1C2a =
[
<*C1out, C2out*>,
and2 ];
set C2C3a =
[
<*C2out, C3out*>,
and2 ];
set C3C1a =
[
<*C3out, C1out*>,
and2 ];
let s be
State of C;
let aC1,aC2,aC3 be
Element of
BOOLEAN such that
A1: aC1
= (s
. C1out) & aC2
= (s
. C2out) & aC3
= (s
. C3out);
A2: (
dom s)
= the
carrier of S by
CIRCUIT1: 3;
A3: C1out
in the
carrier of S & C2out
in the
carrier of S & C3out
in the
carrier of S by
ThSTC0S6;
A4: (
InnerVertices S)
= the
carrier' of S by
FACIRC_1: 37;
hence ((
Following s)
. C1C2a)
= (
and2
. (s
*
<*C1out, C2out*>)) by
ThSTC0S7,
FACIRC_1: 35
.= (
and2
.
<*aC1, aC2*>) by
A1,
A2,
A3,
FINSEQ_2: 125
.= (aC1
'&' aC2) by
FACIRC_1:def 6;
A6: ((
Following s)
. C2C3a)
= (
and2
. (s
*
<*C2out, C3out*>)) by
A4,
ThSTC0S7,
FACIRC_1: 35
.= (
and2
.
<*aC2, aC3*>) by
A1,
A2,
A3,
FINSEQ_2: 125
.= (aC2
'&' aC3) by
FACIRC_1:def 6;
((
Following s)
. C3C1a)
= (
and2
. (s
*
<*C3out, C1out*>)) by
A4,
ThSTC0S7,
FACIRC_1: 35
.= (
and2
.
<*aC3, aC1*>) by
A1,
A2,
A3,
FINSEQ_2: 125
.= (aC3
'&' aC1) by
FACIRC_1:def 6;
hence thesis by
A6;
end;
LmSTC0S15S2s6: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds for s be
State of (
STC0Circ (x1,x2,x3,x4,x5,x6,x7)) holds for a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN st a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7) holds ((
Following (s,5))
.
[
<*(
GFA0CarryOutput (x1,x2,x3)), (
GFA0CarryOutput (x5,x6,x7))*>,
and2 ])
= ((((a1
'&' a2)
'or' (a2
'&' a3))
'or' (a3
'&' a1))
'&' (((a5
'&' a6)
'or' (a6
'&' a7))
'or' (a7
'&' a5))) & ((
Following (s,5))
.
[
<*(
GFA0CarryOutput (x5,x6,x7)), (
GFA0CarryOutput ((
GFA0AdderOutput (x1,x2,x3)),(
GFA0AdderOutput (x5,x6,x7)),x4))*>,
and2 ])
= ((((a5
'&' a6)
'or' (a6
'&' a7))
'or' (a7
'&' a5))
'&' (((((a1
'xor' a2)
'xor' a3)
'&' ((a5
'xor' a6)
'xor' a7))
'or' (((a5
'xor' a6)
'xor' a7)
'&' a4))
'or' (a4
'&' ((a1
'xor' a2)
'xor' a3)))) & ((
Following (s,5))
.
[
<*(
GFA0CarryOutput ((
GFA0AdderOutput (x1,x2,x3)),(
GFA0AdderOutput (x5,x6,x7)),x4)), (
GFA0CarryOutput (x1,x2,x3))*>,
and2 ])
= ((((((a1
'xor' a2)
'xor' a3)
'&' ((a5
'xor' a6)
'xor' a7))
'or' (((a5
'xor' a6)
'xor' a7)
'&' a4))
'or' (a4
'&' ((a1
'xor' a2)
'xor' a3)))
'&' (((a1
'&' a2)
'or' (a2
'&' a3))
'or' (a3
'&' a1)))
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
set S = (
STC0Str (x1,x2,x3,x4,x5,x6,x7));
set C = (
STC0Circ (x1,x2,x3,x4,x5,x6,x7));
set A1out = (
GFA0AdderOutput (x1,x2,x3));
set A2out = (
GFA0AdderOutput (x5,x6,x7));
set C1out = (
GFA0CarryOutput (x1,x2,x3));
set C2out = (
GFA0CarryOutput (x5,x6,x7));
set C3out = (
GFA0CarryOutput (A1out,A2out,x4));
set C1C2a =
[
<*C1out, C2out*>,
and2 ];
set C2C3a =
[
<*C2out, C3out*>,
and2 ];
set C3C1a =
[
<*C3out, C1out*>,
and2 ];
let s be
State of C;
let a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN such that
A2: a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7);
A5: ((
Following (s,4))
. C1out)
= (((a1
'&' a2)
'or' (a2
'&' a3))
'or' (a3
'&' a1)) & ((
Following (s,4))
. C2out)
= (((a5
'&' a6)
'or' (a6
'&' a7))
'or' (a7
'&' a5)) & ((
Following (s,4))
. C3out)
= (((((a1
'xor' a2)
'xor' a3)
'&' ((a5
'xor' a6)
'xor' a7))
'or' (((a5
'xor' a6)
'xor' a7)
'&' a4))
'or' (a4
'&' ((a1
'xor' a2)
'xor' a3))) by
A2,
LmSTC0S15s4a,
LmSTC0S15s4b;
(
Following (s,(4
+ 1)))
= (
Following (
Following (s,4))) by
FACIRC_1: 12;
hence thesis by
A5,
LmSTC0S15S2s4;
end;
LmSTC0S15S2s8: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds for s be
State of (
STC0Circ (x1,x2,x3,x4,x5,x6,x7)) holds for aC1C2a,aC2C3a,aC3C1a be
Element of
BOOLEAN st aC1C2a
= (s
.
[
<*(
GFA0CarryOutput (x1,x2,x3)), (
GFA0CarryOutput (x5,x6,x7))*>,
and2 ]) & aC2C3a
= (s
.
[
<*(
GFA0CarryOutput (x5,x6,x7)), (
GFA0CarryOutput ((
GFA0AdderOutput (x1,x2,x3)),(
GFA0AdderOutput (x5,x6,x7)),x4))*>,
and2 ]) & aC3C1a
= (s
.
[
<*(
GFA0CarryOutput ((
GFA0AdderOutput (x1,x2,x3)),(
GFA0AdderOutput (x5,x6,x7)),x4)), (
GFA0CarryOutput (x1,x2,x3))*>,
and2 ]) holds ((
Following s)
. (
GFA0CarryOutput ((
GFA0CarryOutput (x1,x2,x3)),(
GFA0CarryOutput (x5,x6,x7)),(
GFA0CarryOutput ((
GFA0AdderOutput (x1,x2,x3)),(
GFA0AdderOutput (x5,x6,x7)),x4)))))
= ((aC1C2a
'or' aC2C3a)
'or' aC3C1a)
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
set S = (
STC0Str (x1,x2,x3,x4,x5,x6,x7));
set C = (
STC0Circ (x1,x2,x3,x4,x5,x6,x7));
set A1out = (
GFA0AdderOutput (x1,x2,x3));
set A2out = (
GFA0AdderOutput (x5,x6,x7));
set C1out = (
GFA0CarryOutput (x1,x2,x3));
set C2out = (
GFA0CarryOutput (x5,x6,x7));
set C3out = (
GFA0CarryOutput (A1out,A2out,x4));
set C1C2a =
[
<*C1out, C2out*>,
and2 ];
set C2C3a =
[
<*C2out, C3out*>,
and2 ];
set C3C1a =
[
<*C3out, C1out*>,
and2 ];
let s be
State of C;
let aC1C2a,aC2C3a,aC3C1a be
Element of
BOOLEAN such that
A1: aC1C2a
= (s
. C1C2a) & aC2C3a
= (s
. C2C3a) & aC3C1a
= (s
. C3C1a);
A2: (
dom s)
= the
carrier of S by
CIRCUIT1: 3;
A3: C1C2a
in the
carrier of S & C2C3a
in the
carrier of S & C3C1a
in the
carrier of S by
ThSTC0S6;
(
InnerVertices S)
= the
carrier' of S by
FACIRC_1: 37;
hence ((
Following s)
. (
GFA0CarryOutput (C1out,C2out,C3out)))
= (
or3
. (s
*
<*C1C2a, C2C3a, C3C1a*>)) by
ThSTC0S7,
FACIRC_1: 35
.= (
or3
.
<*aC1C2a, aC2C3a, aC3C1a*>) by
A1,
A2,
A3,
FINSEQ_2: 126
.= ((aC1C2a
'or' aC2C3a)
'or' aC3C1a) by
FACIRC_1:def 7;
end;
LmSTC0S15S2: for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds for s be
State of (
STC0Circ (x1,x2,x3,x4,x5,x6,x7)) holds for a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN st a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7) holds ((
Following (s,6))
. (
STC0OutputS2 (x1,x2,x3,x4,x5,x6,x7)))
= ((((((a1
'&' a2)
'or' (a2
'&' a3))
'or' (a3
'&' a1))
'&' (((a5
'&' a6)
'or' (a6
'&' a7))
'or' (a7
'&' a5)))
'or' ((((a5
'&' a6)
'or' (a6
'&' a7))
'or' (a7
'&' a5))
'&' (((((a1
'xor' a2)
'xor' a3)
'&' ((a5
'xor' a6)
'xor' a7))
'or' (((a5
'xor' a6)
'xor' a7)
'&' a4))
'or' (a4
'&' ((a1
'xor' a2)
'xor' a3)))))
'or' ((((((a1
'xor' a2)
'xor' a3)
'&' ((a5
'xor' a6)
'xor' a7))
'or' (((a5
'xor' a6)
'xor' a7)
'&' a4))
'or' (a4
'&' ((a1
'xor' a2)
'xor' a3)))
'&' (((a1
'&' a2)
'or' (a2
'&' a3))
'or' (a3
'&' a1)))) & ((
Following (s,6))
. x1)
= a1 & ((
Following (s,6))
. x2)
= a2 & ((
Following (s,6))
. x3)
= a3 & ((
Following (s,6))
. x4)
= a4 & ((
Following (s,6))
. x5)
= a5 & ((
Following (s,6))
. x6)
= a6 & ((
Following (s,6))
. x7)
= a7
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
set S = (
STC0Str (x1,x2,x3,x4,x5,x6,x7));
set C = (
STC0Circ (x1,x2,x3,x4,x5,x6,x7));
set A1out = (
GFA0AdderOutput (x1,x2,x3));
set A2out = (
GFA0AdderOutput (x5,x6,x7));
set C1out = (
GFA0CarryOutput (x1,x2,x3));
set C2out = (
GFA0CarryOutput (x5,x6,x7));
set C3out = (
GFA0CarryOutput (A1out,A2out,x4));
set C1C2a =
[
<*C1out, C2out*>,
and2 ];
set C2C3a =
[
<*C2out, C3out*>,
and2 ];
set C3C1a =
[
<*C3out, C1out*>,
and2 ];
set S2out = (
STC0OutputS2 (x1,x2,x3,x4,x5,x6,x7));
let s be
State of C;
let a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN such that
A2: a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7);
A3: x1
in (
InputVertices S) & x2
in (
InputVertices S) & x3
in (
InputVertices S) & x4
in (
InputVertices S) & x5
in (
InputVertices S) & x6
in (
InputVertices S) & x7
in (
InputVertices S) by
ThSTC0S9;
A5: ((
Following (s,5))
. C1C2a)
= ((((a1
'&' a2)
'or' (a2
'&' a3))
'or' (a3
'&' a1))
'&' (((a5
'&' a6)
'or' (a6
'&' a7))
'or' (a7
'&' a5))) & ((
Following (s,5))
. C2C3a)
= ((((a5
'&' a6)
'or' (a6
'&' a7))
'or' (a7
'&' a5))
'&' (((((a1
'xor' a2)
'xor' a3)
'&' ((a5
'xor' a6)
'xor' a7))
'or' (((a5
'xor' a6)
'xor' a7)
'&' a4))
'or' (a4
'&' ((a1
'xor' a2)
'xor' a3)))) & ((
Following (s,5))
. C3C1a)
= ((((((a1
'xor' a2)
'xor' a3)
'&' ((a5
'xor' a6)
'xor' a7))
'or' (((a5
'xor' a6)
'xor' a7)
'&' a4))
'or' (a4
'&' ((a1
'xor' a2)
'xor' a3)))
'&' (((a1
'&' a2)
'or' (a2
'&' a3))
'or' (a3
'&' a1))) by
A2,
LmSTC0S15S2s6;
(
Following (s,(5
+ 1)))
= (
Following (
Following (s,5))) by
FACIRC_1: 12;
hence thesis by
A2,
A3,
CIRCCMB3: 1,
A5,
LmSTC0S15S2s8;
end;
theorem ::
WALLACE1:29
for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds for s be
State of (
STC0Circ (x1,x2,x3,x4,x5,x6,x7)) holds for a1,a2,a3,a4,a5,a6,a7 be
Element of
BOOLEAN st a1
= (s
. x1) & a2
= (s
. x2) & a3
= (s
. x3) & a4
= (s
. x4) & a5
= (s
. x5) & a6
= (s
. x6) & a7
= (s
. x7) holds ((
Following (s,4))
. (
STC0OutputS0 (x1,x2,x3,x4,x5,x6,x7)))
= ((((((a1
'xor' a2)
'xor' a3)
'xor' a4)
'xor' a5)
'xor' a6)
'xor' a7) & ((
Following (s,6))
. (
STC0OutputS1 (x1,x2,x3,x4,x5,x6,x7)))
= (((((a1
'&' a2)
'or' (a2
'&' a3))
'or' (a3
'&' a1))
'xor' (((a5
'&' a6)
'or' (a6
'&' a7))
'or' (a7
'&' a5)))
'xor' (((((a1
'xor' a2)
'xor' a3)
'&' ((a5
'xor' a6)
'xor' a7))
'or' (((a5
'xor' a6)
'xor' a7)
'&' a4))
'or' (a4
'&' ((a1
'xor' a2)
'xor' a3)))) & ((
Following (s,6))
. (
STC0OutputS2 (x1,x2,x3,x4,x5,x6,x7)))
= ((((((a1
'&' a2)
'or' (a2
'&' a3))
'or' (a3
'&' a1))
'&' (((a5
'&' a6)
'or' (a6
'&' a7))
'or' (a7
'&' a5)))
'or' ((((a5
'&' a6)
'or' (a6
'&' a7))
'or' (a7
'&' a5))
'&' (((((a1
'xor' a2)
'xor' a3)
'&' ((a5
'xor' a6)
'xor' a7))
'or' (((a5
'xor' a6)
'xor' a7)
'&' a4))
'or' (a4
'&' ((a1
'xor' a2)
'xor' a3)))))
'or' ((((((a1
'xor' a2)
'xor' a3)
'&' ((a5
'xor' a6)
'xor' a7))
'or' (((a5
'xor' a6)
'xor' a7)
'&' a4))
'or' (a4
'&' ((a1
'xor' a2)
'xor' a3)))
'&' (((a1
'&' a2)
'or' (a2
'&' a3))
'or' (a3
'&' a1)))) & ((
Following (s,6))
. x1)
= a1 & ((
Following (s,6))
. x2)
= a2 & ((
Following (s,6))
. x3)
= a3 & ((
Following (s,6))
. x4)
= a4 & ((
Following (s,6))
. x5)
= a5 & ((
Following (s,6))
. x6)
= a6 & ((
Following (s,6))
. x7)
= a7 by
LmSTC0S15S0,
LmSTC0S15S1,
LmSTC0S15S2;
theorem ::
WALLACE1:30
for x1,x2,x3,x4,x5,x6,x7 be non
pair
set holds for s be
State of (
STC0Circ (x1,x2,x3,x4,x5,x6,x7)) holds (
Following (s,6)) is
stable
proof
let x1,x2,x3,x4,x5,x6,x7 be non
pair
set;
set S = (
STC0Str (x1,x2,x3,x4,x5,x6,x7));
set C = (
STC0Circ (x1,x2,x3,x4,x5,x6,x7));
set S1 = (
STC0IStr (x1,x2,x3,x4,x5,x6,x7));
set C1 = (
STC0ICirc (x1,x2,x3,x4,x5,x6,x7));
set A1out = (
GFA0AdderOutput (x1,x2,x3));
set A2out = (
GFA0AdderOutput (x5,x6,x7));
set C1out = (
GFA0CarryOutput (x1,x2,x3));
set C2out = (
GFA0CarryOutput (x5,x6,x7));
set C3out = (
GFA0CarryOutput (A1out,A2out,x4));
set S2 = (
BitGFA0Str (C1out,C2out,C3out));
set C2 = (
BitGFA0Circ (C1out,C2out,C3out));
set C1C2x =
[
<*C1out, C2out*>,
xor2 ];
set C1C2a =
[
<*C1out, C2out*>,
and2 ];
set C2C3a =
[
<*C2out, C3out*>,
and2 ];
set C3C1a =
[
<*C3out, C1out*>,
and2 ];
set n1 = 4, n2 = 2;
let s be
State of C;
C1
tolerates C2 by
CIRCCOMB: 60;
then
A2: the
Sorts of C1
tolerates the
Sorts of C2 by
CIRCCOMB:def 3;
then
reconsider s1 = (s
| the
carrier of S1) as
State of C1 by
CIRCCOMB: 26;
reconsider s2 = ((
Following (s,n1))
| the
carrier of S2) as
State of C2 by
A2,
CIRCCOMB: 26;
A3: (
InputVertices S1)
misses (
InnerVertices S2) & (
Following (s1,n1)) is
stable by
LmSTC0S2b,
ThSTC0IS18;
C3out
<> C1C2x & C1out
<> C2C3a & C2out
<> C3C1a & C3out
<> C1C2a by
LmSTC0S1;
then (
Following (s2,n2)) is
stable by
GFACIRC1: 40;
then (
Following (s,(n1
+ n2))) is
stable by
A3,
CIRCCMB2: 19,
CIRCCOMB: 60;
hence thesis;
end;