The abstract of the Mizar article:

Full Adder Circuit. Part I

by

Grzegorz Bancerek, and

Yatsuka Nakamura

Received August 10, 1995

MML identifier: FACIRC_1

[ Mizar article, MML identifier index ]

environ

 vocabulary BOOLE, RELAT_1, FUNCT_1, FINSEQ_1, CIRCCOMB, FINSEQ_2, MSUALG_1,
      PARTFUN1, MSAFREE2, FUNCT_4, MARGREL1, MIDSP_3, BINARITH, ZF_LANG, AMI_1,
      ZF_REFLE, CIRCUIT1, QC_LANG1, CARD_3, LATTICES, MCART_1, FINSET_1,
      CIRCUIT2, CLASSES1, FACIRC_1;
 notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, NUMBERS, XREAL_0, NAT_1,
      MCART_1, RELAT_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, MIDSP_3;
 constructors MCART_1, BINARITH, CLASSES1, CIRCUIT1, CIRCUIT2, CIRCCOMB,
      ENUMSET1;
 clusters NUMBERS, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_1, RELSET_1, FINSEQ_2,
      PRVECT_1, MSUALG_1, PRE_CIRC, CIRCCOMB, FINSEQ_1, XREAL_0, ARYTM_3,
      ORDINAL1, ZFMISC_1, ORDINAL2;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


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

definition let IT be set;
 attr IT is pair means
:: FACIRC_1:def 1

 ex x,y being set st IT = [x,y];
end;

definition
 cluster pair -> non empty set;
end;

definition
 let x,y be set;
 cluster [x,y] -> pair;
end;

definition
 cluster pair set;
 cluster non pair set;
end;

definition
 cluster -> non pair Nat;
end;

definition let IT be set;
 attr IT is with_pair means
:: FACIRC_1:def 2

   ex x being pair set st x in IT;
 antonym IT is without_pairs;
end;

definition
 cluster empty -> without_pairs set;
 let x be non pair set;
 cluster {x} -> without_pairs;
 let y be non pair set;
 cluster {x,y} -> without_pairs;
 let z be non pair set;
 cluster {x,y,z} -> without_pairs;
end;

definition
 cluster without_pairs (non empty set);
end;

definition
 let X, Y be without_pairs set;
 cluster X \/ Y -> without_pairs;
end;

definition
 let X be without_pairs set, Y be set;
 cluster X \ Y -> without_pairs;
 cluster X /\ Y -> without_pairs;
 cluster Y /\ X -> without_pairs;
end;

definition
 let x be pair set;
 cluster {x} -> Relation-like;
 let y be pair set;
 cluster {x,y} -> Relation-like;
 let z be pair set;
 cluster {x,y,z} -> Relation-like;
end;

definition
 cluster without_pairs Relation-like -> empty set;
end;

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

definition
 let x be non pair set;
 cluster <*x*> -> nonpair-yielding;
 let y be non pair set;
 cluster <*x,y*> -> nonpair-yielding;
 let z be non pair set;
 cluster <*x,y,z*> -> nonpair-yielding;
end;

theorem :: FACIRC_1:1
 for f being Function st f is nonpair-yielding holds rng f is without_pairs;

definition let n be Nat;
 cluster one-to-one nonpair-yielding FinSeqLen of n;
end;

definition
 cluster one-to-one nonpair-yielding FinSequence;
end;

definition
 let f be nonpair-yielding Function;
 cluster rng f -> without_pairs;
end;

theorem :: FACIRC_1:2
 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;

theorem :: FACIRC_1:3
 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;

theorem :: FACIRC_1:4
 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);

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

theorem :: FACIRC_1:6
 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);

theorem :: FACIRC_1:7
 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);

theorem :: FACIRC_1:8
 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;

theorem :: FACIRC_1:9
 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;

begin :: Boolean Operations

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

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;

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;

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

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;

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;

definition
 func 'xor' -> Function of 2-tuples_on BOOLEAN, BOOLEAN means
:: FACIRC_1:def 4

  for x,y being Element of BOOLEAN holds it.<*x,y*> = x 'xor' y;
 func 'or' -> Function of 2-tuples_on BOOLEAN, BOOLEAN means
:: FACIRC_1:def 5

  for x,y being Element of BOOLEAN holds it.<*x,y*> = x 'or' y;
 func '&' -> Function of 2-tuples_on BOOLEAN, BOOLEAN means
