The Mizar article:

2's Complement Circuit

by
Katsumi Wasaki, and
Pauline N. Kawamoto

Received October 25, 1996

Copyright (c) 1996 Association of Mizar Users

MML identifier: TWOSCOMP
[ MML identifier index ]


environ

 vocabulary FINSEQ_1, CIRCCOMB, AMI_1, MSUALG_1, LATTICES, CIRCUIT1, MSAFREE2,
      FUNCT_1, MARGREL1, RELAT_1, BOOLE, FINSEQ_2, ZF_LANG, BINARITH, FACIRC_1,
      FUNCT_4, CIRCUIT2, TWOSCOMP;
 notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, STRUCT_0,
      MARGREL1, FINSEQ_2, BINARITH, MSUALG_1, MSAFREE2, CIRCUIT1, CIRCUIT2,
      CIRCCOMB, FACIRC_1;
 constructors BINARITH, CIRCUIT1, CIRCUIT2, FACIRC_1;
 clusters MSUALG_1, PRE_CIRC, CIRCCOMB, FACIRC_1, FINSEQ_1, RELSET_1, MARGREL1;
 requirements NUMERALS, SUBSET;
 definitions CIRCUIT2;
 theorems TARSKI, ENUMSET1, MARGREL1, BINARITH, FUNCT_1, FINSEQ_2, CIRCUIT1,
      CIRCUIT2, CIRCCOMB, FACIRC_1, XBOOLE_0, XBOOLE_1;
 schemes FACIRC_1;

begin :: Boolean Operators

::---------------------------------------------------------------------------
:: Preliminaries
::---------------------------------------------------------------------------

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;
  coherence
   proof s.v in (the Sorts of A).v by CIRCUIT1:5;
    hence thesis;
   end;
end;

::---------------------------------------------------------------------------
:: Boolean Operations : 2,3-Input and*, nand*, or*, nor*, xor*
::---------------------------------------------------------------------------

:: 2-Input Operators

 deffunc U(Element of BOOLEAN,Element of BOOLEAN) = $1 '&' $2;

definition
  func and2 -> Function of 2-tuples_on BOOLEAN, BOOLEAN means:
Def1: for x,y being Element of BOOLEAN holds it.<*x,y*> = x '&' y;
  existence
   proof
    thus ex t being Function of 2-tuples_on BOOLEAN, BOOLEAN st
    for x,y being Element of BOOLEAN holds t.<*x,y*> = U(x,y)
       from 2AryBooleEx;
   end;
  uniqueness
   proof
    thus for t1,t2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st
      (for x,y being Element of BOOLEAN holds t1.<*x,y*> = U(x,y)) &
      (for x,y being Element of BOOLEAN holds t2.<*x,y*> = U(x,y))
         holds t1 = t2 from 2AryBooleUniq;
   end;
  func and2a -> Function of 2-tuples_on BOOLEAN, BOOLEAN means:
Def2: for x,y being Element of BOOLEAN holds it.<*x,y*> = 'not' x '&' y;
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' $1 '&' $2;
    thus ex t being Function of 2-tuples_on BOOLEAN, BOOLEAN st
    for x,y being Element of BOOLEAN holds t.<*x,y*> = U(x,y)
       from 2AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' $1 '&' $2;
    thus for t1,t2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st
      (for x,y being Element of BOOLEAN holds t1.<*x,y*> = U(x,y)) &
      (for x,y being Element of BOOLEAN holds t2.<*x,y*> = U(x,y))
         holds t1 = t2 from 2AryBooleUniq;
   end;
  func and2b -> Function of 2-tuples_on BOOLEAN, BOOLEAN means:
Def3: for x,y being Element of BOOLEAN holds it.<*x,y*> = 'not' x '&' 'not' y;
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' $1 '&' 'not' $2;
    thus ex t being Function of 2-tuples_on BOOLEAN, BOOLEAN st
    for x,y being Element of BOOLEAN holds t.<*x,y*> = U(x,y)
       from 2AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' $1 '&' 'not' $2;
    thus for t1,t2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st
      (for x,y being Element of BOOLEAN holds t1.<*x,y*> = U(x,y)) &
      (for x,y being Element of BOOLEAN holds t2.<*x,y*> = U(x,y))
         holds t1 = t2 from 2AryBooleUniq;
   end;
end;

definition
  func nand2 -> Function of 2-tuples_on BOOLEAN, BOOLEAN means:
Def4: for x,y being Element of BOOLEAN holds it.<*x,y*> = 'not' (x '&' y);
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' ($1 '&' $2);
    thus ex t being Function of 2-tuples_on BOOLEAN, BOOLEAN st
    for x,y being Element of BOOLEAN holds t.<*x,y*> = U(x,y)
       from 2AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' ($1 '&' $2);
    thus for t1,t2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st
      (for x,y being Element of BOOLEAN holds t1.<*x,y*> = U(x,y)) &
      (for x,y being Element of BOOLEAN holds t2.<*x,y*> = U(x,y))
         holds t1 = t2 from 2AryBooleUniq;
   end;
  func nand2a -> Function of 2-tuples_on BOOLEAN, BOOLEAN means:
Def5: for x,y being Element of BOOLEAN holds
  it.<*x,y*> = 'not' ('not' x '&' y);
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' ('not' $1 '&' $2);
    thus ex t being Function of 2-tuples_on BOOLEAN, BOOLEAN st
    for x,y being Element of BOOLEAN holds t.<*x,y*> = U(x,y)
       from 2AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' ('not' $1 '&' $2);
    thus for t1,t2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st
      (for x,y being Element of BOOLEAN holds t1.<*x,y*> = U(x,y)) &
      (for x,y being Element of BOOLEAN holds t2.<*x,y*> = U(x,y))
         holds t1 = t2 from 2AryBooleUniq;
   end;
  func nand2b -> Function of 2-tuples_on BOOLEAN, BOOLEAN means:
Def6: for x,y being Element of BOOLEAN holds
  it.<*x,y*> = 'not' ('not' x '&' 'not' y);
  existence
   proof
  deffunc
   U(Element of BOOLEAN,Element of BOOLEAN) = 'not' ('not' $1 '&' 'not' $2);
    thus ex t being Function of 2-tuples_on BOOLEAN, BOOLEAN st
    for x,y being Element of BOOLEAN holds t.<*x,y*> = U(x,y)
       from 2AryBooleEx;
   end;
  uniqueness
   proof
  deffunc
   U(Element of BOOLEAN,Element of BOOLEAN) = 'not' ('not' $1 '&' 'not' $2);
    thus for t1,t2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st
      (for x,y being Element of BOOLEAN holds t1.<*x,y*> = U(x,y)) &
      (for x,y being Element of BOOLEAN holds t2.<*x,y*> = U(x,y))
         holds t1 = t2 from 2AryBooleUniq;
   end;
end;

definition
  func or2 -> Function of 2-tuples_on BOOLEAN, BOOLEAN means:
Def7: for x,y being Element of BOOLEAN holds it.<*x,y*> = x 'or' y;
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN) = $1 'or' $2;
    thus ex t being Function of 2-tuples_on BOOLEAN, BOOLEAN st
    for x,y being Element of BOOLEAN holds t.<*x,y*> = U(x,y)
       from 2AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN) = $1 'or' $2;
    thus for t1,t2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st
      (for x,y being Element of BOOLEAN holds t1.<*x,y*> = U(x,y)) &
      (for x,y being Element of BOOLEAN holds t2.<*x,y*> = U(x,y))
         holds t1 = t2 from 2AryBooleUniq;
   end;
  func or2a -> Function of 2-tuples_on BOOLEAN, BOOLEAN means:
Def8: for x,y being Element of BOOLEAN holds it.<*x,y*> = 'not' x 'or' y;
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' $1 'or' $2;
    thus ex t being Function of 2-tuples_on BOOLEAN, BOOLEAN st
    for x,y being Element of BOOLEAN holds t.<*x,y*> = U(x,y)
       from 2AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' $1 'or' $2;
    thus for t1,t2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st
      (for x,y being Element of BOOLEAN holds t1.<*x,y*> = U(x,y)) &
      (for x,y being Element of BOOLEAN holds t2.<*x,y*> = U(x,y))
         holds t1 = t2 from 2AryBooleUniq;
   end;
  func or2b -> Function of 2-tuples_on BOOLEAN, BOOLEAN means:
Def9: for x,y being Element of BOOLEAN holds it.<*x,y*> = 'not' x 'or' 'not' y;
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' $1 'or' 'not' $2;
    thus ex t being Function of 2-tuples_on BOOLEAN, BOOLEAN st
    for x,y being Element of BOOLEAN holds t.<*x,y*> = U(x,y)
       from 2AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' $1 'or' 'not' $2;
    thus for t1,t2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st
      (for x,y being Element of BOOLEAN holds t1.<*x,y*> = U(x,y)) &
      (for x,y being Element of BOOLEAN holds t2.<*x,y*> = U(x,y))
         holds t1 = t2 from 2AryBooleUniq;
   end;
end;

definition
  func nor2 -> Function of 2-tuples_on BOOLEAN, BOOLEAN means:Def10:
  for x,y being Element of BOOLEAN holds it.<*x,y*> = 'not' (x 'or' y);
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' ($1 'or' $2);
    thus ex t being Function of 2-tuples_on BOOLEAN, BOOLEAN st
    for x,y being Element of BOOLEAN holds t.<*x,y*> = U(x,y)
       from 2AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' ($1 'or' $2);
    thus for t1,t2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st
      (for x,y being Element of BOOLEAN holds t1.<*x,y*> = U(x,y)) &
      (for x,y being Element of BOOLEAN holds t2.<*x,y*> = U(x,y))
         holds t1 = t2 from 2AryBooleUniq;
   end;
  func nor2a -> Function of 2-tuples_on BOOLEAN, BOOLEAN means:Def11:
  for x,y being Element of BOOLEAN holds
    it.<*x,y*> = 'not' ('not' x 'or' y);
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' ('not' $1 'or' $2);
    thus ex t being Function of 2-tuples_on BOOLEAN, BOOLEAN st
    for x,y being Element of BOOLEAN holds t.<*x,y*> = U(x,y)
       from 2AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' ('not' $1 'or' $2);
    thus for t1,t2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st
      (for x,y being Element of BOOLEAN holds t1.<*x,y*> = U(x,y)) &
      (for x,y being Element of BOOLEAN holds t2.<*x,y*> = U(x,y))
         holds t1 = t2 from 2AryBooleUniq;
   end;
  func nor2b -> Function of 2-tuples_on BOOLEAN, BOOLEAN means:Def12:
  for x,y being Element of BOOLEAN holds
    it.<*x,y*> = 'not' ('not' x 'or' 'not' y);
  existence
   proof
  deffunc
   U(Element of BOOLEAN,Element of BOOLEAN) = 'not' ('not' $1 'or' 'not' $2);
    thus ex t being Function of 2-tuples_on BOOLEAN, BOOLEAN st
    for x,y being Element of BOOLEAN holds t.<*x,y*> = U(x,y)
       from 2AryBooleEx;
   end;
  uniqueness
   proof
  deffunc
   U(Element of BOOLEAN,Element of BOOLEAN) = 'not' ('not' $1 'or' 'not' $2);
    thus for t1,t2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st
      (for x,y being Element of BOOLEAN holds t1.<*x,y*> = U(x,y)) &
      (for x,y being Element of BOOLEAN holds t2.<*x,y*> = U(x,y))
         holds t1 = t2 from 2AryBooleUniq;
   end;
