Copyright (c) 1999 Association of Mizar Users
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;
definitions CIRCUIT2, FACIRC_1;
theorems TARSKI, ENUMSET1, RELAT_1, FUNCT_1, FINSEQ_2, MSAFREE2, 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:
Def1:
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:
Def2:
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:
Def3:
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:
Def4:
BorrowIStr(x,y,c) +*
1GateCircStr(<*[<*x,y*>, and2a], [<*y,c*>, and2], [<*x,c*>, and2a]*>, or3);
correctness;
end;
definition
let x,y,c be set;
A1: BorrowIStr(x,y,c) = 1GateCircStr(<*x,y*>, and2a) +*
1GateCircStr(<*y,c*>, and2) +* 1GateCircStr(<*x,c*>, and2a) by Def3;
func BorrowICirc(x,y,c) ->
strict Boolean gate`2=den Circuit of BorrowIStr(x,y,c) equals:
Def5:
1GateCircuit(x,y, and2a) +* 1GateCircuit(y,c, and2) +*
1GateCircuit(x,c, and2a);
coherence by A1;
end;
theorem Th1:
InnerVertices BorrowStr(x,y,c) is Relation
proof
A1: BorrowStr(x,y,c) = BorrowIStr(x,y,c) +*
1GateCircStr(<*[<*x,y*>, and2a], [<*y,c*>, and2], [<*x,c*>, and2a]*>, or3)
by Def4;
A2: BorrowIStr(x,y,c) = 1GateCircStr(<*x,y*>, and2a) +*
1GateCircStr(<*y,c*>, and2) +* 1GateCircStr(<*x,c*>, and2a) by Def3;
A3: InnerVertices 1GateCircStr(<*x,y*>,and2a) is Relation &
InnerVertices 1GateCircStr(<*x,c*>,and2a) is Relation &
InnerVertices 1GateCircStr(<*y,c*>,and2) is Relation by FACIRC_1:38;
then InnerVertices (1GateCircStr(<*x,y*>,and2a)+*1GateCircStr(<*y,c*>,and2
))
is Relation by FACIRC_1:3;
then InnerVertices 1GateCircStr(<*[<*x,y*>, and2a], [<*y,c*>, and2],
[<*x,c*>, and2a]*>, or3) is Relation &
InnerVertices BorrowIStr(x,y,c) is Relation by A2,A3,FACIRC_1:3,38;
hence thesis by A1,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);
A1: M = MI +* S by Def4;
A2: MI = 1GateCircStr(<*x,y*>, and2a) +*
1GateCircStr(<*y,c*>, and2) +* 1GateCircStr(<*x,c*>, and2a) by Def3;
A3: InputVertices 1GateCircStr(<*x,y*>,and2a) is without_pairs &
InputVertices 1GateCircStr(<*x,c*>,and2a) is without_pairs &
InputVertices 1GateCircStr(<*y,c*>,and2) is without_pairs
by FACIRC_1:41;
then InputVertices (1GateCircStr(<*x,y*>,and2a)+*1GateCircStr(<*y,c*>,and2
))
is without_pairs by FACIRC_1:9;
then A4: InputVertices MI is without_pairs by A2,A3,FACIRC_1:9;
InnerVertices S is Relation by FACIRC_1:38;
then A5: InputVertices M =
(InputVertices MI) \/ (InputVertices S \ InnerVertices MI)
by A1,A4,FACIRC_1:6;
given xx being pair set such that
A6: xx in InputVertices M;
A7: InputVertices S = {[<*x,y*>,and2a], [<*y,c*>,and2], [<*x,c*>,and2a]}
by FACIRC_1:42;
A8: InnerVertices 1GateCircStr(<*x,y*>, and2a) = {[<*x,y*>, and2a]} &
InnerVertices 1GateCircStr(<*y,c*>, and2) = {[<*y,c*>, and2]} &
InnerVertices 1GateCircStr(<*x,c*>, and2a) = {[<*x,c*>, and2a]}
by CIRCCOMB:49;
1GateCircStr(<*x,y*>, and2a) tolerates 1GateCircStr(<*y,c*>, and2) &
1GateCircStr(<*x,y*>, and2a) tolerates 1GateCircStr(<*x,c*>, and2a) &
1GateCircStr(<*y,c*>, and2) tolerates 1GateCircStr(<*x,c*>, and2a)
by CIRCCOMB:55;
then A9: InnerVertices (1GateCircStr(<*x,y*>,and2a) +*
1GateCircStr(<*y,c*>,and2)) = {[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]}
by A8,CIRCCOMB:15;
1GateCircStr(<*x,y*>,and2a) +* 1GateCircStr(<*y,c*>,and2)
tolerates 1GateCircStr(<*x,c*>,and2a) by CIRCCOMB:55;
then InnerVertices MI = {[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]} \/
{[<*x,c*>,and2a]}
by A2,A8,A9,CIRCCOMB:15
.= {[<*x,y*>,and2a], [<*y,c*>,and2]} \/ {[<*x,c*>,and2a]} by ENUMSET1:41
.= {[<*x,y*>,and2a], [<*y,c*>,and2], [<*x,c*>,and2a]} by ENUMSET1:43;
then InputVertices S \ InnerVertices MI = {} by A7,XBOOLE_1:37;
hence thesis by A4,A5,A6,FACIRC_1:def 2;
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 v1 as Element of InnerVertices S1 by FACIRC_1:47;
S = S1+*S2+*S3 by Def3;
then A2: S = S1+*(S2+*S3) by CIRCCOMB:10;
then reconsider v = v1 as Element of InnerVertices S by FACIRC_1:21;
A = A1+*A2+*A3 by Def5;
then 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;
A4: dom s1 = the carrier of S1 by CIRCUIT1:4;
reconsider xx = x, yy = y as Vertex of S1 by FACIRC_1:43;
reconsider xx, yy as Vertex of S by A2,FACIRC_1:20;
thus (Following s).[xy, and2a] = (Following s1).v by A2,A3,CIRCCOMB:72
.= and2a.<*s1.xx,s1.yy*> by FACIRC_1:50
.= and2a.<*s.xx,s1.yy*> by A4,FUNCT_1:70
.= and2a.<*s.xx,s.yy*> by A4,FUNCT_1:70
.= '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 v2 as Element of InnerVertices S2 by FACIRC_1:47;
A2: S = S1+*S2+*S3 & S1+*S2 = S2+*S1 by Def3,FACIRC_1:23;
then A3: S = S2+*(S1+*S3) by CIRCCOMB:10;
then reconsider v = v2 as Element of InnerVertices S by FACIRC_1:21;
A = A1+*A2+*A3 & A1+*A2 = A2+*A1 by Def5,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;
A5: dom s2 = the carrier of S2 by CIRCUIT1:4;
reconsider yy = y, cc = c as Vertex of S2 by FACIRC_1:43;
reconsider yy, cc as Vertex of S by A3,FACIRC_1:20;
thus (Following s).[yc, and2] = (Following s2).v by A3,A4,CIRCCOMB:72
.= and2.<*s2.yy,s2.cc*> by FACIRC_1:50
.= and2.<*s.yy,s2.cc*> by A5,FUNCT_1:70
.= and2.<*s.yy,s.cc*> by A5,FUNCT_1:70
.= a '&' b by A1,TWOSCOMP:def 1;
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 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 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 v3 as Element of InnerVertices S3 by FACIRC_1:47;
A2: S = S1+*S2+*S3 by Def3;
then reconsider v = v3 as Element of InnerVertices S by FACIRC_1:21;
A3: A = A1+*A2+*A3 by Def5;
then reconsider s3 = s|the carrier of S3 as State of A3 by FACIRC_1:26;
A4: dom s3 = the carrier of S3 by CIRCUIT1:4;
reconsider xx = x, cc = c as Vertex of S3 by FACIRC_1:43;
reconsider xx, cc as Vertex of S by A2,FACIRC_1:20;
thus (Following s).[xc, and2a] = (Following s3).v by A2,A3,CIRCCOMB:72
.= and2a.<*s3.xx,s3.cc*> by FACIRC_1:50
.= and2a.<*s.xx,s3.cc*> by A4,FUNCT_1:70
.= and2a.<*s.xx,s.cc*> by A4,FUNCT_1:70
.= 'not' a '&' b by A1,TWOSCOMP:def 2;
end;
definition
let x,y,c be set;
A1: BorrowStr(x,y,c) = BorrowIStr(x,y,c) +*
1GateCircStr(<*[<*x,y*>,and2a], [<*y,c*>,and2], [<*x,c*>,and2a]*>, or3)
by Def4;
func BorrowOutput(x,y,c) -> Element of InnerVertices BorrowStr(x,y,c)
equals:
Def6:
[<*[<*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 A1,FACIRC_1:21;
end;
correctness;
end;
definition
let x,y,c be set;
A1: BorrowStr(x,y,c) = BorrowIStr(x,y,c) +*
1GateCircStr(<*[<*x,y*>,and2a], [<*y,c*>,and2], [<*x,c*>,and2a]*>, or3)
by Def4;
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 by A1;
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
A1: BorrowStr(x,y,c) = BorrowIStr(x,y,c) +*
1GateCircStr(<*[<*x,y*>,and2a], [<*y,c*>,and2], [<*x,c*>,and2a]*>, or3)
by Def4;
A2: BorrowIStr(x,y,c) = 1GateCircStr(<*x,y*>, and2a) +*
1GateCircStr(<*y,c*>,and2) +* 1GateCircStr(<*x,c*>, and2a) by Def3;
y in the carrier of 1GateCircStr(<*x,y*>,and2a) by FACIRC_1:43;
then A3: y in
the carrier of 1GateCircStr(<*x,y*>,and2a)+*1GateCircStr(<*y,c*>,and2)
by FACIRC_1:20;
x in the carrier of 1GateCircStr(<*x,c*>,and2a) &
c in the carrier of 1GateCircStr(<*x,c*>,and2a) by FACIRC_1:43;
then x in the carrier of BorrowIStr(x,y,c) &
y in the carrier of BorrowIStr(x,y,c) &
c in the carrier of BorrowIStr(x,y,c)
by A2,A3,FACIRC_1:20;
hence thesis by 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
A1: BorrowStr(x,y,c) = BorrowIStr(x,y,c) +*
1GateCircStr(<*[<*x,y*>,and2a], [<*y,c*>,and2], [<*x,c*>,and2a]*>, or3)
by Def4;
A2: BorrowIStr(x,y,c) = 1GateCircStr(<*x,y*>, and2a) +*
1GateCircStr(<*y,c*>,and2) +* 1GateCircStr(<*x,c*>, and2a) by Def3;
[<*x,y*>,and2a] in InnerVertices 1GateCircStr(<*x,y*>,and2a) &
[<*y,c*>,and2 ] in InnerVertices 1GateCircStr(<*y,c*>,and2 )
by FACIRC_1:47;
then [<*x,c*>,and2a] in InnerVertices 1GateCircStr(<*x,c*>,and2a) &
[<*x,y*>,and2a] in InnerVertices
(1GateCircStr(<*x,y*>,and2a)+*1GateCircStr(<*y,c*>,and2)) &
[<*y,c*>,and2 ] in InnerVertices
(1GateCircStr(<*x,y*>,and2a)+*1GateCircStr(<*y,c*>,and2))
by FACIRC_1:21,47;
then [<*x,y*>,and2a] in InnerVertices BorrowIStr(x,y,c) &
[<*y,c*>,and2 ] in InnerVertices BorrowIStr(x,y,c) &
[<*x,c*>,and2a] in InnerVertices BorrowIStr(x,y,c) by A2,FACIRC_1:21;
hence thesis by A1,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;
InputVertices BorrowStr(x,y,c) = (the carrier of BorrowStr(x,y,c)) \
rng the ResultSort of BorrowStr(x,y,c) by MSAFREE2:def 2;
then A1: InputVertices BorrowStr(x,y,c) =
(the carrier of BorrowStr(x,y,c)) \ InnerVertices BorrowStr(x,y,c)
by MSAFREE2:def 3;
A2: 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) by Th6;
A3: InnerVertices BorrowStr(x,y,c) is Relation by Th1;
assume not thesis;
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 A1,A2,XBOOLE_0:def 4;
then (ex a1,b1 being set st x = [a1,b1]) or
(ex a1,b1 being set st y = [a1,b1]) or
(ex a1,b1 being set 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 x_y =[xy,and2a], y_c = [yc,and2], x_c = [xc,and2a];
set MI = BorrowIStr(x,y,c), S = 1GateCircStr(<*x_y, y_c, x_c*>, or3);
set M = BorrowStr(x,y,c);
A1: M = MI +* S by Def4;
A2: MI = 1GateCircStr(<*x,y*>, and2a) +*
1GateCircStr(<*y,c*>,and2) +* 1GateCircStr(<*x,c*>, and2a) by Def3;
A3: InputVertices 1GateCircStr(<*x,y*>,and2a) is without_pairs &
InputVertices 1GateCircStr(<*x,c*>,and2a) is without_pairs &
InputVertices 1GateCircStr(<*y,c*>,and2) is without_pairs
by FACIRC_1:41;
then A4: InputVertices (1GateCircStr(<*x,y*>,and2a)+*1GateCircStr(<*y,c*>,and2)
)
is without_pairs by FACIRC_1:9;
then A5: InputVertices MI is without_pairs by A2,A3,FACIRC_1:9;
A6: InputVertices 1GateCircStr(<*x,y*>,and2a) = {x,y} &
InputVertices 1GateCircStr(<*x,c*>,and2a) = {x,c} &
InputVertices 1GateCircStr(<*y,c*>,and2 ) = {y,c} by FACIRC_1:40;
InnerVertices S is Relation by FACIRC_1:38;
then A7: InputVertices M =
(InputVertices MI) \/ (InputVertices S \ InnerVertices MI)
by A1,A5,FACIRC_1:6;
A8: InputVertices S = {[<*x,y*>,and2a], [<*y,c*>,and2], [<*x,c*>,and2a]}
by FACIRC_1:42;
A9: InnerVertices 1GateCircStr(<*x,y*>,and2a) = {[<*x,y*>,and2a]} &
InnerVertices 1GateCircStr(<*y,c*>,and2) = {[<*y,c*>,and2]} &
InnerVertices 1GateCircStr(<*x,c*>,and2a)= {[<*x,c*>,and2a]}
by CIRCCOMB:49;
1GateCircStr(<*x,y*>,and2a) tolerates 1GateCircStr(<*y,c*>,and2) &
1GateCircStr(<*x,y*>,and2a) tolerates 1GateCircStr(<*x,c*>,and2a) &
1GateCircStr(<*y,c*>,and2) tolerates 1GateCircStr(<*x,c*>,and2a)
by CIRCCOMB:55;
then A10:
InnerVertices (1GateCircStr(<*x,y*>,and2a) +* 1GateCircStr(<*y,c*>,and2)) =
{[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]} by A9,CIRCCOMB:15;
then A11: InnerVertices (1GateCircStr(<*x,y*>,and2a) +* 1GateCircStr(<*y,c*>
,and2)) =
{[<*x,y*>,and2a], [<*y,c*>,and2]} by ENUMSET1:41;
1GateCircStr(<*x,y*>,and2a) +* 1GateCircStr(<*y,c*>,and2)
tolerates 1GateCircStr(<*x,c*>,and2a) by CIRCCOMB:55;
then A12: InnerVertices MI = {[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]}
\/ {[<*x,c*>,and2a]} by A2,A9,A10,CIRCCOMB:15
.= {[<*x,y*>,and2a], [<*y,c*>,and2]} \/ {[<*x,c*>,and2a]} by ENUMSET1:41
.= {[<*x,y*>,and2a], [<*y,c*>,and2], [<*x,c*>,and2a]} by ENUMSET1:43;
then InputVertices S \ InnerVertices MI = {} by A8,XBOOLE_1:37;
hence InputVertices M =
(InputVertices(1GateCircStr(<*x,y*>,and2a)+*1GateCircStr(<*y,c*>,and2)))
\/ InputVertices 1GateCircStr(<*x,c*>,and2a) by A2,A3,A4,A7,A9,A11,
FACIRC_1:7
.= (InputVertices 1GateCircStr(<*x,y*>,and2a)) \/
(InputVertices 1GateCircStr(<*y,c*>,and2)) \/
(InputVertices 1GateCircStr(<*x,c*>,and2a)) by A3,A9,FACIRC_1:7
.= {x,y,y,c} \/ {c,x} by A6,ENUMSET1:45
.= {y,y,x,c} \/ {c,x} by ENUMSET1:110
.= {y,x,c} \/ {c,x} by ENUMSET1:71
.= {x,y,c} \/ {c,x} by ENUMSET1:99
.= {x,y,c} \/ ({c}\/{x}) by ENUMSET1:41
.= {x,y,c} \/ {c} \/ {x} by XBOOLE_1:4
.= {c,x,y} \/ {c} \/ {x} by ENUMSET1:100
.= {c,c,x,y} \/ {x} by ENUMSET1:44
.= {c,x,y} \/ {x} by ENUMSET1:71
.= {x,y,c} \/ {x} by ENUMSET1:100
.= {x,x,y,c} by ENUMSET1:44
.= {x,y,c} by ENUMSET1:71;
MI tolerates S by CIRCCOMB:55;
hence InnerVertices M = (InnerVertices MI) \/ (InnerVertices S)
by A1,CIRCCOMB:15
.= {[<*x,y*>,and2a], [<*y,c*>,and2], [<*x,c*>,and2a]} \/
{[<*x_y, y_c, x_c*>, or3]} by A12,CIRCCOMB:49
.= {[<*x,y*>,and2a], [<*y,c*>,and2], [<*x,c*>,and2a]} \/
{BorrowOutput(x,y,c)} by Def6;
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 & a2 = s.y & a3 = s.c;
set S = BorrowStr(x,y,c);
A2: InnerVertices S = the OperSymbols of S by FACIRC_1:37;
A3: dom s = the carrier of S by CIRCUIT1:4;
A4: x in the carrier of S & y in the carrier of S & c in the carrier of S
by Th6;
[<*x,y*>,and2a] in InnerVertices BorrowStr(x,y,c) by Th7;
hence (Following s).[<*x,y*>,and2a]
= and2a.(s*<*x,y*>) by A2,FACIRC_1:35
.= and2a.<*a1,a2*> by A1,A3,A4,FINSEQ_2:145
.= 'not' a1 '&' a2 by TWOSCOMP:def 2;
[<*y,c*>,and2] in InnerVertices BorrowStr(x,y,c) by Th7;
hence (Following s).[<*y,c*>,and2]
= and2.(s*<*y,c*>) by A2,FACIRC_1:35
.= and2.<*a2,a3*> by A1,A3,A4,FINSEQ_2:145
.= a2 '&' a3 by TWOSCOMP:def 1;
[<*x,c*>,and2a] in InnerVertices BorrowStr(x,y,c) by Th7;
hence (Following s).[<*x,c*>,and2a]
= and2a.(s*<*x,c*>) by A2,FACIRC_1:35
.= and2a.<*a1,a3*> by A1,A3,A4,FINSEQ_2:145
.= '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; let s be State of BorrowCirc(x,y,c);
reconsider a = c as Vertex of BorrowStr(x,y,c) by Th6;
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; let s be State of BorrowCirc(x,y,c);
reconsider a = x as Vertex of BorrowStr(x,y,c) by Th6;
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; let s be State of BorrowCirc(x,y,c);
reconsider a = y as Vertex of BorrowStr(x,y,c) by Th6;
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;
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];
set xy = <*x,y*>, yc = <*y,c*>, xc = <*x,c*>;
set x_y =[xy,and2a], y_c = [yc,and2], x_c = [xc,and2a];
set S = BorrowStr(x,y,c);
A2: InnerVertices S = the OperSymbols of S by FACIRC_1:37;
A3: dom s = the carrier of S by CIRCUIT1:4;
reconsider x_y, y_c, x_c as Element of InnerVertices S by Th7;
BorrowOutput(x,y,c) = [<*x_y, y_c, x_c*>, or3] by Def6;
hence (Following s).BorrowOutput(x,y,c)
= or3.(s*<*x_y, y_c, x_c*>) by A2,FACIRC_1:35
.= or3.<*a1,a2,a3*> by A1,A3,FINSEQ_2:146
.= 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;
let s be State of BorrowCirc(x,y,c);
let a1,a2,a3 be Element of BOOLEAN such that
A1: a1 = s.x & a2 = s.y & a3 = s.c;
set xy = <*x,y*>, yc = <*y,c*>, xc = <*x,c*>;
set x_y =[xy,and2a], y_c = [yc,and2], x_c = [xc,and2a];
set S = BorrowStr(x,y,c);
reconsider x' = x, y' = y, c' = c as Vertex of S by Th6;
x in InputVertices S & y in InputVertices S & c in InputVertices S
by Th8;
then A2: (Following s).x' = s.x & (Following s).y' = s.y & (Following s).c' =
s.c
by CIRCUIT2:def 5;
A3: Following(s,2) = Following Following s by FACIRC_1:15;
(Following s).x_y = 'not' a1 '&' a2 & (Following s).y_c = a2 '&' a3 &
(Following s).x_c = 'not' a1 '&' a3 by A1,Lm1;
hence Following(s,2).BorrowOutput(x,y,c) =
'not' a1 '&' a2 'or' a2 '&' a3 'or' 'not' a1 '&' a3 by A3,Th13;
thus thesis by A1,A2,A3,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; let s be State of BorrowCirc(x,y,c);
reconsider a = c as Vertex of BorrowStr(x,y,c) by Th6;
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; let s be State of BorrowCirc(x,y,c);
reconsider a = x as Vertex of BorrowStr(x,y,c) by Th6;
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; let s be State of BorrowCirc(x,y,c);
reconsider a = y as Vertex of BorrowStr(x,y,c) by Th6;
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);
let s be State of BorrowCirc(x,y,c);
A1: dom Following Following(s,2) = the carrier of S &
dom Following(s,2) = the carrier of S by CIRCUIT1:4;
reconsider xx = x, yy = y, cc = c as Vertex of S by Th6;
set a1 = s.xx, a2 = s.yy, a3 = s.cc;
set ffs = Following(s,2), fffs = Following ffs;
a1 = s.x & a2 = s.y & a3 = s.c;
then A2: ffs.BorrowOutput(x,y,c) = 'not' a1 '&' a2 'or' a2 '&' a3 'or' 'not'
a1 '&' a3 &
ffs.[<*x,y*>,and2a] = 'not' a1 '&' a2 &
ffs.[<*y,c*>,and2 ] = a2 '&' a3 &
ffs.[<*x,c*>,and2a] = 'not' a1 '&' a3 by Lm2;
A3: ffs = Following Following s by FACIRC_1:15;
A4: x in InputVertices S & y in InputVertices S & c in InputVertices S
by Th8;
then (Following s).x = a1 & (Following s).y = a2 & (Following s).c = a3
by CIRCUIT2:def 5;
then A5: ffs.x = a1 & ffs.y = a2 & ffs.c = a3 by A3,A4,CIRCUIT2:def 5;
now let a be set; assume
A6: a in the carrier of S;
then reconsider v = a as Vertex of S;
A7: v in InputVertices S \/ InnerVertices S by A6,MSAFREE2:3;
thus ffs.a = (fffs).a
proof per cases by A7,XBOOLE_0:def 2;
suppose v in InputVertices S;
hence thesis by CIRCUIT2:def 5;
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 2;
then v = [<*x,y*>,and2a] or v = [<*y,c*>,and2] or v = [<*x,c*>,and2a]
or
v = BorrowOutput(x,y,c) by ENUMSET1:13,TARSKI:def 1;
hence thesis by A2,A5,Lm1,Th13;
end;
end;
hence ffs = fffs by A1,FUNCT_1:9;
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:
Def8:
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: S = S1 +* S2 by Def8;
A2: InputVertices S1 is without_pairs & InnerVertices S1 is Relation
by FACIRC_1:58,59;
A3: InputVertices S2 is without_pairs & InnerVertices S2 is Relation
by Th1,Th2;
c <> [<*x,y*>, 'xor'];
then InputVertices S1 = {x,y,c} & InputVertices S2 = {x,y,c}
by Th9,FACIRC_1:57;
hence InputVertices S = {x,y,c} \/ {x,y,c} by A1,A2,A3,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 S = BitSubtracterWithBorrowStr(x,y,c);
set S1 = 2GatesCircStr(x,y,c, 'xor'), S2 = BorrowStr(x,y,c);
A1: S = S1 +* S2 by Def8;
A2: {[<*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)})
by XBOOLE_1:4;
InnerVertices S1 = {[<*x,y*>, 'xor'], 2GatesCircOutput(x,y,c,'xor')} &
InnerVertices S2 = {[<*x,y*>,and2a], [<*y,c*>,and2], [<*x,c*>,and2a]} \/
{BorrowOutput(x,y,c)} by Th9,FACIRC_1:56;
hence thesis by A1,A2,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'), S2 = BorrowStr(x,y,c);
let S be non empty ManySortedSign;
assume S = BitSubtracterWithBorrowStr(x,y,c);
then x in the carrier of S1 & y in the carrier of S1 & c in the carrier of
S1 &
S = S1 +* S2 by Def8,FACIRC_1:60;
hence thesis by FACIRC_1:20;
end;
definition
let x,y,c be set;
A1: BitSubtracterWithBorrowStr(x,y,c)
= 2GatesCircStr(x,y,c, 'xor') +* BorrowStr(x,y,c) by Def8;
func BitSubtracterWithBorrowCirc(x,y,c) ->
strict Boolean gate`2=den Circuit of BitSubtracterWithBorrowStr(x,y,c)
equals:
Def9:
BitSubtracterCirc(x,y,c) +* BorrowCirc(x,y,c);
coherence by A1;
end;
theorem
InnerVertices BitSubtracterWithBorrowStr(x,y,c) is Relation
proof
A1: BitSubtracterWithBorrowStr(x,y,c) =
2GatesCircStr(x,y,c, 'xor') +* BorrowStr(x,y,c) by Def8;
InnerVertices 2GatesCircStr(x,y,c, 'xor') is Relation &
InnerVertices BorrowStr(x,y,c) is Relation by Th1,FACIRC_1:58;
hence thesis by A1,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
BitSubtracterOutput(x,y,c) in
InnerVertices BitSubtracterWithBorrowStr(x,y,c) &
BorrowOutput(x,y,c) in InnerVertices BitSubtracterWithBorrowStr(x,y,c)
proof
BitSubtracterWithBorrowStr(x,y,c)
= 2GatesCircStr(x,y,c, 'xor') +* BorrowStr(x,y,c) by Def8;
hence thesis by FACIRC_1:21;
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 let x,y,c be non pair set;
set f = 'xor';
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;
let a1,a2,a3 be Element of BOOLEAN; assume
A1: a1 = s.x & a2 = s.y & a3 = s.c;
A2: x in the carrier of S1 & y in the carrier of S1 & c in the carrier of S1
by FACIRC_1:60;
A3: x in the carrier of S2 & y in the carrier of S2 & c in the carrier of S2
by Th6;
A4: A = A1 +* A2 & S = S1+*S2 by Def8,Def9;
then 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 A4,FACIRC_1:26;
reconsider t = s as State of A1+*A2 by A4;
InputVertices S1 is without_pairs & InnerVertices S1 is Relation &
InputVertices S2 is without_pairs & InnerVertices S2 is Relation
by Th1,Th2,FACIRC_1:58,59;
then A5: InnerVertices S1 misses InputVertices S2 &
InnerVertices S2 misses InputVertices S1 by FACIRC_1:5;
A6: BitSubtracterOutput(x,y,c) = 2GatesCircOutput(x,y,c, f) &
BitSubtracterCirc(x,y,c) = 2GatesCircuit(x,y,c, f) by Def1,Def2;
dom s1 = the carrier of S1 by CIRCUIT1:4;
then A7: a1 = s1.x & a2 = s1.y & a3 = s1.c by A1,A2,FUNCT_1:70;
c <> [<*x,y*>, f];
then Following(t,2).2GatesCircOutput(x,y,c, f)
= Following(s1,2).2GatesCircOutput(x,y,c, f) &
Following(s1,2).2GatesCircOutput(x,y,c,f) = a1 'xor' a2 'xor' a3
by A5,A6,A7,FACIRC_1:32,64;
hence Following(s,2).BitSubtracterOutput(x,y,c) = a1 'xor' a2 'xor' a3
by A4,Def1;
dom s2 = the carrier of S2 by CIRCUIT1:4;
then a1 = s2.x & a2 = s2.y & a3 = s2.c by A1,A3,FUNCT_1:70;
then Following(t,2).BorrowOutput(x,y,c)
= Following(s2,2).BorrowOutput(x,y,c) &
Following(s2,2).BorrowOutput(x,y,c)
= 'not' a1 '&' a2 'or' a2 '&' a3 'or' 'not'
a1 '&' a3 by A5,Lm2,FACIRC_1:33;
hence Following(s,2).BorrowOutput(x,y,c)
= 'not' a1 '&' a2 'or' a2 '&' a3 'or' 'not' a1 '&' a3 by A4;
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 f = 'xor';
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;
A1: A = A1 +* A2 & S = S1+*S2 by Def8,Def9;
then 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 A1,FACIRC_1:26;
reconsider t = s as State of A1+*A2 by A1;
InputVertices S1 is without_pairs & InnerVertices S1 is Relation &
InputVertices S2 is without_pairs & InnerVertices S2 is Relation
by Th1,Th2,FACIRC_1:58,59;
then InnerVertices S1 misses InputVertices S2 &
InnerVertices S2 misses InputVertices S1 by FACIRC_1:5;
then A2: Following(s1,2) = Following(t,2)|the carrier of S1 &
Following(s1,3) = Following(t,3)|the carrier of S1 &
Following(s2,2) = Following(t,2)|the carrier of S2 &
Following(s2,3) = Following(t,3)|the carrier of S2 by FACIRC_1:30,31;
c <> [<*x,y*>, f] & A1 = 2GatesCircuit(x,y,c, f) by Def2;
then Following(s1,2) is stable by FACIRC_1:63;
then A3: Following(s1,2) = Following Following(s1,2) by CIRCUIT2:def 6
.= Following(s1,2+1) by FACIRC_1:12;
Following(s2,2) is stable by Th18;
then A4: Following(s2,2) = Following Following(s2,2) by CIRCUIT2:def 6
.= Following(s2,2+1) by FACIRC_1:12;
A5: Following(s,2+1) = Following Following(s,2) by FACIRC_1:12;
A6: dom Following(s,2) = the carrier of S &
dom Following(s,3) = the carrier of S &
dom Following(s1,2) = the carrier of S1 &
dom Following(s2,2) = the carrier of S2 by CIRCUIT1:4;
S = S1+*S2 by Def8;
then A7: the carrier of S = (the carrier of S1) \/ the carrier of S2
by CIRCCOMB:def 2;
now let a be set; assume a in the carrier of S;
then a in the carrier of S1 or a in the carrier of S2 by A7,XBOOLE_0:def
2
;
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 A1,A2,A3,A4,A6,FUNCT_1:70;
hence Following(s,2).a = (Following Following(s,2)).a by A3,A4,FACIRC_1:12
;
end;
hence Following(s,2) = Following Following(s,2) by A5,A6,FUNCT_1:9;
end;