:: Stability of n-bit Generalized Full Adder Circuits (GFAs). Part {II} :: by Katsumi Wasaki :: :: Received December 18, 2007 :: Copyright (c) 2007-2012 Association of Mizar Users begin ::======================================================================== ::======================================================================== :: [n-bit Combined GFA TYPE-0] :: :: Composition : n-bit Ripple Carry Connection using GFA TYPE-0 :: Function : x[1..n] + y[1..n] + 0 = c[n] + s[1..n] (Addition) :: :: x[n] y[n] x[2] y[2] x[1] y[1] :: | / | / | / :: | / | / | / :: +---*---* +---*---* +---*---* +---+ :: | GFA *<----....---+ | GFA *<--+ | GFA *<----|'0'| :: | TYPE0 | | | TYPE0 | | | TYPE0 | +---+ :: *---*---+ | *---*---+ | *---*---+ :: / | |_/ | |_/ | :: / | | | :: c[n] s[n] s[2] s[1] :: :: Calculation : Following(s,1+2*n) is stable. :: ::========================================================================= ::------------------------------------------------ :: 1-1. Definitions of n-Bit GFA Structure and Circuit (TYPE-0) ::------------------------------------------------ :: Combined Circuit Structure (n-bit) of GFA TYPE-0 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 ) ; funcn -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 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 proofend; 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) ) ) ) proofend; 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) ) ) ) ); :: Algebraic Circuit Structure (n-bit) of GFA TYPE-0 definition let n be Nat; let x, y be FinSequence; funcn -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 over 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 over 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 over 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 proofend; 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 over 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) ) ) ) proofend; 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 over 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) ) ) ) ); :: Ripple Carry Output (c[1..n]) of n-bit GFA (TYPE-0) definition let n be Nat; let x, y be FinSequence; funcn -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 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 proofend; 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)) ) ) proofend; 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)) ) ) ); ::----------------------------------------------- :: 1-2. Properties of n-Bit GFA Structure and Circuit (TYPE-0) ::----------------------------------------------- :: Recursive Circuit Composition of (n+1)-depth GFA Structure 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 over 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 ) proofend; :: Special Case : (0)-depth GFA Structure 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)] ) proofend; :: Special Case : (1)-depth GFA Structure with input signals a,b (sequence) 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) ) proofend; :: Special Case : (1)-depth GFA Structure with input signals a,b (set) 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) ) proofend; :: Structural Equivalency of GFA Structure which is used the combined :: input signals p[1..n] ^ p[n+1]. 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)) ) proofend; :: Special Case : (n+1)-depth GFA Structure with input signals :: x[1..n]^a and y[1..n]^b. 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))) ) proofend; :: Main Proposision : (n+1)-depth GFA Structure with input signals :: x[1..n] and y[1..n]. 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))) ) proofend; ::------------------------------------------------------- :: 1-3. InnerVertices and Adder Output of n-Bit GFA Structure (TYPE-0) ::------------------------------------------------------- :: m-bit GFA Circuit contains whole internal signals in :: n-bit GFA Circuit if n<=m. 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)) proofend; :: whole internal signals (n+1)-bit GFA Circuit is the conjunction :: of internal signals in n-bit GFA Circuits and one-bit GFA Circuit. 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))))) proofend; :: k-th (k \in [1,n]) Adder Output of n-bit Combined GFA Circuit (TYPE-0) definition let k, n be Nat; assume that B1: k >= 1 and B2: 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))) ) proofend; 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))) ) ); :: Main Proposision : k-th Ripple Carry Output of n-depth GFA Circuit 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))) proofend; theorem :: GFACIRC2:11 for n being Nat for x, y being FinSequence holds InnerVertices (n -BitGFA0Str (x,y)) is Relation proofend; registration let n be Nat; let x, y be FinSequence; clustern -BitGFA0CarryOutput (x,y) -> pair ; coherence n -BitGFA0CarryOutput (x,y) is pair proofend; 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 ) ) proofend; 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] proofend; :: whole input signals (n+1)-bit GFA Circuit is the conjunction :: of input signals in n-bit GFA Circuits and one-bit GFA Circuit. 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 & InputVertices (n -BitGFA0Str (f,g)) is without_pairs ) proofend; :: Main Proposision : whole input signals of n-depth GFA Circuit 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) proofend; ::-------------------------------- :: 1-5. Stability of n-Bit GFA Circuit (TYPE-0) ::-------------------------------- 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 proofend; begin ::======================================================================== ::======================================================================== :: [n-bit Combined GFA TYPE-1] :: :: Composition : n-bit Ripple Carry Connection using GFA TYPE-1 :: Function : x[1..n] - y[1..n] + 1 = c[n] - s[1..n] (Subtraction) :: :: x[n] -y[n] x[2] -y[2] x[1] -y[1] :: | / | / | / :: | / | / | / :: +---*---O +---*---O +---*---O +---+ :: | GFA *<----....---+ | GFA *<--+ | GFA *<----|'1'| :: | TYPE1 | | | TYPE1 | | | TYPE1 | +---+ :: *---O---+ | *---O---+ | *---O---+ :: / | |_/ | |_/ | :: / | | | :: c[n] -s[n] -s[2] -s[1] :: :: Calculation : Following(s,1+2*n) is stable. :: ::========================================================================= ::------------------------------------------------ :: 2-1. Definitions of n-Bit GFA Structure and Circuit (TYPE-1) ::------------------------------------------------ :: Combined Circuit Structure (n-bit) of GFA TYPE-1 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 ) ; funcn -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 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 proofend; 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) ) ) ) proofend; 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) ) ) ) ); :: Algebraic Circuit Structure (n-bit) of GFA TYPE-1 definition let n be Nat; let x, y be FinSequence; funcn -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 over 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 over 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 over 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 proofend; 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 over 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) ) ) ) proofend; 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 over 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) ) ) ) ); :: Ripple Carry Output (c[1..n]) of n-bit GFA (TYPE-1) definition let n be Nat; let x, y be FinSequence; funcn -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 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 proofend; 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)) ) ) proofend; 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)) ) ) ); ::----------------------------------------------- :: 2-2. Properties of n-Bit GFA Structure and Circuit (TYPE-1) ::----------------------------------------------- :: Recursive Circuit Composition of (n+1)-depth GFA Structure 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 over 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 ) proofend; :: Special Case : (0)-depth GFA Structure 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)] ) proofend; :: Special Case : (1)-depth GFA Structure with input signals a,b (sequence) 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) ) proofend; :: Special Case : (1)-depth GFA Structure with input signals a,b (set) 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) ) proofend; :: Structural Equivalency of GFA Structure which is used the combined :: input signals p[1..n] ^ p[n+1]. 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)) ) proofend; :: Special Case : (n+1)-depth GFA Structure with input signals :: x[1..n]^a and y[1..n]^b. 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))) ) proofend; :: Main Proposision : (n+1)-depth GFA Structure with input signals :: x[1..n] and y[1..n]. 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))) ) proofend; ::------------------------------------------------------- :: 2-3. InnerVertices and Adder Output of n-Bit GFA Structure (TYPE-1) ::------------------------------------------------------- :: m-bit GFA Circuit contains whole internal signals in :: n-bit GFA Circuit if n<=m. 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)) proofend; :: whole internal signals (n+1)-bit GFA Circuit is the conjunction :: of internal signals in n-bit GFA Circuits and one-bit GFA Circuit. 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))))) proofend; :: k-th (k \in [1,n]) Adder Output of n-bit Combined GFA Circuit (TYPE-1) definition let k, n be Nat; assume that B1: k >= 1 and B2: 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))) ) proofend; 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))) ) ); :: Main Proposision : k-th Ripple Carry Output of n-depth GFA Circuit 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))) proofend; theorem :: GFACIRC2:25 for n being Nat for x, y being FinSequence holds InnerVertices (n -BitGFA1Str (x,y)) is Relation proofend; registration let n be Nat; let x, y be FinSequence; clustern -BitGFA1CarryOutput (x,y) -> pair ; coherence n -BitGFA1CarryOutput (x,y) is pair proofend; 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 ) ) proofend; 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] proofend; :: whole input signals (n+1)-bit GFA Circuit is the conjunction :: of input signals in n-bit GFA Circuits and one-bit GFA Circuit. 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 & InputVertices (n -BitGFA1Str (f,g)) is without_pairs ) proofend; :: Main Proposision : whole input signals of n-depth GFA Circuit 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) proofend; ::-------------------------------- :: 2-5. Stability of n-Bit GFA Circuit (TYPE-1) ::-------------------------------- 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 proofend;