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 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

canceled;

theorem :: FACIRC_2:3

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 ManySortedSign ;
coherence

proof end;

end;

registration

cluster void strict 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 of SingleMSS x means :: FACIRC_2:def 2
verum;
existence ;
uniqueness

proof end;

end;

:: deftheorem defines SingleMSA FACIRC_2:def 2 :

theorem :: FACIRC_2:4

for x being set
for S being ManySortedSign holds SingleMSS x tolerates S

proof end;

theorem Th5: :: FACIRC_2:5

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:6

for x being set
for S being non empty strict ManySortedSign
for A being Boolean MSAlgebra of 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

:: original: <*>
redefine func <*> -> FinSeqLen of 0 ;
coherence by CARD_1:47, CIRCCOMB:def 12;

end;

definition

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 of 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 Th7: :: FACIRC_2:7

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 of 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 Th8: :: FACIRC_2:8

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 Th9: :: FACIRC_2:9

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:10

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 Th11: :: FACIRC_2:11

for n being Element of 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:12

for n being Element of 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 Th13: :: FACIRC_2:13

for n being Element of 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 Th14: :: FACIRC_2:14

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:15

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 A1: ( k >= 1 & 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:16

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

let i be Element of NAT ; :: thesis:
let x be FinSeqLen of i + 1; :: thesis:
A1: ( i + 1 <> 0 & len x = i + 1 ) by CIRCCOMB:def 12;
then x <> <*> ;
then consider y being FinSequence, a being set such that
A2: x = y ^ <*a*> by FINSEQ_1:63;
len <*a*> = 1 by FINSEQ_1:57;
then i + 1 = (len y) + 1 by A1, A2, FINSEQ_1:35;
then reconsider y = y as FinSeqLen of i by CIRCCOMB:def 12;
take y = y; :: thesis:
take a = a; :: thesis:
thus x = y ^ <*a*> by A2; :: thesis:

end;

Lm2: now

let i be Element of NAT ; :: thesis:
let x be nonpair-yielding FinSeqLen of i + 1; :: thesis:
consider y being FinSeqLen of i, a being set such that
A1: x = y ^ <*a*> by Lm1;
A2: ( dom y c= dom x & y = x | (dom y) ) by A1, FINSEQ_1:33, FINSEQ_1:39;
y is nonpair-yielding

proof

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

end;

then reconsider y = y as nonpair-yielding FinSeqLen of i ;
( i + 1 in Seg (i + 1) & dom x = Seg (len x) ) by FINSEQ_1:6, FINSEQ_1:def 3;
then ( i + 1 in dom x & x . ((len y) + 1) = a & len y = i ) by A1, CIRCCOMB:def 12, FINSEQ_1:59;
then reconsider a = a as non pair set by FACIRC_1:def 3;
take y = y; :: thesis:
take a = a; :: thesis:
thus x = y ^ <*a*> by A1; :: thesis:

end;

theorem :: FACIRC_2:17

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

proof end;

theorem Th18: :: FACIRC_2:18

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

proof end;

theorem Th19: :: FACIRC_2:19

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 Th20: :: FACIRC_2:20

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 Th21: :: FACIRC_2:21

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 Th22: :: FACIRC_2:22

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

proof end;

theorem Th23: :: FACIRC_2:23

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 Th24: :: FACIRC_2:24

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 set ;
coherence ;

end;

registration

cluster empty -> nonpair-yielding 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 Element of NAT ;
let x, y be FinSequence;
cluster n -BitMajorityOutput x,y -> pair ;
coherence

proof end;

end;

theorem Th25: :: FACIRC_2:25

for x, y being FinSequence
for n being Element of 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 Th26: :: FACIRC_2:26

for n being Element of 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 Th27: :: FACIRC_2:27

for f, g being nonpair-yielding FinSequence
for n being Element of 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 & not InputVertices (n -BitAdderStr f,g) is with_pair )

proof end;

theorem :: FACIRC_2:28

for n being Element of 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 Th29: :: FACIRC_2:29

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 Th30: :: 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 (MajorityCirc x,y,c) holds Following s,2 is stable

proof end;

theorem :: 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)
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 Th32: :: FACIRC_2:32

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;

Lm5: for n being Element of NAT ex N being Function of NAT , NAT st
( N . 0 = 1 & N . 1 = 2 & N . 2 = n )

proof end;

theorem :: FACIRC_2:33

for n being Element of 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:34

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

theorem :: FACIRC_2:35

canceled;

theorem :: FACIRC_2:36

for i being Element of 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;

theorem :: FACIRC_2:37

for n being Element of NAT ex N being Function of NAT , NAT st
( N . 0 = 1 & N . 1 = 2 & N . 2 = n ) by Lm5;