:: Stability of the 7-3 Compressor Circuit for {W}allace Tree. Part {I}
:: by Katsumi Wasaki
::
:: Received December 30, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users


::=========================================================================
registration
let x1, x2, x3, x4 be non pair object ;
cluster {x1,x2,x3,x4} -> without_pairs ;
coherence
not {x1,x2,x3,x4} is with_pair by ENUMSET1:def 2;
let x5 be non pair object ;
cluster {x1,x2,x3,x4,x5} -> without_pairs ;
coherence
not {x1,x2,x3,x4,x5} is with_pair by ENUMSET1:def 3;
let x6 be non pair object ;
cluster {x1,x2,x3,x4,x5,x6} -> without_pairs ;
coherence
not {x1,x2,x3,x4,x5,x6} is with_pair by ENUMSET1:def 4;
let x7 be non pair object ;
cluster {x1,x2,x3,x4,x5,x6,x7} -> without_pairs ;
coherence
not {x1,x2,x3,x4,x5,x6,x7} is with_pair 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) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: WALLACE1:def 1
(BitGFA0Str (x1,x2,x3)) +* (BitGFA0Str (x5,x6,x7));
coherence
(BitGFA0Str (x1,x2,x3)) +* (BitGFA0Str (x5,x6,x7)) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;
end;

:: deftheorem defines STC0IIStr WALLACE1:def 1 :
for x1, x2, x3, x5, x6, x7 being set holds STC0IIStr (x1,x2,x3,x5,x6,x7) = (BitGFA0Str (x1,x2,x3)) +* (BitGFA0Str (x5,x6,x7));

definition
let x1, x2, x3, x5, x6, x7 be set ;
func STC0IICirc (x1,x2,x3,x5,x6,x7) -> strict gate`2=den Boolean Circuit of STC0IIStr (x1,x2,x3,x5,x6,x7) equals :: WALLACE1:def 2
(BitGFA0Circ (x1,x2,x3)) +* (BitGFA0Circ (x5,x6,x7));
coherence
(BitGFA0Circ (x1,x2,x3)) +* (BitGFA0Circ (x5,x6,x7)) is strict gate`2=den Boolean Circuit of STC0IIStr (x1,x2,x3,x5,x6,x7) ;
end;

:: deftheorem defines STC0IICirc WALLACE1:def 2 :
for x1, x2, x3, x5, x6, x7 being set holds STC0IICirc (x1,x2,x3,x5,x6,x7) = (BitGFA0Circ (x1,x2,x3)) +* (BitGFA0Circ (x5,x6,x7));

