:: Full Subtracter Circuit. Part { I }
:: by Katsumi Wasaki and Noboru Endou
::
:: Received March 13, 1999
:: Copyright (c) 1999 Association of Mizar Users

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

proof end;

theorem Th2: :: FSCIRC_1:2

for x, y, c being non pair set holds not InputVertices (BorrowStr x,y,c) is with_pair

proof end;

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

proof end;

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

proof end;

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

proof end;

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)

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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 )

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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 )

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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}

proof end;

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

proof end;

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 )

proof end;

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

proof end;

theorem :: FSCIRC_1:23

for x, y, c being non pair set holds not InputVertices (BitSubtracterWithBorrowStr x,y,c) is with_pair

proof end;

theorem :: FSCIRC_1:24

canceled;

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

proof end;

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

proof end;