Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999 Association of Mizar Users

### Full Subtracter Circuit. Part I

by
Katsumi Wasaki, and
Noboru Endou

MML identifier: FSCIRC_1
[ Mizar article, MML identifier index ]

```environ

vocabulary FUNCT_1, RELAT_1, FINSEQ_1, BOOLE, MSAFREE2, FACIRC_1, BINARITH,
LATTICES, CIRCCOMB, CIRCUIT1, AMI_1, MSUALG_1, TWOSCOMP, FUNCT_4,
PARTFUN1, MARGREL1, ZF_LANG, CIRCUIT2, FSCIRC_1;
notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, RELAT_1, FUNCT_1, STRUCT_0,
MARGREL1, NAT_1, MSUALG_1, MSAFREE2, CIRCUIT1, CIRCUIT2, CIRCCOMB,
TWOSCOMP, FACIRC_1, BINARITH;
constructors BINARITH, CIRCUIT1, CIRCUIT2, ENUMSET1, FACIRC_1, TWOSCOMP;
clusters STRUCT_0, RELSET_1, MSUALG_1, PRE_CIRC, CIRCCOMB, FACIRC_1;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;

begin :: Bit Subtract and Borrow Circuit

reserve x,y,c for set;

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');
end;

definition
let x,y,c be set;
func BitSubtracterCirc(x,y,c) ->
strict Boolean gate`2=den Circuit of 2GatesCircStr(x,y,c, 'xor') equals
:: FSCIRC_1:def 2

2GatesCircuit(x,y,c, 'xor');
end;

definition
let x,y,c be set;
func BorrowIStr(x,y,c) ->
unsplit gate`1=arity gate`2isBoolean
non void strict non empty ManySortedSign equals
:: FSCIRC_1:def 3

1GateCircStr(<*x,y*>, and2a) +* 1GateCircStr(<*y,c*>, and2) +*
1GateCircStr(<*x,c*>, and2a);
end;

definition
let x,y,c be set;
func BorrowStr(x,y,c) ->
unsplit gate`1=arity gate`2isBoolean
non void strict non empty ManySortedSign equals
:: FSCIRC_1:def 4

BorrowIStr(x,y,c) +*
1GateCircStr(<*[<*x,y*>, and2a], [<*y,c*>, and2], [<*x,c*>, and2a]*>, or3);
end;

definition
let x,y,c be set;
func BorrowICirc(x,y,c) ->
strict Boolean gate`2=den Circuit of BorrowIStr(x,y,c) equals
:: FSCIRC_1:def 5

1GateCircuit(x,y, and2a) +* 1GateCircuit(y,c, and2) +*
1GateCircuit(x,c, and2a);
end;

theorem :: FSCIRC_1:1
InnerVertices BorrowStr(x,y,c) is Relation;

theorem :: FSCIRC_1:2
for x,y,c being non pair set holds
InputVertices BorrowStr(x,y,c) is without_pairs;

theorem :: FSCIRC_1:3
for s being State of BorrowICirc(x,y,c), a,b being Element of BOOLEAN
st a = s.x & b = s.y holds (Following s).[<*x,y*>,and2a] = 'not' a '&' b;

theorem :: FSCIRC_1:4
for s being State of BorrowICirc(x,y,c), a,b being Element of BOOLEAN
st a = s.y & b = s.c holds (Following s).[<*y,c*>, and2] = a '&' b;

theorem :: FSCIRC_1:5
for s being State of BorrowICirc(x,y,c), a,b being Element of BOOLEAN
st a = s.x & b = s.c holds (Following s).[<*x,c*>, and2a] = 'not' a '&' b;

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];
end;

definition
let x,y,c be set;
func BorrowCirc(x,y,c) ->
strict Boolean gate`2=den 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);
end;

theorem :: FSCIRC_1:6
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);

theorem :: FSCIRC_1:7
[<*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);

theorem :: 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);

theorem :: 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)}
;

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;

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;

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;

theorem :: 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;

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;

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;

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;

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;

theorem :: 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;

begin :: Bit Subtracter with Borrow Circuit

definition
let x,y,c be set;
func BitSubtracterWithBorrowStr(x,y,c) ->
unsplit gate`1=arity gate`2isBoolean
non void strict non empty ManySortedSign
equals
:: FSCIRC_1:def 8

2GatesCircStr(x,y,c, 'xor') +* BorrowStr(x,y,c);
end;

theorem :: FSCIRC_1:19
for x,y,c being non pair set holds
InputVertices BitSubtracterWithBorrowStr(x,y,c) = {x,y,c};

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)};

theorem :: FSCIRC_1:21
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;

definition
let x,y,c be set;
func BitSubtracterWithBorrowCirc(x,y,c) ->
strict Boolean gate`2=den Circuit of BitSubtracterWithBorrowStr(x,y,c)
equals
:: FSCIRC_1:def 9

BitSubtracterCirc(x,y,c) +* BorrowCirc(x,y,c);
end;

theorem :: FSCIRC_1:22
InnerVertices BitSubtracterWithBorrowStr(x,y,c) is Relation;

theorem :: FSCIRC_1:23
for x,y,c being non pair set holds
InputVertices BitSubtracterWithBorrowStr(x,y,c) is without_pairs;

theorem :: FSCIRC_1:24
BitSubtracterOutput(x,y,c) in
InnerVertices BitSubtracterWithBorrowStr(x,y,c) &
BorrowOutput(x,y,c) in InnerVertices BitSubtracterWithBorrowStr(x,y,c);

theorem :: FSCIRC_1:25
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;

theorem :: FSCIRC_1:26
for x,y,c being non pair set
for s being State of BitSubtracterWithBorrowCirc(x,y,c)
holds Following(s,2) is stable;
```