::-----------------------------------------------
:: 1-2. Properties of `Intermediate' Circuit Structure
::-----------------------------------------------
::---------------------------------------
:: InnerVertices of STC_TYPE0_Inter_Inter.
theorem ThSTC0IIS1: :: WALLACE1:1
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 end;

theorem :: WALLACE1:2
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: :: WALLACE1:3
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 end;

theorem ThSTC0IIS5: :: WALLACE1:4
for x1, x2, x3, x5, x6, x7 being non pair set holds InputVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) is without_pairs
proof end;

::---------------------------------------
:: The Element of Carriers, InnerVertices and InputVertices of
:: STC_TYPE0_Inter_Inter.
theorem ThSTC0IIS6: :: WALLACE1:5
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 end;

theorem ThSTC0IIS7: :: WALLACE1:6
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 end;

theorem ThSTC0IIS8: :: WALLACE1:7
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 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 :: WALLACE1:def 3
 GFA0CarryOutput (x1,x2,x3);
coherence
GFA0CarryOutput (x1,x2,x3) is Element of InnerVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) by ThSTC0IIS7;
func STC0IIAdderOutputA1 (x1,x2,x3,x5,x6,x7) -> Element of InnerVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) equals :: WALLACE1:def 4
 GFA0AdderOutput (x1,x2,x3);
coherence
GFA0AdderOutput (x1,x2,x3) is Element of InnerVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) by ThSTC0IIS7;
func STC0IICarryOutputC2 (x1,x2,x3,x5,x6,x7) -> Element of InnerVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) equals :: WALLACE1:def 5
 GFA0CarryOutput (x5,x6,x7);
coherence
GFA0CarryOutput (x5,x6,x7) is Element of InnerVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) by ThSTC0IIS7;
func STC0IIAdderOutputA2 (x1,x2,x3,x5,x6,x7) -> Element of InnerVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) equals :: WALLACE1:def 6
 GFA0AdderOutput (x5,x6,x7);
coherence
GFA0AdderOutput (x5,x6,x7) is Element of InnerVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) by ThSTC0IIS7;
end;

:: deftheorem defines STC0IICarryOutputC1 WALLACE1:def 3 :
for x1, x2, x3, x5, x6, x7 being set holds STC0IICarryOutputC1 (x1,x2,x3,x5,x6,x7) = GFA0CarryOutput (x1,x2,x3);

:: deftheorem defines STC0IIAdderOutputA1 WALLACE1:def 4 :
for x1, x2, x3, x5, x6, x7 being set holds STC0IIAdderOutputA1 (x1,x2,x3,x5,x6,x7) = GFA0AdderOutput (x1,x2,x3);

:: deftheorem defines STC0IICarryOutputC2 WALLACE1:def 5 :
for x1, x2, x3, x5, x6, x7 being set holds STC0IICarryOutputC2 (x1,x2,x3,x5,x6,x7) = GFA0CarryOutput (x5,x6,x7);

:: deftheorem defines STC0IIAdderOutputA2 WALLACE1:def 6 :
for x1, x2, x3, x5, x6, x7 being set holds STC0IIAdderOutputA2 (x1,x2,x3,x5,x6,x7) = GFA0AdderOutput (x5,x6,x7);

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

:: -----------------------------------
:: Proposition #1-1 (Internal Circuit Outputs after Two-steps)
theorem ThSTC0IIS10: :: WALLACE1:8
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 end;

:: --------------------------
:: Proposition #1-2 (Stability after Two-steps)
theorem ThSTC0IIS12: :: WALLACE1:9
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 end;

::=========================================================================
::---------------------------------------------------------------
:: 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) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: WALLACE1:def 7
(STC0IIStr (x1,x2,x3,x5,x6,x7)) +* (BitGFA0Str ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4));
coherence
(STC0IIStr (x1,x2,x3,x5,x6,x7)) +* (BitGFA0Str ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;
end;

:: deftheorem defines STC0IStr WALLACE1:def 7 :
for x1, x2, x3, x4, x5, x6, x7 being set holds STC0IStr (x1,x2,x3,x4,x5,x6,x7) = (STC0IIStr (x1,x2,x3,x5,x6,x7)) +* (BitGFA0Str ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4));

definition
let x1, x2, x3, x4, x5, x6, x7 be set ;
func STC0ICirc (x1,x2,x3,x4,x5,x6,x7) -> strict gate`2=den Boolean Circuit of STC0IStr (x1,x2,x3,x4,x5,x6,x7) equals :: WALLACE1:def 8
(STC0IICirc (x1,x2,x3,x5,x6,x7)) +* (BitGFA0Circ ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4));
coherence
(STC0IICirc (x1,x2,x3,x5,x6,x7)) +* (BitGFA0Circ ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)) is strict gate`2=den Boolean Circuit of STC0IStr (x1,x2,x3,x4,x5,x6,x7) ;
end;

:: deftheorem defines STC0ICirc WALLACE1:def 8 :
for x1, x2, x3, x4, x5, x6, x7 being set holds STC0ICirc (x1,x2,x3,x4,x5,x6,x7) = (STC0IICirc (x1,x2,x3,x5,x6,x7)) +* (BitGFA0Circ ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4));

::-----------------------------------------------
:: 2-2. Properties of `Intermediate' STC Circuit Structure
::-----------------------------------------------
:: -----------------------------------
:: InnerVertices of of STC_TYPE0_Inter.
theorem ThSTC0IS1: :: WALLACE1:10
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 end;

theorem :: WALLACE1:11
for x1, x2, x3, x4, x5, x6, x7 being set holds InnerVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) is Relation ;

LmSTC0IS1: for x, y, z, p being set holds GFA0AdderOutput (x,y,z) <> [p,and2]
proof 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 end;

theorem ThSTC0IS3: :: WALLACE1:12
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 end;

theorem ThSTC0IS4: :: WALLACE1:13
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 end;

theorem ThSTC0IS5: :: WALLACE1:14
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 end;

:: -----------------------------------
:: The Element of Carriers, InnerVertices and InputVertices of STC_TYPE0_Inter.
theorem ThSTC0IS6: :: WALLACE1:15
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 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 end;

theorem ThSTC0IS7: :: WALLACE1:16
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 end;

theorem :: WALLACE1:17
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 end;

theorem ThSTC0IS9: :: WALLACE1:18
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 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 :: WALLACE1:def 9
 GFA0CarryOutput (x1,x2,x3);
coherence
GFA0CarryOutput (x1,x2,x3) is Element of InnerVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) by ThSTC0IS7;
func STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7) -> Element of InnerVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) equals :: WALLACE1:def 10
 GFA0CarryOutput (x5,x6,x7);
coherence
GFA0CarryOutput (x5,x6,x7) is Element of InnerVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) by ThSTC0IS7;
func STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7) -> Element of InnerVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) equals :: WALLACE1:def 11
 GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4);
coherence
GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4) is Element of InnerVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) by ThSTC0IS7;
func STC0IAdderOutputA3 (x1,x2,x3,x4,x5,x6,x7) -> Element of InnerVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) equals :: WALLACE1:def 12
 GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4);
