:: Full Subtracter Circuit. Part { I }
:: by Katsumi Wasaki and Noboru Endou
::
:: Received March 13, 1999
:: Copyright (c) 1999-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies SUBSET_1, MSAFREE2, FACIRC_1, XBOOLEAN, STRUCT_0, LATTICES,
CIRCCOMB, CIRCUIT1, XBOOLE_0, MSUALG_1, FINSEQ_1, TWOSCOMP, FUNCT_4,
RELAT_1, PARTFUN1, FSM_1, MARGREL1, FUNCT_1, CIRCUIT2, GLIB_000, ARYTM_3,
FSCIRC_1;
notations TARSKI, XBOOLE_0, ENUMSET1, XTUPLE_0, SUBSET_1, RELAT_1, FUNCT_1,
FINSEQ_1, STRUCT_0, MARGREL1, NAT_1, MSUALG_1, MSAFREE2, CIRCUIT1,
CIRCUIT2, CIRCCOMB, TWOSCOMP, FACIRC_1, BINARITH;
constructors ENUMSET1, BINARITH, CIRCUIT1, CIRCUIT2, FACIRC_1, TWOSCOMP,
NAT_1, RELSET_1, XTUPLE_0;
registrations RELSET_1, CARD_3, STRUCT_0, CIRCCOMB, FACIRC_1, ORDINAL1,
FINSEQ_1, FUNCT_1, MSAFREE2, XTUPLE_0;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;
definitions CIRCUIT2, FACIRC_1;
equalities FACIRC_1, MSAFREE2;
expansions CIRCUIT2, FACIRC_1;
theorems TARSKI, ENUMSET1, RELAT_1, FUNCT_1, FINSEQ_2, CIRCUIT1, CIRCUIT2,
CIRCCOMB, FACIRC_1, TWOSCOMP, XBOOLE_0, XBOOLE_1;
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
2GatesCircOutput(x,y,c, 'xor');
coherence;
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
2GatesCircuit(x,y,c, 'xor');
coherence;
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
1GateCircStr(<*x,y*>, and2a) +*
1GateCircStr(<*y,c*>, and2) +* 1GateCircStr(<*x,c*>, and2a);
correctness;
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
BorrowIStr(x,y,c) +* 1GateCircStr(<*[<*x
,y*>, and2a], [<*y,c*>, and2], [<*x,c*>, and2a]*>, or3);
correctness;
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
1GateCircuit(x,y, and2a) +* 1GateCircuit(y,c, and2) +*
1GateCircuit(x,c, and2a);
coherence;
end;
theorem Th1:
InnerVertices BorrowStr(x,y,c) is Relation
proof
InnerVertices 1GateCircStr(<*x,y*>,and2a) is Relation & InnerVertices
1GateCircStr(<*y,c*>,and2) is Relation by FACIRC_1:38;
then
InnerVertices 1GateCircStr(<*x,c*>,and2a) is Relation & InnerVertices (
1GateCircStr(<*x,y*>,and2a)+*1GateCircStr(<*y,c*>,and2 )) is Relation by
FACIRC_1:3,38;
then
InnerVertices 1GateCircStr(<*[<*x,y*>, and2a], [<*y,c*>, and2], [<*x,c*>
, and2a]*>, or3) is Relation & InnerVertices BorrowIStr(x,y,c) is Relation
by FACIRC_1:3,38;
hence thesis by FACIRC_1:3;
end;
theorem Th2:
for x,y,c being non pair set holds InputVertices BorrowStr(x,y,c)
is without_pairs
proof
let x,y,c be non pair set;
set M = BorrowStr(x,y,c), MI = BorrowIStr(x,y,c);
set S = 1GateCircStr(<*[<*x,y*>, and2a], [<*y,c*>, and2], [<*x,c*>, and2a]*>
, or3);
given xx being pair object such that
A1: xx in InputVertices M;
A2: 1GateCircStr(<*x,y*>, and2a) tolerates 1GateCircStr(<*y,c*>, and2) by
CIRCCOMB:47;
A3: InnerVertices 1GateCircStr(<*x,c*>, and2a) = {[<*x,c*>, and2a]} &
1GateCircStr(<*x,y*>,and2a) +* 1GateCircStr(<*y,c*>,and2) tolerates
1GateCircStr(<*x,c*>,and2a) by CIRCCOMB:42,47;
InnerVertices 1GateCircStr(<*x,y*>, and2a) = {[<*x,y*>, and2a]} &
InnerVertices 1GateCircStr(<*y,c*>, and2) = {[<*y,c*>, and2]} by CIRCCOMB:42;
then
InnerVertices (1GateCircStr(<*x,y*>,and2a) +* 1GateCircStr(<*y,c*>,and2
)) = {[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]} by A2,CIRCCOMB:11;
then
A4: InnerVertices MI = {[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]} \/ {[<*x,c*>,
and2a]} by A3,CIRCCOMB:11
.= {[<*x,y*>,and2a], [<*y,c*>,and2]} \/ {[<*x,c*>,and2a]} by ENUMSET1:1
.= {[<*x,y*>,and2a], [<*y,c*>,and2], [<*x,c*>,and2a]} by ENUMSET1:3;
InputVertices S = {[<*x,y*>,and2a], [<*y,c*>,and2], [<*x,c*>,and2a]} by
FACIRC_1:42;
then
A5: InputVertices S \ InnerVertices MI = {} by A4,XBOOLE_1:37;
InputVertices 1GateCircStr(<*x,y*>,and2a) is without_pairs &
InputVertices 1GateCircStr(<*y,c*>,and2) is without_pairs by FACIRC_1:41;
then InputVertices 1GateCircStr(<*x,c*>,and2a) is without_pairs &
InputVertices ( 1GateCircStr(<*x,y*>,and2a)+*1GateCircStr(<*y,c*>,and2 )) is
without_pairs by FACIRC_1:9,41;
then
A6: InputVertices MI is without_pairs by FACIRC_1:9;
InnerVertices S is Relation by FACIRC_1:38;
then
InputVertices M = (InputVertices MI) \/ (InputVertices S \ InnerVertices
MI) by A6,FACIRC_1:6;
hence thesis by A6,A1,A5;
end;
theorem
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
proof
set xy = <*x,y*>, yc = <*y,c*>, xc = <*x,c*>;
set S1 = 1GateCircStr(xy, and2a), A1 = 1GateCircuit(x,y, and2a);
set S2 = 1GateCircStr(yc, and2 ), A2 = 1GateCircuit(y,c, and2 );
set S3 = 1GateCircStr(xc, and2a), A3 = 1GateCircuit(x,c, and2a);
set S = BorrowIStr(x,y,c), A = BorrowICirc(x,y,c);
set v1 = [xy, and2a];
let s be State of A;
let a,b be Element of BOOLEAN such that
A1: a = s.x & b = s.y;
reconsider xx = x, yy = y as Vertex of S1 by FACIRC_1:43;
reconsider v1 as Element of InnerVertices S1 by FACIRC_1:47;
A2: S = S1+*(S2+*S3) by CIRCCOMB:6;
then reconsider v = v1 as Element of InnerVertices S by FACIRC_1:21;
A3: A = A1+*(A2+*A3) by FACIRC_1:25;
then reconsider s1 = s|the carrier of S1 as State of A1 by FACIRC_1:26;
reconsider xx, yy as Vertex of S by A2,FACIRC_1:20;
A4: dom s1 = the carrier of S1 by CIRCUIT1:3;
thus (Following s).[xy, and2a] = (Following s1).v by A2,A3,CIRCCOMB:64
.= and2a.<*s1.xx,s1.yy*> by FACIRC_1:50
.= and2a.<*s.xx,s1.yy*> by A4,FUNCT_1:47
.= and2a.<*s.xx,s.yy*> by A4,FUNCT_1:47
.= 'not' a '&' b by A1,TWOSCOMP:def 2;
end;
theorem
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
proof
set xy = <*x,y*>, yc = <*y,c*>, xc = <*x,c*>;
set S1 = 1GateCircStr(xy, and2a), A1 = 1GateCircuit(x,y, and2a);
set S2 = 1GateCircStr(yc, and2 ), A2 = 1GateCircuit(y,c, and2 );
set S3 = 1GateCircStr(xc, and2a), A3 = 1GateCircuit(x,c, and2a);
set S = BorrowIStr(x,y,c), A = BorrowICirc(x,y,c);
set v2 = [yc, and2];
let s be State of A;
let a,b be Element of BOOLEAN such that
A1: a = s.y & b = s.c;
reconsider yy = y, cc = c as Vertex of S2 by FACIRC_1:43;
reconsider v2 as Element of InnerVertices S2 by FACIRC_1:47;
A2: S1+*S2 = S2+*S1 by FACIRC_1:23;
then
A3: S = S2+*(S1+*S3) by CIRCCOMB:6;
then reconsider v = v2 as Element of InnerVertices S by FACIRC_1:21;
A1+*A2 = A2+*A1 by FACIRC_1:24;
then
A4: A = A2+*(A1+*A3) by A2,FACIRC_1:25;
then reconsider s2 = s|the carrier of S2 as State of A2 by FACIRC_1:26;
reconsider yy, cc as Vertex of S by A3,FACIRC_1:20;
A5: dom s2 = the carrier of S2 by CIRCUIT1:3;
thus (Following s).[yc, and2] = (Following s2).v by A3,A4,CIRCCOMB:64
.= and2.<*s2.yy,s2.cc*> by FACIRC_1:50
.= and2.<*s.yy,s2.cc*> by A5,FUNCT_1:47
.= and2.<*s.yy,s.cc*> by A5,FUNCT_1:47
.= a '&' b by A1,FACIRC_1:def 6;
end;
theorem
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
proof
set xc = <*x,c*>;
set S3 = 1GateCircStr(xc, and2a), A3 = 1GateCircuit(x,c, and2a);
set S = BorrowIStr(x,y,c), A = BorrowICirc(x,y,c);
set v3 = [xc, and2a];
let s be State of A;
let a,b be Element of BOOLEAN such that
A1: a = s.x & b = s.c;
reconsider xx = x, cc = c as Vertex of S3 by FACIRC_1:43;
reconsider s3 = s|the carrier of S3 as State of A3 by FACIRC_1:26;
reconsider v3 as Element of InnerVertices S3 by FACIRC_1:47;
reconsider v = v3 as Element of InnerVertices S by FACIRC_1:21;
A2: dom s3 = the carrier of S3 by CIRCUIT1:3;
reconsider xx, cc as Vertex of S by FACIRC_1:20;
thus (Following s).[xc, and2a] = (Following s3).v by CIRCCOMB:64
.= and2a.<*s3.xx,s3.cc*> by FACIRC_1:50
.= and2a.<*s.xx,s3.cc*> by A2,FUNCT_1:47
.= and2a.<*s.xx,s.cc*> by A2,FUNCT_1:47
.= 'not' a '&' b by A1,TWOSCOMP:def 2;
end;
definition
let x,y,c be set;
func BorrowOutput(x,y,c) -> Element of InnerVertices BorrowStr(x,y,c) equals
[<*[<*x,y*>,and2a], [<*y,c*>,and2], [<*x,c*>,and2a]*>, or3];
coherence
proof
[<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3] in
InnerVertices 1GateCircStr(<*[<*x,y*>,and2a], [<*y,c*>,and2], [<*x,c*>,and2a]*>
,or3) by FACIRC_1:47;
hence thesis by FACIRC_1:21;
end;
correctness;
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
BorrowICirc(x,y,c) +* 1GateCircuit([<*x,y*>,and2a],[<*y,c*>,and2],[
<*x,c*>,and2a],or3);
coherence;
end;
theorem Th6:
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
c in the carrier of 1GateCircStr(<*x,c*>,and2a) by FACIRC_1:43;
then
A1: c in the carrier of BorrowIStr(x,y,c) by FACIRC_1:20;
y in the carrier of 1GateCircStr(<*x,y*>,and2a) by FACIRC_1:43;
then y in the carrier of 1GateCircStr(<*x,y*>,and2a)+*1GateCircStr(<*y,c*>,
and2) by FACIRC_1:20;
then
A2: y in the carrier of BorrowIStr(x,y,c) by FACIRC_1:20;
x in the carrier of 1GateCircStr(<*x,c*>,and2a) by FACIRC_1:43;
then x in the carrier of BorrowIStr(x,y,c) by FACIRC_1:20;
hence thesis by A2,A1,FACIRC_1:20;
end;
theorem Th7:
[<*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
[<*x,y*>,and2a] in InnerVertices 1GateCircStr(<*x,y*>,and2a) by FACIRC_1:47;
then [<*x,y*>,and2a] in InnerVertices (1GateCircStr(<*x,y*>,and2a)+*
1GateCircStr(<*y,c*>,and2)) by FACIRC_1:21;
then
A1: [<*x,y*>,and2a] in InnerVertices BorrowIStr(x,y,c) by FACIRC_1:21;
[<*y,c*>,and2 ] in InnerVertices 1GateCircStr(<*y,c*>,and2 ) by FACIRC_1:47;
then [<*y,c*>,and2 ] in InnerVertices (1GateCircStr(<*x,y*>,and2a)+*
1GateCircStr(<*y,c*>,and2)) by FACIRC_1:21;
then
A2: [<*y,c*>,and2 ] in InnerVertices BorrowIStr(x,y,c) by FACIRC_1:21;
[<*x,c*>,and2a] in InnerVertices 1GateCircStr(<*x,c*>,and2a) by FACIRC_1:47;
then [<*x,c*>,and2a] in InnerVertices BorrowIStr(x,y,c) by FACIRC_1:21;
hence thesis by A1,A2,FACIRC_1:21;
end;
theorem Th8:
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
let x,y,c be non pair set;
assume
A1: not thesis;
A2: c in the carrier of BorrowStr(x,y,c) by Th6;
A3: InnerVertices BorrowStr(x,y,c) is Relation by Th1;
x in the carrier of BorrowStr(x,y,c) & y in the carrier of BorrowStr(x,y
,c) by Th6;
then
x in InnerVertices BorrowStr(x,y,c) or y in InnerVertices BorrowStr(x,y,
c) or c in InnerVertices BorrowStr(x,y,c) by A2,A1,XBOOLE_0:def 5;
then
(ex a1,b1 being object st x = [a1,b1]) or
(ex a1,b1 being object st y = [a1,b1
]) or ex a1,b1 being object st c = [a1,b1] by A3,RELAT_1:def 1;
hence contradiction;
end;
theorem Th9:
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
let x,y,c be non pair set;
set xy = <*x,y*>, yc = <*y,c*>, xc = <*x,c*>;
set xy1 =[xy,and2a], yc1 = [yc,and2], xc1 = [xc,and2a];
set MI = BorrowIStr(x,y,c), S = 1GateCircStr(<*xy1, yc1, xc1*>, or3);
set M = BorrowStr(x,y,c);
A1: InputVertices 1GateCircStr(<*x,y*>,and2a) = {x,y} & InputVertices
1GateCircStr(<*x,c*>,and2a) = {x,c} by FACIRC_1:40;
A2: InputVertices 1GateCircStr(<*y,c*>,and2 ) = {y,c} by FACIRC_1:40;
A3: InnerVertices 1GateCircStr(<*x,y*>,and2a) = {[<*x,y*>,and2a]} &
InnerVertices 1GateCircStr(<*y,c*>,and2) = {[<*y,c*>,and2]} by CIRCCOMB:42;
A4: InnerVertices S is Relation by FACIRC_1:38;
A5: InputVertices 1GateCircStr(<*x,y*>,and2a) is without_pairs &
InputVertices 1GateCircStr(<*y,c*>,and2) is without_pairs by FACIRC_1:41;
then
A6: InputVertices 1GateCircStr(<*x,c*>,and2a) is without_pairs &
InputVertices ( 1GateCircStr(<*x,y*>,and2a)+*1GateCircStr(<*y,c*>, and2) ) is
without_pairs by FACIRC_1:9,41;
then InputVertices MI is without_pairs by FACIRC_1:9;
then
A7: InputVertices M = (InputVertices MI) \/ (InputVertices S \ InnerVertices
MI) by A4,FACIRC_1:6;
A8: InnerVertices 1GateCircStr(<*x,c*>,and2a)= {[<*x,c*>,and2a]} by CIRCCOMB:42
;
1GateCircStr(<*x,y*>,and2a) tolerates 1GateCircStr(<*y,c*>,and2) by
CIRCCOMB:47;
then
A9: InnerVertices (1GateCircStr(<*x,y*>,and2a) +* 1GateCircStr(<*y,c*>,and2
)) = {[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]} by A3,CIRCCOMB:11;
1GateCircStr(<*x,y*>,and2a) +* 1GateCircStr(<*y,c*>,and2) tolerates
1GateCircStr(<*x,c*>,and2a) by CIRCCOMB:47;
then
A10: InnerVertices MI = {[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]} \/ {[<*x,c*>,
and2a]} by A8,A9,CIRCCOMB:11
.= {[<*x,y*>,and2a], [<*y,c*>,and2]} \/ {[<*x,c*>,and2a]} by ENUMSET1:1
.= {[<*x,y*>,and2a], [<*y,c*>,and2], [<*x,c*>,and2a]} by ENUMSET1:3;
InputVertices S = {[<*x,y*>,and2a], [<*y,c*>,and2], [<*x,c*>,and2a]} by
FACIRC_1:42;
then
A11: InputVertices S \ InnerVertices MI = {} by A10,XBOOLE_1:37;
InnerVertices (1GateCircStr(<*x,y*>,and2a) +* 1GateCircStr(<*y,c*> ,
and2)) = {[<*x,y*>,and2a], [<*y,c*>,and2]} by A9,ENUMSET1:1;
hence InputVertices M = (InputVertices(1GateCircStr(<*x,y*>,and2a)+*
1GateCircStr(<*y,c*>,and2))) \/ InputVertices 1GateCircStr(<*x,c*>,and2a) by A6
,A7,A8,A11,FACIRC_1:7
.= (InputVertices 1GateCircStr(<*x,y*>,and2a)) \/ (InputVertices
1GateCircStr(<*y,c*>,and2)) \/ (InputVertices 1GateCircStr(<*x,c*>,and2a))
by A5,A3,FACIRC_1:7
.= {x,y,y,c} \/ {c,x} by A1,A2,ENUMSET1:5
.= {y,y,x,c} \/ {c,x} by ENUMSET1:67
.= {y,x,c} \/ {c,x} by ENUMSET1:31
.= {x,y,c} \/ {c,x} by ENUMSET1:58
.= {x,y,c} \/ ({c}\/{x}) by ENUMSET1:1
.= {x,y,c} \/ {c} \/ {x} by XBOOLE_1:4
.= {c,x,y} \/ {c} \/ {x} by ENUMSET1:59
.= {c,c,x,y} \/ {x} by ENUMSET1:4
.= {c,x,y} \/ {x} by ENUMSET1:31
.= {x,y,c} \/ {x} by ENUMSET1:59
.= {x,x,y,c} by ENUMSET1:4
.= {x,y,c} by ENUMSET1:31;
MI tolerates S by CIRCCOMB:47;
hence InnerVertices M = (InnerVertices MI) \/ (InnerVertices S) by
CIRCCOMB:11
.= {[<*x,y*>,and2a], [<*y,c*>,and2], [<*x,c*>,and2a]} \/ {BorrowOutput(x
,y,c)} by A10,CIRCCOMB:42;
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
let x,y,c be non pair set;
let s be State of BorrowCirc(x,y,c);
let a1,a2,a3 be Element of BOOLEAN such that
A1: a1 = s.x and
A2: a2 = s.y and
A3: a3 = s.c;
set S = BorrowStr(x,y,c);
A4: InnerVertices S = the carrier' of S by FACIRC_1:37;
A5: y in the carrier of S by Th6;
A6: x in the carrier of S by Th6;
A7: dom s = the carrier of S by CIRCUIT1:3;
[<*x,y*>,and2a] in InnerVertices BorrowStr(x,y,c) by Th7;
hence (Following s).[<*x,y*>,and2a] = and2a.(s*<*x,y*>) by A4,FACIRC_1:35
.= and2a.<*a1,a2*> by A1,A2,A7,A6,A5,FINSEQ_2:125
.= 'not' a1 '&' a2 by TWOSCOMP:def 2;
A8: c in the carrier of S by Th6;
[<*y,c*>,and2] in InnerVertices BorrowStr(x,y,c) by Th7;
hence (Following s).[<*y,c*>,and2] = and2.(s*<*y,c*>) by A4,FACIRC_1:35
.= and2.<*a2,a3*> by A2,A3,A7,A5,A8,FINSEQ_2:125
.= a2 '&' a3 by FACIRC_1:def 6;
[<*x,c*>,and2a] in InnerVertices BorrowStr(x,y,c) by Th7;
hence (Following s).[<*x,c*>,and2a] = and2a.(s*<*x,c*>) by A4,FACIRC_1:35
.= and2a.<*a1,a3*> by A1,A3,A7,A6,A8,FINSEQ_2:125
.= 'not' a1 '&' a3 by TWOSCOMP:def 2;
end;
theorem
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
let x,y,c be non pair set;
reconsider a = c as Vertex of BorrowStr(x,y,c) by Th6;
let s be State of BorrowCirc(x,y,c);
s.a is Element of BOOLEAN;
hence thesis by Lm1;
end;
theorem
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
let x,y,c be non pair set;
reconsider a = x as Vertex of BorrowStr(x,y,c) by Th6;
let s be State of BorrowCirc(x,y,c);
s.a is Element of BOOLEAN;
hence thesis by Lm1;
end;
theorem
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
let x,y,c be non pair set;
reconsider a = y as Vertex of BorrowStr(x,y,c) by Th6;
let s be State of BorrowCirc(x,y,c);
s.a is Element of BOOLEAN;
hence thesis by Lm1;
end;
theorem Th13:
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
let x,y,c be non pair set;
set xy = <*x,y*>, yc = <*y,c*>, xc = <*x,c*>;
set xy1 =[xy,and2a], yc1 = [yc,and2], xc1 = [xc,and2a];
set S = BorrowStr(x,y,c);
reconsider xy1, yc1, xc1 as Element of InnerVertices S by Th7;
let s be State of BorrowCirc(x,y,c);
let a1,a2,a3 be Element of BOOLEAN such that
A1: a1 = s.[<*x,y*>,and2a] & a2 = s.[<*y,c*>,and2] & a3 = s.[<*x,c*>, and2a];
A2: dom s = the carrier of S by CIRCUIT1:3;
InnerVertices S = the carrier' of S by FACIRC_1:37;
hence (Following s).BorrowOutput(x,y,c) = or3.(s*<*xy1, yc1, xc1*>) by
FACIRC_1:35
.= or3.<*a1,a2,a3*> by A1,A2,FINSEQ_2:126
.= a1 'or' a2 'or' a3 by FACIRC_1:def 7;
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
let x,y,c be non pair set;
set S = BorrowStr(x,y,c);
reconsider x9 = x, y9 = y, c9 = c as Vertex of S by Th6;
let s be State of BorrowCirc(x,y,c);
set xy = <*x,y*>, yc = <*y,c*>, xc = <*x,c*>;
set xy1 =[xy,and2a], yc1 = [yc,and2], xc1 = [xc,and2a];
A1: Following(s,2) = Following Following s by FACIRC_1:15;
let a1,a2,a3 be Element of BOOLEAN such that
A2: a1 = s.x & a2 = s.y & a3 = s.c;
A3: (Following s).xc1 = 'not' a1 '&' a3 by A2,Lm1;
(Following s).xy1 = 'not' a1 '&' a2 & (Following s).yc1 = a2 '&' a3 by A2,Lm1
;
hence Following(s,2).BorrowOutput(x,y,c) = 'not' a1 '&' a2 'or' a2 '&' a3
'or' 'not' a1 '&' a3 by A1,A3,Th13;
y in InputVertices S by Th8;
then
A4: (Following s).y9 = s.y by CIRCUIT2:def 5;
c in InputVertices S by Th8;
then
A5: (Following s).c9 = s.c by CIRCUIT2:def 5;
x in InputVertices S by Th8;
then (Following s).x9 = s.x by CIRCUIT2:def 5;
hence thesis by A2,A4,A5,A1,Lm1;
end;
theorem
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
let x,y,c be non pair set;
reconsider a = c as Vertex of BorrowStr(x,y,c) by Th6;
let s be State of BorrowCirc(x,y,c);
s.a is Element of BOOLEAN;
hence thesis by Lm2;
end;
theorem
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
let x,y,c be non pair set;
reconsider a = x as Vertex of BorrowStr(x,y,c) by Th6;
let s be State of BorrowCirc(x,y,c);
s.a is Element of BOOLEAN;
hence thesis by Lm2;
end;
theorem
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
let x,y,c be non pair set;
reconsider a = y as Vertex of BorrowStr(x,y,c) by Th6;
let s be State of BorrowCirc(x,y,c);
s.a is Element of BOOLEAN;
hence thesis by Lm2;
end;
theorem
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:
for x,y,c being non pair set for s being State of BorrowCirc(x,y
,c) holds Following(s,2) is stable
proof
let x,y,c be non pair set;
set S = BorrowStr(x,y,c);
reconsider xx = x, yy = y, cc = c as Vertex of S by Th6;
let s be State of BorrowCirc(x,y,c);
set a1 = s.xx, a2 = s.yy, a3 = s.cc;
set ffs = Following(s,2), fffs = Following ffs;
A1: ffs = Following Following s by FACIRC_1:15;
A2: y in InputVertices S by Th8;
then (Following s).y = a2 by CIRCUIT2:def 5;
then
A3: ffs.y = a2 by A1,A2,CIRCUIT2:def 5;
a2 = s.y;
then
A4: ffs.[<*x,c*>,and2a] = 'not' a1 '&' a3 by Lm2;
A5: x in InputVertices S by Th8;
then (Following s).x = a1 by CIRCUIT2:def 5;
then
A6: ffs.x = a1 by A1,A5,CIRCUIT2:def 5;
a1 = s.x;
then
A7: ffs.[<*y,c*>,and2 ] = a2 '&' a3 by Lm2;
A8: c in InputVertices S by Th8;
then (Following s).c = a3 by CIRCUIT2:def 5;
then
A9: ffs.c = a3 by A1,A8,CIRCUIT2:def 5;
a3 = s.c;
then
A10: ffs.[<*x,y*>,and2a] = 'not' a1 '&' a2 by Lm2;
A11: ffs.BorrowOutput(x,y,c) = 'not' a1 '&' a2 'or' a2 '&' a3 'or' 'not' a1
'&' a3 by Lm2;
A12: now
let a be object;
assume
A13: a in the carrier of S;
then reconsider v = a as Vertex of S;
A14: v in InputVertices S \/ InnerVertices S by A13,XBOOLE_1:45;
thus ffs.a = (fffs).a
proof
per cases by A14,XBOOLE_0:def 3;
suppose
v in InputVertices S;
hence thesis by CIRCUIT2:def 5;
end;
suppose
v in InnerVertices S;
then v in {[<*x,y*>,and2a], [<*y,c*>,and2], [<*x,c*>,and2a]} \/ {
BorrowOutput(x,y,c)} by Th9;
then
v in {[<*x,y*>,and2a], [<*y,c*>,and2], [<*x,c*>,and2a]} or v in {
BorrowOutput(x,y,c)} by XBOOLE_0:def 3;
then v = [<*x,y*>,and2a] or v = [<*y,c*>,and2] or v = [<*x,c*>,and2a]
or v = BorrowOutput(x,y,c) by ENUMSET1:def 1,TARSKI:def 1;
hence thesis by A11,A10,A7,A4,A6,A3,A9,Lm1,Th13;
end;
end;
end;
dom Following Following(s,2) = the carrier of S & dom Following(s,2) =
the carrier of S by CIRCUIT1:3;
hence ffs = fffs by A12,FUNCT_1:2;
end;
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
2GatesCircStr(x
,y,c, 'xor') +* BorrowStr(x,y,c);
coherence;
end;
theorem Th19:
for x,y,c being non pair set holds InputVertices
BitSubtracterWithBorrowStr(x,y,c) = {x,y,c}
proof
let x,y,c be non pair set;
set S = BitSubtracterWithBorrowStr(x,y,c);
set S1 = 2GatesCircStr(x,y,c, 'xor'), S2 = BorrowStr(x,y,c);
A1: InputVertices S1 = {x,y,c} & InputVertices S2 = {x,y,c} by Th9,FACIRC_1:57;
InnerVertices S1 is Relation & InnerVertices S2 is Relation by Th1,
FACIRC_1:58;
hence InputVertices S = {x,y,c} \/ {x,y,c} by A1,FACIRC_1:7
.= {x,y,c};
end;
theorem
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
let x,y,c be non pair set;
set S1 = 2GatesCircStr(x,y,c, 'xor'), S2 = BorrowStr(x,y,c);
A1: {[<*x,y*>, 'xor'], 2GatesCircOutput(x,y,c,'xor')} \/ {[<*x,y*>,and2a], [
<*y,c *>,and2], [<*x,c*>,and2a]} \/ {BorrowOutput(x,y,c)} = {[<*x,y*>, 'xor'],
2GatesCircOutput(x,y,c,'xor')} \/ ({[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,
and2a]} \/ {BorrowOutput(x,y,c)}) & InnerVertices S1 = {[<*x,y*>, 'xor'],
2GatesCircOutput(x,y,c,'xor')} by FACIRC_1:56,XBOOLE_1:4;
InnerVertices S2 = {[<*x,y*>,and2a], [<*y,c*>,and2], [<*x,c*>,and2a]} \/
{BorrowOutput(x,y,c)} by Th9;
hence thesis by A1,FACIRC_1:27;
end;
theorem
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
set S1 = 2GatesCircStr(x,y,c, 'xor');
let S be non empty ManySortedSign;
A1: x in the carrier of S1 & y in the carrier of S1 by FACIRC_1:60;
A2: c in the carrier of S1 by FACIRC_1:60;
assume S = BitSubtracterWithBorrowStr(x,y,c);
hence thesis by A1,A2,FACIRC_1:20;
end;
definition
let x,y,c be set;
func BitSubtracterWithBorrowCirc(x,y,c) -> strict Boolean gate`2=den Circuit
of BitSubtracterWithBorrowStr(x,y,c) equals
BitSubtracterCirc(x,y,c) +*
BorrowCirc(x,y,c);
coherence;
end;
theorem
InnerVertices BitSubtracterWithBorrowStr(x,y,c) is Relation
proof
InnerVertices 2GatesCircStr(x,y,c, 'xor') is Relation & InnerVertices
BorrowStr(x,y,c) is Relation by Th1,FACIRC_1:58;
hence thesis by FACIRC_1:3;
end;
theorem
for x,y,c being non pair set holds InputVertices
BitSubtracterWithBorrowStr(x,y,c) is without_pairs
proof
let x,y,c be non pair set;
InputVertices BitSubtracterWithBorrowStr(x,y,c) = {x,y,c} by Th19;
hence thesis;
end;
theorem
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
set f = 'xor';
let x,y,c be non pair set;
set S1 = 2GatesCircStr(x,y,c, 'xor'), S2 = BorrowStr(x,y,c);
set A = BitSubtracterWithBorrowCirc(x,y,c);
set A1 = BitSubtracterCirc(x,y,c), A2 = BorrowCirc(x,y,c);
let s be State of A;
let a1,a2,a3 be Element of BOOLEAN;
assume that
A1: a1 = s.x and
A2: a2 = s.y and
A3: a3 = s.c;
reconsider s1 = s|the carrier of S1 as State of A1 by FACIRC_1:26;
A4: dom s1 = the carrier of S1 by CIRCUIT1:3;
c in the carrier of S1 by FACIRC_1:60;
then
A5: a3 = s1.c by A3,A4,FUNCT_1:47;
y in the carrier of S1 by FACIRC_1:60;
then
A6: a2 = s1.y by A2,A4,FUNCT_1:47;
reconsider t = s as State of A1+*A2;
InputVertices S1 is without_pairs by FACIRC_1:59;
then InnerVertices S2 misses InputVertices S1 by Th1,FACIRC_1:5;
then
A7: Following(t,2).2GatesCircOutput(x,y,c, f) = Following(s1,2).
2GatesCircOutput(x,y,c, f) by FACIRC_1:32;
reconsider s2 = s|the carrier of S2 as State of A2 by FACIRC_1:26;
A8: dom s2 = the carrier of S2 by CIRCUIT1:3;
x in the carrier of S1 by FACIRC_1:60;
then a1 = s1.x by A1,A4,FUNCT_1:47;
hence Following(s,2).BitSubtracterOutput(x,y,c) = a1 'xor' a2 'xor' a3 by A6
,A5,A7,FACIRC_1:64;
InputVertices S2 is without_pairs by Th2;
then InnerVertices S1 misses InputVertices S2 by FACIRC_1:5,58;
then
A9: Following(t,2).BorrowOutput(x,y,c) = Following(s2,2).BorrowOutput(x,y,c
) by FACIRC_1:33;
c in the carrier of S2 by Th6;
then
A10: a3 = s2.c by A3,A8,FUNCT_1:47;
y in the carrier of S2 by Th6;
then
A11: a2 = s2.y by A2,A8,FUNCT_1:47;
x in the carrier of S2 by Th6;
then a1 = s2.x by A1,A8,FUNCT_1:47;
hence thesis by A11,A10,A9,Lm2;
end;
theorem
for x,y,c being non pair set for s being State of
BitSubtracterWithBorrowCirc(x,y,c) holds Following(s,2) is stable
proof
let x,y,c be non pair set;
set S = BitSubtracterWithBorrowStr(x,y,c);
set S1 = 2GatesCircStr(x,y,c, 'xor'), S2 = BorrowStr(x,y,c);
set A = BitSubtracterWithBorrowCirc(x,y,c);
set A1 = BitSubtracterCirc(x,y,c), A2 = BorrowCirc(x,y,c);
let s be State of A;
reconsider s1 = s|the carrier of S1 as State of A1 by FACIRC_1:26;
reconsider s2 = s|the carrier of S2 as State of A2 by FACIRC_1:26;
reconsider t = s as State of A1+*A2;
A1: dom Following(s,3) = the carrier of S by CIRCUIT1:3;
A2: the carrier of S = (the carrier of S1) \/ the carrier of S2 by
CIRCCOMB:def 2;
InputVertices S1 is without_pairs by FACIRC_1:59;
then InnerVertices S2 misses InputVertices S1 by Th1,FACIRC_1:5;
then
A3: Following(s1,2) = Following(t,2)|the carrier of S1 & Following(s1,3) =
Following(t,3)|the carrier of S1 by FACIRC_1:30;
Following(s1,2) is stable by FACIRC_1:63;
then
A4: Following(s1,2) = Following Following(s1,2)
.= Following(s1,2+1) by FACIRC_1:12;
InputVertices S2 is without_pairs by Th2;
then InnerVertices S1 misses InputVertices S2 by FACIRC_1:5,58;
then
A5: Following(s2,2) = Following(t,2)|the carrier of S2 & Following(s2,3) =
Following(t,3)|the carrier of S2 by FACIRC_1:31;
Following(s2,2) is stable by Th18;
then
A6: Following(s2,2) = Following Following(s2,2)
.= Following(s2,2+1) by FACIRC_1:12;
A7: dom Following(s1,2) = the carrier of S1 & dom Following(s2,2) = the
carrier of S2 by CIRCUIT1:3;
A8: now
let a be object;
assume a in the carrier of S;
then a in the carrier of S1 or a in the carrier of S2 by A2,XBOOLE_0:def 3;
then Following(s,2).a = Following(s1,2).a & Following(s,3).a = Following(
s1,3).a or Following(s,2).a = Following(s2,2).a & Following(s,3).a = Following(
s2,3).a by A3,A5,A4,A6,A7,FUNCT_1:47;
hence Following(s,2).a = (Following Following(s,2)).a by A4,A6,FACIRC_1:12;
end;
Following(s,2+1) = Following Following(s,2) & dom Following(s,2) = the
carrier of S by CIRCUIT1:3,FACIRC_1:12;
hence Following(s,2) = Following Following(s,2) by A1,A8,FUNCT_1:2;
end;