end;

definition
  func xor2 -> Function of 2-tuples_on BOOLEAN, BOOLEAN means:
Def13: for x,y being Element of BOOLEAN holds it.<*x,y*> = x 'xor' y;
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN) = $1 'xor' $2;
    thus ex t being Function of 2-tuples_on BOOLEAN, BOOLEAN st
    for x,y being Element of BOOLEAN holds t.<*x,y*> = U(x,y)
       from 2AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN) = $1 'xor' $2;
    thus for t1,t2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st
      (for x,y being Element of BOOLEAN holds t1.<*x,y*> = U(x,y)) &
      (for x,y being Element of BOOLEAN holds t2.<*x,y*> = U(x,y))
         holds t1 = t2 from 2AryBooleUniq;
   end;
  func xor2a -> Function of 2-tuples_on BOOLEAN, BOOLEAN means:
Def14: for x,y being Element of BOOLEAN holds it.<*x,y*> = 'not' x 'xor' y;
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' $1 'xor' $2;
    thus ex t being Function of 2-tuples_on BOOLEAN, BOOLEAN st
    for x,y being Element of BOOLEAN holds t.<*x,y*> = U(x,y)
       from 2AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' $1 'xor' $2;
    thus for t1,t2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st
      (for x,y being Element of BOOLEAN holds t1.<*x,y*> = U(x,y)) &
      (for x,y being Element of BOOLEAN holds t2.<*x,y*> = U(x,y))
         holds t1 = t2 from 2AryBooleUniq;
   end;
  func xor2b -> Function of 2-tuples_on BOOLEAN, BOOLEAN means:
Def15: for x,y being Element of BOOLEAN holds
  it.<*x,y*> = 'not' x 'xor' 'not' y;
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' $1 'xor' 'not' $2;
    thus ex t being Function of 2-tuples_on BOOLEAN, BOOLEAN st
    for x,y being Element of BOOLEAN holds t.<*x,y*> = U(x,y)
       from 2AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' $1 'xor' 'not' $2;
    thus for t1,t2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st
      (for x,y being Element of BOOLEAN holds t1.<*x,y*> = U(x,y)) &
      (for x,y being Element of BOOLEAN holds t2.<*x,y*> = U(x,y))
         holds t1 = t2 from 2AryBooleUniq;
   end;
end;

canceled 2;

theorem
    for x,y being Element of BOOLEAN holds and2.<*x,y*> = x '&' y &
   and2a.<*x,y*> = 'not' x '&' y & and2b.<*x,y*> = 'not' x '&' 'not' y
  by Def1,Def2,Def3;

theorem
    for x,y being Element of BOOLEAN holds nand2.<*x,y*> = 'not' (x '&' y) &
   nand2a.<*x,y*> = 'not' ('not' x '&' y) & nand2b.<*x,y*> = 'not' ('not' x '&'
'not' y)
  by Def4,Def5,Def6;

theorem
    for x,y being Element of BOOLEAN holds or2.<*x,y*> = x 'or' y &
   or2a.<*x,y*> = 'not' x 'or' y & or2b.<*x,y*> = 'not' x 'or' 'not' y
  by Def7,Def8,Def9;

theorem
    for x,y being Element of BOOLEAN holds nor2.<*x,y*> = 'not' (x 'or' y) &
   nor2a.<*x,y*> = 'not' ('not' x 'or' y) & nor2b.<*x,y*> = 'not' ('not' x 'or'
'not' y)
  by Def10,Def11,Def12;

theorem
    for x,y being Element of BOOLEAN holds xor2.<*x,y*> = x 'xor' y &
   xor2a.<*x,y*> = 'not' x 'xor' y & xor2b.<*x,y*> = 'not' x 'xor' 'not' y
  by Def13,Def14,Def15;

theorem
    for x,y being Element of BOOLEAN holds and2.<*x,y*> = nor2b.<*x,y*> &
   and2a.<*x,y*> = nor2a.<*y,x*> & and2b.<*x,y*> = nor2.<*x,y*>
  proof let x,y be Element of BOOLEAN;
    thus and2.<*x,y*> = x '&' y by Def1
                      .= 'not' ('not' x 'or' 'not' y) by BINARITH:12
                      .= nor2b.<*x,y*> by Def12;
    thus and2a.<*x,y*> = 'not' x '&' y by Def2
                      .= 'not' ('not' 'not' x 'or' 'not' y) by BINARITH:12
                      .= 'not' ('not' y 'or' x) by MARGREL1:40
                      .= nor2a.<*y,x*> by Def11;
    thus and2b.<*x,y*> = 'not' x '&' 'not' y by Def3
                .= 'not' ('not' 'not' x 'or' 'not' 'not' y) by BINARITH:12
                      .= 'not' (x 'or' 'not' 'not' y) by MARGREL1:40
                      .= 'not' (x 'or' y) by MARGREL1:40
                      .= nor2.<*x,y*> by Def10;
  end;

theorem
    for x,y being Element of BOOLEAN holds or2.<*x,y*> = nand2b.<*x,y*> &
   or2a.<*x,y*> = nand2a.<*y,x*> & or2b.<*x,y*> = nand2.<*x,y*>
  proof let x,y be Element of BOOLEAN;
    thus or2.<*x,y*> = x 'or' y by Def7
                     .= 'not' ('not' x '&' 'not' y) by BINARITH:def 1
                     .= nand2b.<*x,y*> by Def6;
    thus or2a.<*x,y*> = 'not' x 'or' y by Def8
                     .= 'not' ('not' 'not' x '&' 'not' y) by BINARITH:def 1
                     .= 'not' ('not' y '&' x) by MARGREL1:40
                     .= nand2a.<*y,x*> by Def5;
    thus or2b.<*x,y*> = 'not' x 'or' 'not' y by Def9
             .= 'not' ('not' 'not' x '&' 'not' 'not' y) by BINARITH:def 1
             .= 'not' (x '&' 'not' 'not' y) by MARGREL1:40
             .= 'not' (x '&' y) by MARGREL1:40
             .= nand2.<*x,y*> by Def4;
  end;

theorem
    for x,y being Element of BOOLEAN holds xor2b.<*x,y*> = xor2.<*x,y*>
  proof let x,y be Element of BOOLEAN;
    thus xor2b.<*x,y*> = 'not' x 'xor' 'not' y by Def15
            .= ('not' 'not' x '&' 'not' y) 'or' ('not' x '&' 'not' 'not'
y) by BINARITH:def 2
                      .= (x '&' 'not' y) 'or' ('not' x '&' 'not' 'not'
y) by MARGREL1:40
                      .= ('not' x '&' y) 'or' (x '&' 'not' y) by MARGREL1:40
                      .= x 'xor' y by BINARITH:def 2
                      .= xor2.<*x,y*> by Def13;
  end;

theorem
      and2.<*0,0*>=0 & and2.<*0,1*>=0 & and2.<*1,0*>=0 & and2.<*1,1*>=1 &
   and2a.<*0,0*>=0 & and2a.<*0,1*>=1 & and2a.<*1,0*>=0 & and2a.<*1,1*>=0 &
   and2b.<*0,0*>=1 & and2b.<*0,1*>=0 & and2b.<*1,0*>=0 & and2b.<*1,1*>=0
  proof
    thus and2.<*0,0*> = FALSE '&' FALSE by Def1,MARGREL1:36 .= 0 by MARGREL1:36
,45;
    thus and2.<*0,1*> = FALSE '&' TRUE by Def1,MARGREL1:36 .= 0 by MARGREL1:36,
45;
    thus and2.<*1,0*> = TRUE '&' FALSE by Def1,MARGREL1:36 .= 0 by MARGREL1:36,
45;
    thus and2.<*1,1*> = TRUE '&' TRUE by Def1,MARGREL1:36 .= 1 by MARGREL1:36,
45;
    thus and2a.<*0,0*> = 'not'
FALSE '&' FALSE by Def2,MARGREL1:36 .= 0 by MARGREL1:36,45;
    thus and2a.<*0,1*> = 'not' FALSE '&' TRUE by Def2,MARGREL1:36
                      .= TRUE '&' TRUE by MARGREL1:41
                      .= 1 by MARGREL1:36,45;
    thus and2a.<*1,0*> = 'not'
TRUE '&' FALSE by Def2,MARGREL1:36 .= 0 by MARGREL1:36,45;
    thus and2a.<*1,1*> = 'not' TRUE '&' TRUE by Def2,MARGREL1:36
                      .= FALSE '&' TRUE by MARGREL1:41
                      .= 0 by MARGREL1:36,45;
    thus and2b.<*0,0*> = 'not' FALSE '&' 'not' FALSE by Def3,MARGREL1:36
                      .= TRUE '&' 'not' FALSE by MARGREL1:41
                      .= TRUE '&' TRUE by MARGREL1:41
                      .= 1 by MARGREL1:36,45;
    thus and2b.<*0,1*> = 'not' FALSE '&' 'not' TRUE by Def3,MARGREL1:36
                      .= 'not' FALSE '&' FALSE by MARGREL1:41
                      .= 0 by MARGREL1:36,45;
    thus and2b.<*1,0*> = 'not' TRUE '&' 'not' FALSE by Def3,MARGREL1:36
                      .= FALSE '&' 'not' FALSE by MARGREL1:41
                      .= 0 by MARGREL1:36,45;
    thus and2b.<*1,1*> = 'not' TRUE '&' 'not' TRUE by Def3,MARGREL1:36
                      .= FALSE '&' 'not' TRUE by MARGREL1:41
                      .= 0 by MARGREL1:36,45;
  end;

theorem
      or2.<*0,0*>=0 & or2.<*0,1*>=1 & or2.<*1,0*>=1 & or2.<*1,1*>=1 &
   or2a.<*0,0*>=1 & or2a.<*0,1*>=1 & or2a.<*1,0*>=0 & or2a.<*1,1*>=1 &
   or2b.<*0,0*>=1 & or2b.<*0,1*>=1 & or2b.<*1,0*>=1 & or2b.<*1,1*>=0
  proof
    thus or2.<*0,0*> = FALSE 'or' FALSE by Def7,MARGREL1:36 .= 0 by BINARITH:7,
MARGREL1:36;
    thus or2.<*0,1*> = FALSE 'or' TRUE by Def7,MARGREL1:36 .= 1 by BINARITH:19,
MARGREL1:36;
    thus or2.<*1,0*> = TRUE 'or' FALSE by Def7,MARGREL1:36 .= 1 by BINARITH:19,
MARGREL1:36;
    thus or2.<*1,1*> = TRUE 'or' TRUE by Def7,MARGREL1:36 .= 1 by BINARITH:19,
MARGREL1:36;
    thus or2a.<*0,0*> = 'not' FALSE 'or' FALSE by Def8,MARGREL1:36
                     .= TRUE 'or' FALSE by MARGREL1:41
                     .= 1 by BINARITH:19,MARGREL1:36;
    thus or2a.<*0,1*> = 'not'
FALSE 'or' TRUE by Def8,MARGREL1:36 .= 1 by BINARITH:19,MARGREL1:36;
    thus or2a.<*1,0*> = 'not' TRUE 'or' FALSE by Def8,MARGREL1:36
                     .= FALSE 'or' FALSE by MARGREL1:41
                     .= 0 by BINARITH:7,MARGREL1:36;
    thus or2a.<*1,1*> = 'not'
