let n be Nat; for p, q being FinSeqLen of n
for p1, p2, q1, q2 being FinSequence holds
( n -BitAdderStr ((p ^ p1),(q ^ q1)) = n -BitAdderStr ((p ^ p2),(q ^ q2)) & n -BitAdderCirc ((p ^ p1),(q ^ q1)) = n -BitAdderCirc ((p ^ p2),(q ^ q2)) & n -BitMajorityOutput ((p ^ p1),(q ^ q1)) = n -BitMajorityOutput ((p ^ p2),(q ^ q2)) )
set c = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)];
let p, q be FinSeqLen of n; for p1, p2, q1, q2 being FinSequence holds
( n -BitAdderStr ((p ^ p1),(q ^ q1)) = n -BitAdderStr ((p ^ p2),(q ^ q2)) & n -BitAdderCirc ((p ^ p1),(q ^ q1)) = n -BitAdderCirc ((p ^ p2),(q ^ q2)) & n -BitMajorityOutput ((p ^ p1),(q ^ q1)) = n -BitMajorityOutput ((p ^ p2),(q ^ q2)) )
let p1, p2, q1, q2 be FinSequence; ( n -BitAdderStr ((p ^ p1),(q ^ q1)) = n -BitAdderStr ((p ^ p2),(q ^ q2)) & n -BitAdderCirc ((p ^ p1),(q ^ q1)) = n -BitAdderCirc ((p ^ p2),(q ^ q2)) & n -BitMajorityOutput ((p ^ p1),(q ^ q1)) = n -BitMajorityOutput ((p ^ p2),(q ^ q2)) )
deffunc H1( set , Nat) -> Element of InnerVertices (MajorityStr (((p ^ p1) . ($2 + 1)),((q ^ q1) . ($2 + 1)),$1)) = MajorityOutput (((p ^ p1) . ($2 + 1)),((q ^ q1) . ($2 + 1)),$1);
deffunc H2( non empty ManySortedSign , set , Nat) -> ManySortedSign = $1 +* (BitAdderWithOverflowStr (((p ^ p1) . ($3 + 1)),((q ^ q1) . ($3 + 1)),$2));
deffunc H3( non empty ManySortedSign , non-empty MSAlgebra over $1, set , Nat) -> MSAlgebra over $1 +* (BitAdderWithOverflowStr (((p ^ p1) . ($4 + 1)),((q ^ q1) . ($4 + 1)),$3)) = $2 +* (BitAdderWithOverflowCirc (((p ^ p1) . ($4 + 1)),((q ^ q1) . ($4 + 1)),$3));
consider f1, g1, h1 being ManySortedSet of NAT such that
A1:
n -BitAdderStr ((p ^ p1),(q ^ q1)) = f1 . n
and
A2:
n -BitAdderCirc ((p ^ p1),(q ^ q1)) = g1 . n
and
A3:
f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))
and
A4:
g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE))
and
A5:
h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]
and
A6:
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) = H2(S,z,n) & g1 . (n + 1) = H3(S,A,z,n) & h1 . (n + 1) = H1(z,n) )
by Def4;
consider f2, g2, h2 being ManySortedSet of NAT such that
A7:
n -BitAdderStr ((p ^ p2),(q ^ q2)) = f2 . n
and
A8:
n -BitAdderCirc ((p ^ p2),(q ^ q2)) = g2 . n
and
A9:
f2 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))
and
A10:
g2 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE))
and
A11:
h2 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]
and
A12:
for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f2 . n & A = g2 . n & z = h2 . n holds
( f2 . (n + 1) = S +* (BitAdderWithOverflowStr (((p ^ p2) . (n + 1)),((q ^ q2) . (n + 1)),z)) & g2 . (n + 1) = A +* (BitAdderWithOverflowCirc (((p ^ p2) . (n + 1)),((q ^ q2) . (n + 1)),z)) & h2 . (n + 1) = MajorityOutput (((p ^ p2) . (n + 1)),((q ^ q2) . (n + 1)),z) )
by Def4;
defpred S1[ Nat] means ( $1 <= n implies ( h1 . $1 = h2 . $1 & f1 . $1 = f2 . $1 & g1 . $1 = g2 . $1 ) );
A13:
S1[ 0 ]
by A3, A4, A5, A9, A10, A11;
A14:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume that A15:
(
i <= n implies (
h1 . i = h2 . i &
f1 . i = f2 . i &
g1 . i = g2 . i ) )
and A16:
i + 1
<= n
;
( h1 . (i + 1) = h2 . (i + 1) & f1 . (i + 1) = f2 . (i + 1) & g1 . (i + 1) = g2 . (i + 1) )
A17:
len p = n
by CARD_1:def 7;
A18:
len q = n
by CARD_1:def 7;
A19:
dom p = Seg n
by A17, FINSEQ_1:def 3;
A20:
dom q = Seg n
by A18, FINSEQ_1:def 3;
0 + 1
<= i + 1
by XREAL_1:6;
then A21:
i + 1
in Seg n
by A16, FINSEQ_1:1;
then A22:
(p ^ p1) . (i + 1) = p . (i + 1)
by A19, FINSEQ_1:def 7;
A23:
(p ^ p2) . (i + 1) = p . (i + 1)
by A19, A21, FINSEQ_1:def 7;
A24:
(q ^ q1) . (i + 1) = q . (i + 1)
by A20, A21, FINSEQ_1:def 7;
A25:
(q ^ q2) . (i + 1) = q . (i + 1)
by A20, A21, FINSEQ_1:def 7;
defpred S2[
set ,
set ,
set ,
set ]
means verum;
A26:
ex
S being non
empty ManySortedSign ex
A being
non-empty MSAlgebra over
S ex
x being
set st
(
S = f1 . 0 &
A = g1 . 0 &
x = h1 . 0 &
S2[
S,
A,
x,
0 ] )
by A3, A4;
A27:
for
n being
Nat for
S being non
empty ManySortedSign for
A being
non-empty MSAlgebra over
S for
x being
set st
S = f1 . n &
A = g1 . n &
x = h1 . n &
S2[
S,
A,
x,
n] holds
S2[
H2(
S,
x,
n),
H3(
S,
A,
x,
n),
H1(
x,
n),
n + 1]
;
A28:
for
S being non
empty ManySortedSign for
A being
non-empty MSAlgebra over
S for
z being
set for
n being
Nat holds
H3(
S,
A,
z,
n) is
non-empty MSAlgebra over
H2(
S,
z,
n)
;
for
n being
Nat ex
S being non
empty ManySortedSign ex
A being
non-empty MSAlgebra over
S st
(
S = f1 . n &
A = g1 . n &
S2[
S,
A,
h1 . n,
n] )
from CIRCCMB2:sch 13(A26, A6, A27, A28);
then consider S being non
empty ManySortedSign ,
A being
non-empty MSAlgebra over
S such that A29:
S = f1 . i
and A30:
A = g1 . i
;
thus h1 . (i + 1) =
MajorityOutput (
((p ^ p2) . (i + 1)),
((q ^ q2) . (i + 1)),
(h2 . i))
by A6, A15, A16, A22, A23, A24, A25, A29, A30, NAT_1:13
.=
h2 . (i + 1)
by A12, A15, A16, A29, A30, NAT_1:13
;
( f1 . (i + 1) = f2 . (i + 1) & g1 . (i + 1) = g2 . (i + 1) )
thus f1 . (i + 1) =
S +* (BitAdderWithOverflowStr (((p ^ p2) . (i + 1)),((q ^ q2) . (i + 1)),(h2 . i)))
by A6, A15, A16, A22, A23, A24, A25, A29, A30, NAT_1:13
.=
f2 . (i + 1)
by A12, A15, A16, A29, A30, NAT_1:13
;
g1 . (i + 1) = g2 . (i + 1)
thus g1 . (i + 1) =
A +* (BitAdderWithOverflowCirc (((p ^ p2) . (i + 1)),((q ^ q2) . (i + 1)),(h2 . i)))
by A6, A15, A16, A22, A23, A24, A25, A29, A30, NAT_1:13
.=
g2 . (i + 1)
by A12, A15, A16, A29, A30, NAT_1:13
;
verum
end;
A31:
for i being Nat holds S1[i]
from NAT_1:sch 2(A13, A14);
hence
( n -BitAdderStr ((p ^ p1),(q ^ q1)) = n -BitAdderStr ((p ^ p2),(q ^ q2)) & n -BitAdderCirc ((p ^ p1),(q ^ q1)) = n -BitAdderCirc ((p ^ p2),(q ^ q2)) )
by A1, A2, A7, A8; n -BitMajorityOutput ((p ^ p1),(q ^ q1)) = n -BitMajorityOutput ((p ^ p2),(q ^ q2))
A32:
n -BitMajorityOutput ((p ^ p1),(q ^ q1)) = h1 . n
by A3, A4, A5, A6, Th6;
n -BitMajorityOutput ((p ^ p2),(q ^ q2)) = h2 . n
by A9, A10, A11, A12, Th6;
hence
n -BitMajorityOutput ((p ^ p1),(q ^ q1)) = n -BitMajorityOutput ((p ^ p2),(q ^ q2))
by A31, A32; verum