:: Stability of Parallel 4-2 Compressor Circuits
:: by Katsumi Wasaki
::
:: Received November 5, 2026
:: Copyright (c) 2026 Association of Mizar Users


::------------------------------------------------
:: Component Symbol & Architecture
::
:: Each column of the parallel 4-2 compressor is realized by two GFA stages,
:: where the lateral carry-out $z_{k+1}$ is produced solely by stage 1 and
:: is independent of stage 2. This crucial topological feature prevents carry
:: rippling through the second stage and bounds the settling delay to a
:: constant $T = 4$.
::
:: k-th Column 4-2 Compressor Cell (BitFTA)
::
:: a_k b_k c_k d_k
:: | | | |
:: +--*-------*-------*--+ |
:: | Stage-1 GFA (0/1) | |
:: +--*---------------*--+ |
:: | | |
:: | s1_k | c1_k |
:: | +-------------> z_{k+1} (lateral carry-out)
:: | |
:: v v
:: +--*---------------*-----------------*--+
:: | Stage-2 GFA (0/2) <------------- z_k (lateral carry-in)
:: +--*---------------*--------------------+
:: | |
:: v v
:: Sum_k Carry_k
::
:: Composition : n-bit Cascade composed with +* over a FALSE-constant base
:: gate S0
::
::------------------------------------------------
:: Wavefront Decomposition
::
:: Column k-1 Column k Column k+1
:: a_k-1 b_k-1 c_k-1 a_k b_k c_k a_k+1 b_k+1 c_k+1
:: | | | | | | | | |
:: +-*-----*-----*-+ +-*-----*-----*-+ +-*-----*-----*-+
:: | Stage-1 GFA | | Stage-1 GFA | | Stage-1 GFA | Layer 1
:: +-----*----*----+ +-----*----*----+ +-----*----*----+ 2 steps
:: | | | | | |
:: s1 z_k s1 z_k+1 s1 z_k+2
::z_k-1 | '--------------. | '--------------. | '------>
:: | | d_k-1 | | d_k | | d_k+1
:: | | | | | | | | |
:: v v v v v v v v v
:: +-*---*----*----+ +-*---*----*----+ +-*---*----*----+
:: | Stage-2 GFA | | Stage-2 GFA | | Stage-2 GFA | Layer 2
:: +-----*----*----+ +-----*----*----+ +-----*----*----+ 2 steps
:: | | | | | |
:: v v v v v v
:: S_k-1 C_k-1 S_k C_k S_k+1 C_k+1
::
::------------------------------------------------
::------------------------------------------------
:: Definitions of n-depth FTA Structure and Circuit (TYPE-0)
::------------------------------------------------
:: Signature of the n-bit 4-2 compressor: a FALSE base gate followed by
:: n BitFTA0 stage cells composed with +*, each fed the running carry.
definition
let n be Nat;
let ap, bp, cp, dp 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 -BitFTA0Str (ap,bp,cp,dp) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign means :Def1: :: FTACELL2: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 +* (BitFTA0Str ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),z)) & h . (n + 1) = BitFTA0CarryOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (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 +* (BitFTA0Str ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),z)) & h . (n + 1) = BitFTA0CarryOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (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 +* (BitFTA0Str ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),z)) & h . (n + 1) = BitFTA0CarryOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),z) ) ) ) holds
b1 = b2
proof end;
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 +* (BitFTA0Str ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),z)) & h . (n + 1) = BitFTA0CarryOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),z) ) ) )
proof end;
end;

:: deftheorem Def1 defines -BitFTA0Str FTACELL2:def 1 :
for n being Nat
for ap, bp, cp, dp being FinSequence
for b6 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign holds
( b6 = n -BitFTA0Str (ap,bp,cp,dp) iff ex f, h being ManySortedSet of NAT st
( b6 = 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 +* (BitFTA0Str ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),z)) & h . (n + 1) = BitFTA0CarryOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),z) ) ) ) );

:: Boolean circuit (MSAlgebra) realizing the n-bit compressor signature.
definition
let n be Nat;
let ap, bp, cp, dp be FinSequence;
func n -BitFTA0Circ (ap,bp,cp,dp) -> strict gate`2=den Boolean Circuit of n -BitFTA0Str (ap,bp,cp,dp) means :Def2: :: FTACELL2:def 2
 ex f, g, h being ManySortedSet of NAT st
( n -BitFTA0Str (ap,bp,cp,dp) = 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 +* (BitFTA0Str ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),z)) & g . (n + 1) = A +* (BitFTA0Circ ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),z)) & h . (n + 1) = BitFTA0CarryOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),z) ) ) );
uniqueness
for b1, b2 being strict gate`2=den Boolean Circuit of n -BitFTA0Str (ap,bp,cp,dp) st ex f, g, h being ManySortedSet of NAT st
( n -BitFTA0Str (ap,bp,cp,dp) = 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 +* (BitFTA0Str ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),z)) & g . (n + 1) = A +* (BitFTA0Circ ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),z)) & h . (n + 1) = BitFTA0CarryOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),z) ) ) ) & ex f, g, h being ManySortedSet of NAT st
( n -BitFTA0Str (ap,bp,cp,dp) = 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 +* (BitFTA0Str ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),z)) & g . (n + 1) = A +* (BitFTA0Circ ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),z)) & h . (n + 1) = BitFTA0CarryOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),z) ) ) ) holds
b1 = b2
proof end;
existence
ex b1 being strict gate`2=den Boolean Circuit of n -BitFTA0Str (ap,bp,cp,dp) ex f, g, h being ManySortedSet of NAT st
( n -BitFTA0Str (ap,bp,cp,dp) = 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 +* (BitFTA0Str ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),z)) & g . (n + 1) = A +* (BitFTA0Circ ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),z)) & h . (n + 1) = BitFTA0CarryOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),z) ) ) )
proof end;
end;

:: deftheorem Def2 defines -BitFTA0Circ FTACELL2:def 2 :
for n being Nat
for ap, bp, cp, dp being FinSequence
for b6 being strict gate`2=den Boolean Circuit of n -BitFTA0Str (ap,bp,cp,dp) holds
( b6 = n -BitFTA0Circ (ap,bp,cp,dp) iff ex f, g, h being ManySortedSet of NAT st
( n -BitFTA0Str (ap,bp,cp,dp) = f . n & b6 = 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 +* (BitFTA0Str ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),z)) & g . (n + 1) = A +* (BitFTA0Circ ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),z)) & h . (n + 1) = BitFTA0CarryOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),z) ) ) ) );

:: Carry-out signal vertex after n stages (head of the carry stream).
definition
let n be Nat;
let ap, bp, cp, dp be FinSequence;
func n -BitFTA0CarryOutput (ap,bp,cp,dp) -> Element of InnerVertices (n -BitFTA0Str (ap,bp,cp,dp)) means :Def3: :: FTACELL2: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) = BitFTA0CarryOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),(h . n)) ) );
uniqueness
for b1, b2 being Element of InnerVertices (n -BitFTA0Str (ap,bp,cp,dp)) 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) = BitFTA0CarryOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (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) = BitFTA0CarryOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),(h . n)) ) ) holds
b1 = b2
proof end;
existence
ex b1 being Element of InnerVertices (n -BitFTA0Str (ap,bp,cp,dp)) 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) = BitFTA0CarryOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),(h . n)) ) )
proof end;
end;

