:: Full Subtracter Circuit. Part { I }
:: by Katsumi Wasaki and Noboru Endou
::
:: Received March 13, 1999
:: Copyright (c) 1999-2021 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 InputVertices (BorrowStr (x,y,c)) is without_pairs
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 InputVertices (BitSubtracterWithBorrowStr (x,y,c)) is without_pairs
proof end;

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