:: Full Subtracter Circuit. Part {II}
:: by Shin'nosuke Yamaguchi , Grzegorz Bancerek and Katsumi Wasaki
::
:: Received February 25, 2003
:: Copyright (c) 2003-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 NUMBERS, NAT_1, FINSEQ_1, FSCIRC_1, FUNCT_1, ARYTM_3, XBOOLE_0,
MSUALG_1, FUNCT_4, CIRCCOMB, CARD_1, FINSEQ_2, MARGREL1, FUNCOP_1,
XBOOLEAN, STRUCT_0, PBOOLE, LATTICES, CIRCUIT1, RELAT_1, SUBSET_1,
MSAFREE2, ORDINAL4, XXREAL_0, TARSKI, TWOSCOMP, PARTFUN1, FACIRC_1,
CLASSES1, MCART_1, FSM_1, CIRCUIT2, GLIB_000, FSCIRC_2, FUNCT_7;
notations TARSKI, XBOOLE_0, ENUMSET1, XTUPLE_0, XFAMILY, SUBSET_1, CARD_1,
ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, MCART_1, RELAT_1, STRUCT_0, FUNCT_1,
FUNCT_2, FINSEQ_1, FINSEQ_2, FUNCT_7, PBOOLE, FUNCOP_1, MARGREL1,
BINARITH, CLASSES1, MSUALG_1, MSAFREE2, CIRCUIT1, CIRCUIT2, CIRCCOMB,
TWOSCOMP, FACIRC_1, FACIRC_2, FSCIRC_1, XXREAL_0;
constructors ENUMSET1, CLASSES1, BINARITH, CIRCUIT1, CIRCUIT2, TWOSCOMP,
FSCIRC_1, NAT_1, RELSET_1, XTUPLE_0, XREAL_0, NUMBERS, FUNCT_7, XFAMILY,
FUNCOP_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, NAT_1, FINSEQ_1,
MARGREL1, CARD_3, STRUCT_0, CIRCCOMB, FACIRC_1, CIRCCMB2, FACIRC_2,
MSAFREE2, FINSET_1, CARD_1, XTUPLE_0;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, CIRCUIT2, FACIRC_1, XBOOLE_0;
equalities TARSKI, MSAFREE2, FSCIRC_1, MARGREL1;
expansions TARSKI, CIRCUIT2;
theorems TARSKI, ZFMISC_1, ENUMSET1, NAT_1, ORDINAL1, FUNCT_1, FUNCT_2,
FINSEQ_1, FINSEQ_6, PBOOLE, CIRCUIT2, CIRCCOMB, FACIRC_1, CIRCCMB2,
CIRCUIT1, TWOSCOMP, FSCIRC_1, FACIRC_2, FUNCOP_1, XBOOLE_0, XBOOLE_1,
FINSEQ_2, XREAL_1, CLASSES1, PARTFUN1, CARD_1, XTUPLE_0, XREGULAR,
FUNCT_7;
schemes NAT_1, CIRCCMB2, PBOOLE;
begin
::------------------------------------------------------------
:: Definitions of n-Bit Full Subtracter Structure and Circuit
::------------------------------------------------------------
definition
let n be Nat;
let x,y be FinSequence;
deffunc o(set, Nat) = BorrowOutput(x .($2+1), y.($2+1), $1);
deffunc S(non empty ManySortedSign, set, Nat) =
$1 +* BitSubtracterWithBorrowStr(x .($3+1), y.($3+1), $2);
A1: 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE)
is unsplit gate`1=arity gate`2isBoolean non void non empty strict;
func n-BitSubtracterStr(x,y) ->
unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign means
:Def1:
ex f,g being ManySortedSet of NAT st
it = f.n & f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
g.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] &
for n being Nat, S being non empty ManySortedSign, z be set
st S = f.n & z = g.n
holds f.(n+1) = S +* BitSubtracterWithBorrowStr(x .(n+1), y.(n+1), z) &
g.(n+1) = BorrowOutput(x .(n+1), y.(n+1), z);
uniqueness
proof
for S1,S2 being unsplit gate`1=arity gate`2isBoolean non void non empty
strict non empty ManySortedSign st
(ex f,h being ManySortedSet of NAT st S1 = f.n &
f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
h.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] &
for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x, n)) &
(ex f,h being ManySortedSet of NAT st S2 = f.n &
f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
h.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] &
for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x, n))
holds S1 = S2 from CIRCCMB2:sch 9;
hence thesis;
end;
existence
proof
deffunc S(set, Nat) =
BitSubtracterWithBorrowStr(x .($2+1), y.($2+1), $1);
ex S being unsplit gate`1=arity gate`2isBoolean
non void non empty non empty strict ManySortedSign,
f,h being ManySortedSet of NAT st
S = f.n & f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
h.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] &
for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = h.n
holds f.(n+1) = S +* S(x,n) & h.(n+1) = o(x, n) from CIRCCMB2:sch 8(A1);
hence thesis;
end;
end;
definition
let n be Nat;
let x,y be FinSequence;
func n-BitSubtracterCirc(x,y) ->
Boolean gate`2=den strict Circuit of n-BitSubtracterStr(x,y) means
:Def2:
ex f,g,h being ManySortedSet of NAT st
n-BitSubtracterStr(x,y) = f.n & it = g.n &
f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
g.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
h.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] &
for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for z being set st S = f.n & A = g.n & z = h.n holds
f.(n+1) = S +* BitSubtracterWithBorrowStr(x .(n+1), y.(n+1), z) &
g.(n+1) = A +* BitSubtracterWithBorrowCirc(x .(n+1), y.(n+1), z) &
h.(n+1) = BorrowOutput(x .(n+1), y.(n+1), z);
uniqueness
proof
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE);
set A0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->TRUE);
set Sn = n-BitSubtracterStr(x,y);
set o0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE];
deffunc o(set,Nat) = BorrowOutput(x .($2+1), y.($2+1), $1);
deffunc S(non empty ManySortedSign, set, Nat) =
$1 +* BitSubtracterWithBorrowStr(x .($3+1), y.($3+1), $2);
deffunc A(non empty ManySortedSign, non-empty MSAlgebra over $1,
set, Nat) =
$2 +* BitSubtracterWithBorrowCirc(x .($4+1), y.($4+1), $3);
A1: for S being non empty ManySortedSign, A being non-empty MSAlgebra over S
for z being set, n being Nat holds
A(S,A,z,n) is non-empty MSAlgebra over S(S,z,n);
thus for A1,A2 being Boolean gate`2=den strict Circuit of Sn st
(ex f,g,h being ManySortedSet of NAT st Sn = f.n & A1 = g.n &
f.0 = S0 & g.0 = A0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set st S = f.n & A = g.n & x = h.n
holds f.(n+1) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x, n)) &
(ex f,g,h being ManySortedSet of NAT st Sn = f.n & A2 = g.n &
f.0 = S0 & g.0 = A0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set st S = f.n & A = g.n & x = h.n
holds f.(n+1) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x, n))
holds A1 = A2 from CIRCCMB2:sch 21(A1);
end;
existence
proof
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE);
set A0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->TRUE);
set Sn = n-BitSubtracterStr(x,y);
set o0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE];
deffunc o(set,Nat) = BorrowOutput(x .($2+1), y.($2+1), $1);
deffunc S(non empty ManySortedSign, set, Nat) =
$1 +* BitSubtracterWithBorrowStr(x .($3+1), y.($3+1), $2);
deffunc A(non empty ManySortedSign, non-empty MSAlgebra over $1,
set, Nat) =
$2 +* BitSubtracterWithBorrowCirc(x .($4+1), y.($4+1), $3);
A2: for S being unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign,
z being set, n being Nat holds S(S,z,n)
is unsplit gate`1=arity gate`2isBoolean non void strict;
A3: for S,S1 being unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign, A being Boolean gate`2=den strict Circuit of S
for z being set, n being Nat st S1 = S(S,z,n) holds A(S,A,z,n)
is Boolean gate`2=den strict Circuit of S1;
A4: for S being non empty ManySortedSign, A being non-empty MSAlgebra over S
for z being set, n being Nat holds
A(S,A,z,n) is non-empty MSAlgebra over S(S,z,n);
A5: ex f,h being ManySortedSet of NAT st n-BitSubtracterStr(x,y) = f.n & f.0 =
1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
h.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] &
for n being Nat, S being non empty ManySortedSign, z being set
st S = f.n & z = h.n holds f.(n+1) = S(S,z,n) & h.(n+1) = o(z,n) by Def1;
thus ex A being Boolean gate`2=den strict Circuit of Sn,
f,g,h being ManySortedSet of NAT st Sn = f.n & A = g.n &
f.0 = S0 & g.0 = A0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set st S = f.n & A = g.n & x = h.n
holds f.(n+1) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x, n)
from CIRCCMB2:sch 19(A2,A5,A4,A3);
end;
end;
definition
let n be Nat;
let x,y be FinSequence;
set c = [<*>, (0-tuples_on BOOLEAN)-->TRUE];
func n-BitBorrowOutput(x,y) ->
Element of InnerVertices (n-BitSubtracterStr(x,y)) means
:Def3:
ex h being ManySortedSet of NAT st
it = h.n & h.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] &
for n being Nat holds h.(n+1)
= BorrowOutput(x .(n+1), y.(n+1), h.n);
uniqueness
proof
let o1, o2 be Element of InnerVertices (n-BitSubtracterStr(x,y));
given h1 being ManySortedSet of NAT such that
A1: o1 = h1.n and
A2: h1.0 = c and
A3: for n being Nat holds h1.(n+1) = BorrowOutput(x .(n+1), y.(n+1), h1. n);
given h2 being ManySortedSet of NAT such that
A4: o2 = h2.n and
A5: h2.0 = c and
A6: for n being Nat holds h2.(n+1) = BorrowOutput(x .(n+1), y.(n+1), h2. n);
deffunc F(Nat,set) = BorrowOutput(x .($1+1), y.($1+1), $2);
A7: dom h1 = NAT by PARTFUN1:def 2;
A8: h1.0 = c by A2;
A9: for n being Nat holds h1.(n+1) = F(n,h1.n) by A3;
A10: dom h2 = NAT by PARTFUN1:def 2;
A11: h2.0 = c by A5;
A12: for n being Nat holds h2.(n+1) = F(n,h2.n) by A6;
h1 = h2 from NAT_1:sch 15(A7,A8,A9,A10,A11,A12);
hence thesis by A1,A4;
end;
existence
proof
defpred P[set,set,set] means not contradiction;
deffunc S(non empty ManySortedSign,set,Nat) =
$1 +* BitSubtracterWithBorrowStr(x .($3+1), y.($3+1), $2);
deffunc o(set,Nat) = BorrowOutput(x .($2+1), y.($2+1), $1);
consider f,g being ManySortedSet of NAT such that
A13: n-BitSubtracterStr(x,y) = f.n and
A14: f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) and
A15: g.0 = c and
A16: for n being Nat, S being non empty ManySortedSign,
z be set st S = f.n & z = g.n holds f.(n+1) = S(S,z,n) &
g.(n+1) = o(z,n) by Def1;
defpred P[Nat] means
ex S being non empty ManySortedSign st S = f.$1 & g.$1 in InnerVertices S;
InnerVertices 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) = {c}
by CIRCCOMB:42;
then c in InnerVertices 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE)
by TARSKI:def 1;
then
A17: P[ 0 ] by A14,A15;
A18: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat such that
A19: ex S being non empty ManySortedSign st S = f.i & g.i in InnerVertices S
and
A20: for S being non empty ManySortedSign st S = f.(i+1)
holds not g.(i+1) in InnerVertices S;
consider S being non empty ManySortedSign such that
A21: S = f.i and g.i in InnerVertices S by A19;
BorrowOutput(x .(i+1), y.(i+1), g.i) in
InnerVertices BitSubtracterWithBorrowStr(x .(i+1), y.(i+1), g.i)
by FACIRC_1:21;
then
A22: BorrowOutput(x .(i+1), y.(i+1), g.i) in InnerVertices (S+*
BitSubtracterWithBorrowStr(x .(i+1), y.(i+1), g.i)) by FACIRC_1:22;
A23: f.(i+1) = S +* BitSubtracterWithBorrowStr(x .(i+1), y.(i+1), g.i) by A16
,A21;
g.(i+1) = BorrowOutput(x .(i+1), y.(i+1), g.i) by A16,A21;
hence contradiction by A20,A22,A23;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A17,A18);
then ex S being non empty ManySortedSign st S = f.n & g.n in InnerVertices
S;
then reconsider o = g.n as Element of InnerVertices (n-BitSubtracterStr(x,y
)) by A13;
take o, g;
thus o = g.n & g.0 = c by A15;
let i be Nat;
A24: ex S being non empty ManySortedSign, x being set st
S = f.0 & x = g.0 & P[S, x, 0] by A14;
A25: for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = g.n & P[S, x, n] holds P[S(S,x,n), o(x, n), n+1];
for n being Nat ex S being non empty ManySortedSign st S = f.n
& P[S,g.n,n] from CIRCCMB2:sch 2(A24,A16,A25);
then ex S being non empty ManySortedSign st S = f.i;
hence thesis by A16;
end;
end;
::------------------------------------------------------------
:: Properties of n-Bit Full Subtracter Structure and Circuit
::------------------------------------------------------------
theorem Th1:
for x,y being FinSequence, f,g,h being ManySortedSet of NAT st
f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
g.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
h.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] &
for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for z being set st S = f.n & A = g.n & z = h.n holds
f.(n+1) = S +* BitSubtracterWithBorrowStr(x .(n+1), y.(n+1), z) &
g.(n+1) = A +* BitSubtracterWithBorrowCirc(x .(n+1), y.(n+1), z) &
h.(n+1) = BorrowOutput(x .(n+1), y.(n+1), z)
for n being Nat holds
n-BitSubtracterStr(x,y) = f.n & n-BitSubtracterCirc(x,y) = g.n &
n-BitBorrowOutput(x,y) = h.n
proof
let x,y be FinSequence, f,g,h be ManySortedSet of NAT;
deffunc o(set,Nat) = BorrowOutput(x .($2+1), y.($2+1), $1);
deffunc F(Nat,set) = BorrowOutput(x .($1+1), y.($1+1), $2);
deffunc S(non empty ManySortedSign,set,Nat) =
$1 +* BitSubtracterWithBorrowStr(x .($3+1), y.($3+1), $2);
deffunc A(non empty ManySortedSign,non-empty MSAlgebra over $1,
set,Nat) =
$2 +* BitSubtracterWithBorrowCirc(x .($4+1), y.($4+1), $3);
assume that
A1: f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
g.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->TRUE) and
A2: h.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] and
A3: for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for z being set st S = f.n & A = g.n & z = h.n holds f.(n+1) = S(S,z,n) &
g.(n+1) = A(S,A,z,n) & h.(n+1) = o(z,n);
let n be Nat;
consider f1,g1,h1 being ManySortedSet of NAT such that
A4: n-BitSubtracterStr(x,y) = f1.n and
A5: n-BitSubtracterCirc(x,y) = g1.n and
A6: f1.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) and
A7: g1.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->TRUE) and
A8: h1.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] and
A9: for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for z being set st S = f1.n & A = g1.n & z = h1.n holds
f1.(n+1) = S(S,z,n) & g1.(n+1) = A(S,A,z,n) & h1.(n+1) = o(z,n) by Def2;
A10: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S st
S = f.0 & A = g.0 by A1;
A11: f.0 = f1.0 & g.0 = g1.0 & h.0 = h1.0 by A1,A2,A6,A7,A8;
A12: for S being non empty ManySortedSign, A being non-empty MSAlgebra over S
for z being set, n being Nat holds
A(S,A,z,n) is non-empty MSAlgebra over S(S,z,n);
f = f1 & g = g1 & h = h1 from CIRCCMB2:sch 14(A10,A11,A3,A9,A12);
hence
n-BitSubtracterStr(x,y) = f.n & n-BitSubtracterCirc(x,y) = g.n by A4,A5;
A13: for n being Nat, S being non empty ManySortedSign,
z being set st S = f.n & z = h.n holds f.(n+1) = S(S,z,n) &
h.(n+1) = o(z,n) from CIRCCMB2:sch 15(A1,A3,A12);
A14: f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) by A1;
A15: for n being Nat, z being set st z = h.n holds
h.(n+1) = o(z,n) from CIRCCMB2:sch 3(A14,A13);
A16: dom h = NAT by PARTFUN1:def 2;
A17: h.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] by A2;
A18: for n being Nat holds h.(n+1) = F(n,h.n) by A15;
consider h1 being ManySortedSet of NAT such that
A19: n-BitBorrowOutput(x,y) = h1.n and
A20: h1.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] and
A21: for n being Nat holds h1.(n+1) = BorrowOutput(x .(n+1), y.(n+1), h1 .n)
by Def3;
A22: dom h1 = NAT by PARTFUN1:def 2;
A23: h1.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] by A20;
A24: for n being Nat holds h1.(n+1) = F(n,h1.n) by A21;
h = h1 from NAT_1:sch 15(A16,A17,A18,A22,A23,A24);
hence thesis by A19;
end;
theorem Th2:
for a,b being FinSequence holds
0-BitSubtracterStr(a,b) = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
0-BitSubtracterCirc(a,b) = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
0-BitBorrowOutput(a,b) = [<*>, (0-tuples_on BOOLEAN)-->TRUE]
proof
let a,b be FinSequence;
A1: ex f,g,h being ManySortedSet of NAT st ( 0-BitSubtracterStr(
a,b) = f.0)&( 0-BitSubtracterCirc(a,b) = g.0)&( f.0 = 1GateCircStr(<*>,(0
-tuples_on BOOLEAN)-->TRUE))&( g.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->
TRUE))&( h.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE])&( for n being Nat, S being
non empty ManySortedSign, A being non-empty MSAlgebra over S for z being set st
S = f.n & A = g.n & z = h.n holds f.(n+1) = S +* BitSubtracterWithBorrowStr(a .
(n+1), b.(n+1), z) & g.(n+1) = A +* BitSubtracterWithBorrowCirc(a .(n+1), b.(n+
1), z) & h.(n+1) = BorrowOutput(a.(n+1), b.(n+1), z)) by Def2;
hence 0-BitSubtracterStr(a,b)
= 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE);
thus 0-BitSubtracterCirc(a,b)
= 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->TRUE) by A1;
InnerVertices (0-BitSubtracterStr(a,b))
= { [<*>,(0-tuples_on BOOLEAN)-->TRUE] } by A1,CIRCCOMB:42;
hence thesis by TARSKI:def 1;
end;
theorem Th3:
for a,b being FinSequence, c being set st
c = [<*>, (0-tuples_on BOOLEAN)-->TRUE] holds
1-BitSubtracterStr(a,b) = 1GateCircStr(<*>, (0-tuples_on BOOLEAN)-->TRUE)+*
BitSubtracterWithBorrowStr(a.1, b.1, c) &
1-BitSubtracterCirc(a,b) = 1GateCircuit(<*>, (0-tuples_on BOOLEAN)-->TRUE)+*
BitSubtracterWithBorrowCirc(a.1, b.1, c) &
1-BitBorrowOutput(a,b) = BorrowOutput(a.1, b.1, c)
proof
let a,b being FinSequence, c be set such that
A1: c = [<*>, (0-tuples_on BOOLEAN)-->TRUE];
consider f,g,h being ManySortedSet of NAT such that
A2: 1-BitSubtracterStr(a,b) = f.1 and
A3: 1-BitSubtracterCirc(a,b) = g.1 and
A4: f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) and
A5: g.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->TRUE) and
A6: h.0 = c and
A7: for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for z be set st S = f.n & A = g.n & z = h.n
holds f.(n+1) = S+*BitSubtracterWithBorrowStr(a.(n+1),b.(n+1), z) &
g.(n+1) = A+*BitSubtracterWithBorrowCirc(a.(n+1),b.(n+1), z) &
h.(n+1) = BorrowOutput(a.(n+1), b.(n+1), z) by A1,Def2;
1-BitBorrowOutput(a,b) = h.(0+1) by A1,A4,A5,A6,A7,Th1;
hence thesis by A2,A3,A4,A5,A6,A7;
end;
theorem ::Col002a:
for a,b,c being set st c = [<*>, (0-tuples_on BOOLEAN)-->TRUE] holds
1-BitSubtracterStr(<*a*>,<*b*>)
= 1GateCircStr(<*>, (0-tuples_on BOOLEAN)-->TRUE)
+* BitSubtracterWithBorrowStr(a, b, c) & 1-BitSubtracterCirc(<*a*>,<*b*>)
= 1GateCircuit(<*>, (0-tuples_on BOOLEAN)-->TRUE)
+* BitSubtracterWithBorrowCirc(a, b, c) & 1-BitBorrowOutput(<*a*>,<*b*>)
= BorrowOutput(a, b, c)
proof
let a,b be set;
A1: <*a*>.1 = a;
<*b*>.1 = b;
hence thesis by A1,Th3;
end;
theorem Th5:
for n be Nat for p,q being FinSeqLen of n
for p1,p2, q1,q2 being FinSequence holds
n-BitSubtracterStr(p^p1, q^q1) = n-BitSubtracterStr(p^p2, q^q2) &
n-BitSubtracterCirc(p^p1, q^q1) = n-BitSubtracterCirc(p^p2, q^q2) &
n-BitBorrowOutput(p^p1, q^q1) = n-BitBorrowOutput(p^p2, q^q2)
proof
let n be Nat;
set c = [<*>, (0-tuples_on BOOLEAN)-->TRUE];
let p,q be FinSeqLen of n;
let p1,p2, q1,q2 be FinSequence;
deffunc o(set,Nat)
= BorrowOutput((p^p1) .($2+1), (q^q1).($2+1), $1);
deffunc S(non empty ManySortedSign,set,Nat) =
$1 +* BitSubtracterWithBorrowStr((p^p1) .($3+1), (q^q1).($3+1), $2);
deffunc A(non empty ManySortedSign,non-empty MSAlgebra over $1,
set,Nat) =
$2 +* BitSubtracterWithBorrowCirc((p^p1) .($4+1), (q^q1).($4+1), $3);
consider f1,g1,h1 being ManySortedSet of NAT such that
A1: n-BitSubtracterStr(p^p1,q^q1) = f1.n and
A2: n-BitSubtracterCirc(p^p1,q^q1) = g1.n and
A3: f1.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) and
A4: g1.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->TRUE) and
A5: h1.0 = c and
A6: for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for z be set st S = f1.n & A = g1.n & z = h1.n holds f1.(n+1) = S(S,z,n) &
g1.(n+1) = A(S,A,z,n) & h1.(n+1) = o(z,n) by Def2;
consider f2,g2,h2 being ManySortedSet of NAT such that
A7: n-BitSubtracterStr(p^p2,q^q2) = f2.n and
A8: n-BitSubtracterCirc(p^p2,q^q2) = g2.n and
A9: f2.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) and
A10: g2.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->TRUE) and
A11: h2.0 = c and
A12: for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for z be set st S = f2.n & A = g2.n & z = h2.n holds f2.(n+1) =
S +* BitSubtracterWithBorrowStr((p^p2).(n+1), (q^q2).(n+1), z) & g2.(n+1) =
A +* BitSubtracterWithBorrowCirc((p^p2).(n+1), (q^q2).(n+1), z) &
h2.(n+1) = BorrowOutput((p^p2).(n+1), (q^q2).(n+1), z) by Def2;
defpred L[Nat] means
$1 <= n implies h1.$1 = h2.$1 & f1.$1 = f2.$1 & g1.$1 = g2.$1;
A13: L[ 0 ] by A3,A4,A5,A9,A10,A11;
A14: for i being Nat st L[i] holds L[i+1]
proof
let i be Nat such that
A15: i <= n implies h1.i = h2.i & f1.i = f2.i & g1.i = g2.i and
A16: i+1 <= n;
A17: len p = n by CARD_1:def 7;
A18: len q = n by CARD_1:def 7;
A19: dom p = Seg n by A17,FINSEQ_1:def 3;
A20: dom q = Seg n by A18,FINSEQ_1:def 3;
0+1 <= i+1 by XREAL_1:6;
then
A21: i+1 in Seg n by A16,FINSEQ_1:1;
then
A22: (p^p1).(i+1) = p.(i+1) by A19,FINSEQ_1:def 7;
A23: (p^p2).(i+1) = p.(i+1) by A19,A21,FINSEQ_1:def 7;
A24: (q^q1).(i+1) = q.(i+1) by A20,A21,FINSEQ_1:def 7;
A25: (q^q2).(i+1) = q.(i+1) by A20,A21,FINSEQ_1:def 7;
defpred P[set,set,set,set] means not contradiction;
A26: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S,
x being set st S = f1.0 & A = g1.0 & x = h1.0 & P [S,A,x,0] by A3,A4;
A27: for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set st S = f1.n & A = g1.n & x = h1.n & P[S,A,x,n]
holds P[S(S,x,n), A(S,A,x,n), o(x, n), n+1];
A28: for S being non empty ManySortedSign, A being non-empty MSAlgebra over S
for z being set, n being Nat holds
A(S,A,z,n) is non-empty MSAlgebra over S(S,z,n);
for n being Nat
ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
st S = f1.n & A = g1.n & P[S,A,h1.n,n]
from CIRCCMB2:sch 13(A26,A6,A27,A28);
then consider S being non empty ManySortedSign,
A being non-empty MSAlgebra over S such that
A29: S = f1.i and
A30: A = g1.i;
thus h1.(i+1)
= BorrowOutput((p^p2).(i+1), (q^q2).(i+1), h2.i) by A6,A15,A16,A22,A23,A24
,A25,A29,A30,NAT_1:13
.= h2.(i+1) by A12,A15,A16,A29,A30,NAT_1:13;
thus f1.(i+1)
= S+*BitSubtracterWithBorrowStr((p^p2).(i+1), (q^q2).(i+1), h2.i)
by A6,A15,A16,A22,A23,A24,A25,A29,A30,NAT_1:13
.= f2.(i+1) by A12,A15,A16,A29,A30,NAT_1:13;
thus g1.(i+1)
= A+*BitSubtracterWithBorrowCirc((p^p2).(i+1), (q^q2).(i+1), h2.i)
by A6,A15,A16,A22,A23,A24,A25,A29,A30,NAT_1:13
.= g2.(i+1) by A12,A15,A16,A29,A30,NAT_1:13;
end;
A31: for i being Nat holds L[i] from NAT_1:sch 2(A13,A14);
hence n-BitSubtracterStr(p^p1, q^q1) = n-BitSubtracterStr(p^p2, q^q2) &
n-BitSubtracterCirc(p^p1, q^q1) = n-BitSubtracterCirc(p^p2, q^q2) by A1,A2,A7
,A8;
A32: n-BitBorrowOutput(p^p1, q^q1) = h1.n by A3,A4,A5,A6,Th1;
n-BitBorrowOutput(p^p2, q^q2) = h2.n by A9,A10,A11,A12,Th1;
hence thesis by A31,A32;
end;
theorem ::Col002b:
for n be Element of NAT for x,y being FinSeqLen of n for a,b being set holds
(n+1)-BitSubtracterStr(x^<*a*>, y^<*b*>) = n-BitSubtracterStr(x, y) +*
BitSubtracterWithBorrowStr(a, b, n-BitBorrowOutput(x, y)) &
(n+1)-BitSubtracterCirc(x^<*a*>, y^<*b*>) = n-BitSubtracterCirc(x, y) +*
BitSubtracterWithBorrowCirc(a, b, n-BitBorrowOutput(x, y)) &
(n+1)-BitBorrowOutput(x^<*a*>, y^<*b*>) =
BorrowOutput(a, b, n-BitBorrowOutput(x, y))
proof
let n be Element of NAT;
set c = [<*>, (0-tuples_on BOOLEAN)-->TRUE];
let x,y be FinSeqLen of n;
let a,b be set;
set p = x^<*a*>, q = y^<*b*>;
consider f,g,h being ManySortedSet of NAT such that
A1: n-BitSubtracterStr(p,q) = f.n and
A2: n-BitSubtracterCirc(p,q) = g.n and
A3: f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) and
A4: g.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->TRUE) and
A5: h.0 = c and
A6: for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for z be set st S = f.n & A = g.n & z = h.n holds
f.(n+1) = S +* BitSubtracterWithBorrowStr(p.(n+1), q.(n+1), z) &
g.(n+1) = A +* BitSubtracterWithBorrowCirc(p.(n+1), q.(n+1), z) &
h.(n+1) = BorrowOutput(p.(n+1), q.(n+1), z) by Def2;
A7: n-BitBorrowOutput(x^<*a*>, y^<*b*>) = h.n by A3,A4,A5,A6,Th1;
A8: (n+1)-BitSubtracterStr(x^<*a*>, y^<*b*>) = f.(n+1) by A3,A4,A5,A6,Th1;
A9: (n+1)-BitSubtracterCirc(x^<*a*>, y^<*b*>) = g.(n+1) by A3,A4,A5,A6,Th1;
A10: (n+1)-BitBorrowOutput(x^<*a*>, y^<*b*>) = h.(n+1) by A3,A4,A5,A6,Th1;
A11: len x = n by CARD_1:def 7;
A12: len y = n by CARD_1:def 7;
A13: p.(n+1) = a by A11,FINSEQ_1:42;
A14: q.(n+1) = b by A12,FINSEQ_1:42;
A15: x^<*> = x by FINSEQ_1:34;
A16: y^<*> = y by FINSEQ_1:34;
then
A17: n-BitSubtracterStr(p, q) = n-BitSubtracterStr(x, y) by A15,Th5;
A18: n-BitSubtracterCirc(p, q) = n-BitSubtracterCirc(x, y) by A15,A16,Th5;
n-BitBorrowOutput(p, q) = n-BitBorrowOutput(x, y) by A15,A16,Th5;
hence thesis by A1,A2,A6,A7,A8,A9,A10,A13,A14,A17,A18;
end;
theorem Th7:
for n be Nat for x,y being FinSequence holds
(n+1)-BitSubtracterStr(x, y) = n-BitSubtracterStr(x, y) +*
BitSubtracterWithBorrowStr(x .(n+1), y.(n+1), n-BitBorrowOutput(x, y)) &
(n+1)-BitSubtracterCirc(x, y) = n-BitSubtracterCirc(x, y) +*
BitSubtracterWithBorrowCirc(x .(n+1), y.(n+1), n-BitBorrowOutput(x, y)) &
(n+1)-BitBorrowOutput(x, y) =
BorrowOutput(x .(n+1), y.(n+1), n-BitBorrowOutput(x, y))
proof
let n be Nat;
let x,y be FinSequence;
set c = [<*>, (0-tuples_on BOOLEAN)-->TRUE];
consider f,g,h being ManySortedSet of NAT such that
A1: n-BitSubtracterStr(x,y) = f.n and
A2: n-BitSubtracterCirc(x,y) = g.n and
A3: f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) and
A4: g.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->TRUE) and
A5: h.0 = c and
A6: for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for z be set st S = f.n & A = g.n & z = h.n holds
f.(n+1) = S +* BitSubtracterWithBorrowStr(x .(n+1), y.(n+1), z) &
g.(n+1) = A +* BitSubtracterWithBorrowCirc(x .(n+1), y.(n+1), z) &
h.(n+1) = BorrowOutput(x .(n+1), y.(n+1), z) by Def2;
A7: n-BitBorrowOutput(x, y) = h.n by A3,A4,A5,A6,Th1;
A8: (n+1)-BitSubtracterStr(x, y) = f.(n+1) by A3,A4,A5,A6,Th1;
A9: (n+1)-BitSubtracterCirc(x, y) = g.(n+1) by A3,A4,A5,A6,Th1;
(n+1)-BitBorrowOutput(x, y) = h.(n+1) by A3,A4,A5,A6,Th1;
hence thesis by A1,A2,A6,A7,A8,A9;
end;
::------------------------------------------------------------
:: Inner and Input-Vertex of n-Bit Full Subtracter Structure
::------------------------------------------------------------
theorem Th8:
for n,m be Nat st n <= m for x,y being FinSequence holds
InnerVertices (n-BitSubtracterStr(x,y)) c=
InnerVertices (m-BitSubtracterStr(x,y))
proof
let n,m be Nat such that
A1: n <= m;
let x,y be FinSequence;
consider i being Nat such that
A2: m = n+i by A1,NAT_1:10;
reconsider i as Element of NAT by ORDINAL1:def 12;
defpred L[Nat] means InnerVertices (n-BitSubtracterStr(x,y)) c=
InnerVertices ((n+$1)-BitSubtracterStr(x,y));
A3: L[ 0 ];
A4: for j being Nat st L[j] holds L[j+1]
proof
let j be Nat;
assume
A5: InnerVertices (n-BitSubtracterStr(x,y)) c=
InnerVertices ((n+j)-BitSubtracterStr(x,y));
A6: InnerVertices (n-BitSubtracterStr(x,y)) c=
InnerVertices (n-BitSubtracterStr(x,y)) \/
InnerVertices (BitSubtracterWithBorrowStr(x .((n+j)+1), y.((n+j)+1),
(n+j)-BitBorrowOutput(x, y))) by XBOOLE_1:7;
InnerVertices (n-BitSubtracterStr(x,y)) \/
InnerVertices (BitSubtracterWithBorrowStr(x .((n+j)+1), y.((n+j)+1),
(n+j)-BitBorrowOutput(x, y))) c=
InnerVertices ((n+j)-BitSubtracterStr(x,y)) \/
InnerVertices (BitSubtracterWithBorrowStr(x .((n+j)+1), y.((n+j)+1),
(n+j)-BitBorrowOutput(x, y))) by A5,XBOOLE_1:9;
then InnerVertices (n-BitSubtracterStr(x,y)) c=
InnerVertices ((n+j)-BitSubtracterStr(x,y)) \/
InnerVertices (BitSubtracterWithBorrowStr(x .((n+j)+1), y.((n+j)+1),
(n+j)-BitBorrowOutput(x, y))) by A6;
then InnerVertices (n-BitSubtracterStr(x,y)) c=
InnerVertices (((n+j)-BitSubtracterStr(x,y) +*
BitSubtracterWithBorrowStr(x .((n+j)+1), y.((n+j)+1),
(n+j)-BitBorrowOutput(x, y)))) by FACIRC_1:27;
hence thesis by Th7;
end;
A7: for j being Nat holds L[j] from NAT_1:sch 2(A3,A4);
m = n+i by A2;
hence thesis by A7;
end;
theorem
for n be Element of NAT for x,y being FinSequence holds
InnerVertices ((n+1)-BitSubtracterStr(x,y)) =
InnerVertices (n-BitSubtracterStr(x,y)) \/
InnerVertices BitSubtracterWithBorrowStr(x .(n+1), y.(n+1),
n-BitBorrowOutput(x,y))
proof
let n be Element of NAT;
let x,y be FinSequence;
InnerVertices (n-BitSubtracterStr(x,y) +*
BitSubtracterWithBorrowStr(x .(n+1), y.(n+1), n-BitBorrowOutput(x, y))) =
InnerVertices (n-BitSubtracterStr(x,y)) \/
InnerVertices (BitSubtracterWithBorrowStr(x .(n+1), y.(n+1),
n-BitBorrowOutput(x, y))) by FACIRC_1:27;
hence thesis by Th7;
end;
definition
let k,n be Nat such that
A1: k >= 1 and
A2: k <= n;
let x,y be FinSequence;
func (k,n)-BitSubtracterOutput(x,y) ->
Element of InnerVertices (n-BitSubtracterStr(x,y)) means
:Def4:
ex i being Element of NAT st k = i+1 &
it = BitSubtracterOutput(x .k, y.k, i-BitBorrowOutput(x,y));
uniqueness;
existence
proof consider i being Nat such that
A3: k = 1+i by A1,NAT_1:10;
reconsider i as Element of NAT by ORDINAL1:def 12;
set o = BitSubtracterOutput(x .k, y.k, i-BitBorrowOutput(x,y));
A4: InnerVertices (k-BitSubtracterStr(x,y)) c=
InnerVertices (n-BitSubtracterStr(x,y)) by A2,Th8;
A5: o in InnerVertices BitSubtracterWithBorrowStr(x .(i+1), y.(i+1),
i-BitBorrowOutput(x, y)) by A3,FACIRC_1:21;
A6: k-BitSubtracterStr(x,y) = (i-BitSubtracterStr(x, y)) +*
BitSubtracterWithBorrowStr(x .(i+1), y.(i+1), i-BitBorrowOutput(x, y))
by A3,Th7;
reconsider o as Element of
BitSubtracterWithBorrowStr(x .(i+1), y.(i+1), i-BitBorrowOutput(x, y))
by A5;
(the carrier of
BitSubtracterWithBorrowStr(x .(i+1), y.(i+1), i-BitBorrowOutput(x, y)))
\/ the carrier of i-BitSubtracterStr(x,y)
= the carrier of k-BitSubtracterStr(x,y) by A6,CIRCCOMB:def 2;
then o in the carrier of k-BitSubtracterStr(x,y) by XBOOLE_0:def 3;
then o in InnerVertices (k-BitSubtracterStr(x,y)) by A5,A6,CIRCCOMB:15;
hence thesis by A3,A4;
end;
end;
theorem
for n,k being Element of NAT st k < n for x,y being FinSequence holds
(k+1,n)-BitSubtracterOutput(x,y) =
BitSubtracterOutput(x .(k+1), y.(k+1), k-BitBorrowOutput(x,y))
proof
let n,k be Element of NAT such that
A1: k < n;
let x,y be FinSequence;
A2: k+1 >= 1 by NAT_1:11;
k+1 <= n by A1,NAT_1:13;
then ex i being Element of NAT st ( k+1 = i+1)&( (k+1,n)
-BitSubtracterOutput(x,y) = BitSubtracterOutput(x .(k+1), y.( k+1), i
-BitBorrowOutput(x,y))) by A2,Def4;
hence thesis;
end;
theorem
for n being Element of NAT for x,y being FinSequence holds
InnerVertices (n-BitSubtracterStr(x,y)) is Relation
proof
let n be Element of NAT;
let x,y be FinSequence;
defpred P[Nat] means
InnerVertices ($1-BitSubtracterStr(x,y)) is Relation;
0-BitSubtracterStr(x,y) = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)--> TRUE )
by Th2;
then
A1: P[ 0 ] by FACIRC_1:38;
A2: now
let i be Nat;
assume
A3: P[i];
A4: (i+1)-BitSubtracterStr(x, y) = i-BitSubtracterStr(x, y) +*
BitSubtracterWithBorrowStr(x .(i+1), y.(i+1),
i-BitBorrowOutput(x, y)) by Th7;
InnerVertices BitSubtracterWithBorrowStr(x .(i+1), y.(i+1),
i-BitBorrowOutput(x, y)) is Relation by FSCIRC_1:22;
hence P[i+1] by A3,A4,FACIRC_1:3;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th12:
for x,y,c being set holds InnerVertices BorrowIStr(x,y,c) =
{[<*x,y*>,and2a], [<*y,c*>,and2], [<*x,c*>,and2a]}
proof
let x,y,c be set;
A1: 1GateCircStr(<*x,y*>,and2a) +* 1GateCircStr(<*y,c*>,and2) tolerates
1GateCircStr(<*x,c*>,and2a) by CIRCCOMB:47;
A2: 1GateCircStr(<*x,y*>,and2a) tolerates 1GateCircStr(<*y,c*>,and2)
by CIRCCOMB:47;
InnerVertices BorrowIStr(x,y,c) =
InnerVertices(1GateCircStr(<*x,y*>,and2a) +* 1GateCircStr(<*y,c*>,and2)) \/
InnerVertices(1GateCircStr(<*x,c*>,and2a)) by A1,CIRCCOMB:11
.= InnerVertices(1GateCircStr(<*x,y*>,and2a)) \/
InnerVertices(1GateCircStr(<*y,c*>,and2)) \/
InnerVertices(1GateCircStr(<*x,c*>,and2a)) by A2,CIRCCOMB:11
.= {[<*x,y*>,and2a]} \/ InnerVertices(1GateCircStr(<*y,c*>,and2)) \/
InnerVertices(1GateCircStr(<*x,c*>,and2a)) by CIRCCOMB:42
.= {[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]} \/
InnerVertices(1GateCircStr(<*x,c*>,and2a)) by CIRCCOMB:42
.= {[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]} \/ {[<*x,c*>,and2a]}
by CIRCCOMB:42
.= {[<*x,y*>,and2a],[<*y,c*>,and2]} \/ {[<*x,c*>,and2a]}
by ENUMSET1:1
.= {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]}
by ENUMSET1:3;
hence thesis;
end;
theorem Th13:
for x,y,c being set st
x <> [<*y,c*>, and2] & y <> [<*x,c*>, and2a] & c <> [<*x,y*>, and2a]
holds InputVertices BorrowIStr(x,y,c) = {x,y,c}
proof
let x,y,c be set;
assume that
A1: x <> [<*y,c*>, and2] and
A2: y <> [<*x,c*>, and2a] and
A3: c <> [<*x,y*>, and2a];
A4: 1GateCircStr(<*x,y*>,and2a) tolerates 1GateCircStr(<*y,c*>,and2)
by CIRCCOMB:47;
A5: y in {1,y} by TARSKI:def 2;
A6: y in {2,y} by TARSKI:def 2;
A7: {1,y} in {{1},{1,y}} by TARSKI:def 2;
A8: {2,y} in {{2},{2,y}} by TARSKI:def 2;
<*y,c*> = <*y*>^<*c*> by FINSEQ_1:def 9;
then
A9: <*y*> c= <*y,c*> by FINSEQ_6:10;
<*y*> = {[1,y]} by FINSEQ_1:def 5;
then
A10: [1,y] in <*y*> by TARSKI:def 1;
A11: <*y,c*> in {<*y,c*>} by TARSKI:def 1;
A12: {<*y,c*>} in {{<*y,c*>},{<*y,c*>,and2}} by TARSKI:def 2;
then
A13: y <> [<*y,c*>,and2] by A5,A7,A9,A10,A11,XREGULAR:9;
A14: c in {2,c} by TARSKI:def 2;
A15: {2,c} in {{2},{2,c}} by TARSKI:def 2;
dom<*y,c*> = Seg 2 by FINSEQ_1:89;
then
A16: 2 in dom <*y,c*> by FINSEQ_1:1;
<*y,c*>.2 = c;
then [2,c] in <*y,c*> by A16,FUNCT_1:1;
then
A17: c <> [<*y,c*>,and2] by A11,A12,A14,A15,XREGULAR:9;
dom<*x,y*> = Seg 2 by FINSEQ_1:89;
then
A18: 2 in dom <*x,y*> by FINSEQ_1:1;
<*x,y*>.2 = y;
then
A19: [2,y] in <*x,y*> by A18,FUNCT_1:1;
A20: <*x,y*> in {<*x,y*>} by TARSKI:def 1;
{<*x,y*>} in {{<*x,y*>},{<*x,y*>,and2a}} by TARSKI:def 2;
then y <> [<*x,y*>,and2a] by A6,A8,A19,A20,XREGULAR:9;
then
A21: not [<*x,y*>,and2a] in {y,c} by A3,TARSKI:def 2;
A22: x in {1,x} by TARSKI:def 2;
A23: {1,x} in {{1},{1,x}} by TARSKI:def 2;
<*x,y*> = <*x*>^<*y*> by FINSEQ_1:def 9;
then
A24: <*x*> c= <*x,y*> by FINSEQ_6:10;
<*x*> = {[1,x]} by FINSEQ_1:def 5;
then
A25: [1,x] in <*x*> by TARSKI:def 1;
A26: <*x,y*> in {<*x,y*>} by TARSKI:def 1;
{<*x,y*>} in {{<*x,y*>},{<*x,y*>,and2a}} by TARSKI:def 2;
then
A27: x <> [<*x,y*>,and2a] by A22,A23,A24,A25,A26,XREGULAR:9;
A28: not c in {[<*x,y*>,and2a], [<*y,c*>,and2]} by A3,A17,TARSKI:def 2;
A29: not x in {[<*x,y*>,and2a], [<*y,c*>,and2]} by A1,A27,TARSKI:def 2;
A30: c in {2,c} by TARSKI:def 2;
A31: {2,c} in {{2},{2,c}} by TARSKI:def 2;
dom<*x,c*> = Seg 2 by FINSEQ_1:89;
then
A32: 2 in dom <*x,c*> by FINSEQ_1:1;
<*x,c*>.2 = c;
then
A33: [2,c] in <*x,c*> by A32,FUNCT_1:1;
A34: <*x,c*> in {<*x,c*>} by TARSKI:def 1;
{<*x,c*>} in {{<*x,c*>},{<*x,c*>,and2a}} by TARSKI:def 2;
then
A35: c <> [<*x,c*>,and2a] by A30,A31,A33,A34,XREGULAR:9;
A36: x in {1,x} by TARSKI:def 2;
A37: {1,x} in {{1},{1,x}} by TARSKI:def 2;
<*x,c*> = <*x*>^<*c*> by FINSEQ_1:def 9;
then
A38: <*x*> c= <*x,c*> by FINSEQ_6:10;
<*x*> = {[1,x]} by FINSEQ_1:def 5;
then
A39: [1,x] in <*x*> by TARSKI:def 1;
A40: <*x,c*> in {<*x,c*>} by TARSKI:def 1;
{<*x,c*>} in {{<*x,c*>},{<*x,c*>,and2a}} by TARSKI:def 2;
then x <> [<*x,c*>,and2a] by A36,A37,A38,A39,A40,XREGULAR:9;
then
A41: not [<*x,c*>,and2a] in {x,y,c} by A2,A35,ENUMSET1:def 1;
InputVertices BorrowIStr(x,y,c)
= (InputVertices(1GateCircStr(<*x,y*>,and2a) +*
1GateCircStr(<*y,c*>,and2)) \ InnerVertices(1GateCircStr(<*x,c*>,and2a))) \/
(InputVertices(1GateCircStr(<*x,c*>,and2a)) \
InnerVertices(1GateCircStr(<*x,y*>,and2a) +*
1GateCircStr(<*y,c*>,and2))) by CIRCCMB2:5,CIRCCOMB:47
.= ((InputVertices(1GateCircStr(<*x,y*>,and2a)) \
InnerVertices(1GateCircStr(<*y,c*>,and2))) \/
(InputVertices(1GateCircStr(<*y,c*>,and2)) \
InnerVertices(1GateCircStr(<*x,y*>,and2a)))) \
InnerVertices(1GateCircStr(<*x,c*>,and2a)) \/
(InputVertices(1GateCircStr(<*x,c*>,and2a)) \
InnerVertices(1GateCircStr(<*x,y*>,and2a) +*
1GateCircStr(<*y,c*>,and2))) by CIRCCMB2:5,CIRCCOMB:47
.= ((InputVertices(1GateCircStr(<*x,y*>,and2a)) \
InnerVertices(1GateCircStr(<*y,c*>,and2))) \/
(InputVertices(1GateCircStr(<*y,c*>,and2)) \
InnerVertices(1GateCircStr(<*x,y*>,and2a)))) \
InnerVertices(1GateCircStr(<*x,c*>,and2a)) \/
(InputVertices(1GateCircStr(<*x,c*>,and2a)) \
(InnerVertices(1GateCircStr(<*x,y*>,and2a)) \/
InnerVertices(1GateCircStr(<*y,c*>,and2)))) by A4,CIRCCOMB:11
.= ((InputVertices(1GateCircStr(<*x,y*>,and2a)) \ {[<*y,c*>,and2]}) \/
(InputVertices(1GateCircStr(<*y,c*>,and2)) \
InnerVertices(1GateCircStr(<*x,y*>,and2a)))) \
InnerVertices(1GateCircStr(<*x,c*>,and2a)) \/
(InputVertices(1GateCircStr(<*x,c*>,and2a)) \
(InnerVertices(1GateCircStr(<*x,y*>,and2a)) \/
InnerVertices(1GateCircStr(<*y,c*>,and2)))) by CIRCCOMB:42
.= ((InputVertices(1GateCircStr(<*x,y*>,and2a)) \ {[<*y,c*>,and2]}) \/
(InputVertices(1GateCircStr(<*y,c*>,and2)) \ {[<*x,y*>,and2a]})) \
InnerVertices(1GateCircStr(<*x,c*>,and2a)) \/
(InputVertices(1GateCircStr(<*x,c*>,and2a)) \
(InnerVertices(1GateCircStr(<*x,y*>,and2a)) \/
InnerVertices(1GateCircStr(<*y,c*>,and2)))) by CIRCCOMB:42
.= ((InputVertices(1GateCircStr(<*x,y*>,and2a)) \ {[<*y,c*>,and2]}) \/
(InputVertices(1GateCircStr(<*y,c*>,and2)) \
{[<*x,y*>,and2a]})) \ {[<*x,c*>,and2a]} \/
(InputVertices(1GateCircStr(<*x,c*>,and2a)) \
(InnerVertices(1GateCircStr(<*x,y*>,and2a)) \/
InnerVertices(1GateCircStr(<*y,c*>,and2)))) by CIRCCOMB:42
.= ((InputVertices(1GateCircStr(<*x,y*>,and2a)) \ {[<*y,c*>,and2]}) \/
(InputVertices(1GateCircStr(<*y,c*>,and2)) \
{[<*x,y*>,and2a]})) \ {[<*x,c*>,and2a]} \/
(InputVertices(1GateCircStr(<*x,c*>,and2a)) \ ({[<*x,y*>,and2a]} \/
InnerVertices(1GateCircStr(<*y,c*>,and2)))) by CIRCCOMB:42
.= ((InputVertices(1GateCircStr(<*x,y*>,and2a)) \ {[<*y,c*>,and2]}) \/
(InputVertices(1GateCircStr(<*y,c*>,and2)) \
{[<*x,y*>,and2a]})) \ {[<*x,c*>,and2a]} \/
(InputVertices(1GateCircStr(<*x,c*>,and2a)) \
({[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]})) by CIRCCOMB:42
.= (({x,y} \
{[<*y,c*>,and2]}) \/ (InputVertices(1GateCircStr(<*y,c*>,and2)) \
{[<*x,y*>,and2a]})) \ {[<*x,c*>,and2a]} \/
(InputVertices(1GateCircStr(<*x,c*>,and2a)) \
({[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]})) by FACIRC_1:40
.=(({x,y} \ {[<*y,c*>,and2]}) \/ ({y,c} \
{[<*x,y*>,and2a]})) \ {[<*x,c*>,and2a]} \/
(InputVertices(1GateCircStr(<*x,c*>,and2a)) \
({[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]})) by FACIRC_1:40
.=(({x,y} \ {[<*y,c*>,and2]}) \/ ({y,c} \ {[<*x,y*>,and2a]})) \
{[<*x,c*>,and2a]} \/
({x,c} \ ({[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]})) by FACIRC_1:40
.= (({x,y} \ {[<*y,c*>,and2]}) \/ ({y,c} \ {[<*x,y*>,and2a]})) \
{[<*x,c*>,and2a]} \/
({x,c} \ {[<*x,y*>,and2a],[<*y,c*>,and2]}) by ENUMSET1:1
.= (({x,y} \/ ({y,c} \ {[<*x,y*>,and2a]})) \ {[<*x,c*>,and2a]}) \/
({x,c} \ {[<*x,y*>,and2a],[<*y,c*>,and2]}) by A1,A13,FACIRC_2:1
.= ({x,y} \/ {y,c}) \ {[<*x,c*>,and2a]} \/
({x,c} \ {[<*x,y*>,and2a],[<*y,c*>,and2]}) by A21,ZFMISC_1:57
.= ({x,y} \/ {y,c}) \ {[<*x,c*>,and2a]} \/ {x,c} by A28,A29,ZFMISC_1:63
.= {x,y,y,c} \ {[<*x,c*>,and2a]} \/ {x,c} by ENUMSET1:5
.= {y,y,x,c} \ {[<*x,c*>,and2a]} \/ {x,c} by ENUMSET1:67
.= {y,x,c} \ {[<*x,c*>,and2a]} \/ {x,c} by ENUMSET1:31
.= {x,y,c} \ {[<*x,c*>,and2a]} \/ {x,c} by ENUMSET1:58
.= {x,y,c} \/ {x,c} by A41,ZFMISC_1:57
.= {x,y,c,c,x} by ENUMSET1:9
.= {x,y,c,c} \/ {x} by ENUMSET1:10
.= {c,c,x,y} \/ {x} by ENUMSET1:73
.= {c,x,y} \/ {x} by ENUMSET1:31
.= {c,x,y,x} by ENUMSET1:6
.= {x,x,y,c} by ENUMSET1:70
.= {x,y,c} by ENUMSET1:31;
hence thesis;
end;
theorem Th14:
for x,y,c being set holds InnerVertices BorrowStr(x,y,c) =
{[<*x,y*>,and2a], [<*y,c*>,and2], [<*x,c*>,and2a]} \/ {BorrowOutput(x,y,c)}
proof
let x,y,c be set;
set xy = [<*x,y*>, and2a], yc = [<*y,c*>, and2], xc = [<*x,c*>, and2a];
set Cxy = 1GateCircStr(<*x,y*>, and2a), Cyc = 1GateCircStr(<*y,c*>, and2),
Cxc = 1GateCircStr(<*x,c*>, and2a), Cxyc = 1GateCircStr
(<*[<*x,y*>, and2a], [<*y,c*>, and2], [<*x,c*>, and2a]*>, or3);
A1: Cxy tolerates (Cyc +* Cxc +* Cxyc) by CIRCCOMB:47;
A2: Cyc tolerates (Cxc +* Cxyc) by CIRCCOMB:47;
A3: Cxc tolerates Cxyc by CIRCCOMB:47;
A4: InnerVertices (Cyc +* (Cxc +* Cxyc)) =
InnerVertices Cyc \/ InnerVertices (Cxc +* Cxyc) by A2,CIRCCOMB:11;
A5: InnerVertices (Cxc +* Cxyc) =
InnerVertices Cxc \/ InnerVertices Cxyc by A3,CIRCCOMB:11;
thus
InnerVertices BorrowStr(x,y,c) =
InnerVertices (Cxy +* (Cyc +* Cxc) +* Cxyc) by CIRCCOMB:6
.= InnerVertices (Cxy +* (Cyc +* Cxc +* Cxyc)) by CIRCCOMB:6
.= InnerVertices Cxy \/ InnerVertices (Cyc +* Cxc +* Cxyc)
by A1,CIRCCOMB:11
.= InnerVertices Cxy \/ InnerVertices (Cyc +* (Cxc +* Cxyc))
by CIRCCOMB:6
.= InnerVertices Cxy \/ InnerVertices Cyc \/
(InnerVertices Cxc \/ InnerVertices Cxyc) by A4,A5,XBOOLE_1:4
.= InnerVertices Cxy \/ InnerVertices Cyc \/
InnerVertices Cxc \/ InnerVertices Cxyc by XBOOLE_1:4
.= {xy} \/ InnerVertices Cyc \/
InnerVertices Cxc \/ InnerVertices Cxyc by CIRCCOMB:42
.= {xy} \/ {yc} \/ InnerVertices Cxc \/ InnerVertices Cxyc by CIRCCOMB:42
.= {xy} \/ {yc} \/ {xc} \/ InnerVertices Cxyc by CIRCCOMB:42
.= {xy, yc} \/ {xc} \/ InnerVertices Cxyc by ENUMSET1:1
.= {xy, yc, xc} \/ InnerVertices Cxyc by ENUMSET1:3
.= {xy, yc, xc} \/ {BorrowOutput(x,y,c)} by CIRCCOMB:42;
end;
theorem Th15:
for x,y,c being set st
x <> [<*y,c*>, and2] & y <> [<*x,c*>, and2a] & c <> [<*x,y*>, and2a]
holds InputVertices BorrowStr(x,y,c) = {x,y,c}
proof
let x,y,c be set;
set xy = [<*x,y*>, and2a], yc = [<*y,c*>, and2], xc = [<*x,c*>, and2a];
set S = 1GateCircStr(<*xy, yc, xc*>, or3);
A1: InnerVertices S = {[<*xy, yc, xc*>, or3]} by CIRCCOMB:42;
A2: InputVertices S = rng <*xy, yc, xc*> by CIRCCOMB:42
.= {xy, yc, xc} by FINSEQ_2:128;
set BI = BorrowIStr(x,y,c);
assume that
A3: x <> yc and
A4: y <> xc and
A5: c <> xy;
rng <*x,c*> = {x,c} by FINSEQ_2:127;
then
A6: x in rng <*x,c*> by TARSKI:def 2;
len <*xy, yc, xc*> = 3 by FINSEQ_1:45;
then
A7: Seg 3 = dom <*xy, yc, xc*> by FINSEQ_1:def 3;
then
A8: 3 in dom <*xy, yc, xc*> by FINSEQ_1:1;
<*xy, yc, xc*>.3 = xc;
then [3,xc] in <*xy, yc, xc*> by A8,FUNCT_1:1;
then xc in rng <*xy, yc, xc*> by XTUPLE_0:def 13;
then
A9: the_rank_of xc in the_rank_of [<*xy, yc, xc*>, or3] by CLASSES1:82;
rng <*x,y*> = {x,y} by FINSEQ_2:127;
then
A10: y in rng <*x,y*> by TARSKI:def 2;
A11: 1 in dom <*xy, yc, xc*> by A7,FINSEQ_1:1;
<*xy, yc, xc*>.1 = xy;
then [1,xy] in <*xy, yc, xc*> by A11,FUNCT_1:1;
then xy in rng <*xy, yc, xc*> by XTUPLE_0:def 13;
then
A12: the_rank_of xy in the_rank_of [<*xy, yc, xc*>, or3] by CLASSES1:82;
rng <*y,c*> = {y,c} by FINSEQ_2:127;
then
A13: c in rng <*y,c*> by TARSKI:def 2;
A14: 2 in dom <*xy, yc, xc*> by A7,FINSEQ_1:1;
<*xy, yc, xc*>.2 = yc;
then [2,yc] in <*xy, yc, xc*> by A14,FUNCT_1:1;
then yc in rng <*xy, yc, xc*> by XTUPLE_0:def 13;
then
A15: the_rank_of yc in the_rank_of [<*xy, yc, xc*>, or3] by CLASSES1:82;
A16: {xy, yc, xc} \ {xy, yc, xc} = {} by XBOOLE_1:37;
A17: {x, y, c} \ {[<*xy, yc, xc*>, or3]} = {x, y, c}
proof
thus {x,y,c} \ {[<*xy, yc, xc*>, or3]} c= {x,y,c};
let a be object;
assume
A18: a in {x,y,c};
then a = x or a = y or a = c by ENUMSET1:def 1;
then a <> [<*xy, yc, xc*>, or3] by A6,A9,A10,A12,A13,A15,CLASSES1:82;
then not a in {[<*xy, yc, xc*>, or3]} by TARSKI:def 1;
hence thesis by A18,XBOOLE_0:def 5;
end;
thus InputVertices BorrowStr(x,y,c)
= ((InputVertices BI) \ InnerVertices S) \/
((InputVertices S) \ InnerVertices BI) by CIRCCMB2:5,CIRCCOMB:47
.= {x,y,c} \/ ({xy, yc, xc} \ InnerVertices BI) by A1,A2,A3,A4,A5,A17,Th13
.= {x,y,c} \/ {} by A16,Th12
.= {x,y,c};
end;
theorem Th16:
for x,y,c being set st
x <> [<*y,c*>, and2] & y <> [<*x,c*>, and2a] & c <> [<*x,y*>, and2a] &
c <> [<*x,y*>, 'xor'] holds
InputVertices BitSubtracterWithBorrowStr(x,y,c) = {x,y,c}
proof
let x,y,c be set such that
A1: x <> [<*y,c*>, and2] and
A2: y <> [<*x,c*>, and2a] and
A3: c <> [<*x,y*>, and2a] and
A4: c <> [<*x,y*>, 'xor'];
A5: InputVertices 2GatesCircStr(x,y,c, 'xor') = {x,y,c} by A4,FACIRC_1:57;
InputVertices BorrowStr(x,y,c) = {x,y,c} by A1,A2,A3,Th15;
hence thesis by A5,CIRCCOMB:47,FACIRC_2:21;
end;
theorem Th17:
for x,y,c being 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 set;
2GatesCircStr(x,y,c, 'xor') tolerates BorrowStr(x,y,c) by CIRCCOMB:47;
then InnerVertices BitSubtracterWithBorrowStr(x,y,c) =
InnerVertices 2GatesCircStr(x,y,c, 'xor') \/
InnerVertices BorrowStr(x,y,c) by CIRCCOMB:11
.= {[<*x,y*>, 'xor'], 2GatesCircOutput(x,y,c,'xor')} \/
InnerVertices BorrowStr(x,y,c) by FACIRC_1:56
.= {[<*x,y*>, 'xor'], 2GatesCircOutput(x,y,c,'xor')} \/
({[<*x,y*>,and2a], [<*y,c*>,and2], [<*x,c*>,and2a]} \/
{BorrowOutput(x,y,c)}) by Th14
.= {[<*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;
hence thesis;
end;
registration
let n be Nat;
let x,y be FinSequence;
cluster n-BitBorrowOutput(x,y) -> pair;
coherence
proof
A1: ex h being ManySortedSet of NAT st ( 0-BitBorrowOutput(x,y)
= h.0)&( h.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE])&( for n being Nat holds h.(
n+1) = BorrowOutput(x .(n+1), y.(n+1), h.n)) by Def3;
defpred P[Nat] means $1-BitBorrowOutput(x,y) is pair;
A2: P[ 0 ] by A1;
A3: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
(n+1)-BitBorrowOutput(x, y) =
BorrowOutput(x .(n+1), y.(n+1), n-BitBorrowOutput(x, y)) by Th7
.= [<*[<*x .(n+1),y.(n+1)*>, and2a],
[<*y.(n+1),n-BitBorrowOutput(x, y)*>, and2],
[<*x .(n+1),n-BitBorrowOutput(x, y)*>, and2a]*>, or3];
hence thesis;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
end;
theorem Th18:
for x,y being FinSequence, n being Nat holds
(n-BitBorrowOutput(x,y))`1 = <*> &
(n-BitBorrowOutput(x,y))`2 = (0-tuples_on BOOLEAN)-->TRUE &
proj1 (n-BitBorrowOutput(x,y))`2 = 0-tuples_on BOOLEAN or
card (n-BitBorrowOutput(x,y))`1 = 3 & (n-BitBorrowOutput(x,y))`2 = or3 &
proj1 (n-BitBorrowOutput(x,y))`2 = 3-tuples_on BOOLEAN
proof
let x,y be FinSequence;
defpred P[Nat] means ($1-BitBorrowOutput(x,y))`1 = <*> &
($1-BitBorrowOutput(x,y))`2 = (0-tuples_on BOOLEAN)-->TRUE &
proj1 ($1-BitBorrowOutput(x,y))`2 = 0-tuples_on BOOLEAN or
card ($1-BitBorrowOutput(x,y))`1 = 3 & ($1-BitBorrowOutput(x,y))`2 = or3 &
proj1 ($1-BitBorrowOutput(x,y))`2 = 3-tuples_on BOOLEAN;
A1: dom ((0-tuples_on BOOLEAN)-->TRUE) = 0-tuples_on BOOLEAN by FUNCOP_1:13;
0-BitBorrowOutput(x,y) = [<*>, (0-tuples_on BOOLEAN)-->TRUE] by Th2;
then
A2: P[ 0 ] by A1;
A3: now
let n be Nat;
assume P[n];
set c = n-BitBorrowOutput(x, y);
A4: (n+1)-BitBorrowOutput(x, y) = BorrowOutput(x .(n+1), y.(n+1), c) by Th7
.= [<*[<*x .(n+1),y.(n+1)*>, and2a], [<*y.(n+1),c*>, and2],
[<*x .(n+1),c*>, and2a]*>, or3];
A5: dom or3 = 3-tuples_on BOOLEAN by FUNCT_2:def 1;
thus P[n+1] by A4,A5,FINSEQ_1:45;
end;
thus for i being Nat holds P[i] from NAT_1:sch 2(A2,A3);
end;
theorem Th19:
for n being Nat, x,y being FinSequence, p being set holds
n-BitBorrowOutput(x,y) <> [p, and2] & n-BitBorrowOutput(x,y) <> [p, and2a] &
n-BitBorrowOutput(x,y) <> [p, 'xor']
proof
let n be Nat, x,y be FinSequence, p be set;
A1: dom and2 = 2-tuples_on BOOLEAN by FUNCT_2:def 1;
A2: dom and2a = 2-tuples_on BOOLEAN by FUNCT_2:def 1;
A3: dom 'xor' = 2-tuples_on BOOLEAN by FUNCT_2:def 1;
A4: proj1 [p, and2]`2 = 2-tuples_on BOOLEAN by A1;
A5: proj1 [p, and2a]`2 = 2-tuples_on BOOLEAN by A2;
A6: proj1 [p, 'xor']`2 = 2-tuples_on BOOLEAN by A3;
proj1 (n-BitBorrowOutput(x,y))`2 = 0-tuples_on BOOLEAN or
proj1 (n-BitBorrowOutput(x,y))`2 = 3-tuples_on BOOLEAN by Th18;
hence thesis by A4,A5,A6,FINSEQ_2:110;
end;
::-----------------------------------------------------
:: Relation and Pair for n-Bit Full Subtracter
::-----------------------------------------------------
theorem Th20:
for f,g being nonpair-yielding FinSequence for n being Nat holds
InputVertices ((n+1)-BitSubtracterStr(f,g)) =
(InputVertices (n-BitSubtracterStr(f,g)))\/
((InputVertices BitSubtracterWithBorrowStr(f.(n+1),g.(n+1),
n-BitBorrowOutput(f,g)) \ {n-BitBorrowOutput(f,g)})) &
InnerVertices (n-BitSubtracterStr(f,g)) is Relation &
InputVertices (n-BitSubtracterStr(f,g)) is without_pairs
proof
let f,g be nonpair-yielding FinSequence;
deffunc Sn(Nat) = $1-BitSubtracterStr(f,g);
deffunc S(set, Nat)
= BitSubtracterWithBorrowStr(f.($2+1),g.($2+1), $1);
deffunc F(Nat) = $1-BitBorrowOutput(f,g);
consider h being ManySortedSet of NAT such that
A1: for n being Element of NAT holds h.n = F(n) from PBOOLE:sch 5;
A2: for n being Nat holds h.n = F(n)
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A1;
end;
deffunc h(Nat) = h.$1;
deffunc o(set, Nat) = BorrowOutput(f.($2+1),g.($2+1), $1);
set k = (0-tuples_on BOOLEAN)-->TRUE;
A3: 0-BitSubtracterStr(f,g) = 1GateCircStr(<*>, k) by Th2;
then
A4: InnerVertices Sn(0) is Relation by FACIRC_1:38;
A5: InputVertices Sn(0) is without_pairs by A3,FACIRC_1:39;
h(0) = 0-BitBorrowOutput(f,g) by A2;
then
A6: h.0 in InnerVertices Sn(0);
A7: for n being Nat, x being set
holds InnerVertices S(x,n) is Relation by FSCIRC_1:22;
A8: now
let n be Element of NAT, x be set such that
A9: x = h(n);
A10: h(n) = n-BitBorrowOutput(f,g) by A2;
then
A11: x <> [<*f.(n+1),g.(n+1)*>, and2a] by A9,Th19;
x <> [<*f.(n+1),g.(n+1)*>, 'xor'] by A9,A10,Th19;
hence InputVertices S(x, n) = {f.(n+1), g.(n+1), x} by A11,Th16;
end;
A12: for n being Nat, x being set st x = h.n holds
(InputVertices S(x, n)) \ {x} is without_pairs
proof
let n be Nat, x be set such that
A13: x = h(n);
n in NAT by ORDINAL1:def 12;
then
A14: InputVertices S(x, n) = {f.(n+1), g.(n+1), x} by A8,A13;
thus (InputVertices S(x, n)) \ {x} is without_pairs
proof
let a be pair object;
assume
A15: a in (InputVertices S(x, n)) \ {x};
then a in InputVertices S(x, n) by XBOOLE_0:def 5;
then
A16: a = f.(n+1) or a = g.(n+1) or a = x by A14,ENUMSET1:def 1;
not a in {x} by A15,XBOOLE_0:def 5;
hence contradiction by A16,TARSKI:def 1;
end;
end;
A17: now
let n be Nat, S be non empty ManySortedSign, x be set;
A18: n in NAT by ORDINAL1:def 12;
assume that
A19: S = Sn(n) and
A20: x = h.n;
A21: x = n-BitBorrowOutput(f,g) by A2,A20;
A22: h(n+1) = (n+1)-BitBorrowOutput(f,g) by A2;
thus Sn(n+1) = S +* S(x,n) by A19,A21,Th7;
thus h.(n+1) = o(x, n) by A21,A22,Th7;
InputVertices S(x, n) = {f.(n+1), g.(n+1), x} by A8,A18,A20;
hence x in InputVertices S(x,n) by ENUMSET1:def 1;
A23: InnerVertices S(x, n) =
{[<*f.(n+1),g.(n+1)*>, 'xor'], 2GatesCircOutput(f.(n+1),g.(n+1),x,'xor')}
\/ {[<*f.(n+1),g.(n+1)*>,and2a], [<*g.(n+1),x*>,and2],
[<*f.(n+1),x*>,and2a]} \/ {BorrowOutput(f.(n+1),g.(n+1),x)} by Th17;
o(x,n) in {o(x,n)} by TARSKI:def 1;
hence o(x, n) in InnerVertices S(x, n) by A23,XBOOLE_0:def 3;
end;
A24: for n being Nat holds InputVertices Sn(n+1) =
(InputVertices Sn(n))\/((InputVertices S(h.(n),n)) \ {h.(n)}) &
InnerVertices Sn(n) is Relation &
InputVertices Sn(n) is without_pairs from CIRCCMB2:sch 11(A4,A5,A6,A7
,A12,
A17);
let n be Nat;
h.n = n-BitBorrowOutput(f,g) by A2;
hence thesis by A24;
end;
theorem
for n being Nat
for x,y being nonpair-yielding FinSeqLen of n holds
InputVertices (n-BitSubtracterStr(x,y)) = rng x \/ rng y
proof
defpred P[Nat] means
for x,y being nonpair-yielding FinSeqLen of $1 holds
InputVertices ($1-BitSubtracterStr(x,y)) = rng x \/ rng y;
A1: P[ 0 ]
proof
let x,y be nonpair-yielding FinSeqLen of 0;
set f = (0-tuples_on BOOLEAN)-->TRUE;
0-BitSubtracterStr(x,y) = 1GateCircStr(<*>, f) by Th2;
hence InputVertices (0-BitSubtracterStr(x,y)) = rng <*> by CIRCCOMB:42
.= rng x \/ rng y;
end;
A2: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat such that
A3: P[i];
let x,y be nonpair-yielding FinSeqLen of i+1;
consider x9 being nonpair-yielding FinSeqLen of i,
z1 being non pair set such that
A4: x = x9^<*z1*> by FACIRC_2:34;
consider y9 being nonpair-yielding FinSeqLen of i,
z2 being non pair set such that
A5: y = y9^<*z2*> by FACIRC_2:34;
set S = (i+1)-BitSubtracterStr(x, y);
A6: 1 in Seg 1 by FINSEQ_1:1;
then
A7: 1 in dom <*z1*> by FINSEQ_1:def 8;
len x9 = i by CARD_1:def 7;
then
A8: x .(i+1) = <*z1*>.1 by A4,A7,FINSEQ_1:def 7
.= z1;
A9: 1 in dom <*z2*> by A6,FINSEQ_1:def 8;
len y9 = i by CARD_1:def 7;
then
A10: y .(i+1) = <*z2*>.1 by A5,A9,FINSEQ_1:def 7
.= z2;
A11: {z1,z2,i-BitBorrowOutput(x,y)} = {i-BitBorrowOutput(x,y),z1,z2}
by ENUMSET1:59;
A12: rng x = rng x9 \/ rng <*z1*> by A4,FINSEQ_1:31
.= rng x9 \/ {z1} by FINSEQ_1:38;
A13: rng y = rng y9 \/ rng <*z2*> by A5,FINSEQ_1:31
.= rng y9 \/ {z2} by FINSEQ_1:38;
A14: i-BitBorrowOutput(x,y) <> [<*z1,z2*>, and2a] by Th19;
A15: i-BitBorrowOutput(x,y) <> [<*z1,z2*>, 'xor'] by Th19;
A16: x9 = x9^{} by FINSEQ_1:34;
y9 = y9^{} by FINSEQ_1:34;
then i-BitSubtracterStr(x,y) = i-BitSubtracterStr(x9,y9) by A4,A5,A16,Th5;
hence InputVertices S = (InputVertices (i-BitSubtracterStr(x9,y9)))\/
((InputVertices BitSubtracterWithBorrowStr(z1,z2,
i-BitBorrowOutput(x,y)) \ {i-BitBorrowOutput(x,y)})) by A8,A10,Th20
.= (rng x9 \/ rng y9)\/
((InputVertices BitSubtracterWithBorrowStr(z1,z2,
i-BitBorrowOutput(x,y)) \ {i-BitBorrowOutput(x,y)})) by A3
.= (rng x9 \/ rng y9)\/
({z1,z2,i-BitBorrowOutput(x,y)} \ {i-BitBorrowOutput(x,y)}) by A14,A15,Th16
.= (rng x9 \/ rng y9)\/ {z1,z2} by A11,ENUMSET1:86
.= rng x9 \/ rng y9 \/ ({z1} \/ {z2}) by ENUMSET1:1
.= rng x9 \/ rng y9 \/ {z1} \/ {z2} by XBOOLE_1:4
.= rng x9 \/ {z1} \/ rng y9 \/ {z2} by XBOOLE_1:4
.= rng x \/ rng y by A12,A13,XBOOLE_1:4;
end;
thus for i being Nat holds P[i] from NAT_1:sch 2(A1,A2);
end;
::-----------------------------------------------------
:: Following theorem for n-Bit Full Subtracter Circuit
::-----------------------------------------------------
Lm1: for x,y,c being 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 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: dom s = the carrier of S by CIRCUIT1:3;
A6: x in the carrier of S by FSCIRC_1:6;
A7: y in the carrier of S by FSCIRC_1:6;
A8: c in the carrier of S by FSCIRC_1:6;
[<*x,y*>,and2a] in InnerVertices BorrowStr(x,y,c) by FSCIRC_1:7;
hence (Following s).[<*x,y*>,and2a] = and2a.(s*<*x,y*>) by A4,FACIRC_1:35
.= and2a.<*a1,a2*> by A1,A2,A5,A6,A7,FINSEQ_2:125
.= 'not' a1 '&' a2 by TWOSCOMP:def 2;
[<*y,c*>,and2] in InnerVertices BorrowStr(x,y,c) by FSCIRC_1:7;
hence (Following s).[<*y,c*>,and2] = and2.(s*<*y,c*>) by A4,FACIRC_1:35
.= and2.<*a2,a3*> by A2,A3,A5,A7,A8,FINSEQ_2:125
.= a2 '&' a3 by FACIRC_1:def 6;
[<*x,c*>,and2a] in InnerVertices BorrowStr(x,y,c) by FSCIRC_1:7;
hence (Following s).[<*x,c*>,and2a] = and2a.(s*<*x,c*>) by A4,FACIRC_1:35
.= and2a.<*a1,a3*> by A1,A3,A5,A6,A8,FINSEQ_2:125
.= 'not' a1 '&' a3 by TWOSCOMP:def 2;
end;
theorem Th22:
for x,y,c being 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 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] and
A2: a2 = s.[<*y,c*>,and2] and
A3: a3 = s.[<*x,c*>,and2a];
set xy =[<*x,y*>,and2a], yc = [<*y,c*>,and2], cx = [<*x,c*>,and2a];
set S = BorrowStr(x,y,c);
A4: InnerVertices S = the carrier' of S by FACIRC_1:37;
A5: dom s = the carrier of S by CIRCUIT1:3;
reconsider xy, yc, cx as Element of InnerVertices S by FSCIRC_1:7;
thus (Following s).BorrowOutput(x,y,c)
= or3.(s*<*xy, yc, cx*>) by A4,FACIRC_1:35
.= or3.<*a1,a2,a3*> by A1,A2,A3,A5,FINSEQ_2:126
.= a1 'or' a2 'or' a3 by FACIRC_1:def 7;
end;
Lm2: for x,y,c being set st
x <> [<*y,c*>, and2] & y <> [<*x,c*>, and2a] & c <> [<*x,y*>, and2a]
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 set such that
A1: x <> [<*y,c*>, and2] and
A2: y <> [<*x,c*>, and2a] and
A3: c <> [<*x,y*>, and2a];
let s be State of BorrowCirc(x,y,c);
let a1,a2,a3 be Element of BOOLEAN such that
A4: a1 = s.x and
A5: a2 = s.y and
A6: a3 = s.c;
set xy =[<*x,y*>,and2a], yc = [<*y,c*>,and2], cx = [<*x,c*>,and2a];
set S = BorrowStr(x,y,c);
reconsider x9 = x, y9 = y, c9 = c as Vertex of S by FSCIRC_1:6;
A7: InputVertices S = {x,y,c} by A1,A2,A3,Th15;
then
A8: x in InputVertices S by ENUMSET1:def 1;
A9: y in InputVertices S by A7,ENUMSET1:def 1;
A10: c in InputVertices S by A7,ENUMSET1:def 1;
A11: (Following s).x9 = s.x by A8,CIRCUIT2:def 5;
A12: (Following s).y9 = s.y by A9,CIRCUIT2:def 5;
A13: (Following s).c9 = s.c by A10,CIRCUIT2:def 5;
A14: Following(s,2) = Following Following s by FACIRC_1:15;
A15: (Following s).xy = 'not' a1 '&' a2 by A4,A5,A6,Lm1;
A16: (Following s).yc = a2 '&' a3 by A4,A5,A6,Lm1;
(Following s).cx = 'not' a1 '&' a3 by A4,A5,A6,Lm1;
hence (Following(s,2)).BorrowOutput(x,y,c) =
'not' a1 '&' a2 'or' a2 '&' a3 'or' 'not' a1 '&' a3 by A14,A15,A16,Th22;
thus thesis by A4,A5,A6,A11,A12,A13,A14,Lm1;
end;
theorem Th23:
for x,y,c being set st
x <> [<*y,c*>, and2] & y <> [<*x,c*>, and2a] & c <> [<*x,y*>, and2a]
for s being State of BorrowCirc(x,y,c)
holds Following(s,2) is stable
proof
let x,y,c be set;
set S = BorrowStr(x,y,c);
assume that
A1: x <> [<*y,c*>, and2] and
A2: y <> [<*x,c*>, and2a] and
A3: c <> [<*x,y*>, and2a];
let s be State of BorrowCirc(x,y,c);
A4: dom Following Following(s,2) = the carrier of S by CIRCUIT1:3;
A5: dom Following(s,2) = the carrier of S by CIRCUIT1:3;
reconsider xx = x, yy = y, cc = c as Vertex of S by FSCIRC_1:6;
set a1 = s.xx, a2 = s.yy, a3 = s.cc;
set ffs = Following(s,2), fffs = Following ffs;
A6: a1 = s.x;
A7: a2 = s.y;
A8: a3 = s.c;
A9: ffs.BorrowOutput(x,y,c) = 'not' a1 '&' a2 'or' a2 '&' a3 'or' 'not' a1
'&' a3 by A1,A2,A3,Lm2;
A10: ffs.[<*x,y*>,and2a] = 'not' a1 '&' a2 by A1,A2,A3,A8,Lm2;
A11: ffs.[<*y,c*>,and2] = a2 '&' a3 by A1,A2,A3,A6,Lm2;
A12: ffs.[<*x,c*>,and2a] = 'not' a1 '&' a3 by A1,A2,A3,A7,Lm2;
A13: ffs = Following Following s by FACIRC_1:15;
A14: InputVertices S = {x,y,c} by A1,A2,A3,Th15;
then
A15: x in InputVertices S by ENUMSET1:def 1;
A16: y in InputVertices S by A14,ENUMSET1:def 1;
A17: c in InputVertices S by A14,ENUMSET1:def 1;
A18: (Following s).x = a1 by A15,CIRCUIT2:def 5;
A19: (Following s).y = a2 by A16,CIRCUIT2:def 5;
A20: (Following s).c = a3 by A17,CIRCUIT2:def 5;
A21: ffs.x = a1 by A13,A15,A18,CIRCUIT2:def 5;
A22: ffs.y = a2 by A13,A16,A19,CIRCUIT2:def 5;
A23: ffs.c = a3 by A13,A17,A20,CIRCUIT2:def 5;
now
let a be object;
assume
A24: a in the carrier of S;
then reconsider v = a as Vertex of S;
A25: v in InputVertices S \/ InnerVertices S by A24,XBOOLE_1:45;
thus ffs.a = (fffs).a proof per cases by A25,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 Th14;
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 A9,A10,A11,A12,A21,A22,A23,Lm1,Th22;
end;
end;
end;
hence ffs = fffs by A4,A5,FUNCT_1:2;
end;
theorem
for x,y,c being set st
x <> [<*y,c*>, and2] & y <> [<*x,c*>, and2a] & c <> [<*x,y*>, and2a] &
c <> [<*x,y*>, 'xor']
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 set such that
A1: x <> [<*y,c*>, and2] and
A2: y <> [<*x,c*>, and2a] and
A3: c <> [<*x,y*>, and2a] and
A4: c <> [<*x,y*>, 'xor'];
set f = 'xor';
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
A5: a1 = s.x and
A6: a2 = s.y and
A7: a3 = s.c;
A8: x in the carrier of S1 by FACIRC_1:60;
A9: y in the carrier of S1 by FACIRC_1:60;
A10: c in the carrier of S1 by FACIRC_1:60;
A11: x in the carrier of S2 by FSCIRC_1:6;
A12: y in the carrier of S2 by FSCIRC_1:6;
A13: c in the carrier of S2 by FSCIRC_1:6;
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;
A14: InputVertices S2 = {x,y,c} by A1,A2,A3,Th15;
A15: InnerVertices S1 misses InputVertices S1 by XBOOLE_1:79;
A16: InnerVertices S2 misses InputVertices S2 by XBOOLE_1:79;
A17: InnerVertices S1 misses InputVertices S2 by A4,A14,A15,FACIRC_1:57;
A18: InnerVertices S2 misses InputVertices S1 by A4,A14,A16,FACIRC_1:57;
A19: dom s1 = the carrier of S1 by CIRCUIT1:3;
then
A20: a1 = s1.x by A5,A8,FUNCT_1:47;
A21: a2 = s1.y by A6,A9,A19,FUNCT_1:47;
A22: a3 = s1.c by A7,A10,A19,FUNCT_1:47;
(Following(t,2)).2GatesCircOutput(x,y,c, f) = (Following(s1,2)).
2GatesCircOutput(x,y,c, f) by A18,FACIRC_1:32;
hence (Following(s,2)).BitSubtracterOutput(x,y,c) = a1 'xor' a2 'xor' a3
by A4,A20,A21,A22,FACIRC_1:64;
A23: dom s2 = the carrier of S2 by CIRCUIT1:3;
then
A24: a1 = s2.x by A5,A11,FUNCT_1:47;
A25: a2 = s2.y by A6,A12,A23,FUNCT_1:47;
A26: a3 = s2.c by A7,A13,A23,FUNCT_1:47;
(Following(t,2)).BorrowOutput(x,y,c) = (Following(s2,2)).BorrowOutput(x
,y,c) by A17,FACIRC_1:33;
hence thesis by A1,A2,A3,A24,A25,A26,Lm2;
end;
theorem Th25:
for x,y,c being set st
x <> [<*y,c*>, and2] & y <> [<*x,c*>, and2a] & c <> [<*x,y*>, and2a] &
c <> [<*x,y*>, 'xor']
for s being State of BitSubtracterWithBorrowCirc(x,y,c)
holds Following(s,2) is stable
proof
let x,y,c be set such that
A1: x <> [<*y,c*>, and2] and
A2: y <> [<*x,c*>, and2a] and
A3: c <> [<*x,y*>, and2a] and
A4: c <> [<*x,y*>, '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;
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;
A5: InputVertices S2 = {x,y,c} by A1,A2,A3,Th15;
A6: InnerVertices S1 misses InputVertices S1 by XBOOLE_1:79;
A7: InnerVertices S2 misses InputVertices S2 by XBOOLE_1:79;
A8: InnerVertices S1 misses InputVertices S2 by A4,A5,A6,FACIRC_1:57;
A9: InnerVertices S2 misses InputVertices S1 by A4,A5,A7,FACIRC_1:57;
then
A10: Following(s1,2) = Following(t,2)|the carrier of S1 by FACIRC_1:30;
A11: Following(s1,3) = Following(t,3)|the carrier of S1 by A9,FACIRC_1:30;
A12: Following(s2,2) = Following(t,2)|the carrier of S2 by A8,FACIRC_1:31;
A13: Following(s2,3) = Following(t,3)|the carrier of S2 by A8,FACIRC_1:31;
Following(s1,2) is stable by A4,FACIRC_1:63;
then
A14: Following(s1,2) = Following Following(s1,2)
.= Following(s1,2+1) by FACIRC_1:12;
Following(s2,2) is stable by A1,A2,A3,Th23;
then
A15: Following(s2,2) = Following Following(s2,2)
.= Following(s2,2+1) by FACIRC_1:12;
A16: Following(s,2+1) = Following Following(s,2) by FACIRC_1:12;
A17: dom Following(s,2) = the carrier of S by CIRCUIT1:3;
A18: dom Following(s,3) = the carrier of S by CIRCUIT1:3;
A19: dom Following(s1,2) = the carrier of S1 by CIRCUIT1:3;
A20: dom Following(s2,2) = the carrier of S2 by CIRCUIT1:3;
A21: the carrier of S = (the carrier of S1) \/ the carrier of S2
by CIRCCOMB:def 2;
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 A21,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 A10,A11,A12,A13,A14,A15,A19,A20
,FUNCT_1:47;
hence (Following(s,2)).a = (Following Following(s,2)).a
by A14,A15,FACIRC_1:12;
end;
hence Following(s,2) = Following Following(s,2) by A16,A17,A18,FUNCT_1:2;
end;
theorem
for n being Element of NAT for x,y being nonpair-yielding FinSeqLen of n
for s being State of n-BitSubtracterCirc(x,y)
holds Following(s,1+2*n) is stable
proof
let n be Element of NAT, f,g be nonpair-yielding FinSeqLen of n;
deffunc S(set,Nat)
= BitSubtracterWithBorrowStr(f.($2+1), g.($2+1), $1);
deffunc A(set,Nat)
= BitSubtracterWithBorrowCirc(f.($2+1), g.($2+1), $1);
deffunc o(set,Nat) = BorrowOutput(f.($2+1), g.($2+1), $1);
set S0 = 1GateCircStr(<*>, (0-tuples_on BOOLEAN)-->TRUE);
set A0 = 1GateCircuit(<*>, (0-tuples_on BOOLEAN)-->TRUE);
set N = (1,2) followed_by In(n,NAT);
A1: N.0 = 1 by FUNCT_7:122;
A2: N.1 = 2 by FUNCT_7:123;
A3: N.2 = n by FUNCT_7:124;
deffunc n(Element of NAT) = N.$1;
A4: for x being set, n being Nat holds
A(x,n) is Boolean gate`2=den strict Circuit of S(x,n);
A5: now
let s be State of A0;
Following(s, 1) = Following s by FACIRC_1:14;
hence Following(s, n(0)) is stable by A1,CIRCCMB2:2;
end;
deffunc F(Element of NAT) = $1-BitBorrowOutput(f,g);
consider h being ManySortedSet of NAT such that
A6: for n being Element of NAT holds h.n = F(n) from PBOOLE:sch 5;
A7: for n being Nat, x being set
for A being non-empty Circuit of S(x,n) st x = h.(n) & A = A(x,n)
for s being State of A holds Following(s, n(1)) is stable
proof
let n be Nat, x be set, A be non-empty Circuit of S(x,n);
A8: n in NAT by ORDINAL1:def 12;
assume x = h.n;
then
A9: x = n-BitBorrowOutput(f,g) by A6,A8;
then
A10: x <> [<*f.(n+1),g.(n+1)*>, and2a] by Th19;
x <> [<*f.(n+1),g.(n+1)*>, 'xor'] by A9,Th19;
hence thesis by A2,A10,Th25;
end;
set Sn = n-BitSubtracterStr(f,g);
set An = n-BitSubtracterCirc(f,g);
set o0 = 0-BitBorrowOutput(f,g);
consider f1,g1,h1 being ManySortedSet of NAT such that
A11: n-BitSubtracterStr(f,g) = f1.n and
A12: n-BitSubtracterCirc(f,g) = g1.n and
A13: f1.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) and
A14: g1.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->TRUE) and
A15: h1.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] and
A16: for n being Nat, S being non empty ManySortedSign, A being
non-empty MSAlgebra over S for z being set st S = f1.n & A = g1.n & z = h1.n
holds f1.(n+1) = S +* BitSubtracterWithBorrowStr(f.(n+1), g.(n+1), z) & g1.(n+1
) = A +* BitSubtracterWithBorrowCirc(f.(n+1), g.(n+1), z) & h1.(n+1) =
BorrowOutput(f.(n+1), g.(n+1), z)
by Def2;
now
let i be object;
assume i in NAT;
then reconsider j = i as Element of NAT;
thus h1.i = j-BitBorrowOutput(f,g) by A13,A14,A15,A16,Th1
.= h.i by A6;
end;
then
A17: h1 = h by PBOOLE:3;
A18: ex u,v being ManySortedSet of NAT st Sn = u.(n(2)) & An = v.(n(2)) &
u.0 = S0 & v.0 = A0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign,
A1 being non-empty MSAlgebra over S
for x being set, A2 being non-empty MSAlgebra over S(x,n)
st S = u.n & A1 = v.n & x = h.n & A2 = A(x,n)
holds u.(n+1) = S +* S(x,n) & v.(n+1) = A1 +* A2 & h.(n+1) = o(x, n)
proof
take f1, g1;
thus thesis by A3,A6,A11,A12,A13,A14,A16,A17;
end;
A19: InnerVertices S0 is Relation & InputVertices S0 is without_pairs
by FACIRC_1:38,39;
A20: [<*>, (0-tuples_on BOOLEAN)-->TRUE] = o0 by Th2;
InnerVertices S0 = {[<*>, (0-tuples_on BOOLEAN)-->TRUE]} by CIRCCOMB:42;
then
A21: h.0 = o0 & o0 in InnerVertices S0 by A6,A20,TARSKI:def 1;
A22: for n being Nat, x being set
holds InnerVertices S(x,n) is Relation by FSCIRC_1:22;
A23: for n being Nat, x being set st x = h.n holds
(InputVertices S(x, n)) \ {x} is without_pairs
proof
let n be Nat, x be set such that
A24: x = h.n;
n in NAT by ORDINAL1:def 12;
then
A25: x = n-BitBorrowOutput(f,g) by A6,A24;
then
A26: x <> [<*f.(n+1),g.(n+1)*>, and2a] by Th19;
x <> [<*f.(n+1),g.(n+1)*>, 'xor'] by A25,Th19;
then
A27: InputVertices S(x, n) = {f.(n+1),g.(n+1),x} by A26,Th16;
let a be pair object;
assume
A28: a in (InputVertices S(x, n)) \ {x};
then
A29: a in {f.(n+1),g.(n+1),x} by A27,XBOOLE_0:def 5;
A30: not a in {x} by A28,XBOOLE_0:def 5;
a = f.(n+1) or a = g.(n+1) or a = x by A29,ENUMSET1:def 1;
hence thesis by A30,TARSKI:def 1;
end;
A31: for n being Nat, x being set st x = h.n holds h.(n+1) = o(x, n) &
x in InputVertices S(x,n) & o(x, n) in InnerVertices S(x, n)
proof
let n be Nat, x be set such that
A32: x = h.n;
n in NAT by ORDINAL1:def 12;
then
A33: x = n-BitBorrowOutput(f,g) by A6,A32;
h.(n+1) = (n+1)-BitBorrowOutput(f,g) by A6;
hence h.(n+1) = o(x, n) by A33,Th7;
A34: x <> [<*f.(n+1),g.(n+1)*>, and2a] by A33,Th19;
x <> [<*f.(n+1),g.(n+1)*>, 'xor'] by A33,Th19;
then InputVertices S(x, n) = {f.(n+1),g.(n+1),x} by A34,Th16;
hence x in InputVertices S(x, n) by ENUMSET1:def 1;
set xx = f.(n+1), xy = g.(n+1);
A35: o(x, n) in {o(x, n)} by TARSKI:def 1;
InnerVertices S(x, n) =
{[<*xx,xy*>, 'xor'], 2GatesCircOutput(xx,xy,x,'xor')} \/
{[<*xx,xy*>,and2a], [<*xy,x*>,and2], [<*xx,x*>,and2a]} \/
{BorrowOutput(xx,xy,x)} by Th17;
hence thesis by A35,XBOOLE_0:def 3;
end;
for s being State of n-BitSubtracterCirc(f,g) holds
Following(s,n(0)+n(2)*n(1)) is stable
from CIRCCMB2:sch 22(A4,A5,A7,A18,A19,A21,A22,A23,A31);
hence thesis by A1,A2,A3;
end;