:: Full Subtracter Circuit. Part { I } :: by Katsumi Wasaki and Noboru Endou :: :: Received March 13, 1999 :: Copyright (c) 1999-2012 Association of Mizar Users begin definition let x, y, c be set ; func BitSubtracterOutput (x,y,c) -> Element of InnerVertices (2GatesCircStr (x,y,c,'xor')) equals :: FSCIRC_1:def 1 2GatesCircOutput (x,y,c,'xor'); coherence 2GatesCircOutput (x,y,c,'xor') is Element of InnerVertices (2GatesCircStr (x,y,c,'xor')) ; end; :: deftheorem defines BitSubtracterOutput FSCIRC_1:def_1_:_ for x, y, c being set holds BitSubtracterOutput (x,y,c) = 2GatesCircOutput (x,y,c,'xor'); definition let x, y, c be set ; func BitSubtracterCirc (x,y,c) -> strict gate`2=den Boolean Circuit of 2GatesCircStr (x,y,c,'xor') equals :: FSCIRC_1:def 2 2GatesCircuit (x,y,c,'xor'); coherence 2GatesCircuit (x,y,c,'xor') is strict gate`2=den Boolean Circuit of 2GatesCircStr (x,y,c,'xor') ; end; :: deftheorem defines BitSubtracterCirc FSCIRC_1:def_2_:_ for x, y, c being set holds BitSubtracterCirc (x,y,c) = 2GatesCircuit (x,y,c,'xor'); definition let x, y, c be set ; func BorrowIStr (x,y,c) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: FSCIRC_1:def 3 ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)); correctness coherence ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ; ; end; :: deftheorem defines BorrowIStr FSCIRC_1:def_3_:_ for x, y, c being set holds BorrowIStr (x,y,c) = ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)); definition let x, y, c be set ; func BorrowStr (x,y,c) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: FSCIRC_1:def 4 (BorrowIStr (x,y,c)) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)); correctness coherence (BorrowIStr (x,y,c)) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ; ; end; :: deftheorem defines BorrowStr FSCIRC_1:def_4_:_ for x, y, c being set holds BorrowStr (x,y,c) = (BorrowIStr (x,y,c)) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)); definition let x, y, c be set ; func BorrowICirc (x,y,c) -> strict gate`2=den Boolean Circuit of BorrowIStr (x,y,c) equals :: FSCIRC_1:def 5 ((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2))) +* (1GateCircuit (x,c,and2a)); coherence ((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2))) +* (1GateCircuit (x,c,and2a)) is strict gate`2=den Boolean Circuit of BorrowIStr (x,y,c) ; end; :: deftheorem defines BorrowICirc FSCIRC_1:def_5_:_ for x, y, c being set holds BorrowICirc (x,y,c) = ((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2))) +* (1GateCircuit (x,c,and2a)); theorem Th1: :: FSCIRC_1:1 for x, y, c being set holds InnerVertices (BorrowStr (x,y,c)) is Relation proofend; theorem Th2: :: FSCIRC_1:2 for x, y, c being non pair set holds InputVertices (BorrowStr (x,y,c)) is without_pairs proofend; theorem :: FSCIRC_1:3 for x, y, c being set for s being State of (BorrowICirc (x,y,c)) for a, b being Element of BOOLEAN st a = s . x & b = s . y holds (Following s) . [<*x,y*>,and2a] = ('not' a) '&' b proofend; theorem :: FSCIRC_1:4 for x, y, c being set for s being State of (BorrowICirc (x,y,c)) for a, b being Element of BOOLEAN st a = s . y & b = s . c holds (Following s) . [<*y,c*>,and2] = a '&' b proofend; theorem :: FSCIRC_1:5 for x, y, c being set for s being State of (BorrowICirc (x,y,c)) for a, b being Element of BOOLEAN st a = s . x & b = s . c holds (Following s) . [<*x,c*>,and2a] = ('not' a) '&' b proofend; definition let x, y, c be set ; func BorrowOutput (x,y,c) -> Element of InnerVertices (BorrowStr (x,y,c)) equals :: FSCIRC_1:def 6 [<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3]; coherence [<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3] is Element of InnerVertices (BorrowStr (x,y,c)) proofend; correctness ; end; :: deftheorem defines BorrowOutput FSCIRC_1:def_6_:_ for x, y, c being set holds BorrowOutput (x,y,c) = [<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3]; definition let x, y, c be set ; func BorrowCirc (x,y,c) -> strict gate`2=den Boolean Circuit of BorrowStr (x,y,c) equals :: FSCIRC_1:def 7 (BorrowICirc (x,y,c)) +* (1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3)); coherence (BorrowICirc (x,y,c)) +* (1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3)) is strict gate`2=den Boolean Circuit of BorrowStr (x,y,c) ; end; :: deftheorem defines BorrowCirc FSCIRC_1:def_7_:_ for x, y, c being set holds BorrowCirc (x,y,c) = (BorrowICirc (x,y,c)) +* (1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3)); theorem Th6: :: FSCIRC_1:6 for x, y, c being set holds ( x in the carrier of (BorrowStr (x,y,c)) & y in the carrier of (BorrowStr (x,y,c)) & c in the carrier of (BorrowStr (x,y,c)) ) proofend; theorem Th7: :: FSCIRC_1:7 for x, y, c being set holds ( [<*x,y*>,and2a] in InnerVertices (BorrowStr (x,y,c)) & [<*y,c*>,and2] in InnerVertices (BorrowStr (x,y,c)) & [<*x,c*>,and2a] in InnerVertices (BorrowStr (x,y,c)) ) proofend; theorem Th8: :: FSCIRC_1:8 for x, y, c being non pair set holds ( x in InputVertices (BorrowStr (x,y,c)) & y in InputVertices (BorrowStr (x,y,c)) & c in InputVertices (BorrowStr (x,y,c)) ) proofend; theorem Th9: :: FSCIRC_1:9 for x, y, c being non pair set holds ( InputVertices (BorrowStr (x,y,c)) = {x,y,c} & InnerVertices (BorrowStr (x,y,c)) = {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} \/ {(BorrowOutput (x,y,c))} ) proofend; Lm1: for x, y, c being non pair set for s being State of (BorrowCirc (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*>,and2a] = ('not' a1) '&' a2 & (Following s) . [<*y,c*>,and2] = a2 '&' a3 & (Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3 ) proofend; theorem :: FSCIRC_1:10 for x, y, c being non pair set for s being State of (BorrowCirc (x,y,c)) for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . y holds (Following s) . [<*x,y*>,and2a] = ('not' a1) '&' a2 proofend; theorem :: FSCIRC_1:11 for x, y, c being non pair set for s being State of (BorrowCirc (x,y,c)) for a2, a3 being Element of BOOLEAN st a2 = s . y & a3 = s . c holds (Following s) . [<*y,c*>,and2] = a2 '&' a3 proofend; theorem :: FSCIRC_1:12 for x, y, c being non pair set for s being State of (BorrowCirc (x,y,c)) for a1, a3 being Element of BOOLEAN st a1 = s . x & a3 = s . c holds (Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3 proofend; theorem Th13: :: FSCIRC_1:13 for x, y, c being non pair set for s being State of (BorrowCirc (x,y,c)) for a1, a2, a3 being Element of BOOLEAN st a1 = s . [<*x,y*>,and2a] & a2 = s . [<*y,c*>,and2] & a3 = s . [<*x,c*>,and2a] holds (Following s) . (BorrowOutput (x,y,c)) = (a1 'or' a2) 'or' a3 proofend; Lm2: for x, y, c being non pair set for s being State of (BorrowCirc (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)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) & (Following (s,2)) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following (s,2)) . [<*y,c*>,and2] = a2 '&' a3 & (Following (s,2)) . [<*x,c*>,and2a] = ('not' a1) '&' a3 ) proofend; theorem :: FSCIRC_1:14 for x, y, c being non pair set for s being State of (BorrowCirc (x,y,c)) for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . y holds (Following (s,2)) . [<*x,y*>,and2a] = ('not' a1) '&' a2 proofend; theorem :: FSCIRC_1:15 for x, y, c being non pair set for s being State of (BorrowCirc (x,y,c)) for a2, a3 being Element of BOOLEAN st a2 = s . y & a3 = s . c holds (Following (s,2)) . [<*y,c*>,and2] = a2 '&' a3 proofend; theorem :: FSCIRC_1:16 for x, y, c being non pair set for s being State of (BorrowCirc (x,y,c)) for a1, a3 being Element of BOOLEAN st a1 = s . x & a3 = s . c holds (Following (s,2)) . [<*x,c*>,and2a] = ('not' a1) '&' a3 proofend; theorem :: FSCIRC_1:17 for x, y, c being non pair set for s being State of (BorrowCirc (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)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) by Lm2; theorem Th18: :: FSCIRC_1:18 for x, y, c being non pair set for s being State of (BorrowCirc (x,y,c)) holds Following (s,2) is stable proofend; begin definition let x, y, c be set ; func BitSubtracterWithBorrowStr (x,y,c) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: FSCIRC_1:def 8 (2GatesCircStr (x,y,c,'xor')) +* (BorrowStr (x,y,c)); coherence (2GatesCircStr (x,y,c,'xor')) +* (BorrowStr (x,y,c)) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ; end; :: deftheorem defines BitSubtracterWithBorrowStr FSCIRC_1:def_8_:_ for x, y, c being set holds BitSubtracterWithBorrowStr (x,y,c) = (2GatesCircStr (x,y,c,'xor')) +* (BorrowStr (x,y,c)); theorem Th19: :: FSCIRC_1:19 for x, y, c being non pair set holds InputVertices (BitSubtracterWithBorrowStr (x,y,c)) = {x,y,c} proofend; theorem :: FSCIRC_1:20 for x, y, c being non pair set holds InnerVertices (BitSubtracterWithBorrowStr (x,y,c)) = ({[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} \/ {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]}) \/ {(BorrowOutput (x,y,c))} proofend; theorem :: FSCIRC_1:21 for x, y, c being set for S being non empty ManySortedSign st S = BitSubtracterWithBorrowStr (x,y,c) holds ( x in the carrier of S & y in the carrier of S & c in the carrier of S ) proofend; definition let x, y, c be set ; func BitSubtracterWithBorrowCirc (x,y,c) -> strict gate`2=den Boolean Circuit of BitSubtracterWithBorrowStr (x,y,c) equals :: FSCIRC_1:def 9 (BitSubtracterCirc (x,y,c)) +* (BorrowCirc (x,y,c)); coherence (BitSubtracterCirc (x,y,c)) +* (BorrowCirc (x,y,c)) is strict gate`2=den Boolean Circuit of BitSubtracterWithBorrowStr (x,y,c) ; end; :: deftheorem defines BitSubtracterWithBorrowCirc FSCIRC_1:def_9_:_ for x, y, c being set holds BitSubtracterWithBorrowCirc (x,y,c) = (BitSubtracterCirc (x,y,c)) +* (BorrowCirc (x,y,c)); theorem :: FSCIRC_1:22 for x, y, c being set holds InnerVertices (BitSubtracterWithBorrowStr (x,y,c)) is Relation proofend; theorem :: FSCIRC_1:23 for x, y, c being non pair set holds InputVertices (BitSubtracterWithBorrowStr (x,y,c)) is without_pairs proofend; theorem :: FSCIRC_1:24 for x, y, c being non pair set for s being State of (BitSubtracterWithBorrowCirc (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)) . (BitSubtracterOutput (x,y,c)) = (a1 'xor' a2) 'xor' a3 & (Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) ) proofend; theorem :: FSCIRC_1:25 for x, y, c being non pair set for s being State of (BitSubtracterWithBorrowCirc (x,y,c)) holds Following (s,2) is stable proofend;