TRUE 'or' TRUE by Def8,MARGREL1:36 .= 1 by BINARITH:19,MARGREL1:36;
    thus or2b.<*0,0*> = 'not' FALSE 'or' 'not' FALSE by Def9,MARGREL1:36
                     .= TRUE 'or' 'not' FALSE by MARGREL1:41
                     .= 1 by BINARITH:19,MARGREL1:36;
    thus or2b.<*0,1*> = 'not' FALSE 'or' 'not' TRUE by Def9,MARGREL1:36
                     .= TRUE 'or' 'not' TRUE by MARGREL1:41
                     .= 1 by BINARITH:19,MARGREL1:36;
    thus or2b.<*1,0*> = 'not' TRUE 'or' 'not' FALSE by Def9,MARGREL1:36
                     .= 'not' TRUE 'or' TRUE by MARGREL1:41
                     .= 1 by BINARITH:19,MARGREL1:36;
    thus or2b.<*1,1*> = 'not' TRUE 'or' 'not' TRUE by Def9,MARGREL1:36
                     .= FALSE 'or' 'not' TRUE by MARGREL1:41
                     .= FALSE 'or' FALSE by MARGREL1:41
                     .= 0 by BINARITH:7,MARGREL1:36;
  end;

theorem
      xor2.<*0,0*>=0 & xor2.<*0,1*>=1 & xor2.<*1,0*>=1 & xor2.<*1,1*>=0 &
   xor2a.<*0,0*>=1 & xor2a.<*0,1*>=0 & xor2a.<*1,0*>=0 & xor2a.<*1,1*>=1
  proof
    thus xor2.<*0,0*> = FALSE 'xor' FALSE by Def13,MARGREL1:36 .= 0 by BINARITH
:15,MARGREL1:36;
    thus xor2.<*0,1*> = FALSE 'xor' TRUE by Def13,MARGREL1:36 .= 1 by BINARITH:
14,MARGREL1:36;
    thus xor2.<*1,0*> = TRUE 'xor' FALSE by Def13,MARGREL1:36 .= 1 by BINARITH:
14,MARGREL1:36;
    thus xor2.<*1,1*> = TRUE 'xor' TRUE by Def13,MARGREL1:36 .= 0 by BINARITH:
15,MARGREL1:36;
    thus xor2a.<*0,0*> = 'not'
FALSE 'xor' FALSE by Def14,MARGREL1:36 .= 1 by BINARITH:17,MARGREL1:36;
    thus xor2a.<*0,1*> = 'not' FALSE 'xor' TRUE by Def14,MARGREL1:36
                      .= 'not' 'not' FALSE by BINARITH:13
                      .= 0 by MARGREL1:36,40;
    thus xor2a.<*1,0*> = 'not' TRUE 'xor' FALSE by Def14,MARGREL1:36
                      .= 'not' TRUE by BINARITH:14
                      .= 0 by MARGREL1:36,41;
    thus xor2a.<*1,1*> = 'not' TRUE 'xor' TRUE by Def14,MARGREL1:36
                      .= 'not' 'not' TRUE by BINARITH:13
                      .= 1 by MARGREL1:36,40;
  end;

:: 3-Input Operators

definition
  func and3 -> Function of 3-tuples_on BOOLEAN, BOOLEAN means:
Def16: for x,y,z being Element of BOOLEAN holds
   it.<*x,y,z*> = x '&' y '&' z;
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = $1 '&' $2 '&' $3;
    thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st
    for x,y,z being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z)
       from 3AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = $1 '&' $2 '&' $3;
    thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st
      (for x,y,z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) &
      (for x,y,z being Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z))
         holds t1 = t2 from 3AryBooleUniq;
   end;
  func and3a -> Function of 3-tuples_on BOOLEAN, BOOLEAN means:
Def17: for x,y,z being Element of BOOLEAN holds
   it.<*x,y,z*> = 'not' x '&' y '&' z;
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = 'not' $1 '&' $2 '&' $3;
    thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st
    for x,y,z being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z)
       from 3AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = 'not' $1 '&' $2 '&' $3;
    thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st
      (for x,y,z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) &
      (for x,y,z being Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z))
         holds t1 = t2 from 3AryBooleUniq;
   end;
  func and3b -> Function of 3-tuples_on BOOLEAN, BOOLEAN means:
Def18: for x,y,z being Element of BOOLEAN holds
   it.<*x,y,z*> = 'not' x '&' 'not' y '&' z;
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = 'not' $1 '&' 'not' $2 '&' $3;
    thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st
    for x,y,z being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z)
       from 3AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = 'not' $1 '&' 'not' $2 '&' $3;
    thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st
      (for x,y,z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) &
      (for x,y,z being Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z))
         holds t1 = t2 from 3AryBooleUniq;
   end;
  func and3c -> Function of 3-tuples_on BOOLEAN, BOOLEAN means:
Def19: for x,y,z being Element of BOOLEAN holds
   it.<*x,y,z*> = 'not' x '&' 'not' y '&' 'not' z;
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = 'not' $1 '&' 'not' $2 '&' 'not' $3;
    thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st
    for x,y,z being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z)
       from 3AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = 'not' $1 '&' 'not' $2 '&' 'not' $3;
    thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st
      (for x,y,z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) &
      (for x,y,z being Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z))
         holds t1 = t2 from 3AryBooleUniq;
   end;
end;

definition
  func nand3 -> Function of 3-tuples_on BOOLEAN, BOOLEAN means:
Def20: for x,y,z being Element of BOOLEAN holds
   it.<*x,y,z*> = 'not' (x '&' y '&' z);
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = 'not' ($1 '&' $2 '&' $3);
    thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st
    for x,y,z being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z)
       from 3AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = 'not' ($1 '&' $2 '&' $3);
    thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st
      (for x,y,z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) &
      (for x,y,z being Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z))
         holds t1 = t2 from 3AryBooleUniq;
   end;
  func nand3a -> Function of 3-tuples_on BOOLEAN, BOOLEAN means:
Def21: for x,y,z being Element of BOOLEAN holds
   it.<*x,y,z*> = 'not' ('not' x '&' y '&' z);
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = 'not' ('not' $1 '&' $2 '&' $3);
    thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st
    for x,y,z being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z)
       from 3AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = 'not' ('not' $1 '&' $2 '&' $3);
    thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st
      (for x,y,z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) &
      (for x,y,z being Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z))
         holds t1 = t2 from 3AryBooleUniq;
   end;
  func nand3b -> Function of 3-tuples_on BOOLEAN, BOOLEAN means:
Def22: for x,y,z being Element of BOOLEAN holds
   it.<*x,y,z*> = 'not' ('not' x '&' 'not' y '&' z);
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = 'not' ('not' $1 '&' 'not' $2 '&' $3);
    thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st
    for x,y,z being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z)
       from 3AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = 'not' ('not' $1 '&' 'not' $2 '&' $3);
    thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st
      (for x,y,z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) &
      (for x,y,z being Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z))
         holds t1 = t2 from 3AryBooleUniq;
   end;
  func nand3c -> Function of 3-tuples_on BOOLEAN, BOOLEAN means:
Def23: for x,y,z being Element of BOOLEAN holds
   it.<*x,y,z*> = 'not' ('not' x '&' 'not' y '&' 'not' z);
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = 'not' ('not' $1 '&' 'not' $2 '&' 'not' $3);
    thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st
    for x,y,z being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z)
       from 3AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = 'not' ('not' $1 '&' 'not' $2 '&' 'not' $3);
    thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st
      (for x,y,z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) &
      (for x,y,z being Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z))
         holds t1 = t2 from 3AryBooleUniq;
   end;
end;

definition
  func or3 -> Function of 3-tuples_on BOOLEAN, BOOLEAN means:
Def24: for x,y,z being Element of BOOLEAN holds
   it.<*x,y,z*> = x 'or' y 'or' z;
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = $1 'or' $2 'or' $3;
    thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st
    for x,y,z being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z)
       from 3AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = $1 'or' $2 'or' $3;
    thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st
      (for x,y,z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) &
      (for x,y,z being Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z))
         holds t1 = t2 from 3AryBooleUniq;
   end;
  func or3a -> Function of 3-tuples_on BOOLEAN, BOOLEAN means:
Def25: for x,y,z being Element of BOOLEAN holds
   it.<*x,y,z*> = 'not' x 'or' y 'or' z;
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = 'not' $1 'or' $2 'or' $3;
    thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st
    for x,y,z being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z)
       from 3AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = 'not' $1 'or' $2 'or' $3;
    thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st
      (for x,y,z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) &
      (for x,y,z being Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z))
         holds t1 = t2 from 3AryBooleUniq;
   end;
  func or3b -> Function of 3-tuples_on BOOLEAN, BOOLEAN means:
Def26: for x,y,z being Element of BOOLEAN holds
   it.<*x,y,z*> = 'not' x 'or' 'not' y 'or' z;
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = 'not' $1 'or' 'not' $2 'or' $3;
    thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st
    for x,y,z being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z)
       from 3AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = 'not' $1 'or' 'not' $2 'or' $3;
    thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st
      (for x,y,z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) &
      (for x,y,z being Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z))
         holds t1 = t2 from 3AryBooleUniq;
   end;
  func or3c -> Function of 3-tuples_on BOOLEAN, BOOLEAN means:
Def27: for x,y,z being Element of BOOLEAN holds
   it.<*x,y,z*> = 'not' x 'or' 'not' y 'or' 'not' z;
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = 'not' $1 'or' 'not' $2 'or' 'not' $3;
    thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st
    for x,y,z being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z)
       from 3AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = 'not' $1 'or' 'not' $2 'or' 'not' $3;
    thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st
      (for x,y,z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) &
      (for x,y,z being Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z))
         holds t1 = t2 from 3AryBooleUniq;
   end;
end;

definition
  func nor3 -> Function of 3-tuples_on BOOLEAN, BOOLEAN means:
Def28: for x,y,z being Element of BOOLEAN holds
   it.<*x,y,z*> = 'not' (x 'or' y 'or' z);
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = 'not' ($1 'or' $2 'or' $3);
    thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st
    for x,y,z being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z)
       from 3AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = 'not' ($1 'or' $2 'or' $3);
    thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st
      (for x,y,z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) &
      (for x,y,z being Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z))
         holds t1 = t2 from 3AryBooleUniq;
   end;
  func nor3a -> Function of 3-tuples_on BOOLEAN, BOOLEAN means:
Def29: for x,y,z being Element of BOOLEAN holds
   it.<*x,y,z*> = 'not' ('not' x 'or' y 'or' z);
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = 'not' ('not' $1 'or' $2 'or' $3);
    thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st
    for x,y,z being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z)
       from 3AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = 'not' ('not' $1 'or' $2 'or' $3);
    thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st
      (for x,y,z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) &
      (for x,y,z being Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z))
         holds t1 = t2 from 3AryBooleUniq;
   end;
  func nor3b -> Function of 3-tuples_on BOOLEAN, BOOLEAN means:
Def30: for x,y,z being Element of BOOLEAN holds
   it.<*x,y,z*> = 'not' ('not' x 'or' 'not' y 'or' z);
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = 'not' ('not' $1 'or' 'not' $2 'or' $3);
    thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st
    for x,y,z being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z)
       from 3AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = 'not' ('not' $1 'or' 'not' $2 'or' $3);
    thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st
      (for x,y,z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) &
      (for x,y,z being Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z))
         holds t1 = t2 from 3AryBooleUniq;
   end;
  func nor3c -> Function of 3-tuples_on BOOLEAN, BOOLEAN means:
Def31: for x,y,z being Element of BOOLEAN holds
   it.<*x,y,z*> = 'not' ('not' x 'or' 'not' y 'or' 'not' z);
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = 'not' ('not' $1 'or' 'not' $2 'or' 'not' $3);
    thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st
    for x,y,z being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z)
       from 3AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = 'not' ('not' $1 'or' 'not' $2 'or' 'not' $3);
    thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st
      (for x,y,z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) &
      (for x,y,z being Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z))
         holds t1 = t2 from 3AryBooleUniq;
   end;
end;

definition
  func xor3 -> Function of 3-tuples_on BOOLEAN, BOOLEAN means:
Def32: for x,y,z being Element of BOOLEAN holds
   it.<*x,y,z*> = x 'xor' y 'xor' z;
  existence
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = $1 'xor' $2 'xor' $3;
    thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st
    for x,y,z being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z)
       from 3AryBooleEx;
   end;
  uniqueness
   proof
  deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN)
          = $1 'xor' $2 'xor' $3;
    thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st
      (for x,y,z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) &
      (for x,y,z being Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z))
         holds t1 = t2 from 3AryBooleUniq;
   end;
end;

theorem
    for x,y,z being Element of BOOLEAN holds and3.<*x,y,z*> = x '&' y '&' z &
   and3a.<*x,y,z*> = 'not' x '&' y '&' z &
   and3b.<*x,y,z*> = 'not' x '&' 'not' y '&' z &
   and3c.<*x,y,z*> = 'not' x '&' 'not' y '&' 'not' z
  by Def16,Def17,Def18,Def19;

theorem
    for x,y,z being Element of BOOLEAN holds
  nand3.<*x,y,z*>='not' (x '&' y '&' z) &
   nand3a.<*x,y,z*>='not' ('not' x '&' y '&' z) &
   nand3b.<*x,y,z*>='not' ('not' x '&' 'not' y '&' z) &
   nand3c.<*x,y,z*>='not' ('not' x '&' 'not' y '&' 'not' z)
  by Def20,Def21,Def22,Def23;

theorem
    for x,y,z being Element of BOOLEAN holds or3.<*x,y,z*> = x 'or' y 'or' z &
   or3a.<*x,y,z*> = 'not' x 'or' y 'or' z & or3b.<*x,y,z*> = 'not' x 'or' 'not'
y 'or' z &
   or3c.<*x,y,z*> = 'not' x 'or' 'not' y 'or' 'not' z
  by Def24,Def25,Def26,Def27;

theorem
    for x,y,z being Element of BOOLEAN holds nor3.<*x,y,z*>='not'
(x 'or' y 'or' z) &
   nor3a.<*x,y,z*>='not' ('not' x 'or' y 'or' z) & nor3b.<*x,y,z*>='not' ('not'
x 'or' 'not' y 'or' z) &
   nor3c.<*x,y,z*>='not' ('not' x 'or' 'not' y 'or' 'not' z)
  by Def28,Def29,Def30,Def31;

canceled;

theorem
    for x,y,z being Element of BOOLEAN holds
    and3.<*x,y,z*> = nor3c.<*x,y,z*> & and3a.<*x,y,z*> = nor3b.<*z,y,x*> &
   and3b.<*x,y,z*> = nor3a.<*z,y,x*> & and3c.<*x,y,z*> = nor3.<*x,y,z*>
  proof let x,y,z be Element of BOOLEAN;
    thus and3.<*x,y,z*> = x '&' y '&' z by Def16
                        .= 'not' ('not' x 'or' 'not'
y) '&' z by BINARITH:12
                        .= 'not' ('not' 'not' ('not' x 'or' 'not' y) 'or' 'not'
z) by BINARITH:12
                        .= 'not' (('not' x 'or' 'not' y) 'or' 'not'
z) by MARGREL1:40
                        .= nor3c.<*x,y,z*> by Def31;
    thus and3a.<*x,y,z*> = 'not' x '&' y '&' z by Def17
                        .= 'not' ('not' 'not' x 'or' 'not'
y) '&' z by BINARITH:12
         .= 'not' ('not' 'not' ('not' 'not' x 'or' 'not' y) 'or' 'not'
z) by BINARITH:12
         .= 'not' (('not' 'not' x 'or' 'not' y) 'or' 'not'
z) by MARGREL1:40
                        .= 'not' (('not' y 'or' x) 'or' 'not' z) by MARGREL1:40
                        .= 'not' (('not' z 'or' 'not'
y) 'or' x) by BINARITH:20
                        .= nor3b.<*z,y,x*> by Def30;
    thus and3b.<*x,y,z*> = 'not' x '&' 'not' y '&' z by Def18
                        .= 'not' ('not' 'not' x 'or' 'not' 'not'
y) '&' z by BINARITH:12
            .= 'not' ('not' 'not' ('not' 'not' x 'or' 'not' 'not' y) 'or'
'not' z) by BINARITH:12
            .= 'not' (('not' 'not' x 'or' 'not' 'not' y) 'or' 'not'
z) by MARGREL1:40
            .= 'not' ((x 'or' 'not' 'not' y) 'or' 'not'
z) by MARGREL1:40
            .= 'not' ((y 'or' x) 'or' 'not' z) by MARGREL1:40
            .= 'not' (('not' z 'or' y) 'or' x) by BINARITH:20
            .= nor3a.<*z,y,x*> by Def29;
    thus and3c.<*x,y,z*> = 'not' x '&' 'not' y '&' 'not' z by Def19
            .= 'not' ('not' 'not' x 'or' 'not' 'not' y) '&' 'not'
z by BINARITH:12
            .= 'not' ('not' 'not' ('not' 'not' x 'or' 'not' 'not' y) 'or'
'not' 'not' z) by BINARITH:12
            .= 'not' (('not' 'not' x 'or' 'not' 'not' y) 'or' 'not' 'not'
z) by MARGREL1:40
            .= 'not' ((x 'or' 'not' 'not' y) 'or' 'not' 'not'
z) by MARGREL1:40
            .= 'not' ((x 'or' y) 'or' 'not' 'not'
z) by MARGREL1:40
            .= 'not' ((x 'or' y) 'or' z) by MARGREL1:40
            .= nor3.<*x,y,z*> by Def28;
  end;

theorem
    for x,y,z being Element of BOOLEAN holds
    or3.<*x,y,z*> = nand3c.<*x,y,z*> & or3a.<*x,y,z*> = nand3b.<*z,y,x*> &
   or3b.<*x,y,z*> = nand3a.<*z,y,x*> & or3c.<*x,y,z*> = nand3.<*x,y,z*>
  proof let x,y,z be Element of BOOLEAN;
    thus or3.<*x,y,z*> = x 'or' y 'or' z by Def24
                       .= 'not' ('not' x '&' 'not'
y) 'or' z by BINARITH:def 1
                       .= 'not' ('not' 'not' ('not' x '&' 'not' y) '&' 'not'
z) by BINARITH:def 1
                       .= 'not' (('not' x '&' 'not' y) '&' 'not'
z) by MARGREL1:40
                       .= nand3c.<*x,y,z*> by Def23;
    thus or3a.<*x,y,z*> = 'not' x 'or' y 'or' z by Def25
                       .= 'not' ('not' 'not' x '&' 'not'
y) 'or' z by BINARITH:def 1
            .= 'not' ('not' 'not' ('not' 'not' x '&' 'not' y) '&' 'not'
z) by BINARITH:def 1
                       .= 'not' (('not' 'not' x '&' 'not' y) '&' 'not'
z) by MARGREL1:40
                       .= 'not' ((x '&' 'not' y) '&' 'not'
z) by MARGREL1:40
                       .= 'not' ('not' z '&' 'not'
y '&' x) by MARGREL1:52
                       .= nand3b.<*z,y,x*> by Def22;
    thus or3b.<*x,y,z*> = 'not' x 'or' 'not' y 'or' z by Def26
                       .= 'not' ('not' 'not' x '&' 'not' 'not'
y) 'or' z by BINARITH:def 1
            .= 'not' ('not' 'not' ('not' 'not' x '&' 'not' 'not' y) '&'
'not' z) by BINARITH:def 1
                       .= 'not' (('not' 'not' x '&' 'not' 'not' y) '&' 'not'
z) by MARGREL1:40
                       .= 'not' ((x '&' 'not' 'not' y) '&' 'not'
z) by MARGREL1:40
                       .= 'not' ((x '&' y) '&' 'not' z) by MARGREL1:40
                       .= 'not' ('not' z '&' y '&' x) by MARGREL1:52
                       .= nand3a.<*z,y,x*> by Def21;
    thus or3c.<*x,y,z*> = 'not' x 'or' 'not' y 'or' 'not' z by Def27
                       .= 'not' ('not' 'not' x '&' 'not' 'not' y) 'or' 'not'
z by BINARITH:def 1
            .= 'not' ('not' 'not' ('not' 'not' x '&' 'not' 'not' y) '&'
'not' 'not' z) by BINARITH:def 1
            .= 'not' (('not' 'not' x '&' 'not' 'not' y) '&' 'not' 'not'
z) by MARGREL1:40
                       .= 'not' ((x '&' 'not' 'not' y) '&' 'not' 'not'
z) by MARGREL1:40
                       .= 'not' ((x '&' y) '&' 'not' 'not'
z) by MARGREL1:40
                       .= 'not' ((x '&' y) '&' z) by MARGREL1:40
                       .= nand3.<*x,y,z*> by Def20;
  end;

theorem ::ThCalAnd3:
      and3.<*0,0,0*>=0 & and3.<*0,0,1*>=0 & and3.<*0,1,0*>=0 &
    and3.<*0,1,1*>=0 & and3.<*1,0,0*>=0 & and3.<*1,0,1*>=0 &
    and3.<*1,1,0*>=0 & and3.<*1,1,1*>=1
  proof
    thus and3.<*0,0,0*> = FALSE '&' FALSE '&' FALSE by Def16,MARGREL1:36
                       .= 0 by MARGREL1:36,45;
    thus and3.<*0,0,1*> = FALSE '&' FALSE '&' TRUE by Def16,MARGREL1:36
                       .= FALSE '&' TRUE by MARGREL1:45
                       .= 0 by MARGREL1:36,45;
    thus and3.<*0,1,0*> = FALSE '&' TRUE '&' FALSE by Def16,MARGREL1:36
                       .= 0 by MARGREL1:36,45;
    thus and3.<*0,1,1*> = FALSE '&' TRUE '&' TRUE by Def16,MARGREL1:36
                       .= FALSE '&' TRUE by MARGREL1:45
                       .= 0 by MARGREL1:36,45;
    thus and3.<*1,0,0*> = TRUE '&' FALSE '&' FALSE by Def16,MARGREL1:36
                       .= 0 by MARGREL1:36,45;
    thus and3.<*1,0,1*> = TRUE '&' FALSE '&' TRUE by Def16,MARGREL1:36
                       .= FALSE '&' TRUE by MARGREL1:45
                       .= 0 by MARGREL1:36,45;
    thus and3.<*1,1,0*> = TRUE '&' TRUE '&' FALSE by Def16,MARGREL1:36
                       .= 0 by MARGREL1:36,45;
    thus and3.<*1,1,1*> = TRUE '&' TRUE '&' TRUE by Def16,MARGREL1:36
                       .= TRUE '&' TRUE by MARGREL1:45
                       .= 1 by MARGREL1:36,45;
  end;

