:: Stability of n-bit Generalized Full Adder Circuits (GFAs). Part {II}
:: by Katsumi Wasaki
::
:: Copyright (c) 2007-2021 Association of Mizar Users

::========================================================================
::========================================================================
:: [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 (<*>,());
set o0 = [<*>,()];
A1: ( 1GateCircStr (<*>,()) is unsplit & 1GateCircStr (<*>,()) is gate1=arity & 1GateCircStr (<*>,()) is gate2isBoolean & not 1GateCircStr (<*>,()) is void & not 1GateCircStr (<*>,()) is empty & 1GateCircStr (<*>,()) is strict ) ;
func n -BitGFA0Str (x,y) -> non empty non void strict unsplit gate1=arity gate2isBoolean ManySortedSign means :Def1: :: GFACIRC2:def 1
ex f, h being ManySortedSet of NAT st
( it = f . n & f . 0 = 1GateCircStr (<*>,()) & h . 0 = [<*>,()] & ( 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 gate1=arity gate2isBoolean ManySortedSign st ex f, h being ManySortedSet of NAT st
( b1 = f . n & f . 0 = 1GateCircStr (<*>,()) & h . 0 = [<*>,()] & ( 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 (<*>,()) & h . 0 = [<*>,()] & ( 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
proof end;
existence
ex b1 being non empty non void strict unsplit gate1=arity gate2isBoolean ManySortedSign ex f, h being ManySortedSet of NAT st
( b1 = f . n & f . 0 = 1GateCircStr (<*>,()) & h . 0 = [<*>,()] & ( 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) ) ) )
proof end;
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 gate1=arity gate2isBoolean ManySortedSign holds
( b4 = n -BitGFA0Str (x,y) iff ex f, h being ManySortedSet of NAT st
( b4 = f . n & f . 0 = 1GateCircStr (<*>,()) & h . 0 = [<*>,()] & ( 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;
func n -BitGFA0Circ (x,y) -> strict gate2=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 (<*>,()) & g . 0 = 1GateCircuit (<*>,()) & h . 0 = [<*>,()] & ( 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 gate2=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 (<*>,()) & g . 0 = 1GateCircuit (<*>,()) & h . 0 = [<*>,()] & ( 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 (<*>,()) & g . 0 = 1GateCircuit (<*>,()) & h . 0 = [<*>,()] & ( 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
proof end;
existence
ex b1 being strict gate2=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 (<*>,()) & g . 0 = 1GateCircuit (<*>,()) & h . 0 = [<*>,()] & ( 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) ) ) )
proof end;
end;

:: deftheorem Def2 defines -BitGFA0Circ GFACIRC2:def 2 :
for n being Nat
for x, y being FinSequence
for b4 being strict gate2=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 (<*>,()) & g . 0 = 1GateCircuit (<*>,()) & h . 0 = [<*>,()] & ( 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;
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 = [<*>,()] & ( 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 = [<*>,()] & ( 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 = [<*>,()] & ( for n being Nat holds h . (n + 1) = GFA0CarryOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) ) holds
b1 = b2
proof end;
existence
ex b1 being Element of InnerVertices (n -BitGFA0Str (x,y)) ex h being ManySortedSet of NAT st
( b1 = h . n & h . 0 = [<*>,()] & ( for n being Nat holds h . (n + 1) = GFA0CarryOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) )
proof end;
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 = [<*>,()] & ( 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 (<*>,()) & g . 0 = 1GateCircuit (<*>,()) & h . 0 = [<*>,()] & ( 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 )
proof end;

:: Special Case : (0)-depth GFA Structure
theorem Th2: :: GFACIRC2:2
for a, b being FinSequence holds
( 0 -BitGFA0Str (a,b) = 1GateCircStr (<*>,()) & 0 -BitGFA0Circ (a,b) = 1GateCircuit (<*>,()) & 0 -BitGFA0CarryOutput (a,b) = [<*>,()] )
proof end;

:: 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 = [<*>,()] holds
( 1 -BitGFA0Str (a,b) = (1GateCircStr (<*>,())) +* (BitGFA0Str ((a . 1),(b . 1),c)) & 1 -BitGFA0Circ (a,b) = (1GateCircuit (<*>,())) +* (BitGFA0Circ ((a . 1),(b . 1),c)) & 1 -BitGFA0CarryOutput (a,b) = GFA0CarryOutput ((a . 1),(b . 1),c) )
proof end;

:: Special Case : (1)-depth GFA Structure with input signals a,b (set)
theorem :: GFACIRC2:4
for a, b, c being set st c = [<*>,()] holds
( 1 -BitGFA0Str (<*a*>,<*b*>) = (1GateCircStr (<*>,())) +* (BitGFA0Str (a,b,c)) & 1 -BitGFA0Circ (<*a*>,<*b*>) = (1GateCircuit (<*>,())) +* (BitGFA0Circ (a,b,c)) & 1 -BitGFA0CarryOutput (<*a*>,<*b*>) = GFA0CarryOutput (a,b,c) )
proof end;

:: 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)) )
proof end;

:: 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))) )
proof end;

:: 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))) )
proof end;

::-------------------------------------------------------
:: 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))
proof end;

:: 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)))))
proof end;

:: k-th (k \in [1,n]) Adder Output of n-bit Combined GFA Circuit (TYPE-0)
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: :: 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))) )
proof end;
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)))
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
n -BitGFA0CarryOutput (x,y) is pair
proof end;
end;

Lm1: for x, y being FinSequence
for n being Nat holds
( ( (n -BitGFA0CarryOutput (x,y)) 1 = <*> & (n -BitGFA0CarryOutput (x,y)) 2 = --> 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 (),BOOLEAN holds n -BitGFA0CarryOutput (x,y) <> [p,f]

proof end;

:: 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 )
proof end;

:: 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)
proof end;

