Copyright (c) 1996 Association of Mizar Users
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;