theorem
      and3a.<*0,0,0*>=0 & and3a.<*0,0,1*>=0 & and3a.<*0,1,0*>=0 &
    and3a.<*0,1,1*>=1 & and3a.<*1,0,0*>=0 & and3a.<*1,0,1*>=0 &
    and3a.<*1,1,0*>=0 & and3a.<*1,1,1*>=0
  proof
    thus and3a.<*0,0,0*> = 'not' FALSE '&' FALSE '&' FALSE by Def17,MARGREL1:36
                        .= 0 by MARGREL1:36,45;
    thus and3a.<*0,0,1*> = 'not' FALSE '&' FALSE '&' TRUE by Def17,MARGREL1:36
                        .= FALSE '&' TRUE by MARGREL1:45
                        .= 0 by MARGREL1:36,45;
    thus and3a.<*0,1,0*> = 'not' FALSE '&' TRUE '&' FALSE by Def17,MARGREL1:36
                        .= 0 by MARGREL1:36,45;
    thus and3a.<*0,1,1*> = (TRUE '&' 'not' FALSE) '&' TRUE by Def17,MARGREL1:36
                        .= 'not' FALSE '&' TRUE by MARGREL1:50
                        .= TRUE '&' TRUE by MARGREL1:41
                        .= 1 by MARGREL1:36,45;
    thus and3a.<*1,0,0*> = 'not' TRUE '&' FALSE '&' FALSE by Def17,MARGREL1:36
                        .= 0 by MARGREL1:36,45;
    thus and3a.<*1,0,1*> = 'not' TRUE '&' FALSE '&' TRUE by Def17,MARGREL1:36
                        .= FALSE '&' TRUE by MARGREL1:45
                        .= 0 by MARGREL1:36,45;
    thus and3a.<*1,1,0*> = 'not' TRUE '&' TRUE '&' FALSE by Def17,MARGREL1:36
                        .= 0 by MARGREL1:36,45;
    thus and3a.<*1,1,1*> = (TRUE '&' 'not' TRUE) '&' TRUE by Def17,MARGREL1:36
                        .= 'not' TRUE '&' TRUE by MARGREL1:50
                        .= FALSE '&' TRUE by MARGREL1:41
                        .= 0 by MARGREL1:36,45;
  end;

theorem ::ThCalAnd3_b:
      and3b.<*0,0,0*>=0 & and3b.<*0,0,1*>=1 & and3b.<*0,1,0*>=0 &
    and3b.<*0,1,1*>=0 & and3b.<*1,0,0*>=0 & and3b.<*1,0,1*>=0 &
    and3b.<*1,1,0*>=0 & and3b.<*1,1,1*>=0
  proof
    thus and3b.<*0,0,0*> = 'not' FALSE '&' 'not' FALSE '&' FALSE by Def18,
MARGREL1:36
                        .= 0 by MARGREL1:36,45;
    thus and3b.<*0,0,1*> = 'not' FALSE '&' 'not' FALSE '&' TRUE by Def18,
MARGREL1:36
                        .= TRUE '&' 'not' FALSE '&' TRUE by MARGREL1:41
                        .= TRUE '&' TRUE '&' TRUE by MARGREL1:41
                        .= TRUE '&' TRUE by MARGREL1:45
                        .= 1 by MARGREL1:36,45;
    thus and3b.<*0,1,0*> = 'not' FALSE '&' 'not' TRUE '&' FALSE by Def18,
MARGREL1:36
                        .= 0 by MARGREL1:36,45;
    thus and3b.<*0,1,1*> = 'not' FALSE '&' 'not' TRUE '&' TRUE by Def18,
MARGREL1:36
                        .= 'not' FALSE '&' FALSE '&' TRUE by MARGREL1:41
                        .= FALSE '&' TRUE by MARGREL1:45
                        .= 0 by MARGREL1:36,45;
    thus and3b.<*1,0,0*> = 'not' TRUE '&' 'not' FALSE '&' FALSE by Def18,
MARGREL1:36
                        .= 0 by MARGREL1:36,45;
    thus and3b.<*1,0,1*> = 'not' TRUE '&' 'not' FALSE '&' TRUE by Def18,
MARGREL1:36
                        .= FALSE '&' 'not' FALSE '&' TRUE by MARGREL1:41
                        .= FALSE '&' TRUE by MARGREL1:45
                        .= 0 by MARGREL1:36,45;
    thus and3b.<*1,1,0*> = 'not' TRUE '&' 'not' TRUE '&' FALSE by Def18,
MARGREL1:36
                        .= 0 by MARGREL1:36,45;
    thus and3b.<*1,1,1*> = 'not' TRUE '&' 'not' TRUE '&' TRUE by Def18,MARGREL1
:36
                        .= FALSE '&' 'not' TRUE '&' TRUE by MARGREL1:41
                        .= FALSE '&' TRUE by MARGREL1:45
                        .= 0 by MARGREL1:36,45;
  end;

theorem ::ThCalAnd3_c:
      and3c.<*0,0,0*>=1 & and3c.<*0,0,1*>=0 & and3c.<*0,1,0*>=0 &
    and3c.<*0,1,1*>=0 & and3c.<*1,0,0*>=0 & and3c.<*1,0,1*>=0 &
    and3c.<*1,1,0*>=0 & and3c.<*1,1,1*>=0
  proof
    thus and3c.<*0,0,0*> = 'not' FALSE '&' 'not' FALSE '&' 'not' FALSE
          by Def19,MARGREL1:36
                        .= TRUE '&' 'not' FALSE '&' 'not' FALSE by MARGREL1:41
                        .= TRUE '&' TRUE '&' 'not' FALSE by MARGREL1:41
                        .= TRUE '&' TRUE '&' TRUE by MARGREL1:41
                        .= TRUE '&' TRUE by MARGREL1:45
                        .= 1 by MARGREL1:36,45;
    thus and3c.<*0,0,1*> = 'not' FALSE '&' 'not' FALSE '&' 'not' TRUE
    by Def19,MARGREL1:36
                        .= 'not' FALSE '&' 'not' FALSE '&' FALSE by MARGREL1:41
                        .= 0 by MARGREL1:36,45;
    thus and3c.<*0,1,0*> = 'not' FALSE '&' 'not' TRUE '&' 'not' FALSE
    by Def19,MARGREL1:36
                        .= 'not' FALSE '&' FALSE '&' 'not' FALSE by MARGREL1:41
                        .= 'not' FALSE '&' 'not' FALSE '&' FALSE by MARGREL1:52
                        .= 0 by MARGREL1:36,45;
    thus and3c.<*0,1,1*> = 'not' FALSE '&' 'not' TRUE '&' 'not' TRUE
    by Def19,MARGREL1:36
                        .= 'not' FALSE '&' 'not' TRUE '&' FALSE by MARGREL1:41
                        .= 0 by MARGREL1:36,45;
    thus and3c.<*1,0,0*> = 'not' TRUE '&' 'not' FALSE '&' 'not' FALSE
    by Def19,MARGREL1:36
                 .= FALSE '&' 'not' FALSE '&' 'not' FALSE by MARGREL1:41
                 .= 'not' FALSE '&' 'not' FALSE '&' FALSE by MARGREL1:52
                 .= 0 by MARGREL1:36,45;
    thus and3c.<*1,0,1*> = 'not' TRUE '&' 'not' FALSE '&' 'not' TRUE
    by Def19,MARGREL1:36
                 .= 'not' TRUE '&' 'not' FALSE '&' FALSE by MARGREL1:41
                 .= 0 by MARGREL1:36,45;
    thus and3c.<*1,1,0*> = 'not' TRUE '&' 'not' TRUE '&' 'not' FALSE
    by Def19,MARGREL1:36
                        .= FALSE '&' 'not' TRUE '&' 'not' FALSE by MARGREL1:41
                        .= 'not' TRUE '&' 'not' FALSE '&' FALSE by MARGREL1:52
                        .= 0 by MARGREL1:36,45;
    thus and3c.<*1,1,1*> = 'not' TRUE '&' 'not' TRUE '&' 'not' TRUE
    by Def19,MARGREL1:36
                        .= 'not' TRUE '&' 'not' TRUE '&' FALSE by MARGREL1:41
                        .= 0 by MARGREL1:36,45;
  end;

theorem ::ThCalOr3:
      or3.<*0,0,0*> = 0 & or3.<*0,0,1*> = 1 & or3.<*0,1,0*> = 1 &
    or3.<*0,1,1*> = 1 & or3.<*1,0,0*> = 1 & or3.<*1,0,1*> = 1 &
    or3.<*1,1,0*> = 1 & or3.<*1,1,1*> = 1
  proof
    thus or3.<*0,0,0*> = FALSE 'or' FALSE 'or' FALSE by Def24,MARGREL1:36
                        .= FALSE 'or' FALSE by BINARITH:7
                        .= 0 by BINARITH:7,MARGREL1:36;
    thus or3.<*0,0,1*> = FALSE 'or' FALSE 'or' TRUE by Def24,MARGREL1:36
                        .= 1 by BINARITH:19,MARGREL1:36;
    thus or3.<*0,1,0*> = FALSE 'or' TRUE 'or' FALSE by Def24,MARGREL1:36
                        .= TRUE 'or' FALSE by BINARITH:19
                        .= 1 by BINARITH:19,MARGREL1:36;
    thus or3.<*0,1,1*> = FALSE 'or' TRUE 'or' TRUE by Def24,MARGREL1:36
                        .= 1 by BINARITH:19,MARGREL1:36;
    thus or3.<*1,0,0*> = TRUE 'or' FALSE 'or' FALSE by Def24,MARGREL1:36
                        .= TRUE 'or' FALSE by BINARITH:7
                        .= 1 by BINARITH:19,MARGREL1:36;
    thus or3.<*1,0,1*> = TRUE 'or' FALSE 'or' TRUE by Def24,MARGREL1:36
                        .= 1 by BINARITH:19,MARGREL1:36;
    thus or3.<*1,1,0*> = TRUE 'or' TRUE 'or' FALSE by Def24,MARGREL1:36
                        .= TRUE 'or' FALSE by BINARITH:19
                        .= 1 by BINARITH:19,MARGREL1:36;
    thus or3.<*1,1,1*> = TRUE 'or' TRUE 'or' TRUE by Def24,MARGREL1:36
                        .= 1 by BINARITH:19,MARGREL1:36;
  end;

theorem ::ThCalOr3_a:
      or3a.<*0,0,0*> = 1 & or3a.<*0,0,1*> = 1 & or3a.<*0,1,0*> = 1 &
    or3a.<*0,1,1*> = 1 & or3a.<*1,0,0*> = 0 & or3a.<*1,0,1*> = 1 &
    or3a.<*1,1,0*> = 1 & or3a.<*1,1,1*> = 1
  proof
    thus or3a.<*0,0,0*> = 'not' FALSE 'or' FALSE 'or' FALSE by Def25,MARGREL1:
36
                        .= 'not' FALSE 'or' FALSE by BINARITH:7
                        .= TRUE 'or' FALSE by MARGREL1:41
                        .= 1 by BINARITH:19,MARGREL1:36;
    thus or3a.<*0,0,1*> = 'not' FALSE 'or' FALSE 'or' TRUE by Def25,MARGREL1:36
                        .= 1 by BINARITH:19,MARGREL1:36;
    thus or3a.<*0,1,0*> = 'not' FALSE 'or' TRUE 'or' FALSE by Def25,MARGREL1:36
                        .= TRUE 'or' FALSE by BINARITH:19
                        .= 1 by BINARITH:19,MARGREL1:36;
    thus or3a.<*0,1,1*> = 'not' FALSE 'or' TRUE 'or' TRUE by Def25,MARGREL1:36
                        .= 1 by BINARITH:19,MARGREL1:36;
    thus or3a.<*1,0,0*> = 'not' TRUE 'or' FALSE 'or' FALSE by Def25,MARGREL1:36
                        .= 'not' TRUE 'or' FALSE by BINARITH:7
                        .= FALSE 'or' FALSE by MARGREL1:41
                        .= 0 by BINARITH:7,MARGREL1:36;
    thus or3a.<*1,0,1*> = 'not' TRUE 'or' FALSE 'or' TRUE by Def25,MARGREL1:36
                        .= 1 by BINARITH:19,MARGREL1:36;
    thus or3a.<*1,1,0*> = 'not' TRUE 'or' TRUE 'or' FALSE by Def25,MARGREL1:36
                        .= TRUE 'or' FALSE by BINARITH:19
                        .= 1 by BINARITH:19,MARGREL1:36;
    thus or3a.<*1,1,1*> = 'not' TRUE 'or' TRUE 'or' TRUE by Def25,MARGREL1:36
                        .= 1 by BINARITH:19,MARGREL1:36;
  end;

theorem ::ThCalOr3_b:
      or3b.<*0,0,0*> = 1 & or3b.<*0,0,1*> = 1 & or3b.<*0,1,0*> = 1 &
    or3b.<*0,1,1*> = 1 & or3b.<*1,0,0*> = 1 & or3b.<*1,0,1*> = 1 &
    or3b.<*1,1,0*> = 0 & or3b.<*1,1,1*> = 1
  proof
    thus or3b.<*0,0,0*> = 'not' FALSE 'or' 'not' FALSE 'or' FALSE by Def26,
MARGREL1:36
                        .= TRUE 'or' 'not' FALSE 'or' FALSE by MARGREL1:41
                        .= TRUE 'or' FALSE by BINARITH:19
                        .= 1 by BINARITH:19,MARGREL1:36;
    thus or3b.<*0,0,1*> = 'not' FALSE 'or' 'not' FALSE 'or' TRUE by Def26,
MARGREL1:36
                        .= 1 by BINARITH:19,MARGREL1:36;
    thus or3b.<*0,1,0*> = 'not' FALSE 'or' 'not' TRUE 'or' FALSE by Def26,
MARGREL1:36
                        .= 'not' FALSE 'or' 'not' TRUE by BINARITH:7
                        .= TRUE 'or' 'not' TRUE by MARGREL1:41
                        .= 1 by BINARITH:19,MARGREL1:36;
    thus or3b.<*0,1,1*> = 'not' FALSE 'or' 'not' TRUE 'or' TRUE by Def26,
MARGREL1:36
                        .= 1 by BINARITH:19,MARGREL1:36;
    thus or3b.<*1,0,0*> = 'not' TRUE 'or' 'not' FALSE 'or' FALSE by Def26,
MARGREL1:36
                        .= 'not' TRUE 'or' 'not' FALSE by BINARITH:7
                        .= 'not' TRUE 'or' TRUE by MARGREL1:41
                        .= 1 by BINARITH:19,MARGREL1:36;
    thus or3b.<*1,0,1*> = 'not' TRUE 'or' 'not' FALSE 'or' TRUE by Def26,
MARGREL1:36
                        .= 1 by BINARITH:19,MARGREL1:36;
    thus or3b.<*1,1,0*> = 'not' TRUE 'or' 'not' TRUE 'or' FALSE by Def26,
MARGREL1:36
                        .= 'not' TRUE 'or' 'not' TRUE by BINARITH:7
                        .= FALSE 'or' 'not' TRUE by MARGREL1:41
                        .= FALSE 'or' FALSE by MARGREL1:41
                        .= 0 by BINARITH:7,MARGREL1:36;
    thus or3b.<*1,1,1*> = 'not' TRUE 'or' 'not' TRUE 'or' TRUE by Def26,
MARGREL1:36
                        .= 1 by BINARITH:19,MARGREL1:36;
  end;

theorem ::ThCalOr3_c:
      or3c.<*0,0,0*> = 1 & or3c.<*0,0,1*> = 1 & or3c.<*0,1,0*> = 1 &
    or3c.<*0,1,1*> = 1 & or3c.<*1,0,0*> = 1 & or3c.<*1,0,1*> = 1 &
    or3c.<*1,1,0*> = 1 & or3c.<*1,1,1*> = 0
  proof
    thus or3c.<*0,0,0*> = 'not' FALSE 'or' 'not' FALSE 'or' 'not' FALSE
    by Def27,MARGREL1:36
            .= 'not' FALSE 'or' 'not' FALSE 'or' TRUE by MARGREL1:41
            .= 1 by BINARITH:19,MARGREL1:36;
    thus or3c.<*0,0,1*> = 'not' FALSE 'or' 'not' FALSE 'or' 'not'
TRUE by Def27,MARGREL1:36
                        .= 'not' FALSE 'or' 'not' FALSE 'or' FALSE
                        by MARGREL1:41
                        .= 'not' FALSE 'or' 'not' FALSE by BINARITH:7
                        .= TRUE 'or' 'not' FALSE by MARGREL1:41
                        .= 1 by BINARITH:19,MARGREL1:36;
    thus or3c.<*0,1,0*> = 'not' FALSE 'or' 'not' TRUE 'or' 'not'
FALSE by Def27,MARGREL1:36
                        .= 'not' FALSE 'or' 'not' TRUE 'or' TRUE by MARGREL1:41
                        .= 1 by BINARITH:19,MARGREL1:36;
    thus or3c.<*0,1,1*> = 'not' FALSE 'or' 'not' TRUE 'or' 'not' TRUE
    by Def27,MARGREL1:36
                        .= TRUE 'or' 'not' TRUE 'or' 'not' TRUE by MARGREL1:41
                        .= TRUE 'or' 'not' TRUE by BINARITH:19
                        .= 1 by BINARITH:19,MARGREL1:36;
    thus or3c.<*1,0,0*> = 'not' TRUE 'or' 'not' FALSE 'or' 'not'
FALSE by Def27,MARGREL1:36
                        .= 'not' TRUE 'or' 'not' FALSE 'or' TRUE by MARGREL1:41
                        .= 1 by BINARITH:19,MARGREL1:36;
    thus or3c.<*1,0,1*> = 'not' TRUE 'or' 'not' FALSE 'or' 'not' TRUE
    by Def27,MARGREL1:36
                        .= 'not' TRUE 'or' TRUE 'or' 'not' TRUE by MARGREL1:41
                        .= TRUE 'or' 'not' TRUE by BINARITH:19
                        .= 1 by BINARITH:19,MARGREL1:36;
    thus or3c.<*1,1,0*> = 'not' TRUE 'or' 'not' TRUE 'or' 'not' FALSE
    by Def27,MARGREL1:36
                        .= 'not' TRUE 'or' 'not' TRUE 'or' TRUE by MARGREL1:41
                        .= 1 by BINARITH:19,MARGREL1:36;
    thus or3c.<*1,1,1*> = 'not' TRUE 'or' 'not' TRUE 'or' 'not' TRUE
    by Def27,MARGREL1:36
                        .= FALSE 'or' 'not' TRUE 'or' 'not' TRUE by MARGREL1:41
                        .= FALSE 'or' FALSE 'or' 'not' TRUE by MARGREL1:41
                        .= FALSE 'or' FALSE 'or' FALSE by MARGREL1:41
                        .= FALSE 'or' FALSE by BINARITH:7
                        .= 0 by BINARITH:7,MARGREL1:36;
  end;

theorem ::ThCalXOr3:
      xor3.<*0,0,0*> = 0 & xor3.<*0,0,1*> = 1 & xor3.<*0,1,0*> = 1 &
    xor3.<*0,1,1*> = 0 & xor3.<*1,0,0*> = 1 & xor3.<*1,0,1*> = 0 &
    xor3.<*1,1,0*> = 0 & xor3.<*1,1,1*> = 1
  proof
    thus xor3.<*0,0,0*> = FALSE 'xor' FALSE 'xor' FALSE by Def32,MARGREL1:36
                        .= FALSE 'xor' FALSE by BINARITH:15
                        .= 0 by BINARITH:15,MARGREL1:36;
    thus xor3.<*0,0,1*> = FALSE 'xor' FALSE 'xor' TRUE by Def32,MARGREL1:36
                        .= 1 by BINARITH:15,33,MARGREL1:36;
    thus xor3.<*0,1,0*> = 1 by Def32,BINARITH:33,MARGREL1:36;
    thus xor3.<*0,1,1*> = TRUE 'xor' TRUE by Def32,BINARITH:33,MARGREL1:36
                        .= 0 by BINARITH:15,MARGREL1:36;
    thus xor3.<*1,0,0*> = 1 by Def32,BINARITH:33,MARGREL1:36;
    thus xor3.<*1,0,1*> = TRUE 'xor' TRUE by Def32,BINARITH:33,MARGREL1:36
                        .= 0 by BINARITH:15,MARGREL1:36;
    thus xor3.<*1,1,0*> = TRUE 'xor' TRUE 'xor' FALSE by Def32,MARGREL1:36
                        .= FALSE 'xor' FALSE by BINARITH:15
                        .= 0 by BINARITH:15,MARGREL1:36;
    thus xor3.<*1,1,1*> = TRUE 'xor' TRUE 'xor' TRUE by Def32,MARGREL1:36
                        .= 1 by BINARITH:15,33,MARGREL1:36;
  end;

begin :: 2's Complement Circuit Properties


::---------------------------------------------------------------------------
:: 1bit 2's Complement Circuit (Complementor + Incrementor)
::---------------------------------------------------------------------------

:: Complementor

definition
 let x,b be set;
 func CompStr(x,b) -> unsplit gate`1=arity gate`2isBoolean
   non void strict non empty ManySortedSign equals:Def33:
    1GateCircStr(<*x,b*>,xor2a);
  correctness;
end;

definition
 let x,b be set;
