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