begin
begin
scheme
2AryBooleDef{
F1(
set ,
set )
-> Element of
BOOLEAN } :
( ex
f being
Function of
(2 -tuples_on BOOLEAN),
BOOLEAN st
for
x,
y being
Element of
BOOLEAN holds
f . <*x,y*> = F1(
x,
y) & ( for
f1,
f2 being
Function of
(2 -tuples_on BOOLEAN),
BOOLEAN st ( for
x,
y being
Element of
BOOLEAN holds
f1 . <*x,y*> = F1(
x,
y) ) & ( for
x,
y being
Element of
BOOLEAN holds
f2 . <*x,y*> = F1(
x,
y) ) holds
f1 = f2 ) )
scheme
3AryBooleUniq{
F1(
set ,
set ,
set )
-> Element of
BOOLEAN } :
for
f1,
f2 being
Function of
(3 -tuples_on BOOLEAN),
BOOLEAN st ( for
x,
y,
z being
Element of
BOOLEAN holds
f1 . <*x,y,z*> = F1(
x,
y,
z) ) & ( for
x,
y,
z being
Element of
BOOLEAN holds
f2 . <*x,y,z*> = F1(
x,
y,
z) ) holds
f1 = f2
scheme
3AryBooleDef{
F1(
set ,
set ,
set )
-> Element of
BOOLEAN } :
( ex
f being
Function of
(3 -tuples_on BOOLEAN),
BOOLEAN st
for
x,
y,
z being
Element of
BOOLEAN holds
f . <*x,y,z*> = F1(
x,
y,
z) & ( for
f1,
f2 being
Function of
(3 -tuples_on BOOLEAN),
BOOLEAN st ( for
x,
y,
z being
Element of
BOOLEAN holds
f1 . <*x,y,z*> = F1(
x,
y,
z) ) & ( for
x,
y,
z being
Element of
BOOLEAN holds
f2 . <*x,y,z*> = F1(
x,
y,
z) ) holds
f1 = f2 ) )
definition
correctness
existence
ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'xor' y;
uniqueness
for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'xor' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x 'xor' y ) holds
b1 = b2;
correctness
existence
ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'or' y;
uniqueness
for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'or' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x 'or' y ) holds
b1 = b2;
correctness
existence
ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x '&' y;
uniqueness
for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x '&' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x '&' y ) holds
b1 = b2;
end;
definition
correctness
existence
ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x 'or' y) 'or' z;
uniqueness
for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x 'or' y) 'or' z ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = (x 'or' y) 'or' z ) holds
b1 = b2;
end;
begin
begin
begin
theorem Th43:
for
x,
y,
f being
set holds
(
x in the
carrier of
(1GateCircStr (<*x,y*>,f)) &
y in the
carrier of
(1GateCircStr (<*x,y*>,f)) &
[<*x,y*>,f] in the
carrier of
(1GateCircStr (<*x,y*>,f)) )
theorem Th44:
for
x,
y,
z,
f being
set holds
(
x in the
carrier of
(1GateCircStr (<*x,y,z*>,f)) &
y in the
carrier of
(1GateCircStr (<*x,y,z*>,f)) &
z in the
carrier of
(1GateCircStr (<*x,y,z*>,f)) )
theorem Th52:
for
x,
y,
z being
set for
X being non
empty finite set for
f being
Function of
(3 -tuples_on X),
X for
s being
State of
(1GateCircuit (<*x,y,z*>,f)) holds
(
(Following s) . [<*x,y,z*>,f] = f . <*(s . x),(s . y),(s . z)*> &
(Following s) . x = s . x &
(Following s) . y = s . y &
(Following s) . z = s . z )
theorem
for
x,
y,
z being
set for
f being
Function of
(3 -tuples_on BOOLEAN),
BOOLEAN for
s being
State of
(1GateCircuit (x,y,z,f)) holds
(
(Following s) . [<*x,y,z*>,f] = f . <*(s . x),(s . y),(s . z)*> &
(Following s) . x = s . x &
(Following s) . y = s . y &
(Following s) . z = s . z )
by Th52;
begin
::
deftheorem defines
2GatesCircStr FACIRC_1:def 12 :
for x, y, c being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds 2GatesCircStr (x,y,c,f) = (1GateCircStr (<*x,y*>,f)) +* (1GateCircStr (<*[<*x,y*>,f],c*>,f));
definition
let x,
y,
c be
set ;
let f be
Function of
(2 -tuples_on BOOLEAN),
BOOLEAN;
func 2GatesCircOutput (
x,
y,
c,
f)
-> Element of
InnerVertices (2GatesCircStr (x,y,c,f)) equals
[<*[<*x,y*>,f],c*>,f];
coherence
[<*[<*x,y*>,f],c*>,f] is Element of InnerVertices (2GatesCircStr (x,y,c,f))
correctness
;
end;
::
deftheorem defines
2GatesCircOutput FACIRC_1:def 13 :
for x, y, c being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds 2GatesCircOutput (x,y,c,f) = [<*[<*x,y*>,f],c*>,f];
theorem Th56:
for
x,
y,
c being
set for
f being
Function of
(2 -tuples_on BOOLEAN),
BOOLEAN holds
InnerVertices (2GatesCircStr (x,y,c,f)) = {[<*x,y*>,f],(2GatesCircOutput (x,y,c,f))}
theorem Th57:
for
c,
x,
y being
set for
f being
Function of
(2 -tuples_on BOOLEAN),
BOOLEAN st
c <> [<*x,y*>,f] holds
InputVertices (2GatesCircStr (x,y,c,f)) = {x,y,c}
definition
let x,
y,
c be
set ;
let f be
Function of
(2 -tuples_on BOOLEAN),
BOOLEAN;
func 2GatesCircuit (
x,
y,
c,
f)
-> strict gate`2=den Boolean Circuit of
2GatesCircStr (
x,
y,
c,
f)
equals
(1GateCircuit (x,y,f)) +* (1GateCircuit ([<*x,y*>,f],c,f));
coherence
(1GateCircuit (x,y,f)) +* (1GateCircuit ([<*x,y*>,f],c,f)) is strict gate`2=den Boolean Circuit of 2GatesCircStr (x,y,c,f)
;
end;
::
deftheorem defines
2GatesCircuit FACIRC_1:def 14 :
for x, y, c being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds 2GatesCircuit (x,y,c,f) = (1GateCircuit (x,y,f)) +* (1GateCircuit ([<*x,y*>,f],c,f));
theorem Th60:
for
x,
y,
c being
set for
f being
Function of
(2 -tuples_on BOOLEAN),
BOOLEAN holds
(
x in the
carrier of
(2GatesCircStr (x,y,c,f)) &
y in the
carrier of
(2GatesCircStr (x,y,c,f)) &
c in the
carrier of
(2GatesCircStr (x,y,c,f)) )
theorem
for
x,
y,
c being
set for
f being
Function of
(2 -tuples_on BOOLEAN),
BOOLEAN holds
(
[<*x,y*>,f] in the
carrier of
(2GatesCircStr (x,y,c,f)) &
[<*[<*x,y*>,f],c*>,f] in the
carrier of
(2GatesCircStr (x,y,c,f)) )
Lm1:
for c, x, y being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN
for s being State of (2GatesCircuit (x,y,c,f)) st c <> [<*x,y*>,f] holds
( (Following s) . (2GatesCircOutput (x,y,c,f)) = f . <*(s . [<*x,y*>,f]),(s . c)*> & (Following s) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following s) . x = s . x & (Following s) . y = s . y & (Following s) . c = s . c )
theorem Th62:
for
c,
x,
y being
set for
f being
Function of
(2 -tuples_on BOOLEAN),
BOOLEAN for
s being
State of
(2GatesCircuit (x,y,c,f)) st
c <> [<*x,y*>,f] holds
(
(Following (s,2)) . (2GatesCircOutput (x,y,c,f)) = f . <*(f . <*(s . x),(s . y)*>),(s . c)*> &
(Following (s,2)) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> &
(Following (s,2)) . x = s . x &
(Following (s,2)) . y = s . y &
(Following (s,2)) . c = s . c )
theorem Th64:
for
c,
x,
y being
set st
c <> [<*x,y*>,'xor'] holds
for
s being
State of
(2GatesCircuit (x,y,c,'xor')) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . x &
a2 = s . y &
a3 = s . c holds
(Following (s,2)) . (2GatesCircOutput (x,y,c,'xor')) = (a1 'xor' a2) 'xor' a3
theorem
for
c,
x,
y being
set st
c <> [<*x,y*>,'or'] holds
for
s being
State of
(2GatesCircuit (x,y,c,'or')) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . x &
a2 = s . y &
a3 = s . c holds
(Following (s,2)) . (2GatesCircOutput (x,y,c,'or')) = (a1 'or' a2) 'or' a3
theorem
for
c,
x,
y being
set st
c <> [<*x,y*>,'&'] holds
for
s being
State of
(2GatesCircuit (x,y,c,'&')) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . x &
a2 = s . y &
a3 = s . c holds
(Following (s,2)) . (2GatesCircOutput (x,y,c,'&')) = (a1 '&' a2) '&' a3
begin
::
deftheorem defines
MajorityIStr FACIRC_1:def 17 :
for x, y, c being set holds MajorityIStr (x,y,c) = ((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&'))) +* (1GateCircStr (<*c,x*>,'&'));
definition
let x,
y,
c be
set ;
func MajorityStr (
x,
y,
c)
-> non
empty non
void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals
(MajorityIStr (x,y,c)) +* (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3));
correctness
coherence
(MajorityIStr (x,y,c)) +* (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;
;
end;
::
deftheorem defines
MajorityStr FACIRC_1:def 18 :
for x, y, c being set holds MajorityStr (x,y,c) = (MajorityIStr (x,y,c)) +* (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3));
definition
let x,
y,
c be
set ;
func MajorityICirc (
x,
y,
c)
-> strict gate`2=den Boolean Circuit of
MajorityIStr (
x,
y,
c)
equals
((1GateCircuit (x,y,'&')) +* (1GateCircuit (y,c,'&'))) +* (1GateCircuit (c,x,'&'));
coherence
((1GateCircuit (x,y,'&')) +* (1GateCircuit (y,c,'&'))) +* (1GateCircuit (c,x,'&')) is strict gate`2=den Boolean Circuit of MajorityIStr (x,y,c)
;
end;
::
deftheorem defines
MajorityICirc FACIRC_1:def 19 :
for x, y, c being set holds MajorityICirc (x,y,c) = ((1GateCircuit (x,y,'&')) +* (1GateCircuit (y,c,'&'))) +* (1GateCircuit (c,x,'&'));
definition
let x,
y,
c be
set ;
func MajorityOutput (
x,
y,
c)
-> Element of
InnerVertices (MajorityStr (x,y,c)) equals
[<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3];
coherence
[<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3] is Element of InnerVertices (MajorityStr (x,y,c))
correctness
;
end;
::
deftheorem defines
MajorityOutput FACIRC_1:def 20 :
for x, y, c being set holds MajorityOutput (x,y,c) = [<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3];
definition
let x,
y,
c be
set ;
func MajorityCirc (
x,
y,
c)
-> strict gate`2=den Boolean Circuit of
MajorityStr (
x,
y,
c)
equals
(MajorityICirc (x,y,c)) +* (1GateCircuit ([<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&'],or3));
coherence
(MajorityICirc (x,y,c)) +* (1GateCircuit ([<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&'],or3)) is strict gate`2=den Boolean Circuit of MajorityStr (x,y,c)
;
end;
::
deftheorem defines
MajorityCirc FACIRC_1:def 21 :
for x, y, c being set holds MajorityCirc (x,y,c) = (MajorityICirc (x,y,c)) +* (1GateCircuit ([<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&'],or3));
theorem Th73:
for
x,
y,
c being
set holds
(
[<*x,y*>,'&'] in InnerVertices (MajorityStr (x,y,c)) &
[<*y,c*>,'&'] in InnerVertices (MajorityStr (x,y,c)) &
[<*c,x*>,'&'] in InnerVertices (MajorityStr (x,y,c)) )
theorem Th75:
for
x,
y,
c being non
pair set holds
(
InputVertices (MajorityStr (x,y,c)) = {x,y,c} &
InnerVertices (MajorityStr (x,y,c)) = {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} \/ {(MajorityOutput (x,y,c))} )
Lm2:
for x, y, c being non pair set
for s being State of (MajorityCirc (x,y,c))
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
( (Following s) . [<*x,y*>,'&'] = a1 '&' a2 & (Following s) . [<*y,c*>,'&'] = a2 '&' a3 & (Following s) . [<*c,x*>,'&'] = a3 '&' a1 )
theorem Th79:
for
x,
y,
c being non
pair set for
s being
State of
(MajorityCirc (x,y,c)) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . [<*x,y*>,'&'] &
a2 = s . [<*y,c*>,'&'] &
a3 = s . [<*c,x*>,'&'] holds
(Following s) . (MajorityOutput (x,y,c)) = (a1 'or' a2) 'or' a3
Lm3:
for x, y, c being non pair set
for s being State of (MajorityCirc (x,y,c))
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
( (Following (s,2)) . (MajorityOutput (x,y,c)) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1) & (Following (s,2)) . [<*x,y*>,'&'] = a1 '&' a2 & (Following (s,2)) . [<*y,c*>,'&'] = a2 '&' a3 & (Following (s,2)) . [<*c,x*>,'&'] = a3 '&' a1 )
theorem
for
x,
y,
c being non
pair set holds
InnerVertices (BitAdderWithOverflowStr (x,y,c)) = ({[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} \/ {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']}) \/ {(MajorityOutput (x,y,c))}
theorem
for
x,
y,
c being
set holds
(
BitAdderOutput (
x,
y,
c)
in InnerVertices (BitAdderWithOverflowStr (x,y,c)) &
MajorityOutput (
x,
y,
c)
in InnerVertices (BitAdderWithOverflowStr (x,y,c)) )
by Th21;
theorem
for
x,
y,
c being non
pair set for
s being
State of
(BitAdderWithOverflowCirc (x,y,c)) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . x &
a2 = s . y &
a3 = s . c holds
(
(Following (s,2)) . (BitAdderOutput (x,y,c)) = (a1 'xor' a2) 'xor' a3 &
(Following (s,2)) . (MajorityOutput (x,y,c)) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1) )