A1: CompStr(x,b) = 1GateCircStr(<*x,b*>,xor2a) by Def33;
 func CompCirc(x,b) ->
   strict Boolean gate`2=den Circuit of CompStr(x,b) equals
::COMPCIRC:
     1GateCircuit(x,b,xor2a);
  coherence by A1;
end;

definition
 let x,b be set;
A1: CompStr(x,b) = 1GateCircStr(<*x,b*>,xor2a) by Def33;
 func CompOutput(x,b) -> Element of InnerVertices CompStr(x,b) equals:
Def35:
   [<*x,b*>,xor2a];
  coherence by A1,FACIRC_1:47;
end;

:: Incrementor

definition
 let x,b be set;
 func IncrementStr(x,b) -> unsplit gate`1=arity gate`2isBoolean
   non void strict non empty ManySortedSign equals:
Def36:
   1GateCircStr(<*x,b*>,and2a);
  correctness;
end;

definition
 let x,b be set;
A1: IncrementStr(x,b) = 1GateCircStr(<*x,b*>,and2a) by Def36;
 func IncrementCirc(x,b) ->
   strict Boolean gate`2=den Circuit of IncrementStr(x,b) equals
      1GateCircuit(x,b,and2a);
  coherence by A1;
end;

definition
 let x,b be set;
A1: IncrementStr(x,b) = 1GateCircStr(<*x,b*>,and2a) by Def36;
 func IncrementOutput(x,b) -> Element of InnerVertices IncrementStr(x,b) equals
 :Def38:
   [<*x,b*>,and2a];
  coherence by A1,FACIRC_1:47;
end;

:: 2's-BitComplementor

definition
 let x,b be set;
 func BitCompStr(x,b) -> unsplit gate`1=arity gate`2isBoolean
   non void strict non empty ManySortedSign equals:Def39:
    CompStr(x,b) +* IncrementStr(x,b);
  correctness;
end;

definition
 let x,b be set;