:: deftheorem Def3 defines -BitFTA0CarryOutput FTACELL2:def 3 :
for n being Nat
for ap, bp, cp, dp being FinSequence
for b6 being Element of InnerVertices (n -BitFTA0Str (ap,bp,cp,dp)) holds
( b6 = n -BitFTA0CarryOutput (ap,bp,cp,dp) iff ex h being ManySortedSet of NAT st
( b6 = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat holds h . (n + 1) = BitFTA0CarryOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),(h . n)) ) ) );

::-----------------------------------------------
:: Properties of n-depth FTA Structure and Circuit (TYPE-0)
::-----------------------------------------------
:: Characterization of the recursion: any (structure, circuit, carry)
:: streams satisfying the defining recurrence agree with
:: n-BitFTA0Str / n-BitFTA0Circ / n-BitFTA0CarryOutput at index n.
theorem Th1: :: FTACELL2:1
for ap, bp, cp, dp 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 +* (BitFTA0Str ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),z)) & g . (n + 1) = A +* (BitFTA0Circ ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),z)) & h . (n + 1) = BitFTA0CarryOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),z) ) ) holds
for n being Nat holds
( n -BitFTA0Str (ap,bp,cp,dp) = f . n & n -BitFTA0Circ (ap,bp,cp,dp) = g . n & n -BitFTA0CarryOutput (ap,bp,cp,dp) = h . n )
proof end;

:: Base case: the 0-bit structure, circuit and carry are all the FALSE
:: constant gate (resp. its algebra / output vertex).
theorem Th2: :: FTACELL2:2
for ap, bp, cp, dp being FinSequence holds
( 0 -BitFTA0Str (ap,bp,cp,dp) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & 0 -BitFTA0Circ (ap,bp,cp,dp) = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & 0 -BitFTA0CarryOutput (ap,bp,cp,dp) = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] )
proof end;

:: One-step unfolding: the (n+1)-stage structure, circuit and carry are
:: the n-stage ones composed with one further BitFTA0 cell that is fed the
:: n-stage carry output.
theorem Th3: :: FTACELL2:3
for n being Nat
for ap, bp, cp, dp being FinSequence holds
( (n + 1) -BitFTA0Str (ap,bp,cp,dp) = (n -BitFTA0Str (ap,bp,cp,dp)) +* (BitFTA0Str ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),(n -BitFTA0CarryOutput (ap,bp,cp,dp)))) & (n + 1) -BitFTA0Circ (ap,bp,cp,dp) = (n -BitFTA0Circ (ap,bp,cp,dp)) +* (BitFTA0Circ ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),(n -BitFTA0CarryOutput (ap,bp,cp,dp)))) & (n + 1) -BitFTA0CarryOutput (ap,bp,cp,dp) = BitFTA0CarryOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),(n -BitFTA0CarryOutput (ap,bp,cp,dp))) )
proof end;

LmT01: for ap, bp, cp being non pair set
for x, y, z being set holds InputVertices (BitGFA0Str (ap,bp,cp)) misses InnerVertices (BitGFA0Str (x,y,z))
proof end;

:: The carry output remains stable from T=2 onward.
theorem :: FTACELL2:4
for ap, bp, cp being non pair set
for dp, cin being set
for s being State of (BitFTA0Circ (ap,bp,cp,dp,cin))
for k being Nat st k >= 2 holds
(Following (s,k)) . (BitFTA0CarryOutput (ap,bp,cp,dp,cin)) = (Following (s,2)) . (BitFTA0CarryOutput (ap,bp,cp,dp,cin))
proof end;

::--------------------------------
:: Wavefront Layer Decomposition (TYPE-0)
::--------------------------------
:: Layer 1 = parallel composition of all stage-1 GFAs (independent,
:: 2-step stable). Layer 2 = parallel composition of all stage-2 GFAs
:: (reads Layer-1 adder outputs + previous carry). Notes: the row is
:: C(n) = Layer1(n) +* Layer2(n), so CIRCCMB2:19 gives 2+2 = 4.
:: Wavefront Layer 1 Structure (n-depth) : stage-1 GFAs
definition
let n be Nat;
let ap, bp, cp be FinSequence;
func n -BitFTA0Layer1Str (ap,bp,cp) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign means :Def4: :: FTACELL2:def 4
 ex f being ManySortedSet of NAT st
( it = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & ( for k being Nat
for S being non empty ManySortedSign st S = f . k holds
f . (k + 1) = S +* (BitGFA0Str ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) ) );
uniqueness
for b1, b2 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign st ex f being ManySortedSet of NAT st
( b1 = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & ( for k being Nat
for S being non empty ManySortedSign st S = f . k holds
f . (k + 1) = S +* (BitGFA0Str ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) ) ) & ex f being ManySortedSet of NAT st
( b2 = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & ( for k being Nat
for S being non empty ManySortedSign st S = f . k holds
f . (k + 1) = S +* (BitGFA0Str ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) ) ) holds
b1 = b2
proof end;
existence
ex b1 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex f being ManySortedSet of NAT st
( b1 = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & ( for k being Nat
for S being non empty ManySortedSign st S = f . k holds
f . (k + 1) = S +* (BitGFA0Str ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) ) )
proof end;
end;

:: deftheorem Def4 defines -BitFTA0Layer1Str FTACELL2:def 4 :
for n being Nat
for ap, bp, cp being FinSequence
for b5 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign holds
( b5 = n -BitFTA0Layer1Str (ap,bp,cp) iff ex f being ManySortedSet of NAT st
( b5 = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & ( for k being Nat
for S being non empty ManySortedSign st S = f . k holds
f . (k + 1) = S +* (BitGFA0Str ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) ) ) );

