:: Full Adder Circuit. Part { II } :: by Grzegorz Bancerek , Shin'nosuke Yamaguchi and Katsumi Wasaki :: :: Received March 22, 2002 :: Copyright (c) 2002-2012 Association of Mizar Users begin theorem Th1: :: FACIRC_2:1 for x, y, z being set st x <> z & y <> z holds {x,y} \ {z} = {x,y} proofend; theorem :: FACIRC_2:2 for x, y, z being set holds ( x <> [<*x,y*>,z] & y <> [<*x,y*>,z] ) proofend; registration cluster void -> unsplit gate`1=arity gate`2isBoolean for ManySortedSign ; coherence for b1 being ManySortedSign st b1 is void holds ( b1 is unsplit & b1 is gate`1=arity & b1 is gate`2isBoolean ) proofend; end; registration cluster void strict for ManySortedSign ; existence ex b1 being ManySortedSign st ( b1 is strict & b1 is void ) proofend; end; definition let x be set ; func SingleMSS x -> void strict ManySortedSign means :Def1: :: FACIRC_2:def 1 the carrier of it = {x}; existence ex b1 being void strict ManySortedSign st the carrier of b1 = {x} proofend; uniqueness for b1, b2 being void strict ManySortedSign st the carrier of b1 = {x} & the carrier of b2 = {x} holds b1 = b2 proofend; end; :: deftheorem Def1 defines SingleMSS FACIRC_2:def_1_:_ for x being set for b2 being void strict ManySortedSign holds ( b2 = SingleMSS x iff the carrier of b2 = {x} ); registration let x be set ; cluster SingleMSS x -> non empty void strict ; coherence not SingleMSS x is empty proofend; end; definition let x be set ; func SingleMSA x -> strict Boolean MSAlgebra over SingleMSS x means :: FACIRC_2:def 2 verum; existence ex b1 being strict Boolean MSAlgebra over SingleMSS x st verum ; uniqueness for b1, b2 being strict Boolean MSAlgebra over SingleMSS x holds b1 = b2 proofend; end; :: deftheorem defines SingleMSA FACIRC_2:def_2_:_ for x being set for b2 being strict Boolean MSAlgebra over SingleMSS x holds ( b2 = SingleMSA x iff verum ); theorem :: FACIRC_2:3 for x being set for S being ManySortedSign holds SingleMSS x tolerates S proofend; 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 #) proofend; 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 #) proofend; 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 ) ; funcn -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 for b1, b2 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign st ex f, g being ManySortedSet of NAT st ( b1 = 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) ) ) ) & ex f, g being ManySortedSet of NAT st ( b2 = 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) ) ) ) holds b1 = b2 proofend; existence ex b1 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex f, g being ManySortedSet of NAT st ( b1 = 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) ) ) ) proofend; end; :: deftheorem Def3 defines -BitAdderStr FACIRC_2:def_3_:_ for n being Nat for x, y being FinSequence for b4 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign holds ( b4 = n -BitAdderStr (x,y) iff ex f, g being ManySortedSet of NAT st ( b4 = 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) ) ) ) ); definition let n be Nat; let x, y be FinSequence; funcn -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 for b1, b2 being strict gate`2=den Boolean Circuit of n -BitAdderStr (x,y) st ex f, g, h being ManySortedSet of NAT st ( n -BitAdderStr (x,y) = f . n & b1 = 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) ) ) ) & ex f, g, h being ManySortedSet of NAT st ( n -BitAdderStr (x,y) = f . n & b2 = 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) ) ) ) holds b1 = b2 proofend; existence ex b1 being strict gate`2=den Boolean Circuit of n -BitAdderStr (x,y) ex f, g, h being ManySortedSet of NAT st ( n -BitAdderStr (x,y) = f . n & b1 = 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) ) ) ) proofend; end; :: deftheorem Def4 defines -BitAdderCirc FACIRC_2:def_4_:_ for n being Nat for x, y being FinSequence for b4 being strict gate`2=den Boolean Circuit of n -BitAdderStr (x,y) holds ( b4 = n -BitAdderCirc (x,y) iff ex f, g, h being ManySortedSet of NAT st ( n -BitAdderStr (x,y) = f . n & b4 = 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) ) ) ) ); definition let n be Nat; let x, y be FinSequence; set c = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]; funcn -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 for b1, b2 being Element of InnerVertices (n -BitAdderStr (x,y)) st ex h being ManySortedSet of NAT st ( b1 = 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) ) ) & ex h being ManySortedSet of NAT st ( b2 = 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) ) ) holds b1 = b2 proofend; existence ex b1 being Element of InnerVertices (n -BitAdderStr (x,y)) ex h being ManySortedSet of NAT st ( b1 = 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) ) ) proofend; end; :: deftheorem Def5 defines -BitMajorityOutput FACIRC_2:def_5_:_ for n being Nat for x, y being FinSequence for b4 being Element of InnerVertices (n -BitAdderStr (x,y)) holds ( b4 = n -BitMajorityOutput (x,y) iff ex h being ManySortedSet of NAT st ( b4 = 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) ) ) ); 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 ) proofend; 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)] ) proofend; 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) ) proofend; 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) ) proofend; theorem Th10: :: FACIRC_2:10 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)) ) proofend; theorem :: FACIRC_2:11 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))) ) proofend; theorem Th12: :: FACIRC_2:12 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))) ) proofend; 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)) proofend; 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))))) proofend; definition let k, n be Nat; assume that X1: k >= 1 and X2: 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 for b1, b2 being Element of InnerVertices (n -BitAdderStr (x,y)) st ex i being Element of NAT st ( k = i + 1 & b1 = BitAdderOutput ((x . k),(y . k),(i -BitMajorityOutput (x,y))) ) & ex i being Element of NAT st ( k = i + 1 & b2 = BitAdderOutput ((x . k),(y . k),(i -BitMajorityOutput (x,y))) ) holds b1 = b2 ; existence ex b1 being Element of InnerVertices (n -BitAdderStr (x,y)) ex i being Element of NAT st ( k = i + 1 & b1 = BitAdderOutput ((x . k),(y . k),(i -BitMajorityOutput (x,y))) ) proofend; end; :: deftheorem Def6 defines -BitAdderOutput FACIRC_2:def_6_:_ for k, n being Nat st k >= 1 & k <= n holds for x, y being FinSequence for b5 being Element of InnerVertices (n -BitAdderStr (x,y)) holds ( b5 = (k,n) -BitAdderOutput (x,y) iff ex i being Element of NAT st ( k = i + 1 & b5 = BitAdderOutput ((x . k),(y . k),(i -BitMajorityOutput (x,y))) ) ); 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))) proofend; Lm1: now__::_thesis:_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*> let i be Element of NAT ; ::_thesis: for x being FinSeqLen of i + 1 ex y being FinSeqLen of i ex a being set st x = y ^ <*a*> let x be FinSeqLen of i + 1; ::_thesis: ex y being FinSeqLen of i ex a being set st x = y ^ <*a*> A1: len x = i + 1 by CARD_1:def_7; then x <> <*> ; then consider y being FinSequence, a being set 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: ex a being set st x = y ^ <*a*> take a = a; ::_thesis: x = y ^ <*a*> thus x = y ^ <*a*> by A2; ::_thesis: verum end; Lm2: now__::_thesis:_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*> let i be Element of NAT ; ::_thesis: 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*> let x be nonpair-yielding FinSeqLen of i + 1; ::_thesis: ex y being nonpair-yielding FinSeqLen of i ex a being non pair set st x = y ^ <*a*> consider y being FinSeqLen of i, a being set 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 toFACIRC_1:def_3 ::_thesis: ( not z in proj1 y or not y . z is pair ) assume A4: z in dom y ; ::_thesis: not y . z is pair then y . z = x . z by A3, FUNCT_1:47; hence not y . z is pair by A2, A4, FACIRC_1:def_3; ::_thesis: verum 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: ex a being non pair set st x = y ^ <*a*> take a = a; ::_thesis: x = y ^ <*a*> thus x = y ^ <*a*> by A1; ::_thesis: verum end; theorem :: FACIRC_2:16 for n being Element of NAT for x, y being FinSequence holds InnerVertices (n -BitAdderStr (x,y)) is Relation proofend; theorem Th17: :: FACIRC_2:17 for x, y, c being set holds InnerVertices (MajorityIStr (x,y,c)) = {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} proofend; 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} proofend; 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))} proofend; 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} proofend; 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 proofend; 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} proofend; 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))} proofend; registration cluster empty -> non pair for set ; coherence for b1 being set st b1 is empty holds not b1 is pair ; end; registration cluster empty Relation-like Function-like -> nonpair-yielding for set ; coherence for b1 being Function st b1 is empty holds b1 is nonpair-yielding proofend; let f be nonpair-yielding Function; let x be set ; clusterf . x -> non pair ; coherence not f . x is pair proofend; end; registration let n be Element of NAT ; let x, y be FinSequence; clustern -BitMajorityOutput (x,y) -> pair ; coherence n -BitMajorityOutput (x,y) is pair proofend; end; theorem Th24: :: FACIRC_2:24 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 ) ) proofend; theorem Th25: :: FACIRC_2:25 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'] ) proofend; theorem Th26: :: FACIRC_2:26 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 & InputVertices (n -BitAdderStr (f,g)) is without_pairs ) proofend; theorem :: FACIRC_2:27 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) proofend; 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 ) proofend; 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 proofend; 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 ) proofend; 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 proofend; 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) ) proofend; 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 proofend; Lm5: for n being Element of NAT ex N being Function of NAT,NAT st ( N . 0 = 1 & N . 1 = 2 & N . 2 = n ) proofend; theorem :: FACIRC_2:32 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 proofend; theorem :: FACIRC_2:33 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:34 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:35 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;