FACIRC_2: Full Adder Circuit. Part { II }

:: Full Adder Circuit. Part { II }
:: by Grzegorz Bancerek , Shin'nosuke Yamaguchi and Katsumi Wasaki
::
:: Received March 22, 2002
:: Copyright (c) 2002-2021 Association of Mizar Users

theorem Th1: :: FACIRC_2:1

for x, y, z being set st x <> z & y <> z holds
{x,y} \ {z} = {x,y}

proof end;

theorem :: FACIRC_2:2

for x, y, z being set holds
( x <> [<*x,y*>,z] & y <> [<*x,y*>,z] )

proof end;

registration

cluster void -> unsplit gate`1=arity gate`2isBoolean for ManySortedSign ;

coherence

proof end;

end;

registration

cluster void strict for ManySortedSign ;

existence

proof end;

end;

definition

let x be set ;

func SingleMSS x -> void strict ManySortedSign means :Def1: :: FACIRC_2:def 1
the carrier of it = {x};

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines SingleMSS FACIRC_2:def 1 :

registration

let x be set ;

cluster SingleMSS x -> non empty void strict ;

coherence

proof end;

end;

definition

let x be set ;

func SingleMSA x -> strict Boolean MSAlgebra over SingleMSS x means :: FACIRC_2:def 2
verum;

existence ;
uniqueness

proof end;

end;

:: deftheorem defines SingleMSA FACIRC_2:def 2 :

theorem :: FACIRC_2:3

for x being set
for S being ManySortedSign holds SingleMSS x tolerates S by PARTFUN1:59;

theorem Th4: :: FACIRC_2:4

for x being set
for S being non empty ManySortedSign st x in the carrier of S holds
(SingleMSS x) +* S = ManySortedSign(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S #)

proof end;

theorem :: FACIRC_2:5

for x being set
for S being non empty strict ManySortedSign
for A being Boolean MSAlgebra over S st x in the carrier of S holds
(SingleMSA x) +* A = MSAlgebra(# the Sorts of A, the Charact of A #)

proof end;

notation

synonym <*> for {} ;

end;

definition

let n be Nat;
let x, y be FinSequence;
A1: ( 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) is unsplit & 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) is gate`1=arity & 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) is gate`2isBoolean & not 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) is void & not 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) is empty & 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) is strict ) ;

