GFACIRC2: Stability of n-bit Generalized Full Adder Circuits (GFAs). Part {II}

:: 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

proof end;

existence

proof end;

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 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

proof end;

existence

proof end;

end;

:: deftheorem Def2 defines -BitGFA0Circ GFACIRC2:def 2 :

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 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

proof end;

existence

proof end;

end;

:: deftheorem Def3 defines -BitGFA0CarryOutput GFACIRC2:def 3 :

theorem Th1: :: GFACIRC2:1

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 )

proof end;

theorem Th2: :: GFACIRC2:2

for a, b being FinSequence holds
( 0 -BitGFA0Str a,b = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & 0 -BitGFA0Circ a,b = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & 0 -BitGFA0CarryOutput a,b = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] )

proof end;

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 )

proof end;

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 )

proof end;

theorem Th5: :: GFACIRC2:5

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) )

proof end;

theorem :: GFACIRC2:6

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) )

proof end;

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) )

proof end;

theorem Th8: :: GFACIRC2:8

for n, m being Nat st n <= m holds
for x, y being FinSequence holds InnerVertices (n -BitGFA0Str x,y) c= InnerVertices (m -BitGFA0Str x,y)

proof end;

theorem :: GFACIRC2:9

for n being Nat
for x, y being FinSequence holds InnerVertices ((n + 1) -BitGFA0Str x,y) = (InnerVertices (n -BitGFA0Str x,y)) \/ (InnerVertices (BitGFA0Str (x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput x,y)))

proof end;

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 ;
existence

proof end;

end;

:: deftheorem Def4 defines -BitGFA0AdderOutput GFACIRC2:def 4 :

theorem :: GFACIRC2:10

for n, k being Nat st k < n holds
for x, y being FinSequence holds (k + 1),n -BitGFA0AdderOutput x,y = GFA0AdderOutput (x . (k + 1)),(y . (k + 1)),(k -BitGFA0CarryOutput x,y)

proof end;

theorem :: GFACIRC2:11

for n being Nat
for x, y being FinSequence holds InnerVertices (n -BitGFA0Str x,y) is Relation

proof end;

registration

let n be Nat;
let x, y be FinSequence;
cluster n -BitGFA0CarryOutput x,y -> pair ;
coherence

proof end;

end;

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 ) )

proof end;

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]

proof end;

theorem Th12: :: GFACIRC2:12

for f, g being nonpair-yielding FinSequence
for n being Nat holds
( InputVertices ((n + 1) -BitGFA0Str f,g) = (InputVertices (n -BitGFA0Str f,g)) \/ ((InputVertices (BitGFA0Str (f . (n + 1)),(g . (n + 1)),(n -BitGFA0CarryOutput f,g))) \ {(n -BitGFA0CarryOutput f,g)}) & InnerVertices (n -BitGFA0Str f,g) is Relation & not InputVertices (n -BitGFA0Str f,g) is with_pair )

proof end;

theorem :: GFACIRC2:13

for n being Nat
for x, y being nonpair-yielding FinSeqLen of n holds InputVertices (n -BitGFA0Str x,y) = (rng x) \/ (rng y)

proof end;

theorem :: GFACIRC2:14

for n being Nat
for x, y being nonpair-yielding FinSeqLen of n
for s being State of (n -BitGFA0Circ x,y) holds Following s,(1 + (2 * n)) is stable

proof end;

definition

proof end;

existence

proof end;

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 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

proof end;

existence

proof end;

end;

:: deftheorem Def6 defines -BitGFA1Circ GFACIRC2:def 6 :

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 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

proof end;

existence

proof end;

end;

:: deftheorem Def7 defines -BitGFA1CarryOutput GFACIRC2:def 7 :

theorem Th15: :: GFACIRC2:15

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 )

proof end;

theorem Th16: :: GFACIRC2:16

for a, b being FinSequence holds
( 0 -BitGFA1Str a,b = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & 0 -BitGFA1Circ a,b = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & 0 -BitGFA1CarryOutput a,b = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] )

proof end;

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 )

proof end;

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 )

proof end;

theorem Th19: :: GFACIRC2:19

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) )

proof end;

theorem :: GFACIRC2:20

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) )

proof end;

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) )

proof end;

theorem Th22: :: GFACIRC2:22

for n, m being Nat st n <= m holds
for x, y being FinSequence holds InnerVertices (n -BitGFA1Str x,y) c= InnerVertices (m -BitGFA1Str x,y)

proof end;

theorem :: GFACIRC2:23

for n being Nat
for x, y being FinSequence holds InnerVertices ((n + 1) -BitGFA1Str x,y) = (InnerVertices (n -BitGFA1Str x,y)) \/ (InnerVertices (BitGFA1Str (x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput x,y)))

proof end;

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 ;
existence

proof end;

end;

:: deftheorem Def8 defines -BitGFA1AdderOutput GFACIRC2:def 8 :

theorem :: GFACIRC2:24

for n, k being Nat st k < n holds
for x, y being FinSequence holds (k + 1),n -BitGFA1AdderOutput x,y = GFA1AdderOutput (x . (k + 1)),(y . (k + 1)),(k -BitGFA1CarryOutput x,y)

proof end;

theorem :: GFACIRC2:25

for n being Nat
for x, y being FinSequence holds InnerVertices (n -BitGFA1Str x,y) is Relation

proof end;

registration

let n be Nat;
let x, y be FinSequence;
cluster n -BitGFA1CarryOutput x,y -> pair ;
coherence

proof end;

end;

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 ) )

proof end;

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]

proof end;

theorem Th26: :: GFACIRC2:26

for f, g being nonpair-yielding FinSequence
for n being Nat holds
( InputVertices ((n + 1) -BitGFA1Str f,g) = (InputVertices (n -BitGFA1Str f,g)) \/ ((InputVertices (BitGFA1Str (f . (n + 1)),(g . (n + 1)),(n -BitGFA1CarryOutput f,g))) \ {(n -BitGFA1CarryOutput f,g)}) & InnerVertices (n -BitGFA1Str f,g) is Relation & not InputVertices (n -BitGFA1Str f,g) is with_pair )

proof end;

theorem :: GFACIRC2:27

for n being Nat
for x, y being nonpair-yielding FinSeqLen of n holds InputVertices (n -BitGFA1Str x,y) = (rng x) \/ (rng y)

proof end;

theorem :: GFACIRC2:28

for n being Nat
for x, y being nonpair-yielding FinSeqLen of n
for s being State of (n -BitGFA1Circ x,y) holds Following s,(1 + (2 * n)) is stable

proof end;