let n be Element of NAT ; :: thesis: for p, q being FinSeqLen of
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 ; :: thesis: 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; :: thesis: ( 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 of $1, set , Nat) -> MSAlgebra of $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 such that
A1:
( n -BitAdderStr (p ^ p1),(q ^ q1) = f1 . n & n -BitAdderCirc (p ^ p1),(q ^ q1) = g1 . n )
and
A2:
( f1 . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & g1 . 0 = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & h1 . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] )
and
A3:
for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra of 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 such that
A4:
( n -BitAdderStr (p ^ p2),(q ^ q2) = f2 . n & n -BitAdderCirc (p ^ p2),(q ^ q2) = g2 . n )
and
A5:
( f2 . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & g2 . 0 = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & h2 . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] )
and
A6:
for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra of 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 ) );
A7:
S1[ 0 ]
by A2, A5;
A8:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
:: thesis: ( S1[i] implies S1[i + 1] )
assume that A9:
(
i <= n implies (
h1 . i = h2 . i &
f1 . i = f2 . i &
g1 . i = g2 . i ) )
and A10:
i + 1
<= n
;
:: thesis: ( h1 . (i + 1) = h2 . (i + 1) & f1 . (i + 1) = f2 . (i + 1) & g1 . (i + 1) = g2 . (i + 1) )
(
len p = n &
len q = n )
by FINSEQ_1:def 18;
then A11:
(
dom p = Seg n &
dom q = Seg n )
by FINSEQ_1:def 3;
0 + 1
<= i + 1
by XREAL_1:8;
then
i + 1
in Seg n
by A10, FINSEQ_1:3;
then A12:
(
(p ^ p1) . (i + 1) = p . (i + 1) &
(p ^ p2) . (i + 1) = p . (i + 1) &
(q ^ q1) . (i + 1) = q . (i + 1) &
(q ^ q2) . (i + 1) = q . (i + 1) )
by A11, FINSEQ_1:def 7;
defpred S2[
set ,
set ,
set ,
set ]
means verum;
A13:
ex
S being non
empty ManySortedSign ex
A being
non-empty MSAlgebra of
S ex
x being
set st
(
S = f1 . 0 &
A = g1 . 0 &
x = h1 . 0 &
S2[
S,
A,
x,
0 ] )
by A2;
A14:
for
n being
Nat for
S being non
empty ManySortedSign for
A being
non-empty MSAlgebra of
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]
;
A15:
for
S being non
empty ManySortedSign for
A being
non-empty MSAlgebra of
S for
z being
set for
n being
Nat holds
H3(
S,
A,
z,
n) is
non-empty MSAlgebra of
H2(
S,
z,
n)
;
for
n being
Nat ex
S being non
empty ManySortedSign ex
A being
non-empty MSAlgebra of
S st
(
S = f1 . n &
A = g1 . n &
S2[
S,
A,
h1 . n,
n] )
from CIRCCMB2:sch 13(A13, A3, A14, A15);
then consider S being non
empty ManySortedSign ,
A being
non-empty MSAlgebra of
S such that A16:
(
S = f1 . i &
A = g1 . i )
;
thus h1 . (i + 1) =
MajorityOutput ((p ^ p2) . (i + 1)),
((q ^ q2) . (i + 1)),
(h2 . i)
by A3, A9, A10, A12, A16, NAT_1:13
.=
h2 . (i + 1)
by A6, A9, A10, A16, NAT_1:13
;
:: thesis: ( 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 A3, A9, A10, A12, A16, NAT_1:13
.=
f2 . (i + 1)
by A6, A9, A10, A16, NAT_1:13
;
:: thesis: g1 . (i + 1) = g2 . (i + 1)
thus g1 . (i + 1) =
A +* (BitAdderWithOverflowCirc ((p ^ p2) . (i + 1)),((q ^ q2) . (i + 1)),(h2 . i))
by A3, A9, A10, A12, A16, NAT_1:13
.=
g2 . (i + 1)
by A6, A9, A10, A16, NAT_1:13
;
:: thesis: verum
end;
A17:
for i being Nat holds S1[i]
from NAT_1:sch 2(A7, A8);
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, A4; :: thesis: n -BitMajorityOutput (p ^ p1),(q ^ q1) = n -BitMajorityOutput (p ^ p2),(q ^ q2)
( n -BitMajorityOutput (p ^ p1),(q ^ q1) = h1 . n & n -BitMajorityOutput (p ^ p2),(q ^ q2) = h2 . n )
by A2, A3, A5, A6, Th7;
hence
n -BitMajorityOutput (p ^ p1),(q ^ q1) = n -BitMajorityOutput (p ^ p2),(q ^ q2)
by A17; :: thesis: verum