:: FACIRC_1:def 6

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

definition
 func or3 -> Function of 3-tuples_on BOOLEAN, BOOLEAN means
:: FACIRC_1:def 7

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

definition
 let x be set;
 redefine func <*x*> -> FinSeqLen of 1;
 let y be set;
 func <*x,y*> -> FinSeqLen of 2;
 let z be set;
 func <*x,y,z*> -> FinSeqLen of 3;
end;

definition let n,m be Nat;
 let p be FinSeqLen of n;
 let q be FinSeqLen of m;
 redefine func p^q -> FinSeqLen of n+m;
end;

begin

theorem :: FACIRC_1:10
 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);

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 Nat;
 func Following(s,n) -> State of A means
:: FACIRC_1:def 8

  ex f being Function of NAT, product the Sorts of A st
   it = f.n & f.0 = s &
   for n being Nat holds f.(n+1) = Following f.n;
end;

theorem :: FACIRC_1:11
 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;

theorem :: FACIRC_1:12
 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);

theorem :: FACIRC_1:13
 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);

theorem :: FACIRC_1:14
 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;

theorem :: FACIRC_1:15
 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;

theorem :: FACIRC_1:16
 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);

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 set;
 pred s is_stable_at x means
:: FACIRC_1:def 9

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

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

theorem :: FACIRC_1:18
   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;

theorem :: FACIRC_1:19
 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;

begin :: Combined Circuits

theorem :: FACIRC_1:20
 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;

theorem :: FACIRC_1:21
 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);

theorem :: FACIRC_1:22
   for S1,S2 being non empty ManySortedSign
 for x being set st x in InnerVertices S2 holds x in InnerVertices (S1+*S2);

theorem :: FACIRC_1:23
 for S1,S2 being unsplit gate`1=arity non empty ManySortedSign holds
   S1+*S2 = S2+*S1;

theorem :: FACIRC_1:24
 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;

theorem :: FACIRC_1:25
 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);

theorem :: FACIRC_1:26
 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;

theorem :: FACIRC_1:27
 for S1,S2 being unsplit gate`1=arity non empty ManySortedSign holds
  InnerVertices (S1+*S2) = (InnerVertices S1) \/ InnerVertices S2;

theorem :: FACIRC_1:28
 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;

theorem :: FACIRC_1:29
 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;

theorem :: FACIRC_1:30
 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);

theorem :: FACIRC_1:31
 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);

theorem :: FACIRC_1:32
 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;

theorem :: FACIRC_1:33
 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;

definition
 let S be gate`2=den non void (non empty ManySortedSign);
 let g be Gate of S;
 cluster g`2 -> Function-like Relation-like;
end;

theorem :: FACIRC_1:34
 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);

theorem :: FACIRC_1:35
 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 OperSymbols of S holds (Following s).[p,f] = f.(s*p);

theorem :: FACIRC_1:36
   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 OperSymbols 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];

theorem :: FACIRC_1:37
 for S being unsplit non empty ManySortedSign holds
  InnerVertices S = the OperSymbols of S;

begin :: One Gate Circuit

theorem :: FACIRC_1:38
 for f being set, p being FinSequence holds
  InnerVertices 1GateCircStr(p,f) is Relation;

theorem :: FACIRC_1:39
   for f being set, p being nonpair-yielding FinSequence holds
  InputVertices 1GateCircStr(p,f) is without_pairs;

theorem :: FACIRC_1:40
 for f being set, x,y being set holds
  InputVertices 1GateCircStr(<*x,y*>,f) = {x,y};

theorem :: FACIRC_1:41
 for f being set, x,y being non pair set holds
  InputVertices 1GateCircStr(<*x,y*>,f) is without_pairs;

theorem :: FACIRC_1:42
 for f being set, x,y,z being set holds
  InputVertices 1GateCircStr(<*x,y,z*>,f) = {x,y,z};

theorem :: FACIRC_1:43
 for x,y,f being set 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);

theorem :: FACIRC_1:44
 for x,y,z,f being set 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);

theorem :: FACIRC_1:45
   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);

