:: Full Subtracter Circuit. Part { I }
:: by Katsumi Wasaki and Noboru Endou
::
:: Received March 13, 1999
:: Copyright (c) 1999-2011 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

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;

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}

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;