:: Wavefront Layer 1 Circuit (n-depth) : stage-1 GFAs
definition
let n be Nat;
let ap, bp, cp be FinSequence;
func n -BitFTA0Layer1Circ (ap,bp,cp) -> strict gate`2=den Boolean Circuit of n -BitFTA0Layer1Str (ap,bp,cp) means :Def5: :: FTACELL2:def 5
 ex f, g being ManySortedSet of NAT st
( n -BitFTA0Layer1Str (ap,bp,cp) = f . n & it = g . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & ( for k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S st S = f . k & A = g . k holds
( f . (k + 1) = S +* (BitGFA0Str ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) & g . (k + 1) = A +* (BitGFA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) ) ) );
uniqueness
for b1, b2 being strict gate`2=den Boolean Circuit of n -BitFTA0Layer1Str (ap,bp,cp) st ex f, g being ManySortedSet of NAT st
( n -BitFTA0Layer1Str (ap,bp,cp) = f . n & b1 = g . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & ( for k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S st S = f . k & A = g . k holds
( f . (k + 1) = S +* (BitGFA0Str ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) & g . (k + 1) = A +* (BitGFA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) ) ) ) & ex f, g being ManySortedSet of NAT st
( n -BitFTA0Layer1Str (ap,bp,cp) = f . n & b2 = g . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & ( for k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S st S = f . k & A = g . k holds
( f . (k + 1) = S +* (BitGFA0Str ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) & g . (k + 1) = A +* (BitGFA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) ) ) ) holds
b1 = b2
proof end;
existence
ex b1 being strict gate`2=den Boolean Circuit of n -BitFTA0Layer1Str (ap,bp,cp) ex f, g being ManySortedSet of NAT st
( n -BitFTA0Layer1Str (ap,bp,cp) = f . n & b1 = g . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & ( for k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S st S = f . k & A = g . k holds
( f . (k + 1) = S +* (BitGFA0Str ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) & g . (k + 1) = A +* (BitGFA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) ) ) )
proof end;
end;

:: deftheorem Def5 defines -BitFTA0Layer1Circ FTACELL2:def 5 :
for n being Nat
for ap, bp, cp being FinSequence
for b5 being strict gate`2=den Boolean Circuit of n -BitFTA0Layer1Str (ap,bp,cp) holds
( b5 = n -BitFTA0Layer1Circ (ap,bp,cp) iff ex f, g being ManySortedSet of NAT st
( n -BitFTA0Layer1Str (ap,bp,cp) = f . n & b5 = g . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & ( for k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S st S = f . k & A = g . k holds
( f . (k + 1) = S +* (BitGFA0Str ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) & g . (k + 1) = A +* (BitGFA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) ) ) ) );

:: Wavefront Layer 2 Structure (n-depth) : stage-2 GFAs + carry stream
definition
let n be Nat;
let ap, bp, cp, dp be FinSequence;
func n -BitFTA0Layer2Str (ap,bp,cp,dp) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign means :Def6: :: FTACELL2:def 6
 ex g, h being ManySortedSet of NAT st
( it = g . n & g . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for k being Nat
for S being non empty ManySortedSign
for z being set st S = g . k & z = h . k holds
( g . (k + 1) = S +* (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),z,(dp . (k + 1)))) & h . (k + 1) = GFA0CarryOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))) ) ) );
uniqueness
for b1, b2 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign st ex g, h being ManySortedSet of NAT st
( b1 = g . n & g . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for k being Nat
for S being non empty ManySortedSign
for z being set st S = g . k & z = h . k holds
( g . (k + 1) = S +* (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),z,(dp . (k + 1)))) & h . (k + 1) = GFA0CarryOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))) ) ) ) & ex g, h being ManySortedSet of NAT st
( b2 = g . n & g . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for k being Nat
for S being non empty ManySortedSign
for z being set st S = g . k & z = h . k holds
( g . (k + 1) = S +* (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),z,(dp . (k + 1)))) & h . (k + 1) = GFA0CarryOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))) ) ) ) holds
b1 = b2
proof end;
existence
ex b1 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex g, h being ManySortedSet of NAT st
( b1 = g . n & g . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for k being Nat
for S being non empty ManySortedSign
for z being set st S = g . k & z = h . k holds
( g . (k + 1) = S +* (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),z,(dp . (k + 1)))) & h . (k + 1) = GFA0CarryOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))) ) ) )
proof end;
end;

:: deftheorem Def6 defines -BitFTA0Layer2Str FTACELL2:def 6 :
for n being Nat
for ap, bp, cp, dp being FinSequence
for b6 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign holds
( b6 = n -BitFTA0Layer2Str (ap,bp,cp,dp) iff ex g, h being ManySortedSet of NAT st
( b6 = g . n & g . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for k being Nat
for S being non empty ManySortedSign
for z being set st S = g . k & z = h . k holds
( g . (k + 1) = S +* (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),z,(dp . (k + 1)))) & h . (k + 1) = GFA0CarryOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))) ) ) ) );

:: Wavefront Layer 2 Circuit (n-depth) : stage-2 GFAs + carry stream
definition
let n be Nat;
let ap, bp, cp, dp be FinSequence;
func n -BitFTA0Layer2Circ (ap,bp,cp,dp) -> strict gate`2=den Boolean Circuit of n -BitFTA0Layer2Str (ap,bp,cp,dp) means :Def7: :: FTACELL2:def 7
 ex f, g, h being ManySortedSet of NAT st
( n -BitFTA0Layer2Str (ap,bp,cp,dp) = 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 k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f . k & A = g . k & z = h . k holds
( f . (k + 1) = S +* (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),z,(dp . (k + 1)))) & g . (k + 1) = A +* (BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),z,(dp . (k + 1)))) & h . (k + 1) = GFA0CarryOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))) ) ) );
uniqueness
for b1, b2 being strict gate`2=den Boolean Circuit of n -BitFTA0Layer2Str (ap,bp,cp,dp) st ex f, g, h being ManySortedSet of NAT st
( n -BitFTA0Layer2Str (ap,bp,cp,dp) = 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 k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f . k & A = g . k & z = h . k holds
( f . (k + 1) = S +* (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),z,(dp . (k + 1)))) & g . (k + 1) = A +* (BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),z,(dp . (k + 1)))) & h . (k + 1) = GFA0CarryOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))) ) ) ) & ex f, g, h being ManySortedSet of NAT st
( n -BitFTA0Layer2Str (ap,bp,cp,dp) = 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 k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f . k & A = g . k & z = h . k holds
( f . (k + 1) = S +* (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),z,(dp . (k + 1)))) & g . (k + 1) = A +* (BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),z,(dp . (k + 1)))) & h . (k + 1) = GFA0CarryOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))) ) ) ) holds
b1 = b2
proof end;
existence
ex b1 being strict gate`2=den Boolean Circuit of n -BitFTA0Layer2Str (ap,bp,cp,dp) ex f, g, h being ManySortedSet of NAT st
( n -BitFTA0Layer2Str (ap,bp,cp,dp) = 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 k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f . k & A = g . k & z = h . k holds
( f . (k + 1) = S +* (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),z,(dp . (k + 1)))) & g . (k + 1) = A +* (BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),z,(dp . (k + 1)))) & h . (k + 1) = GFA0CarryOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))) ) ) )
proof end;
end;

:: deftheorem Def7 defines -BitFTA0Layer2Circ FTACELL2:def 7 :
for n being Nat
for ap, bp, cp, dp being FinSequence
for b6 being strict gate`2=den Boolean Circuit of n -BitFTA0Layer2Str (ap,bp,cp,dp) holds
( b6 = n -BitFTA0Layer2Circ (ap,bp,cp,dp) iff ex f, g, h being ManySortedSet of NAT st
( n -BitFTA0Layer2Str (ap,bp,cp,dp) = f . n & b6 = 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 k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f . k & A = g . k & z = h . k holds
( f . (k + 1) = S +* (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),z,(dp . (k + 1)))) & g . (k + 1) = A +* (BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),z,(dp . (k + 1)))) & h . (k + 1) = GFA0CarryOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))) ) ) ) );

LmF: for f1, f2, f3, f4 being Function st f2 tolerates f3 holds
(f1 +* f2) +* (f3 +* f4) = (f1 +* f3) +* (f2 +* f4)
proof end;

LmT05A: for n being Nat
for ap, bp, cp being FinSequence holds (n + 1) -BitFTA0Layer1Str (ap,bp,cp) = (n -BitFTA0Layer1Str (ap,bp,cp)) +* (BitGFA0Str ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1))))
proof end;

