FACIRC_1

:: Full Adder Circuit. Part { I }
::  by Grzegorz Bancerek and Yatsuka Nakamura
::
:: Received August 10, 1995
:: Copyright (c) 1995-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, XBOOLE_0, CARD_1, NAT_1, SUBSET_1, ARYTM_3, RELAT_1,
      FUNCT_1, FINSEQ_1, CIRCCOMB, FINSEQ_2, MSUALG_1, PARTFUN1, MSAFREE2,
      FUNCT_4, TARSKI, STRUCT_0, MARGREL1, XBOOLEAN, CIRCUIT1, FSM_1, CIRCUIT2,
      CARD_3, GLIB_000, LATTICES, MCART_1, FINSET_1, CLASSES1, FACIRC_1,
      ORDINAL1;
 notations TARSKI, XBOOLE_0, ENUMSET1, XTUPLE_0, XFAMILY, SUBSET_1, ORDINAL1,
      NUMBERS, XCMPLX_0, MCART_1, RELAT_1, CARD_1, STRUCT_0, FUNCT_1, FUNCT_2,
      FINSEQ_1, FINSET_1, FINSEQ_2, FUNCT_4, MARGREL1, BINARITH, CARD_3,
      CLASSES1, PARTFUN1, MSUALG_1, MSAFREE2, CIRCUIT1, CIRCUIT2, CIRCCOMB,
      XXREAL_0, NAT_1;
 constructors ENUMSET1, XXREAL_0, NAT_1, CLASSES1, BINARITH, CIRCUIT1,
      CIRCUIT2, CIRCCOMB, RELSET_1, BINOP_1, WELLORD2, DOMAIN_1, XTUPLE_0,
      NUMBERS, VALUED_0, XFAMILY;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, XXREAL_0, FINSEQ_1,
      FINSEQ_2, CARD_3, STRUCT_0, MSUALG_1, CIRCCOMB, NAT_1, XCMPLX_0,
      MSAFREE2, MARGREL1, FINSET_1, XTUPLE_0;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, RELAT_1, MSAFREE2, CIRCUIT2, CIRCCOMB, XBOOLE_0, XTUPLE_0;
 equalities TARSKI, MSAFREE2, MARGREL1, ORDINAL1;
 expansions CIRCUIT2, CIRCCOMB, XBOOLE_0;
 theorems TARSKI, ENUMSET1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4, ORDINAL1,
      FINSEQ_1, FINSEQ_2, MSUALG_1, MSAFREE2, CIRCUIT1, CIRCUIT2, CIRCCOMB,
      XBOOLE_0, XBOOLE_1, CLASSES1, CARD_1, XTUPLE_0, NAT_1;
 schemes NAT_1, RECDEF_1, FUNCT_2;

begin :: Pairs, Set Without Pairs, and Nonpair-yielding Functions

registration
  cluster pair -> non empty for set;
  coherence
  proof
    let z be set;
    given x,y being object such that
A1: z = [x,y];
    thus thesis by A1;
  end;
end;

registration
  cluster non pair for object;
  existence
  proof
    take {};
    let x,y be object;
    thus thesis;
  end;
end;

registration
  cluster -> non pair for Nat;
  coherence
  proof
    let n be Nat;
    given x,y being object such that
A1: n = [x,y];
    n <> 0 by A1;
    then 0 < n;
    then 0 in Segm n by NAT_1:44;
    hence contradiction by A1,TARSKI:def 2;
  end;
end;

definition
::$CD
  let IT be set;
  attr IT is with_pair means
  : Def1:
  ex x being pair object st x in IT;
end;

notation
  let IT be set;
  antonym IT is without_pairs for IT is with_pair;
end;

registration
  cluster empty -> without_pairs for set;
  coherence;
  let x be non pair object;
  cluster {x} -> without_pairs;
  coherence
  by TARSKI:def 1;
  let y be non pair object;
  cluster {x,y} -> without_pairs;
  coherence
  by TARSKI:def 2;
  let z be non pair object;
  cluster {x,y,z} -> without_pairs;
  coherence
  by ENUMSET1:def 1;
end;

registration
  cluster without_pairs for non empty set;
  existence
  proof
    set x = the non pair set;
    take {x};
    thus thesis;
  end;
end;

registration
  let X, Y be without_pairs set;
  cluster X \/ Y -> without_pairs;
  coherence
  proof
    let a be pair object;
    assume a in X \/ Y;
    then a in X or a in Y by XBOOLE_0:def 3;
    hence contradiction by Def1;
  end;
end;

registration
  let X be without_pairs set, Y be set;
  cluster X \ Y -> without_pairs;
  coherence
  by Def1;
  cluster X /\ Y -> without_pairs;
  coherence
  proof
    let a be pair object;
    assume a in X /\ Y;
    then a in X by XBOOLE_0:def 4;
    hence contradiction by Def1;
  end;
  cluster Y /\ X -> without_pairs;
  coherence;
end;

registration
  let x be pair object;
  cluster {x} -> Relation-like;
  coherence
  proof
    let a be object;
    assume a in {x};
    then a = x by TARSKI:def 1;
    then ex y,z being object st a = [y,z] by XTUPLE_0:def 1;
    hence thesis;
  end;
  let y be pair object;
  cluster {x,y} -> Relation-like;
  coherence
  proof
    let a be object;
    assume a in {x,y};
    then a = x or a = y by TARSKI:def 2;
    then ex y,z being object st a = [y,z] by XTUPLE_0:def 1;
    hence thesis;
  end;
  let z be pair object;
  cluster {x,y,z} -> Relation-like;
  coherence
  proof
    let a be object;
    assume a in {x,y,z};
    then a = x or a = y or a = z by ENUMSET1:def 1;
    then ex y,z being object st a = [y,z] by XTUPLE_0:def 1;
    hence thesis;
  end;
end;

registration
  cluster without_pairs Relation-like -> empty for set;
  coherence
  proof
    let x be set;
    assume
A1: not ex a being pair object st a in x;
    assume
A2: for a being object st a in x holds ex y,z being object st a = [y,z];
    assume x is non empty;
    then reconsider X = x as non empty set;
    set a = the Element of X;
    ex y,z being object st a = [y,z] by A2;
    hence contradiction by A1;
  end;
end;

definition
  let IT be Function;
  attr IT is nonpair-yielding means
  for x being set st x in dom IT holds IT.x is non pair;
end;

registration
  let x be non pair object;
  cluster <*x*> -> nonpair-yielding;
  coherence
  proof
    let a be set;
    assume a in dom <*x*>;
    then <*x*>.a in rng <*x*> by FUNCT_1:def 3;
    then <*x*>.a in {x} by FINSEQ_1:39;
    hence thesis by TARSKI:def 1;
  end;
  let y be non pair object;
  cluster <*x,y*> -> nonpair-yielding;
  coherence
  proof
    let a be set;
    assume a in dom <*x,y*>;
    then <*x,y*>.a in rng <*x,y*> by FUNCT_1:def 3;
    then <*x,y*>.a in {x,y} by FINSEQ_2:127;
    hence thesis by TARSKI:def 2;
  end;
  let z be non pair object;
  cluster <*x,y,z*> -> nonpair-yielding;
  coherence
  proof
    let a be set;
    assume a in dom <*x,y,z*>;
    then <*x,y,z*>.a in rng <*x,y,z*> by FUNCT_1:def 3;
    then <*x,y,z*>.a in {x,y,z} by FINSEQ_2:128;
    hence thesis by ENUMSET1:def 1;
  end;
end;

theorem Th1:
  for f being Function st f is nonpair-yielding holds rng f is without_pairs
proof
  let f be Function;
  assume
A1: for x being set st x in dom f holds f.x is non pair;
  let y be pair object;
  assume y in rng f;
  then ex x being object st x in dom f & y = f.x by FUNCT_1:def 3;
  hence thesis by A1;
end;

registration
  let n be Nat;
  cluster one-to-one nonpair-yielding for FinSeqLen of n;
  existence
  proof
    reconsider p = id Seg n as FinSequence by FINSEQ_2:48;
    len p = len idseq n by FINSEQ_2:def 1
      .= n by CARD_1:def 7;
    then reconsider p as FinSeqLen of n by CARD_1:def 7;
    take p;
    thus p is one-to-one;
    let x be set;
    assume
A1: x in dom p;
    x in Seg n by A1;
    hence thesis by FUNCT_1:17;
  end;
end;

registration
  cluster one-to-one nonpair-yielding for FinSequence;
  existence
  proof
    set n = the Nat,p = the one-to-one nonpair-yielding FinSeqLen of n;
    take p;
    thus thesis;
  end;
end;

registration
  let f be nonpair-yielding Function;
  cluster rng f -> without_pairs;
  coherence by Th1;
end;

theorem Th2:
  for S1,S2 being non empty ManySortedSign st S1 tolerates S2 &
InnerVertices S1 is Relation & InnerVertices S2 is Relation holds InnerVertices
  (S1+*S2) is Relation
proof
  let S1, S2 be non empty ManySortedSign;
  assume
A1: S1 tolerates S2;
  assume InnerVertices S1 is Relation & InnerVertices S2 is Relation;
  then reconsider R1 = InnerVertices S1, R2 = InnerVertices S2 as Relation;
  R1 \/ R2 is Relation;
  hence thesis by A1,CIRCCOMB:11;
end;

theorem
  for S1,S2 being unsplit gate`1=arity non empty ManySortedSign st
InnerVertices S1 is Relation & InnerVertices S2 is Relation holds InnerVertices
  (S1+*S2) is Relation by Th2,CIRCCOMB:47;

theorem Th4:
  for S1,S2 being non empty ManySortedSign st S1 tolerates S2 &
  InnerVertices S2 misses InputVertices S1 holds InputVertices S1 c=
  InputVertices (S1+*S2) & InputVertices (S1+*S2) = (InputVertices S1) \/ (
  InputVertices S2 \ InnerVertices S1)
proof
  let S1,S2 be non empty ManySortedSign;
  set S = S1+*S2;
  set R = the ResultSort of S;
  set R1 = the ResultSort of S1;
  set R2 = the ResultSort of S2;
  assume that
A1: S1 tolerates S2 and
A2: InnerVertices S2 misses InputVertices S1;
A3: InnerVertices S = rng R;
  InnerVertices S1 = rng R1 & InnerVertices S2 = rng R2;
  then
A4: rng R = (rng R1) \/ rng R2 by A1,A3,CIRCCOMB:11;
A5: the carrier of S = (the carrier of S1) \/ the carrier of S2 by
CIRCCOMB:def 2;
  hereby
    let x be object;
    assume
A6: x in InputVertices S1;
    then ( not x in rng R1)& not x in rng R2 by A2,XBOOLE_0:3,def 5;
    then
A7: not x in rng R by A4,XBOOLE_0:def 3;
    x in the carrier of S by A5,A6,XBOOLE_0:def 3;
    hence x in InputVertices S by A7,XBOOLE_0:def 5;
  end;
A8: InputVertices S c= (InputVertices S1) \/ InputVertices S2 by A1,CIRCCOMB:11
;
  hereby
    let x be object;
    assume
A9: x in InputVertices (S1+*S2);
    then not x in rng R by XBOOLE_0:def 5;
    then x in InputVertices S1 or x in InputVertices S2 & not x in
    InnerVertices S1 by A4,A8,A9,XBOOLE_0:def 3;
    then x in InputVertices S1 or x in InputVertices S2 \ InnerVertices S1 by
XBOOLE_0:def 5;
    hence x in (InputVertices S1) \/ (InputVertices S2 \ InnerVertices S1) by
XBOOLE_0:def 3;
  end;
  let x be object;
  assume x in (InputVertices S1) \/ (InputVertices S2 \ InnerVertices S1);
  then
A10: x in InputVertices S1 or x in InputVertices S2 \ rng R1 by XBOOLE_0:def 3;
  then
A11: x in the carrier of S by A5,XBOOLE_0:def 3;
  x in InputVertices S1 & not x in rng R2 or x in InputVertices S2 & not
  x in rng R1 by A2,A10,XBOOLE_0:3,def 5;
  then
A12: not x in rng R2 by XBOOLE_0:def 5;
  not x in rng R1 by A10,XBOOLE_0:def 5;
  then not x in rng R by A4,A12,XBOOLE_0:def 3;
  hence thesis by A11,XBOOLE_0:def 5;
end;

theorem Th5:
  for X,R being set st X is without_pairs & R is Relation holds X misses R;

theorem Th6:
  for S1,S2 being unsplit gate`1=arity non empty ManySortedSign st
  InputVertices S1 is without_pairs & InnerVertices S2 is Relation holds
  InputVertices S1 c= InputVertices (S1+*S2) & InputVertices (S1+*S2) = (
  InputVertices S1) \/ (InputVertices S2 \ InnerVertices S1)
proof
  let S1,S2 be unsplit gate`1=arity non empty ManySortedSign;
  assume InputVertices S1 is without_pairs & InnerVertices S2 is Relation;
  then S1 tolerates S2 & InnerVertices S2 misses InputVertices S1 by
CIRCCOMB:47;
  hence thesis by Th4;
end;

theorem Th7:
  for S1,S2 being unsplit gate`1=arity non empty ManySortedSign st
  InputVertices S1 is without_pairs & InnerVertices S1 is Relation &
  InputVertices S2 is without_pairs & InnerVertices S2 is Relation holds
  InputVertices (S1+*S2) = (InputVertices S1) \/ (InputVertices S2)
proof
  let S1,S2 be unsplit gate`1=arity non empty ManySortedSign;
  assume InputVertices S1 is without_pairs & InnerVertices S1 is Relation &
  InputVertices S2 is without_pairs & InnerVertices S2 is Relation;
  then InputVertices (S1+*S2) = (InputVertices S1) \/ (InputVertices S2 \
  InnerVertices S1) & InnerVertices S1 misses InputVertices S2 by Th6;
  hence thesis by XBOOLE_1:83;
end;

theorem Th8:
  for S1,S2 being non empty ManySortedSign st S1 tolerates S2 &
  InputVertices S1 is without_pairs & InputVertices S2 is without_pairs holds
  InputVertices (S1+*S2) is without_pairs
proof
  let S1, S2 be non empty ManySortedSign;
  assume S1 tolerates S2;
  then
A1: InputVertices (S1+*S2) c= (InputVertices S1) \/ InputVertices S2 by
CIRCCOMB:11;
  assume
A2: for x being pair object holds not x in InputVertices S1;
  assume
A3: for x being pair object holds not x in InputVertices S2;
  let x be pair object;
  assume x in InputVertices (S1+*S2);
  then x in InputVertices S1 or x in InputVertices S2 by A1,XBOOLE_0:def 3;
  hence contradiction by A2,A3;
end;

theorem
  for S1,S2 being unsplit gate`1=arity non empty ManySortedSign st
  InputVertices S1 is without_pairs & InputVertices S2 is without_pairs holds
  InputVertices (S1+*S2) is without_pairs by Th8,CIRCCOMB:47;

begin :: Boolean Operations

definition
  let i be Nat, D be non empty set;
  mode Tuple of i,D is Element of i-tuples_on D;
end;

scheme
  2AryBooleEx {F(set,set) -> Element of BOOLEAN}: ex f being Function of 2
-tuples_on BOOLEAN, BOOLEAN st for x,y being Element of BOOLEAN holds f.<*x,y*>
  = F(x,y) proof
  deffunc G(Tuple of 2, BOOLEAN) = F($1.1,$1.2);
  consider f being Function of 2-tuples_on BOOLEAN, BOOLEAN such that
