:: Generalized Full Adder Circuits (GFAs). {P}art {I}
::  by Shin'nosuke Yamaguchi , Katsumi Wasaki and Nobuhiro Shimoi
::
:: Received December 7, 2005
:: Copyright (c) 2005-2021 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 NUMBERS, SUBSET_1, MARGREL1, FUNCT_1, FINSEQ_2, FINSEQ_1,
      XBOOLEAN, TWOSCOMP, CARD_1, RELAT_1, ORDINAL4, TARSKI, XBOOLE_0,
      CLASSES1, FSM_1, FACIRC_1, CIRCUIT2, MSAFREE2, CIRCCOMB, STRUCT_0,
      GLIB_000, MSUALG_1, FUNCT_4, LATTICES, CIRCUIT1, PARTFUN1, ARYTM_3,
      GFACIRC1;
 notations TARSKI, XBOOLE_0, ENUMSET1, XTUPLE_0, SUBSET_1, NAT_1, RELAT_1,
      ORDINAL1, NUMBERS, STRUCT_0, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2,
      MARGREL1, CLASSES1, BINARITH, MSUALG_1, MSAFREE2, CIRCUIT1, CIRCUIT2,
      CIRCCOMB, FACIRC_1, TWOSCOMP;
 constructors ENUMSET1, CLASSES1, BINARITH, CIRCUIT1, CIRCUIT2, FACIRC_1,
      TWOSCOMP, NAT_1, RELSET_1, XTUPLE_0, NUMBERS;
 registrations RELAT_1, MARGREL1, FINSEQ_2, CARD_3, STRUCT_0, CIRCCOMB,
      FACIRC_1, ORDINAL1, FINSEQ_1, FUNCT_1, MSAFREE2, XTUPLE_0;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin :: Preliminaries
::========================================================================
::------------------------------------------
:: schemes for Boolean Operations (1 input)

scheme :: GFACIRC1:sch 1
  1AryBooleEx {F(set) -> Element of BOOLEAN}: ex f being Function of 1
-tuples_on BOOLEAN, BOOLEAN st for x being Element of BOOLEAN holds f.<*x*> = F
  (x);

scheme :: GFACIRC1:sch 2
  1AryBooleUniq {F(set) -> Element of BOOLEAN}: for f1,f2 being Function of 1
-tuples_on BOOLEAN, BOOLEAN st (for x being Element of BOOLEAN holds f1.<*x*> =
  F(x)) & (for x being Element of BOOLEAN holds f2.<*x*> = F(x)) holds f1 = f2;

scheme :: GFACIRC1:sch 3
  1AryBooleDef {F(set) -> Element of BOOLEAN}: (ex f being Function of 1
-tuples_on BOOLEAN, BOOLEAN st for x being Element of BOOLEAN holds f.<*x*> = F
(x)) & for f1,f2 being Function of 1-tuples_on BOOLEAN, BOOLEAN st (for x being
  Element of BOOLEAN holds f1.<*x*> = F(x)) & (for x being Element of BOOLEAN
  holds f2.<*x*> = F(x)) holds f1 = f2;

::-------------------------------------
:: 1-Input Operators (inv1, buf1)

definition
  func inv1 -> Function of 1-tuples_on BOOLEAN, BOOLEAN means
:: GFACIRC1:def 1

  for x being Element of BOOLEAN holds it.<*x*> = 'not' x;
end;

theorem :: GFACIRC1:1
  for x being Element of BOOLEAN holds inv1.<*x*> = 'not' x & inv1.
  <*x*> = nand2.<*x,x*> & inv1.<*0*> = 1 & inv1.<*1*> = 0;

definition
  func buf1 -> Function of 1-tuples_on BOOLEAN, BOOLEAN means
:: GFACIRC1:def 2

  for x being Element of BOOLEAN holds it.<*x*> = x;
end;

theorem :: GFACIRC1:2
  for x being Element of BOOLEAN holds buf1.<*x*> = x & buf1.<*x*> =
  and2.<*x,x*> & buf1.<*0*> = 0 & buf1.<*1*> = 1;

::-------------------------------------
:: 2-Input Operators (and2c, xor2c)

definition
  func and2c -> Function of 2-tuples_on BOOLEAN, BOOLEAN means
:: GFACIRC1:def 3

  for x,y being Element of BOOLEAN holds it.<*x,y*> = x '&' 'not' y;
end;

theorem :: GFACIRC1:3
  for x,y being Element of BOOLEAN holds and2c.<*x,y*> = x '&' 'not' y &
and2c.<*x,y*> = and2a.<*y,x*> & and2c.<*x,y*> = nor2a.<*x,y*> & and2c.<*0,0*>=0
  & and2c.<*0,1*>=0 & and2c.<*1,0*>=1 & and2c.<*1,1*>=0;

definition
  func xor2c -> Function of 2-tuples_on BOOLEAN, BOOLEAN means
:: GFACIRC1:def 4

  for x,y being Element of BOOLEAN holds it.<*x,y*> = x 'xor' 'not' y;
end;

theorem :: GFACIRC1:4
  for x,y being Element of BOOLEAN holds xor2c.<*x,y*> = x 'xor'
'not' y & xor2c.<*x,y*> = xor2a.<*x,y*> & xor2c.<*x,y*> = or2.<*nor2.<*x,y*>,
and2.<*x,y*> *> & xor2c.<*0,0*>=1 & xor2c.<*0,1*>=0 & xor2c.<*1,0*>=0 & xor2c.
  <*1,1*>=1;

theorem :: GFACIRC1:5
  for x,y being Element of BOOLEAN holds inv1.<* xor2.<*x,y*> *> = xor2a
.<*x,y*> & inv1.<* xor2.<*x,y*> *> = xor2c.<*x,y*> & xor2.<* inv1.<*x*>, inv1.
  <*y*> *> = xor2.<*x,y*>;

theorem :: GFACIRC1:6
  for x,y,z being Element of BOOLEAN holds inv1.<* xor2.<* xor2c.<*x,y*>
  , z*> *> = xor2c.<* xor2c.<*x,y*>, z*>;

theorem :: GFACIRC1:7
  for x,y,z being Element of BOOLEAN holds ( 'not' x 'xor' y ) 'xor'
  'not' z = ( x 'xor' 'not' y ) 'xor' 'not' z;

theorem :: GFACIRC1:8
  for x,y,z being Element of BOOLEAN holds xor2c.<* xor2a.<*x,y*>, z *>
  = xor2c.<* xor2c.<*x,y*>, z *>;

theorem :: GFACIRC1:9
  for x,y,z being Element of BOOLEAN holds inv1.<* xor2c.<* xor2b.<*x,y
  *>, z*> *> = xor2.<* xor2.<*x,y*>, z*>;

::========================================================================
:: Generalized Full Adder (GFA) Circuit (TYPE-0)
::========================================================================

begin :: Generalized Full Adder (GFA) Circuit (TYPE-0)
::========================================================================
:: << GFA TYPE-0 >>
::------------------------------------------------------------------------
::   Name     : Generalized Full Adder Type-0 (GFA0)
::   Function : x + y + z = 2 * c + s
::
::   Logic Symbol :      x      y      Combined : GFA0CarryIStr(x,y,z)
::                       |     /                  GFA0CarryStr(x,y,z)
::                       |    /                   GFA0AdderStr(x,y,z)
::                   +---*---*                  --->
::                   |  GFA  *-----z              BitGFA0Str(x,y,z)
::                   | TYPE0 |
::                   *---*---+          Outputs : BitGFA0CarryOutput(x,y,z)
::                  /    |                        BitGFA0AdderOutput(x,y,z)
::                 /     |
::                c      s          Calculation : Following(s,2) is stable.
::=========================================================================
::-------------------------------------------------
:: GFA0 Carry : Circuit Definition of Carry Output
::-------------------------------------------------

