:: Stability of the 7-3 Compressor Circuit for {W}allace Tree. Part {I}
:: by Katsumi Wasaki
::
:: Received December 30, 2019
:: Copyright (c) 2019-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 3.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/3.0/.
environ
vocabularies XBOOLEAN, XBOOLE_0, SUBSET_1, RELAT_1, NUMBERS, ARYTM_3,
XXREAL_0, STRUCT_0, FUNCT_1, FUNCT_4, FINSEQ_1, FINSEQ_2, PARTFUN1,
MCART_1, FSM_1, MARGREL1, MSUALG_1, LATTICES, MSAFREE2, CIRCUIT1,
CIRCUIT2, CIRCCOMB, FACIRC_1, TWOSCOMP, GFACIRC1, WALLACE1;
notations TARSKI, XBOOLE_0, ENUMSET1, XTUPLE_0, SUBSET_1, NAT_1, RELAT_1,
NUMBERS, XCMPLX_0, XXREAL_0, STRUCT_0, FUNCT_1, FUNCT_2, FINSEQ_1,
FINSEQ_2, PARTFUN1, MARGREL1, BINARITH, MSUALG_1, MSAFREE2, CIRCUIT1,
CIRCUIT2, CIRCCOMB, FACIRC_1, TWOSCOMP, GFACIRC1, CIRCCMB3;
constructors NUMBERS, VALUED_0, RELSET_1, ENUMSET1, BINARITH, CIRCUIT2,
FACIRC_1, TWOSCOMP, GFACIRC1, CIRCCMB3;
registrations ORDINAL1, XTUPLE_0, CARD_3, NAT_1, RELAT_1, STRUCT_0, FUNCT_1,
FINSEQ_1, MARGREL1, MSAFREE2, CIRCCOMB, FACIRC_1, CIRCCMB3;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities ORDINAL1, MARGREL1, FACIRC_1, GFACIRC1;
expansions XBOOLE_0, FACIRC_1;
theorems XBOOLEAN, XBOOLE_0, XBOOLE_1, ZFMISC_1, ENUMSET1, FUNCT_1, FINSEQ_1,
FINSEQ_2, CIRCUIT1, CIRCCOMB, FACIRC_1, TWOSCOMP, CIRCCMB2, GFACIRC1,
CIRCCMB3;
begin :: Properties of `Intermediate' STC Circuit Structure (LAYER-I)
::=========================================================================
registration
let x1,x2,x3,x4 be non pair object;
cluster {x1,x2,x3,x4} -> without_pairs;
coherence
by ENUMSET1:def 2;
let x5 be non pair object;
cluster {x1,x2,x3,x4,x5} -> without_pairs;
coherence
by ENUMSET1:def 3;
let x6 be non pair object;
cluster {x1,x2,x3,x4,x5,x6} -> without_pairs;
coherence
by ENUMSET1:def 4;
let x7 be non pair object;
cluster {x1,x2,x3,x4,x5,x6,x7} -> without_pairs;
coherence
by ENUMSET1:def 5;
end;
::---------------------------------------------------------------
:: 1. `Intermediate' Circuit [Layer-I]
::---------------------------------------------------------------
::---------------------------------------------------------------
:: 1-1. Definition for `Intermediate' Circuit [Layer-I]
::---------------------------------------------------------------
::---------------------------------------
:: Combined Circuit Structure of STC_TYPE0_Inter_Inter.
definition
let x1,x2,x3,x5,x6,x7 be set;
func STC0IIStr(x1,x2,x3,x5,x6,x7) ->
unsplit gate`1=arity gate`2isBoolean
non void strict non empty ManySortedSign
equals
BitGFA0Str(x1,x2,x3) +* BitGFA0Str(x5,x6,x7);
coherence;
end;
definition
let x1,x2,x3,x5,x6,x7 be set;
func STC0IICirc(x1,x2,x3,x5,x6,x7) ->
strict Boolean gate`2=den Circuit of STC0IIStr(x1,x2,x3,x5,x6,x7)
equals
BitGFA0Circ(x1,x2,x3) +* BitGFA0Circ(x5,x6,x7);
coherence;
end;
::-----------------------------------------------
:: 1-2. Properties of `Intermediate' Circuit Structure
::-----------------------------------------------
::---------------------------------------
:: InnerVertices of STC_TYPE0_Inter_Inter.
theorem ThSTC0IIS1:
for x1,x2,x3,x5,x6,x7 being set holds
InnerVertices STC0IIStr(x1,x2,x3,x5,x6,x7) =
{[<*x1,x2*>,xor2], GFA0AdderOutput(x1,x2,x3)} \/
{[<*x1,x2*>,and2], [<*x2,x3*>,and2], [<*x3,x1*>,and2],
GFA0CarryOutput(x1,x2,x3)} \/
{[<*x5,x6*>,xor2], GFA0AdderOutput(x5,x6,x7)} \/
{[<*x5,x6*>,and2], [<*x6,x7*>,and2], [<*x7,x5*>,and2],
GFA0CarryOutput(x5,x6,x7)}
proof
let x1,x2,x3,x5,x6,x7 be set;
set S = STC0IIStr(x1,x2,x3,x5,x6,x7);
set S1 = BitGFA0Str(x1,x2,x3);
set A1 = GFA0AdderOutput(x1,x2,x3);
set C1 = GFA0CarryOutput(x1,x2,x3);
set S2 = BitGFA0Str(x5,x6,x7);
set A2 = GFA0AdderOutput(x5,x6,x7);
set C2 = GFA0CarryOutput(x5,x6,x7);
set x1x20 = [<*x1,x2*>, xor2];
set x1x2 = [<*x1,x2*>, and2];
set x2x3 = [<*x2,x3*>, and2];
set x3x1 = [<*x3,x1*>, and2];
set x5x60 = [<*x5,x6*>, xor2];
set x5x6 = [<*x5,x6*>, and2];
set x6x7 = [<*x6,x7*>, and2];
set x7x5 = [<*x7,x5*>, and2];
S1 tolerates S2 by CIRCCOMB:47;
hence InnerVertices S
= (InnerVertices S1) \/ (InnerVertices S2) by CIRCCOMB:11
.= ({x1x20} \/ {A1} \/ {x1x2,x2x3,x3x1} \/ {C1}) \/
(InnerVertices S2) by GFACIRC1:31
.= ({x1x20,A1} \/ {x1x2,x2x3,x3x1} \/ {C1}) \/
(InnerVertices S2) by ENUMSET1:1
.= ({x1x20,A1} \/ ({x1x2,x2x3,x3x1} \/ {C1})) \/
(InnerVertices S2) by XBOOLE_1:4
.= ({x1x20,A1} \/ {x1x2,x2x3,x3x1,C1}) \/
(InnerVertices S2) by ENUMSET1:6
.= ({x1x20,A1} \/ {x1x2,x2x3,x3x1,C1}) \/
({x5x60} \/ {A2} \/ {x5x6,x6x7,x7x5} \/ {C2}) by GFACIRC1:31
.= ({x1x20,A1} \/ {x1x2,x2x3,x3x1,C1}) \/
({x5x60,A2} \/ {x5x6,x6x7,x7x5} \/ {C2}) by ENUMSET1:1
.= ({x1x20,A1} \/ {x1x2,x2x3,x3x1,C1}) \/
({x5x60,A2} \/ ({x5x6,x6x7,x7x5} \/ {C2})) by XBOOLE_1:4
.= ({x1x20,A1} \/ {x1x2,x2x3,x3x1,C1}) \/
({x5x60,A2} \/ {x5x6,x6x7,x7x5,C2}) by ENUMSET1:6
.= {x1x20,A1} \/ {x1x2,x2x3,x3x1,C1} \/
{x5x60,A2} \/ {x5x6,x6x7,x7x5,C2} by XBOOLE_1:4;
end;
theorem :: ThSTC0IIS2:
for x1,x2,x3,x5,x6,x7 being set holds
InnerVertices STC0IIStr(x1,x2,x3,x5,x6,x7) is Relation;
::---------------------------------------
:: InputVertices of of STC_TYPE0_Inter_Inter.
theorem ThSTC0IIS4:
for x1,x2,x3,x5,x6,x7 being non pair set holds
InputVertices STC0IIStr(x1,x2,x3,x5,x6,x7) = {x1,x2,x3,x5,x6,x7}
proof
let x1,x2,x3,x5,x6,x7 be non pair set;
set S = STC0IIStr(x1,x2,x3,x5,x6,x7);
set S1 = BitGFA0Str(x1,x2,x3);
set S2 = BitGFA0Str(x5,x6,x7);
A1: InputVertices S1 = {x1,x2,x3} & InputVertices S2 = {x5,x6,x7}
by GFACIRC1:34;
InnerVertices S1 is Relation & InnerVertices S2 is Relation;
hence
InputVertices S
= {x1,x2,x3} \/ {x5,x6,x7} by A1,FACIRC_1:7
.= {x1,x2,x3,x5,x6,x7} by ENUMSET1:13;
end;
theorem ThSTC0IIS5:
for x1,x2,x3,x5,x6,x7 being non pair set holds
InputVertices STC0IIStr(x1,x2,x3,x5,x6,x7) is without_pairs
proof
let x1,x2,x3,x5,x6,x7 be non pair set;
InputVertices BitGFA0Str(x1,x2,x3) is without_pairs &
InputVertices BitGFA0Str(x5,x6,x7) is without_pairs by GFACIRC1:35;
hence thesis by CIRCCOMB:47,FACIRC_1:8;
end;
::---------------------------------------
:: The Element of Carriers, InnerVertices and InputVertices of
:: STC_TYPE0_Inter_Inter.
theorem ThSTC0IIS6:
for x1,x2,x3,x5,x6,x7 being set holds
x1 in the carrier of STC0IIStr(x1,x2,x3,x5,x6,x7) &
x2 in the carrier of STC0IIStr(x1,x2,x3,x5,x6,x7) &
x3 in the carrier of STC0IIStr(x1,x2,x3,x5,x6,x7) &
x5 in the carrier of STC0IIStr(x1,x2,x3,x5,x6,x7) &
x6 in the carrier of STC0IIStr(x1,x2,x3,x5,x6,x7) &
x7 in the carrier of STC0IIStr(x1,x2,x3,x5,x6,x7) &
[<*x1,x2*>,xor2] in the carrier of STC0IIStr(x1,x2,x3,x5,x6,x7) &
GFA0AdderOutput(x1,x2,x3)
in the carrier of STC0IIStr(x1,x2,x3,x5,x6,x7) &
[<*x1,x2*>,and2] in the carrier of STC0IIStr(x1,x2,x3,x5,x6,x7) &
[<*x2,x3*>,and2] in the carrier of STC0IIStr(x1,x2,x3,x5,x6,x7) &
[<*x3,x1*>,and2] in the carrier of STC0IIStr(x1,x2,x3,x5,x6,x7) &
GFA0CarryOutput(x1,x2,x3)
in the carrier of STC0IIStr(x1,x2,x3,x5,x6,x7) &
[<*x5,x6*>,xor2] in the carrier of STC0IIStr(x1,x2,x3,x5,x6,x7) &
GFA0AdderOutput(x5,x6,x7)
in the carrier of STC0IIStr(x1,x2,x3,x5,x6,x7) &
[<*x5,x6*>,and2] in the carrier of STC0IIStr(x1,x2,x3,x5,x6,x7) &
[<*x6,x7*>,and2] in the carrier of STC0IIStr(x1,x2,x3,x5,x6,x7) &
[<*x7,x5*>,and2] in the carrier of STC0IIStr(x1,x2,x3,x5,x6,x7) &
GFA0CarryOutput(x5,x6,x7)
in the carrier of STC0IIStr(x1,x2,x3,x5,x6,x7)
proof
let x1,x2,x3,x5,x6,x7 be set;
set S = STC0IIStr(x1,x2,x3,x5,x6,x7);
set S1 = BitGFA0Str(x1,x2,x3);
set A1 = GFA0AdderOutput(x1,x2,x3);
set C1 = GFA0CarryOutput(x1,x2,x3);
set S2 = BitGFA0Str(x5,x6,x7);
set A2 = GFA0AdderOutput(x5,x6,x7);
set C2 = GFA0CarryOutput(x5,x6,x7);
set x1x20 = [<*x1,x2*>, xor2];
set x1x2 = [<*x1,x2*>, and2];
set x2x3 = [<*x2,x3*>, and2];
set x3x1 = [<*x3,x1*>, and2];
set x5x60 = [<*x5,x6*>, xor2];
set x5x6 = [<*x5,x6*>, and2];
set x6x7 = [<*x6,x7*>, and2];
set x7x5 = [<*x7,x5*>, and2];
A1: x1 in the carrier of S1 & x2 in the carrier of S1 &
x3 in the carrier of S1 & x1x20 in the carrier of S1 &
A1 in the carrier of S1 &
x1x2 in the carrier of S1 & x2x3 in the carrier of S1 &
x3x1 in the carrier of S1 &
C1 in the carrier of S1 by GFACIRC1:36;
x5 in the carrier of S2 & x6 in the carrier of S2 &
x7 in the carrier of S2 & x5x60 in the carrier of S2 &
A2 in the carrier of S2 &
x5x6 in the carrier of S2 & x6x7 in the carrier of S2 &
x7x5 in the carrier of S2 &
C2 in the carrier of S2 by GFACIRC1:36;
hence thesis by A1,FACIRC_1:20;
end;
theorem ThSTC0IIS7:
for x1,x2,x3,x5,x6,x7 being set holds
[<*x1,x2*>,xor2] in InnerVertices STC0IIStr(x1,x2,x3,x5,x6,x7) &
GFA0AdderOutput(x1,x2,x3)
in InnerVertices STC0IIStr(x1,x2,x3,x5,x6,x7) &
[<*x1,x2*>,and2] in InnerVertices STC0IIStr(x1,x2,x3,x5,x6,x7) &
[<*x2,x3*>,and2] in InnerVertices STC0IIStr(x1,x2,x3,x5,x6,x7) &
[<*x3,x1*>,and2] in InnerVertices STC0IIStr(x1,x2,x3,x5,x6,x7) &
GFA0CarryOutput(x1,x2,x3)
in InnerVertices STC0IIStr(x1,x2,x3,x5,x6,x7) &
[<*x5,x6*>,xor2] in InnerVertices STC0IIStr(x1,x2,x3,x5,x6,x7) &
GFA0AdderOutput(x5,x6,x7)
in InnerVertices STC0IIStr(x1,x2,x3,x5,x6,x7) &
[<*x5,x6*>,and2] in InnerVertices STC0IIStr(x1,x2,x3,x5,x6,x7) &
[<*x6,x7*>,and2] in InnerVertices STC0IIStr(x1,x2,x3,x5,x6,x7) &
[<*x7,x5*>,and2] in InnerVertices STC0IIStr(x1,x2,x3,x5,x6,x7) &
GFA0CarryOutput(x5,x6,x7)
in InnerVertices STC0IIStr(x1,x2,x3,x5,x6,x7)
proof
let x1,x2,x3,x5,x6,x7 be set;
set S = STC0IIStr(x1,x2,x3,x5,x6,x7);
set S1 = BitGFA0Str(x1,x2,x3);
set A1 = GFA0AdderOutput(x1,x2,x3);
set C1 = GFA0CarryOutput(x1,x2,x3);
set S2 = BitGFA0Str(x5,x6,x7);
set A2 = GFA0AdderOutput(x5,x6,x7);
set C2 = GFA0CarryOutput(x5,x6,x7);
set x1x20 = [<*x1,x2*>, xor2];
set x1x2 = [<*x1,x2*>, and2];
set x2x3 = [<*x2,x3*>, and2];
set x3x1 = [<*x3,x1*>, and2];
set x5x60 = [<*x5,x6*>, xor2];
set x5x6 = [<*x5,x6*>, and2];
set x6x7 = [<*x6,x7*>, and2];
set x7x5 = [<*x7,x5*>, and2];
set p1 = {x1x20,A1,x1x2,x2x3,x3x1,C1};
set p2 = {x5x60,A2,x5x6,x6x7,x7x5,C2};
A1: x1x20 in p1 & A1 in p1 &
x1x2 in p1 & x2x3 in p1 & x3x1 in p1 & C1 in p1 by ENUMSET1:def 4;
A2: x5x60 in p2 & A2 in p2 &
x5x6 in p2 & x6x7 in p2 & x7x5 in p2 & C2 in p2 by ENUMSET1:def 4;
InnerVertices S
= {x1x20,A1} \/ {x1x2,x2x3,x3x1,C1} \/ {x5x60,A2} \/ {x5x6,x6x7,x7x5,C2}
by ThSTC0IIS1
.= p1 \/ {x5x60,A2} \/ {x5x6,x6x7,x7x5,C2} by ENUMSET1:12
.= p1 \/ ({x5x60,A2} \/ {x5x6,x6x7,x7x5,C2}) by XBOOLE_1:4
.= p1 \/ p2 by ENUMSET1:12;
hence thesis by A1,A2,XBOOLE_0:def 3;
end;
theorem ThSTC0IIS8:
for x1,x2,x3,x5,x6,x7 being non pair set holds
x1 in InputVertices STC0IIStr(x1,x2,x3,x5,x6,x7) &
x2 in InputVertices STC0IIStr(x1,x2,x3,x5,x6,x7) &
x3 in InputVertices STC0IIStr(x1,x2,x3,x5,x6,x7) &
x5 in InputVertices STC0IIStr(x1,x2,x3,x5,x6,x7) &
x6 in InputVertices STC0IIStr(x1,x2,x3,x5,x6,x7) &
x7 in InputVertices STC0IIStr(x1,x2,x3,x5,x6,x7)
proof
let x1,x2,x3,x5,x6,x7 be non pair set;
set S = STC0IIStr(x1,x2,x3,x5,x6,x7);
InputVertices S = {x1,x2,x3,x5,x6,x7} by ThSTC0IIS4;
hence thesis by ENUMSET1:def 4;
end;
::-------------------------------------------
:: 1-3. Output Definitions of the Combined Circuit
::-------------------------------------------
:: Internal Signal Outputs of STC_TYPE0_Inter_Inter.
definition
let x1,x2,x3,x5,x6,x7 be set;
func STC0IICarryOutputC1(x1,x2,x3,x5,x6,x7) ->
Element of InnerVertices STC0IIStr(x1,x2,x3,x5,x6,x7) equals
GFA0CarryOutput(x1,x2,x3);
coherence by ThSTC0IIS7;
func STC0IIAdderOutputA1(x1,x2,x3,x5,x6,x7) ->
Element of InnerVertices STC0IIStr(x1,x2,x3,x5,x6,x7) equals
GFA0AdderOutput(x1,x2,x3);
coherence by ThSTC0IIS7;
func STC0IICarryOutputC2(x1,x2,x3,x5,x6,x7) ->
Element of InnerVertices STC0IIStr(x1,x2,x3,x5,x6,x7) equals
GFA0CarryOutput(x5,x6,x7);
coherence by ThSTC0IIS7;
func STC0IIAdderOutputA2(x1,x2,x3,x5,x6,x7) ->
Element of InnerVertices STC0IIStr(x1,x2,x3,x5,x6,x7) equals
GFA0AdderOutput(x5,x6,x7);
coherence by ThSTC0IIS7;
end;
::----------------------------------------------------
:: 1-4. Outputs of the Combined Circuit and its Stability
::----------------------------------------------------
::===================================================
:: Temporal (Internal) Calculations after 2-steps
::===================================================
LmSTC0IIS09a:
for a,b,c being non pair set
for x,y,z being set holds
InputVertices BitGFA0Str(a,b,c) misses InnerVertices BitGFA0Str(x,y,z)
proof
let a,b,c be non pair set;
let x,y,z be set;
set S1 = BitGFA0Str(a,b,c);
set S2 = BitGFA0Str(x,y,z);
InputVertices S1 is without_pairs & InnerVertices S2 is Relation
by GFACIRC1:35;
hence thesis;
end;
:: -----------------------------------
:: Proposition #1-1 (Internal Circuit Outputs after Two-steps)
theorem ThSTC0IIS10: :: for Output C1, A1, C2 and A2
for x1,x2,x3,x5,x6,x7 being non pair set
for s being State of STC0IICirc(x1,x2,x3,x5,x6,x7)
for a1,a2,a3,a5,a6,a7 being Element of BOOLEAN st
a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a5 = s.x5 & a6 = s.x6 & a7 = s.x7
holds Following(s,2).STC0IICarryOutputC1(x1,x2,x3,x5,x6,x7)
= (a1 '&' a2) 'or' (a2 '&' a3) 'or' (a3 '&' a1) &
Following(s,2).STC0IIAdderOutputA1(x1,x2,x3,x5,x6,x7)
= a1 'xor' a2 'xor' a3 &
Following(s,2).STC0IICarryOutputC2(x1,x2,x3,x5,x6,x7)
= (a5 '&' a6) 'or' (a6 '&' a7) 'or' (a7 '&' a5) &
Following(s,2).STC0IIAdderOutputA2(x1,x2,x3,x5,x6,x7)
= a5 'xor' a6 'xor' a7 &
Following(s,2).x1 = a1 & Following(s,2).x2 = a2 &
Following(s,2).x3 = a3 &
Following(s,2).x5 = a5 & Following(s,2).x6 = a6 &
Following(s,2).x7 = a7
proof
let x1,x2,x3,x5,x6,x7 be non pair set;
set S = STC0IIStr(x1,x2,x3,x5,x6,x7);
set S1 = BitGFA0Str(x1,x2,x3);
set S2 = BitGFA0Str(x5,x6,x7);
set C = STC0IICirc(x1,x2,x3,x5,x6,x7);
set C1 = BitGFA0Circ(x1,x2,x3);
set C2 = BitGFA0Circ(x5,x6,x7);
set C1out = STC0IICarryOutputC1(x1,x2,x3,x5,x6,x7);
set A1out = STC0IIAdderOutputA1(x1,x2,x3,x5,x6,x7);
set C2out = STC0IICarryOutputC2(x1,x2,x3,x5,x6,x7);
set A2out = STC0IIAdderOutputA2(x1,x2,x3,x5,x6,x7);
let s be State of C;
let a1,a2,a3,a5,a6,a7 be Element of BOOLEAN such that
A1: a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a5 = s.x5 & a6 = s.x6 & a7 = s.x7;
A2: x1 in InputVertices S & x2 in InputVertices S & x3 in InputVertices S &
x5 in InputVertices S & x6 in InputVertices S & x7 in InputVertices S
by ThSTC0IIS8;
reconsider t = s as State of C1+*C2;
reconsider s1 = s|the carrier of S1 as State of C1 by FACIRC_1:26;
A10:dom s1 = the carrier of S1 by CIRCUIT1:3;
C1out in the carrier of S1 & A1out in the carrier of S1 &
InputVertices S1 misses InnerVertices S2 by GFACIRC1:36,LmSTC0IIS09a;
then
A11:Following(t,2).C1out = Following(s1,2).C1out &
Following(t,2).A1out = Following(s1,2).A1out by FACIRC_1:32;
A3: a1 = s1.x1 & a2 = s1.x2 & a3 = s1.x3 by GFACIRC1:36,A1,A10,FUNCT_1:47;
reconsider s2 = s|the carrier of S2 as State of C2 by FACIRC_1:26;
A13:dom s2 = the carrier of S2 by CIRCUIT1:3;
C2out in the carrier of S2 & A2out in the carrier of S2 &
InnerVertices S1 misses InputVertices S2 by GFACIRC1:36,LmSTC0IIS09a;
then
A14:Following(t,2).C2out = Following(s2,2).C2out &
Following(t,2).A2out = Following(s2,2).A2out by FACIRC_1:33;
a5 = s2.x5 & a6 = s2.x6 & a7 = s2.x7 by GFACIRC1:36,A1,A13,FUNCT_1:47;
hence thesis by A1,A2,CIRCCMB3:1,A3,A11,A14,GFACIRC1:39;
end;
:: --------------------------
:: Proposition #1-2 (Stability after Two-steps)
theorem ThSTC0IIS12:
for x1,x2,x3,x5,x6,x7 being non pair set
for s being State of STC0IICirc(x1,x2,x3,x5,x6,x7)
holds Following(s,2) is stable
proof
let x1,x2,x3,x5,x6,x7 be non pair set;
set S1 = BitGFA0Str(x1,x2,x3);
set S2 = BitGFA0Str(x5,x6,x7);
set C = STC0IICirc(x1,x2,x3,x5,x6,x7);
set C1 = BitGFA0Circ(x1,x2,x3);
set C2 = BitGFA0Circ(x5,x6,x7);
set n1=2, n2=2;
A1: InputVertices S1 misses InnerVertices S2 &
InputVertices S2 misses InnerVertices S1 by LmSTC0IIS09a;
let s be State of C;
reconsider s1 = s|the carrier of S1 as State of C1 by FACIRC_1:26;
reconsider s2 = s|the carrier of S2 as State of C2 by FACIRC_1:26;
Following(s1,n1) is stable & Following(s2,n2) is stable by GFACIRC1:40;
then
Following(s,max(n1,n2)) is stable by A1,CIRCCOMB:60,CIRCCMB2:22;
hence thesis;
end;
::=========================================================================
begin :: Properties of `Intermediate' STC Circuit Structure (LAYER-II)
::=========================================================================
::---------------------------------------------------------------
:: 2. `Intermediate' Circuit [Layer-II]
::---------------------------------------------------------------
::---------------------------------------------------------------
:: 2-1. Definition for `Intermediate' Circuit [Layer-II]
::---------------------------------------------------------------
:: Combined Circuit Structure of STC_TYPE0_Inter.
definition
let x1,x2,x3,x4,x5,x6,x7 be set;
func STC0IStr(x1,x2,x3,x4,x5,x6,x7) ->
unsplit gate`1=arity gate`2isBoolean
non void strict non empty ManySortedSign
equals
STC0IIStr(x1,x2,x3,x5,x6,x7) +*
BitGFA0Str(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4);
coherence;
end;
definition
let x1,x2,x3,x4,x5,x6,x7 be set;
func STC0ICirc(x1,x2,x3,x4,x5,x6,x7) ->
strict Boolean gate`2=den Circuit of STC0IStr(x1,x2,x3,x4,x5,x6,x7)
equals
STC0IICirc(x1,x2,x3,x5,x6,x7) +*
BitGFA0Circ(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4);
coherence;
end;
::-----------------------------------------------
:: 2-2. Properties of `Intermediate' STC Circuit Structure
::-----------------------------------------------
:: -----------------------------------
:: InnerVertices of of STC_TYPE0_Inter.
theorem ThSTC0IS1:
for x1,x2,x3,x4,x5,x6,x7 being set holds
InnerVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) =
{[<*x1,x2*>,xor2], GFA0AdderOutput(x1,x2,x3)} \/
{[<*x1,x2*>,and2], [<*x2,x3*>,and2], [<*x3,x1*>,and2],
GFA0CarryOutput(x1,x2,x3)} \/
{[<*x5,x6*>,xor2], GFA0AdderOutput(x5,x6,x7)} \/
{[<*x5,x6*>,and2], [<*x6,x7*>,and2], [<*x7,x5*>,and2],
GFA0CarryOutput(x5,x6,x7)} \/
{[<*GFA0AdderOutput(x1,x2,x3),GFA0AdderOutput(x5,x6,x7)*>,xor2],
GFA0AdderOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4)} \/
{[<*GFA0AdderOutput(x1,x2,x3),GFA0AdderOutput(x5,x6,x7)*>,and2],
[<*GFA0AdderOutput(x5,x6,x7),x4*>,and2],
[<*x4,GFA0AdderOutput(x1,x2,x3)*>,and2],
GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4)}
proof
let x1,x2,x3,x4,x5,x6,x7 be set;
set S = STC0IStr(x1,x2,x3,x4,x5,x6,x7);
set S1 = STC0IIStr(x1,x2,x3,x5,x6,x7);
set A1 = GFA0AdderOutput(x1,x2,x3);
set C1 = GFA0CarryOutput(x1,x2,x3);
set A2 = GFA0AdderOutput(x5,x6,x7);
set C2 = GFA0CarryOutput(x5,x6,x7);
set x1x20 = [<*x1,x2*>, xor2];
set x1x2 = [<*x1,x2*>, and2];
set x2x3 = [<*x2,x3*>, and2];
set x3x1 = [<*x3,x1*>, and2];
set x5x60 = [<*x5,x6*>, xor2];
set x5x6 = [<*x5,x6*>, and2];
set x6x7 = [<*x6,x7*>, and2];
set x7x5 = [<*x7,x5*>, and2];
set S2 = BitGFA0Str(A1,A2,x4);
set A3 = GFA0AdderOutput(A1,A2,x4);
set C3 = GFA0CarryOutput(A1,A2,x4);
set A1A20 = [<*A1,A2*>,xor2];
set A1A2 = [<*A1,A2*>,and2];
set A2x4 = [<*A2,x4*>,and2];
set x4A1 = [<*x4,A1*>,and2];
S1 tolerates S2 by CIRCCOMB:47;
hence InnerVertices S
= (InnerVertices S1) \/ (InnerVertices S2) by CIRCCOMB:11
.= {x1x20,A1} \/ {x1x2,x2x3,x3x1,C1} \/
{x5x60,A2} \/ {x5x6,x6x7,x7x5,C2} \/ (InnerVertices S2) by ThSTC0IIS1
.= {x1x20,A1} \/ {x1x2,x2x3,x3x1,C1} \/
{x5x60,A2} \/ {x5x6,x6x7,x7x5,C2} \/
({A1A20} \/ {A3} \/ {A1A2,A2x4,x4A1} \/ {C3}) by GFACIRC1:31
.= {x1x20,A1} \/ {x1x2,x2x3,x3x1,C1} \/
{x5x60,A2} \/ {x5x6,x6x7,x7x5,C2} \/
({A1A20,A3} \/ {A1A2,A2x4,x4A1} \/ {C3}) by ENUMSET1:1
.= {x1x20,A1} \/ {x1x2,x2x3,x3x1,C1} \/
{x5x60,A2} \/ {x5x6,x6x7,x7x5,C2} \/
({A1A20,A3} \/ ({A1A2,A2x4,x4A1} \/ {C3})) by XBOOLE_1:4
.= {x1x20,A1} \/ {x1x2,x2x3,x3x1,C1} \/
{x5x60,A2} \/ {x5x6,x6x7,x7x5,C2} \/
({A1A20,A3} \/ {A1A2,A2x4,x4A1,C3}) by ENUMSET1:6
.= {x1x20,A1} \/ {x1x2,x2x3,x3x1,C1} \/
{x5x60,A2} \/ {x5x6,x6x7,x7x5,C2} \/
{A1A20,A3} \/ {A1A2,A2x4,x4A1,C3} by XBOOLE_1:4;
end;
theorem :: ThSTC0IS2:
for x1,x2,x3,x4,x5,x6,x7 being set holds
InnerVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) is Relation;
::---------------------------------------
:: InputVertices of of STC_TYPE0_Inter.
LmSTC0IS1:
for x,y,z being set for p being set holds
GFA0AdderOutput(x,y,z) <> [p,and2]
proof
let x,y,z be set, p be set;
GFA0AdderOutput(x,y,z)`2 = xor2;
hence thesis by TWOSCOMP:9,11; :: A1`2 <> [p,and2]`2
end;
LmSTC0IS2b:
for x1,x2,x3,x5,x6,x7 being non pair set
for a,b,c being set
holds
InputVertices STC0IIStr(x1,x2,x3,x5,x6,x7)
misses InnerVertices BitGFA0Str(a,b,c)
proof
let x1,x2,x3,x5,x6,x7 be non pair set;
let a,b,c be set;
set S1 = STC0IIStr(x1,x2,x3,x5,x6,x7);
set S2 = BitGFA0Str(a,b,c);
InputVertices S1 is without_pairs & InnerVertices S2 is Relation
by ThSTC0IIS5;
hence thesis;
end;
theorem ThSTC0IS3:
for x1,x2,x3,x5,x6,x7 being non pair set
for x4 being set st
x4 <> [<*GFA0AdderOutput(x1,x2,x3),GFA0AdderOutput(x5,x6,x7)*>,xor2] &
x4 <> [<*GFA0AdderOutput(x1,x2,x3),GFA0AdderOutput(x5,x6,x7)*>,and2] &
not x4 in InnerVertices STC0IIStr(x1,x2,x3,x5,x6,x7)
holds
InputVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) = {x1,x2,x3,x4,x5,x6,x7}
proof
let x1,x2,x3,x5,x6,x7 be non pair set;
let x4 be set;
set S = STC0IStr(x1,x2,x3,x4,x5,x6,x7);
set S1 = STC0IIStr(x1,x2,x3,x5,x6,x7);
set A1 = GFA0AdderOutput(x1,x2,x3);
set C1 = GFA0CarryOutput(x1,x2,x3);
set A2 = GFA0AdderOutput(x5,x6,x7);
set C2 = GFA0CarryOutput(x5,x6,x7);
set x1x20 = [<*x1,x2*>, xor2];
set x1x2 = [<*x1,x2*>, and2];
set x2x3 = [<*x2,x3*>, and2];
set x3x1 = [<*x3,x1*>, and2];
set x5x60 = [<*x5,x6*>, xor2];
set x5x6 = [<*x5,x6*>, and2];
set x6x7 = [<*x6,x7*>, and2];
set x7x5 = [<*x7,x5*>, and2];
set S2 = BitGFA0Str(A1,A2,x4);
set A1A20 = [<*A1,A2*>,xor2];
set A1A2 = [<*A1,A2*>,and2];
set A2x4 = [<*A2,x4*>,and2];
set x4A1 = [<*x4,A1*>,and2];
assume that
A0: x4 <> A1A20 and
A1: x4 <> A1A2 and
A2: not x4 in InnerVertices S1;
A5: InnerVertices S1
= {x1x20,A1} \/ {x1x2,x2x3,x3x1,C1} \/ {x5x60,A2} \/ {x5x6,x6x7,x7x5,C2}
by ThSTC0IIS1
.= ({A1,x1x20} \/ {A2,x5x60}) \/ {x1x2,x2x3,x3x1,C1} \/ {x5x6,x6x7,x7x5,C2}
by XBOOLE_1:4
.= ({A1,x1x20,A2,x5x60}) \/ {x1x2,x2x3,x3x1,C1} \/ {x5x6,x6x7,x7x5,C2}
by ENUMSET1:5
.= ({A1,A2,x1x20,x5x60}) \/ {x1x2,x2x3,x3x1,C1} \/ {x5x6,x6x7,x7x5,C2}
by ENUMSET1:62
.= ({A1,A2} \/ {x1x20,x5x60}) \/ {x1x2,x2x3,x3x1,C1} \/ {x5x6,x6x7,x7x5,C2}
by ENUMSET1:5
.= {A1,A2} \/ ({x1x20,x5x60} \/ {x1x2,x2x3,x3x1,C1}) \/ {x5x6,x6x7,x7x5,C2}
by XBOOLE_1:4
.= {A1,A2} \/
({x1x20} \/ {x5x60} \/ {x1x2,x2x3,x3x1,C1}) \/ {x5x6,x6x7,x7x5,C2}
by ENUMSET1:1
.= {A1,A2} \/
({x1x20} \/ ({x5x60} \/ {x1x2,x2x3,x3x1,C1})) \/ {x5x6,x6x7,x7x5,C2}
by XBOOLE_1:4
.= {A1,A2} \/ ({x1x20} \/ {x5x60,x1x2,x2x3,x3x1,C1}) \/ {x5x6,x6x7,x7x5,C2}
by ENUMSET1:7
.= {A1,A2} \/
(({x1x20} \/ {x5x60,x1x2,x2x3,x3x1,C1}) \/ {x5x6,x6x7,x7x5,C2})
by XBOOLE_1:4
.= {A1,A2} \/
({x1x20} \/ ({x5x60,x1x2,x2x3,x3x1,C1} \/ {x5x6,x6x7,x7x5,C2}))
by XBOOLE_1:4
.= {A1,A2} \/ ({x1x20} \/ {x5x60,x1x2,x2x3,x3x1,C1,x5x6,x6x7,x7x5,C2})
by ENUMSET1:81
.= {A1,A2} \/ {x5x60,x1x2,x2x3,x3x1,C1,x5x6,x6x7,x7x5,C2,x1x20}
by ENUMSET1:85;
A6: {A1,A2,x4} \ InnerVertices S1
= ({A1,A2} \/ {x4}) \ InnerVertices S1 by ENUMSET1:3
.= ({A1,A2} \ InnerVertices S1) \/ ({x4} \ InnerVertices S1) by XBOOLE_1:42
.= ({A1,A2} \ InnerVertices S1) \/ ({x4}) by A2,ZFMISC_1:59
.= ({}) \/ ({x4}) by A5,XBOOLE_1:46
.= {x4};
A7: A1 <> A2x4 & A2 <> x4A1 by LmSTC0IS1;
InnerVertices S2 misses InputVertices S1 & S1 tolerates S2
by LmSTC0IS2b,CIRCCOMB:47;
hence
InputVertices (S)
= (InputVertices S1) \/ (InputVertices S2 \ InnerVertices S1)
by FACIRC_1:4
.= ({x1,x2,x3,x5,x6,x7}) \/ (InputVertices S2 \ InnerVertices S1)
by ThSTC0IIS4
.= ({x1,x2,x3,x5,x6,x7}) \/ ({x4}) by A0,A1,A7,GFACIRC1:33,A6
.= ({x1,x2,x3} \/ {x5,x6,x7}) \/ ({x4}) by ENUMSET1:13
.= ({x1,x2,x3}) \/ ({x5,x6,x7} \/ ({x4})) by XBOOLE_1:4
.= ({x1,x2,x3}) \/ ({x4,x5,x6,x7}) by ENUMSET1:4
.= {x1,x2,x3,x4,x5,x6,x7} by ENUMSET1:18;
end;
theorem ThSTC0IS4:
for x1,x2,x3,x4,x5,x6,x7 being non pair set holds
InputVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) = {x1,x2,x3,x4,x5,x6,x7}
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
set S1 = STC0IIStr(x1,x2,x3,x5,x6,x7);
{x4} misses InnerVertices S1;
then {x4} \ InnerVertices S1 = {x4} by XBOOLE_1:83;
hence thesis by ZFMISC_1:59,ThSTC0IS3;
end;
theorem ThSTC0IS5:
for x1,x2,x3,x4,x5,x6,x7 being non pair set holds
InputVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) is without_pairs
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
InputVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) = {x1,x2,x3,x4,x5,x6,x7}
by ThSTC0IS4;
hence thesis;
end;
:: -----------------------------------
:: The Element of Carriers, InnerVertices and InputVertices of STC_TYPE0_Inter.
theorem ThSTC0IS6:
for x1,x2,x3,x4,x5,x6,x7 being set holds
x1 in the carrier of STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
x2 in the carrier of STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
x3 in the carrier of STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
x4 in the carrier of STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
x5 in the carrier of STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
x6 in the carrier of STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
x7 in the carrier of STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
[<*x1,x2*>,xor2] in the carrier of STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
GFA0AdderOutput(x1,x2,x3)
in the carrier of STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
[<*x1,x2*>,and2] in the carrier of STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
[<*x2,x3*>,and2] in the carrier of STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
[<*x3,x1*>,and2] in the carrier of STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
GFA0CarryOutput(x1,x2,x3)
in the carrier of STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
[<*GFA0AdderOutput(x1,x2,x3),GFA0AdderOutput(x5,x6,x7)*>,xor2]
in the carrier of STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
GFA0AdderOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4)
in the carrier of STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
[<*GFA0AdderOutput(x1,x2,x3),GFA0AdderOutput(x5,x6,x7)*>,and2]
in the carrier of STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
[<*GFA0AdderOutput(x5,x6,x7),x4*>,and2]
in the carrier of STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
[<*x4,GFA0AdderOutput(x1,x2,x3)*>,and2]
in the carrier of STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4)
in the carrier of STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
[<*x5,x6*>,xor2] in the carrier of STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
GFA0AdderOutput(x5,x6,x7)
in the carrier of STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
[<*x5,x6*>,and2] in the carrier of STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
[<*x6,x7*>,and2] in the carrier of STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
[<*x7,x5*>,and2] in the carrier of STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
GFA0CarryOutput(x5,x6,x7)
in the carrier of STC0IStr(x1,x2,x3,x4,x5,x6,x7)
proof
let x1,x2,x3,x4,x5,x6,x7 be set;
set S = STC0IStr(x1,x2,x3,x4,x5,x6,x7);
set S1 = STC0IIStr(x1,x2,x3,x5,x6,x7);
set A1 = GFA0AdderOutput(x1,x2,x3);
set C1 = GFA0CarryOutput(x1,x2,x3);
set A2 = GFA0AdderOutput(x5,x6,x7);
set C2 = GFA0CarryOutput(x5,x6,x7);
set x1x20 = [<*x1,x2*>, xor2];
set x1x2 = [<*x1,x2*>, and2];
set x2x3 = [<*x2,x3*>, and2];
set x3x1 = [<*x3,x1*>, and2];
set x5x60 = [<*x5,x6*>, xor2];
set x5x6 = [<*x5,x6*>, and2];
set x6x7 = [<*x6,x7*>, and2];
set x7x5 = [<*x7,x5*>, and2];
set S2 = BitGFA0Str(A1,A2,x4);
set A1A20 = [<*A1,A2*>,xor2];
set A1A2 = [<*A1,A2*>,and2];
set A2x4 = [<*A2,x4*>,and2];
set x4A1 = [<*x4,A1*>,and2];
set A3 = GFA0AdderOutput(A1,A2,x4);
set C3 = GFA0CarryOutput(A1,A2,x4);
A1: x1 in the carrier of S1 & x2 in the carrier of S1 &
x3 in the carrier of S1 & x1x20 in the carrier of S1 &
A1 in the carrier of S1 &
x1x2 in the carrier of S1 & x2x3 in the carrier of S1 &
x3x1 in the carrier of S1 &
C1 in the carrier of S1 &
x5 in the carrier of S1 & x6 in the carrier of S1 &
x7 in the carrier of S1 & x5x60 in the carrier of S1 &
A2 in the carrier of S1 &
x5x6 in the carrier of S1 & x6x7 in the carrier of S1 &
x7x5 in the carrier of S1 &
C2 in the carrier of S1 by ThSTC0IIS6;
x4 in the carrier of S2 & A1A20 in the carrier of S2 &
A3 in the carrier of S2 &
A1A2 in the carrier of S2 & A2x4 in the carrier of S2 &
x4A1 in the carrier of S2 &
C3 in the carrier of S2 by GFACIRC1:36;
hence thesis by A1,FACIRC_1:20;
end;
LmSTC0IS7a:
for x,X1,X2,X3 being set
holds x in X1 \/ X2 \/ X3 iff x in X1 or x in X2 or x in X3
proof
let x,X1,X2,X3 be set;
set W = X1 \/ X2 \/ X3;
x in W iff (x in X1 \/ X2) or x in X3 by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
theorem ThSTC0IS7:
for x1,x2,x3,x4,x5,x6,x7 being set holds
[<*x1,x2*>,xor2] in InnerVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
GFA0AdderOutput(x1,x2,x3)
in InnerVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
[<*x1,x2*>,and2] in InnerVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
[<*x2,x3*>,and2] in InnerVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
[<*x3,x1*>,and2] in InnerVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
GFA0CarryOutput(x1,x2,x3)
in InnerVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
[<*GFA0AdderOutput(x1,x2,x3),GFA0AdderOutput(x5,x6,x7)*>,xor2]
in InnerVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
GFA0AdderOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4)
in InnerVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
[<*GFA0AdderOutput(x1,x2,x3),GFA0AdderOutput(x5,x6,x7)*>,and2]
in InnerVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
[<*GFA0AdderOutput(x5,x6,x7),x4*>,and2]
in InnerVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
[<*x4,GFA0AdderOutput(x1,x2,x3)*>,and2]
in InnerVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4)
in InnerVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
[<*x5,x6*>,xor2] in InnerVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
GFA0AdderOutput(x5,x6,x7)
in InnerVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
[<*x5,x6*>,and2] in InnerVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
[<*x6,x7*>,and2] in InnerVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
[<*x7,x5*>,and2] in InnerVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
GFA0CarryOutput(x5,x6,x7)
in InnerVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7)
proof
let x1,x2,x3,x4,x5,x6,x7 be set;
set S = STC0IStr(x1,x2,x3,x4,x5,x6,x7);
set S1 = STC0IIStr(x1,x2,x3,x5,x6,x7);
set A1 = GFA0AdderOutput(x1,x2,x3);
set C1 = GFA0CarryOutput(x1,x2,x3);
set A2 = GFA0AdderOutput(x5,x6,x7);
set C2 = GFA0CarryOutput(x5,x6,x7);
set x1x20 = [<*x1,x2*>, xor2];
set x1x2 = [<*x1,x2*>, and2];
set x2x3 = [<*x2,x3*>, and2];
set x3x1 = [<*x3,x1*>, and2];
set x5x60 = [<*x5,x6*>, xor2];
set x5x6 = [<*x5,x6*>, and2];
set x6x7 = [<*x6,x7*>, and2];
set x7x5 = [<*x7,x5*>, and2];
set S2 = BitGFA0Str(A1,A2,x4);
set A1A20 = [<*A1,A2*>,xor2];
set A1A2 = [<*A1,A2*>,and2];
set A2x4 = [<*A2,x4*>,and2];
set x4A1 = [<*x4,A1*>,and2];
set A3 = GFA0AdderOutput(A1,A2,x4);
set C3 = GFA0CarryOutput(A1,A2,x4);
set p1 = {x1x20,A1,x1x2,x2x3,x3x1,C1};
set p2 = {x5x60,A2,x5x6,x6x7,x7x5,C2};
set p3 = {A1A20,A3,A1A2,A2x4,x4A1,C3};
A1: x1x20 in p1 & A1 in p1 &
x1x2 in p1 & x2x3 in p1 & x3x1 in p1 & C1 in p1 by ENUMSET1:def 4;
A2: x5x60 in p2 & A2 in p2 &
x5x6 in p2 & x6x7 in p2 & x7x5 in p2 & C2 in p2 by ENUMSET1:def 4;
A3: A1A20 in p3 & A3 in p3 &
A1A2 in p3 & A2x4 in p3 & x4A1 in p3 & C3 in p3 by ENUMSET1:def 4;
InnerVertices S =
{x1x20,A1} \/ {x1x2,x2x3,x3x1,C1} \/ {x5x60,A2} \/ {x5x6,x6x7,x7x5,C2} \/
{A1A20,A3} \/ {A1A2,A2x4,x4A1,C3} by ThSTC0IS1
.= p1 \/ {x5x60,A2} \/ {x5x6,x6x7,x7x5,C2} \/
{A1A20,A3} \/ {A1A2,A2x4,x4A1,C3} by ENUMSET1:12
.= p1 \/ ({x5x60,A2} \/ {x5x6,x6x7,x7x5,C2}) \/
{A1A20,A3} \/ {A1A2,A2x4,x4A1,C3} by XBOOLE_1:4
.= p1 \/ p2 \/ {A1A20,A3} \/ {A1A2,A2x4,x4A1,C3} by ENUMSET1:12
.= p1 \/ (p2 \/ {A1A20,A3}) \/ {A1A2,A2x4,x4A1,C3} by XBOOLE_1:4
.= p1 \/ ((p2 \/ {A1A20,A3}) \/ {A1A2,A2x4,x4A1,C3}) by XBOOLE_1:4
.= p1 \/ (p2 \/ ({A1A20,A3} \/ {A1A2,A2x4,x4A1,C3})) by XBOOLE_1:4
.= p1 \/ (p2 \/ ({A1A20,A3,A1A2,A2x4,x4A1,C3})) by ENUMSET1:12
.= p1 \/ p2 \/ p3 by XBOOLE_1:4;
hence thesis by A1,A2,A3,LmSTC0IS7a;
end;
theorem :: ThSTC0IS8:
for x1,x2,x3,x5,x6,x7 being non pair set
for x4 being set st
x4 <> [<*GFA0AdderOutput(x1,x2,x3),GFA0AdderOutput(x5,x6,x7)*>,xor2] &
x4 <> [<*GFA0AdderOutput(x1,x2,x3),GFA0AdderOutput(x5,x6,x7)*>,and2] &
not x4 in InnerVertices STC0IIStr(x1,x2,x3,x5,x6,x7)
holds
x1 in InputVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
x2 in InputVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
x3 in InputVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
x4 in InputVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
x5 in InputVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
x6 in InputVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
x7 in InputVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7)
proof
let x1,x2,x3,x5,x6,x7 be non pair set;
let x4 be set;
set S = STC0IStr(x1,x2,x3,x4,x5,x6,x7);
set S1 = STC0IIStr(x1,x2,x3,x5,x6,x7);
set A1 = GFA0AdderOutput(x1,x2,x3);
set A2 = GFA0AdderOutput(x5,x6,x7);
set A1A20 = [<*A1,A2*>,xor2];
set A1A2 = [<*A1,A2*>,and2];
assume x4 <> A1A20 & x4 <> A1A2 & not x4 in InnerVertices S1;
then InputVertices S = {x1,x2,x3,x4,x5,x6,x7} by ThSTC0IS3;
hence thesis by ENUMSET1:def 5;
end;
theorem ThSTC0IS9:
for x1,x2,x3,x4,x5,x6,x7 being non pair set holds
x1 in InputVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
x2 in InputVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
x3 in InputVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
x4 in InputVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
x5 in InputVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
x6 in InputVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) &
x7 in InputVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7)
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
set S = STC0IStr(x1,x2,x3,x4,x5,x6,x7);
InputVertices S = {x1,x2,x3,x4,x5,x6,x7} by ThSTC0IS4;
hence thesis by ENUMSET1:def 5;
end;
::-------------------------------------------
:: 2-3. Output Definitions of the Combined Circuit
::-------------------------------------------
:: Def. External/Internal Signal Outputs of of STC_TYPE0_Inter.
definition
let x1,x2,x3,x4,x5,x6,x7 be set;
func STC0ICarryOutputC1(x1,x2,x3,x4,x5,x6,x7) ->
Element of InnerVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) equals
GFA0CarryOutput(x1,x2,x3);
coherence by ThSTC0IS7;
func STC0ICarryOutputC2(x1,x2,x3,x4,x5,x6,x7) ->
Element of InnerVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) equals
GFA0CarryOutput(x5,x6,x7);
coherence by ThSTC0IS7;
func STC0ICarryOutputC3(x1,x2,x3,x4,x5,x6,x7) ->
Element of InnerVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) equals
GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),GFA0AdderOutput(x5,x6,x7),x4);
coherence by ThSTC0IS7;
func STC0IAdderOutputA3(x1,x2,x3,x4,x5,x6,x7) ->
Element of InnerVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) equals
GFA0AdderOutput(GFA0AdderOutput(x1,x2,x3),GFA0AdderOutput(x5,x6,x7),x4);
coherence by ThSTC0IS7;
end;
::----------------------------------------------------
:: 2-4. Outputs of the Combined Circuit and its Stability
::---------------------------------------------------
::===================================================
:: Temporal (Internal) Calculations after 2,4-steps
::===================================================
LmSTC0IS15s2: :: Lm2 (step-2, common)
for x1,x2,x3,x4,x5,x6,x7 being non pair set
for s being State of STC0ICirc(x1,x2,x3,x4,x5,x6,x7)
for a1,a2,a3,a4,a5,a6,a7 being Element of BOOLEAN st
a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7
holds Following(s,2).STC0IICarryOutputC1(x1,x2,x3,x5,x6,x7)
= (a1 '&' a2) 'or' (a2 '&' a3) 'or' (a3 '&' a1) &
Following(s,2).STC0IICarryOutputC2(x1,x2,x3,x5,x6,x7)
= (a5 '&' a6) 'or' (a6 '&' a7) 'or' (a7 '&' a5) &
Following(s,2).STC0IIAdderOutputA1(x1,x2,x3,x5,x6,x7)
= a1 'xor' a2 'xor' a3 &
Following(s,2).STC0IIAdderOutputA2(x1,x2,x3,x5,x6,x7)
= a5 'xor' a6 'xor' a7 &
Following(s,2).x1 = a1 & Following(s,2).x2 = a2 &
Following(s,2).x3 = a3 & Following(s,2).x4 = a4 &
Following(s,2).x5 = a5 & Following(s,2).x6 = a6 &
Following(s,2).x7 = a7
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
set S = STC0IStr(x1,x2,x3,x4,x5,x6,x7);
set C = STC0ICirc(x1,x2,x3,x4,x5,x6,x7);
set S1 = STC0IIStr(x1,x2,x3,x5,x6,x7);
set C1 = STC0IICirc(x1,x2,x3,x5,x6,x7);
set A1out = GFA0AdderOutput(x1,x2,x3);
set A2out = GFA0AdderOutput(x5,x6,x7);
set C1out = GFA0CarryOutput(x1,x2,x3);
set C2out = GFA0CarryOutput(x5,x6,x7);
set S2 = BitGFA0Str(A1out,A2out,x4);
set C2 = BitGFA0Circ(A1out,A2out,x4);
let s be State of C;
let a1,a2,a3,a4,a5,a6,a7 be Element of BOOLEAN such that
A2: a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7;
A3: x1 in InputVertices S & x2 in InputVertices S & x3 in InputVertices S &
x4 in InputVertices S & x5 in InputVertices S & x6 in InputVertices S &
x7 in InputVertices S
by ThSTC0IS9;
reconsider t = s as State of C1+*C2;
reconsider s1 = s|the carrier of S1 as State of C1 by FACIRC_1:26;
A4: dom s1 = the carrier of S1 by CIRCUIT1:3;
C1out in the carrier of S1 & C2out in the carrier of S1 &
A1out in the carrier of S1 & A2out in the carrier of S1 &
InputVertices S1 misses InnerVertices S2 by ThSTC0IIS6,LmSTC0IS2b;
then
A5: Following(t,2).C1out = Following(s1,2).C1out &
Following(t,2).C2out = Following(s1,2).C2out &
Following(t,2).A1out = Following(s1,2).A1out &
Following(t,2).A2out = Following(s1,2).A2out by FACIRC_1:32;
a1 = s1.x1 & a2 = s1.x2 & a3 = s1.x3 &
a5 = s1.x5 & a6 = s1.x6 & a7 = s1.x7 by ThSTC0IIS6,A2,A4,FUNCT_1:47;
hence thesis by A2,A3,CIRCCMB3:1,A5,ThSTC0IIS10;
end;
:: --------------------------
:: for Output C1
LmSTC0IS15C1: :: Lm10 (step-2)
for x1,x2,x3,x4,x5,x6,x7 being non pair set
for s being State of STC0ICirc(x1,x2,x3,x4,x5,x6,x7)
for a1,a2,a3,a4,a5,a6,a7 being Element of BOOLEAN st
a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7
holds Following(s,2).STC0ICarryOutputC1(x1,x2,x3,x4,x5,x6,x7)
= (a1 '&' a2) 'or' (a2 '&' a3) 'or' (a3 '&' a1)
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
set C = STC0ICirc(x1,x2,x3,x4,x5,x6,x7);
set S1 = STC0IIStr(x1,x2,x3,x5,x6,x7);
set C1 = STC0IICirc(x1,x2,x3,x5,x6,x7);
set A1out = GFA0AdderOutput(x1,x2,x3);
set A2out = GFA0AdderOutput(x5,x6,x7);
set S2 = BitGFA0Str(A1out,A2out,x4);
set C2 = BitGFA0Circ(A1out,A2out,x4);
set C1out = STC0IICarryOutputC1(x1,x2,x3,x5,x6,x7);
let s be State of C;
let a1,a2,a3,a4,a5,a6,a7 be Element of BOOLEAN such that
A2: a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7;
reconsider t = s as State of C1+*C2;
reconsider s1 = s|the carrier of S1 as State of C1 by FACIRC_1:26;
A3: dom s1 = the carrier of S1 by CIRCUIT1:3;
C1out in the carrier of S1 &
InputVertices S1 misses InnerVertices S2
by LmSTC0IS2b;
then
A4: Following(t,2).C1out = Following(s1,2).C1out by FACIRC_1:32;
a1 = s1.x1 & a2 = s1.x2 & a3 = s1.x3 &
a5 = s1.x5 & a6 = s1.x6 & a7 = s1.x7 by ThSTC0IIS6,A2,A3,FUNCT_1:47;
hence thesis by A4,ThSTC0IIS10;
end;
:: --------------------------
:: for Output C2
LmSTC0IS15C2: :: Lm10 (step-2)
for x1,x2,x3,x4,x5,x6,x7 being non pair set
for s being State of STC0ICirc(x1,x2,x3,x4,x5,x6,x7)
for a1,a2,a3,a4,a5,a6,a7 being Element of BOOLEAN st
a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7
holds Following(s,2).STC0ICarryOutputC2(x1,x2,x3,x4,x5,x6,x7)
= (a5 '&' a6) 'or' (a6 '&' a7) 'or' (a7 '&' a5)
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
set C = STC0ICirc(x1,x2,x3,x4,x5,x6,x7);
set S1 = STC0IIStr(x1,x2,x3,x5,x6,x7);
set C1 = STC0IICirc(x1,x2,x3,x5,x6,x7);
set A1out = GFA0AdderOutput(x1,x2,x3);
set A2out = GFA0AdderOutput(x5,x6,x7);
set S2 = BitGFA0Str(A1out,A2out,x4);
set C2 = BitGFA0Circ(A1out,A2out,x4);
set C2out = STC0IICarryOutputC2(x1,x2,x3,x5,x6,x7);
let s be State of C;
let a1,a2,a3,a4,a5,a6,a7 be Element of BOOLEAN such that
A2: a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7;
reconsider t = s as State of C1+*C2;
reconsider s1 = s|the carrier of S1 as State of C1 by FACIRC_1:26;
A3: dom s1 = the carrier of S1 by CIRCUIT1:3;
C2out in the carrier of S1 &
InputVertices S1 misses InnerVertices S2
by LmSTC0IS2b;
then
A4: Following(t,2).C2out = Following(s1,2).C2out by FACIRC_1:32;
a1 = s1.x1 & a2 = s1.x2 & a3 = s1.x3 &
a5 = s1.x5 & a6 = s1.x6 & a7 = s1.x7 by ThSTC0IIS6,A2,A3,FUNCT_1:47;
hence thesis by A4,ThSTC0IIS10;
end;
:: --------------------------
:: for Output C3
LmSTC0IS15C3s4: :: Lm4 (step-3)
for x1,x2,x3,x4,x5,x6,x7 being non pair set
for s being State of STC0ICirc(x1,x2,x3,x4,x5,x6,x7)
for a123,a567,a4 being Element of BOOLEAN st
a123 = s.GFA0AdderOutput(x1,x2,x3) &
a567 = s.GFA0AdderOutput(x5,x6,x7) &
a4 = s.x4
holds (Following s).[<*GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7)*>,and2] = a123 '&' a567 &
(Following s).[<*GFA0AdderOutput(x5,x6,x7),x4*>,and2] = a567 '&' a4 &
(Following s).[<*x4,GFA0AdderOutput(x1,x2,x3)*>,and2] = a4 '&' a123
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
set S = STC0IStr(x1,x2,x3,x4,x5,x6,x7);
set C = STC0ICirc(x1,x2,x3,x4,x5,x6,x7);
set A1out = GFA0AdderOutput(x1,x2,x3);
set A2out = GFA0AdderOutput(x5,x6,x7);
set A1A2 = [<*A1out,A2out*>,and2];
set A2x4 = [<*A2out,x4*>,and2];
set x4A1 = [<*x4,A1out*>,and2];
let s be State of C;
let a123,a567,a4 be Element of BOOLEAN such that
A1: a123 = s.A1out and
A2: a567 = s.A2out and
A3: a4 = s.x4;
A4: dom s = the carrier of S by CIRCUIT1:3;
A5: A1out in the carrier of S by ThSTC0IS6;
A6: A2out in the carrier of S by ThSTC0IS6;
A7: InnerVertices S = the carrier' of S by FACIRC_1:37;
hence
(Following s).A1A2 = and2.(s*<*A1out,A2out*>) by ThSTC0IS7,FACIRC_1:35
.= and2.<*a123, a567*> by A1,A2,A5,A6,A4,FINSEQ_2:125
.= a123 '&' a567 by FACIRC_1:def 6;
A8: x4 in the carrier of S by ThSTC0IS6;
thus
(Following s).A2x4 = and2.(s*<*A2out,x4*>) by A7,ThSTC0IS7,FACIRC_1:35
.= and2.<*a567, a4*> by A2,A3,A6,A8,A4,FINSEQ_2:125
.= a567 '&' a4 by FACIRC_1:def 6;
thus
(Following s).x4A1 = and2.(s*<*x4,A1out*>) by A7,ThSTC0IS7,FACIRC_1:35
.= and2.<*a4, a123*> by A3,A1,A8,A5,A4,FINSEQ_2:125
.= a4 '&' a123 by FACIRC_1:def 6;
end;
LmSTC0IS15C3s6: :: Lm6 (step-3)
for x1,x2,x3,x4,x5,x6,x7 being non pair set
for s being State of STC0ICirc(x1,x2,x3,x4,x5,x6,x7)
for a1,a2,a3,a4,a5,a6,a7 being Element of BOOLEAN st
a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7
holds Following(s,3).[<*GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7)*>,and2]
= (a1 'xor' a2 'xor' a3) '&' (a5 'xor' a6 'xor' a7) &
Following(s,3).[<*GFA0AdderOutput(x5,x6,x7),x4*>,and2]
= (a5 'xor' a6 'xor' a7) '&' a4 &
Following(s,3).[<*x4,GFA0AdderOutput(x1,x2,x3)*>,and2]
= a4 '&' (a1 'xor' a2 'xor' a3) &
Following(s,3).x1 = a1 & Following(s,3).x2 = a2 &
Following(s,3).x3 = a3 & Following(s,3).x4 = a4 &
Following(s,3).x5 = a5 & Following(s,3).x6 = a6 &
Following(s,3).x7 = a7
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
set S = STC0IStr(x1,x2,x3,x4,x5,x6,x7);
set C = STC0ICirc(x1,x2,x3,x4,x5,x6,x7);
set A1out = GFA0AdderOutput(x1,x2,x3);
set A2out = GFA0AdderOutput(x5,x6,x7);
let s be State of C;
let a1,a2,a3,a4,a5,a6,a7 be Element of BOOLEAN such that
A2: a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7;
A3: x1 in InputVertices S & x2 in InputVertices S & x3 in InputVertices S &
x4 in InputVertices S & x5 in InputVertices S & x6 in InputVertices S &
x7 in InputVertices S
by ThSTC0IS9;
A4: Following(s,2+1) = Following Following(s,2) by FACIRC_1:12;
Following(s,2).STC0IIAdderOutputA1(x1,x2,x3,x5,x6,x7)
= a1 'xor' a2 'xor' a3 &
Following(s,2).STC0IIAdderOutputA2(x1,x2,x3,x5,x6,x7)
= a5 'xor' a6 'xor' a7 by A2,LmSTC0IS15s2;
then
Following(s,2).A1out = a1 'xor' a2 'xor' a3 &
Following(s,2).A2out = a5 'xor' a6 'xor' a7 &
Following(s,2).x4 = a4 by A2,LmSTC0IS15s2;
hence thesis by A2,A3,CIRCCMB3:1,A4,LmSTC0IS15C3s4;
end;
LmSTC0IS15C3s8: :: Lm8 (step-4)
for x1,x2,x3,x5,x6,x7 being non pair set
for x4 being set
for s being State of STC0ICirc(x1,x2,x3,x4,x5,x6,x7)
for a123567,a567x4,ax4123 being Element of BOOLEAN st
a123567 = s.[<*GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7)*>,and2] &
a567x4 = s.[<*GFA0AdderOutput(x5,x6,x7),x4*>,and2] &
ax4123 = s.[<*x4,GFA0AdderOutput(x1,x2,x3)*>,and2]
holds (Following s).GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4)
= a123567 'or' a567x4 'or' ax4123
proof
let x1,x2,x3,x5,x6,x7 be non pair set;
let x4 be set;
set S = STC0IStr(x1,x2,x3,x4,x5,x6,x7);
set C = STC0ICirc(x1,x2,x3,x4,x5,x6,x7);
set A1out = GFA0AdderOutput(x1,x2,x3);
set A2out = GFA0AdderOutput(x5,x6,x7);
set A1A2 = [<*A1out,A2out*>,and2];
set A2x4 = [<*A2out,x4*>,and2];
set x4A1 = [<*x4,A1out*>,and2];
let s be State of C;
let a123567,a567x4,ax4123 be Element of BOOLEAN such that
A1: a123567 = s.A1A2 & a567x4 = s.A2x4 & ax4123 = s.x4A1;
A2: dom s = the carrier of S by CIRCUIT1:3;
A3: A1A2 in the carrier of S & A2x4 in the carrier of S &
x4A1 in the carrier of S by ThSTC0IS6;
InnerVertices S = the carrier' of S by FACIRC_1:37;
hence
(Following s).GFA0CarryOutput(A1out,A2out,x4)
= or3.(s*<*A1A2,A2x4,x4A1*>) by ThSTC0IS7,FACIRC_1:35
.= or3.<*a123567, a567x4, ax4123*> by A1,A3,A2,FINSEQ_2:126
.= a123567 'or' a567x4 'or' ax4123 by FACIRC_1:def 7;
end;
LmSTC0IS15C3: :: Lm10 (step-4)
for x1,x2,x3,x4,x5,x6,x7 being non pair set
for s being State of STC0ICirc(x1,x2,x3,x4,x5,x6,x7)
for a1,a2,a3,a4,a5,a6,a7 being Element of BOOLEAN st
a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7
holds Following(s,4).STC0ICarryOutputC3(x1,x2,x3,x4,x5,x6,x7)
= ((a1 'xor' a2 'xor' a3) '&' (a5 'xor' a6 'xor' a7)) 'or'
((a5 'xor' a6 'xor' a7) '&' a4) 'or'
(a4 '&' (a1 'xor' a2 'xor' a3)) &
Following(s,4).x1 = a1 & Following(s,4).x2 = a2 &
Following(s,4).x3 = a3 & Following(s,4).x4 = a4 &
Following(s,4).x5 = a5 & Following(s,4).x6 = a6 &
Following(s,4).x7 = a7
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
set S = STC0IStr(x1,x2,x3,x4,x5,x6,x7);
set C = STC0ICirc(x1,x2,x3,x4,x5,x6,x7);
set A1out = GFA0AdderOutput(x1,x2,x3);
set A2out = GFA0AdderOutput(x5,x6,x7);
set A1A2 = [<*A1out,A2out*>,and2];
set A2x4 = [<*A2out,x4*>,and2];
set x4A1 = [<*x4,A1out*>,and2];
let s be State of C;
let a1,a2,a3,a4,a5,a6,a7 be Element of BOOLEAN such that
A2: a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7;
A3: x1 in InputVertices S & x2 in InputVertices S & x3 in InputVertices S &
x4 in InputVertices S & x5 in InputVertices S & x6 in InputVertices S &
x7 in InputVertices S
by ThSTC0IS9;
A4: Following(s,3+1) = Following Following(s,3) by FACIRC_1:12;
Following(s,3).A1A2 = (a1 'xor' a2 'xor' a3) '&' (a5 'xor' a6 'xor' a7) &
Following(s,3).A2x4 = (a5 'xor' a6 'xor' a7) '&' a4 &
Following(s,3).x4A1 = a4 '&' (a1 'xor' a2 'xor' a3) &
Following(s,3).x4 = a4 by A2,LmSTC0IS15C3s6;
hence thesis by A2,A3,CIRCCMB3:1,A4,LmSTC0IS15C3s8;
end;
:: --------------------------
:: for Output A3
LmSTC0IS15A3s4: :: Lm4 (step-3)
for x1,x2,x3,x4,x5,x6,x7 being non pair set
for s being State of STC0ICirc(x1,x2,x3,x4,x5,x6,x7)
for a123,a567 being Element of BOOLEAN st
a123 = s.GFA0AdderOutput(x1,x2,x3) & a567 = s.GFA0AdderOutput(x5,x6,x7)
holds (Following s).[<*GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7)*>,xor2]
= a123 'xor' a567
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
set S = STC0IStr(x1,x2,x3,x4,x5,x6,x7);
set C = STC0ICirc(x1,x2,x3,x4,x5,x6,x7);
set A1out = GFA0AdderOutput(x1,x2,x3);
set A2out = GFA0AdderOutput(x5,x6,x7);
set A1A20 = [<*A1out,A2out*>,xor2];
let s be State of C;
let a123, a567 be Element of BOOLEAN such that
A1: a123 = s.A1out & a567 = s.A2out;
A2: dom s = the carrier of S by CIRCUIT1:3;
A3: A1out in the carrier of S & A2out in the carrier of S by ThSTC0IS6;
InnerVertices S = the carrier' of S by FACIRC_1:37;
hence
(Following s).A1A20
= xor2.(s*<*A1out,A2out*>) by ThSTC0IS7,FACIRC_1:35
.= xor2.<*a123, a567*> by A1,A3,A2,FINSEQ_2:125
.= a123 'xor' a567 by FACIRC_1:def 4;
end;
LmSTC0IS15A3s6: :: Lm6 (step-3)
for x1,x2,x3,x4,x5,x6,x7 being non pair set
for s being State of STC0ICirc(x1,x2,x3,x4,x5,x6,x7)
for a1,a2,a3,a4,a5,a6,a7 being Element of BOOLEAN st
a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7
holds Following(s,3).[<*GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7)*>,xor2]
= (a1 'xor' a2 'xor' a3) 'xor' (a5 'xor' a6 'xor' a7) &
Following(s,3).x1 = a1 & Following(s,3).x2 = a2 &
Following(s,3).x3 = a3 & Following(s,3).x4 = a4 &
Following(s,3).x5 = a5 & Following(s,3).x6 = a6 &
Following(s,3).x7 = a7
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
set S = STC0IStr(x1,x2,x3,x4,x5,x6,x7);
set C = STC0ICirc(x1,x2,x3,x4,x5,x6,x7);
let s be State of C;
let a1,a2,a3,a4,a5,a6,a7 be Element of BOOLEAN such that
A2: a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7;
A3: x1 in InputVertices S & x2 in InputVertices S & x3 in InputVertices S &
x4 in InputVertices S & x5 in InputVertices S & x6 in InputVertices S &
x7 in InputVertices S
by ThSTC0IS9;
A4: Following(s,2+1) = Following Following(s,2) by FACIRC_1:12;
Following(s,2).STC0IIAdderOutputA1(x1,x2,x3,x5,x6,x7)
= a1 'xor' a2 'xor' a3 &
Following(s,2).STC0IIAdderOutputA2(x1,x2,x3,x5,x6,x7)
= a5 'xor' a6 'xor' a7 by A2,LmSTC0IS15s2;
hence thesis by A2,A3,CIRCCMB3:1,A4,LmSTC0IS15A3s4;
end;
LmSTC0IS15A3s8: :: Lm8 (step-4)
for x1,x2,x3,x5,x6,x7 being non pair set
for x4 being set
for s being State of STC0ICirc(x1,x2,x3,x4,x5,x6,x7)
for a123567,a4 being Element of BOOLEAN st
a123567 = s.[<*GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7)*>,xor2] &
a4 = s.x4
holds (Following s).GFA0AdderOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4)
= a123567 'xor' a4
proof
let x1,x2,x3,x5,x6,x7 be non pair set;
let x4 be set;
set S = STC0IStr(x1,x2,x3,x4,x5,x6,x7);
set C = STC0ICirc(x1,x2,x3,x4,x5,x6,x7);
set A1out = GFA0AdderOutput(x1,x2,x3);
set A2out = GFA0AdderOutput(x5,x6,x7);
set A1A20 = [<*A1out,A2out*>,xor2];
let s be State of C;
let a123567, a4 be Element of BOOLEAN such that
A1: a123567 = s.A1A20 & a4 = s.x4;
A2: dom s = the carrier of S by CIRCUIT1:3;
A3: A1A20 in the carrier of S & x4 in the carrier of S by ThSTC0IS6;
InnerVertices S = the carrier' of S by FACIRC_1:37;
hence
(Following s).GFA0AdderOutput(A1out,A2out,x4)
= xor2.(s*<*A1A20,x4*>) by ThSTC0IS7,FACIRC_1:35
.= xor2.<*a123567, a4*> by A1,A2,A3,FINSEQ_2:125
.= a123567 'xor' a4 by FACIRC_1:def 4;
end;
LmSTC0IS15A3: :: Lm10 (step-4)
for x1,x2,x3,x4,x5,x6,x7 being non pair set
for s being State of STC0ICirc(x1,x2,x3,x4,x5,x6,x7)
for a1,a2,a3,a4,a5,a6,a7 being Element of BOOLEAN st
a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7
holds Following(s,4).STC0IAdderOutputA3(x1,x2,x3,x4,x5,x6,x7)
= a1 'xor' a2 'xor' a3 'xor' a4 'xor' a5 'xor' a6 'xor' a7 &
Following(s,4).x1 = a1 & Following(s,4).x2 = a2 &
Following(s,4).x3 = a3 & Following(s,4).x4 = a4 &
Following(s,4).x5 = a5 & Following(s,4).x6 = a6 &
Following(s,4).x7 = a7
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
set S = STC0IStr(x1,x2,x3,x4,x5,x6,x7);
set C = STC0ICirc(x1,x2,x3,x4,x5,x6,x7);
set A1out = GFA0AdderOutput(x1,x2,x3);
set A2out = GFA0AdderOutput(x5,x6,x7);
set A1A20 = [<*A1out,A2out*>,xor2];
set A3out = STC0IAdderOutputA3(x1,x2,x3,x4,x5,x6,x7);
let s be State of C;
let a1,a2,a3,a4,a5,a6,a7 be Element of BOOLEAN such that
A2: a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7;
A3: x1 in InputVertices S & x2 in InputVertices S & x3 in InputVertices S &
x4 in InputVertices S & x5 in InputVertices S & x6 in InputVertices S &
x7 in InputVertices S
by ThSTC0IS9;
A4: Following(s,3+1) = Following Following(s,3) by FACIRC_1:12;
A5: Following(s,3).A1A20
= (a1 'xor' a2 'xor' a3) 'xor' (a5 'xor' a6 'xor' a7) &
Following(s,3).x4 = a4 by A2,LmSTC0IS15A3s6;
Following(s,4).A3out
= (a1 'xor' a2 'xor' a3) 'xor' (a5 'xor' a6 'xor' a7) 'xor' a4
by A4,A5,LmSTC0IS15A3s8
.= ((a1 'xor' a2 'xor' a3) 'xor' (a5 'xor' a6)) 'xor' a7 'xor' a4
by XBOOLEAN:73
.= ((a1 'xor' a2 'xor' a3) 'xor' a5) 'xor' a6 'xor' a7 'xor' a4
by XBOOLEAN:73
.= (a1 'xor' a2 'xor' a3) 'xor' a5 'xor' a6 'xor' a4 'xor' a7
by XBOOLEAN:73
.= (a1 'xor' a2 'xor' a3) 'xor' a5 'xor' a4 'xor' a6 'xor' a7
by XBOOLEAN:73
.= (a1 'xor' a2 'xor' a3) 'xor' a4 'xor' a5 'xor' a6 'xor' a7
by XBOOLEAN:73;
hence thesis by A2,A3,CIRCCMB3:1;
end;
:: -----------------------------------
:: Proposition #2-1 (Internal Circuit Outputs after 2,4-steps)
theorem :: ThSTC0IS17: :: for Output C1, C2, C3 and A3
for x1,x2,x3,x4,x5,x6,x7 being non pair set
for s being State of STC0ICirc(x1,x2,x3,x4,x5,x6,x7)
for a1,a2,a3,a4,a5,a6,a7 being Element of BOOLEAN st
a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7
holds Following(s,2).STC0ICarryOutputC1(x1,x2,x3,x4,x5,x6,x7)
= (a1 '&' a2) 'or' (a2 '&' a3) 'or' (a3 '&' a1) &
Following(s,2).STC0ICarryOutputC2(x1,x2,x3,x4,x5,x6,x7)
= (a5 '&' a6) 'or' (a6 '&' a7) 'or' (a7 '&' a5) &
Following(s,4).STC0ICarryOutputC3(x1,x2,x3,x4,x5,x6,x7)
= ((a1 'xor' a2 'xor' a3) '&' (a5 'xor' a6 'xor' a7)) 'or'
((a5 'xor' a6 'xor' a7) '&' a4) 'or'
(a4 '&' (a1 'xor' a2 'xor' a3)) &
Following(s,4).STC0IAdderOutputA3(x1,x2,x3,x4,x5,x6,x7)
= a1 'xor' a2 'xor' a3 'xor' a4 'xor' a5 'xor' a6 'xor' a7 &
Following(s,4).x1 = a1 & Following(s,4).x2 = a2 &
Following(s,4).x3 = a3 & Following(s,4).x4 = a4 &
Following(s,4).x5 = a5 & Following(s,4).x6 = a6 &
Following(s,4).x7 = a7
by LmSTC0IS15C1,LmSTC0IS15C2,LmSTC0IS15C3,LmSTC0IS15A3;
:: --------------------------
:: Proposition #2-2 (Stability after Four-steps)
theorem ThSTC0IS18:
for x1,x2,x3,x4,x5,x6,x7 being non pair set
for s being State of STC0ICirc(x1,x2,x3,x4,x5,x6,x7)
holds Following(s,4) is stable
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
set C = STC0ICirc(x1,x2,x3,x4,x5,x6,x7);
set S1 = STC0IIStr(x1,x2,x3,x5,x6,x7);
set C1 = STC0IICirc(x1,x2,x3,x5,x6,x7);
set A1out = GFA0AdderOutput(x1,x2,x3);
set A2out = GFA0AdderOutput(x5,x6,x7);
set S2 = BitGFA0Str(A1out,A2out,x4);
set C2 = BitGFA0Circ(A1out,A2out,x4);
set n1=2, n2=2;
let s be State of C;
C1 tolerates C2 by CIRCCOMB:60;
then
A2: the Sorts of C1 tolerates the Sorts of C2 by CIRCCOMB:def 3;
then reconsider s1 = s|the carrier of S1 as State of C1 by CIRCCOMB:26;
reconsider s2 = Following(s,n1)|the carrier of S2 as State of C2
by A2,CIRCCOMB:26;
A3: InputVertices S1 misses InnerVertices S2 & Following(s1,n1) is stable
by LmSTC0IS2b,ThSTC0IIS12;
A1out <> [<*A2out,x4*>,and2] & A2out <> [<*x4,A1out*>,and2] by LmSTC0IS1;
then Following(s2,n2) is stable by GFACIRC1:40;
then Following(s,n1+n2) is stable by A3,CIRCCMB2:19,CIRCCOMB:60;
hence thesis;
end;
::=========================================================================
begin :: Properties of STC Circuit Structure (LAYER-III)
::=========================================================================
::---------------------------------------------------------------
:: 3. STC Circuit [Layer-III]
::---------------------------------------------------------------
::---------------------------------------------------------------
:: 3-1. Definition for STC Circuit [Layer-III]
::---------------------------------------------------------------
:: Combined Circuit Structure of STC_TYPE0.
definition
let x1,x2,x3,x4,x5,x6,x7 be set;
func STC0Str(x1,x2,x3,x4,x5,x6,x7) ->
unsplit gate`1=arity gate`2isBoolean
non void strict non empty ManySortedSign
equals
STC0IStr(x1,x2,x3,x4,x5,x6,x7) +*
BitGFA0Str(STC0ICarryOutputC1(x1,x2,x3,x4,x5,x6,x7),
STC0ICarryOutputC2(x1,x2,x3,x4,x5,x6,x7),
STC0ICarryOutputC3(x1,x2,x3,x4,x5,x6,x7));
coherence;
end;
definition
let x1,x2,x3,x4,x5,x6,x7 be set;
func STC0Circ(x1,x2,x3,x4,x5,x6,x7) ->
strict Boolean gate`2=den Circuit of STC0Str(x1,x2,x3,x4,x5,x6,x7)
equals
STC0ICirc(x1,x2,x3,x4,x5,x6,x7) +*
BitGFA0Circ(STC0ICarryOutputC1(x1,x2,x3,x4,x5,x6,x7),
STC0ICarryOutputC2(x1,x2,x3,x4,x5,x6,x7),
STC0ICarryOutputC3(x1,x2,x3,x4,x5,x6,x7));
coherence;
end;
::-----------------------------------------------
:: 3-2. Properties of STC Circuit Structure
::-----------------------------------------------
:: -----------------------------------
:: InnerVertices of of STC_TYPE0
theorem ThSTC0S1a:
for x1,x2,x3,x4,x5,x6,x7 being set holds
InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) =
InnerVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7) \/
{[<*STC0ICarryOutputC1(x1,x2,x3,x4,x5,x6,x7),
STC0ICarryOutputC2(x1,x2,x3,x4,x5,x6,x7)*>,xor2],
GFA0AdderOutput(STC0ICarryOutputC1(x1,x2,x3,x4,x5,x6,x7),
STC0ICarryOutputC2(x1,x2,x3,x4,x5,x6,x7),
STC0ICarryOutputC3(x1,x2,x3,x4,x5,x6,x7))} \/
{[<*STC0ICarryOutputC1(x1,x2,x3,x4,x5,x6,x7),
STC0ICarryOutputC2(x1,x2,x3,x4,x5,x6,x7)*>,and2],
[<*STC0ICarryOutputC2(x1,x2,x3,x4,x5,x6,x7),
STC0ICarryOutputC3(x1,x2,x3,x4,x5,x6,x7)*>,and2],
[<*STC0ICarryOutputC3(x1,x2,x3,x4,x5,x6,x7),
STC0ICarryOutputC1(x1,x2,x3,x4,x5,x6,x7)*>,and2],
GFA0CarryOutput(STC0ICarryOutputC1(x1,x2,x3,x4,x5,x6,x7),
STC0ICarryOutputC2(x1,x2,x3,x4,x5,x6,x7),
STC0ICarryOutputC3(x1,x2,x3,x4,x5,x6,x7))}
proof
let x1,x2,x3,x4,x5,x6,x7 be set;
set S = STC0Str(x1,x2,x3,x4,x5,x6,x7);
set S1 = STC0IStr(x1,x2,x3,x4,x5,x6,x7);
set C1 = STC0ICarryOutputC1(x1,x2,x3,x4,x5,x6,x7);
set C2 = STC0ICarryOutputC2(x1,x2,x3,x4,x5,x6,x7);
set C3 = STC0ICarryOutputC3(x1,x2,x3,x4,x5,x6,x7);
set S2 = BitGFA0Str(C1,C2,C3);
set C1C2x = [<*C1,C2*>, xor2];
set C1C2a = [<*C1,C2*>, and2];
set C2C3a = [<*C2,C3*>, and2];
set C3C1a = [<*C3,C1*>, and2];
set Aout = GFA0AdderOutput(C1,C2,C3);
set Cout = GFA0CarryOutput(C1,C2,C3);
S1 tolerates S2 by CIRCCOMB:47;
hence InnerVertices S
= (InnerVertices S1) \/ (InnerVertices S2) by CIRCCOMB:11
.= (InnerVertices S1) \/
({C1C2x} \/ {Aout} \/ {C1C2a,C2C3a,C3C1a} \/ {Cout}) by GFACIRC1:31
.= (InnerVertices S1) \/ ({C1C2x,Aout} \/ {C1C2a,C2C3a,C3C1a} \/ {Cout})
by ENUMSET1:1
.= (InnerVertices S1) \/ ({C1C2x,Aout} \/ ({C1C2a,C2C3a,C3C1a} \/ {Cout}))
by XBOOLE_1:4
.= (InnerVertices S1) \/ ({C1C2x,Aout} \/ {C1C2a,C2C3a,C3C1a,Cout})
by ENUMSET1:6
.= (InnerVertices S1) \/ {C1C2x,Aout} \/ {C1C2a,C2C3a,C3C1a,Cout}
by XBOOLE_1:4;
end;
theorem ThSTC0S1: :: expanded all InnerVertices by inputs and GFA0's
for x1,x2,x3,x4,x5,x6,x7 being set holds
InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) =
{[<*x1,x2*>,xor2], GFA0AdderOutput(x1,x2,x3)} \/
{[<*x1,x2*>,and2], [<*x2,x3*>,and2], [<*x3,x1*>,and2],
GFA0CarryOutput(x1,x2,x3)} \/
{[<*x5,x6*>,xor2], GFA0AdderOutput(x5,x6,x7)} \/
{[<*x5,x6*>,and2], [<*x6,x7*>,and2], [<*x7,x5*>,and2],
GFA0CarryOutput(x5,x6,x7)} \/
{[<*GFA0AdderOutput(x1,x2,x3),GFA0AdderOutput(x5,x6,x7)*>,xor2],
GFA0AdderOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4)} \/
{[<*GFA0AdderOutput(x1,x2,x3),GFA0AdderOutput(x5,x6,x7)*>,and2],
[<*GFA0AdderOutput(x5,x6,x7),x4*>,and2],
[<*x4,GFA0AdderOutput(x1,x2,x3)*>,and2],
GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4)} \/
{[<*GFA0CarryOutput(x1,x2,x3),GFA0CarryOutput(x5,x6,x7)*>,xor2],
GFA0AdderOutput(GFA0CarryOutput(x1,x2,x3),
GFA0CarryOutput(x5,x6,x7),
GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4))} \/
{[<*GFA0CarryOutput(x1,x2,x3),GFA0CarryOutput(x5,x6,x7)*>,and2],
[<*GFA0CarryOutput(x5,x6,x7),
GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4)*>,and2],
[<*GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4),
GFA0CarryOutput(x1,x2,x3)*>,and2],
GFA0CarryOutput(GFA0CarryOutput(x1,x2,x3),
GFA0CarryOutput(x5,x6,x7),
GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4))}
proof
let x1,x2,x3,x4,x5,x6,x7 be set;
set S = STC0Str(x1,x2,x3,x4,x5,x6,x7);
set S1 = STC0IStr(x1,x2,x3,x4,x5,x6,x7);
set x1x20 = [<*x1,x2*>, xor2];
set x1x2 = [<*x1,x2*>, and2];
set x2x3 = [<*x2,x3*>, and2];
set x3x1 = [<*x3,x1*>, and2];
set x5x60 = [<*x5,x6*>, xor2];
set x5x6 = [<*x5,x6*>, and2];
set x6x7 = [<*x6,x7*>, and2];
set x7x5 = [<*x7,x5*>, and2];
set A1 = GFA0AdderOutput(x1,x2,x3);
set A2 = GFA0AdderOutput(x5,x6,x7);
set A1A20 = [<*A1,A2*>,xor2];
set A1A2 = [<*A1,A2*>,and2];
set A2x4 = [<*A2,x4*>,and2];
set x4A1 = [<*x4,A1*>,and2];
set A3 = GFA0AdderOutput(A1,A2,x4);
set C1 = GFA0CarryOutput(x1,x2,x3);
set C2 = GFA0CarryOutput(x5,x6,x7);
set C3 = GFA0CarryOutput(A1,A2,x4);
set S2 = BitGFA0Str(C1,C2,C3);
set C1C2x = [<*C1,C2*>, xor2];
set C1C2a = [<*C1,C2*>, and2];
set C2C3a = [<*C2,C3*>, and2];
set C3C1a = [<*C3,C1*>, and2];
set Aout = GFA0AdderOutput(C1,C2,C3);
set Cout = GFA0CarryOutput(C1,C2,C3);
thus
InnerVertices S
= (InnerVertices S1) \/ {C1C2x,Aout} \/ {C1C2a,C2C3a,C3C1a,Cout}
by ThSTC0S1a
.= ({x1x20,A1} \/ {x1x2,x2x3,x3x1,C1} \/
{x5x60,A2} \/ {x5x6,x6x7,x7x5,C2} \/
{A1A20,A3} \/ {A1A2,A2x4,x4A1,C3}) \/
{C1C2x,Aout} \/ {C1C2a,C2C3a,C3C1a,Cout} by ThSTC0IS1;
end;
theorem :: ThSTC0S2:
for x1,x2,x3,x4,x5,x6,x7 being set holds
InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) is Relation;
::---------------------------------------
:: InputVertices of of STC_TYPE0.
LmSTC0S1:
for f1 being Function of 2-tuples_on BOOLEAN, BOOLEAN
for x,y,z being set for a,b being set holds
GFA0CarryOutput(x,y,z) <> [<*a,b*>,f1]
proof
let f1 be Function of 2-tuples_on BOOLEAN, BOOLEAN;
let x,y,z be set, a,b be set;
set xy = [<*x,y*>,and2], yz = [<*y,z*>,and2], zx = [<*z,x*>,and2];
set A1 = GFA0CarryOutput(x,y,z);
A1: A1`1 = <*xy,yz,zx*>;
len <*xy,yz,zx*> = 3 & len <*a,b*> = 2 by FINSEQ_1:44,45;
hence thesis by A1; :: [<*a,b*>,f1]`1 <> A1`1
end;
LmSTC0S2b:
for x1,x2,x3,x4,x5,x6,x7 being non pair set
for C1,C2,C3 being set
holds
InputVertices STC0IStr(x1,x2,x3,x4,x5,x6,x7)
misses InnerVertices BitGFA0Str(C1,C2,C3)
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
let C1,C2,C3 be set;
set S1 = STC0IStr(x1,x2,x3,x4,x5,x6,x7);
set S2 = BitGFA0Str(C1,C2,C3);
InputVertices S1 is without_pairs &
InnerVertices S2 is Relation by ThSTC0IS5;
hence thesis;
end;
theorem ThSTC0S4:
for x1,x2,x3,x4,x5,x6,x7 being non pair set holds
InputVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) = {x1,x2,x3,x4,x5,x6,x7}
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
set S = STC0Str(x1,x2,x3,x4,x5,x6,x7);
set S1 = STC0IStr(x1,x2,x3,x4,x5,x6,x7);
set S11 = STC0IIStr(x1,x2,x3,x5,x6,x7);
set x1x20 = [<*x1,x2*>, xor2];
set x1x2 = [<*x1,x2*>, and2];
set x2x3 = [<*x2,x3*>, and2];
set x3x1 = [<*x3,x1*>, and2];
set x5x60 = [<*x5,x6*>, xor2];
set x5x6 = [<*x5,x6*>, and2];
set x6x7 = [<*x6,x7*>, and2];
set x7x5 = [<*x7,x5*>, and2];
set A1 = GFA0AdderOutput(x1,x2,x3);
set A2 = GFA0AdderOutput(x5,x6,x7);
set A1A20 = [<*A1,A2*>,xor2];
set A1A2 = [<*A1,A2*>,and2];
set A2x4 = [<*A2,x4*>,and2];
set x4A1 = [<*x4,A1*>,and2];
set A3 = GFA0AdderOutput(A1,A2,x4);
set C1 = GFA0CarryOutput(x1,x2,x3);
set C2 = GFA0CarryOutput(x5,x6,x7);
set C3 = GFA0CarryOutput(A1,A2,x4);
set S2 = BitGFA0Str(C1,C2,C3);
set C1C2x = [<*C1,C2*>, xor2];
set C1C2a = [<*C1,C2*>, and2];
set C2C3a = [<*C2,C3*>, and2];
set C3C1a = [<*C3,C1*>, and2];
set Aout = GFA0AdderOutput(C1,C2,C3);
set Cout = GFA0CarryOutput(C1,C2,C3);
A2: InnerVertices S1
= {x1x20,A1} \/ {x1x2,x2x3,x3x1,C1} \/
{x5x60,A2} \/ {x5x6,x6x7,x7x5,C2} \/
{A1A20,A3} \/ {A1A2,A2x4,x4A1,C3} by ThSTC0IS1
.= {x1x20,A1} \/ ({x1x2,x2x3,x3x1} \/ {C1}) \/
{x5x60,A2} \/ {x5x6,x6x7,x7x5,C2} \/
{A1A20,A3} \/ {A1A2,A2x4,x4A1,C3} by ENUMSET1:6
.= ({x1x20,A1} \/ {x1x2,x2x3,x3x1}) \/ {C1} \/
{x5x60,A2} \/ {x5x6,x6x7,x7x5,C2} \/
{A1A20,A3} \/ {A1A2,A2x4,x4A1,C3} by XBOOLE_1:4
.= {C1} \/ ({x1x20,A1} \/ {x1x2,x2x3,x3x1}) \/
{x5x60,A2} \/ ({x5x6,x6x7,x7x5} \/ {C2}) \/
{A1A20,A3} \/ {A1A2,A2x4,x4A1,C3} by ENUMSET1:6
.= {C1} \/ {x1x20,A1,x1x2,x2x3,x3x1} \/
{x5x60,A2} \/ ({x5x6,x6x7,x7x5} \/ {C2}) \/
{A1A20,A3} \/ {A1A2,A2x4,x4A1,C3} by ENUMSET1:8
.= ({C1} \/ {x1x20,A1,x1x2,x2x3,x3x1} \/
{x5x60,A2} \/ {x5x6,x6x7,x7x5}) \/ {C2} \/
{A1A20,A3} \/ {A1A2,A2x4,x4A1,C3} by XBOOLE_1:4
.= {C2} \/ ({C1} \/ {x1x20,A1,x1x2,x2x3,x3x1} \/
{x5x60,A2} \/ {x5x6,x6x7,x7x5}) \/
{A1A20,A3} \/ ({A1A2,A2x4,x4A1} \/ {C3}) by ENUMSET1:6
.= {C2} \/ ({C1} \/ {x1x20,A1,x1x2,x2x3,x3x1} \/
({x5x60,A2} \/ {x5x6,x6x7,x7x5})) \/
{A1A20,A3} \/ ({A1A2,A2x4,x4A1} \/ {C3}) by XBOOLE_1:4
.= {C2} \/ ({C1} \/ {x1x20,A1,x1x2,x2x3,x3x1} \/
{x5x60,A2,x5x6,x6x7,x7x5}) \/
{A1A20,A3} \/ ({A1A2,A2x4,x4A1} \/ {C3}) by ENUMSET1:8
.= ({C2} \/ ({C1} \/ {x1x20,A1,x1x2,x2x3,x3x1} \/
{x5x60,A2,x5x6,x6x7,x7x5}) \/
{A1A20,A3} \/ {A1A2,A2x4,x4A1}) \/ {C3} by XBOOLE_1:4
.= {C3} \/ ({C2} \/ ({C1} \/ {x1x20,A1,x1x2,x2x3,x3x1} \/
{x5x60,A2,x5x6,x6x7,x7x5}) \/ ({A1A20,A3} \/ {A1A2,A2x4,x4A1}))
by XBOOLE_1:4
.= {C3} \/ ({C2} \/ ({C1} \/ {x1x20,A1,x1x2,x2x3,x3x1} \/
{x5x60,A2,x5x6,x6x7,x7x5}) \/ {A1A20,A3,A1A2,A2x4,x4A1})
by ENUMSET1:8
.= {C3} \/ ({C2} \/ ({C1} \/ {x1x20,A1,x1x2,x2x3,x3x1} \/
{x5x60,A2,x5x6,x6x7,x7x5} \/ {A1A20,A3,A1A2,A2x4,x4A1}))
by XBOOLE_1:4
.= ({C3} \/ {C2}) \/ ({C1} \/ {x1x20,A1,x1x2,x2x3,x3x1} \/
{x5x60,A2,x5x6,x6x7,x7x5} \/ {A1A20,A3,A1A2,A2x4,x4A1})
by XBOOLE_1:4
.= {C3,C2} \/ ({C1} \/ {x1x20,A1,x1x2,x2x3,x3x1} \/
{x5x60,A2,x5x6,x6x7,x7x5} \/ {A1A20,A3,A1A2,A2x4,x4A1})
by ENUMSET1:1
.= {C3,C2} \/ ({C1} \/ ({x1x20,A1,x1x2,x2x3,x3x1} \/
{x5x60,A2,x5x6,x6x7,x7x5}) \/ {A1A20,A3,A1A2,A2x4,x4A1})
by XBOOLE_1:4
.= {C3,C2} \/ ({C1} \/ (({x1x20,A1,x1x2,x2x3,x3x1} \/
{x5x60,A2,x5x6,x6x7,x7x5}) \/ {A1A20,A3,A1A2,A2x4,x4A1}))
by XBOOLE_1:4
.= ({C3,C2} \/ {C1}) \/ (({x1x20,A1,x1x2,x2x3,x3x1} \/
{x5x60,A2,x5x6,x6x7,x7x5}) \/ {A1A20,A3,A1A2,A2x4,x4A1})
by XBOOLE_1:4
.= {C1,C2,C3} \/ ({x1x20,A1,x1x2,x2x3,x3x1} \/
{x5x60,A2,x5x6,x6x7,x7x5} \/ {A1A20,A3,A1A2,A2x4,x4A1})
by ENUMSET1:2;
A3: C3 <> C1C2x & C1 <> C2C3a & C2 <> C3C1a & C3 <> C1C2a by LmSTC0S1;
InnerVertices S2 is Relation & InputVertices S1 is without_pairs
by ThSTC0IS5;
then
A5: InnerVertices S2 misses InputVertices S1;
S1 tolerates S2 by CIRCCOMB:47;
hence
InputVertices (S)
= (InputVertices S1) \/ (InputVertices S2 \ InnerVertices S1)
by A5,FACIRC_1:4
.= {x1,x2,x3,x4,x5,x6,x7} \/ (InputVertices S2 \ InnerVertices S1)
by ThSTC0IS4
.= {x1,x2,x3,x4,x5,x6,x7} \/ ({C1,C2,C3} \ InnerVertices S1)
by A3,GFACIRC1:33
.= {x1,x2,x3,x4,x5,x6,x7} \/ {} by A2,XBOOLE_1:46
.= {x1,x2,x3,x4,x5,x6,x7};
end;
theorem :: ThSTC0S5:
for x1,x2,x3,x4,x5,x6,x7 being non pair set holds
InputVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) is without_pairs
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
InputVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) = {x1,x2,x3,x4,x5,x6,x7}
by ThSTC0S4;
hence thesis;
end;
:: -----------------------------------
:: The Element of Carriers, InnerVertices and InputVertices of STC_TYPE0.
theorem ThSTC0S6:
for x1,x2,x3,x4,x5,x6,x7 being set holds
x1 in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
x2 in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
x3 in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
x4 in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
x5 in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
x6 in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
x7 in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*x1,x2*>,xor2] in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*x1,x2*>,and2] in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*x2,x3*>,and2] in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*x3,x1*>,and2] in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*x5,x6*>,xor2] in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*x5,x6*>,and2] in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*x6,x7*>,and2] in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*x7,x5*>,and2] in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
GFA0AdderOutput(x1,x2,x3) :: Lv2
in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
GFA0CarryOutput(x1,x2,x3)
in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
GFA0AdderOutput(x5,x6,x7)
in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
GFA0CarryOutput(x5,x6,x7)
in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*GFA0AdderOutput(x1,x2,x3),GFA0AdderOutput(x5,x6,x7)*>,xor2]
in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*GFA0AdderOutput(x1,x2,x3),GFA0AdderOutput(x5,x6,x7)*>,and2]
in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*GFA0AdderOutput(x5,x6,x7),x4*>,and2]
in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*x4,GFA0AdderOutput(x1,x2,x3)*>,and2]
in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
GFA0AdderOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4)
in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4)
in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*GFA0CarryOutput(x1,x2,x3),GFA0CarryOutput(x5,x6,x7)*>,xor2]
in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
GFA0AdderOutput(GFA0CarryOutput(x1,x2,x3),
GFA0CarryOutput(x5,x6,x7),
GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4))
in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*GFA0CarryOutput(x1,x2,x3),GFA0CarryOutput(x5,x6,x7)*>,and2]
in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*GFA0CarryOutput(x5,x6,x7),
GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4)*>,and2]
in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4),
GFA0CarryOutput(x1,x2,x3)*>,and2]
in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7) &
GFA0CarryOutput(GFA0CarryOutput(x1,x2,x3),
GFA0CarryOutput(x5,x6,x7),
GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4))
in the carrier of STC0Str(x1,x2,x3,x4,x5,x6,x7)
proof
let x1,x2,x3,x4,x5,x6,x7 be set;
set S = STC0Str(x1,x2,x3,x4,x5,x6,x7);
set S1 = STC0IStr(x1,x2,x3,x4,x5,x6,x7);
set x1x20 = [<*x1,x2*>, xor2];
set x1x2 = [<*x1,x2*>, and2];
set x2x3 = [<*x2,x3*>, and2];
set x3x1 = [<*x3,x1*>, and2];
set x5x60 = [<*x5,x6*>, xor2];
set x5x6 = [<*x5,x6*>, and2];
set x6x7 = [<*x6,x7*>, and2];
set x7x5 = [<*x7,x5*>, and2];
set A1 = GFA0AdderOutput(x1,x2,x3);
set A2 = GFA0AdderOutput(x5,x6,x7);
set A1A20 = [<*A1,A2*>,xor2];
set A1A2 = [<*A1,A2*>,and2];
set A2x4 = [<*A2,x4*>,and2];
set x4A1 = [<*x4,A1*>,and2];
set A3 = GFA0AdderOutput(A1,A2,x4);
set C1 = GFA0CarryOutput(x1,x2,x3);
set C2 = GFA0CarryOutput(x5,x6,x7);
set C3 = GFA0CarryOutput(A1,A2,x4);
set S2 = BitGFA0Str(C1,C2,C3);
set C1C2x = [<*C1,C2*>, xor2];
set C1C2a = [<*C1,C2*>, and2];
set C2C3a = [<*C2,C3*>, and2];
set C3C1a = [<*C3,C1*>, and2];
set Aout = GFA0AdderOutput(C1,C2,C3);
set Cout = GFA0CarryOutput(C1,C2,C3);
A1: x1 in the carrier of S1 & x2 in the carrier of S1 &
x3 in the carrier of S1 & x1x20 in the carrier of S1 &
A1 in the carrier of S1 &
x1x2 in the carrier of S1 & x2x3 in the carrier of S1 &
x3x1 in the carrier of S1 &
C1 in the carrier of S1 &
x5 in the carrier of S1 & x6 in the carrier of S1 &
x7 in the carrier of S1 & x5x60 in the carrier of S1 &
A2 in the carrier of S1 &
x5x6 in the carrier of S1 & x6x7 in the carrier of S1 &
x7x5 in the carrier of S1 &
C2 in the carrier of S1 &
x4 in the carrier of S1 & A1A20 in the carrier of S1 &
A3 in the carrier of S1 &
A1A2 in the carrier of S1 & A2x4 in the carrier of S1 &
x4A1 in the carrier of S1 &
C3 in the carrier of S1 by ThSTC0IS6;
C1C2x in the carrier of S2 & C1C2a in the carrier of S2 &
C2C3a in the carrier of S2 & C3C1a in the carrier of S2 &
Aout in the carrier of S2 & Cout in the carrier of S2 by GFACIRC1:36;
hence thesis by A1,FACIRC_1:20;
end;
LmSTC0S7a:
for x,X1,X2,X3,X4 being set
holds x in X1 \/ X2 \/ X3 \/ X4 iff x in X1 or x in X2 or x in X3 or x in X4
proof
let x,X1,X2,X3,X4 be set;
set W = X1 \/ X2 \/ X3 \/ X4;
x in W iff (x in X1 \/ X2 \/ X3) or x in X4 by XBOOLE_0:def 3;
hence thesis by LmSTC0IS7a;
end;
theorem ThSTC0S7:
for x1,x2,x3,x4,x5,x6,x7 being set holds
[<*x1,x2*>,xor2] in InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*x1,x2*>,and2] in InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*x2,x3*>,and2] in InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*x3,x1*>,and2] in InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*x5,x6*>,xor2] in InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*x5,x6*>,and2] in InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*x6,x7*>,and2] in InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*x7,x5*>,and2] in InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
GFA0AdderOutput(x1,x2,x3)
in InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
GFA0CarryOutput(x1,x2,x3)
in InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
GFA0AdderOutput(x5,x6,x7)
in InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
GFA0CarryOutput(x5,x6,x7)
in InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*GFA0AdderOutput(x1,x2,x3),GFA0AdderOutput(x5,x6,x7)*>,xor2]
in InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*GFA0AdderOutput(x1,x2,x3),GFA0AdderOutput(x5,x6,x7)*>,and2]
in InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*GFA0AdderOutput(x5,x6,x7),x4*>,and2]
in InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*x4,GFA0AdderOutput(x1,x2,x3)*>,and2]
in InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
GFA0AdderOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4)
in InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4)
in InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*GFA0CarryOutput(x1,x2,x3),GFA0CarryOutput(x5,x6,x7)*>,xor2]
in InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
GFA0AdderOutput(GFA0CarryOutput(x1,x2,x3),
GFA0CarryOutput(x5,x6,x7),
GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4))
in InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*GFA0CarryOutput(x1,x2,x3),GFA0CarryOutput(x5,x6,x7)*>,and2]
in InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*GFA0CarryOutput(x5,x6,x7),
GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4)*>,and2]
in InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
[<*GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4),
GFA0CarryOutput(x1,x2,x3)*>,and2]
in InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
GFA0CarryOutput(GFA0CarryOutput(x1,x2,x3),
GFA0CarryOutput(x5,x6,x7),
GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4))
in InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7)
proof
let x1,x2,x3,x4,x5,x6,x7 be set;
set S = STC0Str(x1,x2,x3,x4,x5,x6,x7);
set S1 = STC0IStr(x1,x2,x3,x4,x5,x6,x7);
set x1x20 = [<*x1,x2*>, xor2];
set x1x2 = [<*x1,x2*>, and2];
set x2x3 = [<*x2,x3*>, and2];
set x3x1 = [<*x3,x1*>, and2];
set x5x60 = [<*x5,x6*>, xor2];
set x5x6 = [<*x5,x6*>, and2];
set x6x7 = [<*x6,x7*>, and2];
set x7x5 = [<*x7,x5*>, and2];
set A1 = GFA0AdderOutput(x1,x2,x3);
set A2 = GFA0AdderOutput(x5,x6,x7);
set A1A20 = [<*A1,A2*>,xor2];
set A1A2 = [<*A1,A2*>,and2];
set A2x4 = [<*A2,x4*>,and2];
set x4A1 = [<*x4,A1*>,and2];
set A3 = GFA0AdderOutput(A1,A2,x4);
set C1 = GFA0CarryOutput(x1,x2,x3);
set C2 = GFA0CarryOutput(x5,x6,x7);
set C3 = GFA0CarryOutput(A1,A2,x4);
set S2 = BitGFA0Str(C1,C2,C3);
set C1C2x = [<*C1,C2*>, xor2];
set C1C2a = [<*C1,C2*>, and2];
set C2C3a = [<*C2,C3*>, and2];
set C3C1a = [<*C3,C1*>, and2];
set Aout = GFA0AdderOutput(C1,C2,C3);
set Cout = GFA0CarryOutput(C1,C2,C3);
set p1 = {x1x20,A1,x1x2,x2x3,x3x1,C1};
set p2 = {x5x60,A2,x5x6,x6x7,x7x5,C2};
set p3 = {A1A20,A3,A1A2,A2x4,x4A1,C3};
set p4 = {C1C2x,Aout,C1C2a,C2C3a,C3C1a,Cout};
A1: x1x20 in p1 & A1 in p1 &
x1x2 in p1 & x2x3 in p1 & x3x1 in p1 & C1 in p1 by ENUMSET1:def 4;
A2: x5x60 in p2 & A2 in p2 &
x5x6 in p2 & x6x7 in p2 & x7x5 in p2 & C2 in p2 by ENUMSET1:def 4;
A3: A1A20 in p3 & A3 in p3 &
A1A2 in p3 & A2x4 in p3 & x4A1 in p3 & C3 in p3 by ENUMSET1:def 4;
A4: C1C2x in p4 & C1C2a in p4 & C2C3a in p4 & C3C1a in p4 &
Aout in p4 & Cout in p4 by ENUMSET1:def 4;
InnerVertices S
= {x1x20,A1} \/ {x1x2,x2x3,x3x1,C1} \/
{x5x60,A2} \/ {x5x6,x6x7,x7x5,C2} \/
{A1A20,A3} \/ {A1A2,A2x4,x4A1,C3} \/
{C1C2x,Aout} \/ {C1C2a,C2C3a,C3C1a,Cout} by ThSTC0S1
.= p1 \/ {x5x60,A2} \/ {x5x6,x6x7,x7x5,C2} \/
{A1A20,A3} \/ {A1A2,A2x4,x4A1,C3} \/
{C1C2x,Aout} \/ {C1C2a,C2C3a,C3C1a,Cout} by ENUMSET1:12
.= p1 \/ ({x5x60,A2} \/ {x5x6,x6x7,x7x5,C2}) \/
{A1A20,A3} \/ {A1A2,A2x4,x4A1,C3} \/
{C1C2x,Aout} \/ {C1C2a,C2C3a,C3C1a,Cout} by XBOOLE_1:4
.= p1 \/ p2 \/ {A1A20,A3} \/ {A1A2,A2x4,x4A1,C3} \/
{C1C2x,Aout} \/ {C1C2a,C2C3a,C3C1a,Cout} by ENUMSET1:12
.= p1 \/ (p2 \/ {A1A20,A3}) \/ {A1A2,A2x4,x4A1,C3} \/
{C1C2x,Aout} \/ {C1C2a,C2C3a,C3C1a,Cout} by XBOOLE_1:4
.= p1 \/ ((p2 \/ {A1A20,A3}) \/ {A1A2,A2x4,x4A1,C3}) \/
{C1C2x,Aout} \/ {C1C2a,C2C3a,C3C1a,Cout} by XBOOLE_1:4
.= p1 \/ (p2 \/ ({A1A20,A3} \/ {A1A2,A2x4,x4A1,C3})) \/
{C1C2x,Aout} \/ {C1C2a,C2C3a,C3C1a,Cout} by XBOOLE_1:4
.= p1 \/ (p2 \/ p3) \/
{C1C2x,Aout} \/ {C1C2a,C2C3a,C3C1a,Cout} by ENUMSET1:12
.= p1 \/ ((p2 \/ p3) \/
{C1C2x,Aout}) \/ {C1C2a,C2C3a,C3C1a,Cout} by XBOOLE_1:4
.= p1 \/ (((p2 \/ p3) \/
{C1C2x,Aout}) \/ {C1C2a,C2C3a,C3C1a,Cout}) by XBOOLE_1:4
.= p1 \/ ((p2 \/ p3) \/
({C1C2x,Aout} \/ {C1C2a,C2C3a,C3C1a,Cout})) by XBOOLE_1:4
.= p1 \/ ((p2 \/ p3) \/ p4) by ENUMSET1:12
.= (p1 \/ (p2 \/ p3)) \/ p4 by XBOOLE_1:4
.= p1 \/ p2 \/ p3 \/ p4 by XBOOLE_1:4;
hence thesis by A1,A2,A3,A4,LmSTC0S7a;
end;
theorem ThSTC0S9:
for x1,x2,x3,x4,x5,x6,x7 being non pair set holds
x1 in InputVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
x2 in InputVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
x3 in InputVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
x4 in InputVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
x5 in InputVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
x6 in InputVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) &
x7 in InputVertices STC0Str(x1,x2,x3,x4,x5,x6,x7)
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
set S = STC0Str(x1,x2,x3,x4,x5,x6,x7);
InputVertices S = {x1,x2,x3,x4,x5,x6,x7} by ThSTC0S4;
hence thesis by ENUMSET1:def 5;
end;
::-------------------------------------------
:: 3-3. Output Definitions of the Combined Circuit
::-------------------------------------------
:: Def. External Signal Outputs of of STC_TYPE0.
definition
let x1,x2,x3,x4,x5,x6,x7 be set;
func STC0OutputS0(x1,x2,x3,x4,x5,x6,x7) ->
Element of InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) equals
GFA0AdderOutput(GFA0AdderOutput(x1,x2,x3),GFA0AdderOutput(x5,x6,x7),x4);
coherence by ThSTC0S7;
func STC0OutputS1(x1,x2,x3,x4,x5,x6,x7) ->
Element of InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) equals
GFA0AdderOutput(GFA0CarryOutput(x1,x2,x3),
GFA0CarryOutput(x5,x6,x7),
GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4));
coherence by ThSTC0S7;
func STC0OutputS2(x1,x2,x3,x4,x5,x6,x7) ->
Element of InnerVertices STC0Str(x1,x2,x3,x4,x5,x6,x7) equals
GFA0CarryOutput(GFA0CarryOutput(x1,x2,x3),
GFA0CarryOutput(x5,x6,x7),
GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4));
coherence by ThSTC0S7;
end;
::----------------------------------------------------
:: 2-4. Outputs of the Combined Circuit and its Stability
::---------------------------------------------------
:: --------------------------
:: for Output S0
LmSTC0S15s0: :: Lm0 (step-4, Output C1 and C2 in STC0_Inter.)
for x1,x2,x3,x4,x5,x6,x7 being non pair set
for s being State of STC0ICirc(x1,x2,x3,x4,x5,x6,x7)
for a1,a2,a3,a4,a5,a6,a7 being Element of BOOLEAN st
a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7
holds Following(s,4).STC0ICarryOutputC1(x1,x2,x3,x4,x5,x6,x7)
= (a1 '&' a2) 'or' (a2 '&' a3) 'or' (a3 '&' a1) &
Following(s,4).STC0ICarryOutputC2(x1,x2,x3,x4,x5,x6,x7)
= (a5 '&' a6) 'or' (a6 '&' a7) 'or' (a7 '&' a5)
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
set C = STC0ICirc(x1,x2,x3,x4,x5,x6,x7);
set S1 = STC0IIStr(x1,x2,x3,x5,x6,x7);
set C1 = STC0IICirc(x1,x2,x3,x5,x6,x7);
set A1out = GFA0AdderOutput(x1,x2,x3);
set A2out = GFA0AdderOutput(x5,x6,x7);
set S2 = BitGFA0Str(A1out,A2out,x4);
set C2 = BitGFA0Circ(A1out,A2out,x4);
set C1out = STC0IICarryOutputC1(x1,x2,x3,x5,x6,x7);
set C2out = STC0IICarryOutputC2(x1,x2,x3,x5,x6,x7);
set n1=2, n2=4;
let s be State of C;
let a1,a2,a3,a4,a5,a6,a7 be Element of BOOLEAN such that
A2: a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7;
reconsider t = s as State of C1+*C2;
reconsider s1 = s|the carrier of S1 as State of C1 by FACIRC_1:26;
A3: dom s1 = the carrier of S1 by CIRCUIT1:3;
A4: Following(s1,n2) = Following(s1,n1) by ThSTC0IIS12,CIRCCMB2:4;
C1out in the carrier of S1 & C2out in the carrier of S1 &
InputVertices S1 misses InnerVertices S2 by LmSTC0IS2b;
then
A5: Following(t,n2).C1out = Following(s1,n1).C1out &
Following(t,n2).C2out = Following(s1,n1).C2out by A4,FACIRC_1:32;
a1 = s1.x1 & a2 = s1.x2 & a3 = s1.x3 &
a5 = s1.x5 & a6 = s1.x6 & a7 = s1.x7 by ThSTC0IIS6,A2,A3,FUNCT_1:47;
hence thesis by A5,ThSTC0IIS10;
end;
LmSTC0S15s4a: :: Lm4a (step-4, C1 and C2 common)
for x1,x2,x3,x4,x5,x6,x7 being non pair set
for s being State of STC0Circ(x1,x2,x3,x4,x5,x6,x7)
for a1,a2,a3,a4,a5,a6,a7 being Element of BOOLEAN st
a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7
holds Following(s,4).STC0ICarryOutputC1(x1,x2,x3,x4,x5,x6,x7)
= (a1 '&' a2) 'or' (a2 '&' a3) 'or' (a3 '&' a1) &
Following(s,4).STC0ICarryOutputC2(x1,x2,x3,x4,x5,x6,x7)
= (a5 '&' a6) 'or' (a6 '&' a7) 'or' (a7 '&' a5) &
Following(s,4).x1 = a1 & Following(s,4).x2 = a2 &
Following(s,4).x3 = a3 & Following(s,4).x4 = a4 &
Following(s,4).x5 = a5 & Following(s,4).x6 = a6 &
Following(s,4).x7 = a7
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
set S = STC0Str(x1,x2,x3,x4,x5,x6,x7);
set C = STC0Circ(x1,x2,x3,x4,x5,x6,x7);
set S1 = STC0IStr(x1,x2,x3,x4,x5,x6,x7);
set C1 = STC0ICirc(x1,x2,x3,x4,x5,x6,x7);
set A1out = GFA0AdderOutput(x1,x2,x3);
set A2out = GFA0AdderOutput(x5,x6,x7);
set C1out = GFA0CarryOutput(x1,x2,x3);
set C2out = GFA0CarryOutput(x5,x6,x7);
set C3out = GFA0CarryOutput(A1out,A2out,x4);
set S2 = BitGFA0Str(C1out,C2out,C3out);
set C2 = BitGFA0Circ(C1out,C2out,C3out);
let s be State of C;
let a1,a2,a3,a4,a5,a6,a7 be Element of BOOLEAN such that
A2: a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7;
A3: x1 in InputVertices S & x2 in InputVertices S & x3 in InputVertices S &
x4 in InputVertices S & x5 in InputVertices S & x6 in InputVertices S &
x7 in InputVertices S
by ThSTC0S9;
reconsider t = s as State of C1+*C2;
reconsider s1 = s|the carrier of S1 as State of C1 by FACIRC_1:26;
A4: dom s1 = the carrier of S1 by CIRCUIT1:3;
C1out in the carrier of S1 & C2out in the carrier of S1 &
InputVertices S1 misses InnerVertices S2 by ThSTC0IS6,LmSTC0S2b;
then
A5: Following(t,4).C1out = Following(s1,4).C1out &
Following(t,4).C2out = Following(s1,4).C2out by FACIRC_1:32;
a1 = s1.x1 & a2 = s1.x2 & a3 = s1.x3 & a4 = s1.x4 &
a5 = s1.x5 & a6 = s1.x6 & a7 = s1.x7 by ThSTC0IS6,A2,A4,FUNCT_1:47;
hence thesis by A2,A3,CIRCCMB3:1,A5,LmSTC0S15s0;
end;
LmSTC0S15s4b: :: Lm4b (step-4, C3 and A3 common)
for x1,x2,x3,x4,x5,x6,x7 being non pair set
for s being State of STC0Circ(x1,x2,x3,x4,x5,x6,x7)
for a1,a2,a3,a4,a5,a6,a7 being Element of BOOLEAN st
a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7
holds Following(s,4).STC0ICarryOutputC3(x1,x2,x3,x4,x5,x6,x7)
= ((a1 'xor' a2 'xor' a3) '&' (a5 'xor' a6 'xor' a7)) 'or'
((a5 'xor' a6 'xor' a7) '&' a4) 'or'
(a4 '&' (a1 'xor' a2 'xor' a3)) &
Following(s,4).STC0IAdderOutputA3(x1,x2,x3,x4,x5,x6,x7)
= a1 'xor' a2 'xor' a3 'xor' a4 'xor' a5 'xor' a6 'xor' a7 &
Following(s,4).x1 = a1 & Following(s,4).x2 = a2 &
Following(s,4).x3 = a3 & Following(s,4).x4 = a4 &
Following(s,4).x5 = a5 & Following(s,4).x6 = a6 &
Following(s,4).x7 = a7
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
set S = STC0Str(x1,x2,x3,x4,x5,x6,x7);
set C = STC0Circ(x1,x2,x3,x4,x5,x6,x7);
set S1 = STC0IStr(x1,x2,x3,x4,x5,x6,x7);
set C1 = STC0ICirc(x1,x2,x3,x4,x5,x6,x7);
set A1out = GFA0AdderOutput(x1,x2,x3);
set A2out = GFA0AdderOutput(x5,x6,x7);
set A3out = GFA0AdderOutput(A1out,A2out,x4);
set C1out = GFA0CarryOutput(x1,x2,x3);
set C2out = GFA0CarryOutput(x5,x6,x7);
set C3out = GFA0CarryOutput(A1out,A2out,x4);
set S2 = BitGFA0Str(C1out,C2out,C3out);
set C2 = BitGFA0Circ(C1out,C2out,C3out);
let s be State of C;
let a1,a2,a3,a4,a5,a6,a7 be Element of BOOLEAN such that
A2: a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7;
A3: x1 in InputVertices S & x2 in InputVertices S & x3 in InputVertices S &
x4 in InputVertices S & x5 in InputVertices S & x6 in InputVertices S &
x7 in InputVertices S
by ThSTC0S9;
reconsider t = s as State of C1+*C2;
reconsider s1 = s|the carrier of S1 as State of C1 by FACIRC_1:26;
A4: dom s1 = the carrier of S1 by CIRCUIT1:3;
C3out in the carrier of S1 & A3out in the carrier of S1 &
InputVertices S1 misses InnerVertices S2 by ThSTC0IS6,LmSTC0S2b;
then
A5: Following(t,4).C3out = Following(s1,4).C3out &
Following(t,4).A3out = Following(s1,4).A3out by FACIRC_1:32;
a1 = s1.x1 & a2 = s1.x2 & a3 = s1.x3 & a4 = s1.x4 &
a5 = s1.x5 & a6 = s1.x6 & a7 = s1.x7 by ThSTC0IS6,A2,A4,FUNCT_1:47;
hence thesis by A2,A3,CIRCCMB3:1,A5,LmSTC0IS15C3,LmSTC0IS15A3;
end;
LmSTC0S15S0: :: (step-4, Output S0)
for x1,x2,x3,x4,x5,x6,x7 being non pair set
for s being State of STC0Circ(x1,x2,x3,x4,x5,x6,x7)
for a1,a2,a3,a4,a5,a6,a7 being Element of BOOLEAN st
a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7
holds Following(s,4).STC0OutputS0(x1,x2,x3,x4,x5,x6,x7)
= a1 'xor' a2 'xor' a3 'xor' a4 'xor' a5 'xor' a6 'xor' a7
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
set A1out = GFA0AdderOutput(x1,x2,x3);
set A2out = GFA0AdderOutput(x5,x6,x7);
set A3out = GFA0AdderOutput(A1out,A2out,x4);
A3out = STC0IAdderOutputA3(x1,x2,x3,x4,x5,x6,x7) &
A3out = STC0OutputS0(x1,x2,x3,x4,x5,x6,x7);
hence thesis by LmSTC0S15s4b;
end;
:: --------------------------
:: for Output S1
LmSTC0S15S1s4: :: Lm4 (step-5)
for x1,x2,x3,x4,x5,x6,x7 being non pair set
for s being State of STC0Circ(x1,x2,x3,x4,x5,x6,x7)
for aC1,aC2 being Element of BOOLEAN st
aC1 = s.GFA0CarryOutput(x1,x2,x3) & aC2 = s.GFA0CarryOutput(x5,x6,x7)
holds (Following s).[<*GFA0CarryOutput(x1,x2,x3),
GFA0CarryOutput(x5,x6,x7)*>,xor2]
= aC1 'xor' aC2
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
set S = STC0Str(x1,x2,x3,x4,x5,x6,x7);
set C = STC0Circ(x1,x2,x3,x4,x5,x6,x7);
set C1out = GFA0CarryOutput(x1,x2,x3);
set C2out = GFA0CarryOutput(x5,x6,x7);
set C1C2x = [<*C1out,C2out*>,xor2];
let s be State of C;
let aC1, aC2 be Element of BOOLEAN such that
A1: aC1 = s.C1out & aC2 = s.C2out;
A2: dom s = the carrier of S by CIRCUIT1:3;
A3: C1out in the carrier of S & C2out in the carrier of S by ThSTC0S6;
InnerVertices S = the carrier' of S by FACIRC_1:37;
hence
(Following s).C1C2x
= xor2.(s*<*C1out,C2out*>) by ThSTC0S7,FACIRC_1:35
.= xor2.<*aC1, aC2*> by A1,A2,A3,FINSEQ_2:125
.= aC1 'xor' aC2 by FACIRC_1:def 4;
end;
LmSTC0S15S1s6a: :: Lm6a (step-5, C1C2x)
for x1,x2,x3,x4,x5,x6,x7 being non pair set
for s being State of STC0Circ(x1,x2,x3,x4,x5,x6,x7)
for a1,a2,a3,a4,a5,a6,a7 being Element of BOOLEAN st
a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7
holds Following(s,5).[<*GFA0CarryOutput(x1,x2,x3),
GFA0CarryOutput(x5,x6,x7)*>,xor2]
= ((a1'&'a2)'or'(a2'&'a3)'or'(a3'&'a1))
'xor'
((a5'&'a6)'or'(a6'&'a7)'or'(a7'&'a5))
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
set C = STC0Circ(x1,x2,x3,x4,x5,x6,x7);
set C1out = GFA0CarryOutput(x1,x2,x3);
set C2out = GFA0CarryOutput(x5,x6,x7);
set C1C2x = [<*C1out,C2out*>,xor2];
let s be State of C;
let a1,a2,a3,a4,a5,a6,a7 be Element of BOOLEAN such that
A2: a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7;
A5: Following(s,4).C1out = (a1'&'a2)'or'(a2'&'a3)'or'(a3'&'a1) &
Following(s,4).C2out = (a5'&'a6)'or'(a6'&'a7)'or'(a7'&'a5)
by A2,LmSTC0S15s4a;
Following(s,4+1) = Following Following(s,4) by FACIRC_1:12;
hence thesis by A5,LmSTC0S15S1s4;
end;
LmSTC0S15S1s6b: :: Lm6b (step-5, C3out)
for x1,x2,x3,x4,x5,x6,x7 being non pair set
for s being State of STC0Circ(x1,x2,x3,x4,x5,x6,x7)
for a1,a2,a3,a4,a5,a6,a7 being Element of BOOLEAN st
a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7
holds Following(s,5).GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4)
= ((a1'xor'a2'xor'a3)'&'(a5'xor'a6'xor'a7))'or'
((a5'xor'a6'xor'a7)'&'a4)'or'(a4'&'(a1'xor'a2'xor'a3))
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
set S = STC0Str(x1,x2,x3,x4,x5,x6,x7);
set C = STC0Circ(x1,x2,x3,x4,x5,x6,x7);
set S1 = STC0IStr(x1,x2,x3,x4,x5,x6,x7);
set C1 = STC0ICirc(x1,x2,x3,x4,x5,x6,x7);
set A1out = GFA0AdderOutput(x1,x2,x3);
set A2out = GFA0AdderOutput(x5,x6,x7);
set C1out = GFA0CarryOutput(x1,x2,x3);
set C2out = GFA0CarryOutput(x5,x6,x7);
set C3out = GFA0CarryOutput(A1out,A2out,x4);
set S2 = BitGFA0Str(C1out,C2out,C3out);
set C2 = BitGFA0Circ(C1out,C2out,C3out);
set n1=4, n2=5;
let s be State of C;
let a1,a2,a3,a4,a5,a6,a7 be Element of BOOLEAN such that
A2: a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7;
reconsider t = s as State of C1+*C2;
reconsider s1 = s|the carrier of S1 as State of C1 by FACIRC_1:26;
A3: dom s1 = the carrier of S1 by CIRCUIT1:3;
A4: Following(s1,n2) = Following(s1,n1) by ThSTC0IS18,CIRCCMB2:4;
C3out in the carrier of S1 &
InputVertices S1 misses InnerVertices S2 by ThSTC0IS6,LmSTC0S2b;
then
A5: Following(t,n2).C3out = Following(s1,n1).C3out by A4,FACIRC_1:32;
a1 = s1.x1 & a2 = s1.x2 & a3 = s1.x3 & a4 = s1.x4 &
a5 = s1.x5 & a6 = s1.x6 & a7 = s1.x7 by ThSTC0IS6,A2,A3,FUNCT_1:47;
hence thesis by A5,LmSTC0IS15C3;
end;
LmSTC0S15S1s8: :: Lm8 (step-6)
for x1,x2,x3,x4,x5,x6,x7 being non pair set
for s being State of STC0Circ(x1,x2,x3,x4,x5,x6,x7)
for aC1C2x,aC3 being Element of BOOLEAN st
aC1C2x = s.[<*GFA0CarryOutput(x1,x2,x3),
GFA0CarryOutput(x5,x6,x7)*>,xor2] &
aC3 = s.GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4)
holds (Following s).GFA0AdderOutput(GFA0CarryOutput(x1,x2,x3),
GFA0CarryOutput(x5,x6,x7),
GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4))
= aC1C2x 'xor' aC3
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
set S = STC0Str(x1,x2,x3,x4,x5,x6,x7);
set C = STC0Circ(x1,x2,x3,x4,x5,x6,x7);
set A1out = GFA0AdderOutput(x1,x2,x3);
set A2out = GFA0AdderOutput(x5,x6,x7);
set C1out = GFA0CarryOutput(x1,x2,x3);
set C2out = GFA0CarryOutput(x5,x6,x7);
set C3out = GFA0CarryOutput(A1out,A2out,x4);
set C1C2x = [<*C1out,C2out*>,xor2];
let s be State of C;
let aC1C2x, aC3 be Element of BOOLEAN such that
A1: aC1C2x = s.C1C2x & aC3 = s.C3out;
A2: dom s = the carrier of S by CIRCUIT1:3;
A3: C1C2x in the carrier of S & C3out in the carrier of S by ThSTC0S6;
InnerVertices S = the carrier' of S by FACIRC_1:37;
hence
(Following s).GFA0AdderOutput(C1out,C2out,C3out)
= xor2.(s*<*C1C2x,C3out*>) by ThSTC0S7,FACIRC_1:35
.= xor2.<*aC1C2x, aC3*> by A1,A2,A3,FINSEQ_2:125
.= aC1C2x 'xor' aC3 by FACIRC_1:def 4;
end;
LmSTC0S15S1: :: Lm10 (step-6, Output S1)
for x1,x2,x3,x4,x5,x6,x7 being non pair set
for s being State of STC0Circ(x1,x2,x3,x4,x5,x6,x7)
for a1,a2,a3,a4,a5,a6,a7 being Element of BOOLEAN st
a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7
holds Following(s,6).STC0OutputS1(x1,x2,x3,x4,x5,x6,x7)
= ((a1'&'a2)'or'(a2'&'a3)'or'(a3'&'a1))
'xor'
((a5'&'a6)'or'(a6'&'a7)'or'(a7'&'a5))
'xor'
(((a1'xor'a2'xor'a3)'&'(a5'xor'a6'xor'a7))'or'
((a5'xor'a6'xor'a7)'&'a4)'or'(a4'&'(a1'xor'a2'xor'a3))) &
Following(s,6).x1 = a1 & Following(s,6).x2 = a2 &
Following(s,6).x3 = a3 & Following(s,6).x4 = a4 &
Following(s,6).x5 = a5 & Following(s,6).x6 = a6 &
Following(s,6).x7 = a7
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
set S = STC0Str(x1,x2,x3,x4,x5,x6,x7);
set C = STC0Circ(x1,x2,x3,x4,x5,x6,x7);
set A1out = GFA0AdderOutput(x1,x2,x3);
set A2out = GFA0AdderOutput(x5,x6,x7);
set C1out = GFA0CarryOutput(x1,x2,x3);
set C2out = GFA0CarryOutput(x5,x6,x7);
set C3out = GFA0CarryOutput(A1out,A2out,x4);
set C1C2x = [<*C1out,C2out*>,xor2];
set S1out = STC0OutputS1(x1,x2,x3,x4,x5,x6,x7);
let s be State of C;
let a1,a2,a3,a4,a5,a6,a7 be Element of BOOLEAN such that
A2: a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7;
A3: x1 in InputVertices S & x2 in InputVertices S & x3 in InputVertices S &
x4 in InputVertices S & x5 in InputVertices S & x6 in InputVertices S &
x7 in InputVertices S
by ThSTC0S9;
A5: Following(s,5).C1C2x
= ((a1'&'a2)'or'(a2'&'a3)'or'(a3'&'a1))
'xor'
((a5'&'a6)'or'(a6'&'a7)'or'(a7'&'a5)) &
Following(s,5).C3out
= ((a1'xor'a2'xor'a3)'&'(a5'xor'a6'xor'a7))'or'
((a5'xor'a6'xor'a7)'&'a4)'or'(a4'&'(a1'xor'a2'xor'a3))
by A2,LmSTC0S15S1s6a,LmSTC0S15S1s6b;
Following(s,5+1) = Following Following(s,5) by FACIRC_1:12;
hence thesis by A2,A3,CIRCCMB3:1,A5,LmSTC0S15S1s8;
end;
:: --------------------------
:: for Output S2
LmSTC0S15S2s4: :: Lm4 (step-5)
for x1,x2,x3,x4,x5,x6,x7 being non pair set
for s being State of STC0Circ(x1,x2,x3,x4,x5,x6,x7)
for aC1,aC2,aC3 being Element of BOOLEAN st
aC1 = s.GFA0CarryOutput(x1,x2,x3) & aC2 = s.GFA0CarryOutput(x5,x6,x7) &
aC3 = s.GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4)
holds (Following s).[<*GFA0CarryOutput(x1,x2,x3),
GFA0CarryOutput(x5,x6,x7)*>,and2]
= aC1 '&' aC2 &
(Following s).[<*GFA0CarryOutput(x5,x6,x7),
GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4)*>,and2]
= aC2 '&' aC3 &
(Following s).[<*GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4),
GFA0CarryOutput(x1,x2,x3)*>,and2]
= aC3 '&' aC1
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
set S = STC0Str(x1,x2,x3,x4,x5,x6,x7);
set C = STC0Circ(x1,x2,x3,x4,x5,x6,x7);
set A1out = GFA0AdderOutput(x1,x2,x3);
set A2out = GFA0AdderOutput(x5,x6,x7);
set C1out = GFA0CarryOutput(x1,x2,x3);
set C2out = GFA0CarryOutput(x5,x6,x7);
set C3out = GFA0CarryOutput(A1out,A2out,x4);
set C1C2a = [<*C1out,C2out*>, and2];
set C2C3a = [<*C2out,C3out*>, and2];
set C3C1a = [<*C3out,C1out*>, and2];
let s be State of C;
let aC1, aC2, aC3 be Element of BOOLEAN such that
A1: aC1 = s.C1out & aC2 = s.C2out & aC3 = s.C3out;
A2: dom s = the carrier of S by CIRCUIT1:3;
A3: C1out in the carrier of S & C2out in the carrier of S &
C3out in the carrier of S by ThSTC0S6;
A4: InnerVertices S = the carrier' of S by FACIRC_1:37;
hence
(Following s).C1C2a
= and2.(s*<*C1out,C2out*>) by ThSTC0S7,FACIRC_1:35
.= and2.<*aC1, aC2*> by A1,A2,A3,FINSEQ_2:125
.= aC1 '&' aC2 by FACIRC_1:def 6;
A6: (Following s).C2C3a
= and2.(s*<*C2out,C3out*>) by A4,ThSTC0S7,FACIRC_1:35
.= and2.<*aC2, aC3*> by A1,A2,A3,FINSEQ_2:125
.= aC2 '&' aC3 by FACIRC_1:def 6;
(Following s).C3C1a
= and2.(s*<*C3out,C1out*>) by A4,ThSTC0S7,FACIRC_1:35
.= and2.<*aC3, aC1*> by A1,A2,A3,FINSEQ_2:125
.= aC3 '&' aC1 by FACIRC_1:def 6;
hence thesis by A6;
end;
LmSTC0S15S2s6: :: Lm6 (step-5, C1C2a, C2C3a and C3C1a)
for x1,x2,x3,x4,x5,x6,x7 being non pair set
for s being State of STC0Circ(x1,x2,x3,x4,x5,x6,x7)
for a1,a2,a3,a4,a5,a6,a7 being Element of BOOLEAN st
a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7
holds
Following(s,5).[<*GFA0CarryOutput(x1,x2,x3),
GFA0CarryOutput(x5,x6,x7)*>,and2]
= ((a1'&'a2)'or'(a2'&'a3)'or'(a3'&'a1))'&'
((a5'&'a6)'or'(a6'&'a7)'or'(a7'&'a5)) &
Following(s,5).[<*GFA0CarryOutput(x5,x6,x7),
GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4)*>,and2]
= ((a5'&'a6)'or'(a6'&'a7)'or'(a7'&'a5))'&'
(((a1'xor'a2'xor'a3)'&'(a5'xor'a6'xor'a7))'or'
((a5'xor'a6'xor'a7)'&'a4)'or'(a4'&'(a1'xor'a2'xor'a3))) &
Following(s,5).[<*GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4),
GFA0CarryOutput(x1,x2,x3)*>,and2]
= (((a1'xor'a2'xor'a3)'&'(a5'xor'a6'xor'a7))'or'
((a5'xor'a6'xor'a7)'&'a4)'or'(a4'&'(a1'xor'a2'xor'a3)))'&'
((a1'&'a2)'or'(a2'&'a3)'or'(a3'&'a1))
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
set S = STC0Str(x1,x2,x3,x4,x5,x6,x7);
set C = STC0Circ(x1,x2,x3,x4,x5,x6,x7);
set A1out = GFA0AdderOutput(x1,x2,x3);
set A2out = GFA0AdderOutput(x5,x6,x7);
set C1out = GFA0CarryOutput(x1,x2,x3);
set C2out = GFA0CarryOutput(x5,x6,x7);
set C3out = GFA0CarryOutput(A1out,A2out,x4);
set C1C2a = [<*C1out,C2out*>, and2];
set C2C3a = [<*C2out,C3out*>, and2];
set C3C1a = [<*C3out,C1out*>, and2];
let s be State of C;
let a1,a2,a3,a4,a5,a6,a7 be Element of BOOLEAN such that
A2: a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7;
A5: Following(s,4).C1out = (a1'&'a2)'or'(a2'&'a3)'or'(a3'&'a1) &
Following(s,4).C2out = (a5'&'a6)'or'(a6'&'a7)'or'(a7'&'a5) &
Following(s,4).C3out
= ((a1'xor'a2'xor'a3)'&'(a5'xor'a6'xor'a7))'or'
((a5'xor'a6'xor'a7)'&'a4)'or'(a4'&'(a1'xor'a2'xor'a3))
by A2,LmSTC0S15s4a,LmSTC0S15s4b;
Following(s,4+1) = Following Following(s,4) by FACIRC_1:12;
hence thesis by A5,LmSTC0S15S2s4;
end;
LmSTC0S15S2s8: :: Lm8 (step-6)
for x1,x2,x3,x4,x5,x6,x7 being non pair set
for s being State of STC0Circ(x1,x2,x3,x4,x5,x6,x7)
for aC1C2a,aC2C3a,aC3C1a being Element of BOOLEAN st
aC1C2a = s.[<*GFA0CarryOutput(x1,x2,x3),
GFA0CarryOutput(x5,x6,x7)*>,and2] &
aC2C3a = s.[<*GFA0CarryOutput(x5,x6,x7),
GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4)*>,and2] &
aC3C1a = s.[<*GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4),
GFA0CarryOutput(x1,x2,x3)*>,and2]
holds (Following s).GFA0CarryOutput(GFA0CarryOutput(x1,x2,x3),
GFA0CarryOutput(x5,x6,x7),
GFA0CarryOutput(GFA0AdderOutput(x1,x2,x3),
GFA0AdderOutput(x5,x6,x7),x4))
= aC1C2a 'or' aC2C3a 'or' aC3C1a
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
set S = STC0Str(x1,x2,x3,x4,x5,x6,x7);
set C = STC0Circ(x1,x2,x3,x4,x5,x6,x7);
set A1out = GFA0AdderOutput(x1,x2,x3);
set A2out = GFA0AdderOutput(x5,x6,x7);
set C1out = GFA0CarryOutput(x1,x2,x3);
set C2out = GFA0CarryOutput(x5,x6,x7);
set C3out = GFA0CarryOutput(A1out,A2out,x4);
set C1C2a = [<*C1out,C2out*>, and2];
set C2C3a = [<*C2out,C3out*>, and2];
set C3C1a = [<*C3out,C1out*>, and2];
let s be State of C;
let aC1C2a, aC2C3a, aC3C1a be Element of BOOLEAN such that
A1: aC1C2a = s.C1C2a & aC2C3a = s.C2C3a & aC3C1a = s.C3C1a;
A2: dom s = the carrier of S by CIRCUIT1:3;
A3: C1C2a in the carrier of S & C2C3a in the carrier of S &
C3C1a in the carrier of S by ThSTC0S6;
InnerVertices S = the carrier' of S by FACIRC_1:37;
hence
(Following s).GFA0CarryOutput(C1out,C2out,C3out)
= or3.(s*<*C1C2a,C2C3a,C3C1a*>) by ThSTC0S7,FACIRC_1:35
.= or3.<*aC1C2a, aC2C3a, aC3C1a*> by A1,A2,A3,FINSEQ_2:126
.= aC1C2a 'or' aC2C3a 'or' aC3C1a by FACIRC_1:def 7;
end;
LmSTC0S15S2: :: Lm10 (step-6, Output S2)
for x1,x2,x3,x4,x5,x6,x7 being non pair set
for s being State of STC0Circ(x1,x2,x3,x4,x5,x6,x7)
for a1,a2,a3,a4,a5,a6,a7 being Element of BOOLEAN st
a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7
holds Following(s,6).STC0OutputS2(x1,x2,x3,x4,x5,x6,x7)
= (((a1'&'a2)'or'(a2'&'a3)'or'(a3'&'a1))'&'
((a5'&'a6)'or'(a6'&'a7)'or'(a7'&'a5)))
'or'
(((a5'&'a6)'or'(a6'&'a7)'or'(a7'&'a5))'&'
(((a1'xor'a2'xor'a3)'&'(a5'xor'a6'xor'a7))'or'
((a5'xor'a6'xor'a7)'&'a4)'or'(a4'&'(a1'xor'a2'xor'a3))))
'or'
((((a1'xor'a2'xor'a3)'&'(a5'xor'a6'xor'a7))'or'
((a5'xor'a6'xor'a7)'&'a4)'or'(a4'&'(a1'xor'a2'xor'a3)))'&'
((a1'&'a2)'or'(a2'&'a3)'or'(a3'&'a1))) &
Following(s,6).x1 = a1 & Following(s,6).x2 = a2 &
Following(s,6).x3 = a3 & Following(s,6).x4 = a4 &
Following(s,6).x5 = a5 & Following(s,6).x6 = a6 &
Following(s,6).x7 = a7
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
set S = STC0Str(x1,x2,x3,x4,x5,x6,x7);
set C = STC0Circ(x1,x2,x3,x4,x5,x6,x7);
set A1out = GFA0AdderOutput(x1,x2,x3);
set A2out = GFA0AdderOutput(x5,x6,x7);
set C1out = GFA0CarryOutput(x1,x2,x3);
set C2out = GFA0CarryOutput(x5,x6,x7);
set C3out = GFA0CarryOutput(A1out,A2out,x4);
set C1C2a = [<*C1out,C2out*>, and2];
set C2C3a = [<*C2out,C3out*>, and2];
set C3C1a = [<*C3out,C1out*>, and2];
set S2out = STC0OutputS2(x1,x2,x3,x4,x5,x6,x7);
let s be State of C;
let a1,a2,a3,a4,a5,a6,a7 be Element of BOOLEAN such that
A2: a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7;
A3: x1 in InputVertices S & x2 in InputVertices S & x3 in InputVertices S &
x4 in InputVertices S & x5 in InputVertices S & x6 in InputVertices S &
x7 in InputVertices S
by ThSTC0S9;
A5: Following(s,5).C1C2a
= ((a1'&'a2)'or'(a2'&'a3)'or'(a3'&'a1))'&'
((a5'&'a6)'or'(a6'&'a7)'or'(a7'&'a5)) &
Following(s,5).C2C3a
= ((a5'&'a6)'or'(a6'&'a7)'or'(a7'&'a5))'&'
(((a1'xor'a2'xor'a3)'&'(a5'xor'a6'xor'a7))'or'
((a5'xor'a6'xor'a7)'&'a4)'or'(a4'&'(a1'xor'a2'xor'a3))) &
Following(s,5).C3C1a
= (((a1'xor'a2'xor'a3)'&'(a5'xor'a6'xor'a7))'or'
((a5'xor'a6'xor'a7)'&'a4)'or'(a4'&'(a1'xor'a2'xor'a3)))'&'
((a1'&'a2)'or'(a2'&'a3)'or'(a3'&'a1))
by A2,LmSTC0S15S2s6;
Following(s,5+1) = Following Following(s,5) by FACIRC_1:12;
hence thesis by A2,A3,CIRCCMB3:1,A5,LmSTC0S15S2s8;
end;
:: -----------------------------------
:: main Proposition #3-1 (Internal Circuit Outputs after 4,6-steps)
theorem :: ThSTC0S17: :: for Output S0, S1 and S2
for x1,x2,x3,x4,x5,x6,x7 being non pair set
for s being State of STC0Circ(x1,x2,x3,x4,x5,x6,x7)
for a1,a2,a3,a4,a5,a6,a7 being Element of BOOLEAN st
a1 = s.x1 & a2 = s.x2 & a3 = s.x3 & a4 = s.x4 &
a5 = s.x5 & a6 = s.x6 & a7 = s.x7
holds
Following(s,4).STC0OutputS0(x1,x2,x3,x4,x5,x6,x7)
= a1'xor'a2'xor'a3'xor'a4'xor'a5'xor'a6'xor'a7 &
Following(s,6).STC0OutputS1(x1,x2,x3,x4,x5,x6,x7)
= ((a1'&'a2)'or'(a2'&'a3)'or'(a3'&'a1))
'xor'
((a5'&'a6)'or'(a6'&'a7)'or'(a7'&'a5))
'xor'
(((a1'xor'a2'xor'a3)'&'(a5'xor'a6'xor'a7))'or'
((a5'xor'a6'xor'a7)'&'a4)'or'(a4'&'(a1'xor'a2'xor'a3))) &
Following(s,6).STC0OutputS2(x1,x2,x3,x4,x5,x6,x7)
= (((a1'&'a2)'or'(a2'&'a3)'or'(a3'&'a1))'&'
((a5'&'a6)'or'(a6'&'a7)'or'(a7'&'a5)))
'or'
(((a5'&'a6)'or'(a6'&'a7)'or'(a7'&'a5))'&'
(((a1'xor'a2'xor'a3)'&'(a5'xor'a6'xor'a7))'or'
((a5'xor'a6'xor'a7)'&'a4)'or'(a4'&'(a1'xor'a2'xor'a3))))
'or'
((((a1'xor'a2'xor'a3)'&'(a5'xor'a6'xor'a7))'or'
((a5'xor'a6'xor'a7)'&'a4)'or'(a4'&'(a1'xor'a2'xor'a3)))'&'
((a1'&'a2)'or'(a2'&'a3)'or'(a3'&'a1))) &
Following(s,6).x1 = a1 & Following(s,6).x2 = a2 &
Following(s,6).x3 = a3 & Following(s,6).x4 = a4 &
Following(s,6).x5 = a5 & Following(s,6).x6 = a6 &
Following(s,6).x7 = a7
by LmSTC0S15S0,LmSTC0S15S1,LmSTC0S15S2;
:: --------------------------
:: main Proposition #3-2 (Stability after 6-steps)
theorem :: ThSTC0S18:
for x1,x2,x3,x4,x5,x6,x7 being non pair set
for s being State of STC0Circ(x1,x2,x3,x4,x5,x6,x7)
holds Following(s,6) is stable
proof
let x1,x2,x3,x4,x5,x6,x7 be non pair set;
set S = STC0Str(x1,x2,x3,x4,x5,x6,x7);
set C = STC0Circ(x1,x2,x3,x4,x5,x6,x7);
set S1 = STC0IStr(x1,x2,x3,x4,x5,x6,x7);
set C1 = STC0ICirc(x1,x2,x3,x4,x5,x6,x7);
set A1out = GFA0AdderOutput(x1,x2,x3);
set A2out = GFA0AdderOutput(x5,x6,x7);
set C1out = GFA0CarryOutput(x1,x2,x3);
set C2out = GFA0CarryOutput(x5,x6,x7);
set C3out = GFA0CarryOutput(A1out,A2out,x4);
set S2 = BitGFA0Str(C1out,C2out,C3out);
set C2 = BitGFA0Circ(C1out,C2out,C3out);
set C1C2x = [<*C1out,C2out*>, xor2];
set C1C2a = [<*C1out,C2out*>, and2];
set C2C3a = [<*C2out,C3out*>, and2];
set C3C1a = [<*C3out,C1out*>, and2];
set n1=4, n2=2;
let s be State of C;
C1 tolerates C2 by CIRCCOMB:60;
then
A2: the Sorts of C1 tolerates the Sorts of C2 by CIRCCOMB:def 3;
then reconsider s1 = s|the carrier of S1 as State of C1 by CIRCCOMB:26;
reconsider s2 = Following(s,n1)|the carrier of S2 as State of C2
by A2,CIRCCOMB:26;
A3: InputVertices S1 misses InnerVertices S2 & Following(s1,n1) is stable
by LmSTC0S2b,ThSTC0IS18;
C3out <> C1C2x & C1out <> C2C3a & C2out <> C3C1a & C3out <> C1C2a
by LmSTC0S1;
then Following(s2,n2) is stable by GFACIRC1:40;
then Following(s,n1+n2) is stable by A3,CIRCCMB2:19,CIRCCOMB:60;
hence thesis;
end;
::========================================================================