A1: for a being Tuple of 2, BOOLEAN holds f.a = G(a) from FUNCT_2:sch 4;
  hereby
    take f;
    let x,y be Element of BOOLEAN;
    reconsider a = <*x,y*> as Tuple of 2, BOOLEAN by FINSEQ_2:101;
    thus f.<*x,y*> = F(a.1,a.2) by A1
      .= F(x,a.2)
      .= F(x,y);
  end;
end;

scheme
  2AryBooleUniq {F(set,set) -> Element of BOOLEAN}: for f1,f2 being Function
of 2-tuples_on BOOLEAN, BOOLEAN st (for x,y being Element of BOOLEAN holds f1.
<*x,y*> = F(x,y)) & (for x,y being Element of BOOLEAN holds f2.<*x,y*> = F(x,y)
  ) holds f1 = f2 proof
  let f1,f2 be Function of 2-tuples_on BOOLEAN, BOOLEAN such that
A1: for x,y being Element of BOOLEAN holds f1.<*x,y*> = F(x,y) and
A2: for x,y being Element of BOOLEAN holds f2.<*x,y*> = F(x,y);
  now
    let a be Tuple of 2, BOOLEAN;
    consider x,y being Element of BOOLEAN such that
A3: a = <*x,y*> by FINSEQ_2:100;
    thus f1.a = F(x,y) by A1,A3
      .= f2.a by A2,A3;
  end;
  hence thesis by FUNCT_2:63;
end;

scheme
  2AryBooleDef {F(set,set) -> Element of BOOLEAN}: (ex f being Function of 2
-tuples_on BOOLEAN, BOOLEAN st for x,y being Element of BOOLEAN holds f.<*x,y*>
= F(x,y)) & for f1,f2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st (for x,
y being Element of BOOLEAN holds f1.<*x,y*> = F(x,y)) & (for x,y being Element
  of BOOLEAN holds f2.<*x,y*> = F(x,y)) holds f1 = f2 proof
  deffunc G(Tuple of 2, BOOLEAN) = F($1.1,$1.2);
  consider f being Function of 2-tuples_on BOOLEAN, BOOLEAN such that
A1: for a being Tuple of 2, BOOLEAN holds f.a = G(a) from FUNCT_2:sch 4;
  hereby
    take f;
    let x,y be Element of BOOLEAN;
    reconsider a = <*x,y*> as Tuple of 2, BOOLEAN by FINSEQ_2:101;
    thus f.<*x,y*> = F(a.1,a.2) by A1
      .= F(x,a.2)
      .= F(x,y);
  end;
  let f1,f2 be Function of 2-tuples_on BOOLEAN, BOOLEAN such that
A2: for x,y being Element of BOOLEAN holds f1.<*x,y*> = F(x,y) and
A3: for x,y being Element of BOOLEAN holds f2.<*x,y*> = F(x,y);
  now
    let a be Tuple of 2, BOOLEAN;
    consider x,y being Element of BOOLEAN such that
A4: a = <*x,y*> by FINSEQ_2:100;
    thus f1.a = F(x,y) by A2,A4
      .= f2.a by A3,A4;
  end;
  hence thesis by FUNCT_2:63;
end;

scheme
  3AryBooleEx {F(set,set,set) -> Element of BOOLEAN}: ex f being Function of 3
-tuples_on BOOLEAN, BOOLEAN st for x,y,z being Element of BOOLEAN holds f.<*x,y
  ,z*> = F(x,y,z) proof
  deffunc G(Tuple of 3, BOOLEAN) = F($1.1,$1.2,$1.3);
  consider f being Function of 3-tuples_on BOOLEAN, BOOLEAN such that
A1: for a being Tuple of 3, BOOLEAN holds f.a = G(a) from FUNCT_2:sch 4;
  hereby
    take f;
    let x,y,z be Element of BOOLEAN;
    reconsider a = <*x,y,z*> as Tuple of 3, BOOLEAN by FINSEQ_2:104;
    thus f.<*x,y,z*> = F(a.1,a.2,a.3) by A1
      .= F(x,a.2,a.3)
      .= F(x,y,a.3)
      .= F(x,y,z);
  end;
end;

scheme
  3AryBooleUniq {F(set,set,set) -> Element of BOOLEAN}: for f1,f2 being
Function of 3-tuples_on BOOLEAN, BOOLEAN st (for x,y,z being Element of BOOLEAN
holds f1.<*x,y,z*> = F(x,y,z)) & (for x,y,z being Element of BOOLEAN holds f2.
  <*x,y,z*> = F(x,y,z)) holds f1 = f2 proof
  let f1,f2 be Function of 3-tuples_on BOOLEAN, BOOLEAN such that
A1: for x,y,z being Element of BOOLEAN holds f1.<*x,y,z*> = F(x,y,z) and
A2: for x,y,z being Element of BOOLEAN holds f2.<*x,y,z*> = F(x,y,z);
  now
    let a be Tuple of 3, BOOLEAN;
    consider x,y,z being Element of BOOLEAN such that
A3: a = <*x,y,z*> by FINSEQ_2:103;
    thus f1.a = F(x,y,z) by A1,A3
      .= f2.a by A2,A3;
  end;
  hence thesis by FUNCT_2:63;
end;

scheme
  3AryBooleDef {F(set,set,set) -> Element of BOOLEAN}: (ex f being Function of
3-tuples_on BOOLEAN, BOOLEAN st for x,y,z being Element of BOOLEAN holds f.<*x,
y,z*> = F(x,y,z)) & for f1,f2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st
(for x,y,z being Element of BOOLEAN holds f1.<*x,y,z*> = F(x,y,z)) & (for x,y,z
  being Element of BOOLEAN holds f2.<*x,y,z*> = F(x,y,z)) holds f1 = f2 proof
  deffunc G(Tuple of 3, BOOLEAN) = F($1.1,$1.2,$1.3);
  consider f being Function of 3-tuples_on BOOLEAN, BOOLEAN such that
A1: for a being Tuple of 3, BOOLEAN holds f.a = G(a) from FUNCT_2:sch 4;
  hereby
    take f;
    let x,y,z be Element of BOOLEAN;
    reconsider a = <*x,y,z*> as Tuple of 3, BOOLEAN by FINSEQ_2:104;
    thus f.<*x,y,z*> = F(a.1,a.2,a.3) by A1
      .= F(x,a.2,a.3)
      .= F(x,y,a.3)
      .= F(x,y,z);
  end;
  let f1,f2 be Function of 3-tuples_on BOOLEAN, BOOLEAN such that
A2: for x,y,z being Element of BOOLEAN holds f1.<*x,y,z*> = F(x,y,z) and
A3: for x,y,z being Element of BOOLEAN holds f2.<*x,y,z*> = F(x,y,z);
  now
    let a be Tuple of 3, BOOLEAN;
    consider x,y,z being Element of BOOLEAN such that
A4: a = <*x,y,z*> by FINSEQ_2:103;
    thus f1.a = F(x,y,z) by A2,A4
      .= f2.a by A3,A4;
  end;
  hence thesis by FUNCT_2:63;
end;

definition
  func 'xor' -> Function of 2-tuples_on BOOLEAN, BOOLEAN means
  : Def3:
  for x,y being Element of BOOLEAN holds it.<*x,y*> = x 'xor' y;
  correctness
  proof
    deffunc F(Element of BOOLEAN,Element of BOOLEAN) = $1 'xor' $2;
    (ex f being Function of 2-tuples_on BOOLEAN, BOOLEAN st for x,y being
Element of BOOLEAN holds f.<*x,y*> = F(x,y)) & for f1,f2 being Function of 2
-tuples_on BOOLEAN, BOOLEAN st (for x,y being Element of BOOLEAN holds f1.<*x,y
    *> = F(x,y)) & (for x,y being Element of BOOLEAN holds f2.<*x,y*> = F(x,y))
    holds f1 = f2 from 2AryBooleDef;
    hence thesis;
  end;
  func 'or' -> Function of 2-tuples_on BOOLEAN, BOOLEAN means
  : Def4:
  for x,y being Element of BOOLEAN holds it.<*x,y*> = x 'or' y;
  correctness
  proof
    deffunc F(Element of BOOLEAN,Element of BOOLEAN) = $1 'or' $2;
    (ex f being Function of 2-tuples_on BOOLEAN, BOOLEAN st for x,y being
Element of BOOLEAN holds f.<*x,y*> = F(x,y)) & for f1,f2 being Function of 2
-tuples_on BOOLEAN, BOOLEAN st (for x,y being Element of BOOLEAN holds f1.<*x,y
    *> = F(x,y)) & (for x,y being Element of BOOLEAN holds f2.<*x,y*> = F(x,y))
    holds f1 = f2 from 2AryBooleDef;
    hence thesis;
  end;
  func '&' -> Function of 2-tuples_on BOOLEAN, BOOLEAN means
  : Def5:
  for x,y being Element of BOOLEAN holds it.<*x,y*> = x '&' y;
  correctness
  proof
    deffunc F(Element of BOOLEAN,Element of BOOLEAN) = $1 '&' $2;
    (ex f being Function of 2-tuples_on BOOLEAN, BOOLEAN st for x,y being
Element of BOOLEAN holds f.<*x,y*> = F(x,y)) & for f1,f2 being Function of 2
-tuples_on BOOLEAN, BOOLEAN st (for x,y being Element of BOOLEAN holds f1.<*x,y
    *> = F(x,y)) & (for x,y being Element of BOOLEAN holds f2.<*x,y*> = F(x,y))
    holds f1 = f2 from 2AryBooleDef;
    hence thesis;
  end;
end;

definition
  func or3 -> Function of 3-tuples_on BOOLEAN, BOOLEAN means
  : Def6:
  for x,y,z being Element of BOOLEAN holds it.<*x,y,z*> = x 'or' y 'or' z;
  correctness
  proof
    deffunc F(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN) = $1
    'or' $2 'or' $3;
    (ex f being Function of 3-tuples_on BOOLEAN, BOOLEAN st for x,y,z
    being Element of BOOLEAN holds f.<*x,y,z*> = F(x,y,z)) & for f1,f2 being
Function of 3-tuples_on BOOLEAN, BOOLEAN st (for x,y,z being Element of BOOLEAN
holds f1.<*x,y,z*> = F(x,y,z)) & (for x,y,z being Element of BOOLEAN holds f2.
    <*x,y,z*> = F(x,y,z)) holds f1 = f2 from 3AryBooleDef;
    hence thesis;
  end;
end;

begin :: Computation and Stabilizable

theorem Th10:
  for S being Circuit-like non void non empty ManySortedSign for
A being non-empty Circuit of S for s being State of A, g being Gate of S holds
  (Following s).the_result_sort_of g = Den(g, A).(s*the_arity_of g)
proof
  let S be Circuit-like non void non empty ManySortedSign;
  let A be non-empty Circuit of S;
  let s be State of A, g be Gate of S;
  set v = the_result_sort_of g;
  dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;
  then (the ResultSort of S).g in rng the ResultSort of S by FUNCT_1:def 3;
  then
A1: v in InnerVertices S by MSUALG_1:def 2;
  then g depends_on_in s = s*the_arity_of g & action_at v = g by CIRCUIT1:def 3
,MSAFREE2:def 7;
  hence thesis by A1,CIRCUIT2:def 5;
end;

definition
  let S be non void Circuit-like non empty ManySortedSign;
  let A be non-empty Circuit of S;
  let s be State of A;
  let n be natural Number;
  func Following(s,n) -> State of A means
  :Def7:
  ex f being sequence of product the Sorts of A st it = f.n & f.0 = s &
  for n being Nat holds f.(n+1) = Following f.n;
  correctness
  proof
    reconsider n as Nat by TARSKI:1;
    set D = product the Sorts of A;
    deffunc R(natural Number,Element of D) = Following $2;
    (ex y being Element of D st ex f being sequence of D st y = f.n &
f.0 = s & for n being Nat holds f.(n+1) = R(n,f.n)) & for y1,y2 being Element
of D st (ex f being sequence of D st y1 = f.n & f.0 = s & for n being Nat
holds f.(n+1) = R(n,f.n)) & (ex f being sequence of D st y2 = f.n & f.0 = s
& for n being Nat holds f.(n+1) = R(n,f.n)) holds y1 = y2 from RECDEF_1:sch 14;
    hence thesis;
  end;
end;

theorem Th11:
  for S being Circuit-like non void non empty ManySortedSign for
  A being non-empty Circuit of S, s being State of A holds Following(s,0) = s
proof
  let S be Circuit-like non void non empty ManySortedSign;
  let A be non-empty Circuit of S, s be State of A;
  ex f being sequence of  product the Sorts of A st Following(s,0) = f
  .0 & f.0 = s & for n being Nat holds f.(n+1) = Following f.n by Def7;
  hence thesis;
end;

theorem Th12:
  for S being Circuit-like non void non empty ManySortedSign for
  A being non-empty Circuit of S, s being State of A for n being Nat holds
  Following(s,n+1) = Following Following(s,n)
proof
  let S be Circuit-like non void non empty ManySortedSign;
  let A be non-empty Circuit of S, s be State of A;
  let n be Nat;
  consider f being sequence of  product the Sorts of A such that
A1: Following(s,n) = f.n and
A2: f.0 = s and
A3: for n being Nat holds f.(n+1) = Following f.n by Def7;
  thus Following(s,n+1) = f.(n+1) by A2,A3,Def7
    .= Following Following(s,n) by A1,A3;
end;

theorem Th13:
  for S being Circuit-like non void non empty ManySortedSign for
  A being non-empty Circuit of S, s being State of A for n,m being Nat holds
  Following(s,n+m) = Following(Following(s,n),m)
proof
  let S be Circuit-like non void non empty ManySortedSign;
  let A be non-empty Circuit of S, s be State of A;
  let n be Nat;
  defpred P[Nat] means Following(s,n+$1) = Following(Following(s,n),$1);
A1: for m being Nat st P[m] holds P[m+1]
  proof
    let m be Nat;
    assume
A2: Following(s,n+m) = Following(Following(s,n),m);
    thus Following(s,n+(m+1)) = Following(s,n+m+1)
      .= Following Following(s,n+m) by Th12
      .= Following(Following(s,n),m+1) by A2,Th12;
  end;
A3: P[0] by Th11;
  thus for i being Nat holds P[i] from NAT_1:sch 2(A3,A1);
end;

theorem Th14:
  for S being non void Circuit-like non empty ManySortedSign for
  A being non-empty Circuit of S, s being State of A holds Following(s,1) =
  Following s
proof
  let S be non void Circuit-like non empty ManySortedSign;
  let A be non-empty Circuit of S, s be State of A;
  0+1 = 1;
  hence Following(s,1) = Following Following(s,0) by Th12
    .= Following s by Th11;
end;

theorem Th15:
  for S being non void Circuit-like non empty ManySortedSign for
  A being non-empty Circuit of S, s being State of A holds Following(s,2) =
  Following Following s
proof
  let S be non void Circuit-like non empty ManySortedSign;
  let A be non-empty Circuit of S, s be State of A;
  2 = 1+1;
  hence Following(s,2) = Following Following(s,0+1) by Th12
    .= Following Following s by Th14;
end;

