The Mizar abstract of FSCIRC

Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users
The abstract of the Mizar article:: Full Subtracter Circuit. Part II
by
Shin'nosuke Yamaguchi,
Grzegorz Bancerek, and
Katsumi Wasaki
Received February 25, 2003
MML identifier: FSCIRC_2
[ Mizar article, MML identifier index ]
environ

 vocabulary BOOLE, MCART_1, RELAT_1, AMI_1, CARD_1, FUNCT_1, FINSEQ_1,
      FINSEQ_2, FUNCT_4, FUNCT_5, FUNCOP_1, PBOOLE, MARGREL1, BINARITH,
      CLASSES1, PARTFUN1, MSUALG_1, MSAFREE2, CIRCUIT1, CIRCUIT2, LATTICES,
      CIRCCOMB, FACIRC_1, ZF_REFLE, ZF_LANG, TWOSCOMP, FSCIRC_1, FSCIRC_2;
 notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, NUMBERS, XREAL_0, NAT_1,
      MCART_1, RELAT_1, CARD_1, STRUCT_0, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2,
      FUNCT_5, PBOOLE, MARGREL1, BINARITH, CLASSES1, MSUALG_1, MSAFREE2,
      CIRCUIT1, CIRCUIT2, CIRCCOMB, TWOSCOMP, FACIRC_1, FACIRC_2, FSCIRC_1;
 constructors ENUMSET1, MCART_1, CLASSES1, FUNCT_5, CIRCUIT1, CIRCUIT2,
      TWOSCOMP, FSCIRC_1, BINARITH, FACIRC_2;
 clusters RELSET_1, FINSEQ_2, MARGREL1, MSUALG_1, PRE_CIRC, CIRCCOMB, FACIRC_1,
      STRUCT_0, RELAT_1, CIRCCMB2, FACIRC_2, MEMBERED, ORDINAL2;
 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 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 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 & 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 Nat st k = i+1 &
   it = BitSubtracterOutput(x .k, y.k, i-BitBorrowOutput(x,y));
end;

theorem :: FSCIRC_2:10
   for n,k being 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 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)};

definition
 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] &
   c <> [<*x,y*>, 'xor']
 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 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;
The abstract of the Mizar article:

Full Subtracter Circuit. Part II