coherence
GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4) is Element of InnerVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) by ThSTC0IS7;
end;

:: deftheorem defines STC0ICarryOutputC1 WALLACE1:def 9 :
for x1, x2, x3, x4, x5, x6, x7 being set holds STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7) = GFA0CarryOutput (x1,x2,x3);

:: deftheorem defines STC0ICarryOutputC2 WALLACE1:def 10 :
for x1, x2, x3, x4, x5, x6, x7 being set holds STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7) = GFA0CarryOutput (x5,x6,x7);

:: deftheorem defines STC0ICarryOutputC3 WALLACE1:def 11 :
for x1, x2, x3, x4, x5, x6, x7 being set holds STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7) = GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4);

:: deftheorem defines STC0IAdderOutputA3 WALLACE1:def 12 :
for x1, x2, x3, x4, x5, x6, x7 being set holds STC0IAdderOutputA3 (x1,x2,x3,x4,x5,x6,x7) = GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4);

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

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

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

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

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

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

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

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

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

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

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

:: -----------------------------------
:: Proposition #2-1 (Internal Circuit Outputs after 2,4-steps)
theorem :: WALLACE1:19
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: :: WALLACE1:20
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 end;

::=========================================================================
::---------------------------------------------------------------
:: 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) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: WALLACE1:def 13
(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
(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)))) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;
end;

:: deftheorem defines STC0Str WALLACE1:def 13 :
for x1, x2, x3, x4, x5, x6, x7 being set holds STC0Str (x1,x2,x3,x4,x5,x6,x7) = (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))));

definition
let x1, x2, x3, x4, x5, x6, x7 be set ;
func STC0Circ (x1,x2,x3,x4,x5,x6,x7) -> strict gate`2=den Boolean Circuit of STC0Str (x1,x2,x3,x4,x5,x6,x7) equals :: WALLACE1:def 14
(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
(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)))) is strict gate`2=den Boolean Circuit of STC0Str (x1,x2,x3,x4,x5,x6,x7) ;
end;

:: deftheorem defines STC0Circ WALLACE1:def 14 :
for x1, x2, x3, x4, x5, x6, x7 being set holds STC0Circ (x1,x2,x3,x4,x5,x6,x7) = (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))));

::-----------------------------------------------
:: 3-2. Properties of STC Circuit Structure
::-----------------------------------------------
:: -----------------------------------
:: InnerVertices of of STC_TYPE0
theorem ThSTC0S1a: :: WALLACE1:21
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 end;

theorem ThSTC0S1: :: WALLACE1:22
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 end;

theorem :: WALLACE1:23
for x1, x2, x3, x4, x5, x6, x7 being set holds InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) is Relation ;

LmSTC0S1: for f1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN
for x, y, z, a, b being set holds GFA0CarryOutput (x,y,z) <> [<*a,b*>,f1]
proof 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 end;

theorem ThSTC0S4: :: WALLACE1:24
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 end;

theorem :: WALLACE1:25
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 end;

:: -----------------------------------
:: The Element of Carriers, InnerVertices and InputVertices of STC_TYPE0.
theorem ThSTC0S6: :: WALLACE1:26
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) 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 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 end;

theorem ThSTC0S7: :: WALLACE1:27
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 end;

theorem ThSTC0S9: :: WALLACE1:28
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 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 :: WALLACE1:def 15
 GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4);
coherence
GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4) is Element of InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) by ThSTC0S7;
func STC0OutputS1 (x1,x2,x3,x4,x5,x6,x7) -> Element of InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) equals :: WALLACE1:def 16
 GFA0AdderOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)));
coherence
GFA0AdderOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))) is Element of InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) by ThSTC0S7;
func STC0OutputS2 (x1,x2,x3,x4,x5,x6,x7) -> Element of InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) equals :: WALLACE1:def 17
 GFA0CarryOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)));
coherence
GFA0CarryOutput ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))) is Element of InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) by ThSTC0S7;
end;

:: deftheorem defines STC0OutputS0 WALLACE1:def 15 :
for x1, x2, x3, x4, x5, x6, x7 being set holds STC0OutputS0 (x1,x2,x3,x4,x5,x6,x7) = GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4);

:: deftheorem defines STC0OutputS1 WALLACE1:def 16 :
for x1, x2, x3, x4, x5, x6, x7 being set holds STC0OutputS1 (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)));

:: deftheorem defines STC0OutputS2 WALLACE1:def 17 :
for x1, x2, x3, x4, x5, x6, x7 being set holds STC0OutputS2 (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)));

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

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

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

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

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

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

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

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

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

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

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

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

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

:: -----------------------------------
:: main Proposition #3-1 (Internal Circuit Outputs after 4,6-steps)
theorem :: WALLACE1:29
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 :: WALLACE1:30
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 end;