theorem :: FACIRC_1:46
   for f,x being set, p being FinSequence holds
   1GateCircStr(p,f,x) is gate`1=arity Circuit-like;

theorem :: FACIRC_1:47
 for p being FinSequence, f be set holds
   [p,f] in InnerVertices 1GateCircStr(p,f);

definition
 let x,y be set;
 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
:: FACIRC_1:def 10

   1GateCircuit(<*x,y*>, f);
end;

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

theorem :: FACIRC_1:48
 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;

theorem :: FACIRC_1:49
 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;

theorem :: FACIRC_1:50
 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;

theorem :: FACIRC_1:51
   for s being State of 1GateCircuit(x,y,f) holds Following s is stable;

definition
 let x,y,z be set;
 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
:: FACIRC_1:def 11

   1GateCircuit(<*x,y,z*>, f);
end;

theorem :: FACIRC_1:52
 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;

theorem :: FACIRC_1:53
 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;

theorem :: FACIRC_1:54
   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;

theorem :: FACIRC_1:55
   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;

begin :: Two Gates Circuit

definition
 let x,y,c be set;
 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
:: FACIRC_1:def 12

   1GateCircStr(<*x,y*>, f) +* 1GateCircStr(<*[<*x,y*>, f], c*>, f);
end;

definition let x,y,c be set;
 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
:: FACIRC_1:def 13

   [<*[<*x,y*>, f], c*>, f];
end;

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

theorem :: FACIRC_1:56
 InnerVertices 2GatesCircStr(x,y,c,f)
    = {[<*x,y*>, f], 2GatesCircOutput(x,y,c,f)};

theorem :: FACIRC_1:57
 c <> [<*x,y*>, f] implies
   InputVertices 2GatesCircStr(x,y,c,f) = {x,y,c};

definition
 let x,y,c be set;
 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
:: FACIRC_1:def 14

   1GateCircuit(x,y, f) +* 1GateCircuit([<*x,y*>, f], c, f);
end;

theorem :: FACIRC_1:58
 InnerVertices 2GatesCircStr(x,y,c,f) is Relation;

theorem :: FACIRC_1:59
 for x,y,c being non pair set holds
   InputVertices 2GatesCircStr(x,y,c,f) is without_pairs;

theorem :: FACIRC_1:60
 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);

theorem :: FACIRC_1:61
   [<*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);

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

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

theorem :: FACIRC_1:62
 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;

theorem :: FACIRC_1:63
 c <> [<*x,y*>, f] implies Following(s,2) is stable;

theorem :: FACIRC_1:64
 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;

theorem :: FACIRC_1:65
   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;

theorem :: FACIRC_1:66
   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;

begin :: Bit Adder Circuit

definition
 let x,y,c be set;
 func BitAdderOutput(x,y,c) ->
      Element of InnerVertices 2GatesCircStr(x,y,c, 'xor') equals
:: FACIRC_1:def 15

   2GatesCircOutput(x,y,c, 'xor');
end;

definition
 let x,y,c be set;
 func BitAdderCirc(x,y,c) ->
      strict Boolean gate`2=den Circuit of 2GatesCircStr(x,y,c, 'xor') equals
:: FACIRC_1:def 16

   2GatesCircuit(x,y,c, 'xor');
end;



definition
 let x,y,c be set;
 func MajorityIStr(x,y,c) ->
    unsplit gate`1=arity gate`2isBoolean
    non void strict non empty ManySortedSign equals
:: FACIRC_1:def 17

   1GateCircStr(<*x,y*>, '&') +* 1GateCircStr(<*y,c*>, '&') +*
       1GateCircStr(<*c,x*>, '&');
end;


definition
 let x,y,c be set;
 func MajorityStr(x,y,c) ->
    unsplit gate`1=arity gate`2isBoolean
    non void strict non empty ManySortedSign equals
:: FACIRC_1:def 18

   MajorityIStr(x,y,c) +*
       1GateCircStr(<*[<*x,y*>, '&'], [<*y,c*>, '&'], [<*c,x*>, '&']*>, or3);
end;