LmT05B: for n being Nat
for ap, bp, cp, dp being FinSequence holds (n + 1) -BitFTA0Layer2Str (ap,bp,cp,dp) = (n -BitFTA0Layer2Str (ap,bp,cp,dp)) +* (BitGFA0Str ((GFA0AdderOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)))),(n -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (n + 1))))
proof end;

:: Main proposition - Two-Layer Circuit Composition (Structure-level)
theorem Th5: :: FTACELL2:5
for n being Nat
for ap, bp, cp, dp being FinSequence holds n -BitFTA0Str (ap,bp,cp,dp) = (n -BitFTA0Layer1Str (ap,bp,cp)) +* (n -BitFTA0Layer2Str (ap,bp,cp,dp))
proof end;

LmT06A: for n being Nat
for ap, bp, cp being FinSequence holds (n + 1) -BitFTA0Layer1Circ (ap,bp,cp) = (n -BitFTA0Layer1Circ (ap,bp,cp)) +* (BitGFA0Circ ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1))))
proof end;

LmT06B: for n being Nat
for ap, bp, cp, dp being FinSequence holds (n + 1) -BitFTA0Layer2Circ (ap,bp,cp,dp) = (n -BitFTA0Layer2Circ (ap,bp,cp,dp)) +* (BitGFA0Circ ((GFA0AdderOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)))),(n -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (n + 1))))
proof end;

:: Main proposition - Two-Layer Circuit Composition (Circuit level)
:: Circ +* (CIRCCOMB:def 4) is partial, so no congruence-rewrite through it
:: (unlike Str, Th5). Both base and step are closed by Sorts/Charact
:: extensionality reduced to the map-level rearrange LmF (CIRCCOMB:23 idiom).
theorem Th6: :: FTACELL2:6
for n being Nat
for ap, bp, cp, dp being FinSequence holds n -BitFTA0Circ (ap,bp,cp,dp) = (n -BitFTA0Layer1Circ (ap,bp,cp)) +* (n -BitFTA0Layer2Circ (ap,bp,cp,dp))
proof end;

LmT00L1: for ap, bp, cp being FinSequence holds 0 -BitFTA0Layer1Str (ap,bp,cp) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))
proof end;

LmT00L2: for ap, bp, cp, dp being FinSequence holds 0 -BitFTA0Layer2Str (ap,bp,cp,dp) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))
proof end;

LmT0L2rel: for n being Nat
for ap, bp, cp, dp being FinSequence holds InnerVertices (n -BitFTA0Layer2Str (ap,bp,cp,dp)) is Relation
proof end;

LmT0L1wp: for n being Nat
for ap, bp, cp being nonpair-yielding FinSequence holds InputVertices (n -BitFTA0Layer1Str (ap,bp,cp)) is without_pairs
proof end;

:: Feed-forward disjointness : Layer 1 inputs miss Layer 2 gates.
theorem Th7: :: FTACELL2:7
for n being Nat
for ap, bp, cp, dp being nonpair-yielding FinSequence holds InputVertices (n -BitFTA0Layer1Str (ap,bp,cp)) misses InnerVertices (n -BitFTA0Layer2Str (ap,bp,cp,dp))
proof end;

LmT0L1rel: for n being Nat
for ap, bp, cp being FinSequence holds InnerVertices (n -BitFTA0Layer1Str (ap,bp,cp)) is Relation
proof end;

LmT0CO: for n being Nat
for ap, bp, cp, dp being FinSequence
for x, y being set holds n -BitFTA0CarryOutput (ap,bp,cp,dp) <> [<*x,y*>,and2]
proof end;

::-----------------------------------------------------------
:: Layer 1 (parallel stage-1 GFAs) stabilizes in 2 steps.
:: Each stage-1 cell is 2-stable (GFACIRC1:40) and the cells are
:: mutually independent, so the parallel-max rule (CIRCCMB2:24) gives 2.
::-----------------------------------------------------------
theorem Th8: :: FTACELL2:8
for n being Nat
for ap, bp, cp being nonpair-yielding FinSequence
for s being State of (n -BitFTA0Layer1Circ (ap,bp,cp)) holds Following (s,2) is stable
proof end;

LmT0L2inner: for n being Nat
for ap, bp, cp, dp being FinSequence holds InnerVertices ((n + 1) -BitFTA0Layer2Str (ap,bp,cp,dp)) = (InnerVertices (n -BitFTA0Layer2Str (ap,bp,cp,dp))) \/ (InnerVertices (BitGFA0Str ((GFA0AdderOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)))),(n -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (n + 1)))))
proof end;

LmT00CO: for ap, bp, cp, dp being FinSequence holds 0 -BitFTA0CarryOutput (ap,bp,cp,dp) = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]
proof end;

LmT0COk: for m being Nat
for ap, bp, cp, dp being FinSequence holds (m + 1) -BitFTA0CarryOutput (ap,bp,cp,dp) = GFA0CarryOutput ((ap . (m + 1)),(bp . (m + 1)),(cp . (m + 1)))
proof end;

LmT0COp: for n being Nat
for ap, bp, cp, dp being FinSequence holds n -BitFTA0CarryOutput (ap,bp,cp,dp) is pair
proof end;

LmT0W1: for a, b, c being non pair set
for X, Y, d being set st Y is pair holds
not GFA0AdderOutput (a,b,c) in InnerVertices (BitGFA0Str (X,Y,d))
proof end;

LmT0W2: for a, b, c being non pair set
for X, Y, d being set st Y is pair holds
not GFA0CarryOutput (a,b,c) in InnerVertices (BitGFA0Str (X,Y,d))
proof end;

LmT0C2i: for k being Nat
for ap, bp, cp, dp being nonpair-yielding FinSequence holds InputVertices (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)))) = {(GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))}
proof end;

LmT0C2s: for k being Nat
for ap, bp, cp, dp being nonpair-yielding FinSequence
for s being State of (BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)))) holds Following (s,2) is stable
proof end;

LmT0Cin0In: for n being Nat
for ap, bp, cp, dp being FinSequence holds [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] in InnerVertices (n -BitFTA0Layer2Str (ap,bp,cp,dp))
proof end;

LmT0WnI: for n being Nat
for ap, bp, cp, dp being nonpair-yielding FinSequence
for u, v, x being non pair set holds
( not GFA0AdderOutput (u,v,x) in InnerVertices (n -BitFTA0Layer2Str (ap,bp,cp,dp)) & not GFA0CarryOutput (u,v,x) in InnerVertices (n -BitFTA0Layer2Str (ap,bp,cp,dp)) )
proof end;

LmT0InAcc: for n being Nat
for ap, bp, cp, dp being nonpair-yielding FinSequence
for w being set holds
( not w in InputVertices (n -BitFTA0Layer2Str (ap,bp,cp,dp)) or not w is pair or ex u, v, x being non pair set st w = GFA0AdderOutput (u,v,x) or ex u, v, x being non pair set st w = GFA0CarryOutput (u,v,x) )
proof end;