theorem Th16:
  for S being Circuit-like non void non empty ManySortedSign for
  A being non-empty Circuit of S, s being State of A for n being Nat holds
  Following(s,n+1) = Following(Following s, n)
proof
  let S be Circuit-like non void non empty ManySortedSign;
  let A be non-empty Circuit of S, s be State of A;
  let n be Nat;
  Following(s,n+1) = Following(Following(s,1), n) by Th13;
  hence thesis by Th14;
end;

definition
  let S be non void Circuit-like non empty ManySortedSign;
  let A be non-empty Circuit of S;
  let s be State of A;
  let x be object;
  pred s is_stable_at x means

  for n being Nat holds (Following(s,n)).x = s.x;
end;

theorem
  for S being non void Circuit-like non empty ManySortedSign for A
  being non-empty Circuit of S, s being State of A for x being set st s
  is_stable_at x for n being Nat holds Following(s,n) is_stable_at x
proof
  let S be non void Circuit-like non empty ManySortedSign;
  let A be non-empty Circuit of S;
  let s be State of A;
  let x be set such that
A1: for n being Nat holds (Following(s,n)).x = s.x;
  let n, m be Nat;
  thus (Following(Following(s,n),m)).x = (Following(s,n+m)).x by Th13
    .= s.x by A1
    .= (Following(s,n)).x by A1;
end;

theorem
  for S being non void Circuit-like non empty ManySortedSign for A
  being non-empty Circuit of S, s being State of A for x being set st x in
  InputVertices S holds s is_stable_at x
proof
  let S be non void Circuit-like non empty ManySortedSign;
  let A be non-empty Circuit of S;
  let s be State of A;
  let x be set;
  defpred P[Nat] means (Following(s,$1)).x = s.x;
  assume
A1: x in InputVertices S;
A2: now
    let n be Nat;
    assume
A3: P[n];
    (Following(s,n+1)).x = (Following Following(s,n)).x by Th12
      .= s.x by A1,A3,CIRCUIT2:def 5;
    hence P[n+1];
  end;
A4: P[0] by Th11;
  thus for n being Nat holds P[n] from NAT_1:sch 2(A4,A2);
end;

theorem Th19:
  for S being non void Circuit-like non empty ManySortedSign for
A being non-empty Circuit of S, s being State of A for g being Gate of S st for
x being set st x in rng the_arity_of g holds s is_stable_at x holds Following s
  is_stable_at the_result_sort_of g
proof
  let S be non void Circuit-like non empty ManySortedSign;
  let A be non-empty Circuit of S;
  let s be State of A;
  let g be Gate of S;
  set p = the_arity_of g;
  assume
A1: for x being set st x in rng p holds s is_stable_at x;
  let n be Nat;
A2: now
    let a be object;
    assume
A3: a in dom p;
    then p.a in rng p by FUNCT_1:def 3;
    then
A4: s is_stable_at p.a by A1;
    ((Following(s, n))*p).a = (Following(s, n)).(p.a) & (s*p).a = s.(p . a
    ) by A3,FUNCT_1:13;
    hence ((Following(s, n))*p).a = (s*p).a by A4;
  end;
A5: rng p c= the carrier of S by FINSEQ_1:def 4;
  dom Following(s, n) = the carrier of S by CIRCUIT1:3;
  then
A6: dom ((Following(s, n))*p) = dom p by A5,RELAT_1:27;
  dom s = the carrier of S by CIRCUIT1:3;
  then dom (s*p) = dom p by A5,RELAT_1:27;
  then
A7: (Following(s, n))*p = s*p by A6,A2,FUNCT_1:2;
  thus (Following(Following s, n)).the_result_sort_of g = (Following(s, n+1)).
  the_result_sort_of g by Th16
    .= (Following Following(s, n)).the_result_sort_of g by Th12
    .= (Den(g,A)).((Following(s, n))*p) by Th10
    .= (Following s).the_result_sort_of g by A7,Th10;
end;

begin :: Combined Circuits

theorem Th20:
  for S1,S2 being non empty ManySortedSign, v being Vertex of S1
  holds v in the carrier of S1+*S2 & v in the carrier of S2+*S1
proof
  let S1,S2 be non empty ManySortedSign;
  let v be Vertex of S1;
  the carrier of (S1+*S2) = (the carrier of S1) \/ the carrier of S2 & the
carrier of (S2+*S1) = (the carrier of S2) \/ the carrier of S1 by
CIRCCOMB:def 2;
  hence thesis by XBOOLE_0:def 3;
end;

theorem Th21:
  for S1,S2 being unsplit gate`1=arity non empty ManySortedSign
for x being set st x in InnerVertices S1 holds x in InnerVertices (S1+*S2) & x
  in InnerVertices (S2+*S1)
proof
  let S1,S2 be unsplit gate`1=arity non empty ManySortedSign;
  S1 tolerates S2 by CIRCCOMB:47;
  then InnerVertices (S1+*S2) = InnerVertices S1 \/ InnerVertices S2 &
  InnerVertices (S2+*S1) = InnerVertices S2 \/ InnerVertices S1 by CIRCCOMB:11;
  hence thesis by XBOOLE_0:def 3;
end;

theorem
  for S1,S2 being non empty ManySortedSign for x being set st x in
  InnerVertices S2 holds x in InnerVertices (S1+*S2)
proof
  let S1,S2 be non empty ManySortedSign;
  set R1 = the ResultSort of S1, R2 = the ResultSort of S2;
  InnerVertices (S1+*S2) = rng (R1+*R2) by CIRCCOMB:def 2;
  then InnerVertices S2 c= InnerVertices (S1+*S2) by FUNCT_4:18;
  hence thesis;
end;

theorem
  for S1,S2 being unsplit gate`1=arity non empty ManySortedSign holds S1
  +*S2 = S2+*S1 by CIRCCOMB:5,47;

theorem
  for S1,S2 being unsplit gate`1=arity gate`2isBoolean non void non
empty ManySortedSign for A1 being Boolean gate`2=den Circuit of S1 for A2 being
  Boolean gate`2=den Circuit of S2 holds A1+*A2 = A2+*A1 by CIRCCOMB:22,60;

theorem Th25:
  for S1,S2,S3 be unsplit gate`1=arity gate`2isBoolean non void
  non empty ManySortedSign for A1 being Boolean Circuit of S1, A2 being Boolean
Circuit of S2 for A3 being Boolean Circuit of S3 holds (A1+*A2)+*A3 = A1+*(A2+*
  A3)
proof
  let S1,S2,S3 be unsplit gate`1=arity gate`2isBoolean non void non empty
  ManySortedSign;
  let A1 be Boolean Circuit of S1;
  let A2 be Boolean Circuit of S2;
  let A3 be Boolean Circuit of S3;
A1: the Sorts of A3 tolerates the Sorts of A1 by CIRCCOMB:59;
  the Sorts of A1 tolerates the Sorts of A2 & the Sorts of A2 tolerates
  the Sorts of A3 by CIRCCOMB:59;
  hence thesis by A1,CIRCCOMB:23;
end;

theorem Th26:
  for S1,S2 being unsplit gate`1=arity gate`2isBoolean non void
  non empty ManySortedSign for A1 being Boolean gate`2=den non-empty Circuit of
S1 for A2 being Boolean gate`2=den non-empty Circuit of S2 for s being State of
A1+*A2 holds s|the carrier of S1 is State of A1 & s|the carrier of S2 is State
  of A2
proof
  let S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty
  ManySortedSign;
  let A1 be Boolean gate`2=den Circuit of S1;
  let A2 be Boolean gate`2=den Circuit of S2;
  let s be State of A1+*A2;
  the Sorts of A1 tolerates the Sorts of A2 by CIRCCOMB:59;
  hence thesis by CIRCCOMB:26;
end;

theorem Th27:
  for S1,S2 being unsplit gate`1=arity non empty ManySortedSign
  holds InnerVertices (S1+*S2) = (InnerVertices S1) \/ InnerVertices S2
proof
  let S1,S2 be unsplit gate`1=arity non empty ManySortedSign;
  S1 tolerates S2 by CIRCCOMB:47;
  hence thesis by CIRCCOMB:11;
end;

theorem Th28:
  for S1,S2 being unsplit gate`1=arity gate`2isBoolean non void
  non empty ManySortedSign st InnerVertices S2 misses InputVertices S1 for A1
being Boolean gate`2=den Circuit of S1 for A2 being Boolean gate`2=den Circuit
  of S2 for s being State of A1+*A2, s1 being State of A1 st s1 = s|the carrier
  of S1 holds (Following s)|the carrier of S1 = Following s1
proof
  let S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty
  ManySortedSign such that
A1: InnerVertices S2 misses InputVertices S1;
  let A1 be Boolean gate`2=den Circuit of S1;
  let A2 be Boolean gate`2=den Circuit of S2;
  let s be State of A1+*A2, s1 be State of A1 such that
A2: s1 = s|the carrier of S1;
  reconsider s2 = s|the carrier of S2 as State of A2 by Th26;
  dom Following s1 = the carrier of S1 & Following s = (Following s2)+*
  Following s1 by A1,A2,CIRCCOMB:33,60,CIRCUIT1:3;
  hence thesis by FUNCT_4:23;
end;

theorem Th29:
  for S1,S2 being unsplit gate`1=arity gate`2isBoolean non void
  non empty ManySortedSign st InnerVertices S1 misses InputVertices S2 for A1
being Boolean gate`2=den Circuit of S1 for A2 being Boolean gate`2=den Circuit
  of S2 for s being State of A1+*A2, s2 being State of A2 st s2 = s|the carrier
  of S2 holds (Following s)|the carrier of S2 = Following s2
proof
  let S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty
  ManySortedSign such that
A1: InnerVertices S1 misses InputVertices S2;
  let A1 be Boolean gate`2=den Circuit of S1;
  let A2 be Boolean gate`2=den Circuit of S2;
  let s be State of A1+*A2, s2 be State of A2 such that
A2: s2 = s|the carrier of S2;
  reconsider s1 = s|the carrier of S1 as State of A1 by Th26;
  dom Following s2 = the carrier of S2 & Following s = (Following s1)+*
  Following s2 by A1,A2,CIRCCOMB:32,60,CIRCUIT1:3;
  hence thesis by FUNCT_4:23;
end;

theorem Th30:
  for S1,S2 being unsplit gate`1=arity gate`2isBoolean non void
  non empty ManySortedSign st InnerVertices S2 misses InputVertices S1 for A1
being Boolean gate`2=den Circuit of S1 for A2 being Boolean gate`2=den Circuit
  of S2 for s being State of A1+*A2, s1 being State of A1 st s1 = s|the carrier
of S1 for n being Nat holds Following(s,n)|the carrier of S1 = Following(s1,n)
proof
  let S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty
  ManySortedSign such that
A1: InnerVertices S2 misses InputVertices S1;
  let A1 be Boolean gate`2=den Circuit of S1;
  let A2 be Boolean gate`2=den Circuit of S2;
  let s be State of A1+*A2, s1 be State of A1 such that
A2: s1 = s|the carrier of S1;
  defpred P[Nat] means Following(s,$1)|the carrier of S1 = Following(s1,$1);
A3: for n being Nat st P[n] holds P[n+1]
  proof
    let n be Nat;
    assume
A4: Following(s,n)|the carrier of S1 = Following(s1,n);
    thus Following(s,n+1)|the carrier of S1 = (Following Following(s,n))|the
    carrier of S1 by Th12
      .= Following Following(s1,n) by A1,A4,Th28
      .= Following(s1,n+1) by Th12;
  end;
  Following(s,0) = s by Th11;
  then
A5: P[0] by A2,Th11;
  thus for n being Nat holds P[n] from NAT_1:sch 2(A5,A3);
end;

theorem Th31:
  for S1,S2 being unsplit gate`1=arity gate`2isBoolean non void
  non empty ManySortedSign st InnerVertices S1 misses InputVertices S2 for A1
being Boolean gate`2=den Circuit of S1 for A2 being Boolean gate`2=den Circuit
  of S2 for s being State of A1+*A2, s2 being State of A2 st s2 = s|the carrier
of S2 for n being Nat holds Following(s,n)|the carrier of S2 = Following(s2,n)
proof
  let S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty
  ManySortedSign such that
A1: InnerVertices S1 misses InputVertices S2;
  let A1 be Boolean gate`2=den Circuit of S1;
  let A2 be Boolean gate`2=den Circuit of S2;
  let s be State of A1+*A2, s2 be State of A2 such that
A2: s2 = s|the carrier of S2;
  defpred P[Nat] means Following(s,$1)|the carrier of S2 = Following(s2,$1);
A3: for n being Nat st P[n] holds P[n+1]
  proof
    let n be Nat;
    assume
A4: Following(s,n)|the carrier of S2 = Following(s2,n);
    thus Following(s,n+1)|the carrier of S2 = (Following Following(s,n))|the
    carrier of S2 by Th12
      .= Following Following(s2,n) by A1,A4,Th29
      .= Following(s2,n+1) by Th12;
  end;
  Following(s,0) = s by Th11;
  then
A5: P[0] by A2,Th11;
  thus for n being Nat holds P[n] from NAT_1:sch 2(A5,A3);
end;

theorem Th32:
  for S1,S2 being unsplit gate`1=arity gate`2isBoolean non void
  non empty ManySortedSign st InnerVertices S2 misses InputVertices S1 for A1
being Boolean gate`2=den Circuit of S1 for A2 being Boolean gate`2=den Circuit
  of S2 for s being State of A1+*A2, s1 being State of A1 st s1 = s|the carrier
  of S1 holds for v being set st v in the carrier of S1 for n being Nat holds (
  Following(s,n)).v = (Following(s1,n)).v
proof
  let S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty
  ManySortedSign such that
A1: InnerVertices S2 misses InputVertices S1;
  let A1 be Boolean gate`2=den Circuit of S1;
  let A2 be Boolean gate`2=den Circuit of S2;
  let s be State of A1+*A2, s1 be State of A1 such that
A2: s1 = s|the carrier of S1;
  let v be set;
  assume
A3: v in the carrier of S1;
  let n be Nat;
A4: the carrier of S1 = dom Following(s1,n) by CIRCUIT1:3;
  Following(s,n)|the carrier of S1 = Following(s1,n) by A1,A2,Th30;
  hence thesis by A3,A4,FUNCT_1:47;
end;

theorem Th33:
  for S1,S2 being unsplit gate`1=arity gate`2isBoolean non void
  non empty ManySortedSign st InnerVertices S1 misses InputVertices S2 for A1
being Boolean gate`2=den Circuit of S1 for A2 being Boolean gate`2=den Circuit
  of S2 for s being State of A1+*A2, s2 being State of A2 st s2 = s|the carrier
  of S2 holds for v being set st v in the carrier of S2 for n being Nat holds (
  Following(s,n)).v = (Following(s2,n)).v
proof
  let S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty
  ManySortedSign such that
A1: InnerVertices S1 misses InputVertices S2;
  let A1 be Boolean gate`2=den Circuit of S1;
  let A2 be Boolean gate`2=den Circuit of S2;
  let s be State of A1+*A2, s1 be State of A2 such that
A2: s1 = s|the carrier of S2;
  let v be set;
  assume
A3: v in the carrier of S2;
  let n be Nat;
A4: the carrier of S2 = dom Following(s1,n) by CIRCUIT1:3;
  Following(s,n)|the carrier of S2 = Following(s1,n) by A1,A2,Th31;
  hence thesis by A3,A4,FUNCT_1:47;
end;

registration
  let S be gate`2=den non void non empty ManySortedSign;
  let g be Gate of S;
  cluster g`2 -> Function-like Relation-like for set;
  coherence
  proof
    consider A being MSAlgebra over S such that
A1: A is gate`2=den by CIRCCOMB:def 11;
    g`2 = [g`1, (the Charact of A).g]`2 by A1
      .= (the Charact of A).g
      .= Den(g, A) by MSUALG_1:def 6;
    hence thesis;
  end;
end;

theorem Th34:
  for S being gate`2=den Circuit-like non void non empty
  ManySortedSign for A being non-empty Circuit of S st A is gate`2=den for s
being State of A, g being Gate of S holds (Following s).the_result_sort_of g =
  g`2.(s*the_arity_of g)