A1: BitCompStr(x,b) = CompStr(x,b) +* IncrementStr(x,b) by Def39;
 func BitCompCirc(x,b) ->
   strict Boolean gate`2=den Circuit of BitCompStr(x,b) equals
      CompCirc(x,b) +* IncrementCirc(x,b);
  coherence by A1;
end;

:: Relation, carrier, InnerVertices, InputVertices and without_pair

:: Complementor

theorem Th30:
 for x,b being non pair set holds InnerVertices CompStr(x,b) is Relation
   proof
   let x,b be non pair set;
       CompStr(x,b) = 1GateCircStr(<*x,b*>,xor2a) by Def33;
   hence thesis by FACIRC_1:38;
  end;

theorem Th31:
 for x,b being non pair set holds
   x in the carrier of CompStr(x,b) &
   b in the carrier of CompStr(x,b) &
   [<*x,b*>,xor2a] in the carrier of CompStr(x,b)
  proof
   let x,b be non pair set;
   set S = CompStr(x,b);
      S = 1GateCircStr(<*x,b*>,xor2a) by Def33;
   hence thesis by FACIRC_1:43;
 end;

theorem Th32:
 for x,b being non pair set holds
  the carrier of CompStr(x,b) = {x,b} \/ {[<*x,b*>,xor2a]}
  proof
   let x,b be non pair set;
   set p = <*x,b*>;
A1:  rng p = {x,b} by FINSEQ_2:147;
     the carrier of CompStr(x,b) = the carrier of 1GateCircStr(p,xor2a) by
Def33
                    .= {x,b} \/ {[p,xor2a]} by A1,CIRCCOMB:def 6;
   hence thesis;
 end;

theorem Th33:
 for x,b being non pair set holds
   InnerVertices CompStr(x,b) = {[<*x,b*>,xor2a]}
   proof
    let x,b be non pair set;
    set p = <*x,b*>;
       InnerVertices CompStr(x,b) = InnerVertices 1GateCircStr(p,xor2a) by
Def33
                    .= {[p,xor2a]} by CIRCCOMB:49;
   hence thesis;
 end;

theorem Th34:
 for x,b being non pair set holds
   [<*x,b*>,xor2a] in InnerVertices CompStr(x,b)
  proof
   let x,b be non pair set;
      InnerVertices CompStr(x,b) = {[<*x,b*>,xor2a]} by Th33;
   hence thesis by TARSKI:def 1;
 end;

theorem Th35:
 for x,b being non pair set holds
  InputVertices CompStr(x,b) = {x,b}
  proof
    let x,b be non pair set;
    set S = CompStr(x,b);
       S = 1GateCircStr(<*x,b*>,xor2a) by Def33;
   hence thesis by FACIRC_1:40;
 end;

theorem ::ThCOMPF2':
   for x,b being non pair set holds
  x in InputVertices CompStr(x,b) &
  b in InputVertices CompStr(x,b)
  proof
   let x,b be non pair set;
      InputVertices CompStr(x,b) = {x,b} by Th35;
   hence thesis by TARSKI:def 2;
  end;

theorem
   for x,b being non pair set holds
  InputVertices CompStr(x,b) is without_pairs
  proof
   let x,b be non pair set;
      InputVertices CompStr(x,b) = {x,b} by Th35;
   hence thesis;
  end;

:: Incrementor

theorem Th38:
 for x,b being non pair set holds InnerVertices IncrementStr(x,b) is Relation
   proof
   let x,b be non pair set;
      IncrementStr(x,b) = 1GateCircStr(<*x,b*>,and2a) by Def36;
   hence thesis by FACIRC_1:38;
  end;

theorem Th39:
 for x,b being non pair set holds
   x in the carrier of IncrementStr(x,b) &
   b in the carrier of IncrementStr(x,b) &
   [<*x,b*>,and2a] in the carrier of IncrementStr(x,b)
  proof
   let x,b be non pair set;
   set S = IncrementStr(x,b);
      S = 1GateCircStr(<*x,b*>,and2a) by Def36;
   hence thesis by FACIRC_1:43;
 end;

theorem Th40:
 for x,b being non pair set holds
  the carrier of IncrementStr(x,b) = {x,b} \/ {[<*x,b*>,and2a]}
  proof
   let x,b be non pair set;
   set p = <*x,b*>;
A1:  rng p = {x,b} by FINSEQ_2:147;
      the carrier of IncrementStr(x,b) = the carrier of 1GateCircStr(p,and2a)
     by Def36
                    .= {x,b} \/ {[p,and2a]} by A1,CIRCCOMB:def 6;
   hence thesis;
 end;

theorem Th41:
 for x,b being non pair set holds
   InnerVertices IncrementStr(x,b) = {[<*x,b*>,and2a]}
   proof
    let x,b be non pair set;
    set p = <*x,b*>;
       InnerVertices IncrementStr(x,b) = InnerVertices 1GateCircStr(p,and2a)
      by Def36
                    .= {[p,and2a]} by CIRCCOMB:49;
   hence thesis;
 end;

theorem Th42:
 for x,b being non pair set holds
   [<*x,b*>,and2a] in InnerVertices IncrementStr(x,b)
  proof
   let x,b be non pair set;
      InnerVertices IncrementStr(x,b) = {[<*x,b*>,and2a]} by Th41;
   hence thesis by TARSKI:def 1;
 end;

theorem Th43:
 for x,b being non pair set holds
  InputVertices IncrementStr(x,b) = {x,b}
  proof
    let x,b be non pair set;
    set S = IncrementStr(x,b);
       S = 1GateCircStr(<*x,b*>,and2a) by Def36;
   hence thesis by FACIRC_1:40;
 end;

theorem ::ThINCF2':
   for x,b being non pair set holds
  x in InputVertices IncrementStr(x,b) &
  b in InputVertices IncrementStr(x,b)
  proof
   let x,b be non pair set;
      InputVertices IncrementStr(x,b) = {x,b} by Th43;
   hence thesis by TARSKI:def 2;
  end;

theorem
   for x,b being non pair set holds
  InputVertices IncrementStr(x,b) is without_pairs
  proof
   let x,b be non pair set;
      InputVertices IncrementStr(x,b) = {x,b} by Th43;
   hence thesis;
  end;

:: 2's-BitComplementor

theorem ::ThBITCOMPIV:
   for x,b being non pair set holds
  InnerVertices BitCompStr(x,b) is Relation
   proof
    let x,b be non pair set;
    set S1 = CompStr(x,b);
    set S2 = IncrementStr(x,b);
A1:   BitCompStr(x,b) = S1+*S2 by Def39;
       InnerVertices S1 is Relation & InnerVertices S2 is Relation
       by Th30,Th38;
   hence thesis by A1,FACIRC_1:3;
  end;

theorem Th47:
 for x,b being non pair set holds
   x in the carrier of BitCompStr(x,b) &
   b in the carrier of BitCompStr(x,b) &
   [<*x,b*>,xor2a] in the carrier of BitCompStr(x,b) &
   [<*x,b*>,and2a] in the carrier of BitCompStr(x,b)
  proof
   let x,b be non pair set;
   set p = <*x,b*>;
   set S1 = CompStr(x,b);
   set S2 = IncrementStr(x,b);
A1:   BitCompStr(x,b) = S1+*S2 by Def39;
       x in the carrier of S1 & b in the carrier of S1 &
     [p,xor2a] in the carrier of S1 &
     x in the carrier of S2 & b in the carrier of S2 &
     [p,and2a] in the carrier of S2 by Th31,Th39;
   hence thesis by A1,FACIRC_1:20;
 end;

theorem Th48:
 for x,b being non pair set holds the carrier of BitCompStr(x,b) =
   {x,b} \/ {[<*x,b*>,xor2a],[<*x,b*>,and2a]}
  proof
   let x,b be non pair set;
   set p = <*x,b*>;
   set S1 = CompStr(x,b);
   set S2 = IncrementStr(x,b);
A1: the carrier of S1 = {x,b} \/ {[p,xor2a]} &
    the carrier of S2 = {x,b} \/ {[p,and2a]} by Th32,Th40;
      the carrier of BitCompStr(x,b) = the carrier of (S1+*S2) by Def39
     .= ({x,b} \/ {[p,xor2a]}) \/ ({x,b} \/ {[p,and2a]}) by A1,CIRCCOMB:def 2
     .= {x,b} \/ ({x,b} \/ {[p,xor2a]}) \/ {[p,and2a]} by XBOOLE_1:4
     .= ({x,b} \/ {x,b}) \/ {[p,xor2a]} \/ {[p,and2a]} by XBOOLE_1:4
     .= {x,b} \/ ({[p,xor2a]} \/ {[p,and2a]}) by XBOOLE_1:4
     .= {x,b} \/ {[p,xor2a],[p,and2a]} by ENUMSET1:41;
   hence thesis;
 end;

theorem Th49:
 for x,b being non pair set holds
   InnerVertices BitCompStr(x,b) = {[<*x,b*>,xor2a],[<*x,b*>,and2a]}
   proof
    let x,b be non pair set;
    set p = <*x,b*>;
    set S1 = CompStr(x,b);
    set S2 = IncrementStr(x,b);
    set S = BitCompStr(x,b);
A1:   S = S1+*S2 by Def39;
A2:   InnerVertices S1 = {[p,xor2a]} & InnerVertices S2 = {[p,and2a]}
       by Th33,Th41;
       InnerVertices S = (InnerVertices S1) \/ InnerVertices S2 by A1,FACIRC_1:
27
                    .= {[p,xor2a], [p,and2a]} by A2,ENUMSET1:41;
   hence thesis;
  end;

theorem Th50:
 for x,b being non pair set holds
   [<*x,b*>,xor2a] in InnerVertices BitCompStr(x,b) &
   [<*x,b*>,and2a] in InnerVertices BitCompStr(x,b)
  proof
   let x,b be non pair set;
     InnerVertices BitCompStr(x,b) =
     {[<*x,b*>,xor2a],[<*x,b*>,and2a]} by Th49;
   hence thesis by TARSKI:def 2;
 end;

theorem Th51:
 for x,b being non pair set holds
  InputVertices BitCompStr(x,b) = {x,b}
  proof
    let x,b be non pair set;
    set S1 = CompStr(x,b);
    set S2 = IncrementStr(x,b);
    set S = BitCompStr(x,b);
A1:   S = S1+*S2 by Def39;
A2:   InnerVertices S1 is Relation & InnerVertices S2 is Relation
       by Th30,Th38;
    InputVertices S1 = {x,b} & InputVertices S2 = {x,b}
       by Th35,Th43;
     then InputVertices S = {x,b} \/ {x,b} by A1,A2,FACIRC_1:7
                    .= {x,b};
   hence thesis;
 end;

theorem Th52:
 for x,b being non pair set holds
  x in InputVertices BitCompStr(x,b) &
  b in InputVertices BitCompStr(x,b)
  proof
   let x,b be non pair set;
      InputVertices BitCompStr(x,b) = {x,b} by Th51;
   hence thesis by TARSKI:def 2;
  end;

theorem ::ThBITCOMPW:
   for x,b being non pair set holds
  InputVertices BitCompStr(x,b) is without_pairs
  proof
   let x,b be non pair set;
      InputVertices BitCompStr(x,b) = {x,b} by Th51;
   hence thesis;
  end;

::------------------------------------------------------------------------
:: for s being State of BitCompCirc(x,b) holds (Following s) is stable
::------------------------------------------------------------------------

theorem Th54:
 for x,b being non pair set for s being State of CompCirc(x,b) holds
  (Following s).CompOutput(x,b) = xor2a.<*s.x,s.b*> &
  (Following s).x = s.x & (Following s).b = s.b
  proof
   let x,b be non pair set;
   let s be State of CompCirc(x,b);
   set p = <*x,b*>;
   set S = CompStr(x,b);
      InputVertices S = {x,b} by Th35;
    then A1: x in InputVertices S & b in InputVertices S by TARSKI:def 2;
A2:  InnerVertices S = the OperSymbols of S by FACIRC_1:37;
A3:  dom s = the carrier of S by CIRCUIT1:4;
A4:  x in the carrier of S & b in the carrier of S by Th31;
A5:  [p,xor2a] in InnerVertices S by Th34;
   thus (Following s).CompOutput(x,b)
       = (Following s).[p,xor2a] by Def35
      .= xor2a.(s*p) by A2,A5,FACIRC_1:35
      .= xor2a.<*s.x,s.b*> by A3,A4,FINSEQ_2:145;
   thus thesis by A1,CIRCUIT2:def 5;
 end;

theorem ::ThCOMPLem22':
   for x,b being non pair set for s being State of CompCirc(x,b)
  for a1,a2 being Element of BOOLEAN st a1 = s.x & a2 = s.b holds
   (Following s).CompOutput(x,b) = 'not' a1 'xor' a2 &
   (Following s).x = a1 & (Following s).b = a2
  proof
   let x,b be non pair set;
   let s be State of CompCirc(x,b);
   let a1,a2 be Element of BOOLEAN; assume
A1:  a1 = s.x & a2 = s.b;
   thus (Following s).CompOutput(x,b)
         = xor2a.<*s.x,s.b*> by Th54
        .= 'not' a1 'xor' a2 by A1,Def14;
   thus thesis by A1,Th54;
 end;

theorem Th56:
 for x,b being non pair set for s being State of BitCompCirc(x,b) holds
  (Following s).CompOutput(x,b) = xor2a.<*s.x,s.b*> &
  (Following s).x = s.x & (Following s).b = s.b
  proof
   let x,b be non pair set;
   let s be State of BitCompCirc(x,b);
   set p = <*x,b*>;
   set S = BitCompStr(x,b);
    A1: x in InputVertices S & b in InputVertices S by Th52;
A2:  InnerVertices S = the OperSymbols of S by FACIRC_1:37;
A3:  dom s = the carrier of S by CIRCUIT1:4;
A4:  x in the carrier of S & b in the carrier of S by Th47;
A5:  [p,xor2a] in InnerVertices S by Th50;
   thus (Following s).CompOutput(x,b)
       = (Following s).[p,xor2a] by Def35
      .= xor2a.(s*p) by A2,A5,FACIRC_1:35
      .= xor2a.<*s.x,s.b*> by A3,A4,FINSEQ_2:145;
   thus thesis by A1,CIRCUIT2:def 5;
  end;

theorem Th57:
 for x,b being non pair set for s being State of BitCompCirc(x,b)
  for a1,a2 being Element of BOOLEAN st a1 = s.x & a2 = s.b holds
   (Following s).CompOutput(x,b) = 'not' a1 'xor' a2 &
   (Following s).x = a1 & (Following s).b = a2
  proof
   let x,b be non pair set;
   let s be State of BitCompCirc(x,b);
   let a1,a2 be Element of BOOLEAN; assume
A1:  a1 = s.x & a2 = s.b;
   thus (Following s).CompOutput(x,b)
         = xor2a.<*s.x,s.b*> by Th56
        .= 'not' a1 'xor' a2 by A1,Def14;
   thus thesis by A1,Th56;
 end;

theorem Th58:
 for x,b being non pair set for s being State of IncrementCirc(x,b) holds
  (Following s).IncrementOutput(x,b) = and2a.<*s.x,s.b*> &
  (Following s).x = s.x & (Following s).b = s.b
  proof
   let x,b be non pair set;
   let s be State of IncrementCirc(x,b);
   set p = <*x,b*>;
   set S = IncrementStr(x,b);
      InputVertices S = {x,b} by Th43;
    then A1: x in InputVertices S & b in InputVertices S by TARSKI:def 2;
A2:  InnerVertices S = the OperSymbols of S by FACIRC_1:37;
A3:  dom s = the carrier of S by CIRCUIT1:4;
A4:  x in the carrier of S & b in the carrier of S by Th39;
A5:  [p,and2a] in InnerVertices S by Th42;
   thus (Following s).IncrementOutput(x,b)
       = (Following s).[p,and2a] by Def38
      .= and2a.(s*p) by A2,A5,FACIRC_1:35
      .= and2a.<*s.x,s.b*> by A3,A4,FINSEQ_2:145;
   thus thesis by A1,CIRCUIT2:def 5;
 end;

theorem ::ThINCLem22':
   for x,b being non pair set for s being State of IncrementCirc(x,b)
  for a1,a2 being Element of BOOLEAN st a1 = s.x & a2 = s.b holds
   (Following s).IncrementOutput(x,b) = 'not' a1 '&' a2 &
   (Following s).x = a1 & (Following s).b = a2
  proof
   let x,b be non pair set;
   let s be State of IncrementCirc(x,b);
   let a1,a2 be Element of BOOLEAN; assume
A1:  a1 = s.x & a2 = s.b;
   thus (Following s).IncrementOutput(x,b)
         = and2a.<*s.x,s.b*> by Th58
        .= 'not' a1 '&' a2 by A1,Def2;
   thus thesis by A1,Th58;
 end;

theorem Th60:
 for x,b being non pair set for s being State of BitCompCirc(x,b) holds
  (Following s).IncrementOutput(x,b) = and2a.<*s.x,s.b*> &
  (Following s).x = s.x & (Following s).b = s.b
  proof
   let x,b be non pair set;
   let s be State of BitCompCirc(x,b);
   set p = <*x,b*>;
   set S = BitCompStr(x,b);
      InputVertices S = {x,b} by Th51;
    then A1: x in InputVertices S & b in InputVertices S by TARSKI:def 2;
A2:  InnerVertices S = the OperSymbols of S by FACIRC_1:37;
A3:  dom s = the carrier of S by CIRCUIT1:4;
A4:  x in the carrier of S & b in the carrier of S by Th47;
A5:  [p,and2a] in InnerVertices S by Th50;
   thus (Following s).IncrementOutput(x,b)
       = (Following s).[p,and2a] by Def38
      .= and2a.(s*p) by A2,A5,FACIRC_1:35
      .= and2a.<*s.x,s.b*> by A3,A4,FINSEQ_2:145;
   thus thesis by A1,CIRCUIT2:def 5;
 end;

theorem Th61:
 for x,b being non pair set for s being State of BitCompCirc(x,b)
  for a1,a2 being Element of BOOLEAN st a1 = s.x & a2 = s.b holds
   (Following s).IncrementOutput(x,b) = 'not' a1 '&' a2 &
   (Following s).x = a1 & (Following s).b = a2
  proof
   let x,b be non pair set;
   let s be State of BitCompCirc(x,b);
   let a1,a2 be Element of BOOLEAN; assume
A1:  a1 = s.x & a2 = s.b;
   thus (Following s).IncrementOutput(x,b)
         = and2a.<*s.x,s.b*> by Th60
        .= 'not' a1 '&' a2 by A1,Def2;
   thus thesis by A1,Th60;
 end;

theorem
  for x,b being non pair set for s being State of BitCompCirc(x,b) holds
  (Following s).CompOutput(x,b) = xor2a.<*s.x,s.b*> &
  (Following s).IncrementOutput(x,b) = and2a.<*s.x,s.b*> &
  (Following s).x = s.x & (Following s).b = s.b
 by Th56,Th60;

theorem ::ThBITCOMPLem22:
   for x,b being non pair set for s being State of BitCompCirc(x,b)
  for a1,a2 being Element of BOOLEAN st a1 = s.x & a2 = s.b holds
  (Following s).CompOutput(x,b) = 'not' a1 'xor' a2 &
  (Following s).IncrementOutput(x,b) = 'not' a1 '&' a2 &
  (Following s).x = a1 & (Following s).b = a2
 by Th57,Th61;

theorem ::ThCLA2F3:
   for x,b being non pair set for s being State of BitCompCirc(x,b) holds
   (Following s) is stable
  proof
   let x,b be non pair set;
    set p = <*x,b*>;
    set S = BitCompStr(x,b);
   let s be State of BitCompCirc(x,b);
   set s1 = Following s, s2 = Following s1;
A1:  dom s1 = the carrier of S & dom s2 = the carrier of S by CIRCUIT1:4;
A2:  the carrier of S = {x,b} \/ {[p,xor2a],[p,and2a]} by Th48;
      now let a be set; assume a in the carrier of S;
      then a in {x,b} or a in {[p,xor2a],[p,and2a]} by A2,XBOOLE_0:def 2;
then A3:    a = x or a = b or a = [p,xor2a] or a = [p,and2a] by TARSKI:def 2;
A4:    s2.x = s1.x & s1.x = s.x & s2.b = s1.b & s1.b = s.b by Th56;
A5:   s1.[p,xor2a] = s1.CompOutput(x,b) by Def35
                  .= xor2a.<*s.x, s.b*> by Th56;
A6:   s1.[p,and2a] = s1.IncrementOutput(x,b) by Def38
                  .= and2a.<*s.x, s.b*> by Th60;
A7:   s2.[p,xor2a] = s2.CompOutput(x,b) by Def35
                  .= xor2a.<*s1.x, s1.b*> by Th56;
        s2.[p,and2a] = s2.IncrementOutput(x,b) by Def38
                  .= and2a.<*s1.x, s1.b*> by Th60;
     hence s2.a = s1.a by A3,A4,A5,A6,A7;
    end;
   hence Following s = Following Following s by A1,FUNCT_1:9;
  end;


Back to top