LmT0Dj1: for k being Nat
for ap, bp, cp, dp being nonpair-yielding FinSequence holds InputVertices (k -BitFTA0Layer2Str (ap,bp,cp,dp)) misses InnerVertices (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))))
proof end;

LmT0Dj2: for m being Nat
for ap, bp, cp, dp being nonpair-yielding FinSequence holds InputVertices (BitGFA0Str ((GFA0AdderOutput ((ap . ((m + 1) + 1)),(bp . ((m + 1) + 1)),(cp . ((m + 1) + 1)))),((m + 1) -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . ((m + 1) + 1)))) misses InnerVertices ((m + 1) -BitFTA0Layer2Str (ap,bp,cp,dp))
proof end;

:: The FALSE constant gate recomputes its output to FALSE in one
:: step, in any circuit containing it as a gate.
theorem Th9: :: FTACELL2:9
for S being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
for A being non-empty gate`2=den Boolean Circuit of S st [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] in InnerVertices S holds
for s being State of A holds (Following s) . [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] = FALSE
proof end;

:: Layer 2 stabilizes in 2 steps from any state where the FALSE
:: base output vertex is already settled. The k = 0 cell composes
:: by cascade with n1 = 0 (the settled base is already stable);
:: later cells compose in parallel.
theorem Th10: :: FTACELL2:10
for n being Nat
for ap, bp, cp, dp being nonpair-yielding FinSequence
for s being State of (n -BitFTA0Layer2Circ (ap,bp,cp,dp)) st s . [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] = FALSE holds
Following (s,2) is stable
proof end;

::--------------------------------
:: Stability of n-depth FTA Circuit (TYPE-0)
::--------------------------------
theorem :: FTACELL2:11
for n being Nat
for ap, bp, cp, dp being nonpair-yielding FinSeqLen of n
for s being State of (n -BitFTA0Circ (ap,bp,cp,dp)) holds Following (s,4) is stable
proof end;

::------------------------------------------------
:: Definitions of n-depth FTA Structure and Circuit (TYPE-1)
::------------------------------------------------
:: Signature of the n-bit 4-2 compressor (TYPE-1): a FALSE base gate
:: followed by n BitFTA1 stage cells composed with +*, each fed the
:: running carry. TYPE-1 negates the second and fourth addends.
definition
let n be Nat;
let ap, bm, cp, dm 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 -BitFTA1Str (ap,bm,cp,dm) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign means :Def8: :: FTACELL2:def 8
 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 +* (BitFTA1Str ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z)) & h . (n + 1) = BitFTA1CarryOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (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 +* (BitFTA1Str ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z)) & h . (n + 1) = BitFTA1CarryOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (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 +* (BitFTA1Str ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z)) & h . (n + 1) = BitFTA1CarryOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z) ) ) ) holds
b1 = b2
proof end;
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 +* (BitFTA1Str ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z)) & h . (n + 1) = BitFTA1CarryOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z) ) ) )
proof end;
end;

:: deftheorem Def8 defines -BitFTA1Str FTACELL2:def 8 :
for n being Nat
for ap, bm, cp, dm being FinSequence
for b6 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign holds
( b6 = n -BitFTA1Str (ap,bm,cp,dm) iff ex f, h being ManySortedSet of NAT st
( b6 = 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 +* (BitFTA1Str ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z)) & h . (n + 1) = BitFTA1CarryOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z) ) ) ) );

:: Boolean circuit (MSAlgebra) realizing the n-bit TYPE-1 signature.
definition
let n be Nat;
let ap, bm, cp, dm be FinSequence;
func n -BitFTA1Circ (ap,bm,cp,dm) -> strict gate`2=den Boolean Circuit of n -BitFTA1Str (ap,bm,cp,dm) means :Def9: :: FTACELL2:def 9
 ex f, g, h being ManySortedSet of NAT st
( n -BitFTA1Str (ap,bm,cp,dm) = 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 +* (BitFTA1Str ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z)) & g . (n + 1) = A +* (BitFTA1Circ ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z)) & h . (n + 1) = BitFTA1CarryOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z) ) ) );
uniqueness
for b1, b2 being strict gate`2=den Boolean Circuit of n -BitFTA1Str (ap,bm,cp,dm) st ex f, g, h being ManySortedSet of NAT st
( n -BitFTA1Str (ap,bm,cp,dm) = 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 +* (BitFTA1Str ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z)) & g . (n + 1) = A +* (BitFTA1Circ ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z)) & h . (n + 1) = BitFTA1CarryOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z) ) ) ) & ex f, g, h being ManySortedSet of NAT st
( n -BitFTA1Str (ap,bm,cp,dm) = 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 +* (BitFTA1Str ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z)) & g . (n + 1) = A +* (BitFTA1Circ ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z)) & h . (n + 1) = BitFTA1CarryOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z) ) ) ) holds
b1 = b2
proof end;
existence
ex b1 being strict gate`2=den Boolean Circuit of n -BitFTA1Str (ap,bm,cp,dm) ex f, g, h being ManySortedSet of NAT st
( n -BitFTA1Str (ap,bm,cp,dm) = 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 +* (BitFTA1Str ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z)) & g . (n + 1) = A +* (BitFTA1Circ ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z)) & h . (n + 1) = BitFTA1CarryOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z) ) ) )
proof end;
end;