proof
  let S be gate`2=den Circuit-like non void non empty ManySortedSign;
  let A be non-empty Circuit of S such that
A1: for g being set st g in the carrier' of S holds g = [g`1, (the
  Charact of A).g];
  let s be State of A, g be Gate of S;
A2: Den(g, A) = (the Charact of A).g by MSUALG_1:def 6
    .= [g`1, (the Charact of A).g]`2
    .= g`2 by A1;
  set v = the_result_sort_of g;
  dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;
  then (the ResultSort of S).g in rng the ResultSort of S by FUNCT_1:def 3;
  then
A3: v in InnerVertices S by MSUALG_1:def 2;
  then g depends_on_in s = s*the_arity_of g & action_at v = g by CIRCUIT1:def 3
,MSAFREE2:def 7;
  hence thesis by A2,A3,CIRCUIT2:def 5;
end;

theorem Th35:
  for S being gate`1=arity gate`2isBoolean unsplit non void non
empty ManySortedSign for A being Boolean gate`2=den non-empty Circuit of S for
  s being State of A, p being FinSequence, f being Function st [p,f] in the
  carrier' of S holds (Following s).[p,f] = f.(s*p)
proof
  let S be gate`1=arity gate`2isBoolean unsplit non void non empty
  ManySortedSign;
  let A be Boolean gate`2=den non-empty Circuit of S;
  let s be State of A, p be FinSequence, f be Function;
  assume [p,f] in the carrier' of S;
  then reconsider g = [p,f] as Gate of S;
A1: g`1 = p & g`2 = f;
A2: the_result_sort_of g = (the ResultSort of S).g by MSUALG_1:def 2
    .= g by CIRCCOMB:44;
  the_arity_of g = (the Arity of S).g by MSUALG_1:def 1
    .= [(the Arity of S).g, g`2]`1
    .= g`1 by CIRCCOMB:def 8;
  hence thesis by A1,A2,Th34;
end;

theorem
  for S being gate`1=arity gate`2isBoolean unsplit non void non empty
  ManySortedSign for A being Boolean gate`2=den non-empty Circuit of S for s
  being State of A, p being FinSequence, f being Function st [p,f] in the
  carrier' of S & for x being set st x in rng p holds s is_stable_at x holds
  Following s is_stable_at [p,f]
proof
  let S be gate`1=arity gate`2isBoolean unsplit non void non empty
  ManySortedSign;
  let A be Boolean gate`2=den non-empty Circuit of S;
  let s be State of A, p be FinSequence, f be Function;
  assume [p,f] in the carrier' of S;
  then reconsider g = [p,f] as Gate of S;
