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