definition
 let x,y,c be set;
 func MajorityICirc(x,y,c) ->
      strict Boolean gate`2=den Circuit of MajorityIStr(x,y,c) equals
:: FACIRC_1:def 19

   1GateCircuit(x,y, '&') +* 1GateCircuit(y,c, '&') +*
       1GateCircuit(c,x, '&');
end;


theorem :: FACIRC_1:67
 InnerVertices MajorityStr(x,y,c) is Relation;

theorem :: FACIRC_1:68
 for x,y,c being non pair set holds
  InputVertices MajorityStr(x,y,c) is without_pairs;

theorem :: FACIRC_1:69
   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;

theorem :: FACIRC_1:70
   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;

theorem :: FACIRC_1:71
   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;

definition
 let x,y,c be set;
 func MajorityOutput(x,y,c) -> Element of InnerVertices MajorityStr(x,y,c)
  equals
:: FACIRC_1:def 20

   [<*[<*x,y*>, '&'], [<*y,c*>, '&'], [<*c,x*>, '&']*>, or3];
end;

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

theorem :: FACIRC_1:72
 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);

theorem :: FACIRC_1:73
 [<*x,y*>,'&'] in InnerVertices MajorityStr(x,y,c) &
 [<*y,c*>,'&'] in InnerVertices MajorityStr(x,y,c) &
 [<*c,x*>,'&'] in InnerVertices MajorityStr(x,y,c);

theorem :: FACIRC_1:74
 for x,y,c being non pair set holds
  x in InputVertices MajorityStr(x,y,c) &
  y in InputVertices MajorityStr(x,y,c) &
  c in InputVertices MajorityStr(x,y,c);

theorem :: FACIRC_1:75
 for x,y,c being non pair set holds
  InputVertices MajorityStr(x,y,c) = {x,y,c} &
  InnerVertices MajorityStr(x,y,c) =
    {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} \/ {MajorityOutput(x,y,c)};

theorem :: FACIRC_1:76
   for x,y,c being non pair set 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;

theorem :: FACIRC_1:77
   for x,y,c being non pair set 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;

theorem :: FACIRC_1:78
   for x,y,c being non pair set 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;

theorem :: FACIRC_1:79
 for x,y,c being non pair set 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;

theorem :: FACIRC_1:80
   for x,y,c being non pair set 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;

theorem :: FACIRC_1:81
   for x,y,c being non pair set 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;

theorem :: FACIRC_1:82
   for x,y,c being non pair set 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;

theorem :: FACIRC_1:83
   for x,y,c being non pair set 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;

theorem :: FACIRC_1:84
 for x,y,c being non pair set for s being State of MajorityCirc(x,y,c)
  holds Following(s,2) is stable;

definition
 let x,y,c be set;
 func BitAdderWithOverflowStr(x,y,c) ->
      unsplit gate`1=arity gate`2isBoolean
      non void strict non empty ManySortedSign
  equals
:: FACIRC_1:def 22

    2GatesCircStr(x,y,c, 'xor') +* MajorityStr(x,y,c);
end;

theorem :: FACIRC_1:85
 for x,y,c being non pair set holds
   InputVertices BitAdderWithOverflowStr(x,y,c) = {x,y,c};

theorem :: FACIRC_1:86
   for x,y,c being non pair set holds
   InnerVertices BitAdderWithOverflowStr(x,y,c) =
     {[<*x,y*>, 'xor'], 2GatesCircOutput(x,y,c,'xor')} \/
     {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} \/ {MajorityOutput(x,y,c)};

theorem :: FACIRC_1:87
   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;

definition
 let x,y,c be set;
 func BitAdderWithOverflowCirc(x,y,c) ->
   strict Boolean gate`2=den Circuit of BitAdderWithOverflowStr(x,y,c) equals
:: FACIRC_1:def 23

   BitAdderCirc(x,y,c) +* MajorityCirc(x,y,c);
end;

theorem :: FACIRC_1:88
   InnerVertices BitAdderWithOverflowStr(x,y,c) is Relation;

theorem :: FACIRC_1:89
   for x,y,c being non pair set holds
  InputVertices BitAdderWithOverflowStr(x,y,c) is without_pairs;

theorem :: FACIRC_1:90
   BitAdderOutput(x,y,c) in InnerVertices BitAdderWithOverflowStr(x,y,c) &
 MajorityOutput(x,y,c) in InnerVertices BitAdderWithOverflowStr(x,y,c);

theorem :: FACIRC_1:91
   for x,y,c being non pair set
 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;

theorem :: FACIRC_1:92
   for x,y,c being non pair set
 for s being State of BitAdderWithOverflowCirc(x,y,c)
  holds Following(s,2) is stable;