func n -BitAdderStr (x,y) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign means :Def3: :: FACIRC_2:def 3
ex f, g being ManySortedSet of NAT st
( it = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = g . n holds
( f . (n + 1) = S +* (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) );

uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def3 defines -BitAdderStr FACIRC_2:def 3 :

definition

let n be Nat;
let x, y be FinSequence;

func n -BitAdderCirc (x,y) -> strict gate`2=den Boolean Circuit of n -BitAdderStr (x,y) means :Def4: :: FACIRC_2:def 4
ex f, g, h being ManySortedSet of NAT st
( n -BitAdderStr (x,y) = f . n & it = g . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f . n & A = g . n & z = h . n holds
( f . (n + 1) = S +* (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = A +* (BitAdderWithOverflowCirc ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) );

uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def4 defines -BitAdderCirc FACIRC_2:def 4 :

definition

let n be Nat;
let x, y be FinSequence;
set c = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)];

func n -BitMajorityOutput (x,y) -> Element of InnerVertices (n -BitAdderStr (x,y)) means :Def5: :: FACIRC_2:def 5
ex h being ManySortedSet of NAT st
( it = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat
for z being set st z = h . n holds
h . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) );

uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def5 defines -BitMajorityOutput FACIRC_2:def 5 :

theorem Th6: :: FACIRC_2:6

for x, y being FinSequence
for f, g, h being ManySortedSet of NAT st f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f . n & A = g . n & z = h . n holds
( f . (n + 1) = S +* (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = A +* (BitAdderWithOverflowCirc ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) holds
for n being Nat holds
( n -BitAdderStr (x,y) = f . n & n -BitAdderCirc (x,y) = g . n & n -BitMajorityOutput (x,y) = h . n )

proof end;

theorem Th7: :: FACIRC_2:7

for a, b being FinSequence holds
( 0 -BitAdderStr (a,b) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & 0 -BitAdderCirc (a,b) = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & 0 -BitMajorityOutput (a,b) = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] )

proof end;

theorem Th8: :: FACIRC_2:8

for a, b being FinSequence
for c being set st c = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] holds
( 1 -BitAdderStr (a,b) = (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) +* (BitAdderWithOverflowStr ((a . 1),(b . 1),c)) & 1 -BitAdderCirc (a,b) = (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) +* (BitAdderWithOverflowCirc ((a . 1),(b . 1),c)) & 1 -BitMajorityOutput (a,b) = MajorityOutput ((a . 1),(b . 1),c) )

proof end;

theorem :: FACIRC_2:9

for a, b, c being set st c = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] holds
( 1 -BitAdderStr (<*a*>,<*b*>) = (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) +* (BitAdderWithOverflowStr (a,b,c)) & 1 -BitAdderCirc (<*a*>,<*b*>) = (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) +* (BitAdderWithOverflowCirc (a,b,c)) & 1 -BitMajorityOutput (<*a*>,<*b*>) = MajorityOutput (a,b,c) )

proof end;

theorem Th10: :: FACIRC_2:10

for n being 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)) )

proof end;

theorem :: FACIRC_2:11

for n being Nat
for x, y being FinSeqLen of n
for a, b being set holds
( (n + 1) -BitAdderStr ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitAdderStr (x,y)) +* (BitAdderWithOverflowStr (a,b,(n -BitMajorityOutput (x,y)))) & (n + 1) -BitAdderCirc ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitAdderCirc (x,y)) +* (BitAdderWithOverflowCirc (a,b,(n -BitMajorityOutput (x,y)))) & (n + 1) -BitMajorityOutput ((x ^ <*a*>),(y ^ <*b*>)) = MajorityOutput (a,b,(n -BitMajorityOutput (x,y))) )

proof end;

theorem Th12: :: FACIRC_2:12

for n being Nat
for x, y being FinSequence holds
( (n + 1) -BitAdderStr (x,y) = (n -BitAdderStr (x,y)) +* (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),(n -BitMajorityOutput (x,y)))) & (n + 1) -BitAdderCirc (x,y) = (n -BitAdderCirc (x,y)) +* (BitAdderWithOverflowCirc ((x . (n + 1)),(y . (n + 1)),(n -BitMajorityOutput (x,y)))) & (n + 1) -BitMajorityOutput (x,y) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),(n -BitMajorityOutput (x,y))) )

proof end;

theorem Th13: :: FACIRC_2:13

for n, m being Element of NAT st n <= m holds
for x, y being FinSequence holds InnerVertices (n -BitAdderStr (x,y)) c= InnerVertices (m -BitAdderStr (x,y))

proof end;

theorem :: FACIRC_2:14

for n being Element of NAT
for x, y being FinSequence holds InnerVertices ((n + 1) -BitAdderStr (x,y)) = (InnerVertices (n -BitAdderStr (x,y))) \/ (InnerVertices (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),(n -BitMajorityOutput (x,y)))))

proof end;

definition

let k, n be Nat;
assume that
A1: k >= 1 and
A2: k <= n ;
let x, y be FinSequence;

func (k,n) -BitAdderOutput (x,y) -> Element of InnerVertices (n -BitAdderStr (x,y)) means :Def6: :: FACIRC_2:def 6
ex i being Element of NAT st
( k = i + 1 & it = BitAdderOutput ((x . k),(y . k),(i -BitMajorityOutput (x,y))) );

uniqueness ;
existence

proof end;

end;

:: deftheorem Def6 defines -BitAdderOutput FACIRC_2:def 6 :

theorem :: FACIRC_2:15

for n, k being Element of NAT st k < n holds
for x, y being FinSequence holds ((k + 1),n) -BitAdderOutput (x,y) = BitAdderOutput ((x . (k + 1)),(y . (k + 1)),(k -BitMajorityOutput (x,y)))

proof end;

Lm1: now :: thesis:

let i be Nat; :: thesis:
let x be FinSeqLen of i + 1; :: thesis:
A1: len x = i + 1 by CARD_1:def 7;
consider y being FinSequence, a being object such that
A2: x = y ^ <*a*> by FINSEQ_1:46;
len <*a*> = 1 by FINSEQ_1:40;
then i + 1 = (len y) + 1 by A1, A2, FINSEQ_1:22;
then reconsider y = y as FinSeqLen of i by CARD_1:def 7;
take y = y; :: thesis:
take a = a; :: thesis:
thus x = y ^ <*a*> by A2; :: thesis:

end;

Lm2: now :: thesis:

let i be Nat; :: thesis:
let x be nonpair-yielding FinSeqLen of i + 1; :: thesis:
consider y being FinSeqLen of i, a being object such that
A1: x = y ^ <*a*> by Lm1;
A2: dom y c= dom x by A1, FINSEQ_1:26;
A3: y = x | (dom y) by A1, FINSEQ_1:21;
y is nonpair-yielding

proof

let z be set ; :: according to FACIRC_1:def 3 :: thesis:
assume A4: z in dom y ; :: thesis:
then y . z = x . z by A3, FUNCT_1:47;
hence not y . z is pair by A2, A4, FACIRC_1:def 3; :: thesis:

end;

then reconsider y = y as nonpair-yielding FinSeqLen of i ;
A5: i + 1 in Seg (i + 1) by FINSEQ_1:4;
dom x = Seg (len x) by FINSEQ_1:def 3;
then A6: i + 1 in dom x by A5, CARD_1:def 7;
A7: x . ((len y) + 1) = a by A1, FINSEQ_1:42;
len y = i by CARD_1:def 7;
then reconsider a = a as non pair set by A6, A7, FACIRC_1:def 3;
take y = y; :: thesis:
take a = a; :: thesis:
thus x = y ^ <*a*> by A1; :: thesis:

end;

theorem :: FACIRC_2:16

for n being Element of NAT
for x, y being FinSequence holds InnerVertices (n -BitAdderStr (x,y)) is Relation

proof end;

theorem Th17: :: FACIRC_2:17

for x, y, c being set holds InnerVertices (MajorityIStr (x,y,c)) = {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']}

proof end;

theorem Th18: :: FACIRC_2:18

for x, y, c being set st x <> [<*y,c*>,'&'] & y <> [<*c,x*>,'&'] & c <> [<*x,y*>,'&'] holds
InputVertices (MajorityIStr (x,y,c)) = {x,y,c}

proof end;

theorem Th19: :: FACIRC_2:19

for x, y, c being set holds InnerVertices (MajorityStr (x,y,c)) = {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} \/ {(MajorityOutput (x,y,c))}

proof end;

theorem Th20: :: FACIRC_2:20

for x, y, c being set st x <> [<*y,c*>,'&'] & y <> [<*c,x*>,'&'] & c <> [<*x,y*>,'&'] holds
InputVertices (MajorityStr (x,y,c)) = {x,y,c}

proof end;

theorem Th21: :: FACIRC_2:21

for S1, S2 being non empty ManySortedSign st S1 tolerates S2 & InputVertices S1 = InputVertices S2 holds
InputVertices (S1 +* S2) = InputVertices S1

proof end;

theorem Th22: :: FACIRC_2:22

for x, y, c being set st x <> [<*y,c*>,'&'] & y <> [<*c,x*>,'&'] & c <> [<*x,y*>,'&'] & c <> [<*x,y*>,'xor'] holds
InputVertices (BitAdderWithOverflowStr (x,y,c)) = {x,y,c}

proof end;

theorem Th23: :: FACIRC_2:23

for x, y, c being set holds InnerVertices (BitAdderWithOverflowStr (x,y,c)) = ({[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} \/ {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']}) \/ {(MajorityOutput (x,y,c))}

proof end;

registration

cluster empty -> non pair for set ;

coherence ;

end;

registration

cluster empty Relation-like Function-like -> nonpair-yielding for set ;

coherence

proof end;

let f be nonpair-yielding Function;
let x be set ;

cluster f . x -> non pair ;

coherence

proof end;

end;

registration

let n be Nat;
let x, y be FinSequence;

cluster n -BitMajorityOutput (x,y) -> pair ;

coherence

proof end;

end;

theorem Th24: :: FACIRC_2:24

for x, y being FinSequence
for n being Nat holds
( ( (n -BitMajorityOutput (x,y)) `1 = <*> & (n -BitMajorityOutput (x,y)) `2 = (0 -tuples_on BOOLEAN) --> FALSE & proj1 ((n -BitMajorityOutput (x,y)) `2) = 0 -tuples_on BOOLEAN ) or ( card ((n -BitMajorityOutput (x,y)) `1) = 3 & (n -BitMajorityOutput (x,y)) `2 = or3 & proj1 ((n -BitMajorityOutput (x,y)) `2) = 3 -tuples_on BOOLEAN ) )

proof end;

theorem Th25: :: FACIRC_2:25

for n being Nat
for x, y being FinSequence
for p being set holds
( n -BitMajorityOutput (x,y) <> [p,'&'] & n -BitMajorityOutput (x,y) <> [p,'xor'] )

proof end;

theorem Th26: :: FACIRC_2:26

for f, g being nonpair-yielding FinSequence
for n being Nat holds
( InputVertices ((n + 1) -BitAdderStr (f,g)) = (InputVertices (n -BitAdderStr (f,g))) \/ ((InputVertices (BitAdderWithOverflowStr ((f . (n + 1)),(g . (n + 1)),(n -BitMajorityOutput (f,g))))) \ {(n -BitMajorityOutput (f,g))}) & InnerVertices (n -BitAdderStr (f,g)) is Relation & InputVertices (n -BitAdderStr (f,g)) is without_pairs )

proof end;

theorem :: FACIRC_2:27

for n being Nat
for x, y being nonpair-yielding FinSeqLen of n holds InputVertices (n -BitAdderStr (x,y)) = (rng x) \/ (rng y)

proof end;

Lm3: for x, y, c being set
for s being State of (MajorityCirc (x,y,c))
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
( (Following s) . [<*x,y*>,'&'] = a1 '&' a2 & (Following s) . [<*y,c*>,'&'] = a2 '&' a3 & (Following s) . [<*c,x*>,'&'] = a3 '&' a1 )

proof end;

theorem Th28: :: FACIRC_2:28

for x, y, c being set
for s being State of (MajorityCirc (x,y,c))
for a1, a2, a3 being Element of BOOLEAN st a1 = s . [<*x,y*>,'&'] & a2 = s . [<*y,c*>,'&'] & a3 = s . [<*c,x*>,'&'] holds
(Following s) . (MajorityOutput (x,y,c)) = (a1 'or' a2) 'or' a3

proof end;

Lm4: for x, y, c being set st x <> [<*y,c*>,'&'] & y <> [<*c,x*>,'&'] & c <> [<*x,y*>,'&'] holds
for s being State of (MajorityCirc (x,y,c))
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
( (Following (s,2)) . (MajorityOutput (x,y,c)) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1) & (Following (s,2)) . [<*x,y*>,'&'] = a1 '&' a2 & (Following (s,2)) . [<*y,c*>,'&'] = a2 '&' a3 & (Following (s,2)) . [<*c,x*>,'&'] = a3 '&' a1 )

proof end;

theorem Th29: :: FACIRC_2:29

for x, y, c being set st x <> [<*y,c*>,'&'] & y <> [<*c,x*>,'&'] & c <> [<*x,y*>,'&'] holds
for s being State of (MajorityCirc (x,y,c)) holds Following (s,2) is stable

proof end;

theorem :: FACIRC_2:30

for x, y, c being set st x <> [<*y,c*>,'&'] & y <> [<*c,x*>,'&'] & c <> [<*x,y*>,'&'] & c <> [<*x,y*>,'xor'] holds
for s being State of (BitAdderWithOverflowCirc (x,y,c))
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
( (Following (s,2)) . (BitAdderOutput (x,y,c)) = (a1 'xor' a2) 'xor' a3 & (Following (s,2)) . (MajorityOutput (x,y,c)) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1) )

proof end;

theorem Th31: :: FACIRC_2:31

for x, y, c being set st x <> [<*y,c*>,'&'] & y <> [<*c,x*>,'&'] & c <> [<*x,y*>,'&'] & c <> [<*x,y*>,'xor'] holds
for s being State of (BitAdderWithOverflowCirc (x,y,c)) holds Following (s,2) is stable

proof end;

theorem :: FACIRC_2:32

for n being 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

proof end;

theorem :: FACIRC_2:33

for i being Nat
for x being FinSeqLen of i + 1 ex y being FinSeqLen of i ex a being object st x = y ^ <*a*> by Lm1;

theorem :: FACIRC_2:34

for i being Nat
for x being nonpair-yielding FinSeqLen of i + 1 ex y being nonpair-yielding FinSeqLen of i ex a being non pair set st x = y ^ <*a*> by Lm2;