begin
:: deftheorem Def1 defines pair FACIRC_1:def 1 :
for IT being set holds
( IT is pair iff ex x, y being set st IT = [x,y] );
:: deftheorem Def2 defines with_pair FACIRC_1:def 2 :
for IT being set holds
( IT is with_pair iff ex x being pair set st x in IT );
:: deftheorem defines nonpair-yielding FACIRC_1:def 3 :
for IT being Function holds
( IT is nonpair-yielding iff for x being set st x in dom IT holds
not IT . x is pair );
theorem Th1:
theorem Th2:
theorem
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem
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
func 'xor' -> Function of
(2 -tuples_on BOOLEAN),
BOOLEAN means :
Def4:
for
x,
y being
Element of
BOOLEAN holds
it . <*x,y*> = x 'xor' y;
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;
func 'or' -> Function of
(2 -tuples_on BOOLEAN),
BOOLEAN means :
Def5:
for
x,
y being
Element of
BOOLEAN holds
it . <*x,y*> = x 'or' y;
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;
func '&' -> Function of
(2 -tuples_on BOOLEAN),
BOOLEAN means :
Def6:
for
x,
y being
Element of
BOOLEAN holds
it . <*x,y*> = x '&' y;
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;
:: deftheorem Def4 defines 'xor' FACIRC_1:def 4 :
for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds
( b1 = 'xor' iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'xor' y );
:: deftheorem Def5 defines 'or' FACIRC_1:def 5 :
for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds
( b1 = 'or' iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'or' y );
:: deftheorem Def6 defines '&' FACIRC_1:def 6 :
for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds
( b1 = '&' iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x '&' y );
definition
func or3 -> Function of
(3 -tuples_on BOOLEAN),
BOOLEAN means :
Def7:
for
x,
y,
z being
Element of
BOOLEAN holds
it . <*x,y,z*> = (x 'or' y) 'or' z;
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;
:: deftheorem Def7 defines or3 FACIRC_1:def 7 :
for b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN holds
( b1 = or3 iff for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x 'or' y) 'or' z );
begin
theorem Th10:
:: deftheorem Def8 defines Following FACIRC_1:def 8 :
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for n being Nat
for b5 being State of A holds
( b5 = Following (s,n) iff ex f being Function of NAT,(product the Sorts of A) st
( b5 = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) ) );
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
:: deftheorem Def9 defines is_stable_at FACIRC_1:def 9 :
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for x being set holds
( s is_stable_at x iff for n being Nat holds (Following (s,n)) . x = s . x );
theorem
theorem
theorem Th19:
begin
theorem Th20:
theorem Th21:
theorem
theorem
theorem
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem
theorem Th37:
begin
theorem Th38:
theorem
theorem Th40:
theorem Th41:
theorem Th42:
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
theorem
theorem Th47:
definition
let x,
y be
set ;
let f be
Function of
(2 -tuples_on BOOLEAN),
BOOLEAN;
func 1GateCircuit (
x,
y,
f)
-> strict gate`2=den Boolean Circuit of
1GateCircStr (
<*x,y*>,
f)
equals
1GateCircuit (
<*x,y*>,
f);
coherence
1GateCircuit (<*x,y*>,f) is strict gate`2=den Boolean Circuit of 1GateCircStr (<*x,y*>,f)
by CIRCCOMB:69;
end;
:: deftheorem defines 1GateCircuit FACIRC_1:def 10 :
for x, y being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds 1GateCircuit (x,y,f) = 1GateCircuit (<*x,y*>,f);
theorem Th48:
theorem Th49:
theorem
theorem
definition
let x,
y,
z be
set ;
let f be
Function of
(3 -tuples_on BOOLEAN),
BOOLEAN;
func 1GateCircuit (
x,
y,
z,
f)
-> strict gate`2=den Boolean Circuit of
1GateCircStr (
<*x,y,z*>,
f)
equals
1GateCircuit (
<*x,y,z*>,
f);
coherence
1GateCircuit (<*x,y,z*>,f) is strict gate`2=den Boolean Circuit of 1GateCircStr (<*x,y,z*>,f)
by CIRCCOMB:69;
end;
:: deftheorem defines 1GateCircuit FACIRC_1:def 11 :
for x, y, z being set
for f being Function of (3 -tuples_on BOOLEAN),BOOLEAN holds 1GateCircuit (x,y,z,f) = 1GateCircuit (<*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 Th53:
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;
theorem
begin
definition
let x,
y,
c be
set ;
let f be
Function of
(2 -tuples_on BOOLEAN),
BOOLEAN;
func 2GatesCircStr (
x,
y,
c,
f)
-> non
empty non
void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals
(1GateCircStr (<*x,y*>,f)) +* (1GateCircStr (<*[<*x,y*>,f],c*>,f));
correctness
coherence
(1GateCircStr (<*x,y*>,f)) +* (1GateCircStr (<*[<*x,y*>,f],c*>,f)) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;
;
end;
:: 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 Th58:
theorem Th59:
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 Th63:
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
definition
let x,
y,
c be
set ;
func BitAdderOutput (
x,
y,
c)
-> Element of
InnerVertices (2GatesCircStr (x,y,c,'xor')) equals
2GatesCircOutput (
x,
y,
c,
'xor');
coherence
2GatesCircOutput (x,y,c,'xor') is Element of InnerVertices (2GatesCircStr (x,y,c,'xor'))
;
end;
:: deftheorem defines BitAdderOutput FACIRC_1:def 15 :
for x, y, c being set holds BitAdderOutput (x,y,c) = 2GatesCircOutput (x,y,c,'xor');
definition
let x,
y,
c be
set ;
func BitAdderCirc (
x,
y,
c)
-> strict gate`2=den Boolean Circuit of
2GatesCircStr (
x,
y,
c,
'xor')
equals
2GatesCircuit (
x,
y,
c,
'xor');
coherence
2GatesCircuit (x,y,c,'xor') is strict gate`2=den Boolean Circuit of 2GatesCircStr (x,y,c,'xor')
;
end;
:: deftheorem defines BitAdderCirc FACIRC_1:def 16 :
for x, y, c being set holds BitAdderCirc (x,y,c) = 2GatesCircuit (x,y,c,'xor');
definition
let x,
y,
c be
set ;
func MajorityIStr (
x,
y,
c)
-> non
empty non
void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals
((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&'))) +* (1GateCircStr (<*c,x*>,'&'));
correctness
coherence
((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&'))) +* (1GateCircStr (<*c,x*>,'&')) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;
;
end;
:: 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,'&'));
theorem Th67:
theorem Th68:
theorem
theorem
theorem
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 Th72:
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 Th74:
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
theorem
theorem
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
theorem
theorem
theorem
theorem Th84:
definition
let x,
y,
c be
set ;
func BitAdderWithOverflowStr (
x,
y,
c)
-> non
empty non
void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals
(2GatesCircStr (x,y,c,'xor')) +* (MajorityStr (x,y,c));
coherence
(2GatesCircStr (x,y,c,'xor')) +* (MajorityStr (x,y,c)) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
;
end;
:: deftheorem defines BitAdderWithOverflowStr FACIRC_1:def 22 :
for x, y, c being set holds BitAdderWithOverflowStr (x,y,c) = (2GatesCircStr (x,y,c,'xor')) +* (MajorityStr (x,y,c));
theorem Th85:
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
definition
let x,
y,
c be
set ;
func BitAdderWithOverflowCirc (
x,
y,
c)
-> strict gate`2=den Boolean Circuit of
BitAdderWithOverflowStr (
x,
y,
c)
equals
(BitAdderCirc (x,y,c)) +* (MajorityCirc (x,y,c));
coherence
(BitAdderCirc (x,y,c)) +* (MajorityCirc (x,y,c)) is strict gate`2=den Boolean Circuit of BitAdderWithOverflowStr (x,y,c)
;
end;
:: deftheorem defines BitAdderWithOverflowCirc FACIRC_1:def 23 :
for x, y, c being set holds BitAdderWithOverflowCirc (x,y,c) = (BitAdderCirc (x,y,c)) +* (MajorityCirc (x,y,c));
theorem
theorem
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) )
theorem