:: deftheorem Def9 defines -BitFTA1Circ FTACELL2:def 9 :
for n being Nat
for ap, bm, cp, dm being FinSequence
for b6 being strict gate`2=den Boolean Circuit of n -BitFTA1Str (ap,bm,cp,dm) holds
( b6 = n -BitFTA1Circ (ap,bm,cp,dm) iff ex f, g, h being ManySortedSet of NAT st
( n -BitFTA1Str (ap,bm,cp,dm) = f . n & b6 = 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 +* (BitFTA1Str ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z)) & g . (n + 1) = A +* (BitFTA1Circ ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z)) & h . (n + 1) = BitFTA1CarryOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z) ) ) ) );

:: Carry-out signal vertex after n stages (head of the carry stream).
definition
let n be Nat;
let ap, bm, cp, dm be FinSequence;
func n -BitFTA1CarryOutput (ap,bm,cp,dm) -> Element of InnerVertices (n -BitFTA1Str (ap,bm,cp,dm)) means :Def10: :: FTACELL2:def 10
 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) = BitFTA1CarryOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),(h . n)) ) );
uniqueness
for b1, b2 being Element of InnerVertices (n -BitFTA1Str (ap,bm,cp,dm)) 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) = BitFTA1CarryOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (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) = BitFTA1CarryOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),(h . n)) ) ) holds
b1 = b2
proof end;
existence
ex b1 being Element of InnerVertices (n -BitFTA1Str (ap,bm,cp,dm)) 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) = BitFTA1CarryOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),(h . n)) ) )
proof end;
end;

:: deftheorem Def10 defines -BitFTA1CarryOutput FTACELL2:def 10 :
for n being Nat
for ap, bm, cp, dm being FinSequence
for b6 being Element of InnerVertices (n -BitFTA1Str (ap,bm,cp,dm)) holds
( b6 = n -BitFTA1CarryOutput (ap,bm,cp,dm) iff ex h being ManySortedSet of NAT st
( b6 = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat holds h . (n + 1) = BitFTA1CarryOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),(h . n)) ) ) );

::-----------------------------------------------
:: Properties of n-depth FTA Structure and Circuit (TYPE-1)
::-----------------------------------------------
:: Characterization of the recursion: any (structure, circuit, carry)
:: streams satisfying the defining recurrence agree with
:: n-BitFTA1Str / n-BitFTA1Circ / n-BitFTA1CarryOutput at index n.
theorem Th12: :: FTACELL2:12
for ap, bm, cp, dm 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 +* (BitFTA1Str ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z)) & g . (n + 1) = A +* (BitFTA1Circ ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z)) & h . (n + 1) = BitFTA1CarryOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z) ) ) holds
for n being Nat holds
( n -BitFTA1Str (ap,bm,cp,dm) = f . n & n -BitFTA1Circ (ap,bm,cp,dm) = g . n & n -BitFTA1CarryOutput (ap,bm,cp,dm) = h . n )
proof end;

:: Base case: the 0-bit structure, circuit and carry are all the FALSE
:: constant gate (resp. its algebra / output vertex).
theorem Th13: :: FTACELL2:13
for ap, bm, cp, dm being FinSequence holds
( 0 -BitFTA1Str (ap,bm,cp,dm) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & 0 -BitFTA1Circ (ap,bm,cp,dm) = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & 0 -BitFTA1CarryOutput (ap,bm,cp,dm) = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] )
proof end;

:: One-step unfolding: the (n+1)-stage structure, circuit and carry are
:: the n-stage ones composed with one further BitFTA1 cell that is fed the
:: n-stage carry output.
theorem Th14: :: FTACELL2:14
for n being Nat
for ap, bm, cp, dm being FinSequence holds
( (n + 1) -BitFTA1Str (ap,bm,cp,dm) = (n -BitFTA1Str (ap,bm,cp,dm)) +* (BitFTA1Str ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),(n -BitFTA1CarryOutput (ap,bm,cp,dm)))) & (n + 1) -BitFTA1Circ (ap,bm,cp,dm) = (n -BitFTA1Circ (ap,bm,cp,dm)) +* (BitFTA1Circ ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),(n -BitFTA1CarryOutput (ap,bm,cp,dm)))) & (n + 1) -BitFTA1CarryOutput (ap,bm,cp,dm) = BitFTA1CarryOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),(n -BitFTA1CarryOutput (ap,bm,cp,dm))) )
proof end;

LmT11: for ap, bm, cp being non pair set
for x, y, z being set holds InputVertices (BitGFA1Str (ap,bm,cp)) misses InnerVertices (BitGFA2Str (x,y,z))
proof end;

:: The carry output remains stable from T=2 onward.
theorem :: FTACELL2:15
for ap, bm, cp being non pair set
for dm, cin being set
for s being State of (BitFTA1Circ (ap,bm,cp,dm,cin))
for k being Nat st k >= 2 holds
(Following (s,k)) . (BitFTA1CarryOutput (ap,bm,cp,dm,cin)) = (Following (s,2)) . (BitFTA1CarryOutput (ap,bm,cp,dm,cin))
proof end;

::------------------------------------------------
:: Wavefront Layer Decomposition (TYPE-1)
:: Layer 1 collects the stage-1 cells BitGFA1Str(a,b,c) of every column;
:: layer 2 collects the stage-2 cells, which for TYPE-1 are BitGFA2Str
:: applied to the stage-1 sum, the lateral carry and the fourth addend.
::------------------------------------------------
:: Wavefront Layer 1 Structure (n-depth) : stage-1 GFA1s
definition
let n be Nat;
let ap, bm, cp be FinSequence;
func n -BitFTA1Layer1Str (ap,bm,cp) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign means :Def11: :: FTACELL2:def 11
 ex f being ManySortedSet of NAT st
( it = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & ( for k being Nat
for S being non empty ManySortedSign st S = f . k holds
f . (k + 1) = S +* (BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) ) );
uniqueness
for b1, b2 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign st ex f being ManySortedSet of NAT st
( b1 = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & ( for k being Nat
for S being non empty ManySortedSign st S = f . k holds
f . (k + 1) = S +* (BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) ) ) & ex f being ManySortedSet of NAT st
( b2 = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & ( for k being Nat
for S being non empty ManySortedSign st S = f . k holds
f . (k + 1) = S +* (BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) ) ) holds
b1 = b2
proof end;
existence
ex b1 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex f being ManySortedSet of NAT st
( b1 = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & ( for k being Nat
for S being non empty ManySortedSign st S = f . k holds
f . (k + 1) = S +* (BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) ) )
proof end;
end;

:: deftheorem Def11 defines -BitFTA1Layer1Str FTACELL2:def 11 :
for n being Nat
for ap, bm, cp being FinSequence
for b5 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign holds
( b5 = n -BitFTA1Layer1Str (ap,bm,cp) iff ex f being ManySortedSet of NAT st
( b5 = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & ( for k being Nat
for S being non empty ManySortedSign st S = f . k holds
f . (k + 1) = S +* (BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) ) ) );

:: Wavefront Layer 1 Circuit (n-depth) : stage-1 GFA1s
definition
let n be Nat;
let ap, bm, cp be FinSequence;
func n -BitFTA1Layer1Circ (ap,bm,cp) -> strict gate`2=den Boolean Circuit of n -BitFTA1Layer1Str (ap,bm,cp) means :Def12: :: FTACELL2:def 12
 ex f, g being ManySortedSet of NAT st
( n -BitFTA1Layer1Str (ap,bm,cp) = f . n & it = g . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & ( for k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S st S = f . k & A = g . k holds
( f . (k + 1) = S +* (BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) & g . (k + 1) = A +* (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) ) ) );
uniqueness
for b1, b2 being strict gate`2=den Boolean Circuit of n -BitFTA1Layer1Str (ap,bm,cp) st ex f, g being ManySortedSet of NAT st
( n -BitFTA1Layer1Str (ap,bm,cp) = f . n & b1 = g . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & ( for k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S st S = f . k & A = g . k holds
( f . (k + 1) = S +* (BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) & g . (k + 1) = A +* (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) ) ) ) & ex f, g being ManySortedSet of NAT st
( n -BitFTA1Layer1Str (ap,bm,cp) = f . n & b2 = g . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & ( for k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S st S = f . k & A = g . k holds
( f . (k + 1) = S +* (BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) & g . (k + 1) = A +* (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) ) ) ) holds
b1 = b2
proof end;
existence
ex b1 being strict gate`2=den Boolean Circuit of n -BitFTA1Layer1Str (ap,bm,cp) ex f, g being ManySortedSet of NAT st
( n -BitFTA1Layer1Str (ap,bm,cp) = f . n & b1 = g . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & ( for k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S st S = f . k & A = g . k holds
( f . (k + 1) = S +* (BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) & g . (k + 1) = A +* (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) ) ) )
proof end;
end;