definition
  let x,y,z be set;
  func GFA0CarryIStr(x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void
  strict non empty ManySortedSign equals
:: GFACIRC1:def 5
  1GateCircStr(<*x,y*>,and2) +*
  1GateCircStr(<*y,z*>,and2) +* 1GateCircStr(<*z,x*>,and2);
end;

definition
  let x,y,z be set;
  func GFA0CarryICirc(x,y,z) -> strict Boolean gate`2=den Circuit of
  GFA0CarryIStr(x,y,z) equals
:: GFACIRC1:def 6
  1GateCircuit(x,y,and2) +* 1GateCircuit(y,z,and2) +*
  1GateCircuit(z,x,and2);
end;

definition
  let x,y,z be set;
  func GFA0CarryStr(x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void
  strict non empty ManySortedSign equals
:: GFACIRC1:def 7
  GFA0CarryIStr(x,y,z) +* 1GateCircStr(<*[
  <*x,y*>,and2], [<*y,z*>,and2], [<*z,x*>,and2]*>,or3);
end;

definition
  let x,y,z be set;
  func GFA0CarryCirc(x,y,z) -> strict Boolean gate`2=den Circuit of
  GFA0CarryStr(x,y,z) equals
:: GFACIRC1:def 8
  GFA0CarryICirc(x,y,z) +* 1GateCircuit([<*x,y*>,and2]
  ,[<*y,z*>,and2],[<*z,x*>,and2],or3);
end;

definition
  let x,y,z be set;
  func GFA0CarryOutput(x,y,z) -> Element of InnerVertices GFA0CarryStr(x,y,z)
  equals
:: GFACIRC1:def 9
  [<*[<*x,y*>,and2],[<*y,z*>,and2],[<*z,x*>,and2]*>,or3];
end;

::-------------------------------------------------------
:: GFA0 Carry : Carrier, InnerVertices and InputVertices
::-------------------------------------------------------
::-------------------------------------------------------
:: InnerVertices

theorem :: GFACIRC1:10
  for x,y,z being set holds InnerVertices GFA0CarryIStr(x,y,z) = {
  [<*x,y*>,and2], [<*y,z*>,and2], [<*z,x*>,and2]};

theorem :: GFACIRC1:11
  for x,y,z being set holds InnerVertices GFA0CarryStr(x,y,z) = {[
  <*x,y*>,and2], [<*y,z*>,and2], [<*z,x*>,and2]} \/ {GFA0CarryOutput(x,y,z)};

theorem :: GFACIRC1:12
  for x,y,z being set holds InnerVertices GFA0CarryStr(x,y,z) is Relation;

::-------------------------------------------------------
:: InputVertices

theorem :: GFACIRC1:13
  for x,y,z being set st x <> [<*y,z*>,and2] & y <> [<*z,x*>,and2]
  & z <> [<*x,y*>,and2] holds InputVertices GFA0CarryIStr(x,y,z) = {x,y,z};

theorem :: GFACIRC1:14
  for x,y,z being set st x <> [<*y,z*>,and2] & y <> [<*z,x*>,and2]
  & z <> [<*x,y*>,and2] holds InputVertices GFA0CarryStr(x,y,z) = {x,y,z};

theorem :: GFACIRC1:15
  for x,y,z being non pair set holds InputVertices GFA0CarryStr(x,y,z)
  is without_pairs;

::-------------------------------------------------------
:: Carrier and misc.

theorem :: GFACIRC1:16
  for x,y,z being set holds x in the carrier of GFA0CarryStr(x,y,z
) & y in the carrier of GFA0CarryStr(x,y,z) & z in the carrier of GFA0CarryStr(
x,y,z) & [<*x,y*>,and2] in the carrier of GFA0CarryStr(x,y,z) & [<*y,z*>,and2]
  in the carrier of GFA0CarryStr(x,y,z) & [<*z,x*>,and2] in the carrier of
GFA0CarryStr(x,y,z) & [<*[<*x,y*>,and2],[<*y,z*>,and2],[<*z,x*>,and2]*>,or3] in
  the carrier of GFA0CarryStr(x,y,z);

theorem :: GFACIRC1:17
  for x,y,z being set holds [<*x,y*>,and2] in InnerVertices
GFA0CarryStr(x,y,z) & [<*y,z*>,and2] in InnerVertices GFA0CarryStr(x,y,z) & [<*
  z,x*>,and2] in InnerVertices GFA0CarryStr(x,y,z) & GFA0CarryOutput(x,y,z) in
  InnerVertices GFA0CarryStr(x,y,z);

theorem :: GFACIRC1:18
  for x,y,z being set st x <> [<*y,z*>,and2] & y <> [<*z,x*>,and2]
  & z <> [<*x,y*>,and2] holds x in InputVertices GFA0CarryStr(x,y,z) & y in
  InputVertices GFA0CarryStr(x,y,z) & z in InputVertices GFA0CarryStr(x,y,z);

theorem :: GFACIRC1:19
  for x,y,z being non pair set holds InputVertices GFA0CarryStr(x,
  y,z) = {x,y,z};

::----------------------------------------------------
:: GFA0 Carry : Stability of the Carry Output Circuit
::----------------------------------------------------

theorem :: GFACIRC1:20
  for x,y,z being set for s being State of GFA0CarryCirc(x,y,z)
for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3 = s.z holds (
Following s).[<*x,y*>,and2] = a1 '&' a2 & (Following s).[<*y,z*>,and2] = a2 '&'
  a3 & (Following s).[<*z,x*>,and2] = a3 '&' a1;

theorem :: GFACIRC1:21
  for x,y,z being set for s being State of GFA0CarryCirc(x,y,z)
for a1,a2,a3 being Element of BOOLEAN st a1 = s.[<*x,y*>,and2] & a2 = s.[<*y,z
  *>,and2] & a3 = s.[<*z,x*>,and2] holds (Following s).GFA0CarryOutput(x,y,z) =
  a1 'or' a2 'or' a3;

theorem :: GFACIRC1:22
  for x,y,z being set st x <> [<*y,z*>,and2] & y <> [<*z,x*>,and2]
  & z <> [<*x,y*>,and2] for s being State of GFA0CarryCirc(x,y,z) for a1,a2,a3
being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3 = s.z holds Following(s,2)
  .GFA0CarryOutput(x,y,z) = (a1 '&' a2) 'or' (a2 '&' a3) 'or' (a3 '&' a1) &
Following(s,2).[<*x,y*>,and2] = a1 '&' a2 & Following(s,2).[<*y,z*>,and2] = a2
  '&' a3 & Following(s,2).[<*z,x*>,and2] = a3 '&' a1;

theorem :: GFACIRC1:23
  for x,y,z being set st x <> [<*y,z*>,and2] & y <> [<*z,x*>,and2]
& z <> [<*x,y*>,and2] for s being State of GFA0CarryCirc(x,y,z) holds Following
  (s,2) is stable;

::=========================================================================
::-------------------------------------------------
:: GFA0 Adder : Circuit Definition of Adder Output
::-------------------------------------------------

definition
  let x,y,z be set;
  func GFA0AdderStr(x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void
  strict non empty ManySortedSign equals
:: GFACIRC1:def 10
  2GatesCircStr(x,y,z, xor2);
end;

definition
  let x,y,z be set;
  func GFA0AdderCirc(x,y,z) -> strict Boolean gate`2=den Circuit of
  GFA0AdderStr(x,y,z) equals
:: GFACIRC1:def 11
  2GatesCircuit(x,y,z, xor2);
end;

definition
  let x,y,z be set;
  func GFA0AdderOutput(x,y,z) -> Element of InnerVertices GFA0AdderStr(x,y,z)
  equals
:: GFACIRC1:def 12
  2GatesCircOutput(x,y,z, xor2);
end;

::-------------------------------------------------------
:: GFA0 Adder : Carrier, InnerVertices and InputVertices
::-------------------------------------------------------
::-------------------------------------------------------
:: InnerVertices

theorem :: GFACIRC1:24
  for x,y,z being set holds InnerVertices GFA0AdderStr(x,y,z) = {[
  <*x,y*>,xor2]} \/ {GFA0AdderOutput(x,y,z)};

::-------------------------------------------------------
:: Carrier and misc.

theorem :: GFACIRC1:25
  for x,y,z being set holds x in the carrier of GFA0AdderStr(x,y,z) & y
in the carrier of GFA0AdderStr(x,y,z) & z in the carrier of GFA0AdderStr(x,y,z)
& [<*x,y*>,xor2] in the carrier of GFA0AdderStr(x,y,z) & [<*[<*x,y*>,xor2], z*>
  , xor2] in the carrier of GFA0AdderStr(x,y,z);

theorem :: GFACIRC1:26
  for x,y,z being set holds [<*x,y*>,xor2] in InnerVertices
GFA0AdderStr(x,y,z) & GFA0AdderOutput(x,y,z) in InnerVertices GFA0AdderStr(x,y,
  z);

theorem :: GFACIRC1:27
  for x,y,z being set st z <> [<*x,y*>, xor2] holds x in
InputVertices GFA0AdderStr(x,y,z) & y in InputVertices GFA0AdderStr(x,y,z) & z
  in InputVertices GFA0AdderStr(x,y,z);

::----------------------------------------------------
:: GFA0 Adder : Stability of the Adder Output Circuit
::----------------------------------------------------

theorem :: GFACIRC1:28
  for x,y,z being set st z <> [<*x,y*>, xor2] for s being State of
GFA0AdderCirc(x,y,z) for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s
.y & a3 = s.z holds (Following s).[<*x,y*>,xor2] = a1 'xor' a2 & (Following s).
  x = a1 & (Following s).y = a2 & (Following s).z = a3;

theorem :: GFACIRC1:29
  for x,y,z being set st z <> [<*x,y*>, xor2] for s being State of
GFA0AdderCirc(x,y,z) for a1a2,a1,a2,a3 being Element of BOOLEAN st a1a2 = s.[<*
x,y*>,xor2] & a3 = s.z holds (Following s).GFA0AdderOutput(x,y,z) = a1a2 'xor'
  a3;

theorem :: GFACIRC1:30
  for x,y,z being set st z <> [<*x,y*>, xor2] for s being State of
GFA0AdderCirc(x,y,z) for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s
  .y & a3 = s.z holds Following(s,2).GFA0AdderOutput(x,y,z) = a1 'xor' a2 'xor'
  a3 & Following(s,2).[<*x,y*>,xor2] = a1 'xor' a2 & Following(s,2).x = a1 &
  Following(s,2).y = a2 & Following(s,2).z = a3;

::=====================================================================
::---------------------------------------------------
:: GFA0 : Circuit Definition of GFA Combined Circuit
::---------------------------------------------------

definition
  let x,y,z be set;
  func BitGFA0Str(x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void
  strict non empty ManySortedSign equals
:: GFACIRC1:def 13
  GFA0AdderStr(x,y,z) +* GFA0CarryStr(x,y,
  z);
end;

definition
  let x,y,z be set;
  func BitGFA0Circ(x,y,z) -> strict Boolean gate`2=den Circuit of BitGFA0Str(x
  ,y,z) equals
:: GFACIRC1:def 14
  GFA0AdderCirc(x,y,z) +* GFA0CarryCirc(x,y,z);
end;

::----------------------------------------------------------
:: GFA0 Combined : Carrier, InnerVertices and InputVertices
::----------------------------------------------------------
::-------------------------------------------------------
:: InnerVertices

theorem :: GFACIRC1:31
  for x,y,z being set holds InnerVertices BitGFA0Str(x,y,z) = {[<*
x,y*>,xor2]} \/ {GFA0AdderOutput(x,y,z)} \/ {[<*x,y*>,and2], [<*y,z*>,and2], [
  <*z,x*>,and2]} \/ {GFA0CarryOutput(x,y,z)};

theorem :: GFACIRC1:32
  for x,y,z being set holds InnerVertices BitGFA0Str(x,y,z) is Relation;

::-------------------------------------------------------
:: InputVertices

theorem :: GFACIRC1:33
  for x,y,z being set st z <> [<*x,y*>,xor2] & x <> [<*y,z*>,and2]
& y <> [<*z,x*>,and2] & z <> [<*x,y*>,and2] holds InputVertices BitGFA0Str(x,y,
  z) = {x,y,z};

theorem :: GFACIRC1:34
  for x,y,z being non pair set holds InputVertices BitGFA0Str(x,y, z) = {x,y,z}
;

theorem :: GFACIRC1:35
  for x,y,z being non pair set holds InputVertices BitGFA0Str(x,y,z) is
  without_pairs;

::-------------------------------------------------------
:: Carrier and misc.

theorem :: GFACIRC1:36
  for x,y,z being set holds x in the carrier of BitGFA0Str(x,y,z) & y in
the carrier of BitGFA0Str(x,y,z) & z in the carrier of BitGFA0Str(x,y,z) & [<*x
,y*>,xor2] in the carrier of BitGFA0Str(x,y,z) & [<*[<*x,y*>,xor2],z*>,xor2] in
the carrier of BitGFA0Str(x,y,z) & [<*x,y*>,and2] in the carrier of BitGFA0Str(
x,y,z) & [<*y,z*>,and2] in the carrier of BitGFA0Str(x,y,z) & [<*z,x*>,and2] in
  the carrier of BitGFA0Str(x,y,z) & [<*[<*x,y*>,and2],[<*y,z*>,and2],[<*z,x*>,
  and2]*>,or3] in the carrier of BitGFA0Str(x,y,z);

theorem :: GFACIRC1:37
  for x,y,z being set holds [<*x,y*>,xor2] in InnerVertices
BitGFA0Str(x,y,z) & GFA0AdderOutput(x,y,z) in InnerVertices BitGFA0Str(x,y,z) &
  [<*x,y*>,and2] in InnerVertices BitGFA0Str(x,y,z) & [<*y,z*>,and2] in
InnerVertices BitGFA0Str(x,y,z) & [<*z,x*>,and2] in InnerVertices BitGFA0Str(x,
  y,z) & GFA0CarryOutput(x,y,z) in InnerVertices BitGFA0Str(x,y,z);

theorem :: GFACIRC1:38
  for x,y,z being set st z <> [<*x,y*>,xor2] & x <> [<*y,z*>,and2] & y
<> [<*z,x*>,and2] & z <> [<*x,y*>,and2] holds x in InputVertices BitGFA0Str(x,y
,z) & y in InputVertices BitGFA0Str(x,y,z) & z in InputVertices BitGFA0Str(x,y,
  z);

::------------------------------------------------------------------
:: GFA0 : Carry and Adder Output Definition of GFA Combined Circuit
::------------------------------------------------------------------

definition
  let x,y,z be set;
  func BitGFA0CarryOutput(x,y,z) -> Element of InnerVertices BitGFA0Str(x,y,z)
  equals
:: GFACIRC1:def 15
  [<*[<*x,y*>,and2],[<*y,z*>,and2],[<*z,x*>,and2]*>,or3];
end;

definition
  let x,y,z be set;
  func BitGFA0AdderOutput(x,y,z) -> Element of InnerVertices BitGFA0Str(x,y,z)
  equals
:: GFACIRC1:def 16
  2GatesCircOutput(x,y,z, xor2);
end;

::-------------------------------------------------------------
:: GFA0 Combined : Stability of the Adder/Carry Output Circuit
::-------------------------------------------------------------

theorem :: GFACIRC1:39
  for x,y,z being set st z <> [<*x,y*>,xor2] & x <> [<*y,z*>,and2] & y
<> [<*z,x*>,and2] & z <> [<*x,y*>,and2] for s being State of BitGFA0Circ(x,y,z)
  for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3 = s.z holds
Following(s,2).GFA0AdderOutput(x,y,z) = a1 'xor' a2 'xor' a3 & Following(s,2).
  GFA0CarryOutput(x,y,z) = a1 '&' a2 'or' a2 '&' a3 'or' a3 '&' a1;

theorem :: GFACIRC1:40
  for x,y,z being set st z <> [<*x,y*>,xor2] & x <> [<*y,z*>,and2] & y
<> [<*z,x*>,and2] & z <> [<*x,y*>,and2] for s being State of BitGFA0Circ(x,y,z)
  holds Following(s,2) is stable;

::========================================================================
:: Generalized Full Adder (GFA) Circuit (TYPE-1)
::========================================================================

begin :: Generalized Full Adder (GFA) Circuit (TYPE-1)
::========================================================================
:: << GFA TYPE-1 >>
::------------------------------------------------------------------------
::   Name     : Generalized Full Adder Type-1 (GFA1)
::   Function : x - y + z = 2 * c - s
::
::   Logic Symbol :      x     -y      Combined : GFA1CarryIStr(x,y,z)
::                       |     /                  GFA1CarryStr(x,y,z)
::                       |    /                   GFA1AdderStr(x,y,z)
::                   +---*---O                  --->
::                   |  GFA  *-----z              BitGFA1Str(x,y,z)
::                   | TYPE1 |
::                   *---O---+          Outputs : BitGFA1CarryOutput(x,y,z)
::                  /    |                        BitGFA1AdderOutput(x,y,z)
::                 /     |
::                c     -s          Calculation : Following(s,2) is stable.
::=========================================================================
::-------------------------------------------------
:: GFA1 Carry : Circuit Definition of Carry Output
::-------------------------------------------------

definition
  let x,y,z be set;
  func GFA1CarryIStr(x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void
  strict non empty ManySortedSign equals
:: GFACIRC1:def 17
  1GateCircStr(<*x,y*>,and2c) +*
  1GateCircStr(<*y,z*>,and2a) +* 1GateCircStr(<*z,x*>,and2);
end;

definition
  let x,y,z be set;
  func GFA1CarryICirc(x,y,z) -> strict Boolean gate`2=den Circuit of
  GFA1CarryIStr(x,y,z) equals
:: GFACIRC1:def 18
  1GateCircuit(x,y,and2c) +* 1GateCircuit(y,z,and2a)
  +* 1GateCircuit(z,x,and2);
end;

definition
  let x,y,z be set;
  func GFA1CarryStr(x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void
  strict non empty ManySortedSign equals
:: GFACIRC1:def 19
  GFA1CarryIStr(x,y,z) +* 1GateCircStr(<*[
  <*x,y*>,and2c], [<*y,z*>,and2a], [<*z,x*>,and2]*>,or3);
end;

definition
  let x,y,z be set;
  func GFA1CarryCirc(x,y,z) -> strict Boolean gate`2=den Circuit of
  GFA1CarryStr(x,y,z) equals
:: GFACIRC1:def 20
  GFA1CarryICirc(x,y,z) +* 1GateCircuit([<*x,y*>,and2c
  ],[<*y,z*>,and2a],[<*z,x*>,and2],or3);
end;

definition
  let x,y,z be set;
  func GFA1CarryOutput(x,y,z) -> Element of InnerVertices GFA1CarryStr(x,y,z)
  equals
:: GFACIRC1:def 21
  [<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3];
end;

::-------------------------------------------------------
:: GFA1 Carry : Carrier, InnerVertices and InputVertices
::-------------------------------------------------------
::-------------------------------------------------------
:: InnerVertices

theorem :: GFACIRC1:41
  for x,y,z being set holds InnerVertices GFA1CarryIStr(x,y,z) = {
  [<*x,y*>,and2c], [<*y,z*>,and2a], [<*z,x*>,and2]};

theorem :: GFACIRC1:42
  for x,y,z being set holds InnerVertices GFA1CarryStr(x,y,z) = {[
  <*x,y*>,and2c], [<*y,z*>,and2a], [<*z,x*>,and2]} \/ {GFA1CarryOutput(x,y,z)};

theorem :: GFACIRC1:43
  for x,y,z being set holds InnerVertices GFA1CarryStr(x,y,z) is Relation;

::-------------------------------------------------------
:: InputVertices

theorem :: GFACIRC1:44
  for x,y,z being set st x <> [<*y,z*>,and2a] & y <> [<*z,x*>,and2
  ] & z <> [<*x,y*>,and2c] holds InputVertices GFA1CarryIStr(x,y,z) = {x,y,z};

theorem :: GFACIRC1:45
  for x,y,z being set st x <> [<*y,z*>,and2a] & y <> [<*z,x*>,and2
  ] & z <> [<*x,y*>,and2c] holds InputVertices GFA1CarryStr(x,y,z) = {x,y,z};

theorem :: GFACIRC1:46
  for x,y,z being non pair set holds InputVertices GFA1CarryStr(x,y,z)
  is without_pairs;

::-------------------------------------------------------
:: Carrier and misc.

theorem :: GFACIRC1:47
  for x,y,z being set holds x in the carrier of GFA1CarryStr(x,y,z
) & y in the carrier of GFA1CarryStr(x,y,z) & z in the carrier of GFA1CarryStr(
x,y,z) & [<*x,y*>,and2c] in the carrier of GFA1CarryStr(x,y,z) & [<*y,z*>,and2a
  ] in the carrier of GFA1CarryStr(x,y,z) & [<*z,x*>,and2] in the carrier of
GFA1CarryStr(x,y,z) & [<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3]
  in the carrier of GFA1CarryStr(x,y,z);

theorem :: GFACIRC1:48
  for x,y,z being set holds [<*x,y*>,and2c] in InnerVertices
GFA1CarryStr(x,y,z) & [<*y,z*>,and2a] in InnerVertices GFA1CarryStr(x,y,z) & [
<*z,x*>,and2] in InnerVertices GFA1CarryStr(x,y,z) & GFA1CarryOutput(x,y,z) in
  InnerVertices GFA1CarryStr(x,y,z);

theorem :: GFACIRC1:49
  for x,y,z being set st x <> [<*y,z*>,and2a] & y <> [<*z,x*>,and2
  ] & z <> [<*x,y*>,and2c] holds x in InputVertices GFA1CarryStr(x,y,z) & y in
  InputVertices GFA1CarryStr(x,y,z) & z in InputVertices GFA1CarryStr(x,y,z);

theorem :: GFACIRC1:50
  for x,y,z being non pair set holds InputVertices GFA1CarryStr(x,
  y,z) = {x,y,z};

::----------------------------------------------------
:: GFA1 Carry : Stability of the Carry Output Circuit
::----------------------------------------------------

theorem :: GFACIRC1:51
  for x,y,z being set for s being State of GFA1CarryCirc(x,y,z)
for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3 = s.z holds (
Following s).[<*x,y*>,and2c] = a1 '&' 'not' a2 & (Following s).[<*y,z*>,and2a]
  = 'not' a2 '&' a3 & (Following s).[<*z,x*>,and2] = a3 '&' a1;

theorem :: GFACIRC1:52
  for x,y,z being set for s being State of GFA1CarryCirc(x,y,z)
for a1,a2,a3 being Element of BOOLEAN st a1 = s.[<*x,y*>,and2c] & a2 = s.[<*y,z
*>,and2a] & a3 = s.[<*z,x*>,and2] holds (Following s).GFA1CarryOutput(x,y,z) =
  a1 'or' a2 'or' a3;

theorem :: GFACIRC1:53
  for x,y,z being set st x <> [<*y,z*>,and2a] & y <> [<*z,x*>,and2
] & z <> [<*x,y*>,and2c] for s being State of GFA1CarryCirc(x,y,z) for a1,a2,a3
being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3 = s.z holds Following(s,2)
.GFA1CarryOutput(x,y,z) = (a1 '&' 'not' a2) 'or' ('not' a2 '&' a3) 'or' (a3 '&'
a1) & Following(s,2).[<*x,y*>,and2c] = a1 '&' 'not' a2 & Following(s,2).[<*y,z
  *>,and2a] = 'not' a2 '&' a3 & Following(s,2).[<*z,x*>,and2] = a3 '&' a1;

theorem :: GFACIRC1:54
  for x,y,z being set st x <> [<*y,z*>,and2a] & y <> [<*z,x*>,and2
  ] & z <> [<*x,y*>,and2c] for s being State of GFA1CarryCirc(x,y,z) holds
  Following(s,2) is stable;

::=========================================================================
::-------------------------------------------------
:: GFA1 Adder : Circuit Definition of Adder Output
::-------------------------------------------------

definition
  let x,y,z be set;
  func GFA1AdderStr(x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void
  strict non empty ManySortedSign equals
:: GFACIRC1:def 22
  2GatesCircStr(x,y,z, xor2c);
end;

definition
  let x,y,z be set;
  func GFA1AdderCirc(x,y,z) -> strict Boolean gate`2=den Circuit of
  GFA1AdderStr(x,y,z) equals
:: GFACIRC1:def 23
  2GatesCircuit(x,y,z, xor2c);
end;

definition
  let x,y,z be set;
  func GFA1AdderOutput(x,y,z) -> Element of InnerVertices GFA1AdderStr(x,y,z)
  equals
:: GFACIRC1:def 24
  2GatesCircOutput(x,y,z, xor2c);
end;

::-------------------------------------------------------
:: GFA1 Adder : Carrier, InnerVertices and InputVertices
::-------------------------------------------------------
::-------------------------------------------------------
:: InnerVertices

theorem :: GFACIRC1:55
  for x,y,z being set holds InnerVertices GFA1AdderStr(x,y,z) = {[
  <*x,y*>,xor2c]} \/ {GFA1AdderOutput(x,y,z)};

::-------------------------------------------------------
:: Carrier and misc.

theorem :: GFACIRC1:56
  for x,y,z being set holds x in the carrier of GFA1AdderStr(x,y,z) & y
in the carrier of GFA1AdderStr(x,y,z) & z in the carrier of GFA1AdderStr(x,y,z)
& [<*x,y*>,xor2c] in the carrier of GFA1AdderStr(x,y,z) & [<*[<*x,y*>,xor2c], z
  *>, xor2c] in the carrier of GFA1AdderStr(x,y,z);

theorem :: GFACIRC1:57
  for x,y,z being set holds [<*x,y*>,xor2c] in InnerVertices
GFA1AdderStr(x,y,z) & GFA1AdderOutput(x,y,z) in InnerVertices GFA1AdderStr(x,y,
  z);

theorem :: GFACIRC1:58
  for x,y,z being set st z <> [<*x,y*>, xor2c] holds x in
InputVertices GFA1AdderStr(x,y,z) & y in InputVertices GFA1AdderStr(x,y,z) & z
  in InputVertices GFA1AdderStr(x,y,z);

::----------------------------------------------------
:: GFA1 Adder : Stability of the Adder Output Circuit
::----------------------------------------------------

theorem :: GFACIRC1:59
  for x,y,z being set st z <> [<*x,y*>, xor2c] for s being State
of GFA1AdderCirc(x,y,z) for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2
  = s.y & a3 = s.z holds (Following s).[<*x,y*>,xor2c] = a1 'xor' 'not' a2 & (
  Following s).x = a1 & (Following s).y = a2 & (Following s).z = a3;

theorem :: GFACIRC1:60
  for x,y,z being set st z <> [<*x,y*>, xor2c] for s being State
of GFA1AdderCirc(x,y,z) for a1a2,a1,a2,a3 being Element of BOOLEAN st a1a2 = s.
  [<*x,y*>,xor2c] & a3 = s.z holds (Following s).GFA1AdderOutput(x,y,z) = a1a2
  'xor' 'not' a3;

theorem :: GFACIRC1:61
  for x,y,z being set st z <> [<*x,y*>, xor2c] for s being State
of GFA1AdderCirc(x,y,z) for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2
  = s.y & a3 = s.z holds Following(s,2).GFA1AdderOutput(x,y,z) = a1 'xor' 'not'
  a2 'xor' 'not' a3 & Following(s,2).[<*x,y*>,xor2c] = a1 'xor' 'not' a2 &
  Following(s,2).x = a1 & Following(s,2).y = a2 & Following(s,2).z = a3;

theorem :: GFACIRC1:62
  for x,y,z being set st z <> [<*x,y*>, xor2c] for s being State
of GFA1AdderCirc(x,y,z) for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2
= s.y & a3 = s.z holds Following(s,2).GFA1AdderOutput(x,y,z) = 'not' (a1 'xor'
  'not' a2 'xor' a3);

::=====================================================================
::---------------------------------------------------
:: GFA1 : Circuit Definition of GFA Combined Circuit
::---------------------------------------------------

definition
  let x,y,z be set;
  func BitGFA1Str(x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void
  strict non empty ManySortedSign equals
:: GFACIRC1:def 25
  GFA1AdderStr(x,y,z) +* GFA1CarryStr(x,y,
  z);
end;

definition
  let x,y,z be set;
  func BitGFA1Circ(x,y,z) -> strict Boolean gate`2=den Circuit of BitGFA1Str(x
  ,y,z) equals
:: GFACIRC1:def 26
  GFA1AdderCirc(x,y,z) +* GFA1CarryCirc(x,y,z);
end;

::----------------------------------------------------------
:: GFA1 Combined : Carrier, InnerVertices and InputVertices
::----------------------------------------------------------
::-------------------------------------------------------
:: InnerVertices

theorem :: GFACIRC1:63
  for x,y,z being set holds InnerVertices BitGFA1Str(x,y,z) = {[<*
x,y*>,xor2c]} \/ {GFA1AdderOutput(x,y,z)} \/ {[<*x,y*>,and2c], [<*y,z*>,and2a],
  [<*z,x*>,and2]} \/ {GFA1CarryOutput(x,y,z)};

theorem :: GFACIRC1:64
  for x,y,z being set holds InnerVertices BitGFA1Str(x,y,z) is Relation;

::-------------------------------------------------------
:: InputVertices

theorem :: GFACIRC1:65
  for x,y,z being set st z <> [<*x,y*>,xor2c] & x <> [<*y,z*>,
  and2a] & y <> [<*z,x*>,and2] & z <> [<*x,y*>,and2c] holds InputVertices
  BitGFA1Str(x,y,z) = {x,y,z};

theorem :: GFACIRC1:66
  for x,y,z being non pair set holds InputVertices BitGFA1Str(x,y, z) = {x,y,z}
;

theorem :: GFACIRC1:67
  for x,y,z being non pair set holds InputVertices BitGFA1Str(x,y,z) is
  without_pairs;

::-------------------------------------------------------
:: Carrier and misc.

theorem :: GFACIRC1:68
  for x,y,z being set holds x in the carrier of BitGFA1Str(x,y,z) & y in
the carrier of BitGFA1Str(x,y,z) & z in the carrier of BitGFA1Str(x,y,z) & [<*x
,y*>,xor2c] in the carrier of BitGFA1Str(x,y,z) & [<*[<*x,y*>,xor2c],z*>,xor2c]
  in the carrier of BitGFA1Str(x,y,z) & [<*x,y*>,and2c] in the carrier of
BitGFA1Str(x,y,z) & [<*y,z*>,and2a] in the carrier of BitGFA1Str(x,y,z) & [<*z,
  x*>,and2] in the carrier of BitGFA1Str(x,y,z) & [<*[<*x,y*>,and2c],[<*y,z*>,
  and2a],[<*z,x*>,and2]*>,or3] in the carrier of BitGFA1Str(x,y,z);

theorem :: GFACIRC1:69
  for x,y,z being set holds [<*x,y*>,xor2c] in InnerVertices
BitGFA1Str(x,y,z) & GFA1AdderOutput(x,y,z) in InnerVertices BitGFA1Str(x,y,z) &
  [<*x,y*>,and2c] in InnerVertices BitGFA1Str(x,y,z) & [<*y,z*>,and2a] in
InnerVertices BitGFA1Str(x,y,z) & [<*z,x*>,and2] in InnerVertices BitGFA1Str(x,
  y,z) & GFA1CarryOutput(x,y,z) in InnerVertices BitGFA1Str(x,y,z);

theorem :: GFACIRC1:70
  for x,y,z being set st z <> [<*x,y*>,xor2c] & x <> [<*y,z*>,and2a] & y
<> [<*z,x*>,and2] & z <> [<*x,y*>,and2c] holds x in InputVertices BitGFA1Str(x,
y,z) & y in InputVertices BitGFA1Str(x,y,z) & z in InputVertices BitGFA1Str(x,y
  ,z);

::------------------------------------------------------------------
:: GFA1 : Carry and Adder Output Definition of GFA Combined Circuit
::------------------------------------------------------------------

definition
  let x,y,z be set;
  func BitGFA1CarryOutput(x,y,z) -> Element of InnerVertices BitGFA1Str(x,y,z)
  equals
:: GFACIRC1:def 27
  [<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3];
end;

definition
  let x,y,z be set;
  func BitGFA1AdderOutput(x,y,z) -> Element of InnerVertices BitGFA1Str(x,y,z)
  equals
:: GFACIRC1:def 28
  2GatesCircOutput(x,y,z, xor2c);
end;

::-------------------------------------------------------------
:: GFA1 Combined : Stability of the Adder/Carry Output Circuit
::-------------------------------------------------------------

theorem :: GFACIRC1:71
  for x,y,z being set st z <> [<*x,y*>,xor2c] & x <> [<*y,z*>,and2a] & y
<> [<*z,x*>,and2] & z <> [<*x,y*>,and2c] for s being State of BitGFA1Circ(x,y,z
) for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3 = s.z holds
  Following(s,2).GFA1AdderOutput(x,y,z) = 'not' (a1 'xor' 'not' a2 'xor' a3) &
Following(s,2).GFA1CarryOutput(x,y,z) = (a1 '&' 'not' a2) 'or' ('not' a2 '&' a3
  ) 'or' (a3 '&' a1);

theorem :: GFACIRC1:72
  for x,y,z being set st z <> [<*x,y*>,xor2c] & x <> [<*y,z*>,and2a] & y
<> [<*z,x*>,and2] & z <> [<*x,y*>,and2c] for s being State of BitGFA1Circ(x,y,z
  ) holds Following(s,2) is stable;

::========================================================================
:: Generalized Full Adder (GFA) Circuit (TYPE-2)
::========================================================================

begin :: Generalized Full Adder (GFA) Circuit (TYPE-2)
::========================================================================
:: << GFA TYPE-2 >>
::------------------------------------------------------------------------
::   Name     : Generalized Full Adder Type-2 (GFA2)
::   Function : - x + y - z = - 2 * c + s
::
::   Logic Symbol :     -x      y      Combined : GFA2CarryIStr(x,y,z)
::                       |     /                  GFA2CarryStr(x,y,z)
::                       |    /                   GFA2AdderStr(x,y,z)
::                   +---O---*                  --->
::                   |  GFA  O---- -z             BitGFA2Str(x,y,z)
::                   | TYPE2 |
::                   O---*---+          Outputs : BitGFA2CarryOutput(x,y,z)
::                  /    |                        BitGFA2AdderOutput(x,y,z)
::                 /     |
::               -c      s          Calculation : Following(s,2) is stable.
::=========================================================================
::-------------------------------------------------
:: GFA2 Carry : Circuit Definition of Carry Output
::-------------------------------------------------

definition
  let x,y,z be set;
  func GFA2CarryIStr(x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void
  strict non empty ManySortedSign equals
:: GFACIRC1:def 29
  1GateCircStr(<*x,y*>,and2a) +*
  1GateCircStr(<*y,z*>,and2c) +* 1GateCircStr(<*z,x*>,nor2);
end;

definition
  let x,y,z be set;
  func GFA2CarryICirc(x,y,z) -> strict Boolean gate`2=den Circuit of
  GFA2CarryIStr(x,y,z) equals
:: GFACIRC1:def 30
  1GateCircuit(x,y,and2a) +* 1GateCircuit(y,z,and2c)
  +* 1GateCircuit(z,x,nor2);
end;

definition
  let x,y,z be set;
  func GFA2CarryStr(x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void
  strict non empty ManySortedSign equals
:: GFACIRC1:def 31
  GFA2CarryIStr(x,y,z) +* 1GateCircStr(<*[
  <*x,y*>,and2a], [<*y,z*>,and2c], [<*z,x*>,nor2]*>,nor3);
end;

definition
  let x,y,z be set;
  func GFA2CarryCirc(x,y,z) -> strict Boolean gate`2=den Circuit of
  GFA2CarryStr(x,y,z) equals
:: GFACIRC1:def 32
  GFA2CarryICirc(x,y,z) +* 1GateCircuit([<*x,y*>,and2a
  ],[<*y,z*>,and2c],[<*z,x*>,nor2],nor3);
end;

definition
  let x,y,z be set;
  func GFA2CarryOutput(x,y,z) -> Element of InnerVertices GFA2CarryStr(x,y,z)
  equals
:: GFACIRC1:def 33
  [<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2]*>,nor3];
end;

::-------------------------------------------------------
:: GFA2 Carry : Carrier, InnerVertices and InputVertices
::-------------------------------------------------------
::-------------------------------------------------------
:: InnerVertices

theorem :: GFACIRC1:73
  for x,y,z being set holds InnerVertices GFA2CarryIStr(x,y,z) = {
  [<*x,y*>,and2a], [<*y,z*>,and2c], [<*z,x*>,nor2]};

theorem :: GFACIRC1:74
  for x,y,z being set holds InnerVertices GFA2CarryStr(x,y,z) = {[
  <*x,y*>,and2a], [<*y,z*>,and2c], [<*z,x*>,nor2]} \/ {GFA2CarryOutput(x,y,z)};

theorem :: GFACIRC1:75
  for x,y,z being set holds InnerVertices GFA2CarryStr(x,y,z) is Relation;

::-------------------------------------------------------
:: InputVertices

theorem :: GFACIRC1:76
  for x,y,z being set st x <> [<*y,z*>,and2c] & y <> [<*z,x*>,
nor2] & z <> [<*x,y*>,and2a] holds InputVertices GFA2CarryIStr(x,y,z) = {x,y,z
  };

theorem :: GFACIRC1:77
  for x,y,z being set st x <> [<*y,z*>,and2c] & y <> [<*z,x*>,
nor2] & z <> [<*x,y*>,and2a] holds InputVertices GFA2CarryStr(x,y,z) = {x,y,z};

theorem :: GFACIRC1:78
  for x,y,z being non pair set holds InputVertices GFA2CarryStr(x,y,z)
  is without_pairs;

::-------------------------------------------------------
:: Carrier and misc.

theorem :: GFACIRC1:79
  for x,y,z being set holds x in the carrier of GFA2CarryStr(x,y,z
) & y in the carrier of GFA2CarryStr(x,y,z) & z in the carrier of GFA2CarryStr(
x,y,z) & [<*x,y*>,and2a] in the carrier of GFA2CarryStr(x,y,z) & [<*y,z*>,and2c
  ] in the carrier of GFA2CarryStr(x,y,z) & [<*z,x*>,nor2] in the carrier of
GFA2CarryStr(x,y,z) & [<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2]*>,nor3
  ] in the carrier of GFA2CarryStr(x,y,z);

theorem :: GFACIRC1:80
  for x,y,z being set holds [<*x,y*>,and2a] in InnerVertices
GFA2CarryStr(x,y,z) & [<*y,z*>,and2c] in InnerVertices GFA2CarryStr(x,y,z) & [
<*z,x*>,nor2] in InnerVertices GFA2CarryStr(x,y,z) & GFA2CarryOutput(x,y,z) in
  InnerVertices GFA2CarryStr(x,y,z);

theorem :: GFACIRC1:81
  for x,y,z being set st x <> [<*y,z*>,and2c] & y <> [<*z,x*>,
nor2] & z <> [<*x,y*>,and2a] holds x in InputVertices GFA2CarryStr(x,y,z) & y
  in InputVertices GFA2CarryStr(x,y,z) & z in InputVertices GFA2CarryStr(x,y,z)
;

theorem :: GFACIRC1:82
  for x,y,z being non pair set holds InputVertices GFA2CarryStr(x,
  y,z) = {x,y,z};

::----------------------------------------------------
:: GFA2 Carry : Stability of the Carry Output Circuit
::----------------------------------------------------

theorem :: GFACIRC1:83
  for x,y,z being set for s being State of GFA2CarryCirc(x,y,z)
for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3 = s.z holds (
Following s).[<*x,y*>,and2a] = 'not' a1 '&' a2 & (Following s).[<*y,z*>,and2c]
  = a2 '&' 'not' a3 & (Following s).[<*z,x*>,nor2] = 'not' a3 '&' 'not' a1;

theorem :: GFACIRC1:84
  for x,y,z being set for s being State of GFA2CarryCirc(x,y,z)
for a1,a2,a3 being Element of BOOLEAN st a1 = s.[<*x,y*>,and2a] & a2 = s.[<*y,z
*>,and2c] & a3 = s.[<*z,x*>,nor2] holds (Following s).GFA2CarryOutput(x,y,z) =
  'not' (a1 'or' a2 'or' a3);

theorem :: GFACIRC1:85
  for x,y,z being set st x <> [<*y,z*>,and2c] & y <> [<*z,x*>,
nor2] & z <> [<*x,y*>,and2a] for s being State of GFA2CarryCirc(x,y,z) for a1,
  a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3 = s.z holds
  Following(s,2).GFA2CarryOutput(x,y,z) = 'not' (('not' a1 '&' a2) 'or' (a2 '&'
  'not' a3) 'or' ('not' a3 '&' 'not' a1)) & Following(s,2).[<*x,y*>,and2a] =
'not' a1 '&' a2 & Following(s,2).[<*y,z*>,and2c] = a2 '&' 'not' a3 & Following(
  s,2).[<*z,x*>,nor2] = 'not' a3 '&' 'not' a1;

theorem :: GFACIRC1:86
  for x,y,z being set st x <> [<*y,z*>,and2c] & y <> [<*z,x*>,
  nor2] & z <> [<*x,y*>,and2a] for s being State of GFA2CarryCirc(x,y,z) holds
  Following(s,2) is stable;

::=========================================================================
::-------------------------------------------------
:: GFA2 Adder : Circuit Definition of Adder Output
::-------------------------------------------------

definition
  let x,y,z be set;
  func GFA2AdderStr(x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void
  strict non empty ManySortedSign equals
:: GFACIRC1:def 34
  2GatesCircStr(x,y,z, xor2c);
end;

definition
  let x,y,z be set;
  func GFA2AdderCirc(x,y,z) -> strict Boolean gate`2=den Circuit of
  GFA2AdderStr(x,y,z) equals
:: GFACIRC1:def 35
  2GatesCircuit(x,y,z, xor2c);
end;

definition
  let x,y,z be set;
  func GFA2AdderOutput(x,y,z) -> Element of InnerVertices GFA2AdderStr(x,y,z)
  equals
:: GFACIRC1:def 36
  2GatesCircOutput(x,y,z, xor2c);
end;

::-------------------------------------------------------
:: GFA2 Adder : Carrier, InnerVertices and InputVertices
::-------------------------------------------------------
::-------------------------------------------------------
:: InnerVertices

theorem :: GFACIRC1:87
  for x,y,z being set holds InnerVertices GFA2AdderStr(x,y,z) = {
  [<*x,y*>,xor2c]} \/ {GFA2AdderOutput(x,y,z)};

::-------------------------------------------------------
:: Carrier and misc.

theorem :: GFACIRC1:88
  for x,y,z being set holds x in the carrier of GFA2AdderStr(x,y,z) & y
in the carrier of GFA2AdderStr(x,y,z) & z in the carrier of GFA2AdderStr(x,y,z)
& [<*x,y*>,xor2c] in the carrier of GFA2AdderStr(x,y,z) & [<*[<*x,y*>,xor2c], z
  *>, xor2c] in the carrier of GFA2AdderStr(x,y,z);

theorem :: GFACIRC1:89
  for x,y,z being set holds [<*x,y*>,xor2c] in InnerVertices
GFA2AdderStr(x,y,z) & GFA2AdderOutput(x,y,z) in InnerVertices GFA2AdderStr(x,y,
  z);

theorem :: GFACIRC1:90
  for x,y,z being set st z <> [<*x,y*>, xor2c] holds x in InputVertices
  GFA2AdderStr(x,y,z) & y in InputVertices GFA2AdderStr(x,y,z) & z in
  InputVertices GFA2AdderStr(x,y,z);

::----------------------------------------------------
:: GFA2 Adder : Stability of the Adder Output Circuit
::----------------------------------------------------

theorem :: GFACIRC1:91
  for x,y,z being set st z <> [<*x,y*>, xor2c] for s being State of
GFA2AdderCirc(x,y,z) for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s
  .y & a3 = s.z holds (Following s).[<*x,y*>,xor2c] = a1 'xor' 'not' a2 & (
  Following s).x = a1 & (Following s).y = a2 & (Following s).z = a3;

theorem :: GFACIRC1:92
  for x,y,z being set st z <> [<*x,y*>, xor2c] for s being State of
GFA2AdderCirc(x,y,z) for a1a2,a1,a2,a3 being Element of BOOLEAN st a1a2 = s.[<*
  x,y*>,xor2c] & a1 = s.x & a2 = s.y & a3 = s.z holds (Following s).
  GFA2AdderOutput(x,y,z) = a1a2 'xor' 'not' a3;

theorem :: GFACIRC1:93
  for x,y,z being set st z <> [<*x,y*>, xor2c] for s being State
of GFA2AdderCirc(x,y,z) for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2
  = s.y & a3 = s.z holds Following(s,2).GFA2AdderOutput(x,y,z) = a1 'xor' 'not'
  a2 'xor' 'not' a3 & Following(s,2).[<*x,y*>,xor2c] = a1 'xor' 'not' a2 &
  Following(s,2).x = a1 & Following(s,2).y = a2 & Following(s,2).z = a3;

theorem :: GFACIRC1:94
  for x,y,z being set st z <> [<*x,y*>, xor2c] for s being State
of GFA2AdderCirc(x,y,z) for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2
  = s.y & a3 = s.z holds Following(s,2).GFA2AdderOutput(x,y,z) = 'not' a1 'xor'
  a2 'xor' 'not' a3;

::=====================================================================
::---------------------------------------------------
:: GFA2 : Circuit Definition of GFA Combined Circuit
::---------------------------------------------------

definition
  let x,y,z be set;
  func BitGFA2Str(x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void
  strict non empty ManySortedSign equals
:: GFACIRC1:def 37
  GFA2AdderStr(x,y,z) +* GFA2CarryStr(x,y,
  z);
end;

definition
  let x,y,z be set;
  func BitGFA2Circ(x,y,z) -> strict Boolean gate`2=den Circuit of BitGFA2Str(x
  ,y,z) equals
:: GFACIRC1:def 38
  GFA2AdderCirc(x,y,z) +* GFA2CarryCirc(x,y,z);
end;

::----------------------------------------------------------
:: GFA2 Combined : Carrier, InnerVertices and InputVertices
::----------------------------------------------------------
::-------------------------------------------------------
:: InnerVertices

theorem :: GFACIRC1:95
  for x,y,z being set holds InnerVertices BitGFA2Str(x,y,z) = {[
<*x,y*>,xor2c]} \/ {GFA2AdderOutput(x,y,z)} \/ {[<*x,y*>,and2a], [<*y,z*>,and2c
  ], [<*z,x*>,nor2]} \/ {GFA2CarryOutput(x,y,z)};

theorem :: GFACIRC1:96
  for x,y,z being set holds InnerVertices BitGFA2Str(x,y,z) is Relation;

::-------------------------------------------------------
:: InputVertices

theorem :: GFACIRC1:97
  for x,y,z being set st z <> [<*x,y*>,xor2c] & x <> [<*y,z*>,
  and2c] & y <> [<*z,x*>,nor2] & z <> [<*x,y*>,and2a] holds InputVertices
  BitGFA2Str(x,y,z) = {x,y,z};

theorem :: GFACIRC1:98
  for x,y,z being non pair set holds InputVertices BitGFA2Str(x,y ,z) = {x,y,z}
;

theorem :: GFACIRC1:99
  for x,y,z being non pair set holds InputVertices BitGFA2Str(x,y,z) is
  without_pairs;

::-------------------------------------------------------
:: Carrier and misc.

theorem :: GFACIRC1:100
  for x,y,z being set holds x in the carrier of BitGFA2Str(x,y,z) & y in
the carrier of BitGFA2Str(x,y,z) & z in the carrier of BitGFA2Str(x,y,z) & [<*x
,y*>,xor2c] in the carrier of BitGFA2Str(x,y,z) & [<*[<*x,y*>,xor2c],z*>,xor2c]
  in the carrier of BitGFA2Str(x,y,z) & [<*x,y*>,and2a] in the carrier of
BitGFA2Str(x,y,z) & [<*y,z*>,and2c] in the carrier of BitGFA2Str(x,y,z) & [<*z,
  x*>,nor2] in the carrier of BitGFA2Str(x,y,z) & [<*[<*x,y*>,and2a],[<*y,z*>,
  and2c],[<*z,x*>,nor2]*>,nor3] in the carrier of BitGFA2Str(x,y,z);

theorem :: GFACIRC1:101
  for x,y,z being set holds [<*x,y*>,xor2c] in InnerVertices
BitGFA2Str(x,y,z) & GFA2AdderOutput(x,y,z) in InnerVertices BitGFA2Str(x,y,z) &
  [<*x,y*>,and2a] in InnerVertices BitGFA2Str(x,y,z) & [<*y,z*>,and2c] in
InnerVertices BitGFA2Str(x,y,z) & [<*z,x*>,nor2] in InnerVertices BitGFA2Str(x
  ,y,z) & GFA2CarryOutput(x,y,z) in InnerVertices BitGFA2Str(x,y,z);

theorem :: GFACIRC1:102
  for x,y,z being set st z <> [<*x,y*>,xor2c] & x <> [<*y,z*>,and2c] & y
<> [<*z,x*>,nor2] & z <> [<*x,y*>,and2a] holds x in InputVertices BitGFA2Str(x
,y,z) & y in InputVertices BitGFA2Str(x,y,z) & z in InputVertices BitGFA2Str(x,
  y,z);

::------------------------------------------------------------------
:: GFA2 : Carry and Adder Output Definition of GFA Combined Circuit
::------------------------------------------------------------------

definition
  let x,y,z be set;
  func BitGFA2CarryOutput(x,y,z) -> Element of InnerVertices BitGFA2Str(x,y,z)
  equals
:: GFACIRC1:def 39
  [<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2]*>,nor3];
end;

definition
  let x,y,z be set;
  func BitGFA2AdderOutput(x,y,z) -> Element of InnerVertices BitGFA2Str(x,y,z)
  equals
:: GFACIRC1:def 40
  2GatesCircOutput(x,y,z, xor2c);
end;

::-------------------------------------------------------------
:: GFA2 Combined : Stability of the Adder/Carry Output Circuit
::-------------------------------------------------------------

theorem :: GFACIRC1:103
  for x,y,z being set st z <> [<*x,y*>,xor2c] & x <> [<*y,z*>,and2c] & y
<> [<*z,x*>,nor2] & z <> [<*x,y*>,and2a] for s being State of BitGFA2Circ(x,y,
  z) for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3 = s.z
holds Following(s,2).GFA2AdderOutput(x,y,z) = 'not' a1 'xor' a2 'xor' 'not' a3
& Following(s,2).GFA2CarryOutput(x,y,z) = 'not' (('not' a1 '&' a2) 'or' (a2 '&'
  'not' a3) 'or' ('not' a3 '&' 'not' a1));

theorem :: GFACIRC1:104
  for x,y,z being set st z <> [<*x,y*>,xor2c] & x <> [<*y,z*>,and2c] & y
<> [<*z,x*>,nor2] & z <> [<*x,y*>,and2a] for s being State of BitGFA2Circ(x,y,
  z) holds Following(s,2) is stable;

::========================================================================
:: Generalized Full Adder (GFA) Circuit (TYPE-3)
::========================================================================

begin :: Generalized Full Adder (GFA) Circuit (TYPE-3)
::========================================================================
:: << GFA TYPE-3 >>
::------------------------------------------------------------------------
::   Name     : Generalized Full Adder Type-3 (GFA3)
::   Function : - x - y - z = - 2 * c - s
::
::   Logic Symbol :     -x     -y      Combined : GFA3CarryIStr(x,y,z)
::                       |     /                  GFA3CarryStr(x,y,z)
::                       |    /                   GFA3AdderStr(x,y,z)
::                   +---O---O                  --->
::                   |  GFA  O---- -z             BitGFA3Str(x,y,z)
::                   | TYPE3 |
::                   O---O---+          Outputs : BitGFA3CarryOutput(x,y,z)
::                  /    |                        BitGFA3AdderOutput(x,y,z)
::                 /     |
::               -c     -s          Calculation : Following(s,2) is stable.
::=========================================================================
::-------------------------------------------------
:: GFA3 Carry : Circuit Definition of Carry Output
::-------------------------------------------------

definition
  let x,y,z be set;
  func GFA3CarryIStr(x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void
  strict non empty ManySortedSign equals
:: GFACIRC1:def 41
  1GateCircStr(<*x,y*>,nor2) +*
  1GateCircStr(<*y,z*>,nor2) +* 1GateCircStr(<*z,x*>,nor2);
end;

definition
  let x,y,z be set;
  func GFA3CarryICirc(x,y,z) -> strict Boolean gate`2=den Circuit of
  GFA3CarryIStr(x,y,z) equals
:: GFACIRC1:def 42
  1GateCircuit(x,y,nor2) +* 1GateCircuit(y,z,nor2)
  +* 1GateCircuit(z,x,nor2);
end;

definition
  let x,y,z be set;
  func GFA3CarryStr(x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void
  strict non empty ManySortedSign equals
:: GFACIRC1:def 43
  GFA3CarryIStr(x,y,z) +* 1GateCircStr(<*[
  <*x,y*>,nor2], [<*y,z*>,nor2], [<*z,x*>,nor2]*>,nor3);
end;

definition
  let x,y,z be set;
  func GFA3CarryCirc(x,y,z) -> strict Boolean gate`2=den Circuit of
  GFA3CarryStr(x,y,z) equals
:: GFACIRC1:def 44
  GFA3CarryICirc(x,y,z) +* 1GateCircuit([<*x,y*>,nor2
  ],[<*y,z*>,nor2],[<*z,x*>,nor2],nor3);
end;

definition
  let x,y,z be set;
  func GFA3CarryOutput(x,y,z) -> Element of InnerVertices GFA3CarryStr(x,y,z)
  equals
:: GFACIRC1:def 45
  [<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,nor3];
end;

::-------------------------------------------------------
:: GFA3 Carry : Carrier, InnerVertices and InputVertices
::-------------------------------------------------------
::-------------------------------------------------------
:: InnerVertices

theorem :: GFACIRC1:105
  for x,y,z being set holds InnerVertices GFA3CarryIStr(x,y,z) =
  {[<*x,y*>,nor2], [<*y,z*>,nor2], [<*z,x*>,nor2]};

theorem :: GFACIRC1:106
  for x,y,z being set holds InnerVertices GFA3CarryStr(x,y,z) = {
[<*x,y*>,nor2], [<*y,z*>,nor2], [<*z,x*>,nor2]} \/ {GFA3CarryOutput(x,y,z)};

theorem :: GFACIRC1:107
  for x,y,z being set holds InnerVertices GFA3CarryStr(x,y,z) is Relation;

::-------------------------------------------------------
:: InputVertices

theorem :: GFACIRC1:108
  for x,y,z being set st x <> [<*y,z*>,nor2] & y <> [<*z,x*>,
nor2] & z <> [<*x,y*>,nor2] holds InputVertices GFA3CarryIStr(x,y,z) = {x,y,z
  };

theorem :: GFACIRC1:109
  for x,y,z being set st x <> [<*y,z*>,nor2] & y <> [<*z,x*>,
nor2] & z <> [<*x,y*>,nor2] holds InputVertices GFA3CarryStr(x,y,z) = {x,y,z};

theorem :: GFACIRC1:110
  for x,y,z being non pair set holds InputVertices GFA3CarryStr(x,y,z)
  is without_pairs;

::-------------------------------------------------------
:: Carrier and misc.

theorem :: GFACIRC1:111
  for x,y,z being set holds x in the carrier of GFA3CarryStr(x,y,
z) & y in the carrier of GFA3CarryStr(x,y,z) & z in the carrier of GFA3CarryStr
  (x,y,z) & [<*x,y*>,nor2] in the carrier of GFA3CarryStr(x,y,z) & [<*y,z*>,
  nor2] in the carrier of GFA3CarryStr(x,y,z) & [<*z,x*>,nor2] in the carrier
of GFA3CarryStr(x,y,z) & [<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,
  nor3] in the carrier of GFA3CarryStr(x,y,z);

theorem :: GFACIRC1:112
  for x,y,z being set holds [<*x,y*>,nor2] in InnerVertices
GFA3CarryStr(x,y,z) & [<*y,z*>,nor2] in InnerVertices GFA3CarryStr(x,y,z) & [
<*z,x*>,nor2] in InnerVertices GFA3CarryStr(x,y,z) & GFA3CarryOutput(x,y,z) in
  InnerVertices GFA3CarryStr(x,y,z);

theorem :: GFACIRC1:113
  for x,y,z being set st x <> [<*y,z*>,nor2] & y <> [<*z,x*>,
nor2] & z <> [<*x,y*>,nor2] holds x in InputVertices GFA3CarryStr(x,y,z) & y
  in InputVertices GFA3CarryStr(x,y,z) & z in InputVertices GFA3CarryStr(x,y,z)
;

theorem :: GFACIRC1:114
  for x,y,z being non pair set holds InputVertices GFA3CarryStr(x
  ,y,z) = {x,y,z};

::----------------------------------------------------
:: GFA3 Carry : Stability of the Carry Output Circuit
::----------------------------------------------------

theorem :: GFACIRC1:115
  for x,y,z being set for s being State of GFA3CarryCirc(x,y,z)
for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3 = s.z holds (
Following s).[<*x,y*>,nor2] = 'not' a1 '&' 'not' a2 & (Following s).[<*y,z*>,
  nor2] = 'not' a2 '&' 'not' a3 & (Following s).[<*z,x*>,nor2] = 'not' a3 '&'
  'not' a1;

theorem :: GFACIRC1:116
  for x,y,z being set for s being State of GFA3CarryCirc(x,y,z)
for a1,a2,a3 being Element of BOOLEAN st a1 = s.[<*x,y*>,nor2] & a2 = s.[<*y,z
*>,nor2] & a3 = s.[<*z,x*>,nor2] holds (Following s).GFA3CarryOutput(x,y,z) =
  'not' (a1 'or' a2 'or' a3);

theorem :: GFACIRC1:117
  for x,y,z being set st x <> [<*y,z*>,nor2] & y <> [<*z,x*>,
nor2] & z <> [<*x,y*>,nor2] for s being State of GFA3CarryCirc(x,y,z) for a1,
  a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3 = s.z holds
  Following(s,2).GFA3CarryOutput(x,y,z) = 'not' (('not' a1 '&' 'not' a2) 'or' (
'not' a2 '&' 'not' a3) 'or' ('not' a3 '&' 'not' a1)) & Following(s,2).[<*x,y*>,
nor2] = 'not' a1 '&' 'not' a2 & Following(s,2).[<*y,z*>,nor2] = 'not' a2 '&'
  'not' a3 & Following(s,2).[<*z,x*>,nor2] = 'not' a3 '&' 'not' a1;

theorem :: GFACIRC1:118
  for x,y,z being set st x <> [<*y,z*>,nor2] & y <> [<*z,x*>,
  nor2] & z <> [<*x,y*>,nor2] for s being State of GFA3CarryCirc(x,y,z) holds
  Following(s,2) is stable;

::=========================================================================
::-------------------------------------------------
:: GFA3 Adder : Circuit Definition of Adder Output
::-------------------------------------------------

definition
  let x,y,z be set;
  func GFA3AdderStr(x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void
  strict non empty ManySortedSign equals
:: GFACIRC1:def 46
  2GatesCircStr(x,y,z, xor2);
end;

definition
  let x,y,z be set;
  func GFA3AdderCirc(x,y,z) -> strict Boolean gate`2=den Circuit of
  GFA3AdderStr(x,y,z) equals
:: GFACIRC1:def 47
  2GatesCircuit(x,y,z, xor2);
end;

definition
  let x,y,z be set;
  func GFA3AdderOutput(x,y,z) -> Element of InnerVertices GFA3AdderStr(x,y,z)
  equals
:: GFACIRC1:def 48
  2GatesCircOutput(x,y,z, xor2);
end;

::-------------------------------------------------------
:: GFA3 Adder : Carrier, InnerVertices and InputVertices
::-------------------------------------------------------
::-------------------------------------------------------
:: InnerVertices

theorem :: GFACIRC1:119
  for x,y,z being set holds InnerVertices GFA3AdderStr(x,y,z) = {
  [<*x,y*>,xor2]} \/ {GFA3AdderOutput(x,y,z)};

::-------------------------------------------------------
:: Carrier and misc.

theorem :: GFACIRC1:120
  for x,y,z being set holds x in the carrier of GFA3AdderStr(x,y,z) & y
in the carrier of GFA3AdderStr(x,y,z) & z in the carrier of GFA3AdderStr(x,y,z)
& [<*x,y*>,xor2] in the carrier of GFA3AdderStr(x,y,z) & [<*[<*x,y*>,xor2], z*>
  , xor2] in the carrier of GFA3AdderStr(x,y,z);

theorem :: GFACIRC1:121
  for x,y,z being set holds [<*x,y*>,xor2] in InnerVertices GFA3AdderStr
  (x,y,z) & GFA3AdderOutput(x,y,z) in InnerVertices GFA3AdderStr(x,y,z);

theorem :: GFACIRC1:122
  for x,y,z being set st z <> [<*x,y*>, xor2] holds x in InputVertices
  GFA3AdderStr(x,y,z) & y in InputVertices GFA3AdderStr(x,y,z) & z in
  InputVertices GFA3AdderStr(x,y,z);

::----------------------------------------------------
:: GFA3 Adder : Stability of the Adder Output Circuit
::----------------------------------------------------

theorem :: GFACIRC1:123
  for x,y,z being set st z <> [<*x,y*>, xor2] for s being State of
GFA3AdderCirc(x,y,z) for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s
.y & a3 = s.z holds (Following s).[<*x,y*>,xor2] = a1 'xor' a2 & (Following s).
  x = a1 & (Following s).y = a2 & (Following s).z = a3;

theorem :: GFACIRC1:124
  for x,y,z being set st z <> [<*x,y*>, xor2] for s being State of
GFA3AdderCirc(x,y,z) for a1a2,a1,a2,a3 being Element of BOOLEAN st a1a2 = s.[<*
  x,y*>,xor2] & a1 = s.x & a2 = s.y & a3 = s.z holds (Following s).
  GFA3AdderOutput(x,y,z) = a1a2 'xor' a3;

theorem :: GFACIRC1:125
  for x,y,z being set st z <> [<*x,y*>, xor2] for s being State
of GFA3AdderCirc(x,y,z) for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2
  = s.y & a3 = s.z holds Following(s,2).GFA3AdderOutput(x,y,z) = a1 'xor' a2
'xor' a3 & Following(s,2).[<*x,y*>,xor2] = a1 'xor' a2 & Following(s,2).x = a1
  & Following(s,2).y = a2 & Following(s,2).z = a3;

theorem :: GFACIRC1:126
  for x,y,z being set st z <> [<*x,y*>, xor2] for s being State
of GFA3AdderCirc(x,y,z) for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2
= s.y & a3 = s.z holds Following(s,2).GFA3AdderOutput(x,y,z) = 'not' ('not' a1
  'xor' 'not' a2 'xor' 'not' a3);

::=====================================================================
::---------------------------------------------------
:: GFA3 : Circuit Definition of GFA Combined Circuit
::---------------------------------------------------

definition
  let x,y,z be set;
  func BitGFA3Str(x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void
  strict non empty ManySortedSign equals
:: GFACIRC1:def 49
  GFA3AdderStr(x,y,z) +* GFA3CarryStr(x,y,
  z);
end;

definition
  let x,y,z be set;
  func BitGFA3Circ(x,y,z) -> strict Boolean gate`2=den Circuit of BitGFA3Str(x
  ,y,z) equals
:: GFACIRC1:def 50
  GFA3AdderCirc(x,y,z) +* GFA3CarryCirc(x,y,z);
end;

::----------------------------------------------------------
:: GFA3 Combined : Carrier, InnerVertices and InputVertices
::----------------------------------------------------------
::-------------------------------------------------------
:: InnerVertices

theorem :: GFACIRC1:127
  for x,y,z being set holds InnerVertices BitGFA3Str(x,y,z) = {[
<*x,y*>,xor2]} \/ {GFA3AdderOutput(x,y,z)} \/ {[<*x,y*>,nor2], [<*y,z*>,nor2]
  , [<*z,x*>,nor2]} \/ {GFA3CarryOutput(x,y,z)};

theorem :: GFACIRC1:128
  for x,y,z being set holds InnerVertices BitGFA3Str(x,y,z) is Relation;

::-------------------------------------------------------
:: InputVertices

theorem :: GFACIRC1:129
  for x,y,z being set st z <> [<*x,y*>,xor2] & x <> [<*y,z*>,
  nor2] & y <> [<*z,x*>,nor2] & z <> [<*x,y*>,nor2] holds InputVertices
  BitGFA3Str(x,y,z) = {x,y,z};

theorem :: GFACIRC1:130
  for x,y,z being non pair set holds InputVertices BitGFA3Str(x,y ,z) = {x,y,z}
;

theorem :: GFACIRC1:131
  for x,y,z being non pair set holds InputVertices BitGFA3Str(x,y,z) is
  without_pairs;

::-------------------------------------------------------
:: Carrier and misc.

theorem :: GFACIRC1:132
  for x,y,z being set holds x in the carrier of BitGFA3Str(x,y,z) & y in
the carrier of BitGFA3Str(x,y,z) & z in the carrier of BitGFA3Str(x,y,z) & [<*x
,y*>,xor2] in the carrier of BitGFA3Str(x,y,z) & [<*[<*x,y*>,xor2],z*>,xor2] in
the carrier of BitGFA3Str(x,y,z) & [<*x,y*>,nor2] in the carrier of BitGFA3Str
(x,y,z) & [<*y,z*>,nor2] in the carrier of BitGFA3Str(x,y,z) & [<*z,x*>,nor2]
in the carrier of BitGFA3Str(x,y,z) & [<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x
  *>,nor2]*>,nor3] in the carrier of BitGFA3Str(x,y,z);

theorem :: GFACIRC1:133
  for x,y,z being set holds [<*x,y*>,xor2] in InnerVertices
BitGFA3Str(x,y,z) & GFA3AdderOutput(x,y,z) in InnerVertices BitGFA3Str(x,y,z) &
  [<*x,y*>,nor2] in InnerVertices BitGFA3Str(x,y,z) & [<*y,z*>,nor2] in
InnerVertices BitGFA3Str(x,y,z) & [<*z,x*>,nor2] in InnerVertices BitGFA3Str(x
  ,y,z) & GFA3CarryOutput(x,y,z) in InnerVertices BitGFA3Str(x,y,z);

theorem :: GFACIRC1:134
  for x,y,z being set st z <> [<*x,y*>,xor2] & x <> [<*y,z*>,nor2] & y
<> [<*z,x*>,nor2] & z <> [<*x,y*>,nor2] holds x in InputVertices BitGFA3Str(x
,y,z) & y in InputVertices BitGFA3Str(x,y,z) & z in InputVertices BitGFA3Str(x,
  y,z);

::------------------------------------------------------------------
:: GFA3 : Carry and Adder Output Definition of GFA Combined Circuit
::------------------------------------------------------------------

definition
  let x,y,z be set;
  func BitGFA3CarryOutput(x,y,z) -> Element of InnerVertices BitGFA3Str(x,y,z)
  equals
:: GFACIRC1:def 51
  [<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,nor3];
end;

definition
  let x,y,z be set;
  func BitGFA3AdderOutput(x,y,z) -> Element of InnerVertices BitGFA3Str(x,y,z)
  equals
:: GFACIRC1:def 52
  2GatesCircOutput(x,y,z, xor2);
end;

::-------------------------------------------------------------
:: GFA3 Combined : Stability of the Adder/Carry Output Circuit
::-------------------------------------------------------------

theorem :: GFACIRC1:135
  for x,y,z being set st z <> [<*x,y*>,xor2] & x <> [<*y,z*>,nor2] & y
<> [<*z,x*>,nor2] & z <> [<*x,y*>,nor2] for s being State of BitGFA3Circ(x,y,
  z) for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3 = s.z
  holds Following(s,2).GFA3AdderOutput(x,y,z) = 'not' ('not' a1 'xor' 'not' a2
'xor' 'not' a3) & Following(s,2).GFA3CarryOutput(x,y,z) = 'not' (('not' a1 '&'
  'not' a2) 'or' ('not' a2 '&' 'not' a3) 'or' ('not' a3 '&' 'not' a1));

theorem :: GFACIRC1:136
  for x,y,z being set st z <> [<*x,y*>,xor2] & x <> [<*y,z*>,nor2] & y
<> [<*z,x*>,nor2] & z <> [<*x,y*>,nor2] for s being State of BitGFA3Circ(x,y,
  z) holds Following(s,2) is stable;