let n be Nat; for x, y being nonpair-yielding FinSeqLen of n
for s being State of (n -BitAdderCirc (x,y)) holds Following (s,(1 + (2 * n))) is stable
let f, g be nonpair-yielding FinSeqLen of n; for s being State of (n -BitAdderCirc (f,g)) holds Following (s,(1 + (2 * n))) is stable
deffunc H1( set , Nat) -> ManySortedSign = BitAdderWithOverflowStr ((f . ($2 + 1)),(g . ($2 + 1)),$1);
deffunc H2( set , Nat) -> MSAlgebra over BitAdderWithOverflowStr ((f . ($2 + 1)),(g . ($2 + 1)),$1) = BitAdderWithOverflowCirc ((f . ($2 + 1)),(g . ($2 + 1)),$1);
deffunc H3( set , Nat) -> Element of InnerVertices (MajorityStr ((f . ($2 + 1)),(g . ($2 + 1)),$1)) = MajorityOutput ((f . ($2 + 1)),(g . ($2 + 1)),$1);
set S0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE));
set A0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE));
set N = (1,2) followed_by (In (n,NAT));
A1:
((1,2) followed_by (In (n,NAT))) . 0 = 1
by FUNCT_7:122;
A2:
((1,2) followed_by (In (n,NAT))) . 1 = 2
by FUNCT_7:123;
A3:
((1,2) followed_by (In (n,NAT))) . 2 = n
by FUNCT_7:124;
deffunc H4( Element of NAT ) -> Element of NAT = ((1,2) followed_by (In (n,NAT))) . $1;
A4:
for x being set
for n being Nat holds H2(x,n) is strict gate`2=den Boolean Circuit of H1(x,n)
;
deffunc H5( Element of NAT ) -> Element of InnerVertices ($1 -BitAdderStr (f,g)) = $1 -BitMajorityOutput (f,g);
consider h being ManySortedSet of NAT such that
A6:
for n being Element of NAT holds h . n = H5(n)
from PBOOLE:sch 5();
A7:
for n being Nat
for x being set
for A being non-empty Circuit of H1(x,n) st x = h . n & A = H2(x,n) holds
for s being State of A holds Following (s,H4(1)) is stable
proof
let n be
Nat;
for x being set
for A being non-empty Circuit of H1(x,n) st x = h . n & A = H2(x,n) holds
for s being State of A holds Following (s,H4(1)) is stable let x be
set ;
for A being non-empty Circuit of H1(x,n) st x = h . n & A = H2(x,n) holds
for s being State of A holds Following (s,H4(1)) is stable let A be
non-empty Circuit of
H1(
x,
n);
( x = h . n & A = H2(x,n) implies for s being State of A holds Following (s,H4(1)) is stable )
A8:
n in NAT
by ORDINAL1:def 12;
assume
x = h . n
;
( not A = H2(x,n) or for s being State of A holds Following (s,H4(1)) is stable )
then A9:
x = n -BitMajorityOutput (
f,
g)
by A6, A8;
then A10:
x <> [<*(f . (n + 1)),(g . (n + 1))*>,'&']
by Th25;
x <> [<*(f . (n + 1)),(g . (n + 1))*>,'xor']
by A9, Th25;
hence
( not
A = H2(
x,
n) or for
s being
State of
A holds
Following (
s,
H4(1)) is
stable )
by A2, A10, Th31;
verum
end;
set Sn = n -BitAdderStr (f,g);
set An = n -BitAdderCirc (f,g);
set o0 = 0 -BitMajorityOutput (f,g);
consider f1, g1, h1 being ManySortedSet of NAT such that
A11:
n -BitAdderStr (f,g) = f1 . n
and
A12:
n -BitAdderCirc (f,g) = g1 . n
and
A13:
f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))
and
A14:
g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE))
and
A15:
h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]
and
A16:
for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f1 . n & A = g1 . n & z = h1 . n holds
( f1 . (n + 1) = S +* (BitAdderWithOverflowStr ((f . (n + 1)),(g . (n + 1)),z)) & g1 . (n + 1) = A +* (BitAdderWithOverflowCirc ((f . (n + 1)),(g . (n + 1)),z)) & h1 . (n + 1) = MajorityOutput ((f . (n + 1)),(g . (n + 1)),z) )
by Def4;
then A17:
h1 = h
by PBOOLE:3;
A18:
ex u, v being ManySortedSet of NAT st
( n -BitAdderStr (f,g) = u . H4(2) & n -BitAdderCirc (f,g) = v . H4(2) & u . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & v . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & h . 0 = 0 -BitMajorityOutput (f,g) & ( for n being Nat
for S being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over H1(x,n) st S = u . n & A1 = v . n & x = h . n & A2 = H2(x,n) holds
( u . (n + 1) = S +* H1(x,n) & v . (n + 1) = A1 +* A2 & h . (n + 1) = H3(x,n) ) ) )
proof
take
f1
;
ex v being ManySortedSet of NAT st
( n -BitAdderStr (f,g) = f1 . H4(2) & n -BitAdderCirc (f,g) = v . H4(2) & f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & v . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & h . 0 = 0 -BitMajorityOutput (f,g) & ( for n being Nat
for S being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over H1(x,n) st S = f1 . n & A1 = v . n & x = h . n & A2 = H2(x,n) holds
( f1 . (n + 1) = S +* H1(x,n) & v . (n + 1) = A1 +* A2 & h . (n + 1) = H3(x,n) ) ) )
take
g1
;
( n -BitAdderStr (f,g) = f1 . H4(2) & n -BitAdderCirc (f,g) = g1 . H4(2) & f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & h . 0 = 0 -BitMajorityOutput (f,g) & ( for n being Nat
for S being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over H1(x,n) st S = f1 . n & A1 = g1 . n & x = h . n & A2 = H2(x,n) holds
( f1 . (n + 1) = S +* H1(x,n) & g1 . (n + 1) = A1 +* A2 & h . (n + 1) = H3(x,n) ) ) )
thus
(
n -BitAdderStr (
f,
g)
= f1 . H4(2) &
n -BitAdderCirc (
f,
g)
= g1 . H4(2) &
f1 . 0 = 1GateCircStr (
<*>,
((0 -tuples_on BOOLEAN) --> FALSE)) &
g1 . 0 = 1GateCircuit (
<*>,
((0 -tuples_on BOOLEAN) --> FALSE)) &
h . 0 = 0 -BitMajorityOutput (
f,
g) & ( for
n being
Nat for
S being non
empty ManySortedSign for
A1 being
non-empty MSAlgebra over
S for
x being
set for
A2 being
non-empty MSAlgebra over
H1(
x,
n) st
S = f1 . n &
A1 = g1 . n &
x = h . n &
A2 = H2(
x,
n) holds
(
f1 . (n + 1) = S +* H1(
x,
n) &
g1 . (n + 1) = A1 +* A2 &
h . (n + 1) = H3(
x,
n) ) ) )
by A3, A6, A11, A12, A13, A14, A16, A17;
verum
end;
A19:
( InnerVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) is Relation & InputVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) is without_pairs )
by FACIRC_1:38, FACIRC_1:39;
A20:
[<*>,((0 -tuples_on BOOLEAN) --> FALSE)] = 0 -BitMajorityOutput (f,g)
by Th7;
InnerVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) = {[<*>,((0 -tuples_on BOOLEAN) --> FALSE)]}
by CIRCCOMB:42;
then A21:
( h . 0 = 0 -BitMajorityOutput (f,g) & 0 -BitMajorityOutput (f,g) in InnerVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) )
by A6, A20, TARSKI:def 1;
A22:
for n being Nat
for x being set holds InnerVertices H1(x,n) is Relation
by FACIRC_1:88;
A23:
for n being Nat
for x being set st x = h . n holds
(InputVertices H1(x,n)) \ {x} is without_pairs
proof
let n be
Nat;
for x being set st x = h . n holds
(InputVertices H1(x,n)) \ {x} is without_pairs let x be
set ;
( x = h . n implies (InputVertices H1(x,n)) \ {x} is without_pairs )
assume A24:
x = h . n
;
(InputVertices H1(x,n)) \ {x} is without_pairs
n in NAT
by ORDINAL1:def 12;
then A25:
x = n -BitMajorityOutput (
f,
g)
by A6, A24;
then A26:
x <> [<*(f . (n + 1)),(g . (n + 1))*>,'&']
by Th25;
x <> [<*(f . (n + 1)),(g . (n + 1))*>,'xor']
by A25, Th25;
then A27:
InputVertices H1(
x,
n)
= {(f . (n + 1)),(g . (n + 1)),x}
by A26, Th22;
let a be
pair object ;
FACIRC_1:def 2 not a in (InputVertices H1(x,n)) \ {x}
assume A28:
a in (InputVertices H1(x,n)) \ {x}
;
contradiction
then A29:
a in {(f . (n + 1)),(g . (n + 1)),x}
by A27, XBOOLE_0:def 5;
A30:
not
a in {x}
by A28, XBOOLE_0:def 5;
(
a = f . (n + 1) or
a = g . (n + 1) or
a = x )
by A29, ENUMSET1:def 1;
hence
contradiction
by A30, TARSKI:def 1;
verum
end;
A31:
for n being Nat
for x being set st x = h . n holds
( h . (n + 1) = H3(x,n) & x in InputVertices H1(x,n) & H3(x,n) in InnerVertices H1(x,n) )
proof
let n be
Nat;
for x being set st x = h . n holds
( h . (n + 1) = H3(x,n) & x in InputVertices H1(x,n) & H3(x,n) in InnerVertices H1(x,n) )let x be
set ;
( x = h . n implies ( h . (n + 1) = H3(x,n) & x in InputVertices H1(x,n) & H3(x,n) in InnerVertices H1(x,n) ) )
assume A32:
x = h . n
;
( h . (n + 1) = H3(x,n) & x in InputVertices H1(x,n) & H3(x,n) in InnerVertices H1(x,n) )
n in NAT
by ORDINAL1:def 12;
then A33:
x = n -BitMajorityOutput (
f,
g)
by A6, A32;
h . (n + 1) = (n + 1) -BitMajorityOutput (
f,
g)
by A6;
hence
h . (n + 1) = H3(
x,
n)
by A33, Th12;
( x in InputVertices H1(x,n) & H3(x,n) in InnerVertices H1(x,n) )
A34:
x <> [<*(f . (n + 1)),(g . (n + 1))*>,'&']
by A33, Th25;
x <> [<*(f . (n + 1)),(g . (n + 1))*>,'xor']
by A33, Th25;
then
InputVertices H1(
x,
n)
= {(f . (n + 1)),(g . (n + 1)),x}
by A34, Th22;
hence
x in InputVertices H1(
x,
n)
by ENUMSET1:def 1;
H3(x,n) in InnerVertices H1(x,n)
set xx =
f . (n + 1);
set xy =
g . (n + 1);
A35:
H3(
x,
n)
in {H3(x,n)}
by TARSKI:def 1;
InnerVertices H1(
x,
n)
= ({[<*(f . (n + 1)),(g . (n + 1))*>,'xor'],(2GatesCircOutput ((f . (n + 1)),(g . (n + 1)),x,'xor'))} \/ {[<*(f . (n + 1)),(g . (n + 1))*>,'&'],[<*(g . (n + 1)),x*>,'&'],[<*x,(f . (n + 1))*>,'&']}) \/ {(MajorityOutput ((f . (n + 1)),(g . (n + 1)),x))}
by Th23;
hence
H3(
x,
n)
in InnerVertices H1(
x,
n)
by A35, XBOOLE_0:def 3;
verum
end;
for s being State of (n -BitAdderCirc (f,g)) holds Following (s,(H4( 0 ) + (H4(2) * H4(1)))) is stable
from CIRCCMB2:sch 22(A4, A5, A7, A18, A19, A21, A22, A23, A31);
hence
for s being State of (n -BitAdderCirc (f,g)) holds Following (s,(1 + (2 * n))) is stable
by A1, A2, A3; verum