:: deftheorem Def12 defines -BitFTA1Layer1Circ FTACELL2:def 12 :
for n being Nat
for ap, bm, cp being FinSequence
for b5 being strict gate`2=den Boolean Circuit of n -BitFTA1Layer1Str (ap,bm,cp) holds
( b5 = n -BitFTA1Layer1Circ (ap,bm,cp) iff ex f, g being ManySortedSet of NAT st
( n -BitFTA1Layer1Str (ap,bm,cp) = f . n & b5 = g . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & ( for k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S st S = f . k & A = g . k holds
( f . (k + 1) = S +* (BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) & g . (k + 1) = A +* (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) ) ) ) );

:: Wavefront Layer 2 Structure (n-depth) : stage-2 GFA2s + carry stream
definition
let n be Nat;
let ap, bm, cp, dm be FinSequence;
func n -BitFTA1Layer2Str (ap,bm,cp,dm) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign means :Def13: :: FTACELL2:def 13
 ex g, h being ManySortedSet of NAT st
( it = g . n & g . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for k being Nat
for S being non empty ManySortedSign
for z being set st S = g . k & z = h . k holds
( g . (k + 1) = S +* (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),z,(dm . (k + 1)))) & h . (k + 1) = GFA1CarryOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))) ) ) );
uniqueness
for b1, b2 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign st ex g, h being ManySortedSet of NAT st
( b1 = g . n & g . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for k being Nat
for S being non empty ManySortedSign
for z being set st S = g . k & z = h . k holds
( g . (k + 1) = S +* (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),z,(dm . (k + 1)))) & h . (k + 1) = GFA1CarryOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))) ) ) ) & ex g, h being ManySortedSet of NAT st
( b2 = g . n & g . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for k being Nat
for S being non empty ManySortedSign
for z being set st S = g . k & z = h . k holds
( g . (k + 1) = S +* (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),z,(dm . (k + 1)))) & h . (k + 1) = GFA1CarryOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))) ) ) ) holds
b1 = b2
proof end;
existence
ex b1 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex g, h being ManySortedSet of NAT st
( b1 = g . n & g . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for k being Nat
for S being non empty ManySortedSign
for z being set st S = g . k & z = h . k holds
( g . (k + 1) = S +* (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),z,(dm . (k + 1)))) & h . (k + 1) = GFA1CarryOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))) ) ) )
proof end;
end;

:: deftheorem Def13 defines -BitFTA1Layer2Str FTACELL2:def 13 :
for n being Nat
for ap, bm, cp, dm being FinSequence
for b6 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign holds
( b6 = n -BitFTA1Layer2Str (ap,bm,cp,dm) iff ex g, h being ManySortedSet of NAT st
( b6 = g . n & g . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for k being Nat
for S being non empty ManySortedSign
for z being set st S = g . k & z = h . k holds
( g . (k + 1) = S +* (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),z,(dm . (k + 1)))) & h . (k + 1) = GFA1CarryOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))) ) ) ) );

:: Wavefront Layer 2 Circuit (n-depth) : stage-2 GFA2s + carry stream
definition
let n be Nat;
let ap, bm, cp, dm be FinSequence;
func n -BitFTA1Layer2Circ (ap,bm,cp,dm) -> strict gate`2=den Boolean Circuit of n -BitFTA1Layer2Str (ap,bm,cp,dm) means :Def14: :: FTACELL2:def 14
 ex f, g, h being ManySortedSet of NAT st
( n -BitFTA1Layer2Str (ap,bm,cp,dm) = 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 k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f . k & A = g . k & z = h . k holds
( f . (k + 1) = S +* (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),z,(dm . (k + 1)))) & g . (k + 1) = A +* (BitGFA2Circ ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),z,(dm . (k + 1)))) & h . (k + 1) = GFA1CarryOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))) ) ) );
uniqueness
for b1, b2 being strict gate`2=den Boolean Circuit of n -BitFTA1Layer2Str (ap,bm,cp,dm) st ex f, g, h being ManySortedSet of NAT st
( n -BitFTA1Layer2Str (ap,bm,cp,dm) = 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 k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f . k & A = g . k & z = h . k holds
( f . (k + 1) = S +* (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),z,(dm . (k + 1)))) & g . (k + 1) = A +* (BitGFA2Circ ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),z,(dm . (k + 1)))) & h . (k + 1) = GFA1CarryOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))) ) ) ) & ex f, g, h being ManySortedSet of NAT st
( n -BitFTA1Layer2Str (ap,bm,cp,dm) = 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 k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f . k & A = g . k & z = h . k holds
( f . (k + 1) = S +* (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),z,(dm . (k + 1)))) & g . (k + 1) = A +* (BitGFA2Circ ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),z,(dm . (k + 1)))) & h . (k + 1) = GFA1CarryOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))) ) ) ) holds
b1 = b2
proof end;
existence
ex b1 being strict gate`2=den Boolean Circuit of n -BitFTA1Layer2Str (ap,bm,cp,dm) ex f, g, h being ManySortedSet of NAT st
( n -BitFTA1Layer2Str (ap,bm,cp,dm) = 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 k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f . k & A = g . k & z = h . k holds
( f . (k + 1) = S +* (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),z,(dm . (k + 1)))) & g . (k + 1) = A +* (BitGFA2Circ ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),z,(dm . (k + 1)))) & h . (k + 1) = GFA1CarryOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))) ) ) )
proof end;
end;