::--------------------------------
:: 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
proof end;

::========================================================================
::========================================================================
:: [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 (<*>,()) is unsplit & 1GateCircStr (<*>,()) is gate1=arity & 1GateCircStr (<*>,()) is gate2isBoolean & not 1GateCircStr (<*>,()) is void & not 1GateCircStr (<*>,()) is empty & 1GateCircStr (<*>,()) is strict ) ;
func n -BitGFA1Str (x,y) -> non empty non void strict unsplit gate1=arity gate2isBoolean ManySortedSign means :Def5: :: GFACIRC2:def 5
ex f, h being ManySortedSet of NAT st
( it = f . n & f . 0 = 1GateCircStr (<*>,()) & h . 0 = [<*>,()] & ( 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 gate1=arity gate2isBoolean ManySortedSign st ex f, h being ManySortedSet of NAT st
( b1 = f . n & f . 0 = 1GateCircStr (<*>,()) & h . 0 = [<*>,()] & ( 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 (<*>,()) & h . 0 = [<*>,()] & ( 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
proof end;
existence
ex b1 being non empty non void strict unsplit gate1=arity gate2isBoolean ManySortedSign ex f, h being ManySortedSet of NAT st
( b1 = f . n & f . 0 = 1GateCircStr (<*>,()) & h . 0 = [<*>,()] & ( 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) ) ) )
proof end;
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 gate1=arity gate2isBoolean ManySortedSign holds
( b4 = n -BitGFA1Str (x,y) iff ex f, h being ManySortedSet of NAT st
( b4 = f . n & f . 0 = 1GateCircStr (<*>,()) & h . 0 = [<*>,()] & ( 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;
func n -BitGFA1Circ (x,y) -> strict gate2=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 (<*>,()) & g . 0 = 1GateCircuit (<*>,()) & h . 0 = [<*>,()] & ( 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 gate2=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 (<*>,()) & g . 0 = 1GateCircuit (<*>,()) & h . 0 = [<*>,()] & ( 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 (<*>,()) & g . 0 = 1GateCircuit (<*>,()) & h . 0 = [<*>,()] & ( 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
proof end;
existence
ex b1 being strict gate2=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 (<*>,()) & g . 0 = 1GateCircuit (<*>,()) & h . 0 = [<*>,()] & ( 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) ) ) )
proof end;
end;

:: deftheorem Def6 defines -BitGFA1Circ GFACIRC2:def 6 :
for n being Nat
for x, y being FinSequence
for b4 being strict gate2=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 (<*>,()) & g . 0 = 1GateCircuit (<*>,()) & h . 0 = [<*>,()] & ( 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;
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 = [<*>,()] & ( 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 = [<*>,()] & ( 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 = [<*>,()] & ( for n being Nat holds h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) ) holds
b1 = b2
proof end;
existence
ex b1 being Element of InnerVertices (n -BitGFA1Str (x,y)) ex h being ManySortedSet of NAT st
( b1 = h . n & h . 0 = [<*>,()] & ( for n being Nat holds h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) )
proof end;
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 = [<*>,()] & ( 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 (<*>,()) & g . 0 = 1GateCircuit (<*>,()) & h . 0 = [<*>,()] & ( 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 )
proof end;

:: Special Case : (0)-depth GFA Structure
theorem Th16: :: GFACIRC2:16
for a, b being FinSequence holds
( 0 -BitGFA1Str (a,b) = 1GateCircStr (<*>,()) & 0 -BitGFA1Circ (a,b) = 1GateCircuit (<*>,()) & 0 -BitGFA1CarryOutput (a,b) = [<*>,()] )
proof end;

:: 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 = [<*>,()] holds
( 1 -BitGFA1Str (a,b) = (1GateCircStr (<*>,())) +* (BitGFA1Str ((a . 1),(b . 1),c)) & 1 -BitGFA1Circ (a,b) = (1GateCircuit (<*>,())) +* (BitGFA1Circ ((a . 1),(b . 1),c)) & 1 -BitGFA1CarryOutput (a,b) = GFA1CarryOutput ((a . 1),(b . 1),c) )
proof end;

:: Special Case : (1)-depth GFA Structure with input signals a,b (set)
theorem :: GFACIRC2:18
for a, b, c being set st c = [<*>,()] holds
( 1 -BitGFA1Str (<*a*>,<*b*>) = (1GateCircStr (<*>,())) +* (BitGFA1Str (a,b,c)) & 1 -BitGFA1Circ (<*a*>,<*b*>) = (1GateCircuit (<*>,())) +* (BitGFA1Circ (a,b,c)) & 1 -BitGFA1CarryOutput (<*a*>,<*b*>) = GFA1CarryOutput (a,b,c) )
proof end;

:: 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)) )
proof end;

:: 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))) )
proof end;

:: 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))) )
proof end;

::-------------------------------------------------------
:: 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))
proof end;

:: 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)))))
proof end;

:: k-th (k \in [1,n]) Adder Output of n-bit Combined GFA Circuit (TYPE-1)
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: :: 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))) )
proof end;
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)))
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
n -BitGFA1CarryOutput (x,y) is pair
proof end;
end;

Lm3: for x, y being FinSequence
for n being Nat holds
( ( (n -BitGFA1CarryOutput (x,y)) 1 = <*> & (n -BitGFA1CarryOutput (x,y)) 2 = --> 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 (),BOOLEAN holds n -BitGFA1CarryOutput (x,y) <> [p,f]

proof end;

:: 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 )
proof end;

:: 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)
proof end;

::--------------------------------
:: 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
proof end;