A1: the_arity_of g = (the Arity of S).g by MSUALG_1:def 1
    .= [(the Arity of S).g, g`2]`1
    .= g`1 by CIRCCOMB:def 8
    .= p;
A2: the_result_sort_of g = (the ResultSort of S).g by MSUALG_1:def 2
    .= g by CIRCCOMB:44;
  assume for x being set st x in rng p holds s is_stable_at x;
  hence thesis by A1,A2,Th19;
end;

theorem Th37:
  for S being unsplit non empty ManySortedSign holds InnerVertices
  S = the carrier' of S
proof
  let S be unsplit non empty ManySortedSign;
  the ResultSort of S = id the carrier' of S by CIRCCOMB:def 7;
  hence thesis;
end;

begin :: One Gate Circuit

theorem Th38:
  for f being set, p being FinSequence holds InnerVertices
  1GateCircStr(p,f) is Relation
proof
  let f be set, p be FinSequence;
  InnerVertices 1GateCircStr(p,f) = {[p,f]} by CIRCCOMB:42;
  hence thesis;
end;

theorem
  for f being set, p being nonpair-yielding FinSequence holds
  InputVertices 1GateCircStr(p,f) is without_pairs
proof
  let f be set, p be nonpair-yielding FinSequence;
  InputVertices 1GateCircStr(p,f) = rng p by CIRCCOMB:42;
  hence thesis;
end;

theorem Th40:
  for f,x,y being object holds InputVertices 1GateCircStr(
  <*x,y*>,f) = {x,y}
proof
  let f, x,y be object;
  set p = <*x,y*>;
  thus InputVertices 1GateCircStr(p,f) = rng p by CIRCCOMB:42
    .= {x,y} by FINSEQ_2:127;
end;

theorem Th41:
  for f being set, x,y being non pair object holds InputVertices
  1GateCircStr(<*x,y*>,f) is without_pairs
proof
  let f be set, x,y be non pair object;
  set p = <*x,y*>;
  let z be pair object;
  assume
A1: z in InputVertices 1GateCircStr(p,f);
  InputVertices 1GateCircStr(p,f) = {x,y} by Th40;
  hence thesis by A1,TARSKI:def 2;
end;

theorem Th42:
  for f,x,y,z being object holds InputVertices
  1GateCircStr(<*x,y,z*>,f) = {x,y,z}
proof
  let f, x,y,z be object;
  set p = <*x,y,z*>;
  thus InputVertices 1GateCircStr(p,f) = rng p by CIRCCOMB:42
    .= {x,y,z} by FINSEQ_2:128;
end;

theorem Th43:
  for x,y,f being object holds x in the carrier of 1GateCircStr(<*x,y
  *>,f) & y in the carrier of 1GateCircStr(<*x,y*>,f) & [<*x,y*>,f] in the
  carrier of 1GateCircStr(<*x,y*>,f)
proof
  let x,y,f be object;
  set p = <*x,y*>;
  x in {x,y} by TARSKI:def 2;
  then
A1: x in rng p by FINSEQ_2:127;
  y in {x,y} by TARSKI:def 2;
  then
A2: y in rng p by FINSEQ_2:127;
  the carrier of 1GateCircStr(p,f) = rng p \/ {[p,f]} & [p,f] in {[p,f]}
  by CIRCCOMB:def 6,TARSKI:def 1;
  hence thesis by A1,A2,XBOOLE_0:def 3;
end;

theorem Th44:
  for x,y,z,f being object holds x in the carrier of 1GateCircStr(<*x
,y,z*>,f) & y in the carrier of 1GateCircStr(<*x,y,z*>,f) & z in the carrier of
  1GateCircStr(<*x,y,z*>,f)
proof
  let x,y,z,f be object;
  set p = <*x,y,z*>;
  set A = the carrier of 1GateCircStr(p,f);
  y in {x,y,z} by ENUMSET1:def 1;
  then
A1: y in rng p by FINSEQ_2:128;
  z in {x,y,z} by ENUMSET1:def 1;
  then
A2: z in rng p by FINSEQ_2:128;
  x in {x,y,z} by ENUMSET1:def 1;
  then A = rng p \/ {[p,f]} & x in rng p by CIRCCOMB:def 6,FINSEQ_2:128;
  hence thesis by A1,A2,XBOOLE_0:def 3;
end;

theorem
  for f,x being set, p being FinSequence holds x in the carrier of
  1GateCircStr(p,f,x) & for y being set st y in rng p holds y in the carrier of
  1GateCircStr(p,f,x)
proof
  let f,x be set;
  let p be FinSequence;
  set A = the carrier of 1GateCircStr(p,f,x);
  A = rng p \/ {x} & x in {x} by CIRCCOMB:def 5,TARSKI:def 1;
  hence thesis by XBOOLE_0:def 3;
end;

theorem
  for f,x being set, p being FinSequence holds 1GateCircStr(p,f,x) is
  gate`1=arity Circuit-like
proof
  let f,x be set;
  let p be FinSequence;
  set S = 1GateCircStr(p,f,x);
  thus S is gate`1=arity
  proof
    let g be set;
    assume g in the carrier' of S;
    then g in {[p,f]} by CIRCCOMB:def 5;
    then
A1: g = [p,f] by TARSKI:def 1;
    thus thesis by A1,CIRCCOMB:def 5;
  end;
  thus S is Circuit-like
  proof
    let S9 be non void non empty ManySortedSign such that
A2: S9 = S;
    let o1, o2 be OperSymbol of S9;
    o1 = [p,f] by A2,CIRCCOMB:37;
    hence thesis by A2,CIRCCOMB:37;
  end;
end;

theorem Th47:
  for p being FinSequence, f be set holds [p,f] in InnerVertices
  1GateCircStr(p,f)
proof
  let p be FinSequence, f be set;
  InnerVertices 1GateCircStr(p,f) = {[p,f]} by CIRCCOMB:42;
  hence thesis by TARSKI:def 1;
end;

definition
  let x,y be object;
  let f be Function of 2-tuples_on BOOLEAN, BOOLEAN;
  func 1GateCircuit(x,y,f) -> Boolean gate`2=den strict Circuit of
  1GateCircStr(<*x,y*>, f) equals
  1GateCircuit(<*x,y*> qua FinSeqLen of 2, f);
  coherence by CIRCCOMB:61;
end;

reserve x,y,z,c for object,
  f for Function of 2-tuples_on BOOLEAN, BOOLEAN;

theorem Th48:
  for X being finite non empty set, f being Function of 2
-tuples_on X, X for s being State of 1GateCircuit(<*x,y*>,f) holds (Following s
).[<*x,y*>, f] = f.<*s.x, s.y*> & (Following s).x = s.x & (Following s).y = s.y
proof
  let X be finite non empty set, f be Function of 2-tuples_on X, X;
  let s be State of 1GateCircuit(<*x,y*>,f);
  set p = <*x,y*>;
  dom s = the carrier of 1GateCircStr(p, f) by CIRCUIT1:3;
  then
A1: dom s = rng p \/ {[p,f]} by CIRCCOMB:def 6;
  y in {x,y} by TARSKI:def 2;
  then y in rng p by FINSEQ_2:127;
  then
A2: y in dom s by A1,XBOOLE_0:def 3;
  x in {x,y} by TARSKI:def 2;
  then x in rng p by FINSEQ_2:127;
  then
A3: x in dom s by A1,XBOOLE_0:def 3;
  thus (Following s).[<*x,y*>, f] = f.(s*<*x,y*>) by CIRCCOMB:56
    .= f.<*s.x, s.y*> by A3,A2,FINSEQ_2:125;
  reconsider x, y as Vertex of 1GateCircStr(p,f) by Th43;
  InputVertices 1GateCircStr(p,f) = rng p by CIRCCOMB:42
    .= {x,y} by FINSEQ_2:127;
  then
  x in InputVertices 1GateCircStr(p,f) & y in InputVertices 1GateCircStr(
  p,f) by TARSKI:def 2;
  hence thesis by CIRCUIT2:def 5;
end;

theorem Th49:
  for X being finite non empty set, f being Function of 2
-tuples_on X, X for s being State of 1GateCircuit(<*x,y*>,f) holds Following s
  is stable
proof
  let X be finite non empty set, f be Function of 2-tuples_on X, X;
  set S = 1GateCircStr(<*x,y*>,f);
  let s be State of 1GateCircuit(<*x,y*>,f);
  set s1 = Following s, s2 = Following s1;
  set p = <*x,y*>;
A1: the carrier of S = rng p \/ {[p,f]} by CIRCCOMB:def 6
    .= {x,y} \/ {[p,f]} by FINSEQ_2:127;
A2: now
    let a be object;
A3: s2.[p,f] = f.<*s1.x, s1.y*> by Th48;
    assume a in the carrier of S;
    then a in {x,y} or a in {[p,f]} by A1,XBOOLE_0:def 3;
    then
A4: a = x or a = y or a = [p,f] by TARSKI:def 1,def 2;
    s1.x = s.x & s1.y = s.y by Th48;
    hence s2.a = s1.a by A4,A3,Th48;
  end;
  dom s1 = the carrier of S & dom s2 = the carrier of S by CIRCUIT1:3;
  hence Following s = Following Following s by A2,FUNCT_1:2;
end;

theorem
  for s being State of 1GateCircuit(x,y,f) holds (Following s).[<*x,y*>,
  f] = f.<*s.x, s.y*> & (Following s).x = s.x & (Following s).y = s.y by Th48;

theorem
  for s being State of 1GateCircuit(x,y,f) holds Following s is stable by Th49;

definition
  let x,y,z be object;
  let f be Function of 3-tuples_on BOOLEAN, BOOLEAN;
  func 1GateCircuit(x,y,z,f) -> Boolean gate`2=den strict Circuit of
  1GateCircStr(<*x,y,z*>, f) equals
  1GateCircuit(<*x,y,z*>, f);
  coherence by CIRCCOMB:61;
end;

theorem Th52:
  for X being finite non empty set, f being Function of 3
-tuples_on X, X for s being State of 1GateCircuit(<*x,y,z*>,f) holds (Following
s).[<*x,y,z*>, f] = f.<*s.x, s.y, s.z*> & (Following s).x = s.x & (Following s)
  .y = s.y & (Following s).z = s.z
proof
  let X be finite non empty set, f be Function of 3-tuples_on X, X;
  let s be State of 1GateCircuit(<*x,y,z*>,f);
  set p = <*x,y,z*>;
  dom s = the carrier of 1GateCircStr(p, f) by CIRCUIT1:3;
  then
A1: dom s = rng p \/ {[p,f]} by CIRCCOMB:def 6;
  y in {x,y,z} by ENUMSET1:def 1;
  then y in rng p by FINSEQ_2:128;
  then
A2: y in dom s by A1,XBOOLE_0:def 3;
  x in {x,y,z} by ENUMSET1:def 1;
  then x in rng p by FINSEQ_2:128;
  then
A3: x in dom s by A1,XBOOLE_0:def 3;
  z in {x,y,z} by ENUMSET1:def 1;
  then z in rng p by FINSEQ_2:128;
  then
A4: z in dom s by A1,XBOOLE_0:def 3;
  thus (Following s).[p, f] = f.(s*p) by CIRCCOMB:56
    .= f.<*s.x, s.y, s.z*> by A3,A2,A4,FINSEQ_2:126;
  reconsider x, y, z as Vertex of 1GateCircStr(p,f) by Th44;
A5: InputVertices 1GateCircStr(p,f) = rng p by CIRCCOMB:42
    .= {x,y,z} by FINSEQ_2:128;
  then
A6: z in InputVertices 1GateCircStr(p,f) by ENUMSET1:def 1;
  x in InputVertices 1GateCircStr(p,f) & y in InputVertices 1GateCircStr(
  p,f) by A5,ENUMSET1:def 1;
  hence thesis by A6,CIRCUIT2:def 5;
end;

theorem Th53:
  for X being finite non empty set, f being Function of 3
-tuples_on X, X for s being State of 1GateCircuit(<*x,y,z*>,f) holds Following
  s is stable
proof
  let X be finite non empty set, f be Function of 3-tuples_on X, X;
  set p = <*x,y,z*>;
  set S = 1GateCircStr(p,f);
  let s be State of 1GateCircuit(p,f);
  set s1 = Following s, s2 = Following s1;
A1: the carrier of S = rng p \/ {[p,f]} by CIRCCOMB:def 6
    .= {x,y,z} \/ {[p,f]} by FINSEQ_2:128;
A2: now
    let a be object;
A3: s1.z = s.z & s2.[p,f] = f.<*s1.x, s1.y, s1.z*> by Th52;
    assume a in the carrier of S;
    then a in {x,y,z} or a in {[p,f]} by A1,XBOOLE_0:def 3;
    then
A4: a = x or a = y or a = z or a = [p,f] by ENUMSET1:def 1,TARSKI:def 1;
    s1.x = s.x & s1.y = s.y by Th52;
    hence s2.a = s1.a by A4,A3,Th52;
  end;
  dom s1 = the carrier of S & dom s2 = the carrier of S by CIRCUIT1:3;
  hence Following s = Following Following s by A2,FUNCT_1:2;
end;

theorem
  for f being Function of 3-tuples_on BOOLEAN, BOOLEAN for s being State
of 1GateCircuit(x,y,z,f) holds (Following s).[<*x,y,z*>, f] = f.<*s.x, s.y, s.z
  *> & (Following s).x = s.x & (Following s).y = s.y & (Following s).z = s.z
by Th52;

theorem
  for f being Function of 3-tuples_on BOOLEAN, BOOLEAN for s being State
  of 1GateCircuit(x,y,z,f) holds Following s is stable by Th53;

begin :: Two Gates Circuit

definition
  let x,y,c be object;
  let f be Function of 2-tuples_on BOOLEAN, BOOLEAN;
  func 2GatesCircStr(x,y,c,f) -> unsplit gate`1=arity gate`2isBoolean non void
  strict non empty ManySortedSign equals
  1GateCircStr(<*x,y*>, f) +* 1GateCircStr
  (<*[<*x,y*>, f], c*>, f);
  correctness;
end;

definition
  let x,y,c be object;
  let f be Function of 2-tuples_on BOOLEAN, BOOLEAN;
  func 2GatesCircOutput(x,y,c,f) -> Element of InnerVertices 2GatesCircStr(x,y
  ,c,f) equals
  [<*[<*x,y*>, f], c*>, f];
  coherence
  proof
    set p = <*[<*x,y*>, f], c*>;
    set S2 = 1GateCircStr(p, f);
    [p,f] in InnerVertices S2 by Th47;
    hence thesis by Th21;
  end;
  correctness;
end;

registration
  let x,y,c be object;
  let f be Function of 2-tuples_on BOOLEAN, BOOLEAN;
  cluster 2GatesCircOutput(x,y,c,f) -> pair;
  coherence;
end;

theorem Th56:
  InnerVertices 2GatesCircStr(x,y,c,f) = {[<*x,y*>, f],
  2GatesCircOutput(x,y,c,f)}
proof
  set p = <*[<*x,y*>, f], c*>;
  set S1 = 1GateCircStr(<*x,y*>, f), S2 = 1GateCircStr(p, f);
  set S = 2GatesCircStr(x,y,c,f);
  S1 tolerates S2 by CIRCCOMB:43;
  hence InnerVertices S = (InnerVertices S1) \/ (InnerVertices S2) by
CIRCCOMB:11
    .= {[<*x,y*>, f]} \/ (InnerVertices S2) by CIRCCOMB:42
    .= {[<*x,y*>, f]} \/ {[p, f]} by CIRCCOMB:42
    .= {[<*x,y*>, f], 2GatesCircOutput(x,y,c,f)} by ENUMSET1:1;
end;

theorem Th57:
  c <> [<*x,y*>, f] implies InputVertices 2GatesCircStr(x,y,c,f) = {x,y,c}
proof
  assume
A1: c <> [<*x,y*>, f];
  set S = 2GatesCircStr(x,y,c,f);
  set S1 = 1GateCircStr(<*x,y*>, f);
  set p = <*[<*x,y*>, f], c*>;
  set S2 = 1GateCircStr(p, f);
  set R = the ResultSort of S;
A2: the carrier of S = (the carrier of S1) \/ the carrier of S2 by
CIRCCOMB:def 2;
A3: rng <*x,y*> = {x,y} by FINSEQ_2:127;
  then
A4: the carrier of S1 = {x,y} \/ {[<*x,y*>,f]} by CIRCCOMB:def 6;
A5: rng R = {[<*x,y*>, f], 2GatesCircOutput(x,y,c,f)} by Th56
    .= {[<*x,y*>, f], [p,f]};
A6: rng p = {[<*x,y*>, f], c} by FINSEQ_2:127;
  then
A7: the carrier of S2 = {[<*x,y*>, f], c} \/ {[p,f]} by CIRCCOMB:def 6;
  thus InputVertices S c= {x,y,c}
  proof
    let z be object;
    assume
A8: z in InputVertices S;
    then z in the carrier of S1 or z in the carrier of S2 by A2,XBOOLE_0:def 3;
    then
    z in {x,y} or z in {[<*x,y*>,f]} or z in {[<*x,y*>, f], c} or z in {[
    p,f]} by A4,A7,XBOOLE_0:def 3;
    then
A9: z = x or z = y or z = [<*x,y*>,f] or z = c or z = [p,f] by TARSKI:def 1
,def 2;
    not z in rng R by A8,XBOOLE_0:def 5;
    hence thesis by A5,A9,ENUMSET1:def 1,TARSKI:def 2;
  end;
  let z be object;
   reconsider zz=z as set by TARSKI:1;
  assume z in {x,y,c};
  then
A10: z = x or z = y or z = c by ENUMSET1:def 1;
  then z in {x,y} or z in rng p by A6,TARSKI:def 2;
  then z in InputVertices S1 or z in InputVertices S2 by A3,CIRCCOMB:42;
  then
A11: z in the carrier of S by A2,XBOOLE_0:def 3;
  z in {x,y} & [<*x,y*>, f] in rng p or z in {c} by A6,A10,TARSKI:def 1,def 2;
  then
A12: the_rank_of zz in the_rank_of [<*x,y*>, f] & the_rank_of [<*x,y*>, f] in
  the_rank_of [p,f] or z = c & c in rng p by A3,A6,CLASSES1:82,TARSKI:def 1
,def 2;
  then the_rank_of zz in the_rank_of [p,f] by CLASSES1:82,ORDINAL1:10;
  then
A13: z <> [p,f];
  z <> [<*x,y*>, f] by A1,A12;
  then not z in rng R by A5,A13,TARSKI:def 2;
  hence thesis by A11,XBOOLE_0:def 5;
end;

definition
  let x,y,c be object;
  let f be Function of 2-tuples_on BOOLEAN, BOOLEAN;
  func 2GatesCircuit(x,y,c,f) -> strict Boolean gate`2=den Circuit of
  2GatesCircStr(x,y,c,f) equals
  1GateCircuit(x,y, f) +* 1GateCircuit([<*x,y*>, f], c, f);
  coherence;
end;

theorem Th58:
  InnerVertices 2GatesCircStr(x,y,c,f) is Relation
proof
  InnerVertices 2GatesCircStr(x,y,c,f) = {[<*x,y*>, f], 2GatesCircOutput(x
  ,y,c,f)} by Th56;
  hence thesis;
end;

theorem Th59:
  for x,y,c being non pair object
   holds InputVertices 2GatesCircStr(x,y,c,f) is without_pairs
proof
  let x,y,c be non pair object;
  InputVertices 2GatesCircStr(x,y,c,f) = {x,y,c} by Th57;
  hence thesis;
end;

theorem Th60:
  x in the carrier of 2GatesCircStr(x,y,c,f) & y in the carrier of
  2GatesCircStr(x,y,c,f) & c in the carrier of 2GatesCircStr(x,y,c,f)
proof
  set S1 = 1GateCircStr(<*x,y*>, f);
  set S2 = 1GateCircStr(<*[<*x,y*>, f], c*>, f);
A1: c in the carrier of S2 by Th43;
  x in the carrier of S1 & y in the carrier of S1 by Th43;
  hence thesis by A1,Th20;
end;

theorem
  [<*x,y*>,f] in the carrier of 2GatesCircStr(x,y,c,f) & [<*[<*x,y*>,f],
  c*>, f] in the carrier of 2GatesCircStr(x,y,c,f)
proof
  set S1 = 1GateCircStr(<*x,y*>, f);
  set S2 = 1GateCircStr(<*[<*x,y*>, f], c*>, f);
  [<*x,y*>, f] in the carrier of S1 & [<*[<*x,y*>,f], c*>, f] in the
  carrier of S2 by Th43;
  hence thesis by Th20;
end;

definition
  let S be unsplit non void non empty ManySortedSign;
  let A be Boolean Circuit of S;
  let s be State of A;
  let v be Vertex of S;
  redefine func s.v -> Element of BOOLEAN;  :: redefines . (FUNCT_1, definition)
  coherence
  proof
    s.v in (the Sorts of A).v by CIRCUIT1:4;
    hence thesis by CIRCCOMB:def 14;
  end;
end;

reserve s for State of 2GatesCircuit(x,y,c,f);

Lm1: c <> [<*x,y*>, f] implies (Following s).2GatesCircOutput(x,y,c,f) = f.<*s
.[<*x,y*>,f], s.c*> & (Following s).[<*x,y*>,f] = f.<*s.x, s.y*> & (Following s
).x = s.x & (Following s).y = s.y & (Following s).c = s.c
proof
  set S1 = 1GateCircStr(<*x,y*>, f), A1 = 1GateCircuit(x,y, f);
  reconsider vx = x, vy = y as Vertex of S1 by Th43;
  reconsider s1 = s|the carrier of S1 as State of A1 by Th26;
  set p = <*[<*x,y*>, f], c*>;
  set xyf = [<*x,y*>,f];
  set S2 = 1GateCircStr(p, f), A2 = 1GateCircuit(xyf,c, f);
  set S = 2GatesCircStr(x,y,c,f);
A1: dom s1 = the carrier of S1 by CIRCUIT1:3;
  reconsider v2 = [p,f] as Element of InnerVertices S2 by Th47;
  InnerVertices S = {[<*x,y*>, f], 2GatesCircOutput(x,y,c,f)} by Th56;
  then reconsider xyf as Element of InnerVertices S by TARSKI:def 2;
A2: rng p = {xyf,c} by FINSEQ_2:127;
  then c in rng p by TARSKI:def 2;
  then
A3: c in InputVertices S2 by CIRCCOMB:42;
  xyf in rng p by A2,TARSKI:def 2;
  then xyf in InputVertices S2 by CIRCCOMB:42;
  then reconsider xyf9 = xyf, c9 = c as Vertex of S2 by A3;
  reconsider xyf1 = xyf as Element of InnerVertices S1 by Th47;
  reconsider s2 = s|the carrier of S2 as State of A2 by Th26;
A4: dom s2 = the carrier of S2 by CIRCUIT1:3;
  assume c <> [<*x,y*>, f];
  then
A5: InputVertices S = {x,y,c} by Th57;
  then
A6: c in InputVertices S by ENUMSET1:def 1;
  thus (Following s).2GatesCircOutput(x,y,c,f) = (Following s2).v2 by
CIRCCOMB:64
    .= f.<*s2.xyf9, s2.c9*> by Th48
    .= f.<*s.[<*x,y*>,f], s2.c9*> by A4,FUNCT_1:47
    .= f.<*s.[<*x,y*>,f], s.c*> by A4,FUNCT_1:47;
  thus (Following s).[<*x,y*>,f] = (Following s1).xyf1 by CIRCCOMB:64
    .= f.<*s1.vx, s1.vy*> by Th48
    .= f.<*s.x, s1.vy*> by A1,FUNCT_1:47
    .= f.<*s.x, s.y*> by A1,FUNCT_1:47;
  x in InputVertices S & y in InputVertices S by A5,ENUMSET1:def 1;
  hence thesis by A6,CIRCUIT2:def 5;
end;

theorem Th62:
  c <> [<*x,y*>, f] implies (Following(s,2)).2GatesCircOutput(x,y,
c,f) = f.<*f.<*s.x, s.y*>, s.c*> & (Following(s,2)).[<*x,y*>,f] = f.<*s.x, s.y
*> & (Following(s,2)).x = s.x & (Following(s,2)).y = s.y & (Following(s,2)).c =
  s.c
proof
  set S = 2GatesCircStr(x,y,c,f);
A1: rng <*x,y*> = {x,y} by FINSEQ_2:127;
  reconsider xx = x, yy = y, cc = c as Vertex of S by Th60;
  set p = <*[<*x,y*>, f], c*>;
  set xyf = [<*x,y*>,f];
  set S1 = 1GateCircStr(<*x,y*>, f), A1 = 1GateCircuit(x,y, f);
  set S2 = 1GateCircStr(p, f), A2 = 1GateCircuit(xyf,c, f);
A2: x in {x,y} by TARSKI:def 2;
  assume c <> [<*x,y*>, f];
  then
A3: InputVertices S = {x,y,c} by Th57;
  then
A4: x in InputVertices S by ENUMSET1:def 1;
  then
A5: (Following s).xx = s.x by CIRCUIT2:def 5;
  InnerVertices S = {[<*x,y*>, f], 2GatesCircOutput(x,y,c,f)} by Th56;
  then reconsider xyf as Element of InnerVertices S by TARSKI:def 2;
A6: rng p = {xyf,c} by FINSEQ_2:127;
  then c in rng p by TARSKI:def 2;
  then
A7: c in InputVertices S2 by CIRCCOMB:42;
  xyf in rng p by A6,TARSKI:def 2;
  then xyf in InputVertices S2 by CIRCCOMB:42;
  then reconsider xyf9 = xyf, c9 = c as Vertex of S2 by A7;
  reconsider vx = x, vy = y as Vertex of S1 by Th43;
  set fs = Following s;
  reconsider fs1 = fs|the carrier of S1 as State of A1 by Th26;
A8: y in {x,y} by TARSKI:def 2;
  reconsider fs2 = fs|the carrier of S2 as State of A2 by Th26;
  reconsider s1 = s|the carrier of S1 as State of A1 by Th26;
A9: dom fs2 = the carrier of S2 by CIRCUIT1:3;
A10: c in InputVertices S by A3,ENUMSET1:def 1;
  then (Following s).cc = s.c by CIRCUIT2:def 5;
  then
A11: (Following Following s).cc = s.c by A10,CIRCUIT2:def 5;
  reconsider xyf1 = xyf as Element of InnerVertices S1 by Th47;
A12: dom fs1 = the carrier of S1 by CIRCUIT1:3;
  reconsider v2 = [p,f] as Element of InnerVertices S2 by Th47;
A13: xyf in InnerVertices S1 by Th47;
A14: dom s1 = the carrier of S1 & InputVertices S1 = rng <*x,y*> by CIRCCOMB:42
,CIRCUIT1:3;
A15: Following(s,1+1) = Following Following s by Th15;
  hence (Following(s,2)).2GatesCircOutput(x,y,c,f) = (Following fs2).v2 by
CIRCCOMB:64
    .= f.<*fs2.xyf9, fs2.c9*> by Th48
    .= f.<*(Following s).xyf, fs2.c*> by A9,FUNCT_1:47
    .= f.<*(Following s).xyf, (Following s).c9*> by A9,FUNCT_1:47
    .= f.<*(Following s).xyf, s.cc*> by A10,CIRCUIT2:def 5
    .= f.<*(Following s1).xyf, s.cc*> by A13,CIRCCOMB:64
    .= f.<*f.<*s1.x, s1.y*>, s.cc*> by Th48
    .= f.<*f.<*s.x,s1.y*>, s.cc*> by A2,A14,A1,FUNCT_1:47
    .= f.<*f.<*s.x,s.y*>, s.c*> by A8,A14,A1,FUNCT_1:47;
A16: y in InputVertices S by A3,ENUMSET1:def 1;
  then
A17: (Following s).yy = s.y by CIRCUIT2:def 5;
  then
A18: (Following Following s).yy = s.y by A16,CIRCUIT2:def 5;
  thus (Following(s,2)).[<*x,y*>,f] = (Following fs1).xyf1 by A15,CIRCCOMB:64
    .= f.<*fs1.vx, fs1.vy*> by Th48
    .= f.<*s.x, fs1.vy*> by A5,A12,FUNCT_1:47
    .= f.<*s.x, s.y*> by A17,A12,FUNCT_1:47;
  (Following Following s).xx = s.x by A4,A5,CIRCUIT2:def 5;
  hence thesis by A18,A11,Th15;
end;

theorem Th63:
  c <> [<*x,y*>, f] implies Following(s,2) is stable
proof
  set S = 2GatesCircStr(x,y,c,f);
  assume
A1: c <> [<*x,y*>, f];
  now
    thus dom Following Following(s,2) = the carrier of S & dom Following(s,2)
    = the carrier of S by CIRCUIT1:3;
    let a be object;
A2: InputVertices S \/ InnerVertices S = the carrier of S by XBOOLE_1:45;
    assume a in the carrier of S;
    then reconsider v = a as Vertex of S;
A3: InnerVertices S = {[<*x,y*>, f], 2GatesCircOutput(x,y,c,f)} by Th56;
A4: (Following(s,2)).c = s.c by A1,Th62;
A5: (Following(s,2)).x = s.x & (Following(s,2)).y = s.y by A1,Th62;
A6: (Following(s,2)).[<*x,y*>,f] = f.<*s.x, s.y*> & (Following(s,2)).
    2GatesCircOutput(x,y,c,f) = f.<*f.<*s.x, s.y*>, s.c*> by A1,Th62;
A7: InputVertices S = {x,y,c} by A1,Th57;
    per cases by A2,XBOOLE_0:def 3;
    suppose
      v in InputVertices S;
      then v = x or v = y or v = c by A7,ENUMSET1:def 1;
      hence (Following Following(s,2)).a = (Following(s,2)).a by A1,Lm1;
    end;
    suppose
      v in InnerVertices S;
      then v = [<*x,y*>, f] or v = 2GatesCircOutput(x,y,c,f) by A3,TARSKI:def 2
;
      hence (Following Following(s,2)).a = (Following(s,2)).a by A1,A6,A5,A4
,Lm1;
    end;
  end;
  hence Following(s,2) = Following Following(s,2) by FUNCT_1:2;
end;

theorem Th64:
  c <> [<*x,y*>, 'xor'] implies for s being State of 2GatesCircuit
(x,y,c,'xor') for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3
= s.c holds (Following(s,2)).2GatesCircOutput(x,y,c,'xor') = a1 'xor' a2 'xor'
  a3
proof
  set f = 'xor';
  assume
A1: c <> [<*x,y*>, f];
  let s be State of 2GatesCircuit(x,y,c,f);
  let a1,a2,a3 be Element of BOOLEAN;
  assume a1 = s.x & a2 = s.y & a3 = s.c;
  hence (Following(s,2)).2GatesCircOutput(x,y,c,f) = f.<*f.<*a1, a2*>, a3*> by
A1,Th62
    .= f.<*a1 'xor' a2, a3*> by Def3
    .= a1 'xor' a2 'xor' a3 by Def3;
end;

theorem
  c <> [<*x,y*>, 'or'] implies for s being State of 2GatesCircuit(x,y,c,
  'or') for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3 = s.c
  holds (Following(s,2)).2GatesCircOutput(x,y,c,'or') = a1 'or' a2 'or' a3
proof
  set f = 'or';
  assume
A1: c <> [<*x,y*>, f];
  let s be State of 2GatesCircuit(x,y,c,f);
  let a1,a2,a3 be Element of BOOLEAN;
  assume a1 = s.x & a2 = s.y & a3 = s.c;
  hence (Following(s,2)).2GatesCircOutput(x,y,c,f) = f.<*f.<*a1, a2*>, a3*> by
A1,Th62
    .= f.<*a1 'or' a2, a3*> by Def4
    .= a1 'or' a2 'or' a3 by Def4;
end;

theorem
  c <> [<*x,y*>, '&'] implies for s being State of 2GatesCircuit(x,y,c,
  '&') for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3 = s.c
  holds (Following(s,2)).2GatesCircOutput(x,y,c,'&') = a1 '&' a2 '&' a3
proof
  set f = '&';
  assume
A1: c <> [<*x,y*>, f];
  let s be State of 2GatesCircuit(x,y,c,f);
  let a1,a2,a3 be Element of BOOLEAN;
  assume a1 = s.x & a2 = s.y & a3 = s.c;
  hence (Following(s,2)).2GatesCircOutput(x,y,c,f) = f.<*f.<*a1, a2*>, a3*> by
A1,Th62
    .= f.<*a1 '&' a2, a3*> by Def5
    .= a1 '&' a2 '&' a3 by Def5;
end;

begin :: Bit Adder Circuit

definition
  let x,y,c be object;
  func BitAdderOutput(x,y,c) -> Element of InnerVertices 2GatesCircStr(x,y,c,
  'xor') equals
  2GatesCircOutput(x,y,c, 'xor');
  coherence;
end;

definition
  let x,y,c be object;
  func BitAdderCirc(x,y,c) -> strict Boolean gate`2=den Circuit of
  2GatesCircStr(x,y,c, 'xor') equals
  2GatesCircuit(x,y,c, 'xor');
  coherence;
end;

definition
  let x,y,c be object;
  func MajorityIStr(x,y,c) -> unsplit gate`1=arity gate`2isBoolean non void
  strict non empty ManySortedSign equals
  1GateCircStr(<*x,y*>, '&') +*
  1GateCircStr(<*y,c*>, '&') +* 1GateCircStr(<*c,x*>, '&');
  correctness;
end;

definition
  let x,y,c be object;
  func MajorityStr(x,y,c) -> unsplit gate`1=arity gate`2isBoolean non void
  strict non empty ManySortedSign equals
  MajorityIStr(x,y,c) +* 1GateCircStr(<*[
  <*x,y*>, '&'], [<*y,c*>, '&'], [<*c,x*>, '&']*>, or3);
  correctness;
end;

definition
  let x,y,c be object;
  func MajorityICirc(x,y,c) -> strict Boolean gate`2=den Circuit of
  MajorityIStr(x,y,c) equals
  1GateCircuit(x,y, '&') +* 1GateCircuit(y,c, '&') +*
  1GateCircuit(c,x, '&');
  coherence;
end;

theorem Th67:
  InnerVertices MajorityStr(x,y,c) is Relation
proof
A1: InnerVertices 1GateCircStr(<*[<*x,y*>, '&'], [<*y,c*>, '&'], [<*c,x*>,
  '&']*>, or3) is Relation by Th38;
  InnerVertices 1GateCircStr(<*x,y*>,'&') is Relation & InnerVertices
  1GateCircStr(<*y,c*>,'&') is Relation by Th38;
  then
A2: InnerVertices (1GateCircStr(<*x,y*>,'&')+*1GateCircStr(<*y,c*>,'&')) is
  Relation by Th2,CIRCCOMB:47;
  InnerVertices 1GateCircStr(<*c,x*>,'&') is Relation by Th38;
  then InnerVertices MajorityIStr(x,y,c) is Relation by A2,Th2,CIRCCOMB:47;
  hence thesis by A1,Th2,CIRCCOMB:47;
end;

theorem Th68:
  for x,y,c being non pair object holds InputVertices MajorityStr(x,y
  ,c) is without_pairs
proof
  let x,y,c be non pair object;
  set M = MajorityStr(x,y,c), MI = MajorityIStr(x,y,c);
  set S = 1GateCircStr(<*[<*x,y*>, '&'], [<*y,c*>, '&'], [<*c,x*>, '&']*>, or3
  );
  given xx being pair object such that
A1: xx in InputVertices M;
A2: 1GateCircStr(<*x,y*>, '&') tolerates 1GateCircStr(<*y,c*>, '&') by
CIRCCOMB:43;
  1GateCircStr(<*x,y*>, '&') tolerates 1GateCircStr(<*c,x*>, '&') &
1GateCircStr(<*y,c*>, '&') tolerates 1GateCircStr(<*c,x*>, '&') by CIRCCOMB:43;
  then
A3: 1GateCircStr(<*x,y*>, '&') +* 1GateCircStr(<*y,c*>, '&') tolerates
  1GateCircStr(<*c,x*>, '&') by A2,CIRCCOMB:3;
  InnerVertices 1GateCircStr(<*x,y*>, '&') = {[<*x,y*>, '&']} &
  InnerVertices 1GateCircStr(<*y,c*>, '&') = {[<*y,c*>, '&']} by CIRCCOMB:42;
  then InnerVertices 1GateCircStr(<*c,x*>, '&') = {[<*c,x*>, '&']} &
InnerVertices (1GateCircStr(<*x,y*>, '&') +* 1GateCircStr(<*y,c*>, '&')) = {[<*
  x,y*>, '&']} \/ {[<*y,c*>, '&']} by A2,CIRCCOMB:11,42;
  then
A4: InnerVertices MI = {[<*x,y*>,'&']} \/ {[<*y,c*>,'&']} \/ {[<*c,x*>, '&'
  ]} by A3,CIRCCOMB:11
    .= {[<*x,y*>,'&'], [<*y,c*>,'&']} \/ {[<*c,x*>,'&']} by ENUMSET1:1
    .= {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} by ENUMSET1:3;
  InputVertices S = {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} by Th42;
  then
A5: InputVertices S \ InnerVertices MI = {} by A4,XBOOLE_1:37;
  InputVertices 1GateCircStr(<*x,y*>,'&') is without_pairs & InputVertices
  1GateCircStr(<*y,c*>,'&') is without_pairs by Th41;
  then
A6: InputVertices (1GateCircStr(<*x,y*>,'&')+*1GateCircStr(<*y,c*>,'&')) is
  without_pairs by Th8,CIRCCOMB:47;
  InputVertices 1GateCircStr(<*c,x*>,'&') is without_pairs by Th41;
  then
A7: InputVertices MI is without_pairs by A6,Th8,CIRCCOMB:47;
  InnerVertices S is Relation by Th38;
  then
  InputVertices M = (InputVertices MI) \/ (InputVertices S \ InnerVertices
  MI) by A7,Th6;
  hence thesis by A7,A1,A5;
end;

theorem
  for s being State of MajorityICirc(x,y,c), a,b being Element of
  BOOLEAN st a = s.x & b = s.y holds (Following s).[<*x,y*>, '&'] = a '&' b
proof
  set xy = <*x,y*>;
  set S1 = 1GateCircStr(xy, '&'), A1 = 1GateCircuit(x,y, '&');
  reconsider xx = x, yy = y as Vertex of S1 by Th43;
  reconsider v1 = [xy, '&'] as Element of InnerVertices S1 by Th47;
  set S2 = 1GateCircStr(<*y,c*>, '&'), A2 = 1GateCircuit(y,c, '&');
  set S3 = 1GateCircStr(<*c,x*>, '&'), A3 = 1GateCircuit(c,x, '&');
  set S = MajorityIStr(x,y,c), A = MajorityICirc(x,y,c);
  let s be State of A;
  let a,b be Element of BOOLEAN such that
A1: a = s.x & b = s.y;
A2: A = A1+*(A2+*A3) by Th25;
  then reconsider s1 = s|the carrier of S1 as State of A1 by Th26;
A3: S = S1+*(S2+*S3) by CIRCCOMB:6;
  then reconsider v = v1 as Element of InnerVertices S by Th21;
  reconsider xx, yy as Vertex of S by A3,Th20;
A4: dom s1 = the carrier of S1 by CIRCUIT1:3;
  thus (Following s).[xy, '&'] = (Following s1).v by A3,A2,CIRCCOMB:64
    .= '&'.<*s1.xx,s1.yy*> by Th48
    .= '&'.<*s.xx,s1.yy*> by A4,FUNCT_1:47
    .= '&'.<*s.xx,s.yy*> by A4,FUNCT_1:47
    .= a '&' b by A1,Def5;
end;

theorem
  for s being State of MajorityICirc(x,y,c), a,b being Element of
  BOOLEAN st a = s.y & b = s.c holds (Following s).[<*y,c*>, '&'] = a '&' b
proof
  set yc = <*y,c*>;
  set S2 = 1GateCircStr(yc, '&'), A2 = 1GateCircuit(y,c, '&');
  reconsider yy = y, cc = c as Vertex of S2 by Th43;
  reconsider v2 = [yc, '&'] as Element of InnerVertices S2 by Th47;
  set S1 = 1GateCircStr(<*x,y*>, '&'), A1 = 1GateCircuit(x,y, '&');
  set S3 = 1GateCircStr(<*c,x*>, '&'), A3 = 1GateCircuit(c,x, '&');
  set S = MajorityIStr(x,y,c), A = MajorityICirc(x,y,c);
  let s be State of A;
  let a,b be Element of BOOLEAN such that
A1: a = s.y & b = s.c;
A2: S1+*S2 = S2+*S1 by CIRCCOMB:5,47;
  then
A3: S = S2+*(S1+*S3) by CIRCCOMB:6;
  then reconsider v = v2 as Element of InnerVertices S by Th21;
  A1+*A2 = A2+*A1 by CIRCCOMB:22,60;
  then
A4: A = A2+*(A1+*A3) by A2,Th25;
  then reconsider s2 = s|the carrier of S2 as State of A2 by Th26;
  reconsider yy, cc as Vertex of S by A3,Th20;
A5: dom s2 = the carrier of S2 by CIRCUIT1:3;
  thus (Following s).[yc, '&'] = (Following s2).v by A3,A4,CIRCCOMB:64
    .= '&'.<*s2.yy,s2.cc*> by Th48
    .= '&'.<*s.yy,s2.cc*> by A5,FUNCT_1:47
    .= '&'.<*s.yy,s.cc*> by A5,FUNCT_1:47
    .= a '&' b by A1,Def5;
end;

theorem
  for s being State of MajorityICirc(x,y,c), a,b being Element of
  BOOLEAN st a = s.c & b = s.x holds (Following s).[<*c,x*>, '&'] = a '&' b
proof
  set cx = <*c,x*>;
  set S3 = 1GateCircStr(cx, '&'), A3 = 1GateCircuit(c,x, '&');
  reconsider cc = c, xx = x as Vertex of S3 by Th43;
  reconsider v3 = [cx, '&'] as Element of InnerVertices S3 by Th47;
  set S = MajorityIStr(x,y,c), A = MajorityICirc(x,y,c);
  let s be State of A;
  let a,b be Element of BOOLEAN such that
A1: a = s.c & b = s.x;
  reconsider cc, xx as Vertex of S by Th20;
  reconsider s3 = s|the carrier of S3 as State of A3 by Th26;
  reconsider v = v3 as Element of InnerVertices S by Th21;
A2: dom s3 = the carrier of S3 by CIRCUIT1:3;
  thus (Following s).[cx, '&'] = (Following s3).v by CIRCCOMB:64
    .= '&'.<*s3.cc,s3.xx*> by Th48
    .= '&'.<*s.cc,s3.xx*> by A2,FUNCT_1:47
    .= '&'.<*s.cc,s.xx*> by A2,FUNCT_1:47
    .= a '&' b by A1,Def5;
end;

definition
  let x,y,c be object;
  func MajorityOutput(x,y,c) -> Element of InnerVertices MajorityStr(x,y,c)
  equals
  [<*[<*x,y*>, '&'], [<*y,c*>, '&'], [<*c,x*>, '&']*>, or3];
  coherence
  proof
    [<*[<*x,y*>, '&'], [<*y,c*>, '&'], [<*c,x*>, '&']*>, or3] in
InnerVertices 1GateCircStr(<*[<*x,y*>, '&'], [<*y,c*>, '&'], [<*c,x*>, '&']*>,
    or3) by Th47;
    hence thesis by Th21;
  end;
  correctness;
end;

definition
  let x,y,c be object;
  func MajorityCirc(x,y,c) -> strict Boolean gate`2=den Circuit of MajorityStr
  (x,y,c) equals
  MajorityICirc(x,y,c) +* 1GateCircuit([<*x,y*>, '&'], [<*y,c*>,
  '&'], [<*c,x*>, '&'], or3);
  coherence;
end;

theorem Th72:
  x in the carrier of MajorityStr(x,y,c) & y in the carrier of
  MajorityStr(x,y,c) & c in the carrier of MajorityStr(x,y,c)
proof
  c in the carrier of 1GateCircStr(<*c,x*>, '&') by Th43;
  then
A1: c in the carrier of MajorityIStr(x,y,c) by Th20;
  y in the carrier of 1GateCircStr(<*x,y*>, '&') by Th43;
  then y in the carrier of 1GateCircStr(<*x,y*>, '&')+*1GateCircStr(<*y,c*> ,
  '&') by Th20;
  then
A2: y in the carrier of MajorityIStr(x,y,c) by Th20;
  x in the carrier of 1GateCircStr(<*c,x*>, '&') by Th43;
  then x in the carrier of MajorityIStr(x,y,c) by Th20;
  hence thesis by A2,A1,Th20;
end;

theorem Th73:
  [<*x,y*>,'&'] in InnerVertices MajorityStr(x,y,c) & [<*y,c*>,'&'
  ] in InnerVertices MajorityStr(x,y,c) & [<*c,x*>,'&'] in InnerVertices
  MajorityStr(x,y,c)
proof
  [<*x,y*>,'&'] in InnerVertices 1GateCircStr(<*x,y*>, '&') by Th47;
  then
  [<*x,y*>,'&'] in InnerVertices (1GateCircStr(<*x,y*>, '&')+*1GateCircStr
  (<*y,c*>, '&')) by Th21;
  then
A1: [<*x,y*>,'&'] in InnerVertices MajorityIStr(x,y,c) by Th21;
  [<*y,c*>,'&'] in InnerVertices 1GateCircStr(<*y,c*>, '&') by Th47;
  then
  [<*y,c*>,'&'] in InnerVertices (1GateCircStr(<*x,y*>, '&')+*1GateCircStr
  (<*y,c*>, '&')) by Th21;
  then
A2: [<*y,c*>,'&'] in InnerVertices MajorityIStr(x,y,c) by Th21;
  [<*c,x*>,'&'] in InnerVertices 1GateCircStr(<*c,x*>, '&') by Th47;
  then [<*c,x*>,'&'] in InnerVertices MajorityIStr(x,y,c) by Th21;
  hence thesis by A1,A2,Th21;
end;

theorem Th74:
  for x,y,c being non pair object holds x in InputVertices
MajorityStr(x,y,c) & y in InputVertices MajorityStr(x,y,c) & c in InputVertices
  MajorityStr(x,y,c)
proof
  let x,y,c be non pair object;
  assume
A1: not thesis;
A2: c in the carrier of MajorityStr(x,y,c) by Th72;
A3: InnerVertices MajorityStr(x,y,c) is Relation by Th67;
  x in the carrier of MajorityStr(x,y,c) & y in the carrier of MajorityStr
  (x,y,c) by Th72;
  then
  x in InnerVertices MajorityStr(x,y,c) or y in InnerVertices MajorityStr(
  x,y,c) or c in InnerVertices MajorityStr(x,y,c) by A2,A1,XBOOLE_0:def 5;
  then
  (ex a,b being object st x = [a,b]) or
(ex a,b being object st y = [a,b]) or ex
  a,b being object st c = [a,b] by A3,RELAT_1:def 1;
  hence contradiction;
end;

theorem Th75:
  for x,y,c being non pair object holds InputVertices MajorityStr(x,y
,c) = {x,y,c} & InnerVertices MajorityStr(x,y,c) = {[<*x,y*>,'&'], [<*y,c*>,'&'
  ], [<*c,x*>,'&']} \/ {MajorityOutput(x,y,c)}
proof
  let x,y,c be non pair object;
  set xy =[<*x,y*>,'&'], yc = [<*y,c*>,'&'], cx = [<*c,x*>,'&'];
  set MI = MajorityIStr(x,y,c), S = 1GateCircStr(<*xy, yc, cx*>, or3);
  set M = MajorityStr(x,y,c);
A1: 1GateCircStr(<*x,y*>, '&') tolerates 1GateCircStr(<*y,c*>, '&') by
CIRCCOMB:43;
A2: InnerVertices S is Relation by Th38;
A3: InputVertices 1GateCircStr(<*y,c*>,'&') = {y,c} by Th40;
A4: InnerVertices 1GateCircStr(<*x,y*>, '&') = {[<*x,y*>, '&']} &
  InnerVertices 1GateCircStr(<*y,c*>, '&') = {[<*y,c*>, '&']} by CIRCCOMB:42;
  then
A5: InnerVertices 1GateCircStr(<*c,x*>, '&') = {[<*c,x*>, '&']} &
InnerVertices (1GateCircStr(<*x,y*>, '&') +* 1GateCircStr(<*y,c*>, '&')) = {[<*
  x,y*>, '&']} \/ {[<*y,c*>, '&']} by A1,CIRCCOMB:11,42;
  1GateCircStr(<*x,y*>, '&') tolerates 1GateCircStr(<*c,x*>, '&') &
1GateCircStr(<*y,c*>, '&') tolerates 1GateCircStr(<*c,x*>, '&') by CIRCCOMB:43;
  then 1GateCircStr(<*x,y*>, '&') +* 1GateCircStr(<*y,c*>, '&') tolerates
  1GateCircStr(<*c,x*>, '&') by A1,CIRCCOMB:3;
  then
A6: InnerVertices MI = {[<*x,y*>,'&']} \/ {[<*y,c*>,'&']} \/ {[<*c,x*>, '&'
  ]} by A5,CIRCCOMB:11
    .= {[<*x,y*>,'&'], [<*y,c*>,'&']} \/ {[<*c,x*>,'&']} by ENUMSET1:1
    .= {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} by ENUMSET1:3;
  InputVertices S = {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} by Th42;
  then
A7: InputVertices S \ InnerVertices MI = {} by A6,XBOOLE_1:37;
A8: InputVertices 1GateCircStr(<*x,y*>,'&') = {x,y} & InputVertices
  1GateCircStr (<*c,x*>,'&') = {c,x} by Th40;
A9: InputVertices 1GateCircStr(<*c,x*>,'&') is without_pairs by Th41;
A10: InputVertices 1GateCircStr(<*x,y*>,'&') is without_pairs & InputVertices
  1GateCircStr(<*y,c*>,'&') is without_pairs by Th41;
  then
A11: InputVertices (1GateCircStr(<*x,y*>,'&')+*1GateCircStr(<*y,c*>,'&')) is
  without_pairs by Th8,CIRCCOMB:47;
  then InputVertices MI is without_pairs by A9,Th8,CIRCCOMB:47;
  then
  InputVertices M = (InputVertices MI) \/ (InputVertices S \ InnerVertices
  MI) by A2,Th6;
  hence InputVertices M = (InputVertices(1GateCircStr(<*x,y*>,'&')+*
  1GateCircStr(<*y,c*>,'&'))) \/ InputVertices 1GateCircStr(<*c,x*>,'&') by A9
,A11,A5,A7,Th7
    .= (InputVertices 1GateCircStr(<*x,y*>,'&')) \/ (InputVertices
1GateCircStr(<*y,c*>,'&')) \/ (InputVertices 1GateCircStr(<*c,x*>,'&')) by A10
,A4,Th7
    .= {x,y,y,c} \/ {c,x} by A8,A3,ENUMSET1:5
    .= {y,y,x,c} \/ {c,x} by ENUMSET1:67
    .= {y,x,c} \/ {c,x} by ENUMSET1:31
    .= {x,y,c} \/ {c,x} by ENUMSET1:58
    .= {x,y,c} \/ ({c}\/{x}) by ENUMSET1:1
    .= {x,y,c} \/ {c} \/ {x} by XBOOLE_1:4
    .= {c,x,y} \/ {c} \/ {x} by ENUMSET1:59
    .= {c,c,x,y} \/ {x} by ENUMSET1:4
    .= {c,x,y} \/ {x} by ENUMSET1:31
    .= {x,y,c} \/ {x} by ENUMSET1:59
    .= {x,x,y,c} by ENUMSET1:4
    .= {x,y,c} by ENUMSET1:31;
  MI tolerates S by CIRCCOMB:47;
  hence InnerVertices M = (InnerVertices MI) \/ (InnerVertices S) by
CIRCCOMB:11
    .= {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} \/ {MajorityOutput(x,y,
  c)} by A6,CIRCCOMB:42;
end;

Lm2: for x,y,c being non pair object
  for s being State of MajorityCirc(x,y,c) for
a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3 = s.c holds (
Following s).[<*x,y*>,'&'] = a1 '&' a2 & (Following s).[<*y,c*>,'&'] = a2 '&'
a3 & (Following s).[<*c,x*>,'&'] = a3 '&' a1
proof
  let x,y,c be non pair object;
  let s be State of MajorityCirc(x,y,c);
  let a1,a2,a3 be Element of BOOLEAN such that
A1: a1 = s.x and
A2: a2 = s.y and
A3: a3 = s.c;
  set S = MajorityStr(x,y,c);
A4: dom s = the carrier of S by CIRCUIT1:3;
A5: y in the carrier of S by Th72;
A6: x in the carrier of S by Th72;
A7: InnerVertices S = the carrier' of S by Th37;
  [<*x,y*>,'&'] in InnerVertices MajorityStr(x,y,c) by Th73;
  hence (Following s).[<*x,y*>,'&'] = '&'.(s*<*x,y*>) by A7,Th35
    .= '&'.<*a1,a2*> by A1,A2,A4,A6,A5,FINSEQ_2:125
    .= a1 '&' a2 by Def5;
A8: c in the carrier of S by Th72;
  [<*y,c*>,'&'] in InnerVertices MajorityStr(x,y,c) by Th73;
  hence (Following s).[<*y,c*>,'&'] = '&'.(s*<*y,c*>) by A7,Th35
    .= '&'.<*a2,a3*> by A2,A3,A4,A5,A8,FINSEQ_2:125
    .= a2 '&' a3 by Def5;
  [<*c,x*>,'&'] in InnerVertices MajorityStr(x,y,c) by Th73;
  hence (Following s).[<*c,x*>,'&'] = '&'.(s*<*c,x*>) by A7,Th35
    .= '&'.<*a3,a1*> by A1,A3,A4,A6,A8,FINSEQ_2:125
    .= a3 '&' a1 by Def5;
end;

theorem
  for x,y,c being non pair object for s being State of MajorityCirc(x,y,c)
for a1,a2 being Element of BOOLEAN st a1 = s.x & a2 = s.y holds (Following s).[
  <*x,y*>,'&'] = a1 '&' a2
proof
  let x,y,c be non pair object;
  reconsider a = c as Vertex of MajorityStr(x,y,c) by Th72;
  let s be State of MajorityCirc(x,y,c);
  s.a is Element of BOOLEAN;
  hence thesis by Lm2;
end;

theorem
  for x,y,c being non pair object for s being State of MajorityCirc(x,y,c)
for a2,a3 being Element of BOOLEAN st a2 = s.y & a3 = s.c holds (Following s).[
  <*y,c*>,'&'] = a2 '&' a3
proof
  let x,y,c be non pair object;
  reconsider a = x as Vertex of MajorityStr(x,y,c) by Th72;
  let s be State of MajorityCirc(x,y,c);
  s.a is Element of BOOLEAN;
  hence thesis by Lm2;
end;

theorem
  for x,y,c being non pair object for s being State of MajorityCirc(x,y,c)
for a1,a3 being Element of BOOLEAN st a1 = s.x & a3 = s.c holds (Following s).[
  <*c,x*>,'&'] = a3 '&' a1
proof
  let x,y,c be non pair object;
  reconsider a = y as Vertex of MajorityStr(x,y,c) by Th72;
  let s be State of MajorityCirc(x,y,c);
  s.a is Element of BOOLEAN;
  hence thesis by Lm2;
end;

theorem Th79:
  for x,y,c being non pair object for s being State of MajorityCirc(x
,y,c) for a1,a2,a3 being Element of BOOLEAN st a1 = s.[<*x,y*>,'&'] & a2 = s.[
<*y,c*>,'&'] & a3 = s.[<*c,x*>,'&'] holds (Following s).MajorityOutput(x,y,c) =
  a1 'or' a2 'or' a3
proof
  let x,y,c be non pair object;
  set xy =[<*x,y*>,'&'], yc = [<*y,c*>,'&'], cx = [<*c,x*>,'&'];
  set S = MajorityStr(x,y,c);
  reconsider xy, yc, cx as Element of InnerVertices S by Th73;
  let s be State of MajorityCirc(x,y,c);
  let a1,a2,a3 be Element of BOOLEAN such that
A1: a1 = s.[<*x,y*>,'&'] & a2 = s.[<*y,c*>,'&'] & a3 = s.[<*c,x*>,'&'];
A2: dom s = the carrier of S by CIRCUIT1:3;
  InnerVertices S = the carrier' of S by Th37;
  hence (Following s).MajorityOutput(x,y,c) = or3.(s*<*xy, yc, cx*>) by Th35
    .= or3.<*a1,a2,a3*> by A1,A2,FINSEQ_2:126
    .= a1 'or' a2 'or' a3 by Def6;
end;

Lm3: for x,y,c being non pair object
  for s being State of MajorityCirc(x,y,c) for
a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3 = s.c holds (
Following(s,2)).MajorityOutput(x,y,c) = a1 '&' a2 'or' a2 '&' a3 'or' a3 '&' a1
& (Following(s,2)).[<*x,y*>,'&'] = a1 '&' a2 & (Following(s,2)).[<*y,c*>,'&'] =
a2 '&' a3 & (Following(s,2)).[<*c,x*>,'&'] = a3 '&' a1
proof
  let x,y,c be non pair object;
  set S = MajorityStr(x,y,c);
  reconsider x9 = x, y9 = y, c9 = c as Vertex of S by Th72;
  let s be State of MajorityCirc(x,y,c);
  set xy =[<*x,y*>,'&'], yc = [<*y,c*>,'&'], cx = [<*c,x*>,'&'];
A1: Following(s,2) = Following Following s by Th15;
  let a1,a2,a3 be Element of BOOLEAN such that
A2: a1 = s.x & a2 = s.y & a3 = s.c;
A3: (Following s).cx = a3 '&' a1 by A2,Lm2;
  (Following s).xy = a1 '&' a2 & (Following s).yc = a2 '&' a3 by A2,Lm2;
  hence (Following(s,2)).MajorityOutput(x,y,c) = a1 '&' a2 'or' a2 '&' a3 'or'
  a3 '&' a1 by A1,A3,Th79;
  y in InputVertices S by Th74;
  then
A4: (Following s).y9 = s.y by CIRCUIT2:def 5;
  c in InputVertices S by Th74;
  then
A5: (Following s).c9 = s.c by CIRCUIT2:def 5;
  x in InputVertices S by Th74;
  then (Following s).x9 = s.x by CIRCUIT2:def 5;
  hence thesis by A2,A4,A5,A1,Lm2;
end;

theorem
  for x,y,c being non pair object for s being State of MajorityCirc(x,y,c)
for a1,a2 being Element of BOOLEAN st a1 = s.x & a2 = s.y holds (Following(s,2)
  ).[<*x,y*>,'&'] = a1 '&' a2
proof
  let x,y,c be non pair object;
  reconsider a = c as Vertex of MajorityStr(x,y,c) by Th72;
  let s be State of MajorityCirc(x,y,c);
  s.a is Element of BOOLEAN;
  hence thesis by Lm3;
end;

theorem
  for x,y,c being non pair object for s being State of MajorityCirc(x,y,c)
for a2,a3 being Element of BOOLEAN st a2 = s.y & a3 = s.c holds (Following(s,2)
  ).[<*y,c*>,'&'] = a2 '&' a3
proof
  let x,y,c be non pair object;
  reconsider a = x as Vertex of MajorityStr(x,y,c) by Th72;
  let s be State of MajorityCirc(x,y,c);
  s.a is Element of BOOLEAN;
  hence thesis by Lm3;
end;

theorem
  for x,y,c being non pair object for s being State of MajorityCirc(x,y,c)
for a1,a3 being Element of BOOLEAN st a1 = s.x & a3 = s.c holds (Following(s,2)
  ).[<*c,x*>,'&'] = a3 '&' a1
proof
  let x,y,c be non pair object;
  reconsider a = y as Vertex of MajorityStr(x,y,c) by Th72;
  let s be State of MajorityCirc(x,y,c);
  s.a is Element of BOOLEAN;
  hence thesis by Lm3;
end;

theorem
  for x,y,c being non pair object for s being State of MajorityCirc(x,y,c)
for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3 = s.c holds (
Following(s,2)).MajorityOutput(x,y,c) = a1 '&' a2 'or' a2 '&' a3 'or' a3 '&' a1
  by Lm3;

theorem Th84:
  for x,y,c being non pair object for s being State of MajorityCirc(x
  ,y,c) holds Following(s,2) is stable
proof
  let x,y,c be non pair object;
  set S = MajorityStr(x,y,c);
  reconsider xx = x, yy = y, cc = c as Vertex of S by Th72;
  let s be State of MajorityCirc(x,y,c);
  set a1 = s.xx, a2 = s.yy, a3 = s.cc;
  set ffs = Following(s,2), fffs = Following ffs;
A1: ffs = Following Following s by Th15;
A2: y in InputVertices S by Th74;
  then (Following s).y = a2 by CIRCUIT2:def 5;
  then
A3: ffs.y = a2 by A1,A2,CIRCUIT2:def 5;
  a2 = s.y;
  then
A4: ffs.[<*c,x*>,'&'] = a3 '&' a1 by Lm3;
A5: x in InputVertices S by Th74;
  then (Following s).x = a1 by CIRCUIT2:def 5;
  then
A6: ffs.x = a1 by A1,A5,CIRCUIT2:def 5;
  a1 = s.x;
  then
A7: ffs.[<*y,c*>,'&'] = a2 '&' a3 by Lm3;
A8: c in InputVertices S by Th74;
  then (Following s).c = a3 by CIRCUIT2:def 5;
  then
A9: ffs.c = a3 by A1,A8,CIRCUIT2:def 5;
  a3 = s.c;
  then
A10: ffs.[<*x,y*>,'&'] = a1 '&' a2 by Lm3;
A11: ffs.MajorityOutput(x,y,c) = a1 '&' a2 'or' a2 '&' a3 'or' a3 '&' a1 by Lm3
;
A12: now
    let a be object;
    assume
A13: a in the carrier of S;
    then reconsider v = a as Vertex of S;
A14: v in InputVertices S \/ InnerVertices S by A13,XBOOLE_1:45;
    thus ffs.a = (fffs).a
    proof
      per cases by A14,XBOOLE_0:def 3;
      suppose
        v in InputVertices S;
        hence thesis by CIRCUIT2:def 5;
      end;
      suppose
        v in InnerVertices S;
        then v in {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} \/ {
        MajorityOutput(x,y,c)} by Th75;
        then v in {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} or v in {
        MajorityOutput(x,y,c)} by XBOOLE_0:def 3;
        then v = [<*x,y*>,'&'] or v = [<*y,c*>,'&'] or v = [<*c,x*>,'&'] or v
        = MajorityOutput(x,y,c) by ENUMSET1:def 1,TARSKI:def 1;
        hence thesis by A11,A10,A7,A4,A6,A3,A9,Lm2,Th79;
      end;
    end;
  end;
  dom Following Following(s,2) = the carrier of S & dom Following(s,2) =
  the carrier of S by CIRCUIT1:3;
  hence ffs = fffs by A12,FUNCT_1:2;
end;

definition
  let x,y,c be object;
  func BitAdderWithOverflowStr(x,y,c) -> unsplit gate`1=arity gate`2isBoolean
  non void strict non empty ManySortedSign equals
  2GatesCircStr(x,y,c, 'xor') +*
  MajorityStr(x,y,c);
  coherence;
end;

theorem Th85:
  for x,y,c being non pair object holds InputVertices
  BitAdderWithOverflowStr(x,y,c) = {x,y,c}
proof
  let x,y,c be non pair object;
  set S = BitAdderWithOverflowStr(x,y,c);
  set S1 = 2GatesCircStr(x,y,c, 'xor'), S2 = MajorityStr(x,y,c);
A1: InputVertices S1 = {x,y,c} & InputVertices S2 = {x,y,c} by Th57,Th75;
  InnerVertices S1 is Relation & InnerVertices S2 is Relation by Th58,Th67;
  hence InputVertices S = {x,y,c} \/ {x,y,c} by A1,Th7
    .= {x,y,c};
end;

theorem
  for x,y,c being non pair object holds InnerVertices
  BitAdderWithOverflowStr(x,y,c) = {[<*x,y*>, 'xor'], 2GatesCircOutput(x,y,c,
'xor')} \/ {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} \/ {MajorityOutput(x,y
  ,c)}
proof
  let x,y,c be non pair object;
  set S1 = 2GatesCircStr(x,y,c, 'xor'), S2 = MajorityStr(x,y,c);
A1: InnerVertices S2 = {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} \/ {
  MajorityOutput(x,y,c)} by Th75;
  {[<*x,y*>, 'xor'], 2GatesCircOutput(x,y,c,'xor')} \/ {[<*x,y*>,'&'], [<*
  y,c*> ,'&'], [<*c,x*>,'&']} \/ {MajorityOutput(x,y,c)} = {[<*x,y*>, 'xor'],
2GatesCircOutput(x,y,c,'xor')} \/ ({[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']
  } \/ {MajorityOutput(x,y,c)}) & InnerVertices S1 = {[<*x,y*>, 'xor'],
  2GatesCircOutput(x,y,c,'xor')} by Th56,XBOOLE_1:4;
  hence thesis by A1,Th27;
end;

theorem
  for S being non empty ManySortedSign st S = BitAdderWithOverflowStr(x,
y,c ) holds x in the carrier of S & y in the carrier of S & c in the carrier of
  S
proof
  set S1 = 2GatesCircStr(x,y,c, 'xor');
  let S be non empty ManySortedSign;
  assume
A1: S = BitAdderWithOverflowStr(x,y,c);
A2: c in the carrier of S1 by Th60;
  x in the carrier of S1 & y in the carrier of S1 by Th60;
  hence thesis by A1,A2,Th20;
end;

definition
  let x,y,c be object;
  func BitAdderWithOverflowCirc(x,y,c) -> strict Boolean gate`2=den Circuit of
  BitAdderWithOverflowStr(x,y,c) equals
  BitAdderCirc(x,y,c) +* MajorityCirc(x,y,c
  );
  coherence;
end;

theorem
  InnerVertices BitAdderWithOverflowStr(x,y,c) is Relation
proof
  InnerVertices 2GatesCircStr(x,y,c, 'xor') is Relation & InnerVertices
  MajorityStr(x,y,c) is Relation by Th58,Th67;
  hence thesis by Th2,CIRCCOMB:47;
end;

theorem
  for x,y,c being non pair object holds InputVertices
  BitAdderWithOverflowStr(x,y,c) is without_pairs
proof
  let x,y,c be non pair object;
  InputVertices BitAdderWithOverflowStr(x,y,c) = {x,y,c} by Th85;
  hence thesis;
end;

theorem
  BitAdderOutput(x,y,c) in InnerVertices BitAdderWithOverflowStr(x,y,c)
& MajorityOutput(x,y,c) in InnerVertices BitAdderWithOverflowStr(x,y,c) by Th21
;

theorem
  for x,y,c being non pair object for s being State of
BitAdderWithOverflowCirc(x,y,c) for a1,a2,a3 being Element of BOOLEAN st a1 = s
  .x & a2 = s.y & a3 = s.c holds (Following(s,2)).BitAdderOutput(x,y,c) = a1
'xor' a2 'xor' a3 & (Following(s,2)).MajorityOutput(x,y,c) = a1 '&' a2 'or' a2
  '&' a3 'or' a3 '&' a1
proof
  let x,y,c be non pair object;
  set S1 = 2GatesCircStr(x,y,c, 'xor'), S2 = MajorityStr(x,y,c);
  set A = BitAdderWithOverflowCirc(x,y,c);
  set A1 = BitAdderCirc(x,y,c), A2 = MajorityCirc(x,y,c);
  let s be State of A;
  reconsider t = s as State of A1+*A2;
  reconsider s1 = s|the carrier of S1 as State of A1 by Th26;
  set f = 'xor';
  let a1,a2,a3 be Element of BOOLEAN;
  assume that
A1: a1 = s.x and
A2: a2 = s.y and
A3: a3 = s.c;
A4: dom s1 = the carrier of S1 by CIRCUIT1:3;
  y in the carrier of S1 by Th60;
  then
A5: a2 = s1.y by A2,A4,FUNCT_1:47;
  InputVertices S1 is without_pairs by Th59;
  then InnerVertices S2 misses InputVertices S1 by Th5,Th67;
  then
A6: (Following(t,2)).2GatesCircOutput(x,y,c, f) = (Following(s1,2)).
  2GatesCircOutput(x,y,c, f) by Th32;
  c in the carrier of S1 by Th60;
  then
A7: a3 = s1.c by A3,A4,FUNCT_1:47;
  reconsider s2 = s|the carrier of S2 as State of A2 by Th26;
A8: dom s2 = the carrier of S2 by CIRCUIT1:3;
  x in the carrier of S1 by Th60;
  then a1 = s1.x by A1,A4,FUNCT_1:47;
  hence (Following(s,2)).BitAdderOutput(x,y,c) = a1 'xor' a2 'xor' a3 by A5,A7
,A6,Th64;
  InputVertices S2 is without_pairs by Th68;
  then InnerVertices S1 misses InputVertices S2 by Th5,Th58;
  then
A9: (Following(t,2)).MajorityOutput(x,y,c) = (Following(s2,2)).
  MajorityOutput(x,y,c) by Th33;
  c in the carrier of S2 by Th72;
  then
A10: a3 = s2.c by A3,A8,FUNCT_1:47;
  y in the carrier of S2 by Th72;
  then
A11: a2 = s2.y by A2,A8,FUNCT_1:47;
  x in the carrier of S2 by Th72;
  then a1 = s2.x by A1,A8,FUNCT_1:47;
  hence thesis by A11,A10,A9,Lm3;
end;

theorem
  for x,y,c being non pair object for s being State of
  BitAdderWithOverflowCirc(x,y,c) holds Following(s,2) is stable
proof
  let x,y,c be non pair object;
  set S1 = 2GatesCircStr(x,y,c, 'xor'), S2 = MajorityStr(x,y,c);
  set A = BitAdderWithOverflowCirc(x,y,c);
  set A1 = BitAdderCirc(x,y,c), A2 = MajorityCirc(x,y,c);
  let s be State of A;
  reconsider s2 = s|the carrier of S2 as State of A2 by Th26;
  reconsider t = s as State of A1+*A2;
  reconsider s1 = s|the carrier of S1 as State of A1 by Th26;
  set S = BitAdderWithOverflowStr(x,y,c);
A1: dom Following(s,3) = the carrier of S by CIRCUIT1:3;
A2: the carrier of S = (the carrier of S1) \/ the carrier of S2 by
CIRCCOMB:def 2;
  InputVertices S1 is without_pairs by Th59;
  then InnerVertices S2 misses InputVertices S1 by Th5,Th67;
  then
A3: Following(s1,2) = Following(t,2)|the carrier of S1 & Following(s1,3) =
  Following(t,3)|the carrier of S1 by Th30;
  Following(s1,2) is stable by Th63;
  then
A4: Following(s1,2) = Following Following(s1,2)
    .= Following(s1,2+1) by Th12;
  InputVertices S2 is without_pairs by Th68;
  then InnerVertices S1 misses InputVertices S2 by Th5,Th58;
  then
A5: Following(s2,2) = Following(t,2)|the carrier of S2 & Following(s2,3) =
  Following(t,3)|the carrier of S2 by Th31;
  Following(s2,2) is stable by Th84;
  then
A6: Following(s2,2) = Following Following(s2,2)
    .= Following(s2,2+1) by Th12;
A7: dom Following(s1,2) = the carrier of S1 & dom Following(s2,2) = the
  carrier of S2 by CIRCUIT1:3;
A8: now
    let a be object;
    assume a in the carrier of S;
    then a in the carrier of S1 or a in the carrier of S2 by A2,XBOOLE_0:def 3;
    then (Following(s,2)).a = (Following(s1,2)).a & (Following(s,3)).a = (
Following(s1,3)).a or (Following(s,2)).a = (Following(s2,2)).a & (Following(s,3
    )).a = (Following(s2,3)).a by A3,A5,A4,A6,A7,FUNCT_1:47;
    hence (Following(s,2)).a = (Following Following(s,2)).a by A4,A6,Th12;
  end;
  Following(s,2+1) = Following Following(s,2) & dom Following(s,2) = the
  carrier of S by Th12,CIRCUIT1:3;
  hence Following(s,2) = Following Following(s,2) by A1,A8,FUNCT_1:2;
end;