:: Full Subtracter Circuit. Part {II} :: by Shin'nosuke Yamaguchi , Grzegorz Bancerek and Katsumi Wasaki :: :: Received February 25, 2003 :: Copyright (c) 2003-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, NAT_1, FINSEQ_1, FSCIRC_1, FUNCT_1, ARYTM_3, XBOOLE_0, MSUALG_1, FUNCT_4, CIRCCOMB, CARD_1, FINSEQ_2, MARGREL1, FUNCOP_1, XBOOLEAN, STRUCT_0, PBOOLE, LATTICES, CIRCUIT1, RELAT_1, SUBSET_1, MSAFREE2, ORDINAL4, XXREAL_0, TARSKI, TWOSCOMP, PARTFUN1, FACIRC_1, CLASSES1, MCART_1, FSM_1, CIRCUIT2, GLIB_000, FSCIRC_2, FUNCT_7; notations TARSKI, XBOOLE_0, ENUMSET1, XTUPLE_0, XFAMILY, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, MCART_1, RELAT_1, STRUCT_0, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FUNCT_7, PBOOLE, FUNCOP_1, MARGREL1, BINARITH, CLASSES1, MSUALG_1, MSAFREE2, CIRCUIT1, CIRCUIT2, CIRCCOMB, TWOSCOMP, FACIRC_1, FACIRC_2, FSCIRC_1, XXREAL_0; constructors ENUMSET1, CLASSES1, BINARITH, CIRCUIT1, CIRCUIT2, TWOSCOMP, FSCIRC_1, NAT_1, RELSET_1, XTUPLE_0, XREAL_0, NUMBERS, FUNCT_7, XFAMILY, FUNCOP_1; registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, NAT_1, FINSEQ_1, MARGREL1, CARD_3, STRUCT_0, CIRCCOMB, FACIRC_1, CIRCCMB2, FACIRC_2, MSAFREE2, FINSET_1, CARD_1, XTUPLE_0; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin ::------------------------------------------------------------ :: Definitions of n-Bit Full Subtracter Structure and Circuit ::------------------------------------------------------------ definition let n be Nat; let x,y be FinSequence; func n-BitSubtracterStr(x,y) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign means :: FSCIRC_2:def 1 ex f,g being ManySortedSet of NAT st it = f.n & f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) & g.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] & for n being Nat, S being non empty ManySortedSign, z be set st S = f.n & z = g.n holds f.(n+1) = S +* BitSubtracterWithBorrowStr(x .(n+1), y.(n+1), z) & g.(n+1) = BorrowOutput(x .(n+1), y.(n+1), z); end; definition let n be Nat; let x,y be FinSequence; func n-BitSubtracterCirc(x,y) -> Boolean gate`2=den strict Circuit of n-BitSubtracterStr(x,y) means :: FSCIRC_2:def 2 ex f,g,h being ManySortedSet of NAT st n-BitSubtracterStr(x,y) = f.n & it = g.n & f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) & g.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->TRUE) & h.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] & for n being Nat, S being non empty ManySortedSign, 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 +* BitSubtracterWithBorrowStr(x .(n+1), y.(n+1), z) & g.(n+1) = A +* BitSubtracterWithBorrowCirc(x .(n+1), y.(n+1), z) & h.(n+1) = BorrowOutput(x .(n+1), y.(n+1), z); end; definition let n be Nat; let x,y be FinSequence; func n-BitBorrowOutput(x,y) -> Element of InnerVertices (n-BitSubtracterStr(x,y)) means :: FSCIRC_2:def 3 ex h being ManySortedSet of NAT st it = h.n & h.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] & for n being Nat holds h.(n+1) = BorrowOutput(x .(n+1), y.(n+1), h.n); end; ::------------------------------------------------------------ :: Properties of n-Bit Full Subtracter Structure and Circuit ::------------------------------------------------------------ theorem :: FSCIRC_2:1 for x,y being FinSequence, f,g,h being ManySortedSet of NAT st f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) & g.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->TRUE) & h.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] & for n being Nat, S being non empty ManySortedSign, 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 +* BitSubtracterWithBorrowStr(x .(n+1), y.(n+1), z) & g.(n+1) = A +* BitSubtracterWithBorrowCirc(x .(n+1), y.(n+1), z) & h.(n+1) = BorrowOutput(x .(n+1), y.(n+1), z) for n being Nat holds n-BitSubtracterStr(x,y) = f.n & n-BitSubtracterCirc(x,y) = g.n & n-BitBorrowOutput(x,y) = h.n; theorem :: FSCIRC_2:2 for a,b being FinSequence holds 0-BitSubtracterStr(a,b) = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) & 0-BitSubtracterCirc(a,b) = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->TRUE) & 0-BitBorrowOutput(a,b) = [<*>, (0-tuples_on BOOLEAN)-->TRUE]; theorem :: FSCIRC_2:3 for a,b being FinSequence, c being set st c = [<*>, (0-tuples_on BOOLEAN)-->TRUE] holds 1-BitSubtracterStr(a,b) = 1GateCircStr(<*>, (0-tuples_on BOOLEAN)-->TRUE)+* BitSubtracterWithBorrowStr(a.1, b.1, c) & 1-BitSubtracterCirc(a,b) = 1GateCircuit(<*>, (0-tuples_on BOOLEAN)-->TRUE)+* BitSubtracterWithBorrowCirc(a.1, b.1, c) & 1-BitBorrowOutput(a,b) = BorrowOutput(a.1, b.1, c); theorem :: FSCIRC_2:4 ::Col002a: for a,b,c being set st c = [<*>, (0-tuples_on BOOLEAN)-->TRUE] holds 1-BitSubtracterStr(<*a*>,<*b*>) = 1GateCircStr(<*>, (0-tuples_on BOOLEAN)-->TRUE) +* BitSubtracterWithBorrowStr(a, b, c) & 1-BitSubtracterCirc(<*a*>,<*b*>) = 1GateCircuit(<*>, (0-tuples_on BOOLEAN)-->TRUE) +* BitSubtracterWithBorrowCirc(a, b, c) & 1-BitBorrowOutput(<*a*>,<*b*>) = BorrowOutput(a, b, c); theorem :: FSCIRC_2:5 for n be Nat for p,q being FinSeqLen of n for p1,p2, q1,q2 being FinSequence holds n-BitSubtracterStr(p^p1, q^q1) = n-BitSubtracterStr(p^p2, q^q2) & n-BitSubtracterCirc(p^p1, q^q1) = n-BitSubtracterCirc(p^p2, q^q2) & n-BitBorrowOutput(p^p1, q^q1) = n-BitBorrowOutput(p^p2, q^q2); theorem :: FSCIRC_2:6 ::Col002b: for n be Element of NAT for x,y being FinSeqLen of n for a,b being set holds (n+1)-BitSubtracterStr(x^<*a*>, y^<*b*>) = n-BitSubtracterStr(x, y) +* BitSubtracterWithBorrowStr(a, b, n-BitBorrowOutput(x, y)) & (n+1)-BitSubtracterCirc(x^<*a*>, y^<*b*>) = n-BitSubtracterCirc(x, y) +* BitSubtracterWithBorrowCirc(a, b, n-BitBorrowOutput(x, y)) & (n+1)-BitBorrowOutput(x^<*a*>, y^<*b*>) = BorrowOutput(a, b, n-BitBorrowOutput(x, y)); theorem :: FSCIRC_2:7 for n be Nat for x,y being FinSequence holds (n+1)-BitSubtracterStr(x, y) = n-BitSubtracterStr(x, y) +* BitSubtracterWithBorrowStr(x .(n+1), y.(n+1), n-BitBorrowOutput(x, y)) & (n+1)-BitSubtracterCirc(x, y) = n-BitSubtracterCirc(x, y) +* BitSubtracterWithBorrowCirc(x .(n+1), y.(n+1), n-BitBorrowOutput(x, y)) & (n+1)-BitBorrowOutput(x, y) = BorrowOutput(x .(n+1), y.(n+1), n-BitBorrowOutput(x, y)); ::------------------------------------------------------------ :: Inner and Input-Vertex of n-Bit Full Subtracter Structure ::------------------------------------------------------------ theorem :: FSCIRC_2:8 for n,m be Nat st n <= m for x,y being FinSequence holds InnerVertices (n-BitSubtracterStr(x,y)) c= InnerVertices (m-BitSubtracterStr(x,y)); theorem :: FSCIRC_2:9 for n be Element of NAT for x,y being FinSequence holds InnerVertices ((n+1)-BitSubtracterStr(x,y)) = InnerVertices (n-BitSubtracterStr(x,y)) \/ InnerVertices BitSubtracterWithBorrowStr(x .(n+1), y.(n+1), n-BitBorrowOutput(x,y)); definition let k,n be Nat such that k >= 1 and k <= n; let x,y be FinSequence; func (k,n)-BitSubtracterOutput(x,y) -> Element of InnerVertices (n-BitSubtracterStr(x,y)) means :: FSCIRC_2:def 4 ex i being Element of NAT st k = i+1 & it = BitSubtracterOutput(x .k, y.k, i-BitBorrowOutput(x,y)); end; theorem :: FSCIRC_2:10 for n,k being Element of NAT st k < n for x,y being FinSequence holds (k+1,n)-BitSubtracterOutput(x,y) = BitSubtracterOutput(x .(k+1), y.(k+1), k-BitBorrowOutput(x,y)); theorem :: FSCIRC_2:11 for n being Element of NAT for x,y being FinSequence holds InnerVertices (n-BitSubtracterStr(x,y)) is Relation; theorem :: FSCIRC_2:12 for x,y,c being set holds InnerVertices BorrowIStr(x,y,c) = {[<*x,y*>,and2a], [<*y,c*>,and2], [<*x,c*>,and2a]}; theorem :: FSCIRC_2:13 for x,y,c being set st x <> [<*y,c*>, and2] & y <> [<*x,c*>, and2a] & c <> [<*x,y*>, and2a] holds InputVertices BorrowIStr(x,y,c) = {x,y,c}; theorem :: FSCIRC_2:14 for x,y,c being set holds InnerVertices BorrowStr(x,y,c) = {[<*x,y*>,and2a], [<*y,c*>,and2], [<*x,c*>,and2a]} \/ {BorrowOutput(x,y,c)}; theorem :: FSCIRC_2:15 for x,y,c being set st x <> [<*y,c*>, and2] & y <> [<*x,c*>, and2a] & c <> [<*x,y*>, and2a] holds InputVertices BorrowStr(x,y,c) = {x,y,c}; theorem :: FSCIRC_2:16 for x,y,c being set st x <> [<*y,c*>, and2] & y <> [<*x,c*>, and2a] & c <> [<*x,y*>, and2a] & c <> [<*x,y*>, 'xor'] holds InputVertices BitSubtracterWithBorrowStr(x,y,c) = {x,y,c}; theorem :: FSCIRC_2:17 for x,y,c being 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)}; registration let n be Nat; let x,y be FinSequence; cluster n-BitBorrowOutput(x,y) -> pair; end; theorem :: FSCIRC_2:18 for x,y being FinSequence, n being Nat holds (n-BitBorrowOutput(x,y))`1 = <*> & (n-BitBorrowOutput(x,y))`2 = (0-tuples_on BOOLEAN)-->TRUE & proj1 (n-BitBorrowOutput(x,y))`2 = 0-tuples_on BOOLEAN or card (n-BitBorrowOutput(x,y))`1 = 3 & (n-BitBorrowOutput(x,y))`2 = or3 & proj1 (n-BitBorrowOutput(x,y))`2 = 3-tuples_on BOOLEAN; theorem :: FSCIRC_2:19 for n being Nat, x,y being FinSequence, p being set holds n-BitBorrowOutput(x,y) <> [p, and2] & n-BitBorrowOutput(x,y) <> [p, and2a] & n-BitBorrowOutput(x,y) <> [p, 'xor']; ::----------------------------------------------------- :: Relation and Pair for n-Bit Full Subtracter ::----------------------------------------------------- theorem :: FSCIRC_2:20 for f,g being nonpair-yielding FinSequence for n being Nat holds InputVertices ((n+1)-BitSubtracterStr(f,g)) = (InputVertices (n-BitSubtracterStr(f,g)))\/ ((InputVertices BitSubtracterWithBorrowStr(f.(n+1),g.(n+1), n-BitBorrowOutput(f,g)) \ {n-BitBorrowOutput(f,g)})) & InnerVertices (n-BitSubtracterStr(f,g)) is Relation & InputVertices (n-BitSubtracterStr(f,g)) is without_pairs; theorem :: FSCIRC_2:21 for n being Nat for x,y being nonpair-yielding FinSeqLen of n holds InputVertices (n-BitSubtracterStr(x,y)) = rng x \/ rng y; theorem :: FSCIRC_2:22 for x,y,c being 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; theorem :: FSCIRC_2:23 for x,y,c being set st x <> [<*y,c*>, and2] & y <> [<*x,c*>, and2a] & c <> [<*x,y*>, and2a] for s being State of BorrowCirc(x,y,c) holds Following(s,2) is stable; theorem :: FSCIRC_2:24 for x,y,c being set st x <> [<*y,c*>, and2] & y <> [<*x,c*>, and2a] & c <> [<*x,y*>, and2a] & c <> [<*x,y*>, 'xor'] 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; theorem :: FSCIRC_2:25 for x,y,c being set st x <> [<*y,c*>, and2] & y <> [<*x,c*>, and2a] & c <> [<*x,y*>, and2a] & c <> [<*x,y*>, 'xor'] for s being State of BitSubtracterWithBorrowCirc(x,y,c) holds Following(s,2) is stable; theorem :: FSCIRC_2:26 for n being Element of NAT for x,y being nonpair-yielding FinSeqLen of n for s being State of n-BitSubtracterCirc(x,y) holds Following(s,1+2*n) is stable;