:: Stability of Parallel 4-2 Compressor Circuits
:: by Katsumi Wasaki
::
:: Received November 5, 2026
:: Copyright (c) 2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 4.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/4.0/.
environ
vocabularies NUMBERS, NAT_1, FINSEQ_1, CIRCCOMB, CARD_1, FINSEQ_2, MARGREL1,
FUNCOP_1, XBOOLEAN, STRUCT_0, XBOOLE_0, MSUALG_1, PBOOLE, FUNCT_1,
ARYTM_3, FUNCT_4, GFACIRC1, LATTICES, CIRCUIT1, RELAT_1, SUBSET_1,
MSAFREE2, XXREAL_0, FACIRC_1, TWOSCOMP, FSM_1, CIRCUIT2, FTACELL1,
FTACELL2, PARTFUN1;
notations TARSKI, XBOOLE_0, ENUMSET1, XTUPLE_0, SUBSET_1, XCMPLX_0, RELAT_1,
CARD_1, STRUCT_0, FUNCT_1, FUNCT_2, FINSEQ_1, FUNCOP_1, FINSEQ_2, PBOOLE,
FUNCT_4, CARD_3, FUNCT_7, ORDINAL1, NAT_1, MARGREL1, MSUALG_1, MSAFREE2,
CIRCUIT1, CIRCUIT2, CIRCCOMB, FACIRC_1, TWOSCOMP, FACIRC_2, GFACIRC1,
FTACELL1, PARTFUN1, NUMBERS, XXREAL_0;
constructors ENUMSET1, CIRCCOMB, CIRCUIT1, CIRCUIT2, FACIRC_1, TWOSCOMP,
GFACIRC1, FTACELL1, PARTFUN1, FUNCT_4, CARD_3, XREAL_0, RELSET_1,
XTUPLE_0, XCMPLX_0, XXREAL_0, NAT_1, NUMBERS, FUNCT_7, XFAMILY, FUNCT_1,
BINARITH;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, NAT_1, FINSEQ_1,
MARGREL1, STRUCT_0, CIRCCOMB, FACIRC_1, CIRCCMB2, FACIRC_2, MSAFREE2,
FINSET_1, CARD_1, XTUPLE_0, CARD_3;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions FACIRC_1, FUNCT_1, XTUPLE_0, CIRCUIT1, CIRCUIT2, MSAFREE2,
XBOOLE_0;
equalities MARGREL1, GFACIRC1, FTACELL1, FACIRC_1;
theorems TARSKI, ENUMSET1, NAT_1, PBOOLE, XBOOLE_0, FUNCOP_1, FINSEQ_1,
CIRCCOMB, FACIRC_1, CIRCCMB2, GFACIRC1, PARTFUN1, FUNCT_4, FUNCT_1,
XTUPLE_0, CIRCUIT1, CIRCUIT2, MSAFREE2, TWOSCOMP, XBOOLEAN;
schemes NAT_1, CIRCCMB2;
begin :: 1. Stability of a Parallel 4-2 Compressor Circuit (TYPE-0)
::------------------------------------------------
:: 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 gate`1=arity gate`2isBoolean non void non empty strict;
func n-BitFTA0Str(ap,bp,cp,dp) ->
unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign means
:Def1:
ex f,h being ManySortedSet of NAT st
it = f.n & f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) &
h.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE] &
for n being Nat, S being non empty ManySortedSign, z be 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
proof
deffunc S(non empty ManySortedSign, set, Nat)
= $1 +* BitFTA0Str(ap.($3+1), bp.($3+1), cp.($3+1), dp.($3+1), $2);
deffunc o(set, Nat)
= BitFTA0CarryOutput(ap.($2+1), bp.($2+1), cp.($2+1), dp.($2+1), $1);
for S1,S2 being unsplit gate`1=arity gate`2isBoolean non void non empty
strict non empty ManySortedSign st
(ex f,h being ManySortedSet of NAT st S1 = f.n & f.0 = S0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)) &
(ex f,h being ManySortedSet of NAT st S2 = f.n & f.0 = S0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n))
holds S1 = S2 from CIRCCMB2:sch 9;
hence thesis;
end;
existence
proof
deffunc S(set, Nat)
= BitFTA0Str(ap.($2+1), bp.($2+1), cp.($2+1), dp.($2+1), $1);
deffunc o(set, Nat)
= BitFTA0CarryOutput(ap.($2+1), bp.($2+1), cp.($2+1), dp.($2+1), $1);
ex S being unsplit gate`1=arity gate`2isBoolean
non void non empty non empty strict ManySortedSign,
f,h being ManySortedSet of NAT st S = f.n & f.0 = S0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = h.n
holds f.(n+1) = S +* S(x,n) & h.(n+1) = o(x,n) from CIRCCMB2:sch 8(A1);
hence thesis;
end;
end;
:: 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) ->
Boolean gate`2=den strict Circuit of n-BitFTA0Str(ap,bp,cp,dp) means
:Def2:
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, S being non empty ManySortedSign,
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
proof
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set A0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set Sn = n-BitFTA0Str(ap,bp,cp,dp);
set o0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
deffunc S(non empty ManySortedSign, set, Nat)
= $1 +* BitFTA0Str(ap.($3+1), bp.($3+1), cp.($3+1), dp.($3+1), $2);
deffunc A(non empty ManySortedSign, non-empty MSAlgebra over $1,
set, Nat)
= $2 +* BitFTA0Circ(ap.($4+1), bp.($4+1), cp.($4+1), dp.($4+1), $3);
deffunc o(set, Nat)
= BitFTA0CarryOutput(ap.($2+1), bp.($2+1), cp.($2+1), dp.($2+1), $1);
A1: for S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set, n being Nat holds
A(S,A,x,n) is non-empty MSAlgebra over S(S,x,n);
for A1,A2 being Boolean gate`2=den strict Circuit of Sn st
(ex f,g,h being ManySortedSet of NAT st Sn= f.n & A1 = g.n &
f.0 = S0 & g.0 = A0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set st S = f.n & A = g.n & x = h.n
holds f.(n+1) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x,n)) &
(ex f,g,h being ManySortedSet of NAT st Sn = f.n & A2 = g.n &
f.0 = S0 & g.0 = A0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set st S = f.n & A = g.n & x = h.n
holds f.(n+1) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x,n))
holds A1 = A2 from CIRCCMB2:sch 21(A1);
hence thesis;
end;
existence
proof
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set A0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set Sn = n-BitFTA0Str(ap,bp,cp,dp);
set o0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
deffunc S(non empty ManySortedSign, set, Nat)
= $1 +* BitFTA0Str(ap.($3+1), bp.($3+1), cp.($3+1), dp.($3+1), $2);
deffunc A(non empty ManySortedSign, non-empty MSAlgebra over $1,
set, Nat)
= $2 +* BitFTA0Circ(ap.($4+1), bp.($4+1), cp.($4+1), dp.($4+1), $3);
deffunc o(set, Nat)
= BitFTA0CarryOutput(ap.($2+1), bp.($2+1), cp.($2+1), dp.($2+1), $1);
A2: for S being unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign, x being set, n being Nat holds
S(S,x,n) is unsplit gate`1=arity gate`2isBoolean non void strict;
A3: ex f,h being ManySortedSet of NAT st Sn = f.n & f.0 = S0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n) by Def1;
A4: for S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set, n being Nat holds
A(S,A,x,n) is non-empty MSAlgebra over S(S,x,n);
A5: for S,S1 being unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign, A being Boolean gate`2=den strict Circuit of S
for x being set, n being Nat st S1 = S(S,x,n) holds
A(S,A,x,n) is Boolean gate`2=den strict Circuit of S1;
ex A being Boolean gate`2=den strict Circuit of Sn,
f,g,h being ManySortedSet of NAT st Sn = f.n & A = g.n &
f.0 = S0 & g.0 = A0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set st S = f.n & A = g.n & x = h.n
holds f.(n+1) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x,n)
from CIRCCMB2:sch 19(A2,A3,A4,A5);
hence thesis;
end;
end;
:: 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:
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
proof
set o0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
deffunc o(Nat,set)
= BitFTA0CarryOutput(ap.($1+1), bp.($1+1), cp.($1+1), dp.($1+1), $2);
let o1, o2 be Element of InnerVertices (n-BitFTA0Str(ap,bp,cp,dp));
given h1 being ManySortedSet of NAT such that
A1: o1 = h1.n and
A2: h1.0 = o0 and
A3: for n being Nat holds h1.(n+1) = o(n,h1.n);
given h2 being ManySortedSet of NAT such that
A4: o2 = h2.n and
A5: h2.0 = o0 and
A6: for n being Nat holds h2.(n+1) = o(n,h2.n);
A7: dom h1 = NAT by PARTFUN1:def 2;
A8: dom h2 = NAT by PARTFUN1:def 2;
h1 = h2 from NAT_1:sch 15(A7,A2,A3,A8,A5,A6);
hence thesis by A1,A4;
end;
existence
proof
defpred P[set,set,set] means not contradiction;
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set Sn = n-BitFTA0Str(ap,bp,cp,dp);
set o0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
deffunc S(non empty ManySortedSign, set, Nat)
= $1 +* BitFTA0Str(ap.($3+1), bp.($3+1), cp.($3+1), dp.($3+1), $2);
deffunc o(set, Nat)
= BitFTA0CarryOutput(ap.($2+1), bp.($2+1), cp.($2+1), dp.($2+1), $1);
consider f,g being ManySortedSet of NAT such that
A9: Sn = f.n and
A10: f.0 = S0 and
A11: g.0 = o0 and
A12: for n being Nat, S being non empty ManySortedSign, z be set
st S = f.n & z = g.n holds f.(n+1) = S(S,z,n) & g.(n+1) = o(z,n) by Def1;
defpred P[Nat] means ex S being non empty ManySortedSign
st S = f.$1 & g.$1 in InnerVertices S;
InnerVertices S0 = {o0} by CIRCCOMB:42;
then o0 in InnerVertices S0 by TARSKI:def 1;
then
A13: P[ 0 ] by A10,A11;
A14: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat such that
A15: ex S being non empty ManySortedSign
st S = f.i & g.i in InnerVertices S and
A16: for S being non empty ManySortedSign
st S = f.(i+1) holds not g.(i+1) in InnerVertices S;
consider S being non empty ManySortedSign such that
A17: S = f.i and g.i in InnerVertices S by A15;
A18: BitFTA0CarryOutput(ap.(i+1), bp.(i+1), cp.(i+1), dp.(i+1), g.i) in
InnerVertices
(S +* BitFTA0Str(ap.(i+1), bp.(i+1), cp.(i+1), dp.(i+1), g.i))
by FACIRC_1:22;
A19: f.(i+1)
= S +* BitFTA0Str(ap.(i+1), bp.(i+1), cp.(i+1), dp.(i+1), g.i)
by A12,A17;
g.(i+1) = BitFTA0CarryOutput(ap.(i+1), bp.(i+1), cp.(i+1), dp.(i+1), g.i)
by A12,A17;
hence contradiction by A16,A18,A19;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A13,A14);
then ex S being non empty ManySortedSign
st S = f.n & g.n in InnerVertices S;
then reconsider o = g.n as Element of InnerVertices Sn by A9;
take o, g;
thus o = g.n & g.0 = o0 by A11;
let i be Nat;
A20: ex S being non empty ManySortedSign, x being set
st S = f.0 & x = g.0 & P[S, x, 0] by A10;
A21: for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = g.n & P[S, x, n] holds P[S(S,x,n), o(x, n), n+1];
for n being Nat ex S being non empty ManySortedSign
st S = f.n & P[S,g.n,n] from CIRCCMB2:sch 2(A20,A12,A21);
then ex S being non empty ManySortedSign st S = f.i;
hence thesis by A12;
end;
end;
::-----------------------------------------------
:: 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:
for ap,bp,cp,dp being FinSequence, 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, S being non empty ManySortedSign,
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)
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
let ap,bp,cp,dp be FinSequence, f,g,h be ManySortedSet of NAT;
set f0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set g0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set h0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
deffunc S(non empty ManySortedSign,set,Nat)
= $1 +* BitFTA0Str(ap.($3+1),bp.($3+1),cp.($3+1),dp.($3+1), $2);
deffunc A(non empty ManySortedSign,non-empty MSAlgebra over $1,
set, Nat) = $2 +* BitFTA0Circ(ap.($4+1),bp.($4+1),cp.($4+1),dp.($4+1), $3);
deffunc o(set, Nat) = BitFTA0CarryOutput(ap.($2+1),bp.($2+1),cp.($2+1),
dp.($2+1), $1);
deffunc F(Nat, set) = BitFTA0CarryOutput(ap.($1+1),bp.($1+1),cp.($1+1),
dp.($1+1), $2);
assume that
A1: f.0 = f0 & g.0 = g0 and
A2: h.0 = h0 and
A3: for n being Nat, S being non empty ManySortedSign,
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(S,z,n) &
g.(n+1) = A(S,A,z,n) & h.(n+1) = o(z,n);
let n be Nat;
consider f1,g1,h1 being ManySortedSet of NAT such that
A4: n-BitFTA0Str(ap,bp,cp,dp) = f1.n and
A5: n-BitFTA0Circ(ap,bp,cp,dp) = g1.n and
A6: f1.0 = f0 and
A7: g1.0 = g0 and
A8: h1.0 = h0 and
A9: for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for z being set st S = f1.n & A = g1.n & z = h1.n holds
f1.(n+1) = S(S,z,n) & g1.(n+1) = A(S,A,z,n) & h1.(n+1) = o(z,n) by Def2;
A10: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
st S = f.0 & A = g.0 by A1;
A11: f.0 = f1.0 & g.0 = g1.0 & h.0 = h1.0 by A1,A2,A6,A7,A8;
A12: for S being non empty ManySortedSign, A being non-empty MSAlgebra over S
for z being set, n being Nat holds
A(S,A,z,n) is non-empty MSAlgebra over S(S,z,n);
f = f1 & g = g1 & h = h1 from CIRCCMB2:sch 14(A10,A11,A3,A9,A12);
hence n-BitFTA0Str(ap,bp,cp,dp) = f.n & n-BitFTA0Circ(ap,bp,cp,dp) = g.n
by A4,A5;
A13: for n being Nat, S being non empty ManySortedSign, z being set
st S = f.n & z = h.n holds f.(n+1) = S(S,z,n) &
h.(n+1) = o(z,n) from CIRCCMB2:sch 15(A1,A3,A12);
A14: f.0 = f0 by A1;
A15: dom h = NAT by PARTFUN1:def 2;
A16: h.0 = h0 by A2;
for n being Nat, z being set st z = h.n
holds h.(n+1) = o(z,n) from CIRCCMB2:sch 3(A14,A13);
then
A17: for n being Nat holds h.(n+1) = F(n,h.n);
consider h1 being ManySortedSet of NAT such that
A18: n-BitFTA0CarryOutput(ap,bp,cp,dp) = h1.n and
A19: h1.0 = h0 and
A20: for n being Nat holds h1.(n+1) = BitFTA0CarryOutput(ap.(n+1),bp.(n+1),
cp.(n+1),dp.(n+1), h1.n) by Def3;
A21: dom h1 = NAT by PARTFUN1:def 2;
A22: h1.0 = h0 by A19;
A23: for n being Nat holds h1.(n+1) = F(n,h1.n) by A20;
h = h1 from NAT_1:sch 15(A15,A16,A17,A21,A22,A23);
hence thesis by A18;
end;
:: Base case: the 0-bit structure, circuit and carry are all the FALSE
:: constant gate (resp. its algebra / output vertex).
theorem Th2:
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
let ap,bp,cp,dp be FinSequence;
set f0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set g0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set h0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
A1: ex f,g,h being ManySortedSet of NAT st (0-BitFTA0Str(ap,bp,cp,dp) = f.0)
& (0-BitFTA0Circ(ap,bp,cp,dp) = g.0)
& (f.0 = f0) & (g.0 = g0) & (h.0 = h0) & (
for n being Nat, S being non empty ManySortedSign, 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)) by Def2;
hence 0-BitFTA0Str(ap,bp,cp,dp) = f0;
thus 0-BitFTA0Circ(ap,bp,cp,dp) = g0 by A1;
InnerVertices (0-BitFTA0Str(ap,bp,cp,dp)) = { h0 } by A1,CIRCCOMB:42;
hence thesis by TARSKI:def 1;
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:
for n be 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
set f0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set g0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set h0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
let n be Nat;
let ap,bp,cp,dp be FinSequence;
consider f,g,h being ManySortedSet of NAT such that
A1: n-BitFTA0Str(ap,bp,cp,dp) = f.n and
A2: n-BitFTA0Circ(ap,bp,cp,dp) = g.n and
A3: f.0 = f0 and
A4: g.0 = g0 and
A5: h.0 = h0 and
A6: for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for z be 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) by Def2;
A7: n-BitFTA0CarryOutput(ap,bp,cp,dp) = h.n by A3,A4,A5,A6,Th1;
A8: (n+1)-BitFTA0Str(ap,bp,cp,dp) = f.(n+1) by A3,A4,A5,A6,Th1;
A9: (n+1)-BitFTA0Circ(ap,bp,cp,dp) = g.(n+1) by A3,A4,A5,A6,Th1;
(n+1)-BitFTA0CarryOutput(ap,bp,cp,dp) = h.(n+1) by A3,A4,A5,A6,Th1;
hence thesis by A1,A2,A6,A7,A8,A9;
end;
::--------------------------------
:: Carry Output Stabilizes at 2 Steps (independent of Carry-in)
::--------------------------------
:: Cell disjointness: the primary (non-pair) inputs of one BitGFA0 cell
:: miss the internal gate vertices of any other BitGFA0 cell.
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
let ap,bp,cp be non pair set;
let x,y,z be set;
InputVertices BitGFA0Str(ap,bp,cp) is without_pairs by GFACIRC1:35;
hence thesis by FACIRC_1:5,GFACIRC1:32;
end;
:: The carry output remains stable from T=2 onward.
theorem :: Th4
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
let ap,bp,cp be non pair set;
let dp,cin be set;
let s be State of BitFTA0Circ(ap,bp,cp,dp,cin);
let k be Nat;
assume
A1: k >= 2;
set S1 = BitGFA0Str(ap,bp,cp);
set C1 = BitGFA0Circ(ap,bp,cp);
set A1v = GFA0AdderOutput(ap,bp,cp);
set S2 = BitGFA0Str(A1v,cin,dp);
set C2 = BitGFA0Circ(A1v,cin,dp);
set A2v = GFA0CarryOutput(ap,bp,cp);
reconsider s1 = s|the carrier of S1 as State of C1 by FACIRC_1:26;
reconsider t = s as State of C1+*C2;
A2: InputVertices S1 misses InnerVertices S2 by LmT01;
A6: Following(t,2).A2v = Following(s1,2).A2v by A2,GFACIRC1:36,FACIRC_1:32;
A7: Following(s1,k) = Following(s1,2) by A1,GFACIRC1:40,CIRCCMB2:4;
thus thesis by A2,GFACIRC1:36,FACIRC_1:32,A6,A7;
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) ->
unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign means
:Def4:
ex f being ManySortedSet of NAT st
it = f.n & f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) &
for k being Nat, 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
proof
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set h = EmptyMS NAT;
deffunc SG(non empty ManySortedSign, set, Nat)
= $1 +* BitGFA0Str(ap.($3+1), bp.($3+1), cp.($3+1));
deffunc oo(set, Nat) = {};
let S1,S2 be unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign;
given f1 being ManySortedSet of NAT such that
E1: S1 = f1.n and E2: f1.0 = S0 and
E3: for k being Nat, S being non empty ManySortedSign st S = f1.k
holds f1.(k+1) = S +* BitGFA0Str(ap.(k+1), bp.(k+1), cp.(k+1));
given f2 being ManySortedSet of NAT such that
E4: S2 = f2.n and E5: f2.0 = S0 and
E6: for k being Nat, S being non empty ManySortedSign st S = f2.k
holds f2.(k+1) = S +* BitGFA0Str(ap.(k+1), bp.(k+1), cp.(k+1));
P1: ex f,hh being ManySortedSet of NAT st S1 = f.n & f.0 = S0 &
hh.0 = {} & for m being Nat, S being non empty ManySortedSign, x being set
st S = f.m & x = hh.m holds f.(m+1) = SG(S,x,m) & hh.(m+1) = oo(x,m)
proof
take f1, h;
thus S1 = f1.n & f1.0 = S0 & h.0 = {} by E1,E2,PBOOLE:5;
let m be Nat, S be non empty ManySortedSign, x be set;
assume that H1: S = f1.m and x = h.m;
thus f1.(m+1) = SG(S,x,m) by E3,H1;
thus h.(m+1) = oo(x,m) by PBOOLE:5;
end;
P2: ex f,hh being ManySortedSet of NAT st S2 = f.n & f.0 = S0 &
hh.0 = {} & for m being Nat, S being non empty ManySortedSign, x being set
st S = f.m & x = hh.m holds f.(m+1) = SG(S,x,m) & hh.(m+1) = oo(x,m)
proof
take f2, h;
thus S2 = f2.n & f2.0 = S0 & h.0 = {} by E4,E5,PBOOLE:5;
let m be Nat, S be non empty ManySortedSign, x be set;
assume that H2: S = f2.m and x = h.m;
thus f2.(m+1) = SG(S,x,m) by E6,H2;
thus h.(m+1) = oo(x,m) by PBOOLE:5;
end;
for T1,T2 being unsplit gate`1=arity gate`2isBoolean non void non empty
strict non empty ManySortedSign st
(ex f,hh being ManySortedSet of NAT st T1 = f.n & f.0 = S0 & hh.0 = {} &
for m being Nat, S being non empty ManySortedSign, x being set
st S = f.m & x = hh.m holds f.(m+1) = SG(S,x,m) & hh.(m+1) = oo(x,m)) &
(ex f,hh being ManySortedSet of NAT st T2 = f.n & f.0 = S0 & hh.0 = {} &
for m being Nat, S being non empty ManySortedSign, x being set
st S = f.m & x = hh.m holds f.(m+1) = SG(S,x,m) & hh.(m+1) = oo(x,m))
holds T1 = T2 from CIRCCMB2:sch 9;
hence S1 = S2 by P1,P2;
end;
existence
proof
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
A1: 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE)
is unsplit gate`1=arity gate`2isBoolean non void non empty strict;
deffunc SG(set, Nat) = BitGFA0Str(ap.($2+1), bp.($2+1), cp.($2+1));
deffunc oo(set, Nat) = {};
consider SX being unsplit gate`1=arity gate`2isBoolean
non void non empty non empty strict ManySortedSign,
f,h being ManySortedSet of NAT such that
B1: SX = f.n & f.0 = S0 & h.0 = {} &
for m being Nat, S being non empty ManySortedSign, x being set
st S = f.m & x = h.m
holds f.(m+1) = S +* SG(x,m) & h.(m+1) = oo(x,m) from CIRCCMB2:sch 8(A1);
take SX, f;
thus SX = f.n by B1;
thus f.0 = S0 by B1;
let k be Nat, S be non empty ManySortedSign;
assume B2: S = f.k;
h.k = h.k;
hence thesis by B1,B2;
end;
end;
:: 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) ->
Boolean gate`2=den strict Circuit of n-BitFTA0Layer1Str(ap,bp,cp) means
:Def5:
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, S being non empty ManySortedSign,
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
proof
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set A0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set Sn = n-BitFTA0Layer1Str(ap,bp,cp);
set h = EmptyMS NAT;
deffunc SG(non empty ManySortedSign, set, Nat)
= $1 +* BitGFA0Str(ap.($3+1), bp.($3+1), cp.($3+1));
deffunc AG(non empty ManySortedSign, non-empty MSAlgebra over $1,
set, Nat) = $2 +* BitGFA0Circ(ap.($4+1), bp.($4+1), cp.($4+1));
deffunc oo(set, Nat) = {};
Q1: for S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set, m being Nat holds
AG(S,A,x,m) is non-empty MSAlgebra over SG(S,x,m);
let AA1,AA2 be Boolean gate`2=den strict Circuit of Sn;
given f1,g1 being ManySortedSet of NAT such that
E1: Sn = f1.n and E1b: AA1 = g1.n and E2: f1.0 = S0 and E2b: g1.0 = A0 and
E3: for k being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S st S = f1.k & A = g1.k holds
f1.(k+1) = S +* BitGFA0Str(ap.(k+1), bp.(k+1), cp.(k+1)) &
g1.(k+1) = A +* BitGFA0Circ(ap.(k+1), bp.(k+1), cp.(k+1));
given f2,g2 being ManySortedSet of NAT such that
E4: Sn = f2.n and E4b: AA2 = g2.n and E5: f2.0 = S0 and E5b: g2.0 = A0 and
E6: for k being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S st S = f2.k & A = g2.k holds
f2.(k+1) = S +* BitGFA0Str(ap.(k+1), bp.(k+1), cp.(k+1)) &
g2.(k+1) = A +* BitGFA0Circ(ap.(k+1), bp.(k+1), cp.(k+1));
P1: ex f,g,hh being ManySortedSet of NAT st Sn = f.n & AA1 = g.n &
f.0 = S0 & g.0 = A0 & hh.0 = {} &
for m being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set st S = f.m & A = g.m & x = hh.m
holds f.(m+1) = SG(S,x,m) & g.(m+1) = AG(S,A,x,m) & hh.(m+1) = oo(x,m)
proof
take f1,g1,h;
thus Sn = f1.n & AA1 = g1.n & f1.0 = S0 & g1.0 = A0 & h.0 = {}
by E1,E1b,E2,E2b,PBOOLE:5;
let m be Nat, S be non empty ManySortedSign;
let A be non-empty MSAlgebra over S, x be set;
assume that H1: S = f1.m & A = g1.m and x = h.m;
thus f1.(m+1) = SG(S,x,m) & g1.(m+1) = AG(S,A,x,m) by E3,H1;
thus h.(m+1) = oo(x,m) by PBOOLE:5;
end;
P2: ex f,g,hh being ManySortedSet of NAT st Sn = f.n & AA2 = g.n &
f.0 = S0 & g.0 = A0 & hh.0 = {} &
for m being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set st S = f.m & A = g.m & x = hh.m
holds f.(m+1) = SG(S,x,m) & g.(m+1) = AG(S,A,x,m) & hh.(m+1) = oo(x,m)
proof
take f2,g2,h;
thus Sn = f2.n & AA2 = g2.n & f2.0 = S0 & g2.0 = A0 & h.0 = {}
by E4,E4b,E5,E5b,PBOOLE:5;
let m be Nat, S be non empty ManySortedSign;
let A be non-empty MSAlgebra over S, x be set;
assume that H2: S = f2.m & A = g2.m and x = h.m;
thus f2.(m+1) = SG(S,x,m) & g2.(m+1) = AG(S,A,x,m) by E6,H2;
thus h.(m+1) = oo(x,m) by PBOOLE:5;
end;
for B1,B2 being Boolean gate`2=den strict Circuit of Sn st
(ex f,g,hh being ManySortedSet of NAT st Sn = f.n & B1 = g.n &
f.0 = S0 & g.0 = A0 & hh.0 = {} &
for m being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set st S = f.m & A = g.m & x = hh.m
holds f.(m+1) = SG(S,x,m) & g.(m+1) = AG(S,A,x,m) & hh.(m+1) = oo(x,m)) &
(ex f,g,hh being ManySortedSet of NAT st Sn = f.n & B2 = g.n &
f.0 = S0 & g.0 = A0 & hh.0 = {} &
for m being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set st S = f.m & A = g.m & x = hh.m
holds f.(m+1) = SG(S,x,m) & g.(m+1) = AG(S,A,x,m) & hh.(m+1) = oo(x,m))
holds B1 = B2 from CIRCCMB2:sch 21(Q1);
hence AA1 = AA2 by P1,P2;
end;
existence
proof
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set A0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set Sn = n-BitFTA0Layer1Str(ap,bp,cp);
set h = EmptyMS NAT;
deffunc SG(non empty ManySortedSign, set, Nat)
= $1 +* BitGFA0Str(ap.($3+1), bp.($3+1), cp.($3+1));
deffunc AG(non empty ManySortedSign, non-empty MSAlgebra over $1,
set, Nat) = $2 +* BitGFA0Circ(ap.($4+1), bp.($4+1), cp.($4+1));
deffunc oo(set, Nat) = {};
A2: for S being unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign, x being set, m being Nat holds
SG(S,x,m) is unsplit gate`1=arity gate`2isBoolean non void strict;
A3: ex f,hh being ManySortedSet of NAT st Sn = f.n & f.0 = S0 &
hh.0 = {} & for m being Nat, S being non empty ManySortedSign, x being set
st S = f.m & x = hh.m holds f.(m+1) = SG(S,x,m) & hh.(m+1) = oo(x,m)
proof
consider f being ManySortedSet of NAT such that
Q2: Sn = f.n and Q3: f.0 = S0 and
Q4: for k being Nat, S being non empty ManySortedSign st S = f.k
holds f.(k+1) = S +* BitGFA0Str(ap.(k+1), bp.(k+1), cp.(k+1)) by Def4;
take f, h;
thus Sn = f.n & f.0 = S0 & h.0 = {} by Q2,Q3,PBOOLE:5;
let m be Nat, S be non empty ManySortedSign, x be set;
assume that R1: S = f.m and x = h.m;
thus f.(m+1) = SG(S,x,m) by Q4,R1;
thus h.(m+1) = oo(x,m) by PBOOLE:5;
end;
A4: for S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set, m being Nat holds
AG(S,A,x,m) is non-empty MSAlgebra over SG(S,x,m);
A5: for S,S1 being unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign, A being Boolean gate`2=den strict Circuit of S
for x being set, m being Nat st S1 = SG(S,x,m) holds
AG(S,A,x,m) is Boolean gate`2=den strict Circuit of S1;
consider AA being Boolean gate`2=den strict Circuit of Sn,
f,g,hh being ManySortedSet of NAT such that
B1: Sn = f.n & AA = g.n & f.0 = S0 & g.0 = A0 & hh.0 = {} &
for m being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set st S = f.m & A = g.m & x = hh.m
holds f.(m+1) = SG(S,x,m) & g.(m+1) = AG(S,A,x,m) & hh.(m+1) = oo(x,m)
from CIRCCMB2:sch 19(A2,A3,A4,A5);
take AA, f, g;
thus Sn = f.n & AA = g.n & f.0 = S0 & g.0 = A0 by B1;
let k be Nat, S be non empty ManySortedSign;
let A be non-empty MSAlgebra over S;
assume that C1: S = f.k & A = g.k;
C3: hh.k = hh.k;
thus f.(k+1) = S +* BitGFA0Str(ap.(k+1), bp.(k+1), cp.(k+1)) by B1,C1,C3;
thus g.(k+1) = A +* BitGFA0Circ(ap.(k+1), bp.(k+1), cp.(k+1)) by B1,C1,C3;
end;
end;
:: 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) ->
unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign means
:Def6:
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, S being non empty ManySortedSign, 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
proof
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set o0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
deffunc S(non empty ManySortedSign, set, Nat)
= $1 +* BitGFA0Str(GFA0AdderOutput(ap.($3+1), bp.($3+1), cp.($3+1)),
$2, dp.($3+1));
deffunc o(set, Nat) = GFA0CarryOutput(ap.($2+1), bp.($2+1), cp.($2+1));
for S1,S2 being unsplit gate`1=arity gate`2isBoolean non void non empty
strict non empty ManySortedSign st
(ex f,h being ManySortedSet of NAT st S1 = f.n & f.0 = S0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)) &
(ex f,h being ManySortedSet of NAT st S2 = f.n & f.0 = S0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n))
holds S1 = S2 from CIRCCMB2:sch 9;
hence thesis;
end;
existence
proof
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set o0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
A1: 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE)
is unsplit gate`1=arity gate`2isBoolean non void non empty strict;
deffunc S(set, Nat)
= BitGFA0Str(GFA0AdderOutput(ap.($2+1), bp.($2+1), cp.($2+1)),
$1, dp.($2+1));
deffunc o(set, Nat) = GFA0CarryOutput(ap.($2+1), bp.($2+1), cp.($2+1));
ex S being unsplit gate`1=arity gate`2isBoolean
non void non empty non empty strict ManySortedSign,
f,h being ManySortedSet of NAT st S = f.n & f.0 = S0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = h.n
holds f.(n+1) = S +* S(x,n) & h.(n+1) = o(x,n) from CIRCCMB2:sch 8(A1);
hence thesis;
end;
end;
:: 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) ->
Boolean gate`2=den strict Circuit of n-BitFTA0Layer2Str(ap,bp,cp,dp)
means
:Def7:
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, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S, 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
proof
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set A0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set Sn = n-BitFTA0Layer2Str(ap,bp,cp,dp);
set o0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
deffunc S(non empty ManySortedSign, set, Nat)
= $1 +* BitGFA0Str(GFA0AdderOutput(ap.($3+1), bp.($3+1), cp.($3+1)),
$2, dp.($3+1));
deffunc A(non empty ManySortedSign, non-empty MSAlgebra over $1,
set, Nat)
= $2 +* BitGFA0Circ(GFA0AdderOutput(ap.($4+1), bp.($4+1), cp.($4+1)),
$3, dp.($4+1));
deffunc o(set, Nat) = GFA0CarryOutput(ap.($2+1), bp.($2+1), cp.($2+1));
A1: for S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set, n being Nat holds
A(S,A,x,n) is non-empty MSAlgebra over S(S,x,n);
for A1,A2 being Boolean gate`2=den strict Circuit of Sn st
(ex f,g,h being ManySortedSet of NAT st Sn= f.n & A1 = g.n &
f.0 = S0 & g.0 = A0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set st S = f.n & A = g.n & x = h.n
holds f.(n+1) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x,n)) &
(ex f,g,h being ManySortedSet of NAT st Sn = f.n & A2 = g.n &
f.0 = S0 & g.0 = A0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set st S = f.n & A = g.n & x = h.n
holds f.(n+1) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x,n))
holds A1 = A2 from CIRCCMB2:sch 21(A1);
hence thesis;
end;
existence
proof
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set A0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set Sn = n-BitFTA0Layer2Str(ap,bp,cp,dp);
set o0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
deffunc S(non empty ManySortedSign, set, Nat)
= $1 +* BitGFA0Str(GFA0AdderOutput(ap.($3+1), bp.($3+1), cp.($3+1)),
$2, dp.($3+1));
deffunc A(non empty ManySortedSign, non-empty MSAlgebra over $1,
set, Nat)
= $2 +* BitGFA0Circ(GFA0AdderOutput(ap.($4+1), bp.($4+1), cp.($4+1)),
$3, dp.($4+1));
deffunc o(set, Nat) = GFA0CarryOutput(ap.($2+1), bp.($2+1), cp.($2+1));
A2: for S being unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign, x being set, n being Nat holds
S(S,x,n) is unsplit gate`1=arity gate`2isBoolean non void strict;
A3: ex f,h being ManySortedSet of NAT st Sn = f.n & f.0 = S0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n) by Def6;
A4: for S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set, n being Nat holds
A(S,A,x,n) is non-empty MSAlgebra over S(S,x,n);
A5: for S,S1 being unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign, A being Boolean gate`2=den strict Circuit of S
for x being set, n being Nat st S1 = S(S,x,n) holds
A(S,A,x,n) is Boolean gate`2=den strict Circuit of S1;
ex A being Boolean gate`2=den strict Circuit of Sn,
f,g,h being ManySortedSet of NAT st Sn = f.n & A = g.n &
f.0 = S0 & g.0 = A0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set st S = f.n & A = g.n & x = h.n
holds f.(n+1) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x,n)
from CIRCCMB2:sch 19(A2,A3,A4,A5);
hence thesis;
end;
end;
::--------------------------------
:: Reassociation into Wavefront Layers (Path core, next stage)
::--------------------------------
:: Map-level four-piece rearrangement (FUNCT_4): the function-graph
:: identity underlying the circuit-level Circ reassociation.
LmF: for f1,f2,f3,f4 being Function st f2 tolerates f3 holds
(f1 +* f2) +* (f3 +* f4) = (f1 +* f3) +* (f2 +* f4)
proof
let f1,f2,f3,f4 be Function such that
A1: f2 tolerates f3;
(f1 +* f2) +* (f3 +* f4) = f1 +* (f2 +* (f3 +* f4)) by FUNCT_4:14
.= f1 +* ((f2 +* f3) +* f4) by FUNCT_4:14
.= f1 +* ((f3 +* f2) +* f4) by A1,FUNCT_4:34
.= f1 +* (f3 +* (f2 +* f4)) by FUNCT_4:14;
hence thesis by FUNCT_4:14;
end;
:: Reassociation theorem (core of the 1-layer approach; first stage)
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
let n be Nat;
let ap,bp,cp be FinSequence;
set s0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
deffunc SS(non empty ManySortedSign, set, Nat)
= $1 +* BitGFA0Str(ap.($3+1),bp.($3+1),cp.($3+1));
deffunc oo(set, Nat) = {};
consider f being ManySortedSet of NAT such that
A1: (n+1)-BitFTA0Layer1Str(ap,bp,cp) = f.(n+1) and
A2: f.0 = s0 and
A3: for k being Nat, S being non empty ManySortedSign st S = f.k
holds f.(k+1) = S +* BitGFA0Str(ap.(k+1),bp.(k+1),cp.(k+1)) by Def4;
set h = EmptyMS NAT;
defpred T[Nat] means f.$1 is unsplit gate`1=arity gate`2isBoolean non void
non empty strict non empty ManySortedSign;
A4: T[0] by A2;
A5: for k being Nat st T[k] holds T[k+1]
proof
let k be Nat;
assume T[k];
then reconsider S = f.k as unsplit gate`1=arity gate`2isBoolean non void
non empty strict non empty ManySortedSign;
f.(k+1) = S +* BitGFA0Str(ap.(k+1),bp.(k+1),cp.(k+1)) by A3;
hence thesis;
end;
A6: for k being Nat holds T[k] from NAT_1:sch 2(A4,A5);
A7: n-BitFTA0Layer1Str(ap,bp,cp) = f.n
proof
reconsider fn = f.n as unsplit gate`1=arity gate`2isBoolean non void
non empty strict non empty ManySortedSign by A6;
B1: ex ff,hh being ManySortedSet of NAT st fn = ff.n & ff.0 = s0 &
hh.0 = {} & for k being Nat, S being non empty ManySortedSign,
x being set st S = ff.k & x = hh.k
holds ff.(k+1) = SS(S,x,k) & hh.(k+1) = oo(x,k)
proof
take f,h;
thus fn = f.n & f.0 = s0 & h.0 = {} by A2,PBOOLE:5;
let k be Nat, S be non empty ManySortedSign, x be set;
assume that C1: S = f.k and x = h.k;
thus f.(k+1) = SS(S,x,k) by A3,C1;
thus h.(k+1) = oo(x,k) by PBOOLE:5;
end;
B2: ex ff,hh being ManySortedSet of NAT st
n-BitFTA0Layer1Str(ap,bp,cp) = ff.n & ff.0 = s0 &
hh.0 = {} & for k being Nat, S being non empty ManySortedSign,
x being set st S = ff.k & x = hh.k
holds ff.(k+1) = SS(S,x,k) & hh.(k+1) = oo(x,k)
proof
consider f2 being ManySortedSet of NAT such that
C1: n-BitFTA0Layer1Str(ap,bp,cp) = f2.n and
C2: f2.0 = s0 and
C3: for k being Nat, S being non empty ManySortedSign st S = f2.k
holds f2.(k+1) = S +* BitGFA0Str(ap.(k+1),bp.(k+1),cp.(k+1)) by Def4;
set h2 = EmptyMS NAT;
take f2,h2;
thus n-BitFTA0Layer1Str(ap,bp,cp) = f2.n & f2.0 = s0 & h2.0 = {}
by C1,C2,PBOOLE:5;
let k be Nat, S be non empty ManySortedSign, x be set;
assume that C4: S = f2.k and x = h2.k;
thus f2.(k+1) = SS(S,x,k) by C3,C4;
thus h2.(k+1) = oo(x,k) by PBOOLE:5;
end;
for S1,S2 being unsplit gate`1=arity gate`2isBoolean non void non empty
strict non empty ManySortedSign st
(ex ff,hh being ManySortedSet of NAT st S1 = ff.n & ff.0 = s0 &
hh.0 = {} & for k being Nat, S being non empty ManySortedSign,
x being set st S = ff.k & x = hh.k
holds ff.(k+1) = SS(S,x,k) & hh.(k+1) = oo(x,k)) &
(ex ff,hh being ManySortedSet of NAT st S2 = ff.n & ff.0 = s0 &
hh.0 = {} & for k being Nat, S being non empty ManySortedSign,
x being set st S = ff.k & x = hh.k
holds ff.(k+1) = SS(S,x,k) & hh.(k+1) = oo(x,k))
holds S1 = S2 from CIRCCMB2:sch 9;
hence thesis by B1,B2;
end;
thus thesis by A1,A3,A7;
end;
:: Layer-2 structure, one-step unfolding: the (n+1)-stage Layer-2
:: structure is the n-stage one composed with one more stage-2 cell
:: (a BitGFA0 fed the stage-1 adder output and the n-stage carry).
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
let n be Nat;
let ap,bp,cp,dp be FinSequence;
set s0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set h0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
deffunc SS(non empty ManySortedSign, set, Nat)
= $1 +* BitGFA0Str(GFA0AdderOutput(ap.($3+1),bp.($3+1),cp.($3+1)),
$2, dp.($3+1));
deffunc oo(set, Nat) = GFA0CarryOutput(ap.($2+1),bp.($2+1),cp.($2+1));
deffunc FC(Nat, set) = GFA0CarryOutput(ap.($1+1),bp.($1+1),cp.($1+1));
consider g,h being ManySortedSet of NAT such that
A1: (n+1)-BitFTA0Layer2Str(ap,bp,cp,dp) = g.(n+1) and
A2: g.0 = s0 and
A3: h.0 = h0 and
A4: for k being Nat, S being non empty ManySortedSign, 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)) by Def6;
defpred TT[Nat] means g.$1 is unsplit gate`1=arity gate`2isBoolean non void
non empty strict non empty ManySortedSign;
A5: TT[0] by A2;
A6: for k being Nat st TT[k] holds TT[k+1]
proof
let k be Nat;
assume TT[k];
then reconsider S = g.k as unsplit gate`1=arity gate`2isBoolean non void
non empty strict non empty ManySortedSign;
g.(k+1) = S +* BitGFA0Str(GFA0AdderOutput(ap.(k+1),bp.(k+1),cp.(k+1)),
h.k, dp.(k+1)) by A4;
hence thesis;
end;
A7: for k being Nat holds TT[k] from NAT_1:sch 2(A5,A6);
A8: for k being Nat holds h.(k+1) = FC(k,h.k)
proof
let k be Nat;
reconsider S = g.k as unsplit gate`1=arity gate`2isBoolean non void
non empty strict non empty ManySortedSign by A7;
reconsider z = h.k as set;
S = g.k & z = h.k;
hence thesis by A4;
end;
consider h3 being ManySortedSet of NAT such that
A9: n-BitFTA0CarryOutput(ap,bp,cp,dp) = h3.n and
A10: h3.0 = h0 and
A11: for k being Nat holds h3.(k+1) = BitFTA0CarryOutput(ap.(k+1),bp.(k+1),
cp.(k+1),dp.(k+1), h3.k) by Def3;
A12: for k being Nat holds h3.(k+1) = FC(k,h3.k)
proof
let k be Nat;
h3.(k+1) = BitFTA0CarryOutput(ap.(k+1),bp.(k+1),cp.(k+1),dp.(k+1),h3.k)
by A11
.= GFA0CarryOutput(ap.(k+1),bp.(k+1),cp.(k+1));
hence thesis;
end;
A13: dom h = NAT by PARTFUN1:def 2;
A14: dom h3 = NAT by PARTFUN1:def 2;
A15: h = h3 from NAT_1:sch 15(A13,A3,A8,A14,A10,A12);
A16: n-BitFTA0Layer2Str(ap,bp,cp,dp) = g.n
proof
reconsider gn = g.n as unsplit gate`1=arity gate`2isBoolean non void
non empty strict non empty ManySortedSign by A7;
gn = n-BitFTA0Layer2Str(ap,bp,cp,dp) by A2,A3,A4,Def6;
hence thesis;
end;
thus thesis by A1,A4,A15,A9,A16;
end;
:: Main proposition - Two-Layer Circuit Composition (Structure-level)
theorem Th5:
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
defpred R[Nat] means for ap,bp,cp,dp being FinSequence holds
$1-BitFTA0Str(ap,bp,cp,dp) = ($1-BitFTA0Layer1Str(ap,bp,cp))
+* ($1-BitFTA0Layer2Str(ap,bp,cp,dp));
A1: R[0]
proof
let ap,bp,cp,dp be FinSequence;
set s0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
consider f being ManySortedSet of NAT such that
B1: 0-BitFTA0Layer1Str(ap,bp,cp) = f.0 and B2: f.0 = s0 and
for k being Nat, S being non empty ManySortedSign st S = f.k
holds f.(k+1) = S +* BitGFA0Str(ap.(k+1),bp.(k+1),cp.(k+1)) by Def4;
consider g,h being ManySortedSet of NAT such that
B3: 0-BitFTA0Layer2Str(ap,bp,cp,dp) = g.0 and B4: g.0 = s0 and
h.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE] and
for k being Nat, S being non empty ManySortedSign, 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)) by Def6;
s0 +* s0
= s0 by CIRCCOMB:4;
hence thesis by B1,B2,B3,B4,Th2;
end;
A2: for k being Nat st R[k] holds R[k+1]
proof
let k be Nat;
assume B1: R[k];
let ap,bp,cp,dp be FinSequence;
set a = k-BitFTA0Layer1Str(ap,bp,cp);
set b = k-BitFTA0Layer2Str(ap,bp,cp,dp);
set s1 = BitGFA0Str(ap.(k+1),bp.(k+1),cp.(k+1));
set s2 = BitGFA0Str(GFA0AdderOutput(ap.(k+1),bp.(k+1),cp.(k+1)),
k-BitFTA0CarryOutput(ap,bp,cp,dp), dp.(k+1));
B2: k-BitFTA0Str(ap,bp,cp,dp) = a +* b by B1;
B3: BitFTA0Str(ap.(k+1),bp.(k+1),cp.(k+1),dp.(k+1),
k-BitFTA0CarryOutput(ap,bp,cp,dp)) = s1 +* s2;
B4: (k+1)-BitFTA0Str(ap,bp,cp,dp) = (a +* b) +* (s1 +* s2) by Th3,B2,B3;
B5: (k+1)-BitFTA0Layer2Str(ap,bp,cp,dp) = b +* s2 by LmT05B;
(a +* b) +* (s1 +* s2) = a +* (b +* (s1 +* s2)) by CIRCCOMB:6
.= a +* ((b +* s1) +* s2) by CIRCCOMB:6
.= a +* ((s1 +* b) +* s2) by FACIRC_1:23
.= a +* (s1 +* (b +* s2)) by CIRCCOMB:6
.= (a +* s1) +* (b +* s2) by CIRCCOMB:6;
hence thesis by B4,LmT05A,B5;
end;
for n being Nat holds R[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
:: Reassociation theorem (core of the 1-layer approach; first stage)
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
let n be Nat;
let ap,bp,cp be FinSequence;
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set A0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
deffunc SG(non empty ManySortedSign, set, Nat)
= $1 +* BitGFA0Str(ap.($3+1),bp.($3+1),cp.($3+1));
deffunc AG(non empty ManySortedSign, non-empty MSAlgebra over $1,
set, Nat) = $2 +* BitGFA0Circ(ap.($4+1),bp.($4+1),cp.($4+1));
deffunc oo(set, Nat) = {};
consider f1,g1 being ManySortedSet of NAT such that
A1: n-BitFTA0Layer1Str(ap,bp,cp) = f1.n and
A2: n-BitFTA0Layer1Circ(ap,bp,cp) = g1.n and
A3: f1.0 = S0 and A4: g1.0 = A0 and
A5: for k being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S st S = f1.k & A = g1.k holds
f1.(k+1) = S +* BitGFA0Str(ap.(k+1),bp.(k+1),cp.(k+1)) &
g1.(k+1) = A +* BitGFA0Circ(ap.(k+1),bp.(k+1),cp.(k+1)) by Def5;
consider f2,g2 being ManySortedSet of NAT such that
(n+1)-BitFTA0Layer1Str(ap,bp,cp) = f2.(n+1) and
A6: (n+1)-BitFTA0Layer1Circ(ap,bp,cp) = g2.(n+1) and
A7: f2.0 = S0 and A8: g2.0 = A0 and
A9: for k being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S st S = f2.k & A = g2.k holds
f2.(k+1) = S +* BitGFA0Str(ap.(k+1),bp.(k+1),cp.(k+1)) &
g2.(k+1) = A +* BitGFA0Circ(ap.(k+1),bp.(k+1),cp.(k+1)) by Def5;
set h1 = EmptyMS NAT, h2 = EmptyMS NAT;
A10: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
st S = f1.0 & A = g1.0 by A3,A4;
A11: f1.0 = f2.0 & g1.0 = g2.0 & h1.0 = h2.0 by A3,A4,A7,A8;
A12: for k being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S for x being set
st S = f1.k & A = g1.k & x = h1.k holds
f1.(k+1) = SG(S,x,k) & g1.(k+1) = AG(S,A,x,k) & h1.(k+1) = oo(x,k)
by A5,PBOOLE:5;
A13: for k being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S for x being set
st S = f2.k & A = g2.k & x = h2.k holds
f2.(k+1) = SG(S,x,k) & g2.(k+1) = AG(S,A,x,k) & h2.(k+1) = oo(x,k)
by A9,PBOOLE:5;
A14: for S being non empty ManySortedSign, A being non-empty MSAlgebra over S
for x being set, k being Nat holds
AG(S,A,x,k) is non-empty MSAlgebra over SG(S,x,k);
A15: f1 = f2 & g1 = g2 & h1 = h2 from CIRCCMB2:sch 14(A10,A11,A12,A13,A14);
thus thesis by A15,A6,A5,A1,A2;
end;
:: Layer-2 circuit, one-step unfolding: the Circ (MSAlgebra) counterpart
:: of LmT05B, unfolding the (n+1)-stage Layer-2 circuit by one stage-2 cell.
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
let n be Nat;
let ap,bp,cp,dp be FinSequence;
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set A0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set h0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
deffunc SG(non empty ManySortedSign, set, Nat)
= $1 +* BitGFA0Str(GFA0AdderOutput(ap.($3+1),bp.($3+1),cp.($3+1)),
$2, dp.($3+1));
deffunc AG(non empty ManySortedSign, non-empty MSAlgebra over $1,
set, Nat)
= $2 +* BitGFA0Circ(GFA0AdderOutput(ap.($4+1),bp.($4+1),cp.($4+1)),
$3, dp.($4+1));
deffunc oo(set, Nat) = GFA0CarryOutput(ap.($2+1),bp.($2+1),cp.($2+1));
deffunc FC(Nat, set) = GFA0CarryOutput(ap.($1+1),bp.($1+1),cp.($1+1));
consider f1,g1,h1 being ManySortedSet of NAT such that
A1: n-BitFTA0Layer2Str(ap,bp,cp,dp) = f1.n and
A2: n-BitFTA0Layer2Circ(ap,bp,cp,dp) = g1.n and
A3: f1.0 = S0 and A4: g1.0 = A0 and A5: h1.0 = h0 and
A6: for k being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S, z being set
st S = f1.k & A = g1.k & z = h1.k holds
f1.(k+1) = S +* BitGFA0Str(GFA0AdderOutput(ap.(k+1),bp.(k+1),cp.(k+1)),
z, dp.(k+1)) &
g1.(k+1) = A +* BitGFA0Circ(GFA0AdderOutput(ap.(k+1),bp.(k+1),cp.(k+1)),
z, dp.(k+1)) &
h1.(k+1) = GFA0CarryOutput(ap.(k+1),bp.(k+1),cp.(k+1)) by Def7;
consider f2,g2,h2 being ManySortedSet of NAT such that
(n+1)-BitFTA0Layer2Str(ap,bp,cp,dp) = f2.(n+1) and
A7: (n+1)-BitFTA0Layer2Circ(ap,bp,cp,dp) = g2.(n+1) and
A8: f2.0 = S0 and A9: g2.0 = A0 and A10: h2.0 = h0 and
A11: for k being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S, z being set
st S = f2.k & A = g2.k & z = h2.k holds
f2.(k+1) = S +* BitGFA0Str(GFA0AdderOutput(ap.(k+1),bp.(k+1),cp.(k+1)),
z, dp.(k+1)) &
g2.(k+1) = A +* BitGFA0Circ(GFA0AdderOutput(ap.(k+1),bp.(k+1),cp.(k+1)),
z, dp.(k+1)) &
h2.(k+1) = GFA0CarryOutput(ap.(k+1),bp.(k+1),cp.(k+1)) by Def7;
A12: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
st S = f1.0 & A = g1.0 by A3,A4;
A13: f1.0 = f2.0 & g1.0 = g2.0 & h1.0 = h2.0 by A3,A4,A5,A8,A9,A10;
A14: for k being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S for x being set
st S = f1.k & A = g1.k & x = h1.k holds
f1.(k+1) = SG(S,x,k) & g1.(k+1) = AG(S,A,x,k) & h1.(k+1) = oo(x,k)
by A6;
A15: for k being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S for x being set
st S = f2.k & A = g2.k & x = h2.k holds
f2.(k+1) = SG(S,x,k) & g2.(k+1) = AG(S,A,x,k) & h2.(k+1) = oo(x,k)
by A11;
A16: for S being non empty ManySortedSign, A being non-empty MSAlgebra over S
for x being set, k being Nat holds
AG(S,A,x,k) is non-empty MSAlgebra over SG(S,x,k);
A17: f1 = f2 & g1 = g2 & h1 = h2 from CIRCCMB2:sch 14(A12,A13,A14,A15,A16);
A18: f1.0 = S0 & g1.0 = A0 by A3,A4;
A19: for k being Nat, S being non empty ManySortedSign, z being set
st S = f1.k & z = h1.k holds f1.(k+1) = SG(S,z,k) &
h1.(k+1) = oo(z,k) from CIRCCMB2:sch 15(A18,A14,A16);
A20: for k being Nat, z being set st z = h1.k
holds h1.(k+1) = oo(z,k) from CIRCCMB2:sch 3(A3,A19);
A21: for k being Nat holds h1.(k+1) = FC(k,h1.k)
proof
let k be Nat;
h1.k = h1.k;
hence thesis by A20;
end;
consider h3 being ManySortedSet of NAT such that
A22: n-BitFTA0CarryOutput(ap,bp,cp,dp) = h3.n and
A23: h3.0 = h0 and
A24: for k being Nat holds h3.(k+1) = BitFTA0CarryOutput(ap.(k+1),bp.(k+1),
cp.(k+1),dp.(k+1), h3.k) by Def3;
A25: for k being Nat holds h3.(k+1) = FC(k,h3.k)
proof
let k be Nat;
h3.(k+1) = BitFTA0CarryOutput(ap.(k+1),bp.(k+1),cp.(k+1),dp.(k+1),h3.k)
by A24
.= GFA0CarryOutput(ap.(k+1),bp.(k+1),cp.(k+1));
hence thesis;
end;
A26: dom h1 = NAT by PARTFUN1:def 2;
A27: dom h3 = NAT by PARTFUN1:def 2;
A28: h1 = h3 from NAT_1:sch 15(A26,A5,A21,A27,A23,A25);
thus thesis by A17,A7,A6,A28,A22,A1,A2;
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:
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
let n be Nat;
let ap,bp,cp,dp be FinSequence;
set A0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
defpred P[Nat] means
$1-BitFTA0Circ(ap,bp,cp,dp) = ($1-BitFTA0Layer1Circ(ap,bp,cp))
+* ($1-BitFTA0Layer2Circ(ap,bp,cp,dp));
A1: P[0]
proof
B1: 0-BitFTA0Layer1Circ(ap,bp,cp) = A0
proof
consider f,g being ManySortedSet of NAT such that
0-BitFTA0Layer1Str(ap,bp,cp) = f.0 and
C1: 0-BitFTA0Layer1Circ(ap,bp,cp) = g.0 and
f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) and
C2: g.0 = A0 and
for k being Nat, S being non empty ManySortedSign,
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)) by Def5;
thus thesis by C1,C2;
end;
B2: 0-BitFTA0Layer2Circ(ap,bp,cp,dp) = A0
proof
consider f,g,h being ManySortedSet of NAT such that
0-BitFTA0Layer2Str(ap,bp,cp,dp) = f.0 and
C1: 0-BitFTA0Layer2Circ(ap,bp,cp,dp) = g.0 and
f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) and
C2: g.0 = A0 and h.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE] and
for k being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S, 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)) by Def7;
thus thesis by C1,C2;
end;
set sa = the Sorts of A0, ca = the Charact of A0;
B3: the Sorts of ((0-BitFTA0Layer1Circ(ap,bp,cp))
+* (0-BitFTA0Layer2Circ(ap,bp,cp,dp))) = the Sorts of A0
proof
the Sorts of ((0-BitFTA0Layer1Circ(ap,bp,cp))
+* (0-BitFTA0Layer2Circ(ap,bp,cp,dp)))
= sa +* sa by B1,B2,CIRCCOMB:def 4
.= sa;
hence thesis;
end;
the Charact of ((0-BitFTA0Layer1Circ(ap,bp,cp))
+* (0-BitFTA0Layer2Circ(ap,bp,cp,dp)))
= ca +* ca by B1,B2,CIRCCOMB:def 4
.= ca;
hence thesis by Th2,B3;
end;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that B1: P[k];
set Lk1 = k-BitFTA0Layer1Circ(ap,bp,cp);
set Lk2 = k-BitFTA0Layer2Circ(ap,bp,cp,dp);
set cc = k-BitFTA0CarryOutput(ap,bp,cp,dp);
set s1 = BitGFA0Circ(ap.(k+1),bp.(k+1),cp.(k+1));
set s2 = BitGFA0Circ(
GFA0AdderOutput(ap.(k+1),bp.(k+1),cp.(k+1)), cc, dp.(k+1));
set cell = BitFTA0Circ(ap.(k+1),bp.(k+1),cp.(k+1),dp.(k+1), cc);
B2: (k+1)-BitFTA0Circ(ap,bp,cp,dp) = (k-BitFTA0Circ(ap,bp,cp,dp)) +* cell
by Th3;
B3: (k+1)-BitFTA0Layer1Circ(ap,bp,cp) = Lk1 +* s1 by LmT06A;
B4: (k+1)-BitFTA0Layer2Circ(ap,bp,cp,dp) = Lk2 +* s2 by LmT06B;
set l1 = the Sorts of Lk1, l2 = the Sorts of Lk2;
set t1 = the Sorts of s1, t2 = the Sorts of s2;
set d1 = the Charact of Lk1, d2 = the Charact of Lk2;
set e1 = the Charact of s1, e2 = the Charact of s2;
B5: l1 tolerates l2 by CIRCCOMB:59;
B6: t1 tolerates t2 by CIRCCOMB:59;
B7: l1 tolerates t1 by CIRCCOMB:59;
B8: l2 tolerates t2 by CIRCCOMB:59;
B9: the Sorts of (k-BitFTA0Circ(ap,bp,cp,dp))
tolerates the Sorts of cell by CIRCCOMB:59;
B10: the Sorts of ((k+1)-BitFTA0Layer1Circ(ap,bp,cp))
tolerates the Sorts of ((k+1)-BitFTA0Layer2Circ(ap,bp,cp,dp))
by CIRCCOMB:59;
:: LHS: descend to map-level via Def4 FIRST, then substitute IH/CELL
:: (map +* is total so congruence holds); no rewrite through Circ +*.
B11: the Sorts of ((k+1)-BitFTA0Circ(ap,bp,cp,dp))
= (the Sorts of (Lk1 +* Lk2)) +* (the Sorts of (s1 +* s2)) by B1,B9,
CIRCCOMB:def 4,B2
.= (l1 +* l2) +* (the Sorts of (s1 +* s2)) by B5,CIRCCOMB:def 4
.= (l1 +* l2) +* (t1 +* t2) by B6,CIRCCOMB:def 4;
B12: the Sorts of (((k+1)-BitFTA0Layer1Circ(ap,bp,cp))
+* ((k+1)-BitFTA0Layer2Circ(ap,bp,cp,dp)))
= (the Sorts of (Lk1 +* s1)) +* (the Sorts of (Lk2 +* s2)) by B4,B3,B10,
CIRCCOMB:def 4
.= (l1 +* t1) +* (the Sorts of (Lk2 +* s2)) by B7,CIRCCOMB:def 4
.= (l1 +* t1) +* (l2 +* t2) by B8,CIRCCOMB:def 4;
B13: the Sorts of ((k+1)-BitFTA0Circ(ap,bp,cp,dp))
= the Sorts of (((k+1)-BitFTA0Layer1Circ(ap,bp,cp))
+* ((k+1)-BitFTA0Layer2Circ(ap,bp,cp,dp)))
by CIRCCOMB:59,LmF,B11,B12;
B14: the Charact of ((k+1)-BitFTA0Circ(ap,bp,cp,dp))
= (the Charact of (Lk1 +* Lk2)) +* (the Charact of (s1 +* s2)) by B1,B9,
CIRCCOMB:def 4,B2
.= (d1 +* d2) +* (the Charact of (s1 +* s2)) by B5,CIRCCOMB:def 4
.= (d1 +* d2) +* (e1 +* e2) by B6,CIRCCOMB:def 4;
B15: the Charact of (((k+1)-BitFTA0Layer1Circ(ap,bp,cp))
+* ((k+1)-BitFTA0Layer2Circ(ap,bp,cp,dp)))
= (the Charact of (Lk1 +* s1)) +* (the Charact of (Lk2 +* s2)) by B4,B3,
B10,CIRCCOMB:def 4
.= (d1 +* e1) +* (the Charact of (Lk2 +* s2)) by B7,CIRCCOMB:def 4
.= (d1 +* e1) +* (d2 +* e2) by B8,CIRCCOMB:def 4;
(d1 +* d2) +* (e1 +* e2) = (d1 +* e1) +* (d2 +* e2) by CIRCCOMB:48,LmF;
hence thesis by B13,B14,B15;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
::--------------------------------
:: Vertex structure of the wavefront layers (goal prerequisites)
::--------------------------------
:: Base values of the layer structures.
LmT00L1: for ap,bp,cp being FinSequence holds
0-BitFTA0Layer1Str(ap,bp,cp)
= 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE)
proof
let ap,bp,cp be FinSequence;
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
consider f being ManySortedSet of NAT such that
A1: 0-BitFTA0Layer1Str(ap,bp,cp) = f.0 and A2: f.0 = S0 and
for k being Nat, S being non empty ManySortedSign st S = f.k
holds f.(k+1) = S +* BitGFA0Str(ap.(k+1),bp.(k+1),cp.(k+1)) by Def4;
thus thesis by A1,A2;
end;
:: The 0-bit Layer-2 structure is the FALSE base gate.
LmT00L2: for ap,bp,cp,dp being FinSequence holds
0-BitFTA0Layer2Str(ap,bp,cp,dp)
= 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE)
proof
let ap,bp,cp,dp be FinSequence;
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
consider g,h being ManySortedSet of NAT such that
A1: 0-BitFTA0Layer2Str(ap,bp,cp,dp) = g.0 and A2: g.0 = S0 and
h.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE] and
for k being Nat, S being non empty ManySortedSign, 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))
by Def6;
thus thesis by A1,A2;
end;
:: InnerVertices of Layer 2 are all pairs (gate vertices + FALSE base output).
LmT0L2rel: for n being Nat for ap,bp,cp,dp being FinSequence holds
InnerVertices (n-BitFTA0Layer2Str(ap,bp,cp,dp)) is Relation
proof
let n be Nat;
let ap,bp,cp,dp be FinSequence;
deffunc S(Nat) = $1-BitFTA0Layer2Str(ap,bp,cp,dp);
defpred P[Nat] means InnerVertices (S($1)) is Relation;
S(0) = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) by LmT00L2;
then
A1: P[ 0 ] by FACIRC_1:38;
A2: now
let i be Nat;
assume B1: P[i];
B2: S(i+1) = S(i) +* BitGFA0Str(
GFA0AdderOutput(ap.(i+1),bp.(i+1),cp.(i+1)),
i-BitFTA0CarryOutput(ap,bp,cp,dp), dp.(i+1)) by LmT05B;
InnerVertices BitGFA0Str(
GFA0AdderOutput(ap.(i+1),bp.(i+1),cp.(i+1)),
i-BitFTA0CarryOutput(ap,bp,cp,dp), dp.(i+1)) is Relation by GFACIRC1:32;
hence P[i+1] by B1,B2,FACIRC_1:3;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
:: InputVertices of Layer 1 are all non-pairs (primary inputs only).
LmT0L1wp: for n being Nat for ap,bp,cp being nonpair-yielding FinSequence holds
InputVertices (n-BitFTA0Layer1Str(ap,bp,cp)) is without_pairs
proof
let n be Nat;
let ap,bp,cp be nonpair-yielding FinSequence;
deffunc S(Nat) = $1-BitFTA0Layer1Str(ap,bp,cp);
defpred P[Nat] means InputVertices (S($1)) is without_pairs;
S(0) = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) by LmT00L1;
then
A1: P[ 0 ] by FACIRC_1:39;
A2: now
let i be Nat;
assume B1: P[i];
set B = BitGFA0Str(ap.(i+1),bp.(i+1),cp.(i+1));
B2: S(i+1) = S(i) +* B by LmT05A;
reconsider w1 = InputVertices (S(i)) as without_pairs set by B1;
reconsider w2 = InputVertices B as without_pairs set by GFACIRC1:35;
InputVertices (S(i+1))
= (w1 \ InnerVertices B) \/ (w2 \ InnerVertices (S(i)))
by B2,CIRCCOMB:47,CIRCCMB2:5;
hence P[i+1];
end;
for i being Nat holds P[i] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
:: Feed-forward disjointness : Layer 1 inputs miss Layer 2 gates.
theorem Th7:
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
let n be Nat;
let ap,bp,cp,dp be nonpair-yielding FinSequence;
InputVertices (n-BitFTA0Layer1Str(ap,bp,cp)) is without_pairs by LmT0L1wp;
hence thesis by FACIRC_1:5,LmT0L2rel;
end;
::-----------------------------------------------------------
:: InnerVertices of Layer 1 are gate outputs (pairs) : a Relation.
::-----------------------------------------------------------
LmT0L1rel: for n being Nat for ap,bp,cp being FinSequence holds
InnerVertices (n-BitFTA0Layer1Str(ap,bp,cp)) is Relation
proof
let n be Nat;
let ap,bp,cp be FinSequence;
deffunc S(Nat) = $1-BitFTA0Layer1Str(ap,bp,cp);
defpred P[Nat] means InnerVertices (S($1)) is Relation;
S(0) = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) by LmT00L1;
then
A1: P[ 0 ] by FACIRC_1:38;
A2: now
let i be Nat;
assume B1: P[i];
B2: S(i+1) = S(i) +* BitGFA0Str(ap.(i+1),bp.(i+1),cp.(i+1)) by LmT05A;
InnerVertices BitGFA0Str(ap.(i+1),bp.(i+1),cp.(i+1)) is Relation
by GFACIRC1:32;
hence P[i+1] by B1,B2,FACIRC_1:3;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
:: Carry output is never a 2-input AND gate (first-component length differs).
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
let n be Nat;
let ap,bp,cp,dp be FinSequence;
let x,y be set;
consider h being ManySortedSet of NAT such that
A1: n-BitFTA0CarryOutput(ap,bp,cp,dp) = h.n and
A2: h.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE] and
A3: for k being Nat holds
h.(k+1) = BitFTA0CarryOutput(ap.(k+1),bp.(k+1),cp.(k+1),dp.(k+1),h.k)
by Def3;
assume A4: n-BitFTA0CarryOutput(ap,bp,cp,dp) = [<*x,y*>,and2];
per cases by NAT_1:6;
suppose n = 0;
hence contradiction by XTUPLE_0:1,A1,A2,A4;
end;
suppose ex m being Nat st n = m+1;
then consider m being Nat such that B1: n = m+1;
n-BitFTA0CarryOutput(ap,bp,cp,dp)
= BitFTA0CarryOutput(ap.(m+1),bp.(m+1),cp.(m+1),dp.(m+1),h.m)
by A1,A3,B1
.= [<*[<*ap.(m+1),bp.(m+1)*>,and2],[<*bp.(m+1),cp.(m+1)*>,and2],
[<*cp.(m+1),ap.(m+1)*>,and2]*>,or3];
then <*x,y*> = <*[<*ap.(m+1),bp.(m+1)*>,and2],[<*bp.(m+1),cp.(m+1)*>,and2],
[<*cp.(m+1),ap.(m+1)*>,and2]*> by XTUPLE_0:1,A4;
then len <*x,y*> = 3 by FINSEQ_1:45;
hence contradiction by FINSEQ_1:44;
end;
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:
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
let n be Nat;
let ap,bp,cp be nonpair-yielding FinSequence;
set A0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
defpred P[Nat] means
for s being State of $1-BitFTA0Layer1Circ(ap,bp,cp)
holds Following(s,2) is stable;
A1: 0-BitFTA0Layer1Circ(ap,bp,cp) = A0
proof
consider f,g being ManySortedSet of NAT such that
0-BitFTA0Layer1Str(ap,bp,cp) = f.0 and
B1: 0-BitFTA0Layer1Circ(ap,bp,cp) = g.0 and
f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) and
B2: g.0 = A0 and
for k being Nat, S being non empty ManySortedSign,
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)) by Def5;
thus thesis by B1,B2;
end;
A2: P[ 0 ]
proof
let s be State of 0-BitFTA0Layer1Circ(ap,bp,cp);
reconsider s0 = s as State of A0 by A1;
B1: Following(s0,1) = Following s0 by FACIRC_1:14;
B2: Following(s0,2) = Following(s0,1) by B1,CIRCCMB2:2,CIRCCMB2:4;
B3: 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE)
= 0-BitFTA0Layer1Str(ap,bp,cp) by LmT00L1;
thus thesis by B3,A1,B2,B1,CIRCCMB2:2;
end;
A3: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume B1: P[i];
reconsider S1 = i-BitFTA0Layer1Str(ap,bp,cp)
as non void Circuit-like non empty ManySortedSign;
set B = BitGFA0Str(ap.(i+1),bp.(i+1),cp.(i+1));
reconsider B as non void Circuit-like non empty ManySortedSign;
reconsider SS = (i+1)-BitFTA0Layer1Str(ap,bp,cp)
as non void Circuit-like non empty ManySortedSign;
reconsider A1a = i-BitFTA0Layer1Circ(ap,bp,cp)
as non-empty Circuit of S1;
reconsider Ba = BitGFA0Circ(ap.(i+1),bp.(i+1),cp.(i+1))
as non-empty Circuit of B;
reconsider AA = (i+1)-BitFTA0Layer1Circ(ap,bp,cp)
as non-empty Circuit of SS;
B2: AA = A1a +* Ba by LmT06A;
B3: A1a tolerates Ba by CIRCCOMB:60;
InputVertices S1 is without_pairs by LmT0L1wp;
then
B4: InputVertices S1 misses InnerVertices B by GFACIRC1:32,FACIRC_1:5;
InputVertices B is without_pairs by GFACIRC1:35;
then
B5: InputVertices B misses InnerVertices S1 by LmT0L1rel,FACIRC_1:5;
B6: for s being State of Ba holds Following(s,2) is stable
by GFACIRC1:40;
now
let s be State of AA;
C1: Following(s,2) is stable
proof
2 = max(2,2);
hence thesis by LmT05A,B2,B3,B4,B5,B1,B6,CIRCCMB2:24;
end;
thus Following(s,2) is stable by C1;
end;
hence P[i+1];
end;
for i being Nat holds P[i] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
:: Layer 2 inner vertices grow by the new stage-2 gates at each step.
:: Backbone for the disjointness reasoning inside Th10.
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
let n be Nat;
let ap,bp,cp,dp be FinSequence;
set B = BitGFA0Str(GFA0AdderOutput(ap.(n+1),bp.(n+1),cp.(n+1)),
n-BitFTA0CarryOutput(ap,bp,cp,dp), dp.(n+1));
reconsider S1 = n-BitFTA0Layer2Str(ap,bp,cp,dp) as unsplit gate`1=arity
gate`2isBoolean non void non empty strict non empty ManySortedSign;
thus InnerVertices ((n+1)-BitFTA0Layer2Str(ap,bp,cp,dp))
= InnerVertices (S1 +* B) by LmT05B
.= InnerVertices (n-BitFTA0Layer2Str(ap,bp,cp,dp))
\/ InnerVertices B by FACIRC_1:27;
end;
::-----------------------------------------------------------
:: Conditional 2-stability of Layer 2 (carry seed settled).
:: Layer 2 contains the FALSE base gate whose output vertex
:: [<*>,(0-tuples_on BOOLEAN)-->FALSE] feeds cell 1, so universal
:: 2-stability fails by one step. Once that vertex is settled at
:: FALSE (true of Following(s,2) in the full circuit), two more
:: steps stabilize the layer: the k = 0 cell composes by cascade
:: with n1 = 0 (CIRCCMB2:19) and later cells compose in parallel
:: (CIRCCMB2:22).
::-----------------------------------------------------------
:: The carry stream starts at the FALSE base output vertex.
LmT00CO: for ap,bp,cp,dp being FinSequence holds
0-BitFTA0CarryOutput(ap,bp,cp,dp) = [<*>,(0-tuples_on BOOLEAN)-->FALSE]
proof
let ap,bp,cp,dp be FinSequence;
consider h being ManySortedSet of NAT such that
A1: 0-BitFTA0CarryOutput(ap,bp,cp,dp) = h.0 and
A2: h.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE] and
for k being Nat holds
h.(k+1) = BitFTA0CarryOutput(ap.(k+1),bp.(k+1),cp.(k+1),dp.(k+1),h.k)
by Def3;
thus thesis by A1,A2;
end;
:: From index 1 on, the carry stream is the stage-1 carry output.
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
let m be Nat;
let ap,bp,cp,dp be FinSequence;
consider h being ManySortedSet of NAT such that
A1: (m+1)-BitFTA0CarryOutput(ap,bp,cp,dp) = h.(m+1) and
h.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE] and
A2: for k being Nat holds
h.(k+1) = BitFTA0CarryOutput(ap.(k+1),bp.(k+1),cp.(k+1),dp.(k+1),h.k)
by Def3;
thus (m+1)-BitFTA0CarryOutput(ap,bp,cp,dp)
= BitFTA0CarryOutput(ap.(m+1),bp.(m+1),cp.(m+1),dp.(m+1),h.m) by A1,A2
.= GFA0CarryOutput(ap.(m+1),bp.(m+1),cp.(m+1));
end;
:: The carry stream vertex is always a pair.
LmT0COp: for n being Nat for ap,bp,cp,dp being FinSequence holds
n-BitFTA0CarryOutput(ap,bp,cp,dp) is pair
proof
let n be Nat;
let ap,bp,cp,dp be FinSequence;
per cases by NAT_1:6;
suppose n = 0;
hence thesis by LmT00CO;
end;
suppose ex m being Nat st n = m+1;
then consider m being Nat such that B1: n = m+1;
n-BitFTA0CarryOutput(ap,bp,cp,dp)
= GFA0CarryOutput(ap.(m+1),bp.(m+1),cp.(m+1)) by B1,LmT0COk
.= [<*[<*ap.(m+1),bp.(m+1)*>,and2],[<*bp.(m+1),cp.(m+1)*>,and2],
[<*cp.(m+1),ap.(m+1)*>,and2]*>,or3];
hence thesis;
end;
end;
:: A stage-1 adder output never occurs among the gates of a
:: stage-2 cell whose middle input is a pair.
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
let a,b,c be non pair set;
let X,Y,d be set such that
A1: Y is pair;
set w = GFA0AdderOutput(a,b,c);
set bA = GFA0AdderOutput(X,Y,d), bC = GFA0CarryOutput(X,Y,d);
assume w in InnerVertices BitGFA0Str(X,Y,d);
then w in {[<*X,Y*>,xor2]} \/ {bA} \/
{[<*X,Y*>,and2],[<*Y,d*>,and2],[<*d,X*>,and2]} \/ {bC} by GFACIRC1:31;
then w in {[<*X,Y*>,xor2]} \/ {bA} \/
{[<*X,Y*>,and2],[<*Y,d*>,and2],[<*d,X*>,and2]} or w in {bC}
by XBOOLE_0:def 3;
then w in ({[<*X,Y*>,xor2]} \/ {bA}) or
w in {[<*X,Y*>,and2],[<*Y,d*>,and2],[<*d,X*>,and2]} or w in {bC}
by XBOOLE_0:def 3;
then A2: w in {[<*X,Y*>,xor2]} or w in {bA} or
w in {[<*X,Y*>,and2],[<*Y,d*>,and2],[<*d,X*>,and2]} or w in {bC}
by XBOOLE_0:def 3;
per cases by A2,TARSKI:def 1,ENUMSET1:def 1;
suppose w = [<*X,Y*>,xor2];
then <*[<*a,b*>,xor2],c*> = <*X,Y*> by XTUPLE_0:1;
hence contradiction by A1,FINSEQ_1:77;
end;
suppose w = bA;
then <*[<*a,b*>,xor2],c*> = <*[<*X,Y*>,xor2],d*> by XTUPLE_0:1;
then B1: [<*a,b*>,xor2] = [<*X,Y*>,xor2] by FINSEQ_1:77;
<*a,b*> = <*X,Y*> by B1,XTUPLE_0:1;
hence contradiction by A1,FINSEQ_1:77;
end;
suppose w = [<*X,Y*>,and2];
hence contradiction by TWOSCOMP:11,TWOSCOMP:9,XTUPLE_0:1;
end;
suppose w = [<*Y,d*>,and2];
hence contradiction by TWOSCOMP:11,TWOSCOMP:9,XTUPLE_0:1;
end;
suppose w = [<*d,X*>,and2];
hence contradiction by TWOSCOMP:11,TWOSCOMP:9,XTUPLE_0:1;
end;
suppose w = bC;
then B1: <*[<*a,b*>,xor2],c*>
= <*[<*X,Y*>,and2],[<*Y,d*>,and2],[<*d,X*>,and2]*> by XTUPLE_0:1;
len <*[<*a,b*>,xor2],c*> = 2 by FINSEQ_1:44;
hence contradiction by B1,FINSEQ_1:45;
end;
end;
:: A stage-1 carry output never occurs among the gates of a
:: stage-2 cell whose middle input is a pair.
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
let a,b,c be non pair set;
let X,Y,d be set such that
A1: Y is pair;
set w = GFA0CarryOutput(a,b,c);
set bA = GFA0AdderOutput(X,Y,d), bC = GFA0CarryOutput(X,Y,d);
assume w in InnerVertices BitGFA0Str(X,Y,d);
then w in {[<*X,Y*>,xor2]} \/ {bA} \/
{[<*X,Y*>,and2],[<*Y,d*>,and2],[<*d,X*>,and2]} \/ {bC} by GFACIRC1:31;
then w in {[<*X,Y*>,xor2]} \/ {bA} \/
{[<*X,Y*>,and2],[<*Y,d*>,and2],[<*d,X*>,and2]} or w in {bC}
by XBOOLE_0:def 3;
then w in ({[<*X,Y*>,xor2]} \/ {bA}) or
w in {[<*X,Y*>,and2],[<*Y,d*>,and2],[<*d,X*>,and2]} or w in {bC}
by XBOOLE_0:def 3;
then A2: w in {[<*X,Y*>,xor2]} or w in {bA} or
w in {[<*X,Y*>,and2],[<*Y,d*>,and2],[<*d,X*>,and2]} or w in {bC}
by XBOOLE_0:def 3;
per cases by A2,TARSKI:def 1,ENUMSET1:def 1;
suppose w = [<*X,Y*>,xor2];
then <*[<*a,b*>,and2],[<*b,c*>,and2],[<*c,a*>,and2]*> = <*X,Y*>
by XTUPLE_0:1;
then len <*X,Y*> = 3 by FINSEQ_1:45;
hence contradiction by FINSEQ_1:44;
end;
suppose w = bA;
then <*[<*a,b*>,and2],[<*b,c*>,and2],[<*c,a*>,and2]*>
= <*[<*X,Y*>,xor2],d*> by XTUPLE_0:1;
then len <*[<*X,Y*>,xor2],d*> = 3 by FINSEQ_1:45;
hence contradiction by FINSEQ_1:44;
end;
suppose w = [<*X,Y*>,and2];
then <*[<*a,b*>,and2],[<*b,c*>,and2],[<*c,a*>,and2]*> = <*X,Y*>
by XTUPLE_0:1;
then len <*X,Y*> = 3 by FINSEQ_1:45;
hence contradiction by FINSEQ_1:44;
end;
suppose w = [<*Y,d*>,and2];
then <*[<*a,b*>,and2],[<*b,c*>,and2],[<*c,a*>,and2]*> = <*Y,d*>
by XTUPLE_0:1;
then len <*Y,d*> = 3 by FINSEQ_1:45;
hence contradiction by FINSEQ_1:44;
end;
suppose w = [<*d,X*>,and2];
then <*[<*a,b*>,and2],[<*b,c*>,and2],[<*c,a*>,and2]*> = <*d,X*>
by XTUPLE_0:1;
then len <*d,X*> = 3 by FINSEQ_1:45;
hence contradiction by FINSEQ_1:44;
end;
suppose w = bC;
then <*[<*a,b*>,and2],[<*b,c*>,and2],[<*c,a*>,and2]*>
= <*[<*X,Y*>,and2],[<*Y,d*>,and2],[<*d,X*>,and2]*> by XTUPLE_0:1;
then [<*b,c*>,and2] = [<*Y,d*>,and2] by FINSEQ_1:78;
then <*b,c*> = <*Y,d*> by XTUPLE_0:1;
hence contradiction by A1,FINSEQ_1:77;
end;
end;
:: Input vertices of a stage-2 cell are exactly its three inputs.
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
let k be Nat;
let ap,bp,cp,dp be nonpair-yielding FinSequence;
set X = GFA0AdderOutput(ap.(k+1),bp.(k+1),cp.(k+1));
set Y = k-BitFTA0CarryOutput(ap,bp,cp,dp);
set d = dp.(k+1);
A1: X <> [<*Y,d*>,and2]
by XTUPLE_0:1,TWOSCOMP:11,TWOSCOMP:9;
A2: Y <> [<*d,X*>,and2] by LmT0CO;
thus thesis by A1,A2,GFACIRC1:33;
end;
:: A stage-2 cell stabilizes in 2 steps.
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
let k be Nat;
let ap,bp,cp,dp be nonpair-yielding FinSequence;
set X = GFA0AdderOutput(ap.(k+1),bp.(k+1),cp.(k+1));
set Y = k-BitFTA0CarryOutput(ap,bp,cp,dp);
set d = dp.(k+1);
A1: X <> [<*Y,d*>,and2]
by XTUPLE_0:1,TWOSCOMP:11,TWOSCOMP:9;
A2: Y <> [<*d,X*>,and2] by LmT0CO;
let s be State of BitGFA0Circ(X,Y,d);
thus thesis by A1,A2,GFACIRC1:40;
end;
:: The FALSE base output vertex is an inner vertex of every
:: layer-2 structure.
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
let n be Nat;
let ap,bp,cp,dp be FinSequence;
set c0 = [<*>,(0-tuples_on BOOLEAN)-->FALSE];
defpred P[Nat] means
c0 in InnerVertices ($1-BitFTA0Layer2Str(ap,bp,cp,dp));
0-BitFTA0Layer2Str(ap,bp,cp,dp)
= 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) by LmT00L2;
then InnerVertices (0-BitFTA0Layer2Str(ap,bp,cp,dp)) = {c0}
by CIRCCOMB:42;
then
A1: P[ 0 ] by TARSKI:def 1;
A2: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume P[i];
then c0 in InnerVertices (i-BitFTA0Layer2Str(ap,bp,cp,dp))
\/ InnerVertices BitGFA0Str(
GFA0AdderOutput(ap.(i+1),bp.(i+1),cp.(i+1)),
i-BitFTA0CarryOutput(ap,bp,cp,dp), dp.(i+1)) by XBOOLE_0:def 3;
hence P[i+1] by LmT0L2inner;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
:: Stage-1 outputs are never layer-2 gates.
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
let n be Nat;
let ap,bp,cp,dp be nonpair-yielding FinSequence;
let u,v,x be non pair set;
set c0 = [<*>,(0-tuples_on BOOLEAN)-->FALSE];
set wA = GFA0AdderOutput(u,v,x), wC = GFA0CarryOutput(u,v,x);
A1: wA <> c0
by XTUPLE_0:1;
A2: wC <> c0
by XTUPLE_0:1;
defpred P[Nat] means
not wA in InnerVertices ($1-BitFTA0Layer2Str(ap,bp,cp,dp)) &
not wC in InnerVertices ($1-BitFTA0Layer2Str(ap,bp,cp,dp));
0-BitFTA0Layer2Str(ap,bp,cp,dp)
= 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) by LmT00L2;
then InnerVertices (0-BitFTA0Layer2Str(ap,bp,cp,dp)) = {c0}
by CIRCCOMB:42;
then
A3: P[ 0 ] by A1,A2,TARSKI:def 1;
A4: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume B1: P[i];
set B = BitGFA0Str(GFA0AdderOutput(ap.(i+1),bp.(i+1),cp.(i+1)),
i-BitFTA0CarryOutput(ap,bp,cp,dp), dp.(i+1));
B2: i-BitFTA0CarryOutput(ap,bp,cp,dp) is pair by LmT0COp;
B3: not wA in InnerVertices B & not wC in InnerVertices B
by B2,LmT0W1,LmT0W2;
B4: InnerVertices ((i+1)-BitFTA0Layer2Str(ap,bp,cp,dp))
= InnerVertices (i-BitFTA0Layer2Str(ap,bp,cp,dp)) \/ InnerVertices B
by LmT0L2inner;
thus not wA in InnerVertices ((i+1)-BitFTA0Layer2Str(ap,bp,cp,dp))
by B4,B1,B3,XBOOLE_0:def 3;
thus not wC in InnerVertices ((i+1)-BitFTA0Layer2Str(ap,bp,cp,dp))
by B4,B1,B3,XBOOLE_0:def 3;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A3,A4);
hence thesis;
end;
:: Every layer-2 input vertex is a primary input or a stage-1 output.
LmT0InAcc: for n being Nat for ap,bp,cp,dp being nonpair-yielding FinSequence
for w being set
st w in InputVertices (n-BitFTA0Layer2Str(ap,bp,cp,dp)) holds
w is non 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
let n be Nat;
let ap,bp,cp,dp be nonpair-yielding FinSequence;
set c0 = [<*>,(0-tuples_on BOOLEAN)-->FALSE];
defpred P[Nat] means for w being set
st w in InputVertices ($1-BitFTA0Layer2Str(ap,bp,cp,dp)) holds
w is non 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));
A1: P[ 0 ]
proof
let w be set;
assume
B1: w in InputVertices (0-BitFTA0Layer2Str(ap,bp,cp,dp));
0-BitFTA0Layer2Str(ap,bp,cp,dp)
= 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) by LmT00L2;
then InputVertices (0-BitFTA0Layer2Str(ap,bp,cp,dp)) = rng <*>
by CIRCCOMB:42
.= {};
hence thesis by B1;
end;
A2: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume B1: P[i];
set X = GFA0AdderOutput(ap.(i+1),bp.(i+1),cp.(i+1));
set Y = i-BitFTA0CarryOutput(ap,bp,cp,dp);
set d = dp.(i+1);
set B = BitGFA0Str(X,Y,d);
set S1 = i-BitFTA0Layer2Str(ap,bp,cp,dp);
B2: (i+1)-BitFTA0Layer2Str(ap,bp,cp,dp) = S1 +* B by LmT05B;
B3: InputVertices (S1 +* B)
= ((InputVertices S1) \ (InnerVertices B))
\/ ((InputVertices B) \ (InnerVertices S1)) by CIRCCOMB:47,CIRCCMB2:5;
B4: InputVertices B = {X,Y,d} by LmT0C2i;
let w be set;
assume B5: w in InputVertices ((i+1)-BitFTA0Layer2Str(ap,bp,cp,dp));
per cases by B5,B2,B3,XBOOLE_0:def 3;
suppose w in (InputVertices S1) \ (InnerVertices B);
then w in InputVertices S1 by XBOOLE_0:def 5;
hence thesis by B1;
end;
suppose B6: w in (InputVertices B) \ (InnerVertices S1);
then C1: w in {X,Y,d} by B4,XBOOLE_0:def 5;
per cases by C1,ENUMSET1:def 1;
suppose C2: w = X;
thus thesis by C2;
end;
suppose C3: w = Y;
per cases by NAT_1:6;
suppose D1: i = 0;
E1: not w in InnerVertices S1 by B6,XBOOLE_0:def 5;
w = c0 by C3,D1,LmT00CO;
hence thesis by LmT0Cin0In,E1;
end;
suppose ex m being Nat st i = m+1;
then consider m being Nat such that E1: i = m+1;
reconsider u1 = ap.(m+1), v1 = bp.(m+1), x1 = cp.(m+1)
as non pair set;
w = GFA0CarryOutput(u1,v1,x1) by C3,E1,LmT0COk;
hence thesis;
end;
end;
suppose w = d;
hence thesis;
end;
end;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
:: Layer-2 inputs never hit the gates of the next stage-2 cell.
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
let k be Nat;
let ap,bp,cp,dp be nonpair-yielding FinSequence;
set X = GFA0AdderOutput(ap.(k+1),bp.(k+1),cp.(k+1));
set Y = k-BitFTA0CarryOutput(ap,bp,cp,dp);
set d = dp.(k+1);
set B = BitGFA0Str(X,Y,d);
set bA = GFA0AdderOutput(X,Y,d), bC = GFA0CarryOutput(X,Y,d);
A1: Y is pair by LmT0COp;
assume InputVertices (k-BitFTA0Layer2Str(ap,bp,cp,dp)) meets
InnerVertices B;
then consider w being object such that
A2: w in InputVertices (k-BitFTA0Layer2Str(ap,bp,cp,dp)) and
A3: w in InnerVertices B by XBOOLE_0:3;
reconsider w as set by TARSKI:1;
per cases by A2,LmT0InAcc;
suppose A4: w is non pair;
w in {[<*X,Y*>,xor2]} \/ {bA} \/
{[<*X,Y*>,and2],[<*Y,d*>,and2],[<*d,X*>,and2]} \/ {bC}
by A3,GFACIRC1:31;
then w in {[<*X,Y*>,xor2]} \/ {bA} \/
{[<*X,Y*>,and2],[<*Y,d*>,and2],[<*d,X*>,and2]} or w in {bC}
by XBOOLE_0:def 3;
then w in ({[<*X,Y*>,xor2]} \/ {bA}) or
w in {[<*X,Y*>,and2],[<*Y,d*>,and2],[<*d,X*>,and2]} or w in {bC}
by XBOOLE_0:def 3;
then B1: w in {[<*X,Y*>,xor2]} or w in {bA} or
w in {[<*X,Y*>,and2],[<*Y,d*>,and2],[<*d,X*>,and2]} or w in {bC}
by XBOOLE_0:def 3;
per cases by B1,TARSKI:def 1,ENUMSET1:def 1;
suppose w = [<*X,Y*>,xor2];
hence contradiction by A4;
end;
suppose w = bA;
hence contradiction by A4;
end;
suppose w = [<*X,Y*>,and2];
hence contradiction by A4;
end;
suppose w = [<*Y,d*>,and2];
hence contradiction by A4;
end;
suppose w = [<*d,X*>,and2];
hence contradiction by A4;
end;
suppose w = bC;
hence contradiction by A4;
end;
end;
suppose ex u,v,x being non pair set st w = GFA0AdderOutput(u,v,x);
then consider u,v,x being non pair set such that
B1: w = GFA0AdderOutput(u,v,x);
thus contradiction by A3,B1,A1,LmT0W1;
end;
suppose ex u,v,x being non pair set st w = GFA0CarryOutput(u,v,x);
then consider u,v,x being non pair set such that
B1: w = GFA0CarryOutput(u,v,x);
thus contradiction by A3,B1,A1,LmT0W2;
end;
end;
:: New-cell inputs never hit earlier layer-2 gates (from stage 2 on).
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
let m be Nat;
let ap,bp,cp,dp be nonpair-yielding FinSequence;
set X = GFA0AdderOutput(ap.(m+1+1),bp.(m+1+1),cp.(m+1+1));
set Y = (m+1)-BitFTA0CarryOutput(ap,bp,cp,dp);
set d = dp.(m+1+1);
set B = BitGFA0Str(X,Y,d);
set L2 = (m+1)-BitFTA0Layer2Str(ap,bp,cp,dp);
A1: InputVertices B = {X,Y,d} by LmT0C2i;
assume InputVertices B meets InnerVertices L2;
then consider w being object such that
A2: w in InputVertices B and
A3: w in InnerVertices L2 by XBOOLE_0:3;
per cases by A2,A1,ENUMSET1:def 1;
suppose A4: w = X;
thus contradiction by A4,A3,LmT0WnI;
end;
suppose A5: w = Y;
reconsider u1 = ap.(m+1), v1 = bp.(m+1), x1 = cp.(m+1)
as non pair set;
not GFA0CarryOutput(u1,v1,x1) in InnerVertices L2 by LmT0WnI;
hence contradiction by A5,LmT0COk,A3;
end;
suppose A6: w = d;
reconsider d1 = d as non pair set;
B1: {d1} misses InnerVertices L2 by LmT0L2rel,FACIRC_1:5;
d1 in {d1} by TARSKI:def 1;
then d1 in {d1} /\ InnerVertices L2 by A6,A3,XBOOLE_0:def 4;
hence contradiction by B1,XBOOLE_0:def 7;
end;
end;
:: The FALSE constant gate recomputes its output to FALSE in one
:: step, in any circuit containing it as a gate.
theorem Th9:
for S being unsplit gate`1=arity gate`2isBoolean non void
non empty ManySortedSign
for A being Boolean gate`2=den non-empty Circuit of S
st [<*>,(0-tuples_on BOOLEAN)-->FALSE] in InnerVertices S
for s being State of A holds
(Following s).[<*>,(0-tuples_on BOOLEAN)-->FALSE] = FALSE
proof
let S be unsplit gate`1=arity gate`2isBoolean non void
non empty ManySortedSign;
let A be Boolean gate`2=den non-empty Circuit of S;
set f0 = (0-tuples_on BOOLEAN)-->FALSE;
assume [<*>,f0] in InnerVertices S;
then
A1: [<*>,f0] in the carrier' of S by FACIRC_1:37;
let s be State of A;
A2: (Following s).[<*>,f0] = f0.(s*<*>) by A1,FACIRC_1:35;
per cases;
suppose A3: s*<*> in dom f0;
dom f0 = 0-tuples_on BOOLEAN by FUNCOP_1:13;
hence thesis by A2,FUNCOP_1:7,A3;
end;
suppose not s*<*> in dom f0;
hence thesis by A2,XBOOLEAN:def 1,FUNCT_1:def 2;
end;
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:
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
let n be Nat;
let ap,bp,cp,dp be nonpair-yielding FinSequence;
set c0 = [<*>,(0-tuples_on BOOLEAN)-->FALSE];
set A0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
defpred P[Nat] means
for s being State of $1-BitFTA0Layer2Circ(ap,bp,cp,dp)
st s.[<*>,(0-tuples_on BOOLEAN)-->FALSE] = FALSE
holds Following(s,2) is stable;
A1: 0-BitFTA0Layer2Circ(ap,bp,cp,dp) = A0
proof
consider f,g,h being ManySortedSet of NAT such that
0-BitFTA0Layer2Str(ap,bp,cp,dp) = f.0 and
B1: 0-BitFTA0Layer2Circ(ap,bp,cp,dp) = g.0 and
f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) and
B2: g.0 = A0 and
h.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE] and
for k being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S, 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)) by Def7;
thus thesis by B1,B2;
end;
A2: P[ 0 ]
proof
let s be State of 0-BitFTA0Layer2Circ(ap,bp,cp,dp);
assume s.c0 = FALSE;
reconsider s0 = s as State of A0 by A1;
B1: Following(s0,1) = Following s0 by FACIRC_1:14;
B2: Following(s0,2) = Following(s0,1) by B1,CIRCCMB2:2,CIRCCMB2:4;
B3: 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE)
= 0-BitFTA0Layer2Str(ap,bp,cp,dp) by LmT00L2;
thus thesis by B3,A1,B2,B1,CIRCCMB2:2;
end;
A3: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume B1: P[i];
set X = GFA0AdderOutput(ap.(i+1),bp.(i+1),cp.(i+1));
set Y = i-BitFTA0CarryOutput(ap,bp,cp,dp);
set B = BitGFA0Str(X,Y,dp.(i+1));
set Bc = BitGFA0Circ(X,Y,dp.(i+1));
set S1 = i-BitFTA0Layer2Str(ap,bp,cp,dp);
set SS = (i+1)-BitFTA0Layer2Str(ap,bp,cp,dp);
set C1 = i-BitFTA0Layer2Circ(ap,bp,cp,dp);
set AA = (i+1)-BitFTA0Layer2Circ(ap,bp,cp,dp);
B2: SS = S1 +* B by LmT05B;
B3: AA = C1 +* Bc by LmT06B;
B4: C1 tolerates Bc by CIRCCOMB:60;
B5: the Sorts of C1 tolerates the Sorts of Bc by B4,CIRCCOMB:def 3;
B6: c0 in InnerVertices S1 by LmT0Cin0In;
let s be State of (i+1)-BitFTA0Layer2Circ(ap,bp,cp,dp);
assume B7: s.c0 = FALSE;
reconsider t = s as State of C1 +* Bc by B3;
reconsider s1 = t|the carrier of S1 as State of C1
by B5,CIRCCOMB:26;
B8: s1.c0 = FALSE by B7,B6,FUNCT_1:49;
B9: Following(s1,2) is stable by B1,B8;
per cases by NAT_1:6;
suppose B10: i = 0;
C1: S1 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) by B10,LmT00L2;
C2: InputVertices S1 = rng <*> by C1,CIRCCOMB:42
.= {};
C3: InputVertices S1 /\ InnerVertices B = {} by C2;
C4: InnerVertices S1 = {c0} by C1,CIRCCOMB:42;
C5: Following s1 = s1
proof
D1: dom s1 = the carrier of S1 by CIRCUIT1:3;
now
let y be object;
assume y in dom Following s1;
then
E2: y in the carrier of S1 by CIRCUIT1:3;
per cases;
suppose E3: y in InputVertices S1;
thus (Following s1).y = s1.y by E3,CIRCUIT2:def 5;
end;
suppose E4: not y in InputVertices S1;
InputVertices S1 = (the carrier of S1)
\ rng the ResultSort of S1 by MSAFREE2:def 2;
then y in rng the ResultSort of S1
by E2,E4,XBOOLE_0:def 5;
then y in InnerVertices S1 by MSAFREE2:def 3;
then
y = c0 by C4,TARSKI:def 1;
hence (Following s1).y = s1.y by C4,B8,LmT0Cin0In,Th9;
end;
end;
hence thesis by CIRCUIT1:3,D1,FUNCT_1:2;
end;
s1 is stable by C5,CIRCUIT2:def 6;
then
C6: Following(s1,0) is stable by FACIRC_1:11;
reconsider sB = Following(t,0)|the carrier of B as State of Bc
by B5,CIRCCOMB:26;
C7: Following(sB,2) is stable by LmT0C2s;
Following(t, 0+2) is stable
by B4,C3,XBOOLE_0:def 7,C6,C7,CIRCCMB2:19;
hence Following(s,2) is stable by B2,B3;
end;
suppose ex m being Nat st i = m+1;
then consider m being Nat such that C1: i = m+1;
C2: InputVertices S1 misses InnerVertices B by LmT0Dj1;
C3: InputVertices B misses InnerVertices S1 by C1,LmT0Dj2;
reconsider sB = t|the carrier of B as State of Bc
by B5,CIRCCOMB:26;
C4: Following(sB,2) is stable by LmT0C2s;
Following(t, max(2,2)) is stable
by CIRCCOMB:60,C2,C3,B9,C4,CIRCCMB2:22;
hence Following(s,2) is stable by B2,B3;
end;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
::--------------------------------
:: Stability of n-depth FTA Circuit (TYPE-0)
::--------------------------------
theorem :: Th11
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
let n be Nat;
let ap,bp,cp,dp be nonpair-yielding FinSeqLen of n;
let s be State of n-BitFTA0Circ(ap,bp,cp,dp);
set S1 = n-BitFTA0Layer1Str(ap,bp,cp);
set S2 = n-BitFTA0Layer2Str(ap,bp,cp,dp);
set C1 = n-BitFTA0Layer1Circ(ap,bp,cp);
set C2 = n-BitFTA0Layer2Circ(ap,bp,cp,dp);
set S = n-BitFTA0Str(ap,bp,cp,dp);
set C = n-BitFTA0Circ(ap,bp,cp,dp);
A1: S = S1 +* S2 by Th5;
A2: C = C1 +* C2 by Th6;
A3: C1 tolerates C2 by CIRCCOMB:60;
A4: the Sorts of C1 tolerates the Sorts of C2 by A3,CIRCCOMB:def 3;
reconsider t = s as State of C1 +* C2 by A2;
reconsider s1 = t|the carrier of S1 as State of C1 by A4,CIRCCOMB:26;
reconsider s2 = Following(t,2)|the carrier of S2 as State of C2
by A4,CIRCCOMB:26;
A5: InputVertices S1 misses InnerVertices S2 by Th7;
A6: Following(s1,2) is stable by Th8;
A7: Following(s2,2) is stable
proof
set c0 = [<*>,(0-tuples_on BOOLEAN)-->FALSE];
B1: c0 in InnerVertices S2 by LmT0Cin0In;
B2: S1 tolerates S2 by CIRCCOMB:47;
InnerVertices S = InnerVertices S1 \/ InnerVertices S2
by A1,B2,CIRCCOMB:11;
then
B3: c0 in InnerVertices S by B1,XBOOLE_0:def 3;
reconsider Cb = C as Boolean gate`2=den non-empty Circuit of S;
reconsider s9 = s as State of Cb;
B5: (Following Following s9).c0 = FALSE by B3,Th9;
s2.c0 = (Following(t,2)).c0 by FUNCT_1:49,B1
.= FALSE by A1,A2,FACIRC_1:15,B5;
hence thesis by Th10;
end;
Following(t,2+2) is stable by CIRCCOMB:60,A5,A6,A7,CIRCCMB2:19;
hence thesis by A1,A2;
end;
begin :: 2. Stability of a Parallel 4-2 Compressor Circuit (TYPE-1)
::------------------------------------------------
:: 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 gate`1=arity gate`2isBoolean non void non empty strict;
func n-BitFTA1Str(ap,bm,cp,dm) ->
unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign means
:Def8:
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, S being non empty ManySortedSign, z be 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
proof
deffunc S(non empty ManySortedSign, set, Nat)
= $1 +* BitFTA1Str(ap.($3+1), bm.($3+1), cp.($3+1), dm.($3+1), $2);
deffunc o(set, Nat)
= BitFTA1CarryOutput(ap.($2+1), bm.($2+1), cp.($2+1), dm.($2+1), $1);
for S1,S2 being unsplit gate`1=arity gate`2isBoolean non void non empty
strict non empty ManySortedSign st
(ex f,h being ManySortedSet of NAT st S1 = f.n & f.0 = S0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)) &
(ex f,h being ManySortedSet of NAT st S2 = f.n & f.0 = S0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n))
holds S1 = S2 from CIRCCMB2:sch 9;
hence thesis;
end;
existence
proof
deffunc S(set, Nat)
= BitFTA1Str(ap.($2+1), bm.($2+1), cp.($2+1), dm.($2+1), $1);
deffunc o(set, Nat)
= BitFTA1CarryOutput(ap.($2+1), bm.($2+1), cp.($2+1), dm.($2+1), $1);
ex S being unsplit gate`1=arity gate`2isBoolean
non void non empty non empty strict ManySortedSign,
f,h being ManySortedSet of NAT st S = f.n & f.0 = S0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = h.n
holds f.(n+1) = S +* S(x,n) & h.(n+1) = o(x,n) from CIRCCMB2:sch 8(A1);
hence thesis;
end;
end;
:: 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) ->
Boolean gate`2=den strict Circuit of n-BitFTA1Str(ap,bm,cp,dm) means
:Def9:
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, S being non empty ManySortedSign,
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
proof
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set A0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set Sn = n-BitFTA1Str(ap,bm,cp,dm);
set o0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
deffunc S(non empty ManySortedSign, set, Nat)
= $1 +* BitFTA1Str(ap.($3+1), bm.($3+1), cp.($3+1), dm.($3+1), $2);
deffunc A(non empty ManySortedSign, non-empty MSAlgebra over $1,
set, Nat)
= $2 +* BitFTA1Circ(ap.($4+1), bm.($4+1), cp.($4+1), dm.($4+1), $3);
deffunc o(set, Nat)
= BitFTA1CarryOutput(ap.($2+1), bm.($2+1), cp.($2+1), dm.($2+1), $1);
A1: for S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set, n being Nat holds
A(S,A,x,n) is non-empty MSAlgebra over S(S,x,n);
for A1,A2 being Boolean gate`2=den strict Circuit of Sn st
(ex f,g,h being ManySortedSet of NAT st Sn= f.n & A1 = g.n &
f.0 = S0 & g.0 = A0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set st S = f.n & A = g.n & x = h.n
holds f.(n+1) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x,n)) &
(ex f,g,h being ManySortedSet of NAT st Sn = f.n & A2 = g.n &
f.0 = S0 & g.0 = A0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set st S = f.n & A = g.n & x = h.n
holds f.(n+1) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x,n))
holds A1 = A2 from CIRCCMB2:sch 21(A1);
hence thesis;
end;
existence
proof
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set A0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set Sn = n-BitFTA1Str(ap,bm,cp,dm);
set o0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
deffunc S(non empty ManySortedSign, set, Nat)
= $1 +* BitFTA1Str(ap.($3+1), bm.($3+1), cp.($3+1), dm.($3+1), $2);
deffunc A(non empty ManySortedSign, non-empty MSAlgebra over $1,
set, Nat)
= $2 +* BitFTA1Circ(ap.($4+1), bm.($4+1), cp.($4+1), dm.($4+1), $3);
deffunc o(set, Nat)
= BitFTA1CarryOutput(ap.($2+1), bm.($2+1), cp.($2+1), dm.($2+1), $1);
A2: for S being unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign, x being set, n being Nat holds
S(S,x,n) is unsplit gate`1=arity gate`2isBoolean non void strict;
A3: ex f,h being ManySortedSet of NAT st Sn = f.n & f.0 = S0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n) by Def8;
A4: for S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set, n being Nat holds
A(S,A,x,n) is non-empty MSAlgebra over S(S,x,n);
A5: for S,S1 being unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign, A being Boolean gate`2=den strict Circuit of S
for x being set, n being Nat st S1 = S(S,x,n) holds
A(S,A,x,n) is Boolean gate`2=den strict Circuit of S1;
ex A being Boolean gate`2=den strict Circuit of Sn,
f,g,h being ManySortedSet of NAT st Sn = f.n & A = g.n &
f.0 = S0 & g.0 = A0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set st S = f.n & A = g.n & x = h.n
holds f.(n+1) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x,n)
from CIRCCMB2:sch 19(A2,A3,A4,A5);
hence thesis;
end;
end;
:: 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:
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
proof
set o0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
deffunc o(Nat,set)
= BitFTA1CarryOutput(ap.($1+1), bm.($1+1), cp.($1+1), dm.($1+1), $2);
let o1, o2 be Element of InnerVertices (n-BitFTA1Str(ap,bm,cp,dm));
given h1 being ManySortedSet of NAT such that
A1: o1 = h1.n and
A2: h1.0 = o0 and
A3: for n being Nat holds h1.(n+1) = o(n,h1.n);
given h2 being ManySortedSet of NAT such that
A4: o2 = h2.n and
A5: h2.0 = o0 and
A6: for n being Nat holds h2.(n+1) = o(n,h2.n);
A7: dom h1 = NAT by PARTFUN1:def 2;
A8: dom h2 = NAT by PARTFUN1:def 2;
h1 = h2 from NAT_1:sch 15(A7,A2,A3,A8,A5,A6);
hence thesis by A1,A4;
end;
existence
proof
defpred P[set,set,set] means not contradiction;
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set Sn = n-BitFTA1Str(ap,bm,cp,dm);
set o0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
deffunc S(non empty ManySortedSign, set, Nat)
= $1 +* BitFTA1Str(ap.($3+1), bm.($3+1), cp.($3+1), dm.($3+1), $2);
deffunc o(set, Nat)
= BitFTA1CarryOutput(ap.($2+1), bm.($2+1), cp.($2+1), dm.($2+1), $1);
consider f,g being ManySortedSet of NAT such that
A9: Sn = f.n and
A10: f.0 = S0 and
A11: g.0 = o0 and
A12: for n being Nat, S being non empty ManySortedSign, z be set
st S = f.n & z = g.n holds f.(n+1) = S(S,z,n) & g.(n+1) = o(z,n) by Def8;
defpred P[Nat] means ex S being non empty ManySortedSign
st S = f.$1 & g.$1 in InnerVertices S;
InnerVertices S0 = {o0} by CIRCCOMB:42;
then o0 in InnerVertices S0 by TARSKI:def 1;
then
A13: P[ 0 ] by A10,A11;
A14: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat such that
A15: ex S being non empty ManySortedSign
st S = f.i & g.i in InnerVertices S and
A16: for S being non empty ManySortedSign
st S = f.(i+1) holds not g.(i+1) in InnerVertices S;
consider S being non empty ManySortedSign such that
A17: S = f.i and g.i in InnerVertices S by A15;
A18: BitFTA1CarryOutput(ap.(i+1), bm.(i+1), cp.(i+1), dm.(i+1), g.i) in
InnerVertices
(S +* BitFTA1Str(ap.(i+1), bm.(i+1), cp.(i+1), dm.(i+1), g.i))
by FACIRC_1:22;
A19: f.(i+1)
= S +* BitFTA1Str(ap.(i+1), bm.(i+1), cp.(i+1), dm.(i+1), g.i)
by A12,A17;
g.(i+1) = BitFTA1CarryOutput(ap.(i+1), bm.(i+1), cp.(i+1), dm.(i+1), g.i)
by A12,A17;
hence contradiction by A16,A18,A19;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A13,A14);
then ex S being non empty ManySortedSign
st S = f.n & g.n in InnerVertices S;
then reconsider o = g.n as Element of InnerVertices Sn by A9;
take o, g;
thus o = g.n & g.0 = o0 by A11;
let i be Nat;
A20: ex S being non empty ManySortedSign, x being set
st S = f.0 & x = g.0 & P[S, x, 0] by A10;
A21: for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = g.n & P[S, x, n] holds P[S(S,x,n), o(x, n), n+1];
for n being Nat ex S being non empty ManySortedSign
st S = f.n & P[S,g.n,n] from CIRCCMB2:sch 2(A20,A12,A21);
then ex S being non empty ManySortedSign st S = f.i;
hence thesis by A12;
end;
end;
::-----------------------------------------------
:: 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:
for ap,bm,cp,dm being FinSequence, 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, S being non empty ManySortedSign,
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)
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
let ap,bm,cp,dm be FinSequence, f,g,h be ManySortedSet of NAT;
set f0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set g0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set h0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
deffunc S(non empty ManySortedSign,set,Nat)
= $1 +* BitFTA1Str(ap.($3+1),bm.($3+1),cp.($3+1),dm.($3+1), $2);
deffunc A(non empty ManySortedSign,non-empty MSAlgebra over $1,
set, Nat) = $2 +* BitFTA1Circ(ap.($4+1),bm.($4+1),cp.($4+1),dm.($4+1), $3);
deffunc o(set, Nat) = BitFTA1CarryOutput(ap.($2+1),bm.($2+1),cp.($2+1),
dm.($2+1), $1);
deffunc F(Nat, set) = BitFTA1CarryOutput(ap.($1+1),bm.($1+1),cp.($1+1),
dm.($1+1), $2);
assume that
A1: f.0 = f0 & g.0 = g0 and
A2: h.0 = h0 and
A3: for n being Nat, S being non empty ManySortedSign,
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(S,z,n) &
g.(n+1) = A(S,A,z,n) & h.(n+1) = o(z,n);
let n be Nat;
consider f1,g1,h1 being ManySortedSet of NAT such that
A4: n-BitFTA1Str(ap,bm,cp,dm) = f1.n and
A5: n-BitFTA1Circ(ap,bm,cp,dm) = g1.n and
A6: f1.0 = f0 and
A7: g1.0 = g0 and
A8: h1.0 = h0 and
A9: for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for z being set st S = f1.n & A = g1.n & z = h1.n holds
f1.(n+1) = S(S,z,n) & g1.(n+1) = A(S,A,z,n) & h1.(n+1) = o(z,n) by Def9;
A10: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
st S = f.0 & A = g.0 by A1;
A11: f.0 = f1.0 & g.0 = g1.0 & h.0 = h1.0 by A1,A2,A6,A7,A8;
A12: for S being non empty ManySortedSign, A being non-empty MSAlgebra over S
for z being set, n being Nat holds
A(S,A,z,n) is non-empty MSAlgebra over S(S,z,n);
f = f1 & g = g1 & h = h1 from CIRCCMB2:sch 14(A10,A11,A3,A9,A12);
hence n-BitFTA1Str(ap,bm,cp,dm) = f.n & n-BitFTA1Circ(ap,bm,cp,dm) = g.n
by A4,A5;
A13: for n being Nat, S being non empty ManySortedSign, z being set
st S = f.n & z = h.n holds f.(n+1) = S(S,z,n) &
h.(n+1) = o(z,n) from CIRCCMB2:sch 15(A1,A3,A12);
A14: f.0 = f0 by A1;
A15: dom h = NAT by PARTFUN1:def 2;
A16: h.0 = h0 by A2;
for n being Nat, z being set st z = h.n
holds h.(n+1) = o(z,n) from CIRCCMB2:sch 3(A14,A13);
then
A17: for n being Nat holds h.(n+1) = F(n,h.n);
consider h1 being ManySortedSet of NAT such that
A18: n-BitFTA1CarryOutput(ap,bm,cp,dm) = h1.n and
A19: h1.0 = h0 and
A20: for n being Nat holds h1.(n+1) = BitFTA1CarryOutput(ap.(n+1),bm.(n+1),
cp.(n+1),dm.(n+1), h1.n) by Def10;
A21: dom h1 = NAT by PARTFUN1:def 2;
A22: h1.0 = h0 by A19;
A23: for n being Nat holds h1.(n+1) = F(n,h1.n) by A20;
h = h1 from NAT_1:sch 15(A15,A16,A17,A21,A22,A23);
hence thesis by A18;
end;
:: Base case: the 0-bit structure, circuit and carry are all the FALSE
:: constant gate (resp. its algebra / output vertex).
theorem Th13:
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
let ap,bm,cp,dm be FinSequence;
set f0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set g0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set h0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
A1: ex f,g,h being ManySortedSet of NAT st (0-BitFTA1Str(ap,bm,cp,dm) = f.0)
& (0-BitFTA1Circ(ap,bm,cp,dm) = g.0)
& (f.0 = f0) & (g.0 = g0) & (h.0 = h0) & (
for n being Nat, S being non empty ManySortedSign, 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)) by Def9;
hence 0-BitFTA1Str(ap,bm,cp,dm) = f0;
thus 0-BitFTA1Circ(ap,bm,cp,dm) = g0 by A1;
InnerVertices (0-BitFTA1Str(ap,bm,cp,dm)) = { h0 } by A1,CIRCCOMB:42;
hence thesis by TARSKI:def 1;
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:
for n be 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
set f0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set g0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set h0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
let n be Nat;
let ap,bm,cp,dm be FinSequence;
consider f,g,h being ManySortedSet of NAT such that
A1: n-BitFTA1Str(ap,bm,cp,dm) = f.n and
A2: n-BitFTA1Circ(ap,bm,cp,dm) = g.n and
A3: f.0 = f0 and
A4: g.0 = g0 and
A5: h.0 = h0 and
A6: for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for z be 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) by Def9;
A7: n-BitFTA1CarryOutput(ap,bm,cp,dm) = h.n by A3,A4,A5,A6,Th12;
A8: (n+1)-BitFTA1Str(ap,bm,cp,dm) = f.(n+1) by A3,A4,A5,A6,Th12;
A9: (n+1)-BitFTA1Circ(ap,bm,cp,dm) = g.(n+1) by A3,A4,A5,A6,Th12;
(n+1)-BitFTA1CarryOutput(ap,bm,cp,dm) = h.(n+1) by A3,A4,A5,A6,Th12;
hence thesis by A1,A2,A6,A7,A8,A9;
end;
::--------------------------------
:: Carry Output Stabilizes at 2 Steps (independent of Carry-in)
::--------------------------------
:: Cell disjointness: the primary (non-pair) inputs of one BitGFA1 cell
:: miss the internal gate vertices of any BitGFA2 cell.
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
let ap,bm,cp be non pair set;
let x,y,z be set;
InputVertices BitGFA1Str(ap,bm,cp) is without_pairs by GFACIRC1:67;
hence thesis by FACIRC_1:5,GFACIRC1:96;
end;
:: The carry output remains stable from T=2 onward.
theorem :: Th15
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
let ap,bm,cp be non pair set;
let dm,cin be set;
let s be State of BitFTA1Circ(ap,bm,cp,dm,cin);
let k be Nat;
assume
A1: k >= 2;
set S1 = BitGFA1Str(ap,bm,cp);
set C1 = BitGFA1Circ(ap,bm,cp);
set A1v = GFA1AdderOutput(ap,bm,cp);
set S2 = BitGFA2Str(A1v,cin,dm);
set C2 = BitGFA2Circ(A1v,cin,dm);
set A2v = GFA1CarryOutput(ap,bm,cp);
reconsider s1 = s|the carrier of S1 as State of C1 by FACIRC_1:26;
reconsider t = s as State of C1+*C2;
A2: InputVertices S1 misses InnerVertices S2 by LmT11;
A5: Following(t,k).A2v = Following(s1,k).A2v by A2,GFACIRC1:68,FACIRC_1:32;
A6: Following(t,2).A2v = Following(s1,2).A2v by A2,GFACIRC1:68,FACIRC_1:32;
thus thesis by A5,A6,A1,GFACIRC1:72,CIRCCMB2:4;
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) ->
unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign means
:Def11:
ex f being ManySortedSet of NAT st
it = f.n & f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) &
for k being Nat, 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
proof
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set h = EmptyMS NAT;
deffunc SG(non empty ManySortedSign, set, Nat)
= $1 +* BitGFA1Str(ap.($3+1), bm.($3+1), cp.($3+1));
deffunc oo(set, Nat) = {};
let S1,S2 be unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign;
given f1 being ManySortedSet of NAT such that
E1: S1 = f1.n and E2: f1.0 = S0 and
E3: for k being Nat, S being non empty ManySortedSign st S = f1.k
holds f1.(k+1) = S +* BitGFA1Str(ap.(k+1), bm.(k+1), cp.(k+1));
given f2 being ManySortedSet of NAT such that
E4: S2 = f2.n and E5: f2.0 = S0 and
E6: for k being Nat, S being non empty ManySortedSign st S = f2.k
holds f2.(k+1) = S +* BitGFA1Str(ap.(k+1), bm.(k+1), cp.(k+1));
P1: ex f,hh being ManySortedSet of NAT st S1 = f.n & f.0 = S0 &
hh.0 = {} & for m being Nat, S being non empty ManySortedSign, x being set
st S = f.m & x = hh.m holds f.(m+1) = SG(S,x,m) & hh.(m+1) = oo(x,m)
proof
take f1, h;
thus S1 = f1.n & f1.0 = S0 & h.0 = {} by E1,E2,PBOOLE:5;
let m be Nat, S be non empty ManySortedSign, x be set;
assume that H1: S = f1.m and x = h.m;
thus f1.(m+1) = SG(S,x,m) by E3,H1;
thus h.(m+1) = oo(x,m) by PBOOLE:5;
end;
P2: ex f,hh being ManySortedSet of NAT st S2 = f.n & f.0 = S0 &
hh.0 = {} & for m being Nat, S being non empty ManySortedSign, x being set
st S = f.m & x = hh.m holds f.(m+1) = SG(S,x,m) & hh.(m+1) = oo(x,m)
proof
take f2, h;
thus S2 = f2.n & f2.0 = S0 & h.0 = {} by E4,E5,PBOOLE:5;
let m be Nat, S be non empty ManySortedSign, x be set;
assume that H2: S = f2.m and x = h.m;
thus f2.(m+1) = SG(S,x,m) by E6,H2;
thus h.(m+1) = oo(x,m) by PBOOLE:5;
end;
for T1,T2 being unsplit gate`1=arity gate`2isBoolean non void non empty
strict non empty ManySortedSign st
(ex f,hh being ManySortedSet of NAT st T1 = f.n & f.0 = S0 & hh.0 = {} &
for m being Nat, S being non empty ManySortedSign, x being set
st S = f.m & x = hh.m holds f.(m+1) = SG(S,x,m) & hh.(m+1) = oo(x,m)) &
(ex f,hh being ManySortedSet of NAT st T2 = f.n & f.0 = S0 & hh.0 = {} &
for m being Nat, S being non empty ManySortedSign, x being set
st S = f.m & x = hh.m holds f.(m+1) = SG(S,x,m) & hh.(m+1) = oo(x,m))
holds T1 = T2 from CIRCCMB2:sch 9;
hence S1 = S2 by P1,P2;
end;
existence
proof
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
A1: 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE)
is unsplit gate`1=arity gate`2isBoolean non void non empty strict;
deffunc SG(set, Nat) = BitGFA1Str(ap.($2+1), bm.($2+1), cp.($2+1));
deffunc oo(set, Nat) = {};
consider SX being unsplit gate`1=arity gate`2isBoolean
non void non empty non empty strict ManySortedSign,
f,h being ManySortedSet of NAT such that
B1: SX = f.n & f.0 = S0 & h.0 = {} &
for m being Nat, S being non empty ManySortedSign, x being set
st S = f.m & x = h.m
holds f.(m+1) = S +* SG(x,m) & h.(m+1) = oo(x,m) from CIRCCMB2:sch 8(A1);
take SX, f;
thus SX = f.n by B1;
thus f.0 = S0 by B1;
let k be Nat, S be non empty ManySortedSign;
assume B2: S = f.k;
h.k = h.k;
hence thesis by B1,B2;
end;
end;
:: 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) ->
Boolean gate`2=den strict Circuit of n-BitFTA1Layer1Str(ap,bm,cp) means
:Def12:
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, S being non empty ManySortedSign,
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
proof
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set A0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set Sn = n-BitFTA1Layer1Str(ap,bm,cp);
set h = EmptyMS NAT;
deffunc SG(non empty ManySortedSign, set, Nat)
= $1 +* BitGFA1Str(ap.($3+1), bm.($3+1), cp.($3+1));
deffunc AG(non empty ManySortedSign, non-empty MSAlgebra over $1,
set, Nat) = $2 +* BitGFA1Circ(ap.($4+1), bm.($4+1), cp.($4+1));
deffunc oo(set, Nat) = {};
Q1: for S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set, m being Nat holds
AG(S,A,x,m) is non-empty MSAlgebra over SG(S,x,m);
let AA1,AA2 be Boolean gate`2=den strict Circuit of Sn;
given f1,g1 being ManySortedSet of NAT such that
E1: Sn = f1.n and E1b: AA1 = g1.n and E2: f1.0 = S0 and E2b: g1.0 = A0 and
E3: for k being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S st S = f1.k & A = g1.k holds
f1.(k+1) = S +* BitGFA1Str(ap.(k+1), bm.(k+1), cp.(k+1)) &
g1.(k+1) = A +* BitGFA1Circ(ap.(k+1), bm.(k+1), cp.(k+1));
given f2,g2 being ManySortedSet of NAT such that
E4: Sn = f2.n and E4b: AA2 = g2.n and E5: f2.0 = S0 and E5b: g2.0 = A0 and
E6: for k being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S st S = f2.k & A = g2.k holds
f2.(k+1) = S +* BitGFA1Str(ap.(k+1), bm.(k+1), cp.(k+1)) &
g2.(k+1) = A +* BitGFA1Circ(ap.(k+1), bm.(k+1), cp.(k+1));
P1: ex f,g,hh being ManySortedSet of NAT st Sn = f.n & AA1 = g.n &
f.0 = S0 & g.0 = A0 & hh.0 = {} &
for m being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set st S = f.m & A = g.m & x = hh.m
holds f.(m+1) = SG(S,x,m) & g.(m+1) = AG(S,A,x,m) & hh.(m+1) = oo(x,m)
proof
take f1,g1,h;
thus Sn = f1.n & AA1 = g1.n & f1.0 = S0 & g1.0 = A0 & h.0 = {}
by E1,E1b,E2,E2b,PBOOLE:5;
let m be Nat, S be non empty ManySortedSign;
let A be non-empty MSAlgebra over S, x be set;
assume that H1: S = f1.m & A = g1.m and x = h.m;
thus f1.(m+1) = SG(S,x,m) & g1.(m+1) = AG(S,A,x,m) by E3,H1;
thus h.(m+1) = oo(x,m) by PBOOLE:5;
end;
P2: ex f,g,hh being ManySortedSet of NAT st Sn = f.n & AA2 = g.n &
f.0 = S0 & g.0 = A0 & hh.0 = {} &
for m being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set st S = f.m & A = g.m & x = hh.m
holds f.(m+1) = SG(S,x,m) & g.(m+1) = AG(S,A,x,m) & hh.(m+1) = oo(x,m)
proof
take f2,g2,h;
thus Sn = f2.n & AA2 = g2.n & f2.0 = S0 & g2.0 = A0 & h.0 = {}
by E4,E4b,E5,E5b,PBOOLE:5;
let m be Nat, S be non empty ManySortedSign;
let A be non-empty MSAlgebra over S, x be set;
assume that H2: S = f2.m & A = g2.m and x = h.m;
thus f2.(m+1) = SG(S,x,m) & g2.(m+1) = AG(S,A,x,m) by E6,H2;
thus h.(m+1) = oo(x,m) by PBOOLE:5;
end;
for B1,B2 being Boolean gate`2=den strict Circuit of Sn st
(ex f,g,hh being ManySortedSet of NAT st Sn = f.n & B1 = g.n &
f.0 = S0 & g.0 = A0 & hh.0 = {} &
for m being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set st S = f.m & A = g.m & x = hh.m
holds f.(m+1) = SG(S,x,m) & g.(m+1) = AG(S,A,x,m) & hh.(m+1) = oo(x,m)) &
(ex f,g,hh being ManySortedSet of NAT st Sn = f.n & B2 = g.n &
f.0 = S0 & g.0 = A0 & hh.0 = {} &
for m being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set st S = f.m & A = g.m & x = hh.m
holds f.(m+1) = SG(S,x,m) & g.(m+1) = AG(S,A,x,m) & hh.(m+1) = oo(x,m))
holds B1 = B2 from CIRCCMB2:sch 21(Q1);
hence AA1 = AA2 by P1,P2;
end;
existence
proof
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set A0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set Sn = n-BitFTA1Layer1Str(ap,bm,cp);
set h = EmptyMS NAT;
deffunc SG(non empty ManySortedSign, set, Nat)
= $1 +* BitGFA1Str(ap.($3+1), bm.($3+1), cp.($3+1));
deffunc AG(non empty ManySortedSign, non-empty MSAlgebra over $1,
set, Nat) = $2 +* BitGFA1Circ(ap.($4+1), bm.($4+1), cp.($4+1));
deffunc oo(set, Nat) = {};
A2: for S being unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign, x being set, m being Nat holds
SG(S,x,m) is unsplit gate`1=arity gate`2isBoolean non void strict;
A3: ex f,hh being ManySortedSet of NAT st Sn = f.n & f.0 = S0 &
hh.0 = {} & for m being Nat, S being non empty ManySortedSign, x being set
st S = f.m & x = hh.m holds f.(m+1) = SG(S,x,m) & hh.(m+1) = oo(x,m)
proof
consider f being ManySortedSet of NAT such that
Q2: Sn = f.n and Q3: f.0 = S0 and
Q4: for k being Nat, S being non empty ManySortedSign st S = f.k
holds f.(k+1) = S +* BitGFA1Str(ap.(k+1), bm.(k+1), cp.(k+1)) by Def11;
take f, h;
thus Sn = f.n & f.0 = S0 & h.0 = {} by Q2,Q3,PBOOLE:5;
let m be Nat, S be non empty ManySortedSign, x be set;
assume that R1: S = f.m and x = h.m;
thus f.(m+1) = SG(S,x,m) by Q4,R1;
thus h.(m+1) = oo(x,m) by PBOOLE:5;
end;
A4: for S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set, m being Nat holds
AG(S,A,x,m) is non-empty MSAlgebra over SG(S,x,m);
A5: for S,S1 being unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign, A being Boolean gate`2=den strict Circuit of S
for x being set, m being Nat st S1 = SG(S,x,m) holds
AG(S,A,x,m) is Boolean gate`2=den strict Circuit of S1;
consider AA being Boolean gate`2=den strict Circuit of Sn,
f,g,hh being ManySortedSet of NAT such that
B1: Sn = f.n & AA = g.n & f.0 = S0 & g.0 = A0 & hh.0 = {} &
for m being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set st S = f.m & A = g.m & x = hh.m
holds f.(m+1) = SG(S,x,m) & g.(m+1) = AG(S,A,x,m) & hh.(m+1) = oo(x,m)
from CIRCCMB2:sch 19(A2,A3,A4,A5);
take AA, f, g;
thus Sn = f.n & AA = g.n & f.0 = S0 & g.0 = A0 by B1;
let k be Nat, S be non empty ManySortedSign;
let A be non-empty MSAlgebra over S;
assume that C1: S = f.k & A = g.k;
C3: hh.k = hh.k;
thus f.(k+1) = S +* BitGFA1Str(ap.(k+1), bm.(k+1), cp.(k+1)) by B1,C1,C3;
thus g.(k+1) = A +* BitGFA1Circ(ap.(k+1), bm.(k+1), cp.(k+1)) by B1,C1,C3;
end;
end;
:: 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) ->
unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign means
:Def13:
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, S being non empty ManySortedSign, 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
proof
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set o0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
deffunc S(non empty ManySortedSign, set, Nat)
= $1 +* BitGFA2Str(GFA1AdderOutput(ap.($3+1), bm.($3+1), cp.($3+1)),
$2, dm.($3+1));
deffunc o(set, Nat) = GFA1CarryOutput(ap.($2+1), bm.($2+1), cp.($2+1));
for S1,S2 being unsplit gate`1=arity gate`2isBoolean non void non empty
strict non empty ManySortedSign st
(ex f,h being ManySortedSet of NAT st S1 = f.n & f.0 = S0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)) &
(ex f,h being ManySortedSet of NAT st S2 = f.n & f.0 = S0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n))
holds S1 = S2 from CIRCCMB2:sch 9;
hence thesis;
end;
existence
proof
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set o0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
A1: 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE)
is unsplit gate`1=arity gate`2isBoolean non void non empty strict;
deffunc S(set, Nat)
= BitGFA2Str(GFA1AdderOutput(ap.($2+1), bm.($2+1), cp.($2+1)),
$1, dm.($2+1));
deffunc o(set, Nat) = GFA1CarryOutput(ap.($2+1), bm.($2+1), cp.($2+1));
ex S being unsplit gate`1=arity gate`2isBoolean
non void non empty non empty strict ManySortedSign,
f,h being ManySortedSet of NAT st S = f.n & f.0 = S0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = h.n
holds f.(n+1) = S +* S(x,n) & h.(n+1) = o(x,n) from CIRCCMB2:sch 8(A1);
hence thesis;
end;
end;
:: 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) ->
Boolean gate`2=den strict Circuit of n-BitFTA1Layer2Str(ap,bm,cp,dm)
means
:Def14:
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, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S, 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
proof
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set A0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set Sn = n-BitFTA1Layer2Str(ap,bm,cp,dm);
set o0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
deffunc S(non empty ManySortedSign, set, Nat)
= $1 +* BitGFA2Str(GFA1AdderOutput(ap.($3+1), bm.($3+1), cp.($3+1)),
$2, dm.($3+1));
deffunc A(non empty ManySortedSign, non-empty MSAlgebra over $1,
set, Nat)
= $2 +* BitGFA2Circ(GFA1AdderOutput(ap.($4+1), bm.($4+1), cp.($4+1)),
$3, dm.($4+1));
deffunc o(set, Nat) = GFA1CarryOutput(ap.($2+1), bm.($2+1), cp.($2+1));
A1: for S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set, n being Nat holds
A(S,A,x,n) is non-empty MSAlgebra over S(S,x,n);
for A1,A2 being Boolean gate`2=den strict Circuit of Sn st
(ex f,g,h being ManySortedSet of NAT st Sn= f.n & A1 = g.n &
f.0 = S0 & g.0 = A0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set st S = f.n & A = g.n & x = h.n
holds f.(n+1) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x,n)) &
(ex f,g,h being ManySortedSet of NAT st Sn = f.n & A2 = g.n &
f.0 = S0 & g.0 = A0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set st S = f.n & A = g.n & x = h.n
holds f.(n+1) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x,n))
holds A1 = A2 from CIRCCMB2:sch 21(A1);
hence thesis;
end;
existence
proof
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set A0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set Sn = n-BitFTA1Layer2Str(ap,bm,cp,dm);
set o0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
deffunc S(non empty ManySortedSign, set, Nat)
= $1 +* BitGFA2Str(GFA1AdderOutput(ap.($3+1), bm.($3+1), cp.($3+1)),
$2, dm.($3+1));
deffunc A(non empty ManySortedSign, non-empty MSAlgebra over $1,
set, Nat)
= $2 +* BitGFA2Circ(GFA1AdderOutput(ap.($4+1), bm.($4+1), cp.($4+1)),
$3, dm.($4+1));
deffunc o(set, Nat) = GFA1CarryOutput(ap.($2+1), bm.($2+1), cp.($2+1));
A2: for S being unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign, x being set, n being Nat holds
S(S,x,n) is unsplit gate`1=arity gate`2isBoolean non void strict;
A3: ex f,h being ManySortedSet of NAT st Sn = f.n & f.0 = S0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n) by Def13;
A4: for S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set, n being Nat holds
A(S,A,x,n) is non-empty MSAlgebra over S(S,x,n);
A5: for S,S1 being unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign, A being Boolean gate`2=den strict Circuit of S
for x being set, n being Nat st S1 = S(S,x,n) holds
A(S,A,x,n) is Boolean gate`2=den strict Circuit of S1;
ex A being Boolean gate`2=den strict Circuit of Sn,
f,g,h being ManySortedSet of NAT st Sn = f.n & A = g.n &
f.0 = S0 & g.0 = A0 & h.0 = o0 &
for n being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S
for x being set st S = f.n & A = g.n & x = h.n
holds f.(n+1) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x,n)
from CIRCCMB2:sch 19(A2,A3,A4,A5);
hence thesis;
end;
end;
::-----------------------------------------------
:: Reassociation into Wavefront Layers (TYPE-1)
::-----------------------------------------------
:: Reassociation theorem (core of the 1-layer approach; first stage)
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
let n be Nat;
let ap,bm,cp be FinSequence;
set s0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
deffunc SS(non empty ManySortedSign, set, Nat)
= $1 +* BitGFA1Str(ap.($3+1),bm.($3+1),cp.($3+1));
deffunc oo(set, Nat) = {};
consider f being ManySortedSet of NAT such that
A1: (n+1)-BitFTA1Layer1Str(ap,bm,cp) = f.(n+1) and
A2: f.0 = s0 and
A3: for k being Nat, S being non empty ManySortedSign st S = f.k
holds f.(k+1) = S +* BitGFA1Str(ap.(k+1),bm.(k+1),cp.(k+1)) by Def11;
set h = EmptyMS NAT;
defpred T[Nat] means f.$1 is unsplit gate`1=arity gate`2isBoolean non void
non empty strict non empty ManySortedSign;
A4: T[0] by A2;
A5: for k being Nat st T[k] holds T[k+1]
proof
let k be Nat;
assume T[k];
then reconsider S = f.k as unsplit gate`1=arity gate`2isBoolean non void
non empty strict non empty ManySortedSign;
f.(k+1) = S +* BitGFA1Str(ap.(k+1),bm.(k+1),cp.(k+1)) by A3;
hence thesis;
end;
A6: for k being Nat holds T[k] from NAT_1:sch 2(A4,A5);
A7: n-BitFTA1Layer1Str(ap,bm,cp) = f.n
proof
reconsider fn = f.n as unsplit gate`1=arity gate`2isBoolean non void
non empty strict non empty ManySortedSign by A6;
B1: ex ff,hh being ManySortedSet of NAT st fn = ff.n & ff.0 = s0 &
hh.0 = {} & for k being Nat, S being non empty ManySortedSign,
x being set st S = ff.k & x = hh.k
holds ff.(k+1) = SS(S,x,k) & hh.(k+1) = oo(x,k)
proof
take f,h;
thus fn = f.n & f.0 = s0 & h.0 = {} by A2,PBOOLE:5;
let k be Nat, S be non empty ManySortedSign, x be set;
assume that C1: S = f.k and x = h.k;
thus f.(k+1) = SS(S,x,k) by A3,C1;
thus h.(k+1) = oo(x,k) by PBOOLE:5;
end;
B2: ex ff,hh being ManySortedSet of NAT st
n-BitFTA1Layer1Str(ap,bm,cp) = ff.n & ff.0 = s0 &
hh.0 = {} & for k being Nat, S being non empty ManySortedSign,
x being set st S = ff.k & x = hh.k
holds ff.(k+1) = SS(S,x,k) & hh.(k+1) = oo(x,k)
proof
consider f2 being ManySortedSet of NAT such that
C1: n-BitFTA1Layer1Str(ap,bm,cp) = f2.n and
C2: f2.0 = s0 and
C3: for k being Nat, S being non empty ManySortedSign st S = f2.k
holds f2.(k+1) = S +* BitGFA1Str(ap.(k+1),bm.(k+1),cp.(k+1)) by Def11;
reconsider h2 = EmptyMS NAT as ManySortedSet of NAT;
take f2,h2;
thus n-BitFTA1Layer1Str(ap,bm,cp) = f2.n & f2.0 = s0 & h2.0 = {}
by C1,C2,PBOOLE:5;
let k be Nat, S be non empty ManySortedSign, x be set;
assume that C4: S = f2.k and x = h2.k;
thus f2.(k+1) = SS(S,x,k) by C3,C4;
thus h2.(k+1) = oo(x,k) by PBOOLE:5;
end;
for S1,S2 being unsplit gate`1=arity gate`2isBoolean non void non empty
strict non empty ManySortedSign st
(ex ff,hh being ManySortedSet of NAT st S1 = ff.n & ff.0 = s0 &
hh.0 = {} & for k being Nat, S being non empty ManySortedSign,
x being set st S = ff.k & x = hh.k
holds ff.(k+1) = SS(S,x,k) & hh.(k+1) = oo(x,k)) &
(ex ff,hh being ManySortedSet of NAT st S2 = ff.n & ff.0 = s0 &
hh.0 = {} & for k being Nat, S being non empty ManySortedSign,
x being set st S = ff.k & x = hh.k
holds ff.(k+1) = SS(S,x,k) & hh.(k+1) = oo(x,k))
holds S1 = S2 from CIRCCMB2:sch 9;
hence thesis by B1,B2;
end;
thus thesis by A1,A3,A7;
end;
:: Layer-2 structure, one-step unfolding: the (n+1)-stage Layer-2
:: structure is the n-stage one composed with one more stage-2 cell
:: (a BitGFA2 fed the stage-1 adder output and the n-stage carry).
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
let n be Nat;
let ap,bm,cp,dm be FinSequence;
set s0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set h0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
deffunc SS(non empty ManySortedSign, set, Nat)
= $1 +* BitGFA2Str(GFA1AdderOutput(ap.($3+1),bm.($3+1),cp.($3+1)),
$2, dm.($3+1));
deffunc oo(set, Nat) = GFA1CarryOutput(ap.($2+1),bm.($2+1),cp.($2+1));
deffunc FC(Nat, set) = GFA1CarryOutput(ap.($1+1),bm.($1+1),cp.($1+1));
consider g,h being ManySortedSet of NAT such that
A1: (n+1)-BitFTA1Layer2Str(ap,bm,cp,dm) = g.(n+1) and
A2: g.0 = s0 and
A3: h.0 = h0 and
A4: for k being Nat, S being non empty ManySortedSign, 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))
by Def13;
defpred TT[Nat] means g.$1 is unsplit gate`1=arity gate`2isBoolean non void
non empty strict non empty ManySortedSign;
A5: TT[0] by A2;
A6: for k being Nat st TT[k] holds TT[k+1]
proof
let k be Nat;
assume TT[k];
then reconsider S = g.k as unsplit gate`1=arity gate`2isBoolean non void
non empty strict non empty ManySortedSign;
g.(k+1) = S +* BitGFA2Str(GFA1AdderOutput(ap.(k+1),bm.(k+1),cp.(k+1)),
h.k, dm.(k+1)) by A4;
hence thesis;
end;
A7: for k being Nat holds TT[k] from NAT_1:sch 2(A5,A6);
A8: for k being Nat holds h.(k+1) = FC(k,h.k)
proof
let k be Nat;
reconsider S = g.k as unsplit gate`1=arity gate`2isBoolean non void
non empty strict non empty ManySortedSign by A7;
reconsider z = h.k as set;
S = g.k & z = h.k;
hence thesis by A4;
end;
consider h3 being ManySortedSet of NAT such that
A9: n-BitFTA1CarryOutput(ap,bm,cp,dm) = h3.n and
A10: h3.0 = h0 and
A11: for k being Nat holds h3.(k+1) = BitFTA1CarryOutput(ap.(k+1),bm.(k+1),
cp.(k+1),dm.(k+1), h3.k) by Def10;
A12: for k being Nat holds h3.(k+1) = FC(k,h3.k)
proof
let k be Nat;
h3.(k+1) = BitFTA1CarryOutput(ap.(k+1),bm.(k+1),cp.(k+1),dm.(k+1),h3.k)
by A11
.= GFA1CarryOutput(ap.(k+1),bm.(k+1),cp.(k+1));
hence thesis;
end;
A13: dom h = NAT by PARTFUN1:def 2;
A14: dom h3 = NAT by PARTFUN1:def 2;
A15: h = h3 from NAT_1:sch 15(A13,A3,A8,A14,A10,A12);
A16: n-BitFTA1Layer2Str(ap,bm,cp,dm) = g.n
proof
reconsider gn = g.n as unsplit gate`1=arity gate`2isBoolean non void
non empty strict non empty ManySortedSign by A7;
gn = n-BitFTA1Layer2Str(ap,bm,cp,dm) by A2,A3,A4,Def13;
hence thesis;
end;
thus thesis by A1,A4,A15,A9,A16;
end;
:: Main proposition - Two-Layer Circuit Composition (Structure-level)
theorem Th16:
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
defpred R[Nat] means for ap,bm,cp,dm being FinSequence holds
$1-BitFTA1Str(ap,bm,cp,dm) = ($1-BitFTA1Layer1Str(ap,bm,cp))
+* ($1-BitFTA1Layer2Str(ap,bm,cp,dm));
A1: R[0]
proof
let ap,bm,cp,dm be FinSequence;
set s0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
consider f being ManySortedSet of NAT such that
B1: 0-BitFTA1Layer1Str(ap,bm,cp) = f.0 and B2: f.0 = s0 and
for k being Nat, S being non empty ManySortedSign st S = f.k
holds f.(k+1) = S +* BitGFA1Str(ap.(k+1),bm.(k+1),cp.(k+1)) by Def11;
consider g,h being ManySortedSet of NAT such that
B3: 0-BitFTA1Layer2Str(ap,bm,cp,dm) = g.0 and B4: g.0 = s0 and
h.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE] and
for k being Nat, S being non empty ManySortedSign, 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))
by Def13;
s0 +* s0
= s0 by CIRCCOMB:4;
hence thesis by B1,B2,B3,B4,Th13;
end;
A2: for k being Nat st R[k] holds R[k+1]
proof
let k be Nat;
assume B1: R[k];
let ap,bm,cp,dm be FinSequence;
set a = k-BitFTA1Layer1Str(ap,bm,cp);
set b = k-BitFTA1Layer2Str(ap,bm,cp,dm);
set s1 = BitGFA1Str(ap.(k+1),bm.(k+1),cp.(k+1));
set s2 = BitGFA2Str(GFA1AdderOutput(ap.(k+1),bm.(k+1),cp.(k+1)),
k-BitFTA1CarryOutput(ap,bm,cp,dm), dm.(k+1));
B2: k-BitFTA1Str(ap,bm,cp,dm) = a +* b by B1;
B3: BitFTA1Str(ap.(k+1),bm.(k+1),cp.(k+1),dm.(k+1),
k-BitFTA1CarryOutput(ap,bm,cp,dm)) = s1 +* s2;
B4: (k+1)-BitFTA1Str(ap,bm,cp,dm) = (a +* b) +* (s1 +* s2) by Th14,B2,B3;
B5: (k+1)-BitFTA1Layer2Str(ap,bm,cp,dm) = b +* s2 by LmT15B;
(a +* b) +* (s1 +* s2) = a +* (b +* (s1 +* s2)) by CIRCCOMB:6
.= a +* ((b +* s1) +* s2) by CIRCCOMB:6
.= a +* ((s1 +* b) +* s2) by FACIRC_1:23
.= a +* (s1 +* (b +* s2)) by CIRCCOMB:6
.= (a +* s1) +* (b +* s2) by CIRCCOMB:6;
hence thesis by B4,LmT15A,B5;
end;
for n being Nat holds R[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
:: Reassociation theorem (core of the 1-layer approach; first stage)
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
let n be Nat;
let ap,bm,cp be FinSequence;
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set A0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
deffunc SG(non empty ManySortedSign, set, Nat)
= $1 +* BitGFA1Str(ap.($3+1),bm.($3+1),cp.($3+1));
deffunc AG(non empty ManySortedSign, non-empty MSAlgebra over $1,
set, Nat) = $2 +* BitGFA1Circ(ap.($4+1),bm.($4+1),cp.($4+1));
deffunc oo(set, Nat) = {};
consider f1,g1 being ManySortedSet of NAT such that
A1: n-BitFTA1Layer1Str(ap,bm,cp) = f1.n and
A2: n-BitFTA1Layer1Circ(ap,bm,cp) = g1.n and
A3: f1.0 = S0 and A4: g1.0 = A0 and
A5: for k being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S st S = f1.k & A = g1.k holds
f1.(k+1) = S +* BitGFA1Str(ap.(k+1),bm.(k+1),cp.(k+1)) &
g1.(k+1) = A +* BitGFA1Circ(ap.(k+1),bm.(k+1),cp.(k+1)) by Def12;
consider f2,g2 being ManySortedSet of NAT such that
(n+1)-BitFTA1Layer1Str(ap,bm,cp) = f2.(n+1) and
A6: (n+1)-BitFTA1Layer1Circ(ap,bm,cp) = g2.(n+1) and
A7: f2.0 = S0 and A8: g2.0 = A0 and
A9: for k being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S st S = f2.k & A = g2.k holds
f2.(k+1) = S +* BitGFA1Str(ap.(k+1),bm.(k+1),cp.(k+1)) &
g2.(k+1) = A +* BitGFA1Circ(ap.(k+1),bm.(k+1),cp.(k+1)) by Def12;
reconsider h1 = EmptyMS NAT, h2 = EmptyMS NAT as ManySortedSet of NAT;
A10: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
st S = f1.0 & A = g1.0 by A3,A4;
A11: f1.0 = f2.0 & g1.0 = g2.0 & h1.0 = h2.0 by A3,A4,A7,A8;
A12: for k being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S for x being set
st S = f1.k & A = g1.k & x = h1.k holds
f1.(k+1) = SG(S,x,k) & g1.(k+1) = AG(S,A,x,k) & h1.(k+1) = oo(x,k)
by A5,PBOOLE:5;
A13: for k being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S for x being set
st S = f2.k & A = g2.k & x = h2.k holds
f2.(k+1) = SG(S,x,k) & g2.(k+1) = AG(S,A,x,k) & h2.(k+1) = oo(x,k)
by A9,PBOOLE:5;
A14: for S being non empty ManySortedSign, A being non-empty MSAlgebra over S
for x being set, k being Nat holds
AG(S,A,x,k) is non-empty MSAlgebra over SG(S,x,k);
A15: f1 = f2 & g1 = g2 & h1 = h2 from CIRCCMB2:sch 14(A10,A11,A12,A13,A14);
thus thesis by A15,A6,A5,A1,A2;
end;
:: Layer-2 circuit, one-step unfolding: the Circ (MSAlgebra) counterpart
:: of LmT15B, unfolding the (n+1)-stage Layer-2 circuit by one stage-2 cell.
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
let n be Nat;
let ap,bm,cp,dm be FinSequence;
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set A0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
set h0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
deffunc SG(non empty ManySortedSign, set, Nat)
= $1 +* BitGFA2Str(GFA1AdderOutput(ap.($3+1),bm.($3+1),cp.($3+1)),
$2, dm.($3+1));
deffunc AG(non empty ManySortedSign, non-empty MSAlgebra over $1,
set, Nat)
= $2 +* BitGFA2Circ(GFA1AdderOutput(ap.($4+1),bm.($4+1),cp.($4+1)),
$3, dm.($4+1));
deffunc oo(set, Nat) = GFA1CarryOutput(ap.($2+1),bm.($2+1),cp.($2+1));
deffunc FC(Nat, set) = GFA1CarryOutput(ap.($1+1),bm.($1+1),cp.($1+1));
consider f1,g1,h1 being ManySortedSet of NAT such that
A1: n-BitFTA1Layer2Str(ap,bm,cp,dm) = f1.n and
A2: n-BitFTA1Layer2Circ(ap,bm,cp,dm) = g1.n and
A3: f1.0 = S0 and A4: g1.0 = A0 and A5: h1.0 = h0 and
A6: for k being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S, z being set
st S = f1.k & A = g1.k & z = h1.k holds
f1.(k+1) = S +* BitGFA2Str(GFA1AdderOutput(ap.(k+1),bm.(k+1),cp.(k+1)),
z, dm.(k+1)) &
g1.(k+1) = A +* BitGFA2Circ(GFA1AdderOutput(ap.(k+1),bm.(k+1),cp.(k+1)),
z, dm.(k+1)) &
h1.(k+1) = GFA1CarryOutput(ap.(k+1),bm.(k+1),cp.(k+1)) by Def14;
consider f2,g2,h2 being ManySortedSet of NAT such that
(n+1)-BitFTA1Layer2Str(ap,bm,cp,dm) = f2.(n+1) and
A7: (n+1)-BitFTA1Layer2Circ(ap,bm,cp,dm) = g2.(n+1) and
A8: f2.0 = S0 and A9: g2.0 = A0 and A10: h2.0 = h0 and
A11: for k being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S, z being set
st S = f2.k & A = g2.k & z = h2.k holds
f2.(k+1) = S +* BitGFA2Str(GFA1AdderOutput(ap.(k+1),bm.(k+1),cp.(k+1)),
z, dm.(k+1)) &
g2.(k+1) = A +* BitGFA2Circ(GFA1AdderOutput(ap.(k+1),bm.(k+1),cp.(k+1)),
z, dm.(k+1)) &
h2.(k+1) = GFA1CarryOutput(ap.(k+1),bm.(k+1),cp.(k+1)) by Def14;
A12: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
st S = f1.0 & A = g1.0 by A3,A4;
A13: f1.0 = f2.0 & g1.0 = g2.0 & h1.0 = h2.0 by A3,A4,A5,A8,A9,A10;
A14: for k being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S for x being set
st S = f1.k & A = g1.k & x = h1.k holds
f1.(k+1) = SG(S,x,k) & g1.(k+1) = AG(S,A,x,k) & h1.(k+1) = oo(x,k)
by A6;
A15: for k being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S for x being set
st S = f2.k & A = g2.k & x = h2.k holds
f2.(k+1) = SG(S,x,k) & g2.(k+1) = AG(S,A,x,k) & h2.(k+1) = oo(x,k)
by A11;
A16: for S being non empty ManySortedSign, A being non-empty MSAlgebra over S
for x being set, k being Nat holds
AG(S,A,x,k) is non-empty MSAlgebra over SG(S,x,k);
A17: f1 = f2 & g1 = g2 & h1 = h2 from CIRCCMB2:sch 14(A12,A13,A14,A15,A16);
A18: f1.0 = S0 & g1.0 = A0 by A3,A4;
A19: for k being Nat, S being non empty ManySortedSign, z being set
st S = f1.k & z = h1.k holds f1.(k+1) = SG(S,z,k) &
h1.(k+1) = oo(z,k) from CIRCCMB2:sch 15(A18,A14,A16);
A20: for k being Nat, z being set st z = h1.k
holds h1.(k+1) = oo(z,k) from CIRCCMB2:sch 3(A3,A19);
A21: for k being Nat holds h1.(k+1) = FC(k,h1.k)
proof
let k be Nat;
h1.k = h1.k;
hence thesis by A20;
end;
consider h3 being ManySortedSet of NAT such that
A22: n-BitFTA1CarryOutput(ap,bm,cp,dm) = h3.n and
A23: h3.0 = h0 and
A24: for k being Nat holds h3.(k+1) = BitFTA1CarryOutput(ap.(k+1),bm.(k+1),
cp.(k+1),dm.(k+1), h3.k) by Def10;
A25: for k being Nat holds h3.(k+1) = FC(k,h3.k)
proof
let k be Nat;
h3.(k+1) = BitFTA1CarryOutput(ap.(k+1),bm.(k+1),cp.(k+1),dm.(k+1),h3.k)
by A24
.= GFA1CarryOutput(ap.(k+1),bm.(k+1),cp.(k+1));
hence thesis;
end;
A26: dom h1 = NAT by PARTFUN1:def 2;
A27: dom h3 = NAT by PARTFUN1:def 2;
A28: h1 = h3 from NAT_1:sch 15(A26,A5,A21,A27,A23,A25);
thus thesis by A17,A7,A6,A28,A22,A1,A2;
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:
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
let n be Nat;
let ap,bm,cp,dm be FinSequence;
set A0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
defpred P[Nat] means
$1-BitFTA1Circ(ap,bm,cp,dm) = ($1-BitFTA1Layer1Circ(ap,bm,cp))
+* ($1-BitFTA1Layer2Circ(ap,bm,cp,dm));
A1: P[0]
proof
B1: 0-BitFTA1Layer1Circ(ap,bm,cp) = A0
proof
consider f,g being ManySortedSet of NAT such that
0-BitFTA1Layer1Str(ap,bm,cp) = f.0 and
C1: 0-BitFTA1Layer1Circ(ap,bm,cp) = g.0 and
f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) and
C2: g.0 = A0 and
for k being Nat, S being non empty ManySortedSign,
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)) by Def12;
thus thesis by C1,C2;
end;
B2: 0-BitFTA1Layer2Circ(ap,bm,cp,dm) = A0
proof
consider f,g,h being ManySortedSet of NAT such that
0-BitFTA1Layer2Str(ap,bm,cp,dm) = f.0 and
C1: 0-BitFTA1Layer2Circ(ap,bm,cp,dm) = g.0 and
f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) and
C2: g.0 = A0 and h.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE] and
for k being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S, 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)) by Def14;
thus thesis by C1,C2;
end;
set sa = the Sorts of A0, ca = the Charact of A0;
B3: the Sorts of ((0-BitFTA1Layer1Circ(ap,bm,cp))
+* (0-BitFTA1Layer2Circ(ap,bm,cp,dm))) = the Sorts of A0
proof
the Sorts of ((0-BitFTA1Layer1Circ(ap,bm,cp))
+* (0-BitFTA1Layer2Circ(ap,bm,cp,dm)))
= sa +* sa by B1,B2,CIRCCOMB:def 4
.= sa;
hence thesis;
end;
the Charact of ((0-BitFTA1Layer1Circ(ap,bm,cp))
+* (0-BitFTA1Layer2Circ(ap,bm,cp,dm)))
= ca +* ca by B1,B2,CIRCCOMB:def 4
.= ca;
hence thesis by Th13,B3;
end;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that B1: P[k];
set Lk1 = k-BitFTA1Layer1Circ(ap,bm,cp);
set Lk2 = k-BitFTA1Layer2Circ(ap,bm,cp,dm);
set cc = k-BitFTA1CarryOutput(ap,bm,cp,dm);
set s1 = BitGFA1Circ(ap.(k+1),bm.(k+1),cp.(k+1));
set s2 = BitGFA2Circ(
GFA1AdderOutput(ap.(k+1),bm.(k+1),cp.(k+1)), cc, dm.(k+1));
set cell = BitFTA1Circ(ap.(k+1),bm.(k+1),cp.(k+1),dm.(k+1), cc);
B2: (k+1)-BitFTA1Circ(ap,bm,cp,dm) = (k-BitFTA1Circ(ap,bm,cp,dm)) +* cell
by Th14;
B3: (k+1)-BitFTA1Layer1Circ(ap,bm,cp) = Lk1 +* s1 by LmT16A;
B4: (k+1)-BitFTA1Layer2Circ(ap,bm,cp,dm) = Lk2 +* s2 by LmT16B;
set l1 = the Sorts of Lk1, l2 = the Sorts of Lk2;
set t1 = the Sorts of s1, t2 = the Sorts of s2;
set d1 = the Charact of Lk1, d2 = the Charact of Lk2;
set e1 = the Charact of s1, e2 = the Charact of s2;
B5: l1 tolerates l2 by CIRCCOMB:59;
B6: t1 tolerates t2 by CIRCCOMB:59;
B7: l1 tolerates t1 by CIRCCOMB:59;
B8: l2 tolerates t2 by CIRCCOMB:59;
B9: the Sorts of (k-BitFTA1Circ(ap,bm,cp,dm))
tolerates the Sorts of cell by CIRCCOMB:59;
B10: the Sorts of ((k+1)-BitFTA1Layer1Circ(ap,bm,cp))
tolerates the Sorts of ((k+1)-BitFTA1Layer2Circ(ap,bm,cp,dm))
by CIRCCOMB:59;
:: LHS: descend to map-level via CIRCCOMB:def 4 FIRST, then
:: substitute IH/CELL (map +* is total so congruence holds);
:: no rewrite through Circ +*.
B11: the Sorts of ((k+1)-BitFTA1Circ(ap,bm,cp,dm))
= (the Sorts of (Lk1 +* Lk2)) +* (the Sorts of (s1 +* s2)) by B1,B9,
CIRCCOMB:def 4,B2
.= (l1 +* l2) +* (the Sorts of (s1 +* s2)) by B5,CIRCCOMB:def 4
.= (l1 +* l2) +* (t1 +* t2) by B6,CIRCCOMB:def 4;
B12: the Sorts of (((k+1)-BitFTA1Layer1Circ(ap,bm,cp))
+* ((k+1)-BitFTA1Layer2Circ(ap,bm,cp,dm)))
= (the Sorts of (Lk1 +* s1)) +* (the Sorts of (Lk2 +* s2)) by B4,B3,B10,
CIRCCOMB:def 4
.= (l1 +* t1) +* (the Sorts of (Lk2 +* s2)) by B7,CIRCCOMB:def 4
.= (l1 +* t1) +* (l2 +* t2) by B8,CIRCCOMB:def 4;
B13: the Sorts of ((k+1)-BitFTA1Circ(ap,bm,cp,dm))
= the Sorts of (((k+1)-BitFTA1Layer1Circ(ap,bm,cp))
+* ((k+1)-BitFTA1Layer2Circ(ap,bm,cp,dm)))
by CIRCCOMB:59,LmF,B11,B12;
B14: the Charact of ((k+1)-BitFTA1Circ(ap,bm,cp,dm))
= (the Charact of (Lk1 +* Lk2)) +* (the Charact of (s1 +* s2)) by B1,B9,
CIRCCOMB:def 4,B2
.= (d1 +* d2) +* (the Charact of (s1 +* s2)) by B5,CIRCCOMB:def 4
.= (d1 +* d2) +* (e1 +* e2) by B6,CIRCCOMB:def 4;
B15: the Charact of (((k+1)-BitFTA1Layer1Circ(ap,bm,cp))
+* ((k+1)-BitFTA1Layer2Circ(ap,bm,cp,dm)))
= (the Charact of (Lk1 +* s1)) +* (the Charact of (Lk2 +* s2)) by B4,B3,
B10,CIRCCOMB:def 4
.= (d1 +* e1) +* (the Charact of (Lk2 +* s2)) by B7,CIRCCOMB:def 4
.= (d1 +* e1) +* (d2 +* e2) by B8,CIRCCOMB:def 4;
(d1 +* d2) +* (e1 +* e2) = (d1 +* e1) +* (d2 +* e2) by CIRCCOMB:48,LmF;
hence thesis by B13,B14,B15;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
::--------------------------------
:: Vertex structure of the wavefront layers (goal prerequisites)
::--------------------------------
:: Base values of the layer structures.
LmT10L1: for ap,bm,cp being FinSequence holds
0-BitFTA1Layer1Str(ap,bm,cp)
= 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE)
proof
let ap,bm,cp be FinSequence;
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
consider f being ManySortedSet of NAT such that
A1: 0-BitFTA1Layer1Str(ap,bm,cp) = f.0 and A2: f.0 = S0 and
for k being Nat, S being non empty ManySortedSign st S = f.k
holds f.(k+1) = S +* BitGFA1Str(ap.(k+1),bm.(k+1),cp.(k+1)) by Def11;
thus thesis by A1,A2;
end;
:: The 0-bit Layer-2 structure is the FALSE base gate.
LmT10L2: for ap,bm,cp,dm being FinSequence holds
0-BitFTA1Layer2Str(ap,bm,cp,dm)
= 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE)
proof
let ap,bm,cp,dm be FinSequence;
set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
consider g,h being ManySortedSet of NAT such that
A1: 0-BitFTA1Layer2Str(ap,bm,cp,dm) = g.0 and A2: g.0 = S0 and
h.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE] and
for k being Nat, S being non empty ManySortedSign, 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))
by Def13;
thus thesis by A1,A2;
end;
:: InnerVertices of Layer 2 are all pairs (gate vertices + FALSE base output).
LmT1L2rel: for n being Nat for ap,bm,cp,dm being FinSequence holds
InnerVertices (n-BitFTA1Layer2Str(ap,bm,cp,dm)) is Relation
proof
let n be Nat;
let ap,bm,cp,dm be FinSequence;
deffunc S(Nat) = $1-BitFTA1Layer2Str(ap,bm,cp,dm);
defpred P[Nat] means InnerVertices (S($1)) is Relation;
S(0) = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) by LmT10L2;
then
A1: P[ 0 ] by FACIRC_1:38;
A2: now
let i be Nat;
assume B1: P[i];
B2: S(i+1) = S(i) +* BitGFA2Str(
GFA1AdderOutput(ap.(i+1),bm.(i+1),cp.(i+1)),
i-BitFTA1CarryOutput(ap,bm,cp,dm), dm.(i+1)) by LmT15B;
InnerVertices BitGFA2Str(
GFA1AdderOutput(ap.(i+1),bm.(i+1),cp.(i+1)),
i-BitFTA1CarryOutput(ap,bm,cp,dm), dm.(i+1)) is Relation by GFACIRC1:96;
hence P[i+1] by B1,B2,FACIRC_1:3;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
:: InputVertices of Layer 1 are all non-pairs (primary inputs only).
LmT1L1wp: for n being Nat for ap,bm,cp being nonpair-yielding FinSequence holds
InputVertices (n-BitFTA1Layer1Str(ap,bm,cp)) is without_pairs
proof
let n be Nat;
let ap,bm,cp be nonpair-yielding FinSequence;
deffunc S(Nat) = $1-BitFTA1Layer1Str(ap,bm,cp);
defpred P[Nat] means InputVertices (S($1)) is without_pairs;
S(0) = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) by LmT10L1;
then
A1: P[ 0 ] by FACIRC_1:39;
A2: now
let i be Nat;
assume B1: P[i];
set B = BitGFA1Str(ap.(i+1),bm.(i+1),cp.(i+1));
B2: S(i+1) = S(i) +* B by LmT15A;
reconsider w1 = InputVertices (S(i)) as without_pairs set by B1;
reconsider w2 = InputVertices B as without_pairs set by GFACIRC1:67;
InputVertices (S(i+1))
= (w1 \ InnerVertices B) \/ (w2 \ InnerVertices (S(i)))
by B2,CIRCCOMB:47,CIRCCMB2:5;
hence P[i+1];
end;
for i being Nat holds P[i] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
:: Feed-forward disjointness : Layer 1 inputs miss Layer 2 gates.
theorem Th18:
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
let n be Nat;
let ap,bm,cp,dm be nonpair-yielding FinSequence;
InputVertices (n-BitFTA1Layer1Str(ap,bm,cp)) is without_pairs by LmT1L1wp;
hence thesis by FACIRC_1:5,LmT1L2rel;
end;
::-----------------------------------------------------------
:: InnerVertices of Layer 1 are gate outputs (pairs) : a Relation.
::-----------------------------------------------------------
LmT1L1rel: for n being Nat for ap,bm,cp being FinSequence holds
InnerVertices (n-BitFTA1Layer1Str(ap,bm,cp)) is Relation
proof
let n be Nat;
let ap,bm,cp be FinSequence;
deffunc S(Nat) = $1-BitFTA1Layer1Str(ap,bm,cp);
defpred P[Nat] means InnerVertices (S($1)) is Relation;
S(0) = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) by LmT10L1;
then
A1: P[ 0 ] by FACIRC_1:38;
A2: now
let i be Nat;
assume B1: P[i];
B2: S(i+1) = S(i) +* BitGFA1Str(ap.(i+1),bm.(i+1),cp.(i+1)) by LmT15A;
InnerVertices BitGFA1Str(ap.(i+1),bm.(i+1),cp.(i+1)) is Relation
by GFACIRC1:64;
hence P[i+1] by B1,B2,FACIRC_1:3;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
:: Carry output is never a 2-input NOR gate (first-component length differs).
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
let n be Nat;
let ap,bm,cp,dm be FinSequence;
let x,y be set;
consider h being ManySortedSet of NAT such that
A1: n-BitFTA1CarryOutput(ap,bm,cp,dm) = h.n and
A2: h.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE] and
A3: for k being Nat holds
h.(k+1) = BitFTA1CarryOutput(ap.(k+1),bm.(k+1),cp.(k+1),dm.(k+1),h.k)
by Def10;
assume A4: n-BitFTA1CarryOutput(ap,bm,cp,dm) = [<*x,y*>,nor2];
per cases by NAT_1:6;
suppose n = 0;
hence contradiction by XTUPLE_0:1,A1,A2,A4;
end;
suppose ex m being Nat st n = m+1;
then consider m being Nat such that B1: n = m+1;
n-BitFTA1CarryOutput(ap,bm,cp,dm)
= BitFTA1CarryOutput(ap.(m+1),bm.(m+1),cp.(m+1),dm.(m+1),h.m)
by A1,A3,B1
.= [<*[<*ap.(m+1),bm.(m+1)*>,and2c],[<*bm.(m+1),cp.(m+1)*>,and2a],
[<*cp.(m+1),ap.(m+1)*>,and2]*>,or3];
then <*x,y*>
= <*[<*ap.(m+1),bm.(m+1)*>,and2c],[<*bm.(m+1),cp.(m+1)*>,and2a],
[<*cp.(m+1),ap.(m+1)*>,and2]*> by XTUPLE_0:1,A4;
then len <*x,y*> = 3 by FINSEQ_1:45;
hence contradiction by FINSEQ_1:44;
end;
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:
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
let n be Nat;
let ap,bm,cp be nonpair-yielding FinSequence;
set A0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
defpred P[Nat] means
for s being State of $1-BitFTA1Layer1Circ(ap,bm,cp)
holds Following(s,2) is stable;
A1: 0-BitFTA1Layer1Circ(ap,bm,cp) = A0
proof
consider f,g being ManySortedSet of NAT such that
0-BitFTA1Layer1Str(ap,bm,cp) = f.0 and
B1: 0-BitFTA1Layer1Circ(ap,bm,cp) = g.0 and
f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) and
B2: g.0 = A0 and
for k being Nat, S being non empty ManySortedSign,
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)) by Def12;
thus thesis by B1,B2;
end;
A2: P[ 0 ]
proof
let s be State of 0-BitFTA1Layer1Circ(ap,bm,cp);
reconsider s0 = s as State of A0 by A1;
B1: Following(s0,1) = Following s0 by FACIRC_1:14;
B2: Following(s0,2) = Following(s0,1) by B1,CIRCCMB2:2,CIRCCMB2:4;
B3: 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE)
= 0-BitFTA1Layer1Str(ap,bm,cp) by LmT10L1;
thus thesis by B3,A1,B2,B1,CIRCCMB2:2;
end;
A3: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume B1: P[i];
reconsider S1 = i-BitFTA1Layer1Str(ap,bm,cp)
as non void Circuit-like non empty ManySortedSign;
set B = BitGFA1Str(ap.(i+1),bm.(i+1),cp.(i+1));
reconsider B as non void Circuit-like non empty ManySortedSign;
reconsider SS = (i+1)-BitFTA1Layer1Str(ap,bm,cp)
as non void Circuit-like non empty ManySortedSign;
reconsider A1a = i-BitFTA1Layer1Circ(ap,bm,cp)
as non-empty Circuit of S1;
reconsider Ba = BitGFA1Circ(ap.(i+1),bm.(i+1),cp.(i+1))
as non-empty Circuit of B;
reconsider AA = (i+1)-BitFTA1Layer1Circ(ap,bm,cp)
as non-empty Circuit of SS;
B2: AA = A1a +* Ba by LmT16A;
B3: A1a tolerates Ba by CIRCCOMB:60;
InputVertices S1 is without_pairs by LmT1L1wp;
then
B4: InputVertices S1 misses InnerVertices B by GFACIRC1:64,FACIRC_1:5;
InputVertices B is without_pairs by GFACIRC1:67;
then
B5: InputVertices B misses InnerVertices S1 by LmT1L1rel,FACIRC_1:5;
B6: for s being State of Ba holds Following(s,2) is stable
by GFACIRC1:72;
now
let s be State of AA;
C1: Following(s,2) is stable
proof
2 = max(2,2);
hence thesis by LmT15A,B2,B3,B4,B5,B1,B6,CIRCCMB2:24;
end;
thus Following(s,2) is stable by C1;
end;
hence P[i+1];
end;
for i being Nat holds P[i] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
:: Layer 2 inner vertices grow by the new stage-2 gates at each step.
:: Backbone for the disjointness reasoning inside Th20.
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
let n be Nat;
let ap,bm,cp,dm be FinSequence;
set B = BitGFA2Str(GFA1AdderOutput(ap.(n+1),bm.(n+1),cp.(n+1)),
n-BitFTA1CarryOutput(ap,bm,cp,dm), dm.(n+1));
reconsider S1 = n-BitFTA1Layer2Str(ap,bm,cp,dm) as unsplit gate`1=arity
gate`2isBoolean non void non empty strict non empty ManySortedSign;
thus InnerVertices ((n+1)-BitFTA1Layer2Str(ap,bm,cp,dm))
= InnerVertices (S1 +* B) by LmT15B
.= InnerVertices (n-BitFTA1Layer2Str(ap,bm,cp,dm))
\/ InnerVertices B by FACIRC_1:27;
end;
::-----------------------------------------------------------
:: Conditional 2-stability of Layer 2 (carry seed settled).
:: Layer 2 contains the FALSE base gate whose output vertex
:: [<*>,(0-tuples_on BOOLEAN)-->FALSE] feeds cell 1, so universal
:: 2-stability fails by one step. Once that vertex is settled at
:: FALSE (true of Following(s,2) in the full circuit), two more
:: steps stabilize the layer: the k = 0 cell composes by cascade
:: with n1 = 0 (CIRCCMB2:19) and later cells compose in parallel
:: (CIRCCMB2:22).
::-----------------------------------------------------------
:: The carry stream starts at the FALSE base output vertex.
LmT10CO: for ap,bm,cp,dm being FinSequence holds
0-BitFTA1CarryOutput(ap,bm,cp,dm) = [<*>,(0-tuples_on BOOLEAN)-->FALSE]
proof
let ap,bm,cp,dm be FinSequence;
consider h being ManySortedSet of NAT such that
A1: 0-BitFTA1CarryOutput(ap,bm,cp,dm) = h.0 and
A2: h.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE] and
for k being Nat holds
h.(k+1) = BitFTA1CarryOutput(ap.(k+1),bm.(k+1),cp.(k+1),dm.(k+1),h.k)
by Def10;
thus thesis by A1,A2;
end;
:: From index 1 on, the carry stream is the stage-1 carry output.
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
let m be Nat;
let ap,bm,cp,dm be FinSequence;
consider h being ManySortedSet of NAT such that
A1: (m+1)-BitFTA1CarryOutput(ap,bm,cp,dm) = h.(m+1) and
h.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE] and
A2: for k being Nat holds
h.(k+1) = BitFTA1CarryOutput(ap.(k+1),bm.(k+1),cp.(k+1),dm.(k+1),h.k)
by Def10;
thus (m+1)-BitFTA1CarryOutput(ap,bm,cp,dm)
= BitFTA1CarryOutput(ap.(m+1),bm.(m+1),cp.(m+1),dm.(m+1),h.m) by A1,A2
.= GFA1CarryOutput(ap.(m+1),bm.(m+1),cp.(m+1));
end;
:: The carry stream vertex is always a pair.
LmT1COp: for n being Nat for ap,bm,cp,dm being FinSequence holds
n-BitFTA1CarryOutput(ap,bm,cp,dm) is pair
proof
let n be Nat;
let ap,bm,cp,dm be FinSequence;
per cases by NAT_1:6;
suppose n = 0;
hence thesis by LmT10CO;
end;
suppose ex m being Nat st n = m+1;
then consider m being Nat such that B1: n = m+1;
n-BitFTA1CarryOutput(ap,bm,cp,dm)
= GFA1CarryOutput(ap.(m+1),bm.(m+1),cp.(m+1)) by B1,LmT1COk
.= [<*[<*ap.(m+1),bm.(m+1)*>,and2c],[<*bm.(m+1),cp.(m+1)*>,and2a],
[<*cp.(m+1),ap.(m+1)*>,and2]*>,or3];
hence thesis;
end;
end;
:: A stage-1 adder output never occurs among the gates of a
:: stage-2 cell whose middle input is a pair.
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
let a,b,c be non pair set;
let X,Y,d be set such that
A1: Y is pair;
set w = GFA1AdderOutput(a,b,c);
set bA = GFA2AdderOutput(X,Y,d), bC = GFA2CarryOutput(X,Y,d);
assume w in InnerVertices BitGFA2Str(X,Y,d);
then w in {[<*X,Y*>,xor2c]} \/ {bA} \/
{[<*X,Y*>,and2a],[<*Y,d*>,and2c],[<*d,X*>,nor2]} \/ {bC} by GFACIRC1:95;
then w in {[<*X,Y*>,xor2c]} \/ {bA} \/
{[<*X,Y*>,and2a],[<*Y,d*>,and2c],[<*d,X*>,nor2]} or w in {bC}
by XBOOLE_0:def 3;
then w in ({[<*X,Y*>,xor2c]} \/ {bA}) or
w in {[<*X,Y*>,and2a],[<*Y,d*>,and2c],[<*d,X*>,nor2]} or w in {bC}
by XBOOLE_0:def 3;
then A2: w in {[<*X,Y*>,xor2c]} or w in {bA} or
w in {[<*X,Y*>,and2a],[<*Y,d*>,and2c],[<*d,X*>,nor2]} or w in {bC}
by XBOOLE_0:def 3;
per cases by A2,TARSKI:def 1,ENUMSET1:def 1;
suppose w = [<*X,Y*>,xor2c];
then <*[<*a,b*>,xor2c],c*> = <*X,Y*> by XTUPLE_0:1;
hence contradiction by A1,FINSEQ_1:77;
end;
suppose w = bA;
then <*[<*a,b*>,xor2c],c*> = <*[<*X,Y*>,xor2c],d*> by XTUPLE_0:1;
then B1: [<*a,b*>,xor2c] = [<*X,Y*>,xor2c] by FINSEQ_1:77;
<*a,b*> = <*X,Y*> by B1,XTUPLE_0:1;
hence contradiction by A1,FINSEQ_1:77;
end;
suppose w = [<*X,Y*>,and2a];
hence contradiction by GFACIRC1:4,TWOSCOMP:9,XTUPLE_0:1;
end;
suppose w = [<*Y,d*>,and2c];
hence contradiction by GFACIRC1:4,GFACIRC1:3,XTUPLE_0:1;
end;
suppose w = [<*d,X*>,nor2];
hence contradiction by GFACIRC1:4,TWOSCOMP:9,XTUPLE_0:1;
end;
suppose w = bC;
then B1: <*[<*a,b*>,xor2c],c*>
= <*[<*X,Y*>,and2a],[<*Y,d*>,and2c],[<*d,X*>,nor2]*> by XTUPLE_0:1;
len <*[<*a,b*>,xor2c],c*> = 2 by FINSEQ_1:44;
hence contradiction by B1,FINSEQ_1:45;
end;
end;
:: A stage-1 carry output never occurs among the gates of a
:: stage-2 cell whose middle input is a pair.
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
let a,b,c be non pair set;
let X,Y,d be set such that
A1: Y is pair;
set w = GFA1CarryOutput(a,b,c);
set bA = GFA2AdderOutput(X,Y,d), bC = GFA2CarryOutput(X,Y,d);
assume w in InnerVertices BitGFA2Str(X,Y,d);
then w in {[<*X,Y*>,xor2c]} \/ {bA} \/
{[<*X,Y*>,and2a],[<*Y,d*>,and2c],[<*d,X*>,nor2]} \/ {bC} by GFACIRC1:95;
then w in {[<*X,Y*>,xor2c]} \/ {bA} \/
{[<*X,Y*>,and2a],[<*Y,d*>,and2c],[<*d,X*>,nor2]} or w in {bC}
by XBOOLE_0:def 3;
then w in ({[<*X,Y*>,xor2c]} \/ {bA}) or
w in {[<*X,Y*>,and2a],[<*Y,d*>,and2c],[<*d,X*>,nor2]} or w in {bC}
by XBOOLE_0:def 3;
then A2: w in {[<*X,Y*>,xor2c]} or w in {bA} or
w in {[<*X,Y*>,and2a],[<*Y,d*>,and2c],[<*d,X*>,nor2]} or w in {bC}
by XBOOLE_0:def 3;
per cases by A2,TARSKI:def 1,ENUMSET1:def 1;
suppose w = [<*X,Y*>,xor2c];
then <*[<*a,b*>,and2c],[<*b,c*>,and2a],[<*c,a*>,and2]*> = <*X,Y*>
by XTUPLE_0:1;
then len <*X,Y*> = 3 by FINSEQ_1:45;
hence contradiction by FINSEQ_1:44;
end;
suppose w = bA;
then <*[<*a,b*>,and2c],[<*b,c*>,and2a],[<*c,a*>,and2]*>
= <*[<*X,Y*>,xor2c],d*> by XTUPLE_0:1;
then len <*[<*X,Y*>,xor2c],d*> = 3 by FINSEQ_1:45;
hence contradiction by FINSEQ_1:44;
end;
suppose w = [<*X,Y*>,and2a];
then <*[<*a,b*>,and2c],[<*b,c*>,and2a],[<*c,a*>,and2]*> = <*X,Y*>
by XTUPLE_0:1;
then len <*X,Y*> = 3 by FINSEQ_1:45;
hence contradiction by FINSEQ_1:44;
end;
suppose w = [<*Y,d*>,and2c];
then <*[<*a,b*>,and2c],[<*b,c*>,and2a],[<*c,a*>,and2]*> = <*Y,d*>
by XTUPLE_0:1;
then len <*Y,d*> = 3 by FINSEQ_1:45;
hence contradiction by FINSEQ_1:44;
end;
suppose w = [<*d,X*>,nor2];
then <*[<*a,b*>,and2c],[<*b,c*>,and2a],[<*c,a*>,and2]*> = <*d,X*>
by XTUPLE_0:1;
then len <*d,X*> = 3 by FINSEQ_1:45;
hence contradiction by FINSEQ_1:44;
end;
suppose w = bC;
then <*[<*a,b*>,and2c],[<*b,c*>,and2a],[<*c,a*>,and2]*>
= <*[<*X,Y*>,and2a],[<*Y,d*>,and2c],[<*d,X*>,nor2]*> by XTUPLE_0:1;
then [<*b,c*>,and2a] = [<*Y,d*>,and2c] by FINSEQ_1:78;
then <*b,c*> = <*Y,d*> by XTUPLE_0:1;
hence contradiction by A1,FINSEQ_1:77;
end;
end;
:: Input vertices of a stage-2 cell are exactly its three inputs.
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
let k be Nat;
let ap,bm,cp,dm be nonpair-yielding FinSequence;
set X = GFA1AdderOutput(ap.(k+1),bm.(k+1),cp.(k+1));
set Y = k-BitFTA1CarryOutput(ap,bm,cp,dm);
set d = dm.(k+1);
A1: X <> [<*Y,d*>,and2c]
by XTUPLE_0:1,GFACIRC1:4,GFACIRC1:3;
thus thesis by A1,LmT1CO,GFACIRC1:97;
end;
:: A stage-2 cell stabilizes in 2 steps.
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
let k be Nat;
let ap,bm,cp,dm be nonpair-yielding FinSequence;
set X = GFA1AdderOutput(ap.(k+1),bm.(k+1),cp.(k+1));
set Y = k-BitFTA1CarryOutput(ap,bm,cp,dm);
set d = dm.(k+1);
A1: X <> [<*Y,d*>,and2c]
by XTUPLE_0:1,GFACIRC1:4,GFACIRC1:3;
let s be State of BitGFA2Circ(X,Y,d);
thus thesis by A1,LmT1CO,GFACIRC1:104;
end;
:: The FALSE base output vertex is an inner vertex of every
:: layer-2 structure.
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
let n be Nat;
let ap,bm,cp,dm be FinSequence;
set c0 = [<*>,(0-tuples_on BOOLEAN)-->FALSE];
defpred P[Nat] means
c0 in InnerVertices ($1-BitFTA1Layer2Str(ap,bm,cp,dm));
0-BitFTA1Layer2Str(ap,bm,cp,dm)
= 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) by LmT10L2;
then InnerVertices (0-BitFTA1Layer2Str(ap,bm,cp,dm)) = {c0}
by CIRCCOMB:42;
then
A1: P[ 0 ] by TARSKI:def 1;
A2: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume P[i];
then c0 in InnerVertices (i-BitFTA1Layer2Str(ap,bm,cp,dm))
\/ InnerVertices BitGFA2Str(
GFA1AdderOutput(ap.(i+1),bm.(i+1),cp.(i+1)),
i-BitFTA1CarryOutput(ap,bm,cp,dm), dm.(i+1)) by XBOOLE_0:def 3;
hence P[i+1] by LmT1L2inner;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
:: Stage-1 outputs are never layer-2 gates.
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
let n be Nat;
let ap,bm,cp,dm be nonpair-yielding FinSequence;
let u,v,x be non pair set;
set c0 = [<*>,(0-tuples_on BOOLEAN)-->FALSE];
set wA = GFA1AdderOutput(u,v,x), wC = GFA1CarryOutput(u,v,x);
A1: wA <> c0 by XTUPLE_0:1;
A2: wC <> c0 by XTUPLE_0:1;
defpred P[Nat] means
not wA in InnerVertices ($1-BitFTA1Layer2Str(ap,bm,cp,dm)) &
not wC in InnerVertices ($1-BitFTA1Layer2Str(ap,bm,cp,dm));
0-BitFTA1Layer2Str(ap,bm,cp,dm)
= 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) by LmT10L2;
then InnerVertices (0-BitFTA1Layer2Str(ap,bm,cp,dm)) = {c0}
by CIRCCOMB:42;
then
A3: P[ 0 ] by A1,A2,TARSKI:def 1;
A4: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume B1: P[i];
set B = BitGFA2Str(GFA1AdderOutput(ap.(i+1),bm.(i+1),cp.(i+1)),
i-BitFTA1CarryOutput(ap,bm,cp,dm), dm.(i+1));
B2: i-BitFTA1CarryOutput(ap,bm,cp,dm) is pair by LmT1COp;
B3: not wA in InnerVertices B & not wC in InnerVertices B
by B2,LmT1W1,LmT1W2;
B4: InnerVertices ((i+1)-BitFTA1Layer2Str(ap,bm,cp,dm))
= InnerVertices (i-BitFTA1Layer2Str(ap,bm,cp,dm)) \/ InnerVertices B
by LmT1L2inner;
thus not wA in InnerVertices ((i+1)-BitFTA1Layer2Str(ap,bm,cp,dm))
by B4,B1,B3,XBOOLE_0:def 3;
thus not wC in InnerVertices ((i+1)-BitFTA1Layer2Str(ap,bm,cp,dm))
by B4,B1,B3,XBOOLE_0:def 3;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A3,A4);
hence thesis;
end;
:: Every layer-2 input vertex is a primary input or a stage-1 output.
LmT1InAcc: for n being Nat for ap,bm,cp,dm being nonpair-yielding FinSequence
for w being set
st w in InputVertices (n-BitFTA1Layer2Str(ap,bm,cp,dm)) holds
w is non 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
let n be Nat;
let ap,bm,cp,dm be nonpair-yielding FinSequence;
set c0 = [<*>,(0-tuples_on BOOLEAN)-->FALSE];
defpred P[Nat] means for w being set
st w in InputVertices ($1-BitFTA1Layer2Str(ap,bm,cp,dm)) holds
w is non 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));
A1: P[ 0 ]
proof
let w be set;
assume
B1: w in InputVertices (0-BitFTA1Layer2Str(ap,bm,cp,dm));
0-BitFTA1Layer2Str(ap,bm,cp,dm)
= 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) by LmT10L2;
then InputVertices (0-BitFTA1Layer2Str(ap,bm,cp,dm)) = rng <*>
by CIRCCOMB:42
.= {};
hence thesis by B1;
end;
A2: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume B1: P[i];
set X = GFA1AdderOutput(ap.(i+1),bm.(i+1),cp.(i+1));
set Y = i-BitFTA1CarryOutput(ap,bm,cp,dm);
set d = dm.(i+1);
set B = BitGFA2Str(X,Y,d);
set S1 = i-BitFTA1Layer2Str(ap,bm,cp,dm);
B2: (i+1)-BitFTA1Layer2Str(ap,bm,cp,dm) = S1 +* B by LmT15B;
B3: InputVertices (S1 +* B)
= ((InputVertices S1) \ (InnerVertices B))
\/ ((InputVertices B) \ (InnerVertices S1)) by CIRCCOMB:47,CIRCCMB2:5;
B4: InputVertices B = {X,Y,d} by LmT1C2i;
let w be set;
assume B5: w in InputVertices ((i+1)-BitFTA1Layer2Str(ap,bm,cp,dm));
per cases by B5,B2,B3,XBOOLE_0:def 3;
suppose w in (InputVertices S1) \ (InnerVertices B);
then w in InputVertices S1 by XBOOLE_0:def 5;
hence thesis by B1;
end;
suppose B6: w in (InputVertices B) \ (InnerVertices S1);
then C1: w in {X,Y,d} by B4,XBOOLE_0:def 5;
per cases by C1,ENUMSET1:def 1;
suppose C2: w = X;
thus thesis by C2;
end;
suppose C3: w = Y;
per cases by NAT_1:6;
suppose D1: i = 0;
E1: not w in InnerVertices S1 by B6,XBOOLE_0:def 5;
w = c0 by C3,D1,LmT10CO;
hence thesis by LmT1Cin0In,E1;
end;
suppose ex m being Nat st i = m+1;
then consider m being Nat such that E1: i = m+1;
reconsider u1 = ap.(m+1), v1 = bm.(m+1), x1 = cp.(m+1)
as non pair set;
w = GFA1CarryOutput(u1,v1,x1) by C3,E1,LmT1COk;
hence thesis;
end;
end;
suppose w = d;
hence thesis;
end;
end;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
:: Layer-2 inputs never hit the gates of the next stage-2 cell.
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
let k be Nat;
let ap,bm,cp,dm be nonpair-yielding FinSequence;
set X = GFA1AdderOutput(ap.(k+1),bm.(k+1),cp.(k+1));
set Y = k-BitFTA1CarryOutput(ap,bm,cp,dm);
set d = dm.(k+1);
set B = BitGFA2Str(X,Y,d);
set bA = GFA2AdderOutput(X,Y,d), bC = GFA2CarryOutput(X,Y,d);
A1: Y is pair by LmT1COp;
assume InputVertices (k-BitFTA1Layer2Str(ap,bm,cp,dm)) meets
InnerVertices B;
then consider w being object such that
A2: w in InputVertices (k-BitFTA1Layer2Str(ap,bm,cp,dm)) and
A3: w in InnerVertices B by XBOOLE_0:3;
reconsider w as set by TARSKI:1;
per cases by A2,LmT1InAcc;
suppose A4: w is non pair;
w in {[<*X,Y*>,xor2c]} \/ {bA} \/
{[<*X,Y*>,and2a],[<*Y,d*>,and2c],[<*d,X*>,nor2]} \/ {bC}
by A3,GFACIRC1:95;
then w in {[<*X,Y*>,xor2c]} \/ {bA} \/
{[<*X,Y*>,and2a],[<*Y,d*>,and2c],[<*d,X*>,nor2]} or w in {bC}
by XBOOLE_0:def 3;
then w in ({[<*X,Y*>,xor2c]} \/ {bA}) or
w in {[<*X,Y*>,and2a],[<*Y,d*>,and2c],[<*d,X*>,nor2]} or w in {bC}
by XBOOLE_0:def 3;
then B1: w in {[<*X,Y*>,xor2c]} or w in {bA} or
w in {[<*X,Y*>,and2a],[<*Y,d*>,and2c],[<*d,X*>,nor2]} or w in {bC}
by XBOOLE_0:def 3;
per cases by B1,TARSKI:def 1,ENUMSET1:def 1;
suppose w = [<*X,Y*>,xor2c];
hence contradiction by A4;
end;
suppose w = bA;
hence contradiction by A4;
end;
suppose w = [<*X,Y*>,and2a];
hence contradiction by A4;
end;
suppose w = [<*Y,d*>,and2c];
hence contradiction by A4;
end;
suppose w = [<*d,X*>,nor2];
hence contradiction by A4;
end;
suppose w = bC;
hence contradiction by A4;
end;
end;
suppose ex u,v,x being non pair set st w = GFA1AdderOutput(u,v,x);
hence contradiction by A3,A1,LmT1W1;
end;
suppose ex u,v,x being non pair set st w = GFA1CarryOutput(u,v,x);
hence contradiction by A3,A1,LmT1W2;
end;
end;
:: New-cell inputs never hit earlier layer-2 gates (from stage 2 on).
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
let m be Nat;
let ap,bm,cp,dm be nonpair-yielding FinSequence;
set X = GFA1AdderOutput(ap.(m+1+1),bm.(m+1+1),cp.(m+1+1));
set Y = (m+1)-BitFTA1CarryOutput(ap,bm,cp,dm);
set d = dm.(m+1+1);
set B = BitGFA2Str(X,Y,d);
set L2 = (m+1)-BitFTA1Layer2Str(ap,bm,cp,dm);
A1: InputVertices B = {X,Y,d} by LmT1C2i;
assume InputVertices B meets InnerVertices L2;
then consider w being object such that
A2: w in InputVertices B and
A3: w in InnerVertices L2 by XBOOLE_0:3;
per cases by A2,A1,ENUMSET1:def 1;
suppose w = X;
hence contradiction by A3,LmT1WnI;
end;
suppose A5: w = Y;
reconsider u1 = ap.(m+1), v1 = bm.(m+1), x1 = cp.(m+1)
as non pair set;
not GFA1CarryOutput(u1,v1,x1) in InnerVertices L2 by LmT1WnI;
hence contradiction by A5,LmT1COk,A3;
end;
suppose A6: w = d;
reconsider d1 = d as non pair set;
B1: {d1} misses InnerVertices L2 by LmT1L2rel,FACIRC_1:5;
d1 in {d1} by TARSKI:def 1;
then d1 in {d1} /\ InnerVertices L2 by A6,A3,XBOOLE_0:def 4;
hence contradiction by B1,XBOOLE_0:def 7;
end;
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:
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
let n be Nat;
let ap,bm,cp,dm be nonpair-yielding FinSequence;
set c0 = [<*>,(0-tuples_on BOOLEAN)-->FALSE];
set A0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
defpred P[Nat] means
for s being State of $1-BitFTA1Layer2Circ(ap,bm,cp,dm)
st s.[<*>,(0-tuples_on BOOLEAN)-->FALSE] = FALSE
holds Following(s,2) is stable;
A1: 0-BitFTA1Layer2Circ(ap,bm,cp,dm) = A0
proof
consider f,g,h being ManySortedSet of NAT such that
0-BitFTA1Layer2Str(ap,bm,cp,dm) = f.0 and
B1: 0-BitFTA1Layer2Circ(ap,bm,cp,dm) = g.0 and
f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) and
B2: g.0 = A0 and
h.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE] and
for k being Nat, S being non empty ManySortedSign,
A being non-empty MSAlgebra over S, 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)) by Def14;
thus thesis by B1,B2;
end;
A2: P[ 0 ]
proof
let s be State of 0-BitFTA1Layer2Circ(ap,bm,cp,dm);
assume s.c0 = FALSE;
reconsider s0 = s as State of A0 by A1;
B1: Following(s0,1) = Following s0 by FACIRC_1:14;
B2: Following(s0,2) = Following(s0,1) by B1,CIRCCMB2:2,CIRCCMB2:4;
B3: 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE)
= 0-BitFTA1Layer2Str(ap,bm,cp,dm) by LmT10L2;
thus thesis by B3,A1,B2,B1,CIRCCMB2:2;
end;
A3: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume B1: P[i];
set X = GFA1AdderOutput(ap.(i+1),bm.(i+1),cp.(i+1));
set Y = i-BitFTA1CarryOutput(ap,bm,cp,dm);
set B = BitGFA2Str(X,Y,dm.(i+1));
set Bc = BitGFA2Circ(X,Y,dm.(i+1));
set S1 = i-BitFTA1Layer2Str(ap,bm,cp,dm);
set SS = (i+1)-BitFTA1Layer2Str(ap,bm,cp,dm);
set C1 = i-BitFTA1Layer2Circ(ap,bm,cp,dm);
set AA = (i+1)-BitFTA1Layer2Circ(ap,bm,cp,dm);
B2: SS = S1 +* B by LmT15B;
B3: AA = C1 +* Bc by LmT16B;
B4: C1 tolerates Bc by CIRCCOMB:60;
B5: the Sorts of C1 tolerates the Sorts of Bc by B4,CIRCCOMB:def 3;
B6: c0 in InnerVertices S1 by LmT1Cin0In;
let s be State of (i+1)-BitFTA1Layer2Circ(ap,bm,cp,dm);
assume B7: s.c0 = FALSE;
reconsider t = s as State of C1 +* Bc by B3;
reconsider s1 = t|the carrier of S1 as State of C1
by B5,CIRCCOMB:26;
B8: s1.c0 = FALSE by B7,B6,FUNCT_1:49;
B9: Following(s1,2) is stable by B1,B8;
per cases by NAT_1:6;
suppose B10: i = 0;
C1: S1 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) by B10,LmT10L2;
C2: InputVertices S1 = rng <*> by C1,CIRCCOMB:42
.= {};
C3: InputVertices S1 /\ InnerVertices B = {} by C2;
C4: InnerVertices S1 = {c0} by C1,CIRCCOMB:42;
C5: Following s1 = s1
proof
D1: dom s1 = the carrier of S1 by CIRCUIT1:3;
now
let y be object;
assume y in dom Following s1;
then
E2: y in the carrier of S1 by CIRCUIT1:3;
per cases;
suppose E3: y in InputVertices S1;
thus (Following s1).y = s1.y by E3,CIRCUIT2:def 5;
end;
suppose E4: not y in InputVertices S1;
InputVertices S1 = (the carrier of S1)
\ rng the ResultSort of S1 by MSAFREE2:def 2;
then y in rng the ResultSort of S1
by E2,E4,XBOOLE_0:def 5;
then y in InnerVertices S1 by MSAFREE2:def 3;
then
y = c0 by C4,TARSKI:def 1;
hence (Following s1).y = s1.y by C4,B8,LmT1Cin0In,Th9;
end;
end;
hence thesis by CIRCUIT1:3,D1,FUNCT_1:2;
end;
s1 is stable by C5,CIRCUIT2:def 6;
then
C6: Following(s1,0) is stable by FACIRC_1:11;
reconsider sB = Following(t,0)|the carrier of B as State of Bc
by B5,CIRCCOMB:26;
C7: Following(sB,2) is stable by LmT1C2s;
Following(t, 0+2) is stable
by B4,C3,XBOOLE_0:def 7,C6,C7,CIRCCMB2:19;
hence Following(s,2) is stable by B2,B3;
end;
suppose ex m being Nat st i = m+1;
then consider m being Nat such that C1: i = m+1;
C2: InputVertices S1 misses InnerVertices B by LmT1Dj1;
C3: InputVertices B misses InnerVertices S1 by C1,LmT1Dj2;
reconsider sB = t|the carrier of B as State of Bc
by B5,CIRCCOMB:26;
C4: Following(sB,2) is stable by LmT1C2s;
Following(t, max(2,2)) is stable
by CIRCCOMB:60,C2,C3,B9,C4,CIRCCMB2:22;
hence Following(s,2) is stable by B2,B3;
end;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
::--------------------------------
:: Stability of n-depth FTA Circuit (TYPE-1)
::--------------------------------
theorem :: Th21
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
let n be Nat;
let ap,bm,cp,dm be nonpair-yielding FinSeqLen of n;
let s be State of n-BitFTA1Circ(ap,bm,cp,dm);
set S1 = n-BitFTA1Layer1Str(ap,bm,cp);
set S2 = n-BitFTA1Layer2Str(ap,bm,cp,dm);
set C1 = n-BitFTA1Layer1Circ(ap,bm,cp);
set C2 = n-BitFTA1Layer2Circ(ap,bm,cp,dm);
set S = n-BitFTA1Str(ap,bm,cp,dm);
set C = n-BitFTA1Circ(ap,bm,cp,dm);
A1: S = S1 +* S2 by Th16;
A2: C = C1 +* C2 by Th17;
A3: C1 tolerates C2 by CIRCCOMB:60;
A4: the Sorts of C1 tolerates the Sorts of C2 by A3,CIRCCOMB:def 3;
reconsider t = s as State of C1 +* C2 by A2;
reconsider s1 = t|the carrier of S1 as State of C1 by A4,CIRCCOMB:26;
reconsider s2 = Following(t,2)|the carrier of S2 as State of C2
by A4,CIRCCOMB:26;
A5: InputVertices S1 misses InnerVertices S2 by Th18;
A6: Following(s1,2) is stable by Th19;
A7: Following(s2,2) is stable
proof
set c0 = [<*>,(0-tuples_on BOOLEAN)-->FALSE];
B1: c0 in InnerVertices S2 by LmT1Cin0In;
B2: S1 tolerates S2 by CIRCCOMB:47;
InnerVertices S = InnerVertices S1 \/ InnerVertices S2
by A1,B2,CIRCCOMB:11;
then
B3: c0 in InnerVertices S by B1,XBOOLE_0:def 3;
reconsider Cb = C as Boolean gate`2=den non-empty Circuit of S;
reconsider s9 = s as State of Cb;
B5: (Following Following s9).c0 = FALSE by B3,Th9;
s2.c0 = (Following(t,2)).c0 by FUNCT_1:49,B1
.= FALSE by A1,A2,FACIRC_1:15,B5;
hence thesis by Th20;
end;
Following(t,2+2) is stable by CIRCCOMB:60,A5,A6,A7,CIRCCMB2:19;
hence thesis by A1,A2;
end;