:: Stability of n-bit Generalized Full Adder Circuits (GFAs). Part {II}
:: by Katsumi Wasaki
::
:: Received December 18, 2007
:: Copyright (c) 2007 Association of Mizar Users
definition
let n be
Nat;
let x,
y be
FinSequence;
set S0 =
1GateCircStr <*> ,
((0 -tuples_on BOOLEAN ) --> FALSE );
set o0 =
[<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )];
A1:
(
1GateCircStr <*> ,
((0 -tuples_on BOOLEAN ) --> FALSE ) is
unsplit &
1GateCircStr <*> ,
((0 -tuples_on BOOLEAN ) --> FALSE ) is
gate`1=arity &
1GateCircStr <*> ,
((0 -tuples_on BOOLEAN ) --> FALSE ) is
gate`2isBoolean & not
1GateCircStr <*> ,
((0 -tuples_on BOOLEAN ) --> FALSE ) is
void & not
1GateCircStr <*> ,
((0 -tuples_on BOOLEAN ) --> FALSE ) is
empty &
1GateCircStr <*> ,
((0 -tuples_on BOOLEAN ) --> FALSE ) is
strict )
;
func n -BitGFA0Str x,
y -> non
empty non
void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign means :
Def1:
:: GFACIRC2:def 1
ex
f,
h being
ManySortedSet of st
(
it = f . n &
f . 0 = 1GateCircStr <*> ,
((0 -tuples_on BOOLEAN ) --> FALSE ) &
h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for
n being
Nat for
S being non
empty ManySortedSign for
z being
set st
S = f . n &
z = h . n holds
(
f . (n + 1) = S +* (BitGFA0Str (x . (n + 1)),(y . (n + 1)),z) &
h . (n + 1) = GFA0CarryOutput (x . (n + 1)),
(y . (n + 1)),
z ) ) );
uniqueness
for b1, b2 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign st ex f, h being ManySortedSet of st
( b1 = f . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = h . n holds
( f . (n + 1) = S +* (BitGFA0Str (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = GFA0CarryOutput (x . (n + 1)),(y . (n + 1)),z ) ) ) & ex f, h being ManySortedSet of st
( b2 = f . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = h . n holds
( f . (n + 1) = S +* (BitGFA0Str (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = GFA0CarryOutput (x . (n + 1)),(y . (n + 1)),z ) ) ) holds
b1 = b2
existence
ex b1 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex f, h being ManySortedSet of st
( b1 = f . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = h . n holds
( f . (n + 1) = S +* (BitGFA0Str (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = GFA0CarryOutput (x . (n + 1)),(y . (n + 1)),z ) ) )
end;
:: deftheorem Def1 defines -BitGFA0Str GFACIRC2:def 1 :
definition
let n be
Nat;
let x,
y be
FinSequence;
func n -BitGFA0Circ x,
y -> strict gate`2=den Boolean Circuit of
n -BitGFA0Str x,
y means :
Def2:
:: GFACIRC2:def 2
ex
f,
g,
h being
ManySortedSet of st
(
n -BitGFA0Str x,
y = f . n &
it = g . n &
f . 0 = 1GateCircStr <*> ,
((0 -tuples_on BOOLEAN ) --> FALSE ) &
g . 0 = 1GateCircuit <*> ,
((0 -tuples_on BOOLEAN ) --> FALSE ) &
h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for
n being
Nat for
S being non
empty ManySortedSign for
A being
non-empty MSAlgebra of
S for
z being
set st
S = f . n &
A = g . n &
z = h . n holds
(
f . (n + 1) = S +* (BitGFA0Str (x . (n + 1)),(y . (n + 1)),z) &
g . (n + 1) = A +* (BitGFA0Circ (x . (n + 1)),(y . (n + 1)),z) &
h . (n + 1) = GFA0CarryOutput (x . (n + 1)),
(y . (n + 1)),
z ) ) );
uniqueness
for b1, b2 being strict gate`2=den Boolean Circuit of n -BitGFA0Str x,y st ex f, g, h being ManySortedSet of st
( n -BitGFA0Str x,y = f . n & b1 = g . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & g . 0 = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra of S
for z being set st S = f . n & A = g . n & z = h . n holds
( f . (n + 1) = S +* (BitGFA0Str (x . (n + 1)),(y . (n + 1)),z) & g . (n + 1) = A +* (BitGFA0Circ (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = GFA0CarryOutput (x . (n + 1)),(y . (n + 1)),z ) ) ) & ex f, g, h being ManySortedSet of st
( n -BitGFA0Str x,y = f . n & b2 = g . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & g . 0 = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra of S
for z being set st S = f . n & A = g . n & z = h . n holds
( f . (n + 1) = S +* (BitGFA0Str (x . (n + 1)),(y . (n + 1)),z) & g . (n + 1) = A +* (BitGFA0Circ (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = GFA0CarryOutput (x . (n + 1)),(y . (n + 1)),z ) ) ) holds
b1 = b2
existence
ex b1 being strict gate`2=den Boolean Circuit of n -BitGFA0Str x,y ex f, g, h being ManySortedSet of st
( n -BitGFA0Str x,y = f . n & b1 = g . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & g . 0 = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra of S
for z being set st S = f . n & A = g . n & z = h . n holds
( f . (n + 1) = S +* (BitGFA0Str (x . (n + 1)),(y . (n + 1)),z) & g . (n + 1) = A +* (BitGFA0Circ (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = GFA0CarryOutput (x . (n + 1)),(y . (n + 1)),z ) ) )
end;
:: deftheorem Def2 defines -BitGFA0Circ GFACIRC2:def 2 :
for
n being
Nat for
x,
y being
FinSequence for
b4 being
strict gate`2=den Boolean Circuit of
n -BitGFA0Str x,
y holds
(
b4 = n -BitGFA0Circ x,
y iff ex
f,
g,
h being
ManySortedSet of st
(
n -BitGFA0Str x,
y = f . n &
b4 = g . n &
f . 0 = 1GateCircStr <*> ,
((0 -tuples_on BOOLEAN ) --> FALSE ) &
g . 0 = 1GateCircuit <*> ,
((0 -tuples_on BOOLEAN ) --> FALSE ) &
h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for
n being
Nat for
S being non
empty ManySortedSign for
A being
non-empty MSAlgebra of
S for
z being
set st
S = f . n &
A = g . n &
z = h . n holds
(
f . (n + 1) = S +* (BitGFA0Str (x . (n + 1)),(y . (n + 1)),z) &
g . (n + 1) = A +* (BitGFA0Circ (x . (n + 1)),(y . (n + 1)),z) &
h . (n + 1) = GFA0CarryOutput (x . (n + 1)),
(y . (n + 1)),
z ) ) ) );
definition
let n be
Nat;
let x,
y be
FinSequence;
func n -BitGFA0CarryOutput x,
y -> Element of
InnerVertices (n -BitGFA0Str x,y) means :
Def3:
:: GFACIRC2:def 3
ex
h being
ManySortedSet of st
(
it = h . n &
h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for
n being
Nat holds
h . (n + 1) = GFA0CarryOutput (x . (n + 1)),
(y . (n + 1)),
(h . n) ) );
uniqueness
for b1, b2 being Element of InnerVertices (n -BitGFA0Str x,y) st ex h being ManySortedSet of st
( b1 = h . n & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for n being Nat holds h . (n + 1) = GFA0CarryOutput (x . (n + 1)),(y . (n + 1)),(h . n) ) ) & ex h being ManySortedSet of st
( b2 = h . n & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for n being Nat holds h . (n + 1) = GFA0CarryOutput (x . (n + 1)),(y . (n + 1)),(h . n) ) ) holds
b1 = b2
existence
ex b1 being Element of InnerVertices (n -BitGFA0Str x,y) ex h being ManySortedSet of st
( b1 = h . n & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for n being Nat holds h . (n + 1) = GFA0CarryOutput (x . (n + 1)),(y . (n + 1)),(h . n) ) )
end;
:: deftheorem Def3 defines -BitGFA0CarryOutput GFACIRC2:def 3 :
theorem Th1: :: GFACIRC2:1
for
x,
y being
FinSequence for
f,
g,
h being
ManySortedSet of st
f . 0 = 1GateCircStr <*> ,
((0 -tuples_on BOOLEAN ) --> FALSE ) &
g . 0 = 1GateCircuit <*> ,
((0 -tuples_on BOOLEAN ) --> FALSE ) &
h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for
n being
Nat for
S being non
empty ManySortedSign for
A being
non-empty MSAlgebra of
S for
z being
set st
S = f . n &
A = g . n &
z = h . n holds
(
f . (n + 1) = S +* (BitGFA0Str (x . (n + 1)),(y . (n + 1)),z) &
g . (n + 1) = A +* (BitGFA0Circ (x . (n + 1)),(y . (n + 1)),z) &
h . (n + 1) = GFA0CarryOutput (x . (n + 1)),
(y . (n + 1)),
z ) ) holds
for
n being
Nat holds
(
n -BitGFA0Str x,
y = f . n &
n -BitGFA0Circ x,
y = g . n &
n -BitGFA0CarryOutput x,
y = h . n )
theorem Th2: :: GFACIRC2:2
theorem Th3: :: GFACIRC2:3
for
a,
b being
FinSequence for
c being
set st
c = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] holds
( 1
-BitGFA0Str a,
b = (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE )) +* (BitGFA0Str (a . 1),(b . 1),c) & 1
-BitGFA0Circ a,
b = (1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE )) +* (BitGFA0Circ (a . 1),(b . 1),c) & 1
-BitGFA0CarryOutput a,
b = GFA0CarryOutput (a . 1),
(b . 1),
c )
theorem :: GFACIRC2:4
for
a,
b,
c being
set st
c = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] holds
( 1
-BitGFA0Str <*a*>,
<*b*> = (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE )) +* (BitGFA0Str a,b,c) & 1
-BitGFA0Circ <*a*>,
<*b*> = (1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE )) +* (BitGFA0Circ a,b,c) & 1
-BitGFA0CarryOutput <*a*>,
<*b*> = GFA0CarryOutput a,
b,
c )
theorem Th5: :: GFACIRC2:5
for
n being
Nat for
p,
q being
FinSeqLen of
for
p1,
p2,
q1,
q2 being
FinSequence holds
(
n -BitGFA0Str (p ^ p1),
(q ^ q1) = n -BitGFA0Str (p ^ p2),
(q ^ q2) &
n -BitGFA0Circ (p ^ p1),
(q ^ q1) = n -BitGFA0Circ (p ^ p2),
(q ^ q2) &
n -BitGFA0CarryOutput (p ^ p1),
(q ^ q1) = n -BitGFA0CarryOutput (p ^ p2),
(q ^ q2) )
theorem :: GFACIRC2:6
for
n being
Nat for
x,
y being
FinSeqLen of
for
a,
b being
set holds
(
(n + 1) -BitGFA0Str (x ^ <*a*>),
(y ^ <*b*>) = (n -BitGFA0Str x,y) +* (BitGFA0Str a,b,(n -BitGFA0CarryOutput x,y)) &
(n + 1) -BitGFA0Circ (x ^ <*a*>),
(y ^ <*b*>) = (n -BitGFA0Circ x,y) +* (BitGFA0Circ a,b,(n -BitGFA0CarryOutput x,y)) &
(n + 1) -BitGFA0CarryOutput (x ^ <*a*>),
(y ^ <*b*>) = GFA0CarryOutput a,
b,
(n -BitGFA0CarryOutput x,y) )
theorem Th7: :: GFACIRC2:7
for
n being
Nat for
x,
y being
FinSequence holds
(
(n + 1) -BitGFA0Str x,
y = (n -BitGFA0Str x,y) +* (BitGFA0Str (x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput x,y)) &
(n + 1) -BitGFA0Circ x,
y = (n -BitGFA0Circ x,y) +* (BitGFA0Circ (x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput x,y)) &
(n + 1) -BitGFA0CarryOutput x,
y = GFA0CarryOutput (x . (n + 1)),
(y . (n + 1)),
(n -BitGFA0CarryOutput x,y) )
theorem Th8: :: GFACIRC2:8
theorem :: GFACIRC2:9
definition
let k,
n be
Nat;
assume A1:
(
k >= 1 &
k <= n )
;
let x,
y be
FinSequence;
func k,
n -BitGFA0AdderOutput x,
y -> Element of
InnerVertices (n -BitGFA0Str x,y) means :
Def4:
:: GFACIRC2:def 4
ex
i being
Nat st
(
k = i + 1 &
it = GFA0AdderOutput (x . k),
(y . k),
(i -BitGFA0CarryOutput x,y) );
uniqueness
for b1, b2 being Element of InnerVertices (n -BitGFA0Str x,y) st ex i being Nat st
( k = i + 1 & b1 = GFA0AdderOutput (x . k),(y . k),(i -BitGFA0CarryOutput x,y) ) & ex i being Nat st
( k = i + 1 & b2 = GFA0AdderOutput (x . k),(y . k),(i -BitGFA0CarryOutput x,y) ) holds
b1 = b2
;
existence
ex b1 being Element of InnerVertices (n -BitGFA0Str x,y) ex i being Nat st
( k = i + 1 & b1 = GFA0AdderOutput (x . k),(y . k),(i -BitGFA0CarryOutput x,y) )
end;
:: deftheorem Def4 defines -BitGFA0AdderOutput GFACIRC2:def 4 :
theorem :: GFACIRC2:10
theorem :: GFACIRC2:11
Lm1:
for x, y being FinSequence
for n being Nat holds
( ( (n -BitGFA0CarryOutput x,y) `1 = <*> & (n -BitGFA0CarryOutput x,y) `2 = (0 -tuples_on BOOLEAN ) --> FALSE & proj1 ((n -BitGFA0CarryOutput x,y) `2 ) = 0 -tuples_on BOOLEAN ) or ( card ((n -BitGFA0CarryOutput x,y) `1 ) = 3 & (n -BitGFA0CarryOutput x,y) `2 = or3 & proj1 ((n -BitGFA0CarryOutput x,y) `2 ) = 3 -tuples_on BOOLEAN ) )
Lm2:
for n being Nat
for x, y being FinSequence
for p being set
for f being Function of (2 -tuples_on BOOLEAN ),BOOLEAN holds n -BitGFA0CarryOutput x,y <> [p,f]
theorem Th12: :: GFACIRC2:12
theorem :: GFACIRC2:13
theorem :: GFACIRC2:14
definition
let n be
Nat;
let x,
y be
FinSequence;
A1:
(
1GateCircStr <*> ,
((0 -tuples_on BOOLEAN ) --> TRUE ) is
unsplit &
1GateCircStr <*> ,
((0 -tuples_on BOOLEAN ) --> TRUE ) is
gate`1=arity &
1GateCircStr <*> ,
((0 -tuples_on BOOLEAN ) --> TRUE ) is
gate`2isBoolean & not
1GateCircStr <*> ,
((0 -tuples_on BOOLEAN ) --> TRUE ) is
void & not
1GateCircStr <*> ,
((0 -tuples_on BOOLEAN ) --> TRUE ) is
empty &
1GateCircStr <*> ,
((0 -tuples_on BOOLEAN ) --> TRUE ) is
strict )
;
func n -BitGFA1Str x,
y -> non
empty non
void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign means :
Def5:
:: GFACIRC2:def 5
ex
f,
h being
ManySortedSet of st
(
it = f . n &
f . 0 = 1GateCircStr <*> ,
((0 -tuples_on BOOLEAN ) --> TRUE ) &
h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for
n being
Nat for
S being non
empty ManySortedSign for
z being
set st
S = f . n &
z = h . n holds
(
f . (n + 1) = S +* (BitGFA1Str (x . (n + 1)),(y . (n + 1)),z) &
h . (n + 1) = GFA1CarryOutput (x . (n + 1)),
(y . (n + 1)),
z ) ) );
uniqueness
for b1, b2 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign st ex f, h being ManySortedSet of st
( b1 = f . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = h . n holds
( f . (n + 1) = S +* (BitGFA1Str (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = GFA1CarryOutput (x . (n + 1)),(y . (n + 1)),z ) ) ) & ex f, h being ManySortedSet of st
( b2 = f . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = h . n holds
( f . (n + 1) = S +* (BitGFA1Str (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = GFA1CarryOutput (x . (n + 1)),(y . (n + 1)),z ) ) ) holds
b1 = b2
existence
ex b1 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex f, h being ManySortedSet of st
( b1 = f . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = h . n holds
( f . (n + 1) = S +* (BitGFA1Str (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = GFA1CarryOutput (x . (n + 1)),(y . (n + 1)),z ) ) )
end;
:: deftheorem Def5 defines -BitGFA1Str GFACIRC2:def 5 :
definition
let n be
Nat;
let x,
y be
FinSequence;
func n -BitGFA1Circ x,
y -> strict gate`2=den Boolean Circuit of
n -BitGFA1Str x,
y means :
Def6:
:: GFACIRC2:def 6
ex
f,
g,
h being
ManySortedSet of st
(
n -BitGFA1Str 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 for
S being non
empty ManySortedSign for
A being
non-empty MSAlgebra of
S for
z being
set st
S = f . n &
A = g . n &
z = h . n holds
(
f . (n + 1) = S +* (BitGFA1Str (x . (n + 1)),(y . (n + 1)),z) &
g . (n + 1) = A +* (BitGFA1Circ (x . (n + 1)),(y . (n + 1)),z) &
h . (n + 1) = GFA1CarryOutput (x . (n + 1)),
(y . (n + 1)),
z ) ) );
uniqueness
for b1, b2 being strict gate`2=den Boolean Circuit of n -BitGFA1Str x,y st ex f, g, h being ManySortedSet of st
( n -BitGFA1Str x,y = f . n & b1 = 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
for S being non empty ManySortedSign
for A being non-empty MSAlgebra of S
for z being set st S = f . n & A = g . n & z = h . n holds
( f . (n + 1) = S +* (BitGFA1Str (x . (n + 1)),(y . (n + 1)),z) & g . (n + 1) = A +* (BitGFA1Circ (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = GFA1CarryOutput (x . (n + 1)),(y . (n + 1)),z ) ) ) & ex f, g, h being ManySortedSet of st
( n -BitGFA1Str x,y = f . n & b2 = 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
for S being non empty ManySortedSign
for A being non-empty MSAlgebra of S
for z being set st S = f . n & A = g . n & z = h . n holds
( f . (n + 1) = S +* (BitGFA1Str (x . (n + 1)),(y . (n + 1)),z) & g . (n + 1) = A +* (BitGFA1Circ (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = GFA1CarryOutput (x . (n + 1)),(y . (n + 1)),z ) ) ) holds
b1 = b2
existence
ex b1 being strict gate`2=den Boolean Circuit of n -BitGFA1Str x,y ex f, g, h being ManySortedSet of st
( n -BitGFA1Str x,y = f . n & b1 = 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
for S being non empty ManySortedSign
for A being non-empty MSAlgebra of S
for z being set st S = f . n & A = g . n & z = h . n holds
( f . (n + 1) = S +* (BitGFA1Str (x . (n + 1)),(y . (n + 1)),z) & g . (n + 1) = A +* (BitGFA1Circ (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = GFA1CarryOutput (x . (n + 1)),(y . (n + 1)),z ) ) )
end;
:: deftheorem Def6 defines -BitGFA1Circ GFACIRC2:def 6 :
for
n being
Nat for
x,
y being
FinSequence for
b4 being
strict gate`2=den Boolean Circuit of
n -BitGFA1Str x,
y holds
(
b4 = n -BitGFA1Circ x,
y iff ex
f,
g,
h being
ManySortedSet of st
(
n -BitGFA1Str x,
y = f . n &
b4 = 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 for
S being non
empty ManySortedSign for
A being
non-empty MSAlgebra of
S for
z being
set st
S = f . n &
A = g . n &
z = h . n holds
(
f . (n + 1) = S +* (BitGFA1Str (x . (n + 1)),(y . (n + 1)),z) &
g . (n + 1) = A +* (BitGFA1Circ (x . (n + 1)),(y . (n + 1)),z) &
h . (n + 1) = GFA1CarryOutput (x . (n + 1)),
(y . (n + 1)),
z ) ) ) );
definition
let n be
Nat;
let x,
y be
FinSequence;
func n -BitGFA1CarryOutput x,
y -> Element of
InnerVertices (n -BitGFA1Str x,y) means :
Def7:
:: GFACIRC2:def 7
ex
h being
ManySortedSet of st
(
it = h . n &
h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for
n being
Nat holds
h . (n + 1) = GFA1CarryOutput (x . (n + 1)),
(y . (n + 1)),
(h . n) ) );
uniqueness
for b1, b2 being Element of InnerVertices (n -BitGFA1Str x,y) st ex h being ManySortedSet of st
( b1 = h . n & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for n being Nat holds h . (n + 1) = GFA1CarryOutput (x . (n + 1)),(y . (n + 1)),(h . n) ) ) & ex h being ManySortedSet of st
( b2 = h . n & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for n being Nat holds h . (n + 1) = GFA1CarryOutput (x . (n + 1)),(y . (n + 1)),(h . n) ) ) holds
b1 = b2
existence
ex b1 being Element of InnerVertices (n -BitGFA1Str x,y) ex h being ManySortedSet of st
( b1 = h . n & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for n being Nat holds h . (n + 1) = GFA1CarryOutput (x . (n + 1)),(y . (n + 1)),(h . n) ) )
end;
:: deftheorem Def7 defines -BitGFA1CarryOutput GFACIRC2:def 7 :
theorem Th15: :: GFACIRC2:15
for
x,
y being
FinSequence for
f,
g,
h being
ManySortedSet of 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 for
S being non
empty ManySortedSign for
A being
non-empty MSAlgebra of
S for
z being
set st
S = f . n &
A = g . n &
z = h . n holds
(
f . (n + 1) = S +* (BitGFA1Str (x . (n + 1)),(y . (n + 1)),z) &
g . (n + 1) = A +* (BitGFA1Circ (x . (n + 1)),(y . (n + 1)),z) &
h . (n + 1) = GFA1CarryOutput (x . (n + 1)),
(y . (n + 1)),
z ) ) holds
for
n being
Nat holds
(
n -BitGFA1Str x,
y = f . n &
n -BitGFA1Circ x,
y = g . n &
n -BitGFA1CarryOutput x,
y = h . n )
theorem Th16: :: GFACIRC2:16
theorem Th17: :: GFACIRC2:17
for
a,
b being
FinSequence for
c being
set st
c = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] holds
( 1
-BitGFA1Str a,
b = (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE )) +* (BitGFA1Str (a . 1),(b . 1),c) & 1
-BitGFA1Circ a,
b = (1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> TRUE )) +* (BitGFA1Circ (a . 1),(b . 1),c) & 1
-BitGFA1CarryOutput a,
b = GFA1CarryOutput (a . 1),
(b . 1),
c )
theorem :: GFACIRC2:18
for
a,
b,
c being
set st
c = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] holds
( 1
-BitGFA1Str <*a*>,
<*b*> = (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE )) +* (BitGFA1Str a,b,c) & 1
-BitGFA1Circ <*a*>,
<*b*> = (1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> TRUE )) +* (BitGFA1Circ a,b,c) & 1
-BitGFA1CarryOutput <*a*>,
<*b*> = GFA1CarryOutput a,
b,
c )
theorem Th19: :: GFACIRC2:19
for
n being
Nat for
p,
q being
FinSeqLen of
for
p1,
p2,
q1,
q2 being
FinSequence holds
(
n -BitGFA1Str (p ^ p1),
(q ^ q1) = n -BitGFA1Str (p ^ p2),
(q ^ q2) &
n -BitGFA1Circ (p ^ p1),
(q ^ q1) = n -BitGFA1Circ (p ^ p2),
(q ^ q2) &
n -BitGFA1CarryOutput (p ^ p1),
(q ^ q1) = n -BitGFA1CarryOutput (p ^ p2),
(q ^ q2) )
theorem :: GFACIRC2:20
for
n being
Nat for
x,
y being
FinSeqLen of
for
a,
b being
set holds
(
(n + 1) -BitGFA1Str (x ^ <*a*>),
(y ^ <*b*>) = (n -BitGFA1Str x,y) +* (BitGFA1Str a,b,(n -BitGFA1CarryOutput x,y)) &
(n + 1) -BitGFA1Circ (x ^ <*a*>),
(y ^ <*b*>) = (n -BitGFA1Circ x,y) +* (BitGFA1Circ a,b,(n -BitGFA1CarryOutput x,y)) &
(n + 1) -BitGFA1CarryOutput (x ^ <*a*>),
(y ^ <*b*>) = GFA1CarryOutput a,
b,
(n -BitGFA1CarryOutput x,y) )
theorem Th21: :: GFACIRC2:21
for
n being
Nat for
x,
y being
FinSequence holds
(
(n + 1) -BitGFA1Str x,
y = (n -BitGFA1Str x,y) +* (BitGFA1Str (x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput x,y)) &
(n + 1) -BitGFA1Circ x,
y = (n -BitGFA1Circ x,y) +* (BitGFA1Circ (x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput x,y)) &
(n + 1) -BitGFA1CarryOutput x,
y = GFA1CarryOutput (x . (n + 1)),
(y . (n + 1)),
(n -BitGFA1CarryOutput x,y) )
theorem Th22: :: GFACIRC2:22
theorem :: GFACIRC2:23
definition
let k,
n be
Nat;
assume A1:
(
k >= 1 &
k <= n )
;
let x,
y be
FinSequence;
func k,
n -BitGFA1AdderOutput x,
y -> Element of
InnerVertices (n -BitGFA1Str x,y) means :
Def8:
:: GFACIRC2:def 8
ex
i being
Nat st
(
k = i + 1 &
it = GFA1AdderOutput (x . k),
(y . k),
(i -BitGFA1CarryOutput x,y) );
uniqueness
for b1, b2 being Element of InnerVertices (n -BitGFA1Str x,y) st ex i being Nat st
( k = i + 1 & b1 = GFA1AdderOutput (x . k),(y . k),(i -BitGFA1CarryOutput x,y) ) & ex i being Nat st
( k = i + 1 & b2 = GFA1AdderOutput (x . k),(y . k),(i -BitGFA1CarryOutput x,y) ) holds
b1 = b2
;
existence
ex b1 being Element of InnerVertices (n -BitGFA1Str x,y) ex i being Nat st
( k = i + 1 & b1 = GFA1AdderOutput (x . k),(y . k),(i -BitGFA1CarryOutput x,y) )
end;
:: deftheorem Def8 defines -BitGFA1AdderOutput GFACIRC2:def 8 :
theorem :: GFACIRC2:24
theorem :: GFACIRC2:25
Lm3:
for x, y being FinSequence
for n being Nat holds
( ( (n -BitGFA1CarryOutput x,y) `1 = <*> & (n -BitGFA1CarryOutput x,y) `2 = (0 -tuples_on BOOLEAN ) --> TRUE & proj1 ((n -BitGFA1CarryOutput x,y) `2 ) = 0 -tuples_on BOOLEAN ) or ( card ((n -BitGFA1CarryOutput x,y) `1 ) = 3 & (n -BitGFA1CarryOutput x,y) `2 = or3 & proj1 ((n -BitGFA1CarryOutput x,y) `2 ) = 3 -tuples_on BOOLEAN ) )
Lm4:
for n being Nat
for x, y being FinSequence
for p being set
for f being Function of (2 -tuples_on BOOLEAN ),BOOLEAN holds n -BitGFA1CarryOutput x,y <> [p,f]
theorem Th26: :: GFACIRC2:26
theorem :: GFACIRC2:27
theorem :: GFACIRC2:28