begin
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:
ex
f,
h being
ManySortedSet of
NAT 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 NAT 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 NAT 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 NAT 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 :
for n being Nat
for x, y being FinSequence
for b4 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign holds
( b4 = n -BitGFA0Str (x,y) iff ex f, h being ManySortedSet of NAT st
( b4 = 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) ) ) ) );
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:
ex
f,
g,
h being
ManySortedSet of
NAT 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 NAT 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 NAT 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 NAT 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 NAT 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:
ex
h being
ManySortedSet of
NAT 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 NAT 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 NAT 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 NAT 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 :
for n being Nat
for x, y being FinSequence
for b4 being Element of InnerVertices (n -BitGFA0Str (x,y)) holds
( b4 = n -BitGFA0CarryOutput (x,y) iff ex h being ManySortedSet of NAT st
( b4 = 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)) ) ) );
theorem Th1:
for
x,
y being
FinSequence for
f,
g,
h being
ManySortedSet of
NAT 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:
theorem Th3:
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
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:
for
n being
Nat for
p,
q being
FinSeqLen of
n 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
for
n being
Nat for
x,
y being
FinSeqLen of
n 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:
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:
theorem
definition
let k,
n be
Nat;
assume that A1:
k >= 1
and A2:
k <= n
;
let x,
y be
FinSequence;
func (
k,
n)
-BitGFA0AdderOutput (
x,
y)
-> Element of
InnerVertices (n -BitGFA0Str (x,y)) means :
Def4:
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 :
for k, n being Nat st k >= 1 & k <= n holds
for x, y being FinSequence
for b5 being Element of InnerVertices (n -BitGFA0Str (x,y)) holds
( b5 = (k,n) -BitGFA0AdderOutput (x,y) iff ex i being Nat st
( k = i + 1 & b5 = GFA0AdderOutput ((x . k),(y . k),(i -BitGFA0CarryOutput (x,y))) ) );
theorem
theorem
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:
theorem
theorem
begin
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:
ex
f,
h being
ManySortedSet of
NAT 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 NAT 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 NAT 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 NAT 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 :
for n being Nat
for x, y being FinSequence
for b4 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign holds
( b4 = n -BitGFA1Str (x,y) iff ex f, h being ManySortedSet of NAT st
( b4 = 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) ) ) ) );
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:
ex
f,
g,
h being
ManySortedSet of
NAT 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 NAT 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 NAT 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 NAT 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 NAT 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:
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) = 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 NAT 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 NAT 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 NAT 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 :
for n being Nat
for x, y being FinSequence
for b4 being Element of InnerVertices (n -BitGFA1Str (x,y)) holds
( b4 = n -BitGFA1CarryOutput (x,y) iff ex h being ManySortedSet of NAT st
( b4 = 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)) ) ) );
theorem Th15:
for
x,
y being
FinSequence for
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 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:
theorem Th17:
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
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:
for
n being
Nat for
p,
q being
FinSeqLen of
n 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
for
n being
Nat for
x,
y being
FinSeqLen of
n 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:
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:
theorem
definition
let k,
n be
Nat;
assume that A1:
k >= 1
and A2:
k <= n
;
let x,
y be
FinSequence;
func (
k,
n)
-BitGFA1AdderOutput (
x,
y)
-> Element of
InnerVertices (n -BitGFA1Str (x,y)) means :
Def8:
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 :
for k, n being Nat st k >= 1 & k <= n holds
for x, y being FinSequence
for b5 being Element of InnerVertices (n -BitGFA1Str (x,y)) holds
( b5 = (k,n) -BitGFA1AdderOutput (x,y) iff ex i being Nat st
( k = i + 1 & b5 = GFA1AdderOutput ((x . k),(y . k),(i -BitGFA1CarryOutput (x,y))) ) );
theorem
theorem
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:
theorem
theorem