:: deftheorem Def14 defines -BitFTA1Layer2Circ FTACELL2:def 14 :
for n being Nat
for ap, bm, cp, dm being FinSequence
for b6 being strict gate`2=den Boolean Circuit of n -BitFTA1Layer2Str (ap,bm,cp,dm) holds
( b6 = n -BitFTA1Layer2Circ (ap,bm,cp,dm) iff ex f, g, h being ManySortedSet of NAT st
( n -BitFTA1Layer2Str (ap,bm,cp,dm) = f . n & b6 = 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 k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f . k & A = g . k & z = h . k holds
( f . (k + 1) = S +* (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),z,(dm . (k + 1)))) & g . (k + 1) = A +* (BitGFA2Circ ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),z,(dm . (k + 1)))) & h . (k + 1) = GFA1CarryOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))) ) ) ) );

LmT15A: for n being Nat
for ap, bm, cp being FinSequence holds (n + 1) -BitFTA1Layer1Str (ap,bm,cp) = (n -BitFTA1Layer1Str (ap,bm,cp)) +* (BitGFA1Str ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1))))
proof end;

LmT15B: for n being Nat
for ap, bm, cp, dm being FinSequence holds (n + 1) -BitFTA1Layer2Str (ap,bm,cp,dm) = (n -BitFTA1Layer2Str (ap,bm,cp,dm)) +* (BitGFA2Str ((GFA1AdderOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)))),(n -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (n + 1))))
proof end;

:: Main proposition - Two-Layer Circuit Composition (Structure-level)
theorem Th16: :: FTACELL2:16
for n being Nat
for ap, bm, cp, dm being FinSequence holds n -BitFTA1Str (ap,bm,cp,dm) = (n -BitFTA1Layer1Str (ap,bm,cp)) +* (n -BitFTA1Layer2Str (ap,bm,cp,dm))
proof end;

LmT16A: for n being Nat
for ap, bm, cp being FinSequence holds (n + 1) -BitFTA1Layer1Circ (ap,bm,cp) = (n -BitFTA1Layer1Circ (ap,bm,cp)) +* (BitGFA1Circ ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1))))
proof end;

LmT16B: for n being Nat
for ap, bm, cp, dm being FinSequence holds (n + 1) -BitFTA1Layer2Circ (ap,bm,cp,dm) = (n -BitFTA1Layer2Circ (ap,bm,cp,dm)) +* (BitGFA2Circ ((GFA1AdderOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)))),(n -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (n + 1))))
proof end;

:: Main proposition - Two-Layer Circuit Composition (Circuit level)
:: Circ +* (CIRCCOMB:def 4) is partial, so no congruence-rewrite through it
:: (unlike Str, Th16). Both base and step are closed by Sorts/Charact
:: extensionality reduced to the map-level rearrange LmF (CIRCCOMB:23 idiom).
theorem Th17: :: FTACELL2:17
for n being Nat
for ap, bm, cp, dm being FinSequence holds n -BitFTA1Circ (ap,bm,cp,dm) = (n -BitFTA1Layer1Circ (ap,bm,cp)) +* (n -BitFTA1Layer2Circ (ap,bm,cp,dm))
proof end;

LmT10L1: for ap, bm, cp being FinSequence holds 0 -BitFTA1Layer1Str (ap,bm,cp) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))
proof end;

LmT10L2: for ap, bm, cp, dm being FinSequence holds 0 -BitFTA1Layer2Str (ap,bm,cp,dm) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))
proof end;

LmT1L2rel: for n being Nat
for ap, bm, cp, dm being FinSequence holds InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm)) is Relation
proof end;

LmT1L1wp: for n being Nat
for ap, bm, cp being nonpair-yielding FinSequence holds InputVertices (n -BitFTA1Layer1Str (ap,bm,cp)) is without_pairs
proof end;

:: Feed-forward disjointness : Layer 1 inputs miss Layer 2 gates.
theorem Th18: :: FTACELL2:18
for n being Nat
for ap, bm, cp, dm being nonpair-yielding FinSequence holds InputVertices (n -BitFTA1Layer1Str (ap,bm,cp)) misses InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm))
proof end;

LmT1L1rel: for n being Nat
for ap, bm, cp being FinSequence holds InnerVertices (n -BitFTA1Layer1Str (ap,bm,cp)) is Relation
proof end;

LmT1CO: for n being Nat
for ap, bm, cp, dm being FinSequence
for x, y being set holds n -BitFTA1CarryOutput (ap,bm,cp,dm) <> [<*x,y*>,nor2]
proof end;

::-----------------------------------------------------------
:: Layer 1 (parallel stage-1 GFA1s) stabilizes in 2 steps.
:: Each stage-1 cell is 2-stable (GFACIRC1:72) and the cells are
:: mutually independent, so the parallel-max rule (CIRCCMB2:24) gives 2.
::-----------------------------------------------------------
theorem Th19: :: FTACELL2:19
for n being Nat
for ap, bm, cp being nonpair-yielding FinSequence
for s being State of (n -BitFTA1Layer1Circ (ap,bm,cp)) holds Following (s,2) is stable
proof end;

LmT1L2inner: for n being Nat
for ap, bm, cp, dm being FinSequence holds InnerVertices ((n + 1) -BitFTA1Layer2Str (ap,bm,cp,dm)) = (InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm))) \/ (InnerVertices (BitGFA2Str ((GFA1AdderOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)))),(n -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (n + 1)))))
proof end;

LmT10CO: for ap, bm, cp, dm being FinSequence holds 0 -BitFTA1CarryOutput (ap,bm,cp,dm) = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]
proof end;

LmT1COk: for m being Nat
for ap, bm, cp, dm being FinSequence holds (m + 1) -BitFTA1CarryOutput (ap,bm,cp,dm) = GFA1CarryOutput ((ap . (m + 1)),(bm . (m + 1)),(cp . (m + 1)))
proof end;

LmT1COp: for n being Nat
for ap, bm, cp, dm being FinSequence holds n -BitFTA1CarryOutput (ap,bm,cp,dm) is pair
proof end;

LmT1W1: for a, b, c being non pair set
for X, Y, d being set st Y is pair holds
not GFA1AdderOutput (a,b,c) in InnerVertices (BitGFA2Str (X,Y,d))
proof end;

LmT1W2: for a, b, c being non pair set
for X, Y, d being set st Y is pair holds
not GFA1CarryOutput (a,b,c) in InnerVertices (BitGFA2Str (X,Y,d))
proof end;

LmT1C2i: for k being Nat
for ap, bm, cp, dm being nonpair-yielding FinSequence holds InputVertices (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)))) = {(GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))}
proof end;

LmT1C2s: for k being Nat
for ap, bm, cp, dm being nonpair-yielding FinSequence
for s being State of (BitGFA2Circ ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)))) holds Following (s,2) is stable
proof end;

LmT1Cin0In: for n being Nat
for ap, bm, cp, dm being FinSequence holds [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] in InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm))
proof end;

LmT1WnI: for n being Nat
for ap, bm, cp, dm being nonpair-yielding FinSequence
for u, v, x being non pair set holds
( not GFA1AdderOutput (u,v,x) in InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm)) & not GFA1CarryOutput (u,v,x) in InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm)) )
proof end;

LmT1InAcc: for n being Nat
for ap, bm, cp, dm being nonpair-yielding FinSequence
for w being set holds
( not w in InputVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm)) or not w is pair or ex u, v, x being non pair set st w = GFA1AdderOutput (u,v,x) or ex u, v, x being non pair set st w = GFA1CarryOutput (u,v,x) )
proof end;

LmT1Dj1: for k being Nat
for ap, bm, cp, dm being nonpair-yielding FinSequence holds InputVertices (k -BitFTA1Layer2Str (ap,bm,cp,dm)) misses InnerVertices (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))))
proof end;

LmT1Dj2: for m being Nat
for ap, bm, cp, dm being nonpair-yielding FinSequence holds InputVertices (BitGFA2Str ((GFA1AdderOutput ((ap . ((m + 1) + 1)),(bm . ((m + 1) + 1)),(cp . ((m + 1) + 1)))),((m + 1) -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . ((m + 1) + 1)))) misses InnerVertices ((m + 1) -BitFTA1Layer2Str (ap,bm,cp,dm))
proof end;

:: Layer 2 stabilizes in 2 steps from any state where the FALSE
:: base output vertex is already settled. The k = 0 cell composes
:: by cascade with n1 = 0 (the settled base is already stable);
:: later cells compose in parallel.
theorem Th20: :: FTACELL2:20
for n being Nat
for ap, bm, cp, dm being nonpair-yielding FinSequence
for s being State of (n -BitFTA1Layer2Circ (ap,bm,cp,dm)) st s . [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] = FALSE holds
Following (s,2) is stable
proof end;

::--------------------------------
:: Stability of n-depth FTA Circuit (TYPE-1)
::--------------------------------
theorem :: FTACELL2:21
for n being Nat
for ap, bm, cp, dm being nonpair-yielding FinSeqLen of n
for s being State of (n -BitFTA1Circ (ap,bm,cp,dm)) holds Following (s,4) is stable
proof end;